Linear Optimization

Operations Research Optimization Theoretical Computer Science·Captain: ORdos

Smale's Ninth Problem: Strongly Polynomial Linear ProgrammingOpen Problem

The problem of solving linear inequalities

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

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

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

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

Why it matters

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

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

The question and what is known

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

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

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

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

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

A hierarchy of formalization targets

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

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

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

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

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

2^n - 1 \text{ pivots}

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

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

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

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

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

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

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

Formalization scope

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

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

Selected references

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

29 thms6 active usersReviewed

Completed

Discrete Geometry Operations Research Optimization·Captain: mikedeng1

Selected Topics in Column Generation I: Discretization — Every Integer Point of a Rational Polyhedron Is a Generating Integer Point Plus an Integer Combination of Integer RaysResearch Paper

Motivation

Dantzig–Wolfe decomposition and column generation solve large integer programs by replacing a set of "easy" constraints with a description of its feasible points, and then pricing out the points one at a time. For linear programs this rests on the Minkowski–Weyl representation: every point of a polyhedron is a convex combination of its extreme points plus a nonnegative combination of its extreme rays. For integer programs that representation is not enough. Imposing integrality on the convex multipliers of the extreme points of $\mathrm{conv}(X)$ does not give back the integer program, because an optimal integer point may lie in the interior of $\mathrm{conv}(X)$ .

Lübbecke and Desrosiers, in their survey Selected Topics in Column Generation (Operations Research 53(6), 2005), present discretization (Johnson 1989, Vanderbeck 2000) as the true integer analogue of the decomposition principle. Its basis is their Theorem 1: the integer points of a rational polyhedron are generated by finitely many integer points and finitely many integer rays with integer multipliers. The paper states this result and refers its proof to Nemhauser and Wolsey, Integer and Combinatorial Optimization (1988). It underlies the integer master problem (25) of branch-and-price.

Setting

Let $D$ be an $m \times n$ matrix and $\mathbf d$ an $m$ -vector with rational entries. The polyhedron is

P = \{\mathbf x \in \mathbb R^n \mid D\mathbf x \geqslant \mathbf d,\ \mathbf x \geqslant \mathbf 0\},

and its set of integer points is $X = P \cap \mathbb Z^n$ , the points of $P$ whose coordinates are all integers. Because $P \subseteq \mathbb R^n_+$ , $X = P \cap \mathbb Z^n_+$ .

The recession cone of $P$ is $\{\mathbf r \in \mathbb R^n \mid D\mathbf r \geqslant \mathbf 0,\ \mathbf r \geqslant \mathbf 0\}$ . An integer ray of $P$ is a nonzero vector of $\mathbb Z^n$ in this cone. Extreme rays are not required.

In Lean these are polyhedronP D d, integerPoints D d, recessionConeP D and IsIntegerRay D w in the namespace Lubbecke2005.Discretization, with integer vectors cast to real vectors by castVec.

Formalization targets

Goal: Theorem 1 (pp. 1011–1012)

If $P \neq \emptyset$ , there exist a finite set of integer points $\{\mathbf p_q\}_{q \in Q} \subseteq X$ and a finite set of integer rays $\{\mathbf p_r\}_{r \in R}$ of $P$ such that

X = \Bigl\{\mathbf x \in \mathbb R^n_+ \ \Big|\ \mathbf x = \sum_{q \in Q} \mathbf p_q \lambda_q + \sum_{r \in R} \mathbf p_r \lambda_r,\ \sum_{q \in Q} \lambda_q = 1,\ \boldsymbol\lambda \in \mathbb Z_+^{|Q|+|R|}\Bigr\}. \qquad (24)

Since the multipliers are nonnegative integers summing to one over $Q$ , (24) says that $X$ is the union, over $q \in Q$ , of the translates $\mathbf p_q + \mathbb Z_+\{\mathbf p_r\}_{r\in R}$ of the monoid generated by the rays. No bound on $|Q|$ or $|R|$ is part of the goal.

Milestone: Remark in §3.3 (p. 1012)

If $X \subseteq [0,1]^n$ , every point of $X$ is a vertex of $\mathrm{conv}(X)$ . In this case convexification and discretization coincide.

Significance

The result. Theorem 1 converts an integer program $\min\{c(\mathbf x) \mid A\mathbf x \geqslant \mathbf b,\ \mathbf x \in X\}$ into the integer master program (25) over the multipliers $\boldsymbol\lambda$ , with one column per generating point and per generating ray. When $X$ is bounded the rays disappear, exactly one $\lambda_q$ equals one, and (25) is a linear integer program even for a nonlinear cost $c$ . The representation is what makes branching on master variables, and the passage between compact and extensive formulations, well defined in branch-and-price.

Formalizing it. The result is classical (Nemhauser–Wolsey 1988, going back to Giles and Pulleyblank and to Meyer's theorem that the integer hull of a rational polyhedron is a polyhedron). On Prove2Me, the real representation (8) is formalized as LinearOptimization.polyhedron_resolution (Bertsimas–Tsitsiklis Thm 4.15) and the integer hull theorem as LinearOptimization.integer_hull_is_polyhedron (Thm 11.3); both are included as reference items. The convexification counterpart of §3.2, that the Lagrangian dual equals the LP over $\mathrm{conv}(X)$ , is LinearOptimization.lagrangean_dual_eq_lp_over_hull. No machine-checked statement of the integer representation (24), with integer multipliers and integer rays, was found on the platform. The mission produces that statement and, once solved, its proof.

Difficulty

The obvious attempt applies the real representation (8) and rounds. It fails twice. First, the extreme points of $P$ need not be integral, and an integer point written as a real combination of vertices and rays has no reason to have integer multipliers. Second, the extreme rays of $P$ generate the recession cone over $\mathbb R_+$ , but the integer points of that cone are not in general nonnegative integer combinations of the (scaled) extreme rays; a generating set of the lattice points of a cone must usually contain non-extreme vectors. The finiteness of $Q$ is also not automatic: $X$ itself is typically infinite, and taking $Q = X$ trivializes the statement.

Rationality of the data is essential. For $P = \{\mathbf x \in \mathbb R^2_+ \mid \sqrt2\,x_1 - x_2 \geqslant 0\}$ , every integer ray has slope below $\sqrt 2$ , so finitely many base points and rays generate only points with $x_2 \leqslant \rho x_1 + C$ for some $\rho < \sqrt 2$ , while $X$ contains $(k, \lfloor\sqrt2 k\rfloor)$ for every $k$ .

Formalization scope

Vectors are Fin n → ℝ; integer vectors are Fin n → ℤ cast coordinatewise. Both sides of (24) are sets of real vectors.
$D$ and $\mathbf d$ are ℚ-valued and cast to ℝ. This is an addition: the paper names no field, and the theorem is false for irrational data (see Difficulty). The cited source, Nemhauser–Wolsey, works with rational data.
The hypothesis $P \neq \emptyset$ is kept as on the page. $X$ may still be empty (e.g. $P = \{1/2\}$ ); then $Q = \emptyset$ and both sides of (24) are empty. The statement allows this.
$Q$ and $R$ are Fin k and Fin l for existentially chosen $k, l \in \mathbb N$ ; the finiteness is the content of the theorem. The multiplier vector $\boldsymbol\lambda \in \mathbb Z_+^{|Q|+|R|}$ is written as a pair of ℕ-valued vectors.
"Integer rays of $P$ " is read as nonzero integer vectors in the recession cone $\{D\mathbf r \geqslant \mathbf 0, \mathbf r \geqslant \mathbf 0\}$ ; extremality is not required, as the page does not require it (contrast (8), which says "extreme rays").
The constraint $\mathbf x \in \mathbb R^n_+$ on the right side of (24) is kept although it is implied.
In the Remark, "vertices of $\mathrm{conv}(X)$ " is read as extreme points of the convex hull; $X$ is finite there, so the two notions agree.

A formalization with real multipliers would be the resolution theorem (8), already on the platform, and one with $Q$ or $R$ infinite would be trivial; both are excluded by the statement.

Useful infrastructure: lattice points of rational polyhedral cones (Hilbert bases, Gordan's lemma), the integer hull theorem, and the real resolution theorem. A proof of Gordan's lemma for rational cones in this vocabulary would be reusable well beyond this mission. Contributions toward any of these are welcome.

Selected references

M. E. Lübbecke and J. Desrosiers, Selected Topics in Column Generation, Operations Research 53(6):1007–1023, 2005. https://doi.org/10.1287/opre.1050.0234
G. L. Nemhauser and L. A. Wolsey, Integer and Combinatorial Optimization, Wiley, 1988. https://doi.org/10.1002/9781118627372
R. R. Meyer, On the existence of optimal solutions to integer and mixed-integer programming problems, Mathematical Programming 7:223–235, 1974. https://doi.org/10.1007/BF01585518
F. Vanderbeck, On Dantzig–Wolfe decomposition in integer programming and ways to perform branching in a branch-and-price algorithm, Operations Research 48(1):111–128, 2000. https://doi.org/10.1287/opre.48.1.111.12453
A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986.

5 thms5 active usersReviewed

Completed

Number Theory Operations Research Optimization·Captain: mikedeng1

An Application of Simultaneous Diophantine Approximation in Combinatorial Optimization: A Small Integral Objective with the Same Optimal Solutions and Dual BasesResearch Paper

Motivation

An algorithm for linear programming is strongly polynomial if the number of arithmetic operations it performs is bounded by a polynomial in the dimension of the problem alone (the number of variables and constraints), independently of the bit lengths of the numbers in the input. Many combinatorial optimization problems are linear programs over polyhedra of the form $P = \{x \in \mathbb{R}^n : Ax \le b\}$ whose constraint matrix $A$ has entries $0, +1, -1$ , but whose objective vector $w$ is an arbitrary rational weight vector. Polynomial-time algorithms for such problems (for instance the ellipsoid-based algorithms of Grötschel, Lovász and Schrijver for maximum-weight cliques in perfect graphs, submodular flows, and matroid polyhedra) have running times that depend on the length of $w$ .

Frank and Tardos (Combinatorica 1987) remove this dependence once and for all: they replace $w$ by an integral objective $\tilde w$ whose entries have $O(n^3)$ bits and which has exactly the same optimal solutions and the same optimal dual bases as $w$ over every such polyhedron. Any algorithm that is polynomial in $n$ and in the length of the objective then becomes strongly polynomial. The tool is simultaneous Diophantine approximation, used through the lattice-basis-reduction algorithm of Lenstra, Lenstra and Lovász (Math. Ann. 1982). The technique extends Tardos's strongly polynomial algorithm for linear programs with small constraint matrices (Oper. Res. 1986), which applies only to explicitly given programs.

Setting

For $x \in \mathbb{R}^n$ write $\|x\|_\infty = \max_j |x(j)|$ and $\|x\|_1 = \sum_j |x(j)|$ ; $\operatorname{sign}$ takes the values $-1, 0, +1$ .

Decomposition. Fix a positive integer $N$ . A decomposition of $w \in \mathbb{R}^n$ is an expression

w = \sum_{i=1}^k \lambda_i v_i, \qquad \lambda_i > 0,\ v_i \in \mathbb{Z}^n.

It satisfies condition (iii) if for $i = 2, \dots, k$ the vector $v_i$ is nonzero and $\lambda_i/\lambda_{i-1} \le 1/(N\|v_i\|_\infty)$ : the coefficients decrease so quickly that each term is negligible against the previous one.

Preprocessing. Given a rational $w$ and $N$ , the paper's preprocessing algorithm finds a decomposition with $k \le n$ , condition (iii), and the size bound (ii)' $\|v_i\|_\infty \le 2^{n^2+n}N^n$ , and outputs

\tilde w = \sum_{i=1}^k M^{k-i} v_i, \qquad M = 2^{n^2+n} N^{n+1}.

Linear programs. Let $A$ be an $m \times n$ matrix with entries in $\{0, \pm 1\}$ and $b \in \mathbb{R}^m$ . The primal program is $\max\{wx : Ax \le b\}$ and the dual program is $\min\{yb : yA = w,\ y \ge 0\}$ . A point $\bar x \in P$ is $w$ -maximal if $w\bar x = \max(wx : x \in P)$ . A dual basis is a maximal set of row indices of $A$ whose rows are linearly independent; it determines at most one $y$ with $yA = w$ supported on it (the basic dual solution), and it is an optimal dual basis if that $y$ exists and is optimal for the dual program.

Formalization targets

Goal — Theorem 4.2 (p. 58)

For every $w \in \mathbb{Q}^n$ , with $N = (n+1)! + 1$ , there is $\tilde w \in \mathbb{Z}^n$ with

\|\tilde w\|_\infty \le 2^{4n^3} N^{n(n+2)}

such that for every $0, \pm1$ matrix $A$ with $n$ columns and every $b$ : (i) $x \in P$ is $w$ -maximal if and only if it is $\tilde w$ -maximal; (ii) a set of rows of $A$ is an optimal dual basis for $w$ if and only if it is one for $\tilde w$ . The vector $\tilde w$ depends on $w$ only, not on $A$ or $b$ .

Milestones

Dirichlet's theorem (p. 52): for $N \ge 1$ and $\alpha \in \mathbb{R}^n$ there are $p \in \mathbb{Z}^n$ and $1 \le q \le N^n$ with $|q\alpha(i) - p(i)| < 1/N$ for all $i$ .
Theorem 3.1 (p. 53): every $w \in \mathbb{R}^n$ has a decomposition with $k \le n$ , $\|v_i\|_\infty \le N^n$ and condition (iii).
Lemma 3.2 (pp. 54–55): under condition (iii), for integral $b$ with $\|b\|_1 \le N - 1$ , $\operatorname{sign}(b \cdot w) = \operatorname{sign}(b \cdot v_j)$ for the smallest $j$ with $b \cdot v_j \ne 0$ , and $b \cdot w = 0$ if there is no such $j$ .
Theorem 3.3 (p. 56): the preprocessed $\tilde w$ satisfies $\|\tilde w\|_\infty \le 2^{4n^3}N^{n(n+2)}$ and $\operatorname{sign}(w \cdot b) = \operatorname{sign}(\tilde w \cdot b)$ for all integral $b$ with $\|b\|_1 \le N-1$ .
The case $N = n+1$ (p. 55): an integral $\tilde w$ with $\|\tilde w\|_\infty \le 2^{4n^3}(n+1)^{n(n+2)}$ and $\tilde w(X) \le \tilde w(Y) \iff w(X) \le w(Y)$ for all subsets $X, Y$ of coordinates.
Lemma 4.1 (i) (p. 57): if $\operatorname{sign}(w' \cdot h) = \operatorname{sign}(w'' \cdot h)$ for all integral $h$ with $\|h\|_1 \le (n+1)!$ , then $w'$ and $w''$ have the same maximizers over $\{Ax \le b\}$ for every $0, \pm1$ matrix $A$ .
Lemma 4.1 (ii) (p. 57): under the same hypothesis, a dual basis is optimal for $w'$ if and only if it is optimal for $w''$ .

Significance

The result gives a general reduction: whenever a class of polyhedra with $0, \pm1$ constraint matrices admits an optimization algorithm that is polynomial in $n$ and in the length of the objective, it admits a strongly polynomial one. The paper applies this to maximum-weight cliques in perfect graphs, optimization over submodular flow polyhedra, and matroid polyhedra membership, and its Section 5 applies the same rounding to the integer programming algorithms of Lenstra and Kannan. The subset-sum corollary (milestone 5) is independently useful: every rational weight function on a finite set can be replaced by an integral one with $O(n^3)$ -bit entries that orders all subset sums identically.

All statements of this mission have been proved on paper since 1987. None is formalized on Prove2Me, and Mathlib contains only the one-dimensional Dirichlet approximation theorem. The mission produces a machine-checked version of the exact statements, with the explicit constants of the paper; the complexity claims (operation counts, strong polynomiality) are not part of it.

Difficulty

The goal combines two independent parts. The number-theoretic part (milestones 1–5) needs a multidimensional Dirichlet theorem, an induction producing the decomposition, and exact inequality chains with the constants $2^{n^2+n}N^n$ and $2^{4n^3}N^{n(n+2)}$ . The linear-programming part (milestones 6–7) needs bounds on the entries of inverses of nonsingular $0, \pm1$ submatrices, the existence of optimal dual solutions supported on a dual basis, LP duality and complementary slackness. The obvious first idea, scaling $w$ to an integer vector by a common denominator, preserves every sign but gives no bound on $\|\tilde w\|_\infty$ in terms of $n$ ; the bound is the content of the theorem. Likewise, rounding each coordinate of $w$ separately to a fixed precision does not preserve the sign of $w \cdot b$ when $w \cdot b$ is tiny but nonzero.

Formalization scope

Vectors are functions on Fin n: the input $w$ is rational (Fin n → ℚ) in the goal, in Theorem 3.3 and in the subset-sum corollary, as in the algorithm's input line; it is real in Theorem 3.1, Lemma 3.2 and Lemma 4.1, as on the page. Integral vectors are Fin n → ℤ, and $A$ is a Matrix (Fin m) (Fin n) ℤ with every entry in $\{-1, 0, 1\}$ , cast to $\mathbb{R}$ ; $b \in \mathbb{R}^m$ is unrestricted. Decompositions are indexed by $i \in \{1, \dots, k\} \subseteq \mathbb{N}$ as in the paper. $\|b\|_1$ is always the explicit sum $\sum_j |b(j)|$ , compared with $N - 1$ in $\mathbb{Z}$ ; $\|v\|_\infty$ of an integer vector is a natural number (supNorm). Sign equality uses SignType.sign and includes the zero case. Condition (iii) is stated multiplicatively together with $v_i \ne 0$ , which the paper's quotient presupposes; without $v_i \ne 0$ Lemma 3.2 fails. An optimal dual basis is a maximal linearly independent set of row indices together with an optimal dual solution supported on it.

Two formalizations would make the goal trivial and are excluded: dropping the bound on $\|\tilde w\|_\infty$ (a multiple of $w$ then works), and letting $\tilde w$ depend on $A$ and $b$ (the goal states $\exists \tilde w$ before $\forall A, b$ ). The $0, \pm1$ assumption on $A$ is part of every Section 4 statement.

A complete development needs a multidimensional pigeonhole argument, determinant and adjugate bounds for $0, \pm 1$ matrices, and basic LP duality (strong duality, complementary slackness, basic optimal dual solutions); the last two are reusable across linear-programming missions. Proofs of individual milestones, reusable lemmas on LP duality, and alternative proofs of Dirichlet's theorem are all welcome.

Selected references

A. Frank and É. Tardos, An application of simultaneous diophantine approximation in combinatorial optimization, Combinatorica 7(1) (1987) 49–65. https://doi.org/10.1007/BF02579200
A. K. Lenstra, H. W. Lenstra Jr. and L. Lovász, Factoring polynomials with rational coefficients, Math. Ann. 261 (1982) 515–534. https://doi.org/10.1007/BF01457454
É. Tardos, A strongly polynomial algorithm to solve combinatorial linear programs, Operations Research 34(2) (1986) 250–256. https://doi.org/10.1287/opre.34.2.250
M. Grötschel, L. Lovász and A. Schrijver, The ellipsoid method and its consequences in combinatorial optimization, Combinatorica 1 (1981) 169–197. https://doi.org/10.1007/BF02579273
J. W. S. Cassels, An Introduction to the Theory of Numbers (title as printed in the paper's reference [2]), Springer, Berlin, 1971; cited in the paper as [2, Sect. 1.10] for Dirichlet's theorem.

11 thms5 active usersReviewed

Completed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems 3: Capacity Scaling for the Hitchcock ProblemResearch Paper

Motivation

The Hitchcock transportation problem asks how to ship a commodity from $m$ supply points to $n$ demand points at minimum total cost. It was posed by Hitchcock in 1941 and is one of the founding problems of linear programming and network optimization; it is solved routinely in logistics, and its structure (a bipartite network with supplies, demands and per-unit costs) recurs in assignment, optimal transport and matching.

The classical algorithms for it, the Ford–Fulkerson primal–dual method among them, augment flow one path at a time. With integral data their number of augmentations is bounded only by the total supply $\sum_i a_i$ , which is exponential in the number of binary digits used to write the data. Edmonds and Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems (J. ACM 19(2), 1972, doi:10.1145/321694.321699), introduced capacity scaling: solve a coarse version of the problem first, then refine one binary digit at a time. Their Theorem 9 (p. 260) bounds the total number of augmentations by a quantity proportional to $\max(m,n)$ times the number of bits of the data, which made the transportation problem, and through standard reductions the minimum-cost flow problem, one of the first network problems with a polynomial-time ("good") algorithm in the sense of Edmonds.

Timeline. Hitchcock (1941) posed the problem; Ford and Fulkerson (1956–1962) gave the primal–dual labeling method and the optimality conditions by node potentials; Edmonds and Karp (1972) gave the scaling method and the bound formalized here. Strongly polynomial algorithms, independent of the size of the numbers, came later (Tardos 1985; Orlin 1988).

Setting

The network of Figure 1 (p. 259) has a source $s$ , a sink $t$ , supply nodes $s_1,\dots,s_m$ and demand nodes $t_1,\dots,t_n$ , with $m,n\ge 1$ . Its arcs are $(s,s_i)$ with capacity $a_i$ and cost $0$ ; $(s_i,t_j)$ with capacity $+\infty$ and cost $d_{ij}\ge 0$ ; $(t_j,t)$ with capacity $b_j$ and cost $0$ ; and the return arc $(t,s)$ with capacity $+\infty$ and cost $0$ . The supplies $a_i$ and demands $b_j$ are positive integers with $\sum_i a_i=\sum_j b_j=:B$ .

A flow assigns a nonnegative number to every arc, at most the capacity, with inflow equal to outflow at every node. Write $f_{0i}=f(s,s_i)$ , $f_{ij}=f(s_i,t_j)$ , $f_{j0}=f(t_j,t)$ ; the value of $f$ is $f(t,s)$ , and a maximum flow is one of largest value. Its cost is $\sum_{i,j} d_{ij} f_{ij}$ ; a flow is extreme if no flow of the same value is cheaper. A flow is pseudo-extreme if there are real $u_i, v_j$ with $u_i-v_j+d_{ij}\ge 0$ for all $i,j$ and $f_{ij}=0$ whenever $u_i-v_j+d_{ij}>0$ .

An augmenting path relative to $f$ is a sequence of distinct nodes from $s$ to $t$ in which each step either follows an arc with spare capacity or traverses backwards an arc carrying positive flow; augmenting pushes the minimum spare amount $\varepsilon$ along it and raises $f(t,s)$ by $\varepsilon$ .

For $p\ge 0$ , Problem $p$ has the same network and costs, with capacities $\lfloor a_i/2^p\rfloor$ and $\lfloor b_j/2^p\rfloor$ . Choose $l$ with every $a_i,b_j<2^l$ . The scaling method solves Problems $l-1,l-2,\dots,0$ in turn. Each phase performs augmentations keeping every flow pseudo-extreme, until no augmenting path is left. Problem $l-1$ starts from the zero flow, and Problem $p-1$ starts from twice the final flow of Problem $p$ .

Formalization targets

Goal: Theorem 9

For every run of the scaling method, the total number $\sum_{p<l} K_p$ of flow augmentations satisfies

\sum_{p=0}^{l-1} K_p \;\le\; \max(m,n)\left(2+\left\lfloor \log_2\frac{\sum_{i=1}^m a_i}{\max(m,n)}\right\rfloor\right).

The bound holds for every $l$ admissible for the data and every choice of costs, and is stated with the paper's constant exactly.

Milestones

§1.1: augmentation preserves feasibility and raises the value by $\varepsilon>0$ ; a flow is maximum iff no augmenting path exists.
Theorem 8: a maximum flow is extreme iff there are potentials $u_0,\dots,u_m$ , $v_0,\dots,v_n$ with (5a)–(5f).
§2.2: a pseudo-extreme maximum flow is extreme.
Lemma 3: if $f$ is pseudo-extreme in Problem $p$ , then $2f$ is pseudo-extreme in Problem $p-1$ .
The maximum-flow value of Problem $p$ is $f_p^*=\min\big(\sum_i\lfloor a_i/2^p\rfloor,\sum_j\lfloor b_j/2^p\rfloor\big)$ .
Eq. (6): $\sum_p K_p\le f_0^*-\sum_{p=1}^{l-1} f_p^*$ .
$f_p^*\ge\max\big(0,\,B/2^p-\max(m,n)\big)$ .

Significance

The result. Theorem 9 shows that scaling reduces the number of augmentations from order $B$ to order $\max(m,n)\log_2(B/\max(m,n))$ , which is roughly the length of the binary encoding of the data. Combined with the $O(mn)$ cost of one augmentation it gives a polynomial-time algorithm for the transportation problem; through the reduction of minimum-cost flow to transportation (p. 261) it gives one for minimum-cost flow. Capacity and cost scaling became standard techniques in network optimization and in combinatorial optimization generally. Theorem 8 and the pseudo-extreme criterion are the optimality certificates for transportation, a special case of linear-programming complementary slackness.

Formalizing it. The theorem has been proved since 1972. This mission produces a machine-checked version of the bound, of the exact counting argument (eq. (6)) and of the arithmetic estimate that turns it into the stated constant, together with the potential-based optimality conditions for the transportation network. To our knowledge no machine-checked bound on the number of augmentations of a flow algorithm exists on the platform.

Difficulty

The obvious argument bounds the number of augmentations by the increase in flow value, since each augmentation raises the value by a positive integer. Applied to Problem 0 directly this gives only $B$ . The scaling bound needs three things that the naive count does not supply. First, doubling the final flow of Problem $p$ must give a feasible, still pseudo-extreme, starting flow for Problem $p-1$ (Lemma 3). Second, the gap between that start and the optimum of Problem $p-1$ must be small, which requires the exact maximum-flow value $f_p^*$ of each scaled problem. Third, the telescoping sum of the gaps must be estimated against $\log_2(B/\max(m,n))$ with the floors handled exactly. Integrality of every intermediate flow is not assumed; it has to be carried along the run from the integral capacities and the zero start.

Formalization scope

Everything lives in the namespace EdmondsKarp.Scaling. Nodes form an inductive type (s, t, src i, dst j). A flow is a structure with components f0, fx, fz, ret for the four arc families, real valued; the infinite capacities are encoded by the absence of an upper bound. IsMaxFlow is a predicate comparing values with every flow, not a supremum. Problem $p$ uses natural-number division for $\lfloor a_i/2^p\rfloor$ . Augmenting paths are lists of distinct nodes from s to t whose consecutive pairs have positive residual amount (resCap, valued in WithTop ℝ); they never use the return arc.

A run of the scaling method (IsScalingRun) is a family of phases $F\,p\,0,\dots,F\,p\,(K\,p)$ for $p<l$ . It starts from $0$ in Problem $l-1$ , restarts from $2F\,p\,(K\,p)$ in Problem $p-1$ , and advances by one augmentation per step. Every flow is pseudo-extreme, and each phase ends with no augmenting path left. The paper's path-selection rule (minimum weight for the modified reduced costs $\bar\Delta$ ) is abstracted to this invariant, which the paper states for it, so every run of the paper's method is covered.

The goal compares the count, cast to $\mathbb{Z}$ , with $\max(m,n)\,(2+\lfloor\log_2(B/\max(m,n))\rfloor)$ , using Real.logb 2 and Int.floor. The constant is the printed one; neither $O(\cdot)$ nor a weaker constant is acceptable. Positivity of all $a_i,b_j$ is a hypothesis, because without it the printed bound is false (for $m=5$ , $n=1$ , $a=(1,0,0,0,0)$ , $b=(1)$ one augmentation is needed and the bound is negative). A formalization in which runs could be empty or never reach a maximum flow would trivialize the goal; the run predicate forbids this, and it is satisfiable (for instance with $m=n=1$ , $a=b=(1)$ , $l=1$ and one augmentation).

A complete development needs max-flow/min-cut for the bipartite network, integrality of flows along a run, the exact value of $f_p^*$ , the telescoping identity and floor/logarithm estimates. LP duality or complementary slackness is needed only for Theorem 8. The augmenting-path and max-flow lemmas are reusable for other bipartite flow problems. Contributions welcome: proofs of any milestone, and a formalization of the paper's exact $\bar\Delta$ path rule showing that it satisfies the invariant.

Selected references

J. Edmonds, R. M. Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, Journal of the ACM 19(2):248–264, 1972. https://doi.org/10.1145/321694.321699
F. L. Hitchcock, The Distribution of a Product from Several Sources to Numerous Localities, Journal of Mathematics and Physics 20:224–230, 1941. https://doi.org/10.1002/sapm1941201224
L. R. Ford, D. R. Fulkerson, Flows in Networks, Princeton University Press, 1962. https://doi.org/10.1515/9781400875184
É. Tardos, A strongly polynomial minimum cost circulation algorithm, Combinatorica 5:247–255, 1985. https://doi.org/10.1007/BF02579369
J. B. Orlin, A faster strongly polynomial minimum cost flow algorithm, Proc. STOC 1988, 377–387. https://doi.org/10.1145/62212.62249

12 thms5 active usersReviewed

Computational Geometry Operations Research Theoretical Computer Science·Captain: mikedeng1

Linear Programming in Linear Time When the Dimension Is Fixed: Fixed-Dimension LP Feasibility Decided in Linear Time on the Real RAMResearch Paper

Motivation

A linear program asks for a point $x\in\mathbb{R}^d$ minimizing $c^Tx$ subject to $n$ linear inequalities $\sum_{j=1}^d a_{ij}x_j\ge b_i$ . Many problems in computational geometry and statistics are linear programs with few variables and very many constraints: separating two point sets by a line or plane, fitting a line in the Chebyshev ( $L_\infty$ ) norm, finding the smallest disk or ball containing a point set (a related convex problem). For these problems the number of variables $d$ is a small constant, and what matters is how the running time grows with $n$ .

Nimrod Megiddo showed that for every fixed $d$ the problem can be solved in time $C(d)\cdot n$ (J. ACM 31(1), 1984).

Timeline.

1983. Megiddo (SIAM J. Comput. 12) and, independently, Dyer (SIAM J. Comput. 13 (1984)) give linear-time algorithms for $d=2$ and $d=3$ .
1984. Megiddo extends the method to every fixed $d$ , with $C(d)<2^{2^{d+2}}$ (the paper formalized here).
1988–1991. Clarkson (J. ACM 42 (1995), conference version 1988) gives a randomized algorithm with expected time $O(d^2n)+d^{O(\sqrt d)}\log n$ . Seidel (Discrete Comput. Geom. 6 (1991)) gives a simple randomized $O(d!\,n)$ algorithm.
1992–1996. Matoušek, Sharir and Welzl and, independently, Kalai give subexponential randomized bounds. Chazelle and Matoušek derandomize the linear dependence with $C(d)=d^{O(d)}$ (J. Algorithms 21 (1996)).

Setting

Fix $d$ . An instance is a matrix $A\in\mathbb{R}^{n\times d}$ and a vector $b\in\mathbb{R}^n$ , and its feasible region is the polyhedron $P(A,b)=\{x\in\mathbb{R}^d: Ax\ge b\}$ . Here $n$ is the number of constraints and $d$ the number of variables.

The model of computation is the real RAM. A program is a finite list of instructions acting on real registers, integer pointer registers and a memory $\mathbb{Z}\to\mathbb{R}$ . It performs exact $+,-,\times,/$ on reals at unit cost, tests the sign of a real, sets, copies, increments, decrements and compares pointers, and loads and stores through pointers. The input is the standard encoding of $(A,b)$ in memory: the numbers $n$ and $d$ , then $A$ row by row, then $b$ . A program decides an instance within $T$ steps with output $\beta\in\{\text{accept},\text{reject}\}$ if it halts on that output after at most $T$ steps.

Megiddo's method rests on multidimensional search. There is an unknown point $x^*\in\mathbb{R}^d$ and an oracle that, for any hyperplane $\{x: a^Tx=b\}$ , answers whether $a^Tx^*<b$ , $=b$ or $>b$ . Given hyperplanes $H_i=\{a_i^Tx=b_i\}$ with $a_i\ne0$ , the question is how many oracle calls determine the position of $x^*$ relative to all of them. A search strategy is a ternary decision tree: inner nodes are hyperplane queries, leaves carry outputs, and the tree is built from the data alone. For linear programming, $x^*$ is an optimal solution, or a minimizer of the infeasibility function $f(x)=\max_i(b_i-a_i^Tx)$ when the system is infeasible. The oracle is implemented by solving problems in $d-1$ variables.

Formalization targets

Goal: linear-time feasibility on the real RAM

\forall d\ \exists R\ \exists C\ \forall n\ \forall A\in\mathbb{R}^{n\times d},\,b\in\mathbb{R}^n:\quad R\text{ decides within }C\,(n+1)\text{ steps whether } \{x: Ax\ge b\}\neq\emptyset.

The program and the constant depend on $d$ only. No explicit form of $C(d)$ is fixed.

Milestones

One query settles half of $n$ hyperplanes on the line ( $A(1)=1$ , $B(1)=\tfrac12$ ).
$v(\epsilon)=(1,\epsilon,\dots,\epsilon^{d-1})$ is orthogonal to some $a_i$ for at most $n(d-1)$ values of $\epsilon$ , so there is a basis in which all $a_{ij}\ne0$ .
For hyperplanes of opposite slopes in the $(x_1,x_2)$ plane, the answers for $H^{(1)}_{ik}$ and $H^{(2)}_{ik}$ settle one of $H_i$ , $H_k$ .
A linearly dependent pair of opposite slopes has $a_{i1}=a_{k1}=0$ , and the middle hyperplane settles one of them.
Approach I: $2^{d-1}$ queries settle at least $\lfloor 2^{1-2^d}n\rfloor$ hyperplanes.
$C(d)\log n$ queries settle all $n$ hyperplanes.
If a hyperplane contains no optimal point, all optimal points lie on one side of it.
The oracle, Case I: at an optimum relative to $\{x_d=0\}$ , two auxiliary systems decide the side or certify global optimality.
The oracle, Case II: at a minimizer of $f$ on $\{x_d=0\}$ , systems (1) and (2) decide the side or certify infeasibility.

Significance

The result. For every fixed dimension, linear programming is solvable in time linear in the number of constraints. The algorithm is also strongly polynomial in fixed dimension: its operation count does not depend on the bit size of the data. Deciding whether the optimum is at most $t$ is feasibility of $Ax\ge b$ together with $-c^Tx\ge-t$ , so the goal also covers the decision form of optimization. The prune-and-search technique of the paper, which discards a constant fraction of the constraints per round, became a standard tool of computational geometry.

Formalizing it. The result is proved and classical. The platform already has the cases $d=1$ (linear time) and $d=2$ (quadratic time, by Fourier–Motzkin elimination) on the same machine and input encoding (SmaleNinth.real_ram_decides_one_variable_lp_linear, SmaleNinth.real_ram_decides_two_variable_lp_quadratic). No machine-checked proof of the general statement is known. The work consists of the query-complexity layer (milestones 1–6), the convex-analytic correctness of the oracle (milestones 7–9), and a real-RAM implementation with a step count linear in $n$ , including linear-time median selection. Alternative proofs, for example through Clarkson's or Seidel's algorithms made deterministic, are welcome for the goal.

Difficulty

The obvious approach is to find the optimum by testing constraints one by one or by eliminating variables. Fourier–Motzkin elimination produces $\Theta(n^2)$ constraints after one step. Pivoting methods have no known bound linear in $n$ . The key difficulty is to discard a constant fraction of the constraints using only a constant number of recursive calls in dimension $d-1$ , when no single hyperplane test gives information about more than one constraint. The multidimensional search layer gives this, and it is where the pairing of hyperplanes by slope and the degenerate cases (dependent pairs, zero coefficients) have to be handled exactly. At the machine level, the step count must stay linear in $n$ for a fixed program, so every median selection and every recursive call must be implemented within the budget, with the recursion depth depending on $d$ only.

Formalization scope

Machine and input. The machine is the platform's real RAM SmaleNinth.RAMProgram with RAMDecidesInTime, and the input convention is SmaleNinth.encodeLP (published definitions, reused unchanged). No instruction is added: there is no LP, median, floor or sort primitive. Time is the number of machine steps.
Quantifier order. $\forall d\ \exists R\ \exists C\ \forall n, A, b$ . The bound is $C(n+1)$ in the number $n$ of constraints, so that the machine can halt at $n=0$ . The paper's $C(d)<2^{2^{d+2}}$ counts unspecified units of "effort" with an unquantified $\theta(nd)$ term, and it is not transferred to machine steps. Where a milestone's proof fixes a constant exactly, the constant is stated: $2^{d-1}$ queries and $\lfloor n/2^{2^d-1}\rfloor$ settled hyperplanes in milestone 5.
Feasibility only. The machine outputs accept or reject. Returning an optimizer, "unbounded", or a minimizer of $f$ is not part of the goal. The case $d=0$ is included.
Query trees. Nodes are queries compare (a ⬝ᵥ x) b and nothing else, leaves hold fixed values, and correctness is required for every $x$ . A tree over arbitrary tests of $x$ would make milestones 5 and 6 empty, and it is excluded by the definition.
Indices. The paper's $x_1,x_2$ are indices 0, 1 of Fin (d + 2), and its $x_d$ is Fin.last d of Fin (d + 1).
Corrections. Two passages of §4 are stated in corrected form. The Case I auxiliary objective includes the $\pm c_d$ term of the direction. In Case II, feasibility of (1) puts improvement in $\{x_d>0\}$ , where the page's last sentence says $\{x_d<0\}$ . The pairing claim carries $a_{k1}a_{i2}-a_{k2}a_{i1}\ne0$ , the hypothesis its argument uses, since linear independence alone does not give it.
Not included. Approach II and its bound $O(n(\log n)^{d^2})$ , the remarks on slowly growing $d$ , the randomized variants, and the applications of §1.
Reusable parts. The query-tree definition and milestones 1–6 apply to any prune-and-search problem with a hyperplane oracle. The oracle lemmas (7–9) are statements about convex piecewise-linear functions and polyhedra.

Selected references

N. Megiddo, Linear programming in linear time when the dimension is fixed, J. ACM 31(1):114–127, 1984. https://doi.org/10.1145/2422.322418
N. Megiddo, Linear-time algorithms for linear programming in $R^3$ and related problems, SIAM J. Comput. 12(4):759–776, 1983. https://doi.org/10.1137/0212052
M. E. Dyer, Linear time algorithms for two- and three-variable linear programs, SIAM J. Comput. 13(1):31–45, 1984. https://doi.org/10.1137/0213003
K. L. Clarkson, Las Vegas algorithms for linear and integer programming when the dimension is small, J. ACM 42(2):488–499, 1995. https://doi.org/10.1145/201019.201036
R. Seidel, Small-dimensional linear programming and convex hulls made easy, Discrete Comput. Geom. 6:423–434, 1991. https://doi.org/10.1007/BF02574699
B. Chazelle, J. Matoušek, On linear-time deterministic algorithms for optimization problems in fixed dimension, J. Algorithms 21(3):579–597, 1996. https://doi.org/10.1006/jagm.1996.0046

16 thms5 active usersReviewed

Combinatorics·Captain: Shuze Chen

The Polynomial Hirsch ConjectureOpen Problem

Motivation

The simplex method walks along edges of a polytope from vertex to vertex. Whether any pivot rule could ever make that walk short in the worst case is governed by a prior, purely geometric question: how far apart, in the edge graph, can two vertices of a polytope be? Warren Hirsch conjectured in 1957 that the diameter of a $d$ -dimensional polytope with $n$ facets is at most $n - d$ . Half a century of upper bounds stalled at quasi-polynomial, and Santos disproved the conjecture itself in 2012 — but only by a constant factor. The surviving question, the subject of the Polymath 3 project, is the polynomial Hirsch conjecture: is the diameter bounded by a polynomial in $n$ and $d$ ?

Timeline

1957. Hirsch states the conjecture $\mathrm{diam} \le n - d$ in a letter to Dantzig, who publishes it in Linear Programming and Extensions (1963).
1964–1966. Klee determines the exact maximum diameter of $3$ -polytopes with $n$ facets, $\lfloor 2n/3\rfloor - 1$ — the Hirsch bound holds up to dimension three.
1967. Klee and Walkup (Acta Math.) refute the unbounded-polyhedron version, prove the bounded conjecture for $n - d \le 5$ , and reduce the general case to the $d$ -step conjecture ( $n = 2d$ ).
1970. Larman (Proc. LMS) proves $\mathrm{diam} \le n\,2^{d-3}$ — linear in the number of facets for each fixed dimension, still the best bound of that shape.
1989. Naddef (Math. Programming) proves $0/1$ -polytopes satisfy the Hirsch bound, with diameter at most $d$ .
1992. Kalai and Kleitman (Bull. AMS) prove $\mathrm{diam} \le n^{\log_2 d + 2}$ in under a page — the quasi-polynomial barrier every later bound refines. The same year brings subexponential pivot rules (Kalai; Matoušek–Sharir–Welzl), the algorithmic counterpart.
2010. Eisenbrand, Hähnle, Razborov, and Rothvoß (Math. OR) show the known upper-bound arguments survive in a purely combinatorial abstraction — which admits almost-quadratic lower bounds, so a polynomial bound must use real geometry. Kalai launches Polymath 3 on the polynomial version.
2010–2012. Santos (Annals of Math.) disproves the Hirsch conjecture: a $43$ -dimensional polytope with $86$ facets and diameter at least $44$ , via spindles of large width.
2014–2019. Todd (SIAM J. Discrete Math.) sharpens Kalai–Kleitman to $(n-d)^{\log_2 d}$ ; Sukegawa refines further. Matschke, Santos, and Weibel (Proc. LMS 2015) shrink the counterexample to dimension $20$ with $40$ facets and diameter $21$ . All known violations remain constant-factor; all known bounds remain quasi-polynomial.

Setting

Work in $\mathbb{R}^d$ . An H-polytope is a set cut out by finitely many linear inequalities: given vectors $a_1, \dots, a_n \in \mathbb{R}^d$ and reals $b_1, \dots, b_n$ , it is

P \;=\; \{\, x \in \mathbb{R}^d \mid \langle a_i, x\rangle \le b_i \text{ for } i = 1, \dots, n \,\},

where $\langle a_i, x\rangle = \sum_{j=1}^d a_{ij} x_j$ is the standard inner (dot) product — so each condition $\langle a_i, x\rangle \le b_i$ is one linear inequality, with normal vector $a_i$ and offset $b_i$ . Throughout, $P$ is assumed nonempty and bounded. The parameter $n$ counts the inequalities in the given description; since every polytope with $f$ facets admits a description by exactly $f$ inequalities, bounds stated in terms of $n$ over all descriptions are equivalent to bounds in terms of facet counts.

A vertex of $P$ is an extreme point. Two vertices $u \ne v$ are adjacent when the segment $[u, v]$ is an extreme subset of $P$ ; for a polytope the convex extreme subsets are exactly the faces, so this says precisely that $[u,v]$ is a one-dimensional face — an edge. The combinatorial diameter of $P$ is the diameter of the graph of vertices and edges. Throughout, "diameter at most $B$ " is expressed as: every two vertices are joined by a walk of $B$ steps, each step staying put or crossing an edge — a form that is monotone in $B$ and asserts connectivity of the graph (Balinski's theorem) as part of the claim.

Formalization targets

Goal — the polynomial Hirsch conjecture

\exists\, c, k \in \mathbb{N}:\ \text{every nonempty bounded } P = \{x \in \mathbb{R}^d \mid \langle a_i, x \rangle \le b_i,\ i \le n\} \text{ has diameter} \le c\,(n + d)^k.

Every polynomial in $n$ and $d$ is dominated by some $c(n+d)^k$ and conversely, so this is exactly polynomiality, with no committed degree — the form that survives any future sharpening of constants or exponents.

Milestones — the known ladder

Six classical results over the same definitions: the Hirsch bound $n - d$ in dimension $d \le 3$ (Klee; Klee–Walkup); Larman's bound $n \cdot 2^{d-3}$ ; Naddef's bound $d$ for $0/1$ -polytopes; the Kalai–Kleitman bound $n^{\log_2 d + 2}$ ; Todd's bound $(n-d)^{\log_2 d}$ for full-dimensional $P$ with $n \ge d \ge 3$ ; and — in the other direction — the Santos counterexample: a nonempty bounded H-polytope whose diameter exceeds $n - d$ .

Significance

A polynomial diameter bound is necessary for any pivot rule of the simplex method to run in polynomial time in the worst case: if vertices can be super-polynomially far apart, no edge-following algorithm can connect them quickly. A refutation would close off one of the main hoped-for routes to a strongly polynomial linear programming algorithm (Smale's ninth problem). The conjecture is also the test question of polyhedral graph theory: the Kalai–Kleitman argument uses so little about polytopes that it holds for far more general set systems, and Eisenbrand, Hähnle, Razborov, and Rothvoß (Math. OR 2010) showed such abstractions admit almost-quadratic lower bounds — so a proof of the conjecture must use geometry the abstract setting lacks, and a disproof must beat the abstraction barrier's constructions with actual polytopes.

None of these results has been formalized in any proof assistant; Mathlib has extreme points and faces of convex sets, but no polytope combinatorics — no vertex-edge graph, no diameter, no facet counting. This mission builds that layer: an H-polytope model, adjacency via faces, and walk-based diameter bounds, against which both the upper-bound ladder and the Santos disproof can be machine-checked. The Kalai–Kleitman proof is one page from first principles and is the natural summit; the Santos construction is a concrete finite object whose verification is a different, computational kind of challenge.

Difficulty

The naive approach — walk toward the target vertex by always improving some linear objective — is exactly the simplex method, and proving any polynomial bound on such walks is open for every known pivot rule; monotone variants of the diameter question have exponential lower bounds. The obvious inductive strategy (bound the diameter by recursing on facets) is precisely what Kalai–Kleitman optimizes, and it provably cannot go below quasi-polynomial without using metric or topological properties of actual polytopes, by the abstraction lower bound above. On the other side, making diameters large is blocked by the wedge/spindle calculus only producing constant-factor violations. The problem sits in a genuine gap: no technique on either side is known to reach polynomial.

Formalization scope

The Lean model commits to: ambient space EuclideanSpace ℝ (Fin d); the polytope as Hpoly a b = {x | ∀ i, ⟪a i, x⟫ ≤ b i} for a : Fin n → EuclideanSpace ℝ (Fin d), b : Fin n → ℝ, with nonemptiness and Bornology.IsBounded as explicit hypotheses (boundedness is essential: Klee–Walkup's unbounded counterexample would otherwise trivialize the Santos milestone); vertices as Set.extremePoints ℝ; adjacency as u ≠ v ∧ IsExtreme ℝ P (segment ℝ u v); and diameter bounds as the walk predicate DiamLE, whose stationary steps make it monotone in the bound. Real-exponent bounds enter through Real.logb and the natural floor. In larman_bound and the two Hirsch-form bounds the subtraction is natural-number (truncated) subtraction, which only weakens nothing: the stated forms are true as written for all $n, d$ in scope. The dimension parameter $d$ is the ambient dimension; lower-dimensional polytopes are included, and every milestone is stated so as to remain true for them, with todd_bound requiring full-dimensionality ((interior P).Nonempty) as in its source.

Welcome contributions: any milestone in any order (dimension_three_bound for $d \le 1$ cases and structural lemmas about Adj and DiamLE are natural entry points, and kalai_kleitman_bound is the summit); reusable infrastructure — polytopes have finitely many extreme points, faces of H-polytopes, Balinski connectivity — published as platform theorems; and, as a separate expedition, the explicit Santos or Matschke–Santos–Weibel polytope. Statements about unbounded polyhedra, the simplex method itself, and subexponential pivot rules are left to future missions.

Selected references

V. Klee, D. Walkup, The d-step conjecture for polyhedra of dimension d < 6, Acta Math. 117 (1967). doi:10.1007/BF02392971
D. Larman, Paths on polytopes, Proc. London Math. Soc. 20 (1970). doi:10.1112/plms/s3-20.2.249
D. Naddef, The Hirsch conjecture is true for (0,1)-polytopes, Math. Programming 45 (1989). doi:10.1007/BF01589418
G. Kalai, D. Kleitman, A quasi-polynomial bound for the diameter of graphs of polyhedra, Bull. AMS 26 (1992). arXiv:math/9204233
F. Santos, A counterexample to the Hirsch conjecture, Annals of Mathematics 176 (2012). arXiv:1006.2814
M. Todd, An improved Kalai–Kleitman bound for the diameter of a polyhedron, SIAM J. Discrete Math. 28 (2014). arXiv:1402.3579
B. Matschke, F. Santos, C. Weibel, The width of five-dimensional prismatoids, Proc. London Math. Soc. 110 (2015). arXiv:1202.4701
F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Diameter of polyhedra: limits of abstraction, Math. Oper. Res. 35 (2010). doi:10.1287/moor.1100.0470
F. Santos, Recent progress on the combinatorial diameter of polytopes and simplicial complexes, TOP 21 (2013) (survey). arXiv:1307.5900

81 thms5 active usersReviewed

Completed

Operations Research Optimization·Captain: Shuze Chen

Introduction to Linear Optimization X: Max-Flow Min-CutTextbook

How much flow can be sent from a source $s$ to a sink $t$ through a network with arc capacities $u_{ij}\in(0,\infty]$ — and what certifies that no more is possible? This mission formalizes §7.4-7.5 of Bertsimas & Tsitsiklis. The circulation calculus of §7.4 supplies the two structural tools: the flow decomposition theorem (Lemma 7.1 — every nonzero nonnegative circulation is a positive combination $\mathbf{f}=\sum_i a_i\mathbf{f}^i$ of simple circulations with only forward arcs, with integer $a_i$ when $\mathbf{f}$ is integer) and the optimality criterion for the minimum cost network flow problem (Theorem 7.6 — a feasible flow is optimal if and only if there is no unsaturated cycle with negative cost). Section 7.5 then formulates the maximum flow problem ( $\max b_s$ s.t. $\mathbf{A}\mathbf{f}=\mathbf{b}$ , $b_t=-b_s$ , $b_i=0$ for $i\ne s,t$ , $0\le\mathbf{f}\le\mathbf{u}$ ), defines augmenting paths (Definition 7.2: $f_{ij}<u_{ij}$ on forward arcs, $f_{ij}>0$ on backward arcs) and the Ford–Fulkerson algorithm, and proves integer invariance and finite termination for integer capacities (Theorem 7.8). The goal is Theorem 7.10:

(a) if the Ford–Fulkerson algorithm terminates because no augmenting path can be found, the current flow is optimal;

(b) the value of the maximum flow equals the minimum cut capacity

C(S)=\sum_{\{(i,j)\in\mathcal{A}\mid i\in S,\,j\notin S\}}u_{ij}

— the archetypal combinatorial min-max theorem, which the book notes can also be read as LP duality (pp. 311-312).

14 thms5 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Linear Programming: Foundations and Extensions I: Degeneracy and Termination of the Simplex Method under Bland's RuleTextbook

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

10 thms4 active usersReviewed

Completed

Algorithmic Game Theory Convex Optimization Operations Research·Captain: mikedeng1

Theory of Games and Economic Behavior III: Mixed Strategies, the Minimax Theorem and Good StrategiesTextbook

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

(13:A*) $\operatorname{Max}_x \operatorname{Min}_y \phi \le \operatorname{Min}_y \operatorname{Max}_x \phi$ .
(13:D*) If $\operatorname{Max}\operatorname{Min} = \operatorname{Min}\operatorname{Max}$ , the saddle points of $\phi$ are exactly $A^\phi \times B^\phi$ .
(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$ .
(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$ .
(16:F) The weak form with $\ge 0$ in place of $> 0$ .
(17:6) The minimax theorem: a saddle point of $K$ exists (already on the platform as AGT.zero_sum_minimax, proved).
(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.

11 thms4 active usersReviewed

Completed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

Numerical Techniques for Stochastic Optimization I: Edmundson–Madansky Bounds for Independent Random Data and Simple RecourseTextbook

Motivation

In a two-stage stochastic linear program a decision $x$ is taken before random data $\xi$ are observed, and a corrective recourse decision $y$ is taken afterwards at a cost. The objective contains the expectation of an optimal value of a linear program, $\int Q(x,\xi(\omega))\,P(d\omega)$ , and for continuous or high-dimensional $\xi$ that integral cannot be evaluated exactly. Practical methods therefore replace $\xi$ by a discrete random vector and control the error by computable lower and upper bounds on the expected recourse cost. Chapter 2 of Ermoliev and Wets (eds.), Numerical Techniques for Stochastic Optimization (Springer 1988), by P. Kall, A. Ruszczyński and K. Frauendorfer, surveys these bounds as they were used in the codes of the time: Jensen's inequality from below, the Edmundson–Madansky inequality from above, and the special structure of simple recourse, where the expected cost is available in closed form.

Timeline. Jensen's inequality (1906) gives the lower bound for a convex integrand. A. Madansky, "Bounds on the expectation of a convex function of a multivariate random variable", Ann. Math. Statist. 30 (1959), and H. P. Edmundson (RAND report, 1956) gave the upper bound by the two-point law on the endpoints of an interval, and its product version for independent components. Kall and Stoyan (1982), Huang, Ziemba and Ben-Tal (1977), Frauendorfer and Kall (1988) developed partition refinement of both bounds, the scheme this chapter describes; Frauendorfer (1988) extended the upper bound to dependent data on boxes.

Setting

The two-stage problem (2.11) is: minimize $\psi(x)=c^Tx+\int_\Omega Q(x,\xi(\omega))\,P(d\omega)$ subject to $Ax=b$ , $x\ge 0$ . The recourse cost $Q(x,\xi)$ is the optimal value of the second-stage problem (2.12),

Q(x,\xi)=\min\{q^Ty : Wy=h-Tx,\ y\ge 0\},\qquad \xi=(q,h,T),

with a deterministic $m_2\times n_2$ matrix $W$ (fixed recourse), and $Q=+\infty$ when (2.12) is infeasible. Throughout the chapter the book assumes complete recourse, $\{Wy:y\ge0\}=\mathbb R^{m_2}$ , and dual feasibility: for every realization of $q$ some $u$ satisfies $W^Tu\le q$ . Under these assumptions $Q$ is finite. The expected recourse function is $\mathcal Q(x)=\int Q(x,\xi(\omega))\,P(d\omega)$ .

The Edmundson–Madansky law of an interval $[a,b]$ , $a<b$ , with mean $\xi^0$ puts mass $p_1=(b-\xi^0)/(b-a)$ at $a$ and $p_2=(\xi^0-a)/(b-a)$ at $b$ (2.32). For a box $\Xi=\times_{j=1}^m[a_j,b_j]$ and means $\xi^0_j$ , the vector $\hat\xi$ with independent components of these two-point laws sits at the vertex $v$ with probability $\prod_j p_j(v_j)$ .

Simple recourse is the case $W=[I,-I]$ , $q=[q^+,q^-]$ with $q^+_j+q^-_j\ge0$ , deterministic $T$ and random $h$ only. With $\chi=Tx$ the recourse cost splits into one-row costs $Q_j(\chi_j,h_j)=q^+_j(h_j-\chi_j)$ if $h_j\ge\chi_j$ , and $q^-_j(\chi_j-h_j)$ otherwise.

Formalization targets

Goal: the Edmundson–Madansky bound for independent components (p. 46)

If $\xi$ has independent components $\xi_j\in[a_j,b_j]$ with means $\xi^0_j$ , and $\varphi$ is convex on $\Xi=\times_j[a_j,b_j]$ , then

E\varphi(\xi)\le\sum_{v\in\mathrm{vert}\,\Xi}\Big(\prod_{j=1}^m p_j(v_j)\Big)\varphi(v).

The book applies it to $\varphi=Q(x,\cdot)$ ; the goal is stated for every convex $\varphi$ , with the explicit weights of (2.32).

Milestones

Properties (b), (d), (e) of p. 40: $Q(x,\cdot)$ is piecewise linear and convex in $(h,T)$ ; $Q(\cdot,\xi)$ is convex piecewise linear in $x$ ; the expected recourse function is finite and convex under finite second moments.
The Jensen lower bound (2.26)–(2.27) on a partition (a published, proved theorem, reused).
The dual-multiplier lower bound (2.30)–(2.31).
The one-dimensional Edmundson–Madansky inequality (2.32)–(2.34).
For simple recourse: separability (2.46)–(2.49), the closed form (2.51) of $EQ_j$ , and the bounds (2.55)–(2.56) from the one-block problem.

Significance

The upper bound is the half of the bounding scheme that is not automatic. Jensen's inequality needs only a mean; an upper bound on the expectation of a convex function needs a bounded support and, in the product form, independence. Together they give a certified interval for the optimal value of a two-stage problem, and repeated partitioning of the support shrinks that interval; this is the basis of the sequential approximation methods of §2.2.4 and of later codes. The dual-multiplier bound and the simple-recourse formulas are the pieces that make those intervals cheap to compute.

The results are classical and proved in the literature cited on the page. The one-dimensional Edmundson–Madansky inequality and the general extreme-point form of the upper bound (a measure on the extreme points reproducing the barycentre) are already formalized on Prove2Me in the Introduction to Stochastic Programming series, as is the partition Jensen bound. The product form for independent components is not: deriving it from the extreme-point form requires constructing the product kernel, which is the content of this mission. The recourse properties (b), (d), (e) for a general distribution with finite second moments, the dual-multiplier bound and the simple-recourse formulas are not formalized anywhere known to this mission.

Difficulty

The obvious argument inducts on the dimension, applying the one-dimensional inequality in one coordinate while the others are held fixed. That step needs the conditional law of the remaining coordinates given the first to be their unconditional law, i.e. independence expressed as a product decomposition of the joint law, and it needs $\varphi$ with one coordinate replaced by an endpoint to remain convex on the lower-dimensional box and integrable. For dependent components the inequality is false with these weights: on $[0,1]^2$ with means $(\tfrac12,\tfrac12)$ and $\varphi(x,y)=(x-y)^2$ , the product law gives $\tfrac12$ while mass $\tfrac12$ at $(1,0)$ and at $(0,1)$ gives $1$ . The book's remark that the product law is extremal among all laws on $\Xi$ with the given mean fails for this reason when $m\ge2$ , and is not part of this mission.

For the recourse properties the difficulty is bookkeeping: $Q$ is an extended-real optimal value, and finiteness, measurability in $\omega$ and integrability must be derived from complete recourse, dual feasibility and the moment hypothesis rather than assumed.

Formalization scope

Vectors are functions from finite index types to $\mathbb R$ (ι → ℝ), matrices are Mathlib Matrix, and random data live on a probability space (Ω, P). The recourse cost is an EReal infimum over the feasible set, so infeasibility gives $+\infty$ and unboundedness $-\infty$ exactly as on p. 39; theorems that integrate it carry complete recourse and dual feasibility, which make it finite. The expected recourse function integrates the real part of the recourse cost. Independence of the components is ProbabilityTheory.iIndepFun; the box is Set.pi univ (fun j => Icc (a j) (b j)), with $a_j<b_j$ , and values in the box are required almost surely. The upper bound is the explicit sum over Boolean vertex labels of products of the weights (2.32); no abstract extremal measure is used.

Conventions fixed where the page is silent or ambiguous:

Properties (b), (d), (e) are stated on all of $\mathbb R^{n_1}$ : under the standing complete-recourse assumption $K_2=\mathbb R^{n_1}$ . "Convex piecewise linear" is rendered as a maximum of finitely many affine functions.
The book's hypothesis of finite second moments in (e) is kept as stated, componentwise.
The book writes $Q$ for both $Q(x,\xi)$ and $\mathcal Q(x)$ , and reuses $\tilde Q$ , $\tilde\psi$ for different functions in (2.27) and (2.30)–(2.31); the Lean names are recourseCost, expectedRecourse and dualLowerBound.
In (2.51) a conditional mean on a null event is $0$ in Lean; it always appears multiplied by that event's probability, so the formula is unchanged.
In (2.56) the minimum is a real infimum over the nonempty first-stage feasible set; attainment is not claimed.
No constant of the chapter is hidden behind $O(\cdot)$ ; all bounds are explicit.

A goal stated for affine $\varphi$ (where it is an equality), or with $\hat\xi$ allowed to be any discrete law with the right mean, would be trivial or a different theorem; the weights are the products of (2.32), and independence of the components is a hypothesis.

A complete development needs: finite-dimensional LP duality with extended-real values (reusable across all recourse missions), measurability and integrability of optimal-value functions, the conditional-independence step for product measures, and the one-dimensional chord inequality. The partitioned upper bound (2.37) and the discrete reformulation (2.21), (2.28) are natural follow-up statements on the same definitions.

Selected references

P. Kall, A. Ruszczyński, K. Frauendorfer, "Approximation Techniques in Stochastic Programming", in Yu. Ermoliev and R. J-B Wets (eds.), Numerical Techniques for Stochastic Optimization, Springer Series in Computational Mathematics 10, Springer 1988, Ch. 2, pp. 33–64. https://doi.org/10.1007/978-3-642-61370-8
A. Madansky, "Bounds on the expectation of a convex function of a multivariate random variable", Annals of Mathematical Statistics 30 (1959), 743–746. https://doi.org/10.1214/aoms/1177706203
P. Kall, Stochastic Linear Programming, Springer 1976. https://doi.org/10.1007/978-3-642-66252-2
R. J-B Wets, "Stochastic programs with fixed recourse: the equivalent deterministic program", SIAM Review 16 (1974), 309–339. https://doi.org/10.1137/1016053
K. Frauendorfer, "Solving SLP recourse problems with arbitrary multivariate distributions — the dependent case", Mathematics of Operations Research 13 (1988), 377–394. https://doi.org/10.1287/moor.13.3.377
J. R. Birge, F. Louveaux, Introduction to Stochastic Programming, Springer 1997, Ch. 8. https://doi.org/10.1007/b97617

13 thms4 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

Selected Topics in Column Generation III: Ryan–Foster Branching — a Fractional Basic Set-Partitioning Solution Covers Some Row Pair FractionallyResearch Paper

Motivation

Column generation solves linear programs with far too many variables to list: one works with a small subset $J' \subseteq J$ of the columns, the restricted master problem (RMP), and adds columns of negative reduced cost as a pricing problem finds them (Lübbecke and Desrosiers 2005, §2.1). Many integer programs from vehicle routing, crew scheduling and crew pairing are reformulated so that the master problem is a set-partitioning problem: every row (a customer, a flight leg, a task) must be covered by exactly one selected column (a route, a pairing, a schedule). The linear relaxation of such a master is solved by column generation, and an integer solution is then sought by branch-and-price, branch-and-bound with column generation at every node.

Branching in branch-and-price is not free. Fixing a master variable $\lambda_j$ to $0$ does not stop the pricing problem from regenerating the same column, and handling that complicates the pricing problem. The rule that avoids this for set partitioning goes back to Ryan and Foster (1981): branch on a pair of rows, requiring them to be covered either by the same column or by two different columns. Both requirements are constraints the pricing problem can respect directly. Lübbecke and Desrosiers call it "the most common scheme in conjunction with column generation" (§7.3, p. 1020) and state the proposition that makes it well defined as their Proposition 3.

Timeline:

1981: Ryan and Foster introduce the pair-of-rows branching rule for set partitioning in crew scheduling.
1998: the branch-and-price survey of Barnhart et al. (1998) presents the rule as the branching scheme for set-partitioning masters.
2005: Lübbecke and Desrosiers state it as Proposition 3 of their survey, attributing it to Ryan and Foster without proof.

Setting

Rows are indexed by $\{1, \dots, m\}$ and columns by a finite set $J'$ . A matrix $A = (a_{rj}) \in \{0,1\}^{m \times |J'|}$ has every entry equal to $0$ or $1$ ; column $j$ covers row $r$ when $a_{rj} = 1$ . The set-partitioning system of the RMP's linear relaxation is

A\lambda = \mathbf 1, \qquad \lambda \ge \mathbf 0, \qquad \lambda \in \mathbb R^{J'} .

A vector $\lambda$ is a basic feasible solution of this system when it satisfies all its constraints and, among the constraints active at $\lambda$ (the $m$ equality rows, and the constraints $\lambda_j \ge 0$ with $\lambda_j = 0$ ), there are $|J'|$ linearly independent ones. Equivalently, $\lambda$ is feasible and the columns of $A$ in the support of $\lambda$ are linearly independent. A solution is fractional when it is not a $0/1$ vector, $\lambda \notin \{0,1\}^{|J'|}$ .

For two rows $r, s$ the Ryan–Foster quantity is $\sum_{j \in J'} a_{rj} a_{sj} \lambda_j$ , written pairCover A lam r s in Lean: the total weight on the columns that cover both rows. For $r = s$ it is the row sum, equal to $1$ on every feasible $\lambda$ .

Formalization targets

Goal: Proposition 3 (p. 1020)

For every $0/1$ matrix $A$ and every fractional basic feasible solution $\lambda$ of $A\lambda = \mathbf 1$ , $\lambda \ge \mathbf 0$ ,

\exists\, r, s \in \{1, \dots, m\}: \qquad 0 < \sum_{j \in J'} a_{rj}\, a_{sj}\, \lambda_j < 1 .

The two rows are automatically distinct. The statement concerns every fractional basic solution, not only an optimal one, and no cost vector enters it.

Milestone: the branches keep every integer solution (§7.3, p. 1020)

For every $0/1$ solution $\lambda \in \{0,1\}^{|J'|}$ of $A\lambda = \mathbf 1$ and every pair of rows $r, s$ ,

\sum_{j \in J'} a_{rj}\, a_{sj}\, \lambda_j \in \{0, 1\} .

This is the paper's requirement that "integer solutions remain intact" (p. 1019), specialised to the two branches " $= 1$ " and " $= 0$ " of the paragraph after Proposition 3.

Significance

Proposition 3 is what makes Ryan–Foster branching a valid branching scheme in the sense of §7.3: the current fractional solution violates both branches for the chosen pair, so it is excluded from both children, while by the milestone every integer solution survives in one of them. The same pair-of-rows idea underlies branching in bin packing, graph colouring, vehicle routing and crew scheduling codes, where it is used because both branches translate into constraints on the pricing problem rather than on individual master variables.

The paper states the result and refers its proof to Ryan and Foster (1981); no machine-checked version of the proposition is known. This mission produces a formal statement tied to a standard, representation-aware definition of basic solutions (Bertsimas–Tsitsiklis Definition 2.9, already on the platform) and, once proved, a verified lemma that any formal development of branch-and-price for set partitioning can cite.

Difficulty

An argument that uses only feasibility and a fractional coordinate cannot work. Without basicness the claim is false: with one row and two identical columns, $A = [1\ 1]$ , the vector $\lambda = (\tfrac12, \tfrac12)$ is feasible and fractional, yet the only pair of rows is $r = s$ , whose quantity is $1$ . The difficulty is to turn basicness, a linear-algebra condition, into a combinatorial statement about which rows the fractional columns cover. A set-partitioning matrix need not have full row rank, so the familiar description of basic solutions through an invertible basis matrix is not available in general.

Formalization scope

Rows are Fin m and columns Fin n, so $J'$ is identified with $\{0, \dots, n-1\}$ . $A$ is a real matrix Matrix (Fin m) (Fin n) ℝ with the hypothesis IsZeroOneMatrix A (every entry $0$ or $1$ ); $\lambda$ is lam : Fin n → ℝ, since λ is a Lean keyword. Columns are $0/1$ vectors; the equivalent reading as subsets of the rows is only prose.
"Basic solution" is not defined in the paper. It is read as Bertsimas–Tsitsiklis Definition 2.9 for the standard-form constraint family: LinearOptimization.IsBasicFeasibleSolution (LinearOptimization.stdFormSystem A (fun _ => 1)) lam, from the platform definitions BasicSolution and ActiveConstraints. This definition needs no full-row-rank assumption, which a set-partitioning matrix need not satisfy, and it is not replaced by an ad hoc support condition.
Typo correction. The paper writes "i.e., $\lambda \notin \{0,1\}^m$ ". Since $\lambda$ has one coordinate per column, the statement reads it as $\lambda \notin \{0,1\}^{|J'|}$ : ¬ IsZeroOneVector lam.
The rows $r, s$ range over all of $\{1, \dots, m\}$ , including $r = s$ , as on the page; no distinctness is assumed or required.
"Fractional basic solution" is any such solution, not the RMP optimum; no costs or optimality hypothesis enter.
The milestone reads the paragraph after Proposition 3, together with the validity requirement "integer solutions remain intact" (p. 1019), as the dichotomy for all $0/1$ solutions of $A\lambda = \mathbf 1$ . The sentence about transferring the branching information to the pricing problem is not formalized.
Edge cases: for $m = 0$ basicness forces $\lambda = 0$ , and for $n = 0$ the vector is empty; in both cases no fractional basic solution exists and the goal is vacuous, as on the page.
A trivializing formalization is ruled out: dropping basicness makes the goal false (the $[1\ 1]$ example above), dropping the $0/1$ hypothesis on $A$ changes the meaning of the quantity, and replacing "fractional basic" by an unsatisfiable hypothesis would make it empty; the hypotheses are satisfied, for instance, by three rows, the columns $\{1,2\}, \{2,3\}, \{1,3\}$ and $\lambda = (\tfrac12, \tfrac12, \tfrac12)$ .

A complete development needs linear-algebra facts about basic solutions of standard-form systems without a rank assumption (support columns linearly independent), which are reusable beyond this mission. Contributions welcome: that characterization as a lemma, and proofs of the milestone and of the goal.

Selected references

M. E. Lübbecke and J. Desrosiers, Selected Topics in Column Generation, Operations Research 53(6):1007–1023, 2005. https://doi.org/10.1287/opre.1050.0234
D. M. Ryan and B. A. Foster, An integer programming approach to scheduling, in A. Wren (ed.), Computer Scheduling of Public Transport, North-Holland, 1981, pp. 269–280.
C. Barnhart, E. L. Johnson, G. L. Nemhauser, M. W. P. Savelsbergh and P. H. Vance, Branch-and-Price: Column Generation for Solving Huge Integer Programs, Operations Research 46(3):316–329, 1998. https://doi.org/10.1287/opre.46.3.316
D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Definition 2.9.

5 thms4 active usersReviewed

Completed

Discrete Geometry Operations Research Optimization·Captain: mikedeng1

Elementare Theorie der konvexen Polyeder II: Finitely Many Linear Inequalities Define a Convex Polytope Iff Their Normals Positively Span and the Region Has an Interior PointResearch Paper

Motivation

A convex polytope has two standard descriptions: as the convex hull of finitely many points, and as the intersection of finitely many half-spaces. Linear programming uses both at once. The feasible region of a linear program is given by inequalities, while the simplex method and the theory of basic solutions work with its vertices. That the two descriptions define the same class of sets is the Minkowski–Weyl theorem.

Hermann Weyl's 1935 paper Elementare Theorie der konvexen Polyeder (Comment. Math. Helv., 1935, pp. 290–306) gave an elementary, self-contained proof of this equivalence. An English translation appeared in Contributions to the Theory of Games I (Annals of Mathematics Studies 24, 1950), where it served as the polyhedral foundation for the minimax theorem and linear inequality theory in early game theory and linear programming.

Timeline:

Minkowski (1896, 1910): convex bodies, supporting planes and polyhedra in Geometrie der Zahlen, the setting Weyl's paper takes up.
Farkas (1902): the lemma on homogeneous linear inequalities that is Weyl's Satz 3.
Weyl (1935): the finite-basis theorem for cones (Hauptsatz, Satz 1), the duality between a cone and its extreme supports (§3), and the two descriptions of a convex polyhedron (§4). The paper states explicit conditions under which a finite system of inequalities defines a polytope.
Motzkin (1936), Gale, Kuhn, Tucker (1951): systematic treatments of linear inequalities built on this foundation.

Setting

Write $(a x) = a_1 x_1 + \dots + a_n x_n$ for vectors of $\mathbb{R}^n$ . A point system is a finite set $S \subseteq \mathbb{R}^n$ . It is non-degenerate if no $\alpha \neq 0$ has $(\alpha s) = 0$ for all $s \in S$ . A vector $\alpha \neq 0$ is a support of $S$ if $(\alpha s) \ge 0$ for all $s \in S$ . A support is an extreme support if equality holds at $n-1$ linearly independent points of $S$ . A point $x$ is representable by $S$ if $x = \sum_{s \in S} c_s s$ with all $c_s \ge 0$ .

Read as inequalities $(a \xi) \ge 0$ , $a \in S$ , the same $S$ defines the cone $(S)$ of solutions. An extreme solution is a nonzero $\xi \in (S)$ at which $n-1$ linearly independent inequalities of $S$ are tight. The dual system $\Sigma$ consists of the inequalities $(\alpha x) \ge 0$ , one for each extreme solution $\alpha$ , and $(\Sigma)$ is the cone it defines.

For polytopes, Weyl passes to the hyperplane $x_n = -1$ , identified with $\mathbb{R}^m$ , $m = n-1$ . A convex polyhedron is $\operatorname{conv} S$ for a finite $S \subseteq \mathbb{R}^m$ whose affine span is all of $\mathbb{R}^m$ . Given a finite index set $J$ , normals $A_j \in \mathbb{R}^m$ and constants $b_j \in \mathbb{R}$ , the inequalities $A_j \cdot x - b_j \ge 0$ cut out a region

H = \{x \in \mathbb{R}^m : A_j \cdot x - b_j \ge 0 \ \text{for all } j \in J\}.

In Weyl's notation, row $j$ is $(\alpha x) \equiv \alpha_1 x_1 + \dots + \alpha_{n-1}x_{n-1} - \alpha_n \ge 0$ , with $A_j = (\alpha_1,\dots,\alpha_{n-1})$ and $b_j = \alpha_n$ .

Formalization targets

Goal: §4 II (pp. 302–303)

Assume no row is identically zero ( $A_j \ne 0$ or $b_j \ne 0$ ). Then

H \text{ is a convex polyhedron} \iff \Big(\forall \pi' \in \mathbb{R}^m\ \exists \nu \ge 0:\ \pi' = \sum_j \nu_j A_j\Big) \ \wedge\ \Big(\exists c:\ A_j \cdot c - b_j > 0 \ \forall j\Big).

In words, the normals must positively span $\mathbb{R}^m$ and $H$ must contain an inner point. The goal is the equivalence, not either half alone.

Milestones, in the order the proof of §4 II uses them

Satz 1 (Hauptsatz), p. 291: for a non-degenerate $S$ , every $x$ with $(\alpha x) \ge 0$ for all extreme supports $\alpha$ is representable by $S$ .
Zusatz, pp. 294–295: a non-degenerate $S$ has no extreme support iff $0 = \sum_s c_s s$ with all $c_s > 0$ .
Satz 3, p. 296 (Farkas): if $(p\xi) \ge 0$ on all of $(S)$ , then $p$ is a nonnegative combination of $S$ . This milestone is the published platform theorem LinearOptimization.farkas_cone_corollary.
Satz 6, p. 297: for non-degenerate $S$ , $p \in (\Sigma)$ iff $(p\xi) \ge 0$ for all $\xi \in (S)$ .
§3 II, p. 298: for non-degenerate $S$ , every $\pi \in (S)$ is a nonnegative combination of finitely many extreme solutions.
Satz 9, p. 299: if $S$ is non-degenerate and $(S)$ has an inner point, then $\Sigma$ is non-degenerate.
§4 I, p. 301: a convex polyhedron $\operatorname{conv} S$ has an extreme support and equals the set cut out by its extreme supports.

Significance

The result. §4 II gives both directions of the Minkowski–Weyl theorem for full-dimensional polytopes, together with a test on the data $(A, b)$ : positive spanning of the normals is equivalent to boundedness, and a strictly feasible point is equivalent to full dimension. Several parts of LP theory start from this equivalence: finiteness of the vertex set of a bounded feasible region, the existence of an optimal vertex, and the passage between the primal (inequality) and dual (generator) descriptions used in polyhedral combinatorics.

Formalizing it. The theorem has been proved since 1935; the work here is formalization. Mathlib has convex hulls, extreme points, and pointed cones with their duals, but no Minkowski–Weyl theorem for polytopes or for cones. On this platform, Farkas-type lemmas (LinearOptimization.farkas_cone_corollary) and the statement that a nonempty bounded polyhedron is the hull of its extreme points (Bertsimas–Tsitsiklis Thm 2.9) are published. Neither gives the "only if" direction, the positive-spanning criterion, or full-dimensionality.

Difficulty

The "only if" direction and the reduction from a strictly feasible bounded region to cones are routine. The hard step is the finiteness statement: why a finite set of inequalities has only finitely many generators, and why these generate the whole region. Mathlib's compactness results give "a compact convex set is the closed hull of its extreme points" (Krein–Milman). That result does not show that the extreme points are finite in number, nor that there are finitely many of them in a form that can be computed from the inequalities. Weyl's route avoids topology. It goes through the Hauptsatz, proved by induction on dimension, and the duality between $S$ and $\Sigma$ . Each step of that duality needs non-degeneracy, and keeping that hypothesis alive through the dualization (Satz 9) is where care is needed.

Formalization scope

The homogeneous space is Fin n → ℝ, with dot product ⬝ᵥ. Point systems are Finsets; the zero vector is allowed in them. "Representable" is an explicit nonnegative sum over the Finset.
Non-degeneracy is the literal condition " $(\alpha s)=0$ for all $s \in S$ implies $\alpha = 0$ ", not span = ⊤.
Extreme supports and extreme solutions quantify over all vectors with the property. Positive multiples are not identified, and no representatives are chosen.
Extreme solutions are required to be nonzero and to lie in $(S)$ . This is implicit in the paper.
§4 is stated in affine form on Fin m → ℝ, a point $x$ standing for Weyl's $(x,-1)$ . Linear independence of $n-1$ homogenized points becomes affine independence of $m$ points, and non-degeneracy becomes affineSpan ℝ S = ⊤.
A "convex polyhedron" is the hull of a finite set with full affine span. Dropping full-dimensionality would make the "only if" false, since a segment in $\mathbb{R}^2$ has no inner point.
Added hypotheses: no zero row in the goal (Weyl's half-spaces have nonzero normal $(\alpha_1,\dots,\alpha_n)$ , p. 291). Non-degeneracy of $S$ in Satz 6 and in the p. 298 representation, where it is inherited from Satz 4.
Condition (i) of the goal is positive spanning, i.e. nonnegative coefficients. Linear spanning of $\mathbb{R}^m$ would be strictly weaker and would make the statement false.
A trivializing formalization is ruled out: the goal is an equivalence, "convex polyhedron" is an existential over finite point sets with full affine span, and no hypothesis restricts $J$ , $m$ or the data beyond the nonzero rows. For $m = 0$ the statement is true and non-vacuous.
Useful infrastructure, reusable beyond this mission: a Minkowski–Weyl theorem for polyhedral cones in Fin n → ℝ, extreme rays of pointed polyhedral cones, and the homogenization dictionary between cones in $\mathbb{R}^{m+1}$ and polytopes in $\mathbb{R}^m$ . Proofs of any milestone, and alternative routes to the goal (e.g. via Fourier–Motzkin elimination), are welcome.

Selected references

H. Weyl, Elementare Theorie der konvexen Polyeder, Commentarii Mathematici Helvetici (1935), 290–306. https://doi.org/10.1007/bf01292722
H. Weyl, The elementary theory of convex polyhedra, in: H. W. Kuhn, A. W. Tucker (eds.), Contributions to the Theory of Games I, Annals of Mathematics Studies 24, Princeton University Press, 1950.
J. Farkas, Theorie der einfachen Ungleichungen, Journal für die reine und angewandte Mathematik 124 (1902), 1–27. https://doi.org/10.1515/crll.1902.124.1
H. Minkowski, Geometrie der Zahlen, Teubner, Leipzig, 1896/1910.
A. Schrijver, Theory of Linear and Integer Programming, Wiley, 1986, §7.2 (Minkowski–Weyl).

13 thms4 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Robust solutions of Linear Programming problems contaminated with uncertain data: A Violation-Probability Bound for the Robust CounterpartResearch Paper

Motivation

Linear programs solved in practice carry data that are measured, estimated or rounded. Ben-Tal and Nemirovski (Math. Program. 88, 2000) examined the NETLIB collection of real-world LPs and found that in 13 of them a relative perturbation of only 0.01% in the "ugly" coefficients of the inequality constraints can make the nominal optimal solution more than 50% infeasible (§2.3). Their remedy is the robust counterpart methodology: replace the nominal problem by a deterministic problem whose feasible solutions remain nearly feasible for every, or for all but a small probability of, data realizations.

The paper made the approach concrete for entry-wise uncertainty and gave the probabilistic guarantee that became a standard tool of robust and chance-constrained optimization. The main steps of the history are:

1973, A. L. Soyster: the interval (worst-case, "box") counterpart, here called (IRC).
1998–1999, Ben-Tal and Nemirovski (Math. Oper. Res. 23; Oper. Res. Lett. 25), and independently El Ghaoui and co-authors: robust optimization with ellipsoidal uncertainty sets.
2000, this paper: the ellipsoid-plus-box counterpart (RC[ε, δ, Ω]) and Proposition 1, which bounds each constraint's violation probability by $\exp\{-\Omega^2/2\}$ under independent symmetric perturbations.
2004, Bertsimas and Sim (Oper. Res. 52): the budgeted counterpart, with an analogous probability bound.

Setting

An uncertain linear program is

\text{minimize } c^Tx\quad\text{s.t.}\quad Ex=e,\qquad Ax\le b,\qquad \ell\le x\le u,\tag{LP}

with $x\in\mathbb{R}^n$ , $E\in\mathbb{R}^{p\times n}$ , $A=(a_{ij})\in\mathbb{R}^{m\times n}$ , and bounds $\ell_j\in\mathbb{R}\cup\{-\infty\}$ , $u_j\in\mathbb{R}\cup\{+\infty\}$ . For each inequality row $i$ a set $J_i\subseteq\{1,\dots,n\}$ lists the uncertain entries $a_{ij}$ , $j\in J_i$ . Only these entries are uncertain; $E,e,b,\ell,u,c$ are exact.

Given an uncertainty level $\epsilon>0$ and a feasibility tolerance $\delta>0$ , write $b_i^+=b_i+\delta\max[1,|b_i|]$ .

$x$ is reliable if it is feasible for (LP) and $\sum_{j\notin J_i}a_{ij}x_j+\sum_{j\in J_i}\tilde a_{ij}x_j\le b_i^+$ for every $i$ and every choice of $\tilde a_{ij}$ with $|\tilde a_{ij}-a_{ij}|\le\epsilon|a_{ij}|$ .
In the random symmetric uncertainty model, the true coefficients are $\tilde a_{ij}=(1+\epsilon\xi_{ij})a_{ij}$ , where $\xi_{ij}=0$ for $j\notin J_i$ and, for each row $i$ , $\{\xi_{ij}\}_{j\in J_i}$ are independent random variables, each symmetrically distributed in $[-1,1]$ .
$x$ is almost reliable with level $\kappa$ if it is feasible for (LP) and $\Pr\{\sum_j\tilde a_{ij}x_j>b_i^+\}\le\kappa$ for every $i$ .

The robust counterpart (RC[ε, δ, Ω]), with a safety parameter $\Omega>0$ , has variables $x_j$ , $y_{ij}$ , $z_{ij}$ and constraints $Ex=e$ , $Ax\le b$ , $\ell\le x\le u$ , $-y_{ij}\le x_j-z_{ij}\le y_{ij}$ for all $i,j$ , and

\sum_j a_{ij}x_j+\epsilon\Big[\sum_{j\in J_i}|a_{ij}|y_{ij}+\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2z_{ij}^2}\Big]\le b_i^+\qquad\forall i.

The interval robust counterpart (IRC[ε, δ]) has variables $x_j,y_j$ and the constraint $\sum_ja_{ij}x_j+\epsilon\sum_{j\in J_i}|a_{ij}|y_j\le b_i^+$ with $-y_j\le x_j\le y_j$ , besides the nominal ones. Problem (∗) is the same with $y_j$ replaced by $|x_j|$ .

Formalization targets

Goal: Proposition 1 (pp. 418–419)

If $x$ extends to a feasible solution $(x,y,z)$ of (RC[ε, δ, Ω]), then $x$ is feasible for (LP) and, for every $i$ ,

\Pr\Big\{\sum_j(1+\epsilon\xi_{ij})a_{ij}x_j>b_i+\delta\max[1,|b_i|]\Big\}\le\exp\{-\Omega^2/2\}.

Milestones

The reduction in the proof of Proposition 1 (p. 419), in corrected pointwise form: a violation of row $i$ forces $\sum_{j\in J_i}\xi_{ij}a_{ij}z_{ij}>\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2z_{ij}^2}$ .
Eq. (1), p. 419: for independent symmetric $\eta_j\in[-1,1]$ and reals $p_j$ ,

\Pr\Big\{\sum_j\eta_jp_j>\Omega\sqrt{\textstyle\sum_jp_j^2}\Big\}\le\exp\{-\Omega^2/2\}.

$x$ is reliable iff it is feasible for (∗) (p. 417).
(∗) is equivalent to (IRC[ε, δ]) (pp. 417–418).
Every feasible solution of (IRC) yields one of (RC) with $y_{ij}=y_j$ , $z_{ij}=0$ (p. 420).
Feasibility for (LP) together with $\sum_ja_{ij}x_j+\epsilon\beta_i(x)\le b_i^+$ , $\beta_i(x)=\Omega\sqrt{\sum_{j\in J_i}a_{ij}^2x_j^2}$ , suffices to extend $x$ to (RC) (p. 420).
The ratio $\alpha_i(x)/\beta_i(x)$ , $\alpha_i(x)=\sum_{j\in J_i}|a_{ij}||x_j|$ , is at most $\sqrt{\mathrm{card}(J_i)}/\Omega$ , with equality attained (p. 420, corrected).

Significance

Proposition 1 turns a probabilistic requirement, which is hard to handle directly, into a single convex (second-order-cone) program. The bound $\exp\{-\Omega^2/2\}$ does not depend on the dimension, on the number of uncertain entries, or on which symmetric distributions the perturbations follow, so $\Omega$ can be chosen from the desired reliability level alone. Together with milestones 3–6, the mission certifies the whole chain: the worst-case notion of reliability is exactly Soyster's linear program (IRC), and (RC) is never more conservative than (IRC), with an advantage that can reach the factor $\sqrt{\mathrm{card}(J_i)}/\Omega$ .

The results are proved in the paper; to our knowledge none of them is machine-checked. A formal development produces a reusable model of entry-wise uncertain LPs, the counterparts (∗), (IRC) and (RC) as Lean predicates, and a Hoeffding-type bound for weighted sums of symmetric bounded variables in the exact form (1). The platform's HighDimProb.Concentration.hoeffding_rademacher covers the Rademacher special case only.

Difficulty

The deterministic parts (milestones 1, 3–7) are elementary: worst cases of interval perturbations, and the Cauchy–Schwarz inequality. The obstacle lies in the probabilistic step. The printed proof passes from $\xi_{ij}a_{ij}$ to $\xi_{ij}|a_{ij}|$ with an equality that holds only in distribution, and contains index misprints, so it cannot be transcribed line by line; the reduction has to be restated pointwise. Eq. (1) is a tail bound for general symmetric variables in $[-1,1]$ , not only for random signs; the step (c) of the printed proof of (1) is written as an equality that holds only for random signs, so that proof too needs repair. The degenerate case $\sum_jp_j^2=0$ must be handled rather than assumed away.

Formalization scope

Data are a structure UncertainLP n p m over Fin indices (0-based), with A : Matrix (Fin m) (Fin n) ℝ, J : Fin m → Finset (Fin n) arbitrary, and EReal bounds so that infinite bounds are expressible. The objective $c$ is omitted: no statement involves it.
The probability space is $(S,\mathbb P)$ with IsProbabilityMeasure; the name $S$ avoids a clash with the safety parameter $\Omega$ . Symmetry is equality of the laws of $\xi_{ij}$ and $-\xi_{ij}$ ; values lie in $[-1,1]$ at every outcome; independence is required within each row only, with no identical distribution (§3.1 says only "independent", which is weaker than the "iid" of §2.2). Probabilities are P.real.
The hypotheses $\epsilon>0$ , $\delta>0$ , $\Omega>0$ are the paper's standing assumptions and are carried by every theorem that mentions the parameter.
Corrections of the printed text: $a_{ij}x_i\to a_{ij}x_j$ in (IRC); $\sum_{j\in J}\to\sum_{j\in J_i}$ in (RC); the reduction of milestone 1 is stated with $a_{ij}$ and $z_{ij}$ in place of the printed $|a_{ij}|$ , $x_i-y_{ij}$ and $y_j$ , $y_{ij}$ ; and the ratio of milestone 7 carries the factor $1/\Omega$ that the printed " $\sqrt{\mathrm{card}(J_i)}$ " omits.
Ruling out trivializations: the violation event uses the signed multiplicative model $(1+\epsilon\xi_{ij})a_{ij}$ , never $|a_{ij}|$ or an additive perturbation; the goal concludes both nominal feasibility (i) and the probability bound (ii′) for every row; no hypothesis excludes the degenerate case $\sum_{j\in J_i}a_{ij}^2z_{ij}^2=0$ ; and the probability model is satisfiable (e.g. by $\xi\equiv0$ or by Rademacher signs), so the goal is not vacuous.
The numerical remarks of the paper (0.92, 5.24, $10^{-6}$ , "at least 30") and the NETLIB case study are not formalized.
Reusable beyond this mission: the uncertain-LP model and the three counterparts, and the tail bound (1). Contributions of general lemmas about symmetric bounded random variables are welcome.

Selected references

A. Ben-Tal, A. Nemirovski, Robust solutions of Linear Programming problems contaminated with uncertain data, Math. Program. Ser. A 88 (2000) 411–424. https://doi.org/10.1007/s101070000163
A. L. Soyster, Convex programming with set-inclusive constraints and applications to inexact linear programming, Oper. Res. 21 (1973) 1154–1157. https://doi.org/10.1287/opre.21.5.1154
A. Ben-Tal, A. Nemirovski, Robust convex optimization, Math. Oper. Res. 23 (1998) 769–805. https://doi.org/10.1287/moor.23.4.769
A. Ben-Tal, A. Nemirovski, Robust solutions of uncertain linear programs, Oper. Res. Lett. 25 (1999) 1–13. https://doi.org/10.1016/S0167-6377(99)00016-4
D. Bertsimas, M. Sim, The price of robustness, Oper. Res. 52 (2004) 35–53. https://doi.org/10.1287/opre.1030.0065
W. Hoeffding, Probability inequalities for sums of bounded random variables, J. Amer. Statist. Assoc. 58 (1963) 13–30. https://doi.org/10.1080/01621459.1963.10500830

12 thms4 active usersReviewed

Completed

Algorithmic Game Theory Operations Research·Captain: mikedeng1

The Assignment Game I: The Core 2: The High-Price and Low-Price Corners of the CoreResearch Paper

Motivation

A two-sided market in which each seller owns one indivisible good (a house, in the paper's example) and each buyer wants at most one is the simplest model in which prices emerge from bargaining between individuals rather than from a supply curve. Shapley and Shubik, The Assignment Game I: The Core (Int. J. Game Theory 1 (1971)), treat this market as a cooperative game with transferable utility and describe its core, the set of payoff divisions that no group of traders can improve upon by trading among themselves. The paper is the foundation of the literature on assignment markets, auctions of heterogeneous items, and two-sided matching with money.

This mission formalizes the paper's structural result on the shape of the core, Theorem 3 (p. 121): among all core outcomes there is a high-price corner in which every seller simultaneously receives the highest payoff available in the core and every buyer the lowest, and a low-price corner with the roles reversed; these two corners are the farthest-apart pair of core points. The authors note (p. 121, footnote 2) that a similar theorem for markets without money is proved by Gale and Shapley (1962), where it becomes the existence of seller-optimal and buyer-optimal stable matchings.

Setting

Let $M$ be a finite set of sellers and $N$ a finite set of buyers, with $m = |M|$ and $n = |N|$ not necessarily equal. For each seller $i$ and buyer $j$ a number $a_{ij} \ge 0$ is given: the gain the pair can realize by trading (Eq. (2.5), p. 114; Sec. 2.3, p. 116).

A coalition $S \subseteq M \cup N$ is described by its seller part $A = S \cap M$ and buyer part $B = S \cap N$ . A matching inside $(A, B)$ is a set $P \subseteq A \times B$ of seller–buyer pairs in which no player occurs twice. The characteristic function (Eq. (2.6), p. 115) gives the coalition the best total gain it can realize by pairing its members:

\operatorname{worth}(A, B) = \max_{P \text{ matching in } (A,B)} \sum_{(i,j) \in P} a_{ij}.

A matching of the whole market attaining $\operatorname{worth}(M, N)$ is an optimal assignment.

A payoff vector is a pair $(u, v)$ with $u \in \mathbb{R}^M$ (sellers' payoffs) and $v \in \mathbb{R}^N$ (buyers' payoffs). The core (p. 118) consists of the payoff vectors with

\sum_{i \in M} u_i + \sum_{j \in N} v_j = \operatorname{worth}(M, N) \quad (3.5), \qquad \sum_{i \in A} u_i + \sum_{j \in B} v_j \ge \operatorname{worth}(A, B) \ \text{ for all } A \subseteq M,\ B \subseteq N \quad (3.6).

Singleton coalitions have worth $0$ , so core vectors are nonnegative; the paper calls them "imputations in the core".

For a seller $i$ , write $u^*_i$ and $u_{*i}$ for the highest and lowest value of $u_i$ over the core; for a buyer $j$ , write $v^*_j$ and $v_{*j}$ likewise.

Formalization targets

Goal: Theorem 3 (p. 121)

The low-price corner $(u_*, v^*)$ and the high-price corner $(u^*, v_*)$ are in the core, and for all core vectors $(u', v')$ , $(u'', v'')$ ,

\sum_{i \in M} (u'_i - u''_i)^2 + \sum_{j \in N} (v'_j - v''_j)^2 \le \sum_{i \in M} (u_{*i} - u^*_i)^2 + \sum_{j \in N} (v^*_j - v_{*j})^2 .

Milestones, in attack order

Sec. 3.2, p. 118 — the core is nonempty.
Sec. 3.3, p. 120 — the core is closed, convex and bounded (a polytope).
Sec. 3.3, proof of the Lemma, p. 121 — on an optimal assignment $P$ , every core vector has $u_i + v_j = a_{ij}$ for $(i, j) \in P$ and pays $0$ to players $P$ leaves unassigned.
Lemma, p. 121 — for core vectors $(u', v')$ , $(u'', v'')$ , the vectors $(\min(u', u''), \max(v', v''))$ and $(\max(u', u''), \min(v', v''))$ (coordinatewise) are in the core.
Sec. 3.3, p. 122 — any two core vectors satisfy $|u'_i - u''_i| \le u^*_i - u_{*i}$ and $|v'_j - v''_j| \le v^*_j - v_{*j}$ for every $i$ and $j$ .

Milestone 5 is the strongest form of the distance clause of the goal: it gives the same conclusion for every distance that depends only on the absolute values of the coordinate differences, as the paper remarks on p. 122.

Significance

The result. Theorem 3 says that the core of an assignment market is elongated along the direction of market-wide price movements: "intergroup allocations are relatively indeterminate, intragroup allocations are relatively precise" (p. 121). The high-price corner is the outcome most favourable to all sellers at once, and the low-price corner the one most favourable to all buyers; that such simultaneous optima exist is a property of this game, not of cores in general. The low-price corner, the buyers' optimum, is the outcome reached by the ascending multi-item auction of Demange, Gale and Sotomayor (J. Polit. Econ. 94 (1986)), and the lattice structure underlies the incentive analysis of assignment mechanisms.

Formalizing it. The theorem is classical and fully proved in the paper; Prove2Me has no formalization of it, and nothing on the platform treats transferable-utility assignment games (the platform's stable-matching material concerns the non-transferable-utility model). The mission produces a reusable definition of the assignment game and its core, the lattice property of the core, and the extremal-corner theorem, stated with the core's extrema defined intrinsically rather than as parameters.

Difficulty

The proof in the paper takes a finite family of core vectors realizing all the extremal values and applies the Lemma repeatedly (p. 122). That argument presupposes that each extremum $u^*_i$ , $u_{*i}$ , $v^*_j$ , $v_{*j}$ is attained by some core vector, which the paper takes from the core being a nonempty polytope without stating it separately. Nonemptiness is itself the substantive result of the paper's linear-programming analysis (Theorem 2, via the duality theorem and the integrality of the assignment polytope), and it is not available here as a black box. The other nontrivial point is the Lemma's efficiency claim: that the coordinatewise min/max vectors still distribute exactly $\operatorname{worth}(M, N)$ , which depends on the structure of an optimal assignment and fails for the naive combination $(\max(u', u''), \max(v', v''))$ .

Formalization scope

Players and matrix. $M$ and $N$ are arbitrary finite types (Fintype); either may be empty and $m \ne n$ is allowed. The matrix is a : M → N → ℝ, and every theorem carries the paper's standing assumption $a_{ij} \ge 0$ as a hypothesis. No other hypothesis is added.
Coalitions are pairs (A, B) : Finset M × Finset N. Matchings are finsets of pairs with injective projections. The paper maximizes over exactly $k = \min(|S \cap M|, |S \cap N|)$ disjoint pairs; the formalization maximizes over matchings of every size, which gives the same value because $a_{ij} \ge 0$ .
Naming. The characteristic function is worth, since v denotes buyers' payoffs.
Core is a Set ((M → ℝ) × (N → ℝ)) defined by (3.5) and (3.6) over all coalitions, with no separate nonnegativity clause (it follows from singleton coalitions).
Extremal payoffs uHi, uLo, vHi, vLo are sSup/sInf in ℝ of the image of the core under a coordinate. On an empty or unbounded set these return $0$ ; the goal does not assume the core nonempty or bounded, so it is not vacuous and does not hide milestones 1–2 as hypotheses. The goal's membership clauses imply attainment of the extrema.
Distance. The goal uses the Euclidean distance on $\mathbb{R}^M \times \mathbb{R}^N$ through sums of squared coordinate differences. Lean's default dist on a product of function types is the sup-distance and is not used.
Ruled out. A formalization in which $u^*, u_*, v^*, v_*$ are free parameters constrained only by the conclusion, or in which the goal assumes a nonempty bounded core, would trivialize or weaken Theorem 3; the extrema here are computed from the core.
Not formalized. The dimension statements of p. 120 ("typically equal to min(m,n)") are informal. The LP characterization of the core (Theorem 2) is the subject of the companion mission of this series and is not restated.
Welcome contributions. Lemmas about matchings inside coalitions (injectivity, sums over images), the implication "dual feasible $\Rightarrow$ coalitionally rational", and general facts about sSup/sInf of compact coordinate images are reusable for any assignment-market or TU-matching development.

Selected references

L. S. Shapley and M. Shubik, The Assignment Game I: The Core, International Journal of Game Theory 1 (1971), 111–130. https://doi.org/10.1007/BF01753437
D. Gale and L. S. Shapley, College Admissions and the Stability of Marriage, American Mathematical Monthly 69 (1962), 9–15. https://doi.org/10.2307/2312726
G. Demange, D. Gale and M. Sotomayor, Multi-Item Auctions, Journal of Political Economy 94 (1986), 863–872. https://doi.org/10.1086/261393
G. B. Dantzig, Linear Programming and Extensions, Princeton University Press, 1963. https://doi.org/10.1515/9781400884179

7 thms4 active usersReviewed

Completed

Operations Research Optimization·Captain: mikedeng1

A Branch and Bound Algorithm for the Generalized Assignment Problem: The Knapsack Penalty Bound Equals the Lagrangean Bound at Second-Smallest CostsResearch Paper

Motivation

The generalized assignment problem (GAP) asks for the cheapest way to give each of $n$ tasks to exactly one of $m$ agents when every agent has a limited amount of a resource and different agents consume different amounts of it for the same task. It models assigning jobs to machines or computers, software tasks to programmers, commercials to time slots, and customers to single-source plants in capacitated facility location. The problem is NP-hard, so exact methods rely on lower bounds that are cheap to compute and strong enough to prune a branch and bound tree.

G. Terry Ross and Richard M. Soland (Mathematical Programming 8, 1975) gave such a bound. The relaxation that ignores the resource limits is solved by giving every task to its cheapest agent; the overloaded agents are then repaired by one small binary knapsack problem each, whose optimal values are added as penalties. Their paper then shows that this repaired bound is not an ad hoc heuristic: it is exactly the value of a Lagrangean relaxation of the GAP at an explicit choice of multipliers. This identity made the Ross–Soland bound the reference point for the later Lagrangean and column-generation methods for the GAP (for example Fisher, Jaikumar and Van Wassenhove, Management Science 1986 and Savelsbergh, Operations Research 1997).

Setting

Agents are $I=\{1,\dots,m\}$ and tasks $J=\{1,\dots,n\}$ . Giving task $j$ to agent $i$ costs $c_{ij}$ and uses $r_{ij}\ge 0$ units of agent $i$ 's resource; agent $i$ has $b_i>0$ units. The problem is

\text{(P)}\qquad \min\ \sum_{i\in I}\sum_{j\in J}c_{ij}x_{ij}\quad\text{s.t.}\quad\sum_{j\in J}r_{ij}x_{ij}\le b_i\ (i\in I),\quad\sum_{i\in I}x_{ij}=1\ (j\in J),\quad x_{ij}\in\{0,1\}.

Dropping the resource constraints gives the relaxation (PR). It is solved by choosing, for each task $j$ , a cheapest agent $i_j$ with $c_{i_jj}=\min_{i}c_{ij}$ and setting $x_{i_jj}=1$ ; its value is $Z=\sum_jc_{i_jj}$ . Let $J_i=\{j: i_j=i\}$ be the tasks this solution gives to agent $i$ , $I'=\{i:\sum_{j\in J_i}r_{ij}>b_i\}$ the overloaded agents, and $d_i=\sum_{j\in J_i}r_{ij}-b_i$ the excess of agent $i$ . The penalty of moving task $j$ away from $i_j$ is $p_j=\min_{k\ne i_j}(c_{kj}-c_{i_jj})$ . For $i\in I'$ the binary knapsack problem

\text{(PK}_i)\qquad\min\ z_i=\sum_{j\in J_i}p_jy_{ij}\quad\text{s.t.}\quad\sum_{j\in J_i}r_{ij}y_{ij}\ge d_i,\quad y_{ij}\in\{0,1\}

chooses the cheapest set of tasks to move off agent $i$ ; call its optimal value $z^*_i$ . The knapsack bound is

\mathrm{LB}=Z+\sum_{i\in I'}z^*_i .

Dualizing the assignment constraints with multipliers $\lambda_j$ gives the Lagrangean relaxation

\text{(PR}_\lambda)\qquad\min\ \sum_{i\in I}\sum_{j\in J}c_{ij}x_{ij}+\sum_{j\in J}\lambda_j\Bigl(1-\sum_{i\in I}x_{ij}\Bigr)\quad\text{s.t.}\quad\sum_{j\in J}r_{ij}x_{ij}\le b_i\ (i\in I),\quad x_{ij}\in\{0,1\}.

Finally $c_{1j}$ and $c_{2j}$ are the smallest and second smallest of $c_{1j},\dots,c_{mj}$ , counted with multiplicity.

Formalization targets

Goal: the knapsack bound is the Lagrangean bound at $\lambda=c_2$

For every cheapest-agent choice $j\mapsto i_j$ and every choice of optimal knapsack solutions,

\mathrm{LB}=\min\Bigl\{\sum_{i}\sum_{j}c_{ij}x_{ij}+\sum_{j}c_{2j}\Bigl(1-\sum_{i}x_{ij}\Bigr)\ :\ x\ \text{feasible for (PR}_\lambda)\Bigr\},

the minimum being attained, and consequently $\mathrm{LB}\le\sum_i\sum_jc_{ij}x_{ij}$ for every $x$ feasible for (P). This is the paper's "principal result of this Lagrangean analysis" (§2, p. 96). It has no constants to improve; it is an identity between two optimization problems.

Milestones

In the paper's order of use: (PR) is solved by the cheapest agents (pp. 93–94); every lower bound on (PR $_\lambda$ ) is a lower bound on (P) (p. 95); (PR $_\lambda$ ) separates into one binary knapsack per agent (p. 95); at $\lambda=c_2$ the variables that are zero in the (PR) solution can be fixed at zero, the substitution $y_{ij}=1-x_{ij}$ turns agent $i$ 's part into (PK $_i$ ), $p_j=c_{2j}-c_{1j}$ , and agent $i$ 's part has value $-\sum_{j\in J_i}p_j+z^*_i$ (p. 96). Two side results close the section: the solution obtained by moving the tasks the knapsacks select has cost exactly LB, so it is optimal whenever it is feasible (pp. 94–95); and the optimal dual multipliers of the bounded-variable linear program (PR $_L$ ) are exactly the vectors with $c_{1j}\le\lambda_j\le c_{2j}$ (pp. 95–96).

Significance

The identity says that a bound computed from one sorting pass and a handful of small knapsacks equals a Lagrangean dual bound at a closed-form multiplier. Validity of LB for (P) then follows from weak Lagrangean duality alone, and the multiplier $c_2$ is the upper end of the range of optimal dual multipliers of the linear program (PR $_L$ ), which the paper singles out as a suitable choice of multipliers. The rebuilt solution gives the algorithm a feasible incumbent at no extra cost whenever the knapsack repairs happen to respect all budgets.

The result is proved in the paper, in one sentence. The mission turns that sentence into checked statements: the separation of (PR $_\lambda$ ), the reduction of each agent's subproblem to (PK $_i$ ), the handling of ties among cheapest agents, and the role of nonnegative resources. As far as a search of the platform shows, nothing about the generalized assignment problem or its Lagrangean bounds has been formalized; the definitions here (assignment relaxations, per-agent knapsacks, bounded-variable duals) are reusable for other GAP and facility-location missions.

Difficulty

The Lagrangean relaxation at $\lambda=c_2$ is a larger problem than the knapsack bound suggests: a feasible $x$ may give a task to several agents or to none, and may use any agent, not only the cheapest one. The knapsack bound, by contrast, only looks at the tasks each agent receives in the (PR) solution. The paper bridges the two in one sentence of three observations, and each observation depends on a condition the sentence does not state: the sign of the resource coefficients, the treatment of agents that are not overloaded (for which no knapsack is solved), and ties among cheapest agents, which make some penalties zero and require the statement to hold for every tie-break. An inequality in one direction only (LB is a valid bound) is not the claim; the equality needs a feasible point of (PR $_\lambda$ ) whose value is exactly LB.

Formalization scope

Agents are Fin m and tasks Fin n, indexed from 0. Costs, resources, budgets, multipliers and variables are real numbers; a 0-1 variable is a real equal to 0 or 1, so the paper's sums are literal. The cheapest-agent selection is an arbitrary function a : Fin n → Fin m with IsCheapest c a, so every statement holds for every tie-break. $p_j$ and $c_{2j}$ are minima over the other agents, which requires $m\ge2$ (hm : 1 < m); $c_{2j}$ is proved to be the second smallest cost with multiplicity. Optimal values are never encoded as sInf: $z^*_i$ is the objective of a given optimal knapsack solution, and "the bound provided by (PR $_\lambda$ )" is stated as a lower bound over all feasible points that is attained.

Standing hypotheses: $b_i>0$ (printed on p. 92), $r_{ij}\ge0$ (implicit in "the resource required", and necessary: with a negative $r_{ij}$ both (PR $_\lambda$ ) and (P) can fall below LB), and $m\ge2$ . All costs are finite; the "not permissible" pairs of the paper's numerical example are outside the model.

A formalization that states only $\mathrm{LB}\le$ every (PR $_\lambda$ ) value, or that restricts the (PR $_\lambda$ ) competitors to the (PR) support or to at most one agent per task, would be a weaker theorem and does not meet the goal. The (PR $_L$ ) dual is written out explicitly with multipliers $u_{ij}\ge0$ for the bounds $x_{ij}\le1$ ; "each optimal dual multiplier lies anywhere in the range $c_{1j}\le\lambda_j\le c_{2j}$ " is read as "the optimal multipliers are exactly this box".

Needed infrastructure is only finite sums over Fin and Finset.inf'. Proofs of the milestones, and lemmas on separable binary programs that could serve other Lagrangean-relaxation missions, are welcome.

Selected references

G. T. Ross and R. M. Soland, A branch and bound algorithm for the generalized assignment problem, Mathematical Programming 8 (1975) 91–103. https://doi.org/10.1007/BF01580430
A. M. Geoffrion, Lagrangean relaxation for integer programming, Mathematical Programming Study 2 (1974) 82–114. https://doi.org/10.1007/BFb0120690
M. L. Fisher, R. Jaikumar and L. N. Van Wassenhove, A multiplier adjustment method for the generalized assignment problem, Management Science 32 (1986) 1095–1103. https://doi.org/10.1287/mnsc.32.9.1095
M. Savelsbergh, A branch-and-price algorithm for the generalized assignment problem, Operations Research 45 (1997) 831–841. https://doi.org/10.1287/opre.45.6.831

10 thms4 active usersReviewed

Completed

Convex Optimization Operations Research Optimization·Captain: mikedeng1

On Polyhedral Approximations of the Second-Order Cone I: A Compact Polyhedral Approximation of the Lorentz ConeResearch Paper

Motivation

Conic quadratic programs (second-order cone programs) minimize a linear objective subject to linear constraints and constraints of the form $\|A_\ell x-b_\ell\|_2\le c_\ell^Tx-d_\ell$ . They model robust linear programs with ellipsoidal uncertainty, truss topology design, contact problems with Coulomb friction, and convex quadratically constrained quadratic programs. In theory they are no harder than linear programs of the same size; in practice, linear programming software handles far larger instances than conic quadratic solvers did at the time of writing (Ben-Tal & Nemirovski 2001, pp. 193–195). This raises a question about geometry rather than algorithms: can a second-order cone be replaced by a polyhedral cone of moderate size without losing much accuracy?

The obvious answer — circumscribe the cone by a polyhedral cone with many facets — fails: the number of facets must grow exponentially in the dimension, even for constant accuracy. Ben-Tal and Nemirovski showed that auxiliary variables change the picture completely: a projection of a polyhedral cone can approximate the Lorentz cone with size only $O(k\ln(1/\varepsilon))$ . The construction is now standard; it underlies, for instance, the lifted linear-programming branch-and-bound algorithm for mixed-integer conic quadratic programs of Vielma, Ahmed & Nemhauser 2008.

Setting

For $y\in\mathbb R^k$ let $\|y\|_2=\sqrt{y_1^2+\dots+y_k^2}$ . The $(k+1)$ -dimensional Lorentz cone is

L^k=\{(y,t)\in\mathbb R^k\times\mathbb R\mid t\ge\|y\|_2\}.

Fix $\varepsilon>0$ . A polyhedral $\varepsilon$ -approximation of $L^k$ is a linear map

\Pi(y,t,u):\mathbb R^k\times\mathbb R\times\mathbb R^{p}\to\mathbb R^{q}

such that

if $(y,t)\in L^k$ , there is $u\in\mathbb R^p$ with $\Pi(y,t,u)\ge0$ (componentwise);
if $\Pi(y,t,u)\ge0$ for some $u$ , then $\|y\|_2\le(1+\varepsilon)t$ .

Equivalently, the polyhedral cone $\{(y,t,u)\mid\Pi(y,t,u)\ge0\}$ projects onto a cone lying between $L^k$ and its $(1+\varepsilon)$ -extension. The size of the approximation is $p+q$ : the number of auxiliary variables plus the number of linear inequalities (an equation counts as two).

The construction in the paper uses a tower of variables: for $k=2^\theta$ , the coordinates $y_1,\dots,y_k$ form generation $0$ , each consecutive pair of generation $\ell-1$ has a successor in generation $\ell$ ( $y_i^\ell$ has parents $y_{2i-1}^{\ell-1},y_{2i}^{\ell-1}$ ), and the single variable of generation $\theta$ is $t$ . It also uses an explicit linear system (8) in variables $\xi^j,\eta^j$ , $j=0,\dots,\nu$ , with trigonometric coefficients $\cos(\pi/2^{j+1})$ , $\sin(\pi/2^{j+1})$ , $\tan(\pi/2^{\nu+1})$ , whose accuracy is $\delta(\nu)=1/\cos(\pi/2^{\nu+1})-1$ .

Formalization targets

Goal: Theorem 1.1

There is an absolute constant $C$ such that for every positive integer $k$ and every $\varepsilon\in(0,1]$ , $L^k$ admits a polyhedral $\varepsilon$ -approximation with

p_k+q_k\le C\,k\ln\frac{2}{\varepsilon}.

The constant is not fixed; the goal asserts only the order of growth, which is what the paper claims.

Milestones

§2, Eq. (5). For $k=2^\theta$ , $\theta\ge1$ : $(y,t)$ extends to a tower solving $\sqrt{[y_{2i-1}^{\ell-1}]^2+[y_{2i}^{\ell-1}]^2}\le y_i^\ell$ for all $i,\ell$ if and only if $\|y\|_2\le t$ .
§2, Eqs. (6)–(7). Placing polyhedral $\varepsilon_\ell$ -approximations of $L^2$ on every level of the tower yields a polyhedral approximation of $L^k$ with $1+\varepsilon=\prod_{\ell=1}^\theta(1+\varepsilon_\ell)$ .
Proposition 2.1 (i), (ii) and Eq. (9). System (8) is a polyhedral $\delta(\nu)$ -approximation of $L^2$ , and $\delta(\nu)=O(4^{-\nu})$ .
Proof of Theorem 1.1, system (10), property 3. System (8) with parameter $\nu_\ell$ on level $\ell$ of the tower approximates $L^{2^\theta}$ with quality $\beta=\prod_{\ell=1}^\theta 1/\cos(\pi/2^{\nu_\ell+1})-1$ .
Proof of Theorem 1.1, choice of $\nu_\ell$ . With $\nu_\ell=\lfloor c\,\ell\ln(2/\varepsilon)\rfloor$ : $\beta\le\varepsilon$ and $\sum_\ell 2^{\theta-\ell}\nu_\ell\le C\,2^\theta\ln(2/\varepsilon)$ .

Significance

The theorem shows that conic quadratic constraints are, up to a factor logarithmic in the accuracy, no more expensive to express as linear constraints than they are in their native form. Consequences listed in the paper include approximating convex quadratically constrained quadratic programs, robust counterparts of linear programs with ellipsoidal uncertainty, and problems with low-dimensional cones (Coulomb friction, $k\le3$ ; truss design, $k\le2$ ) by linear programs of comparable size. Together with the matching lower bound of §3 of the same paper (a separate mission of this series), it pins down the size of the best polyhedral approximation up to constants. The recursive halving of dimensions through the tower of 3-dimensional cones is a reusable device for other rotation-invariant cones.

The result is proved in the paper; as far as is known it has not been machine-checked. This mission produces a formal proof of the construction, including the trigonometric estimate $\delta(\nu)=O(4^{-\nu})$ and the explicit linear encoding with its size count. Explicit values of the absolute constants are welcome as additional results.

Difficulty

The planar estimate is the core. Part (ii) of Proposition 2.1 must hold for every solution of the inequality system (8), not only for the solution one would write down for a given point of $L^2$ ; an argument that tracks only the intended solution proves part (i) and nothing about part (ii). The accuracy must also come out as $1/\cos(\pi/2^{\nu+1})-1$ , geometric in $\nu$ ; a bound that decays only polynomially in $\nu$ would give size $\mathrm{poly}(1/\varepsilon)$ instead of $\ln(1/\varepsilon)$ . The naive idea of approximating $L^k$ directly by tangent hyperplanes is ruled out by the exponential facet count mentioned above; the auxiliary variables are indispensable. The second difficulty is bookkeeping: packaging $k-1$ copies of system (8) on a tower of depth $\theta=\log_2 k$ into a single linear map, counting its variables and inequalities exactly, handling $k$ that is not a power of two, and summing the accuracies so that the total size is $O(k\ln(2/\varepsilon))$ rather than $O(k\ln k\ln(1/\varepsilon))$ .

Formalization scope

Vectors of $\mathbb R^k$ are Fin k → ℝ. The norm $\|y\|_2$ is written out as eucNorm y = Real.sqrt (∑ i, y i ^ 2); the norm Mathlib attaches to Fin k → ℝ is the sup norm, under which the cone would be polyhedral and the theorem trivial.
A polyhedral approximation is an $\mathbb R$ -linear map (Fin k → ℝ) × ℝ × (Fin p → ℝ) →ₗ[ℝ] (Fin q → ℝ) and $\ge0$ is the componentwise order. Linearity is essential: with an arbitrary map, $\Pi(y,t)=t-\|y\|_2$ would be an exact approximation with $p=0$ , $q=1$ . Affine maps are not allowed either; the paper's approximations are homogeneous.
The paper's absolute constants $O(1)$ are existential constants quantified before $k$ , $\varepsilon$ and $\theta$ . The goal requires $k\ge1$ and $\varepsilon\in(0,1]$ , as in the paper; $\ln$ is Real.log.
System (8) and system (10) are stated as propositions with the absolute values written out; their parameters $\nu$ , $\nu_\ell$ are required to be positive integers, as in the paper (at $\nu=0$ the coefficient $\tan(\pi/2)$ would be evaluated as $0$ by Lean).
Tower variables are indexed Y ℓ i with 0-based i, so the parents of Y ℓ i are Y (ℓ-1) (2i) and Y (ℓ-1) (2i+1); the milestones on (6)–(7) and (10) are stated on solution sets rather than on an explicit linear map. The size counts of (10) (properties 1–2) are not separate milestones; the arithmetic milestone on $\nu_\ell$ records the bound on $\sum_\ell 2^{\theta-\ell}\nu_\ell$ to which they reduce.
$\delta(\nu)=O(1/4^\nu)$ is stated as $\exists C>0,\ \forall\nu\ge1,\ \delta(\nu)\le C/4^\nu$ .

A complete development needs: elementary trigonometry of $\pi/2^{j}$ (available in Mathlib), rotations in the plane, finite products and sums over $\{1,\dots,\theta\}$ , and a way to assemble many small linear systems into one linear map with an exact count of rows and columns. The last piece, and the tower of variables with the reduction from arbitrary $k$ to a power of two, are reusable for other lifted polyhedral approximations. Contributions of any milestone, of explicit linear encodings of (8) and (10), and of the extension from $k=2^\theta$ to all $k$ are welcome.

Selected references

A. Ben-Tal and A. Nemirovski, On Polyhedral Approximations of the Second-Order Cone, Mathematics of Operations Research 26(2):193–205, 2001. https://doi.org/10.1287/moor.26.2.193.10561
J. P. Vielma, S. Ahmed and G. L. Nemhauser, A lifted linear programming branch-and-bound algorithm for mixed-integer conic quadratic programs, INFORMS Journal on Computing 20(3):438–450, 2008. https://doi.org/10.1287/ijoc.1070.0256
A. Ben-Tal and A. Nemirovski, Robust convex optimization, Mathematics of Operations Research 23(4):769–805, 1998. https://doi.org/10.1287/moor.23.4.769
A. Ben-Tal and A. Nemirovski, Lectures on Modern Convex Optimization, SIAM, 2001. https://doi.org/10.1137/1.9780898718829

13 thms4 active usersReviewed

Completed

Convex Optimization Operations Research Optimization+1·Captain: mikedeng1

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

Motivation

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

Setting

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

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

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

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

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

Formalization targets

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

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

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

Supporting milestones

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

Significance

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

Difficulty

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

Formalization scope

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

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

Selected references

J.R. Birge and F. Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer Series in Operations Research and Financial Engineering, Springer, 2011. https://doi.org/10.1007/978-1-4614-0237-4
R.J-B. Wets, "Programming Under Uncertainty: The Equivalent Convex Program," SIAM Journal on Applied Mathematics 14 (1966), 89-105 (Lipschitz continuity of the recourse function, cited by the book as Wets [1972] for the closely related result used in Theorem 6). https://doi.org/10.1137/0114008
D.P. Walkup and R.J-B. Wets, "Stochastic Programs with Recourse," SIAM Journal on Applied Mathematics 15 (1967), 1299-1314 (finiteness of the recourse function and coincidence of the possibility and expectation feasibility sets, underlying Proposition 3 and Theorem 4). https://doi.org/10.1137/0115113

8 thms4 active usersReviewed

Completed

Optimization Theoretical Computer Science·Captain: moutei

Primal-Dual Online Algorithms II: Finite LP Duality and Complementary SlacknessTextbook

Motivation

Almost every competitive online algorithm built by the primal-dual method rests on the same two facts about a pair of linear programs. The first is weak duality: any feasible solution of the dual is a lower bound on any feasible solution of the primal. The second is complementary slackness: if a feasible primal-dual pair satisfies a local, per-coordinate tightness condition, the pair is optimal — and if it satisfies that condition only up to factors $\alpha$ and $\beta$ , the primal is within $\alpha\beta$ of optimal.

The second fact in its approximate form is the engine of the whole method. An online algorithm cannot compute an optimum; what it can do is maintain a primal solution and a dual solution side by side so that each new request preserves an approximate tightness invariant. The approximate complementary slackness theorem then converts that local invariant into a global competitive ratio, with no reference to the optimum at all. Chapter 2 of Buchbinder's thesis states it as the background result on which the rest of the work is built.

Setting

Fix finite index types $I$ (primal variables) and $J$ (primal constraints), a matrix $A : I \times J \to \mathbb{R}$ , a cost vector $c : I \to \mathbb{R}$ and a right-hand side $b : J \to \mathbb{R}$ . The covering primal and packing dual are

(P)\quad \min \sum_{i} c_i x_i \ \text{ s.t. } \ \sum_{i} A_{ij} x_i \ \ge\ b_j \ \ (\forall j), \qquad x \ge 0,

(D)\quad \max \sum_{j} b_j y_j \ \text{ s.t. } \ \sum_{j} A_{ij} y_j \ \le\ c_i \ \ (\forall i), \qquad y \ge 0.

Note the index convention: $A_{ij}$ carries the primal-variable index first, so the primal constraint indexed by $j$ sums over $i$ and the dual constraint indexed by $i$ sums over $j$ .

Given $\alpha, \beta \ge 1$ , the pair $(x,y)$ satisfies approximate complementary slackness when

primal side: for every $i$ with $x_i > 0$ , $\quad c_i/\alpha \ \le\ \sum_j A_{ij} y_j \ \le\ c_i$ ;
dual side: for every $j$ with $y_j > 0$ , $\quad b_j \ \le\ \sum_i A_{ij} x_i \ \le\ \beta\, b_j$ .

Formalization targets

Goal — approximate complementary slackness

For a primal-feasible $x$ , a dual-feasible $y$ , and $\alpha,\beta \ge 1$ satisfying the two conditions above,

\sum_{i} c_i x_i \ \le\ \alpha\beta \sum_{j} b_j y_j .

Taking $\alpha = \beta = 1$ recovers exact complementary slackness and hence optimality of both members of the pair. The goal is stated with the source's hypotheses, including the two-sided bounds, rather than the weakest hypotheses that make the inequality go through; a separate item records the minimal-hypothesis strengthening.

Weak duality

\sum_j b_j y_j \ \le\ \sum_i c_i x_i \quad \text{for every feasible } x \text{ and } y,

with no nonnegativity assumption on $A$ , $b$ or $c$ beyond feasibility itself.

Strong duality — imported, not reproved

Strong duality is not proved in this mission. The platform already carries LinearOptimization.lp_strong_duality, proved in this exact environment, for linear programs in Bertsimas–Tsitsiklis general form over Fin-indexed data. This mission's contribution is an adapter: from a primal optimum of $(P)$ , produce a dual optimum of $(D)$ of equal value, for Fin-indexed instances. Reference items point at the imported theorem, its dual construction, and the dual-of-dual identity.

The biconditional — a dual optimum exists if and only if a primal optimum does — is deliberately left open. Weak duality does not derive the existence of a primal optimum from the existence of a dual one; the reverse implication needs strong duality applied to the dual program together with the dual-of-dual identity, and that reduction is not yet compiled. It is offered as a parallel target rather than claimed as established.

Significance

This mission is the foundation of the series. Every later mission — set cover, ski rental, and the online covering and packing problems that follow — states its approximation or competitiveness result as an instance of approximate complementary slackness. Formalizing it once, over arbitrary finite index types, is what makes the later missions short.

It also fills a real gap. Mathlib currently has no linear-programming duality: four separate attempts were closed unmerged. Approximate $(\alpha,\beta)$ complementary slackness appears not to be formalized in any public library, so the goal theorem is, as far as we can determine, first of its kind.

Difficulty

The goal is a summation argument, not a deep theorem: the work is in handling the per-coordinate case split on $x_i > 0$ versus $x_i = 0$ and in interchanging a double sum. Three mechanical milestones isolate exactly those steps. The strong-duality adapter is the hard item, because it must reconcile two different presentations of the same program — index types, matrix orientation, and bundling all differ between our definitions and the imported theorem's.

Formalization scope

Definitions cover §2.1 of the source. Four distinct notions of "the program has a finite optimum" are separated on purpose — attained optimum, nonempty feasible set, bounded objective, and the conjunction — because the source's informal word "bounded" conflates them. The definitions are stated over arbitrary finite index types; the strong-duality items are stated only for Fin, because that is the only index type for which the imported dependency path exists.

Selected references

Niv Buchbinder, Designing Competitive Online Algorithms via a Primal-Dual Approach, PhD thesis, Tel Aviv University, 2008, §2.1, pp. 7–9. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf
Dimitris Bertsimas and John N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 — the general form used by the imported strong-duality theorem.

11 thms4 active usersReviewed

Completed

Operations Research Optimization·Captain: Shuze Chen

Introduction to Linear Optimization XIII: Lagrangean Duality and Integer ProgrammingTextbook

Linear programming has a complete duality theory; integer programming does not — and the Lagrangean dual measures exactly how far duality reaches. This mission formalizes the duality theory of integer programming from Section 11.4 of Bertsimas–Tsitsiklis, built on the general linear programming duality of Section 4.10. For the integer program

Z_{IP} = \min\{c'x : Ax \ge b,\ Dx \ge d,\ x \text{ integer}\}

with integer data, the complicating constraints $Ax \ge b$ are dualized with multipliers $p \ge 0$ over the tractable set $X = \{x \text{ integer} \mid Dx \ge d\}$ : the dual function is

Z(p) = \min_{x \in X}\big(c'x + p'(b - Ax)\big)

and the Lagrangean dual is $Z_D = \max_{p \ge 0} Z(p)$ . Weak duality $Z_D \le Z_{IP}$ (Theorem 11.2) always holds, but strong duality can fail. The convex hull $CH(X)$ of the integer points of a polyhedron with integer data is itself a polyhedron (Theorem 11.3, Meyer's theorem), and the capstone — Theorem 11.4, the central result of Section 11.4 — identifies the Lagrangean dual exactly: $Z_D$ equals the optimal cost of the linear program

\min\{c'x : Ax \ge b,\ x \in CH(X)\}

. This is the geometric explanation of the strength of Lagrangean relaxation, yields the bound ordering $Z_{LP} \le Z_D \le Z_{IP}$ , and Corollary 11.1 characterizes exactly when the bounds collapse. The polyhedral engine is the general weak/strong duality pair (Theorems 4.17/4.18) over a primal $\min c'x$ s.t. $Ax \ge b$ , $x \in P = \{x \mid Dx \ge d\}$ , and the formulation-strength comparison $P_{sub} \subseteq P_{cut}$ of Theorem 10.1 supplies the motivating principle that tighter relaxations of the same integer set give sharper bounds.

18 thms4 active usersReviewed

Completed

Operations Research Optimization·Captain: Shuze Chen

Introduction to Linear Optimization VII: Cones, Extreme Rays, and the Resolution TheoremTextbook

How can an unbounded polyhedron be described by finitely many geometric objects? Sections 4.8-4.9 of Bertsimas-Tsitsiklis build the cone machinery: recession cones $\{d \mid Ad \ge 0\}$ and their rays, extreme rays (defined, like basic solutions, by $n-1$ linearly independent active constraints), the pointedness criterion (Theorem 4.12: $0$ is an extreme point of a polyhedral cone iff the cone contains no line iff $n$ of the constraint vectors are linearly independent), and the characterization of unbounded linear programs (Theorems 4.13-4.14: over a pointed polyhedral cone, and then over any polyhedron with an extreme point, the optimal cost is $-\infty$ iff some extreme ray $d$ has $c'd < 0$ ). The capstone is the resolution theorem (Theorem 4.15): a nonempty polyhedron $P$ with at least one extreme point equals $Q = \{\sum_i \lambda_i x^i + \sum_j \theta_j w^j \mid \lambda_i \ge 0, \theta_j \ge 0, \sum_i \lambda_i = 1\}$ — the convex hull of its extreme points plus the cone generated by a complete set of its extreme rays. It specializes to Theorem 2.9 / Corollary 4.4 (a nonempty bounded polyhedron is the convex hull of its extreme points) and Corollary 4.5 (a pointed polyhedral cone is generated by its extreme rays). The converse, Theorem 4.16, states that every finitely generated set is a polyhedron — in particular the convex hull of finitely many vectors is a polyhedron. Together these form the Minkowski-Weyl equivalence of the two representations of polyhedra, verified absent from Mathlib and the genuine content of this mission.

21 thms4 active usersReviewed

Machine Learning Probability Statistics·Captain: mikedeng1

The Dantzig Selector: Statistical Estimation When p Is Much Larger than n 2: Oracle Inequality within a Logarithmic Factor of the Ideal Mean Squared ErrorResearch Paper

Motivation

Many regression problems have far more unknown coefficients $p$ than observations $n$ : gene expression studies with tens of samples and thousands of genes, imaging from few measurements, nonparametric curve recovery from a finite number of noisy samples. Estimation is hopeless in general, but becomes possible when the parameter is sparse, that is, has few nonzero entries. Candès and Tao (arXiv:math/0506081; Ann. Statist. 35(6), 2007, doi:10.1214/009053606000001523) proposed the Dantzig selector, an estimator computed by a single linear program, and showed that its squared error is within a logarithmic factor of what an oracle that knew which coefficients matter could achieve.

The estimator became one of the two standard $\ell_1$ methods for high-dimensional regression, alongside the Lasso; the comparison of the two by Bickel, Ritov and Tsybakov (arXiv:0801.1095, 2009) is built on it. This mission targets the paper's main result, the oracle inequality (Theorem 1.2). A companion mission covers the simpler $\ell_2$ bound for sparse parameters (Theorem 1.1).

Setting

Observations follow the linear model

y = X\beta + z,

where $X\in\mathbb R^{n\times p}$ is a deterministic design matrix with columns $X_1,\dots,X_p$ , each of Euclidean norm $\|X_j\|_{\ell_2}=1$ ; $\beta\in\mathbb R^p$ is an unknown deterministic parameter; and $z=(z_1,\dots,z_n)$ has independent $N(0,\sigma^2)$ coordinates, $\sigma>0$ . The vector $\beta$ is $S$ -sparse if at most $S$ of its entries are nonzero.

Two constants of $X$ measure how close sparse sets of columns are to being orthonormal. The restricted isometry constant $\delta_S$ is the smallest $\delta\ge0$ such that $(1-\delta)\|c\|_{\ell_2}^2\le\|Xc\|_{\ell_2}^2\le(1+\delta)\|c\|_{\ell_2}^2$ for every $c$ supported on at most $S$ indices. The restricted orthogonality constant $\theta_{S,S'}$ (defined for $S+S'\le p$ ) is the smallest $\theta\ge0$ with $|\langle Xc,Xc'\rangle|\le\theta\|c\|_{\ell_2}\|c'\|_{\ell_2}$ whenever $c,c'$ are supported on disjoint sets of sizes at most $S$ and $S'$ . Below $\delta:=\delta_{2S}$ and $\theta:=\theta_{S,2S}$ .

For a tuning level $\lambda_p>0$ , a Dantzig selector $\hat\beta$ is any solution of

\min_{\tilde\beta\in\mathbb R^p}\|\tilde\beta\|_{\ell_1}\quad\text{subject to}\quad\|X^*(y-X\tilde\beta)\|_{\ell_\infty}=\sup_{1\le j\le p}|\langle y-X\tilde\beta,X_j\rangle|\le\lambda_p\sigma .

The ideal mean squared error is $\sum_{i=1}^p\min(\beta_i^2,\sigma^2)$ : the risk of an oracle that keeps exactly the coordinates above the noise level.

Formalization targets

Goal: Theorem 1.2 (pp. 8–9)

Let $t>0$ , $a\ge0$ , and $\lambda_p:=(\sqrt{1+a}+t^{-1})\sqrt{2\log p}$ . If $\beta$ is $S$ -sparse and $\delta_{2S}+\theta_{S,2S}<1-t$ , then with probability exceeding $1-(\sqrt{\pi\log p}\cdot p^a)^{-1}$ every Dantzig selector obeys

\|\hat\beta-\beta\|_{\ell_2}^2\le C_2^2\cdot\lambda_p^2\cdot\Big(\sigma^2+\sum_{i=1}^p\min(\beta_i^2,\sigma^2)\Big),

with the explicit constant (1.14)

C_2=\frac{2C_0}{1-\delta-\theta}+\frac{2\theta(1+\delta)}{(1-\delta-\theta)^2}+\frac{1+\delta}{1-\delta-\theta},\qquad C_0=2\sqrt2\Big(1+\frac{1-\delta^2}{1-\delta-\theta}\Big)+\Big(1+\frac1{\sqrt2}\Big)\frac{(1+\delta)^2}{1-\delta-\theta}.

Milestones

Lemma 3.2: $\|X\beta\|_{\ell_2}\le\sqrt{1+\delta}\,(\|\beta\|_{\ell_2}+(2S)^{-1/2}\|\beta\|_{\ell_1})$ for every $\beta$ .
Lemma A.1 (dual sparse reconstruction, $\ell_2$ version): for $c$ supported on $|T|\le2S$ , a vector $\beta$ on $T$ whose correlations $\langle X\beta,X_j\rangle$ equal $c_j$ on $T$ and are small off $T$ except on an exceptional set of size at most $S$ , with bounds (6.1)–(6.6).
Corollary A.2 ( $\ell_\infty$ version): the same without exceptional set, constants $1/(1-\delta-\theta)$ .
Corollary A.3 (constrained thresholding): an $S$ -sparse $\beta$ with $\|\beta\|_{\ell_2}<\lambda\sqrt S$ splits as $\beta'+\beta''$ with $\beta'$ small in $\ell_2$ and $\ell_1$ and $\|X^*X\beta''\|_{\ell_\infty}<\frac{1-\delta^2}{1-\delta-\theta}\lambda$ .
Gaussian tail bound (Section 3, p. 15): $P(\sup_j|\langle z,X_j\rangle|>u)\le2p\,\varphi(u)/u$ for standard Gaussian noise.
Lemma 3.1: the $\ell_2$ mass of $h$ on $T_0$ and its top $S$ positions outside $T_0$ is controlled by $\|X^T_{T_{01}}Xh\|_{\ell_2}$ and $\|h\|_{\ell_1(T_0^c)}$ .

Significance

The result. Theorem 1.2 says that a single linear program, which knows neither the support of $\beta$ nor which coefficients exceed the noise, matches the oracle risk $\sum_i\min(\beta_i^2,\sigma^2)$ up to a factor $O(\log p)$ , uniformly over $S$ -sparse parameters and with explicit, nonasymptotic constants. For coefficients well below the noise level it is far sharper than the $\sigma^2 S\log p$ bound of Theorem 1.1. It is the template for later oracle inequalities for $\ell_1$ -penalized estimators under restricted isometry or restricted eigenvalue conditions.

Formalizing it. The theorem is proved in the paper, but parts of the argument are only sketched: Corollary A.2 refers to the 2005 Decoding by Linear Programming paper for its convergence argument, and Corollary A.3's $\ell_1$ bound is printed with a constant its own proof does not deliver. A machine-checked proof settles these steps. The restricted isometry and orthogonality constants used here are already published on the platform from the decoding series; the appendix lemmas on dual vectors are reusable for any compressed-sensing result in that framework. No formalization of the Dantzig selector's oracle inequality is known to us.

Difficulty

The natural proof compares $\hat\beta$ with the hard-thresholded parameter $\beta^{(1)}$ that keeps only the large coefficients: if $\beta^{(1)}$ were feasible for the Dantzig constraint, the analysis of Theorem 1.1 would apply directly. It is not feasible in general, because the small coefficients $\beta^{(2)}$ , though individually below the noise level, can add up to a large correlation $X^*X\beta^{(2)}$ . The central difficulty is to split $\beta^{(2)}$ into a part with controlled $\ell_1$ and $\ell_2$ norm and a part invisible to the constraint; this requires constructing dual vectors with prescribed correlations (Lemma A.1, Corollary A.2), via an iterative, geometrically convergent correction. The probabilistic part is a Gaussian tail estimate plus a union bound, and the bookkeeping of constants must be carried through exactly.

Formalization scope

Vectors are functions Fin p → ℝ, the design is Matrix (Fin n) (Fin p) ℝ, and the noise is a family z : Fin n → Ω → ℝ of mutually independent random variables (iIndepFun) each with law gaussianReal 0 σ². $\delta_{2S}$ and $\theta_{S,2S}$ are the published CandesTao.Decoding.restrictedIsometryConst X (2*S) and restrictedOrthogonalityConst X S (2*S) (infima, absolute value in the orthogonality condition). Domain: $S\ge1$ and $3S\le p$ (the paper defines $\theta_{S,S'}$ for $S+S'\le p$ ), which forces $p\ge3$ and $\log p>0$ . A Dantzig selector is any $\ell_1$ minimizer over the feasible set; the $\ell_\infty$ constraint is a bound on every coordinate.

The goal bounds from above the (outer) probability of the bad event "no Dantzig selector exists, or some Dantzig selector violates (1.13)". Because the event includes non-existence, a definition no vector satisfies cannot make the theorem vacuous; and the constant $C_2$ is the printed (1.14), evaluated at $\delta_{2S}$ , $\theta_{S,2S}$ of $X$ , not a free constant chosen after the fact.

Corrected constant: Corollary A.3 is stated with $\|\beta'\|_{\ell_1}\le2\frac{1+\delta}{1-\delta-\theta}\|\beta\|_{\ell_2}^2/\lambda$ , the bound its proof gives once Corollary A.2 is applied at an integer sparsity level; the printed statement omits the factor $2$ . Corollary A.2 carries Lemma A.1's standing hypothesis $\delta+\theta<1$ . The deterministic lemmas (3.1, 3.2, A.1–A.3) assume nothing about column norms, since their statements do not need it.

Useful infrastructure: monotonicity of $\delta_S$ and $\theta_{S,S'}$ in their indices (the proof applies the lemmas at a smaller sparsity level), the Gaussian tail bound $1-\Phi(u)<\varphi(u)/u$ , existence of minimizers of the Dantzig linear program, and a sorting/blocking toolkit for "the $S$ largest positions". Proofs of individual milestones are welcome independently.

Selected references

E. Candès and T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6):2313–2351, 2007. arXiv:math/0506081v3, doi:10.1214/009053606000001523
E. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51(12):4203–4215, 2005. arXiv:math/0502327, doi:10.1109/TIT.2005.858979
P. Bickel, Y. Ritov and A. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4):1705–1732, 2009. arXiv:0801.1095, doi:10.1214/08-AOS620
D. Donoho and I. Johnstone, Ideal spatial adaptation by wavelet shrinkage, Biometrika 81(3):425–455, 1994. doi:10.1093/biomet/81.3.425

11 thms3 active usersReviewed

Dynamic Programming Markov Chain Operations Research·Captain: mikedeng1

On Sequential Decisions and Markov Chains 2: Under Irreducibility, an Optimal Solution of a Linear Program over State-Action Frequencies Yields an Optimal Stationary ProcedureResearch Paper

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

11 thms3 active usersReviewed

Machine Learning Probability Statistics·Captain: mikedeng1

The Dantzig Selector: Statistical Estimation When p Is Much Larger than n 1: ℓ2 Error Bound for Sparse Parameters under the Uniform Uncertainty PrincipleResearch Paper

Motivation

In many statistical applications the number of unknown parameters $p$ is far larger than the number of observations $n$ : gene-expression studies with tens of samples and thousands of genes, imaging problems with fewer measurements than pixels, and nonparametric curve estimation from finitely many noisy samples. Least squares is useless in this regime, since the system $X\beta=y$ is underdetermined. If the parameter is sparse (only a few of its entries are nonzero), estimation becomes possible, and the question is how accurate a computationally tractable estimator can be.

Candès and Tao (arXiv:math/0506081; Ann. Statist. 35(6), 2007, doi:10.1214/009053606000001523) introduced the Dantzig selector, an estimator computed by a linear program, and proved that its squared error is within a factor of order $\log p$ of the error of an oracle that knows where the nonzero entries are. The paper, with its discussion in the same issue, is one of the founding results of high-dimensional sparse regression, alongside the Lasso analysis of Bickel, Ritov and Tsybakov (arXiv:0801.1095).

Timeline. Candès and Tao (2005, arXiv:math/0502327) showed that $\ell_1$ minimization recovers a sparse vector exactly from noiseless data when the restricted isometry constants of the design satisfy $\delta_S+\theta_{S,S}+\theta_{S,2S}<1$ . The Dantzig selector paper (first posted 2005, published 2007) carried this to Gaussian noise, with the $\ell_2$ error bound formalized here (Theorem 1.1) and an oracle inequality (Theorem 1.2). Bickel, Ritov and Tsybakov (2009) replaced the restricted isometry hypothesis by weaker restricted eigenvalue conditions and showed that the Lasso and the Dantzig selector behave alike.

Setting

Observe $y\in\mathbb R^n$ from the linear model

y=X\beta+z ,

where $X\in\mathbb R^{n\times p}$ is a deterministic design matrix with columns $X_1,\dots,X_p$ , each of Euclidean norm $\|X_j\|_{\ell_2}=1$ ; $\beta\in\mathbb R^p$ is an unknown deterministic parameter; and $z=(z_1,\dots,z_n)$ is a vector of independent $N(0,\sigma^2)$ random variables with $\sigma>0$ . The vector $\beta$ is $S$ -sparse if at most $S$ of its entries are nonzero.

For $T\subseteq\{1,\dots,p\}$ let $X_T$ be the submatrix of the columns indexed by $T$ . The restricted isometry constant $\delta_S$ is the smallest $\delta\ge0$ with

(1-\delta)\|c\|_{\ell_2}^2\le\|X_Tc\|_{\ell_2}^2\le(1+\delta)\|c\|_{\ell_2}^2

for all $|T|\le S$ and all coefficient vectors $c$ ; the restricted orthogonality constant $\theta_{S,S'}$ (for $S+S'\le p$ ) is the smallest $\theta\ge0$ with $|\langle X_Tc,X_{T'}c'\rangle|\le\theta\|c\|_{\ell_2}\|c'\|_{\ell_2}$ for all disjoint $T,T'$ with $|T|\le S$ , $|T'|\le S'$ .

Given a tuning parameter $\lambda_p>0$ , the Dantzig selector $\hat\beta$ is any solution of

\min_{\tilde\beta\in\mathbb R^p}\|\tilde\beta\|_{\ell_1}\quad\text{subject to}\quad\|X^*(y-X\tilde\beta)\|_{\ell_\infty}=\max_{1\le j\le p}|\langle y-X\tilde\beta,X_j\rangle|\le\lambda_p\cdot\sigma .

Formalization targets

Goal: Theorem 1.1

Let $S\ge1$ , $3S\le p$ , $\beta$ $S$ -sparse, and $\delta_{2S}+\theta_{S,2S}<1$ . For every $a\ge0$ , with $\lambda_p=\sqrt{2(1+a)\log p}$ , with probability exceeding $1-(\sqrt{\pi\log p}\cdot p^a)^{-1}$ the program has a solution and every solution satisfies

\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\cdot\lambda_p^2\cdot S\cdot\sigma^2,\qquad C_1=\frac{4}{1-\delta_{2S}-\theta_{S,2S}} .

For $a=0$ this is $\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\cdot(2\log p)\cdot S\cdot\sigma^2$ , display (1.10) of the paper. The constant is the one the paper's proof establishes (see Formalization scope).

Milestones

The cone constraint (3.2): if $\|\beta+h\|_{\ell_1}\le\|\beta\|_{\ell_1}$ and $\beta$ vanishes off $T_0$ , then $\|h_{T_0^c}\|_{\ell_1}\le\|h_{T_0}\|_{\ell_1}$ .
The tube constraint (3.3): with unit-normed columns, if $|\langle z,X_j\rangle|\le\lambda_p$ for all $j$ and $\hat\beta$ is feasible, then $\|X^*X(\hat\beta-\beta)\|_{\ell_\infty}\le2\lambda_p$ .
Lemma 3.1 (under the section’s unit-column assumption): an $\ell_2$ bound on $h$ over $T_0\cup T_1$ ( $T_1$ the $S$ largest entries of $h$ off $T_0$ ) in terms of $\|X_{T_{01}}^TXh\|_{\ell_2}$ and $\|h\|_{\ell_1(T_0^c)}$ , and $\|h\|_{\ell_2}^2\le\|h\|_{\ell_2(T_{01})}^2+S^{-1}\|h\|_{\ell_1(T_0^c)}^2$ .
The deterministic core: with $\sigma=1$ , on the event $|\langle z,X_j\rangle|\le\lambda_p$ for all $j$ , every Dantzig selector satisfies $\|\hat\beta-\beta\|_{\ell_2}^2\le C_1^2\lambda_p^2S$ .
The Gaussian tail bound: for standard normal $z$ and $Z_j=\langle z,X_j\rangle$ , $\mathbb P(\sup_j|Z_j|>u)\le2p\,\varphi(u)/u$ with $\varphi(u)=(2\pi)^{-1/2}e^{-u^2/2}$ .

Significance

The result. Theorem 1.1 shows that an estimator computable by linear programming reaches, up to the factor $2\log p$ and the constant $C_1^2$ , the squared error $S\sigma^2$ that least squares would attain if the support of $\beta$ were known in advance, even when $p\gg n$ . The factor $\log p$ is the price of not knowing the support; the paper argues (p. 5) that, apart from this factor, (1.10) is unimprovable in general. The bound is non-asymptotic, with an explicit constant and an explicit failure probability, and it holds for every $S$ -sparse $\beta$ simultaneously in the sense that the good event (the noise being nearly orthogonal to every column) does not depend on $\beta$ . Its deterministic part, Lemma 3.1, is reused verbatim in the proof of the paper's oracle inequality (Theorem 1.2) and became a standard tool in compressed sensing.

Formalizing it. The result is proved, and to our knowledge no machine-checked proof exists. A formalization produces a checked version of the cone-and-tube argument behind most $\ell_1$ -recovery guarantees, a Lean statement of the restricted isometry machinery for noisy data, and a checked Gaussian maximal inequality usable for other high-dimensional estimators. It also settles the exact constant: the paper prints $C_1=4/(1-\delta_S-\theta_{S,2S})$ , while its proof gives $\delta_{2S}$ in place of $\delta_S$ .

Difficulty

Lemma 3.1 is the main obstacle. The obvious approach bounds $\|h\|_{\ell_2}$ directly through restricted isometry, and it fails because the error $h$ is not sparse: it spreads over all $p$ coordinates, and restricted isometry controls $X$ only on vectors with at most $2S$ nonzero entries. The two constraints (3.2) and (3.3) only say that $h$ is concentrated in $\ell_1$ on the $S$ coordinates of $T_0$ and that $X^*Xh$ is small coordinatewise, and turning that into an $\ell_2$ bound on all of $h$ is where the work lies. In Lean this requires bookkeeping that is routine on paper: ordering the coordinates of $h$ off $T_0$ by magnitude, with ties and a possibly incomplete last group of coordinates, and working with the span of a selected set of columns. On the probabilistic side, the tail bound needs the law of $\langle z,X_j\rangle$ (a weighted sum of independent Gaussians), a sharp Gaussian tail estimate of Mills-ratio type, and a union over $p$ events. A cruder sub-Gaussian bound $2e^{-u^2/2}$ would not give the stated failure probability.

Formalization scope

Indices are Fin n and Fin p; vectors are functions into ℝ. The norms, the column $X_j$ and the constants $\delta_S$ , $\theta_{S,S'}$ are the published definitions CandesTao_Decoding_Norms and CandesTao_Decoding_RestrictedIsometry (the smallest admissible constants, via sInf), from the formalization of Candès and Tao's Decoding by Linear Programming. The noise is a family z : Fin n → Ω → ℝ on a probability space, mutually independent (iIndepFun), each coordinate with law gaussianReal 0 σ². The $\ell_\infty$ constraint is coordinatewise. A Dantzig selector is any minimizer; uniqueness is not assumed. Section 3 works with $\sigma=1$ ; the goal is stated for general $\sigma>0$ .

Committed conventions and corrections:

Corrected constant. Theorem 1.1 is printed with $C_1=4/(1-\delta_S-\theta_{S,2S})$ , but the proof (pp. 18–19) applies Lemma 3.1, whose $\delta$ is $\delta_{2S}$ . Since $\delta_S\le\delta_{2S}$ , the printed constant is stronger than what is proved. The goal and the deterministic core are stated with $C_1=4/(1-\delta_{2S}-\theta_{S,2S})$ .
Domain. $1\le S$ and $3S\le p$ , because $\theta_{S,2S}$ is defined only for $S+2S\le p$ . This forces $p\ge3$ and $\log p>0$ .
Failure event. The probability bounded is that of the set where no Dantzig selector exists or some Dantzig selector violates the bound. A version that only constrains existing solutions, or that assumes the feasible set is nonempty, would be weaker. The bound is strict, as in the paper's "exceeding", and is on the outer measure, so no measurability of the event is assumed.
Standing assumptions are binders: unit-normed columns, independent Gaussian noise, deterministic $X$ and $\beta$ .

A trivializing formalization is excluded: the hypothesis $\delta_{2S}+\theta_{S,2S}<1$ is on the actual least constants of $X$ , not on free parameters, and it is satisfiable (for instance by $X=I_p$ , where both constants vanish).

Needed infrastructure: sums of independent real Gaussians (Mathlib has gaussianReal and its convolution), a Mills-ratio tail bound, a sorting-based block decomposition of a Finset, and orthogonal projection onto the span of finitely many columns. The block decomposition and the tail bound are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of Lemma 3.1.

Selected references

E. Candès and T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6) (2007), 2313–2351. arXiv:math/0506081, doi:10.1214/009053606000001523
E. Candès and T. Tao, Decoding by linear programming, IEEE Trans. Inform. Theory 51(12) (2005), 4203–4215. arXiv:math/0502327
P. Bickel, Y. Ritov and A. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4) (2009), 1705–1732. arXiv:0801.1095

9 thms3 active usersReviewed

Completed

Operations Research Stochastic Systems·Captain: mikedeng1

Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance II: An O(n²) Extended Formulation of the Multiclass M/M/1 Performance PolymatroidResearch Paper

Motivation

A single server shared by several classes of customers is the basic model of scheduling under uncertainty: jobs of different types arrive at random, need random amounts of work, and a scheduler decides at every moment which type to serve. A classical way to optimize such a system, the achievable region approach, describes the set of all performance vectors that some scheduling policy can attain, and optimizes a linear cost over that set with linear programming. For the multiclass M/M/1 queue under preemptive, work-conserving scheduling, this set is a polyhedron described by conservation laws (Coffman and Mitrani, 1980; Gelenbe and Mitrani, 1980; Shanthikumar and Yao, 1992): it is the base of a polymatroid, its vertices are the performance vectors of the $n!$ strict priority rules, and minimizing a linear cost over it is solved greedily, which recovers the $c\mu$ rule.

That description uses one inequality for every nonempty set of classes, $2^n-1$ constraints in all. Bertsimas, Paschalidis and Tsitsiklis (working paper 1992, Annals of Applied Probability 1994) derived performance bounds for general multiclass networks from quadratic potential functions. Specialized to one station, their nonparametric method produces a different polyhedron, in $O(n^2)$ variables with $O(n^2)$ constraints, and they show that its projection is exactly the conservation-law polyhedron (Theorem 8.4). The paper remarks that this confirms, for this polymatroid, the belief that problems solvable in polynomial time admit polynomial-size formulations.

Setting

There are $n$ customer classes $E=\{1,\dots,n\}$ . Class $i$ has arrival rate $\lambda_i>0$ and service rate $\mu_i>0$ ; its traffic intensity is $\rho_i=\lambda_i/\mu_i$ , and the queue is stable: $\sum_{i\in E}\rho_i<1$ . For $S\subseteq E$ define

b(S)=\frac{\sum_{i\in S}\rho_i/\mu_i}{1-\sum_{i\in S}\rho_i},\qquad b(\emptyset)=0 .

In the queue, $n_i$ is the steady-state mean number of class $i$ customers and $n_i/\mu_i$ their mean remaining work; $b(S)$ is the mean work of the classes in $S$ when those classes have preemptive priority over the rest.

The performance polymatroid P1 (Theorem 8.3) is the set of $(n_i)\in\mathbb R_+^n$ with

\sum_{i\in S}\frac{n_i}{\mu_i}\ge b(S)\quad (S\subset E),\qquad \sum_{i\in E}\frac{n_i}{\mu_i}=b(E).

For a permutation $\pi=(\pi_1,\dots,\pi_n)$ of $E$ , the vector $v(\pi)$ is the solution of the triangular system $\sum_{j=1}^{k}x_{\pi_j}/\mu_{\pi_j}=b(\{\pi_1,\dots,\pi_k\})$ , $k=1,\dots,n$ (Eq. (58) with $f_i^S=1/\mu_i$ ).

The extended formulation P2 (Theorem 8.4) is the set of nonnegative $(n_i)_{i\in E}$ and $(I_{ij})_{i,j\in E}$ satisfying

\mu_iI_{ii}-\lambda_in_i=\lambda_i,\qquad \mu_iI_{ij}+\mu_jI_{ji}-\lambda_jn_i-\lambda_in_j=0\ (i\neq j),\qquad \sum_{i\in E}I_{ij}=n_j .

In the queue, $I_{ij}$ is the steady-state mean of the number of class $j$ customers on the event that the server is busy with class $i$ . The projection $\mathrm{P2}'$ of P2 is the set of $(n_i)$ for which some $(I_{ij})$ makes $((n_i),(I_{ij}))$ a point of P2.

Formalization targets

Goal: Theorem 8.4

\mathrm{P2}'=\mathrm{P1}.

Both inclusions are part of the goal. The statement fixes no constants and holds for every $n$ , every positive rate vector and every stable load.

Milestones

§8.2, proof of Theorem 8.3. The extreme points of P1 are exactly the vectors $v(\pi)$ , and P1 is their convex hull:

\operatorname{ext}\mathrm{P1}=\{v(\pi)\},\qquad \mathrm{P1}=\operatorname{conv}\{v(\pi)\}.

§8.2, proof of Theorem 8.4. The easy inclusion, which the paper obtains from its Theorem 4.4:

\mathrm{P2}'\subseteq\mathrm{P1}.

Significance

The result. Theorem 8.4 replaces $2^n-1$ constraints by $O(n^2)$ constraints in $O(n^2)$ variables without changing the projected set. Any linear program over the M/M/1 performance region, including problems with side constraints where the greedy $c\mu$ rule no longer applies, can then be solved with a polynomial-size LP. It also identifies the paper's nonparametric method as exact at a single station: the method loses nothing there, which is the baseline against which its gaps in networks are measured.

Formalizing it. The result is proved in the paper, but the reverse inclusion $\mathrm{P1}\subseteq\mathrm{P2}'$ is argued through achievability: every point of P1 is the performance of some (randomized) policy, and every policy's performance satisfies the equations of P2. That argument rests on stochastic objects (invariant distributions under arbitrary policies, and time-0 randomizations over priority rules) that the paper does not define precisely. The paper points to a purely combinatorial derivation in Paschalidis' thesis, which we have not seen. A machine-checked proof of the polyhedral identity is therefore new content: it supplies the deterministic argument the paper delegates. The polymatroid structure of P1 (Milestone 1) is classical for supermodular set functions; this mission requires it for this specific $b$ . We know of no formalization of either result.

Difficulty

The inclusion $\mathrm{P2}'\subseteq\mathrm{P1}$ only combines the equations of P2 with nonnegativity. The reverse inclusion is the hard half: for each point of P1 one must exhibit a nonnegative matrix $(I_{ij})$ satisfying $n^2$ linear equations, and the inequalities of P1 say nothing directly about the off-diagonal entries $I_{ij}$ . The paper's own argument does not help here, since it produces $I$ as a steady-state expectation under a scheduling policy, an object defined through a Markov chain and given in no closed form. The sign constraints $I_{ij}\ge0$ are where the $2^n-1$ inequalities of P1 are encoded, and a proof has to explain how $O(n^2)$ sign conditions on auxiliary variables carry exactly the information of exponentially many inequalities in the original ones.

Formalization scope

Classes are Fin n; rates are real functions lam mu : Fin n → ℝ with 0 < lam i, 0 < mu i and ∑ i, lam i / mu i < 1. The paper's $n_i$ is written x i, because n is the number of classes. A point of P2 is a pair (x, I) with I i j $=I_{ij}$ , including the diagonal entries. P1 is the platform definition AllocationIndices.achievablePolytope with the matrix $A^S_i=1/\mu_i$ : inequality for every $S\neq E$ , equality at $S=E$ , nonnegativity. The paper writes $N$ for the class set $E$ in (65) and (71); every such sum runs over all classes. The constraints (64)–(65) bound $n_i/\mu_i$ , not $n_i$ . $v(\pi)$ is given by its closed form, $v(\pi)_{\pi_k}=\mu_{\pi_k}\bigl(b(\{\pi_1,\dots,\pi_k\})-b(\{\pi_1,\dots,\pi_{k-1}\})\bigr)$ , which solves (58). The standing hypothesis $\lambda_i>0$ is presupposed by the model (Poisson arrivals at rate $\lambda_i$ ); the load condition is the paper's stability condition and keeps every denominator of $b$ positive.

No statement involves a policy, a Markov chain or an expectation; the queueing meaning above is motivation only. In particular, neither "P1 is the achievable region" nor "the performance vector of each priority rule is achievable" is formalized. The goal is the full set identity: stating only $\mathrm{P2}'\subseteq\mathrm{P1}$ , or assuming $\mathrm{P1}=\operatorname{conv}\{v(\pi)\}$ as a hypothesis of the goal, would not be Theorem 8.4.

A complete development needs: supermodularity of $b$ under the load condition; the greedy (Edmonds) description of base polytopes of supermodular functions, which is reusable well beyond this mission; and a nonnegative solution of the P2 system at each $v(\pi)$ . Contributions of any of these as separate lemmas are welcome.

Selected references

D. Bertsimas, I. Ch. Paschalidis, J. N. Tsitsiklis, Optimization of Multiclass Queueing Networks: Polyhedral and Nonlinear Characterizations of Achievable Performance, MIT Sloan School WP #3509-92-MSA, 1992; Annals of Applied Probability 4(1):43–75, 1994. https://doi.org/10.1214/aoap/1177005200
E. G. Coffman, I. Mitrani, A characterization of waiting time performance realizable by single-server queues, Operations Research 28(3):810–821, 1980. https://doi.org/10.1287/opre.28.3.810
J. G. Shanthikumar, D. D. Yao, Multiclass queueing systems: polymatroidal structure and optimal scheduling control, Operations Research 40(S2):S293–S299, 1992. https://doi.org/10.1287/opre.40.3.S293
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):257–306, 1996. https://doi.org/10.1287/moor.21.2.257
J. Edmonds, Submodular functions, matroids, and certain polyhedra, in Combinatorial Structures and Their Applications, Gordon and Breach, 1970, pp. 69–87.

5 thms3 active usersReviewed

Operations Research Optimization Probability·Captain: mikedeng1

Air Travel Demand and Airline Seat Inventory Management I: Marginal Seat Allocation Among Distinct Fare ClassesTextbook

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

Eq. (5.6): $\bar b_i(S) + \bar l_i(S) = \bar r_i$ for requests of finite mean.
Eq. (5.11): $\bar R_i(S) - \bar R_i(S-1) = f_i \cdot P[r_i \ge S]$ for $S \ge 1$ .
Eqs. (6.1)–(6.2): $\bar P_i$ and $\mathrm{EMSR}_i$ are non-increasing in $S$ .
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$ .
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

8 thms3 active usersReviewed

Linear Optimization

Missions

Smale's Ninth Problem: Strongly Polynomial Linear ProgrammingOpen Problem

The problem of solving linear inequalities

Why it matters

The question and what is known

A hierarchy of formalization targets

Formalization scope

Selected references

Selected Topics in Column Generation I: Discretization — Every Integer Point of a Rational Polyhedron Is a Generating Integer Point Plus an Integer Combination of Integer RaysResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (pp. 1011–1012)

Milestone: Remark in §3.3 (p. 1012)

Significance

Difficulty

Formalization scope

Selected references

An Application of Simultaneous Diophantine Approximation in Combinatorial Optimization: A Small Integral Objective with the Same Optimal Solutions and Dual BasesResearch Paper

Motivation

Setting

Formalization targets

Goal — Theorem 4.2 (p. 58)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems 3: Capacity Scaling for the Hitchcock ProblemResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 9

Milestones

Significance

Difficulty

Formalization scope

Selected references

Linear Programming in Linear Time When the Dimension Is Fixed: Fixed-Dimension LP Feasibility Decided in Linear Time on the Real RAMResearch Paper

Motivation

Setting

Formalization targets

Goal: linear-time feasibility on the real RAM

Milestones

Significance

Difficulty

Formalization scope

Selected references

The Polynomial Hirsch ConjectureOpen Problem

Motivation

Timeline

Setting

Formalization targets

Goal — the polynomial Hirsch conjecture

Milestones — the known ladder

Significance

Difficulty

Formalization scope

Selected references

Introduction to Linear Optimization X: Max-Flow Min-CutTextbook

Linear Programming: Foundations and Extensions I: Degeneracy and Termination of the Simplex Method under Bland's RuleTextbook

Motivation

Setting

Formalization targets

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

Milestones

Significance

Difficulty

Formalization scope

Selected references

Theory of Games and Economic Behavior III: Mixed Strategies, the Minimax Theorem and Good StrategiesTextbook

Motivation

Setting

Formalization targets

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

Milestones, in attack order

Significance

Difficulty

Formalization scope

Goal: the knapsack bound is the Lagrangean bound at $\lambda=c_2$