Linear Optimization

Why the assignment dual matters

The subgradient method maximizes a concave, piecewise-linear function $w(\pi)=\min_k\{c_k+\pi\cdot v_k\}$ by moving along a subgradient $v_k$ of an active piece with a prescribed step. Held, Wolfe and Crowder's 1974 paper Validation of subgradient optimization tested the method on three families of Lagrangean duals from combinatorial optimization — the assignment problem, a relaxation of the travelling salesman problem in the style of Held and Karp, and multicommodity flows — and gave the first systematic account of when the method works in practice.

On randomly generated assignment problems of order $n\le 30$ the authors observed that the method usually did not merely converge: it stopped, after finitely many steps, at an iterate whose subgradient was exactly zero. Their explanation is a structural fact about the assignment dual, Theorem 3.1 of the paper: when the optimal assignment is unique — the typical case for random integer costs — the set of optimal dual prices has full dimension $n$, so a sequence of steps of decreasing length can land inside it. This mission formalizes that theorem and the steps of its proof.

Setting

There are $n$ men and $n$ jobs, and a real $n\times n$ cost matrix $A=(a_{ir})$: $a_{ir}$ is the cost for which man $i$ does job $r$. A one-to-one assignment is a permutation $\sigma$ of $\{1,\dots,n\}$, where $\sigma(r)$ is the man doing job $r$; its cost is $\sum_r a_{\sigma(r)\,r}$. The assignment problem (3.1) asks for a permutation of minimal cost; the assignment is unique if exactly one permutation attains that minimum.

The linear relaxation of (3.1), over doubly stochastic matrices $x=(x_{ir})$, has the dual linear program (3.2), $\max\{\sum_i\pi_i+\sum_r\rho_r : \pi_i+\rho_r\le a_{ir}\}$. For fixed prices $\pi\in\mathbb R^n$ on the men the best $\rho$ is $\rho_r=\min_s[a_{sr}-\pi_s]$, which leaves the dual function (3.3)

the inner minimum being over the men $s$ for each job $r$. The optimal set is $\Omega=\{\pi : w(\pi')\le w(\pi)\ \text{for all }\pi'\}$.

To put $w$ in the form $\min_k\{c_k+\pi\cdot v_k\}$ the paper uses assignments in a weaker sense: arbitrary functions $A:\{1,\dots,n\}\to\{1,\dots,n\}$, $n^n$ of them, with cost $c_A=\sum_r a_{A(r)\,r}$ and vector $(v_A)_i=1-\#\{r:A(r)=i\}$ (3.4). The subgradient step raises the price of a man assigned no job and lowers the price of a man assigned several; $v_A=0$ exactly when $A$ is a permutation.

In the Lean development these are assignCost, assignVec, IsOptimalAssignment, w and optSet in the namespace HeldWolfeCrowder.Assignment.

Formalization targets

Goal: Theorem 3.1 (p. 70)

If the assignment problem has a unique optimal permutation, then

The hypothesis is uniqueness among permutations; the conclusion is the dimension of the affine hull of the optimal set.

Milestones, in the order the proof uses them

1. Eq. (3.4): $w(\pi)=\min_A\{c_A+\sum_i\pi_i(v_A)_i\}$ over all $n^n$ assignments $A$.
2. §3, Eqs. (3.1)–(3.3): $w$ attains its maximum, and $\max w$ equals the cost of an optimal permutation.
3. Eq. (3.5): if $\sigma$ is the unique optimal permutation, some maximizer $\bar\pi$ of $w$ has, for every job $r$, the minimum $\min_s[a_{sr}-\bar\pi_s]$ attained only at $s=\sigma(r)$.
4. Eq. (3.6): for an optimal permutation $\sigma$, the set $\Pi=\{\pi : a_{ir}-\pi_i>a_{\sigma(r)\,r}-\pi_{\sigma(r)}\ \text{for all } r,\ i\ne\sigma(r)\}$ is convex and open, $v=0$ on it, and $\Pi\subseteq\Omega$.

Significance

The theorem turns an empirical observation into a statement about the problem: finite termination of the subgradient method on assignment problems is a property of the dual, not luck. Since $w$ is unchanged by adding the same constant to every price, $\Omega$ always contains a line; Theorem 3.1 says that, under uniqueness, it is as large as it can be. The paper (p. 70) cites the argument of its Section 2 that, with a full-dimensional optimal set, termination of the method is "nearly certain".

The result is proved in the paper; none of it is known to be machine-checked. What the formalization adds is a checked link between three classical ingredients: the integrality of the assignment polytope (Birkhoff–von Neumann, which Mathlib has as doublyStochastic_eq_convexHull_permMatrix), linear-programming duality, and strict complementary slackness, which neither Mathlib nor the platform has in the form needed. The piecewise-linear representation (3.4) is reusable wherever the assignment dual appears as a Lagrangean subproblem.

Difficulty

The inclusion $\Pi\subseteq\Omega$ is elementary; the substance is that $\Pi$ is nonempty. The obvious candidate — any optimal dual solution — fails: an optimal $\pi$ may leave ties $a_{sr}-\pi_s=a_{\sigma(r)\,r}-\pi_{\sigma(r)}$ for some $s\ne\sigma(r)$, so it sits on the boundary of $\Omega$ and shows nothing about dimension. What is needed is an optimal price vector with all these inequalities strict at once, and uniqueness of the optimal permutation is a statement about the primal side only; transferring it to the dual side goes through the linear relaxation (3.1), whose uniqueness is not the hypothesis, and through a strict complementarity property that is not available in Mathlib or on the platform.

Formalization scope

Men and jobs are both Fin n; the costs are a : Matrix (Fin n) (Fin n) ℝ with a i r the cost of man i on job r; prices are π : Fin n → ℝ (no inner product or norm is needed, so no EuclideanSpace). The inner minimum of (3.3) is Finset.univ.inf' over the men, well defined for every n. One-to-one assignments are Equiv.Perm (Fin n) with σ r the man doing job r, so the orientation of the matrix matches (3.3); arbitrary assignments are functions Fin n → Fin n. "Of dimension $n$" is Module.finrank ℝ (vectorSpan ℝ (optSet a)) = n. The page prints the index condition of (3.6) as "$i\ne r$"; the formalization uses $i\ne\sigma(r)$, which is what the argument requires. The case $n=0$ is allowed and trivial.

A statement asserting only that $\Omega$ is nonempty, or that it has dimension at least one, is not this theorem: both hold for every cost matrix, the second because $\Omega$ is invariant under adding a constant to all prices. The goal requires the full value $n$, and its hypothesis is uniqueness of the optimal permutation, not of the optimal linear-programming solution.

A complete development needs: the assignment linear program and its integrality (Mathlib's Birkhoff–von Neumann theorem), weak and strong duality between (3.1) and (3.2) or directly $\max w=\min_\sigma c_\sigma$, and a strict complementarity statement for this primal–dual pair; the last two are reusable beyond this mission. Contributions of any of these, and of alternative arguments for (3.5) that avoid strict complementary slackness, are welcome.

Selected references

• M. Held, P. Wolfe, H. P. Crowder, Validation of subgradient optimization, Mathematical Programming 6 (1974) 62–88. https://doi.org/10.1007/BF01580223
• M. Held, R. M. Karp, The traveling-salesman problem and minimum spanning trees: Part II, Mathematical Programming 1 (1971) 6–25. https://doi.org/10.1007/BF01584070
• H. W. Kuhn, The Hungarian method for the assignment problem, Naval Research Logistics Quarterly 2 (1955) 83–97. https://doi.org/10.1002/nav.3800020109
• A. J. Goldman, A. W. Tucker, Theory of linear programming, in H. W. Kuhn, A. W. Tucker (eds.), Linear Inequalities and Related Systems, Annals of Mathematics Studies 38, Princeton University Press, 1956, 53–97.
• Mathlib, Mathlib/Analysis/Convex/Birkhoff.lean (Birkhoff–von Neumann theorem, doublyStochastic_eq_convexHull_permMatrix). https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Analysis/Convex/Birkhoff.lean

Motivation

Integer programs are routinely solved by first solving their linear programming (LP) relaxation and then searching for an integer optimum near the fractional one. How near an integer optimum must be is the subject of proximity theorems. They bound the search region of branch-and-bound and of dynamic programming, and they turn a fractional optimum into a starting point for exact algorithms.

The classical bound is due to Cook, Gerards, Schrijver and Tardos (Math. Programming 34, 1986): for an integer program in inequality form $\max\{c^Tx : Ax\le b,\ x\in\mathbb Z^n\}$ that is feasible and bounded, every optimal LP solution $x^*$ has an optimal integer solution $z^*$ with $\|x^*-z^*\|_\infty\le n\cdot\delta$, where $\delta$ is the largest absolute value of a subdeterminant of $A$. For programs in standard form $Ax=b$ with $m$ rows this gives, via the Hadamard bound, $\|z^*-x^*\|_1\le n^2\cdot m^{m/2}\Delta^m$, which grows with the number of variables $n$.

Eisenbrand and Weismantel (ACM Trans. Algorithms 16(1), Article 5, 2019; conference version SODA 2018) removed the dependence on $n$ altogether, using the Steinitz lemma on rearranging vectors so that all partial sums stay short. Their bound depends only on $m$ and on the largest absolute value $\Delta$ of an entry of $A$, and it is the basis of their faster algorithms for integer programs with few constraints.

Setting

Fix natural numbers $m$ (rows) and $n$ (variables). The data are a matrix $A\in\mathbb Z^{m\times n}$, a right-hand side $b\in\mathbb Z^m$, an objective $c\in\mathbb Z^n$ and upper bounds $u\in\mathbb N^n$. A natural number $\Delta$ bounds the entries: $|a_{ij}|\le\Delta$ for all $i,j$. The integer program (10) is

and its LP relaxation is the same problem over $x\in\mathbb R^n$. Its feasible region $P=\{x\in\mathbb R^n: Ax=b,\ 0\le x\le u\}$ is a polytope, lpPolytope A b u. An optimal vertex solution is an optimal solution of the LP relaxation (IsLPOptimal) that is an extreme point of $P$. An optimal integer solution is IsIPOptimal. Both are maxima.

Distances are measured in the $\ell_1$-norm $\|z-x\|_1=\sum_i|z_i-x_i|$.

A vector $y\in\mathbb Z^n$ is a cycle of $z^*-x^*$ (Eq. (14)) if $Ay=0$ and, for every $i$, $|y_i|\le|(z^*-x^*)_i|$ and $y_i(z^*-x^*)_i\ge0$: an integer kernel vector that is sign-compatible with $z^*-x^*$ and dominated by it (IsCycle).

The Steinitz lemma (Theorem 1.1) concerns vectors $x_1,\dots,x_n$ in an $m$-dimensional normed space with $\sum_i x_i=0$ and $\|x_i\|\le1$. It asserts a permutation $\pi$ with $\|\sum_{j\le k}x_{\pi(j)}\|\le c(m)$ for all $k$, and the paper uses Sevast'anov's constant $c(m)=m$.

Formalization targets

Goal: Theorem 3.3 (p. 5:8)

If (10) has an integer feasible point and $x^*$ is an optimal vertex solution of its LP relaxation, then there is an optimal solution $z^*$ of (10) with

The constant is the paper's. The goal holds for all $m$, $n$, $b$, $c$ and $u$; only $m$ and $\Delta$ enter the bound.

Milestones, in the order the proof uses them

1. Lemma 3.1 (p. 5:8): for an LP optimum $x^*$, an integer optimum $z^*$ and a cycle $y$ of $z^*-x^*$, the vector $z^*-y$ is integer feasible, $x^*+y$ is LP feasible, and $c^Ty\le0$.
2. Lemma 3.2 (p. 5:8): if $z^*$ minimizes $\|z^*-x^*\|_1$ among the optimal integer solutions, then $z^*-x^*$ has no nonzero cycle.
3. Theorem 1.1 with $c(m)=m$ (p. 5:4): the Steinitz lemma in any $m$-dimensional real normed space.
4. Proof of Theorem 3.3 (pp. 5:8–5:9): round a vertex $x^*$ towards an integer vector and write $\{x^*\}$ for the remainder. Then $\|-A\{x^*\}\|_\infty\le\Delta m$ and $-A\{x^*\}=w_1+\dots+w_m$ with integer $w_j$, $\|w_j\|_\infty\le\Delta$.
5. Proof of Theorem 3.3, Eq. (20) (p. 5:9): a sequence of integer vectors of $\ell_\infty$-norm at most $m\Delta$ in which no value repeats $m+1$ times has length at most $m(2m\Delta+1)^m$.
6. Eq. (21) (p. 5:9), a consequence: $c^T(x^*-z^*)\le\|c\|_\infty\cdot m(2m\Delta+1)^m$ for every optimal integer solution $z^*$.

Significance

The bound is independent of the number of variables. Combined with the paper's dynamic program, it gives the paper's running-time results for integer programs with upper bounds: an optimal LP vertex is computed, and the integer optimum is searched for within an $\ell_1$-ball of radius $m(2m\Delta+1)^m$ around it. Eq. (21) bounds the absolute integrality gap by the same quantity, scaled by $\|c\|_\infty$. The Steinitz lemma with constant $m$ is a general tool in discrepancy theory and in scheduling algorithms.

All of these results have published proofs. No machine-checked proof of Theorem 3.3 or of the Steinitz lemma is known to this mission, and Mathlib has no Steinitz lemma. The mission asks for complete Lean proofs of the milestones and of the goal. A proof of the Steinitz lemma with constant $m$ for arbitrary norms is reusable well beyond integer programming.

Difficulty

Lemmas 3.1 and 3.2 and the counting step are elementary. The substance lies in two places. The first is the Steinitz lemma with the linear constant $m$ for an arbitrary norm: the bound must hold uniformly in the number $n$ of vectors, and the constant must be exactly $m$, because the goal's constant $(2m\Delta+1)^m$ counts integer points of $\ell_\infty$-norm at most $m\Delta$. The second is the passage from a vertex to at most $m$ fractional coordinates. The paper argues this in one sentence ("$x^*$ has at most $m$ positive entries"), which is not literally true for (10) with upper bounds: coordinates at their upper bound $u_i>0$ are positive. The correct fact concerns coordinates strictly between $0$ and $u_i$, and it has to be derived from the extreme-point property of $P$.

Formalization scope

• All declarations live in the namespace IPProximity.Eisenbrand. The data are integral: A : Matrix (Fin m) (Fin n) ℤ, b : Fin m → ℤ, c : Fin n → ℤ, u : Fin n → ℕ (entries $u_i=0$ allowed), Δ : ℕ. They are cast to ℝ once, inside the LP definitions. $m=0$ and $n=0$ are allowed.
• "Vertex" is Mathlib's Set.extremePoints ℝ (lpPolytope A b u). It is not defined through bases or by counting fractional coordinates.
• The $\ell_1$-distance is the explicit sum ∑ i, |(z i : ℝ) - x i|. Mathlib's norm on Fin n → ℝ is the sup norm, and it is used only where the paper has $\|\cdot\|_\infty$ (the $\|c\|_\infty$ of Eq. (21)).
• The goal adds one hypothesis the paper leaves implicit: (10) has an integer feasible point. The paper's proof begins with "Let $z^*$ be an optimal integer solution"; without this hypothesis the conclusion is false.
• Eq. (14) is formalized literally, so $y=0$ is a cycle, and Lemma 3.2 is stated for nonzero cycles, which is what its proof establishes. Dropping the vertex hypothesis would make the goal false, so the goal keeps it. The constant is exactly $m(2m\Delta+1)^m$, with no hidden existential constant.
• The Steinitz milestone is stated for any finite-dimensional real normed space of dimension $m$ with the explicit constant $m$. The goal needs only the $\ell_\infty$ case on $\mathbb R^m$.
• Out of scope: the dynamic program and the running-time theorems of Sections 2 and 4, and the refinement $\|z^*-x^*\|_1\le2\Delta$ for $m=1$.

Contributions welcome: proofs of any milestone, in particular the Steinitz lemma, and a proof of the goal from the milestones.

Selected references

• F. Eisenbrand, R. Weismantel, Proximity Results and Faster Algorithms for Integer Programming Using the Steinitz Lemma, ACM Transactions on Algorithms 16(1), Article 5, 2019. https://doi.org/10.1145/3340322
• W. Cook, A. M. H. Gerards, A. Schrijver, É. Tardos, Sensitivity theorems in integer linear programming, Mathematical Programming 34, 251–264, 1986. https://doi.org/10.1007/BF01582230
• E. Steinitz, Bedingt konvergente Reihen und konvexe Systeme, Journal für die reine und angewandte Mathematik 143, 128–176, 1913. https://doi.org/10.1515/crll.1913.143.128
• S. Sevast'janov, Approximate solution of some problems of scheduling theory (in Russian), Metody Diskretnogo Analiza 32, 66–75, 1978 (reference [31] of the paper).
• V. S. Grinberg, S. V. Sevast'yanov, Value of the Steinitz constant, Functional Analysis and Its Applications 14(2), 125–126, 1980 (reference [16] of the paper).

Motivation

Stochastic programs are solved in practice on a finite set of scenarios: a discrete probability distribution $P=\sum_{i=1}^N p_i\delta_{\omega_i}$ that approximates the true distribution of the uncertain data. The size of the resulting deterministic problem grows with $N$, and for multistage models it grows very fast, so $N$ is often reduced before solving. The question is which scenarios to delete and how to reweight the remaining ones so that the optimal value and solutions of the stochastic program change as little as possible.

Dupačová, Gröwe-Kuska and Römisch (Math. Program. Ser. A 95 (2003) 493–511) answered this with probability metrics. Stability results for stochastic programs bound the change of the optimal value by a Fortet–Mourier type distance, which is in turn bounded by a Kantorovich functional $\hat\mu_c$ (an optimal transport cost). Scenario reduction then becomes: find a measure $Q$ supported on a subset of the scenarios with $\hat\mu_c(P,Q)$ small. Section 3 of the paper solves the weight part of this problem in closed form. That result, together with the heuristics built on it (backward reduction and forward selection), became the standard scenario-reduction method, implemented for example in the GAMS tool SCENRED.

Setting

Let $\Omega$ be a set and $c:\Omega\times\Omega\to\mathbb R_+$ a cost function with $c(\omega,\tilde\omega)=0$ if and only if $\omega=\tilde\omega$, and $c(\omega,\tilde\omega)=c(\tilde\omega,\omega)$ (conditions (C1)–(C2), p. 498). The original distribution has scenarios $\omega_1,\dots,\omega_N\in\Omega$ with weights $p_i>0$ and $\sum_i p_i=1$. Write $c_{ij}=c(\omega_i,\omega_j)$.

A set $J\subset\{1,\dots,N\}$ of scenarios is deleted. The reduced measure is $Q=\sum_{j\notin J}q_j\delta_{\omega_j}$ with reduced weights $q_j\ge0$, $\sum_{j\notin J}q_j=1$. A transport plan from $P$ to $Q$ is a nonnegative matrix $(\eta_{ij})_{i\le N,\,j\notin J}$ with row sums $\sum_{j\notin J}\eta_{ij}=p_i$ and column sums $\sum_i\eta_{ij}=q_j$. The Kantorovich functional (10) is the value of this transportation problem,

and $D_J=\min\{D(J;q): q\ \text{reduced weights}\}$ is the best distance achievable once $J$ is fixed. The optimal deletion problem (13) asks for $\min\{D_J:\#J=k\}$ for a given $1\le k<N$.

In the Lean development these objects are IsReducedWeight, IsTransportPlan, transportCost, transportValue ($D(J;q)$), optWeightsValue ($D_J$) and optimalDeletionValue (the value of (13)), all in the namespace ScenarioReduction.Redistribution.

Formalization targets

Goal: Theorem 2 (optimal weights), p. 500

For every $J\neq\{1,\dots,N\}$,

and the minimum is attained at the optimal redistribution rule $\bar q_j=p_j+\sum_{i\in J_j}p_i$, where $J_j=\{i\in J: j(i)=j\}$ and $j(i)\in\arg\min_{j\notin J}c(\omega_i,\omega_j)$, for every such choice of $j(\cdot)$.

Milestones

1. Primal–dual representation of $D(J;q)$ (first display of the proof, p. 501): the transportation problem and its linear-programming dual both attain $D(J;q)$.
2. Lower bound (p. 501): $\sum_{i\in J}p_i\min_{k\notin J}c_{ik}\le D(J;q)$ for every feasible $q$.
3. Upper bound at $\bar q$ (p. 501): $\bar q$ is feasible and $D(J;\bar q)\le\sum_{i\in J}p_i\min_{j\notin J}c_{ij}$.
4. Theorem 3 (p. 501): for weights prescribed by $q_j=p_j+\lambda_jp_J$, $D(J;q)\le\sum_{i\in J}p_i\sum_{j\notin J}\lambda_jc(\omega_i,\omega_j)$, with equality if $\#J=1$ and $c$ satisfies the triangle inequality.
5. Theorem 4 (p. 503): the greedy recursions (16) and (17) give a lower and an upper bound for $\min\{D_J:\#J=k\}$, and the backward set $\{l_1,\dots,l_k\}$ is optimal under a nonemptiness condition.

Significance

Theorem 2 reduces the continuous part of scenario reduction to a formula: once the set of kept scenarios is chosen, the best reweighting is to move the mass of every deleted scenario to a nearest kept scenario, and the resulting distance is an explicit sum. This leaves only the combinatorial choice of $J$, which Theorem 4 brackets by two greedy procedures; these are the backward-reduction and forward-selection algorithms of the paper and of later work by Heitsch and Römisch. Theorem 3 covers the case in which the reduced weights are fixed by the modeller, for instance to keep a uniform distribution uniform.

The results are proved in the paper by elementary linear-programming arguments. As far as is known, none of them has a machine-checked proof. Formalizing them produces a verified finite transportation-problem layer with a general (not necessarily metric) cost and a deleted index set, and verified correctness certificates for the two standard scenario-reduction heuristics.

Difficulty

The upper bound of Theorem 2 is a direct construction. The content lies in the lower bound, which must hold for every reweighting $q$ simultaneously; this needs the dual side of the transportation problem, and the full primal–dual representation (Milestone 1) requires strong duality for a transportation problem with only the kept columns, which Mathlib does not provide in this form. A naive argument that bounds each plan row by row gives the lower bound directly for plans, but relating it to $D(J;q)$ as an infimum also requires that plans exist and that the infimum is attained. In Theorem 4, the recursions (16) and (17) are greedy and do not in general produce optimal sets; the lower bound works only because its inner minimum ranges over all $j\neq l$, not over the kept scenarios.

Formalization scope

Scenarios are indexed by Fin N (0-based), scenarios are a function ω : Fin N → Ω into an arbitrary type Ω, the cost is c : Ω → Ω → ℝ, and weights, plans and dual variables are real-valued functions on Fin N and Fin N × Fin N. Only the entries at kept indices $j\notin J$ enter any constraint, cost or objective. No measure theory is used: the index-level transportation problem is the paper's own representation of $\hat\mu_c$ for discrete measures (p. 495). Every theorem carries the standing assumptions of Section 3: $c\ge0$, (C1), (C2), $p_i>0$ and $\sum_ip_i=1$. Measurability of $c$ and conditions (C3) and (C4) concern $\Omega\subset\mathbb R^s$ and play no role for finitely supported measures; they are dropped, so the statements are more general than the page. The hypothesis $J\neq\{1,\dots,N\}$, implicit in Theorem 2, is stated explicitly; in Theorem 4, $1\le k<N$ plays this role.

$D(J;q)$ and $D_J$ are real infima (sInf) of transport costs and are only asserted about where the underlying sets are nonempty and bounded below; "min" is stated as attainment (IsLeast), not as an equality of infima. $D(J;q)$ is defined as the transportation problem and is not defined by the closed form $\sum_{i\in J}p_i\min_{j\notin J}c_{ij}$; under that definition Theorem 2 would be trivial, and it is ruled out here. Likewise the reduced-weight constraint does not force $q=\bar q$.

Needed infrastructure: finite transportation problems with nonnegativity and marginal constraints, existence of optimal plans (compactness of the feasible polytope), and LP duality for transportation problems. The transportation-problem layer is reusable beyond this mission. Contributions welcome: proofs of the milestones, a general strong-duality result for finite transportation problems, and the examples of p. 502 (single scenario deletion, keeping one scenario).

Selected references

• J. Dupačová, N. Gröwe-Kuska, W. Römisch, Scenario reduction in stochastic programming: An approach using probability metrics, Math. Program. Ser. A 95 (2003) 493–511. https://doi.org/10.1007/s10107-002-0331-0
• S. T. Rachev, Probability Metrics and the Stability of Stochastic Models, Wiley, 1991.
• H. Heitsch, W. Römisch, Scenario reduction algorithms in stochastic programming, Comput. Optim. Appl. 24 (2003) 187–206. https://doi.org/10.1023/A:1021805924152
• W. Römisch, R. Schultz, Stability analysis for stochastic programs, Ann. Oper. Res. 30 (1991) 241–266. https://doi.org/10.1007/BF02204819

Motivation

Chapter 5 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), presents the achievable region methodology of Tsoucas, Bertsimas and Niño-Mora, Glazebrook and Garbe, and Dacre, Glazebrook and Niño-Mora: instead of arguing about policies, one argues about the set of performance vectors they can produce. For a multi-armed bandit the natural performance of a policy is the vector of discounted numbers of times each state is continued; the expected return is linear in it; and the set of achievable performances turns out to be a polytope cut out by conservation laws, one inequality per subset of states, with equality exactly for the priority policies that put that subset last. Optimizing a linear objective over a polytope is a linear program, its dual is solved by an adaptive greedy algorithm, and the primal solution is the performance of a priority policy whose priorities are the algorithm's outputs, the Gittins indices. This gives yet another proof of the index theorem (Section 5.3) and, more importantly, a definition, generalized conservation laws (Section 5.4), of the class of systems for which the same argument works: branching bandits, multi-class queues, job scheduling with discounted rewards, systems with imposed priority classes. The chapter's main result, Theorem 5.5, is the statement that every such system is solved by an index policy.

Setting

There are $N$ job types $E = \{1, \dots, N\}$. A policy $\pi$ has a performance $x^\pi \in \mathbb{R}^N_+$, a vector of expectations; a permutation $\sigma$ of $E$ defines the permutation policy giving $\sigma_N$ highest and $\sigma_1$ lowest priority, and $S_k = \{\sigma_1, \dots, \sigma_k\}$ is the set of the $k$ lowest-priority types. The system satisfies GCL(1) if there are a base function $b : 2^E \to \mathbb{R}_+$ and a matrix $A = (A_i^S)$, positive on $S$ and zero off it, such that for every policy

with equality in the first for every permutation policy whose $|S|$ lowest-priority types are $S$. GCL(2) reverses the inequality. The adaptive greedy algorithm $AG(A, r)$ picks $i_N$ maximizing $r_i/A_i^E$, sets $\bar y_E$ to the maximum, removes $i_N$, and repeats with the adjusted rewards $r_i - \sum_{j \ge k} A_i^{S_j}\bar y_{S_j}$ divided by $A_i^{S_{k-1}}$; its outputs are the order $i_1, \dots, i_N$, the dual variables $\bar y_{S_k}$ and the indices $\nu_{i_k} = \sum_{j \ge k} \bar y_{S_j}$.

For the SFABP of Section 5.3, $n$ identical bandit processes on $E$ with kernel $P$ and discount factor $a$ in the model of the Bandit Algorithms series, $x_i^\pi = \mathbb{E}^\pi \sum_t a^t I_i(t)$ is the discounted number of continuations of a bandit in state $i$, $A_i^S = \mathbb{E}[1 + a + \cdots + a^{T_i^S - 1}]$ is the discounted return time to $S$ from $i \in S$, and $b(S)$ is the minimal cost $\sum_{i \in S} A_i^S x_i^\pi$, namely $(1-a)^{-1}\mathbb{E}[a^\tau]$ with $\tau$ the number of continuations needed to bring every bandit into $S$.

Formalization targets

Goal: Theorem 5.5

For a GCL(1) system whose achievable region is convex, and any reward vector $r$: the achievable region is the polytope

its extreme points are performances of permutation policies; $AG(A, r)$ has an output; and for every output the permutation policy in the order it finds, the Gittins index policy, maximizes $\sum_i r_i x_i^\pi$ over all policies.

Milestones

Lemma 5.1 (the SFABP satisfies the conservation laws, with equality for policies giving priority to states outside $S$); the identification on p. 123 of the adaptive greedy indices of a SFABP with the Gittins indices, together with their monotonicity along the order found; Theorem 5.10, the GCL(2) counterpart of the goal for cost minimization.

Significance

Theorem 5.5 is the index theorem in its most general form of this kind: it says nothing about Markov chains, only that performances are expectations, objectives are linear and conservation laws hold, and it delivers both the optimal policy and the algorithm that computes its priorities in polynomial time in the number of job types. It is the theorem behind the index results for branching bandits and Klimov's multi-class queue and behind the suboptimality bounds of Sections 5.5 and 5.7, all of which are calculations on the polytope. Lemma 5.1 and the p. 123 identification are what tie the abstract theorem to the Gittins index: they show that the multi-armed bandit is a GCL(1) system and that the priorities the algorithm produces are the same indices as Chapters 2 to 4 define through stopping times.

None of these is machine-checked. Formalizing Theorem 5.5 puts an LP-duality index theorem on the platform in a form any system can instantiate by verifying its conservation laws; formalizing Lemma 5.1 relates the Bandit Algorithms run law to the single-chain return times, which is the first conservation law on that model; and the p. 123 theorem gives an algorithmic characterization of the Gittins index on finite chains, distinct from the restart and largest-remaining-index characterizations of Chapter 2.

Difficulty

The goal's optimality clause is weak LP duality once one shows that the greedy dual variables are nonpositive except $\bar y_E$ and satisfy the dual constraints with equality, which is a finite induction on the stages; the extreme-point clause needs that every vertex of a polyhedron is the unique maximizer of some linear functional, and the region clause that a compact convex set is the convex hull of its extreme points (Krein–Milman in finite dimension, or the polyhedral fact directly). None of this is in Mathlib in the required form. Lemma 5.1 is probabilistic: the lower bound requires the strong Markov property of the continued bandit under an arbitrary past-measurable policy, a pathwise accounting of the discounted periods paid for by each continuation from $S$, and the observation that at most $\tau$ slots can be spent on bandits that have never been in $S$; the equality for priority policies requires that these policies use exactly those slots first and then tile the future with return excursions, and the product form of $b(S)$ requires independence of the bandits' process-time trajectories under the run law, which is built decision time by decision time rather than as a product. The p. 123 theorem is the computation (5.13) to (5.14) combined with the optimal-stopping characterization of Chapter 2 for the stop sets $\{i_1, \dots, i_{k-2}\}$, which lie between $\{\nu < \nu(i_{k-1})\}$ and $\{\nu \le \nu(i_{k-1})\}$; ties make the induction delicate, and the statement is claimed for every tie-breaking.

Formalization scope

GCL(1) and GCL(2) systems are structures over an arbitrary policy type: performance, base function, matrix, permutation policies and the three laws are fields, so the theorems are statements about finite-dimensional data and the platform's proof needs no probability. The adaptive greedy algorithm is specified relationally, as the set of its possible outputs with arbitrary tie-breaking, and the conclusion holds for each of them; existence of an output is asserted separately. The optimality clause is stated as a comparison with every policy rather than as a real supremum. The hypothesis that the achievable region is convex is explicit: the book's argument from extreme points to the whole polytope uses randomization of policies, and without it the region of a system with only its permutation policies is finite. The SFABP items use $n$ identical bandits on Fin N in the Bandit Algorithms model, the coefficients $A_i^S$ through Mission I's stoppedTime at the return time, and $b(S)$ in the product form $(1-a)^{-1}\prod_{j : k_j \notin S}\mathbb{E}[a^{T^S_{k_j}}]$, which is the minimal cost the argument on p. 120 establishes; the book prints a sum, which is $0$ when all bandits start in $S$ where the minimal cost is $1/(1-a)$. Discount factors are in $(0, 1)$ throughout.

Trivializing readings are excluded: $A_i^S > 0$ for $i \in S$ is part of the structure and of Lemma 5.1's conclusion, the polytope equations are over all subsets, and the index clause quantifies over every greedy output. Welcome contributions: the nonpositivity and dual feasibility of the greedy variables, the vertex-exposure lemma for polyhedra, and the product decomposition of the run law of identical bandits.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 5. doi:10.1002/9780470980033
• D. Bertsimas, J. Niño-Mora, Conservation laws, extended polymatroids and multiarmed bandit problems; a polyhedral approach to indexable systems, Mathematics of Operations Research 21(2), 1996. doi:10.1287/moor.21.2.257
• P. Tsoucas, The region of achievable performance in a model of Klimov, IBM Research Report RC16543, 1991.
• E. G. Coffman, I. Mitrani, A characterization of waiting time performance realizable by single-server queues, Operations Research 28(3), 1980. doi:10.1287/opre.28.3.810
• K. D. Glazebrook, R. Garbe, Almost optimal policies for stochastic systems which almost satisfy conservation laws, Annals of Operations Research 92, 1999. doi:10.1023/A:1018992306696
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. doi:10.1017/9781108571401

Motivation

Two-stage stochastic programs with recourse — choose a first-stage decision $x$ now, observe a random outcome $\xi$, then choose a second-stage recourse decision $y(\xi)$ to repair whatever $x$ left infeasible or suboptimal — are the workhorse model of the field, used for capacity planning, inventory and financial portfolio problems since the 1950s (Dantzig 1955; Beale 1955). When $\xi$ ranges over a finite set of scenarios, the recourse function $Q$ that averages the second-stage cost over scenarios is piecewise linear and convex in $x$, so the overall problem is itself a large linear program — but one whose constraint matrix has a scenario for every column block and can be far too large to hand to a general-purpose LP solver directly. Van Slyke and Wets' L-shaped method (1969), the subject of this mission, is the algorithm that made two-stage recourse problems with finite scenario sets practically solvable: it is Benders decomposition specialized to this block structure, alternating between a small master program over $x$ (and a scalar $\theta$ approximating the recourse cost) and, at each candidate $x$, a batch of second-stage linear programs that either certify $x$'s second-stage feasibility or supply a linear underestimate — a cut — of $Q$ around $x$. Birge & Louveaux's Introduction to Stochastic Programming (2nd ed., Springer 2011), Chapter 5 §5.1, gives the algorithm and proves its two central guarantees: a shortcut feasibility test for a special case (Theorem 1) and the algorithm's finite convergence in general (Theorem 2), which is this mission's goal.

Setting

A two-stage recourse instance consists of a first-stage feasible region $K_1 = \{x \mid Ax = b,\ x \ge 0\}$ for $x \in \mathbb{R}^{n_1}$, and, for each of $K$ finite scenarios $k = 1, \dots, K$ (occurring with probability $p_k$), second-stage data $(q_k, h_k, T_k)$ defining the recourse subproblem

where the recourse matrix $W$ is fixed — the same across every scenario, the case this chapter treats. $K_2 = \{x \mid Q(x,\xi_k) < \infty \text{ for all } k\}$ is the set of $x$ for which every scenario's subproblem is feasible, and the two-stage problem is

A basis of the recourse subproblem is an injective choice of $m_2$ of $W$'s columns (where $m_2$ is $W$'s row count); each basis $b$ determines a simplex multiplier $\pi = (W_b^\top)^{-1} q_b$, and when $b$ attains the true optimum of $Q(x,\xi_k)$, LP duality gives $Q(x,\xi_k) = \pi^\top(h_k - T_k x)$ — the mechanism that turns a batch of second-stage LP solves into linear cuts on $x$.

Formalization targets

The L-shaped algorithm proceeds in three steps, repeated until neither applies:

• Step 1 solves the current master program (the $K_1$-feasible $x$, plus $\theta$ once at least one optimality cut exists, minimizing $c^\top x + \theta$ subject to every cut recorded so far — or just $c^\top x$ over $K_1$ before the first optimality cut, matching the book's convention that $\theta$ "is set equal to $-\infty$ and is not considered" until then).
• Step 2 tests each scenario's second-stage feasibility at the Step-1 optimum via an auxiliary LP; if some scenario fails (the LP's optimal value is positive), its optimal basis yields a feasibility cut and the algorithm returns to Step 1.
• Step 3, once every scenario is feasible, checks whether $\theta$ already dominates the true recourse cost at $x$ (using each scenario's optimal basis via LP duality); if not, an optimality cut is added and the algorithm returns to Step 1; if so, $x$ is optimal and the algorithm stops.

Goal — Chapter 5, Theorem 2 (p. 198)

Formalized as: starting from the empty cut set, there is a finite-length run of the algorithm's Step-1/2/3 transition relation, of length bounded by the total number of distinct feasibility- and optimality-cut witnesses available, ending at a state admitting no further step — at which point either the master program has become infeasible (certifying $K_1 \cap K_2 = \varnothing$) or its optimum is second-stage feasible, passes every fresh Step-3 test, and is optimal for the two-stage problem.

Milestone — Chapter 5, Theorem 1 (p. 194)

A shortcut avoiding $K$ separate feasibility LPs at Step 2: under these structural assumptions on $W$, checking feasibility at the single componentwise-worst right-hand side certifies feasibility at every scenario simultaneously.

Significance

Van Slyke and Wets' method (and Benders decomposition more generally, of which it is the recourse-problem specialization) underlies essentially every large-scale two-stage stochastic program solved in practice, and its finite-convergence guarantee — not merely that an optimum exists, but that this specific cutting-plane procedure reaches it in finitely many outer iterations — is what makes the method a decision procedure rather than a heuristic. The proof's content is an explicit finiteness argument (the number of distinct simplex bases of the recourse subproblem and the feasibility-test LP is finite, so the algorithm cannot generate infinitely many distinct cuts before either exhausting the feasible region or converging), not a general compactness or fixed-point argument; formalizing it means formalizing the cutting-plane mechanism itself as a transition system and proving termination combinatorially, over the finite type of available bases, rather than proving only that some optimal $x$ exists.

Difficulty

The natural shortcut — state only "an optimal $x$ exists, or $K_1 \cap K_2 = \varnothing$" — is not Theorem 2's actual content and is not what this mission targets: that weaker claim would already follow from $K_1 \cap K_2$ being a nonempty polyhedron (or empty), with no reference to the algorithm at all, and would not require the finiteness-of-bases argument the book's proof turns on. The genuine difficulty is representing Steps 1-3 faithfully as a relation on accumulating cut sets, and pinning the termination bound to the actual combinatorial object the book cites (the finite set of bases of the two LPs the algorithm solves at each iteration) rather than to a numeral or an abstract compactness bound. A second, quieter difficulty is Step 1's own optimum: once optimality cuts exist, the master program optimizes $c^\top x + \theta$ jointly, but before the first one it optimizes $c^\top x$ alone; conflating the two (e.g. always requiring $\theta$ to be part of the optimum) does not match Step 1 as the book states it.

Formalization scope

First-stage and second-stage vectors are Fin n1 → ℝ / Fin n2 → ℝ; the finite scenario set is Fin K with probability vector p. A basis is {b : Fin m2 → Fin n2 // Function.Injective b} (m2 = the recourse matrix's row count), matching "an injective choice of $m_2$ columns of $W$"; its finiteness is definitional, from Fin m2 → Fin n2 being finite. Simplex multipliers use Matrix.inv, whose junk value 0 on a singular matrix is never reachable in a proof because multipliers are only ever used through an IsOptimalAt/IsFeasBasisOptimalAt hypothesis that pins the basis to one genuinely attaining the LP's true optimum. The recourse value $Q(x,\xi_k)$ is EReal-valued (reusing this series' Instance/QVal convention from Chunk 03), so an optimality-cut witness's claimed value is compared to it by an explicit EReal cast, never by EReal arithmetic. The algorithm's state is a pair of finite sets of witnesses recorded so far (Finset (Fin K × FeasBasis n2 m2) × Finset (Fin K → Basis n2 m2)); Step is an inductive relation with one constructor per Step-2 and Step-3 branch, each requiring its witness not already recorded, and the goal states a bounded-length Step-path from the empty state to a state admitting no further Step. This mission does not restate Chapter 3's polyhedrality fact about $K_2$ as a separate lemma: the finiteness fact it is invoked for is already exposed directly and structurally by the finite Fintype bound on the number of bases, so no additional axiom stands in for it (see MODERATION_NOTES.md). Lemmas 3-9 and Theorem 10 of §5.2 (Regularized Decomposition, a different algorithm) are out of scope. The trivializing formalization this mission rules out is exactly the one named under Difficulty above: a bare existence-of-optimal-or- infeasible-$x$ statement with no reference to Steps 1-3 or to a finite bound on the number of iterations — such a statement would be true of any nonempty polyhedron and would not be Theorem 2.

Selected references

• R. Van Slyke and R. Wets, L-Shaped Linear Programs with Applications to Optimal Control and Stochastic Programming, SIAM Journal on Applied Mathematics, 17(4), 1969, pp. 638-663. https://doi.org/10.1137/0117061
• J. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer, 2011, Chapter 5. https://doi.org/10.1007/978-1-4614-0237-4
• G. Dantzig, Linear Programming under Uncertainty, Management Science, 1(3-4), 1955, pp. 197-206. https://doi.org/10.1287/mnsc.1.3-4.197

Motivation

Two-player zero-sum games and linear programming are, on their surface, unrelated pieces of 20th-century mathematics: von Neumann's minimax theorem for games (1928) was proved with tools from topology, and linear programming duality (Dantzig, 1940s) with convexity and geometry. Yet the two are formally equivalent — Dantzig recounts von Neumann conjecturing the equivalence outright, on first hearing a description of linear programming, because he had "just recently completed a book with Oscar Morgenstern on the theory of games" [Albers, Alexanderson, and Reid, More Mathematical People, 1990]. Freund and Schapire (1999) later showed that both concepts reduce, in one uniform way, to online regret minimization: a decades-old topological existence proof and a decades-old LP-duality argument both become corollaries of a single fact about no-regret learning. This mission formalizes the algorithmic content of that reduction — Hazan's Lemma 8.4, which is not merely an existence statement but a concrete, efficient algorithm with an explicit convergence rate.

Setting

A two-player zero-sum game in normal form is a real matrix $A \in \mathbb{R}^{n \times m}$ (Hazan restricts entries to $[-1,1]$ for interpretability as losses/rewards, a convention this mission's theorems drop as inessential — the argument is invariant to scaling and shifting). The row player picks a mixed strategy $x$ in the probability simplex $\Delta_n = \{x \in \mathbb{R}^n : x_i \ge 0, \sum_i x_i = 1\}$; the column player picks $y \in \Delta_m$. The row player's expected loss, and simultaneously the column player's expected reward, is the bilinear form $x^{\mathsf T} A y$.

The row player's guaranteed loss is $\lambda_R = \min_{x \in \Delta_n} \max_{y \in \Delta_m} x^{\mathsf T} A y$: the smallest loss she can secure no matter what the column player does. Symmetrically, the column player's guaranteed reward is $\lambda_C = \max_{y \in \Delta_m} \min_{x \in \Delta_n} x^{\mathsf T} A y$. Always $\lambda_R \ge \lambda_C$ ("weak duality" — an elementary max-min/min-max inequality, Direction 1 of Section 8.3). Von Neumann's minimax theorem (Theorem 8.3) is the nontrivial converse: $\lambda_R = \lambda_C$, a common value $\lambda^\star$ called the value of the game, whose optimal strategies form a Nash equilibrium — already on the platform as AGT.zero_sum_minimax.

Algorithm 28 ("Simple LP", p. 147) computes an approximate equilibrium constructively. The row player runs a multiplicative-weights / Exponentiated Gradient update against the sequence of best-response losses the column player generates in a repeated $T$-round play of the game: starting from the uniform strategy $x_1 = (1/n, \dots, 1/n)$, at each round $t$ the column player best-responds with $y_t \in \arg\max_{y \in \Delta_m} x_t^{\mathsf T} A y$, and the row player updates $x_{t+1}(i) \propto x_t(i)\, e^{-\eta (A y_t)_i}$. The algorithm returns the time-averaged strategy $\bar{x} = \frac{1}{T}\sum_{t=1}^T x_t$.

Formalization targets

Goal — Lemma 8.4

for the vector $\bar{x}$ returned by Algorithm 28 after $T$ rounds with learning rate $\eta = \sqrt{2 \log n / T}$. The book calls $\bar{x}$ a "$\sqrt{2 \log n}/\sqrt{T}$-approximate solution" to the zero-sum game — and, via Section 8.2.1's equivalence, to the linear program the game encodes — in exactly this sense. The goal is stated against $\lambda_R$, the quantity the algorithm's own analysis produces; Theorem 8.3 identifies it with $\lambda_C$ and with the book's $\lambda^\star$, so nothing about the bound is lost by this choice of rendering.

Supporting milestone — Eq. (8.1)

the external-regret bound the row player's multiplicative-weights update achieves against the adaptively-chosen linear loss sequence $f_t(\cdot) = (\cdot)^{\mathsf T} A y_t$ — the single analytical fact the goal's proof needs.

Significance

The result itself. Lemma 8.4 gives a genuinely efficient algorithm: $O(\log n / \varepsilon^2)$ rounds of a trivial multiplicative update to reach an $\varepsilon$-approximate value and equilibrium of an $n \times m$ zero-sum game, and — through the equivalence with LP duality — an approximation algorithm for a broad class of linear programs, predating and prefiguring the multiplicative-weights-based approximation schemes surveyed by Arora, Hazan, and Kale (2012). It is also the constructive engine behind Theorem 8.3: unlike the classical topological proof of the minimax theorem, this one produces the equilibrium, not just its existence.

Formalizing it. The equilibrium-existence half of this story, Theorem 8.3, is already a published, proved-format Prove2Me theorem (AGT.zero_sum_minimax, from the Algorithmic Game Theory series) and is reused here as a reference item rather than redrafted. What that theorem does not capture — and what makes this mission non-trivial rather than a restatement — is the quantitative, algorithmic content: that one specific, simple, Hedge-type update, run for a specific number of rounds, provably gets within a specific, explicit distance of the value, using only the existence of some sublinear-regret online algorithm as a black box.

Difficulty

The tempting shortcut is to formalize only "no-regret learning dynamics converge to an equilibrium" as a qualitative statement, discharging it by citing AGT.zero_sum_minimax (equilibria exist) plus a generic regret bound. That collapses Lemma 8.4 into a restatement of Theorem 8.3 and drops exactly what is new here: the explicit rate $\sqrt{2\log n}/\sqrt{T}$, tied to one concrete update rule (Algorithm 28) rather than an arbitrary sublinear-regret black box. The real content is in chaining three quantitative facts — Eq. (8.1)'s specific regret bound for the multiplicative-weights update, the column player's best-response equality (Eq. (8.2)), and the definitional unfolding of $\lambda_R$ — with none of the slack that a purely qualitative "an algorithm with sublinear regret exists" argument would tolerate.

Formalization scope

Matrices are Matrix (Fin n) (Fin m) ℝ with n, m ≥ 1 (empty strategy sets are excluded throughout, matching this mission's reference item AGT.zero_sum_minimax); mixed strategies use Mathlib's stdSimplex ℝ (Fin n). lambdaR/lambdaC are rendered with iInf/iSup over simplex membership, the same convention Introduction to Online Convex Optimization III fixed for RegretT earlier in this series. Algorithm 28's run is packaged as a Prop-valued structure (IsSimpleLPRun) rather than a computable function, in the style of this series' other algorithm-run definitions (IsHedgeRun, IsOnlineGradientDescent): initial uniform strategy, a best-response condition on the column player at every round, and the multiplicative-weights recursion on the row player, with the learning rate η left free and fixed to √(2 log n / T) only at the point the theorems need the book's specific constant.

The trivializing risk here is stating only that some sublinear-regret algorithm secures the bound (already implied, vacuously, by AGT.zero_sum_minimax plus any regret bound); this mission rules that out by fixing the exact update rule of Algorithm 28 in IsSimpleLPRun and proving the bound for that rule specifically, with the book's exact constant √(2 log n)/√T, not an unspecified O(·).

Chapter 5's Corollary 5.7 (the general RFTL/Exponentiated-Gradient regret bound) belongs to a different mission of this series and is not imported; eg_regret_bound restates, locally and self-containedly, exactly the instance of it this chapter's proof needs. A later mission for Chapter 5, once published, could supersede this local restatement by specializing its general bound — a natural contribution for a solver with that mission's Lean available.

Selected references

• J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen, 1928.
• Y. Freund and R. E. Schapire, "Adaptive Game Playing Using Multiplicative Weights", Games and Economic Behavior, 1999. https://doi.org/10.1006/game.1999.0738
• E. Hazan, Introduction to Online Convex Optimization, 2nd ed., 2022. arXiv:1909.05207v3
• N. Nisan, T. Roughgarden, E. Tardos, and V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007. https://doi.org/10.1017/CBO9780511800481
• S. Arora, E. Hazan, and S. Kale, "The Multiplicative Weights Update Method: a Meta-Algorithm and Applications", Theory of Computing, 2012. https://doi.org/10.4086/toc.2012.v008a006

Interior point methods solve linear programs by moving through the interior of the feasible set instead of along its edges — the approach that turned Karmarkar's 1984 breakthrough into today's practical large-scale solvers. This mission formalizes the primal path following algorithm of Chapter 9 of Bertsimas–Tsitsiklis. For $\mu > 0$ the logarithmic barrier

replaces the constraint $\mathbf{x} \ge \mathbf{0}$; the minimizers $\mathbf{x}(\mu)$ of $B_\mu$ over $\{A\mathbf{x} = \mathbf{b}\}$ trace the central path, characterized by the KKT conditions (9.17): $A\mathbf{x} = \mathbf{b}$, $\mathbf{x} \ge \mathbf{0}$, $A'\mathbf{p} + \mathbf{s} = \mathbf{c}$, $\mathbf{s} \ge \mathbf{0}$, $XS\mathbf{e} = \mu\mathbf{e}$ (Lemma 9.5). The algorithm follows the path with one Newton step of the barrier problem per shrink $\mu^{k+1} = \alpha\mu^k$, maintaining the proximity invariant

. The goal theorem is Theorem 9.7: with $\alpha = 1 - \frac{\sqrt{\beta}-\beta}{\sqrt{\beta}+\sqrt{n}}$ and a $\beta$-close start, after $K = \Big\lceil \frac{\sqrt{\beta}+\sqrt{n}}{\sqrt{\beta}-\beta}\,\log\frac{(\mathbf{s}^0)'\mathbf{x}^0(1+\beta)}{\varepsilon(1-\beta)} \Big\rceil$ iterations the algorithm reaches primal and dual feasible solutions with duality gap $(\mathbf{s}^K)'\mathbf{x}^K \le \varepsilon$ — the explicit form of the celebrated $O(\sqrt{n}\log(1/\varepsilon))$ iteration bound. Alongside it we formalize the generic potential-reduction scheme (Theorem 9.4): any algorithm cutting $G(\mathbf{x},\mathbf{s}) = q\log\mathbf{s}'\mathbf{x} - \sum_j \log x_j - \sum_j \log s_j$ by $\delta$ per step reaches gap $\varepsilon$ within an explicit $K$.

Can the feasibility of a system of linear inequalities be decided in a provably small number of iterations? The ellipsoid method — the algorithm with which Khachiyan showed in 1979 that linear programming is polynomially solvable — answers this with pure convex geometry. This mission formalizes Chapter 8 of Bertsimas–Tsitsiklis. An ellipsoid is

with $D$ symmetric positive definite. The geometric engine is Theorem 8.1: the half-ellipsoid $E \cap \{\mathbf{x} \mid \mathbf{a}'\mathbf{x} \ge \mathbf{a}'\mathbf{z}\}$ is contained in the explicitly constructed ellipsoid $E' = E(\bar{\mathbf{z}}, \bar{D})$,

and the volume contracts:

. Two integer-data estimates make the contraction decisive: every extreme point of $P = \{\mathbf{x} \mid A\mathbf{x} \ge \mathbf{b}\}$ with entries bounded by $U$ has coordinates in $[-(nU)^n, (nU)^n]$ (Lemma 8.2), and a full-dimensional bounded such polyhedron has $\mathrm{Vol}(P) > n^{-n}(nU)^{-n^2(n+1)}$ (Lemma 8.4). The goal theorem is Theorem 8.2: started on a ball $E(\mathbf{x}_0, r^2 I)$ of volume at most $V$ containing $P$, with $v$ a lower bound on $\mathrm{Vol}(P)$ when $P$ is nonempty, the ellipsoid method correctly decides whether $P$ is empty within $t^* = \lceil 2(n+1)\log(V/v) \rceil$ iterations — the explicit iteration count behind the polynomial-time headline.

Why do network linear programs return integer answers for free? This mission formalizes the structural theory of the minimum cost network flow problem of Chapter 7 of Bertsimas & Tsitsiklis: a directed graph $G=(\mathcal{N},\mathcal{A})$ with external supplies $b_i$, arc costs $c_{ij}$, and the node-arc incidence matrix $\mathbf{A}$ — an $n\times m$ matrix in which every column has exactly one $+1$ (start node) and one $-1$ (end node) — so that flow conservation reads $\mathbf{A}\mathbf{f}=\mathbf{b}$, forcing the standing assumption $\sum_{i\in\mathcal{N}} b_i=0$. Because the rows of $\mathbf{A}$ sum to zero, the book works with the truncated matrix $\tilde{\mathbf{A}}$ of the first $n-1$ rows. The combinatorial heart is the correspondence between algebra and graph structure: a set $T$ of $n-1$ arcs forming a tree determines a unique tree solution of $\tilde{\mathbf{A}}\mathbf{f}=\tilde{\mathbf{b}}$, $f_{ij}=0$ off $T$ (Theorem 7.3); connectedness makes $\tilde{\mathbf{A}}$ full-rank (Corollary 7.1); and a flow vector is a basic solution if and only if it is a tree solution (Theorem 7.4). The goal theorem is the integrality theorem (Theorem 7.5): for the uncapacitated problem on a connected graph, every basis matrix $\mathbf{B}$ has an integer inverse $\mathbf{B}^{-1}$ (its determinant is $\pm 1$ by the tree/lower-triangular argument), integer supplies make every basic solution integer, and integer costs make every dual basic solution integer — whence integer optimal primal and dual solutions exist whenever the optimal cost is finite (Corollary 7.2). This is the fountainhead of combinatorial integrality in linear optimization, feeding the max-flow min-cut mission that follows.

How does the optimal cost of a linear program respond when the problem data change? Chapter 5 of Bertsimas-Tsitsiklis studies the standard form problem $\min\{c'x \mid Ax = b,\ x \ge 0\}$ (rows of $A$ linearly independent) as the requirement vector $b$ and the cost vector $c$ vary. On the convex set $S = \{b \mid P(b) \neq \emptyset\}$ of feasible right-hand sides, and under the standing assumption that the dual feasible set is nonempty, the optimal cost $F(b)$ is finite and convex (Theorem 5.1) — indeed $F(b) = \max_{i} (p^i)'b$ over the extreme points $p^1, \dots, p^N$ of the dual feasible set, a piecewise linear convex function whose breakpoints are exactly where the dual optimum is non-unique. The capstone (Theorem 5.2) identifies the generalized gradients of $F$: if the primal at $b^*$ is feasible with finite optimal cost, then $p$ is an optimal solution of the dual if and only if $p$ is a subgradient of $F$ at $b^*$ (Definition 5.1: $F(b^*) + p'(b - b^*) \le F(b)$ for all $b \in S$) — the precise sense in which dual variables are marginal costs. Dually (Theorem 5.3), the set $T$ of cost vectors with finite optimal cost is convex, the optimal cost $G(c)$ is concave on $T$, and near any $c$ with a unique primal optimum $x^*$, $G$ is linear with gradient $x^*$. Local ranging (Section 5.1) and parametric programming (Section 5.5) are the procedural companions, folded into the design notes.

Every linear programming problem has a shadow. To the primal $\min c'x$ we associate the dual $\max p'b$, whose variables price the primal constraints: one dual variable per primal constraint and one dual constraint per primal variable, with signs governed by the correspondence of Table 4.1. This mission formalizes §4.1–4.5 of Bertsimas–Tsitsiklis: the dual of a general-form linear program, the involution "the dual of the dual is the primal" (Theorem 4.1), and weak duality $p'b \le c'x$ for any primal-feasible $x$ and dual-feasible $p$ (Theorem 4.3) with its two corollaries — an unbounded primal forces an infeasible dual (Corollary 4.1), and feasible $x, p$ with $p'b = c'x$ are automatically both optimal (Corollary 4.2). The goal theorem is strong duality (Theorem 4.4): if a linear programming problem has an optimal solution, so does its dual, and the respective optimal costs are equal — proved in the book by running the simplex method with the lexicographic pivoting rule of Mission IV on a standard-form transform. The statement is deliberately the book's attainment form: by Table 4.2 the primal and the dual can be simultaneously infeasible (Example 4.5), so an unguarded equality of optimal values is false. The mission closes with complementary slackness (Theorem 4.5): feasible $x$ and $p$ are simultaneously optimal if and only if $p_i(a_i'x - b_i) = 0$ for all $i$ and $(c_j - p'A_j)x_j = 0$ for all $j$ — the certificate structure behind the dual simplex method and every LP optimality check.

How does one actually solve a linear program? Chapter 2 showed that if a standard-form problem $\min c'x$ subject to $Ax = b$, $x \ge 0$ has an optimal solution, it has an optimal basic feasible solution; the simplex method searches among basic feasible solutions, moving along edges of the feasible set in cost-reducing directions. This mission formalizes the mathematics of Chapter 3 of Bertsimas–Tsitsiklis: feasible directions, the reduced costs

measuring the cost rate along the basic directions, the optimality conditions of Theorem 3.1 ($\bar{c} \ge 0$ implies optimality, and conversely at nondegenerate optima), the basis change of Theorem 3.2, and the pivot iteration itself — encoded as a predicate relating a basis/BFS pair to its successor, so that every theorem covers every pivoting rule. The goal theorem is Theorem 3.3: if the feasible set is nonempty and every basic feasible solution is nondegenerate, the simplex method terminates after a finite number of iterations, ending either with an optimal basis and an associated optimal basic feasible solution, or with a direction $d$ satisfying $Ad = 0$, $d \ge 0$, $c'd < 0$ certifying optimal cost $-\infty$. The secondary capstone, Theorem 3.4, removes the nondegeneracy assumption: under the lexicographic pivoting rule every tableau row other than the zeroth stays lexicographically positive, the zeroth row strictly increases lexicographically, and the simplex method terminates on every problem — the anticycling guarantee that also supplies the optimal-basis existence used by the strong duality theorem of Mission V.

Every linear programming problem asks to minimize a linear cost $c'x$ over a polyhedron — a set of the form $P = \{x \in \mathbb{R}^n \mid Ax \ge b\}$, or in standard form $\{x \mid Ax = b,\ x \ge 0\}$. Chapter 2 of Bertsimas–Tsitsiklis develops the geometry of these feasible sets, and its central achievement is making the intuitive notion of a "corner point" rigorous. There are three natural candidates: the extreme point — a point of $P$ that cannot be written as a convex combination of two other points of $P$ (purely geometric, representation-independent); the vertex — the unique minimizer of some linear cost $c'y$ over $P$ (geometric, via supporting hyperplanes); and the basic feasible solution — a feasible point at which $n$ linearly independent constraints are active (algebraic, the object the simplex method actually computes with). This mission formalizes polyhedra, active constraints, vertices and basic (feasible) solutions, and proves the fundamental Theorem 2.3: for a nonempty polyhedron all three notions coincide. Around the capstone sit the supporting pillars: polyhedra are convex (Theorem 2.1), the characterization of points pinned down by $n$ linearly independent active constraints (Theorem 2.2), finiteness of the set of basic solutions (Corollary 2.1), and the basis-column characterization of basic solutions in standard form (Theorem 2.4) — the combinatorial engine behind the simplex method of Chapter 3 and the root of the entire series.