Linear Optimization

Motivation

Two-stage adaptive optimization models decisions taken in two rounds: a first-stage decision $x$ is fixed before an uncertain parameter is revealed, and a second-stage decision $y(b)$ is chosen after the parameter $b$ is observed, so that the second stage may depend on $b$ arbitrarily. The objective is the worst case over an uncertainty set $\mathcal U$ of possible parameters. Such models arise in robust network design, capacity planning and two-stage covering problems, and they generalize the two-stage robust combinatorial problems (set cover, facility location) studied by Dhamdhere, Goyal, Ravi and Singh.

Optimizing over all functions $y(\cdot)$ is intractable in general: Bertsimas and Goyal note that the optimal second stage is piecewise linear in $b$ with possibly exponentially many pieces (Bemporad, Borrelli and Morari, 2003). A standard remedy, introduced for robust linear programs by Ben-Tal, Goryashko, Guslitzer and Nemirovski (2004), restricts the second stage to affine policies (linear decision rules) $y(b)=Pb+q$; the best affine policy is computable by a single convex program and performs well empirically. The question is when this restriction loses nothing.

Timeline of the relevant results:

• 2004. Ben-Tal, Goryashko, Guslitzer and Nemirovski introduce affinely adjustable robust counterparts and show that the best affine policy is tractable for many uncertainty sets (doi:10.1007/s10107-003-0454-y).
• 2010. Bertsimas, Iancu and Parrilo prove that affine policies are optimal for a class of multistage robust problems with one-dimensional uncertainty per stage and box uncertainty sets (doi:10.1287/moor.1100.0444).
• 2012. Bertsimas and Goyal, the source of this mission, prove that an affine policy is optimal for model (1) whenever $\mathcal U$ is a simplex (Theorem 1), and show that this exactness breaks down for slightly larger sets (doi:10.1007/s10107-011-0444-4).

Setting

Let $A\in\mathbb R^{m\times n_1}$, $B\in\mathbb R^{m\times n_2}$, $c\in\mathbb R^{n_1}_+$ and $d\in\mathbb R^{n_2}_+$. The problem $\Pi_{Adapt}(\mathcal U)$ of model (1) is

$$z_{Adapt}(\mathcal U)=\min\ c^Tx+\max_{b\in\mathcal U}d^Ty(b)\quad\text{s.t.}\quad Ax+By(b)\ge b,\ \ x\ge 0,\ \ y(b)\ge 0\quad\forall b\in\mathcal U,$$

where inequalities between vectors are componentwise. A pair $(x,y)$ satisfying the constraints is feasible; its worst-case cost is $c^Tx+\max_{b\in\mathcal U}d^Ty(b)$. A feasible pair is optimal when its worst-case cost equals $z_{Adapt}(\mathcal U)$, and an affine policy is a second stage of the form $y(b)=Pb+q$ with $P\in\mathbb R^{n_2\times m}$, $q\in\mathbb R^{n_2}$, still required to be nonnegative on $\mathcal U$. The value $z_{Aff}(\mathcal U)$ is the same minimum restricted to affine policies.

A simplex in $\mathbb R^m$ is the convex hull

$$\mathcal U=\operatorname{conv}(b^1,\dots,b^{m+1})$$

of $m+1$ affinely independent points, that is, points for which $b^1-b^{m+1},\dots,b^m-b^{m+1}$ are linearly independent. The proof works with the $m\times m$ matrix $Q=[(b^1-b^{m+1})\cdots(b^m-b^{m+1})]$, the matrix $Y=[(y^*(b^1)-y^*(b^{m+1}))\cdots(y^*(b^m)-y^*(b^{m+1}))]$ of display (2), and the affine rule $\tilde y(b)=YQ^{-1}(b-b^{m+1})+y^*(b^{m+1})$. In Lean these are Qmat v, Ymat v g and interpolant v g, with vertices v : Fin (m+1) → Fin m → ℝ.

Formalization targets

Goal: Theorem 1

If $\mathcal U=\operatorname{conv}(b^1,\dots,b^{m+1})$ with affinely independent $b^j\in\mathbb R^m_+$ and $\Pi_{Adapt}(\mathcal U)$ is feasible, then there exist $\hat x$, $P\in\mathbb R^{n_2\times m}$ and $q\in\mathbb R^{n_2}$ such that

$$(\hat x,\ \hat y),\qquad \hat y(b)=Pb+q\ \ (b\in\mathcal U),$$

is an optimal solution of $\Pi_{Adapt}(\mathcal U)$, optimal among all (not only affine) two-stage solutions. In particular $z_{Aff}(\mathcal U)=z_{Adapt}(\mathcal U)$.

Milestones

The proof of Theorem 1 has no numbered lemma; the milestones are its displayed steps, in attack order:

1. $Q$ is invertible (PDF p. 6).
2. For $b=\sum_j\alpha_jb^j$ with $\sum_j\alpha_j=1$: $Q^{-1}(b-b^{m+1})=(\alpha_1,\dots,\alpha_m)^T$ (PDF p. 6).
3. $\tilde y\big(\sum_j\alpha_jb^j\big)=\sum_j\alpha_j\,y^*(b^j)$ (PDF pp. 6–7).
4. Displays (3)–(5): for any feasible $(x^*,y^*)$, the pair $(x^*,\tilde y)$ is feasible and every bound on the worst-case cost of $(x^*,y^*)$ also bounds that of $(x^*,\tilde y)$ (PDF p. 7).

Significance

The result. Theorem 1 identifies a class of uncertainty sets on which the tractable affine restriction is exact, for every constraint matrix $A$ and $B$ and every nonnegative cost. It is the positive anchor of the paper: Sections 3 and 4 show that with $m+3$ extreme points the best affine policy can already be worse by a factor $2-\delta$, and that on sets with exponentially many extreme points the gap can be $\Omega(m^{1/2-\delta})$; Section 6 uses a dominating simplex, on which affine policies are exact, to build an $O(\sqrt m)$-approximation for general $\mathcal U$. The theorem also says that on a simplex the whole adaptive problem reduces to $m+1$ scenario copies of a linear program.

Formalizing it. The result is proved on paper; no machine-checked version is known on Prove2Me. This mission produces the model (1) in Lean, the barycentric-coordinate identity for a simplex in matrix form, and a statement of optimality that asserts attainment of the minimum in (1), which the paper's proof takes for granted.

Difficulty

Two steps are not routine to formalize. First, the paper starts from "an optimal solution $x^*,y^*(b)$", that is, it assumes the minimum in (1) is attained. Over arbitrary functions $y(\cdot)$ this is not automatic; on a simplex it follows because the problem reduces to a finite linear program on the vertices, whose optimum is attained, but Mathlib has no theory of linear-programming attainment, so this reduction has to be built. Second, the affine-independence step needs the passage from affine independence of $m+1$ points to invertibility of the $m\times m$ matrix $Q$, and the identity $Q^{-1}(b-b^{m+1})=\alpha$ requires the barycentric coordinates and the inverse matrix to be matched index by index. The naive idea of comparing $z_{Aff}$ and $z_{Adapt}$ as real infima does not prove the goal: equality of the two infima says nothing about the existence of an optimal solution.

Formalization scope

Vectors in $\mathbb R^m$ are Fin m → ℝ, with the componentwise order; matrices are Matrix (Fin m) (Fin n) ℝ. The paper's indices start at $1$, Lean's at $0$: $b^j$ is v (j-1) and $b^{m+1}$ is v (Fin.last m). The simplex is convexHull ℝ (Set.range v); it is compact, convex and, by affine independence, full-dimensional, so these standing assumptions of (1) are not stated separately. Nonnegativity of $\mathcal U$ is the hypothesis that all $m+1$ vertices are nonnegative (the page writes $j=1,\dots,m$, a slip for $m+1$). Feasibility of (1) is a hypothesis, as the paper assumes. Optimality (IsOptimalAdapt) means: feasible, and every worst-case cost bound achieved by any feasible two-stage solution is achieved by this one. The values $z_{Adapt}$ and $z_{Aff}$ are infima of the sets of achievable bounds; they are provided for reference and the goal does not depend on them.

The goal must not be replaced by $z_{Aff}(\mathcal U)\le z_{Adapt}(\mathcal U)$, by optimality among affine policies only, or by a version that assumes an optimal solution exists: each of these drops the content "there is an optimal solution and it is affine". The goal does not mention $Q$, $Y$ or the interpolant.

A complete development needs: linear-programming attainment for a finite system of linear inequalities with a cost bounded below (reusable well beyond this mission), the linear-algebra lemmas relating affine independence to an invertible edge matrix (reusable for barycentric coordinates in general), and the convex-hull representation of points of a simplex. Contributions of any of these as separate lemmas are welcome.

Selected references

• D. Bertsimas, V. Goyal, On the power and limitations of affine policies in two-stage adaptive optimization, Math. Program. Ser. A, 2012. doi:10.1007/s10107-011-0444-4
• A. Ben-Tal, A. Goryashko, E. Guslitzer, A. Nemirovski, Adjustable robust solutions of uncertain linear programs, Math. Program. 99(2), 351–376, 2004. doi:10.1007/s10107-003-0454-y
• D. Bertsimas, D. A. Iancu, P. A. Parrilo, Optimality of affine policies in multistage robust optimization, Math. Oper. Res. 35(2), 363–394, 2010. doi:10.1287/moor.1100.0444
• A. Bemporad, F. Borrelli, M. Morari, Min–max control of constrained uncertain discrete-time linear systems, IEEE Trans. Autom. Control 48(9), 1600–1606, 2003. doi:10.1109/TAC.2003.816984

Motivation

Linear programming asks for the best value of a linear objective under linear constraints. In the form studied by George B. Dantzig in 1951, all variables are nonnegative and the constraints are equalities. The simplex technique moves between small sets of columns, seeking a feasible vector first and then improving its objective. Its basic promise is operational: a run should end with a valid answer, whether that answer is a maximum, infeasibility, or an objective that can grow without bound. Dantzig's chapter sets out both phases and the tests that distinguish these outcomes.

The formulation matters to readers of optimization because it separates the algebraic claim about a linear program from a particular rule for selecting the next column. The chapter permits any entering column satisfying the stated improvement test. This mission captures the correctness claim for every sequence of admissible choices under the chapter's nondegeneracy assumption, with one additional general-position condition needed for the Phase I argument.

Setting

Fix integers $1\le m\le n$. Let $P_0\in\mathbb R^m$ be a right-hand side, $P_1,\ldots,P_n\in\mathbb R^m$ be columns, and $c_1,\ldots,c_n\in\mathbb R$ be objective coefficients. A feasible solution is a weight vector $\lambda\in\mathbb R^n$ with $\lambda_j\ge0$ and $\sum_j\lambda_jP_j=P_0$. Its objective value is $z(\lambda)=\sum_j\lambda_jc_j$. It is maximum feasible when $z(\mu)\le z(\lambda)$ for every feasible $\mu$. Unboundedness means that feasible objective values exceed every real threshold.

Dantzig assumes nondegeneracy: every indexed selection of $m$ points among $P_0,P_1,\ldots,P_n$ is linearly independent. A Phase II state uses exactly $m$ basic columns $B$, each with a positive weight, and represents $P_0$ with them. Every column has unique coordinates $P_j=\sum_{i\in B}x_{ij}P_i$, and $z_j=\sum_{i\in B}x_{ij}c_i$ is the corresponding objective value. A column with $c_j>z_j$ can improve the objective. When some $x_{ij}>0$, the step uses the smallest ratio $\lambda_i/x_{ij}$ over those positive coordinates and replaces a minimizing basic column.

A Phase I state begins from $m-1$ basic columns $S$ and a fixed reference point $G$. Positive weights $w_i$ and $\rho>0$ satisfy $G+\rho P_0=\sum_{i\in S}w_iP_i$. Write $P_j=y_{0j}P_0+\sum_{i\in S}y_{ij}P_i$. A column with $y_{0j}>0$ either gives a new Phase I basis through the positive-ratio test or supplies the nonnegative weights in equation (39), which start Phase II.

Formalization targets

The goal is the correctness of the complete two-phase transition system. There is no infinite admissible run. Every state with no outgoing transition has one of three outcomes:

$$\begin{array}{ll} \text{Phase I:}& y_{0j}\le0\ (\forall j),\quad \text{no feasible solution};\\ \text{Phase II:}& \exists j\ (c_j>z_j\ \land\ x_{ij}\le0\ (\forall i\in B)),\quad \forall M\in\mathbb R\ \exists\lambda\text{ feasible}: z(\lambda)>M;\\ \text{Phase II:}& c_j\le z_j\ (\forall j),\quad z(\mu)\le z(\lambda)\text{ for every feasible }\mu. \end{array}$$

The five milestones follow the chapter's own statements: Theorem 3's infeasibility certificate, Section 2's termination and hand-off, Theorem 1's improving family and two cases, Section 1's termination alternatives, and Theorem 2's optimality test. The goal includes the hand-off from the first phase to the second; the milestones make each outcome separately auditable.

Significance

The result gives a complete outcome guarantee for the chapter's procedure under its stated nondegeneracy regime. A terminal basis satisfying $c_j\le z_j$ is certified optimal against every feasible solution, not just against nearby bases. The other terminal tests certify properties of the original problem: nonexistence of feasible weights or arbitrarily large feasible objective values. This is the distinction needed to use the procedure as an algorithm for an LP rather than merely a local improvement rule.

The chapter's Theorems A and B assert existence of a basic feasible solution, and existence of a basic optimal one when the objective is bounded above. A proved platform theorem on basic optimal solutions covers these structural results after changing minimization cost $q$ to $-c$; it is included by reference. Existing simplex results in the platform's minimization convention do not state Dantzig's Phase I reference-point process or his $x_{ij}$ and $z_j$ tests. Formalizing this mission adds that two-phase interface and a machine-checkable statement of its outcomes.

Difficulty

An improving column alone does not say whether another basis exists. In Phase II, the signs of its basis coordinates determine whether the positive weights meet a finite ratio limit or instead continue along an unbounded feasible family. In Phase I, the analogous limit must preserve strictly positive weights on exactly $m-1$ columns. The printed argument says that a coefficient vanishes at the limit, but does not exclude two coefficients vanishing together. That gap matters because the next state in the paper's recurrence must again have strictly positive basic weights. The mission states a general-position condition on $G$ that rules out this simultaneous-vanishing case. It is an explicit addition to the printed assumptions and should be reviewed as such.

Formalization scope

Lean uses Fin n → (Fin m → ℝ) for the columns, Fin m → ℝ for $P_0$ and $G$, Fin n → ℝ for weights and costs, and finite sets for bases. Its zero-based Fin n labels correspond to the paper's $1,\ldots,n$. Each state carries its basis cardinality, independence, coordinate equations, and strictly positive basic weights. This keeps the coordinate functions defined on genuine bases and prevents a zero-weight intermediate state from counting as a valid pivot. The transition relation records every admissible entering column and minimizing leaving index; the pivot-selection heuristics (20) and (21) are outside the claim.

The phrases “upper bound of $z$ is infinite” and “process terminates” are read as, respectively, objective values above every real threshold on the original feasible set and absence of an infinite sequence of admissible steps. “A feasible solution has been obtained” is the explicit vector of equation (39), not an unnamed existence assertion. Maximum feasible means feasible plus comparison with every feasible vector, avoiding a real supremum's empty-set default. The dimensions $1\le m\le n$ make both kinds of basis possible and prevent a vacuous nondegeneracy condition. General position asks every family containing $G$, $P_0$, and $m-2$ distinct $P_j$ to be independent. The paper does not write this condition, so its inclusion is a substantive qualification of the target.

The printed indices in (30), (45), and a sentence following (18) do not match their defining ranges. The Lean statements use all $n$ columns for $j$ and the current $m-1$ Phase I columns for $i$. The indices in (17) and (45) also carry the entering conditions $c_j>z_j$ and $y_{0j}>0$, respectively. These corrections preserve the paper's described procedure and prevent a terminal test from becoming trivial through a basic column. Contributions may address the finite-state termination argument, the ratio-test lemmas, coordinate uniqueness, and the translation from terminal signs to the three global LP outcomes. The operation counts and geometric interpretation on the last pages are outside the formalization.

Selected references

• George B. Dantzig, “Maximization of a Linear Function of Variables Subject to Linear Inequalities,” in T. C. Koopmans (ed.), Activity Analysis of Production and Allocation, Wiley, 1951, Chapter XXI, pp. 339–347. Book catalog search.
• Hartmann_Psi, “A bounded feasible standard-form LP attains its minimum at a basic feasible solution,” Prove2Me, proved platform theorem. Theorem record.
• Shuze Chen, “Finite termination of the simplex method under nondegeneracy,” Prove2Me, proved platform theorem in a minimization convention. Theorem record.

Motivation

A matching in a graph is a set of edges no two of which share a node. Given a real weight on every edge, the maximum-weight matching problem asks for a matching of largest total weight. It is one of the basic problems of combinatorial optimization: assignment, pairing and scheduling problems reduce to it, and it is the standard example of a combinatorial problem that is solvable in polynomial time although it is not obviously a linear program.

For bipartite graphs the problem is a linear program in disguise: the polytope cut out by nonnegativity and the node-degree inequalities has only 0–1 vertices (the Birkhoff–von Neumann theorem in the square case; Mathlib has it as extremePoints_doublyStochastic). For general graphs this fails already on a triangle, where the vector with every coordinate $1/2$ satisfies all degree inequalities but is not a combination of matchings. Edmonds' 1965 paper (DOI 10.6028/jres.069b.013) adds one family of inequalities, one for each odd set of nodes, and proves that the resulting polyhedron has exactly the matching vectors as its vertices. The companion paper Paths, trees, and flowers gives the cardinality algorithm on which the weighted algorithm of §7 is built.

Timeline:

• 1931: König and Egerváry prove the min–max theorems for bipartite matching; 1946: Birkhoff shows that the doubly stochastic matrices are the convex hull of the permutation matrices (the bipartite perfect-matching polytope).
• 1947: Tutte characterizes graphs with a perfect matching.
• 1965: Edmonds, Paths, trees, and flowers: the blossom algorithm for maximum-cardinality matching.
• 1965: Edmonds, this paper: Theorem (P) (the matching polyhedron) and Theorem (M) (blossom-shrinking optimality certificates), with a weighted matching algorithm.

Setting

Let $G$ be a finite graph with node set $V$ and edge set $E$; each edge meets two different nodes, its ends. Real variables $x_e$ correspond to the edges $e\in E$. The polyhedron $C\subseteq\mathbb R^E$ is the set of vectors $x$ satisfying

1. $x_e\ge 0$ for every edge $e$;
2. $\sum_{e \text{ meets } v} x_e\le 1$ for every node $v$;
3. $\sum_{e \text{ has both ends in } S} x_e\le r$ for every set $S$ of $2r+1$ nodes, $r$ a strictly positive integer.

The matching vectors $P$ are the vectors with every component $0$ or $1$ that satisfy (2); they are the incidence vectors of matchings. For edge weights $c\in\mathbb R^E$, the linear form (4) is $W(c,x)=\sum_e c_e x_e$.

The dual program has a variable $y_v$ for each node and $z_S$ for each odd set $S$ ($|S|=2r_S+1$, $r_S\ge1$). Its objective is (5) $U(y,z)=\sum_v y_v+\sum_S r_S z_S$, subject to (6) $y,z\ge0$ and (7) $y_{v_1}+y_{v_2}+\sum_{S\ni v_1,v_2}z_S\ge c_e$ for every edge $e$ with ends $v_1,v_2$. For a matching $M$, conditions (8)–(10) are the complementary slackness conditions: $y_v=0$ at nodes not covered by $M$, equality in (7) on $M$, and every odd set with $z_S>0$ contains exactly $r_S$ edges of $M$.

A blossom sequence $\{G_i\}_{i=0}^n$ (Theorem (M)) starts from $G_0=G$ with matching $M_0=M$ and repeatedly shrinks an odd circuit $B_i$ (a blossom, $2a_i+1$ edges of which $a_i$ are matched) to a single node, carrying node weights $w(v^i)$ and edge weights $w(e^i)$ that obey conditions (a)–(k) of p. 127.

In the Lean development these are Graph, IsMatching, incidence, matchingPolyhedron ($C$), matchingVectors ($P$), W, U, DualFeasible ((6)–(7)), CompSlack ((8)–(10)) and BlossomSequence, all in the namespace EdmondsMatching65.Polyhedron.

Formalization targets

Goal: Theorem (P)

$$\operatorname{ext}(C)=P.$$

The vertices (extreme points) of $C$ are exactly the matching vectors of $G$. Hence the maximum weight of a matching equals $\max\{W(c,x):x\in C\}$ for every $c$.

Milestones

1. $P\subseteq\operatorname{ext}(C)$ (§2, p. 126).
2. If for every $c$ some 0–1 point of $C$ maximizes $W(c,\cdot)$ over $C$, then $\operatorname{ext}(C)=P$ (§2, p. 126).
3. Weak duality: $W(c,x)\le U(y,z)$ for $x\in C$ and $\langle y,z\rangle$ satisfying (6)–(7) (§3, p. 126).
4. If $M$ is a matching and $\langle y,z\rangle$ satisfies (6)–(10), then $W(c,\chi^M)=U(y,z)$ (§3, p. 127).
5. A blossom sequence for $M$ yields $\langle y,z\rangle$ satisfying (6)–(10) (§5, pp. 127–128).
6. For every $c$ some maximum matching has a blossom sequence (§6, p. 128).
7. Theorem (M): a matching is maximum if and only if a blossom sequence for it exists (§4, p. 127).
8. For every $c$ there are a matching $M$ and $\langle y,z\rangle$ satisfying (6)–(10) (§3, p. 127).

Significance

The result. Theorem (P) turns maximum-weight matching in general graphs into a linear program over an explicitly described polyhedron, and Theorem (M) with the §5 translation gives a short certificate of optimality for every maximum matching. Together they established the template of polyhedral combinatorics: describe the convex hull of the combinatorial objects by inequalities, and prove the description through linear programming duality and an algorithm. The matching polytope underlies the analysis of the weighted blossom algorithm, separation over odd-set inequalities (Padberg–Rao), and many later integrality results; Edmonds' own §8 states the extension to degree-constrained subgraphs.

Formalizing it. The theorem has been proved since 1965 and appears in every text on combinatorial optimization; this mission asks for a machine-checked proof of the polytope statement for general finite graphs, including parallel edges, together with the duality certificate and the blossom-sequence characterization. The prove2me platform has a proved form of Edmonds' perfect matching polytope theorem on complete graphs in convex-decomposition form (MetricTSP.pm_polytope_decomposition), a different polytope with a different conclusion; nothing states Theorem (P) or Theorem (M).

Difficulty

The inclusion $P\subseteq\operatorname{ext}(C)$ and weak duality are routine. The difficulty is the reverse inclusion: showing that no fractional point of $C$ is a vertex. The bipartite argument (a fractional point has a cycle of fractional edges along which it can be perturbed both ways) breaks on odd cycles: perturbing along an odd circuit violates a degree inequality, and the odd-set inequalities that cut off the half-integral points are exponentially many and overlap. The paper's route needs, for every weight vector, an optimal matching together with a dual solution satisfying (6)–(10), and the existence of that certificate is the substance of the weighted matching algorithm: the blossom sequence of Theorem (M) must be constructed, and the translation (11)–(16) from node and edge weights of the contracted graphs to $\langle y,z\rangle$ must be verified through the whole shrinking history.

Formalization scope

• The graph is a finite node type V, a finite edge type E and an end map ends : E → Sym2 V with no loops. Parallel edges are allowed: the contracted graphs of Theorem (M) have them, and Theorem (P) holds for multigraphs; simple graphs are the case of an injective end map.
• Vectors are E → ℝ, one coordinate per edge. Vertices are Mathlib's Set.extremePoints ℝ. Odd sets carry an explicit r : ℕ with 1 ≤ r and |S| = 2r + 1; even sets and singletons carry no inequality.
• Edge weights are arbitrary reals; matchings need not be perfect and may be empty. No connectivity, no parity of |V|.
• The dual variable z is a function on all node sets of which only odd sets are read.
• A contracted graph Gᵢ is a partition of V into blocks; an edge of G is an edge of Gᵢ when its ends lie in different blocks. Each Mᵢ must be a matching of Gᵢ, and all of (a)–(k) appear as fields of BlossomSequence; a sequence missing any of them would make milestone 6 trivial or milestone 5 false.
• A trivializing formalization is ruled out: coordinates indexed by node pairs (Sym2 V → ℝ) leave non-edge coordinates free and give a polyhedron with no extreme points, and the goal is stated as equality of extreme points, not as a convex-hull identity or as the existence of a dual certificate.
• Needed infrastructure: extreme points of polyhedra as unique maximizers of linear forms, finite LP weak duality over these index sets, and the weighted blossom algorithm (or another proof of milestone 8). The polyhedral lemmas are reusable for other integrality results; contributions on any milestone are welcome.

Selected references

• J. Edmonds, Maximum Matching and a Polyhedron With 0,1-Vertices, J. Res. Nat. Bur. Standards Sect. B 69B (1965), 125–130. https://doi.org/10.6028/jres.069b.013
• J. Edmonds, Paths, Trees, and Flowers, Canad. J. Math. 17 (1965), 449–467. https://doi.org/10.4153/CJM-1965-045-4
• W. T. Tutte, The Factorization of Linear Graphs, J. London Math. Soc. 22 (1947), 107–111. https://doi.org/10.1112/jlms/s1-22.2.107
• M. W. Padberg, M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Math. Oper. Res. 7 (1982), 67–80. https://doi.org/10.1287/moor.7.1.67
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Chapter 25.

Linear programming for Markov decision problems

A Markov decision problem asks how to control a system that moves at random between finitely many states, where each decision changes the probabilities of the next move and incurs a cost. Cyrus Derman's 1962 paper On Sequential Decisions and Markov Chains (Management Science 9(1):16–24) treats two criteria: the long-run average cost per period, and the total cost of driving the system into an absorbing state. Its Theorem 2 shows that, once attention is restricted to stationary procedures, each problem can be solved as a linear program over the state-action frequencies of the procedure. This mission formalizes that theorem, its supporting displays (3)–(10) and its Lemma on linear-fractional programs.

The linear programming formulation is now the standard computational and theoretical tool for constrained Markov decision processes, and its variables, the occupation measures, are the objects of most later work on that topic. Derman's paper is among the first to state it for the average-cost criterion. Manne (Linear Programming and Sequential Decisions, Management Science, 1960) gave an earlier average-cost formulation for an inventory model. The reduction of a ratio of linear functions to a linear program in Derman's Lemma is the transformation published in the same year by Charnes and Cooper (Programming with Linear Fractional Functionals, Naval Research Logistics Quarterly, 1962).

Setting

There are finitely many states $0, \dots, L$ and decisions $d_1, \dots, d_K$, all available in every state. Making decision $d_k$ in state $i$ sends the system to state $j$ with probability $q_{ij}(k) \ge 0$, where $\sum_j q_{ij}(k) = 1$, and costs $w_{ik}$.

A procedure of class $C'$ is stationary randomized: in state $i$ it makes decision $d_k$ with probability $D_{ik}$, where $D_{ik} \ge 0$ and $\sum_k D_{ik} = 1$, independently of the past and of the time. Under such a procedure the states form a Markov chain with transition probabilities $p_{ij} = \sum_k q_{ij}(k) D_{ik}$. Write $W_t$ for the expected cost at time $t$ when $X_0 = i$.

• Problem 1 (average cost): minimize $Q_R(i) = \limsup_{T\to\infty} \frac{1}{T}\sum_{t=0}^{T} W_t$. Here $w_{ik} > 0$, and Assumption A says that under every procedure of $C'$ all states belong to one class.
• Problem 2 (total cost): the state $L$ is absorbing under every decision and $w_{Lk} = 0$. Minimize $S_R(i) = \sum_{t=0}^{\infty} W_t$, the expected cost of reaching $L$. Assumption B says that under every procedure of $C'$, $L$ is reached from every state with probability one.

The state-action frequencies of a procedure $D \in C'$ with stationary distribution $\pi$ are $x_{jk} = \pi_j D_{jk}$. They satisfy the linear constraints

$$\text{(10)}\qquad x_{jk} \ge 0,\qquad \sum_k x_{jk} - \sum_{i}\sum_k x_{ik}\, q_{ij}(k) = 0 \ \ (j),\qquad \sum_j\sum_k x_{jk} = 1 .$$

For Problem 2, Derman adjoins a state $-1$ that restarts the chain uniformly on $0, \dots, L$ and is entered from $L$. The expected total cost then becomes a ratio of two linear functions of the frequencies of this augmented chain, (9).

Formalization targets

Goal: Theorem 2, pinned-down reading

The printed statement, "If Assumption A (B) holds, then problem 1 (2) can be formulated as a linear programming problem", is not a mathematical statement as it stands. The goal is the reading established by its proof (pp. 20–23).

Under Assumption A with $w > 0$, the program

$$\min \ \sum_{j,k} x_{jk} w_{jk} \quad \text{subject to (10)}$$

has an optimal solution. For every optimal $x^*$, every row sum $\sum_k x^*_{jk}$ is positive, and $D^*_{jk} = x^*_{jk}/\sum_k x^*_{jk}$ satisfies $Q_{D^*}(i) \le Q_D(i)$ for all $D \in C'$ and all $i$.

Under Assumption B with the Problem 2 costs, the linear program obtained from (9) by the Lemma's transformation, $\min \sum w_{jk} z_{jk}$ subject to (12), has an optimal solution. For every optimal $(z^*, z^*_{n+1})$ one has $z^*_{n+1} > 0$, and the procedure decoded from $x^* = z^*/z^*_{n+1}$ satisfies $S_{D^*}(i) \le S_D(i)$ for all $D \in C'$ and all $i$.

Milestones

In the order the proof uses them: the Cesàro limit and the unique positive stationary distribution of a one-class chain ((3), (5)); the taboo-probability identity (4); the formula (6) for $Q_R$; the cycle formula (7) for the averaged total cost; the remark that minimizing the average of the $S_R(i)$ minimizes each one; the correspondence between $C'$ and the solutions of (10); and the Lemma reducing a linear-fractional program under conditions (i) and (ii) to the linear program (12).

Significance

The theorem replaces a search over infinitely many randomized procedures by a single finite linear program. It also yields the structural fact that an optimal stationary procedure can be read off from any optimal solution. The variables $x_{jk}$ make constraints on long-run frequencies of actions expressible as linear constraints. That is the origin of the theory of constrained Markov decision processes, and of the dual linear programs whose variables are value functions. The Lemma is the classical linear-fractional reduction, used well beyond this setting.

All of these results are proved in the paper and in later textbooks (for example Puterman, Markov Decision Processes, 1994, §8.8 and §9.5). None of them has been formalized: Mathlib has Perron–Frobenius-type facts for irreducible matrices but no linear programming theory, no taboo probabilities and no Markov decision model. The mission produces machine-checked versions of the proof's chain of equalities and of the decoding step, written so that they can be reused for occupation-measure arguments.

Difficulty

Several steps fail in the naive argument. The correspondence between procedures and solutions of (10) needs every row sum $\sum_k x_{jk}$ to be positive. That uses Assumption A for a procedure obtained by completing the decoded rows arbitrarily, together with the uniqueness and positivity of the stationary distribution. Positivity of the stationary vector of an irreducible but possibly periodic chain, and the Cesàro (not ordinary) convergence of $P^t$, have no ready-made form in Mathlib. The total-cost identity (7) needs the regenerative identity (4), whose sums must first be shown to converge, and needs the augmented chain to be irreducible, which follows from Assumption B but is not assumed. Problem 2 needs one more step: a minimizer of the averaged total cost is optimal from every starting state, which uses the finiteness of all $S_R(i)$.

Formalization scope

States and decisions are finite Lean types S and Act. Probabilities and costs are real numbers, a procedure of $C'$ is a nonnegative real matrix with unit row sums, and the chain is chainMatrix q D. Assumption A is irreducibility (Matrix.IsIrreducible) of every such chain matrix. Assumption B is reachability of $L$ from every state; for a finite chain in which $L$ is absorbing, this is equivalent to absorption with probability one. $Q_R(i)$ is a real limsup of a bounded sequence, with the paper's sum over $t = 0, \dots, T$. $S_R(i)$ takes values in $[0, \infty]$. The paper requires $w_{ik} > 0$ on p. 17 and $w_{Lk} = 0$ in Problem 2. The formalization uses $w_{ik} > 0$ for $i \ne L$ in Problem 2, and keeps the two problems as separate implications. The adjoined state $-1$ is none : Option S, with the transition law that produces Derman's $p_{-1,i} = 1/(L+1)$, $p_{L,-1} = 1$ for every procedure. The published JewellMRP.InfiniteStep definitions of an ergodic matrix and of a stationary vector are reused.

The goal states optimality of the decoded procedure against every competitor in $C'$, for every optimal solution of the linear program, with existence of an optimal solution as a separate clause. A statement that only identifies feasible sets, or that only asserts that some optimal procedure exists, does not count as Theorem 2. Optimality over all history-dependent procedures is Theorem 1, a separate mission of this series.

Welcome contributions: the stationary-distribution facts for irreducible finite stochastic matrices (reusable across Markov chain work), a small linear-programming existence lemma (a linear function attains its minimum on a nonempty compact polytope), and the Lemma's transformation, which is self-contained.

Selected references

• C. Derman, On Sequential Decisions and Markov Chains, Management Science 9(1):16–24, 1962. https://doi.org/10.1287/mnsc.9.1.16
• A. S. Manne, Linear Programming and Sequential Decisions, Management Science 6(3):259–267, 1960. https://doi.org/10.1287/mnsc.6.3.259
• A. Charnes and W. W. Cooper, Programming with Linear Fractional Functionals, Naval Research Logistics Quarterly 9(3–4):181–186, 1962. https://doi.org/10.1002/nav.3800090303
• K. L. Chung, Markov Chains with Stationary Transition Probabilities, Springer, 1960. https://doi.org/10.1007/978-3-642-49686-8
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Why airlines allocate seats by fare class

An airline sells the seats of one flight leg at several prices. Low fares fill seats that would otherwise fly empty; high fares are bought by passengers who book late and cannot be predicted exactly. Seat inventory control decides how many seats each fare class may sell. Peter Belobaba's 1987 MIT dissertation (MIT Flight Transportation Laboratory Report R87-7) gave the probabilistic treatment of this problem that became the expected marginal seat revenue (EMSR) method, which was in use across the airline industry for decades.

This mission formalizes the first, simplest model of the thesis: distinct (non-nested) fare-class inventories on a single leg, where a seat assigned to a class may be sold only in that class or not at all. The thesis surveys this model in Sect. 4.2 (pp. 84–94), where an integer-programming formulation from McDonnell-Douglas and its solution by ranking marginal values are described (p. 90), and develops it probabilistically in Sect. 5.1 (pp. 102–107).

Setting

A leg has capacity $n$ seats (the thesis also writes $C$). There are finitely many fare classes $i$. Class $i$ has an average fare $f_i \ge 0$ and receives a random number of requests $r_i \in \{0,1,2,\dots\}$, with law $p_i$. The seats are split into allocations $S_i \in \mathbb{N}$, one per class.

With $S$ seats, a class books requests until its seats run out, so its bookings and spill (refused requests) are

$$b = \min(r, S), \qquad l = (r - S)^+ \qquad \text{(Eq. (5.3))}.$$

The expected revenue of class $i$ is $\bar R_i(S_i) = f_i \cdot \bar b_i(S_i)$ with $\bar b_i(S_i) = E[\min(r_i,S_i)]$, and the leg's expected revenue is $\bar R = \sum_i \bar R_i(S_i)$ (Eq. (5.9)). Write

$$\bar P_i(S) = P[r_i \ge S], \qquad \mathrm{EMSR}_i(S) = f_i \cdot \bar P_i(S) \qquad \text{(Eqs. (5.11), (6.1), (6.2))},$$

the expected marginal seat revenue of the $S$-th seat of class $i$. The value of the $k$-th seat of class $i$ in the integer program of p. 90 is $m_i(k) = \mathrm{EMSR}_i(k)$, $k = 1, \dots, n$.

Formalization targets

Goal: the $n$ largest marginal values give the optimal booking limits (p. 90)

Let $T$ be any set of $n$ pairs $(i,k)$, $1 \le k \le n$, such that every $m_i(k)$ with $(i,k) \in T$ is at least every $m_j(l)$ with $(j,l) \notin T$, and let $S^T_i = \#\{k : (i,k) \in T\}$. Then $\sum_i S^T_i = n$ and

$$\sum_i f_i\, E[\min(r_i, S_i)] \;\le\; \sum_i f_i\, E[\min(r_i, S^T_i)] \qquad \text{for every } S \text{ with } \textstyle\sum_i S_i \le n .$$

The goal fixes no distribution, number of classes or fare ordering, and it holds for every tie-breaking among equal marginal values.

Milestones

1. Eq. (5.6): $\bar b_i(S) + \bar l_i(S) = \bar r_i$ for requests of finite mean.
2. Eq. (5.11): $\bar R_i(S) - \bar R_i(S-1) = f_i \cdot P[r_i \ge S]$ for $S \ge 1$.
3. Eqs. (6.1)–(6.2): $\bar P_i$ and $\mathrm{EMSR}_i$ are non-increasing in $S$.
4. Eq. (4.5): the 0–1 vector equal to $1$ on a set of $n$ largest $m_i(k)$ is an optimal solution of the linear program $\max \sum_{i,k} X_{ik} m_i(k)$ subject to $\sum X_{ik} \le n$, $0 \le X_{ik} \le 1$.
5. Eq. (5.13), discrete form: an allocation of exactly $C$ seats maximises $\bar R$ among such allocations if and only if some $\lambda$ satisfies $\mathrm{EMSR}_i(S_i) \ge \lambda$ whenever $S_i \ge 1$ and $\mathrm{EMSR}_i(S_i + 1) \le \lambda$, for all $i$.

Significance

The goal is the reason distinct-inventory allocation is computationally easy: a revenue-maximising allocation is obtained by sorting $n \times (\text{number of classes})$ numbers, with no search over allocations. The same marginal-value principle underlies the EMSR rules for nested classes in the rest of the thesis, and the identity (5.11) is the link between an expected-revenue function and its marginal seat values used throughout revenue management. Milestone 5 is the integer form of the Lagrangian condition of Eq. (5.13); the thesis states it only for a continuous relaxation, and its equality form is generally unattainable with integer seats.

These results are classical and their proofs are elementary; to our knowledge none of them has been machine-checked. The mission produces a reusable formal model of a single-leg, distinct-inventory allocation problem with integer demand (bookings, spill, revenue and marginal values of a PMF ℕ), and checked statements of the marginal-allocation principle for it.

Difficulty

The thesis argues with continuous densities and derivatives, setting $\partial \bar R / \partial S_i$ equal across classes. That argument does not transfer to integer seats: the derivative of a step-shaped expected-revenue function does not exist, equality of marginal values across classes generally fails at every integer allocation, and the tail probability must be $P[r \ge S]$ rather than the $P[r > S]$ of Eq. (5.2) for the marginal identity to hold. The integer statements need their own exchange argument. A second subtlety is ties: "the $n$ largest values" is not unique, and the goal must hold for every admissible choice, including choices in which a class's selected seat numbers are not an initial segment $\{1, \dots, S_i\}$.

Formalization scope

All declarations live in the namespace SeatInventory.Distinct. Conventions:

• Integer demand. The law of class $i$'s requests is d i : PMF ℕ; expectations are series over $\mathbb{N}$. The thesis's continuous densities are replaced by this discrete model, which the thesis itself requires for seat allocations (p. 103).
• Tail convention. $\bar P(S) = P[r \ge S]$, as in Eq. (6.2) and the prose of Eq. (5.11) ("the probability of selling $S_i$ or more seats"), not the $P[r > S]$ of Eq. (5.2).
• Seat numbers start at 1, and the pairs $(i,k)$ range over $k \in \{1, \dots, n\}$, as the 600 variables of a 150-seat, four-class problem on p. 90 indicate.
• Nonnegative fares $f_i \ge 0$ are assumed in every statement that needs them; with a negative fare the capacity constraint $\sum S_i \le n$ would not bind and the claims fail.
• Finite mean of the requests is assumed explicitly for Eq. (5.6); the thesis assumes it silently. Expected bookings are bounded and need no assumption.
• Capacity. The goal and the LP compare against allocations with $\sum_i S_i \le n$ (the LP's constraint); milestone 5 compares allocations of exactly $C$ seats (Eq. (5.8)).
• No independence assumption. Expected revenue of distinct inventories depends only on each class's marginal law, so the statements take one law per class.
• "Decreasing" is non-increasing. The thesis's justification in Sect. 6.1.1 gives only monotonicity; strict decrease fails for bounded demand.
• LP integrality. "The solution will be integer" is stated as: the indicator of every set of $n$ largest values is optimal. With ties the LP also has fractional optima.

The expected revenue in the goal is computed from the booking rule $\min(r_i, S_i)$; it is not defined as a sum of marginal values, and the optimal allocation is not defined as an argmax of $\bar R$. Either shortcut would make the goal a tautology and is ruled out.

Needed infrastructure: tail sums of a PMF ℕ, telescoping of $E[\min(r, S)]$, and a finite exchange argument for sums of the $n$ largest values of a function on a finite set; the last two are reusable for any separable concave resource-allocation problem. Contributions of proofs of any milestone, and of a verified sorting routine that produces a set of $n$ largest values, are welcome.

Selected references

• P. P. Belobaba, Air Travel Demand and Airline Seat Inventory Management, PhD thesis, MIT Flight Transportation Laboratory Report R87-7, 1987 (no DOI).
• P. P. Belobaba, Airline yield management: an overview of seat inventory control, Transportation Science 21(2), 63–73, 1987. https://doi.org/10.1287/trsc.21.2.63
• P. P. Belobaba, Application of a probabilistic decision model to airline seat inventory control, Operations Research 37(2), 183–197, 1989. https://doi.org/10.1287/opre.37.2.183
• K. Littlewood, Forecasting and control of passenger bookings, AGIFORS Symposium Proceedings 12, 1972; reprinted in Journal of Revenue and Pricing Management 4(2), 111–123, 2005. https://doi.org/10.1057/palgrave.rpm.5170134

Motivation

The simplex method is the standard algorithm for linear programming, and its correctness rests on one question: does it stop? Each pivot of the method moves from one dictionary to another without decreasing the objective value, but a pivot can leave the objective unchanged. When that happens repeatedly, the method can return to a dictionary it has already visited and loop forever. This behaviour, cycling, is not hypothetical: Vanderbei's Chapter 3 exhibits a problem with four decision variables and three constraints on which the "largest coefficient" entering rule with a natural tie-breaking rule cycles through six dictionaries (Vanderbei 2014, pp. 26–27).

The chapter answers the question with two pivoting rules under which the simplex method provably terminates, and then draws the consequence that makes linear programming a finite theory: the fundamental theorem of linear programming. This mission formalizes the chapter's four numbered theorems in Vanderbei's own setting of standard-form problems with slack variables.

Timeline. Hoffman (1953) and Beale (1955) gave the first examples of cycling. The perturbation and lexicographic methods go back to Charnes (1952) and to Dantzig, Orden and Wolfe (1955). Bland (1977) introduced the smallest-index rule and proved that the simplex method terminates under it (Bland 1977).

Setting

A linear program in standard form has $m$ constraints and $n$ decision variables:

$$\text{maximize } \sum_{j=1}^n c_j x_j \quad\text{subject to}\quad \sum_{j=1}^n a_{ij}x_j \le b_i\ (i=1,\dots,m),\qquad x_j \ge 0\ (j=1,\dots,n).$$

A solution $x$ is feasible if it satisfies every constraint, and optimal if in addition it maximizes the objective among feasible solutions. The problem is infeasible if no feasible solution exists, and unbounded if it has feasible solutions with arbitrarily large objective values.

The slack variables $w_i = b_i - \sum_j a_{ij}x_j$ are appended to the list of variables as $x_{n+i} = w_i$, so that the constraints become the linear system $[A\ I]\,x = b$ with $x \ge 0$ in $\mathbb{R}^{n+m}$. A dictionary is given by a set $\mathcal B$ of $m$ basic indices whose columns of $[A\ I]$ are linearly independent; the remaining indices $\mathcal N$ are nonbasic. Solving for the basic variables gives

$$\zeta = \bar\zeta + \sum_{j\in\mathcal N}\bar c_j x_j,\qquad x_i = \bar b_i - \sum_{j\in\mathcal N}\bar a_{ij}x_j\quad (i\in\mathcal B).$$

The basic solution of the dictionary sets the nonbasic variables to zero. The dictionary is feasible if $\bar b_i \ge 0$ for every $i\in\mathcal B$, and degenerate if $\bar b_i = 0$ for some $i\in\mathcal B$.

The simplex method (Phase II) starts at a feasible dictionary and repeats a pivot: an entering variable $x_k$ is chosen among the nonbasic variables with $\bar c_k > 0$, and a leaving variable $x_l$ among the basic variables with $\bar a_{lk} > 0$ that minimize the ratio $\bar b_l/\bar a_{lk}$; then $x_k$ becomes basic and $x_l$ nonbasic. The method stops when no $\bar c_j$ is positive (the dictionary is optimal) or when the entering column has no positive $\bar a_{ik}$ (the problem is unbounded). A pivoting rule resolves the remaining choices. Bland's rule chooses both the entering and the leaving variable as the candidate with the smallest index. The lexicographic rule perturbs the right-hand sides by symbols $0<\epsilon_m\ll\dots\ll\epsilon_1\ll$ all data and chooses the leaving variable by the perturbed ratio test.

Formalization targets

Goal: Theorem 3.3 (termination under Bland's rule, p. 31)

From every feasible dictionary $D_0$, there is no infinite sequence of pivots

$$D_0\to D_1\to D_2\to\cdots$$

in which both the entering and the leaving variable follow Bland's rule; and a finite sequence of such pivots reaches a dictionary $D_T$ at which the method stops, optimal or exhibiting unboundedness.

Milestones

• Theorem 3.1 (p. 27): if the simplex method fails to terminate, it must cycle, i.e. an infinite run visits some dictionary twice.
• Theorem 3.2 (p. 30): the simplex method always terminates when the leaving variable is selected by the lexicographic rule.
• Theorem 3.4 (p. 33), the fundamental theorem: (1) with no optimal solution the problem is infeasible or unbounded; (2) if a feasible solution exists, a basic feasible solution exists; (3) if an optimal solution exists, a basic optimal solution exists.

Significance

The result. Termination under Bland's rule is what turns the simplex method from a heuristic into an algorithm. Combined with Phase I, it yields the fundamental theorem of linear programming, which reduces the search for an optimum to finitely many basic solutions and underlies the duality theory of the following chapters. Bland's rule also needs no perturbation or extra bookkeeping, and it is the anticycling rule used in many correctness proofs of simplex-type and combinatorial pivoting algorithms, including oriented-matroid programming.

Formalizing it. All four theorems are classical and proved. The Prove2Me library has the lexicographic rule and a nondegenerate termination theorem in the tableau setting of Bertsimas and Tsitsiklis (equality form $Ax=b$, $x\ge 0$, full row rank), and the existence of basic feasible and optimal solutions in that form. It has no statement of Bland's theorem, and none of Vanderbei's dictionary formulation over $[A\ I]$. This mission produces a machine-checkable model of dictionaries and pivoting rules in that formulation, and targets Bland's theorem, whose proof is a genuine combinatorial argument rather than a monotonicity argument.

Difficulty

The natural argument for termination is monotonicity: each pivot increases the objective, so no dictionary repeats. It fails exactly at degenerate pivots, where the step length $\bar b_l/\bar a_{lk}$ is zero and the objective and the basic solution do not change. Bland's rule gives no potential function that strictly increases along degenerate pivots, so the proof has to reason about a hypothetical cycle as a whole: which variables enter and leave the basis within it, and how two dictionaries of the cycle, in which the same variable leaves and later enters, constrain each other's coefficients. Relating the coefficients of two different dictionaries of the same problem is the step that has no counterpart in the model's definitions and has to be developed.

For Theorem 3.2, the symbols $\epsilon_i$ cannot be replaced by a fixed small real number: the method treats them as formal quantities on separate scales, and the statement is about that symbolic rule.

Formalization scope

Vectors are Fin n → ℝ, Fin m → ℝ, and the constraint matrix is Matrix (Fin m) (Fin n) ℝ. The $n+m$ variables are indexed by Fin (n + m) with the decision variables first and the slacks after them, which is the order $x_1,\dots,x_n,x_{n+1}=w_1,\dots,x_{n+m}=w_m$ that Bland's rule compares. A dictionary is a structure holding its basic set, a proof that it has $m$ elements and a proof that its columns of $[A\ I]$ are linearly independent; the coefficients $\bar b,\bar a,\bar c,\bar\zeta$ are computed as coordinates in the basis of basic columns. A dictionary is therefore determined by its basic set, as the proof of Theorem 3.1 uses. "Basic solution" is defined through such a dictionary, not as a support condition.

Termination is stated as the nonexistence of an infinite run from a feasible dictionary, for Theorems 3.2 and 3.3. The goal adds that a finite Bland run reaches a stopping dictionary, so that it cannot hold because pivots fail to exist. The lexicographic rule is encoded by lexicographic comparison of the coefficient vectors $(\bar b_i, r_{i1},\dots,r_{im})/\bar a_{ik}$ of the perturbed ratios; the symbol $\epsilon_p$ is attached in the starting dictionary to its $p$-th basic variable in increasing index order, which for the initial dictionary is the $p$-th constraint. Unboundedness in Theorem 3.4 is "for every $M$ a feasible solution with objective $>M$", as defined on p. 7. The statements carry no explicit constants.

A formalization that stated Theorem 3.3 for arbitrary pivot sequences with pairwise distinct bases would be Theorem 3.1's counting argument, not Bland's theorem; the goal is stated for pivots that follow Bland's rule and only those.

A complete development needs: the pivot update of a dictionary and the invariance of the solution set under it, feasibility preservation by the ratio test, the relation between the objective rows of two dictionaries, and finiteness of the set of bases. These are reusable for any later formalization of simplex-type algorithms. Proofs of the milestones, alternative proofs of Theorem 3.3, and Phase I (to connect Theorem 3.4 with the algorithm) are welcome.

Selected references

• R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., International Series in Operations Research & Management Science 196, Springer, 2014, Chapter 3. https://doi.org/10.1007/978-1-4614-7630-6
• R. G. Bland, New finite pivoting rules for the simplex method, Mathematics of Operations Research 2(2):103–107, 1977. https://doi.org/10.1287/moor.2.2.103
• G. B. Dantzig, A. Orden, P. Wolfe, The generalized simplex method for minimizing a linear form under linear inequality restraints, Pacific Journal of Mathematics 5(2):183–195, 1955. https://doi.org/10.2140/pjm.1955.5.183
• E. M. L. Beale, Cycling in the dual simplex algorithm, Naval Research Logistics Quarterly 2(4):269–275, 1955. https://doi.org/10.1002/nav.3800020406
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §3.4 (lexicographic rule and Bland's rule in tableau form).

Motivation

A zero-sum two-person game in normalized form is a real matrix $\mathcal H(\tau_1, \tau_2)$: player 1 chooses a row $\tau_1$, player 2 simultaneously chooses a column $\tau_2$, and player 2 pays player 1 the amount $\mathcal H(\tau_1, \tau_2)$. Matrix games are the base case of non-cooperative game theory, the prototype of every minimax statement in optimization, statistics (Wald's decision theory) and online learning, and, through their equivalence with linear programming, a standard tool of operations research.

Chapter III of von Neumann and Morgenstern's Theory of Games and Economic Behavior (1944; third edition 1953) gives the book's complete solution of these games. Timeline:

• 1928. J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Math. Annalen 100, proves that every matrix game has a value in mixed strategies (the minimax theorem), by a topological argument. https://doi.org/10.1007/BF01448847
• 1937. von Neumann's growth-model paper gives a second proof via a fixed-point argument, later generalized by Kakutani (1941).
• 1938. J. Ville gives the first elementary proof, based on convexity.
• 1944. The Theory of Games presents Ville's route: a theorem of the alternative for matrices (§16) yields the minimax theorem (17:6), from which §17 derives the structure of the sets of good strategies.
• 1951. Gale, Kuhn and Tucker, and Dantzig, relate matrix games to linear-programming duality.

Setting

Player 1 has $\beta_1 \ge 1$ pure strategies $\tau_1$, player 2 has $\beta_2 \ge 1$ pure strategies $\tau_2$, and $\mathcal H$ is an arbitrary real $\beta_1 \times \beta_2$ matrix (14.1.1). A mixed strategy of player 1 is a probability vector $\xi$ in the simplex

$$S_{\beta_1} = \Big\{ \xi \in \mathbb R^{\beta_1} : \xi_{\tau_1} \ge 0,\ \sum_{\tau_1} \xi_{\tau_1} = 1 \Big\},$$

and similarly $\eta \in S_{\beta_2}$ for player 2. The pure strategy $\tau$ is the coordinate vector $\delta^{\tau}$. The expected payoff is the bilinear form (17:2)

$$K(\xi, \eta) = \sum_{\tau_1=1}^{\beta_1} \sum_{\tau_2=1}^{\beta_2} \mathcal H(\tau_1, \tau_2)\, \xi_{\tau_1} \eta_{\tau_2}.$$

The good strategies of player 1 form the set $\bar A$ of those $\xi \in S_{\beta_1}$ at which $\operatorname{Min}_\eta K(\xi, \eta)$ assumes its maximum; those of player 2 form the set $\bar B$ of those $\eta \in S_{\beta_2}$ at which $\operatorname{Max}_\xi K(\xi, \eta)$ assumes its minimum ((17:B:a), (17:B:b)). A saddle point of $K$ is a pair with $K(\xi', \eta) \le K(\xi, \eta) \le K(\xi, \eta')$ for all $\xi', \eta'$. With pure strategies alone one has $v_1 = \operatorname{Max}_{\tau_1}\operatorname{Min}_{\tau_2}\mathcal H$ and $v_2 = \operatorname{Min}_{\tau_2}\operatorname{Max}_{\tau_1}\mathcal H$; the game is specially strictly determined when $v_1 = v_2$.

For a general real function $\phi(x, y)$ (§13) the same notions are $\operatorname{Max}_x \operatorname{Min}_y \phi$, $\operatorname{Min}_y \operatorname{Max}_x \phi$, saddle points, and the sets $A^\phi$ (maximizers of $\operatorname{Min}_y \phi$) and $B^\phi$ (minimizers of $\operatorname{Max}_x \phi$), always under the book's standing hypothesis that these maxima and minima exist.

Formalization targets

Goal: (17:D), good strategies characterized by their supports

For all $\xi \in S_{\beta_1}$ and $\eta \in S_{\beta_2}$: $\xi \in \bar A$ and $\eta \in \bar B$ if and only if

$$\xi_{\tau_1} = 0 \text{ whenever } \sum_{\tau_2} \mathcal H(\tau_1, \tau_2)\eta_{\tau_2} < \max_{\tau_1'} \sum_{\tau_2} \mathcal H(\tau_1', \tau_2)\eta_{\tau_2},$$ $$\eta_{\tau_2} = 0 \text{ whenever } \sum_{\tau_1} \mathcal H(\tau_1, \tau_2)\xi_{\tau_1} > \min_{\tau_2'} \sum_{\tau_1} \mathcal H(\tau_1, \tau_2')\xi_{\tau_1}.$$

The statement fixes no value and no constant; it says which pairs of mixed strategies are optimal.

Milestones, in attack order

1. (13:A*) $\operatorname{Max}_x \operatorname{Min}_y \phi \le \operatorname{Min}_y \operatorname{Max}_x \phi$.
2. (13:D*) If $\operatorname{Max}\operatorname{Min} = \operatorname{Min}\operatorname{Max}$, the saddle points of $\phi$ are exactly $A^\phi \times B^\phi$.
3. (17:A) $\operatorname{Min}_\eta K(\xi, \eta) = \operatorname{Min}_{\tau_2} \sum_{\tau_1} \mathcal H(\tau_1, \tau_2)\xi_{\tau_1}$, and dually for $\operatorname{Max}_\xi$.
4. (16:C) For every matrix $a(i, j)$ exactly one of: some $x \in S_m$ with $\sum_j a(i,j)x_j \le 0$ for all $i$; some $w \in S_n$ with $\sum_i a(i,j)w_i > 0$ for all $j$.
5. (16:F) The weak form with $\ge 0$ in place of $> 0$.
6. (17:6) The minimax theorem: a saddle point of $K$ exists (already on the platform as AGT.zero_sum_minimax, proved).
7. (17:C:f) $\xi \in \bar A$ and $\eta \in \bar B$ iff $\xi, \eta$ is a saddle point of $K$.

After the goal: (17:E) the game is specially strictly determined iff each player has a pure good strategy.

Significance

(17:D) is the complementary-slackness description of the optimal strategy pairs of a matrix game: a good strategy puts weight only on pure strategies that are best replies to the opponent's good strategy, and conversely any pair of mutually supported best replies is optimal. It is the basis of support-enumeration methods for matrix games, of the equalizing arguments used to solve small games by hand (the book's Chapter IV applies it to Matching Pennies, Stone–Paper–Scissors and Poker), and of the rectangular structure $\bar A \times \bar B$ of the set of optimal pairs. (17:E) connects the mixed-strategy solution to the pure-strategy theory of §14 and to the perfect-information games of §15.

The results are classical and proved in the book. The minimax theorem itself is already machine-checked on the platform (AGT.zero_sum_minimax), and Mathlib contains Sion's minimax theorem and the basic saddle-point lemmas for extended-real functions on sets. This mission adds the book's own chain: the §13 saddle-point calculus under its standing attainment hypothesis, the theorems of the alternative (16:C) and (16:F) in the simplex-normalized form the book uses, the reduction (17:A) to pure strategies, and the characterizations (17:C:f), (17:D), (17:E) of good strategies, which are not on the platform in any form.

Difficulty

The "if" direction of (17:D) cannot be proved from the support conditions alone by local reasoning: that a pair of mutual best replies consists of good strategies uses that the value $\operatorname{Max}_\xi \operatorname{Min}_\eta K$ equals $\operatorname{Min}_\eta \operatorname{Max}_\xi K$, i.e. the minimax theorem. Without that equality the "if" direction of (13:D*) fails (points of $A^\phi \times B^\phi$ exist but are not saddle points), so the calculus of §13 alone does not suffice. Likewise (16:C) is not a direct instance of the Farkas lemma forms on the platform: its alternatives are normalized to the simplex and the second one is strict, and both the existence and the mutual exclusion must be shown.

Formalization scope

Lean conventions, fixed throughout:

• Pure strategies are Fin β₁, Fin β₂ (numbered from $0$), the matrix is H : Fin β₁ → Fin β₂ → ℝ, and $S_\beta$ is Mathlib's stdSimplex ℝ (Fin β).
• Nonempty strategy sets ($\beta \ge 1$, from "τ = 1, …, β" in 14.1.1): every theorem assumes 0 < β₁, 0 < β₂, or mixed strategies $\xi \in S_{\beta_1}$, $\eta \in S_{\beta_2}$, which force it. The theorems of the alternative assume $n, m \ge 1$ (a matrix with rows and columns).
• Standing hypothesis of 13.2.1 ("we are restricting our considerations to such functions, for which Max and Min exist"): the §13 results (13:A*), (13:D*) are stated for an arbitrary $\phi : X \times Y \to \mathbb R$ under the predicate MaxMinAttained φ, which says that $\operatorname{Min}_y \phi(x, y)$, $\operatorname{Max}_x \phi(x, y)$, $\operatorname{Max}_x \operatorname{Min}_y \phi$ and $\operatorname{Min}_y \operatorname{Max}_x \phi$ are attained. (13:D*) also carries the hypothesis of 13.5.2 that saddle points exist, stated as $\operatorname{Max}_x \operatorname{Min}_y \phi = \operatorname{Min}_y \operatorname{Max}_x \phi$.
• $\operatorname{Max}$ and $\operatorname{Min}$ are the real ⨆, ⨅; they are the book's attained values under the hypotheses above (compactness of the simplex and continuity of $K$ for the mixed game). (17:A) asserts attainment explicitly (IsLeast, IsGreatest). "Does not assume its maximum at $\tau_1$" in the goal is written without any Max operator.
• $\bar A$, $\bar B$ are defined as maximizers and minimizers directly from $K$, not through an assumed value $v'$.

A trivializing formalization is ruled out: $\bar A$ and $\bar B$ are not taken as hypotheses or defined through the support conditions, strategy sets cannot be empty, and no Max over an empty or unbounded set occurs.

Contributions welcome: proofs of the milestones, especially (16:C) (from Mathlib's convex separation or from a platform Farkas lemma) and the bridge from AGT.zero_sum_minimax to (17:C:f). The §13 lemmas and the (17:A) reduction are reusable by any mission about matrix games or bilinear saddle points.

Selected references

• J. von Neumann and O. Morgenstern, Theory of Games and Economic Behavior, 60th-anniversary edition, Princeton University Press, 2007 (reprint of the 3rd edition, 1953), §§13, 16, 17. https://doi.org/10.1515/9781400829460
• J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen 100 (1928), 295–320. https://doi.org/10.1007/BF01448847
• J. Ville, "Sur la théorie générale des jeux où intervient l'habileté des joueurs", in É. Borel, Traité du calcul des probabilités et de ses applications, IV.2, Gauthier-Villars, 1938, 105–113.
• S. Kakutani, "A generalization of Brouwer's fixed point theorem", Duke Mathematical Journal 8 (1941), 457–459. https://doi.org/10.1215/S0012-7094-41-00838-4
• D. Gale, H. W. Kuhn and A. W. Tucker, "Linear programming and the theory of games", in Activity Analysis of Production and Allocation, Wiley, 1951, 317–329.