The OR Formalization Drive

Markov chain Monte Carlo turns hard integration problems into long simulations: to estimate an expectation $E_\pi f$ one runs a Markov chain with stationary distribution $\pi$ and reports the sample average $\bar f_n$. The ergodic theorem guarantees $\bar f_n \to E_\pi f$, but honest error bars require more: a central limit theorem

On general state spaces this is famously delicate - a merely ergodic chain with a square-integrable functional can fail the CLT, so the classical theory trades convergence rates (drift, minorization, geometric or polynomial total-variation rates) and mixing conditions ($\alpha$-, $\rho$-, $\varphi$-mixing) against moment conditions on $f$. This mission formalizes G. L. Jones's survey "On the Markov chain central limit theorem" (Probability Surveys, 2004): the drift-condition CLTs of Meyn-Tweedie and Jarner-Roberts, the classical mixing CLTs of Ibragimov-Linnik, Doukhan-Massart-Rio and Billingsley, the characterizations via uniform integrability and boundedness in probability, and their assembly into the summary theorem: six practically checkable regimes - from polynomial ergodicity with bounded functionals to uniform ergodicity with second moments - each of which guarantees the CLT for every initial distribution. The stationarity, total-variation and mixing infrastructure is general state space and reusable well beyond this mission.

Modern A/B tests must infer lifetime treatment effects — e.g. customer lifetime value under a new feature — from short-horizon experiment data. Chen, Simchi-Levi and Wang (arXiv:2407.19618) model the experiment as a Markov decision process and exploit a structural fact of many practical interventions: the treatment is local, modifying the system at a single crucial state only. This mission formalizes the core asymptotic theory of the paper: for any differentiable estimator built from the experiment's transition and reward statistics, information sharing — pooling across test arms the samples collected away from the treated state — keeps the estimator asymptotically normal with the same asymptotic bias and never increases its asymptotic variance (Theorem 9), and is asymptotically efficient among unbiased estimators (Theorem 5). The route runs through a Markov chain central limit theorem with the asymptotic variance identified as the autocovariance series, and the linearization/delta method for functionals of chain statistics.

Motivation

Luenberger's Optimization by Vector Space Methods (Wiley, 1969) organizes a large part of optimization theory around a single geometric idea: minimum norm problems in inner product spaces, solved by orthogonal projection. Chapter 3 is the technical heart of that program. Its projection theorem and normal equations underlie least-squares data fitting, Fourier approximation, minimum-energy control, and the whole statistical estimation theory of Chapter 4 — which Missions II and III of this series formalize on top of the present one.

Setting

Throughout, spaces are real. A pre-Hilbert space is a real vector space $X$ with an inner product $\langle\cdot,\cdot\rangle$ inducing the norm $\|x\| = \langle x,x\rangle^{1/2}$; a Hilbert space $H$ is a complete pre-Hilbert space. Vectors $x, y$ are orthogonal when $\langle x, y\rangle = 0$; for a subset $S$, the orthogonal complement $S^\perp$ is the set of vectors orthogonal to every element of $S$. Given $y_1,\dots,y_n \in H$, their Gram matrix is $G(y_1,\dots,y_n)_{ij} = \langle y_i, y_j\rangle$ and its determinant $g(y_1,\dots,y_n)$ is the Gram determinant. A linear variety is a translate $x + M$ of a subspace $M$.

Formalization targets

The goal is §3.10 Theorem 2, the dual approximation problem: for linearly independent $y_1,\dots,y_n \in H$ and constants $c_1,\dots,c_n$, among all $x \in H$ satisfying the constraints

there is a unique vector of minimum norm, and it has the form

The milestone list follows the chapter's own development: the projection theorem in its pre-Hilbert form (§3.3 Theorem 1) and classical form (§3.3 Theorem 2), the orthogonal decomposition $H = M \oplus M^\perp$ with $M^{\perp\perp} = M$ (§3.4 Theorem 1), the normal equations and Gram matrices (§3.6), the Gram determinant formula $\delta^2 = g(y_1,\dots,y_n,x)/g(y_1,\dots,y_n)$ for the minimum distance (§3.6 Theorem 1), best approximation by Fourier sums over orthonormal families (§3.7, §3.9), minimum norm over a linear variety (§3.10 Theorem 1), and the extension from subspaces to closed convex sets with its variational inequality characterization (§3.12 Theorem 1).

Significance

The dual approximation theorem converts an infinite-dimensional constrained minimum norm problem into an $n \times n$ linear system — the book's model example of finite reduction, applied there to minimum-energy control of a motor (§3.11) and, in Chapter 4, to every linear estimation problem: least squares, Gauss–Markov, and recursive (Kalman) estimation are all instances of these results in a Hilbert space of random variables.

All results here are classical and proved in the source; the mission's product is a faithful machine-checked development with reusable statements. Mathlib already contains close relatives of several milestones (orthogonal projection onto complete subspaces, Submodule.orthogonal), so part of the work is connecting the book's formulations to that library; the Gram determinant distance formula and the dual approximation theorem itself have no direct Mathlib counterpart.

Difficulty

The individual milestones are standard Hilbert space theory. The care is in the statements, not tricks: the pre-Hilbert version of the projection theorem asserts uniqueness and the orthogonality characterization without existence, while existence requires completeness and closedness — conflating the two versions produces unprovable or vacuous statements. The Gram determinant formula requires the $(n+1) \times (n+1)$ Gram matrix of the extended family $(y_1,\dots,y_n,x)$, where index bookkeeping (Fin.snoc) is easy to get wrong. In §3.12 the variational inequality $\langle x - k_0, k - k_0\rangle \le 0$ replaces the equality characterization valid for subspaces; the inequality direction is a known trap.

Formalization scope

The development commits to: real scalars (the book allows complex; this series does not), an abstract space H : Type with [NormedAddCommGroup H] [InnerProductSpace ℝ H] and [CompleteSpace H] exactly where the source assumes a Hilbert space; subspaces as Submodule ℝ H with explicit IsClosed hypotheses; finite families as Fin n → H; Gram matrices as Matrix (Fin n) (Fin n) ℝ via Matrix.of; minimum distances as infima (⨅) over coerced submodules. Best approximation statements are phrased as explicit inequalities ‖x - m₀‖ ≤ ‖x - m‖ rather than through any projection operator, so they are usable without choosing Mathlib's orthogonalProjection API. Statements deliberately carry no more hypotheses than the source: §3.3 Theorem 1 and the normal equations hold in any real inner product space; completeness appears only where existence is claimed.

Proofs are expected to lean on Mathlib's inner product space library; contributions of reusable bridging lemmas (e.g. between ⨅-formulations and orthogonalProjection) are welcome as child lemmas via proof sketches.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969. Chapter 3, pp. 46–77. ISBN 0-471-55359-X.

Motivation

Chapter 4 of Luenberger's Optimization by Vector Space Methods (Wiley, 1969) develops linear least-squares estimation as an application of the Hilbert space projection theorem formalized in Mission I of this series. The chapter's centerpiece is the classical Gauss–Markov theorem: among all linear unbiased estimators of an unknown parameter vector from noisy linear measurements, the estimator $(W^\top Q^{-1} W)^{-1} W^\top Q^{-1} y$ has minimum variance — componentwise, not merely in trace. This result is foundational for statistics and econometrics, and its Hilbert-space derivation is the cleanest known.

Setting

Measurements are modeled as $y = W\beta + \varepsilon$, where $y$ is an $m$-dimensional data vector, $W$ a known $m \times n$ matrix ($n < m$) with linearly independent columns, $\beta$ an unknown $n$-dimensional parameter vector, and $\varepsilon$ a random $m$-vector of measurement errors with $E\varepsilon = 0$ and covariance $E[\varepsilon\varepsilon^\top] = Q$, positive definite. A linear estimate is $\hat\beta = Ky$ for a constant $n \times m$ matrix $K$; it is unbiased when $E\hat\beta = \beta$ for every $\beta$, which holds iff $KW = I$. The optimality criterion is the error second moment $E\|\hat\beta - \beta\|^2$, and the book's key observation (p. 85) is that the problem splits into $n$ independent minimum norm problems, one per component, each solvable by the dual approximation theorem of Mission I.

Formally, randomness is carried by an abstract probability space: a measure space $(\Omega, \mu)$ with $\mu$ a probability measure, random vectors as functions $\Omega \to \mathbb{R}^m$ with explicit integrability hypotheses for all first and second moments, and $E[\cdot] = \int \cdot \, d\mu$.

Formalization targets

The goal is §4.4 Theorem 1 (Gauss–Markov): with $K_0 = (W^\top Q^{-1} W)^{-1} W^\top Q^{-1}$,

with error covariance

Milestones: the deterministic least-squares estimate $\hat\beta = (W^\top W)^{-1} W^\top y$ (§4.3 Theorem 1); the book's deterministic reduction — minimize the diagonal entries of $KQK^\top$ subject to $KW = I$ (p. 85); the minimum-variance estimate $\hat\beta = E[\beta y^\top] (E[y y^\top])^{-1} y$ for random $\beta$ (§4.5 Theorem 1); and the information-form identities $RW^\top(WRW^\top + Q)^{-1} = (W^\top Q^{-1}W + R^{-1})^{-1}W^\top Q^{-1}$ and $R - RW^\top(WRW^\top+Q)^{-1}WR = (W^\top Q^{-1}W + R^{-1})^{-1}$ (§4.5 Corollary 2).

Significance

The Gauss–Markov theorem justifies weighted least squares as the optimal linear unbiased procedure and is the standard benchmark against which biased and nonlinear estimators are measured. The minimum-variance estimate of §4.5 is the Bayesian counterpart with prior covariance $R$; the information-form identities connect the two and exhibit Gauss–Markov as the limit $R^{-1} \to 0$. Mission III builds the recursive (Kalman) estimator directly on these results.

All results are classical and proved in the source. Mathlib has mature measure-theoretic integration but, to date, no Gauss–Markov theorem and no linear estimation theory; the matrix milestones (trace reduction, information form) are also absent as stated. The probabilistic statements here are deliberately phrased with elementary integrals of products of real-valued components — no Bochner integration of vector-valued maps — so they are approachable with MeasureTheory.integral alone.

Difficulty

The subtlety is bookkeeping, not depth. Unbiasedness must be encoded as the algebraic constraint $KW = I$ (the book proves the equivalence with $E\hat\beta = \beta$ for all $\beta$); the componentwise variance claim is strictly stronger than the trace claim and requires the per-component minimum norm argument, not a single matrix inequality. Positive definiteness of $Q$ enters through invertibility of $W^\top Q^{-1} W$, which itself needs the linear independence of the columns of $W$ — dropping either hypothesis makes the goal false. In the probabilistic statements every integral needs an integrability hypothesis; the drafts supply integrability of all pairwise products of components, from which integrability of every derived expression follows.

Formalization scope

Random vectors are plain functions Ω → Fin m → ℝ on a MeasurableSpace Ω with a probability measure μ; second moments are hypotheses of the form ∫ ω, ε ω i * ε ω j ∂μ = Q i j with explicit Integrable assumptions; no independence, Gaussianity, or distributional assumptions are used anywhere. Matrices are Matrix (Fin m) (Fin n) ℝ with Mathlib's Matrix.PosDef, nonconstructive inverse ⁻¹, and mulVec. Norms on parameter space are written as explicit finite sums of squares, avoiding any ambiguity between Euclidean and supremum norms on pi types. The estimators under comparison are strictly linear ($\hat\beta = Ky$, no affine offset), exactly as in the source; §4.5's affine extension (its Problem 6) is out of scope.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969. Chapter 4, pp. 78–102. ISBN 0-471-55359-X.
• A. C. Aitken, On least squares and linear combination of observations, Proc. Roy. Soc. Edinburgh 55 (1935), 42–48 (the weighted-least-squares form of Gauss–Markov).

Motivation

Many convex programs impose inequalities valued in a vector space: componentwise inequalities, positive-semidefinite constraints, and families of ordered resource constraints are all instances of one cone order. Chapter 8 of David G. Luenberger's Optimization by Vector Space Methods develops a global theory for this setting. A perturbation of the constraint produces a convex value function, continuous linear functionals positive on the ordering cone become Lagrange multipliers, and a strict-feasibility condition yields an attained dual optimum. This mission formalizes the progression in §§8.2–8.6, culminating in the book's Lagrange Duality Theorem.

Setting

Let $X$ and $Z$ be real normed spaces, let $\Omega\subseteq X$ be a nonempty convex set, and let $P\subseteq Z$ be a convex cone. The cone induces the relation

A continuous linear functional $z^*\in Z^*$ is dual-positive when $z^*(p)\ge0$ for every $p\in P$. A map $G:X\to Z$ is cone-convex on $\Omega$ when its value at a convex combination is below the corresponding convex combination of its values in this cone order. The primal program is

where $f$ is real-valued and convex on $\Omega$.

For a multiplier $z^*$, the Lagrangian and its possibly infinite dual value are

The perturbed primal value $\omega(z)$ replaces the zero right-hand side by $G(x)\le_P z$. Lean represents $\omega$ and $\phi$ in EReal, so infeasible perturbations have value $+\infty$ and objectives unbounded below can have value $-\infty$ without arbitrary defaults.

Formalization targets

Main goal: Lagrange duality

Assume $P$ has nonempty interior, the primal value $\mu$ is finite, and there is a strictly feasible point $x_s\in\Omega$ with

Prove that a dual-positive $z_0^*$ exists and attains

If $x_0$ attains the primal infimum, also prove complementarity $z_0^*(G(x_0))=0$ and that $x_0$ minimizes $L(\,·\,,z_0^*)$ over $\Omega$.

Milestones

Five source milestones delimit the reusable theory. A closed convex cone is recovered from all dual-positive inequalities (§8.2, Proposition 1). The finite-height epigraph of the extended perturbation value is convex, and that value is antitone in the cone order (§8.3, Propositions 1–2). A Lagrangian saddle point is sufficient for primal feasibility and optimality when the cone is closed (§8.4, Theorem 2). Finally, multipliers for two perturbed right-hand sides bound the change in optimal objective value from both sides (§8.5, Theorem 1). The root then states §8.6, Theorem 1 rather than duplicating the equivalent multiplier theorem from §8.3.

Significance

The capstone provides both equality of optimal values and an attained multiplier. It applies to a single vector inequality, so finite systems of scalar inequalities and matrix-cone constraints fit the same statement once their ordering cones are supplied. Complementarity and Lagrangian minimization turn a primal optimizer and multiplier into a certificate. The sensitivity milestone additionally gives quantitative information about how the optimum changes when the constraint right-hand side moves.

Formalization produces a reusable cone-order layer independent of coordinate choices. coneLE, dualPositive, and ConeConvexOn can support later Kuhn–Tucker, vector optimization, and conic programming developments. The EReal value functions preserve infeasibility and unboundedness, two cases that a real-valued sInf encoding would collapse. This is a formalization mission for a classical theorem, not a claim that the underlying duality result is open.

Difficulty

The theorem's strict-feasibility condition is load-bearing. Feasibility $-G(x)\in P$ cannot replace interior feasibility, and nonempty interior of $P$ alone does not supply a Slater point. Equality constraints also cannot be converted into pairs of inequalities while retaining strict feasibility; Luenberger explicitly warns about this after the theorem.

The cone assumptions differ across milestones. The main strong-duality theorem does not require $P$ to be closed or pointed, whereas the bipolar and saddle-sufficiency statements require closedness. Using Mathlib's stronger ProperCone everywhere would silently add both topological and order hypotheses and shrink the theorem. Another tempting simplification is to make both value functions real. That loses the empty feasible set and unbounded dual subproblem, precisely the boundary cases used when comparing perturbations. The saddle inequalities must also have the correct orientation: the multiplier coordinate is maximized and the primal coordinate is minimized.

Formalization scope

The mission uses ConvexCone ℝ Z with a custom induced relation; it deliberately does not assume a lattice order on $Z$. Multipliers are continuous linear maps $Z\to\mathbb R$. The root assumes a real finite optimum through IsGLB and a real witness $\mu$, while lagrangeDualValue and perturbationValue retain EReal codomains. The strict condition is written as membership of $-G(x_s)$ in interior P, exactly matching $G(x_s)<_P0$.

No finite-dimensionality, reflexivity, completeness, closedness, or pointedness is added to the root. Closedness appears only where the source uses cone separation to recover primal feasibility. The sensitivity item assumes the two candidate points are feasible, their multipliers are dual-positive and complementary, and each point minimizes its shifted Lagrangian; these hypotheses spell out “solutions and corresponding multipliers” without relying on informal terminology.

Contributions may formalize cone separation, perturbation-value geometry, saddle certificates, or strong duality. Finite-dimensional orthant and positive-semidefinite specializations are useful corollaries but do not replace the general goal. Local multiplier rules, equality constraints, differentiable Kuhn–Tucker conditions, and Chapter 9's local theory remain outside this mission.

Selected references

• David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969, Chapter 8, §§8.2–8.6, pp. 214–225. Open Library record
• Stephen Boyd and Lieven Vandenberghe, Convex Optimization, Cambridge University Press, 2004, Chapter 5. Official book page

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.

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.

Motivation

Label correcting methods are the workhorse family of shortest-path algorithms — Dijkstra's method, Bellman–Ford, SLF/LLL variants and A* all fit the template analyzed in §2.3.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005), where shortest paths appear as the purely deterministic face of dynamic programming. The correctness proof (Prop. 2.3.1) is short on paper but genuinely nondeterministic — any node may be removed from the candidate list, children processed in any order — so a formal proof certifies a whole family of concrete algorithms at once.

Setting

A finite directed graph with arc set $\mathcal{A}$, real arc lengths $a_{ij}$, origin $s$ and destination $t \ne s$ (BertsekasSPGraph). Walks are nonempty node lists whose consecutive pairs are arcs (BertsekasIsWalkFrom), with length the sum of arc lengths (BertsekasWalkLength); the shortest distance is the infimum of walk lengths in the extended reals, $+\infty$ if no walk exists (BertsekasShortestDistance). The standing assumption of §2.3: every cycle has nonnegative length (negative arcs allowed).

The algorithm state (BertsekasLCState) carries labels $d_j \in \overline{\mathbb{R}}$, the scalar UPPER, and the candidate list OPEN. Initially $d_s = 0$, all other labels $\infty$, UPPER $= \infty$, OPEN $= \{s\}$. One iteration (BertsekasLCStep, nondeterministic): remove any $i$ from OPEN; for each child $j$ of $i$ in any order, if $d_i + a_{ij} < \min\{d_j, \text{UPPER}\}$ set $d_j := d_i + a_{ij}$, and put $j$ in OPEN if $j \ne t$, or update UPPER if $j = t$. The algorithm terminates when OPEN is empty.

Target

for every execution, under the nonnegative arc length assumption of §2.3 ($a_{ij} \ge 0$ for every arc) — BertsekasDP.label_correcting_correctness_of_nonneg_arcs (goal). Milestones: termination — no infinite execution exists, which needs only the weaker nonnegative-cycle assumption (label_correcting_terminates) — and the workhorse invariant that every finite label is the length of an actual walk from $s$, which needs neither (label_correcting_invariant).

The nonnegative-arc hypothesis is essential and not a formalization artifact: the algorithm prunes with the test $d_i + a_{ij} < \min\{d_j, \mathrm{UPPER}\}$, and with a negative arc a longer prefix can still reach $t$ more cheaply, so the pruned node is never entered into OPEN. An earlier version of this mission's goal carried only the nonnegative-cycle assumption of §2.1 and was disproved by the counterexample $s=0$, $t=2$, $a_{02}=1$, $a_{01}=2$, $a_{12}=-2$ (a graph with no cycles at all), where the algorithm terminates with $\mathrm{UPPER}=1$ while the shortest distance is $0$. Exercise 2.7 of the source treats the nonnegative-cycle case, which requires a modified algorithm.

Significance

Prop. 2.3.1 certifies simultaneously breadth-first search, Dijkstra (best-first), depth-first and small-label-first variants — every removal discipline is one refinement of the nondeterministic relation. Formally, the development contributes a reusable small-step framework for label-setting/correcting algorithms on which sharper results (Dijkstra's single-pass property, A* admissibility, §2.3.3) can later be built. The result is classical; the formal content is the induction along the nondeterministic step relation.

Difficulty

Termination is the subtle half: labels do not decrease monotonically along the run in an obvious well-founded way; the book's argument counts the finitely many distinct walk lengths below a bound — this needs the nonnegative-cycle assumption and a careful bound relating labels to simple-path lengths. The invariant proof must thread through the fold over children within a single step.

Formalization scope

Finite node type with decidable equality; arcs as a Finset of ordered pairs; lengths total on $V \times V$ (only arc values matter). The step relation is fully nondeterministic in pivot choice and child order (a permutation quantifier); correctness quantifies over all reachable terminal states — there is no fixed schedule to exploit. Distances live in EReal, so the no-path case is the honest empty infimum, not a sentinel. The trivializing risk of restricting to nonnegative arcs is avoided: only cycles are constrained.

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (Prop. 2.3.1, §2.3.) http://www.athenasc.com/dpbook.html
• E. W. Dijkstra, A note on two problems in connexion with graphs, Numer. Math. 1 (1959), 269–271. https://doi.org/10.1007/BF01386390
• R. Bellman, On a routing problem, Quart. Appl. Math. 16 (1958), 87–90. https://doi.org/10.1090/qam/102435

Motivation

In 1999 Artzner, Delbaen, Eber and Heath asked what a risk measure ought to satisfy, wrote down four axioms, and observed that the industry standard of the day -- Value-at-Risk -- fails one of them. The failing axiom is subadditivity: merging two positions should never require more capital than holding them apart. VaR can violate it, so under VaR a diversified book can appear riskier than its parts.

That observation did not stay academic. It is the reason the Basel framework moved its market-risk capital standard from Value-at-Risk to Expected Shortfall. Few results in mathematical finance have had a more direct regulatory consequence, and the mathematics is elementary enough to state completely.

Setting

A position is a payoff X : Fin (n+1) -> R across finitely many equally-weighted states, and a risk measure rho sends it to the capital that must be added to make it acceptable. Following Definition 2.4 of the paper, rho is coherent when it is translation-invariant, subadditive, positively homogeneous and monotone. Nonemptiness of the state space is carried in the index type so the worst case is always attained; no probability measure is needed for these four axioms, which is faithful to the paper -- Artzner et al. state T, S, PH and M without reference to one.

Value-at-Risk is defined here at an integer tolerance k rather than a probability level, which keeps the quantile unambiguous on a finite space: VaR X k is the least capital leaving at most k states in loss, corresponding to level k/(n+1).

The goal

The mission's goal theorem is the negative result: Value-at-Risk is not subadditive. A witness is 25 equiprobable states with X losing 100 in state 0 alone and Y losing 100 in state 1 alone. Each has one losing state in twenty-five, so at tolerance k = 1 both have VaR = 0; their sum loses in two states, exceeding the tolerance, so VaR (X+Y) 1 = 100 > 0 + 0. The witness was checked numerically before this mission was drafted; what is open is the Lean proof.

The milestones establish the positive contrast on the same footing: worst-case risk, the most conservative measure, satisfies all four axioms, so the failure is specific to VaR rather than inherent to risk measurement.

Source

P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, Coherent Measures of Risk, Mathematical Finance 9 (1999) 203-228. Axioms T, S, PH and M are Definition 2.4; the failure of subadditivity for VaR and the diversification consequence are discussed in Section 3.

Motivation

The separation theorem — certainty equivalence for linear-quadratic control with imperfect state information — is one of the celebrated structural results of stochastic control: the optimal controller splits into a least-squares estimator and the deterministic LQR actuator, designed independently. It underlies every LQG autopilot and Kalman-filter-based regulator. Section 5.2 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) proves it from the DP algorithm over information vectors, with Lemma 5.2.1 supplying the key fact that the estimation error is beyond the controller's influence. No formal analogue exists in Mathlib.

Setting

Linear dynamics and measurements

with quadratic cost $\mathbb{E}\big[x_N^\top Q_N x_N + \sum_{k<N}(x_k^\top Q_k x_k + u_k^\top R_k u_k)\big]$, $Q_k \succeq 0$, $R_k \succ 0$. The initial state and the zero-mean disturbances/noises are independent with finite ranges; independence is structural — the sample space is the product of an initial-state coordinate and per-stage noise coordinates (BertsekasLQGModel, BertsekasLQGSample, BertsekasLQGProb). A policy maps the realized measurement history $(z_0,\dots,z_k)$ to $u_k$; the closed-loop process is BertsekasLQGTraj, the expected cost BertsekasLQGCost. The estimator $\mathbb{E}[x_k \mid I_k]$ is an explicit conditional average (BertsekasCondExpVec, BertsekasLQGEstimate); the gains $L_k$ come from the time-varying Riccati recursion (BertsekasLQGRiccati, BertsekasLQGGain).

Target

— BertsekasDP.lqg_certainty_equivalence (goal). Milestone: Lemma 5.2.1 in pointwise form — the error $x_k - \mathbb{E}[x_k \mid I_k]$ is the same under any two policies, outcome by outcome (lqg_estimation_error_policy_independent).

Significance

This is the theorem that justifies designing estimator and controller separately — remove it and the entire LQG methodology loses its warrant. The formalization also yields the first machine-checked instance of the informational decomposition (control-dependent part + policy-independent error) that recurs throughout imperfect-information control. Notably the result needs no Gaussian assumption — only zero mean and independence — and the finite-support model makes that generality exact. The result is classical (Joseph–Tou 1961, Gunckel–Franklin 1963; the book's §5.2); the formal proof is new.

Difficulty

The heart is Lemma 5.2.1: showing the estimation error coincides, sample by sample, with the error of the control-free system — which requires proving that the observation-history σ-events under any policy coincide with those of the control-free system (controls are determined by the history, so they shift observations by a known amount). Then the DP argument over information histories must carry the quadratic decomposition through the backward recursion. Bookkeeping over histories-as-lists is the main formal burden; probability theory stays finite.

Formalization scope

Finite-support randomness (all expectations are finite sums); conditional expectation with the explicit junk value 0 on zero-probability events — the goal's hypothesis is accordingly restricted to outcomes of positive probability. Policies are functions of the measurement list only (equivalent to the book's information vector for deterministic policies, since past controls are recoverable from past measurements). Matrices are time-varying; positive definiteness of $R_k$ makes every matrix inverse in the gains genuine. Measurement noise covariance is not assumed positive definite — the estimator is the abstract conditional expectation, not the Kalman filter (whose recursive form, §5.2.1, would be a natural follow-up mission).

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (§5.2, Lemma 5.2.1.) http://www.athenasc.com/dpbook.html
• P. D. Joseph, J. T. Tou, On linear control theory, Trans. AIEE 80 (1961), 193–196. https://doi.org/10.1109/TAI.1961.6371743
• T. L. Gunckel, G. F. Franklin, A general solution for linear sampled-data control, J. Basic Eng. 85 (1963), 197–201. https://doi.org/10.1115/1.3656559

Motivation

Infinite-horizon dynamic programming is the mathematical core of Markov decision processes and reinforcement learning: Bellman equations, value iteration, policy iteration, and their guarantees. Chapter 7 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005) develops the finite-state theory in its cleanest generality — stochastic shortest path (SSP) problems first (Prop. 7.2.1–7.2.2), with discounted problems (Prop. 7.3.1) and average-cost problems (Prop. 7.4.1–7.4.2) derived from the SSP analysis. These propositions are cited throughout the MDP/RL literature as the base case of the theory; none of them exists in Mathlib.

Setting

States $1, \dots, n$ plus an implicit cost-free absorbing termination state $t$; finite nonempty control sets $U(i)$; costs $g(i,u)$; sub-stochastic transitions $p_{ij}(u) \ge 0$, $\sum_j p_{ij}(u) \le 1$, the deficit being the termination probability (BertsekasSSPModel). Operators

(BertsekasSSPPolicyOp, BertsekasSSPBellmanOp), $N$-stage costs by backward recursion with policy shift (BertsekasSSPNCost), and the survival mass $P\{x_m \ne t\}$ (BertsekasSSPSurvival). Assumption 7.2.1: for some $m > 0$, every admissible policy has survival mass $< 1$ from every state after $m$ stages. The discounted setting reuses the same model with stochastic rows and $0 < \alpha < 1$ (BertsekasDiscounted*); the average-cost setting adds a designated state $s$ with the avoidance probability of Assumption 7.4.1 (BertsekasSSPAvoidProb).

Target

Under Assumption 7.2.1, there is a vector $J^*$ with

and a stationary policy attaining $J^*$ — BertsekasDP.ssp_main_theorem (goal, Prop. 7.2.1(a),(b)). Milestones: 7.2.1(c) policy evaluation, 7.2.1(d) optimality iff greediness, 7.2.2 policy iteration, 7.3.1 the full discounted counterpart, 7.4.1 the average-cost Bellman equation, 7.4.2 average-cost policy iteration.

Significance

These are the convergence guarantees behind value iteration and policy iteration — the two algorithms at the root of dynamic programming practice and of RL analyses (Q-learning's target operator is exactly $T$). The SSP form is the strongest of the three: the discounted theory is its special case (termination with probability $1 - \alpha$ per stage) and the average-cost theory reduces to it through cycles at the recurrent state. Formalized, the chapter yields a reusable finite-MDP theory: monotone operators, $m$-stage contractions, and the machinery for later Vol. II material. All results are proved in the book; the formalization is new.

Difficulty

$T$ is not a one-stage contraction in the sup-norm under Assumption 7.2.1 — only an $m$-stage contraction, uniformly over the finitely many $m$-stage policy prefixes; extracting the uniform contraction factor $\rho < 1$ (via finiteness of the policy space) is the crux of the whole chapter. The limit of $N$-stage costs for nonstationary policies must be established, not assumed (tail-sum estimate $\rho^{\lfloor N/m \rfloor}$). For the average-cost results the associated-SSP construction (stop on reaching $s$) must be built inside the proof. The liminf phrasing of average-cost optimality is deliberate: for arbitrary nonstationary policies the Cesàro limit need not exist.

Formalization scope

Finite states Fin n, finite control type, constraint sets as Finsets with attained minima; no termination state in the carrier — termination is the sub-stochastic deficit, exactly as the book treats it computationally. Policies are sequences of stage policies (Markov); costs of nonstationary policies via the shift recursion. Convergence is Tendsto in the product topology (equivalently sup-norm, $n$ finite). Average cost uses real liminf and division with the $N = 0$ term junk-valued at 0 (irrelevant at infinity). The discounted theorem packages parts (a)–(e) in one statement mirroring Prop. 7.3.1.

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (§7.1–7.4.) http://www.athenasc.com/dpbook.html
• D. P. Bertsekas, J. N. Tsitsiklis, An analysis of stochastic shortest path problems, Math. Oper. Res. 16 (1991), 580–595. https://doi.org/10.1287/moor.16.3.580
• M. L. Puterman, Markov Decision Processes, Wiley, 1994. https://doi.org/10.1002/9780470316887

A performance guarantee for a simple replenishment rule

When replenishment takes several periods, an inventory decision commits stock before the demand that will consume it is known. Too much stock incurs holding costs; too little loses sales. An optimal decision can depend on the entire pipeline of outstanding orders. A rule with only two adjustable parameters is easier to implement, but its simplicity alone gives no guarantee on the cost it can incur.

Capped base-stock policies combine an inventory-position target with a maximum order quantity. The class was introduced and analyzed by Xin (2021). The present target is the finite-lead-time guarantee in Linwei Xin's Capped Base-Stock Policies: A 2.33-Approximation, specifically the author-supplied manuscript with source label thm-main. A public listing of the paper identifies the July 17, 2026 working paper; the supplied text is the authoritative version for this formalization.

Demand, stock, and delayed orders

Periods are discrete. Demand is a sequence of independent, identically distributed nonnegative real random variables $D_t$ with finite, strictly positive mean $\mu$. The deterministic lead time is an integer $L\ge1$. Holding and lost-sales rates are $h>0$ and $p>0$.

At the beginning of period $t$, $I_t$ is on-hand inventory and $x_{1,t},\ldots,x_{L,t}$ are outstanding orders, with $x_{1,t}$ due immediately. That arrival is received, an order $q_t\ge0$ is placed, demand is realized, and costs are charged. The new order arrives $L$ periods later. The equations are

Here $u^+=\max\{u,0\}$. Unfilled demand is lost rather than backlogged. With $\ell_t=(D_t-I_t-x_{1,t})^+$, the period cost is $hI_{t+1}+p\ell_t$. Initial inventory and every pipeline coordinate are zero. A nonanticipative policy chooses orders using only information available before the current demand; policies may depend on the entire observed past and on independent private randomization.

For a policy $\pi$, its long-run expected average cost is

The capped rule is $q_t=\min\{(S-I_t-\sum_{i=1}^Lx_{i,t})^+,r\}$ for finite $S,r\ge0$. Write $C^*_{\rm CBS}=\inf_{S,r\ge0}C(\pi_{S,r})$. Ordinary base stock is already included by taking $r=S$; no infinite order cap is required.

Formalization targets

For $0\le r\le\mu$ and $m\ge1$, set

Empty sums are zero. The lower certificate is

The pair $(0,0)$ is feasible. Both horizon constraints are retained. With

the goal is Theorem 1's complete assertion:

The exact rational constant is used; the title's 2.33 is a rounded description. Multiplicative inequalities also make sense when the optimal cost is zero.

Five supporting targets reproduce selected source statements: Proposition 1's lower-certificate bound; Proposition 2's finite-cap cost conclusion; Lemma 2's bound on a consecutive block in the greedy recursion; Proposition 3's ordinary-base-stock cost bound; and Proposition 4's two-branch inequality. The finite-cap and ordinary-base-stock parameters remain exactly $(S,r)=((L+1)r+z,r)$ and $S=(L+1)r+2z$, respectively. Labels accompany the printed numbering so the supplied source is unambiguous.

What completing the mission establishes

The result gives a uniform cost guarantee for this policy class across all positive holding and penalty rates, every positive integer lead time, and arbitrary nonnegative demand laws with finite positive mean. It bounds the infimum of costs over the policy parameters; it does not by itself provide an algorithm for selecting parameters or assert that the infimum is attained. At $L=1$ the displayed coefficient is 2, while its uniform upper bound is $7/3$.

The manuscript supplies mathematical proofs. This mission asks for checked proofs of their formal statements. Compiling the declarations confirms that they are well formed, not that the claims are proved. A completed development would provide reusable delayed-inventory dynamics, measurable history policies, average-cost optimization objects, finite-horizon demand envelopes, and policy-comparison results.

Where the formal work lies

The pipeline carries consequences of past decisions across multiple demand periods. Nonanticipativity and independence must be stated precisely before expectation and convexity arguments can be used. Also, existence of a stationary distribution alone does not identify its expected cost with a long-run cost from an empty initial system. The manuscript invokes stationary results from prior inventory work, including Xin and Goldberg (2016), and uses stationary CBS quantities in intermediate arguments. Their needed hypotheses and connections to the original objective require proof within a complete development.

The two cost bounds depend on both coordinates of a feasible lower-certificate pair. Losing either horizon constraint changes that certificate. Replacing it with an arbitrary scalar lower bound or assuming the policy comparisons would remove substantive parts of the result.

Formalization scope and conventions

Stock, orders, and demand take arbitrary nonnegative real values. Time is represented from zero in the operational model, corresponding to period one in the manuscript. The formal representation uses a canonical probability model with independent demand coordinates and an independent uniform private seed; measurable time-dependent decision functions use only preceding demands and that seed. Connecting arbitrary standard-Borel randomized controls to this canonical realization is a representation obligation. The zero-start optimum ranges over these general history policies, not only stationary or capped policies.

Expected nonnegative costs, their upper limits, and cost infima are represented in the extended nonnegative reals. Thus a policy with infinite expected cost does not acquire a fictitious zero value through a totalized real integral. The finite-horizon envelope expectations use the original integrable demand law. The greedy lemma uses integer-indexed sequences so subtraction of earlier times has no natural-number truncation; its blocks are nonempty, as required to define their maximum.

Definitions contain no unproved facts. In particular, stationarity, convergence from the empty initial state, lower bounds, and upper policy comparisons are not fields assumed by the model. Contributions to these intermediate obligations and to any of the five source targets support the central theorem.

Selected references

• Linwei Xin, Capped Base-Stock Policies: A 2.33-Approximation, working paper, 2026. SSRN listing. Author-supplied LaTeX is authoritative: Theorem 1 (thm-main), Proposition 1 (lemma-lb), Proposition 2 (prop-finite-cap-bound), Lemma 2 (lem-greedy-window), Proposition 3 (prop-base-stock-bound), Proposition 4 (lem-two-branch). Source SHA-256: f353793c255e1ebed5f3ec541037284bd926183e3e5b71941f13e79c2d67cb7a.
• Linwei Xin, Technical Note—Understanding the Performance of Capped Base-Stock Policies in Lost-Sales Inventory Models, Operations Research 69(1), 61–70, 2021. DOI.
• Linwei Xin and David A. Goldberg, Optimality Gap of Constant-Order Policies Decays Exponentially in the Lead Time for Lost Sales Models, Operations Research 64(6), 1556–1565, 2016. DOI.

Motivation

The discrete-time Riccati equation is the central object of linear-quadratic optimal control — the design equation behind LQR/LQG controllers in every modern control stack. Proposition 4.4.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005, §4.1) packages its asymptotic theory: under controllability and observability the Riccati iteration converges to the unique positive semidefinite solution of the algebraic Riccati equation and the resulting closed loop is stable. Alongside it, Lemma 4.2.1 of §4.2 develops K-convexity, the analytical engine behind Scarf's optimality of $(s,S)$ inventory policies — a foundational result of operations research. Neither the Riccati asymptotics nor K-convexity exists in Mathlib.

Setting

Matrices $A \in \mathbb{R}^{n\times n}$, $B \in \mathbb{R}^{n\times m}$, $Q = C^\top C \succeq 0$, $R \succ 0$. The Riccati operator (BertsekasRiccatiMap)

$(A,B)$ is controllable if $[B, AB, \dots, A^{n-1}B]$ has rank $n$ (BertsekasControllablePair); $(A,C)$ is observable if $(A^\top, C^\top)$ is controllable (BertsekasObservablePair). Separately, $g : \mathbb{R} \to \mathbb{R}$ is $K$-convex (BertsekasKConvex, Def. 4.2.1) if $K + g(z+y) \ge g(y) + \tfrac{z}{b}(g(y) - g(y-b))$ for all $z \ge 0$, $b > 0$, $y$.

Target

with $L = -(B^\top P B + R)^{-1} B^\top P A$ — BertsekasDP.riccati_convergence_stability (goal). Milestones: Lemma 4.2.1(a)–(d) (kconvex_of_convex, kconvex_combination, kconvex_expectation, kconvex_sS_structure), culminating in the $(s,S)$ structure theorem for continuous coercive $K$-convex functions.

Significance

The Riccati result is the mathematical license behind steady-state LQR design: it guarantees the design equation has one meaningful solution, that iterating the finite-horizon recursion finds it, and that the resulting feedback is stabilizing. Formally it would seed a Mathlib-adjacent theory of matrix fixed-point iterations, positive semidefinite order, and spectral-radius stability. The K-convexity milestones are self-contained real analysis, each of independent reuse value for inventory theory; part (d) is the engine of $(s,S)$-policy optimality. All results are classical and proved in the book; the formal work is new.

Difficulty

The Riccati proof interleaves monotonicity of $F$ on the psd cone, boundedness from controllability (a steering argument), positivity from observability, and stability extracted from the fixed-point identity via a Lyapunov argument — several pieces of matrix analysis (psd order, congruence, Schur-type manipulations, spectral radius vs. convergence of powers) that must be built or located in Mathlib. The naive route of diagonalizing $A$ fails: nothing is symmetric about $A + BL$. For Lemma 4.2.1(d), the difficulty is that $g$ is not convex: the minimizer structure must come from the K-convexity inequality applied at carefully chosen points, plus continuity and coercivity.

Formalization scope

Real matrices over Fin n; Matrix.PosSemidef/PosDef; matrix inverse is Mathlib's total inverse (zero on singular input — harmless here since $B^\top P B + R \succ 0$ along the relevant iterates, which the proof must establish); convergence in the entrywise topology; eigenvalues via spectrum ℂ of the complexified matrix, all strictly inside the unit circle. Rank-based controllability exactly as Def. 4.1.1. K-convexity is stated for all real $K$; note $K \ge 0$ is forced whenever it is satisfiable ($z = 0$), and the expectation milestone is stated for finitely supported disturbances (integrability automatic).

Selected references

• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (Prop. 4.4.1, Def. 4.1.1, §4.2, Lemma 4.2.1.) http://www.athenasc.com/dpbook.html
• R. E. Kalman, Contributions to the theory of optimal control, Bol. Soc. Mat. Mexicana 5 (1960), 102–119.
• H. Scarf, The optimality of (S, s) policies in the dynamic inventory problem, in Mathematical Methods in the Social Sciences, Stanford Univ. Press, 1960.

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

Two-stage stochastic linear programming with recourse models a decision made before uncertainty resolves (the first-stage variables $x$) followed by a corrective decision made after (the second-stage, or recourse, variables $y$). Solving such a program means minimizing $c^{\mathsf T}x + Q(x)$, where $Q(x)$ is the expected cost of the best recourse action given $x$ -- an object defined only implicitly, as the value of an embedded linear program that must be solved (or bounded) for every realization of the uncertain data. Before any algorithm for this problem can be justified -- the L-shaped method, stochastic decomposition, scenario decomposition, all developed in later chapters of Birge & Louveaux, Introduction to Stochastic Programming (Springer, 2011) -- one needs to know that $Q$ is well-behaved enough to optimize over at all: that the feasible region is closed and convex, that $Q$ itself is a finite, Lipschitz, convex function on it, that an optimal solution is actually attained rather than only approached in the limit, and finally what an optimality condition for the resulting nonsmooth convex program even looks like. This mission formalizes exactly that foundational layer, Chapter 3, Section 3.1 of the book.

Setting

Fix natural numbers $n_1, n_2, m_1, m_2$ and a finite scenario count $K$. A two-stage recourse instance consists of first-stage data $A \in \mathbb{R}^{m_1 \times n_1}$, $b \in \mathbb{R}^{m_1}$, $c \in \mathbb{R}^{n_1}$, a fixed recourse matrix $W \in \mathbb{R}^{m_2 \times n_2}$, and, for each scenario $k = 1,\dots,K$, a cost vector $q_k \in \mathbb{R}^{n_2}$, a right-hand side $h_k \in \mathbb{R}^{m_2}$, a technology matrix $T_k \in \mathbb{R}^{m_2 \times n_1}$, and a probability $p_k \ge 0$ with $\sum_k p_k = 1$ (Eq. (1.1)). The first-stage feasible region is $K_1 = \{x \mid Ax = b,\ x \ge 0\}$.

For a fixed $x$ and scenario $k$, the second-stage value is

(Eq. (1.6)), taken as an extended real: $+\infty$ if no feasible $y$ exists, $-\infty$ if the inner program is unbounded below. The expected recourse value is $Q(x) = \sum_k p_k\, Q(x,\xi_k)$ (Eq. (1.3)), combined so that $+\infty + (-\infty) = +\infty$ -- the book's own convention (p. 109): infeasibility in one scenario is treated as fatal even if another scenario is unboundedly favorable. The second-stage feasibility set is $K_2 = \{x \mid Q(x) < \infty\}$, and the deterministic-equivalent objective is $z(x) = c^{\mathsf T}x + Q(x)$ (Eq. (1.2)). For $x$ with $Q(x)$ finite, the subdifferential $\partial Q(x)$ is the set of $\eta$ satisfying $Q(x) + \eta^{\mathsf T}(y-x) \le Q(y)$ for every $y$ (p. 115).

A simple-recourse instance is the special case $W = [I,-I]$: the recourse cost splits as $q = (q^+,q^-)$, and $Q(x)$ decomposes componentwise via the closed form of Eq. (1.9)-(1.10) using the (left- and right-limit) distribution functions $F_i^-, F_i^+$ of each $h_i$.

Formalization targets

Goal -- Chapter 3, Theorem 9 (p. 116)

given that (1.2) has a finite optimal value. This is the KKT-style necessary and sufficient optimality condition for the two-stage recourse LP, and the weakest of the mission's targets in the sense that everything else supports it: convexity and finiteness of $Q$ (Theorem 6) are what make the left-to-right implication meaningful, closedness/convexity of $K_2$ (Theorem 5) makes the feasible region well-posed, and attainment (Theorem 8) is what makes "$x^*$ is optimal" a statement about a point that exists rather than an infimum that may not be reached.

Supporting milestones

• Theorem 5(a) (p. 111): $K_2$ is closed and convex.
• Theorem 6(a) (p. 112): $Q$ is finite on $K_2$, and Lipschitzian and convex there.
• Theorem 8 (p. 115): under boundedness of $K_1 \cap K_2$ or eventual linearity of $Q$ along recession directions, a finite optimal value is attained.
• Corollary 10 (p. 116): Theorem 9 specialized to simple recourse, with $\partial Q(x^*)$ replaced by its explicit componentwise description.

Significance

Theorem 9 is the hinge on which the rest of the book's algorithmic chapters turn. The L-shaped method (Chapter 5) is a cutting-plane scheme whose cuts are literally elements of $\partial Q(x)$; stochastic decomposition and sampling-based methods use the same subdifferential structure with estimated cuts; the differentiable specialization (Eq. (1.14), $c + \nabla Q(x^*) = A^{\mathsf T}\lambda^* + \mu^*$) underlies nonlinear-programming approaches to the smooth case. None of this is meaningful without first knowing $Q$ is convex, finite where it needs to be, and that a minimizer exists to characterize. Formalizing this mission's four milestones from the actual definition of $Q$ as an embedded linear program's value -- rather than assuming these properties -- is exactly the content the book itself proves (or, for Theorem 6, explicitly cites to Wets [1972] and Kall [1976] rather than proving); this mission asks for genuine Lean proofs of Theorems 5, 8, 9 and Corollary 10 from the LP structure of $Q$, and records Theorem 6 as a stated (not re-derived) input, matching the book's own presentation.

Difficulty

The obvious shortcut is to treat $Q$ as an opaque convex function and apply a textbook convex-KKT theorem off the shelf. This fails to capture what Theorem 9 actually is: a statement about the specific function $Q(x) = \sum_k p_k \min_y\{q_k^{\mathsf T}y \mid Wy = h_k - T_k x,\ y \ge 0\}$, built from finitely many parametric linear programs, each of which can be infeasible ($Q(x,\xi_k) = +\infty$) or unbounded ($Q(x,\xi_k) = -\infty$) depending on $x$. Convexity of $Q$ must come from convexity of the value function of a parametric LP in its right-hand side (the book's Theorem 2 argument: a convex combination of optimal solutions at two right-hand sides is feasible, hence suboptimal, at the combined right-hand side) -- not from an assumed hypothesis. Handling $\pm\infty$ correctly is a second, easy-to-miss source of error: the book fixes an explicit, non-default convention ($+\infty$ dominates $-\infty$) for combining per-scenario values, the opposite of the convention Mathlib's own extended-real arithmetic uses, so any formalization that reaches for EReal's built-in addition to aggregate $Q$ silently states a different theorem. Theorem 8's attainment condition is a genuine existence result, not an automatic consequence of convexity: continuity alone does not give attainment on an unbounded feasible region, and the book's own counterexample (Eq. (1.11), a negative-exponential tail with infimum $0$ attained by no finite $x$) shows the boundedness/recession hypotheses are load-bearing.

Formalization scope

The scenario set is modeled as Fin K, a finite discrete random variable, matching Section 3.1b's development; under this model "$\xi$ has finite second moments" (the standing hypothesis of Theorems 4-11 in the general, possibly-continuous case) holds automatically and so does not appear as a separate hypothesis anywhere in this mission. Q(x,\xi_k) is defined as an EReal via sInf of the second-stage LP's feasible objective values -- sInf of the empty set is ⊤, and of a set unbounded below is ⊥ -- and is genuinely derived from that inner minimization rather than assumed convex; this rules out the chapter's trivializing formalization, which the paper-level triage explicitly warns against: taking Q(x) as an opaque convex-function hypothesis instead of deriving its properties from the inner LP's structure. Aggregating the $K$ per-scenario values into $Q(x)$ uses a bespoke bookAdd operation implementing the book's stated convention $+\infty+(-\infty)=+\infty$, since Mathlib's EReal addition is defined with the opposite convention ($\bot+\top=\top+\bot=\bot$). $\partial Q(x)$ is the ordinary subgradient-inequality set for this extended-real-valued function.

Theorem 8's condition (b) is stated with the book's own quantifier structure: the threshold $\bar\lambda$ and the recession value depend on the point $x$ and direction $v$ exactly as written, with no strengthening. Theorem 6(a)'s Lipschitz bound is stated, not derived -- the book itself cites it to Wets [1972] and Kall [1976] without proof -- so a faithful Lean proof of that milestone is expected to remain out of scope for this mission. Corollary 10 similarly takes the closed form of $\partial Q_i(x)$ from Eq. (1.10) as a hypothesis on an abstract $Q$, matching how the book itself uses (1.10) as an already-established fact rather than re-deriving it from the second-stage LP in the corollary's own proof. Theorem 11's subdifferential-decomposition result ($\partial Q(x) = E_\omega[\partial Q(x,\xi(\omega))] + N(K_2,x)$) is deliberately left out of this mission's scope: it is not needed by Theorem 9's own proof, and its normal-cone term would require relatively-complete-recourse machinery this mission does not otherwise need. No prior-art match was found on the platform: VectorSpaceOpt.fenchel_duality and the Luenberger-derived VectorSpaceOpt.generalized_kuhn_tucker / kkt_complementary_slackness family use a differentiable (Gateaux-derivative) or conjugate-function KKT model over general normed spaces, not this chapter's finite-dimensional, possibly-nondifferentiable subgradient formulation over the specific polyhedral set $K_1$, so none is a faithful match and all items here are original drafts.

Selected references

• J.R. Birge and 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
• R.J-B. Wets, "Programming Under Uncertainty: The Equivalent Convex Program," SIAM Journal on Applied Mathematics 14 (1966), 89-105 (Lipschitz continuity of the recourse function, cited by the book as Wets [1972] for the closely related result used in Theorem 6). https://doi.org/10.1137/0114008
• D.P. Walkup and R.J-B. Wets, "Stochastic Programs with Recourse," SIAM Journal on Applied Mathematics 15 (1967), 1299-1314 (finiteness of the recourse function and coincidence of the possibility and expectation feasibility sets, underlying Proposition 3 and Theorem 4). https://doi.org/10.1137/0115113

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.