Why robustify a sampled stochastic program

Many decision problems under uncertainty take the form of a stochastic program: choose a decision $v$ from a feasible set $\mathcal F$ to maximise the expected utility $\mathbb E_{x\sim\mu}[f(v,x)]$, where the distribution $\mu$ of the uncertain parameter $x\in\mathbb R^m$ is known only through i.i.d. samples $x_1,\dots,x_n$. The standard remedy, sample average approximation, maximises $\frac1n\sum_i f(v,x_i)$ instead. Its consistency (convergence of the optimal expected utility of its solutions to the true optimum) is classical, but it needs regularity assumptions of its own, for example those of King and Wets (Stochastics and Stochastic Reports, 1991), cited on p. 98 of the paper; the paper presents its construction as a route to consistency under weaker conditions.

Robust optimization (RO) takes a different route: it protects each sample by an uncertainty set and optimises against the worst point in it. Xu, Caramanis and Mannor (Math. Oper. Res. 2012) show that RO over several overlapping uncertainty sets is equivalent to a distributionally robust stochastic program (their Theorem 2.1, the subject of mission I of this series). Section 3 of the paper uses that equivalence to show that a specific robustification of the sampled problem, with $\ell_\infty$ boxes of shrinking radius around each sample, is consistent under only boundedness and equicontinuity of $f$. This mission formalizes that result, Theorem 3.1.

Setting

Equip $\mathbb R^m$ with the sup norm $\|z\|_\infty=\max_k|z_k|$, its Borel $\sigma$-algebra and Lebesgue measure $dx$. The data are:

• a set of decisions $V$ and a nonempty feasible set $\mathcal F\subseteq V$;
• a utility $f:V\times\mathbb R^m\to\mathbb R$, Borel measurable in $x$ for each $v$;
• a true density $h^*$ on $\mathbb R^m$ (nonnegative, $\int h^*\,dx=1$) and i.i.d. samples $x_1,x_2,\dots$ with distribution $h^*(x)\,dx$;
• radii $\epsilon(n)>0$.

For a sample $x_1,\dots,x_n$ the boxes are $\mathcal Z_i=\{x_i+\delta\mid\|\delta\|_\infty\le\epsilon(n)\}$, and the box-robust sample objective is

$$J_n(v)=\frac1n\sum_{i=1}^n\ \inf_{\|\delta_i\|_\infty\le\epsilon(n)}f(v,x_i+\delta_i)=\sum_{i=1}^n\frac1n\inf_{x_i'\in\mathcal Z_i}f(v,x_i').$$

The RO solution $v(n)$ is a maximiser of $J_n$ over $\mathcal F$. The equicontinuity modulus of $f$ is

$$d(\epsilon)=\sup_{v,\,x,\ \|\delta\|_\infty\le\epsilon}|f(v,x)-f(v,x+\delta)|.$$

The proof works with the distribution set $\mathcal P_n$ of probability measures $\mu$ with $\mu(\bigcup_{i\in S}\mathcal Z_i)\ge|S|/n$ for every $S\subseteq\{1,\dots,n\}$, and with the uniform box kernel density estimator

$$h_n(x)=(n\epsilon(n)^m)^{-1}\sum_{i=1}^nK\Big(\frac{x-x_i}{\epsilon(n)}\Big),\qquad K(z)=\frac{\mathbf 1(\|z\|_\infty\le1)}{2^m}.$$

Formalization targets

Goal: Theorem 3.1 (p. 98)

Assume $|f(v,x)|\le C$ for all $v,x$; $d(\epsilon)\to0$ as $\epsilon\downarrow0$; $\epsilon(n)\downarrow0$ and $n\epsilon(n)^m\uparrow\infty$. Then for every choice of maximisers $v(n)$, with probability one,

$$\lim_{n\to\infty}\int_{\mathbb R^m}f(v(n),x)\,h^*(x)\,dx=\sup_{v\in\mathcal F}\int_{\mathbb R^m}f(v,x)\,h^*(x)\,dx .$$

Milestones (proof of Theorem 3.1, p. 99)

1. $h_n$ is the density of a probability measure in $\mathcal P_n$.
2. $J_n(v)\le\int f(v,x)\,h_n(x)\,dx$ for every $v$.
3. Oscillation over a box: $\sup_{\mathcal Z_i}f(v,\cdot)-\inf_{\mathcal Z_i}f(v,\cdot)\le d(2\epsilon(n))$.
4. Eq. (7): with $M_n=C\int|h_n-h^*|\,dx$, for every $v$,

$$J_n(v)-M_n\le\int f(v,x)h^*(x)\,dx\le J_n(v)+M_n+d(2\epsilon(n)).$$

5. Strong $L^1$ consistency of the box kernel density estimator: if $\epsilon(n)\to0$ and $n\epsilon(n)^m\to\infty$, then $\int|h_n-h^*|\,dx\to0$ almost surely.

Milestones 1–4 are deterministic statements about a fixed sample; milestone 5 is the only probabilistic input.

Significance

Theorem 3.1 gives consistency of a tractable robust reformulation of a sampled stochastic program under conditions the paper notes are weaker than those of King and Wets for sampled stochastic programs: $f$ need only be bounded and equicontinuous in $x$, uniformly in $v$, and the true distribution need only have a density. It also gives an explicit schedule for the size of the uncertainty set, $\epsilon(n)\to0$ with $n\epsilon(n)^m\to\infty$, the bandwidth condition of kernel density estimation. Section 4 of the paper applies the same distributional interpretation to regularised learning methods such as the support vector machine and the Lasso.

The result is proved in the paper, with the $L^1$ consistency of kernel density estimators (Devroye 1983; Devroye and Györfi 1985) cited rather than proved. No part of it is formalized in Lean or on this platform as far as a search of the platform found. A complete development would produce, besides Theorem 3.1, a machine-checked strong $L^1$ consistency theorem for kernel density estimators, which is a basic result of nonparametric statistics in its own right.

Difficulty

The deterministic part (milestones 1–4) is measure-theoretic bookkeeping: the kernel integrates to one only because the box is a sup-norm ball of volume $(2\epsilon)^m$, and every infimum and supremum must be handled with care, since $f$ need not attain them.

The obstacle is milestone 5. Almost-sure $L^1$ convergence of $h_n$ to an arbitrary density $h^*$, with no continuity or support assumption, does not follow from the strong law of large numbers applied pointwise: $h_n(x)$ is an average of $n$ terms whose law changes with $n$ through $\epsilon(n)$, and almost-sure convergence at each fixed $x$ does not give convergence of the integral along a single sample path. The theorem needs both a bias estimate valid for every integrable density and a concentration estimate for the random $L^1$ error. Mathlib has Lebesgue differentiation and the strong law, but no kernel density estimator and no such concentration result.

Formalization scope

• $\mathbb R^m$ is Fin m → ℝ, whose Mathlib norm is the sup norm; boxes are Metric.closedBall. The integrals $\int f(v,x)h^*(x)\,dx$ are Bochner integrals against Lebesgue measure of integrable integrands.
• The samples are a sequence X : ℕ → Ω → Fin m → ℝ on a probability space, independent (iIndepFun) and each with law volume.withDensity h*; $x_1,x_2,\dots$ become X 0, X 1, …, and the $n$-th problem uses the first $n$. "With probability one" is ∀ᵐ ω ∂P.
• The goal quantifies over every selection $v(n)$ of maximisers, with no measurability assumed; a version with one chosen maximiser would be weaker and is ruled out.
• Readings and corrections of the printed text:
  • the kernel argument printed $(x-x_i)/\epsilon$ on p. 98 is read as $(x-x_i)/\epsilon(n)$, as the proof on p. 99 writes it;
  • "$\max_{v,x}|f(v,x)|\le C$" is read as the uniform bound $|f|\le C$ and the "max" in $d(\epsilon)$ as a supremum;
  • "$d(\epsilon)\downarrow0$" is read as $d(\epsilon)\to0$ as $\epsilon\downarrow0$;
  • implicit hypotheses made explicit: $\mathcal F\ne\emptyset$, $\epsilon(n)>0$, measurability of $f(v,\cdot)$, $h^*$ a Lebesgue density;
  • the monotonicity in "$\epsilon(n)\downarrow0$, $n\epsilon(n)^m\uparrow\infty$" is kept in the goal; milestone 5 uses the limits only, as the paper states it;
  • the paper's $M_n$ ("there exists $\{M_n\}\to0$") is made explicit as $M_n=C\int|h_n-h^*|$, so Eq. (7) is stated for every sample.
• Remark 3.2 and Appendix B (an integrable envelope in place of boundedness) are not part of this mission.
• Every real infimum and supremum ranges over a nonempty set of values bounded by $C$ in absolute value, so no statement holds through a junk value; a formalization in which the supremum over $\mathcal F$ or the box infimum could be vacuous is excluded.
• The definitions (boxes, $\mathcal P_n$, the kernel, the estimator, $J_n$, $d$) live in one definition file. $\mathcal P_n$ duplicates, with weights $1/n$, the distribution set of mission I; the duplication is deliberate because draft missions cannot import each other.
• Welcome contributions: the kernel density estimator and its strong $L^1$ consistency as reusable infrastructure, and any of the deterministic milestones.

Selected references

• H. Xu, C. Caramanis, S. Mannor, A Distributional Interpretation of Robust Optimization, Mathematics of Operations Research 37(1):95–110, 2012. https://doi.org/10.1287/moor.1110.0531
• L. Devroye, The equivalence of weak, strong and complete convergence in $L_1$ for kernel density estimates, Annals of Statistics 11(3):896–904, 1983.
• L. Devroye, L. Györfi, Nonparametric Density Estimation: The $L_1$ View, Wiley, 1985.
• A. J. King, R. J.-B. Wets, Epi-consistency of convex stochastic programs, Stochastics and Stochastic Reports 34(1), 1991 (reference [22] of the paper).

Motivation

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

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

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

Setting

An uncertain linear program is

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

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

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

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

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

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

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

Formalization targets

Goal: Proposition 1 (pp. 418–419)

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

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

Milestones

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

Algorithmic stability asks how much the output of a learning algorithm changes when its training sample is perturbed. Since Devroye and Wagner (IEEE Trans. Inf. Theory 1979) it has served as a route to generalization bounds that does not go through the complexity of the hypothesis class. Bousquet and Elisseeff (JMLR 2002) popularised uniform stability, and Mukherjee, Niyogi, Poggio and Rifkin (Adv. Comput. Math. 2006) showed that for empirical risk minimisation in supervised learning, a leave-one-out type of stability is necessary and sufficient for consistency.

Shalev-Shwartz, Shamir, Srebro and Sridharan (JMLR 11, 2010) study stability in Vapnik's General Learning Setting, where uniform convergence can fail even though the problem is learnable. In Appendix A.2 they compare replace-one and leave-one-out (LOO) stability. For an empirical risk minimiser they prove that LOO stability is equivalent to consistency and to generalization, provided each property holds with one rate for all distributions (Theorem 31, p. 2667). This mission formalizes that theorem and the lemmas of Section 5.3 on which its proof rests.

Timeline:

• 1979, Devroye–Wagner: leave-one-out estimates for local rules.
• 2002, Bousquet–Elisseeff: uniform stability implies generalization.
• 2002, Kutin–Niyogi (UAI 2002): a taxonomy of stability notions.
• 2006, Mukherjee et al.: LOO stability characterises consistency of ERM in supervised learning.
• 2010, Shalev-Shwartz et al.: in the General Learning Setting, for ERMs, LOO stability, universal consistency and universal generalization are equivalent (Theorem 31). Universally consistent AERMs need not be LOO stable (Example 6).

Setting

A learning problem consists of an instance space $\mathcal Z$ with a $\sigma$-algebra, a nonempty hypothesis class $\mathcal H$, and an objective $f:\mathcal H\times\mathcal Z\to\mathbb R$ with $|f(h;z)|\le B$ for all $h,z$. For a probability measure $\mathcal D$ on $\mathcal Z$:

• the risk is $F(h)=\mathbb E_{z\sim\mathcal D}[f(h;z)]$ and the optimal risk is $F^*=\inf_{h}F(h)$;
• for a sample $S=(z_1,\dots,z_m)\sim\mathcal D^m$ of $m$ i.i.d. draws, the empirical risk is $F_S(h)=\frac1m\sum_{i}f(h;z_i)$, and $F_S(\hat h_S)=\inf_hF_S(h)$ denotes the minimal empirical risk;
• a learning rule $A$ maps each sample of size $m\ge1$ to a hypothesis $A(S)$. It is an ERM if $F_S(A(S))=F_S(\hat h_S)$ for every sample. It is an AERM with rate $\varepsilon_{\mathrm{erm}}$ if $\mathbb E[F_S(A(S))-F_S(\hat h_S)]\le\varepsilon_{\mathrm{erm}}(m)$;
• $A$ is consistent with rate $\varepsilon$ if $\mathbb E_{S\sim\mathcal D^m}[F(A(S))-F^*]\le\varepsilon(m)$. It generalizes with rate $\varepsilon$ if $\mathbb E[|F(A(S))-F_S(A(S))|]\le\varepsilon(m)$, and it on-average generalizes if $|\mathbb E[F(A(S))-F_S(A(S))]|\le\varepsilon(m)$;
• writing $S^{\setminus i}$ for $S$ with $z_i$ removed, $A$ is LOO stable with rate $\varepsilon$ (Definition 29) if

$$\frac1m\sum_{i=1}^m\mathbb E_{S\sim\mathcal D^m}\Big[\big|f(A(S^{\setminus i});z_i)-f(A(S);z_i)\big|\Big]\le\varepsilon(m).$$

A rate is a sequence $\varepsilon(m)$ that is non-increasing and tends to $0$. A property holds universally if it holds under every $\mathcal D$ with one and the same rate.

Formalization targets

Goal: Theorem 31

For an ERM $A$:

$$A\ \text{universally LOO stable}\iff A\ \text{universally consistent}\iff A\ \text{universally generalizes}.$$

The statement has no rates. Each side asserts that some rate exists and serves every distribution.

Milestones

In the order the proof uses them:

1. Utility Lemma 12: $\mathbb E|X-\mathbb EX|\le B/\sqrt m$ for the mean $X$ of $m$ i.i.d. variables bounded by $B$.
2. Utility Lemma 13: $X\le Y$ a.s. implies $\mathbb E|X|\le|\mathbb EX|+2\mathbb E|Y|$.
3. Lemma 14: an AERM that on-average generalizes with rate $\varepsilon_{\mathrm{oag}}$ generalizes with rate $\varepsilon_{\mathrm{oag}}+2\varepsilon_{\mathrm{erm}}+2B/\sqrt m$.
4. Lemma 15: under the same hypotheses the rule is consistent with rate $\varepsilon_{\mathrm{oag}}+\varepsilon_{\mathrm{erm}}$.
5. Lemma 16 (Main Converse Lemma): in a learnable problem, $\mathbb E|F_S(\hat h_S)-F^*|\le2\varepsilon_{\mathrm{cons}}(m')+2B/\sqrt m+2Bm'^2/m$ for $2\le m'\le m/2$.
6. Lemma 17: Eq. (12), together with an AERM that is consistent, gives generalization with rate $\varepsilon_{\mathrm{emp}}+\varepsilon_{\mathrm{erm}}+\varepsilon_{\mathrm{cons}}$.
7. First display of the proof of Theorem 31: a generalizing ERM is LOO stable with rate $\varepsilon_{\mathrm{gen}}(m-1)$.
8. Second display: a LOO stable ERM on-average generalizes on samples of size $m-1$ with rate $\varepsilon_{\mathrm{stable}}(m)+2B/m$.

Significance

Theorem 31 shows that for exact ERMs, LOO stability is not only sufficient but necessary for consistency. It transfers the supervised-learning characterisation of Mukherjee et al. to the General Learning Setting, where uniform convergence is no longer available as an intermediate. The hypothesis is sharp in one direction: Example 6 of the paper gives a universally consistent AERM that is not LOO stable. The equivalence therefore depends on exact minimisation, and an asymptotic minimiser does not suffice.

The lemmas are useful on their own. Lemmas 14 and 15 are the standard bridges between on-average generalization, generalization and consistency. Lemma 16 says that the minimal empirical risk estimates $F^*$ consistently in every learnable problem, even when no ERM learns. Lemma 16 also underlies Theorem 7, the paper's main characterisation of learnability, which is the subject of mission I of this series.

The results are proved in the paper. As far as is known they have not been formalized in any proof assistant. The platform has the textbook side of this framework (Shalev-Shwartz and Ben-David, Understanding Machine Learning, Chapter 13). Those statements are in $\mathbb R^d$ and use a replace-one stability notion; they do not cover leave-one-out stability or the General Learning Setting.

Difficulty

The implications between stability and generalization change the sample size: $S^{\setminus i}$ has $m-1$ points, so a statement about the rule at size $m$ has to be compared with the rule at size $m-1$ under the marginal law of the reduced sample. The step from universal consistency to generalization needs Lemma 16. That lemma estimates $F^*$ from a sample on which the ERM itself may be inconsistent, and it is the only place where universality of the consistency rate is used. Per-distribution consistency of an ERM does not imply generalization (Example 1 of the paper). An argument that fixes $\mathcal D$ throughout therefore cannot succeed.

Formalization scope

Samples are tuples $S:\mathrm{Fin}\,m\to\mathcal Z$ with law Measure.pi (the i.i.d. product), and $S^{\setminus i}$ is Fin.removeNth i S. A learning rule is a family $A_m:\mathcal Z^m\to\mathcal H$. Its value at $m=0$ is never used, and LOO stability is required only for $m\ge2$. $F_S(\hat h_S)$ is the infimum $\inf_hF_S(h)$ and no minimiser is chosen. An ERM is a rule attaining this infimum at every sample. A rate is non-increasing on $m\ge1$ and tends to $0$. Universal properties are stated as "there exists $\varepsilon$ with IsRate ε such that for every probability measure $\mathcal D$ …", with the rate chosen before the distribution. The bound $B$ is any bound on $|f|$; the paper's $B$ is $\sup|f|$, and all its rates increase with $B$.

Measurability is not discussed in the paper. The formalization assumes that each $f(h;\cdot)$ is measurable and that the rule is measurable in the sense that $(S,z)\mapsto f(A_m(S);z)$ is jointly measurable. Lemmas 14–17 also assume that $S\mapsto\inf_hF_S(h)$ is measurable. For a measurable ERM this holds automatically, so Theorem 31 makes no such assumption. Without these assumptions Lean's integral of a non-measurable function is $0$ and every rate bound would hold trivially. For the same reason Utility Lemma 13 assumes $X,Y$ integrable. The ERM hypothesis of the goal must not be weakened to an AERM: the statement would then be false (Example 6).

One statement corrects the printed text. In the second display of the proof of Theorem 31 (p. 2668), the chain adds $2B/m$ and then drops it. The milestone states the bound the argument proves, $\varepsilon_{\mathrm{stable}}(m)+2B/m$. The rate-free Theorem 31 is unaffected.

The development needs product measures, independence and variance bounds, all available in Mathlib, and the marginals of Measure.pi under removal of a coordinate. The definitions of risks, rules and stability notions can be reused by other stability results. Proofs of any milestone are welcome, and so are alternative proofs of the goal.

Selected references

• S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, Stability and Uniform Convergence, Journal of Machine Learning Research 11 (2010) 2635–2670. https://jmlr.org/papers/v11/shalev-shwartz10a.html
• O. Bousquet, A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://www.jmlr.org/papers/v2/bousquet02a.html
• S. Mukherjee, P. Niyogi, T. Poggio, R. Rifkin, Learning theory: stability is sufficient for generalization and necessary and sufficient for consistency of empirical risk minimization, Advances in Computational Mathematics 25 (2006) 161–193. https://doi.org/10.1007/s10444-004-7634-z
• S. Kutin, P. Niyogi, Almost-everywhere algorithmic stability and generalization error, UAI 2002. https://arxiv.org/abs/1301.0579
• L. Devroye, T. Wagner, Distribution-free performance bounds for potential function rules, IEEE Transactions on Information Theory 25(5) (1979) 601–604. https://doi.org/10.1109/TIT.1979.1056087

Motivation

Statistical learning theory asks when a rule that sees only an i.i.d. sample $z_1,\dots,z_m$ from an unknown distribution $D$ can return a hypothesis whose expected loss is close to the best possible. In supervised classification the classical answer is uniform convergence: learnability holds exactly when empirical risks converge to expected risks uniformly over the hypothesis class, and then empirical risk minimization (ERM) learns. Shalev-Shwartz, Shamir, Srebro and Sridharan (JMLR 11, 2010) showed that in Vapnik's broader General Learning Setting this picture breaks down. Their motivating example is stochastic convex optimization in a Hilbert space: minimizing an expected convex, Lipschitz objective over a bounded convex set from samples. This problem underlies regularized linear prediction, kernel methods and online-to-batch conversions, and the paper shows (§4.1) that in infinite dimension uniform convergence can fail and the plain empirical minimizer can fail to converge, while the problem is still learnable.

This mission formalizes the positive half of that example: Tikhonov-regularized ERM learns every such problem, with an explicit bound holding with probability $1-\delta$ (Theorem 3, p. 2644), through the stability of strongly convex empirical minimization (Theorem 2).

Setting

Let $Z$ be a measurable space of instances and $E$ a real Hilbert space. A stochastic convex optimization problem consists of a nonempty, closed, convex, bounded set $\mathcal H\subseteq E$ and an objective $f:E\times Z\to\mathbb R$ such that for every $z$ the map $h\mapsto f(h;z)$ is convex and $L$-Lipschitz on $\mathcal H$, each $f(h;\cdot)$ is measurable, and $|f(h;z)|\le C$ on $\mathcal H\times Z$. For a distribution $D$ on $Z$ define the risk and optimal risk

$$F(h)=\mathbb E_{z\sim D}[f(h;z)],\qquad F^*=\inf_{h\in\mathcal H}F(h),$$

and for a sample $S=(z_1,\dots,z_m)\sim D^m$ the empirical risk $F_S(h)=\frac1m\sum_{i=1}^m f(h;z_i)$. A function $g$ is $\lambda$-strongly convex on $\mathcal H$ if $g-\frac\lambda2\|\cdot\|^2$ is convex there. The regularized empirical minimizer is

$$\hat h_\lambda\in\operatorname*{arg\,min}_{h\in\mathcal H}\Big(F_S(h)+\frac\lambda2\|h\|^2\Big).\tag{5}$$

For the general part, a learning rule $A$ maps samples to hypotheses; it is an AERM with rate $\varepsilon_{\mathrm{erm}}$ if $\mathbb E[F_S(A(S))-\inf_hF_S(h)]\le\varepsilon_{\mathrm{erm}}(m)$, consistent with rate $\varepsilon_{\mathrm{cons}}$ if $\mathbb E[F(A(S))-F^*]\le\varepsilon_{\mathrm{cons}}(m)$, and uniform-RO stable with rate $\varepsilon_{\mathrm{stable}}$ if replacing any one sample point changes the loss at any test point by at most $\varepsilon_{\mathrm{stable}}(m)$ on average over the replaced index (Definition 4).

Formalization targets

Goal: Theorem 3

If $\|h\|\le B$ on $\mathcal H$, $L,B>0$, $\delta\in(0,1)$, $m\ge1$ and $\lambda=\sqrt{16L^2/(\delta B^2m)}$, then with probability at least $1-\delta$ over $S\sim D^m$

$$F(\hat h_\lambda)-F^*\ \le\ 4\sqrt{\frac{L^2B^2}{\delta m}}\Big(1+\frac8{\delta m}\Big).$$

The constants are the paper's.

Milestones, in the order the proof uses them

1. Quadratic growth at a minimizer of a $\lambda$-strongly convex $g$: $g(h')-g(h)\ge\frac\lambda2\|h'-h\|^2$ (§4.2, p. 2644).
2. Eq. (6): if $f(\cdot;z)$ is $\lambda$-strongly convex and $L$-Lipschitz, empirical minimizers of $S$ and of $S^{(i)}$ satisfy $|f(\hat h_S,z)-f(\hat h_S^{(i)},z)|\le 4L^2/(\lambda m)$ for all $z$ (p. 2645).
3. Theorem 8: a uniform- or average-RO stable AERM is consistent with rate $\varepsilon_{\mathrm{stable}}+\varepsilon_{\mathrm{erm}}$ and generalizes with rate $\varepsilon_{\mathrm{stable}}+2\varepsilon_{\mathrm{erm}}+2C/\sqrt m$ (p. 2649).
4. $\mathbb E_{S\sim D^m}[F(\hat h_S)-F^*]\le 4L^2/(\lambda m)$ for the strongly convex empirical minimizer (p. 2645).
5. Theorem 2: with probability $1-\delta$, $F(\hat h_S)-F^*\le 4L^2/(\delta\lambda m)$ (p. 2644).
6. Theorem 2 applied to $r(h;z)=\frac\lambda2\|h\|^2+f(h;z)$: with probability $1-\delta$, $\frac\lambda2\|\hat h_\lambda\|^2+F(\hat h_\lambda)\le\inf_h\big(\frac\lambda2\|h\|^2+F(h)\big)+4(L+\lambda B)^2/(\delta\lambda m)$ (p. 2645).

Significance

The result. Theorem 3 shows that every convex, Lipschitz, bounded stochastic optimization problem over a bounded subset of a Hilbert space is learnable at rate $O(LB/\sqrt{\delta m})$, with no dimension dependence and no uniform convergence. Together with the counterexamples of §4.1 it separates learnability from uniform convergence and from ERM, and it motivates the paper's general characterization: a problem is learnable if and only if it admits a uniform-RO stable asymptotic empirical risk minimizer (Theorem 7). Theorem 8 is the sufficiency half of that characterization and is reused wherever stability arguments give generalization bounds.

Formalizing it. The results are proved in the paper; to our knowledge none has a machine-checked proof. The closest platform material is the textbook treatment in Understanding Machine Learning, chapter 13 (Shalev-Shwartz and Ben-David): Corollary 13.9 (UnderstandingML.convex_lipschitz_bounded_learnable), Corollary 13.6 (rlm_lipschitz_stable) and Lemma 13.5 (strongly_convex_lemma). Those are stated in $\mathbb R^d$, bound the risk in expectation, use the regularizer $\lambda\|w\|^2$ over all of $\mathbb R^d$, and have different constants; the present mission works in an arbitrary Hilbert space, over a constraint set $\mathcal H$, with high-probability bounds and the paper's constants. Its definitions of learning rules, AERM, consistency and replace-one stability in the General Learning Setting are reusable by the other missions of this series.

Difficulty

The obvious route, bounding $\sup_{h\in\mathcal H}|F(h)-F_S(h)|$, is unavailable: §4.1 exhibits problems of exactly this type in which that supremum stays bounded away from zero for every sample size. Any successful argument therefore has to rely on a property of the learning rule rather than of the class $\mathcal H$, and the plain empirical minimizer does not have it: §4.1 shows it can stay a constant away from $F^*$ at every sample size. A second difficulty is purely formal: the regularization parameter $\lambda$ depends on $\delta$ and $m$, so the regularized minimizer changes with them, and all expectations involve a data-dependent hypothesis in a possibly non-separable Hilbert space, where measurability is not automatic.

Formalization scope

Lean conventions, fixed for every item:

• $E$ is a real inner product space with CompleteSpace E, never assumed finite-dimensional; $\mathcal H$ is Hset : Set E, and all infima, suprema, strong convexity and Lipschitz conditions are taken on Hset only. $F^*$ is ⨅ h : Hset, F h.
• Samples are Fin m → Z, $D^m$ is Measure.pi, $S^{(i)}$ is Function.update S i z', and $m\ge1$ throughout.
• The paper's standing loss bound $|f|\le B$ (p. 2637) is named $C$, because Theorem 3 uses $B$ for the norm bound $\|h\|\le B$. $L>0$ and $B>0$ are implicit in Theorem 3's choice of $\lambda$ and are stated.
• Strong convexity is Mathlib's StrongConvexOn Hset λ, which is the paper's definition.
• Minimizers are selections $S\mapsto\hat h_S\in\mathcal H$ satisfying the minimization property; the theorems hold for every such selection, hence for the minimizer, which is unique by strong convexity.
• Measurability, not discussed in the paper, is the series' single standing convention: each $f(h;\cdot)$ is measurable and the selection makes $(S,z)\mapsto f(\hat h_S;z)$ jointly measurable; for Theorem 8, the rule is measurable in the same sense and $S\mapsto\inf_hF_S(h)$ is measurable.
• "With probability at least $1-\delta$" is the bound $D^m\{\text{failure}\}\le\delta$ with $0<\delta<1$.

No statement of the paper is corrected: all printed constants were checked against the proofs and are reproduced exactly.

A formalization in which the expected excess risk is a Bochner integral of a non-measurable or non-integrable function, or in which $F^*$ is an infimum over all of $E$ or over an unbounded family, would make the bounds trivially true; the measurability hypotheses, the bound $|f|\le C$ and the infimum over the nonempty set $\mathcal H$ rule this out.

Contributions welcome: proofs of the milestones in order, and in particular a reusable replace-one identity $\mathbb E[F_S(A(S))]=\frac1m\sum_i\mathbb E[f(A(S^{(i)});z'_i)]$ under Measure.pi, and Markov's inequality in the form used for high-probability bounds.

Selected references

• S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, Stability and Uniform Convergence, Journal of Machine Learning Research 11 (2010) 2635–2670. https://jmlr.org/papers/v11/shalev-shwartz10a.html
• S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Stochastic Convex Optimization, COLT 2009. https://www.cs.mcgill.ca/~colt2009/papers/018.pdf
• O. Bousquet, A. Elisseeff, Stability and Generalization, Journal of Machine Learning Research 2 (2002) 499–526. https://jmlr.org/papers/v2/bousquet02a.html
• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, chapter 13. https://doi.org/10.1017/CBO9781107298019
• V. N. Vapnik, Statistical Learning Theory, Wiley, 1998.

Motivation

Paging is the problem of managing a two-level memory: a fast cache holds $k$ pages out of an address space of $n$ pages, requests to pages arrive one at a time, and a request to a page outside the cache (a page fault) forces the algorithm to bring that page in and, when the cache is full, to evict another. The cost is the number of faults. An on-line algorithm decides which page to evict without knowing future requests. The comparison of paging policies with the optimal off-line policy is where competitive analysis began.

Sleator and Tarjan showed that LRU and FIFO are within a factor $k$ of the off-line optimum and that no deterministic on-line algorithm does better than $k$ (Sleator–Tarjan 1985). Randomization changes the picture: Fiat, Karp, Luby, McGeoch, Sleator and Young introduced the marking algorithm and proved that its expected cost is within a factor $2H_k$ of the optimum, where $H_k = 1 + \frac12 + \dots + \frac1k \approx \ln k$ (arXiv:cs/0205038).

Timeline.

• 1985: Sleator and Tarjan: LRU and FIFO are $k$-competitive; no deterministic algorithm beats $k$.
• 1988: Karlin, Manasse, Rudolph and Sleator coin "competitive" and analyse flush-when-full (Algorithmica 3).
• 1990: Manasse, McGeoch and Sleator introduce the $k$-server problem and define competitiveness for randomized algorithms (J. Algorithms 11).
• 1991: Fiat et al.: the marking algorithm is $2H_k$-competitive, and $H_{n-1}$-competitive when $k = n-1$; no randomized paging algorithm beats $H_k$.
• 1991: McGeoch and Sleator give an $H_k$-competitive randomized paging algorithm (Algorithmica 6).
• 2000: Achlioptas, Chrobak and Noga determine the exact competitive ratio of the marking algorithm, $2H_k - 1$ (Theoret. Comput. Sci. 234).

Setting

The paper works in the uniform $k$-server problem, which is isomorphic to paging. There is a set $M$ of $n$ vertices, enumerated $e(0), \dots, e(n-1)$, and moving a server between two distinct vertices costs $1$. There are $k$ servers, $1 \le k \le n$. A request is a vertex, and after each request some server must be on it. Cached pages are covered vertices; a fault is a server move.

The marking algorithm starts with its servers on $e(0), \dots, e(k-1)$ and keeps a set of marked vertices, initially the covered ones. On a request to $r$:

1. Marking. $r$ is marked; the moment $k+1$ vertices are marked, all marks except the one on $r$ are erased.
2. Serving. If $r$ is covered, nothing moves. Otherwise a server is chosen uniformly at random among the covered unmarked vertices and moved to $r$.

The marks are updated before the server is chosen. For a finite request sequence $\sigma$, $C_M(\sigma)$ is the algorithm's expected number of server moves. $\mathrm{OPT}(\sigma)$ is the least number of moves with which $k$ servers, starting from the same configuration $C_0$ and knowing $\sigma$ in advance, can serve $\sigma$.

A randomized algorithm is $c$-competitive if there is a constant $a$ such that $C_M(\sigma) \le c \cdot C_B(\sigma) + a$ for every request sequence $\sigma$ and every algorithm $B$.

The marks divide $\sigma$ into phases. A new phase begins at the request that would make $k+1$ vertices marked. A vertex is clean in a phase if it was not requested in the previous phase and not yet in this one, and stale if it was requested in the previous phase but not yet in this one.

Formalization targets

Goal: Theorem 1

$$\exists\, a \in \mathbb R\ \ \forall \sigma:\qquad C_M(\sigma) \;\le\; 2H_k \cdot \mathrm{OPT}(\sigma) + a .$$

The constant $a$ may depend on $n$, $k$ and the enumeration, never on $\sigma$.

Milestones (proof of Theorem 1, pp. 4–5)

1. Without loss of generality the adversary is lazy: no move on a covered request, exactly one move otherwise (reference item, already proved on the platform).
2. At the start of every phase the marked vertices are exactly the covered ones, and the first request of a phase is unmarked.
3. In a phase with $l$ clean requests, a lazy adversary pays $C_A \ge l - d$, where $d$ counts its servers off the marking algorithm's servers at the start of the phase.
4. It also pays $C_A \ge d'$, where $d'$ counts its servers off the final marked set at the end of the phase.
5. Hence $C_A \ge \max(l-d, d') \ge \tfrac12(l - d + d')$.
6. A request to a stale vertex is a fault with probability $c/s$ ($c$ clean vertices requested so far, $s$ stale vertices left).
7. The marking algorithm's expected cost in a phase is at most $l(H_k - H_l + 1) \le lH_k$.

Companions

• Theorem 2: for $k = n-1$, $C_M(\sigma) \le H_{n-1} \cdot \mathrm{OPT}(\sigma) + a$.
• Tightness remark (pp. 5–6): for $k = 2$, $n = 4$ there is no $a$ with $C_M(\sigma) \le H_2 \cdot \mathrm{OPT}(\sigma) + a$ for all $\sigma$.

Significance

The result. Theorem 1 was the first proof that randomization beats the deterministic barrier $k$ for paging, bringing the ratio down to $O(\log k)$. Together with the paper's lower bound $H_k$ for every randomized algorithm, it determines the randomized competitive ratio of paging up to a factor $2$. Its phase and clean/stale accounting is reused throughout the analysis of randomized caching.

Formalizing it. The theorem is proved (1991). As far as is known it has no machine-checked proof. Formalizing it requires a probabilistic model of a randomized on-line algorithm, an off-line optimum, and a phase decomposition with an exchangeability argument, and these are the first such objects in this library. Theorem 2 and the $k = 2$, $n = 4$ example use the same definitions and also check that the formal algorithm is the paper's. The sharp ratio $2H_k - 1$ is a natural follow-up.

Difficulty

The comparison is between a random process and a deterministic adversary, and each side has its own obstacle.

On the algorithm's side, the configuration inside a phase is random, and the fault probability of a stale request depends on the whole history of the phase. The claim that the $c$ uncovered stale vertices form a uniformly random subset of the $s$ stale ones is an exchangeability property of the process, and must be established from the step-by-step uniform choice. The worst-case ordering of the requests within a phase then has to be justified as a bound, not assumed.

On the adversary's side, the per-phase bound $\max(l-d, d')$ does not sum directly. The $d$ and $d'$ terms telescope across phases only because the configuration of the marking algorithm at each phase boundary is deterministic. The first phase, which begins after an initial run of requests to $e(0), \dots, e(k-1)$, and the last, incomplete phase have to be absorbed into the additive constant.

Formalization scope

The vertex set is an abstract metric space $M$ with $e : \mathrm{Fin}\,n \simeq M$ and $\mathrm{dist}(x,y) = 1$ for $x \ne y$. The natural metric $|i - j|$ on $\mathrm{Fin}\,n$ is deliberately not used. The configurations and the off-line optimum $\mathrm{OPT}$ are the published KServer definitions (KServer.Config, KServer.offlineCost), with $\mathrm{OPT}$ taken from the marking algorithm's initial configuration. An off-line algorithm starting elsewhere changes the cost by at most $k$, which is absorbed into $a$.

The marking algorithm is a Markov chain on pairs (covered set, marked set). Each step is a PMF, with the eviction drawn by PMF.uniformOfFinset from the covered unmarked vertices. The expected cost is the sum over requests of the probability that the request is not covered, which is exact because the algorithm moves exactly one server per fault. Harmonic numbers are Mathlib's harmonic, cast to $\mathbb R$. Phases, clean counts and lazy off-line schedules are defined once, in the mission's definition file, and all milestones use them.

A trivializing formalization is ruled out as follows. The additive constant is quantified before $\sigma$, so a per-sequence constant cannot be used. The comparison is with the optimum over all off-line schedules, not a particular one. The random choice is among the covered unmarked vertices, with marks updated first. The hypothesis $1 \le k \le n$ excludes the degenerate case $k = 0$, where $H_0 = 0$.

Proofs of individual milestones are welcome. The laziness reduction for off-line schedules, the exchangeability lemma for the uniform eviction process, and the harmonic-sum identity $\sum_{j=l+1}^{k} l/j = l(H_k - H_l)$ are reusable beyond this mission.

Selected references

• A. Fiat, R. M. Karp, M. Luby, L. A. McGeoch, D. D. Sleator, N. E. Young, Competitive Paging Algorithms, J. Algorithms 12(4):685–699, 1991; arXiv:cs/0205038v1. https://arxiv.org/abs/cs/0205038
• D. D. Sleator, R. E. Tarjan, Amortized Efficiency of List Update and Paging Rules, Comm. ACM 28(2):202–208, 1985. https://doi.org/10.1145/2786.2793
• A. R. Karlin, M. S. Manasse, L. Rudolph, D. D. Sleator, Competitive Snoopy Caching, Algorithmica 3:79–119, 1988. https://doi.org/10.1007/BF01762111
• M. S. Manasse, L. A. McGeoch, D. D. Sleator, Competitive Algorithms for Server Problems, J. Algorithms 11(2):208–230, 1990. https://doi.org/10.1016/0196-6774(90)90003-W
• L. A. McGeoch, D. D. Sleator, A Strongly Competitive Randomized Paging Algorithm, Algorithmica 6:816–825, 1991. https://doi.org/10.1007/BF01759073
• D. Achlioptas, M. Chrobak, J. Noga, Competitive Analysis of Randomized Paging Algorithms, Theoret. Comput. Sci. 234:203–218, 2000. https://doi.org/10.1016/S0304-3975(98)00116-9

Motivation

In a linear regression with many more candidate variables than observations, least squares is not defined uniquely and does not estimate anything useful. The Lasso (Tibshirani, 1996) replaces it by an $\ell_1$-penalised least-squares problem, which is convex, can be solved at scale, and returns sparse coefficient vectors. The question that a statistician, a signal-processing engineer or an operations researcher fitting a sparse model must answer before trusting it is quantitative: how far is the Lasso estimate from the true coefficient vector, how well does it predict, and how many variables does it select, as functions of the sample size $n$, the number of variables $M$ and the sparsity $s$ of the truth?

Bickel, Ritov and Tsybakov (arXiv:0801.1095, Ann. Statist. 37(4), 2009) answered this under the restricted eigenvalue (RE) condition, which they introduced, with explicit constants and an explicit failure probability. Their Theorem 7.2, the goal of this mission, is a standard reference result of high-dimensional statistics and a model for the Lasso analyses in the textbooks of Bühlmann and van de Geer (2011) and Wainwright (2019).

Timeline, restricted to what each work proved:

• 2007: Candès and Tao (arXiv:math/0506081) prove $\ell_2$ bounds for the Dantzig selector under a uniform uncertainty principle.
• 2007: Bunea, Tsybakov and Wegkamp (doi:10.1214/07-EJS008) prove sparsity oracle inequalities for the Lasso under mutual-coherence conditions; Lemma B.1 of the present paper is essentially their Lemma 1.
• 2008/2009: Bickel, Ritov and Tsybakov prove Theorem 7.2 under RE$(s,3)$ and RE$(s,m,3)$, conditions weaker than those of the previous works.

Setting

A deterministic design matrix $X\in\mathbb R^{n\times M}$ with columns $x_{(1)},\dots,x_{(M)}$ is observed together with

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

where $\beta^*\in\mathbb R^M$ is unknown and $w=(W_1,\dots,W_n)$ has independent $\mathcal N(0,\sigma^2)$ entries with $\sigma>0$. Throughout, $n\ge1$, $M\ge2$, and every diagonal entry of the Gram matrix $\Psi_n=X^\top X/n$ equals $1$.

For $\delta\in\mathbb R^M$ write $|\delta|_p=(\sum_j|\delta_j|^p)^{1/p}$, $J(\delta)=\{j:\delta_j\ne0\}$ for the support, $\mathcal M(\delta)=|J(\delta)|$ for the sparsity, and $\delta_J$ for the vector that agrees with $\delta$ on $J$ and vanishes off $J$. The largest eigenvalue of $\Psi_n$ is $\phi_{\max}$.

The Lasso estimator with tuning parameter $r>0$ is any minimiser

$$\hat\beta_L\in\arg\min_{\beta\in\mathbb R^M}\Big\{\frac1n|y-X\beta|_2^2+2r|\beta|_1\Big\}.$$

Minimisers exist but need not be unique.

Assumption RE$(s,c_0)$ ($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 .$$

Assumption RE$(s,m,c_0)$ ($1\le s\le M/2$, $m\ge s$, $s+m\le M$) 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 in absolute value coordinates of $\delta$ outside $J_0$.

Formalization targets

Goal: Theorem 7.2

Let $\mathcal M(\beta^*)\le s$, let RE$(s,3)$ hold, and let $r=A\sigma\sqrt{\log M/n}$ with $A>2\sqrt2$. With probability at least $1-M^{1-A^2/8}$, every Lasso solution satisfies

$$|\hat\beta_L-\beta^*|_1\le\frac{16A}{\kappa^2(s,3)}\sigma s\sqrt{\frac{\log M}{n}},\qquad |X(\hat\beta_L-\beta^*)|_2^2\le\frac{16A^2}{\kappa^2(s,3)}\sigma^2s\log M,\qquad \mathcal M(\hat\beta_L)\le\frac{64\phi_{\max}}{\kappa^2(s,3)}s,$$

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

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

Milestones

In the order in which the paper's proof uses them:

1. (B.4): the noise event $\mathcal A=\bigcap_j\{2|\tfrac1n x_{(j)}^\top w|\le r\}$ has $\mathbb P(\mathcal A^c)\le M^{1-A^2/8}$.
2. (B.6): the optimality conditions of the Lasso.
3. Lemma B.1 (Section 7 case): the basic inequality (B.1) for all $\beta$, the residual bound (B.2) and the sparsity bound $\mathcal M(\hat\beta_L)\le4\phi_{\max}\|f_{\hat\beta_L}-f\|_n^2/r^2$ (B.3).
4. Corollary B.2: the error $\delta=\hat\beta_L-\beta$ lies in the cone $|\delta_{J_0^c}|_1\le3|\delta_{J_0}|_1$.
5. (B.30)–(B.31): on $\mathcal A$, $\frac1n|X\delta|_2^2\le16r^2s/\kappa^2$ and $|\delta_{J_0}|_2\le4r\sqrt s/\kappa^2$.
6. (B.27) and (B.28) with $c_0=3$: $\ell_1$ and $\ell_2$ norms of a cone vector.
7. The $\ell_p$ interpolation $\sum a_j^p\le b_1^{2-p}b_2^{p-1}$.

Significance

The result. Theorem 7.2 gives, for fixed $n$ and $M$ rather than asymptotically, the rate $s\log M/n$ for the prediction loss and $s\sqrt{\log M/n}$ for the $\ell_1$ loss of the Lasso, under a condition on the design only (RE), with no assumption on how $M$ compares with $n$. The dependence on $M$ is only logarithmic, which is what makes the Lasso usable when $M\gg n$. Bound (7.9) shows that the Lasso selects at most a constant multiple of $s$ variables, and (7.10) covers every $\ell_p$ loss between $\ell_1$ and $\ell_2$. Together with Theorem 7.1 for the Dantzig selector, the result shows that the two estimators have the same rates.

Formalizing it. The theorem is proved on paper. As far as a search of the platform shows, there is no machine-checked proof of a probabilistic Lasso rate. The closest platform statement, HighDimStat.SparseLinear.lasso_l2_error_bound (Wainwright, Theorem 7.13(a)), is deterministic, assumes a lower bound on the regularisation parameter in place of Gaussian noise, uses a restricted eigenvalue condition over the cone of one fixed support, and concludes an $\ell_2$ bound with a different constant. A formal proof of Theorem 7.2 would supply the Gaussian maximal inequality, the Lasso optimality conditions, and the cone and interpolation inequalities as reusable lemmas.

Difficulty

Each step is short on paper, and none of the steps is deep. The main work is in three places. First, the probability: the event on which the deterministic argument runs involves all $M$ correlations $\frac1n x_{(j)}^\top w$ at once, and its probability must be bounded by exactly $M^{1-A^2/8}$, which requires the law of a linear combination of independent Gaussians and a sharp Gaussian tail estimate, not a generic concentration bound with unspecified constants. Second, the Lasso is defined only through its minimising property, while the sparsity bound (7.9) is a statement about the number of non-zero coordinates of a minimiser of a non-differentiable objective; the characterisation (B.6) of minimisers is not in Mathlib. Third, (7.10) involves two restricted eigenvalue constants, a ranking of coordinates with possible ties, and real exponents, and every constant has to come out exactly.

The obvious idea of proving (7.7)–(7.10) for one fixed minimiser does not suffice: the statement quantifies over every minimiser on a single event.

Formalization scope

The design $X$ is a Matrix (Fin n) (Fin M) ℝ; vectors are functions Fin M → ℝ. The noise is a family W : Fin n → Ω → ℝ of independent, measurable random variables with law gaussianReal 0 σ² on a probability space, and $y(\omega)=X\beta^*+W(\omega)$. The probabilistic conclusion is one measurable event $E$ with $\mathbb P(E)\ge1-M^{1-A^2/8}$ on which every minimiser of (7.2) satisfies all bounds; the event does not depend on the minimiser, on $m$ or on $p$. $\log$ is the natural logarithm.

RE$(s,3)$ and RE$(s,m,3)$ are stated through witnesses: a predicate "$\kappa\sqrt n|\delta_{J_0}|_2\le|X\delta|_2$ for every admissible $J_0$ and $\delta$", and the theorem holds for every witness $\kappa>0$. Because the paper's $\kappa(s,c_0)$ is an attained minimum, every witness is at most it and the bounds decrease in $\kappa$, so this is equivalent to the printed statement. The assumption quantifies over every $J_0$ with $|J_0|\le s$, as on page 7, not only over the support of $\beta^*$. $\phi_{\max}$ is the supremum of $\frac1n|Xx|_2^2$ over unit vectors $x$. Lemma B.1 is stated in its Section-7 specialisation (unit column norms, $f=X\beta^*$), the form used in the proof of Theorem 7.2; (B.28) is stated for every $c_0>0$ and (B.27) likewise, since the paper writes them with $c_0=1$ and invokes them with $c_0=3$. The printed Theorem 7.2 needs no correction; all four constants were checked against the proof.

A formalization in which the noise is not Gaussian, the Lasso predicate can be vacuous, the RE condition is imposed only on the support of $\beta^*$, or the probability is that of a non-measurable set, is not this theorem and is ruled out by the statement.

Needed infrastructure: Gaussian tail bounds and the law of a linear combination of independent Gaussians (largely in Mathlib), subdifferential calculus for $\ell_1$-penalised least squares, and elementary finite-sum inequalities. The cone inequalities (B.27)–(B.28), the interpolation inequality and the optimality conditions (B.6) are reusable in other sparse-estimation missions; contributions to any milestone are welcome.

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 ; https://doi.org/10.1214/08-AOS620
• F. Bunea, A. B. Tsybakov, M. H. Wegkamp, Sparsity oracle inequalities for the Lasso, Electron. J. Statist. 1, 169–194, 2007. https://doi.org/10.1214/07-EJS008
• 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://arxiv.org/abs/math/0506081
• R. Tibshirani, Regression shrinkage and selection via the lasso, J. R. Statist. Soc. B 58(1), 267–288, 1996. https://doi.org/10.1111/j.2517-6161.1996.tb02080.x
• M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Chapter 7. https://doi.org/10.1017/9781108627771