All missions

Motivation

A binary classifier is judged by its misclassification probability, the chance that it mislabels a fresh example. That probability is unknown; what a learner sees is the training error, the fraction of mistakes on the sample it was trained on. A generalization bound controls the gap between the two simultaneously for every classifier in a class, so that a classifier chosen by looking at the data still has a guaranteed error. The classical bounds of Vapnik and Chervonenkis measure the class by its VC dimension, a fixed combinatorial quantity that does not depend on the data distribution, and the paper recalls evidence that such fixed complexity penalties cannot be universally effective for model selection (p. 464).

Bartlett and Mendelson's paper in the Journal of Machine Learning Research (2002) studies two data-dependent alternatives, the Rademacher and Gaussian complexities, and proves risk bounds and structural rules for them. This mission formalizes the paper's classification bound, Theorem 5(b), which replaces the VC penalty by half the Rademacher complexity of the class. The source is the published JMLR article (jmlr.org/papers/v3/bartlett02a), pp. 463–482; all page numbers below are the journal's.

Timeline. Uniform convergence of empirical frequencies with a VC-dimension rate is due to Vapnik and Chervonenkis (1971). Rademacher penalties for model selection were introduced by Koltchinskii (2001) and by Bartlett, Boucheron and Lugosi (2002), who also proved Theorem 5(a) with the maximum discrepancy. The 2002 paper proves part (b) in Appendix B (p. 480) by adapting its proof of the general risk bound, Theorem 8 (p. 467).

Setting

Let $\mathcal X$ be a measurable space and $P$ a probability distribution on $\mathcal X \times \{\pm 1\}$; a pair $(X, Y) \sim P$ is an example $X$ with label $Y$. Let $F$ be a set of $\{\pm 1\}$-valued functions on $\mathcal X$ (the classifiers), and let $(X_i, Y_i)_{i=1}^n$ be an i.i.d. sample drawn from $P^n$.

• The misclassification probability of $f \in F$ is $P(Y \ne f(X))$.
• The training error of $f$ is $\hat P_n(Y \ne f(X)) = \frac1n \#\{i : Y_i \ne f(X_i)\}$, where $\hat P_n$ is the empirical measure of the sample (p. 463).
• Let $\sigma_1, \dots, \sigma_n$ be independent uniform $\{\pm 1\}$-valued random variables, independent of the sample. The empirical Rademacher complexity of a class $G$ of real functions on $\mathcal X$ at the points $x_1, \dots, x_n$ is

$$\hat R_n(G)(x) = \mathbb E_\sigma \sup_{g \in G}\Big|\frac2n \sum_{i=1}^n \sigma_i\, g(x_i)\Big|,$$

and the Rademacher complexity is $R_n(G) = \mathbb E\, \hat R_n(G)(X_1, \dots, X_n)$ with $X_1, \dots, X_n$ i.i.d. (Definition 2, p. 464). Note the factor $2/n$ and the absolute value.

• In Theorem 5, $R_n(F)$ is the Rademacher complexity of $F$ itself, viewed as a class of real functions with values $\pm1$, under the marginal of $P$ on $\mathcal X$.
• With the 0–1 loss $\mathcal L(Y, f(X)) = \mathbf 1(Y \ne f(X))$, the largest gap on a sample is $\Phi = \sup_{h \in \mathcal L \circ F}(\mathbb E h - \hat{\mathbb E}_n h) = \sup_{f\in F}\big(P(Y \ne f(X)) - \hat P_n(Y \ne f(X))\big)$.

Formalization targets

Goal: Theorem 5(b), p. 465

For every $0 < \delta < 1$, with probability at least $1 - \delta$ over the sample, every $f \in F$ satisfies

$$P(Y \ne f(X)) \le \hat P_n(Y \ne f(X)) + \frac{R_n(F)}{2} + \sqrt{\frac{\ln(1/\delta)}{2n}} .$$

The bound is uniform: the probability that some $f$ violates it is at most $\delta$.

Milestones (Appendix B, p. 480)

1. Bounded differences. Replacing one example changes $\Phi$ by at most $1/n$.
2. McDiarmid step. With probability at least $1-\delta$, every $f \in F$ satisfies

$$P(Y \ne f(X)) \le \hat P_n(Y \ne f(X)) + \mathbb E\,\Phi + \sqrt{\frac{\ln(1/\delta)}{2n}} .$$

3. Symmetrization. $\mathbb E\,\Phi \le R_n(F)/2$.

Supporting platform items, referenced and not restated: McDiarmid's inequality for i.i.d. samples (StabGen.Uniform.mcdiarmid_inequality, open) and the symmetrization lemma in the normalization of Shalev-Shwartz and Ben-David (UnderstandingML.representativeness_le_rademacher, proved).

Significance

The result. Theorem 5(b) is a distribution-dependent risk bound for classification whose complexity term can be estimated from a single sample. The paper shows (Theorem 6, p. 465) that it is never much worse than the VC bound, since the empirical Rademacher complexity of a $\{\pm1\}$ class is $O(\sqrt{d/n})$ in terms of its empirical VC dimension $d$, and it can be much better. It also serves as the template for margin bounds for large-margin classifiers, kernel machines and voting methods in Section 4 of the paper.

Formalizing it. The result is proved in the paper; no machine-checked proof is known to exist. A formal proof needs McDiarmid's inequality, a symmetrization argument with a ghost sample, and the reduction of the 0–1 loss class to the classifier class through the identity $\mathbf 1(Y \ne f(X)) = (1 - Y f(X))/2$. The milestones split these, so they can be proved independently. The symmetrization milestone also corrects a printed slip (see Formalization scope).

Difficulty

The bounded-difference step and the final union of the two halves are short. The difficulty is in the symmetrization. The supremum over an uncountable class is not automatically measurable, so the expectations in the paper's chain need not exist as written; a proof must work with exactly the random variables it integrates and use only the measurability it is given. The exchange of a sample point with its ghost copy, the conditioning on the sample, and the replacement of $\sigma_i Y_i$ by $\sigma_i$ must each be justified on finite sign averages and product measures. The obvious shortcut, bounding the gap by the Rademacher complexity of the loss class $\mathcal L \circ F$, does not give the stated term: with the absolute value of Definition 2, the loss class's complexity is not $R_n(F)/2$, because $(1 - Y_i f(X_i))/2$ contributes a sign sum that does not depend on $f$.

Formalization scope

Lean conventions:

• Labels $\{\pm1\}$ are the units $\mathbb Z^\times = \{1, -1\}$, coerced to $\mathbb R$; the real class of $F$ is $\{x \mapsto (f(x) : \mathbb R)\}$. Sample indices are $0, \dots, n-1$; the sample law is the product measure $P^n$.
• The Rademacher complexities take values in $[0, \infty]$: the sign expectation is the exact average over the $2^n$ sign vectors, and the sample expectation is a lower Lebesgue integral. An unbounded class therefore has complexity $+\infty$, not a junk $0$. The goal compares values in $[0,\infty]$ with ENNReal.ofReal on the real terms.
• "With probability at least $1-\delta$, every $f$ in $F$" is encoded as: the outer $P^n$-measure of $\{S : \exists f \in F,\ \text{the bound fails}\}$ is at most $\delta$.

Hypotheses added relative to the page, each necessary or a reading of the page:

• $n \ge 1$: at $n = 0$ Lean's $2/0 = 0$ makes $R_0(F) = 0$ and the bound false.
• $0 < \delta < 1$, as in Theorem 8 (p. 467).
• Every $f \in F$ is measurable, and three random variables are measurable: the gap supremum $\Phi$, the double-sample supremum $(S, S') \mapsto \sup_f(\hat P'_n - \hat P_n)(Y \ne f(X))$, and $x \mapsto \hat R_n(F)(x)$. The paper does not discuss measurability; these are exactly the variables the proof integrates, as in the proved platform item UnderstandingML.representativeness_le_rademacher. They hold, for instance, for countable classes.
• The two intermediate milestones assume $F$ nonempty, so that the real suprema in them are genuine.

Corrected slip: the chain on p. 480 ends "$= \mathbb E \sup_f \frac1n\sum_i\sigma_i f(X_i) = R_n(F)/2$". The last equality is only "$\le$": $R_n$ carries an absolute value, and for $F = \{f\}$ the left side of that step is $0$ while $R_n(F)/2 > 0$. The symmetrization milestone states the chain's conclusion with $\le$, which is all Theorem 5(b) needs.

Not a valid formalization: a version with a real-valued supremum or Bochner integral for $R_n$ (which would read $0$ on an unbounded or non-integrable class and make the bound false or free), one that drops the absolute value or uses the $1/n$ normalization, or one that measures $R_n$ of the loss class instead of $F$. Theorem 5(a) (maximum discrepancy, due to Bartlett, Boucheron and Lugosi) is not part of this mission.

Contributions welcome: proofs of the three milestones and the goal; the general McDiarmid inequality (the referenced open item); and reusable lemmas on measurable suprema of classifier families.

Selected references

• P. L. Bartlett, S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3 (2002) 463–482. https://www.jmlr.org/papers/v3/bartlett02a.html
• P. L. Bartlett, S. Boucheron, G. Lugosi, Model selection and error estimation, Machine Learning 48 (2002) 85–113. https://doi.org/10.1023/A:1013999503812
• V. Koltchinskii, Rademacher penalties and structural risk minimization, IEEE Transactions on Information Theory 47(5) (2001) 1902–1914. https://doi.org/10.1109/18.930926
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics 1989, LMS Lecture Note Series 141, 148–188. https://doi.org/10.1017/CBO9781107359949.008
• V. N. Vapnik, A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and its Applications 16 (1971) 264–280. https://doi.org/10.1137/1116025

Motivation

A learning algorithm picks a predictor $f$ from a class $F$ after looking at $n$ training examples, and the quantity of interest is its expected loss on a fresh example. Since $f$ depends on the data, its training error is a biased estimate of that loss, and a risk bound quantifies the bias uniformly over the class: with high probability, every $f \in F$ has expected loss at most an observable sample average plus a complexity penalty. Classical penalties (VC dimension, covering numbers, fat-shattering dimension) are fixed in advance; data-dependent penalties such as the Rademacher complexity can be estimated from the sample itself and adapt to the distribution, which matters for model selection by complexity regularization.

Bartlett and Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results (JMLR 3, 2002, jmlr.org), state such a bound in a general decision-theoretic setting (Theorem 8, p. 467): the loss is any $[0,1]$-valued function of an outcome and an action, and the sample average is taken of a dominating cost $\phi \ge \mathcal L$, which may be Lipschitz and hence amenable to the structural results of the paper's §3 even when $\mathcal L$ is a discontinuous $0$–$1$ loss. Multiclass classification with error-correcting output codes is the paper's example. The ingredients — McDiarmid's inequality (McDiarmid, 1989) and symmetrization — are standard; the paper combines them for this setting with a centred cost class. The source is the published JMLR article (pp. 463–482); all page numbers below are its printed pages.

Setting

Let $\mathcal X$ be an input space, $\mathcal Y$ an output space and $\mathcal A$ an action space with a distinguished action $0 \in \mathcal A$, each a measurable space. A probability measure $P$ on $\mathcal X \times \mathcal Y$ generates independent examples $(X_1, Y_1), \dots, (X_n, Y_n)$, and $(X, Y)$ is a fresh draw from $P$.

• A loss is $\mathcal L : \mathcal Y \times \mathcal A \to [0,1]$; a cost $\phi : \mathcal Y \times \mathcal A \to [0,1]$ dominates it if $\phi(y,a) \ge \mathcal L(y,a)$ for all $y, a$.
• $F$ is a class of maps $\mathcal X \to \mathcal A$; the expected loss of $f$ is $\mathbf E\mathcal L(Y, f(X)) = \int \mathcal L(y, f(x))\, dP(x,y)$.
• The empirical mean of $h : \mathcal X \times \mathcal Y \to \mathbb R$ is $\hat{\mathbf E}_n h = \frac1n\sum_{i=1}^n h(X_i, Y_i)$.
• The centred cost class is $\tilde\phi\circ F = \{(x,y) \mapsto \phi(y, f(x)) - \phi(y, 0) : f \in F\}$.
• For a class $G$ of real functions on a space $\mathcal Z$ and a sample $z_1, \dots, z_n$, the empirical Rademacher complexity is

$$\hat R_n(G) = \mathbf E_\sigma \sup_{g \in G}\Bigl|\frac2n\sum_{i=1}^n \sigma_i g(z_i)\Bigr|,$$

with $\sigma_1, \dots, \sigma_n$ independent uniform signs, and the Rademacher complexity is $R_n(G) = \mathbf E\hat R_n(G)$, the expectation over an i.i.d. sample (Definition 2, p. 464). The factor is $2/n$ and the absolute value is inside the supremum.

In Lean these are RadGauss.RiskBound.empiricalRademacher, rademacherComplexity, empMean, supDev (the uniform deviation $\sup_{h \in G}(\mathbf Eh - \hat{\mathbf E}_nh)$), doubleSupDev and phiTildeComp.

Formalization targets

Goal: Theorem 8 (p. 467)

For every integer $n \ge 1$ and every $0 < \delta < 1$, with probability at least $1-\delta$ over the sample, every $f \in F$ satisfies

$$\mathbf E\mathcal L(Y, f(X)) \le \hat{\mathbf E}_n\phi(Y, f(X)) + R_n(\tilde\phi\circ F) + \sqrt{\frac{8\ln(2/\delta)}{n}} .$$

The event is uniform over $F$. The constant $\sqrt 8$ is the printed one.

Milestones (the steps of the paper's proof)

1. Theorem 9 (McDiarmid's inequality), p. 467: for independent, not necessarily identically distributed $X_i$ and $f$ with bounded differences $c_i$,

$$P\{f(X_1,\dots,X_n) - \mathbf Ef(X_1,\dots,X_n) \ge t\} \le e^{-2t^2/\sum_i c_i^2}.$$

2. Bounded differences, p. 467: replacing one example changes $\sup_{h \in \tilde\phi\circ F}(\mathbf Eh - \hat{\mathbf E}_nh)$ by at most $2/n$.
3. Concentration, p. 467: with probability at least $1 - \delta/2$,

$$\sup_{h}(\mathbf Eh - \hat{\mathbf E}_nh) \le \mathbf E\sup_{h}(\mathbf Eh - \hat{\mathbf E}_nh) + \sqrt{2\ln(2/\delta)/n}.$$

4. Combined bound, p. 468: with probability at least $1-\delta$, for all $f \in F$,

$$\mathbf E\mathcal L(Y, f(X)) \le \hat{\mathbf E}_n\phi(Y, f(X)) + \mathbf E\sup_{h \in \tilde\phi\circ F}(\mathbf Eh - \hat{\mathbf E}_nh) + \sqrt{8\ln(2/\delta)/n}.$$

5. Symmetrization, p. 468:

$$\mathbf E\sup_{h \in \tilde\phi\circ F}(\mathbf Eh - \hat{\mathbf E}_nh) \le R_n(\tilde\phi\circ F).$$

The platform's Proved UnderstandingML.representativeness_le_rademacher (Shalev-Shwartz and Ben-David, Lemma 26.2) is included as a supporting reference: it is the middle inequality of milestone 5 in the $1/n$, absolute-value-free normalization.

Significance

Theorem 8 bounds the expected loss of any predictor in the class, including one selected by the data, by quantities the learner can compute or estimate: the empirical cost and the Rademacher complexity of the centred cost class, which concentrates around its empirical version. Combined with the paper's structural results (§3: contraction by Lipschitz maps, convex hulls, sums), it yields margin bounds for voting methods, neural networks and kernel machines (§4) from complexities of simple base classes. Centring by $\phi(y,0)$ matters: with the absolute value inside the supremum, $R_n(\phi\circ F)$ can exceed $R_n(\tilde\phi\circ F)$ by order $1/\sqrt n$ even for a single function.

The result is proved in the paper. As far as the platform's catalog shows, it has no machine-checked proof in this normalization; McDiarmid's inequality in the non-identically distributed form, the $2/n$ bounded-difference step and the absolute-value Rademacher symmetrization with factor $2/n$ are not on the platform. A Lean proof would give a reusable risk-bound template for any loss dominated by a bounded cost.

Difficulty

The obvious argument — bound $\mathbf E\phi(Y,f(X)) - \hat{\mathbf E}_n\phi(Y,f(X))$ for a fixed $f$ by Hoeffding's inequality — does not survive the choice of $f$ after seeing the data: the deviation must be controlled uniformly over $F$, and $F$ is typically infinite. The supremum over $F$ is a single random variable, but its expectation is not obviously small, and relating it to the Rademacher complexity requires a ghost sample and a sign-swap symmetry of the product measure. In a formal development, the supremum of an uncountable family is not automatically measurable; the expectations the argument manipulates must be genuine, not lower integrals, which is why the statements carry explicit measurability hypotheses. McDiarmid's inequality itself, for independent but not identically distributed coordinates, is a martingale-difference concentration argument that is not in Mathlib in this form.

Formalization scope

• Sample and law. A sample is S : Fin n → X × Y, its law the product Measure.pi (fun _ => P). "With probability at least $1-\delta$, every $f \in F$ satisfies …" is encoded by bounding the (outer) measure of $\{S \mid \exists f \in F,\ \neg\,\text{bound}\}$ by $\delta$, with $0 < \delta < 1$.
• Complexities in $[0,\infty]$. $\hat R_n$ is an average over all $2^n$ sign vectors (Fin n → Bool, true $= +1$) of $[0,\infty]$-valued suprema; $R_n$ is its Lebesgue integral. The goal is stated in $[0,\infty]$, with the real terms embedded by ENNReal.ofReal (all are nonnegative). A real supremum or a Bochner integral would silently return $0$ on an unbounded class or a non-integrable integrand, making the bound trivially false or vacuous; this is ruled out by the choice of codomain.
• Added hypotheses, all implicit in the paper. $n \ge 1$ (at $n = 0$ Lean's $1/0 = 0$ makes the bound read $\mathbf E\mathcal L \le 0$, which is false); measurability of $\mathcal L$, $\phi$ and every $f \in F$; a distinguished action $0$ ([Zero A]).
• Measurability guard. The goal and milestones 3–5 assume measurability of exactly the random variables the proof integrates: the uniform deviation $S \mapsto \sup_{h \in \tilde\phi\circ F}(\mathbf Eh - \hat{\mathbf E}_nh)$, the empirical Rademacher complexity $S \mapsto \hat R_n(\tilde\phi\circ F)$, and the double-sample deviation $(S,S') \mapsto \sup_h(\frac1n\sum_i h(S'_i) - \hat{\mathbf E}_nh)$. These hold, for example, for countable $F$; the same guard is used by UnderstandingML.representativeness_le_rademacher.
• No printed slip was found in the statements formalized here. In Theorem 9, if every $c_i = 0$ the printed exponent has a zero denominator; Lean reads it as $0$ and the bound as $1$, which is true.
• Not formalized: the paper's Theorem 10 and the applications; this mission covers Definition 2 and §2 up to the end of the proof of Theorem 8.

Contributions welcome: a proof of McDiarmid's inequality for Measure.pi (reusable well beyond this mission), the ghost-sample symmetrization with the sign-swap invariance of $P^n \otimes P^n$, and the final assembly.

Selected references

• P. L. Bartlett and S. Mendelson, Rademacher and Gaussian Complexities: Risk Bounds and Structural Results, Journal of Machine Learning Research 3 (2002), 463–482. https://www.jmlr.org/papers/v3/bartlett02a.html
• C. McDiarmid, On the method of bounded differences, Surveys in Combinatorics 1989, London Math. Soc. Lecture Note Series 141, Cambridge University Press, 148–188. https://doi.org/10.1017/CBO9781107359949.008
• S. Shalev-Shwartz and S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 26. https://doi.org/10.1017/CBO9781107298019
• V. Koltchinskii and D. Panchenko, Empirical margin distributions and bounding the generalization error of combined classifiers, Annals of Statistics 30 (2002), 1–50. https://doi.org/10.1214/aos/1015362183

Motivation

Expander graphs are sparse graphs in which every set of vertices has many neighbours. Families of them with bounded degree and expansion bounded away from zero are a basic tool of theoretical computer science: they are the main component of the sorting network of Ajtai, Komlós and Szemerédi (AKS 1983), the building block of superconcentrators and other graphs with strong connectivity properties, and an ingredient of many later constructions in coding theory, derandomization and complexity.

Expansion is hard to certify. Checking that every set of vertices has many neighbours means looking at exponentially many sets, and computing the exact expansion of a graph is coNP-complete. A spectral quantity, by contrast, is computable in polynomial time. N. Alon's paper Eigenvalues and expanders (Combinatorica 6 (1986) 83–96) proves that for regular bipartite graphs the two notions are equivalent: a graph is a strong expander if and only if the second-smallest eigenvalue of its Laplacian is bounded away from 0, with explicit constants in both directions. This is a discrete counterpart of Cheeger's inequality for Riemannian manifolds.

Timeline.

• 1983: Ajtai, Komlós and Szemerédi use bounded-degree bipartite expanders to build sorting networks of depth $O(\log n)$.
• 1984: Tanner (SIAM J. Alg. Disc. Meth. 5) bounds the neighbourhood size of a set in a regular bipartite graph by its second eigenvalue, the direction "eigenvalue gap implies expansion".
• 1985: Alon and Milman (J. Combin. Theory Ser. B 38) prove isoperimetric inequalities for graphs in terms of $\lambda(G)$ and introduce enlargers.
• 1986: Alon proves the converse direction, "expansion implies an eigenvalue gap" (Lemma 2.4 and Theorem 3.4 of the paper).

Setting

All graphs are finite and simple. For a graph $G = (V, E)$ and a set $X \subseteq V$, $N(X) = \{v \in V : vx \in E \text{ for some } x \in X\}$ is the set of neighbours of $X$; it may meet $X$.

The Laplacian of $G$ is $Q_G = \mathrm{diag}(d(v))_{v \in V} - A_G$, where $A_G$ is the 0–1 adjacency matrix and $d(v)$ the degree of $v$. It is symmetric with eigenvalues $0 = \lambda_0 \le \lambda_1 \le \dots \le \lambda_{n-1}$, counted with multiplicity, and $\lambda(G) = \lambda_1$ is its second-smallest eigenvalue. It is positive exactly when $G$ is connected.

• An $(n, d, c)$-magnifier is a graph on $n$ vertices with maximal degree $d$ in which every $X \subseteq V$ with $|X| \le n/2$ satisfies $|N(X) - X| \ge c|X|$.
• An $(n, d, \varepsilon)$-enlarger is a graph on $n$ vertices with maximal degree $d$ and $\lambda(G) \ge \varepsilon$.
• A bipartite graph $G = (I, O; E)$ has inputs $I$, outputs $O$ and edges only between $I$ and $O$. It is a strong $(n, d, c)$-expander if $|I| = |O| = n$, the maximal degree is $d$, and for every $X \subseteq I$

$$|N(X)| \ge \Bigl(1 + c\Bigl(1 - \frac{|X|}{n}\Bigr)\Bigr)|X|.$$

Formalization targets

Goal: Theorem 3.4

Let $G = (I, O; E)$ be a $d$-regular bipartite graph with $|I| = |O| = n$ and $\lambda = \lambda(G)$.

1. If $G$ is a strong $(n, d, c)$-expander then

$$\lambda \ge \frac{c^2}{1024 + 2c^2}.$$

2. If $\lambda \ge \varepsilon$ then $G$ is a strong $(n, d, c)$-expander with

$$c = \frac{2d\varepsilon - \varepsilon^2}{d^2}.$$

Milestones, in the order of the paper

• Lemma 2.2 (Alon–Milman, already on the platform): for disjoint sets $A, B$ at distance $\varrho > 1$, $b \le (1-a)/(1 + (\lambda/d)a\varrho^2)$.
• Corollary 2.3: every $(n, d, \varepsilon)$-enlarger is an $(n, d, 2\varepsilon/(d+2\varepsilon))$-magnifier.
• Eq. (2.1): if $f$ is an eigenvector of $Q_G$ for $\lambda(G)$ and $g$ its positive part, then $\sum_{uv \in E}(g(u)-g(v))^2 \le \lambda \sum_v g^2(v)$.
• Lemma 2.4: every $(n, d, c)$-magnifier has $\lambda(G) \ge c^2/(4 + 2c^2)$.
• Lemma 3.1: a strong $(n, d, c)$-expander is a $(2n, d, c/16)$-magnifier.
• Proof of Lemma 3.3, spectrum: the two largest eigenvalues of $C^TC$, with $C$ the $I \times O$ biadjacency matrix, are $d^2$ and $(d - \lambda)^2$.
• Proof of Lemma 3.3, Tanner's bound: $|N(X)| \ge d^2|X| / \bigl(\alpha(d^2 - (d-\lambda)^2) + (d-\lambda)^2\bigr)$ with $\alpha = |X|/n$.
• Lemma 3.3: a $d$-regular bipartite graph is a strong $(n, d, (2d\lambda - \lambda^2)/d^2)$-expander.

Part (1) of the goal combines Lemmas 3.1 and 2.4; part (2) follows from Lemma 3.3.

Significance

The result. Theorem 3.4 makes expansion of regular bipartite graphs checkable in polynomial time up to a constant-factor loss. A random regular bipartite graph can be generated and its expansion certified by computing one eigenvalue. Lemma 2.4 is one of the first discrete Cheeger inequalities. Together with Corollary 2.3 it shows that magnifiers and enlargers are the same graphs up to the constants, and it underlies the later theory of spectral expanders, including the Alon–Boppana bound and Ramanujan graphs.

The formalization. The results are proved in the paper. The work is to formalize the known proofs. That includes Tanner's eigenvalue bound, which the paper only cites, and a max-flow min-cut argument, for which Mathlib has no general theorem. No machine-checked version of Lemma 2.4, Lemma 3.1, Lemma 3.3 or Theorem 3.4 is known to exist. Lemma 2.2 is already stated and proved on the platform as part of the Alon–Milman mission.

Difficulty

The direction "eigenvalue gap implies expansion" is a variational argument on the spectrum of $C^TC$. The converse is the hard one. A first attempt bounds $\lambda(G)$ from below by testing the Rayleigh quotient on indicator vectors of sets. That only gives upper bounds on $\lambda$: any one test vector does. A lower bound has to control every vector orthogonal to the constants at once. The paper first reduces to the positive part of an eigenvector (Eq. (2.1)). It then turns the combinatorial expansion of the graph into an analytic inequality for that function, using a network flow whose existence comes from the max-flow min-cut theorem. Step (ii) of the flow conditions printed on p. 87 is false as stated: the arcs $(u, u)$ of the network absorb part of the flow. The flow argument has to be repaired before it can be formalized.

Lemma 3.1 has its own obstacle: one-sided expansion of inputs must be converted into expansion of arbitrary vertex sets that mix inputs and outputs. This needs the strong form of expansion; for ordinary expanders the lemma is false.

Formalization scope

Graphs are SimpleGraph V on a Fintype. A bipartite graph lives on the sum type I ⊕ O, and IsIOBipartite forbids edges inside I and inside O. Cardinalities $|N(X)|$ are Set.ncard. "Maximal degree $d$" is read as G.maxDegree ≤ d; every statement is monotone in $d$ or fixes $d$ by regularity (G.IsRegularOfDegree d). The condition $|X| \le n/2$ is written $2|X| \le n$ in $\mathbb{N}$. All constants are real, and every subtraction and division is taken in $\mathbb{R}$.

Reused published items:

• $\lambda(G)$ is AlonMilman.Diameter.lambda1, the second-smallest eigenvalue of G.lapMatrix ℝ, which is $0$ by convention on fewer than two vertices.
• $N(X)$ is AKSSorting.Core.neighbours.
• Lemma 2.2 is AlonMilman.Diameter.theorem_2_5, which carries Alon–Milman's standing hypotheses that $G$ is connected and $n \ge 2$; outside them the inequality is trivial.

The page omits a few degenerate cases, and the following hypotheses are added for them. Each is necessary, with a counterexample recorded in the item's statement:

• $n \ge 1$ and $c \ge 0$ in Theorem 3.4 (1);
• $\varepsilon > 0$ in Theorem 3.4 (2);
• $n \ge 2$ and $c \ge 0$ in Lemma 2.4;
• $n \ge 2$ in Lemma 3.1 and in the $C^TC$ statement;
• $d \ge 1$ in Lemma 3.3;
• $\varepsilon \ge 0$ in Corollary 2.3.

Eq. (2.1) is stated in multiplied form, so no quotient by $\sum g^2$ appears.

The closing sentences of Theorem 2.5 and Theorem 3.4 ("Thus … one can prove efficiently …") are not formalized. Read as implications between expanders they reduce to monotonicity in $c$, because $c' \le c$; their content is algorithmic.

Several encodings would trivialize the mission and are excluded:

• a $\lambda$ other than the published second-smallest Laplacian eigenvalue, in particular one defined as the best constant of a quotient;
• expansion or magnifier conditions with a negative constant in a hypothesis;
• $|X| \le n/2$ with truncating natural-number division.

Contributions are welcome:

• Tanner's bound in Lean, which is reusable for any regular bipartite graph;
• a max-flow min-cut theorem for finite networks;
• the corrected flow lemma behind Eqs. (2.2)–(2.3);
• the spectral facts about $\lambda(G)$ for bipartite graphs ($\lambda \le d$ for $n \ge 2$, and $\lambda = d - \sigma_2(C)$).

Selected references

• N. Alon, Eigenvalues and expanders, Combinatorica 6 (1986) 83–96. https://doi.org/10.1007/BF02579166
• N. Alon and V. D. Milman, λ₁, isoperimetric inequalities for graphs, and superconcentrators, J. Combin. Theory Ser. B 38 (1985) 73–88. https://doi.org/10.1016/0095-8956(85)90092-9
• R. M. Tanner, Explicit concentrators from generalized N-gons, SIAM J. Algebraic Discrete Methods 5 (1984) 287–293. https://doi.org/10.1137/0605030
• M. Ajtai, J. Komlós and E. Szemerédi, Sorting in c log n parallel steps, Combinatorica 3 (1983) 1–19. https://doi.org/10.1007/BF02579338

Motivation

Every linear program comes with a second linear program, its dual, whose feasible solutions certify bounds on the optimum of the first. The duality theorem of linear programming says that these certificates are perfect: when both programs are feasible, the best bound equals the optimum. The theorem underlies the analysis of the simplex method, sensitivity analysis and shadow prices in operations research, the minimax theorem for zero-sum games, max-flow/min-cut and König-type min-max theorems in combinatorial optimization, and the primal–dual design of approximation and online algorithms.

The Farkas lemma, a theorem of the alternative for linear systems, contains the essence of duality: a system of linear equations or inequalities either has a (nonnegative) solution, or a single linear combination of its rows proves that it has none. It goes back to Farkas (1902) and Minkowski's work on finitely generated cones; the duality theorem itself is due to von Neumann (1947) and Gale, Kuhn and Tucker (1951).

This mission formalizes Chapter 6 of Matoušek and Gärtner's textbook Understanding and Using Linear Programming (Springer, 2007): the duality theorem in the book's form, weak duality, the Farkas lemma in its algebraic, geometric and three-variant forms, and the lemmas of two self-contained proofs of the Farkas lemma, one analytic (nearest points in finitely generated cones) and one via minimally infeasible systems.

Setting

Let $A$ be a real matrix with $m$ rows and $n$ columns, $b\in\mathbb{R}^m$, $c\in\mathbb{R}^n$. Vector inequalities are componentwise. The primal and dual linear programs are

$$\text{(P)}\quad\max\ c^{T}x \ \text{ s.t. } Ax\le b,\ x\ge 0, \qquad\qquad \text{(D)}\quad\min\ b^{T}y \ \text{ s.t. } A^{T}y\ge c,\ y\ge 0.$$

A feasible solution of (P) is an $x\in\mathbb{R}^n$ satisfying its constraints; an optimal solution is a feasible $x^*$ with $c^{T}x\le c^{T}x^*$ for every feasible $x$. (P) is unbounded if its objective takes arbitrarily large values on feasible solutions. For the minimization (D) the notions are mirrored: an optimal $y^*$ has $b^{T}y^*\le b^{T}y$ for all feasible $y$, and (D) is unbounded if $b^{T}y$ takes arbitrarily small values.

For $a_1,\dots,a_n\in\mathbb{R}^m$, the convex cone generated by them is $C=\{t_1a_1+\dots+t_na_n : t_i\ge 0\}$; a primitive cone is one generated by $k\le m$ linearly independent vectors. A system $Ax\le b$ of $m$ inequalities is minimally infeasible if it has no solution but dropping any one inequality makes it solvable.

Formalization targets

Goal: the duality theorem (§6.1, p. 83)

For (P) and (D) as above, exactly one of the following occurs:

1. neither (P) nor (D) is feasible;
2. (P) is unbounded and (D) is infeasible;
3. (P) is infeasible and (D) is unbounded;
4. both are feasible; then both have optimal solutions, and every optimal $x^*$ of (P) and optimal $y^*$ of (D) satisfy

$$c^{T}x^*=b^{T}y^*.$$

Milestones

• Proposition 6.1.1 (weak duality). $c^{T}x\le b^{T}y$ for all feasible $x$ of (P) and $y$ of (D); hence (P) unbounded forces (D) infeasible, and (D) unbounded forces (P) infeasible.
• Proposition 6.4.1 (Farkas lemma). Exactly one of: $Ax=b$ has a solution $x\ge 0$; some $y$ has $y^{T}A\ge 0^{T}$ and $y^{T}b<0$. Already on the platform as LinearOptimization.farkas_lemma (Proved) and linked as a reference.
• Proposition 6.4.3 (three variants). Solvability of $Ax=b$, $x\ge0$; of $Ax\le b$, $x\ge 0$; and of $Ax\le b$ with $x$ free, each characterized by a certificate condition on $y$.
• Proposition 6.4.2 (geometric Farkas lemma). $b$ lies in the cone generated by $a_1,\dots,a_n$, or a hyperplane through $0$ separates the cone from $b$ strictly — exactly one.
• Lemmas 6.5.4, 6.5.5, 6.5.3, 6.5.1. Primitive cones are closed; a finitely generated cone is a finite union of primitive cones; hence it is closed (6.5.3, on the platform as Polyhedral.isClosed_conicSpan, Proved); hence it has a point nearest to any $b\notin C$.
• Lemmas 6.6.2 and 6.6.1. $Ax=b$ is solvable iff every $y$ with $y^{T}A=0^{T}$ has $y^{T}b=0$; in a minimally infeasible system, for every $i$ some $\tilde x^{(i)}$ satisfies all inequalities except the $i$th with equality.

Significance

The result. The duality theorem converts optimality into feasibility: a pair $(x,y)$ of primal and dual feasible solutions with $c^{T}x=b^{T}y$ is a short, checkable certificate that both are optimal, and the theorem guarantees such a certificate exists whenever an optimum does. It classifies every primal–dual pair into four behaviours and excludes the other five combinations of feasible-bounded, unbounded and infeasible. Later chapters of the same book rest on it: the minimax theorem for zero-sum games, the integrality of bipartite matching polytopes, the LP rounding for unrelated-machine scheduling, and the Delsarte bound for codes.

Formalizing it. All results here are classical and fully proved in the book; the work is formalization. Mathlib contains a Farkas lemma for proper cones in Hilbert spaces and closedness facts for finitely generated cones, and the platform already has Bertsimas–Tsitsiklis-style duality for a general-form minimization (LinearOptimization.lp_strong_duality) and matrix Farkas lemmas. What is missing is the textbook statement in Matoušek's inequality form (P)/(D), with its four-case exclusive classification, together with the chain of named lemmas that make two different elementary proofs of the Farkas lemma machine-checkable. The analytic chain (6.5.x) and the minimally-infeasible chain (6.6.x) are reusable independently of LP.

Difficulty

Weak duality is a two-line computation. The difficulty is entirely in the reverse direction, that a feasible bounded (P) forces the dual to be feasible with the same value. Any proof must use something beyond linear algebra over $\mathbb{R}$: either the termination of the simplex method with an anticycling rule, a topological fact (a finitely generated cone is closed), or an extremal argument (an optimal solution of an auxiliary LP). The naive geometric argument — take the nearest point of the cone to $b$ — fails without closedness, and closedness of the cone generated by a set is false for infinitely generated cones (the cone over a disc touching the origin is an open half-plane plus a point), so finiteness has to be used, which is the role of the primitive-cone decomposition. In the four-case theorem itself, the remaining obstacle is attainment: "bounded and feasible" must be upgraded to "an optimum exists" for both programs, which is not a consequence of Farkas-type statements alone.

Formalization scope

• Vectors are Fin n → ℝ and matrices Matrix (Fin m) (Fin n) ℝ; the book's indices $1,\dots,n$ become $0,\dots,n-1$. The row vector $y^{T}A$ is Aᵀ *ᵥ y, so $y^{T}A\ge 0^{T}$ is 0 ≤ Aᵀ *ᵥ y; scalar products are ⬝ᵥ.
• Optimal solutions and unboundedness are stated against every feasible point; no sSup/sInf is used, so no junk value of an empty or unbounded supremum enters. "Exactly one of the four cases" is ∃! k : Fin 4, DualityCase A b c k, with the book's case $k$ at index $k-1$; a plain disjunction would be weaker than the book.
• Cone items live in EuclideanSpace ℝ (Fin m), so the nearest point of Lemma 6.5.1 is Euclidean and $y^{T}x$ is the inner product. The convex cone generated by $a_1,\dots,a_n$ is the set of nonnegative combinations (it contains $0$, also for $n=0$).
• A trivializing formalization — case 4 read as "if both have optimal solutions then their values agree", which is weak duality plus nothing — is ruled out: case 4 asserts the existence of both optima from feasibility alone.
• Lemma 6.3.1 (the dual solution read off the final simplex tableau) and Lemma 6.5.2 (nearest point in a nonempty closed set, available in Mathlib as IsClosed.exists_infDist_eq_dist) are not separate targets. The Fourier–Motzkin elimination of §6.7 has no numbered result.
• Contributions welcome: proofs of any milestone, the two Farkas-lemma chains, and bridges to the general-form duality already on the platform.

Selected references

• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, Chapter 6. https://doi.org/10.1007/978-3-540-30717-4
• J. Farkas, Theorie der einfachen Ungleichungen, J. Reine Angew. Math. 124 (1902), 1–27. https://doi.org/10.1515/crll.1902.124.1
• 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.
• M. Conforti, M. Di Summa and G. Zambelli, Minimally infeasible set-partitioning problems with balanced constraints, Mathematics of Operations Research (cited in the book as to appear; the source of the proof in §6.6).
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 4.

Motivation

Many design problems in control, finance and operations research are convex programs with uncertain constraints: a decision $\theta$ must satisfy $\theta\in\Theta_\delta$ for a parameter $\delta$ that is not known in advance. Enforcing the constraint for every possible $\delta$ (robust optimization) is often intractable or too conservative, and a chance-constrained formulation needs the distribution of $\delta$, which in practice is rarely known. The scenario approach replaces the uncertain constraint by the constraints of $N$ observed samples $\delta_1,\dots,\delta_N$ and solves the resulting ordinary convex program. The question it answers is how much of the unseen uncertainty the resulting decision still violates.

The answer, the generalization theorem of the scenario approach, is distribution-free: the probability that the scenario solution violates more than a fraction $\varepsilon$ of the uncertainty is bounded by a binomial tail that depends only on $N$ and on the number $d$ of decision variables. This mission formalizes that theorem as it is presented in Chapters 3 and 5 of Campi and Garatti's textbook Introduction to the Scenario Approach (SIAM/MOS 2018), the first mission of a series on the book.

Timeline. Calafiore and Campi introduced scenario programs and bounded the violation of their solutions through the count of support constraints (Math. Program. 2005; IEEE TAC 2006). Campi and Garatti proved in 2008 that the binomial-tail bound of Theorem 3.7 holds for every convex scenario program under existence and uniqueness of the solution, and that it is attained with equality by fully supported problems (SIAM J. Optim. 2008), which settled the tightness question. The textbook (DOI 10.1137/1.9781611975444) presents the theorem with a complete proof for fully supported problems in the plane.

Setting

Fix a cost vector $c\in\mathbb R^d$, a domain $\Theta\subseteq\mathbb R^d$, a measurable space $\Delta$ of uncertainty instances with a probability $\mathbb P$, and a constraint set $\Theta_\delta\subseteq\mathbb R^d$ for each $\delta\in\Delta$.

• The violation of a decision $\theta$ (Definition 3.1) is $V(\theta)=\mathbb P\{\delta\in\Delta:\theta\notin\Theta_\delta\}$, the probability that $\theta$ fails the constraint of a fresh instance.
• For a sample $(\delta_1,\dots,\delta_m)$, the scenario program is

$$\min_{\theta\in\Theta}c^T\theta\quad\text{subject to}\quad\theta\in\bigcap_{i=1}^{m}\Theta_{\delta_i}.$$

A solution is a feasible point of least cost. With $m=N$ i.i.d. samples its solution is denoted $\theta^*$; it is a random vector, a function of the sample, and $V(\theta^*)$ is a random variable in $[0,1]$.

• Assumption 3.4 (convexity): $\Theta$ and every $\Theta_\delta$ are convex and closed. Assumption 3.6 (existence and uniqueness): for every $m$ and every sample, the program with $m$ constraints has exactly one solution.
• A constraint is a support constraint (Definition 5.1) if its removal improves the solution. A problem is fully supported (Definition 5.4) if for every $m\ge d$ the program with $m$ constraints has, with probability 1, exactly $d$ support constraints.

Formalization targets

Goal: Theorem 3.7

For $1\le d\le N$ and every $\varepsilon\in[0,1]$, under Assumptions 3.4 and 3.6,

$$\mathbb P^N\{V(\theta^*)>\varepsilon\}\le\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}.$$

The right-hand side is the upper tail of a Beta$(d,N-d+1)$ distribution. The statement leaves $\mathbb P$, $\Theta$ and the constraint family completely unspecified beyond the two assumptions.

Milestones

1. Helly's lemma (Lemma 5.3), referenced from the platform in its $d$-dimensional form.
2. Theorem 5.2: for every $m$ and every sample, a convex scenario program has at most $d$ support constraints.
3. Eq. (5.3): for a fully supported problem with $d=N=2$, $\mathbb P^2\{V(\theta^*)>\varepsilon\}=1-\varepsilon^2$.
4. Eq. (5.2): for fully supported problems, Theorem 3.7 holds with equality.
5. Eqs. (3.5)–(3.6): the bound is the Beta$(d,N-d+1)$ distribution function (a published incomplete-beta identity).
6. Eq. (3.9): $\sum_{i=0}^{d-1}\binom Ni\varepsilon^i(1-\varepsilon)^{N-i}\le 2^{d-1}(1-\varepsilon/2)^N\le2^{d-1}e^{-\varepsilon N/2}$.
7. Theorem 3.8: $\mathbb E[V(\theta^*)]\le d/(N+1)$.
8. Theorem 1.3: if $N\ge\frac2\varepsilon(\ln\frac1\beta+d-1)$, then $V(\theta^*)\le\varepsilon$ with probability at least $1-\beta$.

Significance

Theorem 3.7 is what makes the scenario approach usable as a design method: it certifies the reliability of a decision computed from data without any knowledge of the data-generating distribution, requiring only independence of the samples. Theorems 3.8 and 1.3 are its two most used consequences, an expected-violation bound and an explicit sample size, and later chapters of the book (constraint removal, the FAST algorithm, empirical-cost results) build on the same statement. Equality for fully supported problems shows that the bound cannot be improved for any $d$ and $N$.

The theorem is proved in the literature; it has no machine-checked proof. A formalization produces, beyond the result itself, a reusable library of scenario programs, violation probabilities and support constraints on which the rest of the series (constraint removal, nonconvex support sets) can be stated, and it checks the measure-theoretic content that the book deliberately leaves aside ("measurability issues are glossed over throughout", p. 33).

Difficulty

The deterministic part, at most $d$ support constraints, is a short consequence of Helly's theorem. The probabilistic part is where the obvious approach fails. A uniform-convergence argument over all $\theta$ (Vapnik–Chervonenkis theory, footnote 11 of the book) gives bounds of the wrong order and can be vacuous, because it ignores that only the solution matters. The sharp bound is an exact statement about the law of $V(\theta^*)$, not a union bound, and problems with fewer than $d$ support constraints, or with degenerate configurations of constraints, must be shown to be no worse than fully supported ones; the book treats the general case only in the plane and refers to Campi & Garatti 2008 for general $d$. Handling the null sets and the exchangeability of the samples under the product measure is a substantial part of the work.

Formalization scope

• Decisions live in EuclideanSpace ℝ (Fin d); the cost is inner ℝ c θ. A sample of size $m$ is ω : Fin m → Δ with law Measure.pi (fun _ : Fin m => P), and P is a probability measure.
• The violation is the real number (P {δ | θ ∉ Θδ δ}).toReal; probabilities of events over the sample are compared in $[0,\infty]$ through ENNReal.ofReal.
• The solution $\theta^*$ is a function θstar : (Fin N → Δ) → EuclideanSpace ℝ (Fin d) together with the hypothesis that θstar ω solves the program for every sample; it is never an arbitrary map.
• Assumption 3.6 is stated for every $m$ including $m=0$ (a unique minimizer on $\Theta$ itself) and for every sample, as on the page.
• Hypotheses the page leaves implicit are explicit: the constraint relation $\{(\theta,\delta):\theta\in\Theta_\delta\}$ is jointly measurable and θstar is measurable (the book's p. 33 convention); $\varepsilon\in[0,1]$; $d\ge1$.
• A support constraint is one whose removal leaves a feasible point of strictly smaller cost than the solution; the count is a Finset.card over Fin m.
• Theorem 3.8 asserts integrability of $V(\theta^*)$ together with the bound, so it cannot hold through the convention that a non-integrable function integrates to $0$. Theorem 1.3's own sentence omits the assumptions; they are added as in §3.2.1, where it is derived from Theorem 3.7.

A statement in which $\theta^*$ is any feasible point of the program, or merely a measurable function of the sample, is false and does not count as a formalization of Theorem 3.7; nor does one in which Assumption 3.6 is weakened to almost every sample. Contributions of general infrastructure are welcome: exchangeability arguments for product measures, the binomial–beta identity, and Helly-type counting lemmas are reusable well beyond this mission.

Selected references

• M. C. Campi, S. Garatti, Introduction to the Scenario Approach, MOS-SIAM Series on Optimization 26, SIAM/MOS, 2018. https://doi.org/10.1137/1.9781611975444
• M. C. Campi, S. Garatti, The exact feasibility of randomized solutions of uncertain convex programs, SIAM Journal on Optimization 19(3), 2008. https://doi.org/10.1137/07069821X
• G. Calafiore, M. C. Campi, Uncertain convex programs: randomized solutions and confidence levels, Mathematical Programming 102, 2005. https://doi.org/10.1007/s10107-003-0499-y
• G. Calafiore, M. C. Campi, The scenario approach to robust control design, IEEE Transactions on Automatic Control 51(5), 2006. https://doi.org/10.1109/TAC.2006.875041
• E. Helly, Über Mengen konvexer Körper mit gemeinschaftlichen Punkten, Jahresbericht der DMV 32, 1923.

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.

Motivation

The k-server problem of Manasse, McGeoch and Sleator (J. Algorithms 11 (1990)) asks how $k$ mobile servers in a metric space should respond, on-line, to a sequence of requests at points of the space, each of which must be covered by a server. It is the central model of on-line computation: paging is the special case of a uniform metric, and many caching and scheduling problems reduce to it. For two servers the deterministic picture is complete: the optimal competitive ratio is $2$ on every metric space with at least three points.

Randomization changes the picture, and the smallest nontrivial case already shows how. On the equilateral triangle the optimal randomized ratio against an oblivious adversary is $3/2$. Karlin, Manasse, McGeoch and Owicki (Algorithmica 11 (1994) 542–571) computed the exact optimal randomized ratio for several nonuniform triangles, where the distances differ, and showed that it depends on the geometry. Their Theorem 12 settles the whole family of isosceles triangles with edge lengths $1$, $d$, $d$. These exact values are among the few known optimal randomized ratios for server problems.

Timeline:

• 1990: Manasse, McGeoch and Sleator introduce the $k$-server problem and prove the deterministic two-server ratio is $2$.
• 1990–1994: Karlin, Manasse, McGeoch and Owicki submit this paper (received August 1990, revised September 1991) and publish it in Algorithmica in 1994, with the isosceles-triangle ratios of Theorem 12 and the 3-4-5 triangle ratio $1652/1069$ of Theorem 13.
• Later: Karloff, Rabani and Ravid extend the technique to $\Omega(\log\log k)$ and $\Omega(\log k)$ randomized lower bounds (cited on p. 564); Bubeck, Coester and Rabani (STOC 2023) refute the randomized $k$-server conjecture.

Setting

Fix an integer $d\ge1$. The isosceles triangle $M$ has three points $a$, $b$, $c$ with

$$\operatorname{dist}(a,b)=1,\qquad \operatorname{dist}(a,c)=\operatorname{dist}(b,c)=d.$$

A configuration $C:\{0,1\}\to M$ places two labelled servers on points of $M$. A deterministic on-line algorithm assigns to every finite request sequence $\sigma=(r_1,\dots,r_n)$ a configuration, computed from $\sigma$ alone and covering the last request; its value on the empty sequence is its initial configuration. Its cost $C_A(\sigma)$ is the total distance its servers move while serving $\sigma$ request by request. The off-line optimum $C_{opt}(\sigma)$ from an initial configuration $C_0$ is the least total movement of any schedule that starts at $C_0$ and covers each request in turn, knowing $\sigma$ in advance.

A randomized algorithm is a probability distribution on deterministic on-line algorithms; its expected cost is $\mathbf{E}C_A(\sigma)$. It is $\rho$-competitive against an oblivious adversary from $C_0$ if every algorithm in its support starts at $C_0$ and there is a constant $a$ such that

$$\mathbf{E}C_A(\sigma)\le\rho\cdot C_{opt}(\sigma)+a\qquad\text{for every request sequence }\sigma.$$

The request sequence is fixed in advance and does not react to the algorithm's coin flips.

Write $e_p=(1+1/p)^p$ and

$$\alpha_d=\frac{e_{2d-1}+1/4d}{(e_{2d-1}-1)+1/2d},\qquad e_{2d-1}=\left(\frac{2d}{2d-1}\right)^{2d-1}.$$

In Lean this is NonuniformCompetitive.Isosceles.isoscelesRatio d.

Formalization targets

Goal: Theorem 12

For every $d\ge1$ and every initial configuration $C_0$:

$$\forall A,\ \forall\rho,\quad A\text{ is }\rho\text{-competitive from }C_0\ \Longrightarrow\ \rho\ge\alpha_d,$$ $$\exists A:\ A\text{ is }\alpha_d\text{-competitive from }C_0.$$

The two claims are also milestones of their own (no_better_ratio, ratio_attained).

The phase LP (§5, pp. 565–566)

For free real $\pi_1,\dots,\pi_{2d-1}$ and real $\alpha$ with

$$(\pi_k)2d+\sum_{i=1}^k(1-\pi_i)\le\alpha k\ \ (1\le k<2d),\qquad 2d+\sum_{i=1}^{2d-1}(1-\pi_i)+\tfrac12\le\alpha\cdot2d,$$

one has $\alpha\ge\alpha_d$ (lp_lower_bound); and $\pi_k=(\alpha_d-1)\big((2d/(2d-1))^k-1\big)$, $\pi_{2d}=1$ is nondecreasing from $\pi_1\ge0$ to $1$ and makes every constraint an equality (lp_attained).

The limit remark (§5, p. 566)

$$\alpha_1<\alpha_2<\alpha_3<\cdots,\qquad \lim_{d\to\infty}\alpha_d=\frac{e}{e-1}$$

(ratio_increases_to_e_ratio).

Significance

The theorem gives an exact optimal randomized ratio for an infinite family of metric spaces. It shows that the optimal randomized two-server ratio is not a constant: it runs from $3/2$ on the equilateral triangle to $e/(e-1)\approx1.582$ as the triangle becomes long and thin, where the problem resembles ski rental. With the deterministic ratio $2$, it quantifies exactly how much randomization gains on these spaces.

The results are proved in the paper; none is formalized on Prove2Me, and no machine-checked proof of them is known. A formal proof would require the paper's phase framework (Theorems 1–3 and the appendix's Theorem 15) for server problems, which this mission does not state separately, and a concrete randomized algorithm as a measurable mixed strategy. Both would be reusable for Theorem 13 (the 3-4-5 triangle) and for other exact ratios on small metric spaces.

Difficulty

The phase LP milestones are finite real arithmetic. The difficulty is the passage between them and the goal. The lower bound must hold for every randomized algorithm, not only phase-based lazy ones: an arbitrary algorithm may condition on the whole history, move non-lazily, and randomize in ways that do not reduce to the probabilities $\pi_k$. The paper handles this with Theorem 3, which says that the LP bound of phase-based algorithms bounds the competitive factor of all algorithms; its proof uses an averaging argument over histories that must be made rigorous. The upper bound needs a mixed strategy over infinitely many phases, with measurable costs, an explicit additive constant covering the first partial phase from an arbitrary initial configuration, and an accounting of $C_{opt}$ across phase boundaries.

Formalization scope

The model is the platform's published KServer_model and KServer_randomized (reference items): labelled servers Fin 2 → M; a deterministic on-line algorithm as a map from request prefixes to configurations; a randomized algorithm as a probability measure over deterministic algorithms, with the cost of each fixed sequence measurable in the random outcome; expected cost as a lower Lebesgue integral in $[0,\infty]$; the off-line optimum as a real infimum over schedules from $C_0$ (nonempty and bounded below by $0$); and IsCompetitiveFrom A C₀ c with a real additive constant.

Committed conventions:

• The triangle is any metric space whose points are exactly $a,b,c$ at distances $1,d,d$, with $d$ a natural number and $d\ge1$. Every such space is isometric to the paper's triangle; at $d=0$ it would not be a triangle.
• Both claims are stated for every initial configuration, including both servers on one point. The paper treats the initial state $\{a,b\}$ separately and absorbs the first partial phase into the additive constant.
• The lower bound quantifies over all randomized algorithms (deterministic ones are point masses), never over phase-based ones only.
• In the LP milestones the $\pi_k$ are free reals, as printed; no box $0\le\pi_k\le1$ is imposed.
• "Grows" in the limit remark is read as strictly increasing.
• The paper prints the recurrence on p. 565 as $\pi_k=\frac{\alpha-1+(\pi_{k-1})2d-1}{2d}$; the equations $(*)$ give $\pi_k=\frac{\alpha-1+2d\,\pi_{k-1}}{2d-1}$. The recurrence is not used; the closed form printed on p. 566 is correct and is the one stated.

Without the measurability field of a randomized algorithm the lower integral would under-report expected cost and the attainment claim would become easier than the paper's; the published definition includes it. The lower bound is not vacuous: the triangle hypotheses are satisfiable for every $d\ge1$.

Welcome contributions: a formal version of the phase framework (Theorems 1–3, 15) for finite metric spaces, reusable across missions III and IV; a measurable construction of phase-based randomized algorithms; and proofs of the LP milestones.

Selected references

• A. R. Karlin, M. S. Manasse, L. A. McGeoch, S. Owicki, Competitive Randomized Algorithms for Nonuniform Problems, Algorithmica 11 (1994) 542–571. https://doi.org/10.1007/BF01189993
• M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, J. Algorithms 11 (1990) 208–230. https://doi.org/10.1016/0196-6774(90)90003-W
• H. Karloff, Y. Rabani, Y. Ravid, Lower Bounds for Randomized k-Server and Motion-Planning Algorithms, SIAM J. Comput. 23 (1994) 293–312. https://doi.org/10.1137/S0097539792224838
• S. Bubeck, C. Coester, Y. Rabani, The Randomized k-Server Conjecture Is False!, STOC 2023. https://arxiv.org/abs/2211.05753