Machine Learning

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

Motivation

Classifiers trained to high standard accuracy on image benchmarks can be made to fail by perturbations of the input that are small in the $\ell_\infty$ norm (Szegedy et al., 2014; Goodfellow et al., 2015). Adversarial training reaches high robust accuracy on the training set, but on CIFAR10 the robust accuracy on held-out data is much lower than on the training set (Madry et al., 2018). That is, robust generalization fails.

Schmidt, Santurkar, Tsipras, Talwar and Mądry (arXiv:1804.11285) ask whether this is a statistical phenomenon: does learning a robust classifier need more samples than learning an accurate one, even in the simplest distributional model? This mission formalizes their answer for a mixture of two Gaussians. In that model, with $\|\theta^\star\|_2 = \sqrt d$ and $\sigma \le c\, d^{1/4}$, a single sample suffices for standard generalization (their Theorem 4). Robust generalization, by contrast, needs a number of samples that grows polynomially with the dimension, for every learning algorithm.

Setting

Write $\mathbb R^d$ for the feature space and $\{\pm 1\}$ for the labels.

• The $\ell_\infty$ perturbation set of radius $\varepsilon$ around $x$ is $\mathcal B_\infty^\varepsilon(x) = \{x' \in \mathbb R^d : \|x' - x\|_\infty \le \varepsilon\}$.
• For $\theta \in \mathbb R^d$ and $\sigma > 0$, the $(\theta, \sigma)$-Gaussian model $P_{\theta,\sigma}$ is the law of $(x, y)$ obtained by drawing $y$ uniformly from $\{\pm1\}$ and then $x \sim \mathcal N(y\theta, \sigma^2 I)$ (Definition 1). Here $\sigma$ is a standard deviation.
• The $\ell_\infty^\varepsilon$-robust classification error of a classifier $f : \mathbb R^d \to \{\pm1\}$ under a distribution $P$ is $\mathbb P_{(x,y) \sim P}[\exists\, x' \in \mathcal B_\infty^\varepsilon(x) : f(x') \ne y]$ (Definitions 2–3). With $\varepsilon = 0$ it is the ordinary classification error.
• A learning algorithm $g_n$ maps $n$ labelled samples $S \in (\mathbb R^d \times \{\pm 1\})^n$ to a classifier $f_n = g_n(S)$.
• The expected robust error $\Xi$ of $g_n$ is the robust error of $g_n(S)$ under $P_{\theta,\sigma}$, averaged over $S \sim P_{\theta,\sigma}^{\otimes n}$ and then over a prior $\theta \sim \mathcal N(0, I)$. The learner sees $S$ but not $\theta$.

Formalization targets

Goal: Corollary 23 (p. 30)

For every learning algorithm $g_n$, every $\sigma > 0$ and every $\varepsilon \ge 0$,

$$n \le \frac{\varepsilon^2\sigma^2}{8\log d} \quad\Longrightarrow\quad \Xi \ \ge\ \Big(1 - \frac1d\Big)\frac12 .$$

Theorem 11 (p. 28)

For every learning algorithm $g_n$, every $\sigma > 0$ and every $\varepsilon \ge 0$,

$$\Xi \ \ge\ \frac12\, \mathbb P_{v \sim \mathcal N(0, I)}\Big[\sqrt{\tfrac{n}{\sigma^2+n}}\,\|v\|_\infty \le \varepsilon\Big].$$

Intermediate statements (milestones)

1. Eq. (2). Given $n$ samples $z_i \sim \mathcal N(\theta, \sigma^2 I)$, the posterior of $\theta \sim \mathcal N(0, I)$ is $\mathcal N(\mu', \Sigma')$ with $\mu' = (\sigma^2+n)^{-1}\sum_i z_i$ and $\Sigma' = \frac{\sigma^2}{\sigma^2+n} I$. The expectations over $\theta$ and over the samples may therefore be exchanged.
2. Eq. (3). Averaging $P_{\theta,\sigma}$ over $\theta \sim \mathcal N(m, s^2 I)$ gives $P_{m, \sqrt{s^2+\sigma^2}}$.
3. The bound on $\Psi$. If $\|m\|_\infty \le \varepsilon$, every classifier has $\ell_\infty^\varepsilon$-robust error at least $\frac12$ under $P_{m,s}$.
4. The law of $\bar z$. The sample mean $\bar z$ of the $z_i$ is marginally $\mathcal N(0, (1+\sigma^2/n) I)$.
5. Maximum of $d$ Gaussians. $\mathbb P_{v\sim\mathcal N(0,I_d)}[\|v\|_\infty \le 2\sqrt{2\log d}] \ge 1 - 1/d$.

Corollary 23 is the goal because it is the statement the paper advertises: its main-text Theorem 6 is Corollary 23 with $\sigma = c_1 d^{1/4}$.

Significance

In the same model with $\|\theta^\star\|_2 = \sqrt d$ and $\sigma$ of order $d^{1/4}$, a single sample suffices to reach standard error below 1% (Theorem 4 of the paper), and on the order of $\varepsilon^2\sqrt d$ samples suffice for robust error below 1% when $\varepsilon$ is below a small constant (Theorem 5; Corollary 22, formalized in mission 3 of this series). Corollary 23 shows that, up to the logarithmic factor, no learner can do better. Robust generalization then needs $\varepsilon^2 \sqrt d / \log d$ times as many samples as standard generalization. The gap is information-theoretic: it concerns every algorithm, not a particular training procedure or model class. The authors present this as a candidate explanation for the robust-generalization gap observed on CIFAR10. The ½ is tight: a constant classifier attains it.

The paper's proof is complete and short. As far as a search of the platform shows, none of its statements has been formalized. A machine-checked version requires multivariate Gaussian conjugacy, Gaussian convolution identities, the outer-measure robust event, and a union bound for the maximum of Gaussians. The Gaussian conjugacy and convolution facts are standard and appear throughout Bayesian statistics. As of this Mathlib version they are not available for stdGaussian on EuclideanSpace.

Difficulty

The obvious attempt fixes $\theta$ and bounds the robust error for each $\theta$. That fails: a learner may ignore the data and output the Bayes-optimal robust classifier for one fixed $\theta$, so for each $\theta$ some learner does well. The lower bound holds only on average over the prior on $\theta$. The classifier $f_n$ depends on the samples, and the samples depend on $\theta$, so the classifier and the test distribution are correlated through $\theta$. A second obstacle is measure-theoretic. The robust error of a classifier is the probability of an $\ell_\infty$-thickening of an arbitrary set $\{f \ne y\}$. Such a set need not be Borel, and it must be bounded below with no structure on the classifier beyond what the learner provides. The same statement with the $\ell_2$ ball is a different theorem.

Formalization scope

• $\mathbb R^d$ is EuclideanSpace ℝ (Fin d) with its Borel σ-algebra; $\mathcal N(0, I)$ is Mathlib's stdGaussian; $\mathcal N(m, s^2 I)$ is its image under $v \mapsto m + s v$, so every Gaussian parameter in the development is a standard deviation.
• The $\ell_\infty$ ball is written coordinatewise ($|x'_i - x_i| \le \varepsilon$ for all $i$), because the ambient norm is $\ell_2$. $\|v\|_\infty \le r$ is written the same way.
• Labels are Bool, with true for $+1$. A classifier is ℝ^d → Bool, and a learning algorithm is (Fin n → ℝ^d × Bool) → ℝ^d → Bool.
• A model is a measure on $\mathbb R^d \times$ Bool; $n$ samples form the product measure Measure.pi.
• The robust event need not be Borel. Its probability is the outer measure, which is its probability under the completion. The expectations are lower Lebesgue integrals.
• Theorem 11 and Corollary 23 assume the learner is jointly measurable in (samples, input). This is the only condition on it. $\log$ is the natural logarithm. With Lean's conventions $\log 0 = \log 1 = 0$ and $x/0 = 0$, the goal's hypothesis forces $n = 0$ for $d \le 1$, where the statement is still true.
• The paper writes the posterior mean as $\frac{n}{\sigma^2+n}\bar z$, with "$\bar z = \sum_i z_i$" on p. 28. The formalization uses $(\sigma^2+n)^{-1}\sum_i z_i$, which is the posterior mean. It agrees with the paper when $\bar z$ is read as the sample mean, as it is on p. 30.

A formalization that fixes $\theta$ instead of averaging over the prior, that restricts the learner (to linear classifiers, or to classifiers that do not depend on the data), that uses the $\ell_2$ ball, or that assumes the posterior formula as a hypothesis states a different theorem. These are ruled out by the definitions file.

Needed infrastructure: the multivariate Gaussian conjugacy and convolution identities for stdGaussian pushforwards, translation invariance of outer measure under Gaussian shifts, and a sub-Gaussian tail bound for one coordinate. The Gaussian identities are reusable well beyond this mission. Contributions of general Gaussian lemmas, stated for stdGaussian on any finite-dimensional inner product space, are welcome. Related platform work: missions 2–4 of this series formalize the Bernoulli-model lower bound and the two upper bounds of the same paper.

Selected references

• L. Schmidt, S. Santurkar, D. Tsipras, K. Talwar, A. Mądry, Adversarially Robust Generalization Requires More Data, NeurIPS 2018; arXiv:1804.11285v2, 2018. https://arxiv.org/abs/1804.11285
• A. Madry, A. Makelov, L. Schmidt, D. Tsipras, A. Vladu, Towards Deep Learning Models Resistant to Adversarial Attacks, ICLR 2018. https://arxiv.org/abs/1706.06083
• C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, R. Fergus, Intriguing properties of neural networks, ICLR 2014. https://arxiv.org/abs/1312.6199
• I. Goodfellow, J. Shlens, C. Szegedy, Explaining and Harnessing Adversarial Examples, ICLR 2015. https://arxiv.org/abs/1412.6572
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013 (Theorem 5.8). https://doi.org/10.1093/acprof:oso/9780199535255.001.0001

Motivation

A forecaster who announces "70% chance of rain" is calibrated if, among the days on which that number was announced, it rained on about 70% of them. Dawid (The well-calibrated Bayesian, JASA 1982) proposed calibration as the minimal requirement of an honest probability forecaster. Oakes (Self-calibrating priors do not exist, JASA 1985) showed that no deterministic forecasting rule can be calibrated against every sequence of outcomes: an adversary who knows the rule can always choose the outcome that contradicts the forecast.

Foster and Vohra (Calibrated learning and correlated equilibrium, Games Econ. Behav. 21 (1997) 40–55) use calibration as the bridge between learning and equilibrium in repeated games. Their Theorem 1 says that if each player best-responds to calibrated forecasts of the opponent, the empirical distribution of play converges to the set of correlated equilibria. That theorem is only useful if calibrated forecasts can actually be produced whatever the opponent does. Theorem 3 of the paper, credited to an unpublished 1991 manuscript of the same authors and proved in the paper's Appendix, says they can, provided the forecaster randomizes.

Timeline. Dawid (1982) defines calibration. Oakes (1985) rules out deterministic calibrated forecasting against arbitrary sequences. Foster and Vohra (1991 manuscript; 1997 paper, Theorem 3 and Appendix) give a randomized forecaster calibrated against any opponent, through a pairwise ("internal") no-regret property. The full argument appeared in Foster and Vohra, Asymptotic calibration, Biometrika 85 (1998). Hart and Mas-Colell (A simple adaptive procedure leading to correlated equilibrium, Econometrica 2000) later made internal regret the standard route to correlated equilibrium.

Setting

Player 2 has $n\ge 1$ pure strategies $j\in\{0,\dots,n-1\}$. In every round, player 1 announces a forecast $p\in\mathbb R^n$, a probability vector ($p_j\ge 0$, $\sum_j p_j = 1$), and player 2 plays a strategy $j$. The two moves are simultaneous: player 2 does not see the current forecast.

A history $h$ of length $t$ is the list of the $t$ pairs (forecast, play), oldest first. For a forecast vector $p$ and a strategy $j$:

• $N(p,t)$ is the number of rounds of $h$ in which $p$ was forecast;
• $\rho(p,j,t)$ is the fraction of those rounds in which player 2 played $j$ (and $0$ if $N(p,t)=0$);
• the calibration score (Eq. (1), p. 49) is

$$C_t = \sum_p\sum_j \bigl|\rho(p,j,t) - p_j\bigr|\,\frac{N(p,t)}{t}.$$

A randomized forecaster $F$ maps each history to a probability distribution on forecasts. A learning rule $A$ of player 2 maps each history to a probability distribution on strategies. In round $t+1$ the forecast is drawn from $F(h)$ and the play from $A(h)$, independently given the history $h$ of the first $t$ rounds. This defines the law $\mathbb P_{F,A}$ of the first $t$ rounds (histLaw F A t).

For the Appendix: with $k$ forecasts, losses $L_t^i$ and mixing weights $w_t^i$, the pairwise regret of replacing forecast $i$ by forecast $j$ is

$$R_T^{i\to j} = \max\Bigl\{0,\ \sum_{t=1}^T w_t^i\,(L_t^i - L_t^j)\Bigr\}.$$

Formalization targets

Goal: Theorem 3 (p. 49)

There is a forecaster $F$, with probability-vector forecasts, such that for every learning rule $A$ of player 2 and every $\varepsilon>0$,

$$\lim_{t\to\infty}\mathbb P_{F,A}\bigl(C_t<\varepsilon\bigr) = 1.$$

The forecaster is fixed before the opponent; no rate is claimed, and the rate may depend on $A$.

Milestones, in the order the Appendix uses them

1. Flow conservation is solvable (p. 52). For every nonnegative $k\times k$ matrix $R$, $k\ge 1$, there is a probability vector $w$ with $w^i\sum_j R^{i\to j} = \sum_j w^j R^{j\to i}$ for all $i$.
2. Lemma 1 (No-Regret) (p. 52). With losses in $[0,1]$ and weights solving flow conservation for the previous regrets,

$$R_T^{i\to j}\le\sqrt{2kT}\quad\text{for all } i,j,T.$$

3. Regrets sandwich L-2 calibration (p. 54). For a grid $p^1,\dots,p^k$ that is $\varepsilon$-dense in squared distance and losses $L_t^i = |X_t - p^i|^2$,

$$\sum_i\max_j \frac{R_T^{i\to j}}{T}\ \le\ C_{2,w}(T)\ \le\ \varepsilon + \sum_i\max_j\frac{R_T^{i\to j}}{T},$$

with $C_{2,w}$ the fractional L-2 calibration score. 4. L-1 versus L-2 (p. 54). For each $j$, $\sum_p|\rho(p,j,t)-p_j|\,N(p,t)/t \le \sqrt{\sum_p(\rho(p,j,t)-p_j)^2 N(p,t)/t}$.

Significance

The result. Theorem 3 makes the hypothesis of Theorem 1 attainable: combined, they show that there are learning procedures under which play converges in probability to the set of correlated equilibria of any finite game (the paper's Corollary, p. 49). The intermediate Lemma 1 is an early internal-regret bound; internal (swap) regret minimization later became the standard algorithmic route to correlated equilibria and to calibrated prediction in online learning.

Formalizing it. The result is proved, in the 1997 Appendix in telegraphic form and in full in Foster and Vohra (1998). The Appendix leaves several steps informal (see Formalization scope), so a machine-checked proof must supply them. No formalization of calibration or of internal regret was found on Prove2Me as of 2026-09-26. The mission produces a formal model of randomized forecasters against adaptive opponents, a checked internal-regret bound with an explicit constant, and the passage from regret to calibration.

Difficulty

The obvious approach is to pick, at each round, a forecast that corrects the current miscalibration. This is a deterministic rule, and by Oakes' theorem an opponent can defeat it. Randomization alone does not help either: the forecaster must randomize in a way that controls every pairwise regret $R^{i\to j}$ at once, not only the regret against the best fixed forecast. External no-regret does not imply calibration.

Two further gaps separate Lemma 1 from Theorem 3. First, the Appendix controls a fractional score in which the event "forecast $p^i$ was issued" is replaced by its probability $w_t^i$. The realized calibration score involves the random choices, so a concentration argument is needed against an adaptive opponent. Second, a fixed grid gives calibration only up to its mesh $\varepsilon$. Exact convergence requires letting the grid size $k$ grow and $\varepsilon$ shrink over time, and the scores of the different phases must be combined.

Formalization scope

• Model. Strategies are Fin n; forecasts are vectors Fin n → ℝ that are probability vectors (IsDist). Histories are Lean lists of (forecast, play) pairs, oldest first. Forecaster and opponent are maps from histories to Mathlib PMFs. The history law is built with PMF.bind/PMF.map, with the two draws independent given the past. $\mathbb P(C_t<\varepsilon)$ is the toOuterMeasure of the law, in ℝ≥0∞; no σ-algebra on histories is used.
• Opponent. The opponent may be randomized and may depend on all past forecasts and plays; fixed sequences and deterministic rules are special cases. The opponent never sees the current forecast. Letting it see the current forecast would make the goal false, and restricting to fixed sequences would make it weaker than the paper.
• Quantifiers. The forecaster is chosen before the opponent (∃ F, ∀ A). The reverse order is trivial, since one can forecast $A$'s next play.
• Conventions. Rounds are counted from $0$, so the paper's rounds $1,\dots,t$ are the first $t$ list entries. The paper's $R_{t-1}$ is the regret over the $0$-based rounds before $t$. Forecasts are grouped by exact equality of real vectors. Sums over $p$ run over the forecasts that occur, and every other term vanishes. Scores divide by the history length, and are $0$ for the empty history. "Converges in probability" is the $\lim\mathbb P(C_t<\varepsilon)=1$ form the page states. The grid of milestone 3 is indexed $1,\dots,k$ (the page writes $i = 0,\dots,k$ on p. 53 and $1,\dots,k$ in Lemma 1), and "within $\varepsilon$" is read in squared Euclidean distance.
• Pinned reading. The page writes the middle term of milestone 3 as $E(C_2(t))$ with a garbled formula. The mission states the inequality for the fractional score $C_{2,w}$, for which it holds.
• Steps the paper leaves informal, not stated as milestones. (a) "$E(C_2(t))\le\varepsilon + O(k/\sqrt2)$" when the weights solve flow conservation; the $O$-term is garbled and should decay in $t$. (b) "if we let $k$ grow slowly and $\varepsilon$ go slowly to zero … $C_2(t)\to 0$ in expectation which implies $C_2(t)\to0$ in probability by Jensen's inequality", together with the passage from the fractional score to the realized one. Solvers will have to formalize these steps on the way to the goal.
• Not included. The Corollary on p. 49 (convergence in probability of play to the correlated equilibria when both players use the scheme). It needs the game layer and a quantitative form of Theorem 1, and the page gives no proof.
• Infrastructure welcome. Finite Markov chain stationary distributions (for milestone 1), for which Prove2Me has MarkovChain.exists_isStationary for row-stochastic matrices. Also useful: martingale concentration for PMF-built processes, and Cauchy–Schwarz with weights. The history-law construction is reusable for any repeated forecasting game.

Selected references

• D. P. Foster and R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21 (1997) 40–55. https://doi.org/10.1006/game.1997.0595
• D. P. Foster and R. V. Vohra, Asymptotic calibration, Biometrika 85 (1998) 379–390. https://doi.org/10.1093/biomet/85.2.379
• A. P. Dawid, The well-calibrated Bayesian, J. Amer. Statist. Assoc. 77 (1982) 605–613. https://doi.org/10.1080/01621459.1982.10477856
• D. Oakes, Self-calibrating priors do not exist, J. Amer. Statist. Assoc. 80 (1985) 339. https://doi.org/10.1080/01621459.1985.10478117
• S. Hart and A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68 (2000) 1127–1150. https://doi.org/10.1111/1468-0262.00153

Motivation

A correlated equilibrium (Aumann 1974) is a joint distribution over the players' strategy profiles such that no player gains by deviating from the strategy the distribution recommends to them. It is the equilibrium notion that learning dynamics in repeated games most naturally reach, and a basic question in learning in games is which simple rules, played repeatedly, drive the empirical distribution of play to the set of correlated equilibria.

Foster and Vohra (1997) answer this with a hypothesis on forecasts instead of a particular algorithm. Each player forecasts the other's next move and best-responds to the forecast. They only require the forecasts to be calibrated in the sense of Dawid (1982): among the rounds in which a player forecast a given probability vector, the empirical frequencies of the opponent's moves must approach that vector. Their Theorem 1 says that this already forces the empirical joint distribution of play to approach the set of correlated equilibria. The paper uses this to argue that Bayesian players under a common prior, whose forecasts are calibrated by Dawid's theorem, end up playing a correlated equilibrium. That is an alternative to Aumann's (1987) derivation of correlated equilibrium from common priors and rationality.

Timeline:

• Aumann (1974, 1987) introduces correlated equilibrium and derives it from Bayesian rationality.
• Dawid (1982) proposes calibration as a minimal requirement on probability forecasts.
• Foster and Vohra (1997) prove Theorem 1 (this mission) and show that calibrated forecasts exist once the forecaster may randomize.
• Hart and Mas-Colell (2000) give regret matching, an adaptive procedure with the same limit set.

Setting

A finite two-player game $G$ has strategy sets $S(1) = \{0, \dots, m-1\}$ and $S(2) = \{0, \dots, n-1\}$ and payoff matrices $u_1, u_2 : S(1) \times S(2) \to \mathbb{R}$, which the players maximize. A joint distribution $D$ is a nonnegative $m \times n$ matrix with entries summing to $1$. It is a correlated equilibrium if

$$\sum_{x,y} D(x,y)\, u_1(\Phi(x), y) \le \sum_{x,y} D(x,y)\, u_1(x,y) \quad \text{for all } \Phi : S(1) \to S(1),$$

and symmetrically for player 2. The set of correlated equilibria is $\pi(G)$.

The game is played in rounds $s = 0, 1, 2, \dots$. In round $s$ player 1 issues a forecast $f_1(s)$, a probability vector over $S(2)$, and player 2 issues a forecast $f_2(s)$ over $S(1)$. Each player then plays a best response to its forecast, $x(s) = R_1(f_1(s))$ and $y(s) = R_2(f_2(s))$. Here $R_1$ and $R_2$ are best-reply functions: $R_1(p)$ maximizes $\sum_y p_y u_1(\cdot, y)$ for every probability vector $p$, and $R_1$ is a fixed function of the forecast alone. This is the paper's standing assumption of a stationary, deterministic tie-breaking rule.

For a forecast sequence $f$ and the opponent's plays $z$, $N(p,t)$ counts the rounds among the first $t$ in which $f$ forecast $p$. $\rho(p,j,t)$ is the fraction of those rounds in which the opponent played $j$, and $0$ if there are none. The forecast is calibrated with respect to $z$ if for every $j$

$$\sum_p |\rho(p,j,t) - p_j|\, \frac{N(p,t)}{t} \longrightarrow 0 \qquad (t \to \infty).$$

The empirical joint distribution $D_t(x,y)$ is the fraction of the first $t$ rounds in which player 1 played $x$ and player 2 played $y$.

Formalization targets

Goal: Theorem 1

If $f_1$ is calibrated with respect to $y$ and $f_2$ is calibrated with respect to $x$, then

$$\min_{D \in \pi(G)} \ \max_{x \in S(1),\, y \in S(2)} |D_t(x,y) - D(x,y)| \longrightarrow 0 \qquad (t \to \infty).$$

The goal fixes no rate and no particular forecasting method: it asserts only convergence of $D_t$ to the set $\pi(G)$, for every calibrated forecast.

Milestones: the steps of the proof (pp. 44–45)

1. $D_t$ lies in the simplex for $t \ge 1$.
2. For each $x \in S(1)$, the set $M_b(x)$ of mixtures to which $x$ is a best response is closed and convex.
3. The mixtures $M_p(x)$ at which player 1 actually plays $x$ satisfy $M_p(x) \subseteq M_b(x)$.
4. The identity writing $D_t(x,y)$ as a forecast-weighted term plus a calibration error.
5. Calibration makes the error term vanish.
6. The weighted average of the forecasts at which player 1 plays $x$ lies in $M_b(x)$.
7. For a convergent subsequence $D_{t_i} \to D$, every row of $D$ with positive mass, normalized, lies in $M_b(x)$.
8. Every subsequential limit of $D_t$ is a correlated equilibrium.

Further result: matching pennies (p. 46)

With the constant forecast $(1/2, 1/2)$ and the non-stationary tie-break "heads on even rounds, tails on odd rounds", both forecasts are calibrated and every play is a best reply, yet $D_t$ does not approach $\pi(G)$. The stationarity assumption cannot be dropped.

Significance

The result. Theorem 1 separates what learning needs from how it is achieved. Any forecasting procedure that is calibrated, combined with myopic best responses, yields correlated equilibrium behaviour in the long run. The paper's Theorem 3 constructs a randomized calibrated forecaster, so the theorem gives an uncoupled learning procedure for correlated equilibrium, one that needs no knowledge of the opponent's payoffs. The converse direction, that every correlated equilibrium arises this way for almost every game, is the paper's Theorem 2 (a separate mission of this series).

Formalizing it. The theorem is proved in the paper and has no machine-checked proof on Prove2Me or, to the knowledge of this mission, elsewhere. The platform's existing correlated-equilibrium results (the Algorithmic Game Theory swap-regret development, AGT.swap_regret_correlated_equilibrium) reach correlated equilibrium through swap regret of mixed strategies, a different hypothesis and a different object. This mission adds a formal notion of calibration and the convergence argument, both reusable for the paper's Theorems 2 and 3 and for later work on calibration and learning.

Difficulty

The obvious reading of calibration is that each player's forecast converges to the opponent's empirical distribution; if that held, best responses to it would give convergence. It does not hold. Calibration constrains the opponent's frequencies only conditionally on the forecast issued, and the forecasts need not converge at all. What must be shown is a statement about the conditional distributions of the joint play given each strategy of player 1, while the set of forecasts issued keeps growing. Rows of the limit with zero mass carry no conditional distribution. The "min → 0" form also asks for more than a property of limit points: it is a uniform statement about all large $t$.

Formalization scope

• Strategies are Fin m and Fin n; payoffs are real matrices; forecasts are real vectors required to be probability vectors in every round.
• A correlated equilibrium is the joint-distribution form of p. 44 (the correlated strategy on a finite probability space is represented by its law). It is the $\varepsilon = 0$, two-player, payoff (not cost) instance of the published AGT.IsCorrelatedEquilibrium, restated rather than imported.
• The stationary deterministic tie-break is modelled by arbitrary best-reply functions $R_i$ of the forecast. They do not depend on the round, and the statements quantify over all of them, which includes the lowest-index rule.
• Forecasts are sequences $f_i : \mathbb{N} \to \mathbb{R}^k$. The theorem uses only the realized forecasts, and every sequence is realized by a rule reading the round number from the history.
• Rounds are indexed from $0$: "the first $t$ rounds" are $0, \dots, t-1$. $D_0 = 0$ by Lean's division convention; only $t \ge 1$ and limits are used.
• The calibration sum runs over the forecasts issued in the first $t$ rounds, which is the paper's sum over all $p$ with its zero terms removed. $\rho(p,j,t) = 0$ when $N(p,t) = 0$, as on the page.
• "min … → 0" is stated as: for every $\varepsilon > 0$, eventually some $D \in \pi(G)$ is within $\varepsilon$ of $D_t$ in every coordinate. The two forms are equivalent because $\pi(G)$ is compact and nonempty. The formalization avoids an infimum over $\pi(G)$, which Lean would evaluate to $0$ on an empty set.
• A statement that drops the best-reply property, the probability-vector condition on forecasts, or the stationarity of $R_i$ is not Theorem 1: the matching pennies example shows the last one is essential. Swapping the calibration hypotheses (player 1's forecast calibrated against player 1's own plays) type-checks when $m = n$ and is not the theorem.
• Only the two-player case is claimed. The paper says the results "generalize easily to the $n$-person case" without proof.

Proofs of any milestone, and reusable lemmas about calibration scores and compactness of the simplex of joint distributions, are welcome.

Selected references

• D. P. Foster, R. V. Vohra, Calibrated learning and correlated equilibrium, Games and Economic Behavior 21 (1997) 40–55. https://doi.org/10.1006/game.1997.0595
• R. J. Aumann, Subjectivity and correlation in randomized strategies, Journal of Mathematical Economics 1 (1974) 67–96. https://doi.org/10.1016/0304-4068(74)90037-8
• R. J. Aumann, Correlated equilibrium as an expression of Bayesian rationality, Econometrica 55 (1987) 1–18. https://doi.org/10.2307/1911154
• A. P. Dawid, The well-calibrated Bayesian, Journal of the American Statistical Association 77 (1982) 605–610. https://doi.org/10.1080/01621459.1982.10477856
• S. Hart, A. Mas-Colell, A simple adaptive procedure leading to correlated equilibrium, Econometrica 68 (2000) 1127–1150. https://doi.org/10.1111/1468-0262.00153

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