The OR Formalization Drive

Completed

Operations Research Probability Statistics+1·Captain: Shuze Chen

The Markov Chain Central Limit TheoremResearch Paper

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

\sqrt{n}(\bar f_n - E_\pi f) \to_d N(0, \sigma_f^2).

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.

154 thms18 active usersReviewed

Completed

Experimental Design Operations Research Probability+2·Captain: Shuze Chen

Treatment Locality in A/B TestingResearch Paper

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.

42 thms4 active users

Completed

Functional Analysis Operations Research Optimization·Captain: Shuze Chen

Vector Space Methods I: Minimum Norm Problems in Hilbert SpaceTextbook

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

\langle x, y_i\rangle = c_i, \qquad i = 1,\dots,n,

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

x_0 = \sum_{i=1}^n \beta_i\, y_i, \qquad \text{where} \qquad \sum_{j=1}^n \beta_j \langle y_j, y_i\rangle = c_i .

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.

10 thms1 active userReviewed

Completed

Functional Analysis Operations Research Optimization+2·Captain: Shuze Chen

Vector Space Methods II: Gauss–Markov EstimationTextbook

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}$ ,

K_0 W = I, \qquad E\big[(K_0 y - \beta)_i^2\big] \le E\big[(K y - \beta)_i^2\big] \quad \text{for every } i \text{ and every } K \text{ with } KW = I,

with error covariance

E\big[(K_0 y - \beta)(K_0 y - \beta)^\top\big] = (W^\top Q^{-1} W)^{-1}.

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).

8 thms1 active userReviewed

Operations Research Theoretical Computer Science·Captain: Shuze Chen

The 4/3 Conjecture for Metric TSPOpen Problem

Motivation

The traveling salesman problem — visit $n$ cities by the cheapest round trip — is the most widely known problem in combinatorial optimization, and its central open question concerns a linear program. The subtour-elimination relaxation (the Held–Karp bound) replaces tours by fractional edge weights, and both in theory and in practice (it powers the lower bounds inside the Concorde solver) it is remarkably close to the true optimum. How close, in the worst case, is the integrality gap of the relaxation: the supremum of $\mathrm{OPT}/\mathrm{LP}$ over metric instances. Explicit instance families push the gap up to $4/3$ ; the best proven upper bound sits just barely below $3/2$ . The 4/3 conjecture — the gap is exactly $4/3$ — has been the benchmark question of approximation algorithms for four decades.

Timeline

1954. Dantzig, Fulkerson, and Johnson solve a 49-city instance by hand with the cutting planes that become the subtour-elimination LP.
1970–1971. Held and Karp introduce the 1-tree/Lagrangian bound and show it equals the subtour LP value — since then, "the Held–Karp bound".
1976/1978. Christofides, and independently Serdyukov, give the $3/2$ -approximation: minimum spanning tree plus a matching on odd-degree vertices.
1980. Wolsey (Math. Prog. Study 13) shows Christofides' analysis goes through against the LP: $\mathrm{OPT} \le \frac{3}{2}\,\mathrm{LP}$ , so the integrality gap is at most $3/2$ . Shmoys and Williamson (IPL 1990) rediscover this via a monotonicity property.
1995. Goemans (Math. Programming 69) analyzes the worst-case ratios of TSP relaxations and states the $4/3$ conjecture explicitly; the $4/3$ lower-bound families (three parallel paths) are by then folklore.
2011–2014. For graph metrics (shortest-path metrics of unweighted graphs) the barrier breaks: Oveis Gharan–Saberi–Singh and Mömke–Svensson beat $3/2$ , and Sebő–Vygen (Combinatorica 2014) reach $7/5$ — the conjectured-optimal shape of progress, but only for a special class.
2020–2022. Karlin, Klein, and Oveis Gharan prove a $3/2 - \varepsilon$ approximation for general metric TSP (STOC 2021) and then an integrality-gap bound $\gamma \le 3/2 - \varepsilon$ with $\varepsilon > 10^{-36}$ (FOCS 2022), via max-entropy sampling of spanning trees and strongly Rayleigh distributions — the first general improvement over Wolsey in forty years, by an astronomically small margin.
Today. The gap between the $4/3$ lower bound and the $3/2 - 10^{-36}$ upper bound is the conjecture. For half-integral LP solutions — where the conjectured extremal instances live — the bound has been pushed to $1.4983$ (Gupta, Lee, Li, Mucha, Newman, and Sarkar, via matroid-based rounding).

Setting

An instance on $n \ge 3$ cities is a cost function $c$ assigning to each ordered pair of cities $u, v$ a real cost $c(u,v)$ , required to be a metric cost: symmetric ( $c(u,v) = c(v,u)$ ), zero on the diagonal ( $c(v,v) = 0$ ), and satisfying the triangle inequality $c(u,w) \le c(u,v) + c(v,w)$ . Nonnegativity follows; distinct cities at distance zero are allowed, as usual for metric TSP.

A tour visits every city exactly once and returns to its start. Formally a tour is given by an ordering: a permutation $\pi$ of the cities, traversed as $\pi(0), \pi(1), \dots, \pi(n-1)$ and back to $\pi(0)$ ; its cost $\mathrm{tourCost}(c, \pi)$ is the sum of the costs of consecutive steps, and $\mathrm{OPT}(c)$ — written tspOpt c — is the minimum over all orderings.

The subtour-elimination (Held–Karp) relaxation replaces the tour by a fractional edge weight $x(u,v)$ for each pair of cities. A weight vector $x$ is feasible (IsHeldKarp x) when it is symmetric with zero diagonal, has entries in $[0,1]$ , gives every city fractional degree two ( $\sum_u x(v,u) = 2$ ), and crosses every nontrivial cut at least twice: for every set $S$ of cities other than $\emptyset$ and all cities, $\sum_{u \in S} \sum_{v \notin S} x(u,v) \ge 2$ . The Held–Karp bound hkValue c is the infimum of $\frac{1}{2}\sum_u \sum_v c(u,v)\,x(u,v)$ over feasible $x$ (the double sum counts each edge twice, hence the $\frac12$ ). The incidence vector of any tour is feasible, so $\mathrm{LP} \le \mathrm{OPT}$ always.

Formalization targets

Goal — the 4/3 conjecture

\mathrm{OPT}(c) \;\le\; \tfrac{4}{3}\,\mathrm{LP}(c) \qquad \text{for every } n \ge 3 \text{ and every metric cost } c.

Together with the known lower-bound families this says the integrality gap is exactly $4/3$ . The goal carries no algorithm and no constant to improve: it is the terminal statement of the ladder, open in both directions (a proof or a counterexample instance would each settle it).

Milestones — the known ladder

Five results over the same definitions: the relaxation is valid ( $\mathrm{LP} \le \mathrm{OPT}$ ); instance families force the gap arbitrarily close to $4/3$ ; tree doubling gives $\mathrm{OPT} \le 2\,\mathrm{LP}$ ; Wolsey's theorem gives $\mathrm{OPT} \le \frac{3}{2}\,\mathrm{LP}$ , the classical upper bound; and the Karlin–Klein–Oveis Gharan record $\mathrm{OPT} \le (\frac{3}{2} - \varepsilon)\,\mathrm{LP}$ for some $\varepsilon > 10^{-36}$ (FOCS 2022). The last milestone is a statement-level target: its known proof (max-entropy sampling, strongly Rayleigh polynomials) is far beyond current formalization practice, so the mission's usable proving frontier remains Wolsey — the milestone records the state of the art as a formal statement.

Significance

The 4/3 conjecture is the reference open problem of approximation algorithms: the quality of the subtour LP calibrates every algorithmic advance on TSP, and the conjectured extremal instances guide the search for better rounding schemes. The bound is also what practical solvers actually compute — branch-and-cut on this LP solves instances with tens of thousands of cities — so the conjecture is a statement about the observed tightness of the world's most-used combinatorial lower bound.

Nothing in this circle exists in any proof assistant: Mathlib has no TSP, no LP relaxations, no polyhedral combinatorics of tours. The mission's milestones force the base layer into existence — tours over Equiv.Perm, cut constraints over Finset, and, for the upper bounds, the parity and tree arguments (spanning trees against the LP, T-joins for the $3/2$ bound) whose infrastructure is reusable for matching theory and network design far beyond TSP.

Difficulty

The naive plan — round the LP solution to a tour — has no known analysis losing less than $3/2$ in general, and the half-integral extremal instances show the hard cases are structured and simple-looking at once. Christofides' matching argument is provably stuck at $3/2$ against the LP; forty years of work moved the constant by $10^{-36}$ , and that advance needed an entirely new probabilistic toolkit. On the other side, no instance family with ratio above $4/3$ has ever been found despite extensive computational search over small instances (Benoit–Boyd and successors). Both directions of the goal are genuinely open territory.

Formalization scope

The Lean model commits to: cities Fin n; costs c : Fin n → Fin n → ℝ with IsMetricCost (symmetry, zero diagonal, triangle inequality — nonnegativity is derived, and semimetrics are included as in the standard statement of the conjecture); tours as orderings π : Equiv.Perm (Fin n) traversed cyclically via finRotate, so every permutation denotes a Hamiltonian cycle and every Hamiltonian cycle is denoted; both optimal values as sInf over nonempty, bounded-below sets of reals, so they are genuine minima for n ≥ 3. The hypothesis 3 ≤ n is load-bearing: for n ≤ 2 the degree-2 constraints are infeasible, sInf ∅ = 0 by convention, and the bounds would be false — every theorem therefore carries it.

Welcome contributions: the milestones in any order — held_karp_le_opt is the natural entry point (the tour's incidence vector crosses every cut at least twice); integrality_gap_lower_bound needs the three-path instance family and a case analysis on its tours; tree_doubling_bound needs spanning trees against the LP; wolsey_bound adds the T-join/parity argument and is the summit. Reusable infrastructure — spanning tree polytopes, T-joins, Eulerian traversals, cut lemmas — is welcome as platform theorems. Graph-TSP ( $7/5$ ), path TSP, and asymmetric TSP are deliberately left to future missions; the Karlin–Klein–Oveis Gharan bound is stated as a milestone, but its sampling machinery is expected to arrive, if ever, as shared infrastructure built over many contributions.

Selected references

G. Dantzig, R. Fulkerson, S. Johnson, Solution of a large-scale traveling-salesman problem, Oper. Res. 2 (1954).
M. Held, R. Karp, The traveling-salesman problem and minimum spanning trees, Oper. Res. 18 (1970); Part II, Math. Programming 1 (1971).
N. Christofides, Worst-case analysis of a new heuristic for the travelling salesman problem, CMU report (1976); A. Serdyukov, Upravlyaemye Sistemy 17 (1978).
L. Wolsey, Heuristic analysis, linear programming and branch and bound, Math. Prog. Study 13 (1980). doi:10.1007/BFb0120913
D. Shmoys, D. Williamson, Analyzing the Held-Karp TSP bound: a monotonicity property with application, Inf. Process. Lett. 35 (1990). doi:10.1016/0020-0190(90)90028-V
M. Goemans, Worst-case comparison of valid inequalities for the TSP, Math. Programming 69 (1995). doi:10.1007/BF01585563
A. Sebő, J. Vygen, Shorter tours by nicer ears, Combinatorica 34 (2014). arXiv:1201.1870
A. Karlin, N. Klein, S. Oveis Gharan, A (slightly) improved approximation algorithm for metric TSP, STOC 2021. arXiv:2007.01409
A. Karlin, N. Klein, S. Oveis Gharan, A (slightly) improved bound on the integrality gap of the subtour LP for TSP, FOCS 2022. arXiv:2105.10043
V. Traub, J. Vygen, Approximation Algorithms for Traveling Salesman Problems, Cambridge University Press, 2024. book page

23 thms1 active userReviewed

Operations Research Theoretical Computer Science·Captain: Shuze Chen

The k-Server ConjectureOpen Problem

Motivation

The $k$ -server problem was introduced by Manasse, McGeoch, and Sleator (STOC 1988 / J. Algorithms 1990) as a common generalization of paging, weighted caching, and related sequential decision problems, and their $k$ -server conjecture has since become the central open question of competitive analysis. The conjecture asserts that a single ratio — exactly $k$ — governs deterministic online server management on every metric space.

Timeline

1985. Sleator and Tarjan introduce competitive analysis — an online algorithm judged against the offline optimum on every input — for list update and paging, and ask for a theory of such guarantees.
1988–1990. Manasse, McGeoch, and Sleator introduce the $k$ -server problem (STOC 1988; J. Algorithms 1990) and settle its extremes: no deterministic algorithm beats ratio $k$ on any space with more than $k$ points (Corollary 7), two servers admit a $2$ -competitive algorithm (Theorem 5, algorithm RES), and $k$ servers on $k+1$ points admit a $k$ -competitive one (Theorem 4, algorithm BAL). Section 8 poses the $k$ -server conjecture, in the symmetric finite setting of the paper.
1990. Fiat, Rabani, and Ravid (FOCS 1990) give the first competitive ratio depending on $k$ alone — exponential in $k$ , but finite on every metric space.
1991. Chrobak, Karloff, Payne, and Vishwanathan (SIAM J. Discrete Math.) prove the conjecture on the real line via Double Coverage; Chrobak and Larmore (SIAM J. Comput.) extend it to all tree metrics.
1995. Koutsoupias and Papadimitriou (J. ACM) prove the Work Function Algorithm is $(2k-1)$ -competitive on every metric space — the breakthrough, and still the best general bound. Their Conjecture 1.1 fixes the conjecture's modern form: for every metric space there is an online algorithm with competitive ratio $k$ .
1996. The same authors verify the conjecture on spaces of $k+2$ points via the dual 2-evader problem (Inf. Process. Lett. 57).
2004. Bartal and Koutsoupias prove the WFA itself is $k$ -competitive on the line, weighted stars, and all spaces of $k+2$ points.
2021. Coester and Koutsoupias (ICALP) give a unifying potential for all known WFA analyses and push the frontier to the circle.
2023. Bubeck, Coester, and Rabani (STOC) refute the randomized analogue: no $o(\log^2 k)$ -competitive randomized algorithm exists in general. The deterministic conjecture — this mission's goal — survives as the central open question, with the gap between $k$ and $2k-1$ unmoved since 1995.
2026. Coester, Koutsoupias, and Zbysiński post The $k$ -server conjecture is true (arXiv:2609.15979), a claimed proof of the full conjecture: the Work Function Algorithm itself is $k$ -competitive on every metric space, via a matrix representation of work functions and a potential function built on it. The preprint is not yet peer-reviewed; this mission's goal stays open until a machine-checked proof exists.

Setting

Fix a metric space $M$ with distance function $d$ , and a number of servers $k \ge 1$ . A configuration records where the $k$ servers stand: it is a function $C$ assigning to each server $i \in \{1, \dots, k\}$ a point $C(i) \in M$ . Moving the servers from configuration $C$ to configuration $C'$ means server $i$ travels from $C(i)$ to $C'(i)$ ; the movement cost is the total distance traveled,

\mathrm{moveCost}(C, C') \;=\; \sum_{i=1}^{k} d\bigl(C(i),\, C'(i)\bigr).

A request sequence is a finite list $\sigma = (r_1, \dots, r_n)$ of points of $M$ , presented one at a time; write $\sigma_{\le j} = (r_1, \dots, r_j)$ for the list of the first $j$ requests (so $\sigma_{\le 0}$ is the empty list).

A deterministic online algorithm $A$ is a rule that, for every finite request sequence $\ell$ , specifies a configuration $A(\ell)$ — where the servers stand after serving the requests of $\ell$ in order. In particular $A(\text{empty list})$ is the initial configuration, before any request arrives. Two points about this way of modeling an algorithm:

Online and deterministic, by construction. The configuration after $j$ requests is $A(\sigma_{\le j})$ , a function of those first $j$ requests only — the algorithm cannot see the future, and makes no random choices.
The service constraint. Whenever a request sequence ends with a request $r$ , some server must stand at $r$ immediately after: for every list $\ell$ and every point $r$ , the configuration reached after serving $\ell$ followed by $r$ places at least one server at the point $r$ .

Running $A$ on $\sigma = (r_1, \dots, r_n)$ produces the configurations $A(\sigma_{\le 0}),\, A(\sigma_{\le 1}),\, \dots,\, A(\sigma_{\le n})$ , and its cost is the total movement along this trajectory:

\mathrm{cost}_A(\sigma) \;=\; \sum_{j=1}^{n} \mathrm{moveCost}\bigl(A(\sigma_{\le j-1}),\, A(\sigma_{\le j})\bigr).

For comparison, an offline schedule for $\sigma$ starting at a configuration $C_0$ is any sequence of configurations $S_0 = C_0, S_1, \dots, S_n$ in which $S_j$ places a server at the request $r_j$ , for each $j$ — chosen with the whole of $\sigma$ known in advance. The optimal offline cost $\mathrm{OPT}(C_0, \sigma)$ is the infimum, over all such schedules, of the total movement $\sum_{j=1}^{n} \mathrm{moveCost}(S_{j-1}, S_j)$ .

Finally, $A$ is $c$ -competitive if there is a constant $a$ — depending on the algorithm, hence possibly on the metric space and the initial configuration, but never on the request sequence — with

\mathrm{cost}_A(\sigma) \;\le\; c \cdot \mathrm{OPT}\bigl(A(\text{empty list}),\, \sigma\bigr) + a \qquad \text{for every request sequence } \sigma.

Formalization targets

Goal — the $k$ -server conjecture

\text{For every } k \ge 1,\ \text{every metric space } M,\ \text{and every initial configuration } C_0:\ \exists\, A \text{ starting at } C_0 \text{ that is } k\text{-competitive.}

The goal fixes no algorithm: any $k$ -competitive construction settles it. This is the weakest stable form of the conjecture — it survives every improvement in constants or techniques short of a disproof.

Milestones — the known ladder

The milestones are the classical results between the trivial and the conjectured, each an existence or impossibility statement over the same definitions: the lower bound $c \ge k$ on any space with at least $k+1$ points; the conjecture for $k = 2$ ; for spaces of exactly $k+1$ points; for the real line; the $(2k-1)$ upper bound of the Work Function Algorithm on every space; the conjecture for spaces of exactly $k+2$ points; the conjecture for three servers in the Manhattan plane $(\mathbb{R}^2, \ell^1)$ — the one settled case over a genuinely two-dimensional continuum (Bein–Chrobak–Larmore 2002; reproved by the unifying potential of Coester–Koutsoupias 2021); Coester–Koutsoupias's 2021 result that the Work Function Algorithm itself — not just some algorithm — is $3$ -competitive for three servers on trees, stated over an explicit formalization of the WFA; and the 2023 Bubeck–Coester–Rabani refutation of the randomized analogue: there are $(k+1)$ -point spaces on which every randomized algorithm is $\Omega(\log^2 k)$ -competitive, stated over a mixed-strategy model of randomized online algorithms.

Significance

A proof of the conjecture would close the founding problem of competitive analysis and pin down the exact power of determinism in online optimization over arbitrary metrics; a disproof would separate general metric spaces from every special class where the ratio $k$ is known tight. Either outcome recalibrates the field's standard model of adversarial request sequences.

None of these results — not even the lower bound — has a machine-checked proof, and online algorithms as a subject are absent from Mathlib. This mission builds the base layer: a faithful model of online service systems (configurations, online algorithms as prefix functions, offline schedules, competitiveness), the classical possibility and impossibility results over it, and, at the top, the Koutsoupias–Papadimitriou bound, whose potential-function argument is self-contained but delicate. The model is reusable for paging, weighted caching, metrical task systems, and the randomized $k$ -server problem.

Difficulty

The obvious first idea — the greedy algorithm, moving the nearest server to each request — is not competitive for any constant, already on three points of the line: two nearby points can ping-pong one server forever while a server parked slightly farther away never moves. Every known competitive algorithm must sometimes move a server other than the nearest one, and the whole difficulty of the conjecture is quantifying exactly how much such foresight-free hedging can achieve. The Work Function Algorithm's analysis via a potential over offline work functions loses a factor of two for reasons nobody has been able to remove; on the lower-bound side, no metric space is known where the deterministic ratio exceeds $k$ .

Formalization scope

The Lean model commits to: configurations as functions Fin k → M (labeled servers — equivalent in cost to the unlabeled multiset model, since offline can permute labels for free); algorithms as total functions List M → (Fin k → M) with the service constraint, so a step may move several servers (the standard laziness reduction makes this equivalent to one-move-per-request); costs in ℝ via Metric.dist; the offline optimum as an sInf over schedules, which agrees with the attained minimum on finite spaces; and the additive-constant form of competitiveness, quantified as ∃ a, ∀ σ.

Two conventions guard against trivialization. The additive constant is quantified before the request sequence — allowing it to depend on $\sigma$ would make every algorithm $1$ -competitive. And the lower-bound milestone requires $k+1$ distinct points (Finset.card = k + 1); on spaces with at most $k$ points the conjecture is trivially true and the lower bound false.

Three further definitional layers extend the model. The work function workFunction C₀ σ C is the sInf of (schedule cost + final move to C) over schedules serving σ from C₀, and the Work Function Algorithm WFA is defined on finite spaces with k ≥ 1 servers: after each request it moves to a configuration containing the request minimizing (movement cost) + (work function of the history including the request), a minimizer existing by finiteness and ties broken by a fixed arbitrary choice — matching the standard definition with its "ties broken arbitrarily" (our fixed choice is one admissible instance). A tree is a finite metric space carrying a tree graph whose weighted path lengths realize the metric — exactly "the set of vertices of a tree" of the sources. A randomized algorithm is a mixed strategy: a probability measure over an index type together with a deterministic algorithm per outcome and measurable per-sequence cost; its expected cost is a lower Lebesgue integral in $[0,\infty]$ , and $c$ -competitiveness from $C_0$ demands every outcome start at $C_0$ and one additive constant work for all request sequences.

Welcome contributions: proofs of any milestone in any order (the lower bound and the $(k+1)$ -point case are the natural entry points); alternative algorithms for milestones already closed; and infrastructure lemmas about moveCost, schedules, and work functions published as reusable platform theorems.

Selected references

M. Manasse, L. McGeoch, D. Sleator, Competitive algorithms for server problems, J. Algorithms 11 (1990). doi:10.1016/0196-6774(90)90003-W
A. Fiat, Y. Rabani, Y. Ravid, Competitive k-server algorithms, FOCS 1990. doi:10.1109/FSCS.1990.89566
M. Chrobak, H. Karloff, T. Payne, S. Vishwanathan, New results on server problems, SIAM J. Discrete Math. 4 (1991). doi:10.1137/0404017
M. Chrobak, L. Larmore, An optimal on-line algorithm for k servers on trees, SIAM J. Comput. 20 (1991). doi:10.1137/0220008
E. Koutsoupias, C. Papadimitriou, On the k-server conjecture, J. ACM 42 (1995). doi:10.1145/210118.210128
E. Koutsoupias, C. Papadimitriou, The 2-evader problem, Inf. Process. Lett. 57(5) (1996), 249–252.
C. Coester, E. Koutsoupias, Towards the k-server conjecture: a unifying potential, pushing the frontier to the circle, ICALP 2021. arXiv:2102.10474
S. Bubeck, C. Coester, Y. Rabani, The randomized k-server conjecture is false!, STOC 2023. arXiv:2211.05753
E. Koutsoupias, The k-server problem (survey), Computer Science Review 3 (2009). doi:10.1016/j.cosrev.2009.04.002

122 thms11 active usersReviewed

Completed

Convex Optimization Operations Research·Captain: wenxinzhang

Vector Space Methods IX: Global Lagrange DualityTextbook

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

z_1\le_P z_2\quad\Longleftrightarrow\quad z_2-z_1\in P.

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

\mu=\inf\{f(x):x\in\Omega,\ G(x)\le_P0\},

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

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

L(x,z^*)=f(x)+z^*(G(x)),\qquad \phi(z^*)=\inf_{x\in\Omega}L(x,z^*).

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

-G(x_s)\in\operatorname{int}P.

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

\mu=\phi(z_0^*)= \max_{z^*\ \text{dual-positive}}\phi(z^*).

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

14 thms3 active usersReviewed

Completed

Markov Chain Operations Research Stochastic Systems·Captain: tianyipeng

Markov Entanglement: Index Policies for Restless Bandits are Asymptotically SeparableResearch Paper

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.

12 thms2 active usersReviewed

Combinatorics Operations Research Probability·Captain: Shuze Chen

The Komlos ConjectureOpen Problem

Motivation

Discrepancy theory asks how evenly a collection of objects can be split into two parts. Its central open question is a conjecture of Komlós, first circulated in the 1980s: any finite family of vectors of Euclidean length at most one can be signed $\pm 1$ so that the signed sum is bounded in every coordinate by a universal constant — independent of how many vectors there are and of the dimension they live in.

Timeline

1963. Steinitz-type vector balancing questions circulate; Bárány and Grinberg later (1981) show any norm admits a dimension-dependent bound $2d$ , setting the theme: how much of the dependence on dimension is real?
1981. Beck and Fiala (Discrete Appl. Math.) prove degree- $t$ set systems have discrepancy at most $2t - 1$ , by the floating-colors argument, and conjecture $O(\sqrt{t})$ .
1980s. Komlós poses the vector form — unit $\ell^2$ -norm columns, constant $\ell^\infty$ discrepancy — which implies the Beck–Fiala conjecture; it circulates through Spencer's Ten Lectures (1987) as the central open problem of the area.
1985. Spencer (Trans. AMS) proves "six standard deviations suffice": discrepancy $6\sqrt{n}$ for $n$ sets on $n$ points, beating random signing via the partial-coloring method.
1998. Banaszczyk (Random Struct. Algorithms) proves the Komlós bound $O(\sqrt{\log n})$ by a recursive Gaussian-measure argument over convex bodies.
2010–2016. The constructive era: Bansal (2010) makes Spencer algorithmic by SDP random walks, Lovett and Meka (2012) simplify, and Bansal, Dadush, and Garg (STOC 2016) give a polynomial-time algorithm matching Banaszczyk's bound.
2023. Kunisky (SIAM J. Discrete Math.) constructs instances from unsatisfiable formulas with discrepancy approaching $1+\sqrt{2}$ — the strongest lower bound on the conjectured constant.
2025. Bansal and Jiang (arXiv:2508.03961) break the Banaszczyk barrier: $\tilde{O}((\log n)^{1/4})$ for Komlós, and the Beck–Fiala conjecture resolved for $t \ge \log^2 n$ — the first movement in nearly thirty years. The gap between $2.414\ldots$ and $\tilde{O}((\log n)^{1/4})$ is the conjecture.

Setting

Fix $n$ vectors $v_1, \dots, v_n \in \mathbb{R}^m$ with Euclidean norm $\lVert v_i \rVert_2 \le 1$ . A sign vector is an $\varepsilon \in \{-1, +1\}^n$ : one sign $\varepsilon_i \in \{\pm 1\}$ per vector. Writing $v_{ij}$ for the $j$ -th coordinate of the vector $v_i$ , the discrepancy of the family under $\varepsilon$ is the largest coordinate, in absolute value, of the signed sum $\sum_i \varepsilon_i v_i$ — that is, $\max_{j \le m} \lvert \sum_{i \le n} \varepsilon_i v_{ij} \rvert$ , the $\ell^\infty$ norm of the signed sum. The Komlós property at constant $K$ — KomlosBound K — says that every such family, in every $n$ and every $m$ , admits a sign vector with every coordinate of the signed sum at most $K$ in absolute value.

Set systems embed as the special case of $0/1$ -incidence matrices: if $A$ is an $m \times n$ matrix of $0$ s and $1$ s in which every column has at most $t$ ones (every element lies in at most $t$ sets), the columns scaled by $1/\sqrt{t}$ have norm at most one, so the Komlós property gives discrepancy $K\sqrt{t}$ — the Beck–Fiala conjecture.

Formalization targets

Goal — the Komlós conjecture

\exists\, K \in \mathbb{R}: \quad \text{every } v_1, \dots, v_n \in \mathbb{R}^m \text{ with } \lVert v_i\rVert_2 \le 1 \text{ admits } \varepsilon \in \{\pm 1\}^n \text{ with } \max_j \Big|\sum_i \varepsilon_i v_{ij}\Big| \le K.

The goal fixes no value of $K$ : any finite universal constant settles it, so the statement survives every improvement in the constant.

Milestones — the known ladder

Eight results over the same definitions: Beck–Fiala's $2t - 1$ for degree- $t$ set systems; Spencer's $6\sqrt{n}$ for $n$ sets on $n$ points; Banaszczyk's $O(\sqrt{\log n})$ for the Komlós setting; its corollary $O(\sqrt{t \log n})$ for set systems; the reduction "Komlós at $K$ implies Beck–Fiala at $K\sqrt{t}$ "; Kunisky's lower bound $K \ge 1 + \sqrt{2}$ ; and the two 2025 Bansal–Jiang breakthroughs — $\tilde{O}((\log n)^{1/4})$ for the Komlós setting, and the Beck–Fiala conjecture's bound $O(\sqrt{t})$ in the regime $t = \Omega(\log^2 n)$ .

Significance

The conjecture is the meeting point of the two main techniques of discrepancy theory — partial coloring and the Gaussian/convex-geometric method — and each further improvement has forced a new technique into existence. A proof would resolve the Beck–Fiala conjecture in full and sharpen the hereditary-discrepancy landscape; a disproof would break the widely-shared expectation that vector balancing is dimension-free. The problem is also a benchmark for algorithmic discrepancy: every known bound now has a polynomial-time counterpart, and the constructive tools built for it (random-walk roundings, spectral partial colorings) are used across approximation algorithms and ranging into differential privacy.

None of this literature is formalized anywhere; Mathlib has no discrepancy theory at all. The definitions here are elementary — finite sums, absolute values, one norm hypothesis — so the mission's entry cost is unusually low for an open-problem mission: the Beck–Fiala theorem and the scaling reduction are self-contained finite combinatorics, while Spencer and Banaszczyk each force a genuinely new proof technique (pigeonhole partial coloring; Gaussian measure on convex bodies) into Lean.

Difficulty

Random signs lose: they give $\Theta(\sqrt{n})$ , not a constant, so the naive probabilistic argument is ruled out from the start. The Beck–Fiala argument caps discrepancy by degree, not by norm, and provably cannot be pushed below $2t - O(1)$ by its own bookkeeping. Partial coloring alone loses a logarithm through its iteration, and Banaszczyk's method is blocked at $\sqrt{\log n}$ by the Gaussian measure of the cube. The 2025 advance decouples the two methods but still pays iterated polylogarithmic factors. Nothing currently known contracts the remaining gap to a constant, and the lower bound says the constant, if it exists, is at least $1 + \sqrt{2}$ — so any proof must handle instances strictly harder than the set-system case.

Formalization scope

The Lean model commits to: vectors as EuclideanSpace ℝ (Fin m), whose norm is the $\ell^2$ norm (the hypothesis $\lVert v_i \rVert \le 1$ reads ‖v i‖ ≤ 1); the $\ell^\infty$ conclusion written coordinatewise as ∀ j, |∑ i, ε i * v i j| ≤ K, avoiding any auxiliary sup-norm structure; sign vectors as real vectors with ε i = 1 ∨ ε i = -1; and set systems as matrices A : Fin m → Fin n → ℝ with an entrywise $0/1$ hypothesis and column-degree counted by Set.ncard. Quantifier order matters everywhere: in KomlosBound K the constant is fixed before $n$ and $m$ — a $K$ depending on $n$ would make the statement the trivial $\sqrt{n}$ bound. In beck_fiala the hypothesis $t \ge 1$ is required (the degree- $0$ system has discrepancy $0 > 2t-1$ otherwise); the Banaszczyk-form bounds use $\log(n+2)$ so that the bound is positive already at $n \le 1$ . In the Bansal–Jiang milestones the asymptotic $\tilde{O}$ and $\Omega$ are rendered by existential constants quantified before all instances: the hidden $\mathrm{poly}(\log\log n)$ factor becomes $(\log\log(n+8))^{\gamma}$ for some fixed $\gamma > 0$ (the inner shift $+8$ keeps the iterated logarithm positive), and the threshold $t = \Omega(\log^2 n)$ becomes $C_0 \log^2(n+2) \le t$ for some fixed $C_0 > 0$ .

Welcome contributions: any milestone in any order — beck_fiala and komlos_implies_beck_fiala are self-contained finite arguments and the natural entry points; spencer_six_deviations and banaszczyk_bound each import a major technique; komlos_lower_bound needs an explicit construction and a case analysis over all sign vectors. Reusable infrastructure — partial colorings, Gaussian measure bounds for convex bodies, hereditary discrepancy — is welcome as platform theorems. The matrix Spencer conjecture, prefix discrepancy, and the Steinitz problem are related but deliberately left to future missions.

Selected references

J. Beck, T. Fiala, "Integer-making" theorems, Discrete Applied Mathematics 3 (1981). doi:10.1016/0166-218X(81)90022-6
J. Spencer, Six standard deviations suffice, Trans. Amer. Math. Soc. 289 (1985). doi:10.1090/S0002-9947-1985-0784009-0
W. Banaszczyk, Balancing vectors and Gaussian measures of n-dimensional convex bodies, Random Structures & Algorithms 12 (1998). doi link
N. Bansal, D. Dadush, S. Garg, An algorithm for Komlós conjecture matching Banaszczyk's bound, FOCS 2016 / SIAM J. Comput. arXiv:1605.02882
N. Bansal, H. Jiang, Decoupling via affine spectral-independence: Beck–Fiala and Komlós bounds beyond Banaszczyk, 2025. arXiv:2508.03961
D. Kunisky, The discrepancy of unsatisfiable matrices and a lower bound for the Komlós conjecture constant, SIAM J. Discrete Math. 37 (2023). arXiv:2111.02974
B. Chazelle, The Discrepancy Method, Cambridge University Press, 2000. author's page

24 thms7 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: Shuze Chen

Dynamic Programming and Optimal Control I: The DP AlgorithmTextbook

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

x_{k+1} = f_k(x_k, u_k, w_k), \qquad k = 0, 1, \dots, N-1,

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

J_\pi(x_0) = \mathbb{E}\Big[ g_N(x_N) + \sum_{k=0}^{N-1} g_k(x_k, \mu_k(x_k), w_k) \Big].

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

J_N = g_N, \qquad J_k(x) = \min_{u \in U_k(x)} \mathbb{E}_w\big[ g_k(x,u,w) + J_{k+1}(f_k(x,u,w)) \big].

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

J_0(x_0) \;=\; \min_{\pi \text{ admissible}} J_\pi(x_0), \qquad \text{with the minimum attained,}

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.

5 thms2 active usersReviewed

Completed

Graph Theory Operations Research·Captain: Shuze Chen

Dynamic Programming and Optimal Control II: Label Correcting MethodsTextbook

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

\text{OPEN} = \varnothing \implies \text{UPPER} = \operatorname{dist}(s, t) \in \overline{\mathbb{R}},

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

6 thms4 active users

Completed

Operations Research Probability·Captain: viratkota

Coherent Measures of Risk: the axioms, and why Value-at-Risk fails themResearch Paper

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.

4 thms1 active userReviewed

Linear Optimization Operations Research Optimization+1·Captain: ORdos

Smale's Ninth Problem: Strongly Polynomial Linear ProgrammingOpen Problem

The problem of solving linear inequalities

The linear feasibility problem takes a matrix $A \in \mathbb{R}^{m\times n}$ and a vector $b \in \mathbb{R}^m$ and asks whether the system of $m$ linear inequalities in $n$ real unknowns

\{\,x \in \mathbb{R}^n \mid Ax \ge b\,\} \;\ne\; \emptyset

has a solution. By linear programming duality, optimizing a linear objective over such a set reduces to feasibility, so this decision problem carries the whole complexity of linear programming.

What "polynomial time" means here depends on the machine. In the bit model the input is a list of rational numbers, its size $L$ counts the bits of all numerators and denominators, and an algorithm is polynomial if it runs in time $\mathrm{poly}(m, n, L)$ . In the real-number model the input is a list of $mn + m$ exact real numbers, each arithmetic operation ( $+, -, \times, \div$ ), comparison, or memory move costs one unit, and a running time may only depend on $m$ and $n$ . An algorithm polynomial in this second sense is what Smale asks for; the closely related bit-model notion — $\mathrm{poly}(m,n)$ arithmetic operations and polynomially bounded intermediate bit sizes — is called strongly polynomial. This mission fixes the real-number model precisely as a Blum–Shub–Smale (BSS) machine (Blum–Shub–Smale 1989): a finite program of instructions acting on a bi-infinite tape $\mathbb{Z} \to \mathbb{R}$ of real registers — loads of arbitrary real machine constants, exact field arithmetic at fixed addresses, two-sided tape shifts, a sign-test branch, and accept/reject — with cost equal to the number of executed instructions. The convention that costs something: the program must be uniform, one finite instruction list serving every $m$ , $n$ , and every real instance. Uniformity is exactly what separates the question from point-location tricks available to non-uniform families of decision trees.

Why it matters

For optimization, the question is the last gap in the complexity of its central problem. Linear programs with combinatorial structure already admit strongly polynomial algorithms — Tardos (1986) solved every LP whose running time may depend on the entries of $A$ but not on $b$ or $c$ , covering network flows and all $\{0,\pm1\}$ -constraint problems — and a positive answer for general LP would extend that unification to the whole class, while explaining why simplex-type methods behave so well in practice (Spielman–Teng 2004).

For the theory of computation over the reals, the problem is a benchmark for what unit-cost exact arithmetic can do: it is Problem 9 on Smale's list of mathematical problems for the twenty-first century (Smale 1998), posed in the BSS model as the real-number analogue of the P-versus-NP style questions of that program, and it interacts with polyhedral combinatorics through the polynomial Hirsch conjecture: a polynomial bound on polytope diameters is a necessary condition for any polynomial pivot rule. A problem that calibrates both the practice of optimization and the foundations of real computation is a subject, not a special case.

The question and what is known

\textbf{Question (Smale's 9th).}\quad \text{Is there a uniform BSS program deciding } \{x \mid Ax \ge b\} \ne \emptyset \text{ in } \mathrm{poly}(m,n) \text{ steps?}

The timeline splits into a negative branch (lower bounds against algorithm classes) and a positive branch (polynomial algorithms in weaker senses).

Lower bounds. Klee–Minty (1972) constructed a deformed cube on which Dantzig's largest-coefficient simplex rule visits all $2^n$ vertices; analogous exponential examples were later found for essentially every deterministic pivot rule, and randomized rules were driven to subexponential lower bounds by Friedmann–Hansen–Zwick (2011) — against upper bounds of $\exp(O(\sqrt{n \log n}))$ from Kalai (1992) and Matoušek–Sharir–Welzl (1996). On the interior-point side, Allamigeon–Benchimol–Gaubert–Joswig (2018) showed by tropical methods that log-barrier path following is not strongly polynomial, and Allamigeon–Gaubert–Vandame (2022) extended this to every self-concordant barrier: no interior-point method of that class can settle the question positively.

Polynomial algorithms in weaker senses. Khachiyan (1979/80) proved LP feasibility is polynomial in the bit model via the ellipsoid method; Karmarkar (1984) and then Renegar (1988) brought interior-point methods to $O(\sqrt{n}\,L)$ iterations. Megiddo (1984) solved LP in linear time for every fixed dimension; Tardos (1986) gave the combinatorial strongly polynomial class; Vavasis–Ye (1996) and Dadush–Huiberts–Natura–Végh (2020) replaced the bit size by condition measures of $A$ alone; Ye (2011) proved policy iteration strongly polynomial for fixed-discount Markov decision processes.

The central difficulty is visible in every positive result: each known iteration count is controlled by a scale-dependent quantity — bit length, condition number, barrier curvature — that is unbounded over the real instances with $m, n$ fixed. The naive plan, "run the ellipsoid method and round", fails at its first step in the real model: the number of iterations needed to separate a feasible system from an infeasible one grows with the thinness of the feasible set, which is not a function of $(m, n)$ ; no data-independent perturbation $\varepsilon$ exists when the data are arbitrary reals. All results above are proved on paper only; none has a machine-checked proof in the literature. What is already formalized, on this platform, is the substrate this mission builds on: the simplex iteration (mission Introduction to Linear Optimization IV), the ellipsoid method with its volume-halving correctness theorem (XI), interior-point path following (XII), and self-concordance with the barrier method (Convex Optimization VI).

A hierarchy of formalization targets

The mission's milestone list realizes this hierarchy in order; each level states what it deliberately leaves open.

Level 0 — the model works. A uniform BSS program decides one-variable feasibility in linear time:

\exists\,P,\,C\ \ \forall m,\ \forall (a,b) \in \mathbb{R}^m \times \mathbb{R}^m:\ P \text{ decides } \{x \in \mathbb{R} \mid a_i x \ge b_i\ \forall i\} \ne \emptyset \text{ within } C(m{+}1) \text{ steps}.

It fixes nothing about $n \ge 2$ ; its role is to certify that the machine model and cost semantics of the goal are non-vacuous.

Level 1 — the classical method is exponential. On the Klee–Minty cube, Dantzig's rule admits a run of

2^n - 1 \text{ pivots}

from the all-slack basis to the optimum. It leaves open all other pivot rules — extensions to further rules are welcome as strengthenings.

Level 2 — the bit model succeeds. Through the Cramer–Hadamard solution bound $|x_j| \le n!\,U^n$ and the perturbation estimates, Khachiyan's theorem: for integer data bounded by $U$ , every admissible ellipsoid run decides feasibility within

t^* \le 10^6\,(n{+}2)^4(\log_2 U + n + 2) \text{ iterations}.

The generous constants are deliberate — only the polynomial order is load-bearing. This level leaves open exactly the dependence on $\log U$ .

Level 3 — the goal (open). A uniform program with data-independent polynomial cost:

\exists\,P,\,C,\,d\ \ \forall m, n, A, b:\ P \text{ decides } \{x \mid Ax \ge b\} \ne \emptyset \text{ within } C\,(mn + m + 2)^d \text{ steps}.

The statement asserts only the shape of the truth — no hard-coded degree or constant — so it is stable under every future quantitative improvement. These levels do not exhaust the project: Tardos' combinatorial LP theorem, Ye's fixed-discount MDP result, and impossibility statements for restricted program classes in the style of Allamigeon–Gaubert–Vandame are natural later milestones.

Formalization scope

Polyhedra, simplex states, pivots, and ellipsoid runs are the platform's existing LinearOptimization development over Matrix (Fin m) (Fin n) ℝ, with $\{x \mid Ax \ge b\}$ as polyhedron A b; algorithms with data-dependent iteration counts are formalized as run predicates, as in the parent missions. The new SmaleNinth definitions supply what the goal genuinely needs and the run-predicate style cannot express: a concrete inductive type of BSS programs with operational semantics and unit-cost accounting, the Klee–Minty data with Dantzig's rule, and the explicit Khachiyan constants. One convention closes the degenerate escape hatch: the goal quantifies over finite BSSProgram terms under the fixed encodeLP input convention — formalizing "algorithm" as an arbitrary function $\mathbb{R}^{mn+m} \to \mathrm{Bool}$ would make the statement trivially true and is not the theorem. Division is totalized as $x/0 = 0$ and the branch test is $x_i \le 0$ ; both are benign for the class of programs quantified over.

The machine module is infrastructure beyond this mission — any real-number complexity statement (other Smale problems, sums-of-square-roots, BSS-completeness) can reuse it, as can any pivot-rule lower bound reuse the Klee–Minty module. Formalization forces distinctions the literature leaves informal: which machine variant carries the unit-cost claim, how ties in Dantzig's rule are resolved, and which of the interchangeable Khachiyan constants each estimate actually needs. Welcome contributions include proofs of any milestone, alternative exponential instances for other pivot rules, sharper constants in the Khachiyan module, and ports of the known strongly polynomial special cases.

Selected references

L. Blum, M. Shub, S. Smale, On a theory of computation and complexity over the real numbers, Bull. AMS 21(1):1–46, 1989. DOI
S. Smale, Mathematical problems for the next century, Math. Intelligencer 20(2):7–15, 1998. DOI
V. Klee, G. J. Minty, How good is the simplex algorithm?, in Inequalities III, Academic Press, 1972, pp. 159–175.
L. G. Khachiyan, Polynomial algorithms in linear programming, USSR Comput. Math. Math. Phys. 20:53–72, 1980. DOI
N. Karmarkar, A new polynomial-time algorithm for linear programming, Combinatorica 4:373–395, 1984. DOI
J. Renegar, A polynomial-time algorithm, based on Newton's method, for linear programming, Math. Programming 40:59–93, 1988. DOI
É. Tardos, A strongly polynomial algorithm to solve combinatorial linear programs, Oper. Res. 34(2):250–256, 1986. DOI
N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. DOI
G. Kalai, A subexponential randomized simplex algorithm, STOC 1992. DOI
O. Friedmann, T. D. Hansen, U. Zwick, Subexponential lower bounds for randomized pivoting rules for the simplex algorithm, STOC 2011. DOI
D. A. Spielman, S.-H. Teng, Smoothed analysis of algorithms: why the simplex algorithm usually takes polynomial time, J. ACM 51(3):385–463, 2004. DOI
S. A. Vavasis, Y. Ye, A primal-dual interior point method whose running time depends only on the constraint matrix, Math. Programming 74:79–120, 1996. DOI
Y. Ye, The simplex and policy-iteration methods are strongly polynomial for the Markov decision problem with a fixed discount rate, Math. Oper. Res. 36(4):593–603, 2011. DOI
X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, Log-barrier interior point methods are not strongly polynomial, SIAM J. Appl. Algebra Geom. 2(1):140–178, 2018. DOI
X. Allamigeon, S. Gaubert, N. Vandame, No self-concordant barrier interior point method is strongly polynomial, STOC 2022. arXiv
D. Dadush, S. Huiberts, B. Natura, L. A. Végh, A scaling-invariant algorithm for linear programming whose running time depends only on the constraint matrix, STOC 2020. arXiv
D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Chapters 3, 8, 9 — formalized in the Introduction to Linear Optimization mission series).
B. Korte, J. Vygen, Combinatorial Optimization: Theory and Algorithms, 6th ed., Springer, 2018, §4.1–4.5.

29 thms6 active usersReviewed

Completed

Control Theory Dynamic Programming Operations Research+1·Captain: Shuze Chen

Dynamic Programming and Optimal Control V: LQG and Certainty EquivalenceTextbook

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

x_{k+1} = A_k x_k + B_k u_k + w_k, \qquad z_k = C_k x_k + v_k,

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

\pi^*(I_k) = L_k\, \mathbb{E}[x_k \mid I_k] \ \text{ along its own trajectories} \quad\Longrightarrow\quad J(\pi^*) \le J(\pi)\ \ \forall \pi,

— 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

5 thms4 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization+1·Captain: Shuze Chen

Dynamic Programming and Optimal Control VII: Infinite Horizon ProblemsTextbook

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

(T_\mu J)(i) = g(i,\mu(i)) + \sum_j p_{ij}(\mu(i)) J(j), \qquad (TJ)(i) = \min_{u \in U(i)}\Big[g(i,u) + \sum_j p_{ij}(u) J(j)\Big]

(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

T^k J_0 \to J^* \ \ \forall J_0, \qquad J^* = T J^* \text{ uniquely}, \qquad J^*(i) \le J_\pi(i) = \lim_N J^N_\pi(i) \ \ \forall \pi \text{ admissible},

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

8 thms3 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: StellaXin

Capped Base-Stock Policies: A 2.33-ApproximationResearch Paper

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

I_{t+1}=(I_t+x_{1,t}-D_t)^+,\qquad x_{i,t+1}=x_{i+1,t}\ (i<L),\qquad x_{L,t+1}=q_t.

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

C(\pi)=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[hI_{t+1}^\pi+p\ell_t^\pi],\qquad \mathrm{OPT}=\inf_{\pi\in\Pi}C(\pi).

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

I_r^m=\max_{0\le k\le m}\sum_{i=1}^k(r-D_i),\qquad G_m(r,z)=\mathbb E\left[\left(I_r^m+\sum_{i=1}^m(D_i-r)-z\right)^+\right].

Empty sums are zero. The lower certificate is

\underline C=\inf\{hz+p(\mu-r):0\le r\le\mu,\ z\ge0,\ G_L(r,z)\le L(\mu-r),\ G_{L+1}(r,z)\le(L+1)(\mu-r)\}.

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

\kappa_L=1+\frac{4L^2}{(L+1)(3L-1)},

the goal is Theorem 1's complete assertion:

C^*_{\rm CBS}\le\kappa_L\underline C,\qquad C^*_{\rm CBS}\le\kappa_L\mathrm{OPT}\le\frac73\mathrm{OPT}.

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.

14 thms1 active userReviewed

Completed

Control Theory Dynamic Programming Operations Research+1·Captain: Shuze Chen

Dynamic Programming and Optimal Control IV: LQR and the Riccati EquationTextbook

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)

F(P) = A^\top\big(P - P B (B^\top P B + R)^{-1} B^\top P\big) A + Q.

$(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

\exists\, P \succ 0:\quad F(P) = P,\quad P \text{ unique among } P' \succeq 0,\quad F^{k}(P_0) \to P \ \ \forall P_0 \succeq 0,\quad \rho\big(A + BL\big) < 1,

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.

9 thms5 active usersReviewed

Completed

Dynamic Programming Operations Research Optimization·Captain: Shuze Chen

Dynamic Programming and Optimal Control VI: Lookahead and RolloutTextbook

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})$ :

g(i_{\bar m}) \;\le\; H(i_1), \qquad g(i_{\bar m}) \;=\; \min\Big\{ H(i_1),\ \min_{j \in N(i_1)} H(j),\ \dots,\ \min_{j \in N(i_{\bar m - 1})} H(j) \Big\},

— 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

9 thms2 active usersReviewed

Completed

Convex Optimization Linear Optimization Operations Research+2·Captain: mikedeng1

Introduction to Stochastic Programming I: Convexity, Attainment and Optimality of the Two-Stage Recourse ProblemTextbook

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

Q(x,\xi_k) = \min_{y}\{q_k^{\mathsf T}y \mid Wy = h_k - T_k x,\ y \ge 0\}

(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)

x^* \in K_1 \text{ is optimal in (1.2)} \iff \exists\, \lambda^* \in \mathbb{R}^{m_1},\ \mu^* \in \mathbb{R}^{n_1}_{\ge 0},\ (\mu^*)^{\mathsf T}x^* = 0,\ \text{ s.t. } -c + A^{\mathsf T}\lambda^* + \mu^* \in \partial Q(x^*),

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

9 thms5 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Introduction to Stochastic Programming II: The Value of Perfect Information and of the Stochastic SolutionTextbook

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)

0 \;\le\; EVRS - EPEV \;\le\; VSS \;\le\; EVRS - SPEV \;\le\; EVRS - WS .

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.

7 thms2 active usersReviewed

The OR Formalization Drive

Missions

The Markov Chain Central Limit TheoremResearch Paper

Treatment Locality in A/B TestingResearch Paper

Vector Space Methods I: Minimum Norm Problems in Hilbert SpaceTextbook

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Vector Space Methods II: Gauss–Markov EstimationTextbook

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

The 4/3 Conjecture for Metric TSPOpen Problem

Motivation

Timeline

Setting

Formalization targets

Goal — the 4/3 conjecture

Milestones — the known ladder

Significance

Difficulty

Formalization scope

Selected references

The k-Server ConjectureOpen Problem

Motivation

Timeline

Setting

Formalization targets

Goal — the kkk-server conjecture

Milestones — the known ladder

Significance

Difficulty

Formalization scope

Selected references

Vector Space Methods IX: Global Lagrange DualityTextbook

Motivation

Setting

Formalization targets

Main goal: Lagrange duality

Milestones

Significance

Difficulty

Formalization scope

Selected references

Markov Entanglement: Index Policies for Restless Bandits are Asymptotically SeparableResearch Paper

The Komlos ConjectureOpen Problem

Motivation

Timeline

Setting

Formalization targets

Goal — the Komlós conjecture

Milestones — the known ladder

Significance

Difficulty

Formalization scope

Selected references

Dynamic Programming and Optimal Control I: The DP AlgorithmTextbook

Motivation

Setting

Target

Significance

Difficulty

Formalization scope

Selected references

Dynamic Programming and Optimal Control II: Label Correcting MethodsTextbook

Motivation

Setting

Target

Significance

Difficulty

Formalization scope

Selected references

Goal — the $k$ -server conjecture