Operations Research

Motivation

A network of resistors solves an optimization problem. Nobody tells the electrons what to do; each one moves under a purely local rule, and the current distribution that emerges minimizes energy dissipation over all distributions satisfying Kirchhoff's node law. Add a wire and the network can only become easier to traverse. This is the encouraging case, and Chapter 4 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) opens with it.

Road traffic is the discouraging case. Drivers also follow a local rule — take the fastest route — and the pattern that emerges is again characterized by an optimization problem, but not the one anyone wants solved. Braess's paradox is the sharp form of the discrepancy: in a small road network carrying six cars per unit time, every route takes 83 time units at equilibrium; open an extra road, and at the new equilibrium every route takes 92. Building road capacity made everyone slower. The difference from the electrical case is that a driver's choice imposes a delay on everyone else sharing the road and the driver does not pay for it, and correcting that — pricing the externality — is how a decentralized rule can be made to produce good global behaviour. That idea recurs in Chapters 7 and 8 of the book as the basis of Internet congestion control.

Setting

The network is a set $\mathcal{J}$ of $J$ directed links. A route $r$ is a subset of links, and $\mathcal{R}$ is the set of $R$ routes under consideration — not necessarily all physically possible ones. The link-route incidence matrix $A$ has $A_{jr}=1$ when $j \in r$ and $A_{jr}=0$ otherwise. Writing $x_r$ for the flow on route $r$, the flow on link $j$ is

Each link has a delay function $D_j(y_j)$, continuous and increasing in the flow on that link, and the delay along a route is the sum of the delays of its links, $\sum_j D_j(y_j)A_{jr}$. Drivers care only about getting from origin to destination: $\mathcal{S}$ is the set of source–destination pairs, each route $r$ serves exactly one of them, written $s(r)$, and the flow requirement between pair $\sigma$ is $f_\sigma$.

A routing pattern is stable when no driver has an incentive to switch. Definition 4.2 makes this precise: a Wardrop equilibrium is a feasible vector of route flows $x$ such that

Every route actually carrying traffic is a shortest route, in delay, for the traffic it carries.

Formalization targets

Goal — Theorem 4.3, a Wardrop equilibrium exists

The goal asserts existence only, for an arbitrary network, arbitrary route set and arbitrary continuous increasing delay functions. It fixes no uniqueness claim, because the equilibrium flows need not be unique even though the link loads are, and no efficiency claim, because Braess's paradox is precisely the statement that the equilibrium is not efficient.

Supporting levels

Kirchhoff's node law as the equations satisfied by the expected reward in the random-walk game of section 4.1; the two Braess networks of Figures 4.4a and 4.4b, with their equilibrium delays $83$ and $92$; convexity of $\int_0^{y}D(u)\,du$ for increasing $D$; the optimization characterization that makes the goal reachable — a minimizer of $\sum_j\int_0^{y_j}D_j(u)\,du$ over the feasible flows is a Wardrop equilibrium; and the exact externality decomposition of the queueing network of section 4.3.1.

Significance

The result itself. Theorem 4.3 is what makes the Wardrop equilibrium a usable object: a traffic model that could fail to have an equilibrium would be describing nothing. Its proof does more than establish existence — it identifies the equilibrium as the solution of a specific convex program, minimizing $\sum_j\int_0^{y_j}D_j(u)\,du$. That function is not the total delay $\sum_j y_jD_j(y_j)$, and the gap between the two is exactly Braess's paradox: selfish routing optimizes the wrong objective. Once the two objectives are written side by side, the fix is readable off them, and it is the fix used in practice — a toll on link $j$ equal to $y_jD_j'(y_j)$, the marginal delay a driver imposes on everyone else, makes the selfish objective coincide with the social one. Section 4.3 then carries the same accounting into queueing and loss networks, where the derivative of the mean cost splits into a term for the delay a customer suffers and a term for the knock-on cost it inflicts.

Formalizing it. Nothing here is open; Wardrop stated the principle in 1952 and Beckmann, McGuire and Winsten gave the optimization formulation in 1956. What the mission produces is a machine-checked model of selfish routing — incidence matrix, link flows, delay functions, the equilibrium condition — and a formal record of Braess's paradox as a concrete pair of networks rather than a story. Mathlib has no traffic or congestion-game theory.

Difficulty

Existence is not a fixed-point argument in the obvious variable: the best-response map of the routing game is not continuous, since a small change in flows can flip which route is shortest and move all the traffic. The book's route is to replace the equilibrium condition by the stationarity conditions of a convex program on a compact feasible set, where existence is routine and the content is the translation. The translation is where the care is needed, and it is stated here as a separate milestone: the first-order conditions say the Lagrange multiplier $\lambda_{s(r)}$ equals the route delay on routes carrying traffic and is a lower bound on the others, which is Definition 4.2 restated.

The subtlety worth naming in advance is that "increasing" is doing real work in two different places. It makes $\int_0^{y}D(u)\,du$ convex, which is what makes the program tractable; and it is what makes each $D_j(y_j)$ interpretable as a price. Neither convexity of $D_j$ itself nor strict monotonicity is needed, and assuming them would be assuming more than the book does.

Formalization scope

Links, routes and source–destination pairs are indexed by finite types. The incidence matrix is real-valued with entries constrained to be $0$ or $1$, matching the book's definition in this chapter (unlike Chapter 3, which allows general non-negative integers). The map from routes to source–destination pairs is given as a function $s$ rather than as the matrix $H$, which is exactly the book's statement that each column of $H$ sums to $1$.

Delay functions are total functions $\mathbb{R}\to\mathbb{R}$, continuous and monotone. This excludes the vertical asymptote that Figure 4.5 permits — a link with a finite capacity at which delay blows up — and that restriction is recorded here rather than left implicit. The equilibrium condition is stated as the inequality "$\text{delay on } r \le \text{delay on } r'$ for every $r'$ serving the same pair", which is Definition 4.2 with the minimum written out; the two are equivalent because $r$ itself serves $s(r)$, and the inequality form avoids having to produce a minimum over a possibly empty set.

The goal is not vacuous: the feasibility hypotheses ($f_\sigma\ge0$, and each source–destination pair served by at least one route) are exactly what makes the feasible set non-empty, and without them the existence claim would be false rather than trivial.

Contributions welcome beyond the listed items: uniqueness of the equilibrium link loads $y$; the marginal-cost toll that aligns the selfish and social optima; Rayleigh monotonicity (Exercise 4.3, that effective resistance does not decrease when a resistance is increased); the price of anarchy for affine delays; and Theorem 4.6 on the derivatives of the loss-network rate of return with respect to offered traffic and capacity.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 4 (pp. 85–107); Definition 4.2, Theorem 4.3, sections 4.1–4.3. DOI 10.1017/cbo9781139565363
• J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers 1 (1952), 325–362. DOI 10.1680/ipeds.1952.11259
• M. Beckmann, C. B. McGuire and C. B. Winsten, Studies in the Economics of Transportation, Yale University Press, 1956.
• D. Braess, Über ein Paradoxon aus der Verkehrsplanung, Unternehmensforschung 12 (1968), 258–268. DOI 10.1007/BF01918335
• Peter Doyle and J. Laurie Snell, Random Walks and Electric Networks, Mathematical Association of America, 1984. arXiv:math/0001057
• R. G. Gallager, A minimum delay routing algorithm using distributed computation, IEEE Transactions on Communications 25 (1977), 73–85. DOI 10.1109/TCOM.1977.1093711

Motivation

A queueing network is a collection of service stations through which customers — jobs, packets, telephone calls, patients — move one at a time. The state of such a network is a vector of occupancy counts, one per station, and the number of states grows exponentially in the number of stations, so solving the equilibrium equations directly is hopeless for any network worth modelling. The product form is what rescues the subject: for a large and identifiable class of networks the equilibrium distribution factorizes into one term per station, as if the stations were independent, and a network of $J$ stations costs $J$ one-dimensional calculations instead of one exponentially large one.

Chapter 2 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) establishes this for migration processes, the Markov model in which individuals move between colonies one at a time at a rate that factorizes as $\lambda_{jk}\varphi_j(n_j)$: a part depending only on the two colonies and a part depending only on the occupancy of the source. The class covers single-server and $s$-server queues, infinite-server queues, and networks of them, open or closed.

Setting

There are $J$ colonies, and a state is a vector $n = (n_1,\dots,n_J)$ of non-negative integers, $n_j$ being the number of individuals in colony $j$. Three operators move one individual:

An open migration process is the Markov process on $\mathbb{Z}_+^J$ with transition rates

where $\varphi_j(0)=0$: nothing leaves an empty colony. Immigration into colony $k$ is Poisson of rate $\nu_k$. Taking $\mu\equiv 0$ and $\nu\equiv 0$ and restricting to states of a fixed total $\sum_j n_j = N$ gives a closed migration process. Setting $\varphi_j(n)=\min(n,s)$ models an $s$-server queue at colony $j$; $\varphi_j(n)=n$ models individuals moving independently.

The traffic equations define $(\alpha_j)$ from the rates. In the open case they are

and in the closed case $\alpha_j\sum_k \lambda_{jk}=\sum_k \alpha_k\lambda_{kj}$ with $\alpha_j>0$ and $\sum_j\alpha_j=1$. Finally set

Formalization targets

Goal — Theorem 2.8, the product form of an open migration process

If $g_1,\dots,g_J<\infty$ then

is an equilibrium distribution: it satisfies the equilibrium equations for the open migration rates, and it sums to one over $\mathbb{Z}_+^J$. Both halves are asserted, because the first alone is satisfied by every positive multiple of $\pi$ and the second is what makes the convergence hypothesis $g_j<\infty$ do work.

Supporting levels

The closed-network product form of Theorem 2.4; the two families of partial balance equations (2.3) and (2.4) that the proof reduces to; Theorem 2.9, that the time reversal of a stationary open migration process is again an open migration process with rates $\lambda'_{jk}=\alpha_k\lambda_{kj}/\alpha_j$, $\mu'_j=\nu_j/\alpha_j$ and $\nu'_k=\alpha_k\mu_k$; the single M/M/1 queue that the chapter starts from; the cycle identity (2.6) behind Little's law; and the traffic equations of Kendall's family-size process, an open migration process with infinitely many colonies.

Significance

The result itself. Theorem 2.8 says that at a fixed time the occupancies $n_1,\dots,n_J$ of an open migration network are independent, each distributed as if its colony were fed by a Poisson stream of rate $\alpha_j\lambda_j$ — even though the actual arrival stream into a colony is in general not Poisson, and the occupancies are emphatically not independent as processes. That gap between the one-time-marginal and the process is the reason the theorem is useful and the reason it is easy to misapply. Everything downstream in the book rests on it: the loss networks of Chapter 3 are the truncation of a product-form process to a capacity set, and the flow-level models of Chapter 8 ask when a product form survives a bandwidth-sharing policy. Theorem 2.9 supplies the reversibility argument from which Burke's theorem and the Poisson character of the exit streams follow.

Formalizing it. The mathematics is classical — Jackson (1957), Whittle (1968), Kelly (1979) — and none of it is open. What the mission produces is a machine-checked model of a queueing network: the migration operators, the rate matrix, the traffic equations and the product form, in a form later missions in this series import rather than restate. Mathlib has no queueing theory and no theory of continuous-time Markov chains on a countable state space, so this is the first such development. It builds on the DetailedBalance / FullBalance layer published in mission I.

Difficulty

An open migration process is not reversible — the detailed balance equations fail, as Figure 2.5 of the book shows with an arrival stream of geometrically sized bursts — so the method of Chapter 1 does not apply and the equilibrium equations must be met head on. The content of the proof is that they split: a separate balance holds for each colony $j$ (rate of individuals leaving colony $j$ equals rate arriving into it) and one more across the boundary with the outside world, and each of those is equivalent to a traffic equation. Finding that split is the step, and it is why the partial balance equations are milestones in their own right.

The formal obstacle is different and worth naming. The equilibrium equation at a state $n$ sums over the states that can jump into $n$, and the naive transcription $\sum_{j,k}\pi(T^{jk}n)q(T^{jk}n,n)$ silently assumes $T^{jk}n$ is a state, which fails when $n_j=0$. Over $\mathbb{Z}_+^J$ such a term must be dropped, and a formalization that keeps it — with $n_j-1$ read as truncated subtraction — states something false.

Formalization scope

The state space is Fin J → ℕ, a function from a finite index type of colonies to occupancy counts, with J finite; no irreducibility is assumed, since none of the statements below need it. Rates are real-valued and the whole rate matrix is a single function of two states, assembled as a sum of indicator terms over the possible transitions, so the equilibrium equations can be stated as the FullBalance predicate of mission I, with unconditional sums over the countable state space. This is what avoids the trap above: a sum over actual states never includes a would-be-negative one, and any spurious coincidence of operators at a boundary carries a $\varphi_j(0)=0$ factor and contributes nothing.

Conventions the development commits to: $\lambda_{jj}=0$, so a transfer is always between distinct colonies; $\varphi_j(0)=0$ and $\varphi_j(r)>0$ for $r\ge 1$; $\alpha_j>0$; and $g_j$ is asserted via HasSum, which states convergence and the value at once, rather than as an extended real that might be infinite. Occupancy vectors use truncated natural subtraction, so the partial balance and reversed-rate statements carry an explicit $n_j\ge 1$ where the book's state space carries it implicitly; the goal itself does not need such a guard.

A trivializing formalization is ruled out by the second conjunct of the goal: the equilibrium equations alone are a homogeneous linear condition satisfied by $\pi\equiv 0$, whereas the requirement that $\pi$ sum to $1$ forces the constants $g_j$ to be exactly the ones stated.

Contributions welcome beyond the listed items: Burke's theorem (2.1) and the Poisson character of the exit streams, Corollary 2.10, the closed-form of the telephone banking example (Exercise 2.6), the Chinese restaurant process of Exercise 2.13, and Bartlett's theorem (2.17) on linear migration processes over a general space.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 2 (pp. 22–48); Theorems 2.4, 2.8, 2.9, 2.13, equations (2.1)–(2.6). DOI 10.1017/cbo9781139565363
• James R. Jackson, Networks of waiting lines, Operations Research 5 (1957), 518–521. DOI 10.1287/opre.5.4.518
• P. Whittle, Equilibrium distributions for an open migration process, Journal of Applied Probability 5 (1968), 567–571. DOI 10.2307/3211921
• Frank Kelly, Reversibility and Stochastic Networks, Cambridge University Press, 2011 (reissue of the 1979 edition), Chapters 2 and 3.
• David G. Kendall, Some problems in mathematical genealogy, in Perspectives in Probability and Statistics (J. Gani, ed.), Academic Press, 1975, 325–345.
• John D. C. Little, A proof for the queuing formula: $L = \lambda W$, Operations Research 9 (1961), 383–387. DOI 10.1287/opre.9.3.383

Motivation

In the early twentieth century Agner Krarup Erlang worked for the Copenhagen Telephone Company and faced a sizing question that every shared-resource operator still faces: how many parallel circuits must a telephone link carry so that an arriving call is almost never turned away? The answer he published — the Erlang loss formula — is still the standard dimensioning tool for circuit-switched links, call centres, hospital beds, rental fleets, and any system in which a customer who finds every server occupied leaves rather than waits.

The formula is the first capstone of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014), where it closes Chapter 1 and supplies the building block for the loss networks of Chapter 3. It is also the cleanest possible demonstration of the book's method: write down the transition rates of a Markov process, guess that the process is reversible, solve the detailed balance equations, and read the answer off the normalizing constant. This mission formalizes that chapter: the reversibility apparatus, the birth-and-death chain of the loss link, and Erlang's formula itself.

Setting

A link carries $C$ parallel circuits. Calls arrive as a Poisson process of rate $\lambda$ and each call, while it lasts, occupies one circuit for an exponentially distributed holding time of parameter $\mu$; holding times are independent of one another and of the arrival times. A call that arrives to find all $C$ circuits busy is lost — it does not queue.

Let $X(t)\in\{0,1,\dots,C\}$ be the number of busy circuits. Then $X$ is a Markov process with transition rates

and $q(j,k)=0$ otherwise. A collection of numbers $\pi=(\pi(j))$ is in detailed balance with rates $q$ when

and satisfies the equilibrium (full balance) equations when

Detailed balance is the statement that, in equilibrium, transitions from $j$ to $k$ occur as frequently as transitions from $k$ to $j$. Writing $\nu=\lambda/\mu$ for the traffic intensity, Erlang's formula is

Formalization targets

Goal — Erlang's formula

The goal fixes no numerical constant: it says that whatever probability vector solves the detailed balance equations of the loss link assigns exactly $E(\nu,C)$ to the blocking state. The hypothesis is detailed balance rather than full balance, which is what the book's derivation actually uses and is the stronger assumption to discharge.

Supporting levels

together with the reversibility results that justify the method: detailed balance implies full balance, the reversed process of Proposition 1.1 has rates $q'(j,k)=\pi(k)q(k,j)/\pi(j)$ and retains $\pi$ as an equilibrium distribution, and $q'=q$ holds exactly when $\pi$ and $q$ are in detailed balance.

Significance

The result itself. $E(\nu,C)$ is the blocking probability of the link, so it converts a traffic measurement $\nu$ and a target grade of service into a circuit count. It is insensitive: the same formula holds for any holding-time distribution with mean $1/\mu$, which is why it survives as an engineering tool far outside the exponential model that produces it here. Chapter 3 of the book builds loss networks on top of it, and the Erlang fixed point that approximates a whole network is a system of coupled copies of this one formula. The derivative identity is the ingredient that makes $E(\nu,C)$ tractable in optimization: it shows $E$ is increasing in $\nu$, and the recursion it encodes is how the formula is evaluated numerically without overflow.

Formalizing it. Nothing here is open mathematics; the value of the mission is a machine-checked statement of the loss model and a reusable reversibility layer. Mathlib has no theory of detailed balance or of reversible Markov processes over a countable state space, so this mission contributes the first: the predicates DetailedBalance and FullBalance, the reversed rate matrix, and the three structural facts relating them. Those are shared by every later mission in this series — the migration processes of Chapter 2 and the loss networks of Chapter 3 are all proved reversible or quasi-reversible by exactly these means.

Difficulty

The obvious route to $\pi(C)$ is to solve the equilibrium equations directly, and for a birth-and-death chain that is a three-term recursion whose general solution needs two boundary conditions. Detailed balance replaces it with a two-term recursion and one boundary condition, and the whole content of the reversibility section is that the substitution is legitimate. The remaining work is bookkeeping that Lean makes less forgiving than the page does: the detailed balance equations must be indexed so that the $j=0$ and $j=C$ boundaries are not silently assumed away, the normalizing sum must be shown positive before it can be inverted, and the induction that produces $\nu^{j}/j!$ has to carry the Fin (C+1) index through Nat.factorial. For the derivative identity, the naive differentiation of a quotient gives $\left(\sum_{j\le C-1}\nu^{j}/j!\right)$ in the numerator, and recognizing it as $\bigl(1-E(\nu,C)\bigr)$ times the denominator is the step that produces the stated form.

Formalization scope

The state space is Fin (C + 1), so the link with $C$ circuits has $C+1$ states and finiteness is built in; $\pi$ is a plain function Fin (C + 1) → ℝ constrained by hypotheses rather than a PMF, so that the normalization $\sum_j \pi(j) = 1$ appears explicitly wherever it is used. FullBalance is written with unconditional sums (tsum) over an arbitrary state space, so the same predicate serves the countable chains of later chapters; over a Fintype it is the finite sum. Rates are real-valued and q j j = 0 by construction, matching the book's convention that a Markov process must change state when it jumps.

The rates carry $\lambda,\mu>0$ as hypotheses. This rules out the degenerate reading in which $\mu = 0$ makes every downward rate vanish: with $\mu=0$ the detailed balance equations force $\pi(j)\lambda = 0$ for $j<C$, so the only normalized solution is the point mass at $C$, and $\pi(C)=1$ while Lean evaluates $E(\lambda/0,C)=E(0,C)=0$ for $C\ge1$; the goal would be false. Erlang's formula is stated for the last state Fin.last C, not for an unconstrained index, so it cannot be satisfied by a degenerate reindexing.

Contributions welcome beyond the listed items: the insensitivity of $E(\nu,C)$ to the holding time distribution, the recursion $E(\nu,C)=\nu E(\nu,C-1)/(C+\nu E(\nu,C-1))$, the finite-source variant $\pi_M(j)\propto\binom{M}{j}(\eta/\mu)^{j}$ and the PASTA statement that an arriving call in that model sees $\pi_{M-1}$, and the parking-space identity $\sum_{C\ge 0}E(\nu,C)$ of Exercise 1.9.

Selected references

• Frank Kelly and Elena Yudovina, Stochastic Networks, Cambridge University Press, 2014, Chapter 1 (pp. 13–21), equations (1.2), (1.4), (1.5), Proposition 1.1, Exercises 1.7 and 1.8. DOI 10.1017/cbo9781139565363
• A. K. Erlang, Solution of some problems in the theory of probabilities of significance in automatic telephone exchanges, Elektrotkeknikeren 13 (1917), 5–13.
• Frank Kelly, Reversibility and Stochastic Networks, Cambridge University Press, 2011 (reissue of the 1979 edition), Chapter 1.
• J. R. Norris, Markov Chains, Cambridge University Press, 1998. DOI 10.1017/CBO9780511810633

Motivation

Many results in economics and operations research reduce to a single question: does a system of interacting, mutually reinforcing choices settle at an equilibrium? A firm choosing input levels that are complements, a Cournot duopoly whose best responses move together, a matching market where agents' preferences reinforce assortative pairings — each is a fixed-point problem, but classical fixed-point theory (Brouwer, Kakutani) asks for convexity and continuity that these problems rarely have. Tarski's fixed point theorem [1955] showed that order, not topology, suffices: every increasing (monotone) self-map of a nonempty complete lattice has a fixed point, and the fixed points themselves form a nonempty complete lattice, with no continuity or convexity assumed at all. Zhou [1994] extended this from single-valued functions to set-valued correspondences, which is what is needed once "best response" becomes "the (possibly non-unique) set of optimizers." This mission formalizes Zhou's theorem (Topkis's Theorem 2.5.1) together with its parametric extension (Theorem 2.5.2), the two capstones of the lattice-theoretic toolkit that the rest of Topkis's monograph — and, within this series, its mission on supermodular games (Supermodularity and Complementarity V) — builds on directly.

Setting

A lattice $(X, \preceq)$ is a partially ordered set in which every pair of elements $x, y$ has a join $x \vee y$ (least upper bound) and a meet $x \wedge y$ (greatest lower bound). $X$ is a complete lattice if every subset (not just every pair) has a supremum and an infimum in $X$; a nonempty complete lattice always has a greatest element $\top$ and a least element $\bot$.

To compare sets of points — not just points — Topkis defines the induced set ordering $\sqsubseteq$: for $A, B \subseteq X$, $A \sqsubseteq B$ holds when every $a \in A$ and $b \in B$ satisfy $a \wedge b \in A$ and $a \vee b \in B$. Restricted to singletons, $\{a\} \sqsubseteq \{b\}$ says exactly $a \preceq b$, so $\sqsubseteq$ is the natural extension of $\preceq$ from points to sets, and it is the order with respect to which set-valued maps (correspondences) $Y : X \to \mathcal{P}(X)$ are called increasing: $x \preceq x'$ implies $Y(x) \sqsubseteq Y(x')$.

A subset $S \subseteq X$ is a sublattice if it is closed under the binary join and meet of $X$. $S$ is subcomplete if, more strongly, the supremum and infimum in $X$ of every nonempty subset of $S$ exist and lie in $S$ — so a subcomplete sublattice is itself a complete lattice under the order it inherits. A point $x \in X$ is a fixed point of a correspondence $Y$ if $x \in Y(x)$.

Formalization targets

Goal — Theorem 2.5.1 (Zhou's fixed point theorem)

Let $X$ be a nonempty complete lattice and $Y : X \to \mathcal{P}(X)$ an increasing correspondence with $Y(x)$ subcomplete for every $x$. Then:

and the set of fixed points of $Y$, under its inherited order, is itself a nonempty complete lattice.

Theorem 2.5.2 (the parametric extension)

Let $T$ be a partially ordered set and $Y(x,t)$ a jointly increasing, subcomplete-valued correspondence on $X \times T$. Then for each $t$ the greatest and least fixed points $g(t)$, $l(t)$ of $Y(\cdot, t)$ exist and are increasing functions of $t$; under the further hypothesis that $\sup Y(x',t') \prec \inf Y(x',t'')$ whenever $t' \prec t''$, both become strictly increasing in $t$. This is the theorem that gives comparative statics their bite: it says an equilibrium moves monotonically — even strictly — as a parameter of the underlying system changes.

Two supporting results are formalized as milestones because Theorem 2.5.1's own proof invokes them directly: Lemma 2.4.2 (supremum and infimum are monotone under $\sqsubseteq$, whenever they exist) and Theorem 2.4.2 (an intersection of increasing correspondences, if it stays nonempty, is itself increasing).

Significance

The result itself. Tarski–Zhou is the order-theoretic alternative to Brouwer–Kakutani: where the latter needs a convex, compact strategy space and a continuous map, Tarski–Zhou needs only a lattice order and monotonicity, and it delivers something Brouwer–Kakutani does not — a greatest and a least fixed point, with an explicit order-theoretic formula for each, and the guarantee that the whole fixed-point set is a complete lattice in its own right. This is exactly the machinery behind existence proofs for supermodular games (Topkis's own Theorem 4.2.1, where the fixed points of the best-response correspondence are the pure-strategy Nash equilibria) and behind monotone comparative statics more broadly (Milgrom–Roberts [1994], of which Theorem 2.5.2 is a strict generalization to correspondences).

Formalizing it. Mathlib already has Tarski's theorem for single-valued monotone functions (OrderHom.lfp/gfp, fixedPoints.completeLattice, Knaster–Tarski). Nothing in Mathlib currently proves it for set-valued correspondences: this mission is a genuine strengthening of existing formalized mathematics, not a restatement of it, and it introduces the induced set ordering and subcompleteness — reused throughout the rest of this book's mission series — for the first time.

Difficulty

The natural first idea — "apply Knaster–Tarski to some selection function built from $Y$" — fails because there is no canonical way to select a single point from each $Y(x)$ that remains monotone without already knowing the theorem: an arbitrary selection from an increasing correspondence need not itself be increasing (this is exactly the subtlety Topkis's Theorem 2.4.3 addresses only for correspondences with a greatest/least element). The real argument instead builds the candidate fixed point directly as a supremum over an auxiliary set $\{x : Y(x) \cap [x,\infty) \neq \emptyset\}$ and establishes it is a fixed point using the monotonicity lemma (Lemma 2.4.2) at each step — no selection is ever made. A second subtlety is that the fixed-point set is not, in general, a sublattice of $X$: Topkis's Example 2.5.1 exhibits an increasing self-map of $[0,3]^2 \subset \mathbb{R}^2$ whose four fixed points are not closed under $\vee$/$\wedge$. Part (b)'s claim that the fixed points form their own complete lattice must therefore be proved without ever assuming, or implying, that ambient joins and meets of fixed points are again fixed points.

Formalization scope

$X$ is formalized as an abstract CompleteLattice, not ℝⁿ — the theorem is genuinely about order, and specializing to $ℝⁿ$ would hide exactly the generality Zhou's result adds over finite-dimensional fixed-point theorems. The induced set ordering InducedSetOrder and the predicate Subcomplete are defined once in this mission and reused by every later mission in the series that reasons about correspondences ordered by $\sqsubseteq$. A formalization that replaced the correspondence $Y$ by a single-valued function would trivialize the mission into a restatement of Mathlib's existing Knaster–Tarski theorem; the set-valued, subcomplete-ranged correspondence is not an optional generality but the entire content being added. Part (b) of Theorem 2.5.1 is formalized as a completeness statement about the induced order on the fixed-point set itself — not as a claim that the fixed-point set is closed under $X$'s ambient join and meet, which Example 2.5.1 refutes. "Partially ordered set" throughout is Lean's PartialOrder, matching the book's own usage in Chapter 2.

Selected references

• Tarski, A., A lattice-theoretical fixpoint theorem and its applications, Pacific Journal of Mathematics 5(2), 1955, pp. 285–309. https://doi.org/10.2140/pjm.1955.5.285
• Zhou, L., The set of Nash equilibria of a supermodular game is a complete lattice, Games and Economic Behavior 7(2), 1994, pp. 295–300. https://doi.org/10.1006/game.1994.1051
• Milgrom, P. and Roberts, J., Comparing equilibria, American Economic Review 84(3), 1994, pp. 441–459. https://www.jstor.org/stable/2118061
• Topkis, D. M., Supermodularity and Complementarity, Princeton University Press, 2011 (DOI 10.1515/9781400822539), Chapter 2, §2.2–2.5.

Motivation

Two-stage stochastic programs with recourse require evaluating $Q(x) = \mathbb E_\xi[Q(x,\xi)]$, the expected value of a recourse function, at every candidate first-stage decision $x$. When $\xi$ is high-dimensional or continuously distributed, this expectation is a multivariate integral of a piecewise-linear, generally nondifferentiable integrand, and classical quadrature rules — built for smooth integrands in low dimension — do not apply (Birge & Louveaux, §8.1). What does apply is convexity: $Q(x,\cdot)$ is convex whenever the recourse problem is a linear program in $\xi$, and convexity alone is enough to sandwich $\mathbb E_\xi[Q(x,\xi)]$ between two computable discrete approximations. This chapter develops that sandwich, and it is the standard device used throughout the stochastic-programming literature to bound and iteratively refine the recourse function: the lower bound goes back to Jensen [1906]; the upper bound is due to Edmundson [1956] and Madansky [1959], with the mean-consistent LP refinement due to Madansky [1960] and Gassmann & Ziemba [1986]. Refinements of both bounds appear in Huang, Ziemba & Ben-Tal [1977], Kall & Stoyan [1982] and Frauendorfer [1988].

Setting

Fix a probability space $(\Omega, \mathcal F, P)$ and an integrand $g : D \times \Xi \to \mathbb R$, where $\Xi \subseteq E$ is the (convex, closed) support of a random vector $\xi : \Omega \to \Xi$ and $E$ is a real vector space (in the recourse application, $g(x,\cdot) = Q(x,\cdot)$ and $D$ is the first-stage feasible region). Write $\mathbb E(g(x)) = \mathbb E_\xi[g(x,\xi)] = \int_\Xi g(x,\xi)\, P(d\xi)$.

A partition of $\Xi$ into $\nu$ measurable blocks $S^\nu = \{S_1,\dots,S_\nu\}$ determines, for each block, its probability $p_l = P[\xi \in S_l]$ and its conditional mean $\xi^l = \mathbb E[\xi \mid S_l]$. Equivalently — and this is the convention this mission's Lean development uses — the blocks may be taken directly on the sample space as the pulled-back sets $S_l = \xi^{-1}(\text{region}_l) \subseteq \Omega$, with $p_l = P(S_l)$ and $\xi^l = p_l^{-1}\int_{S_l}\xi\,dP$ the Bochner integral average of $\xi$ over the block; the two descriptions coincide.

Formalization targets

Goal — Chapter 8, Theorem 1 (Jensen lower bound), p. 346

This is the sharpest statement the chapter proves for the lower bound: it holds for every finite measurable partition, with no assumption beyond convexity of $g(x,\cdot)$ and integrability.

Chapter 8, Theorem 2 (Edmundson-Madansky upper bound), pp. 347-348

For $\Xi$ compact, let $\mathrm{ext}\,\Xi$ be the extreme points of $\mathrm{co}\,\Xi$, carrying the Borel field of all its subsets. If, for every $\xi \in \Xi$, $\varphi(\xi,\cdot)$ is a probability measure on $\mathrm{ext}\,\Xi$ with barycenter $\xi$ (i.e. $\int_{\mathrm{ext}\,\Xi} e\,\varphi(\xi,de) = \xi$) and $\omega \mapsto \varphi(\xi(\omega), A)$ is measurable for every $A$, then

Together the two targets give the chapter's headline sandwich: for convex $g(x,\cdot)$, the finite-partition Jensen value and the Edmundson-Madansky value bracket the true expectation, and refining the partition (resp. the disintegration) tightens both sides toward it.

Significance

The Jensen bound is the workhorse of discrete-distribution approximation in stochastic programming: it is what makes $Q^\nu(x) = \sum_l p_l Q(x,\xi^l)$ a valid, refinable lower-approximation of the true recourse function, and it underlies the partition-refinement schemes (§8.2, following Birge & Wets [1986] and Frauendorfer & Kall [1988]) used inside the $L$-shaped method and separable-programming solvers described later in the chapter (§8.3). The Edmundson-Madansky bound is its indispensable upper counterpart: without it there is no certificate of how far a lower approximation can be from the truth, and the mean-consistent LP refinement (eq. 2.9, not part of this mission) reduces to a moment-problem computation over $\lambda$. Both bounds are, to date, unformalized: the platform holds no theorem matching either a finite-partition conditional-Jensen inequality or an extreme-point disintegration bound (searched GET /theorems?q=... for "Jensen", "conditional expectation", "Edmundson Madansky", "partition convex" — no relevant hits), so this mission is a first formalization of both, not a reformulation of existing platform content. Mathlib supplies the raw convexity substrate this mission is built from — finite Jensen (Analysis/Convex/Jensen.lean) and, critically, the set-average integral Jensen inequality (ConvexOn.map_set_average_le in Analysis/Convex/Integral.lean), exactly the per-block step the book's proof of Theorem 1 performs — but no existing lemma assembles these into the partitioned, conditional-mean statement the book actually states.

Difficulty

The obvious shortcut is to prove "convex functions lie above their tangent line" and stop — this captures no partition structure at all and is not the theorem the book states (the theorem is about $\Sigma_l p_l g(x,\xi^l)$, a sum over blocks, not a single linearization). The real content is bookkeeping across the partition: writing $\mathbb E(g(x))$ as $\sum_l P(S_l)\,\mathbb E[g(x,\xi)\mid S_l]$ (an exact identity, no convexity needed), then applying ordinary Jensen inside each block to replace $\mathbb E[g(x,\xi)\mid S_l]$ by $g(x,\xi^l)$ from below — the inequality only enters at the second step, once per block. Proving this in Lean means correctly discharging, for every block, the side conditions Mathlib's integral-Jensen lemma needs (closedness of $\Xi$, continuity of $g(x,\cdot)$ on $\Xi$, integrability on the block) and then summing the $\nu$ per-block inequalities against weights $p_l$ that themselves depend on the partition — an easy step to get wrong by, e.g., letting $\xi^l$ be an arbitrary point of $S_l$ rather than exactly its conditional mean, which understates what Jensen actually forces. Theorem 2 additionally requires setting up the disintegration $\lambda$ correctly: $\lambda$ is a probability measure defined as an integral of the kernel-like family $\varphi$ against $P\circ\xi^{-1}$, and both the barycenter condition on $\varphi$ and the measurability of $\omega \mapsto \varphi(\xi(\omega),A)$ are load-bearing — dropping either makes $\lambda$ ill-defined or the bound's proof inapplicable.

Formalization scope

$\Xi \subseteq E$ for $E$ a complete real normed vector space (NormedAddCommGroup E, NormedSpace ℝ E, CompleteSpace E); no finite-dimensionality is assumed since neither theorem's proof needs it. The parameter $x$ ranges over an arbitrary type $\alpha$ with $D \subseteq \alpha$, and $g$ is left as a bare function α → E → ℝ, matching the book's level of abstraction (the recourse LP's own data $A,b,c,q,W,T,h$ is never used in either proof).

The partition is formalized directly on the sample space $\Omega$ (a Partition structure: pairwise-disjoint measurable blocks covering $\Omega$, each of positive measure) rather than on $\Xi$, per the equivalence noted under Setting; $\xi^l$ is defined as the Bochner-integral average $p_l^{-1}\int_{S_l}\xi\,dP$, so it is forced to be the conditional mean and cannot be weakened to an arbitrary sample point of the block — the change the chunk brief flags as the main faithfulness trap for this chapter.

Two explicit hypotheses are added beyond the book's own statement of Theorem 1, both needed by Mathlib's integral-Jensen lemma rather than narrowings of the mathematical content: ContinuousOn (g x) Ξ (finite-dimensional convex functions are automatically continuous on the interior of their domain, which is what the book implicitly relies on; stated explicitly since $E$ is not assumed finite-dimensional) and integrability of $\xi$ and of $g(x,\xi(\cdot))$ (needed for $\mathbb E(g(x))$ and each $\xi^l$ to be well-defined). For Theorem 2, the disintegrating family $\varphi$ is E → Measure Ext for an abstract type Ext (standing for $\mathrm{ext}\,\Xi$) with the discrete MeasurableSpace (every subset measurable, matching the book's "Borel field ... the collection of all subsets"), mapped into $E$ by an embedding toE whose range is exactly (convexHull ℝ Ξ).extremePoints ℝ; the measure $\lambda$ (named μExt in the Lean code, since λ is a reserved keyword) is a hypothesis satisfying its defining equation (2.6) rather than constructed, since constructing a measure from a set function is a separate, book-external piece of measure theory the chapter's own proof does not perform either — it simply asserts $\lambda$ is the probability measure with that value on every set.

A trivializing formalization is ruled out explicitly: a version that lets $\xi^l$ range over an arbitrary point of $S_l$, or that proves only the ordinary (unconditional) Jensen inequality without ever introducing the partition, states something strictly weaker than the book and is not what is formalized here.

Both draft theorems end in := by sorry; a full Lean proof of Theorem 1 combines Mathlib's ConvexOn.map_set_average_le applied per block with the exact decomposition of $\int_\Omega$ into $\sum_l \int_{S_l}$ over the partition's disjoint, covering blocks. Reusable beyond this mission: the Partition structure and its weight/condMean accessors generalize to any chapter needing a finite measurable partition with conditional means (this book's later approximation schemes, §8.2-8.5 and Chapter 10, all build on the same device). Contributions solving either theorem, or formalizing the partition-refinement monotonicity $\mathbb E(g(x)) \ge \mathbb E^{\nu+1}(g(x)) \ge \mathbb E^\nu(g(x))$ (eq. 2.3, not part of this mission's milestone list since it is not itself a numbered theorem) as a follow-up, are welcome.

Selected references

• J.R. Birge, F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4
• J.L.W.V. Jensen, Sur les fonctions convexes et les inégalités entre les valeurs moyennes, Acta Mathematica 30 (1906), 175-193. https://doi.org/10.1007/BF02418571
• H.P. Edmundson, Bounds on the expectation of a convex function of a random variable, The RAND Corporation, Paper 982, 1956.
• A. Madansky, Bounds on the expectation of a convex function of a multivariate random variable, Annals of Mathematical Statistics 30 (1959), 743-746. https://doi.org/10.1214/aoms/1177706207
• A. Madansky, Inequalities for stochastic linear programming problems, Management Science 6 (1960), 197-204. https://doi.org/10.1287/mnsc.6.2.197
• H.I. Gassmann, W.T. Ziemba, A tight upper bound for the expectation of a convex function of a multivariate random variable, Mathematical Programming Study 27 (1986), 39-53. https://doi.org/10.1007/BFb0121114
• J.R. Birge, R.J-B. Wets, Designing approximation schemes for stochastic optimization problems, in particular for stochastic programs with recourse, Mathematical Programming Study 27 (1986), 54-102. https://doi.org/10.1007/BFb0121122

Motivation

Every stochastic program is, in practice, compared against a shortcut. A decision maker facing genuine uncertainty is tempted either to replace the random data by its mean and solve one deterministic problem, or to imagine that perfect information about the future were available and solve a separate deterministic problem per scenario. Both temptations have precise answers: the expected value of perfect information (EVPI) measures how much a decision maker should be willing to pay for a perfect forecast, and the value of the stochastic solution (VSS) measures the cost of ignoring uncertainty altogether by solving the mean-value problem. Both concepts originate in decision analysis — EVPI traces to Raiffa and Schlaifer (1961) — and were brought into stochastic programming by Madansky (1960), who proved the first chain of inequalities relating the wait-and-see value, the recourse value and the expected-value-solution's cost. Birge and Louveaux, Introduction to Stochastic Programming, 2nd ed. (Springer, 2011), Chapter 4, gives the standard modern treatment, including a refined family of bounds — built from pairs subproblems against a chosen reference scenario — that sharpen VSS beyond the original mean-scenario comparison. This mission formalizes that chapter's capstone: the five-quantity, four-inequality chain that pins VSS between two computable optimal values.

Setting

Fix a two-stage stochastic program with fixed recourse: a finite family of K scenarios $\xi_1,\dots,\xi_K$ in $\mathbb R^d$, each occurring with probability $p_k \ge 0$, $\sum_k p_k = 1$; a first-stage feasible set $K_1 \subseteq \mathbb R^{n_1}$; and, for every first-stage decision $x \in \mathbb R^{n_1}$ and every scenario $\xi \in \mathbb R^d$, a scenario cost $z(x,\xi)$ — the optimal value of $c^Tx + \min\{q^Ty \mid Wy = h(\xi) - Tx,\ y \ge 0\}$. By convention $z(x,\xi) = +\infty$ when $x$ has no feasible second-stage recourse under $\xi$, and $z(x,\xi) = -\infty$ when the second-stage program is unbounded below.

From $z$, five basic quantities are defined (Birge & Louveaux §4.1–§4.2):

• The recourse problem's value, $RP = \min_{x \in K_1} \mathbb E_\xi\, z(x,\xi)$ — the best a decision maker can do without foreknowledge of $\xi$ (the "here-and-now" solution).
• The wait-and-see value, $WS = \mathbb E_\xi\big[\min_{x \in K_1} z(x,\xi)\big]$ — the average cost if $\xi$ were revealed before choosing $x$.
• The expected value of perfect information, $EVPI = RP - WS$.
• The expected value problem's solution $\bar x(\bar\xi)$, optimal for the deterministic problem at the mean scenario $\bar\xi = \mathbb E(\xi)$; its recourse cost, the expected result of using the EV solution, is $EEV = \mathbb E_\xi\, z(\bar x(\bar\xi), \xi)$.
• The value of the stochastic solution, $VSS = EEV - RP$ — the extra cost of implementing the mean-scenario decision instead of solving the recourse problem.

Section 4.6 refines VSS by replacing the mean scenario with an arbitrary reference scenario $\xi^r$ (not necessarily one of the $K$ possible scenarios, e.g. a worst case), with assumed probability $p_r = P(\xi=\xi^r)$:

• $\bar x^r$, optimal for $\min_{x\in K_1} z(x,\xi^r)$, gives the expected value of the reference-scenario solution, $EVRS = \mathbb E_\xi\, z(\bar x^r,\xi)$, and the generalized $VSS = EVRS - RP$.
• For each scenario $\xi^k$, the pairs subproblem of $\xi^r$ and $\xi^k$ treats them as a two-point distribution with weights $p_r$ and $1-p_r$: its optimal value is $\min_{x\in K_1}\big[p_r\,z(x,\xi^r) + (1-p_r)\,z(x,\xi^k)\big]$, attained at some $\bar x^k$. Averaging these optimal values over $k$ (rescaled by $1/(1-p_r)$) gives the sum of pairs expected values, $SPEV$. Taking, instead, the smallest full expected cost $\mathbb E_\xi\,z(\bar x^k,\xi)$ among the $K{+}1$ candidate solutions $\{\bar x^1,\dots,\bar x^K,\bar x^r\}$ gives the expectation of pairs expected value, $EPEV$.

Formalization targets

Goal — Chapter 4, Theorem 9 (p. 174)

Four links, each with independent content: nonnegativity of the leftmost gap, then two genuine inequalities (from the pairs-subproblem comparisons of Propositions 7 and 8), then the identity $VSS = EVRS - RP$ folded against $RP \ge WS$'s reverse-direction cousin. This is the weakest statement that keeps all five quantities distinct — stating only the outer bound $0 \le VSS \le EVRS-WS$ would erase exactly the refinement (via pairs subproblems) that makes the chapter's method useful.

Supporting propositions (milestones, in attack order)

• Proposition 1 (p. 166): $WS \le RP \le EEV$.
• Proposition 5(a) (pp. 167–168): $0 \le EVPI$ and $0 \le VSS$ (mean-scenario form), for any stochastic program.
• Proposition 7 (p. 173): $WS \le SPEV \le RP$.
• Proposition 8 (p. 174): $RP \le EPEV \le EVRS$.

Significance

The chain gives a decision maker two computable, non-obvious bounds on VSS — a quantity that is otherwise expensive to pin down exactly, since $RP$ itself already requires solving the full recourse problem. $EVRS - EPEV$ and $EVRS - SPEV$ are both computable from $K+1$ (or $K$) two-scenario LPs, far cheaper than the full $K$-scenario recourse problem, so Theorem 9 turns an expensive exact quantity into a pair of cheap certified bounds. Formalizing it fixes, once and for all, the exact hypotheses and quantifier structure of Madansky's original inequality (Proposition 1) together with the later pairs-subproblem refinement (Propositions 6–8, Birge 1982), often cited informally as "the VSS bounds" without distinguishing $EEV$, $EVRS$, $EPEV$ and $SPEV$. No part of this chain is on Mathlib or Formalpedia today (checked by concept query, not title); this is a first, from-scratch treatment of two-stage recourse value-of-information theory as formal objects.

Difficulty

The obvious first idea — collapse $RP$, $WS$, $EV$, $EEV$, $EVRS$, $EPEV$, $SPEV$ to one "the optimal value of the LP" and prove a single inequality — throws away the entire content of the chapter. Each quantity restricts the minimization to a different feasible object: $RP$ minimizes jointly over $x$; $WS$ swaps the order of $\min$ and $\mathbb E$; $EEV$/$EVRS$ evaluate one fixed $x$ under every scenario; $SPEV$ and $EPEV$ each minimize over a family of pairs subproblems rather than the full $K$-scenario problem. The chain's proof (Propositions 7–8) depends on this precisely: Proposition 7's lower bound uses that each pairs-subproblem-optimal $(\bar x^k,\bar y^k)$ is feasible (not necessarily optimal) for the single-scenario problem at $\xi^r$, and its upper bound uses that the recourse-optimal $(x^*, y^*(\xi^r), y^*(\xi^k))$ is feasible (not necessarily optimal) for the pairs subproblem — a feasible-but-not-optimal argument in each direction, not a direct comparison of objective values. Losing track of which solution is fixed and which is optimized destroys the argument entirely.

Formalization scope

An Instance bundles the finite scenario set (Fin K, probabilities p : Fin K → ℝ with p ≥ 0, ∑ p = 1, scenarios xi : Fin K → (Fin d → ℝ)), the first-stage feasible set K1 : Set (Fin n1 → ℝ), and the scenario cost z : (Fin n1 → ℝ) → (Fin d → ℝ) → EReal, using the extended reals to carry the book's own +∞/−∞ conventions for infeasibility and unboundedness rather than silently restricting to a finite-valued special case (a genuine risk of trivialization here, since Example 2 of the chapter exhibits $EEV = +\infty$). All optimal values (RP, WS, EV, EVPI, EEV, VSS, EVRS, generalized VSS, SPEV, EPEV) are defined directly from z, matching the book's own level of abstraction in this chapter (which never unfolds z into the underlying LP's $A,b,c,q,W,T,h$ data — those appear only in Chapter 3). Because EEV, the mean-scenario VSS, EVRS, the generalized VSS, and EPEV are each defined relative to an optimal solution of some sub-problem — the book itself only ever says "let $\bar x(\bar\xi)$ denote some optimal solution" — every theorem using them states that solution and its optimality as explicit hypotheses (x ∈ K1 and z x … = ⨅ …), never baking it into a Classical.choiced value; this keeps the quantifier structure faithful to the book's own "let ... be an optimal solution" phrasing. Proposition 5's part (b) — the upper bound $EVPI \le EEV-EV$, $VSS \le EEV-EV$ "for stochastic programs with fixed recourse matrix and fixed objective coefficients" — needs a different scope: that hypothesis is a structural property of the underlying LP data ($W$, $c$, $q$ fixed across scenarios) invisible once $z$ is abstracted away as above, and pinning it down would require modeling the LP's $A,b,c,q,W,T,h(\xi)$ data explicitly (as Chapter 3's mission does for its convexity theorem). That part is out of scope here and is not needed for Theorem 9's own chain, which rests only on Proposition 5(a).

Collapsing any two of $RP$, $WS$, $EV$, $EEV$, $EVRS$, $EPEV$, $SPEV$ to a single "value of the LP" — the trivialization this book-wide series flags for Chapter 4 — is ruled out by construction: each is its own definition over its own feasible object, and Theorem 9's statement names all five quantities in the chain rather than only its outer bound. The two occurrences of "VSS" in the chapter (the original mean-scenario $EEV-RP$ of §4.2, and the reference-scenario $EVRS-RP$ generalization of §4.6, used only in Theorem 9) are likewise kept as two distinct definitions rather than conflated under one name.

Every addition and subtraction between EReal values in this mission — inside expect, WS, EVPI, VSS, EVRS's appearance in VSSRef, the pair sum inside pairsValue, the sum inside SPEV, and all four differences in Theorem 9's own chain — uses three explicit operations, badd/bsub/bsum, that implement the book's own convention (p. 164) that +∞ (infeasibility) dominates, i.e. (+∞)+(−∞)=+∞, rather than Mathlib's native EReal addition, whose ⊤+⊥=⊥ would make VSS ≥ 0 (Proposition 5(a)) and the goal's own leftmost inequality false whenever a witness solution is infeasible in a positive-probability scenario — exactly the situation of the book's own Example 2 (pp. 174-175). The reference scenario's probability $p_r=\Pr(\xi=\xi^r)$ (p. 172) is likewise not a free parameter but a definition, refProb, computed from the instance itself as $\sum_{k:\,\xi^k=\xi^r}p_k$; SPEV's sum is correspondingly restricted to the scenarios other than the reference scenario ($\xi^k\ne\xi^r$), matching the book's own proof of Proposition 7, which uses $\sum_{k\ne r}p_k=1-p_r$. The single hypothesis refProb I xir < 1 on Propositions 7, 8 and the goal says that some other scenario remains possible, which the book's own $(1-p_r)^{-1}$ factor presupposes.

Reusable beyond this mission: the Instance definition and the RP/WS/EV quantities are the natural base for any later chapter of this series that needs the two-stage recourse value (e.g. Chapter 3's convexity mission, Chapter 5's L-shaped method); contributions extending this Instance to the full LP data of the underlying two-stage program, or adding Proposition 5(b) and Proposition 2's Jensen-inequality argument on top of it, are welcome.

Selected references

• J.R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, 2011, Chapter 4. DOI: 10.1007/978-1-4614-0237-4
• A. Madansky, "Inequalities for Stochastic Linear Programming Problems", Management Science 6(2), 1960, 197–204.
• H. Raiffa and R. Schlaifer, Applied Statistical Decision Theory, Harvard Business School, 1961.
• J.R. Birge, "The Value of the Stochastic Solution in Stochastic Linear Programs with Fixed Recourse", Mathematical Programming 24(1), 1982, 314–325.

Motivation

When exact dynamic programming is intractable, practice runs on approximations: one-step and multistep lookahead with a cost-to-go surrogate, open-loop feedback control, and rollout — the algorithm that improved backgammon programs and became a conceptual ancestor of Monte-Carlo tree search and modern policy improvement schemes. Chapter 6 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) gives the basic guarantees: performance bounds for limited lookahead (Props. 6.3.1–6.3.2), superiority of open-loop feedback control over open-loop control (Prop. 6.2.1), and the cost-improvement theory of rollout on discrete deterministic problems (Props. 6.4.1–6.4.3). These are the theorems that make "approximate DP" more than a heuristic.

Setting

Two frameworks. For the stochastic bounds (§6.2–6.3): the basic finite-horizon model of Mission I of this series (BertsekasDPModel), its policy cost recursion, and the open-loop cost of a fixed control sequence (BertsekasDPOpenLoopCost). For rollout (§6.4.1): a graph search problem — a finite digraph with destination set and terminal costs $g(i)$ on destinations (BertsekasGraphSearch); a base heuristic $\mathcal{H}$ producing from every node a path to a destination (BertsekasBaseHeuristic), with projection $p(i)$ and heuristic cost $H(i) = g(p(i))$; the rollout algorithm $R\mathcal{H}$ repeatedly moves to a neighbor $j$ minimizing $H(j)$ (BertsekasIsRolloutRun). $\mathcal{H}$ is sequentially consistent if its paths have the tail property (Def. 6.4.1), sequentially improving if $\min_{j \in N(i)} H(j) \le H(i)$ (Def. 6.4.2).

Target

For sequentially improving $\mathcal{H}$ and any terminating rollout run $(i_1, \dots, i_{\bar m})$:

— BertsekasDP.rollout_sequential_improvement (goal, Prop. 6.4.2). Milestones: Props. 6.4.1 (termination under sequential consistency with the book's tie-breaking), 6.4.3 (exact cost identity via the defects $\delta_i$), 6.3.1, 6.3.2 (lookahead bounds), 6.2.1 (OLFC).

Significance

Prop. 6.4.2 is the "rollout never hurts" theorem — the formal warrant for policy improvement by simulation, with Prop. 6.3.1 its stochastic counterpart (via Example 6.3.1 the rollout of any policy improves that policy). Prop. 6.3.2 is the robustness version that quantifies the cost of inexact minimization, used for CEC bounds. Formalizing the chapter yields a reusable graph-search + base-heuristic vocabulary and connects it to the Mission I stochastic model. Everything here is proved in the book; the formal versions are new.

Difficulty

The rollout proofs are elementary but exact: the min formula (6.37) requires tracking the running minimum along the run, and the IsLeast membership half forces identifying which neighbor value is attained. Termination under sequential consistency (6.4.1) is the delicate one — it fails without the tie-breaking convention (the book gives a cycling counterexample), so the formal statement carries the convention explicitly and the proof must extract a termination measure from "strict decreases are finitely many, plateaus shorten the heuristic path". The stochastic bounds are clean backward inductions over the Mission I recursion.

Formalization scope

Graph search: finite node type, arcs as ordered pairs, vertex costs only (no arc costs — the book's reduction absorbs them into destination costs); heuristic paths as lists; rollout runs as lists (finite, complete runs) except 6.4.1, where the run is an infinite sequence absorbed at destinations so that termination is a genuine claim. Ties in neighbor selection are allowed everywhere except where 6.4.1's convention pins them. Stochastic side: state-independent constraint sets for OLFC (as in §6.2); restricted lookahead sets $\bar U_k(x) \subseteq U_k(x)$ per Eq. (6.19); all statements at the level of the Mission I model.

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (§6.2–6.4.) http://www.athenasc.com/dpbook.html
• G. Tesauro, G. R. Galperin, On-line policy improvement using Monte-Carlo search, NIPS 1996. https://papers.nips.cc/paper/1302
• D. P. Bertsekas, J. N. Tsitsiklis, C. Wu, Rollout algorithms for combinatorial optimization, J. Heuristics 3 (1997), 245–262. https://doi.org/10.1023/A:1009635226865

Motivation

Dynamic programming is the backbone of stochastic optimal control, operations research, and reinforcement learning. Its cornerstone — that the backward recursion of Bellman computes the optimal cost of a finite-horizon stochastic control problem — is stated as Proposition 1.3.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., Athena Scientific, 2005), the standard graduate text on the subject. Every convergence result for value iteration, every performance bound for approximate DP, and every correctness proof for a planning algorithm ultimately leans on this proposition. A machine-checked version of it — over a clean, reusable model of the basic problem — is the natural foundation stone for formalized control theory and RL theory alike.

Setting

The basic problem (§1.2 of the book): a discrete-time system

with state $x_k \in S$, control $u_k$ constrained to a finite nonempty set $U_k(x_k) \subseteq C$, and disturbance $w_k$ drawn from a finite space $W$ with conditional probabilities $p_k(w \mid x_k, u_k)$. A policy is a sequence $\pi = \{\mu_0, \mu_1, \dots\}$ of feedback maps $\mu_k : S \to C$; it is admissible if $\mu_k(x) \in U_k(x)$ everywhere. Its expected cost from $x_0$ is

In the Lean development these are BertsekasDPModel, BertsekasDPPolicyCost (backward recursion on remaining stages), and the DP recursion BertsekasDPValue:

Section 1.6 of the book develops the minimax variant, where the disturbance is chosen antagonistically from a finite membership set $W_k(x,u)$; the mission mirrors it with BertsekasMinimaxDPModel, BertsekasMinimaxPolicyCost, BertsekasMinimaxValue.

Target

formalized as BertsekasDP.dp_algorithm_optimality: the DP value at the horizon is an IsLeast of the set of admissible policy costs. Milestones: the min–max interchange Lemma 1.6.1 (minimax_selection_interchange) and the minimax DP validity (minimax_dp_algorithm).

Significance

The proposition itself is the license to compute optimal policies stage by stage; downstream, Missions VI and VII of this series (lookahead bounds, infinite-horizon theory) consume exactly this model and recursion. Formalizing it produces the reusable model of the basic problem — the shared vocabulary for the whole series. The result is classical and proved in the book; the contribution here is a machine-checked proof over a model faithful to the book's, with the measurable-selection subtleties deliberately avoided by finiteness (see scope).

Difficulty

The proof is a backward induction, but the standard informal argument ("interchange expectation and minimization") must be carried out honestly: the induction hypothesis is about all states simultaneously, the minimizing control must be selected as a function of the state (choice over a finite set), and the policy-cost recursion must be related to the value recursion stage by stage. The minimax milestone needs the interchange lemma with its $> -\infty$ proviso — the classic trap is losing that hypothesis and asserting a false unconditioned interchange.

Formalization scope

Finite disturbance space (Fintype W), finite nonempty control-constraint sets (Finset, inf'), arbitrary (possibly infinite) state space; expectations are finite weighted sums, probabilities are required to be distributions only at admissible controls. Stage data are total functions on $\mathbb{N}$; only stages $0,\dots,N-1$ matter. Policies are deterministic Markov feedback maps — for this class the book's result is exactly recovered. The trivializing risks (empty constraint sets, junk beyond horizon) are ruled out by the nonemptiness field and by evaluating at exactly $N$ remaining stages. Lemma 1.6.1 is stated in the extended reals over arbitrary types with the book's finiteness-of-infimum proviso.

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. ISBN 1-886529-26-4. (Prop. 1.3.1, §1.2–1.3, §1.6.) http://www.athenasc.com/dpbook.html
• R. Bellman, Dynamic Programming, Princeton University Press, 1957.

Restless multi-armed bandits are the standard model for allocating a scarce resource across many independently-evolving agents: N arms, each a small Markov chain, and a budget that lets you activate only a fixed fraction of them at each step. The joint problem is PSPACE-hard, so practice runs on index policies — score each arm by a priority index computed from its own local state, then activate the top ones until the budget runs out — and evaluates them by value decomposition: approximate the joint Q-function by a sum of per-arm local Q-functions, each computed from a single arm's chain. The decomposition is used everywhere from Whittle-index heuristics to modern multi-agent RL, and it is used without an error bound.

Chen and Peng (arXiv:2506.02385) supply one. Their companion mission established the general principle: the value decomposition error of a multi-agent chain is controlled by its measure of Markov entanglement, the distance from the chain's transition matrix to the nearest separable one. This mission carries that principle to the restless-bandit setting and proves that index policies are asymptotically separable — their entanglement decays like 1/sqrt(N), so the decomposition error is sublinear in N while the joint Q-function itself is of order N. The relative error vanishes as the system grows, which is exactly why the practice works.

The argument runs through the mean-field limit. Because the arms are homogeneous, the only thing that matters about a joint state is its configuration: the fraction of arms in each local state. Under an index policy the configuration evolves by a map that does not depend on N at all, and under two standard technical conditions — a uniform global attractor property and non-degeneracy — that map has a unique attracting fixed point m*. The chain of reasoning is: policy entanglement is bounded by how far the realised policy sits from the mean-field limiting policy (Proposition 1); that distance is bounded by the configuration's deviation from m* (Lemma 2/8); and the deviation concentrates at rate 1/sqrt(N) by a concentration-plus-local-stability argument adapted from Gast, Gaujal and Yan. The concentration and stability inputs (Lemmas 9, 10, 11) are results of Gast et al. and are formalized here as well, so the mission stands on its own.

The mission also formalizes the mean-field map on the whole simplex and checks it against the N-agent characterisation, which is what makes the piecewise-affine and stability analysis expressible at all.

When is a system of linear constraints infeasible? Sections 4.6-4.7 of Bertsimas-Tsitsiklis answer with the archetypal theorem of the alternative. The capstone is Farkas' lemma (Theorem 4.6): for an $m \times n$ matrix $A$ and $b \in \mathbb{R}^m$, exactly one of the following holds — (a) some $x \ge 0$ satisfies $Ax = b$, or (b) some $p$ satisfies $p'A \ge 0'$ and $p'b < 0$; such a $p$ is a certificate of infeasibility, geometrically a hyperplane separating $b$ from the cone of the columns of $A$. The mission also carries the cone-membership restatement (Corollary 4.3), the inequality form (Theorem 4.7: every solution of $Ax \le b$ satisfies $c'x \le d$ iff some $p \ge 0$ has $p'A = c'$ and $p'b \le d$), and the application to asset pricing (Theorem 4.8: a market's prices admit no arbitrage iff there is a nonnegative state-price vector $q$ with $p_i = \sum_s q_s r_{si}$). The book proves Farkas' lemma from LP strong duality; Section 4.7 then reverses the arrow from first principles: every polyhedron is closed (Theorem 4.9), Weierstrass' theorem (Theorem 4.10, already in Mathlib), and the separating hyperplane theorem (Theorem 4.11: for nonempty closed convex $S$ and $x^* \notin S$ there exists $c$ with $c'x^* < c'x$ for all $x \in S$), from which Farkas' lemma — and hence the duality theorem itself — follows geometrically.

Chapter One of Jim Hefferon's Linear Algebra develops Gauss's method and asks what row reduction actually preserves. The answer arrives as the Linear Combination Lemma: row operations change the rows of a matrix but never the subspace those rows span, and that invariant is complete. The goal theorem is that completeness — two matrices are row equivalent exactly when they have the same row space — which is what makes reduced echelon form a genuine canonical form. The milestones are the two results the chapter builds on the way: that row operations leave a system's solution set alone, and that a solution set is always one particular solution translated by the solutions of the associated homogeneous system.

Where should one look for the optimum of a linear programming problem? Chapter 1 of Bertsimas–Tsitsiklis suggests that optima "tend to occur at corners" of the feasible polyhedron; §§2.5–2.6 turn this intuition into theorems. Not every polyhedron has a corner — a halfspace in $\mathbb{R}^n$ ($n > 1$) has none — and the exact dividing line is the presence of an infinite line: a nonempty polyhedron

has an extreme point if and only if it does not contain a line, if and only if $n$ of the vectors $a_1, \dots, a_m$ are linearly independent (Theorem 2.6). In particular every nonempty bounded polyhedron and every nonempty standard-form polyhedron has a basic feasible solution (Corollary 2.2). The capstone, Theorem 2.8, is the sharpest form of the corner principle: if $P$ has at least one extreme point, then for any cost vector $c$ either the optimal cost is $-\infty$, or there is an extreme point of $P$ that is optimal — existence of an optimal solution comes for free once the cost is bounded below. Its companion Theorem 2.7 places an optimal extreme point under the weaker assumption that an optimal solution exists, and Corollary 2.3 — the fundamental theorem of linear programming — concludes that every feasible LP either has optimal cost $-\infty$ or attains an optimal solution, in stark contrast with nonlinear problems such as minimizing $1/x$ over $x \ge 1$. These results license the extreme-point search that the simplex method (Mission IV) performs.

Beneath Exp3, Exp4 and their relatives lies one algorithm: minimize past losses plus a convex regularizer. Chapters 26–28 of Lattimore–Szepesvári develop this unifying view. For a Legendre potential $F$ with Bregman divergence $D_F$, both mirror descent and follow-the-regularised-leader satisfy the master bound $R_n(a) \le \frac{F(a) - F(a_1)}{\eta} + \frac{1}{\eta}\sum_t D_F(a_t, \tilde a_{t+1})$; the negentropy potential on the simplex recovers Exp3 exactly. The goal theorem is the payoff for adversarial linear bandits: FTRL on the unit ball with the self-concordant-flavoured potential $F(a) = -\log(1-\|a\|) - \|a\|$ achieves $R_n \le 2\sqrt{3nd\log n}$ — improving the $\sqrt{d}$ factor over the Exp3-style approach of Chapter 27 and matching the $\Omega(d\sqrt{n})$ lower bound of Mission XI up to logarithms.

Real decisions come with context: a news site chooses an article for a particular user. Competing with the single best arm is then meaningless; the right benchmark is the best mapping from contexts to arms, or more generally the best of $M$ expert policies. Chapter 18 of Lattimore–Szepesvári formalizes this via Exp4 — exponential weighting over experts, fed by the importance-weighted estimator of Mission V. The goal theorem: with learning rate $\eta = \sqrt{2\log(M)/(nk)}$, Exp4 satisfies $R_n \le \sqrt{2nk\log M}$ against the best of $M$ experts. Since $M$ enters only logarithmically, the learner can compete with exponentially large policy classes — the conceptual gateway from bandits to reinforcement learning with function approximation.

Formalize sample-path stability for a continuous-time, unit-rate, infinite-buffer single-server queue. Starting from cumulative arriving service work, define the reflected transient workload, the workload constructed from the infinite past, long-run offered load, and two-time stationarity. Prove that subcritical load forces finite-time coupling and consequently that every finite initial workload converges in its two-time finite-dimensional distributions to the stationary workload law.

Formalize sample-path Little's Law for deterministic continuous-time queueing trajectories, decomposed into area, sojourn, arrival-rate, boundary, and squeeze lemmas.

Motivation

The free energy principle (FEP) proposes that a self-organizing system — a brain, an organism, an agent — persists by minimizing one quantity: the variational free energy of its sensory states under an internal generative model. Introduced by Karl Friston as a principle of brain function [Friston 2006] and stated in its unified form [Friston 2010], the principle makes a precise mathematical claim at its core: whatever internal state estimate the system holds, the free energy of incoming data is never below the data's surprisal (negative log marginal likelihood), and the excess is exactly the Kullback–Leibler divergence between the system's recognition density and the Bayesian posterior implied by the model. Active inference extends the same functional from perception to action and planning [Friston et al. 2017], and the same bound is known in machine learning as the evidence lower bound (ELBO) of variational inference [Parr et al. 2022].

Timeline of the mathematical content this mission formalizes:

• 2006 — Friston, A free energy principle for the brain (J. Physiol. Paris 100): the bound stated for perception as variational inference on a generative model.
• 2010 — Friston, The free-energy principle: a unified brain theory? (Nat. Rev. Neurosci. 11, 127–138): free energy as an upper bound on surprisal, presented as the core of a unified account.
• 2017 — Friston, FitzGerald, Rigoli, Schwartenbeck, Pezzulo, Active inference: a process theory (Neural Comput. 29(1), 1–49): the same functional drives policy selection through expected free energy.
• 2022 — Parr, Pezzulo, Friston, Active Inference (MIT Press): textbook treatment; the posterior-form identity $F = D_{\mathrm{KL}}(Q\,\|\,P(s|o)) - \log P(o)$ as the central equation.
• 2026 — fep_formal (Active Inference Institute): a machine-checked Lean 4 catalogue of 155 Free Energy Principle topics, compiled with zero proof holes against a pinned Mathlib. This mission transcribes the catalogue's core-free-energy chain — topic fep-002 and the foundation module active_inference — onto the platform, turning the first link of the FEP development into solvable community infrastructure.

Setting

Everything is finite, and laws are normalized real mass functions.

A finite law on a finite type $\alpha$ is a function $p : \alpha \to \mathbb{R}$ with $p(x) \ge 0$ for every $x$ and $\sum_x p(x) = 1$. A finite kernel from $\alpha$ to $\beta$ assigns to each $x \in \alpha$ a normalized row over $\beta$. The mission's definitions Def_fep_finite_laws and Def_fep_finite_information package these carriers with entropy, cross-entropy, and the KL divergence

a totalized real-valued divergence that is finite even at zero-mass atoms (the convention $0 \cdot \log 0 = 0$ via Real.negMulLog) and nonnegative on normalized laws.

A finite generative model for active inference (definition Def_fep_generative_model) over finite types $\mathsf{Policy}, \mathsf{State}, \mathsf{Outcome}$ consists of: an initial state law $P(s)$; a policy-conditioned transition kernel; a state-to-outcome likelihood kernel; a preference law over outcomes; and a policy prior. Under a policy $\pi$ the model predicts the state law $P(s \mid \pi)$ and the outcome law $P(o \mid \pi)$. A recognition density is any finite law $Q$ over states — the system's internal estimate. At an outcome $o$ with positive predicted mass, the Bayesian posterior $P(\cdot \mid o, \pi)$ is the exact finite Bayes rule. The outcome surprisal is $-\log P(o \mid \pi)$, and the posterior-form variational free energy of a recognition density $Q$ is