Linear Optimization

Why a likelihood maximum needs a diagnostic

The conditional logit model assigns probabilities to choices among alternatives whose observable attributes differ from trial to trial. A fitted parameter vector is usually obtained by maximizing a log-likelihood. For a finite data set, however, maximization need not produce a finite vector: some directions in parameter space can keep improving the likelihood while their length grows without bound. McFadden identifies a condition that rules out these directions and then gives a quadratic program that can test the condition. This mission formalizes that test, Lemma 4 of the published 1974 chapter Conditional Logit Analysis of Qualitative Choice Behavior.

The chapter develops a statistical model from observable choice data and addresses the existence of a maximum likelihood estimate in Lemma 3. Lemma 4 turns its existence condition into a finite optimization problem. The diagnostic matters because an optimization routine returning increasingly large parameter estimates is not, by itself, evidence that a finite maximizer exists. The result specifies a mathematical test tied to the observed choice counts and the attributes of the alternatives.

Choice experiments and weighted differences

There are $N\geq1$ trials. Trial $n$ offers $J_n$ alternatives, indexed by $i$ and $j$. Alternative $i$ has an attribute vector $z_{in}\in\mathbb R^K$, and $S_{in}$ counts how many times it was selected in that trial. Each trial has at least two alternatives and $R_n=\sum_iS_{in}>0$ observations. The vector $\theta\in\mathbb R^K$ is the unknown parameter of the underlying conditional logit model. Equation (16) assigns alternative $i$ a probability proportional to $\exp(z_{in}\cdot\theta)$, with the probabilities normalized over the alternatives in the same trial McFadden, pp. 113–114, equation (16).

For the test, define the weighted difference

$$w_{nij}=S_{in}(z_{jn}-z_{in})\in\mathbb R^K.$$

It is indexed by every trial and every ordered pair of alternatives, including $i=j$ and alternatives whose observed count is zero. Such terms simply produce zero vectors. Keeping them in the index set makes the formal statement agree with the chapter's quantifiers and its quadratic program.

Axiom 5, called full rank in the chapter, says that the rows obtained by subtracting each trial's probability weighted mean attribute vector from its alternative attributes have rank $K$. Equivalently, the vectors $z_{jn}-z_{in}$ span $\mathbb R^K$; the probability weights in that mean are strictly positive and sum to one. Axiom 6 says that no nonzero direction $\gamma\in\mathbb R^K$ satisfies $w_{nij}\cdot\gamma\leq0$ for every ordered index triple. These are conditions on the same observed experiment, but they serve different roles: full rank concerns the attribute geometry, while Axiom 6 also uses the choice counts McFadden, p. 116, Axioms 5–6.

Formalization targets

Lemma 4: a quadratic-programming test

Let $Q$ be the set of feasible vectors

$$Q=\left\{y=\sum_{n=1}^{N}\sum_{i,j=1}^{J_n}\alpha_{ijn}w_{nij}: \alpha_{ijn}\geq1\text{ for all }n,i,j\right\}.$$

The mission's goal is the equivalence in Lemma 4:

$$\text{Axiom 6 holds} \quad\Longleftrightarrow\quad \min_{y\in Q}y\cdot y=0.$$

The right side means that the program attains a value of zero. An infimum of zero without an attained feasible point would be a weaker statement and would not express the lemma. The three milestones follow the three assertions in the printed proof: a zero minimum implies Axiom 6; an interior origin in the cone generated by the $w_{nij}$ gives positive coefficients and a zero minimum; and a noninterior origin gives a separating direction that violates Axiom 6 McFadden, p. 117, Lemma 4 and equation (22).

What the result provides

Lemma 3 of the chapter states that Axiom 6 characterizes the existence of a vector maximizing the conditional-logit log-likelihood under the preceding axioms. Lemma 4 gives a finite quadratic-programming criterion for that same condition. It therefore allows the model's existence question to be checked from data before treating a numerical optimizer's output as an estimate McFadden, pp. 116–117, Lemmas 3–4.

The paper proves these results. The work here is to produce machine-checkable statements for the finite-dimensional data, the two axioms, the feasible set, and the equivalence, followed by proofs in the solver stage. The cone and separation milestones can support later formalizations of existence conditions in other finite exponential-family models, provided their hypotheses and signs are checked anew. This mission does not claim a general theorem for all such models.

Why the equivalence is delicate

The tempting diagnostic is to ask whether a numerical solve returns a small objective value. That does not settle the mathematical question: the objective's infimum could approach zero without the feasible set containing a zero vector. The paper's conclusion is about a minimum, so attainment must remain visible in the formal statement. There is also a distinction between positive coefficients in a cone representation and the printed constraints $\alpha_{ijn}\geq1$ in equation (22). Both conditions must appear in their proper places.

The full-rank condition alone does not ensure that the vectors $w_{nij}$ span the attribute space if a trial has no observed choices. The section describes $R_n$ repetitions of each trial, and the formal data require $R_n>0$. This convention is needed for the strict-inequality claim in the first paragraph of Lemma 4's proof. The geometry also has to account for every ordered pair, even when its vector is zero; dropping these indices would alter the program stated in the chapter.

Formalization scope

Lean represents a nonempty set of trials by Fin N, alternatives in trial $n$ by Fin (J n), counts by natural numbers, and attributes by EuclideanSpace ℝ (Fin K). The count $R_n$ is the sum of observed choice counts. The model requires $J_n\geq2$ and $R_n>0$ for each trial. There is no extra assumption that $K>0$: the zero-dimensional case is included and the equivalence has its ordinary degenerate meaning there.

Axiom 5 is encoded through the equivalent span of within-trial attribute differences. This removes the parameter dependent logit probabilities from a theorem that only uses rank. Axiom 6 retains exactly the nonpositive sign and every $n,i,j$ from the page. The feasible set uses coefficients at least one, while the auxiliary generated cone uses nonnegative coefficients. The quadratic objective is the square of the Euclidean norm. IsLeast on its image over the feasible set expresses an attained minimum, so the statement cannot be satisfied by a vacuous or unattained infimum.

The definition bundle and the three proof-step theorems are the mission's direct scope. A complete development needs finite-dimensional inner-product geometry, finite sums, a cone interior argument, and separation. The definitions of weighted differences and the feasible set are reusable for studying nearby existence tests. Contributions that prove the stated milestones or supply faithful finite-dimensional geometry for them are welcome; substitutions that weaken the coefficient constraint or the attainment claim do not establish Lemma 4.

Selected references

• Daniel McFadden, “Conditional Logit Analysis of Qualitative Choice Behavior,” in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, 1974, pp. 105–142; especially pp. 113–117, Axioms 5–6, Lemmas 3–4, and equation (22). Book catalog search.

Motivation

The smallest enclosing ball problem asks, for finitely many points $p_1,\dots,p_n\in\mathbb{R}^d$, for a ball of the smallest radius that contains all of them. It appears in clustering, in collision detection and bounding-volume hierarchies, in facility location (placing one service point so that the farthest client is as close as possible), and in the analysis of geometric algorithms. Sylvester posed the planar version in 1857; Megiddo (1983) gave a linear-time algorithm in fixed dimension, and Welzl (1991) a simple randomized one.

This mission formalizes Section 8.7 of Matoušek and Gärtner, Understanding and Using Linear Programming (Springer, 2007), which uses the problem to introduce convex programming. Unlike the geometric problems of the book's Chapter 2, the smallest ball cannot be written as a linear program. The section shows instead that it is a convex quadratic program, derives the Karush–Kuhn–Tucker (KKT) conditions for convex programs in equational form from the duality theorem of linear programming, and uses them to prove that the smallest enclosing ball exists and is unique. It is the book's bridge from linear to convex optimization.

Setting

A function $f:\mathbb{R}^n\to\mathbb{R}$ is convex if $f((1-t)x+ty)\le(1-t)f(x)+tf(y)$ for all $x,y\in\mathbb{R}^n$ and $t\in[0,1]$. A convex program in equational form is

$$\text{minimize } f(x)\quad\text{subject to } Ax=b,\ x\ge 0,$$

with $A$ a real $m\times n$ matrix with columns $a_1,\dots,a_n$, $b\in\mathbb{R}^m$ and $f$ convex. A vector $x$ is feasible if $Ax=b$ and $x\ge 0$ componentwise, and optimal if it is feasible and $f(x)\le f(x')$ for every feasible $x'$. For differentiable $f$, $\nabla f(x)$ is the row vector of partial derivatives, so $\nabla f(x^*)(x-x^*)$ is a scalar.

For points $p_1,\dots,p_n\in\mathbb{R}^d$, write $P=\{p_1,\dots,p_n\}$ and let $Q$ be the $d\times n$ matrix whose $j$th column is $p_j$. The program studied is

$$\text{(8.15)}\qquad \text{minimize } f(x)=x^TQ^TQx-\sum_{j=1}^n x_j\,p_j^Tp_j\quad\text{subject to } \sum_{j=1}^n x_j=1,\ x\ge 0 .$$

A ball is a closed Euclidean ball $B(c,r)=\{z\in\mathbb{R}^d:\|z-c\|\le r\}$. The ball $B(c,r)$ is the unique smallest enclosing ball of a set $S$ if $r\ge 0$, $S\subseteq B(c,r)$, every ball containing $S$ has radius at least $r$, and every ball containing $S$ of radius at most $r$ has center $c$.

Formalization targets

Goal: Theorem 8.7.4

For $n\ge 1$ points $p_1,\dots,p_n\in\mathbb{R}^d$, the objective $f$ of (8.15) is convex, and

1. (8.15) has an optimal solution $x^*$;
2. there is a point $p^*$ with $p^*=Qx^*$ for every optimal $x^*$, and for every optimal $x^*$

$$-f(x^*)\ge 0\quad\text{and}\quad B\big(p^*,\sqrt{-f(x^*)}\big)\ \text{is the unique smallest enclosing ball of } P .$$

Milestones

• Fact 8.7.1. For $C\subseteq\mathbb{R}^n$ convex, $f$ differentiable and convex, and $x^*\in C$: $x^*$ minimizes $f$ over $C$ iff $\nabla f(x^*)(x-x^*)\ge 0$ for all $x\in C$.
• Proposition 8.7.2 (KKT conditions). For $f$ convex with continuous partial derivatives and $x^*$ feasible: $x^*$ is optimal iff there is $\tilde y\in\mathbb{R}^m$ with

$$\nabla f(x^*)_j+\tilde y^Ta_j\ \begin{cases}=0&\text{if } x^*_j>0,\\ \ge 0&\text{otherwise,}\end{cases}\qquad j=1,\dots,n.$$

• Lemma 8.7.3. If $s_1,\dots,s_k$ lie on the boundary of the ball $B$ with center $s^*$, then $B$ is the unique smallest enclosing ball of $\{s_1,\dots,s_k\}$ iff for every $u\in\mathbb{R}^d$ some $j$ has $u^T(s_j-s^*)\le 0$.

Significance

The result. Theorem 8.7.4 gives existence and uniqueness of the smallest enclosing ball together with an explicit certificate: the center is a convex combination $Qx^*$ of the input points, the squared radius is the negated optimum value, and the points $p_j$ with $x^*_j>0$ lie on the boundary. It reduces the geometric problem to a convex quadratic program, for which interior-point and simplex-type solvers exist, and it is the basis of the combinatorial characterization "the center lies in the convex hull of the boundary points" used by Welzl-type algorithms. Proposition 8.7.2 is the KKT theorem for equational-form convex programs; it holds without any constraint qualification because the constraints are linear.

Formalizing it. All results here are classical and proved in the book; none is open. The mission produces machine-checked statements and, when solved, proofs of: the first-order optimality criterion for convex functions on convex sets in $\mathbb{R}^n$; the equational-form KKT theorem derived from LP duality; the boundary characterization of unique smallest enclosing balls; and existence and uniqueness of the smallest enclosing ball in every dimension. Mathlib has first-order necessary conditions at local minima and general convexity theory, but no KKT theorem for linearly constrained convex programs in this form and no smallest-enclosing-ball theory.

Difficulty

Existence of an optimum and convexity of $f$ are routine. For the KKT conditions, the necessary direction needs multipliers, which do not come from calculus alone: the obvious Lagrange-multiplier argument handles only equality constraints and says nothing about the sign pattern forced by $x\ge 0$. For the goal, a solver must connect three layers — the gradient of a quadratic form in matrix notation, the multiplier conditions, and the Euclidean geometry of distances to $p^*$ — and uniqueness of the ball does not follow from uniqueness of the optimizer $x^*$, which in general is not unique (repeated or cospherical points). The statement quantifies over all optimal $x^*$ and asserts that they all yield the same center.

Formalization scope

• Vectors of $\mathbb{R}^n$ are Fin n → ℝ, so the book's indices $1,\dots,n$ become $0,\dots,n-1$. Points of $\mathbb{R}^d$ are EuclideanSpace ℝ (Fin d), so $\|\cdot\|$ and $p^Tq$ are Euclidean. The matrix $Q$ is Matrix (Fin d) (Fin n) ℝ.
• Optimality is stated against every feasible point; no infimum or supremum is taken. $\nabla f(x^*)(x-x^*)$ is the Fréchet derivative applied to $x-x^*$, and $\nabla f(x^*)_j$ its value on the $j$th unit vector. "Continuous partial derivatives" is ContDiff ℝ 1 f. Convexity is ConvexOn ℝ Set.univ f.
• Balls are closed. The squared radius $-f(x^*)$ is expressed by asserting $-f(x^*)\ge 0$ and taking the radius $\sqrt{-f(x^*)}$. "Unique ball of smallest radius" is written out as minimality of the radius among all enclosing closed balls plus equality of centers for every enclosing ball of radius at most the optimum; merely stating that the ball encloses $P$ would not be the theorem.
• The goal assumes $n\ge 1$ (for $n=0$ the feasible set is empty). In Fact 8.7.1 the minimizer $x^*$ is assumed to lie in $C$, as "minimizes $f$ over $C$" presupposes. In Lemma 8.7.3 the radius is nonnegative and each $s_j$ is at distance exactly $r$ from $s^*$.
• Needed infrastructure: gradients of quadratic forms on Fin n → ℝ, LP duality for the pair (maximize $c^Tx$, $Ax=b$, $x\ge0$) / (minimize $b^Ty$, $A^Ty\ge c$), compactness of the standard simplex, and elementary Euclidean geometry. The first-order criterion and the KKT theorem are reusable beyond this mission; proofs through any route are welcome.

Selected references

• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.7, pp. 184–191. https://doi.org/10.1007/978-3-540-30717-4
• S. Boyd and L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. https://doi.org/10.1017/CBO9780511804441
• N. Megiddo, Linear-time algorithms for linear programming in $\mathbb{R}^3$ and related problems, SIAM J. Comput. 12(4), 1983. https://doi.org/10.1137/0212052
• E. Welzl, Smallest enclosing disks (balls and ellipsoids), in New Results and New Trends in Computer Science, LNCS 555, Springer, 1991. https://doi.org/10.1007/BFb0038202
• J. J. Sylvester, A question in the geometry of situation, Quarterly Journal of Pure and Applied Mathematics 1, 1857.

Motivation

A basic question of combinatorial geometry asks when a family of sets can be pierced (or stabbed) by few points. For intervals on the real line the answer is classical: if every two of finitely many closed intervals intersect, one point meets all of them, namely the rightmost left endpoint. This is the one-dimensional case of Helly's theorem. The situation changes as soon as the sets are allowed to have holes. Unions of two intervals can intersect pairwise without any point being common to three of them, so no single point suffices, and it is not obvious that any bound depending only on the number of holes exists.

This mission formalizes the answer given in Section 8.6 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer, 2007): pairwise intersecting unions of $d$ intervals can always be pierced by $2d^2$ points. The section uses the result to illustrate a general method of combinatorics, in which a linear programming relaxation of a covering problem is bounded through LP duality and then rounded. The same scheme, a bound on the fractional transversal number followed by a rounding step, appears across discrete geometry and combinatorial optimization.

Timeline.

• 1970: Gyárfás and Lehel prove that a bound depending only on $d$ exists; their bound is exponential in $d$ (A Helly-type problem in trees, in Combinatorial Theory and its Applications, North-Holland).
• 1992: Alon and Kleitman solve the Hadwiger–Debrunner $(p,q)$-problem with a method combining fractional transversals and LP duality (Adv. Math. 96).
• 1997: Kaiser proves the bound $d^2$ using algebraic topology (Discrete Comput. Geom. 18).
• 1998: Alon gives the short LP-duality proof of the bound $2d^2$ formalized here (Discrete Comput. Geom. 19).
• 2001: Matoušek shows that the transversal number cannot in general be below a constant multiple of $d^2/\log d$ (Discrete Comput. Geom. 26).

Setting

Fix an integer $d \ge 1$. A $d$-interval is a union of $d$ closed intervals on the real line,

$$J = [a_1,b_1] \cup \dots \cup [a_d,b_d], \qquad a_k \le b_k .$$

The numbers $a_k$ and $b_k$ are the endpoints of $J$. A finite family $\mathcal J$ of $d$-intervals is pairwise intersecting if $J_1 \cap J_2 \ne \emptyset$ for all $J_1, J_2 \in \mathcal J$. A set $X$ of real numbers is a transversal of $\mathcal J$ if every $J \in \mathcal J$ contains a point of $X$.

More generally, for a finite set $V$ and a system $\mathcal F$ of subsets of $V$: a transversal is a set $X \subseteq V$ meeting every member; the transversal number $\tau(\mathcal F)$ is the smallest size of a transversal; a matching is a subsystem of pairwise disjoint members, and the matching number $\nu(\mathcal F)$ is the largest size of a matching. The fractional transversal number $\tau^*(\mathcal F)$ is the optimal value of the linear program

$$\min \sum_{v\in V} x_v \quad \text{s.t.} \quad \sum_{v \in F} x_v \ge 1 \ (F \in \mathcal F),\ x \ge 0,$$

and the fractional matching number $\nu^*(\mathcal F)$ is the optimal value of

$$\max \sum_{F\in\mathcal F} y_F \quad \text{s.t.} \quad \sum_{F :\, v \in F} y_F \le 1 \ (v \in V),\ y \ge 0 .$$

Formalization targets

Goal: Theorem 8.6.1

$$\mathcal J \text{ finite, pairwise intersecting family of } d\text{-intervals} \;\Longrightarrow\; \exists X \subset \mathbb R,\ |X| \le 2d^2,\ X \cap J \ne \emptyset \ \ \forall J \in \mathcal J .$$

This is the book's theorem with its constant $2d^2$.

Milestones

1. Lemma 8.6.2. If $J_1,\dots,J_n$ ($n \ge 1$, repetitions allowed) are $d$-intervals with $J_i \cap J_j \ne \emptyset$ for all $i,j$, then some endpoint of some $J_i$ lies in at least $n/2d$ of the $J_j$.
2. §8.6, p. 182. For every finite set system with nonempty members,

$$\nu(\mathcal F) \le \nu^*(\mathcal F) = \tau^*(\mathcal F) \le \tau(\mathcal F).$$

3. Lemma 8.6.3. If $\mathcal J$ is a finite pairwise intersecting family of $d$-intervals and $P$ its set of endpoints, there are weights $x_p \ge 0$, $p \in P$, with $\sum_{p \in J \cap P} x_p \ge 1$ for every $J \in \mathcal J$ and $\sum_{p\in P} x_p \le 2d$.

Significance

The result. Theorem 8.6.1 shows that the piercing number of pairwise intersecting $d$-intervals is bounded by a function of $d$ alone, and that this function is polynomial. The section also states, without proof, the extension $\tau(\mathcal J) \le 2d^2\,\nu(\mathcal J)$ for arbitrary finite families of $d$-intervals. Upper bounds of this kind feed into piercing and hitting-set questions for families with bounded "complexity", and the chain $\nu \le \nu^* = \tau^* \le \tau$ is the standard frame in which such bounds are proved.

Formalizing it. The theorem, both lemmas and the duality chain are proved in the literature and in the book. None of them is on the platform. The work consists of formalizing the book's proof: a double-counting argument, LP duality for the pair of fractional programs together with the rationality of an optimal basic solution, and a rounding step. The general-set-system milestone is reusable for any transversal problem, independent of $d$-intervals.

Difficulty

The obvious generalization of the one-dimensional argument fails: for $d \ge 2$ no point need be common to all members, so there is no single extremal endpoint to choose, and a greedy piercing procedure has no control over how many points it uses. The difficulty is to obtain a bound that does not depend on the size of the family. In the book's route the counting statement of Lemma 8.6.2 holds only for equal weights, while the fractional programs produce arbitrary real weights, and the passage between the two, as well as the passage from a fractional transversal of small total weight to an actual finite set of points, are the steps that need care.

Formalization scope

A $d$-interval is stored as data: two functions left, right : Fin d → ℝ with left k ≤ right k, together with the set toSet $= \bigcup_k [a_k,b_k]$. Components are indexed $0,\dots,d-1$. Endpoints are those of the given components, so they depend on the representation, as in the book's proofs. Families are Finsets of such data; Lemma 8.6.2 uses a Fin n-indexed sequence, since the proof of Lemma 8.6.3 applies it to a sequence with repetitions. The hypotheses $d \ge 1$ (the book's definition) and, in Lemma 8.6.2, $n \ge 1$ are explicit. The quantity $n/2d$ is real division. Transversal sizes are cardinalities of a Finset ℝ bounded by $2d^2$.

For set systems, $V$ is a finite type and $\mathcal F$ a Finset (Finset V) with nonempty members; without this assumption no transversal exists and both fractional programs degenerate. The numbers $\tau^*$ and $\nu^*$ are expressed through optimal feasible solutions, not as infima or suprema, so no junk value of an empty or unbounded set is involved. $\tau$ is an sInf over $\mathbb N$ that is attained under the nonemptiness assumption, and $\nu$ is a maximum over the finite family of matchings.

A trivializing formalization is ruled out: the pairwise-intersection hypothesis is satisfiable by nonempty families, the transversal is required to meet the actual sets $J$, not a representation artifact, and the bound $2d^2$ and $2d$ are the book's constants, not weakened ones.

Needed infrastructure: finite sums over Finset ℝ, LP duality for a finite primal–dual pair in inequality form (or a direct proof of the chain), rationality of an optimal vertex, and a left-to-right sweep over a sorted finite set of reals. Contributions of a general LP duality statement for set-system relaxations are welcome and reusable.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.6. https://doi.org/10.1007/978-3-540-30717-4
• N. Alon, Piercing d-intervals, Discrete Comput. Geom. 19 (1998) 333–334.
• N. Alon, D. Kleitman, Piercing convex sets and the Hadwiger–Debrunner (p, q)-problem, Adv. Math. 96 (1992) 103–112.
• T. Kaiser, Transversals of d-intervals, Discrete Comput. Geom. 18 (1997) 195–203.
• J. Matoušek, Lower bounds on the transversal numbers of d-intervals, Discrete Comput. Geom. 26 (2001) 283–287.
• A. Gyárfás, J. Lehel, A Helly-type problem in trees, in Combinatorial Theory and its Applications (P. Erdős, A. Rényi, V. T. Sós, eds.), North-Holland, 1970, 571–584.

Motivation

A deep-space probe sends a vector $w\in\mathbb{R}^k$ encoded as $z=Qw\in\mathbb{R}^n$, and up to about 8% of the transmitted numbers may be corrupted arbitrarily. Section 8.5 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007, DOI 10.1007/978-3-540-30717-4) shows that decoding reduces to finding a sparse solution of an underdetermined linear system $Ax=b$, and that under suitable conditions this sparse solution is found exactly by a single linear program. The same problem arises in signal processing (sparse representations in redundant wavelet dictionaries) and in computer tomography, and it is the core of what became known as compressed sensing.

Timeline, as recorded in the book's references:

• 1999: Chen, Donoho and Saunders introduce basis pursuit, minimizing the $\ell_1$-norm subject to $Ax=b$ (SIAM J. Sci. Comput. 20).
• 2005: Candès, Rudelson, Tao and Vershynin prove that for every $\alpha\in(0,1)$ there is $\beta(\alpha)>0$ such that a random $\lfloor\alpha n\rfloor\times n$ matrix is exact for $\lfloor\beta n\rfloor$-sparse vectors with probability exponentially close to 1 (FOCS 2005).
• 2006: Donoho, via neighborliness of centrally symmetric polytopes, obtains the constants $\alpha=0.75$, $\beta=0.08$ used in the book, and shows that no $\lfloor 0.75n\rfloor\times n$ matrix is exact for $r>0.25n$ when $n$ is large (Discrete Comput. Geom. 35).
• 2006: Linial and Novik prove further upper bounds showing that these existence results are asymptotically optimal (Discrete Comput. Geom. 36).

Setting

Let $A$ be a real $m\times n$ matrix with $m<n$ and $b\in\mathbb{R}^m$. The support of $x\in\mathbb{R}^n$ is $\operatorname{supp}(x)=\{i: x_i\ne 0\}$. For an integer $r\ge 0$, a sparse solution of $Ax=b$ is an $x$ with $Ax=b$ and $|\operatorname{supp}(x)|\le r$. The $\ell_1$-norm is $\|x\|_1=|x_1|+\dots+|x_n|$.

Basis pursuit is the optimization problem

$$\text{(BP)}\qquad\text{minimize } \|x\|_1\ \text{ subject to } x\in\mathbb{R}^n,\ Ax=b,$$

which is equivalent to the linear program

$$\text{(BP}'\text{)}\qquad\text{minimize } u_1+\dots+u_n\ \text{ subject to } Ax=b,\ -u\le x\le u,\ u\ge 0 .$$

The matrix $A$ is BP-exact for $r$ if for every $b\in\mathbb{R}^m$: whenever $Ax=b$ has a solution $\tilde x$ with at most $r$ nonzero components, $\tilde x$ is the unique optimal solution of (BP). The crosspolytope is $B^n_1=\{x:\|x\|_1\le 1\}$, the kernel of $A$ is $L=\{x: Ax=0\}$, and $L+z=\{\ell+z:\ell\in L\}$. For $z$ with $\|z\|_1=1$, the cone at $z$ is $C_z=\{t(x-z): t\ge 0,\ x\in B^n_1\}$, and $L$ is good for $z$ if $(L+z)\cap B^n_1=\{z\}$.

Formalization targets

Goal: Lemma 8.5.4 (reformulation of BP-exactness)

For $m<n$ and $r\le m$:

$$A \text{ is BP-exact for } r\iff \forall z\in\mathbb{R}^n\ \text{with}\ \|z\|_1=1,\ |\operatorname{supp}(z)|\le r:\quad (L+z)\cap B^n_1=\{z\}.$$

This is the book's geometric characterization of exact recovery, and the statement on which the known probabilistic proofs are built.

Milestones

1. Observation 8.5.1: $Ax=b$ has at most one sparse solution for every $b$ if and only if every $2r$ or fewer columns of $A$ are linearly independent.
2. The remark after it (p. 169): under $m<n$, that column condition forces $m\ge 2r$.
3. Equivalence of (BP) and (BP′) (p. 170): in every optimal solution of (BP′), $u_i=|x_i|$; and $x$ is optimal for (BP) iff $(x,|x|)$ is optimal for (BP′).
4. From the proof of Lemma 8.5.4 (p. 173): if $Az=b$, the solution set of $Ax=b$ is exactly $L+z$.
5. From "Intuition for BP-exactness" (p. 174): for $\|z\|_1=1$ and $|\operatorname{supp}(z)|\le r$, $L$ is good for $z$ iff $L\cap C_z=\{0\}$.

Further draft item: Theorem 8.5.2

With $m=\lfloor 0.75n\rfloor$, $r=\lfloor 0.08n\rfloor$ and $A$ an $m\times n$ matrix of independent $N(0,1)$ entries, there is a constant $c>0$ such that for every $n$

$$\Pr[A \text{ is BP-exact for } r]\ \ge\ 1-e^{-cm}.$$

The book states this without proof. It is included as a separate theorem, not a milestone of the goal.

Significance

Lemma 8.5.4 converts an algorithmic property, that an $\ell_1$ linear program returns a prescribed sparse vector for every right-hand side, into a purely geometric property of the kernel of $A$ relative to the low-dimensional faces of the crosspolytope. With milestone 5 it becomes the statement that $L$ avoids a finite family of cones, which is where union bounds over faces and estimates for random subspaces enter. Observation 8.5.1 separates what is information-theoretically possible (uniqueness of sparse solutions) from what is computationally achievable by linear programming; finding a sparse solution directly is NP-hard in general. Theorem 8.5.2 is the quantitative payoff: a fixed fraction of arbitrary gross errors can be corrected by solving one linear program.

All of these results are proved in the literature; Lemma 8.5.4, Observation 8.5.1 and the milestones are elementary, and Theorem 8.5.2 rests on Donoho's polytope-neighborliness analysis. The platform has a related formalization of Wainwright's restricted nullspace property (Theorem 7.8 of High-Dimensional Statistics, namespace HighDimStat.SparseLinear), which fixes a support set $S$ rather than characterizing exactness for all $r$-sparse vectors through the crosspolytope. A machine-checked proof of Theorem 8.5.2 with the constants $0.75$ and $0.08$ is, to our knowledge, not available anywhere; it would require substantial Gaussian and high-dimensional geometry infrastructure.

Difficulty

For the goal and milestones the difficulty is bookkeeping, not ideas: the scaling between a sparse solution $\tilde x$ and the boundary point $\tilde x/\|\tilde x\|_1$, the case $\tilde x=0$, and the fact that BP-exactness quantifies over all right-hand sides $b$ while the geometric side quantifies over boundary points of the crosspolytope.

Theorem 8.5.2 is of a different order. A union bound over the $\binom{n}{r}2^r$ faces of dimension $r-1$ reduces it to bounding the probability that a random $(n-m)$-dimensional subspace meets one cone $C_F$ nontrivially, and getting that probability small enough to beat the combinatorial factor with the stated numerical constants is the hard part. Rough asymptotic estimates do not give $0.08$ at $\alpha=0.75$.

Formalization scope

Vectors are functions Fin n → ℝ (the book's indices $1,\dots,n$ become $0,\dots,n-1$) and matrices are Matrix (Fin m) (Fin n) ℝ. The $\ell_1$-norm is written out as $\sum_i|x_i|$, since Mathlib's norm on Fin n → ℝ is the sup norm. The support is a Finset of indices. Optimality in (BP) and (BP′) is stated against every feasible point; no infimum is taken, so an empty or unbounded feasible set cannot create a spurious optimum. "Every $2r$ or fewer columns" ranges over finsets of distinct column indices, column $j$ being Aᵀ j. The hypotheses $m<n$ and $r\le m$ of Lemma 8.5.4 are kept as on the page, although the equivalence does not use them; $m<n$ is also the standing assumption of §8.5 needed for $m\ge 2r$.

In Theorem 8.5.2 the random matrix has the product law of independent gaussianReal 0 1 entries, the constant $c>0$ is quantified before $n$, and measurability of the BP-exact event is part of the conclusion, so the bound concerns a genuine probability rather than an outer measure.

A trivializing formalization is ruled out: BP-exactness requires uniqueness among all minimizers for every right-hand side, not just optimality of $\tilde x$, and the crosspolytope condition is an equality of sets, not an inclusion that $z$ alone would satisfy.

All definitions live in one module (MatousekLP.SparseRecovery.BasisPursuit); the $\ell_1$ and support vocabulary is reusable for later sparse-recovery missions. Contributions are welcome on every milestone, on the goal, and on the infrastructure towards Theorem 8.5.2 (Gaussian measures on matrix spaces, measurability of the BP-exact event, the face structure of the crosspolytope).

Selected references

• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.5. https://doi.org/10.1007/978-3-540-30717-4
• S. S. Chen, D. L. Donoho and M. A. Saunders, Atomic decomposition by basis pursuit, SIAM J. Sci. Comput. 20(1), 1999, 33–61. https://doi.org/10.1137/S1064827596304010
• E. J. Candès, M. Rudelson, T. Tao and R. Vershynin, Error correction via linear programming, Proc. 46th IEEE FOCS, 2005, 295–308. https://doi.org/10.1109/SFCS.2005.5464411
• D. L. Donoho, High-dimensional centrally symmetric polytopes with neighborliness proportional to dimension, Discrete Comput. Geom. 35, 2006, 617–652. https://doi.org/10.1007/s00454-005-1220-0
• N. Linial and I. Novik, How neighborly can a centrally symmetric polytope be?, Discrete Comput. Geom. 36, 2006, 273–281. https://doi.org/10.1007/s00454-006-1235-1

Motivation

A binary error-correcting code is a set of $n$-bit words chosen so that the words stay distinguishable after a few bits have been corrupted in transmission. A code can correct any $r$ errors exactly when every two of its words differ in at least $2r+1$ positions. The more words the code has, the more information each transmitted block carries. So the central quantitative question of coding theory is how large a code of given length and minimum distance can be. Codes are used in every technology that transmits or stores data, from disks and phones to deep-space probes.

In 1973 Philippe Delsarte showed that an upper bound on this maximum size is the optimum value of an explicit linear program (Delsarte, An algebraic approach to the association schemes of coding theory, Philips Res. Repts. Suppl. 10, 1973). The bound was far stronger than the classical volume argument and remains a standard tool. This mission formalizes the self-contained proof of the bound in §8.4 of Matoušek and Gärtner's textbook (Springer 2007). That proof follows Best, Brouwer, MacWilliams, Odlyzko and Sloane (IEEE Trans. Inform. Theory 24, 1978). The mission also covers the step of Delsarte's original argument that the book isolates as a lemma.

Timeline.

• 1950: Hamming introduces single-error-correcting codes and the sphere-packing bound.
• 1973: Delsarte proves the linear programming bound using association schemes.
• 1978: Best et al. give the elementary parity proof and small improvements, among them $A(17,3) \le 6552$.
• 2005: Schrijver replaces the linear program by a semidefinite program and improves many entries of the code tables (IEEE Trans. Inform. Theory 51).

Setting

A word is $\mathbf w = (w_1,\dots,w_n) \in \{0,1\}^n$, and a code is any set $C \subseteq \{0,1\}^n$. The Hamming distance $d_H(\mathbf w,\mathbf w')$ is the number of positions $j$ with $w_j \ne w'_j$. The weight $|\mathbf w|$ is the number of ones in $\mathbf w$. The word $\mathbf w \oplus \mathbf w'$ is the entrywise sum modulo 2. For $I \subseteq \{1,\dots,n\}$, the restricted distance $d^I_H(\mathbf w,\mathbf w')$ counts only the differing positions that lie in $I$.

A code has distance $d$ if $d_H(\mathbf w,\mathbf w') \ge d$ for all distinct $\mathbf w,\mathbf w' \in C$ (Definition 8.4.1). The quantity $A(n,d)$ is the maximum of $|C|$ over all codes $C \subseteq \{0,1\}^n$ with distance $d$.

For $0 \le i,t \le n$ the Krawtchouk numbers are

$$K_t(n,i) = \sum_{j=0}^{\min(i,t)} (-1)^j \binom ij \binom{n-i}{t-j}.$$

The distance distribution of a code $C$ is

$$\tilde x_i(C) = \frac{1}{|C|}\,\bigl|\{(\mathbf w,\mathbf w')\in C^2 : d_H(\mathbf w,\mathbf w') = i\}\bigr|, \qquad i=0,\dots,n.$$

The Delsarte linear program has variables $x_0,\dots,x_n$. It maximizes $x_0+\dots+x_n$ subject to:

• $x_0 = 1$;
• $x_i = 0$ for $1 \le i \le d-1$;
• $\sum_{i=0}^n K_t(n,i)\,x_i \ge 0$ for $1 \le t \le n$;
• $x \ge 0$.

For Delsarte's original argument, $M_i$ is the $2^n\times 2^n$ matrix whose $(\mathbf v,\mathbf w)$ entry is $1$ when $d_H(\mathbf v,\mathbf w) = i$ and $0$ otherwise. The weights are $\tilde y_i = |\{(\mathbf w,\mathbf w')\in C^2 : d_H = i\}| / (2^n\binom ni)$.

Formalization targets

Goal: Theorem 8.4.3 (the Delsarte bound)

$$A(n,d) \;\le\; \max\Bigl\{\textstyle\sum_{i=0}^n x_i \;:\; x \text{ feasible for the Delsarte program}\Bigr\}\quad\text{for all } n, d.$$

The goal is stated against every upper bound $v$ of the objective on the feasible set. No particular optimum value is fixed, so the statement covers every $n$ and $d$ at once.

Milestones, in attack order

1. Lemma 8.4.5. For every $I$ and $C$, the pairs in $C^2$ with even $d^I_H$ are at least as many as the pairs with odd $d^I_H$.
2. Corollary 8.4.6. $\sum_{(\mathbf w,\mathbf w')\in C^2}(-1)^{(\mathbf w\oplus\mathbf w')^T\mathbf v}\ge 0$ for every $\mathbf v$.
3. Proposition 8.4.4. $\sum_{i=0}^n K_t(n,i)\,\tilde x_i(C) \ge 0$ for every $C$ and every $t = 1,\dots,n$.
4. §8.4, p. 160. The values $\tilde x_i(C)$ sum to $|C|$. For a nonempty code with distance $d$, the vector $\tilde x(C)$ is feasible for the program.
5. Lemma 8.4.2 (sphere-packing bound). $A(n,2r+1) \le \lfloor 2^n / \sum_{i=0}^r\binom ni\rfloor$.
6. Lemma 8.4.7. $\tilde M = \sum_{i=0}^n \tilde y_i M_i$ is positive semidefinite.

Significance

The Delsarte bound turns an extremal problem over the $2^{2^n}$ subsets of the cube into a linear program with $n+1$ variables. For $A(17,3)$ it gives $6553$, while the sphere-packing bound gives $7281$. Many entries of the standard code tables rest on this bound or its refinements. The positive semidefiniteness in Lemma 8.4.7 is the starting point of the semidefinite programming bounds of Schrijver and of later work. The same framework also underlies the linear programming bounds for spherical codes and sphere packings.

The theorem is classical and fully proved in the literature. Neither Mathlib nor this platform has a formal statement or proof of it. Mathlib has Hamming distance and binomial coefficients, but it has no $A(n,d)$, no Krawtchouk numbers and no LP bound for codes. This mission would produce the first formal statement and proof. It would also produce reusable identities on Krawtchouk sums and character sums over $\{0,1\}^n$.

Difficulty

Two of the program's constraints are immediate once $\tilde x_i$ is defined: $\tilde x_0 = 1$, and $\tilde x_i = 0$ for $i < d$. The difficulty lies in the Krawtchouk constraints. They do not follow from counting pairs at a single distance. They require a sign-weighted count over all words of weight $t$, and the sum must then be regrouped by the distance of each pair. That regrouping identifies a count of words, split by how many ones they share with a fixed word, with the Krawtchouk number. Formally this is an exchange of finite sums together with a binomial counting identity, and the index bookkeeping, including the range $j \le \min(i,t)$, has to be exact.

The obvious attempt proves the inequality one distance class at a time. It fails because the individual terms $K_t(n,i)\,\tilde x_i$ have no sign. Only the whole sum is nonnegative.

Formalization scope

• Words and codes. Words are Fin n → Bool, with bit $1$ as true. The book's positions $1,\dots,n$ become 0, …, n-1. Codes are Finsets of words, and $d_H$ is Mathlib's hammingDist.
• The maximum $A(n,d)$. $A(n,d)$ is a Finset.sup over the finite family of codes with distance $d$. This family contains the empty code, so the maximum is attained.
• Krawtchouk numbers. $K_t(n,i)$ is an integer, and its natural-number subtractions are honest for $i \le n$ and $j \le t$.
• LP variables and the $x_i = 0$ constraints. The LP variables are indexed by Fin (n+1) with no index shift. The constraints $x_i = 0$ are imposed for $1 \le i < d$, so they are vacuous for $d \le 1$.
• The empty code. Lean's convention $1/0 = 0$ gives $\tilde x(\emptyset) = 0$. Proposition 8.4.4 then holds trivially, and the feasibility milestone carries the hypothesis $C \ne \emptyset$ that the book's division presupposes.
• The sphere-packing floor. The floor in the sphere-packing bound is natural-number division by a denominator that is at least $1$.
• Positive semidefiniteness. This is Mathlib's Matrix.PosSemidef over $\mathbb R$.

No trivialization. The goal is not stated as "$A(n,d) \le \sup$" with a real supremum, which Lean would evaluate to $0$ on an empty or unbounded set. Its hypothesis ranges over upper bounds of a feasible program: $(1,0,\dots,0)$ is always feasible, so the hypothesis is never vacuous.

Contributions welcome. Useful lemmas include:

• Krawtchouk identities, for example $\sum_{t}K_t(n,i) = 2^n[i=0]$ and $K_i(n,t)\binom ni = K_t(n,i)\binom nt$;
• counting words of weight $t$ that meet a fixed support in exactly $j$ positions;
• general facts on character sums $\sum_{\mathbf w\in C}(-1)^{\mathbf w^T\mathbf v}$.

These are reusable for other LP and SDP bounds in coding theory.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.4. https://doi.org/10.1007/978-3-540-30717-4
• P. Delsarte, An algebraic approach to the association schemes of coding theory, Philips Research Reports Supplements 10, 1973.
• M. R. Best, A. E. Brouwer, F. J. MacWilliams, A. M. Odlyzko, N. J. A. Sloane, Bounds for binary codes of length less than 25, IEEE Trans. Inform. Theory 24 (1978), 81–93. https://doi.org/10.1109/TIT.1978.1055827
• A. Schrijver, New code upper bounds from the Terwilliger algebra and semidefinite programming, IEEE Trans. Inform. Theory 51 (2005), 2859–2866. https://doi.org/10.1109/TIT.2005.851748

Why zero-sum games belong in a linear programming course

A two-player zero-sum game models any situation in which one party's gain is exactly the other party's loss: a military allocation in the spirit of Colonel Blotto, a sealed-bid contest, rock–paper–scissors. The central question is what each player should do when the opponent is also reasoning about them. John von Neumann answered it in 1928 with the minimax theorem (von Neumann 1928): each player has a strategy guaranteeing the same number, the value of the game, whatever the opponent does. The theorem underlies modern game theory, robust decision making, and the analysis of online learning algorithms, where regret bounds are routinely derived from it.

Section 8.1 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007) presents the theorem as an application of linear programming duality. This mission is the sixth of a series formalizing the capstone results of the book.

Setting

Alice has $m \ge 1$ pure strategies and Bob has $n \ge 1$. A real $m \times n$ payoff matrix $M = (m_{ij})$ records Alice's gain, and Bob's loss, when Alice plays her $i$th and Bob his $j$th pure strategy. A mixed strategy of Alice is a probability vector $\mathbf x \in \mathbb R^m$, $\sum_i x_i = 1$, $\mathbf x \ge \mathbf 0$; a mixed strategy of Bob is a probability vector $\mathbf y \in \mathbb R^n$. When the players randomize independently, Alice's expected payoff is

$$\mathbf x^T M \mathbf y = \sum_{i,j} m_{ij} x_i y_j .$$

The worst-case payoffs are

$$\beta(\mathbf x) = \min_{\mathbf y} \mathbf x^T M \mathbf y, \qquad \alpha(\mathbf y) = \max_{\mathbf x} \mathbf x^T M \mathbf y,$$

over mixed strategies. A mixed strategy of Bob is a best response against $\mathbf x$ if it minimizes $\mathbf x^T M\mathbf y$; a mixed strategy of Alice is a best response against $\mathbf y$ if it maximizes it. A pair $(\tilde{\mathbf x}, \tilde{\mathbf y})$ is a mixed Nash equilibrium (Definition 8.1.1) if each is a best response against the other. Alice's $\tilde{\mathbf x}$ is worst-case optimal if $\beta(\tilde{\mathbf x}) = \max_{\mathbf x} \beta(\mathbf x)$; Bob's $\tilde{\mathbf y}$ is worst-case optimal if $\alpha(\tilde{\mathbf y}) = \min_{\mathbf y}\alpha(\mathbf y)$.

The proof in the book passes through three linear programs: the dual of (8.1), which for a fixed $\mathbf x$ maximizes $x_0$ subject to $M^T \mathbf x - \mathbf 1 x_0 \ge \mathbf 0$; program (8.2), the same with $\mathbf x$ as variables subject to $\sum_i x_i = 1$, $\mathbf x \ge \mathbf 0$; and program (8.4), which minimizes $y_0$ subject to $M \mathbf y - \mathbf 1 y_0 \le \mathbf 0$, $\sum_j y_j = 1$, $\mathbf y \ge \mathbf 0$.

Formalization targets

Goal: Theorem 8.1.3 (minimax theorem for zero-sum games)

For every $m \times n$ payoff matrix with $m, n \ge 1$: worst-case optimal mixed strategies exist for both players; for any worst-case optimal $\tilde{\mathbf x}$ of Alice and $\tilde{\mathbf y}$ of Bob, the pair $(\tilde{\mathbf x}, \tilde{\mathbf y})$ is a mixed Nash equilibrium; and there is a single number $v$, the value of the game, with

$$\beta(\tilde{\mathbf x}) = \tilde{\mathbf x}^T M \tilde{\mathbf y} = \alpha(\tilde{\mathbf y}) = v$$

for every such pair. The third clause is what distinguishes the theorem from the existence of some saddle point.

Milestones

1. $\beta$ and $\alpha$ are attained minima and maxima (p. 135).
2. Lemma 8.1.2(i): $\beta(\mathbf x) \le \mathbf x^T M \mathbf y \le \alpha(\mathbf y)$ for all mixed $\mathbf x, \mathbf y$, hence $\max_{\mathbf x}\beta \le \min_{\mathbf y}\alpha$.
3. Lemma 8.1.2(ii): both strategies of a mixed Nash equilibrium are worst-case optimal.
4. Lemma 8.1.2(iii): $\beta(\tilde{\mathbf x}) = \alpha(\tilde{\mathbf y})$ implies that $(\tilde{\mathbf x}, \tilde{\mathbf y})$ is a mixed Nash equilibrium.
5. The dual of (8.1) has optimal value $\beta(\mathbf x)$ (p. 137).
6. Eq. (8.3): an optimal solution $(\tilde x_0, \tilde{\mathbf x})$ of (8.2) satisfies $\tilde x_0 = \beta(\tilde{\mathbf x}) = \max_{\mathbf x}\beta(\mathbf x)$.
7. Eq. (8.5): an optimal solution $(\tilde y_0, \tilde{\mathbf y})$ of (8.4) satisfies $\tilde y_0 = \alpha(\tilde{\mathbf y}) = \min_{\mathbf y}\alpha(\mathbf y)$.
8. Programs (8.2) and (8.4) both have optimal solutions, and their optimum values coincide (p. 138).
9. The minimax equality (p. 137):

$$\max_{\mathbf x}\min_{\mathbf y}\mathbf x^T M \mathbf y = \min_{\mathbf y}\max_{\mathbf x}\mathbf x^T M \mathbf y .$$

Significance

The theorem gives a complete prescription for zero-sum play: a worst-case optimal strategy secures at least the value against any opponent, and a worst-case optimal opponent holds the player to at most the value, so both players can announce their strategies in advance without loss. With Lemma 8.1.2(ii) it yields a characterization: a pair of mixed strategies is a Nash equilibrium if and only if both are worst-case optimal. The minimax equality is used downstream in online learning (regret-to-value arguments), in robust optimization, and in Yao's principle for randomized algorithms.

The mathematics is classical and proved; what this mission adds is a machine-checked version in the book's own formulation. The platform already has AGT.zero_sum_minimax (Algorithmic Game Theory I), which proves the existence of a saddle point, and the general FamousTheorems.sion_minimax_theorem. Neither states that every pair of worst-case optimal strategies is an equilibrium with a common value, and neither exhibits the LP route: the dual of (8.1), the programs (8.2) and (8.4), and their duality. The mission records that route statement by statement, so that it can be reused as a worked instance of LP duality.

Difficulty

Lemma 8.1.2 is routine; the entire content is the reverse inequality $\max_{\mathbf x}\beta(\mathbf x) \ge \min_{\mathbf y}\alpha(\mathbf y)$. The obvious attack, maximizing $\beta$ directly, fails because $\beta$ is a minimum of linear functions and hence not linear, so its maximization is not a linear program as written. The obstacle is removed only by an appeal to LP duality in the proof, together with the facts that the simplices are nonempty and compact, and that the relevant programs are feasible and bounded so that optima exist. None of this is supplied by the pure-strategy structure of the game: pure Nash equilibria need not exist (rock–paper–scissors has none).

Formalization scope

Pure strategies are indexed by Fin m and Fin n, with the book's standing assumption $m, n \ge 1$ carried as hypotheses 1 ≤ m, 1 ≤ n by every theorem; the book's indices $1,\dots,m$ become $0,\dots,m-1$. Mixed strategies are Mathlib's stdSimplex ℝ (Fin m), the payoff is x ⬝ᵥ (M *ᵥ y). $\beta(\mathbf x)$ is the real sInf and $\alpha(\mathbf y)$ the real sSup of the payoffs over the opponent's simplex; milestone 1 states that these are attained. A mixed Nash equilibrium is defined in the verbal form of Definition 8.1.1 (mutual best responses). Worst-case optimality is defined against all mixed strategies, never as a saddle-point condition, so the goal is not circular with Lemma 8.1.2(iii). LP optimality is stated as "feasible and at least as good as every feasible point", so no supremum over a possibly empty or unbounded feasible set is used.

The book's clause that worst-case optimal strategies "can be efficiently computed by linear programming" is algorithmic and is not part of the formal statement; there is no complexity model. A goal asserting only the existence of worst-case optimal strategies, or only the existence of some equilibrium, would drop the theorem's third clause and is ruled out: the common value $v$ is quantified before all pairs of worst-case optimal strategies.

A complete development needs compactness of the standard simplex, continuity of the bilinear payoff, and a strong duality theorem for linear programs in the form of the programs (8.2)/(8.4); the latter is reusable across the whole series. Proofs by other routes (Sion's theorem, a separating hyperplane argument, fixed points) are welcome for the goal; the LP milestones stand on their own as statements about the programs.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.1, pp. 131–142. https://doi.org/10.1007/978-3-540-30717-4
• J. von Neumann, "Zur Theorie der Gesellschaftsspiele", Mathematische Annalen 100 (1928), 295–320. https://doi.org/10.1007/BF01448847
• M. Sion, "On general minimax theorems", Pacific Journal of Mathematics 8 (1958), 171–176. https://doi.org/10.2140/pjm.1958.8.171

Motivation

Every finite algorithm for linear programming rests on one structural fact: if a linear program has an optimum at all, it has one at a point singled out by finitely many linear conditions. The simplex method walks between such points, and exact complexity analyses, sensitivity analysis and integrality arguments all start from them. Chapter 4 of J. Matoušek and B. Gärtner, Understanding and Using Linear Programming (Springer, 2007, DOI 10.1007/978-3-540-30717-4), establishes this fact for linear programs in equational form, in the definitions that the rest of the book (the simplex method of Chapter 5, duality in Chapter 6, the applications in Chapter 8) uses.

This mission is the second of a series formalizing that book. It fixes the book's notion of a basic feasible solution and of a vertex, and targets the theorem that optimal solutions exist whenever the program is feasible and bounded, and can then be chosen basic.

Setting

A linear program in equational form is

$$\text{maximize } c^{T}x \quad\text{subject to}\quad Ax=b,\ x\ge 0,$$

where $A$ is a real $m\times n$ matrix, $b\in\mathbb{R}^m$, $c\in\mathbb{R}^n$, and $x\ge 0$ means every coordinate of $x$ is nonnegative. A feasible solution is an $x\in\mathbb{R}^n$ satisfying both constraints; the set of them is $P$. An optimal solution is a feasible $x$ with $c^{T}y\le c^{T}x$ for every feasible $y$. The objective is bounded from above if some real $M$ satisfies $c^{T}x\le M$ for all feasible $x$.

Throughout Section 4.2 the book assumes that $A$ has $n\ge m$ columns and rank $m$ (its rows are linearly independent). For $S\subseteq\{1,\dots,n\}$, $A_S$ denotes the matrix formed by the columns of $A$ with indices in $S$. A basis is an $m$-element set $B$ for which $A_B$ is nonsingular, i.e. its columns are linearly independent. A basic feasible solution is a feasible $x$ for which some basis $B$ has $x_j=0$ for every $j\notin B$.

A point $v$ is a vertex of $P$ if $v\in P$ and some nonzero $c\in\mathbb{R}^n$ satisfies $c^{T}v>c^{T}y$ for every $y\in P\setminus\{v\}$: $v$ is the unique maximizer over $P$ of a nonzero linear function.

Formalization targets

Goal: Theorem 4.2.3 (p. 46)

For $A$ of rank $m$ with $n\ge m$,

$$\Bigl(P\neq\emptyset\ \wedge\ \exists M\ \forall x\in P,\ c^{T}x\le M\Bigr)\ \Longrightarrow\ \exists\,x^{*}\ \text{optimal},$$ $$\exists\,x^{*}\ \text{optimal}\ \Longrightarrow\ \exists\,\tilde x\ \text{optimal and basic feasible}.$$

Both parts are one theorem, as in the book. Part (i) says optimal solutions fail to exist only for the two obvious reasons, infeasibility and unboundedness; part (ii) says an optimum can always be found among basic feasible solutions.

Milestones

1. Lemma 4.2.1 (p. 45): a feasible $x$ is basic if and only if the columns of $A_K$ are linearly independent, where $K=\{j : x_j>0\}$.
2. Proposition 4.2.2 (p. 45): for a basis $B$ there is at most one feasible solution vanishing outside $B$.
3. The statement proved inside the proof of Theorem 4.2.3 (p. 47): if the objective is bounded above, every feasible $x_0$ is dominated by a basic feasible $\tilde x$, $c^{T}\tilde x\ge c^{T}x_0$.
4. Theorem 4.4.1 (p. 54): a point of $P$ is a vertex of $P$ if and only if it is a basic feasible solution.

Significance

Theorem 4.2.3 gives a finite, if impractical, algorithm for linear programming: enumerate the at most $\binom{n}{m}$ sets $B$, solve $A_Bx_B=b$, and keep the best nonnegative solution. It is the correctness backbone of the simplex method, which visits basic feasible solutions in a smarter order, and it is the source of the book's claim that a feasible and bounded linear program has an optimal solution. Theorem 4.4.1 identifies this algebraic notion with the geometric corners of the feasible polyhedron, which is what makes statements such as "the LP relaxation has an integral vertex" in later chapters meaningful.

All of these results are classical and fully proved in the book. The value of formalizing them here is the definition layer: later missions of this series (Bland's rule, the central path, the scheduling application) state their results about bases and basic feasible solutions in exactly these definitions, and a proved Theorem 4.2.3 in this form lets them import the existence of an optimal basic solution instead of re-deriving it. Related facts are already machine-checked on Prove2Me in the formulation of Bertsimas and Tsitsiklis (Introduction to Linear Optimization I and II: minimization over polyhedra $\{x : a_i^{T}x\ge b_i\}$, extreme points, basic solutions as $n$ active linearly independent constraints). Those statements concern a different presentation of the program and a different notion of basic solution; connecting them to the equational-form statements here is itself a welcome contribution.

Difficulty

The obvious argument for part (i), "a continuous function on a closed set bounded above attains its supremum", fails: the feasible set is usually unbounded, and a linear function bounded above on an unbounded closed convex set need not obviously attain its supremum without using the polyhedral structure. The existence of an optimum is exactly the nontrivial content of part (i); compactness is not available.

For milestone 1, the delicate direction is the converse: a set of linearly independent columns indexed by $K$ must be completed to an $m$-element basis, which requires the rank-$m$ assumption. For Theorem 4.4.1, the direction from vertex to basic feasible solution is not local: a vertex is defined by an optimization property, while basicness is a statement about the support of the point.

Formalization scope

All items live in the namespace MatousekLP.BFS and share one definition module, MatousekLP.BFS.EquationalForm. Conventions:

• vectors are Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ; the book's indices $1,\dots,n$ are 0, …, n-1;
• $Ax=b$ is A *ᵥ x = b, $x\ge 0$ is 0 ≤ x (pointwise), $c^{T}x$ is c ⬝ᵥ x;
• a subset $B$ of indices is a Finset (Fin n); "$A_B$ nonsingular" is linear independence over $\mathbb{R}$ of the family of columns of $A$ indexed by the elements of $B$, together with B.card = m;
• the standing assumption of §4.2 is the pair of hypotheses m ≤ n and A.rank = m on every theorem;
• "optimal" and "bounded from above" are stated against every feasible point. No real supremum over the feasible set appears anywhere, so an empty or unbounded feasible set cannot make a statement hold through a default value;
• "vertex" is the book's unique-maximizer definition of p. 53, not Mathlib's Set.extremePoints; the book's remark on p. 55 that the two coincide is not used as a definition;
• Theorem 4.4.1 carries the extra hypothesis $n\ge 1$: for $n=0$ there is no nonzero vector in $\mathbb{R}^0$, the single feasible point $0$ is basic but not a vertex, and the book's equivalence fails.

A formalization in which "optimal" were defined through sSup of the objective over the feasible set would make part (ii) trivially true or false on unbounded programs; the definitions here rule that out. Dropping the rank hypothesis would make part (ii) false (no basis exists when the rows are dependent), so it is not optional.

Reusable infrastructure: the column-restriction and basis vocabulary, the support set $K$, and the extension of a linearly independent set of columns to a basis of the column space are needed again in the simplex chapter. Proofs of any milestone, and bridges to Mathlib's Set.extremePoints or to the Bertsimas–Tsitsiklis statements on the platform, are welcome.

Selected references

• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Universitext, Springer, 2007, Chapter 4, pp. 41–56. https://doi.org/10.1007/978-3-540-30717-4
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 2.
• G. M. Ziegler, Lectures on Polytopes, Graduate Texts in Mathematics 152, Springer, 1995. https://doi.org/10.1007/978-1-4613-8431-1

Motivation

A b-matching with upper bounds in a graph $G=(V,E)$ assigns a nonnegative integer $x_e\le d_e$ to every edge so that the edges at each node $i$ carry at most $b_i$ in total. Maximizing a linear objective over such assignments is an integer program that contains ordinary matching ($b\equiv 1$, $d\equiv 1$) and appears in assignment, transportation and scheduling models with capacities on both nodes and arcs. Edmonds and Johnson showed that the integer hull of this system is described by adding the blossom (matching) inequalities to the linear relaxation (Edmonds–Johnson 1970; cited in the paper as [8], [13]). There are exponentially many blossom inequalities, so a cutting-plane method needs a separation procedure: given a fractional point $\bar x$, find a violated blossom inequality or certify that none exists.

M. W. Padberg and M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Mathematics of Operations Research 7 (1982), gave this procedure. Section 1 of the paper computes a minimum-capacity cut with an odd number of odd-labelled nodes in polynomial time; Sections 2 and 3 reduce blossom separation to that computation. This mission formalizes Section 3, the case with upper bounds $d$. The companion mission Odd Minimum Cut-Sets and b-Matchings 1 formalizes Section 1.

Timeline: Edmonds (1965) describes the perfect matching polytope; Edmonds and Johnson (1970) extend the description to capacitated $b$-matching; Gomory and Hu (1961) give the cut-tree that Section 1 of Padberg–Rao relies on; Padberg and Rao (1982) reduce separation to odd minimum cuts. Later work (Letchford, Reinelt and Theis, 2008) shortened the resulting algorithms; the reduction itself is the one stated here.

Setting

Let $G=(V,E)$ be a finite simple undirected graph, $b\in\mathbb Z_{>0}^V$ and $d\in\mathbb Z_{>0}^E$. The system is

$$Ax\le b,\qquad x\le d,\qquad x\ge 0, \tag{3.1}$$

with $A$ the node–edge incidence matrix. For $W\subseteq V$ write $E(W)$ for the edges with both ends in $W$ and $(W:V-W)$ for the cut-set of $W$, the edges with exactly one end in $W$. For $T\subseteq (W:V-W)$ with $b(W)+d(T)=\sum_{i\in W}b_i+\sum_{e\in T}d_e$ odd, the blossom inequality is

$$x(W)+x(T)=\sum_{e\in E(W)}x_e+\sum_{e\in T}x_e\le \tfrac12\bigl(b(W)+d(T)-1\bigr). \tag{3.3}$$

Let $\bar x$ be a real point feasible for (3.1) and $\bar s=b-A\bar x$ its node slacks. Let $E(\bar x)$ be the edges with $\bar x_e>0$. The labelled weighted graph $G(\bar x,d)$ has nodes $V$, a special node $S$, and one new node $i_e$ for each $e\in E(\bar x)$. For each such edge $e=[i,j]$, where $i$ is the end the construction scans first, it has an edge $[i,i_e]$ of weight $d_e-\bar x_e$ and an edge $[i_e,j]$ of weight $\bar x_e$. Each $i\in V$ is joined to $S$ with weight $\bar s_i$. There are no other edges. A node $i_e$ is odd iff $d_e$ is odd; $S$ is odd iff $b(V)$ is odd; a node $i\in V$ is odd iff $b_i$ plus the $d_e$ of the subdivided edges scanned from $i$ is odd. A node set $U$ is odd when it contains an odd number of odd nodes, and $\bar y(U:\tilde V-U)$ denotes the total weight of the edges leaving $U$ (its cut capacity).

Formalization targets

Goal: Theorem 3.1

For every feasible $\bar x$ and every scan order,

$$\exists\,W\subseteq V,\ T\subseteq (W:V-W):\ b(W)+d(T)\text{ odd},\ \bar x(W)+\bar x(T)>\tfrac12\bigl(b(W)+d(T)-1\bigr)$$ $$\Longleftrightarrow\quad \exists\,U\subseteq \tilde V \text{ odd}:\ \bar y(U:\tilde V-U)<1 .$$

The paper's closing sentence, that $W$ and $T$ can be obtained constructively from the proof of Lemma 3.2, describes the proof and is not part of the formal statement.

Milestones

1. Eq. (3.6): $2x(W)+x(W:V-W)+x(T)+s(W)+t(T)=b(W)+d(T)$ for $T\subseteq(W:V-W)$, with $t=d-x$.
2. Eq. (3.7): $\bar x$ violates (3.3) for $(W,T)$ iff $\bar x(W:V-W)+d(T)-2\bar x(T)+\bar s(W)<1$.
3. Lemma 3.1: if $T\subseteq (W:V-W)\cap E(\bar x)$ and $b(W)+d(T)$ is odd, some odd $U$ with $S\notin U$ has $\bar y(U:\tilde V-U)$ equal to the left side of (3.7) (Eq. (3.8)).
4. Lemma 3.2: every odd $U$ with $S\notin U$ and capacity $<1$ arises this way from some $(W,T)$ with $b(W)+d(T)$ odd.

Significance

Theorem 3.1 is what makes the blossom inequalities of capacitated $b$-matching usable in a linear-programming based cutting-plane method: combined with the odd minimum cut algorithm of Section 1, it separates them in polynomial time. By the equivalence of separation and optimization, it also yields a polynomial-time algorithm for capacitated $b$-matching through the ellipsoid method. The paper notes the further consequence that every odd cut-set of capacity less than one, not only a minimum one, gives a violated inequality.

The results are proved in the 1982 paper; none of them has a machine-checked proof that this mission is aware of. What the mission adds is a formal statement of the graph $G(\bar x,d)$ and of the reduction, and a checked proof of it. The definitions of the capacitated $b$-matching system, its blossom inequalities and the subdivided graph are reusable for later work on matching polytopes and on the uncapacitated case of Section 2.

Difficulty

The identities (3.6) and (3.7) are bookkeeping over incidences. The substance is the correspondence between node sets $W$ with complemented edge sets $T$ and odd node sets $U$ of $G(\bar x,d)$. In one direction the right $U$ must pick, for every cut edge, the side of $i_e$ that makes the edge contribute $\bar x_e$ or $d_e-\bar x_e$ as (3.7) requires, and its parity must be computed through the orientation-dependent labels. In the other direction an arbitrary odd cut of capacity below one must be shown to have this shape; this uses $d_e\ge 1$ to exclude every other position of a new node $i_e$, and it uses the evenness of the total label to pass from an odd set containing $S$ to its complement. A point $\bar x$ whose blossom violation uses an edge $e\in T$ with $\bar x_e=0$ has no new node for $e$. Such a $T$ has to be ruled out, and the argument uses the capacity bound. It is not an assumption of the theorem.

Formalization scope

The graph is a Mathlib SimpleGraph V on a finite type with decidable adjacency; edges are elements of G.edgeFinset : Finset (Sym2 V). The data are b : V → ℕ and d : Sym2 V → ℕ, positive on nodes and on edges, and a real point x : Sym2 V → ℝ. Feasibility means the linear relaxation of (3.1); integrality of $\bar x$ is not assumed. All halves and differences are computed in ℝ. When $W=V$ the cut-set is empty, so the paper's convention "$T$ is empty" holds automatically.

$G(\bar x,d)$ is fixed by definitions from $(G,b,d,\bar x)$ and an orientation tail choosing the end of each edge scanned first; every theorem quantifies over the orientation. The node type is Option V ⊕ {e // e ∈ E(x̄)}, with none the special node $S$. Weights are a symmetric function on nodes with $0$ meaning "no edge". The labels are given in closed form. The paper assigns them by a sequential scan that flips the parity of the scanned end by $d_e$, and addition mod 2 does not depend on the order of the scan. "The cut capacity of an odd minimum cut-set is less than one" is stated as "some odd cut has capacity less than one"; the two agree, and the formulation avoids a minimum over a possibly empty family.

Two trivializing formalizations are ruled out: $G(\bar x,d)$ is constructed, not an arbitrary labelled graph assumed to satisfy (3.8); and no infimum over odd cuts is taken, since a real sInf of an empty family is $0$ and would make the right side true when no odd cut exists.

Contributions welcome: proofs of the milestones, lemmas on cut capacities of symmetric weight functions on finite types, and parity bookkeeping for labelled node sets.

Selected references

• M. W. Padberg, M. R. Rao, Odd Minimum Cut-Sets and b-Matchings, Mathematics of Operations Research 7(1), 67–80, 1982. https://doi.org/10.1287/moor.7.1.67
• J. Edmonds, E. L. Johnson, Matching: a well-solved class of integer linear programs, in Combinatorial Structures and Their Applications, Gordon and Breach, 89–92, 1970; reprinted in Combinatorial Optimization — Eureka, You Shrink!, LNCS 2570, 27–30, 2003. https://doi.org/10.1007/3-540-36478-1_3
• R. E. Gomory, T. C. Hu, Multi-terminal network flows, Journal of the SIAM 9(4), 551–570, 1961. https://doi.org/10.1137/0109047
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B, 125–130, 1965. https://doi.org/10.6028/jres.069B.013
• A. N. Letchford, G. Reinelt, D. O. Theis, Odd minimum cut sets and b-matchings revisited, SIAM Journal on Discrete Mathematics 22(4), 1480–1487, 2008. https://doi.org/10.1137/060664793