Operations Research

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.