Statistics

Motivation

In best arm identification with fixed confidence, a learner samples $K$ unknown distributions ("arms") one at a time, and must eventually stop and name the arm with the largest mean, with an error probability at most a prescribed risk $\delta$, while using as few samples as possible. The problem goes back to the sequential design of experiments (Chernoff, 1959; Even-Dar, Mannor and Mansour, 2006) and underlies adaptive A/B testing, clinical trial design and hyperparameter selection.

Any fixed-confidence strategy consists of three parts: a sampling rule, a stopping rule and a decision rule. Garivier and Kaufmann (arXiv:1602.04589, COLT 2016) proposed the Track-and-Stop strategy, the first shown to match the asymptotic lower bound on the expected sample complexity. Its stopping rule is a generalized likelihood ratio (GLR) test, Chernoff's stopping rule. Its correctness, the guarantee that the recommended arm is wrong with probability at most $\delta$, must hold whatever the sampling rule, which is what allows the sampling rule to be tuned freely for efficiency. This mission formalizes that guarantee for Bernoulli arms, Theorem 10 of the paper, with its explicit threshold $\beta(t,\delta) = \log(2t(K-1)/\delta)$.

Setting

The arms are $\mathcal A = \{1,\dots,K\}$. A Bernoulli bandit model is a mean vector $\boldsymbol\mu = (\mu_1,\dots,\mu_K) \in [0,1]^K$: pulling arm $a$ returns reward $1$ with probability $\mu_a$ and $0$ otherwise, independently of the past. The class $\mathcal S$ contains the models with a unique optimal arm $a^*(\boldsymbol\mu)$, i.e. $\mu_{a^*} > \mu_i$ for all $i \ne a^*$.

At round $t$ the learner chooses an arm $A_t$ as a (possibly randomized) function of the past observations and observes a reward $X_t$. Write $N_a(t)$ for the number of pulls of arm $a$ among the first $t$ rounds, $s_a(t)$ for the number of those pulls that returned $1$, and $\hat\mu_a(t) = N_a(t)^{-1}\sum_{s \le t} X_s \mathbb 1\{A_s = a\}$ for the empirical mean. The likelihood of arm $a$'s observations under mean $u$ is $p_u(\underline X^a_{N_a(t)}) = u^{s_a(t)}(1-u)^{N_a(t)-s_a(t)}$.

The GLR statistic for "arm $a$ is at least as good as arm $b$" is

$$Z_{a,b}(t) = \log \frac{\max_{\mu'_a \ge \mu'_b} p_{\mu'_a}(\underline X^a_{N_a(t)})\, p_{\mu'_b}(\underline X^b_{N_b(t)})}{\max_{\mu'_a \le \mu'_b} p_{\mu'_a}(\underline X^a_{N_a(t)})\, p_{\mu'_b}(\underline X^b_{N_b(t)})}.$$

Chernoff's stopping rule with exploration rate $\beta(t,\delta)$ is

$$\tau_\delta = \inf\{t \ge 1 : \exists a \in \mathcal A,\ \forall b \ne a,\ Z_{a,b}(t) > \beta(t,\delta)\},$$

and the decision rule recommends $\hat a_{\tau_\delta} \in \operatorname{argmax}_a \hat\mu_a(\tau_\delta)$.

The Krichevsky–Trofimov (KT) distribution on binary sequences $x \in \{0,1\}^n$ is $\mathrm{kt}(x) = \int_0^1 \big(\pi\sqrt{u(1-u)}\big)^{-1} p_u(x)\,\mathrm du$, the Bernoulli likelihood mixed over the Beta$(1/2,1/2)$ prior.

Formalization targets

Goal: Theorem 10

For every $\delta \in (0,1)$, every sampling strategy, and the threshold $\beta(t,\delta) = \log\big(2t(K-1)/\delta\big)$,

$$\forall \boldsymbol\mu \in \mathcal S,\qquad \mathbb P_{\boldsymbol\mu}\big(\tau_\delta < \infty,\ \hat a_{\tau_\delta} \ne a^*\big) \le \delta .$$

Milestone: Lemma 11 (Willems, Shtarkov and Tjalkens, 1995)

$\mathrm{kt}$ is a probability law on $\{0,1\}^n$, and for $n \ge 1$,

$$\sup_{x\in\{0,1\}^n}\ \sup_{u\in[0,1]} \frac{p_u(x)}{\mathrm{kt}(x)} \le 2\sqrt n .$$

Milestone: the pairwise crossing bound of Appendix C.1

With $T_{a,b} = \inf\{t : Z_{a,b}(t) > \beta(t,\delta)\}$, for all arms with $\mu_a < \mu_b$,

$$\mathbb P_{\boldsymbol\mu}(T_{a,b} < \infty) \le \frac{\delta}{K-1}.$$

Significance

Theorem 10 decouples correctness from efficiency. Because the guarantee holds for every sampling strategy, any sampling rule, including the C-Tracking and D-Tracking rules of Track-and-Stop, the uniform rule, or a heuristic, inherits $\delta$-correctness as soon as it is paired with Chernoff's stopping rule at this threshold. The asymptotic optimality result of the paper (Theorem 14) then only has to control the sample complexity. The threshold is explicit, with no unspecified constant, in contrast to the deviational threshold of Proposition 12.

The result is proved in the paper, in Appendix C.1, and rests on Lemma 11, which the paper quotes from the universal coding literature without proof. As far as the platform's catalog shows, none of these results is formalized. The platform holds a machine-checkable statement of the analogous result for Gaussian arms with the Lattimore–Szepesvári threshold (BanditAlgorithm.chernoff_stopping_rule_sound, Lemma 33.7 of Bandit Algorithms), which is a different model and a different threshold. Formalizing Theorem 10 adds a proof of Lemma 11 (the KT regret bound, reusable in information theory and universal prediction), the Bernoulli GLR statistic, and a change of measure from the true bandit law to a Bayesian mixture law on the trajectory space.

Difficulty

The obvious approach bounds, for each fixed $t$, the probability that $Z_{a,b}(t)$ exceeds $\beta(t,\delta)$ by a concentration inequality and sums over $t$. This fails: the sampling strategy is arbitrary and adaptive, so $N_a(t)$ and $N_b(t)$ are random and depend on the past rewards, and a fixed-sample-size deviation bound does not apply; a union bound over the possible values of the counts loses more than the threshold allows. The maximum likelihood in the numerator of $Z_{a,b}$ is also not a probability density, so the likelihood ratio cannot directly be read as a change of measure. The argument must control the whole trajectory law under an arbitrary randomized policy, and must handle empty samples (an arm never pulled contributes likelihood $1$) and the boundary means $0$ and $1$.

Formalization scope

The formalization is in Lean 4 with Mathlib and reuses the platform's canonical bandit model: StochasticBandit, BanditPolicy (a Markov kernel per round from the observed history to the next arm, so randomized strategies are included), banditTrajMeasure (the law of the infinite trajectory, where coordinate $s$ is round $s+1$) and IsSoundBAI from BanditTrajectory; bernoulliBandit from bernoulliRelativeEntropy; and only the pull counts trajPullCount and empirical means trajEmpiricalMean from TrackAndStop. The Gaussian GLR and threshold of TrackAndStop are not used.

Conventions committed to:

• Arms are Fin K. Bernoulli means range over $[0,1]$, degenerate laws included; the paper's exponential-family mean space is $(0,1)$, so the $[0,1]$ statement implies the paper's.
• $Z_{a,b}(t)$ is defined as the ratio of the two maxima over $[0,1]^2$, not by the closed form (7), which holds only when $\hat\mu_a(t) \ge \hat\mu_b(t)$. Both maxima are attained and positive.
• The stopping rule ranges over $t \ge 1$; at $t = 0$ there is no observation and the paper's $\beta(0,\delta) = \log 0$ is undefined. $\tau_\delta = \infty$ when the rule never fires.
• The decision rule is quantified: the goal holds for every recommendation that maximizes the empirical mean at $\tau_\delta$, whatever the tie-breaking.
• Probabilities of events are outer measures under the trajectory law; no measurability is assumed.
• $K \ge 1$ only. For $K = 1$ the statement is trivially true (no suboptimal arm).

Disclosed deviations from the page: Lemma 11's ratio bound is stated for $n \ge 1$, since at $n = 0$ the printed bound reads $1 \le 0$; the use of the lemma in Appendix C.1 is unaffected. Appendix C.1 calls the result "Proposition 10" (a slip for Theorem 10) and prints the KT density as $1/\sqrt{\pi u(1-u)}$ (a slip for $1/(\pi\sqrt{u(1-u)})$ of Lemma 11, which is the normalized one); the formalization follows Lemma 11.

A trivializing formalization is ruled out: stating the result for Gaussian arms or with the Lattimore–Szepesvári threshold is the platform's existing Lemma 33.7 and is not Theorem 10, and a free decision rule without the argmax hypothesis would make the claim false rather than faithful.

Contributions welcome: a proof of Lemma 11; a change-of-measure lemma for banditTrajMeasure under a mixture of environments; and the union-bound reduction from the goal to the pairwise claim.

Selected references

• A. Garivier, E. Kaufmann, Optimal Best Arm Identification with Fixed Confidence, COLT 2016 (JMLR W&CP 49), arXiv:1602.04589v2, 2016. https://arxiv.org/abs/1602.04589
• F. M. J. Willems, Y. M. Shtarkov, T. J. Tjalkens, The context-tree weighting method: basic properties, IEEE Transactions on Information Theory 41(3), 1995. https://doi.org/10.1109/18.382012
• R. Krichevsky, V. Trofimov, The performance of universal encoding, IEEE Transactions on Information Theory 27(2), 1981. https://doi.org/10.1109/TIT.1981.1056331
• H. Chernoff, Sequential design of experiments, Annals of Mathematical Statistics 30(3), 1959. https://doi.org/10.1214/aoms/1177706205
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 33. https://doi.org/10.1017/9781108571401

Motivation

Estimating a probability by the relative frequency of the event in an independent sample is justified for one event by the law of large numbers. Statistics and learning theory need more: the frequencies of a whole class of events $S$ must approach their probabilities simultaneously, so that a quantity chosen after looking at the data (the empirical risk minimizer, the empirical distribution function) is still close to its expectation. Glivenko's theorem on the empirical distribution function is the classical instance; empirical risk minimization rests on the same property for the class of loss sets of a model.

Vapnik and Chervonenkis, On the Uniform Convergence of Relative Frequencies of Events to Their Probabilities, Theory Probab. Appl. 16 (1971), treat this question in two parts. The first gives a distribution-free sufficient condition through the growth function (Theorems 1–3). The second, which this mission formalizes, gives a condition that is necessary and sufficient for a fixed distribution: Theorem 4, the entropy criterion.

Timeline. 1933: Glivenko and Cantelli prove uniform convergence for the class of rays $\{x \le a\}$ on the line. 1968: Vapnik and Chervonenkis announce the results in Dokl. Akad. Nauk SSSR 181. 1971: the full paper appears, with the growth-function bound and the entropy criterion. Later work (Talagrand 1987; Dudley, Giné and Zinn 1991) recasts such criteria as the theory of Glivenko–Cantelli classes.

Setting

Let $X$ be a set carrying a probability measure $P$, and $S$ a collection of measurable subsets of $X$ (events). A sample of size $l$ is a sequence $x_1, \dots, x_l$ of independent draws from $P$; repetitions are allowed. For $A \in S$ the relative frequency $\nu_A^{(l)}$ is the fraction of sample terms lying in $A$, and $P_A = P(A)$. The maximal deviation is

$$\pi^{(l)}(x_1, \dots, x_l) = \sup_{A \in S} \bigl|\nu_A^{(l)} - P_A\bigr| .$$

The relative frequencies converge in probability to the probabilities uniformly over $S$ when $\mathbf{P}\{\pi^{(l)} > \varepsilon\} \to 0$ as $l \to \infty$ for every $\varepsilon > 0$.

Each $A \in S$ induces in a sample the subsample of terms lying in $A$. The index $\Delta^S(x_1, \dots, x_l)$ is the number of different subsamples induced by the sets of $S$; it lies between $0$ and $2^l$. The entropy of $S$ in samples of size $l$ is

$$H^S(l) = \mathbf{E} \log_2 \Delta^S(x_1, \dots, x_l) .$$

For a sample of size $2l$, split into halves $x_1, \dots, x_l$ and $x_{l+1}, \dots, x_{2l}$ with relative frequencies $\nu'_A$ and $\nu''_A$, the semi-sample deviation is $\rho^{(l)} = \sup_{A \in S} |\nu'_A - \nu''_A|$. Finally $\Phi(n, r)$ is defined by the recurrence $\Phi(n, r) = \Phi(n, r-1) + \Phi(n-1, r-1)$, $\Phi(0, r) = \Phi(n, 0) = 1$.

Formalization targets

Goal: Theorem 4 (p. 275)

$$\Bigl(\forall \varepsilon > 0:\ \lim_{l\to\infty} \mathbf{P}\{\pi^{(l)} > \varepsilon\} = 0\Bigr) \iff \lim_{l \to \infty} \frac{H^S(l)}{l} = 0 .$$

Milestones

1. Entropy rate. (12) $\Delta^S(x_1, \dots, x_l) \le \Delta^S(x_1, \dots, x_k)\Delta^S(x_{k+1}, \dots, x_l)$; the subadditivity $H^S(l_1 + l_2) \le H^S(l_1) + H^S(l_2)$; Lemma 3, $H^S(l)/l \to c \in [0, 1]$; Lemma 4, $\mathbf{P}(|l^{-1}\log_2 \Delta^S - c| > \varepsilon) \to 0$.
2. Sufficiency. Lemma 2, $\mathbf{P}\{\pi^{(l)} > \varepsilon\} \le 2\,\mathbf{P}\{\rho^{(l)} \ge \varepsilon/2\}$ for $l \ge 2/\varepsilon^2$; the per-sample permutation bound $2\Delta^S(x_1, \dots, x_{2l}) e^{-\varepsilon^2 l/8}$; and

$$\mathbf{P}\{\rho^{(l)} \ge \tfrac{\varepsilon}{2}\} \le 2\Bigl(\frac{2}{e}\Bigr)^{\varepsilon^2 l/8} + \mathbf{P}\Bigl\{\tfrac{1}{2l}\log_2 \Delta^S(x_1, \dots, x_{2l}) > \tfrac{\varepsilon^2}{16}\Bigr\} .$$

3. Necessity. Lemma 1 (Sauer–Shelah in sequence form); step 1°, $1 - \mathbf{P}(C') \ge (1 - \mathbf{P}(Q))^2$ with $C' = \{\rho^{(l)} > 2\varepsilon\}$; (26), $\mathbf{P}\{\Delta^S > \Phi([ql], l)\} \to 1$ when $0 < q < \frac14$ and $q\log_2(2e/q) < c$; and (29), $\mathbf{P}\{\pi^{(l)} > \varepsilon\} \to 1$ when moreover $0 < \varepsilon < q/7$.

Significance

Theorem 4 characterizes uniform convergence for a given distribution exactly, with no gap between the necessary and the sufficient condition. It separates the cases the growth-function bound cannot: a class may have $m^S(l) = 2^l$ for every $l$ (all open subsets of $[0,1]$) and still satisfy $H^S(l)/l \to 0$ under a particular $P$, or fail it. The entropy $H^S(l)$ is the distribution-dependent quantity from which later work on Glivenko–Cantelli classes and on consistency of empirical risk minimization proceeds; the 1981 paper of the same authors extends the criterion to classes of functions. The quantitative form (29) states more than the negation of convergence: when the entropy rate is positive, the maximal deviation stays above a fixed $\varepsilon$ with probability tending to one.

The result has been proved since 1971; it has not been formalized. The platform holds Sauer–Shelah variants over sets of distinct points and PAC bounds with other constants, but no statement of the VC entropy or of Theorem 4. The mission produces machine-checked statements of the entropy criterion and of its supporting lemmas with the paper's own constants ($l \ge 2/\varepsilon^2$, $2e^{-\varepsilon^2 l/8}$, $\delta = \varepsilon^2/16$, $\varepsilon < q/7$).

Difficulty

The sufficiency half is a variant of the proof of the growth-function bound; its new ingredient is the concentration of $l^{-1} \log_2 \Delta^S$ (Lemma 4), which needs subadditivity and a law of large numbers over independent blocks of the sample rather than a single mean estimate. The hypergeometric tail estimate behind the permutation bound is omitted in the paper ("a simple but long computation").

Necessity is harder. The obvious attempt, bounding $\mathbf{P}\{\pi^{(l)} > \varepsilon\}$ from below by exhibiting a single bad event, fails: $S$ may be uncountable and no single $A$ deviates with non-vanishing probability. A positive entropy rate has to be converted into a combinatorial statement about typical samples ((26) combines Lemma 4 with an estimate of $\Phi([ql], l)$), and that statement back into a lower bound on a probability over the product measure; the constants $q < \frac14$ and $\varepsilon < q/7$ must be tracked through both conversions, and the conclusion $\lim \mathbf{P}\{\pi^{(l)} > \varepsilon\} = 1$ needs the unweakened inequality of step 1°.

Formalization scope

A sample of size $l$ is a function Fin l → X (positions $0, \dots, l-1$) and its law is the product measure Measure.pi (fun _ => P), with P a probability measure. A subsample is a set of positions, so the index counts distinct Finset (Fin l) of the form $\{i : x_i \in A\}$. The halves of x : Fin (l + l) → X are x ∘ Fin.castAdd l and x ∘ Fin.natAdd l. $P_A$ is P.real A; the suprema $\pi^{(l)}$ and $\rho^{(l)}$ are real suprema over the subtype of $S$ (values in $[0,1]$; $0$ for $S = \emptyset$). $H^S(l)$ is a Bochner integral of Real.logb 2 of the index, and $[ql]$ is ⌊q * l⌋₊. Probabilities are values in $[0, \infty]$, except in the inequalities between probabilities (step 1°, the sufficiency estimate), which use Measure.real.

Measurability. The paper assumes, and the statements carry as hypotheses, that the events of $S$ are measurable (p. 264), that $\pi^{(l)}$ is a random variable (p. 265), that $\rho^{(l)}$ is measurable (p. 268), and that the index is measurable in the sample (p. 273). Each statement carries the ones its proof uses. Without them the Bochner integral defining $H^S(l)$ can be the junk value $0$ and the equivalence can fail; replacing them by "$S$ countable" would weaken the theorem. The goal is not trivialized by degenerate cases: the equivalence is not vacuous for any class, and $S = \emptyset$ gives the true instance $H^S = 0$, $\pi^{(l)} = 0$.

Corrections of the printed text. Lemma 2 is printed for $l > 2/\varepsilon^2$; its proof gives $l \ge 2/\varepsilon^2$, which is stated. On p. 275 Lemma 2 is recalled as "$2\mathbf{P}(C) \ge \frac12 P(Q)$", meaning $\mathbf{P}(C) \ge \frac12\mathbf{P}(Q)$. On p. 276 the first display carries a stray upper limit "4" on the integral, and the region of integration is printed $\{\log_2 \Delta^S \le 2\delta\}$ where $\{\log_2\Delta^S \le 2\delta l\}$ is meant. The event $C'$ is defined with "$> 2\varepsilon$" (p. 276) but integrated in step 3° as $\theta(\cdot - 2\varepsilon)$, which counts "$\ge 2\varepsilon$"; the strict form is stated, and the estimate of step 3° is itself strict. Step 1° is stated unweakened. Milestone texts are verbatim.

Contributions welcome: a reusable development of the index and its submultiplicativity, the hypergeometric tail bound for sampling without replacement, a block law of large numbers for subadditive functionals of i.i.d. samples, and the permutation-invariance argument for product measures on Fin (l + l) → X.

Selected references

• V. N. Vapnik and A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and Its Applications 16(2) (1971), 264–280. https://doi.org/10.1137/1116025
• V. N. Vapnik and A. Ya. Chervonenkis, Necessary and sufficient conditions for the uniform convergence of means to their expectations, Theory of Probability and Its Applications 26(3) (1981), 532–553. https://doi.org/10.1137/1126059
• M. Talagrand, The Glivenko–Cantelli problem, Annals of Probability 15(3) (1987), 837–870. https://doi.org/10.1214/aop/1176992069
• R. M. Dudley, E. Giné and J. Zinn, Uniform and universal Glivenko–Cantelli classes, Journal of Theoretical Probability 4(3) (1991), 485–510. https://doi.org/10.1007/BF01210321

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

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

High-dimensional statistics studies estimation when the number of parameters $p$ is comparable to, or larger than, the number of observations $n$. The standard estimators in this regime are regularized M-estimators: minimise an empirical loss plus a penalty that encodes structure, such as the Lasso ($\ell_1$ penalty, sparse vectors), the group Lasso (block norms, group sparsity) and nuclear-norm regularization (low-rank matrices). Before 2009 each of these estimators came with its own consistency proof. Negahban, Ravikumar, Wainwright and Yu (arXiv:1010.2731; Statistical Science 27(4), 2012, doi:10.1214/12-STS400) isolated two properties that these proofs share, decomposability of the regularizer and restricted strong convexity of the loss, and proved one deterministic theorem from them. The Lasso rates of Bickel, Ritov and Tsybakov (arXiv:0801.1095), rates under $\ell_q$-sparsity, and group-sparse and low-rank rates then follow as corollaries. The framework is the organising principle of Chapter 9 of Wainwright's textbook High-Dimensional Statistics (Cambridge University Press, 2019).

Setting

Let $E$ be a finite-dimensional real inner product space with inner product $\langle\cdot,\cdot\rangle$ and induced error norm $\|\cdot\|$. Given a loss $\mathcal L:E\to\mathbb R$, a regularizer $\mathcal R:E\to\mathbb R$ and a constant $\lambda_n>0$, program (1) is

$$\hat\theta_{\lambda_n}\in\arg\min_{\theta\in E}\{\mathcal L(\theta)+\lambda_n\mathcal R(\theta)\}.$$

For a subspace $S$ write $u_S$ for the orthogonal projection of $u$ onto $S$, and $S^\perp$ for the orthogonal complement.

• Decomposability. For subspaces $\mathcal M\subseteq\overline{\mathcal M}$, the norm $\mathcal R$ is decomposable with respect to $(\mathcal M,\overline{\mathcal M}^\perp)$ if $\mathcal R(\theta+\gamma)=\mathcal R(\theta)+\mathcal R(\gamma)$ for all $\theta\in\mathcal M$ and $\gamma\in\overline{\mathcal M}^\perp$. Example: the $\ell_1$-norm with $\mathcal M=\overline{\mathcal M}=\{\theta:\theta_j=0\ \forall j\notin S\}$.
• Dual norm. $\mathcal R^*(v)=\sup_{\mathcal R(u)\le1}\langle u,v\rangle$.
• Subspace compatibility constant. $\Psi(\overline{\mathcal M})=\sup_{u\in\overline{\mathcal M}\setminus\{0\}}\mathcal R(u)/\|u\|$; for the $\ell_1$-norm on an $s$-dimensional coordinate subspace, $\Psi=\sqrt s$.
• The set $\mathbb C$. For a point $\theta^*\in E$,

$$\mathbb C(\mathcal M,\overline{\mathcal M}^\perp;\theta^*)=\{\Delta\mid\mathcal R(\Delta_{\overline{\mathcal M}^\perp})\le3\mathcal R(\Delta_{\overline{\mathcal M}})+4\mathcal R(\theta^*_{\mathcal M^\perp})\}.$$

• Restricted strong convexity (RSC). With the Taylor error $\delta\mathcal L(\Delta,\theta^*)=\mathcal L(\theta^*+\Delta)-\mathcal L(\theta^*)-\langle\nabla\mathcal L(\theta^*),\Delta\rangle$, the loss satisfies RSC with curvature $\kappa_{\mathcal L}>0$ and tolerance $\tau_{\mathcal L}(\theta^*)$ if $\delta\mathcal L(\Delta,\theta^*)\ge\kappa_{\mathcal L}\|\Delta\|^2-\tau^2_{\mathcal L}(\theta^*)$ for every $\Delta\in\mathbb C(\mathcal M,\overline{\mathcal M}^\perp;\theta^*)$.

The conditions of the paper's main theorem are (G1): $\mathcal R$ is a norm, decomposable with respect to $(\mathcal M,\overline{\mathcal M}^\perp)$ with $\mathcal M\subseteq\overline{\mathcal M}$; and (G2): $\mathcal L$ is convex, differentiable and satisfies RSC. The Lean development lives in the namespace UnifiedMEstimator.General, with these objects named IsNormFn, IsDecomposable, dualNorm, compat, setC, taylorErr, RSC and IsOptimal.

Formalization targets

Goal: Theorem 1 (p. 10), tolerance term corrected

Under (G1) and (G2), if $\lambda_n>0$ and $\lambda_n\ge2\mathcal R^*(\nabla\mathcal L(\theta^*))$, then every optimal solution of program (1) satisfies

$$\|\hat\theta_{\lambda_n}-\theta^*\|^2\le9\,\frac{\lambda_n^2}{\kappa_{\mathcal L}^2}\,\Psi^2(\overline{\mathcal M})+\frac{2\tau_{\mathcal L}^2(\theta^*)+4\lambda_n\mathcal R(\theta^*_{\mathcal M^\perp})}{\kappa_{\mathcal L}}.$$

The bound holds for every pair $(\mathcal M,\overline{\mathcal M})$ over which $\mathcal R$ decomposes, and for every optimum, not only a distinguished one.

Milestones

1. Lemma 1 (p. 7): under the dual-norm condition on $\lambda_n$, the error $\hat\Delta=\hat\theta_{\lambda_n}-\theta^*$ lies in $\mathbb C(\mathcal M,\overline{\mathcal M}^\perp;\theta^*)$. This milestone links an existing platform statement of the same lemma (Wainwright, Proposition 9.13).
2. Section 2.4, p. 10, first display: if $\theta^*\in\mathcal M$ and $\Delta\in\mathbb C$, then $\mathcal R(\Delta)\le4\Psi(\overline{\mathcal M})\|\Delta\|$.

Further statements

• Corollary 1 (p. 11): if $\theta^*\in\mathcal M$ and $\tau_{\mathcal L}(\theta^*)=0$, then $\|\hat\theta_{\lambda_n}-\theta^*\|\le3\lambda_n\Psi(\overline{\mathcal M})/\kappa_{\mathcal L}$ and $\mathcal R(\hat\theta_{\lambda_n}-\theta^*)\le12\lambda_n\Psi^2(\overline{\mathcal M})/\kappa_{\mathcal L}$.
• Section 2.4, p. 10, second display: a lower bound $\delta\mathcal L\ge\kappa_1\|\Delta\|^2-\kappa_2 g\,\mathcal R^2(\Delta)$ on the unit ball gives curvature $\kappa_1-16\kappa_2\Psi^2(\overline{\mathcal M})g$ on $\mathbb C$ when $\theta^*\in\mathcal M$.
• Example 1 (p. 5) and the value $\Psi(\mathcal M(S))=\sqrt{|S|}$ (p. 9): the $\ell_1$-norm instance, which shows that the hypotheses of the goal can be met.

Significance

Theorem 1 reduces a consistency proof for a new regularized estimator to two checks: that the regularizer decomposes over a pair of subspaces adapted to the model, and that the loss is curved on the set $\mathbb C$, together with a bound on $\mathcal R^*(\nabla\mathcal L(\theta^*))$ that is usually a concentration inequality. The paper derives from it the $s\log p/n$ Lasso rate under restricted eigenvalue conditions, rates for weakly sparse ($\ell_q$-ball) vectors, and group-Lasso rates; companion papers use it for low-rank matrix estimation, matrix completion and generalized linear models. Because the bound holds for every pair $(\mathcal M,\overline{\mathcal M})$, it gives an explicit trade-off between an estimation error and an approximation error $\mathcal R(\theta^*_{\mathcal M^\perp})$.

The theorem is proved in the paper's supplementary appendix. No machine-checked proof of it is known. On Prove2Me, Wainwright's textbook restatement (Theorem 9.19, HighDimStat.Decomposability.thm9_19_general_bound) is a related but different statement: its RSC condition is local, on a ball, with a tolerance proportional to $\mathcal R^2(\Delta)$, and it has extra side conditions and a different bound. A formal proof of the present goal certifies the deterministic core that every corollary of the paper relies on.

Difficulty

The obvious argument compares the objective at $\hat\theta$ and at $\theta^*$ and applies RSC to the error. RSC, however, is available only on the set $\mathbb C$, not on all of $E$: in high dimensions the loss is flat in many directions, so strong convexity fails. The work is to show first that the error lies in $\mathbb C$ (Lemma 1, which rests on decomposability and the choice of $\lambda_n$), and then to relate the regularizer to the error norm through the projections onto $\overline{\mathcal M}$ and $\overline{\mathcal M}^\perp$. The distinction between $\mathcal M$ and $\overline{\mathcal M}$ matters throughout: the compatibility constant is taken on the larger space $\overline{\mathcal M}$, while the approximation error projects $\theta^*$ onto the complement of the smaller one. The bound comes from a quadratic inequality in $\|\hat\Delta\|$, and the constants depend on how its terms are split.

Formalization scope

Representation. The parameter space is an arbitrary finite-dimensional real inner product space E (equivalently $\mathbb R^p$ with any inner product, as the paper allows); matrices are covered by the same abstraction. Subspaces are Submodule ℝ E, projections are Submodule.starProjection, and the gradient is Mathlib's gradient, under the hypothesis that $\mathcal L$ is differentiable. The dual norm and $\Psi$ are real suprema (sSup). They equal the paper's quantities because $\mathcal R$ is required to be a genuine norm (nonnegative, definite, absolutely homogeneous, subadditive) and $E$ is finite-dimensional; $\Psi(\{0\})=0$. The tolerance is a real number $\tau$ entering as $\tau^2$; RSC contains $\kappa>0$ and is quantified over exactly $\mathbb C(\mathcal M,\overline{\mathcal M}^\perp;\theta^*)$ for the same pair and point as the decomposability. Every statement is for every optimal solution of program (1). The data $Z_1^n$ are fixed and absorbed into $\mathcal L$, and $\theta^*$ is an arbitrary point: the paper's requirement that $\theta^*$ minimise the population risk is never used by the theorem and is dropped.

Corrections of the printed statements.

1. Display (22) prints the tolerance term as $\frac{\lambda_n}{\kappa_{\mathcal L}}\cdot2\tau^2_{\mathcal L}(\theta^*)$. As printed the statement is false: for $E=\mathbb R$, $\mathcal R=|\cdot|$, $\mathcal M=\overline{\mathcal M}=\mathbb R$, $\mathcal L(\theta)=(\max(0,|\theta|-1))^2$, $\theta^*=0.9$, $\lambda_n=0.01$, $\kappa_{\mathcal L}=1/2$, $\tau^2_{\mathcal L}=10$, the optimum is $0$ and $\|\hat\Delta\|^2=0.81$ exceeds the printed bound $0.4036$. The goal states $2\tau^2_{\mathcal L}(\theta^*)/\kappa_{\mathcal L}$; the two forms agree when $\tau_{\mathcal L}=0$, and the constants $9$ and $4$ are the paper's.
2. Corollary 1's (25a) prints $\|\hat\theta-\theta^*\|\le9\lambda_n^2\Psi^2(\overline{\mathcal M})/\kappa_{\mathcal L}$, which fails for $\mathcal L(\theta)=(\theta-0.002)^2$, $\theta^*=0.001$, $\lambda_n=0.004$ on $\mathbb R$; the mission states $3\lambda_n\Psi(\overline{\mathcal M})/\kappa_{\mathcal L}$. Its "$\mathbb C(\mathcal M,\overline{\mathcal M},\theta^*)$" is read as $\mathbb C(\mathcal M,\overline{\mathcal M}^\perp;\theta^*)$.

Trivializations ruled out. A regularizer predicate weaker than a norm would let the real suprema collapse to the junk value $0$ and make the $\lambda_n$ condition or the $\Psi$ term free; RSC over all of $E$ would be classical strong convexity, and RSC over the cone without the $4\mathcal R(\theta^*_{\mathcal M^\perp})$ slack would make the goal false; decomposability without $\mathcal M\subseteq\overline{\mathcal M}$ or with the bars misplaced changes the theorem. None of these is used. The $\ell_1$ example and a checked one-dimensional instance show that all hypotheses of the goal can hold simultaneously.

Infrastructure and contributions. A complete development needs: Hölder's inequality for a norm and its dual norm, boundedness of the two suprema in finite dimension, the decomposability inequality $\mathcal R(\theta^*+\Delta)-\mathcal R(\theta^*)\ge\mathcal R(\Delta_{\overline{\mathcal M}^\perp})-\mathcal R(\Delta_{\overline{\mathcal M}})-2\mathcal R(\theta^*_{\mathcal M^\perp})$, the first-order characterization of convexity, and the solution of a scalar quadratic inequality. The dual-norm and compatibility-constant lemmas are reusable for every decomposable-regularizer mission. Proofs of the milestones, of the goal, and of the $\ell_1$ instance are all welcome.

Selected references

• S. N. Negahban, P. Ravikumar, M. J. Wainwright, B. Yu, A Unified Framework for High-Dimensional Analysis of M-Estimators with Decomposable Regularizers, Statistical Science 27(4), 2012, 538–557. arXiv:1010.2731v3, doi:10.1214/12-STS400
• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous Analysis of Lasso and Dantzig Selector, Annals of Statistics 37(4), 2009, 1705–1732. arXiv:0801.1095
• M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Chapter 9. doi:10.1017/9781108627771