Optimization

Motivation

In high-dimensional linear regression the number of unknown coefficients $M$ may be much larger than the number of observations $n$, and the coefficient vector can only be recovered because it is assumed to be sparse: few of its entries are non-zero. Two convex estimators dominate this setting: the Lasso of Tibshirani (1996), an $\ell_1$-penalized least-squares estimator, and the Dantzig selector of Candès and Tao (2007), which minimizes the $\ell_1$ norm subject to a bound on the correlation between the residual and the columns of the design. Both are used routinely in statistics, signal processing and machine learning, and their rates of convergence determine how many observations suffice to estimate a sparse vector.

Bickel, Ritov and Tsybakov (arXiv:0801.1095; Ann. Statist. 37(4), 2009) analysed the two estimators side by side under a single, weak condition on the design, the restricted eigenvalue (RE) assumption. This mission formalizes their rates for the Dantzig selector, Theorem 7.1 of the paper.

Timeline. Candès and Tao (Ann. Statist. 35, 2007) introduced the Dantzig selector and bounded its $\ell_2$ error under a uniform uncertainty principle on the design. Bickel, Ritov and Tsybakov (2009) replaced that condition by the RE assumptions, which are implied by it (their Lemma 4.1), and obtained $\ell_p$ bounds for every $1\le p\le2$ and a prediction bound, with explicit constants. Later work (van de Geer and Bühlmann, EJS 2009) compared RE with the compatibility condition and other design conditions.

Setting

Observations follow the linear model

$$y=X\beta^*+w,$$

where $X\in\mathbb R^{n\times M}$ is a deterministic design matrix, $n\ge1$, $M\ge2$, $\beta^*\in\mathbb R^M$ is unknown, and $w=(W_1,\dots,W_n)$ has independent $\mathcal N(0,\sigma^2)$ coordinates with $\sigma>0$. The columns are normalized: every diagonal element of the Gram matrix $X^TX/n$ equals 1.

For $\beta\in\mathbb R^M$, $J(\beta)=\{j:\beta_j\ne0\}$ is its support and $\mathcal M(\beta)=|J(\beta)|$ its sparsity; $\beta^*$ satisfies $\mathcal M(\beta^*)\le s$ for an integer $1\le s\le M$. Norms are $|\delta|_p=(\sum_j|\delta_j|^p)^{1/p}$ and $|v|_2^2=\sum_iv_i^2$; for an index set $J$, $\delta_J$ keeps the coordinates of $\delta$ in $J$ and sets the others to 0, and $J^c$ is the complement of $J$.

With a tuning level $r=A\sigma\sqrt{\log M/n}$, $A>\sqrt2$, the Dantzig selector is any minimizer

$$\hat\beta_D\in\arg\min_{\beta\in\Lambda}|\beta|_1,\qquad \Lambda=\Big\{\beta\in\mathbb R^M:\ \Big|\tfrac1nX^T(y-X\beta)\Big|_\infty\le r\Big\}.$$

The cone condition at an index set $J_0$ with constant $c_0>0$ is $|\delta_{J_0^c}|_1\le c_0|\delta_{J_0}|_1$. Assumption RE$(s,c_0)$ asks that

$$\kappa(s,c_0)=\min_{|J_0|\le s}\ \min_{\delta\ne0,\ |\delta_{J_0^c}|_1\le c_0|\delta_{J_0}|_1}\frac{|X\delta|_2}{\sqrt n\,|\delta_{J_0}|_2}>0 .$$

Assumption RE$(s,m,c_0)$ is the same with $|\delta_{J_{01}}|_2$ in the denominator, where $J_{01}=J_0\cup J_1$ and $J_1$ collects the $m$ largest $|\delta_j|$ outside $J_0$; it is used for $s\le m$, $s+m\le M$.

Formalization targets

Goal: Theorem 7.1

With probability at least $1-M^{1-A^2/2}$, every Dantzig selector satisfies

$$|\hat\beta_D-\beta^*|_1\le\frac{8A}{\kappa^2(s,1)}\,\sigma s\sqrt{\frac{\log M}{n}},\qquad |X(\hat\beta_D-\beta^*)|_2^2\le\frac{16A^2}{\kappa^2(s,1)}\,\sigma^2s\log M,$$

and, on the same event, if RE$(s,m,1)$ holds, simultaneously for all $1<p\le2$,

$$|\hat\beta_D-\beta^*|_p^p\le2^{p-1}\,8\Big\{1+\sqrt{\tfrac sm}\Big\}^{2(p-1)}s\Big(\frac{A\sigma}{\kappa^2(s,m,1)}\sqrt{\frac{\log M}{n}}\Big)^p .$$

Milestones

In the order the proof of the paper uses them:

1. The noise event $\mathcal B=\bigcap_j\{|\frac1n\sum_iX_{ij}W_i|\le r\|f_j\|_n\}$ has $\mathbb P\{\mathcal B^c\}\le M^{1-A^2/2}$ (proof of Lemma B.3).
2. Lemma B.3, (B.9): for any $\beta$ satisfying the Dantzig constraint, $\delta=\hat\beta_D-\beta$ satisfies the cone condition at $J(\beta)$ with $c_0=1$.
3. (B.25): on $\mathcal B$, $\beta^*\in\Lambda$, $\frac1n|X^TX\delta|_\infty\le2r$, and $\frac1n|X\delta|_2^2\le4r\sqrt s\,|\delta_{J_0}|_2$.
4. (B.26): under RE$(s,1)$, $\frac1n|X\delta|_2^2\le16r^2s/\kappa^2$ and $|\delta_{J_0}|_2\le4r\sqrt s/\kappa^2$.
5. (B.27): on the cone, $|\delta|_1\le(1+c_0)\sqrt s\,|\delta_{J_0}|_2$.
6. (B.28): on the cone, $|\delta|_2\le(1+c_0\sqrt{s/m})\,|\delta_{J_{01}}|_2$.
7. (B.29): under RE$(s,m,1)$, $|\delta|_2^2\le16(1+\sqrt{s/m})^2(r\sqrt s/\kappa^2)^2$.
8. Interpolation: $\sum_ja_j\le b_1$, $\sum_ja_j^2\le b_2$, $a_j\ge0$ imply $\sum_ja_j^p\le b_1^{2-p}b_2^{p-1}$ for $1<p\le2$.

Significance

The result. Theorem 7.1 shows that, up to the factor $\log M$, the Dantzig selector estimates an $s$-sparse vector as well as least squares would if the support were known: the prediction error $\frac1n|X(\hat\beta_D-\beta^*)|_2^2$ is of order $\sigma^2s\log M/n$, and the $\ell_p$ errors are of order $s^{1/p}\sigma\sqrt{\log M/n}$. The bounds hold for any $M$, including $M\gg n$, provided only that RE holds, and every constant is explicit. The paper's Theorem 7.2 gives the same rates for the Lasso; comparing the two is the paper's main message.

Formalizing it. The theorem is proved in the paper; to the best of current knowledge it has not been machine-checked. A complete formal proof would provide: a verified Gaussian maximal inequality for the noise event, the deterministic cone and RE arithmetic that underlies essentially all $\ell_1$-regularized estimation theory, and a reusable $\ell_1$–$\ell_2$ interpolation lemma. Most milestones are deterministic and independent of the probability layer.

Difficulty

The obvious argument — compare $\hat\beta_D$ with $\beta^*$ in Euclidean norm using the smallest eigenvalue of $X^TX/n$ — fails because that eigenvalue is 0 whenever $M>n$. The proof must instead show that the error vector lies in a cone on which $X$ is injective in a quantitative sense, and this uses the optimality of $\hat\beta_D$ (not just feasibility) together with the event $\mathcal B$ on which $\beta^*$ itself is feasible. The $\ell_p$ bound needs a second, stronger condition RE$(s,m,1)$ and a control of the tail of the error outside the $m$ largest coordinates. On the formal side, handling the non-uniqueness of the minimizer, real powers with exponent $p-1$ or $2-p$, and the union over $M$ Gaussian tails with the exact constant $M^{1-A^2/2}$ all need care.

Formalization scope

Vectors are functions Fin M → ℝ, the design is Matrix (Fin n) (Fin M) ℝ; the paper's dictionary of functions enters only through $X$. The unit diagonal of $X^TX/n$ is a hypothesis, not a normalization performed in the proof. The noise is W : Fin n → Ω → ℝ on a probability space, measurable, mutually independent, each of law $\mathcal N(0,\sigma^2)$; $\log$ is the natural logarithm. The Dantzig selector is a predicate (feasible and of minimal $\ell_1$ norm among feasible vectors), and every result is stated for every minimizer. RE$(s,c_0)$ and RE$(s,m,c_0)$ are stated through a witness $\kappa$ (a number with the defining lower-bound property); $\kappa(s,c_0)$ is the largest witness and the bounds decrease in $\kappa$, so the statements are equivalent to the paper's while avoiding the value of a real infimum over an empty set. Two witnesses are kept apart: $\kappa$ for RE$(s,1)$ in (7.4)–(7.5), $\kappa'$ for RE$(s,m,1)$ in (7.6). Ties in the choice of the $m$ largest coordinates are handled by quantifying over every admissible $J_1$. The probability statement asserts one measurable event $E$ with $\mathbb P(E)\ge1-M^{1-A^2/2}$ on which all three bounds hold for every minimizer, every admissible $m$, every witness $\kappa'$ and every $p$.

The event $E$ is fixed before the minimizer is quantified, so a formalization in which the event depends on $\hat\beta_D$, or in which RE is a hypothesis about the random error vector rather than the design, would be a different (weaker) statement and is not accepted. The deterministic milestones (B.26)–(B.29) take the conclusion of (B.25) as a hypothesis; they are true for every vector satisfying their hypotheses and are not restricted to the event.

A complete development needs Gaussian tail bounds and a union bound (Mathlib's gaussianReal), finite Hölder-type inequalities for real exponents, and elementary sorting arguments for the tail outside $J_{01}$. The cone, RE and interpolation lemmas are reusable for the Lasso (Theorem 7.2, a sister mission) and beyond. Proofs of any milestone are welcome independently.

Selected references

• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 1705–1732, 2009. arXiv:0801.1095v3: https://arxiv.org/abs/0801.1095
• E. Candès, T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6), 2313–2351, 2007. https://doi.org/10.1214/009053606000001523
• R. Tibshirani, Regression shrinkage and selection via the lasso, J. R. Stat. Soc. B 58(1), 267–288, 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x
• S. van de Geer, P. Bühlmann, On the conditions used to prove oracle results for the Lasso, Electron. J. Statist. 3, 1360–1392, 2009. https://doi.org/10.1214/09-EJS506

Motivation

Two estimators dominate sparse high-dimensional regression, where the number $M$ of candidate regressors can far exceed the sample size $n$. The Lasso (Tibshirani, 1996) minimises a least-squares criterion plus an $\ell_1$ penalty. The Dantzig selector (Candès and Tao, 2007) minimises the $\ell_1$ norm of the coefficients subject to a bound on the correlation between the residual and the regressors, and is computed by a linear program. They were proposed independently and first analysed under different assumptions: sparsity oracle inequalities for the Lasso (Bunea, Tsybakov and Wegkamp, 2007) and $\ell_2$ bounds for the Dantzig selector under a uniform uncertainty principle (Candès and Tao, 2007). A practitioner choosing between them needs to know whether guarantees for one say anything about the other.

Bickel, Ritov and Tsybakov (arXiv:0801.1095; Ann. Statist. 37(4), 2009, doi:10.1214/08-AOS620) analyse both estimators in parallel under one assumption on the design, the restricted eigenvalue condition. Their main message is that, under sparsity, the two estimators "exhibit similar behavior" (p. 2). Section 5 makes this precise: the prediction losses of the two estimators are close. The result holds in a nonparametric model: the regression function need not be a combination of the regressors. This mission formalizes that comparison, Theorem 5.1 of the paper.

Setting

Let $f_1,\dots,f_M$ be real functions (the dictionary) on a set $\mathcal Z$, and $Z_1,\dots,Z_n\in\mathcal Z$ fixed design points, with $n\ge1$ and $M\ge2$. The design matrix is $X=(f_j(Z_i))\in\mathbb R^{n\times M}$. Observations are $Y_i=f(Z_i)+W_i$, where $f$ is an unknown function and $W_1,\dots,W_n$ are independent $\mathcal N(0,\sigma^2)$ with $\sigma>0$. Write $y=(Y_i)$, $\boldsymbol f=(f(Z_i))$ and $w=(W_i)$, so $y=\boldsymbol f+w$.

The empirical norm of $g$ is $\|g\|_n=(\tfrac1n\sum_i g(Z_i)^2)^{1/2}$. Every column has $\|f_j\|_n\neq0$, and $f_{\max}=\max_j\|f_j\|_n$. For $\beta\in\mathbb R^M$, $f_\beta=\sum_j\beta_jf_j$ has value vector $X\beta$. The support is $J(\beta)=\{j:\beta_j\ne0\}$ and the sparsity is $\mathcal M(\beta)=|J(\beta)|$. For $J\subseteq\{1,\dots,M\}$, $\delta_J$ agrees with $\delta$ on $J$ and vanishes elsewhere.

Fix $r>0$. The Lasso $\hat\beta_L$ is any minimiser of

$$\frac1n\sum_{i=1}^n\big(Y_i-f_\beta(Z_i)\big)^2+2r\sum_{j=1}^M\|f_j\|_n|\beta_j| .$$

With $D=\mathrm{diag}(\|f_1\|_n^2,\dots,\|f_M\|_n^2)$, the Dantzig constraint is $|\tfrac1nD^{-1/2}X^\top(y-X\beta)|_\infty\le r$. The Dantzig selector $\hat\beta_D$ is any vector of smallest $|\beta|_1=\sum_j|\beta_j|$ that satisfies it. The estimators are $\hat f_L=f_{\hat\beta_L}$ and $\hat f_D=f_{\hat\beta_D}$.

Assumption RE$(s,c_0)$ with $1\le s\le M$, $c_0>0$ asks that

$$\kappa(s,c_0)=\min_{|J_0|\le s}\ \min_{\delta\ne0,\ |\delta_{J_0^c}|_1\le c_0|\delta_{J_0}|_1}\ \frac{|X\delta|_2}{\sqrt n\,|\delta_{J_0}|_2}>0 .$$

Throughout, $r=A\sigma\sqrt{\log M/n}$, where $\log$ is the natural logarithm.

Formalization targets

Goal: Theorem 5.1

Assume RE$(s,1)$ with $1\le s\le M$, and let $A>2\sqrt2$. With probability at least $1-M^{1-A^2/8}$, every Lasso solution with $\mathcal M(\hat\beta_L)\le s$ and every Dantzig selector satisfy

$$\Big|\,\|\hat f_D-f\|_n^2-\|\hat f_L-f\|_n^2\,\Big|\le16A^2\,\frac{\mathcal M(\hat\beta_L)\sigma^2}{n}\,\frac{f_{\max}^2}{\kappa^2(s,1)}\,\log M .$$

Milestones

The proof uses one probabilistic event and two one-sided deterministic inequalities.

1. The Lasso satisfies the Dantzig constraint (2.3).
2. The noise event $\mathcal A=\bigcap_j\{2|\tfrac1n\sum_iX_{ij}W_i|\le r\|f_j\|_n\}$ has $\mathbb P(\mathcal A^c)\le M^{1-A^2/8}$ (B.4).
3. On $\mathcal A$, $|\tfrac1nX^\top(\boldsymbol f-X\hat\beta_L)|_\infty\le 3rf_{\max}/2$ (Lemma B.1, (B.2)).
4. The Dantzig error lies in the cone $|\delta_{J_0^c}|_1\le|\delta_{J_0}|_1$ (Lemma B.3, (B.9)).
5. On the larger event $\mathcal B\supseteq\mathcal A$, $|\tfrac1nX^\top(\boldsymbol f-X\hat\beta_D)|_\infty\le 2rf_{\max}$ (Lemma B.3, (B.10)).
6. $\|\hat f_D-f\|_n^2\le\|\hat f_L-f\|_n^2+16f_{\max}^2r^2\mathcal M(\hat\beta_L)/\kappa^2$ on $\mathcal B$ (B.15).
7. $\|\hat f_L-f\|_n^2\le\|\hat f_D-f\|_n^2+9f_{\max}^2r^2\mathcal M(\hat\beta_L)/\kappa^2$ on $\mathcal A$ (B.17).

Further result: Theorem 5.2

Assume $\|f_j\|_n=1$ for all $j$ and RE$(s,5)$. With probability at least $1-M^{1-A^2/8}$, whenever $\mathcal M(\hat\beta_D)\le s$,

$$\|\hat f_L-f\|_n^2\le10\|\hat f_D-f\|_n^2+81A^2\,\frac{\mathcal M(\hat\beta_D)\sigma^2}{n}\,\frac{\log M}{\kappa^2(s,5)} .$$

Significance

The result. Theorem 5.1 bounds the gap between the two prediction losses by the rate $\mathcal M(\hat\beta_L)\sigma^2\log M/n$ of a sparse regression with $\mathcal M(\hat\beta_L)$ parameters. The bound carries a factor $f^2_{\max}/\kappa^2(s,1)$ that measures how ill-conditioned the Gram matrix is on sparse vectors. A prediction bound for one estimator therefore transfers to the other at this cost. The paper uses this transfer in Proposition 6.3, which combines Theorem 5.1 with the Lasso oracle inequality of Section 6 to derive an oracle inequality for the Dantzig selector. The theorem requires no assumption relating $f$ to the dictionary.

Formalizing it. The result has been proved since 2009, and this mission formalizes that proof. None of the objects involved exists on Prove2Me yet: the weighted Lasso, the Dantzig selector and the Gaussian noise events. The Wainwright series on the platform defines a differently normalised Lasso with an unweighted penalty, a single fixed support and a different restricted eigenvalue condition, so it cannot be reused here. A machine-checked proof would also confirm the paper's constants, $16A^2$ and the thresholds $2\sqrt2$ and $M^{1-A^2/8}$, which appear in all later analyses.

Difficulty

Each estimator is defined only implicitly, as the solution of an optimisation problem, and neither need be unique. Comparing their losses directly gives $\pm\tfrac2n\delta^\top X^\top(\boldsymbol f-X\hat\beta)$ plus $\tfrac1n|X\delta|_2^2$ with $\delta=\hat\beta_L-\hat\beta_D$. A crude bound on the cross term, $|\delta|_1\cdot|X^\top(\cdot)|_\infty$, yields an error proportional to $|\delta|_1$. This does not produce the sparse rate unless $|\delta|_1$ is controlled by $|X\delta|_2$. That control needs $\delta$ to lie in the restricted eigenvalue cone at the support of the random, data-dependent vector $\hat\beta_L$. The restricted eigenvalue condition must therefore hold uniformly over supports of size at most $s$; a condition for one fixed support does not suffice. The probabilistic part is a union bound over $M$ Gaussian coordinates, and it must be arranged so that a single event serves every minimiser of both programs.

Formalization scope

The dictionary and the design points enter every statement only through $X$ and $\boldsymbol f$, so the Lean statements take X : Matrix (Fin n) (Fin M) ℝ and f : Fin n → ℝ directly, and $f$ is arbitrary. The noise is a family W : Fin n → Ω → ℝ of measurable, mutually independent random variables with law gaussianReal 0 σ², and $y=f+W(\omega)$. The Lasso and the Dantzig selector are predicates (IsLasso, IsDantzig), and every theorem is stated for every solution. The Dantzig constraint is written coordinatewise as $|\tfrac1n\sum_iX_{ij}(y_i-(X\beta)_i)|\le r\|f_j\|_n$. The Lasso penalty and the Dantzig constraint are weighted by $\|f_j\|_n$, and the Dantzig objective $|\beta|_1$ is unweighted, exactly as in the paper. Theorem 5.1 does not normalise the columns.

RE$(s,c_0)$ is stated through a witness: a real $\kappa>0$ with $\kappa\sqrt n|\delta_{J_0}|_2\le|X\delta|_2$ on the cone, for all $|J_0|\le s$. The paper's $\kappa(s,c_0)$ is attained, so it is the largest witness. Every bound decreases in $\kappa$, so this reading is equivalent to the paper's and avoids a real infimum over an empty set. "With probability at least $p$" becomes the existence of a measurable event $E$ with $\mathbb P(E)\ge p$ on which the conclusion holds for every Lasso solution and every Dantzig selector. The condition $\mathcal M(\hat\beta_L)\le s$ is imposed inside the event, per realisation. The milestones (B.2), (B.10), (B.15) and (B.17) are stated deterministically, on the noise events $\mathcal A$ and $\mathcal B$ as predicates on the noise vector; this is how the proof uses them. (B.4) is stated for every $A>0$, which is stronger than the paper's $A>2\sqrt2$ and still true.

The goal cannot be made vacuous. For $A>2\sqrt2$ the probability bound $1-M^{1-A^2/8}$ is positive. Lasso solutions exist because $r>0$ and every $\|f_j\|_n>0$, and Dantzig selectors exist because the Lasso is feasible. RE$(s,1)$ with $\kappa=1$ holds for $X=\sqrt n\,I$.

A complete development needs:

• subgradient optimality for the weighted Lasso;
• a Gaussian tail bound $\mathbb P(|\eta|\ge t)\le e^{-t^2/2}$ together with the law of a weighted sum of independent Gaussians;
• Cauchy–Schwarz on supports;
• the quadratic bound $bx-x^2\le b^2/4$.

The noise-event lemmas and the Lasso optimality condition can be reused by the companion missions on this paper. Proofs of any milestone are welcome, including proofs that route (B.4) through Mathlib's sub-Gaussian API.

Selected references

• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 1705–1732, 2009. arXiv:0801.1095v3: https://arxiv.org/abs/0801.1095 ; doi:10.1214/08-AOS620
• E. Candès, T. Tao, The Dantzig selector: statistical estimation when p is much larger than n, Ann. Statist. 35(6), 2313–2351, 2007. https://doi.org/10.1214/009053606000001523
• R. Tibshirani, Regression shrinkage and selection via the lasso, J. R. Stat. Soc. B 58(1), 267–288, 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x
• F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Sparsity oracle inequalities for the Lasso, Electron. J. Stat. 1, 169–194, 2007. https://doi.org/10.1214/07-EJS008

Motivation

The traveling salesman problem with the triangle inequality asks for a shortest closed tour through $n$ points whose distances form a metric. It is NP-hard, so in practice tours are built by fast construction heuristics, and the natural question is how far such a tour can be from optimal in the worst case. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) gave the first systematic worst-case analysis of the standard heuristics. Their results are reproduced in textbooks on approximation algorithms and combinatorial optimization, and they are the reference point against which later guarantees (Christofides' $3/2$ algorithm, the double-tree $2$-approximation) are compared.

The simplest heuristic studied is the nearest neighbor algorithm (Bellmore and Nemhauser, 1968; the "next best method" of Gavett, 1965): from the current node, always move to the closest node not yet visited, and return to the start at the end. The paper shows that this greedy rule is never worse than logarithmic (Theorem 1) and that the logarithm cannot be removed (Theorem 2). This mission is about Theorem 2, the lower bound.

Setting

A traveling salesman graph on $n$ nodes is a complete graph with a distance $d(a,b)\in\mathbb R$ that is symmetric, $d(a,b)=d(b,a)$, nonnegative, $d(a,b)\ge 0$, and satisfies the triangle inequality $d(a,c)\le d(a,b)+d(b,c)$. A tour lists the nodes in a visiting order $\tau(0),\dots,\tau(n-1)$ and returns to $\tau(0)$; its length is the sum of the $n$ distances along it. OPTIMAL is the least length of a tour.

The nearest neighbor algorithm starts at an arbitrary node $\tau(0)$; having reached $\tau(k)$, it moves to a node $\tau(k+1)$ that minimizes $d(\tau(k),\cdot)$ over the nodes not yet visited, breaking ties arbitrarily; after the last node it returns to $\tau(0)$. The length of the resulting tour is written NEARNEIBER. Because the start node and the ties are free, one instance has in general several nearest-neighbor tours. A lower bound needs only one of them; an upper bound must hold for all.

The instances of the proof are built from a recursive family of weighted graphs. With $l_i=\frac16(4\cdot 2^i-(-1)^i+3)$ (so $l_1,l_2,l_3,l_4=2,3,6,11$), the graph $F_1$ is a triangle with unit weights, and $F_{i+1}$ consists of two copies of $F_i$ joined through one new node by two edges of length $1$ and two edges of length $l_i$. Each $F_i$ has $2^{i+1}-1$ nodes and a path $P_i$ from its start node to its middle node through every node, of length $L_i$ with $L_1=2$, $L_{i+1}=2L_i+2l_i$. The graph $G_i$ adds two closing edges to $F_i$, and $\bar G_i$ is the complete graph on the same nodes whose distance is the shortest-path distance of $G_i$.

Formalization targets

Goal: Theorem 2 (p. 566)

For each $m>3$ there is a traveling salesman graph with $n=2^m-1$ nodes and a nearest-neighbor tour on it such that

$$\frac{\mathrm{NEARNEIBER}}{\mathrm{OPTIMAL}}>\frac13\lg(n+1)+\frac49 .$$

The statement is existential in both the instance and the run of the algorithm, exactly as in the paper.

Milestones, in the order the proof uses them

1. (2.12): the difference equation $L_{i+1}=2L_i+2l_i$, $L_1=2$, has the solution $L_i=\frac19(6\,i\,2^i+8\cdot2^i+(-1)^i-9)$.
2. $\bar G_i$ is a traveling salesman graph: the shortest-path distance of $G_i$ is symmetric, nonnegative and satisfies the triangle inequality.
3. (2.13)–(2.17): the shortest-path distances in $F_{i+1}$ between the seven named nodes $A,\dots,G$ of Fig. 1, e.g. $\overline{AG}=l_{i+2}-2$.
4. Property a): every edge of $G_i$ is a shortest path between its endpoints.
5. Property b): the nearest neighbor algorithm started at the start node of $\bar G_i$ can follow $P_i$ and return along the edge of length $l_i-1$.
6. The optimal tour: $\mathrm{OPTIMAL}(\bar G_i)=2^{i+1}-1$.
7. The exact ratio: the tour along $P_i$ has length $L_i+l_i-1$, so its ratio is $(L_i+l_i-1)/n$.
8. The inequality: $(L_i+l_i-1)/n>\frac13\lg(n+1)+\frac49$ for $i\ge3$.

The instance for $m$ is $\bar G_{m-1}$.

Significance

Theorem 1 of the same paper shows $\mathrm{NEARNEIBER}/\mathrm{OPTIMAL}\le\frac12\lceil\lg n\rceil+\frac12$ for every nearest-neighbor tour on every traveling salesman graph. Theorem 2 shows that this bound has the right order: no constant-factor guarantee holds for the nearest neighbor rule, and the gap between the two constants ($\frac13$ against $\frac12$) is all that remains. This separates the nearest neighbor rule from the insertion rules analysed later in the same paper, of which nearest and cheapest insertion are within a factor $2$ of optimal. It is the standard example of a natural greedy heuristic whose approximation ratio grows with $n$.

The upper bound, Theorem 1, is already on Prove2Me with a machine-checked proof (SupplyChainTheory.nearest_neighbor_bound); its statement notes that the lower-bound instances are not formalized there. This mission supplies them: an explicit recursive family of metric instances, the shortest-path computations that certify it, and the arithmetic of its ratio. The result is proved in the paper; to our knowledge it has not been formalized in any proof assistant. The construction (a recursively defined weighted graph with a closed-form shortest-path table) is also a reusable pattern for other worst-case lower bounds of greedy heuristics.

Difficulty

The arithmetic ((2.12) and the final inequality) is routine. The content is in properties a) and b). A shortest-path distance is an infimum over all walks, and property a) asks that no detour through the recursive structure is shorter than the direct edge, at every level of the recursion. The paper handles this by an induction on (2.13)–(2.17) that tracks only seven nodes per level, and argues that distances inside a copy of $F_i$ are not shortened by embedding it into $F_{i+1}$. Property b) then needs that at each step of $P_i$ the chosen node is at least as close as every unvisited node, including nodes in the other copy and nodes reached through the start or right nodes; ties occur, and the claim is only that some resolution of them follows $P_i$. Checking small cases by computer does not give either property for all $i$.

Formalization scope

Nodes of an instance are Fin n, a tour is a permutation of Fin n, the tour length is the sum over consecutive pairs including the closing edge, and OPTIMAL is a minimum over the finite set of permutations. The model is the paper's: symmetric, nonnegative distances with the triangle inequality. The distance structure also carries $d(a,a)=0$, a normalization not in the paper; the diagonal never enters a tour length. A nearest-neighbor tour is a permutation in which each step goes to a node at least as close as every unvisited node, from an arbitrary start with arbitrary ties.

Ratios are multiplied out: the goal is $(\frac13\log_2(n+1)+\frac49)\cdot\mathrm{OPTIMAL}<\mathrm{NEARNEIBER}$ together with $\mathrm{OPTIMAL}>0$, the paper's standing assumption (1.1). $\lg(n+1)$ is Real.logb 2 of $n+1$, as printed. Because of the strict inequality and the conjunct $\mathrm{OPTIMAL}>0$, the all-zero distance does not satisfy the goal, so the statement cannot be met by a degenerate instance.

In the construction the nodes of $F_i$, $G_i$, $\bar G_i$ are numbered $0,\dots,2^{i+1}-2$ from left to right (start node $0$, middle node $2^i-1$, right node $2^{i+1}-2$); in $F_{i+1}$ the left copy comes first, then the new node, then the right copy. Graphs are edge lists with real weights and $l_i$ is defined in $\mathbb R$ exactly as in (2.11). The shortest-path distance is the infimum of walk weights over an inductive walk predicate; it would be $0$ for two nodes with no connecting walk, a case that does not arise because every $G_i$ and $F_i$ is connected. $L_i$ is defined by its difference equation; its identification with the length of the tour along $P_i$ is milestone 7. All construction statements assume $i\ge1$.

A complete development needs a small library for shortest-path distances of finite weighted edge lists (symmetry, triangle inequality, attainment, behaviour under relabelling and under gluing two graphs at a few nodes); this part is reusable beyond the mission. Contributions welcome: proofs of any milestone, and such general shortest-path lemmas as separate theorems. Theorem 1 is not part of this mission.

Selected references

• D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM J. Comput. 6(3):563–581, 1977. https://doi.org/10.1137/0206041
• M. Bellmore, G. L. Nemhauser, The Traveling Salesman Problem: A Survey, Operations Research 16(3):538–558, 1968. https://doi.org/10.1287/opre.16.3.538
• J. W. Gavett, Three Heuristic Rules for Sequencing Jobs to a Single Production Facility, Management Science 11(8):B166–B176, 1965. https://doi.org/10.1287/mnsc.11.8.B166
• N. Christofides, Worst-Case Analysis of a New Heuristic for the Travelling Salesman Problem, Report 388, Graduate School of Industrial Administration, Carnegie Mellon University, 1976.

Motivation

Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It models cutting stock, memory allocation, file placement and the loading of trucks, and it is NP-hard, so in practice lists are packed by simple rules that look at one item at a time. The two most widely used rules are First-Fit and Best-Fit, and the question that Johnson, Demers, Ullman, Garey and Graham answered in 1974 is how far from optimal they can be in the worst case.

Their headline answer is that both rules use at most about $\tfrac{17}{10}$ times the optimal number of bins, and that $\tfrac{17}{10}$ is asymptotically attained. The lists that force this ratio use items larger than $\tfrac12$. When all items are known to be small, which is typical of memory and storage applications, the guarantee is much better, and this mission is about that refinement: the paper's Theorem 2.3 and its corollary, which determine the asymptotic worst-case ratio of First-Fit and Best-Fit exactly as a function of the largest allowed item size $\alpha\le\tfrac12$.

Timeline. Ullman (1971) introduced the worst-case analysis of First-Fit with a $\tfrac{17}{10}L^*+3$ bound. Garey, Graham and Ullman (1972) and Johnson's thesis (MIT, 1973) extended it to Best-Fit and to the decreasing variants. The 1974 SIAM paper collects these results; Theorem 2.3 there is the parametric bound for items of size at most $\alpha$. The additive constants in the unrestricted $\tfrac{17}{10}$ bound were sharpened over the following four decades, culminating in Dósa and Sgall's proof (2013) that $FF(L)\le\lfloor\tfrac{17}{10}L^*\rfloor$.

Setting

A list is a finite sequence $L=(a_1,\dots,a_n)$ of real numbers in $(0,1]$. Its optimum $L^*$ is the least number of bins into which the elements of $L$ can be placed so that no bin contains numbers whose sum exceeds $1$. The level of a bin is the sum of the numbers in it. For a real $\alpha>0$, write $L\subseteq(0,\alpha]$ when every element of $L$ is at most $\alpha$.

First-Fit ($FF$) considers bins $B_1,B_2,\dots$, all initially empty, and places $a_1,a_2,\dots,a_n$ in that order: $a_i$ goes into the bin $B_j$ of least index whose level $\beta$ satisfies $\beta\le 1-a_i$. Best-Fit ($BF$) is the same except that, among the bins with $\beta\le 1-a_i$, it chooses one of largest level $\beta$ (least index among ties). $FF(L)$ and $BF(L)$ denote the numbers of nonempty bins at the end.

The restricted worst-case ratios are

$$R^\alpha_{FF}(k)=\max\Big\{\frac{FF(L)}{L^*}: L\subseteq(0,\alpha],\ L^*=k\Big\},\qquad R^\alpha_{BF}(k)=\max\Big\{\frac{BF(L)}{L^*}: L\subseteq(0,\alpha],\ L^*=k\Big\}.$$

Throughout, $0<\alpha\le\tfrac12$ and $m=\lfloor\alpha^{-1}\rfloor$, an integer with $m\ge 2$ and $\tfrac1{m+1}<\alpha\le\tfrac1m$.

Formalization targets

Goal: the asymptotic ratio (Corollary of Theorem 2.3, p. 308)

$$\lim_{k\to\infty}R^\alpha_{FF}(k)=\lim_{k\to\infty}R^\alpha_{BF}(k)=1+\frac{1}{\lfloor\alpha^{-1}\rfloor}.$$

The goal is stated as a limit, which is the stable form of the result: it is unaffected by any improvement of the additive constants below.

Theorem 2.3(i): the lower bound (p. 307)

For each $k\ge1$ there is a list $L\subseteq(0,\alpha]$ with $L^*=k$ and $FF(L)\ge\frac{m+1}{m}L^*-\frac1m$; likewise for $BF$.

Two steps of the First-Fit upper bound (p. 308)

If no element of $L$ exceeds $\frac1m$, then in the First-Fit packing every bin except possibly the last contains at least $m$ elements, and all but at most two bins have level at least $\frac{m}{m+1}$.

Theorem 2.3(ii): the upper bounds (p. 307)

For every list $L\subseteq(0,\alpha]$,

$$FF(L)\le\frac{m+1}{m}L^*+2,\qquad BF(L)\le\frac{m+1}{m}L^*+2.$$

Significance

The theorem gives an exact, parametric description of how the worst case of the two greedy rules improves as items shrink: the asymptotic ratio is $\tfrac32$ when items are at most $\tfrac12$, $\tfrac43$ when at most $\tfrac13$, and tends to $1$ as the maximum item size tends to $0$. Combined with the $\tfrac{17}{10}$ bound for unrestricted lists, it shows that the bad behaviour of First-Fit is caused entirely by items larger than $\tfrac12$. Such parametric bounds are the standard way bin-packing heuristics are compared in the literature on online and semi-online packing, and the construction in part (i) is a reusable template for lower-bound lists.

The paper proves the First-Fit upper bound and the lower bound (the verification of the lower-bound construction is left to the reader). The Best-Fit upper bound is stated but not proved: the paper says only that "a similar, but slightly more complicated, argument can be used". A formal proof of the goal therefore requires supplying that argument. None of these results is known to have a machine-checked proof; Mathlib contains no bin-packing development.

Difficulty

For First-Fit the upper bound is a counting argument, but it rests on a property of the run, not of the final packing: an item that went into a later bin did not fit into an earlier bin at the moment it was placed. Turning that into a statement about the final levels requires an invariant maintained through the whole sequence of placements.

The Best-Fit upper bound is harder because that property fails: Best-Fit may put a small item into a fuller, later bin while an earlier, lighter bin still has room, so a light early bin and a light later bin can coexist longer than under First-Fit. The paper gives no argument for this case.

The lower bound requires computing the exact behaviour of both algorithms on a specific interleaved list with item sizes perturbed by powers of $m$, and computing $L^*$ exactly for that list, which needs a matching lower bound on the optimum.

Formalization scope

A list is L : List ℝ with the hypothesis IsList L (every element in $(0,1]$); $L\subseteq(0,\alpha]$ is the additional hypothesis ∀ a ∈ L, a ≤ α. $L^*$ is optBins L, a sInf in ℕ over numbers of bins admitting a feasible assignment; the hypothesis IsList makes the set nonempty. The runs ffPack L and bfPack L are folds over the list that keep the nonempty bins in the order they were opened, each with its contents; an item that fits nowhere opens a new bin at the end, which is the paper's "least $j$" over infinitely many empty bins. Comparisons are exact (classical decidability on ℝ), and $FF(L)$, $BF(L)$ are the lengths of the final bin lists. $m$ is Nat.floor α⁻¹, cast before any division.

The ratios $R^\alpha_{FF}(k)$, $R^\alpha_{BF}(k)$ are suprema taken in ℝ≥0∞: an unbounded family would give $+\infty$, never a default value, and at $k=0$ the only admissible list is empty and the value is $0$. The goal is a Tendsto … atTop (𝓝 (1 + (⌊α⁻¹⌋₊)⁻¹)) statement in ℝ≥0∞. A real-valued sSup would have returned $0$ on an unbounded family and made a false bound look provable; that encoding is ruled out. The upper bounds keep the additive constant $2$ and the lower bound the subtractive $\frac1m$ exactly as printed.

The two proof steps are stated under the proof's own hypothesis "no element exceeding $1/m$", which is weaker than $L\subseteq(0,\alpha]$.

A complete development needs invariants of the First-Fit and Best-Fit folds, a lower bound $L^*\ge\sum_i a_i$, and exact evaluation of both runs on the construction of part (i). Lemmas about the fold encoding of First-Fit and Best-Fit and about $L^*$ are reusable in the companion missions on the $\tfrac{17}{10}$, $\tfrac{11}{9}$ and $\tfrac{71}{60}$ bounds of the same paper. Contributions on the Best-Fit upper bound are especially welcome, since the source gives no proof.

Selected references

• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM Journal on Computing 3(4):299–325, 1974. https://doi.org/10.1137/0203025
• J. D. Ullman, The Performance of a Memory Allocation Algorithm, Technical Report 100, Princeton University, 1971.
• M. R. Garey, R. L. Graham, J. D. Ullman, Worst-Case Analysis of Memory Allocation Algorithms, Proc. 4th ACM Symposium on Theory of Computing, 143–150, 1972. https://doi.org/10.1145/800152.804907
• D. S. Johnson, Near-Optimal Bin Packing Algorithms, PhD thesis, Massachusetts Institute of Technology, 1973. http://hdl.handle.net/1721.1/57819
• G. Dósa, J. Sgall, First Fit Bin Packing: A Tight Analysis, Proc. 30th STACS, LIPIcs 20:538–549, 2013. https://doi.org/10.4230/LIPIcs.STACS.2013.538

Motivation

The uncapacitated facility location (UFL) problem is one of the basic models of location theory and operations research: a firm chooses which warehouses, plants or servers to open, paying a fixed cost for each open site and a service cost for every client according to its distance to the nearest open site. It is also a standard test case for approximation algorithms.

Local search is the simplest of these and the one most used in practice: start from any set of open facilities and repeatedly add, drop or exchange one facility while this lowers the cost. The question is how bad a solution can be when no such move helps. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) answered it for UFL with an exact constant.

Timeline. Korupolu, Plaxton and Rajaraman (SODA 1998, J. Algorithms 2000) analysed local search with add, drop and swap moves and proved a locality gap of at most 5; their analysis contains the service cost bound restated here as Lemma 4.1. Charikar and Guha (FOCS 1999) proved a locality gap of 3 for a different local search, in which one facility is added and any number are dropped. Arya et al. (STOC 2001; journal version 2004) proved that the add/drop/swap neighbourhood itself has locality gap at most 3, and gave an instance showing that 3 cannot be improved (§4.3).

Setting

A metric instance consists of a finite set $C$ of clients, a finite set $F$ of facilities, and a distance $d$ on $C \cup F$ that is nonnegative, symmetric and satisfies the triangle inequality. The cost of serving client $j$ by facility $i$ is $c_{ji} = d(j,i)$; the distance $c_{ii'}$ between two facilities is also available. Each facility $i \in F$ has an opening cost $f_i \ge 0$.

A solution is a nonempty set $S \subseteq F$ of open facilities. Every client is served by its nearest open facility, so

$$\mathrm{cost}_f(S) = \sum_{i \in S} f_i, \qquad \mathrm{cost}_s(S) = \sum_{j \in C} \min_{i \in S} c_{ji}, \qquad \mathrm{cost}(S) = \mathrm{cost}_f(S) + \mathrm{cost}_s(S).$$

The neighbourhood of $S$ is the set of solutions reachable by adding one facility, dropping one facility, or swapping one open facility for another:

$$\mathcal B(S) = \{S + \{s'\}\} \cup \{S - \{s\} \mid s \in S\} \cup \{S - \{s\} + \{s'\} \mid s \in S\}.$$

$S$ is locally optimum if $\mathrm{cost}(S) \le \mathrm{cost}(S')$ for every $S' \in \mathcal B(S)$. The locality gap is the supremum, over all instances, of the ratio between the cost of a worst local optimum and the cost of a global optimum.

The proofs use the following notation, which appears in the milestones but not in the goal. Fix a second solution $O$ and nearest-facility assignments $\sigma_S : C \to S$, $\sigma_O : C \to O$; write $S_j = c_{j\sigma_S(j)}$, $O_j = c_{j\sigma_O(j)}$, $N_S(s) = \sigma_S^{-1}(s)$, $N_O(o) = \sigma_O^{-1}(o)$ and $N^o_s = N_O(o) \cap N_S(s)$. A facility $s \in S$ captures $o \in O$ if $|N^o_s| > \tfrac12 |N_O(o)|$; $s$ is good if it captures no facility of $O$ and bad otherwise. The proof of the facility cost bound uses a permutation $\pi$ of the clients that maps each $N_O(o)$ onto itself, moves every client of a non-capturing block $N^o_s$ out of that block (Property 3.1), and fixes every client of a capturing block that it would map into the same block.

Formalization targets

Goal: Theorem 4.3

$$\mathrm{cost}(S) \le 3 \cdot \mathrm{cost}(O) \quad \text{for every locally optimum } S \text{ and every solution } O.$$

This is the locality gap bound of Theorem 4.3 (p. 557) in its strongest printed form: $O$ is any solution, not only an optimal one.

Milestones

1. Lemma 4.1 (service cost), p. 554: $\mathrm{cost}_s(S) \le \mathrm{cost}_f(O) + \mathrm{cost}_s(O)$.
2. The refined mapping $\pi$ of the proof of Lemma 4.2, p. 555: such a permutation exists for any two assignments.
3. Inequality (5), p. 555: the drop move for a good facility $s$,

$$-f_s + \sum_{j \in N_S(s),\ \pi(j) \neq j} (O_j + O_{\pi(j)} + S_{\pi(j)} - S_j) + 2 \sum_{j \in N_S(s),\ \pi(j) = j} O_j \ge 0.$$

4. Inequality (6), pp. 555–556: the swap of a bad facility $s$ with the facility $o$ it captures that is nearest to it.
5. Inequality (8), p. 556: for a bad facility $s$ capturing the set $P \subseteq O$, the analogue of (5) with $\sum_{o' \in P} f_{o'} - f_s$ in place of $-f_s$.
6. Lemma 4.2 (facility cost), p. 555: $\mathrm{cost}_f(S) \le \mathrm{cost}_f(O) + 2 \cdot \mathrm{cost}_s(O)$.

A companion item, not a milestone, states the bound in the proof of Theorem 4.4 with $\alpha = \sqrt2$: a local optimum of the instance with facility costs $\sqrt2 f_i$ costs at most $(1+\sqrt2)\,\mathrm{cost}(O)$ in the original instance.

Significance

The result. Theorem 4.3 shows that the simplest local search for metric UFL is within a factor 3 of optimal at every local optimum, with no LP and no rounding, and the tight example of §4.3 shows the analysis cannot be improved for this neighbourhood. Because Lemmas 4.1 and 4.2 hold against every solution $O$, scaling the facility costs before running local search trades the two bounds against each other and gives the $1 + \sqrt2 + \epsilon$ guarantee of Theorem 4.4. The same capture-and-reassign technique is used for k-median (§3) and capacitated facility location (§5).

Formalizing it. The theorem is proved on paper; no machine-checked proof of it or of any locality gap bound for facility location is known to this mission. A formal development would check the reassignment arguments, which are stated case by case in the paper, and would produce reusable Lean infrastructure for metric facility location instances, nearest-facility costs and neighbourhood-based local optimality.

Difficulty

The service cost bound is routine; the facility cost bound is where the work lies. The natural first idea, closing a facility $s \in S$ and sending each of its clients to the facility of $S$ nearest to that client's optimal facility, fails when $s$ serves most of the clients of some $o \in O$: the nearest facility of $S$ to $o$ may be $s$ itself, so the client has nowhere to go. The proof separates good facilities, which can be dropped, from bad ones, which must be swapped with a captured facility, and pays for the clients that cannot be moved through the distance between $s$ and its nearest captured facility. The combinatorial core is the construction of a permutation within each $N_O(o)$ that avoids every non-capturing block and has fixed points only where they are unavoidable.

Formalization scope

Clients and facilities are finite types Cl and Fa. The distance is a real-valued function on Cl ⊕ Fa that is nonnegative, symmetric and satisfies the triangle inequality; $d(x,x) = 0$ is not assumed, since the paper neither states nor uses it. Opening costs are a function f : Fa → ℝ with 0 ≤ f i, and demands are unit, as in the paper.

Solutions are nonempty Finsets. The service cost is $\sum_j \min_{i \in S} c_{ji}$ (Finset.inf') and is defined only for nonempty sets, so no junk value for $\emptyset$ enters. Accordingly the drop move is considered only when a facility remains open; with at least one client, $\emptyset$ cannot serve anyone and is not a solution. Local optimality is required for all moves of $\mathcal B(S)$: every added facility, every dropped facility and every swap, not only the moves used in the proof. The goal is stated as the multiplied-out inequality $\mathrm{cost}(S) \le 3\,\mathrm{cost}(O)$ for every nonempty $O$, never as a ratio, since $\mathrm{cost}(O)$ may be $0$.

In the milestones, the nearest-facility assignments $\sigma_S$, $\sigma_O$ are arbitrary among the nearest ones (ties broken arbitrarily), and the family of bijections $\pi : N_O(o) \to N_O(o)$ is a single permutation of the clients with $\sigma_O \circ \pi = \sigma_O$. Inequality (5) assumes at least one client, which the paper assumes implicitly: with no clients and $S = \{s\}$ it would read $-f_s \ge 0$. The goal and Lemma 4.2 need no such assumption.

A statement that assumes local optimality only for the moves the proof uses, that fixes $O$ to be a global optimum defined by hypotheses, or that allows the empty set a zero service cost would be a different theorem; none of these is used.

Needed infrastructure: sums over nearest-facility assignments and their fibers $N_O(o)$, the permutation $\pi$, and bookkeeping of the three kinds of moves. The instance, cost and local optimality definitions are reusable for other local search analyses of metric location problems. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

• V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local Search Heuristics for k-Median and Facility Location Problems, SIAM J. Comput. 33(3):544–562, 2004. https://doi.org/10.1137/S0097539702416402
• M. R. Korupolu, C. G. Plaxton, R. Rajaraman, Analysis of a Local Search Heuristic for Facility Location Problems, J. Algorithms 37(1):146–188, 2000. https://doi.org/10.1006/jagm.2000.1100
• M. Charikar, S. Guha, Improved Combinatorial Algorithms for the Facility Location and k-Median Problems, FOCS 1999, 378–388. https://doi.org/10.1109/SFFCS.1999.814609

Motivation

A feedforward neural network is a directed acyclic graph of neurons, each computing a fixed scalar activation of a weighted sum of its inputs; fixing the graph and the activation and letting the weights vary gives a hypothesis class. Chapter 20 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), studies these classes through the book's three lenses. Approximation: every Boolean function is implemented by a network of depth 2 (Claim 20.1), but only at exponential size (Theorem 20.2), while a sign neuron implements conjunctions and disjunctions (Lemma 20.4), the bridge to Boolean circuits and hence to everything computable in bounded time. Estimation: the VC dimension of the class of sign networks over a graph with $|E|$ edges is $O(|E|\log|E|)$ (Theorem 20.6), so the sample complexity is governed by the number of weights. Optimization: training is NP-hard even for tiny networks, and the practical answer is SGD with the gradient computed by backpropagation, whose correctness the chapter derives from the chain rule.

Setting

A layered graph has layers $V_0, \dots, V_T$, every edge joining $V_{t-1}$ to $V_t$; $V_0$ holds the $n$ inputs and a constant neuron outputting $1$. With weights $w : E \to \mathbb{R}$ and an activation $\sigma$, the outputs are computed layer by layer, $a_{t+1,i} = \sum_{j : (v_{t,j}, v_{t+1,i}) \in E} w_{t,i,j}\,o_{t,j}$ and $o_{t+1,i} = \sigma(a_{t+1,i})$. The class $H_{V,E,\sigma} = \{h_{V,E,\sigma,w} : w : E \to \mathbb{R}\}$ (20.1); for binary classification the output layer is a single neuron and $\sigma$ is the sign function, so $H_{V,E,\operatorname{sign}}$ is a set of $\{\pm1\}$-valued predictors on $\mathbb{R}^n$. The size of the network is $|V|$, its depth $T$. The growth function $\tau_H(m) = \max_{|C| \le m}|H_C|$ extends to classes with any finite codomain (p. 275), and the proof of Theorem 20.6 uses two of its properties, stated as Exercises 3 and 4: the growth function of a product class is at most the product of the growth functions, and likewise for a composition class. For backpropagation the activation is any differentiable $\sigma$ and the loss is $\frac12\|o_T - y\|^2$; the backward pass sets $\delta_T = o_T - y$ and $\delta_t = \delta_{t+1}\operatorname{diag}(\sigma'(a_{t+1}))W_t$.

Formalization targets

Goal: Theorem 20.6

The VC dimension of $H_{V,E,\operatorname{sign}}$ is $O(|E|\log|E|)$. Explicitly, for a layered graph of depth at least $1$ with a single output neuron,

$$\operatorname{VCdim}(H_{V,E,\operatorname{sign}}) \le 2|E|\log_2(16|E|),$$

stated as: every $m \le \operatorname{VCdim}$ satisfies this bound (so the VC dimension is finite).

Milestones

Claim 20.1 (the depth-2 graph with $|V_1| = 2^n + 1$ whose sign class contains every function $\{\pm1\}^n \to \{\pm1\}$); Theorem 20.2 (every sign network implementing all functions $\{0,1\}^n \to \{0,1\}$ has $2^{n/3} \le 2|V|$); Lemma 20.4 (conjunction and disjunction as sign neurons); Exercise 4 (growth function of a composition); the correctness of backpropagation (§20.6: the partial derivative for the edge $(v_{t,j}, v_{t+1,i})$ is $\delta_{t+1,i}\sigma'(a_{t+1,i})o_{t,j}$). Further items: Exercise 3 (growth function of a product) and the intermediate bound $\tau_H(m) \le (em)^{|E|}$ of the proof of Theorem 20.6.

Significance

Theorem 20.6 is the reason networks are learnable at all in the book's sense: by the fundamental theorem, a class with finite VC dimension is agnostic PAC learnable with sample complexity linear in that dimension, and here the dimension is essentially the number of tunable parameters. The proof technique, due to Kakade and Tewari's lecture notes, is a composition-and-product argument on growth functions that applies to any layered class of threshold units and is reusable well beyond this chapter. Theorem 20.2 is the matching negative fact on expressive power, and it is a corollary of the same bound: a class that shatters $2^n$ points needs $\Omega(2^n)$ edges. Backpropagation's correctness is the one theorem about training the chapter can offer, given the hardness results, and it is the algorithm every practitioner runs.

Difficulty

Claim 20.1 and Lemma 20.4 are explicit constructions: the neuron $g_i(x) = \operatorname{sign}(\langle x, u_i\rangle - n + 1)$ detects $x = u_i$ because $\langle x, u_i\rangle \le n - 2$ otherwise, and the output neuron takes the disjunction; formally one must build the weight function and evaluate the forward pass on the $2^n$ inputs. Exercises 3 and 4 are counting: a restricted product is determined by its two restricted factors, and a restricted composition $f_2 \circ f_1$ on $C$ is determined by $f_1|_C$ and $f_2|_{f_1(C)}$, with $|f_1(C)| \le |C|$. Theorem 20.6 then needs: the class of one neuron is the class of homogenous halfspaces on its $d_{t,i}$ incoming coordinates, of VC dimension at most $d_{t,i}$ (Mission VI), Sauer's lemma in the form $\tau(m) \le (em)^{d}$ for every $m \ge 1$ (Mission IV; for $m \le d$ use $2^m \le (em)^m$), the layer class as a product and the network as a composition of layer classes, and finally the arithmetic $2^m \le (em)^{|E|} \Rightarrow m \le 2|E|\log_2(16|E|)$, which replaces the book's appeal to Lemma A.2 (for $m \ge 8|E|$ one has $\ln m \le \frac{m\ln 2}{2|E|}$). Theorem 20.2 follows from the goal with $|E| \le |V|^2$. Backpropagation is a chain-rule computation in a single real variable: the loss as a function of one weight is a composition of finitely many differentiable maps, and the derivative unwinds to the backward recursion; the formal effort is in the induction along layers with the natural-number indexing of the model.

Formalization scope

Layers and neurons are indexed by natural numbers: a LayeredGraph records the depth, the layer widths and, for each $t < T$, the finite set of edges $(v_{t,j}, v_{t+1,i})$ as pairs $(i, j)$ within the layer widths. Weights are functions on all index triples, and only those on edges are used, so the class is the image of all weight functions, as in (20.1). The forward computation netOutput is a recursion on the layer index; netInput is $a_{t+1,i}$. The sign activation returns $\pm1$ with $\operatorname{sign}(0) = -1$, the book's convention elsewhere, and a neuron with no incoming edges outputs $\sigma(0)$ (p. 270). The binary class signNetClass n G is Bool-valued, true iff the output neuron's input is positive, and is stated for graphs of depth at least $1$ (for depth $0$ the edges out of the input layer would be used but not counted in $|E|$). Growth functions with finite codomain are growthY, an sSup over restriction sizes, well defined because the codomains are finite; the Bool case is Mission IV's growth, and VC dimension and shattering are Mission IV's. Theorem 20.6 and Theorem 20.2 are given with explicit constants derived from the proof, since $O(\cdot)$ statements have no formal content; the drafter verified $\max\{m : 2^m \le (em)^{|E|}\} \le 2|E|\log_2(16|E|)$ numerically for $|E|$ up to $3000$ and at $10^4, \dots, 10^7$, and $2^n \le 2|V|^2\log_2(16|V|^2) \le 8|V|^3$. Backpropagation is stated for an arbitrary layered graph (phantom edges have weight $0$, p. 279), any differentiable activation, and one edge at a time as a HasDerivAt of the loss in that weight; $\delta_t$ is defined by recursion on $T - t$. The book's layer indices in (20.3) are shifted by one in the statement.

Not stated: Theorem 20.3 (Turing machines), Theorem 20.5 and Exercise 1 (sigmoid approximation, which needs a convention for outputs in $[-1,1]$ that the chapter leaves open), Theorem 20.7 and Exercise 6 (NP-hardness), Exercise 5 (the $\Omega(|E|^2)$ sigmoid lower bound, which assumes an exact threshold), the sigmoid half of Theorem 20.2, and the SGD pseudocode of §20.6, which is a heuristic without a stated guarantee.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 20. doi:10.1017/CBO9781107298019
• M. Anthony, P. L. Bartlett, Neural Network Learning: Theoretical Foundations, Cambridge University Press, 1999. doi:10.1017/CBO9780511624216
• D. E. Rumelhart, G. E. Hinton, R. J. Williams, Learning representations by back-propagating errors, Nature 323, 1986. doi:10.1038/323533a0
• I. Parberry, Circuit Complexity and Neural Networks, MIT Press, 1994.
• E. B. Baum, D. Haussler, What size net gives valid generalization?, Neural Computation 1(1), 1989. doi:10.1162/neco.1989.1.1.151