Statistics · Prove2Me

Machine Learning Probability·Captain: mikedeng1

Adversarially Robust Generalization Requires More Data 2: A Robust-Error Lower Bound for Linear Classifiers in the Bernoulli ModelResearch Paper

Motivation

Classifiers trained by standard methods reach high accuracy on image benchmarks and yet change their prediction under perturbations of each pixel that are invisible to a human. Training against such perturbations (adversarial training) improves robustness, but on CIFAR10 and SVHN the robust test accuracy stays far below the robust training accuracy: robust models overfit. Schmidt, Santurkar, Tsipras, Talwar and Mądry (arXiv:1804.11285, 2018) asked whether this gap is a failure of current methods or an information-theoretic fact about the number of samples needed. They introduced two simple data models in which a single sample suffices for standard accuracy and proved that robust accuracy needs many more samples.

This mission formalizes their lower bound for the second model, the Bernoulli model on the hypercube, which was designed to resemble MNIST (whose images are close to binary). In this model the lower bound holds for linear classifiers, and the paper shows separately that a non-linear classifier (thresholding followed by a linear rule) escapes it. The result therefore isolates a concrete way in which the model class, not only the amount of data, governs robust generalization.

Setting

Let $d\ge0$ and $\tau>0$ . Points are $x\in\{\pm1\}^d\subset\mathbb R^d$ , labels $y\in\{\pm1\}$ . For a parameter $\theta^\star\in\{\pm1\}^d$ , the $(\theta^\star,\tau)$ -Bernoulli model draws $y$ uniformly from $\{\pm1\}$ and then, independently for every coordinate $i$ , sets $x_i=y\theta^\star_i$ with probability $\tfrac12+\tau$ and $x_i=-y\theta^\star_i$ with probability $\tfrac12-\tau$ (Definition 7). The two classes are noisy copies of the opposite vertices $\pm\theta^\star$ .

The adversary may move a test point anywhere in the $\ell_\infty$ ball

\mathcal B^\varepsilon_\infty(x)=\{x'\in\mathbb R^d:\|x'-x\|_\infty\le\varepsilon\},

leaving the hypercube. The $\ell_\infty^\varepsilon$ -robust classification error of a classifier $f:\mathbb R^d\to\{\pm1\}$ is (Definition 3)

\beta(f)=\Pr_{(x,y)}\big[\exists x'\in\mathcal B^\varepsilon_\infty(x):\ f(x')\ne y\big].

A linear classifier is $f_w(x)=\operatorname{sgn}\langle w,x\rangle$ for $w\in\mathbb R^d$ . A linear-classifier learning algorithm $g_n$ is any function from $n$ labelled samples to a weight vector $w\in\mathbb R^d$ .

The lower bound is Bayesian: $\theta^\star$ is drawn uniformly from $\{\pm1\}^d$ , the learner receives $n$ independent samples $S$ from the $(\theta^\star,\tau)$ -model, outputs $w=g_n(S)$ , and is charged the robust error of $f_w$ on a fresh sample, averaged over $\theta^\star$ and $S$ . The posterior mean $\mathbb E[\theta^\star_i\mid S]=\Pr[\theta^\star_i=+1\mid S]-\Pr[\theta^\star_i=-1\mid S]$ measures how much the learner can know about coordinate $i$ .

Formalization targets

Goal: Theorem 31 (p. 35)

For $0<\tau\le\tfrac14$ , $0\le\varepsilon<3\tau$ , $0<\gamma<\tfrac12$ and every linear learner $g_n$ : if

n\le\frac{\varepsilon^2\gamma^2}{5000\,\tau^4\log(4d/\gamma)},

then

\mathbb E_{\theta^\star,S}\big[\beta(f_{g_n(S)})\big]\ge\tfrac12-\gamma .

Milestones

Eqs. (4)–(5), p. 33: in one dimension the posterior odds of $\theta$ equal $\prod_k\big(\tfrac{1/2+\tau}{1/2-\tau}\big)^{y_kx_k}$ .
Lemma 29, p. 33: for $\tau\le\tfrac14$ and $n\le1/\tau^2$ , with probability $1-\delta$ ,

\Big|\log\tfrac{\Pr[\theta=+1\mid S]}{\Pr[\theta=-1\mid S]}\Big|\le15\tau\sqrt{2n\log(2/\delta)} .

Proof of Theorem 31, p. 36: with probability $1-\gamma/2$ , $|\mathbb E[\theta^\star_i\mid S]|\le15\tau\sqrt{2n\log(4d/\gamma)}$ for all $i$ .
§4, p. 10: $\sup_{\|\Delta\|_\infty\le\varepsilon}\langle yw,\Delta\rangle=\varepsilon\|w\|_1$ , so $w$ robustly classifies $(x,y)$ iff $\langle yw,x\rangle>\varepsilon\|w\|_1$ .
Proof of Theorem 31, p. 37: when $\theta^\star$ has independent coordinates with means bounded by $b$ in absolute value, a fresh sample satisfies $\langle w,yx\rangle\le\frac{2\tau b}{\gamma}\|w\|_1$ with probability at least $(1-\gamma)/2$ .

The goal keeps the paper's explicit constants ( $5000$ , $3\tau$ , $\log(4d/\gamma)$ ) because Theorem 31 is itself the explicit form of the paper's asymptotic Theorem 9.

Significance

With $\tau\asymp d^{-1/4}$ a single sample already yields a linear classifier with small standard error (Theorem 8 of the paper), while Theorem 31 shows that for $\varepsilon$ of order $\tau$ every linear learner needs on the order of $\sqrt d/\log d$ samples to get expected robust error below $\tfrac12-\gamma$ against an $\ell_\infty$ adversary (the paper's Theorem 9 states this as $n\le c_2\varepsilon^2\gamma^2 d/\log(d/\gamma)$ for $\tau=c_1d^{-1/4}$ ). The companion upper bound (Theorem 10) shows that thresholding the input first makes one sample enough for any $\varepsilon<1$ . Together these give a rigorous example in which robust generalization is polynomially harder than standard generalization for a model class, and in which a change of model class removes the gap.

The theorem and its proof are published and not in doubt. The platform holds no statement of this lower bound, of Lemma 29, or of the ℓ∞/ℓ1 robustness criterion for linear classifiers (searched 2026-09-26). The mission produces a checked statement of the result with every hypothesis explicit, including the tie convention and the domain of $\varepsilon$ that the printed statement leaves implicit, and a finite, measure-free encoding of a Bayesian learning lower bound that other hypercube models can reuse.

Difficulty

The obvious attempt bounds the robust error of the best classifier the learner could output, but the learner is arbitrary: it may output any $w$ , including ones that use the samples in unusual ways. The argument must therefore hold for every function of the samples, which is why $\theta^\star$ is random and why the error is averaged over it; for a fixed $\theta^\star$ the learner $g_n\equiv\theta^\star$ is robust and the statement is false. The technical difficulty is to pass from "the posterior of every coordinate is nearly uniform" (a statement about $d$ separate one-dimensional problems) to a bound on the margin $\langle w,yx\rangle$ relative to $\|w\|_1$ that holds for every $w$ at once, uniformly in how $w$ spreads its weight across coordinates. Concentration of $\langle w,yx\rangle$ is not available for a general $w$ (a single heavy coordinate defeats it), so only a weak, constant-probability tail bound survives, which is why the final error is $\tfrac12-\gamma$ rather than close to $1$ .

Formalization scope

Everything is finite. Hypercube points are sign vectors Fin d → Bool, labels are Bool with true ↦ $+1$ , and every probability is an explicit finite sum of weights; no measure theory is involved. $\mathbb R^d$ is EuclideanSpace ℝ (Fin d). Committed conventions:

The coordinates of $x$ are sampled independently (the reading of "sampling each coordinate" that the paper's proofs use).
$\|\cdot\|_\infty\le\varepsilon$ and $\|w\|_1$ are written coordinatewise; the adversary's ball is the $\ell_\infty$ ball, not the Euclidean one.
$f_w(x)=+1$ when $\langle w,x\rangle=0$ (the paper's $\operatorname{sgn}(0)$ is not in $\{\pm1\}$ ).
The robust error is Definition 3's event $\exists x'\in\mathcal B^\varepsilon_\infty(x),\ f(x')\ne y$ , not the margin criterion; the equivalence is milestone 4.
Added hypotheses: $\varepsilon\ge0$ in the goal (for $\varepsilon<0$ the ball is empty and the printed statement fails at $n=0$ ), and $\delta>0$ in Lemma 29 (at $\delta=0$ Lean's $\log(2/0)=0$ makes it false). Posteriors are defined by Bayes' rule as ratios of joint weights.

The learner is any function of the samples to $\mathbb R^d$ ; restricting to a specific learner, fixing $\theta^\star$ , letting the learner output an arbitrary classifier (for which the theorem is false), or bounding only the standard error ( $\varepsilon=0$ ) would each trivialize or falsify the target and are excluded. Useful infrastructure: Hoeffding's inequality for sums of independent $\pm1$ variables, Markov's inequality over finite sums, and the ℓ∞/ℓ1 duality on EuclideanSpace. Related platform work: the other three missions of this series (the Gaussian lower bound, the Gaussian robust upper bound, and the Bernoulli thresholding upper bound). Contributions of general lemmas on finite product measures over the hypercube are welcome.

Selected references

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

7 thms2 active usersReviewed

Bandit Algorithms Machine Learning Operations Research·Captain: mikedeng1

Online Decision Making with High-Dimensional Covariates: Regret Bound of the LASSO BanditResearch Paper

Motivation

Many sequential decisions are personalised: a physician chooses a drug dose for each arriving patient, a platform chooses which offer to show each arriving user. Each decision is made after observing a vector of covariates describing the individual, and its outcome is observed only for the option chosen. This is the contextual (covariate) bandit problem, studied in operations research and machine learning since Auer (JMLR 2002) and Goldenshluger and Zeevi (Stochastic Systems 2013).

In medical and e-commerce applications the covariate vector is often high-dimensional: the number of covariates $d$ is comparable to or larger than the number of decisions that will ever be made, while the outcome of each option depends on a few of them. Low-dimensional bandit algorithms then incur regret that grows polynomially with $d$ . Bastani and Bayati (Operations Research 2020) proposed the LASSO Bandit, which estimates each option's reward model with the LASSO, and proved a regret bound that grows only logarithmically in $d$ . The paper evaluates the method on warfarin dosing data.

Timeline:

2002–2003: Auer introduces linear-reward contextual bandits with confidence bounds.
2013: Goldenshluger and Zeevi give a forced-sampling algorithm for two arms in low dimension with $O(\log T)$ regret under a margin condition and an arm-optimality condition, and an information-theoretic lower bound of the same order.
2020: Bastani and Bayati extend the forced-sampling scheme to $K$ arms and high-dimensional sparse parameters, with regret $O(s_0^2[\log T+\log d]^2)$ .

Setting

There are $K$ arms with unknown parameters $\beta_1,\dots,\beta_K\in\mathbb R^d$ . At each time $t=1,2,\dots,T$ a covariate vector $X_t\in\mathbb R^d$ arrives; the $X_t$ are i.i.d. with law $\mathcal P_X$ and take values in a fixed set $\mathcal X$ . If arm $i$ is pulled, the reward is $X_t^\top\beta_i+\varepsilon_{i,t}$ , where the noises $\varepsilon_{i,t}$ are independent, $\sigma$ -subgaussian ( $\mathbb E[e^{s\varepsilon}]\le e^{\sigma^2s^2/2}$ for all $s$ ), and independent of the covariates. A policy chooses the arm $\pi_t$ from $X_t$ and the past covariates, arms and observed rewards. Its cumulative expected regret is

R_T=\sum_{t=1}^T\mathbb E\Big[\max_jX_t^\top\beta_j-X_t^\top\beta_{\pi_t}\Big].

The sparsity $s_0$ is the smallest integer $s_0\ge1$ with $\|\beta_i\|_0\le s_0$ for all $i$ .

The four assumptions are: (1) $\|x\|_\infty\le x_{\max}$ on $\mathcal X$ and $\|\beta_i\|_1\le b$ ; (2) a margin condition $\Pr[0<|X^\top(\beta_i-\beta_j)|\le\kappa]\le C_0\kappa$ ; (3) arm optimality: every arm is either suboptimal by a margin $h$ at every covariate, or optimal by margin $h$ on a region $U_i$ of probability at least $p_*$ ; (4) a compatibility condition: the conditional second-moment matrix $\Sigma_i=\mathbb E[XX^\top\mid X\in U_i]$ of each optimal arm lies in the set $\mathcal C(\mathrm{supp}(\beta_i),\phi_0)$ of matrices $M\succeq0$ with $\|v_I\|_1^2\le|I|\,v^\top Mv/\phi_0^2$ whenever $\|v_{I^c}\|_1\le3\|v_I\|_1$ .

The LASSO estimator on $n$ samples is any minimizer of $\|Y-\mathbf X\beta'\|_2^2/n+\lambda\|\beta'\|_1$ . The LASSO Bandit forces arm $i$ at the prescribed times $\mathcal T_i=\{(2^n-1)Kq+j : n\ge0,\ q(i-1)<j\le qi\}$ . At every other time it keeps the arms whose forced-sample estimate $\hat\beta(\mathcal T_{i,t-1},\lambda_1)$ is within $h/2$ of the best. Among them it plays the arm with the largest all-sample estimate $\hat\beta(\mathcal S_{i,t-1},\lambda_{2,t-1})$ , trained on every past pull of the arm, with $\lambda_{2,t}=\lambda_{2,0}\sqrt{(\log t+\log d)/t}$ .

Formalization targets

Goal: Theorem 1 (regret of the LASSO Bandit)

For $q\ge4\lceil q_0\rceil$ , $K\ge2$ , $d>2$ , $T\ge C_5$ , $\lambda_1=\phi_0^2p_*h/(64s_0x_{\max})$ and $\lambda_{2,0}=[\phi_0^2/(2s_0)]\sqrt{1/(p_*C_1)}$ ,

R_T\le C_3(\log T)^2+\big[2Kbx_{\max}(6q+4)+C_3\log d\big]\log T+\big(2bx_{\max}C_5+2Kbx_{\max}+C_4\big),

with the explicit constants $C_1,\dots,C_5$ , $q_0$ of the paper (p. 285).

Milestones

Proposition 1: a LASSO tail inequality for adaptively collected rows with conditionally subgaussian noise.
Lemma 1: a LASSO tail inequality when a constant fraction of the rows is i.i.d. with a compatible second-moment matrix.
Proposition 2: the forced-sample estimator of an optimal arm is within $h/(4x_{\max})$ of $\beta_i$ except with probability $5/t^4$ .
Proposition 3: the all-sample estimator of an optimal arm is within $16\sqrt{(\log t+\log d)/(p_*^3C_1t)}$ of $\beta_i$ except with probability $2/t+2e^{-p_*^2C_2^2t/32}$ .

Significance

The theorem shows that exploiting sparsity makes the regret depend on the ambient dimension only through $\log d$ , while its dependence on the horizon is within one $\log T$ factor of the $\Omega(\log T)$ lower bound known in low dimension. Proposition 1 is a LASSO oracle inequality for adapted designs, where each row may depend on earlier observations. It applies whenever a LASSO is fitted to data gathered by a feedback policy: adaptive experiments, dynamic pricing, sequential treatment assignment.

The results are proved in the paper and its online appendix; none of them has a machine-checked proof. This mission produces a formal model of the covariate bandit with a non-anticipating algorithm, a formal LASSO for adapted designs, and, when complete, a verified regret bound with every constant explicit. Proposition 1 and Lemma 1 are reusable beyond bandits.

Difficulty

The all-sample estimator is trained on the times at which the algorithm chose an arm, and those choices depend on earlier estimates. Its design rows are therefore neither independent nor identically distributed, and the standard LASSO analysis, which starts from i.i.d. rows and a restricted-eigenvalue bound on their population covariance, does not apply. The forced samples are i.i.d. but only $O(\log t)$ in number, too few for the $\sqrt{\log t/t}$ rate the regret bound needs. Controlling the compatibility constant of the adaptively selected sample covariance, and the martingale noise term, is where the naive argument breaks.

Formalization scope

Arms are Fin K (paper arm $i$ is i.val + 1), coordinates Fin d, times are natural numbers from $1$ . The model is a structure IsCovariateNoiseModel on a probability space: i.i.d. measurable covariates in a measurable set $\mathcal X$ , independent subgaussian noises (Mathlib's HasSubgaussianMGF with parameter $\sigma^2$ ), noise independent of covariates. Assumptions 1–4 are separate predicates. $\|x\|_\infty$ is Mathlib's sup norm, logarithms are natural, and $\Sigma_i$ is the uncentred conditional second moment.

The LASSO minimizer and the arg max need not be unique, so the algorithm takes a selection rule and a tie-breaking rule as parameters, and the theorems hold for all of them. Each round reads only the current covariate, the past covariates, the past arms and their observed rewards. The regret theorem and Proposition 3, whose data set $\mathcal S_{i,t}$ is chosen by the algorithm, require both rules to be measurable. Otherwise the trajectory would not be a random variable, and the expectations in $R_T$ could be integrals of non-measurable functions, which Lean evaluates to $0$ and which would make the goal trivially true. For the same reason every assumption constant is required to be positive, and $T\ge C_5$ is imposed on the horizon. Only the explicit inequality of Theorem 1 is stated, not the trailing $O(s_0^2[\log T+\log d]^2)$ or $q_0=O(s_0^2\log d)$ . Proposition 2 is stated for optimal arms (see its note).

A complete development needs matrix concentration for bounded i.i.d. rows, the Azuma–Hoeffding inequality, and the deterministic LASSO basic inequality under a compatibility condition. Contributions of any of these as standalone lemmas are welcome.

Selected references

H. Bastani and M. Bayati, Online Decision Making with High-Dimensional Covariates, Operations Research 68(1):276–294, 2020. https://doi.org/10.1287/opre.2019.1902
A. Goldenshluger and A. Zeevi, A Linear Response Bandit Problem, Stochastic Systems 3(1):230–261, 2013. https://doi.org/10.1287/11-SSY032
P. Auer, Using Confidence Bounds for Exploitation-Exploration Trade-offs, Journal of Machine Learning Research 3:397–422, 2002. https://www.jmlr.org/papers/v3/auer02a.html
P. Bühlmann and S. van de Geer, Statistics for High-Dimensional Data, Springer, 2011. https://doi.org/10.1007/978-3-642-20192-9

9 thms2 active usersReviewed

Operations Research Optimization Probability+1·Captain: mikedeng1

Acceleration of Stochastic Approximation by Averaging: Almost-Sure Convergence and Asymptotic Normality of the Averaged IterateResearch Paper

Motivation

Stochastic approximation finds a root $x^*$ of an unknown map $R:\mathbb R^N\to\mathbb R^N$ from noisy evaluations $y_t=R(x_{t-1})+\xi_t$ , by the Robbins–Monro recursion $x_t=x_{t-1}-\gamma_ty_t$ . It underlies stochastic gradient descent, recursive estimation in statistics, adaptive control and simulation-based optimization. The classical theory (Sacks 1958) shows that the fastest attainable rate, $\sqrt t(x_t-x^*)\Rightarrow N(0,G^{-1}S(G^{-1})^T)$ with $G=R'(x^*)$ and $S$ the noise covariance, is achieved by the matrix step $\gamma_t=t^{-1}G^{-1}$ , which requires knowing $G$ .

Polyak and Juditsky (SIAM J. Control Optim. 30 (1992) 838–855) proved that the same optimal covariance is attained without any knowledge of $G$ : run the recursion with scalar steps that decrease more slowly than $1/t$ and output the running average $\bar x_t$ of the iterates. Ruppert (Cornell ORIE technical report, 1988) obtained the one-dimensional case independently. The method, known as Polyak–Ruppert averaging, is the standard device for variance reduction in stochastic approximation.

Timeline:

1951, Robbins and Monro: the recursion and its convergence in probability.
1958, Sacks: asymptotic normality of $x_t$ for $\gamma_t=\gamma/t$ .
1988, Ruppert: averaging in one dimension, i.i.d.-type noise.
1990–1992, Polyak; Polyak and Juditsky: averaging in $\mathbb R^N$ for linear problems with martingale-difference noise (Theorem 1) and nonlinear problems (Theorem 2).

Setting

Let $(\Omega,\mathcal F,(\mathcal F_t)_{t\ge0},P)$ be a filtered probability space and $(\xi_t)_{t\ge1}$ an adapted $\mathbb R^N$ -valued noise process. Given a nonrandom $x_0\in\mathbb R^N$ and step sizes $\gamma_t>0$ , algorithm (7) is

x_t=x_{t-1}-\gamma_t\bigl(R(x_{t-1})+\xi_t\bigr),\qquad\bar x_t=\frac1t\sum_{i=0}^{t-1}x_i .

The error is $\Delta_t=x_t-x^*$ and the estimation error is $\bar\Delta_t=\bar x_t-x^*$ .

The hypotheses are:

Assumption 3.1: a Lyapunov function $V$ with $V(x)\ge\alpha|x|^2$ , Lipschitz gradient, $V(0)=0$ , $\nabla V(x-x^*)^TR(x)>0$ for $x\neq x^*$ , and $\nabla V(x-x^*)^TR(x)\ge\lambda_1V(x-x^*)$ near $x^*$ .
Assumption 3.2: $|R(x)-G(x-x^*)|\le K_1|x-x^*|^{1+\lambda}$ near $x^*$ , with $0<\lambda\le1$ and every eigenvalue of $G$ having positive real part.
Assumption 3.3: $\xi_t$ is a martingale difference with $E(|\xi_t|^2\mid\mathcal F_{t-1})+|R(x_{t-1})|^2\le K_2(1+|x_{t-1}|^2)$ . It splits as $\xi_t=\xi_t(0)+\zeta_t$ , where $\xi_t(0)$ is a martingale difference whose conditional covariance tends to $S\succ0$ in probability and whose conditional second moments are uniformly integrable, and $E(|\zeta_t|^2\mid\mathcal F_{t-1})\le\delta(x_{t-1}-x^*)$ with $\delta(x)\to0$ as $x\to0$ .
Assumption 3.4: $(\gamma_t-\gamma_{t+1})/\gamma_t=o(\gamma_t)$ , $\sum_t\gamma_t^{(1+\lambda)/2}t^{-1/2}<\infty$ , $\gamma_t\to0$ and $\sum_t\gamma_t^2<\infty$ .

The linear case, algorithm (2), is $R(x)=Ax-b$ with every eigenvalue of $A$ having positive real part.

Formalization targets

Goal: Theorem 2

Under Assumptions 3.1–3.4,

\bar x_t\to x^*\ \text{a.s.},\qquad\sqrt t\,(\bar x_t-x^*)\xrightarrow{D}N\bigl(0,\;G^{-1}S(G^{-1})^T\bigr).

Milestones

Lemma 1, Part 2: under condition (4) on the steps, $t\gamma_t\to\infty$ .
Lemma 1: the matrices $\varphi_j^t=A^{-1}-\gamma_j\sum_{i=j}^{t-1}\prod_{k=j}^{i-1}(I-\gamma_kA)$ are uniformly bounded, and $\frac1t\sum_{j<t}\|\varphi_j^t\|\to0$ .
Lemma 2: the representation (A9) of $\sqrt t\,\bar\Delta_t$ for the linear error recursion.
Theorem 1(a): the linear case, $\sqrt t(\bar x_t-x^*)\Rightarrow N(0,A^{-1}S(A^{-1})^T)$ .
Proof of Theorem 2, Part 1: $V(\Delta_t)$ converges almost surely to a finite limit.
Proof of Theorem 2, p. 850: $x_t\to x^*$ almost surely.
Proof of Theorem 2, Part 4: the average of the linearised process $\Delta^1_t=\Delta^1_{t-1}-\gamma_t(G\Delta^1_{t-1}+\xi_t)$ satisfies $\sqrt t(\bar\Delta^1_t-\bar\Delta_t)\to0$ almost surely.

Significance

Theorem 2 shows that averaging turns a robust, slowly-stepped recursion into an asymptotically efficient estimator. The covariance $G^{-1}S(G^{-1})^T$ is the lower bound for this class of problems: for linear recursive estimates with independent noise it is the bound of [26] in the paper. Downstream, the result is what is invoked for the asymptotic efficiency of averaged stochastic gradient descent (Theorem 3 of the paper) and of recursive M-estimators in regression (Theorem 4).

The result is proved, with a published proof, but has no machine-checked version. As far as a search of the platform shows, no statement of Theorem 1 or Theorem 2 exists on Prove2Me. The platform does have a scalar martingale central limit theorem (Martingale.clt_of_mds, proved, with unconditional Lindeberg condition), which is usable through the Cramér–Wold device. Formalizing Theorem 2 also requires the Robbins–Siegmund almost-supermartingale theorem, a multivariate CLT for martingale differences under conditional Lindeberg and conditional covariance conditions, and the Kronecker lemma. Mathlib has none of these three in the required form, and each is reusable well beyond this mission. Non-asymptotic SGD rates already on the platform (the Bottou–Curtis–Nocedal and Lan missions) are different results.

Difficulty

The obvious approach analyses $x_t$ directly. It fails: with steps decreasing more slowly than $1/t$ , $\sqrt t(x_t-x^*)$ diverges, and only the average has the $\sqrt t$ rate. The average must be compared with the averaged noise through the matrix sums of Lemma 1, whose bounds are uniform in both indices. Those bounds rely on the step condition $(\gamma_t-\gamma_{t+1})/\gamma_t=o(\gamma_t)$ in a quantitative way.

The nonlinear case adds a second difficulty. The iterates are first shown to converge almost surely, by a Lyapunov argument. The nonlinear error is then transferred to a linearised process at the $\sqrt t$ scale, which needs a summability estimate on $|\Delta_i|^{1+\lambda}i^{-1/2}$ obtained through stopping times. A central limit theorem for the linear process alone does not give the result, because the linearisation error must vanish after multiplication by $\sqrt t$ .

Formalization scope

Points are in EuclideanSpace ℝ (Fin N) and matrices are Matrix (Fin N) (Fin N) ℝ, acting through Matrix.toEuclideanLin. Matrix norms are operator norms. Conditional expectations are MeasureTheory.condExp on a Filtration ℕ. "Given $\mathcal F_{t-1}$ " is written with shifted indices ( $\xi_{t+1}$ given $\mathcal F_t$ ). The algorithm is a recursive definition from $(x_0,\gamma,R,\xi)$ , with $\gamma_0,\xi_0$ unused and $\bar x_t$ averaging $x_0,\dots,x_{t-1}$ . Convergence in distribution is TendstoInDistribution to multivariateGaussian 0 V. Convergence of conditional covariances in probability is entrywise TendstoInMeasure. A limsup or supremum "tending to 0 in probability" is unfolded into its $\eta$ – $\delta$ definition.

Corrections of the printed text, each used by the paper's own proof:

Assumption 3.1 prints $V(x^*)=0$ and $\ge\lambda V(x)$ . Stated as $V(0)=0$ and $\ge\lambda_1V(x-x^*)$ (as printed they force $x^*=0$ ). The drift constant is renamed $\lambda_1$ , since the paper uses $\lambda$ also in Assumption 3.2.
Eq. (10) is garbled as printed. It is stated as $\sum\gamma_t^{(1+\lambda)/2}t^{-1/2}<\infty$ , the form of Assumptions 4.7 and 5.6 and of p. 851.
Assumption 3.3's $\delta(x_{t-1})$ is stated as $\delta(x_{t-1}-x^*)$ .
$\gamma_t\to0$ and $\sum\gamma_t^2<\infty$ are added to Assumption 3.4. The proof uses them (p. 849), and they do not follow from it.
$R$ is assumed continuous. The paper states no regularity of $R$ , but its proof of almost sure convergence (pp. 849–850) needs $\nabla V(x-x^*)^TR(x)$ bounded away from $0$ on annuli around $x^*$ , which continuity and Assumption 3.1 provide.
Lemma 1 and Theorem 1(a) are stated under condition (4) only. The constant-step condition (3) is false as printed ( $A=\mathrm{diag}(1,10)$ , $\gamma=1$ ), and Theorem 2 does not use it.
(A3) is stated with the norm inside, as its proof establishes.
(A9) and the linearised process of Part 4 are stated with $-\gamma_t\xi_t$ noise signs, and with $\Delta^1_0=\Delta_0$ . The printed $+$ signs contradict (A8) at $t=2$ .

Several formalizations would make the goal trivial, and all are ruled out:

conditional expectations of non-integrable functions, which are $0$ in Lean (every noise process is required to be in $L^2$ );
a real supremum for the uniform integrability in Assumption 3.3, which is $0$ on unbounded families;
an arbitrary process with a property in place of the recursion (7);
a degenerate Dirac target (the covariance $G^{-1}S(G^{-1})^T$ is positive definite under the hypotheses).

Welcome contributions: the Robbins–Siegmund theorem, a vector martingale CLT under conditional Lindeberg conditions, the Kronecker lemma, and the matrix estimates of Lemma 1.

Selected references

B. T. Polyak, A. B. Juditsky, Acceleration of stochastic approximation by averaging, SIAM J. Control Optim. 30(4), 838–855, 1992. https://doi.org/10.1137/0330046
H. Robbins, S. Monro, A stochastic approximation method, Ann. Math. Statist. 22, 400–407, 1951. https://doi.org/10.1214/aoms/1177729586
J. Sacks, Asymptotic distribution of stochastic approximation procedures, Ann. Math. Statist. 29, 373–405, 1958. https://doi.org/10.1214/aoms/1177706619
D. Ruppert, Efficient estimations from a slowly convergent Robbins–Monro process, Cornell University ORIE Technical Report 781, 1988 (no stable online link located).
H. Robbins, D. Siegmund, A convergence theorem for non negative almost supermartingales and some applications, in Optimizing Methods in Statistics, Academic Press, 233–257, 1971. https://doi.org/10.1016/B978-0-12-604550-5.50015-8

10 thms2 active usersReviewed

Completed

Machine Learning Probability·Captain: mikedeng1

The Optimal Sample Complexity of PAC Learning: The Optimal Realizable Sample Complexity BoundResearch Paper

Motivation

The sample complexity of a learning problem is the number of labelled examples needed to learn to a prescribed accuracy with a prescribed confidence. In Valiant's probably approximately correct (PAC) model it is the basic quantity of statistical learning theory: it says how much data is necessary and sufficient, as a function of the complexity of the hypothesis class, when the target concept belongs to that class (the realizable case).

For a class of Vapnik–Chervonenkis (VC) dimension $d$ the answer was known up to a logarithmic factor for about 25 years:

1982–1989. Vapnik (1982) and Blumer, Ehrenfeucht, Haussler and Warmuth (J. ACM 1989) showed that any learner that outputs a classifier consistent with the sample succeeds with $O\left(\frac1\varepsilon\left(d\log\frac1\varepsilon+\log\frac1\delta\right)\right)$ examples.
1989. Ehrenfeucht, Haussler, Kearns and Valiant (Inform. Comput. 1989) together with Blumer et al. proved the lower bound $\Omega\left(\frac1\varepsilon\left(d+\log\frac1\delta\right)\right)$ for every learner.
1994. Haussler, Littlestone and Warmuth (Inform. Comput. 1994) showed $\mathcal M(\varepsilon,\delta)=O\left(\frac d\varepsilon\mathrm{Log}\frac1\delta\right)$ with a variant of the one-inclusion graph predictor, which is sometimes better but also does not match the lower bound.
2007–2015. The gap was closed for restricted classes, such as intersection-closed classes (Auer and Ortner 2007; Darnstädt 2015), but not for classes such as linear separators.
2015. Simon (COLT 2015) analysed a majority vote of consistent classifiers trained on disjoint parts of the data and reduced the logarithmic factor to a very slowly growing function of $1/\varepsilon$ .
2016. Hanneke (JMLR 17(38), 2016; arXiv:1507.00473) removed the logarithmic factor for every class, with an explicit learner: a majority vote of consistent classifiers trained on recursively constructed, overlapping subsamples.

Setting

Let $\mathcal X$ be a set with a $\sigma$ -algebra and $\mathcal Y=\{-1,+1\}$ . A classifier is a measurable map $h:\mathcal X\to\mathcal Y$ ; the concept space $\mathbb C$ is a set of classifiers with $|\mathbb C|\ge3$ . A finite sequence $x_1,\ldots,x_k$ is shattered by $\mathbb C$ if every labelling $y_1,\ldots,y_k$ is realized by some $h\in\mathbb C$ ; the VC dimension $d$ is the largest such $k$ , assumed finite (then $d\ge1$ ).

A data set is a finite sequence $S$ of pairs in $\mathcal X\times\mathcal Y$ , and $\mathbb C[S]$ is the set of $h\in\mathbb C$ with $h(x)=y$ for all $(x,y)\in S$ . For a probability measure $P$ and a target $f^\star\in\mathbb C$ , the error of $h$ is $\mathrm{er}_P(h;f^\star)=P(\mathrm{ER}(h))$ , where $\mathrm{ER}(h)=\{x:h(x)\ne f^\star(x)\}$ . A learning algorithm maps data sets to classifiers.

For $\varepsilon,\delta\in(0,1)$ , the sample complexity $\mathcal M(\varepsilon,\delta)$ (Definition 1) is the least $m$ such that some algorithm $\mathcal A$ satisfies, for every probability measure $\mathcal P$ on $\mathcal X$ and every $f^\star\in\mathbb C$ , with $X_1,\ldots,X_m$ independent with law $\mathcal P$ ,

\mathbb P\left(\mathrm{er}_{\mathcal P}\left(\mathcal A\big((X_i,f^\star(X_i))_{i\le m}\big);f^\star\right)\le\varepsilon\right)\ge1-\delta,

and $\mathcal M(\varepsilon,\delta)=\infty$ if there is no such $m$ .

The learner of the paper uses three ingredients. A sample-consistent learner $L$ returns an element of $\mathbb C[S]$ whenever that set is nonempty. The majority vote is $\mathrm{Majority}(h_1,\ldots,h_k)(x)=2\mathbb 1\left[\sum_i h_i(x)\ge0\right]-1$ . The subsample algorithm $\mathbb A(S;T)$ returns $\{S\cup T\}$ if $|S|\le3$ ; otherwise it splits $S$ into a head $S_0$ of $|S|-3\lfloor|S|/4\rfloor$ points and three blocks $S_1,S_2,S_3$ of $\lfloor|S|/4\rfloor$ points, and returns the concatenation of $\mathbb A(S_0;S_2\cup S_3\cup T)$ , $\mathbb A(S_0;S_1\cup S_3\cup T)$ and $\mathbb A(S_0;S_1\cup S_2\cup T)$ . The learned classifier is $\hat h=\mathrm{Majority}(L(\mathbb A(S;\emptyset)))$ .

Formalization targets

Goal: Theorem 2 with its explicit constant

\mathcal M(\varepsilon,\delta)\le\frac{1800}{\varepsilon}\left(d+\ln\left(\frac{18}{\delta}\right)\right)\qquad(\varepsilon,\delta\in(0,1)).

The paper states Theorem 2 as $\mathcal M(\varepsilon,\delta)=O\left(\frac1\varepsilon\left(d+\mathrm{Log}\frac1\delta\right)\right)$ with a numerical constant; its proof establishes the bound above with $c=1800$ , and that explicit form is the goal. Improving the constant would give a stronger theorem; this statement stays valid.

Milestones, in attack order

Lemma 4 (Blumer et al. 1989): with probability $1-\delta$ , every $h\in\mathbb C[\{(Z_i,f^\star(Z_i))\}_{i\le m}]$ has $\mathrm{er}_P(h;f^\star)\le\frac2m\left(d\,\mathrm{Log}_2\frac{2em}d+\mathrm{Log}_2\frac2\delta\right)$ .
Lemma 5: $a\ln(c_1(c_2+b/a))\le a\ln(c_1(c_2+e))+b/e$ for $a,b,c_1\ge1$ , $c_2\ge0$ .
Structure of $\mathbb A$ : every subsample $\hat S$ satisfies $T\subseteq\hat S\subseteq S\cup T$ , and the number of subsamples does not depend on $T$ .
The Chernoff event $E_i''$ : if $Q(E)\ge\frac{23}n\ln\frac9\delta$ , then with probability $1-\delta/9$ at least $\frac7{10}Q(E)n$ of $n$ i.i.d. points fall in $E$ .
The bound (8) and its comparison with $\frac{150}{m+1}\left(d+\ln\frac{18}\delta\right)$ .
Majority averaging: $\mathrm{er}(h_{\mathrm{maj}})\le12\,\mathbb E\left[\mathcal P(\mathrm{ER}(h_I)\cap\mathrm{ER}(\tilde h))\right]$ for three equal-size committees.
Claim (9): with probability $1-\delta$ , $\mathrm{er}_{\mathcal P}(\hat h_{m,T};f^\star)\le\frac{1800}{m+1}\left(d+\ln\frac{18}\delta\right)$ .
Sample size (10): $\mathrm{Majority}(L(\mathbb A(\cdot;\emptyset)))$ is $(\varepsilon,\delta)$ -PAC from $\left\lfloor\frac{1800}\varepsilon\left(d+\ln\frac{18}\delta\right)\right\rfloor$ examples.

Significance

Together with the classical lower bound, Theorem 2 gives $\mathcal M(\varepsilon,\delta)=\Theta\left(\frac1\varepsilon\left(d+\log\frac1\delta\right)\right)$ : the realizable PAC sample complexity is determined up to a numerical constant by the VC dimension alone. It settles a question open since 1989, shows that the $\log\frac1\varepsilon$ factor in the classical bounds is an artifact of empirical risk minimization rather than of the learning problem, and supplies an explicit, simple learner that attains the optimal rate. Later work on optimal learners (majority votes over bagged or subsampled ERMs, optimal learning in other settings) builds on this construction.

The result is proved on paper. To our knowledge no proof assistant contains it, and the formal libraries lack parts of its infrastructure: the classical bound for consistent learners (Lemma 4), multiplicative Chernoff bounds for empirical counts, and conditioning on independent parts of an i.i.d. sample. This mission produces a machine-checked statement of the optimal bound with the paper's explicit constant, a verified formal model of the learner, and reusable components for these three.

Difficulty

The obvious approach is to sharpen the analysis of a single consistent classifier, as in the classical bound. Decades of effort along these lines did not remove the $\log\frac1\varepsilon$ factor, and the paper removes it only by aggregating many classifiers. The error of a majority vote is not controlled by the errors of its voters one at a time. The proof controls the probability that two voters trained on overlapping subsamples err at the same point, which requires tracking which parts of the sample are independent of which trained classifiers through a recursion of depth $\log_4 m$ . In a formal development the difficult parts are the conditional-independence bookkeeping for random subsamples of a product measure, the induction over the sample size with a data set $T$ that varies with the level, and the numerical constants, which are tight (the key comparison is $149.9997<150$ ).

Formalization scope

Representation. Labels are Bool (true for $+1$ ); data sets are lists and $\cup$ is concatenation; $\mathbb C$ is a set of measurable functions with $|\mathbb C|\ge3$ ; the VC dimension is a supremum in $\mathbb N\cup\{\infty\}$ , assumed equal to a natural number $d$ . The i.i.d. sample is the product measure $\mathcal P^m$ on $\mathrm{Fin}\,m\to\mathcal X$ . "With probability at least $1-\delta$ " is stated as a bound $\le\delta$ on the outer measure of the failure event. $\mathcal M$ takes values in $\mathbb N\cup\{\infty\}$ , so the goal is stated as $\mathcal M(\varepsilon,\delta)\le\left\lfloor\frac{1800}\varepsilon\left(d+\ln\frac{18}\delta\right)\right\rfloor$ , which is equivalent. Ties in the majority vote go to $+1$ , as printed.
Algorithms. $\mathcal M$ quantifies over deterministic algorithms that output measurable classifiers, chosen before $\mathcal P$ and $f^\star$ and seeing only the labelled sample. The paper also admits randomized algorithms (footnote 2), which can only lower $\mathcal M$ , so the goal implies the paper's statement.
Measurability. The paper assumes that every event in its probability claims is measurable (p. 3). The formalization makes this explicit with two hypotheses: the class is well-behaved (the event of Lemma 4 and the double-sample event of Blumer et al. are null-measurable for every distribution), and the base learner $L$ is jointly measurable in the sample and the point. Both hold for every countable class of measurable classifiers, with $L$ returning the first consistent classifier of an enumeration. Without the first hypothesis Lemma 4 fails for some classes of VC dimension 1.
Ruled out. The following formalizations would make the goal trivial or weaker, and are not used here:
- a sample complexity whose algorithm may depend on $\mathcal P$ or $f^\star$ , which gives $\mathcal M\equiv0$ ;
- a goal with an existential constant or a ceiling in place of $1800$ and the floor;
- measurability hypotheses that no infinite class satisfies;
- milestones 7–8 stated for an arbitrary family of subsamples instead of the algorithm $\mathbb A$ .
Needed infrastructure. VC theory for consistent learners (Lemma 4, via the double-sample argument), multiplicative Chernoff bounds for binomial counts, and conditioning of product measures on coordinate blocks. These are reusable beyond this mission. Contributions welcome: a proof of Lemma 4, the Chernoff milestone, the numerical milestone 5, and the majority-vote averaging step, each of which is independent of the others.

Selected references

S. Hanneke, The Optimal Sample Complexity of PAC Learning, Journal of Machine Learning Research 17(38):1–15, 2016. arXiv:1507.00473v4
A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Learnability and the Vapnik–Chervonenkis dimension, Journal of the ACM 36(4):929–965, 1989. doi:10.1145/76359.76371
A. Ehrenfeucht, D. Haussler, M. Kearns, L. Valiant, A general lower bound on the number of examples needed for learning, Information and Computation 82(3):247–261, 1989. doi:10.1016/0890-5401(89)90002-3
H. U. Simon, An almost optimal PAC algorithm, Proceedings of the 28th Conference on Learning Theory (COLT), PMLR 40:1552–1563, 2015. proceedings.mlr.press/v40/Simon15a
D. Haussler, N. Littlestone, M. K. Warmuth, Predicting {0,1}-functions on randomly drawn points, Information and Computation 115(2):248–292, 1994. doi:10.1006/inco.1994.1097
P. Auer, R. Ortner, A new PAC bound for intersection-closed concept classes, Machine Learning 66(2–3):151–163, 2007. doi:10.1007/s10994-006-8638-3
V. Vapnik, Estimation of Dependences Based on Empirical Data, Springer, 1982.

11 thms2 active usersReviewed

Convex Optimization Machine Learning Probability+1·Captain: mikedeng1

The Power of Convex Relaxation: Near-Optimal Matrix Completion I: Exact Nuclear-Norm Recovery with Quadratic Dependence on the RankResearch Paper

Motivation

Matrix completion asks to recover a low-rank matrix from a small random subset of its entries. It models collaborative filtering (a ratings matrix with most entries missing), sensor-network localization from partial distance matrices, and system identification. The natural estimator, the matrix of least rank that agrees with the observations, is NP-hard to compute in general. Candès and Recht (Found. Comput. Math. 2009) proposed to replace the rank by the nuclear norm (the sum of the singular values), its convex envelope, and proved that this convex program recovers the matrix exactly from $O(n^{6/5} r \log n)$ random entries under incoherence assumptions.

Candès and Tao (IEEE Trans. Inf. Theory 2010) sharpened the sample size to within logarithmic factors of the information-theoretic minimum $n r\log n$ . This mission formalizes their first result, Theorem 1.1, whose proof is a direct moment computation, together with the lemmas on which that proof rests.

Timeline:

2009, Candès–Recht: exact recovery from $m \gtrsim \mu_0 n^{6/5} r \log n$ entries.
2010, Candès–Tao (this paper): $m \gtrsim \mu^4 n r^2 (\log n)^2$ (Theorem 1.1, general-rank form) and $m \gtrsim \mu^2 n r \log^6 n$ (Theorem 1.2), plus a lower bound of order $n r \log n$ for every method (Theorem 1.7).
2011, Gross (IEEE Trans. Inf. Theory) and Recht (JMLR): $m \gtrsim \mu_0 n r \log^2 n$ by the "golfing scheme", with a different proof.

Setting

Let $M \in \mathbb R^{n\times n}$ have rank $r$ and singular value decomposition $M = \sum_{k=1}^r \sigma_k u_k v_k^*$ with $\sigma_k > 0$ and orthonormal $u_k$ , $v_k$ . Write $P_U = \sum_k u_k u_k^*$ , $P_V = \sum_k v_k v_k^*$ and $E = \sum_k u_k v_k^*$ . The matrix obeys the strong incoherence property with parameter $\mu > 0$ if, for all indices $a, a', b, b'$ ,

\Bigl|\langle e_a, P_U e_{a'}\rangle - \tfrac{r}{n}1_{a=a'}\Bigr| \le \mu\tfrac{\sqrt r}{n},\qquad \Bigl|\langle e_b, P_V e_{b'}\rangle - \tfrac{r}{n}1_{b=b'}\Bigr| \le \mu\tfrac{\sqrt r}{n},\qquad |E_{ab}| \le \mu\tfrac{\sqrt r}{n}.

For a set $\Omega \subset [n]\times[n]$ of observed positions, the nuclear-norm program is

\text{minimize } \|X\|_* \quad \text{subject to } X_{ab} = M_{ab}\ \ ((a,b)\in\Omega). \qquad \text{(I.3)}

In the uniform model $\Omega$ is a uniformly random $m$ -subset of $[n]\times[n]$ ; in the Bernoulli model each entry is included independently with probability $p = m/n^2$ .

The proof works with the tangent space $T$ at $M$ and its projection $\mathcal P_T(X) = P_UX + XP_V - P_UXP_V$ , the sampling projection $\mathcal P_\Omega$ , and the centered operators $\mathcal Q_\Omega = p^{-1}\mathcal P_\Omega - \mathcal I$ and $\mathcal Q_T = \mathcal P_T - \rho'\mathcal I$ , where $\rho = r/n$ and $\rho' = 2\rho - \rho^2$ . The candidate certificate $Y$ of (III.10) is the matrix of least Frobenius norm with $\mathcal P_\Omega(Y) = Y$ and $\mathcal P_T(Y) = E$ .

Formalization targets

Goal: Theorem 1.1, general-rank form (I.11)

There is an absolute constant $C$ such that, for every strongly incoherent $M$ of rank $r$ and every $m \le n^2$ ,

m \ge C\mu^4 n r^2(\log n)^2 \implies \Pr_{\text{uniform}}\bigl[M \text{ is the unique solution of (I.3)}\bigr] \ge 1 - n^{-3}.

Milestones

Lemma 3.1: a matrix $Y$ supported on $\Omega$ with $\mathcal P_T(Y) = E$ and $\|\mathcal P_{T^\perp}(Y)\| < 1$ , together with injectivity of $\mathcal P_\Omega$ on $T$ , certifies that $M$ is the unique solution (already proved on the platform).
Lemma 5.1 (exponent bound): $|J|+|K|-|Q|-|\Omega| \le -|Q'|+1$ for every admissible pair.
Lemma 5.2 (pair counting): at most $(Cj(k+1))^{2j(k+1)+q}$ strongly admissible pairs have $|Q'| = q$ .
Theorem 3.4 (moment bound I): with $A = (\mathcal Q_\Omega\mathcal Q_T)^k\mathcal Q_\Omega(E)$ and $r_\mu = \mu^2 r$ ,

\mathbb E\operatorname{trace}(A^*A)^j \le (Cj(k+1))^{2j(k+1)}\, n\,(n r_\mu^2/m)^{j(k+1)}.

Corollary 3.5: under the goal's sampling condition and the Bernoulli model, with probability at least $1-n^{-3}$ , $\mathcal P_\Omega$ is injective on $T$ and $\|\mathcal P_{T^\perp}(Y)\| \le 1/2$ .

The Bernoulli-to-uniform transfer (at most doubling the failure probability) is already on the platform and is included as a supporting item.

Significance

Theorem 1.1 shows that a tractable convex program recovers every strongly incoherent matrix of bounded rank from $O(n(\log n)^2)$ random entries, while Theorem 1.7 of the same paper shows that no method can succeed with fewer than order $n\log n$ . The gap is a single logarithmic factor. The result also requires nothing of the singular values, only of the singular vectors.

The theorem is proved in the literature, and later work improved the rank dependence (Theorem 1.2 of the same paper, and the golfing-scheme results of Gross and Recht). As far as is known, none of these results has a machine-checked proof. The mission produces a formal version of the full moment-method argument. Its combinatorial core, the admissible-pair calculus of Sections IV–V, is a self-contained counting problem for closed paths in a grid and is reusable for other trace-moment bounds of random operators. The Candès–Recht mission on the platform already supplies the deterministic duality step (Lemma 3.1) and the model transfer.

Difficulty

The obvious route bounds the Neumann series $\sum_k \|(\mathcal Q_\Omega\mathcal P_T)^k\mathcal Q_\Omega(E)\|$ term by term with noncommutative Khintchine inequalities and decoupling. That is how the earlier $n^{6/5}$ bound was obtained, and it degrades as $k$ grows because the indicator variables in the higher terms are strongly coupled. The moment method replaces these tools by an exact expansion of $\mathbb E\operatorname{trace}(A^*A)^j$ as a sum over "spider" configurations of paths in $[n]\times[n]$ . The difficulty moves into combinatorics. Configurations have to be grouped by admissible pairs, the exponent of $n$ has to be matched against the powers of $1/p$ (Lemma 5.1), and the configurations have to be counted with enough precision that the sum over $q$ converges (Lemma 5.2). A naive count of pairs gives $(2j(k+1))^{4j(k+1)}$ , which is too large by a square.

Formalization scope

Square case. Theorem 1.1 is printed for $n_1\times n_2$ matrices, but the paper proves only the square case (Section I-H: "we shall work exclusively with square matrices"). Every statement is for Matrix (Fin n) (Fin n) ℝ.
General rank. The goal and Corollary 3.5 are stated in the general-rank form (I.11), $m \ge C\mu^4 n r^2(\log n)^2$ . The paper states this form explicitly on p. 2055, and the proof of Corollary 3.5 derives it as (III.26). For $r = O(1)$ it is the printed Theorem 1.1 and the printed Corollary 3.5.
Constants. Every constant ("numerical constant $C$ ", $c_0$ , and $O(M)^M := (CM)^M$ ) is an existential absolute constant quantified before $n$ , $r$ , $m$ , $M$ , $\mu$ , $j$ , $k$ and $q$ . A constant allowed to depend on $n$ or $M$ would make (I.11) unsatisfiable for large $C$ and the goal vacuous; that formalization is ruled out.
Standing assumptions. The paper assumes $n \ge C'$ and $m \ge 2nr$ (I.22) throughout. In the goal and in Corollary 3.5 they are absorbed by $C$ , since strong incoherence forces $\mu \ge 1$ . Theorem 3.4 carries $2nr \le m$ explicitly. Theorem 3.4 omits $r = O(1)$ and (I.10), since Section V uses only its own proviso $m \ge n r_\mu^2$ . Every statement also carries $m \le n^2$ , without which the uniform model is empty.
Probability. The uniform model is the platform's successProb (a ratio of finite counts). The Bernoulli model uses bernoulliEventProb and bernoulliExpectation with $p = m/n^2$ . The logarithm is natural, and the failure probability is written 1 / n^3.
Recovery. "Unique solution of (I.3)" is IsUniqueMinimizer: every other matrix that agrees with $M$ on $\Omega$ has strictly larger nuclear norm. Stating recovery conditionally on the existence of a certificate would reduce the goal to Lemma 3.1; the goal instead bounds the probability of recovery itself.
Admissible pairs. The index $i \in [j]$ is 0-based, the cyclic successor is finRotate, and the lexicographic order is compared through positions. Pair values are counted in Fin (2j(k+1)+1), which contains every admissible value, so the count is exact and finite.
New definitions. centeredTangentProjection ( $\mathcal Q_T$ ), momentMatrix ( $A$ ), and the admissible-pair calculus. Strong incoherence (A1–A2) is the shared definition CandesTao.Shared.StrongIncoherence, used by this mission and by the companion mission II. The $\mathcal Q_T$ definition is drafted independently in mission II.

Contributions are welcome on any milestone. Lemmas 5.1 and 5.2 are finite combinatorics and need no analysis. Theorem 3.4 additionally needs the expansion (IV.4) of the trace moment and the moment bounds for centered Bernoulli variables of Section IV-C. Corollary 3.5 also uses Theorem 3.2 (Rudelson selection estimate) and Lemma 3.3 (replacing $\mathcal P_T$ by $\mathcal Q_T$ ), which are milestones of the companion mission The Power of Convex Relaxation: Near-Optimal Matrix Completion II.

Selected references

E. J. Candès and T. Tao, The Power of Convex Relaxation: Near-Optimal Matrix Completion, IEEE Trans. Inf. Theory 56(5):2053–2080, 2010. https://doi.org/10.1109/TIT.2010.2044061
E. J. Candès and B. Recht, Exact Matrix Completion via Convex Optimization, Found. Comput. Math. 9(6):717–772, 2009. https://doi.org/10.1007/s10208-009-9045-5
D. Gross, Recovering Low-Rank Matrices From Few Coefficients in Any Basis, IEEE Trans. Inf. Theory 57(3):1548–1566, 2011. https://doi.org/10.1109/TIT.2011.2104999
B. Recht, A Simpler Approach to Matrix Completion, J. Mach. Learn. Res. 12:3413–3430, 2011. https://jmlr.org/papers/v12/recht11a.html

14 thms2 active usersReviewed

Completed

Machine Learning Probability·Captain: naimengye

Understanding Machine Learning XX: Rademacher ComplexitiesTextbook

Motivation

Chapter 4 showed that uniform convergence suffices for learnability; Chapter 26 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), measures its rate. The representativeness of a sample, $\sup_{h \in H}(L_D(h) - L_S(h))$ , is the quantity that controls the excess risk of ERM, and the Rademacher complexity $R(F \circ S) = \frac1m\mathbb{E}_\sigma\sup_{f \in F}\sum_i\sigma_i f(z_i)$ estimates it from the sample itself: the symmetrization argument gives $\mathbb{E}\operatorname{Rep} \le 2\,\mathbb{E}R$ (Lemma 26.2), and McDiarmid's bounded-differences inequality turns expectations into high-probability statements, yielding the generalization bounds of Theorem 26.5, including the data-dependent ones in which the complexity is computed on the training set. A small calculus of Rademacher complexities follows, affine images, convex hulls, Massart's lemma for finite sets and the contraction lemma for Lipschitz compositions, and it is applied to linear classes with $\ell_2$ and $\ell_1$ constraints. The chapter's payoff is dimension-free generalization bounds for linear predictors with Lipschitz losses (Theorem 26.12), for hard-SVM (Theorems 26.13–26.14), and for predictors with low $\ell_1$ norm (Theorem 26.15).

Setting

For a loss class $F = \ell \circ H$ and a sample $S = (z_1, \dots, z_m)$ , $\operatorname{Rep}_D(F, S) = \sup_{f \in F}(L_D(f) - L_S(f))$ (26.1), $F \circ S = \{(f(z_1), \dots, f(z_m)) : f \in F\}$ , and for $A \subseteq \mathbb{R}^m$ , $R(A) = \frac1m\mathbb{E}_\sigma[\sup_{a \in A}\sum_i\sigma_i a_i]$ with $\sigma$ uniform on $\{\pm1\}^m$ (26.5). The linear classes are $H_2 \circ S = \{(\langle w, x_i\rangle)_i : \|w\|_2 \le 1\}$ in a Hilbert space and $H_1 \circ S$ with $\|w\|_1 \le 1$ in $\mathbb{R}^n$ (26.14). Losses of the form $\ell(w, (x, y)) = \varphi(\langle w, x\rangle, y)$ with $a \mapsto \varphi(a, y)$ $\rho$ -Lipschitz (26.18) cover the hinge and absolute losses.

Formalization targets

Goal: Theorem 26.5

Assume $|\ell(h, z)| \le c$ for all $z$ and $h \in H$ . Then, each with probability at least $1 - \delta$ over $S \sim D^m$ :

for all $h \in H$ , $L_D(h) - L_S(h) \le 2\,\mathbb{E}_{S' \sim D^m}R(\ell \circ H \circ S') + c\sqrt{2\ln(2/\delta)/m}$ ;
for all $h \in H$ , $L_D(h) - L_S(h) \le 2R(\ell \circ H \circ S) + 4c\sqrt{2\ln(4/\delta)/m}$ ;
for any $h^\star \in H$ , $L_D(\mathrm{ERM}_H(S)) - L_D(h^\star) \le 2R(\ell \circ H \circ S) + 5c\sqrt{2\ln(8/\delta)/m}$ .

Milestones

Lemma 26.2 (symmetrization); Lemma 26.8 (Massart); Lemma 26.9 (contraction); Theorem 26.12 (linear predictors with $\ell_2$ constraints); Theorem 26.13 (hard-SVM). Further items: Theorem 26.3, Lemma 26.4 (McDiarmid), Lemmas 26.6, 26.7, 26.10, 26.11, Theorem 26.14 and Theorem 26.15.

Significance

Rademacher complexity is the modern language of uniform convergence: it is data-dependent, it is dimension-free for linear classes, and it composes with Lipschitz losses, which is why the SVM bounds of this chapter do not depend on the dimension of $w$ and apply verbatim to kernel methods (Remark 26.2). Theorem 26.5 is the template every such bound follows, symmetrization plus McDiarmid, and the two data-dependent parts are the first bounds in the book that use the training set both to learn and to certify. Massart's lemma and the contraction lemma are the two tools that make the calculus work, the first converting finiteness into a logarithmic dependence, the second removing the loss function from the picture. Theorem 26.13 finally justifies the margin-based sample complexity $R^2\|w^\star\|^2/\epsilon^2$ of hard-SVM, and Theorem 26.14 gives a bound computable from the output alone.

Difficulty

Lemma 26.2 is the symmetrization argument: a ghost sample, the exchange of $z_j$ and $z'_j$ (26.7), the introduction of one Rademacher sign at a time (26.8)–(26.9), and the split of the supremum. Formally it needs Fubini over the product of $2m$ copies of $D$ and the sign average, and the measurability of the suprema, which the statements assume. McDiarmid's inequality is a martingale argument with Hoeffding's lemma at each step; it is the substantial probabilistic input, and Theorem 26.5 combines it with Lemma 26.2, a union bound and Hoeffding's inequality along the decomposition (26.10). Lemma 26.6 is the symmetry $\sigma \mapsto -\sigma$ ; Lemma 26.7 is the fact that a linear functional on the simplex is maximized at a vertex; Massart's lemma is the exponential-moment bound $\mathbb{E}e^{\sigma a} \le e^{a^2/2}$ with Jensen and an optimized scaling; the contraction lemma is Kakade and Tewari's coordinate-by-coordinate argument (26.12)–(26.13), which in a formal proof must be run as an induction over the coordinates. Lemmas 26.10 and 26.11 are Cauchy–Schwarz and Hölder followed by Jensen, respectively Massart on the $2n$ coordinate vectors. Theorem 26.12 chains contraction, Lemma 26.10 and Theorem 26.5 on the almost-sure event $\|x\| \le R$ ; Theorem 26.13 specializes it to the ramp loss with $B = \|w^\star\|$ , where the hard-SVM output has zero empirical ramp loss; Theorem 26.14 is a union bound over the nested classes $\|w\| \le 2^i$ with $\delta_i = \delta/(2i^2)$ ; Theorem 26.15 repeats Theorem 26.12 with Lemma 26.11.

Formalization scope

The Rademacher complexity is a finite average over the $2^m$ sign vectors, so no measure on $\{\pm1\}^m$ is needed, and the supremum over $A$ is the real supremum over the subtype $A$ ; the theorems assume $A$ nonempty and bounded, which every evaluation set of a bounded loss class satisfies. Risks are Mission I's risk and empRisk, samples are Fin m-indexed under iidLaw, and probability statements bound the outer measure of the failure event. Expectations of suprema over uncountable classes are Bochner integrals, so Lemma 26.2, Theorem 26.3 and Theorem 26.5 carry explicit hypotheses that $S \mapsto \operatorname{Rep}_D(F, S)$ and $S \mapsto R(F \circ S)$ are measurable, the book's Remark 3.1 made visible; for the linear classes of §26.3–§26.4 these hold automatically when the Hilbert space is separable (the supremum over the ball is a supremum over a countable dense subset), which is why Theorems 26.12–26.14 assume SecondCountableTopology. McDiarmid's inequality is stated for a measurable function on a product of arbitrary probability measures. Theorem 26.13's error is $P[y\langle w_S, x\rangle \le 0]$ , which dominates $P[y \ne \operatorname{sign}\langle w_S, x\rangle]$ whatever $\operatorname{sign}(0)$ is, and the hard-SVM learner is any map returning a minimum-norm margin-1 separator on separable samples; measurability of the learner is not needed because the bound is uniform over the ball. Theorem 26.14 is given with the constants of its proof, $\sqrt{4(\ln(4\log_2\|w_S\|) + \ln(1/\delta))/m}$ rather than the printed $\sqrt{\ln(4\log_2\|w_S\|/\delta)/m}$ , and for $\|w_S\| \ge 2$ , where $i = \lceil\log_2\|w_S\|\rceil$ satisfies $1 \le i \le 2\log_2\|w_S\|$ as the proof requires; the item text records this. Norms on $\mathbb{R}^n$ as Fin n → ℝ are sup norms (Lemma 26.11, Theorem 26.15), Euclidean norms are written out (Massart), and inner product spaces carry the Euclidean norm.

Not stated: Definition 26.1 (already Mission II's IsRepresentative), the validation heuristic (26.2)–(26.3), Remark 26.1 (the improved rate under separability, no proof), Remark 26.2.

Selected references

S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 26. doi:10.1017/CBO9781107298019
P. L. Bartlett, S. Mendelson, Rademacher and Gaussian complexities: risk bounds and structural results, Journal of Machine Learning Research 3, 2002.
V. Koltchinskii, D. Panchenko, Rademacher processes and bounding the risk of function learning, in High Dimensional Probability II, Birkhäuser, 2000. doi:10.1007/978-1-4612-1358-1_29
C. McDiarmid, On the method of bounded differences, in Surveys in Combinatorics, Cambridge University Press, 1989. doi:10.1017/CBO9781107359949.008
S. M. Kakade, K. Sridharan, A. Tewari, On the complexity of linear prediction: risk bounds, margin bounds, and regularization, NIPS 2008.
S. Boucheron, O. Bousquet, G. Lugosi, Theory of classification: a survey of some recent advances, ESAIM: Probability and Statistics 9, 2005. doi:10.1051/ps:2005018

10 thms2 active usersReviewed

Completed

Machine Learning Probability·Captain: naimengye

Understanding Machine Learning XIV: Nearest NeighborTextbook

Motivation

Every learning paradigm of the book so far, ERM, SRM, MDL, RLM, is defined by a hypothesis class: the learner searches a predefined set of functions. Nearest Neighbor is the first method that is not. It memorizes the training set and labels a new point by the labels of its closest neighbors, on the assumption that the features are relevant to the labels in a way that makes close-by points likely to share a label. Chapter 19 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), makes that assumption precise, a Lipschitz conditional probability, and proves a finite-sample guarantee: the expected error of the 1-NN rule on $m$ examples is at most twice the Bayes error plus $4c\sqrt d\, m^{-1/(d+1)}$ (Theorem 19.3). The classical results of Cover and Hart (1967) and Stone (1977) are asymptotic; the book insists, as it did in §7.4, on a bound that says what a finite sample buys under an explicit prior assumption. The chapter also proves that the exponential dependence on the dimension is not an artifact (Theorem 19.4, the curse of dimensionality) and, in its exercises, extends the analysis to the $k$ -NN rule, whose error converges to $(1 + \sqrt{8/k})$ times the Bayes error (Theorem 19.5).

Setting

The instance domain $X$ carries a metric $\rho$ ; for the analysis $X = [0,1]^d$ with the Euclidean distance and $Y = \{0,1\}$ with the 0–1 loss. For a sample $S = (x_1, y_1), \dots, (x_m, y_m)$ and a point $x$ , let $\pi_1(x), \dots, \pi_m(x)$ reorder the sample by distance to $x$ . The $k$ -NN rule returns the majority label among $y_{\pi_1(x)}, \dots, y_{\pi_k(x)}$ ; the 1-NN rule is $h_S(x) = y_{\pi_1(x)}$ ; in general, for $\varphi : (X \times Y)^k \to Y$ , the $k$ -NN rule with respect to $\varphi$ is $h_S(x) = \varphi\big((x_{\pi_1(x)}, y_{\pi_1(x)}), \dots, (x_{\pi_k(x)}, y_{\pi_k(x)})\big)$ (19.1).

A distribution $D$ over $X \times Y$ has marginal $D_X$ and conditional probability $\eta(x) = P[y = 1 \mid x]$ ; the Bayes optimal rule is $h^\star(x) = \mathbb{1}[\eta(x) > 1/2]$ , and the standing assumption is that $\eta$ is $c$ -Lipschitz: $|\eta(x) - \eta(x')| \le c\|x - x'\|$ . In the formalization a distribution with conditional probability $\eta$ is written condLaw DX η: draw $x \sim D_X$ , then $y \sim \mathrm{Bernoulli}(\eta(x))$ . Every distribution with a regression function is of this form, so nothing is lost.

Formalization targets

Goal: Theorem 19.3

For $X = [0,1]^d$ , $Y = \{0,1\}$ , a distribution $D$ over $X \times Y$ whose conditional probability $\eta$ is $c$ -Lipschitz, and $h_S$ the result of the 1-NN rule on $S \sim D^m$ ,

\mathbb{E}_{S \sim D^m}[L_D(h_S)] \le 2L_D(h^\star) + 4c\sqrt d\, m^{-\frac{1}{d+1}}.

Milestones

Lemma 19.1 (the Lipschitz reduction: $\mathbb{E}_S[L_D(h_S)] \le 2L_D(h^\star) + c\,\mathbb{E}_{S,x}\|x - x_{\pi_1(x)}\|$ ); Lemma 19.2 (the expected mass of the sets among $C_1, \dots, C_r$ missed by an i.i.d. sample of size $m$ is at most $r/(me)$ ); Theorem 19.4 (for integer $c \ge 2$ and every learning rule there is a distribution with $c$ -Lipschitz $\eta$ and Bayes error $0$ on which the rule's expected error is at least $1/4$ whenever $2m \le (c+1)^d$ ); Lemma 19.7 (the majority of $k \ge 10$ independent Bernoulli labels errs, against a label drawn from their mean $p$ , at most $(1 + \sqrt{8/k})$ times as often as $\mathbb{1}[p > 1/2]$ ); Theorem 19.5 (the $k$ -NN bound $\mathbb{E}_S[L_D(h_S)] \le (1 + \sqrt{8/k})L_D(h^\star) + (6c\sqrt d + k)m^{-1/(d+1)}$ ). Lemma 19.6, the $k$ -fold version of Lemma 19.2 with bound $2rk/m$ , is a further item.

Significance

Theorem 19.3 is the book's answer to the question it raised in §7.4: consistency results say that the 1-NN error converges to twice the Bayes error, but not how fast, and the rate necessarily depends on the distribution. The Lipschitz constant $c$ and the dimension $d$ are exactly the prior knowledge the rule relies on, and Theorem 19.4 shows through the No-Free-Lunch theorem that a sample of size exponential in $d$ is genuinely required for some distributions in the class. Theorem 19.5 quantifies what larger $k$ buys, the factor $2$ improving to $1 + \sqrt{8/k}$ , at the price of the additive term growing linearly in $k$ . On the platform, this mission introduces the conditional-probability model of a distribution over $X \times \{0,1\}$ and the Bayes rule, which Chapters 24 (generative models) and the nonparametric parts of the book use again, and the box-cover argument of Lemma 19.2, a small combinatorial-probability tool of independent use.

Difficulty

Lemma 19.1 is a computation once the expectation over $S$ and $(x, y)$ is decomposed as the book does: sample the unlabeled points first, find the nearest neighbor, then draw the two labels; the identity $P[y \ne y'] = 2\eta(x)(1 - \eta(x)) + (\eta(x) - \eta(x'))(2\eta(x) - 1)$ and $L_D(h^\star) = \mathbb{E}_x\min\{\eta, 1 - \eta\} \ge \mathbb{E}_x\,\eta(1 - \eta)$ finish it. Formally the work is in the decomposition itself, which is Fubini for condLaw and the product law, and in the measurability of the rule, which the statement assumes. Lemma 19.2 is $\mathbb{E}[\mathbb{1}[C_i \cap S = \emptyset]] = (1 - P[C_i])^m \le e^{-P[C_i]m}$ and $\max_a ae^{-ma} \le 1/(me)$ . Theorem 19.3 covers the cube by boxes of side $\varepsilon$ , applies Lemma 19.2 to the boxes and sets $\varepsilon = 2m^{-1/(d+1)}$ ; a formal proof must handle $1/\varepsilon$ not being an integer (take $T = \lceil 1/\varepsilon \rceil$ boxes per side, so $r \le (2/\varepsilon)^d$ when $\varepsilon \le 1$ , which is what the book's $2^d\varepsilon^{-d}$ already allows for) and the regime $m < 2^{d+1}$ , where the trivial bound $\mathbb{E}\|x - x_{\pi_1(x)}\| \le \sqrt d$ suffices. Theorem 19.4 is the No-Free-Lunch theorem on the grid of spacing $1/c$ , plus the observation that any $\{0,1\}$ -valued function on the grid extends to a $c$ -Lipschitz $[0,1]$ -valued function on the cube (McShane). Lemma 19.6 is Chernoff's bound below the mean; Lemma 19.7 is the delicate one: Chernoff with the function $h(a) = (1 + a)\log(1 + a) - a$ and the inequality $(1 - 2p)e^{-kp + \frac k2(\log(2p) + 1)} \le \sqrt{8/k}\,p$ for $p \in [0, 1/2]$ , $k \ge 10$ , which the book states without proof. Theorem 19.5 assembles Lemmas 19.6 and 19.7 along the four steps of Exercise 4; to reach the book's constants with an integer number of boxes one takes $T = \lceil m^{1/(d+1)}/2.07 \rceil$ boxes per side and Chernoff at $\delta = 1/3$ in Lemma 19.6, or notes that the bound is trivial unless $m^{1/(d+1)} > 6c\sqrt d + k$ .

Formalization scope

Labels are Bool; bernoulliLaw p is the Bernoulli law on Bool, condLaw DX η the distribution with marginal DX and conditional probability η, and bayesRule η the Bayes rule. The cube is the subtype cube d of EuclideanSpace ℝ (Fin d), so its metric is Euclidean and its Borel structure is inherited; the Lipschitz hypothesis is LipschitzWith c η with c : ℝ≥0, together with η x ∈ [0,1] (a conditional probability). A $k$ -NN rule is a learner h with IsKNNRuleWith k φ h: for every sample of size $m \ge k$ and every $x$ there is some reordering of the sample by distance to $x$ whose first $k$ entries feed $\varphi$ ; ties are therefore broken arbitrarily, and the theorems hold for every choice. Majority votes predict $1$ iff strictly more than half of the $k$ labels are $1$ , the book's $\mathbb{1}[p' > 1/2]$ of Lemma 19.7. The nearest-neighbor distance is nnDist S x = ⨅ i, dist x (S i).1. Expectations over $S \sim D^m$ are Bochner integrals against iidLaw D m (Mission I), and the expectation statements assume the rule is measurable in $(S, x)$ , the book's Remark 3.1; without it the integrals would be junk. Lemmas 19.2 and 19.6 are stated for arbitrary measurable subsets of an arbitrary measurable space, as in the book, with $m \ge 1$ (for $m = 0$ the left side is $\sum_i P[C_i]$ while Lean reads $r/(0 \cdot e)$ as $0$ ). Lemma 19.7 uses the product of Bernoulli laws on Fin k → Bool.

Two statements are given as their proofs support them, and the deviations are recorded in the item texts. Theorem 19.4 takes $c \ge 2$ an integer (the grid has spacing $1/c$ ), fixes $m$ with $2m \le (c+1)^d$ before choosing the distribution (Theorem 5.1 produces a distribution per $m$ ), and concludes that the expected true error is at least $1/4$ (Equation (5.2) in the proof of Theorem 5.1; the book's "greater than $1/4$ " is what its proof gives for $2m < (c+1)^d$ only in the form of that expectation). Theorem 19.5 keeps the book's constants; the drafter checked that they are reachable with an integer number of boxes. Not stated: the general weighted-average rules of §19.1 beyond (19.1), the efficient implementation of §19.3, Exercise 3 (a one-line inequality, absorbed into the proof of Theorem 19.5).

Selected references

S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 19. doi:10.1017/CBO9781107298019
T. Cover, P. Hart, Nearest neighbor pattern classification, IEEE Transactions on Information Theory 13(1), 1967. doi:10.1109/TIT.1967.1053964
C. J. Stone, Consistent nonparametric regression, Annals of Statistics 5(4), 1977. doi:10.1214/aos/1176343886
L. Devroye, L. Györfi, G. Lugosi, A Probabilistic Theory of Pattern Recognition, Springer, 1996. doi:10.1007/978-1-4612-0711-5
L.-A. Gottlieb, A. Kontorovich, R. Krauthgamer, Efficient classification for metric data, COLT 2010; IEEE Transactions on Information Theory 60(9), 2014. doi:10.1109/TIT.2014.2339840

9 thms2 active usersReviewed

Completed

Machine Learning Optimization·Captain: naimengye

Understanding Machine Learning XI: Support Vector Machines and MarginTextbook

Motivation

The sample complexity of learning halfspaces in $\mathbb{R}^d$ grows with $d$ , which is bad news when features are many or infinite. Chapter 15 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) introduces the support vector machine, the learning rule that replaces dimension by geometry. Among the halfspaces separating a sample, Hard-SVM picks the one of largest margin, the distance from the hyperplane to the nearest example (Claim 15.1, Lemma 15.2); if the data are separable with margin $\gamma$ and lie in a ball of radius $\rho$ , the resulting classifier has error $O(\rho/(\gamma\sqrt m))$ whatever the dimension (Theorem 15.4), and the Perceptron of Chapter 9 makes at most $(\rho/\gamma)^2$ updates (Remark 15.1). Soft-SVM drops separability by allowing slack variables, and Claim 15.5 identifies it with regularized hinge-loss minimization, so that the stability theory of Chapter 13 applies: the hinge loss is $\|x\|$ -Lipschitz (Claim 15.6), and Corollary 15.7 gives an expected-risk bound depending only on the norms of the data and of the comparison halfspace. The chapter closes with the optimality conditions that explain the name: the Hard-SVM solution is a combination of the examples on the margin (Theorem 15.8, via the Fritz John conditions, Lemma 15.9).

Setting

Vectors live in $\mathbb{R}^d$ as in Mission VI; labels are real numbers, with $y \in \{\pm 1\}$ as a hypothesis wherever the book needs it. A sample is linearly separable if some halfspace $(w, b)$ has $y_i(\langle w, x_i\rangle + b) > 0$ for all $i$ , and the margin of $(w, b)$ on the sample is $\min_i y_i(\langle w, x_i\rangle + b)$ . Hard-SVM solutions are minimizers of $\|w\|$ subject to $y_i(\langle w, x_i\rangle + b) \ge 1$ , formalized as a relation; the minimizer is unique whenever the constraints are feasible, and the homogenous version sets $b = 0$ . A distribution over $\mathbb{R}^d \times \{\pm 1\}$ is separable with a $(\gamma, \rho)$ -margin if some unit $w^\star$ (and $b^\star$ ) has $y(\langle w^\star, x\rangle + b^\star) \ge \gamma$ and $\|x\| \le \rho$ almost surely. Soft-SVM is the problem $\lambda\|w\|^2 + \frac1m\sum\xi_i$ under $y_i(\langle w, x_i\rangle + b) \ge 1 - \xi_i$ , $\xi_i \ge 0$ ; its homogenous form is the regularized loss minimization rule of Mission IX for the hinge loss $\max\{0, 1 - y\langle w, x\rangle\}$ , and the 0–1 loss is $\mathbb{1}[y\langle w, x\rangle \le 0]$ . Expectations over samples are integrals against $D^m$ , with the measurability conventions of Mission IX.

Formalization targets

Goal: Corollary 15.7, last part

For $D$ on $\{\|x\| \le \rho\} \times \{\pm 1\}$ almost surely, $B > 0$ , and the Soft-SVM learner with $\lambda = \sqrt{2\rho^2/(B^2 m)}$ : $\mathbb{E}_S[L^{0-1}_D(A(S))] \le \mathbb{E}_S[L^{hinge}_D(A(S))]$ , and for every $w$ with $\|w\| \le B$ , $\mathbb{E}_S[L^{hinge}_D(A(S))] \le L^{hinge}_D(w) + \sqrt{8\rho^2 B^2/m}$ .

Milestones

Claim 15.1. The distance from $x$ to $\{v : \langle w, v\rangle + b = 0\}$ with $\|w\| = 1$ is $|\langle w, x\rangle + b|$ .

Lemma 15.2. For a sample with both labels present, the normalized Hard-SVM output has unit norm and margin at least that of every unit-norm halfspace.

Theorem 15.4. Under homogenous $(\gamma, \rho)$ -separability, with probability at least $1 - \delta$ the 0–1 risk of the Hard-SVM output is at most $\sqrt{4(\rho/\gamma)^2/m} + \sqrt{2\log(2/\delta)/m}$ .

Claim 15.5. Every feasible slack vector has average at least the hinge loss, and the hinge losses are feasible slacks.

Claim 15.6. For $y \in \{\pm 1\}$ , $w \mapsto \max\{0, 1 - y\langle w, x\rangle\}$ is $\|x\|$ -Lipschitz.

Corollary 15.7, first parts. For every $u$ , $\mathbb{E}_S[L^{hinge}_D(A(S))]$ and $\mathbb{E}_S[L^{0-1}_D(A(S))]$ are at most $L^{hinge}_D(u) + \lambda\|u\|^2 + 2\rho^2/(\lambda m)$ .

Theorem 15.8. The homogenous Hard-SVM solution is $\sum_{i \in I}\alpha_i x_i$ with $I = \{i : |\langle w_0, x_i\rangle| = 1\}$ .

Lemma 15.9. Fritz John conditions, in the correct form with a multiplier on $\nabla f$ .

Further items: Exercise 15.1 (the two Hard-SVM formulations agree) and Exercise 15.2 (the Perceptron makes at most $(\rho/\gamma)^2$ updates).

Significance

SVM is the bridge between the statistical theory of Part I and the kernel methods of Chapter 16: because the bounds of Theorem 15.4 and Corollary 15.7 involve only $\rho$ , $\gamma$ and $B$ , the same algorithm can be run after an embedding into a huge or infinite-dimensional feature space, and Theorem 15.8, that the solution lies in the span of the examples, is what makes the embedding computable. Corollary 15.7 is also the first place where the abstract machinery of Chapter 13 is applied to a specific learning rule.

Nothing here is machine-checked. One correction is built in: the Fritz John lemma is stated with the multiplier $\alpha_0 \ge 0$ on $\nabla f(w^\star)$ and nonnegative multipliers not all zero, since the printed form, with $\nabla f(w^\star)$ unweighted and $\alpha$ unrestricted, fails already for $f(w) = w$ and $g_1(w) = w^2$ on the line. Theorem 15.8 is unaffected: its constraints are affine, so the multiplier on $\nabla f$ can be taken to be $1$ .

Difficulty

Claim 15.6 and Claim 15.5 are short inequalities and the intended entry points, and Exercise 15.2 is Theorem 9.1 of Mission VI with $B \le 1/\gamma$ and $R \le \rho$ . Claim 15.1 is the book's computation with the foot of the perpendicular $v = x - (\langle w, x\rangle + b)w$ and a Pythagorean inequality for every other point of the hyperplane, packaged as an infimum distance. Lemma 15.2 is the rescaling argument of the book, together with the observation that both labels force $w_0 \ne 0$ ; Exercise 15.1 needs the positivity of the optimal margin on a separable sample. Corollary 15.7 is Corollaries 13.8 and 13.9 of Mission IX for the hinge loss, whose Lipschitz constant is $\|x\|$ only on the support of $D$ , so the stability argument must be run with the almost-sure bound; the 0–1 clause is the pointwise inequality $\ell_{0-1} \le \ell_{hinge}$ . Theorem 15.4 is the content of §26.3: Rademacher complexity of the class of norm-bounded halfspaces, the contraction lemma for the ramp loss, the observation that the Hard-SVM output has zero ramp loss on the sample and norm at most $1/\gamma$ , and a concentration step, all of which will be items of the Rademacher mission. Theorem 15.8 is the KKT theorem for a strictly convex quadratic with affine constraints (Slater's condition holds), and Lemma 15.9 is the general Fritz John theorem for differentiable data, whose proof goes through a separation or penalty argument; neither is in Mathlib.

Formalization scope

Hard-SVM and Soft-SVM are relations and learners, not programs; the margin is a real infimum over the sample; the ramp loss is defined but its bounds belong to Chapter 26. Theorem 15.4 is stated for any learner that returns the Hard-SVM solution whenever the sample is feasible, which is almost surely the case under the margin assumption, and bounds the failure event in outer measure. Corollary 15.7 carries the measurability conventions of Mission IX. The Fritz John lemma is stated correctly rather than as printed. The duality of §15.4, the SGD implementation of §15.5 (whose guarantee needs the trajectory bound of §14.5.3 rather than Theorem 14.11 as stated in Mission X), Exercises 15.3 and 15.4, and Remark 15.2 are not stated.

Trivializing readings are excluded: both labels must be present for the normalized Hard-SVM output, the margin assumption and the support condition are almost sure with respect to $D$ , and the risks are genuine integrals. Welcome contributions: the uniqueness of the Hard-SVM minimizer, the KKT conditions for affine constraints, and the pointwise comparison of the 0–1, ramp and hinge losses.

Selected references

S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 15. doi:10.1017/CBO9781107298019
C. Cortes, V. Vapnik, Support-vector networks, Machine Learning 20(3), 1995. doi:10.1007/BF00994018
B. E. Boser, I. M. Guyon, V. N. Vapnik, A training algorithm for optimal margin classifiers, Proceedings of COLT, 1992. doi:10.1145/130385.130401
F. John, Extremum problems with inequalities as subsidiary conditions, in Studies and Essays Presented to R. Courant, 1948.
N. Cristianini, J. Shawe-Taylor, An Introduction to Support Vector Machines, Cambridge University Press, 2000. doi:10.1017/CBO9780511801389

15 thms2 active usersReviewed

Completed

Machine Learning Optimization Probability·Captain: naimengye

Understanding Machine Learning IX: Convex Learning Problems, Regularization and StabilityTextbook

Motivation

Chapters 12 and 13 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) leave binary classification for the general framework in which a hypothesis is a vector $w \in \mathbb{R}^d$ and the loss $\ell(w, z)$ is a convex function of $w$ . Convexity makes the ERM problem tractable (Lemma 12.11), but Examples 12.8 and 12.9 show that convexity, even with a bounded class, does not by itself make a problem learnable: one-dimensional linear regression with the squared loss defeats every learner. The chapter therefore isolates two families, the convex-Lipschitz-bounded and the convex-smooth-bounded problems (Definitions 12.12 and 12.13), and Chapter 13 proves that both are learnable, not by ERM but by Regularized Loss Minimization with Tikhonov regularization, $A(S) \in \operatorname{argmin}_w L_S(w) + \lambda\|w\|^2$ . The proof goes through a new idea: stability. Theorem 13.2 expresses the expected overfitting $\mathbb{E}[L_D(A(S)) - L_S(A(S))]$ exactly as the expected effect of replacing one training example, strong convexity of the regularized objective bounds that effect (Lemma 13.5, Corollaries 13.6 and 13.7), and balancing the regularization against the fit gives oracle inequalities (Corollaries 13.8 and 13.10) and sample-complexity guarantees (Corollaries 13.9 and 13.11), with ridge regression as the worked example (Theorem 13.1).

Setting

Hypotheses are vectors in $\mathbb{R}^d$ with the Euclidean norm, as in Mission VI; risk, empirical risk, the product law of a sample and agnostic PAC learnability are those of Mission I. A problem is convex when $H$ is convex and every $\ell(\cdot, z)$ is convex; it is convex-Lipschitz-bounded with parameters $\rho, B$ when moreover $\|w\| \le B$ on $H$ and every $\ell(\cdot, z)$ is $\rho$ -Lipschitz on $\mathbb{R}^d$ , and convex-smooth-bounded with parameters $\beta, B$ when every $\ell(\cdot, z)$ is nonnegative and differentiable with a $\beta$ -Lipschitz gradient. Lipschitzness and smoothness are required on all of $\mathbb{R}^d$ because the RLM rule is unconstrained and its outputs need not lie in $H$ . The RLM rule is a relation: $w$ is an output on $S$ if it minimizes $L_S(w) + \lambda\|w\|^2$ over $\mathbb{R}^d$ , and a learner implements the rule if all its outputs are minimizers. For the losses of the chapter the minimizer exists and is unique. Given $S = (z_1, \dots, z_m)$ and a further example $z'$ , $S^{(i)}$ is $S$ with $z_i$ replaced by $z'$ ; a learner is on-average-replace-one-stable with rate $\epsilon(m)$ if $\mathbb{E}_{(S,z') \sim D^{m+1},\, i \sim U(m)}[\ell(A(S^{(i)}), z_i) - \ell(A(S), z_i)] \le \epsilon(m)$ for every distribution. Strong convexity is Mathlib's StrongConvexOn, which is Definition 13.4 verbatim.

Expectations over samples are integrals against product laws. For them to be genuine, the theorems about arbitrary learners assume a jointly measurable loss bounded by a constant and a measurable learner, and the theorems about RLM assume a jointly measurable, nonnegative loss bounded at the origin and a measurable learner; for RLM the latter is automatic, since the minimizer is unique.

Formalization targets

Goal: Corollary 13.9

For a convex-Lipschitz-bounded problem with parameters $\rho, B > 0$ and the RLM learner with $\lambda(m) = \sqrt{2\rho^2/(B^2 m)}$ : for every distribution, every $m \ge 1$ and every $w \in H$ , $\mathbb{E}_S[L_D(A(S))] \le L_D(w) + \rho B\sqrt{8/m}$ ; hence for every $\epsilon > 0$ and $m \ge 8\rho^2B^2/\epsilon^2$ , $\mathbb{E}_S[L_D(A(S))] \le L_D(w) + \epsilon$ .

Milestones

Examples 12.8–12.9. Linear regression on $\mathbb{R}$ with the squared loss is not agnostic PAC learnable, over $H = \mathbb{R}$ or over $H = [-1, 1]$ .

Theorem 13.2. For any measurable learner and $m \ge 1$ , $\mathbb{E}_S[L_D(A(S)) - L_S(A(S))]$ equals the replace-one expectation of (13.6).

Lemma 13.5. $\lambda\|w\|^2$ is $2\lambda$ -strongly convex; a strongly convex function plus a convex one is strongly convex; at a minimizer $u$ of a $\lambda$ -strongly convex $f$ , $f(w) - f(u) \ge \frac\lambda2\|w - u\|^2$ .

Corollary 13.6. For a convex $\rho$ -Lipschitz loss and $\lambda > 0$ , RLM satisfies $\ell(A(S^{(i)}), z_i) - \ell(A(S), z_i) \le 2\rho^2/(\lambda m)$ for every $S, z', i$ , is stable with that rate, and has $\mathbb{E}_S[L_D(A(S)) - L_S(A(S))] \le 2\rho^2/(\lambda m)$ .

Corollary 13.7. For a convex, nonnegative, $\beta$ -smooth loss and $\lambda \ge 2\beta/m$ , the replace-one expectation is at most $(48\beta/(\lambda m))\,\mathbb{E}[L_S(A(S))]$ , and at most $48\beta C/(\lambda m)$ if $\ell(0, z) \le C$ .

Corollary 13.8. $\mathbb{E}_S[L_D(A(S))] \le L_D(w^*) + \lambda\|w^*\|^2 + 2\rho^2/(\lambda m)$ for every $w^*$ .

Corollary 13.10. $\mathbb{E}_S[L_D(A(S))] \le (1 + 48\beta/(\lambda m))\,\mathbb{E}_S[L_S(A(S))] \le (1 + 48\beta/(\lambda m))(L_D(w^*) + \lambda\|w^*\|^2)$ .

Corollary 13.11. A convex-smooth-bounded problem with $\ell(0, z) \le 1$ is learned by RLM with $\lambda = \epsilon/(3B^2)$ once $m \ge 150\beta B^2/\epsilon^2$ .

Theorem 13.1. Ridge regression on the unit ball with labels in $[-1, 1]$ , $\lambda = \epsilon/(3B^2)$ and $m \ge 150 B^2/\epsilon^2$ has $\mathbb{E}_S[L_D(A(S))] \le \min_{\|w\| \le B} L_D(w) + \epsilon$ .

Further items: Lemma 12.11, the hinge loss as a convex surrogate of the 0–1 loss, the stability-implies-no-overfitting remark of §13.2, and the ridge regression system (13.4)–(13.5).

Significance

Stability is the third route to learnability in the book after uniform convergence and nonuniform learnability, and the only one that applies to convex-Lipschitz-bounded problems in general, for which uniform convergence can fail (the book's Exercise 13.2). The chain from strong convexity through replace-one stability to oracle inequalities is the template for the analysis of every regularized learner, and Theorem 13.2 is an exact identity, not a bound. Ridge regression, support vector machines (Chapter 15) and the regularized algorithms of later chapters are all instances.

Nothing here is machine-checked. The sample sizes of Corollary 13.11 and Theorem 13.1 are the book's $150$ . Chaining Corollary 13.10 as printed would need $216$ , but the derivation of Corollary 13.7 actually gives the stability rate $20\beta/(\lambda m)$ , with which $90$ suffices.

Difficulty

Lemma 12.11 and the hinge surrogate are direct. Lemma 13.5 is elementary but part (3) needs the limit $\alpha \to 0$ of the strong-convexity inequality at a minimizer. Examples 12.8–12.9 require constructing the two finitely supported distributions of the book and computing the risk of a fixed output on each; the probability that all $m$ examples are of the second type is at least $0.99$ under both, and the deterministic learner's output on that sample decides which distribution defeats it. Theorem 13.2 is the exchangeability argument of the book: $\mathbb{E}[\ell(A(S), z')] = \mathbb{E}[\ell(A(S^{(i)}), z_i)]$ because swapping $z_i$ and $z'$ preserves the product law; the formal work is the measure-preserving transposition on $Z^{m+1}$ and the integrability of the functions involved. Corollaries 13.6 and 13.7 follow the book's pointwise derivation from (13.7) to (13.11) and (13.12) to (13.14), where the smooth case uses the self-boundedness $\|\nabla\ell\|^2 \le 2\beta\ell$ of nonnegative smooth functions and the inequality $(a + b)^2 \le 3(a^2 + b^2)$ ; passing to expectations then uses Theorem 13.2 and, for the smooth case, the symmetry $\mathbb{E}[\ell(A(S^{(i)}), z')] = \mathbb{E}[\ell(A(S), z_i)]$ . Corollaries 13.8 to 13.11 are the arithmetic of the book once (13.16), $\mathbb{E}[L_S(A(S))] \le L_D(w^*) + \lambda\|w^*\|^2$ , is in hand, with the corrected constant for 13.11. The ridge system is the gradient condition for a strongly convex quadratic, and Theorem 13.1 is Corollary 13.11 applied to $\frac12(\langle w, x\rangle - y)^2$ , which is $\|x\|^2$ -smooth with $\ell(0, z) = y^2/2 \le 1/2$ on the support. In every expectation statement the measurability of $S \mapsto A(S)$ for the RLM rule, which the theorems take as a hypothesis, is provable from uniqueness of the minimizer and is worth a lemma.

Formalization scope

Losses are real-valued functions of a vector and an example; Lipschitz and smoothness conditions are global on $\mathbb{R}^d$ . The RLM rule is a minimizer relation with the regularization parameter as an explicit argument, and Corollary 13.9's learner uses a parameter depending on $m$ . Stability quantifies over $m \ge 1$ and averages over the replaced index. Expectation statements carry measurability hypotheses that make every integral genuine, and the theorems about arbitrary learners assume a bounded loss. The minimum over $H$ is stated as "for every $w \in H$ ", so no minimizer is needed. Definitions 12.1–12.9 and Claims 12.4–12.9 (general convex analysis) are not restated, nor are Examples 12.10–12.11, the discussion of §12.3 beyond the surrogate property, Remark 13.1, and Exercises 12.1–12.4 and 13.1–13.2.

Trivializing readings are excluded: the nonlearnability examples are stated as negations of the framework's learnability, the stability identity is an equality with both sides genuine integrals, and the constants of the oracle inequalities are the book's. Welcome contributions: the transposition invariance of product laws behind Theorem 13.2, the bound $\|A(S)\|^2 \le L_S(0)/\lambda$ for RLM outputs, the measurability of the RLM minimizer, and the self-boundedness inequality (12.6).

Selected references

S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapters 12 and 13. doi:10.1017/CBO9781107298019
O. Bousquet, A. Elisseeff, Stability and generalization, Journal of Machine Learning Research 2, 2002.
S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, stability and uniform convergence, Journal of Machine Learning Research 11, 2010.
A. N. Tikhonov, On the stability of inverse problems, Doklady Akademii Nauk SSSR 39(5), 1943.
S. Boyd, L. Vandenberghe, Convex Optimization, Cambridge University Press, 2004. doi:10.1017/CBO9780511804441

13 thms2 active usersReviewed

Completed

Combinatorics Machine Learning·Captain: naimengye

Understanding Machine Learning VII: Boosting and AdaBoostTextbook

Motivation

Boosting answers a question raised by Kearns and Valiant: can a learner that is only slightly better than random guessing be turned into one that is arbitrarily accurate? Chapter 10 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) defines γ-weak learnability (Definition 10.1), the PAC requirement with the accuracy $\epsilon$ replaced by the fixed value $1/2 - \gamma$ , and presents AdaBoost, the algorithm of Freund and Schapire that, given weak hypotheses, reweights the training set round by round and outputs a weighted majority vote. The chapter's main result (Theorem 10.2) is that the training error of AdaBoost's output decreases as $e^{-2\gamma^2 T}$ in the number of rounds. Since the output is a halfspace over the predictions of $T$ base hypotheses, the chapter then bounds the VC-dimension of that class (Lemma 10.3), so that the number of rounds becomes a knob for the bias–complexity tradeoff. Example 10.1 shows a concrete weak learner, ERM over decision stumps for the class of 3-piece classifiers on the line, and the chapter remarks that, statistically, weak learnability is no easier than strong learnability: a class of infinite VC-dimension is not weakly learnable either.

Setting

The framework is that of Missions I and IV: binary classification over a domain $X$ with the 0–1 loss, distributions $D$ over $X$ with a labeling function $f$ , learners as functions of the sample, the VC-dimension, and ERM. Labels and hypotheses are Boolean, with $\pm 1$ values obtained through $\operatorname{sgn}(\text{true}) = 1$ , $\operatorname{sgn}(\text{false}) = -1$ , and $\operatorname{sign}(z)$ is true exactly when $z > 0$ . A γ-weak learner for $H$ with the function $m_H : (0,1) \to \mathbb{N}$ returns, for every $\delta$ , every $D$ and every measurable $f$ realizable by $H$ , a hypothesis with $L_{(D,f)}(h) \le 1/2 - \gamma$ with probability at least $1 - \delta$ once $m \ge m_H(\delta)$ ; the failure event is bounded in outer measure as in Definition 3.1.

AdaBoost is formalized as a deterministic function of the sample $S = (x_1, y_1), \dots, (x_m, y_m)$ and of the sequence of weak hypotheses $h_0, h_1, \dots$ that the weak learner returned. The distributions are defined by recursion: $D^{(0)}$ is uniform, $\epsilon_t = \sum_i D^{(t)}_i \mathbb{1}[h_t(x_i) \ne y_i]$ , $w_t = \frac12 \log(1/\epsilon_t - 1)$ , and $D^{(t+1)}_i \propto D^{(t)}_i \exp(-w_t y_i h_t(x_i))$ ; the output after $T$ rounds is $x \mapsto \operatorname{sign}(\sum_{t < T} w_t h_t(x))$ . Rounds are indexed from $0$ , so $D^{(0)}$ is the book's $D^{(1)}$ . The class $L(B, T)$ of Equation (10.4) consists of the functions $x \mapsto \operatorname{sign}(\sum_{t=1}^T w_t h_t(x))$ with $h_t \in B$ . Decision stumps over $\mathbb{R}$ are the threshold functions $x \mapsto [\theta < x]$ and their negations $x \mapsto [x \le \theta]$ ; a 3-piece classifier is $b$ outside $[\theta_1, \theta_2]$ and $-b$ inside, with $\theta_1 < \theta_2$ .

Formalization targets

Goal: Theorem 10.2

If $\gamma > 0$ and every round $t < T$ has $0 < \epsilon_t \le 1/2 - \gamma$ , then the empirical 0–1 risk of AdaBoost's output after $T$ rounds is at most $\exp(-2\gamma^2 T)$ .

Milestones

§10.1. A class of infinite VC-dimension is not γ-weak-learnable for any $\gamma > 0$ (domain with measurable singletons, measurable hypotheses).

Example 10.1. There is one sample-size function with which every ERM learner over the decision stumps is a $1/12$ -weak learner for the 3-piece classifiers.

Exercise 10.3. For a nonempty sample and $\epsilon_t \in (0,1)$ , the error of $h_t$ under $D^{(t+1)}$ is exactly $1/2$ .

Lemma 10.3. If $T \ge 3$ and $\mathrm{VCdim}(B) = d \ge 3$ , then $\mathrm{VCdim}(L(B,T)) \le T(d+1)(3\log(T(d+1)) + 2)$ .

Further item: Exercise 10.4 (1), $\mathrm{VCdim}(B) \le \mathrm{VCdim}(L(B,T))$ for $T \ge 1$ .

Significance

Theorem 10.2 is the reason AdaBoost works and the template for every analysis of boosting: a potential function, here $\frac1m \sum_i e^{-y_i f_t(x_i)}$ , bounds the 0–1 training error and contracts by the factor $2\sqrt{\epsilon_{t}(1-\epsilon_{t})} \le \sqrt{1 - 4\gamma^2}$ at every round. Lemma 10.3 supplies the other half of the picture, an estimation-error bound growing only like $T \cdot \mathrm{VCdim}(B)$ up to logarithms, so that Theorem 6.8 turns the pair into a generalization guarantee for boosting. The remark of §10.1 places weak learning in the statistical landscape of Part I: the VC-dimension characterizes it too, and the gain of boosting is computational.

Nothing here is machine-checked. Two points where the book's text needs care are built into the statements. The weight $w_t$ is undefined when $\epsilon_t = 0$ , and the algorithm's normalization then divides $0$ by $0$ ; in Lean the logarithm of a negative number is $0$ , so with $\epsilon_t = 0$ the formal algorithm would ignore a perfect weak hypothesis and the bound could fail. The theorems therefore assume $\epsilon_t > 0$ , which is the case in which the book's formulas are defined. And the book's derivation of "infinite VC-dimension implies not weakly learnable" from the lower bound of Theorem 6.8 at $\epsilon = 1/2 - \gamma$ uses that bound outside the range in which Chapter 28 proves it; the statement itself is true, by the $km$ -point form of the No-Free-Lunch argument (Exercise 5.3 of Mission III) and Lemma B.1.

Difficulty

Exercise 10.4 (1) is a one-line embedding of $B$ into $L(B, T)$ with the weights $(1, 0, \dots, 0)$ and is the entry point. Exercise 10.3 is the computation of the book: after the update, the weight of the mistakes of $h_t$ is $e^{w_t}\epsilon_t$ and the weight of the correct examples is $e^{-w_t}(1 - \epsilon_t)$ , and with $e^{w_t} = \sqrt{(1-\epsilon_t)/\epsilon_t}$ these are equal. Theorem 10.2 needs, by induction on the round, the closed form $D^{(t)}_i = e^{-y_i f_{t}(x_i)}/\sum_j e^{-y_j f_{t}(x_j)}$ of the distribution, the pointwise bound $\mathbb{1}[\operatorname{sign}(f(x)) \ne y] \le e^{-y f(x)}$ for the sign convention used, the telescoping product (10.2), the identity $Z_{t+1}/Z_t = 2\sqrt{\epsilon_t(1-\epsilon_t)}$ , the monotonicity of $a(1-a)$ on $[0, 1/2]$ and $1 - a \le e^{-a}$ . Lemma 10.3 counts dichotomies: Sauer's lemma bounds the restrictions of $B$ to a shattered set by $(em/d)^d$ , choosing $T$ of them gives $(em/d)^{dT}$ , the halfspaces of $\mathbb{R}^T$ contribute $(em/T)^T$ by Theorem 9.2, and the inequality $2^m \le m^{(d+1)T}$ is solved with Lemma A.1; the finite-VC lower bound $m \le d + 1$ handles small $m$ , and the numeric slack of the book's chain must be checked. Example 10.1 combines a geometric observation, that one of the three regions of a 3-piece classifier has mass at most $1/3$ and a stump agrees with the other two, with the agnostic guarantee for ERM over the stumps from Theorem 6.7, applied with accuracy $1/12$ ; the best stump may only approach error $1/3$ because constant functions are not stumps, and the slack absorbs this. The §10.1 remark is the argument sketched above.

Formalization scope

AdaBoost is a function of the sample and of the returned weak hypotheses; the weak learner's randomness and its failure probability (Remark 10.2) are not modelled, and Theorem 10.2 is the deterministic statement the book proves. Rounds are indexed from $0$ . The output uses $\operatorname{sign}(0) =$ negative, consistently with Mission VI. The class $L(B,T)$ is a set of functions, so Lemma 10.3 is a statement about the VC-dimension of Mission IV, with the bound taken in $\mathbb{N} \cup \{\infty\}$ through the integer part of the real right-hand side and the natural logarithm. Decision stumps are closed under negation, as the book's $\operatorname{sign}(x - \theta)\cdot b$ ; constant functions are not stumps. The efficient ERM for decision stumps (§10.1.1), the face-recognition features (§10.4), Exercises 10.1, 10.2, 10.4 (2)–(3) and 10.5 are not stated. The claims of §10.3 that piecewise-constant classifiers with $T$ pieces lie in $L(\text{stumps}, T)$ and that this class shatters $T+1$ points depend on treating $\operatorname{sign}(x - (-\infty))$ as a stump and on the sign convention; with real thresholds, $L(\text{stumps}, 2)$ does not shatter three points under either convention, so these claims are not stated.

Trivializing readings are excluded: the weak-error hypotheses are strict where the book's formulas require it, the VC bounds are in $\mathbb{N} \cup \{\infty\}$ , and the weak-learner guarantee quantifies over all distributions and all realizable labelings. Welcome contributions: the closed form of $D^{(t)}$ , the contraction identity for $Z_{t+1}/Z_t$ , and the dichotomy count behind Lemma 10.3.

Selected references

S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 10. doi:10.1017/CBO9781107298019
Y. Freund, R. E. Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, Journal of Computer and System Sciences 55(1), 1997. doi:10.1006/jcss.1997.1504
R. E. Schapire, The strength of weak learnability, Machine Learning 5(2), 1990. doi:10.1007/BF00116037
M. Kearns, L. Valiant, Cryptographic limitations on learning Boolean formulae and finite automata, Journal of the ACM 41(1), 1994. doi:10.1145/174644.174647
R. E. Schapire, Y. Freund, Boosting: Foundations and Algorithms, MIT Press, 2012.

8 thms2 active usersReviewed

Completed

Machine Learning Optimization·Captain: naimengye

Understanding Machine Learning VI: Linear Predictors, the Perceptron and Least SquaresTextbook

Motivation

Part II of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) turns from the theory of learnability to hypothesis classes that can actually be learned by algorithms, and it starts with the family that almost every practical method is built on: linear predictors. Chapter 9 introduces the affine functions $L_d$ and the three classes obtained by composing them with a link: halfspaces for classification, linear regression for real-valued prediction, and logistic regression in between. For each class it gives an ERM algorithm and the guarantee that goes with it. For halfspaces in the separable case the algorithm is Rosenblatt's Perceptron, and the guarantee is the classical mistake bound (Theorem 9.1): the number of updates is at most $(RB)^2$ , where $R$ bounds the data and $B$ is the norm of the smallest vector separating it with margin one. The chapter then computes the VC-dimension of halfspaces (Theorems 9.2 and 9.3), which by the fundamental theorem of Mission IV makes them learnable, derives the Least Squares normal equations for regression, and observes that the logistic loss is convex, the property later chapters exploit.

Setting

Vectors live in $\mathbb{R}^d$ with its Euclidean inner product and norm. The affine functions are $h_{w,b}(x) = \langle w, x\rangle + b$ , homogenous when $b = 0$ ; a halfspace hypothesis is $x \mapsto \operatorname{sign}(\langle w, x\rangle + b)$ , formalized as a Boolean predictor that is true exactly when $\langle w, x\rangle + b > 0$ (the book leaves $\operatorname{sign}(0)$ unspecified; the VC computations do not depend on the convention). A sample $(x_1, y_1), \dots, (x_m, y_m)$ with labels $y_i \in \{\pm 1\}$ is separable if some $w$ has $y_i\langle w, x_i\rangle > 0$ for all $i$ ; the constants of Theorem 9.1 are $B = \inf\{\|w\| : \forall i,\ y_i\langle w, x_i\rangle \ge 1\}$ and $R = \max_i \|x_i\|$ . The Batch Perceptron starts at $w^{(0)} = 0$ and, while some example has $y_i\langle w^{(t)}, x_i\rangle \le 0$ , adds $y_i x_i$ ; since the algorithm may pick any mistaken example, a run is any sequence of updates obeying this rule, and the theorem is stated for all runs. For regression the loss is $(h(x) - y)^2$ and the Least Squares system is $Aw = b$ with $A = \sum_i x_i x_i^\top$ , written as the linear map $w \mapsto \sum_i \langle x_i, w\rangle x_i$ , and $b = \sum_i y_i x_i$ . The logistic function is $\varphi_{sig}(z) = 1/(1 + e^{-z})$ and the logistic loss is $\log(1 + \exp(-y\langle w, x\rangle))$ . The learning-theoretic notions (ERM, PAC and agnostic PAC learnability, VC-dimension) are those of Missions I and IV.

Formalization targets

Goal: Theorem 9.1 (Perceptron convergence)

For a separable sample with labels in $\{\pm 1\}$ , every run of the Batch Perceptron of $T$ iterations satisfies $T \le (RB)^2$ , and some run of at most $(RB)^2$ iterations ends with $y_i\langle w^{(T)}, x_i\rangle > 0$ for every $i$ .

Milestones

Equation (9.1). A sample is separable if and only if some $w$ satisfies $y_i\langle w, x_i\rangle \ge 1$ for all $i$ .

Theorem 9.2. The VC-dimension of the homogenous halfspaces in $\mathbb{R}^d$ is $d$ .

Theorem 9.3. The VC-dimension of the halfspaces in $\mathbb{R}^d$ is $d+1$ .

Least Squares (9.6). The system $Aw = b$ always has a solution, and $w$ solves it if and only if $h_w$ is an ERM hypothesis for the squared loss over the homogenous linear predictors.

Further items: Exercise 9.3, the tightness of Theorem 9.1 (for every $m$ a sample with $R \le 1$ , $(BR)^2 \le m$ and a run of exactly $m$ updates); the learnability of halfspaces by ERM, a consequence of Theorem 9.3 and the fundamental theorem; Exercise 9.2, $A$ is invertible iff the $x_i$ span $\mathbb{R}^d$ ; and the convexity of the logistic loss in $w$ .

Significance

The Perceptron bound is one of the oldest results of learning theory (Novikoff 1962) and the model for every mistake bound in the online-learning chapters: it is independent of the dimension and of the number of examples, depending only on the geometry of the data through $R$ and $B$ . Theorems 9.2 and 9.3 are the first VC-dimension computations of a class used in practice and give, through Theorem 6.8, the sample complexity $\Theta((d + \log(1/\delta))/\epsilon)$ of learning halfspaces. The normal equations are the algorithmic content of linear regression, and the convexity of the logistic loss is why logistic regression is tractable in the nonseparable case, where ERM for halfspaces with the 0–1 loss is hard.

Nothing here is machine-checked in this form. Mathlib has the inner-product geometry, the Cauchy–Schwarz inequality, linear algebra of finite-dimensional spaces and convexity of compositions, but neither the Perceptron nor the VC-dimension of halfspaces.

Difficulty

Equation (9.1) is a rescaling and the intended entry point. The convexity of the logistic loss is the composition of the convex function $\log(1 + e^{-t})$ with the linear map $w \mapsto y\langle w, x\rangle$ . Exercise 9.2 is the identification of the kernel of $\sum_i \langle x_i, \cdot\rangle x_i$ with the orthogonal complement of the span. The normal equations require showing that a convex quadratic is minimized exactly where its gradient vanishes, and that $b$ lies in the range of $A$ , which is the span of the $x_i$ . Theorem 9.1 is the book's proof: by induction on the run, $\langle w^*, w^{(T)}\rangle \ge T$ and $\|w^{(T)}\|^2 \le TR^2$ for any feasible $w^*$ , then Cauchy–Schwarz, and finally the passage from a feasible $w^*$ to the infimum $B$ ; the existence clause follows because a run can be extended as long as the stopping condition fails and all runs are bounded. Theorem 9.2 is the linear-dependence argument of the book, with a case analysis on the signs of the coefficients and on which side is nonempty, and the shattering of the standard basis; Theorem 9.3 lifts it to $\mathbb{R}^{d+1}$ by appending a constant coordinate. The learnability of halfspaces is Theorem 6.7 applied to a class that must be shown measurable, nonempty, of finite VC-dimension and pointwise separable; the last needs rational approximations $(w_n, b_n)$ in which the offset moves below $b$ more slowly than $w_n$ approaches $w$ , so that boundary points keep their label.

Formalization scope

Halfspaces are Boolean predictors with $\operatorname{sign}(0)$ negative; the classes are sets of functions, so the VC-dimension is that of Mission IV. The Perceptron is a relation on sequences, not a program: this captures the algorithm's freedom to choose any mistaken example and makes the bound apply to all implementations. $B$ is an infimum, which is attained (the feasible set is closed and the norm is coercive), but the theorem does not need attainment. $R$ is a real supremum over the finite index set, equal to $0$ for the empty sample, where every run has length $0$ . The Least Squares statement is about the homogenous class and the sample $i \mapsto (x_i, y_i)$ , with ERM in the sense of Mission I; the bias term is handled by the book's reduction, appending a constant coordinate, and is not formalized separately. The learnability item states qualitative learnability and the ERM guarantee with an unspecified sample-complexity function; the quantitative rate is Theorem 6.8 of Mission IV. Linear programming (§9.1.1), the pseudo-inverse (§9.2.1), polynomial regression (§9.2.2), Exercises 9.1 and 9.4–9.6 are not stated.

Trivializing readings are excluded: labels are constrained to $\pm 1$ , runs must start at $0$ and update only on mistakes, the VC equalities are in $\mathbb{N} \cup \{\infty\}$ , and the ERM equivalence is a biconditional. Welcome contributions: the two Perceptron invariants as separate lemmas, the shattering of the standard basis, and the pointwise separability of halfspaces.

Selected references

S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 9. doi:10.1017/CBO9781107298019
F. Rosenblatt, The perceptron: a probabilistic model for information storage and organization in the brain, Psychological Review 65(6), 1958. doi:10.1037/h0042519
A. B. J. Novikoff, On convergence proofs on perceptrons, Proceedings of the Symposium on the Mathematical Theory of Automata 12, 1962.
S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6, 1954. doi:10.4153/CJM-1954-037-2
S. Ben-David, H. U. Simon, Efficient learning of linear perceptrons, Advances in Neural Information Processing Systems 13, 2001.

8 thms2 active usersReviewed

Completed

Machine Learning Probability·Captain: naimengye

Understanding Machine Learning V: Nonuniform Learnability, Structural Risk Minimization and Minimum Description LengthTextbook

Motivation

The fundamental theorem of Mission IV says that a class of binary classifiers is PAC learnable exactly when its VC-dimension is finite. That leaves out classes one would like to learn, such as all polynomial classifiers over the line, whose VC-dimension is infinite although each degree separately is learnable. Chapter 7 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) relaxes the definition. In nonuniform learnability (Definition 7.1) the sample size may depend on the hypothesis the learner is competing with: the learner must, for every $h \in H$ , eventually do as well as $h$ up to $\epsilon$ , but how soon may depend on $h$ . The chapter's main result (Theorem 7.2) characterizes the nonuniformly learnable classes of binary classifiers as the countable unions of agnostic PAC learnable classes. The learning rule behind it is Structural Risk Minimization (SRM): write $H = \bigcup_n H_n$ , weight the pieces, and minimize the empirical risk plus a confidence term that grows with the index (Theorems 7.3–7.5). Applied to a countable class described by a prefix-free code, SRM becomes the Minimum Description Length rule and yields a quantitative form of Occam's razor (Lemma 7.6, Theorem 7.7). The chapter closes the circle with a No-Free-Lunch result for the relaxed notion (Remark 7.2, Exercise 7.5).

Setting

The framework is that of Missions I, II and IV: examples in a domain $Z$ , a hypothesis type with a class $H$ , a loss $\ell$ , risk $L_D$ and empirical risk $L_S$ , learners as functions of the sample, the uniform convergence property with an explicit rate $m^{UC}_H$ , agnostic PAC learnability, and for binary classification the 0–1 loss, the VC-dimension and pointwise separability. The new module adds Definition 7.1 with an explicit rate $m^{NUL}$ and, as in Definition 3.4, learners whose outputs lie in $H$ ; the same notion for a family of learners indexed by the confidence $\delta$ , since the SRM and MDL rules take $\delta$ as an input; the rate $\epsilon_n(m,\delta) = \inf\{\epsilon \in (0,1) : m^{UC}_{H_n}(\epsilon,\delta) \le m\}$ of Equation (7.1), which is meaningful only when that set is nonempty; the index $n(h) = \min\{n : h \in H_n\}$ of Equation (7.4); the SRM rule as a minimizer of $L_S(h) + \epsilon_{n(h)}(m, w(n(h))\delta)$ over the admissible hypotheses, those whose index has positive weight and a defined rate; prefix-free description languages $d : H \to \{0,1\}^*$ and the MDL rule; and shattering of an infinite set.

Formalization targets

Goal: Theorem 7.2

For a class $H$ of measurable binary classifiers over a domain with measurable singletons, every subclass of which is pointwise separable, $H$ is nonuniformly learnable if and only if there are classes $H_n$ with $\bigcup_n H_n = H$ , each agnostic PAC learnable.

Milestones

Theorem 7.3. If $H = \bigcup_n H_n$ is nonempty and each $H_n$ has the uniform convergence property, then $H$ is nonuniformly learnable (general loss).

Theorem 7.4. For weights $w(n) \in [0,1]$ with partial sums at most $1$ , uniformly convergent pieces $H_n$ with rates $m^{UC}_{H_n}$ , $\delta \in (0,1)$ , any $D$ and any $m$ : with probability at least $1-\delta$ , for every $n$ with $w(n) > 0$ at which $\epsilon_n(m, w(n)\delta)$ is defined and every $h \in H_n$ , $|L_D(h) - L_S(h)| \le \epsilon_n(m, w(n)\delta)$ .

Theorem 7.5. With $w(n) = 6/(\pi^2 n^2)$ and $H_0 = \emptyset$ , every family of learners implementing the SRM rule satisfies the nonuniform guarantee with rate $m^{NUL}(\epsilon,\delta,h) = m^{UC}_{H_{n(h)}}(\epsilon/2,\ 6\delta/(\pi n(h))^2)$ .

Lemma 7.6 (Kraft). For a prefix-free set $S$ of binary strings, every finite subfamily satisfies $\sum_{\sigma} 2^{-|\sigma|} \le 1$ .

Theorem 7.7. For a prefix-free description language on a class with a $[0,1]$ -valued loss, $m \ge 1$ and $\delta > 0$ : with probability at least $1-\delta$ , every $h \in H$ satisfies $L_D(h) \le L_S(h) + \sqrt{(|h| + \ln(2/\delta))/(2m)}$ .

Further items: nonuniform learnability is implied by agnostic PAC learnability (§7.1); a nonuniformly learnable class of binary classifiers is a countable union of classes of finite VC-dimension (Exercise 7.5 (1)–(2)); a class shattering an infinite set admits no countable cover by classes of finite VC-dimension (Exercise 7.5 (3)) and is not nonuniformly learnable; over an infinite domain the class of all measurable classifiers is not nonuniformly learnable (Remark 7.2).

Significance

Theorem 7.2 is the second characterization theorem of the book's Part I and the one that explains why model selection works: any class that can be stratified into learnable pieces is learnable in the nonuniform sense, with the price of not knowing the index paid in sample size rather than in principle. SRM is the abstract form of every penalized learning rule, and the MDL bound of Theorem 7.7 is the cleanest instance, a bound in which the only property of the hypothesis that matters is the length of its description. Remark 7.2 shows the relaxation is not free: even nonuniformly, no learner handles all classifiers over an infinite domain.

Nothing here is machine-checked. The chapter's arguments are short but they combine everything before them: Hoeffding, the union bound with weights, the VC lower bound of Corollary 6.4 and the fundamental theorem. Three places where the book's statements need care are recorded in the formalization: the rate $\epsilon_n$ is an infimum that may be undefined for small $m$ ; the SRM rule takes $\delta$ as an input and so is a family of learners; and the fundamental theorem's uniform-convergence direction needs a measurability condition, which appears in Theorem 7.2 as hereditary pointwise separability.

Difficulty

The relaxation remark is a direct comparison of two definitions. Kraft's inequality is the coin-tossing argument of the book or an induction on the maximal length: it is the intended entry point. Theorem 7.4 is Theorem 7.3's engine: for each index and each $\epsilon$ in the set of Equation (7.1), the uniform convergence property bounds the failure by $w(n)\delta$ ; the passage from "every $\epsilon$ in the set" to the infimum uses continuity of the outer measure along an increasing union; the union over $n$ uses countable subadditivity and the partial-sum condition. Theorem 7.5 is Theorem 7.4 on the good event together with the two inequalities of the book's proof, using that the target is admissible when $m \ge m^{UC}_{H_{n(h)}}(\epsilon/2, w(n(h))\delta)$ and that admissibility of the SRM output gives the bound for it. Theorem 7.3 asks for a single learner: SRM with a confidence schedule $\delta_m \to 0$ chosen so that, for each fixed index, the rate at level $\delta_m$ eventually falls below any $\epsilon$ , together with an approximate minimizer within $1/m$ ; the target hypothesis is admissible for $m$ large. Theorem 7.7 is Theorem 7.4 with singleton pieces and the weights $2^{-|h|}$ , a one-sided Hoeffding bound for each $h$ , and Kraft's inequality. Exercise 7.5 (3) is the combinatorial construction of the book's hint, disjoint finite subsets $K_n$ of the shattered set with $|K_n| > \mathrm{VCdim}(H_n)$ and a labeling that no $H_n$ realizes. The first half of Theorem 7.2 is Corollary 6.4 applied to the nonuniform learner at fixed $\epsilon_0, \delta_0$ , with constants chosen so that the two probability bounds actually contradict; the second half is the fundamental theorem on each piece followed by Theorem 7.3.

Formalization scope

Learners output hypotheses in $H$ , in Definition 7.1 as in Definition 3.4. The rate $\epsilon_n$ is an infimum over the set of Equation (7.1), and every statement that uses it is guarded by the nonemptiness of that set; the weight $w(n)$ may be $0$ , and $H_0 = \emptyset$ encodes the book's indices $1, 2, \dots$ . The SRM rule minimizes over admissible hypotheses, and an SRM family is one that returns an admissible minimizer whenever some hypothesis is admissible, which is the book's assumption that the argmin is attained (automatic for the 0–1 loss). Theorem 7.4's sum condition is on partial sums, and Kraft's inequality is on finite subfamilies, so no divergent series is silently zero. Theorem 7.7 assumes a $[0,1]$ -valued loss and $m \ge 1$ . The binary-classification results assume measurable singletons and measurable hypotheses; Theorem 7.2 also assumes every subclass pointwise separable, which every class over a countable domain satisfies. Definition 7.8 (consistency) and the Memorize algorithm of §7.4 are not stated.

Trivializing readings are excluded: outputs in $H$ keep the risk an honest integral, the rate is never a junk infimum of the empty set, and the failure events are bounded in outer measure. Welcome contributions: a reusable weighted union bound over a countable family of uniform-convergence events, the continuity argument for the infimum rate, and the shattered-set combinatorics of Exercise 7.5.

Selected references

S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 7. doi:10.1017/CBO9781107298019
V. N. Vapnik, The Nature of Statistical Learning Theory, Springer, 1995. doi:10.1007/978-1-4757-2440-0
J. Rissanen, Modeling by shortest data description, Automatica 14(5), 1978. doi:10.1016/0005-1098(78)90005-5
A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Occam's razor, Information Processing Letters 24(6), 1987. doi:10.1016/0020-0190(87)90114-1
L. G. Kraft, A device for quantizing, grouping, and coding amplitude modulated pulses, MSc thesis, MIT, 1949.

12 thms2 active usersReviewed

Completed

Machine Learning Probability·Captain: naimengye

Understanding Machine Learning III: The No-Free-Lunch TheoremTextbook

Motivation

Missions I and II of this series showed that finite hypothesis classes are learnable, with and without the realizability assumption, by empirical risk minimization. Chapter 5 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) asks the converse question: is prior knowledge, in the form of a restricted hypothesis class, really necessary? Could there be a universal learner, an algorithm that, given enough examples from any distribution, outputs a predictor of low risk? The No-Free-Lunch theorem (Theorem 5.1) answers no: for binary classification with the 0–1 loss over a domain $X$ , for every learning algorithm and every training-set size $m$ smaller than $|X|/2$ there is a distribution on which the learner fails with probability at least $1/7$ , even though that distribution is perfectly predictable by some function $f$ , so that another learner (ERM over $\{f\}$ ) succeeds. The consequence for the framework is Corollary 5.2: over an infinite domain, the class of all functions is not PAC learnable. This is the first lower bound of the book and the reason the rest of it is about the complexity of hypothesis classes rather than about universal algorithms.

Setting

The framework is the UnderstandingML_Framework module of Mission I, cited as a reference. Binary classification over a domain $X$ uses examples in $X \times \{0,1\}$ , hypotheses $h : X \to \{0,1\}$ and the 0–1 loss, so the risk of $h$ under a distribution $D$ over $X \times \{0,1\}$ is $L_D(h) = D(\{(x,y) : h(x) \ne y\})$ , computed as the integral of the 0–1 loss. A learner is a function from samples of each size to hypotheses, and a sample of size $m$ has the law $D^m$ . PAC learnability of a class $H$ (Definition 3.1) requires a sample-complexity function $m_H$ and a learner $A$ such that for every $\epsilon, \delta \in (0,1)$ , every distribution $D$ over $X$ and every measurable labeling function $f$ realizable by $H$ , samples of size $m \ge m_H(\epsilon,\delta)$ yield $L_{(D,f)}(A(S)) \le \epsilon$ with probability at least $1-\delta$ .

Two conventions specific to this mission. The domain $X$ is assumed to have measurable singletons (the book's Remark 3.1 assumes away measurability issues); this makes the finitely supported distributions of the proof honest probability measures and makes every $L_D(h)$ under them a genuine integral. And " $m$ smaller than $|X|/2$ " is written $2m < |X|$ in the extended natural numbers, so that an infinite domain satisfies it for every $m$ .

Formalization targets

Goal: Theorem 5.1 (No-Free-Lunch)

Let $A$ be any learning algorithm for binary classification with respect to the 0–1 loss over a domain $X$ with measurable singletons, and let $m$ be a training-set size with $2m < |X|$ . Then there exists a probability distribution $D$ over $X \times \{0,1\}$ such that

there is a measurable $f : X \to \{0,1\}$ with $L_D(f) = 0$ ;
there is a measurable set $E$ of samples of size $m$ with $D^m(E) \ge 1/7$ on which $L_D(A(S)) \ge 1/8$ .

Milestones

Lemma B.1 (Appendix B). If $Z$ takes values in $[0,1]$ and $E[Z] = \mu$ , then for every $a \in (0,1)$ , $P[Z > 1-a] \ge (\mu - (1-a))/a$ , and consequently $P[Z > a] \ge (\mu - a)/(1-a) \ge \mu - a$ .

Equation (5.2). Under the hypotheses of Theorem 5.1 there are $D$ and a measurable $f$ with $L_D(f) = 0$ and $\mathbb{E}_{S \sim D^m}[L_D(A(S))] \ge 1/4$ .

Corollary 5.2. For an infinite domain $X$ with measurable singletons, the class of all functions $X \to \{0,1\}$ is not PAC learnable.

Two further items: Exercise 5.1, the passage from an expectation of at least $1/4$ to a probability of at least $1/7$ of exceeding $1/8$ for a $[0,1]$ -valued variable; and Exercise 5.3, the $k$ -fold version of Equation (5.2), with bound $1/2 - 1/(2k)$ when $km \le |X|$ , $k \ge 2$ and $X$ is nonempty.

Significance

The No-Free-Lunch theorem is the book's first impossibility result and the conceptual pivot of Part I: it shows that learnability is a property of the pair (hypothesis class, learner) and not of the learner alone, and it motivates the bias–complexity tradeoff of §5.2 and the VC-dimension of Chapter 6, whose lower bound (Theorem 6.7, the "only if" direction of the fundamental theorem) is proved by the same symmetrization argument. Corollary 5.2 is the statement that the class of all functions has infinite sample complexity, the negative half of the characterization of learnable classes.

Nothing here is machine-checked. The proof is combinatorial and elementary but has real content for a formalization: a finite subset $C$ of the domain, the $2^{2m}$ labelings of $C$ , the uniform distribution on $C$ labeled by each of them, an exchange of a maximum, an average and a minimum over labelings and sample sequences, and a pairing argument on labelings that differ at exactly one unseen point. Lemma B.1 is a reverse Markov inequality for bounded variables that later chapters also use.

Difficulty

Lemma B.1 is Markov's inequality applied to $1 - Z$ and is the entry point; Exercise 5.1 is its instance with $a = 1/8$ and $\mu \ge 1/4$ , giving $(1/4 - 1/8)/(7/8) = 1/7$ , together with the inclusion of $\{\theta > 1/8\}$ in $\{\theta \ge 1/8\}$ . Theorem 5.1 follows from Equation (5.2) and Exercise 5.1 once one knows that $S \mapsto L_D(A(S))$ is, under the finitely supported $D^m$ , almost everywhere equal to a measurable function with values in $[0,1]$ ; the set $E$ is the intersection of the event with the finite support of $D^m$ , which is measurable because singletons are. Equation (5.2) is the heart of the mission. One picks $C \subseteq X$ of size $2m$ (available because $2m < |X|$ ), lets $D_i$ be uniform on $C$ labeled by the $i$ -th function $f_i : C \to \{0,1\}$ extended by $0$ off $C$ , and computes $\mathbb{E}_{S \sim D_i^m}[L_{D_i}(A(S))]$ as an average over the $(2m)^m$ sequences of instances, which requires identifying $D_i^m$ as a finitely supported measure on sequences, that is, the product of finitely supported measures. The inequalities (5.4)–(5.6) exchange max, average and min and restrict to the unseen points, and the pairing argument shows that for each unseen point the average over $i$ of the indicator that $A$ errs on it is exactly $1/2$ . Exercise 5.3 is the same argument with $|C| = km$ , where at least $(k-1)m$ points are unseen. Corollary 5.2 takes $\epsilon < 1/8$ , $\delta < 1/7$ , $m = m_H(\epsilon,\delta)$ and a set $C$ of size $2m$ in the infinite domain, and derives the contradiction from Theorem 5.1 via the identification of $L_D$ for $D$ uniform on $C$ labeled by $f$ with the true error $L_{(D_X, f)}$ of Definition 3.1, where $D_X$ is uniform on $C$ ; the case $m = 0$ is handled separately with a single point.

Formalization scope

The items are stated in the joint-distribution form of the book's Chapter 5, with $D$ over $X \times \{0,1\}$ and $L_D$ the risk under the 0–1 loss, rather than in the $(D, f)$ form of Definition 3.1; Corollary 5.2 is the bridge and is stated with the framework's PACLearnable. Witness labeling functions are required to be measurable, because a non-measurable $f$ would make $L_D(f) = 0$ true by Lean's convention for non-integrable functions rather than by content. Clause (2) of Theorem 5.1 is stated in the inner form (a measurable set of probability at least $1/7$ inside the event) rather than as a lower bound on the outer measure of the event, which for a non-measurable event would be the weaker statement. The size condition uses ENat.card, so infinite domains satisfy it. Learners are deterministic functions of the sample; the book's argument goes through for randomized learners by averaging, but the framework does not model them.

Trivializing readings are excluded: the distribution must be a probability measure, the failing set must be measurable with an honest lower bound, and the witness $f$ must be measurable. Welcome contributions: the finitely supported product law on sequences, the averaging identity (5.3), and the pairing argument on labelings of $C$ .

Selected references

S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 5 and Appendix B. doi:10.1017/CBO9781107298019
D. H. Wolpert, W. G. Macready, No free lunch theorems for optimization, IEEE Transactions on Evolutionary Computation 1(1), 1997. doi:10.1109/4235.585893
A. Ehrenfeucht, D. Haussler, M. Kearns, L. Valiant, A general lower bound on the number of examples needed for learning, Information and Computation 82(3), 1989. doi:10.1016/0890-5401(89)90002-3
V. N. Vapnik, Statistical Learning Theory, Wiley, 1998.

5 thms2 active usersReviewed

Completed

Machine Learning Probability·Captain: naimengye

Understanding Machine Learning II: Learning via Uniform ConvergenceTextbook

Motivation

Mission I of this series set up the statistical learning framework of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) and proved, in the book's Chapters 2 and 3, that finite classes are PAC learnable under the realizability assumption. Chapter 4 removes that assumption. Its idea is the one that organizes the rest of the theory: if the empirical risks $L_S(h)$ of all hypotheses in $H$ are simultaneously close to their true risks $L_D(h)$ , then minimizing $L_S$ over $H$ is nearly as good as minimizing $L_D$ over $H$ , whatever the distribution $D$ is. A sample with that property is called $\epsilon$ -representative (Definition 4.1), and a class for which representative samples are guaranteed at some sample size is said to have the uniform convergence property (Definition 4.3). Lemma 4.2 turns representativeness into a guarantee for ERM, Corollary 4.4 turns uniform convergence into agnostic PAC learnability, Hoeffding's inequality (Lemma 4.5) gives uniform convergence for a single hypothesis, and a union bound gives it for a finite class: Corollary 4.6, the capstone, says every finite class with a loss in $[0,1]$ is agnostic PAC learnable by ERM with sample complexity $\lceil 2\log(2|H|/\delta)/\epsilon^2 \rceil$ .

Setting

The framework is the UnderstandingML_Framework module of Mission I, cited here as a reference. A domain $Z$ is a measurable space, hypotheses form a type with a class $H$ , and a loss $\ell : H \times Z \to \mathbb{R}$ is given. The risk is $L_D(h) = \mathbb{E}_{z \sim D}\,\ell(h,z)$ , the empirical risk on $S = (z_1,\dots,z_m)$ is $L_S(h) = \frac1m \sum_i \ell(h, z_i)$ , and a sample of size $m$ has the product law $D^m$ . A hypothesis is an ERM hypothesis for $S$ if it lies in $H$ and minimizes $L_S$ over $H$ ; a learner is a function from samples of each size to hypotheses, and an ERM learner returns an ERM hypothesis on every sample.

$S$ is $\epsilon$ -representative with respect to $H$ , $\ell$ and $D$ if $|L_S(h) - L_D(h)| \le \epsilon$ for every $h \in H$ . $H$ has the uniform convergence property with the function $m^{UC}_H$ if for every $\epsilon, \delta \in (0,1)$ and every distribution $D$ over $Z$ , a sample of $m \ge m^{UC}_H(\epsilon, \delta)$ i.i.d. examples is $\epsilon$ -representative with probability at least $1 - \delta$ . $H$ is agnostic PAC learnable with the function $m_H$ and the learner $A$ if $A$ returns hypotheses in $H$ and, for every $\epsilon, \delta \in (0,1)$ , every $D$ and every $m \ge m_H(\epsilon,\delta)$ , $L_D(A(S)) \le \min_{h' \in H} L_D(h') + \epsilon$ with probability at least $1 - \delta$ over $S \sim D^m$ . As in Mission I, "with probability at least $1-\delta$ " is an upper bound $\delta$ on the outer measure of the failure event, " $\min_{h' \in H} L_D(h') + \epsilon < L_D(h)$ " is written as " $\exists h' \in H$ , $L_D(h') + \epsilon < L_D(h)$ ", and sample-complexity functions are carried explicitly rather than as minimal functions.

Formalization targets

Goal: Corollary 4.6

Let $H$ be a finite hypothesis class, $Z$ a domain and $\ell : H \times Z \to [0,1]$ a loss function whose sections $\ell(h,\cdot)$ are measurable. Then

$H$ has the uniform convergence property with the function $m^{UC}_H(\epsilon,\delta) = \lceil \log(2|H|/\delta)/(2\epsilon^2) \rceil$ ;
every ERM learner for $H$ is an agnostic PAC learner with the function $m_H(\epsilon,\delta) = \lceil 2\log(2|H|/\delta)/\epsilon^2 \rceil$ , which is $m^{UC}_H(\epsilon/2,\delta)$ ;
if $H$ is nonempty, $H$ is agnostic PAC learnable.

Milestones

Lemma 4.2. If $S$ is $\epsilon/2$ -representative and $h_S$ is an ERM hypothesis for $S$ , then $L_D(h_S) \le L_D(h) + \epsilon$ for every $h \in H$ .

Corollary 4.4. If $H$ has the uniform convergence property with $m^{UC}_H$ , then every ERM learner for $H$ is an agnostic PAC learner with the function $(\epsilon,\delta) \mapsto m^{UC}_H(\epsilon/2, \delta)$ , and $H$ is agnostic PAC learnable as soon as an ERM learner exists.

Lemma 4.5 (Hoeffding's inequality). For a probability measure $D$ , a measurable $\theta$ with $a \le \theta \le b$ almost surely and mean $\mu = \int \theta\,dD$ , and $\epsilon > 0$ ,

D^m\Big[\Big|\tfrac1m \textstyle\sum_{i=1}^m \theta(\omega_i) - \mu\Big| > \epsilon\Big] \le 2\exp\!\big(-2m\epsilon^2/(b-a)^2\big).

Significance

Chapter 4 is where the book's account of learnability becomes distribution-free in the agnostic sense: nothing is assumed about $D$ beyond being a probability distribution, and the guarantee is relative to the best hypothesis in the class. Lemma 4.2 and Corollary 4.4 are the reduction that every later generalization bound in the book (VC dimension, Rademacher complexity, covering numbers, compression) plugs into: prove uniform convergence, get ERM learnability. Corollary 4.6 is the first instance, and its $\log|H|/\epsilon^2$ dependence, against the $\log|H|/\epsilon$ of the realizable case, is the standard illustration of the price of agnosticism. Hoeffding's inequality is stated in the form the book uses everywhere afterward, for the product law of one distribution, with an almost-sure range bound and the mean written as an integral.

Nothing here is machine-checked. Mathlib has no Hoeffding inequality for sums of i.i.d. bounded variables on a product measure in this form, so Lemma 4.5 is a genuine contribution; its proof in the book's Appendix B goes through Hoeffding's lemma on the moment generating function of a bounded centered variable and the Chernoff bounding method, both of which will be needed by the concentration results of later missions.

Difficulty

Lemma 4.2 is three inequalities on real numbers and is the intended entry point. Corollary 4.4 is Lemma 4.2 applied on the complement of the failure event of uniform convergence at $\epsilon/2$ : the failure set of the learner is contained in the failure set of representativeness, and outer measure is monotone. Hoeffding's inequality is the substantial item: one needs the moment generating function bound $\mathbb{E}\,e^{\lambda(\theta-\mu)} \le e^{\lambda^2(b-a)^2/8}$ (Lemma B.7 of the book, by convexity of the exponential on $[a,b]$ ), independence of the coordinates under Measure.pi to factor the expectation of the product, Markov's inequality, and the optimization over $\lambda$ ; the two tails are treated separately and added. The degenerate cases are genuine: for $m = 0$ the bound is $2$ and the claim holds trivially, and for $a = b$ Lean's convention $x/0 = 0$ makes the bound $2$ again. Corollary 4.6 combines Hoeffding for each $h \in H$ with a union bound over the finite class and an arithmetic step showing that $m \ge \log(2|H|/\delta)/(2\epsilon^2)$ gives $2|H|e^{-2m\epsilon^2} \le \delta$ ; the empty class makes the uniform convergence clause vacuous. The second and third clauses of the goal then follow from Corollary 4.4, the third by exhibiting an ERM learner, which exists for a nonempty finite class by choosing a minimizer of $L_S$ .

Formalization scope

The four items live in the general loss framework, not the binary-classification special case, because the chapter is stated for an arbitrary loss; Mission I's IsRepresentative and HasUniformConvergenceWith already carry the chapter's definitions, so no new definition module is introduced. Losses in Corollary 4.6 are real-valued with the range condition $\ell(h,z) \in [0,1]$ for every $z$ and measurability of $\ell(h,\cdot)$ for $h \in H$ , which is what the book's " $\ell : H \times Z \to [0,1]$ " and Remark 3.1 give. The book's " $m_H(\epsilon,\delta) \le \cdots$ " is stated as "the guarantee holds with the function $\lceil \cdots \rceil$ ", the same convention as Mission I. In Corollary 4.4 the ERM clause is universal over ERM learners, matching "the ERM paradigm is a successful agnostic PAC learner" for every choice of minimizer; the existence of an ERM learner is a separate hypothesis for the learnability clause because a class with no minimizers on some sample has no ERM rule. Hoeffding's inequality is on i.i.d. coordinates of Measure.pi; the book's " $E[\theta_i] = \mu$ " is the definition of $\mu$ rather than an assumption.

Trivializing readings are excluded: the failure events are bounded in outer measure, so measurability of the events is not a loophole; representativeness is required for every $h \in H$ ; the sample-complexity functions are the book's, with ceilings. Welcome contributions: Hoeffding's lemma on bounded centered variables, the factorization of the moment generating function under Measure.pi, and a reusable union bound over a finite class.

Selected references

S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 4 and Appendix B. doi:10.1017/CBO9781107298019
W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58(301), 1963. doi:10.1080/01621459.1963.10500830
V. N. Vapnik, A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and its Applications 16(2), 1971. doi:10.1137/1116025
S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013, Chapter 2. doi:10.1093/acprof:oso/9780199535255.001.0001

5 thms2 active usersReviewed

Completed

Machine Learning Probability·Captain: naimengye

Understanding Machine Learning I: The Statistical Learning Framework, ERM and Finite ClassesTextbook

Motivation

Chapters 2 and 3 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (Cambridge University Press, 2014, doi:10.1017/CBO9781107298019), set up the framework in which the whole book asks what learning is. A learner sees a sample drawn independently from an unknown distribution over examples, chooses a hypothesis from a class fixed in advance, and is judged by its risk, the expected loss on a fresh example. The natural rule is Empirical Risk Minimization: pick a hypothesis that does best on the sample. Chapter 2 shows that ERM over an unrestricted class overfits, that restricting the class is what makes learning possible, and that a finite class never overfits once the sample is larger than $\log(|H|/\delta)/\epsilon$ (Corollary 2.3). Chapter 3 turns this into a definition, Probably Approximately Correct learnability with its sample-complexity function $m_H(\epsilon, \delta)$ , restates the finite-class result as Corollary 3.2, and then generalizes in two directions that the rest of the book lives in: the agnostic model, in which no hypothesis need be perfect and the learner competes with the best hypothesis in the class, and general loss functions, which cover regression, multiclass prediction and unsupervised tasks. Chapter 4 adds the notion of an ε-representative sample and of uniform convergence, the tool by which the finite-class result extends to the agnostic case; its definitions are included here since they complete the framework.

Setting

A domain $Z$ of examples, a class $H$ of hypotheses and a loss $\ell : H \times Z \to \mathbb{R}$ . The risk of $h$ under a distribution $D$ is $L_D(h) = \mathbb{E}_{z \sim D}\,\ell(h, z)$ and its empirical risk on $S = (z_1, \dots, z_m)$ is $L_S(h) = \frac1m\sum_i \ell(h, z_i)$ ; a sample is drawn i.i.d., $S \sim D^m$ ; an ERM hypothesis minimizes $L_S$ over $H$ ; a learning algorithm maps samples of each size to hypotheses. In binary classification the examples are $(x, f(x))$ with $x \sim D$ over $X$ and $f$ a labeling function, and the true error is $L_{(D,f)}(h) = D(\{x : h(x) \ne f(x)\})$ ; the realizability assumption says some $h^\star \in H$ has $L_{(D,f)}(h^\star) = 0$ . $H$ is PAC learnable if some sample-complexity function $m_H$ and algorithm guarantee, for all $\epsilon, \delta \in (0,1)$ , all $D$ and all realizable $f$ , true error at most $\epsilon$ with probability at least $1 - \delta$ from $m \ge m_H(\epsilon, \delta)$ examples; agnostic PAC learnability with respect to a loss asks instead for $L_D(h) \le \min_{h' \in H} L_D(h') + \epsilon$ for every distribution over $Z$ .

Formalization targets

Goal: Corollary 3.2

Every finite hypothesis class is PAC learnable with sample complexity

m_H(\epsilon, \delta) \le \Big\lceil \frac{\log(|H|/\delta)}{\epsilon} \Big\rceil,

by the ERM rule: for a nonempty finite class of measurable hypotheses there is an ERM learner satisfying the PAC guarantee with that sample-complexity function.

Milestone

Corollary 2.3: under realizability, with $m \ge \log(|H|/\delta)/\epsilon$ examples, every ERM hypothesis has true error at most $\epsilon$ with probability at least $1 - \delta$ .

Significance

Corollaries 2.3 and 3.2 are the first learning theorem of the book and the template for all later sample-complexity bounds: a bad hypothesis is consistent with an i.i.d. sample with probability at most $(1 - \epsilon)^m \le e^{-\epsilon m}$ , and a union bound over the class turns this into a guarantee that holds uniformly over all distributions and all realizable labelings. Everything that follows, uniform convergence for finite classes, the fundamental theorem for classes of finite VC dimension, structural risk minimization, replaces the count $|H|$ by a finer measure of the class's complexity but keeps the argument. None of this is machine-checked. The mission fixes on the platform the objects that the rest of the series uses without change: risks, empirical risks, the product law of a sample, the ERM relation, and the four learnability notions of Definitions 3.1, 3.4, 4.1 and 4.3.

Difficulty

The milestone needs that, for a fixed measurable hypothesis whose true error exceeds $\epsilon$ , the product law gives the event "zero empirical risk" probability at most $(1-\epsilon)^m$ ; this is the product structure of Measure.pi on the event that each labeled example lies in the measurable set where the hypothesis agrees with $f$ , followed by $1 - \epsilon \le e^{-\epsilon}$ , the union bound over the finite class and the observation that under realizability every ERM hypothesis has zero empirical risk, so a bad ERM hypothesis is a consistent bad hypothesis. The goal packages this as a learner: existence of an ERM hypothesis for every sample (a finite nonempty class has a minimizer), and the arithmetic of the ceiling.

Formalization scope

The framework is the book's, with the risk as a Bochner integral, the sample law as a product measure, ERM as a relation and learners as deterministic functions of the sample; failure probabilities are stated as upper bounds on the outer measure of the failure set, the strong form of "with probability at least $1 - \delta$ "; the comparison with $\min_{h' \in H} L_D(h')$ is written without an infimum. Sample-complexity functions are carried explicitly: the book's $m_H$ as the minimal such function is not defined, and " $m_H \le f$ " is stated as "the learner satisfies the guarantee with the function $f$ ". Hypotheses and labeling functions are assumed measurable (Remark 3.1). The union bound (Lemma 2.2) is Mathlib's measure_union_le and is not an item. Hypotheses: $\epsilon > 0$ , $\delta \in (0,1)$ , $H$ finite (and nonempty for the learner to exist).

Trivializing readings are excluded: the milestone's failure event ranges over every ERM hypothesis, and the goal quantifies over all distributions, all realizable labelings and all $\epsilon, \delta$ . Welcome contributions: the product-law bound for a fixed hypothesis and the union bound over a finset, which every later mission of the series reuses.

Selected references

S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapters 2–4. doi:10.1017/CBO9781107298019
L. G. Valiant, A theory of the learnable, Communications of the ACM 27(11), 1984. doi:10.1145/1968.1972
V. N. Vapnik, The Nature of Statistical Learning Theory, Springer, 1995. doi:10.1007/978-1-4757-2440-0
D. Haussler, Decision theoretic generalizations of the PAC model for neural net and other learning applications, Information and Computation 100(1), 1992. doi:10.1016/0890-5401(92)90010-D

3 thms2 active usersReviewed

Completed

Combinatorics Machine Learning Probability·Captain: naimengye

An Introduction to Computational Learning Theory II: Occam's Razor, Set Cover and Decision ListsTextbook

Motivation

Chapter 2 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), gives a formal justification of Occam's Razor inside the PAC model. An Occam algorithm is judged not by the predictive power of its hypothesis but by how succinctly the hypothesis explains the sample before it: it must be consistent with the data and short, in the sense that its representation has fewer bits than the data it reproduces. The chapter's theorems say that, when the examples are drawn independently from a fixed distribution, such compression automatically yields prediction: a consistent hypothesis drawn from a small class is, with high probability, accurate on unseen examples. This turns the design of PAC learning algorithms into a combinatorial task, finding a short consistent hypothesis, and the chapter demonstrates the method three times: it shaves a logarithmic factor off the conjunction bound of Chapter 1, it learns conjunctions with few relevant variables through the greedy set-cover heuristic, and it learns Rivest's decision lists, a class strictly more expressive than $k$ -CNF and $k$ -DNF, by a greedy algorithm whose correctness is a one-line consequence of consistency.

Setting

The framework is that of Mission I: a measurable instance space, concepts as boolean functions, a target distribution $D$ , the product law of a sample of $m$ labeled examples, the error $\mathrm{error}(h) = \Pr_{x \sim D}[h(x) \neq c(x)]$ , and consistency of a hypothesis with a sample. Hypotheses may be represented by binary strings through a representation map, with size the bit length; an $(\alpha, \beta)$ -Occam algorithm outputs a consistent hypothesis of size at most $(n \cdot \mathrm{size}(c))^\alpha m^\beta$ with $0 \le \beta < 1$ . The set cover problem asks for a minimum subcollection of a collection $\mathcal{S}$ of subsets of a finite universe $U$ that covers $U$ ; the greedy heuristic repeatedly picks the set covering the most uncovered elements. A $k$ -decision list is a sequence of conditions, each a conjunction of at most $k$ literals, with a bit attached to each and a default bit; it evaluates to the bit of the first satisfied condition. The greedy decision-list algorithm repeatedly finds a useful condition, one satisfied by some remaining examples all of which carry the same label, appends it with that label and removes those examples.

Formalization targets

Goal: Theorem 2.2 (Occam's Razor, cardinality version)

For a finite hypothesis class $H$ , a target $c$ , a distribution $D$ and $0 < \epsilon \le 1$ , the probability that a sample of $m$ examples is consistent with some $h \in H$ of error greater than $\epsilon$ is at most $|H|(1 - \epsilon)^m$ ; hence

m \ge \frac{1}{\epsilon}\Big(\ln|H| + \ln\frac{1}{\delta}\Big)

makes this probability at most $\delta$ , and any algorithm that outputs a consistent hypothesis from $H$ has error greater than $\epsilon$ with probability at most $|H|(1-\epsilon)^m$ .

Milestones

Theorem 2.1 (an $(\alpha, \beta)$ -Occam algorithm is a PAC algorithm, with explicit sample-size conditions in place of the constant $a$ ); the greedy set-cover bound of §2.3 ( $|U_i| \le (1 - 1/\mathrm{opt})^i|U|$ and $\mathrm{opt}\ln|U|$ sets cover); the improved conjunction bound of §2.2; Theorem 2.3 ( $k$ -decision lists are PAC learnable by the greedy algorithm, which never fails and whose outputs are consistent).

Significance

Theorem 2.2 is the single most used tool of the subject: every finite-class sample bound, including the ones for conjunctions, decision lists, $k$ -CNF and the discretized geometric classes, is an instance of it, and the Vapnik–Chervonenkis theory of Chapter 3 is its extension to infinite classes with the growth function in place of $|H|$ . Theorem 2.1 is the philosophical statement, that succinct explanation implies prediction, and its converse (Exercise 2.3, and more strongly the boosting theorem of Chapter 4) makes Occam learning equivalent to PAC learning. The greedy set-cover bound is Chvátal's classical approximation guarantee, used in the book for learning with few relevant variables and again in later chapters. Theorem 2.3 is Rivest's result, and its proof exhibits the pattern "consistency by construction plus a counting bound" in its purest form. None of these is machine-checked. Their formalization gives the platform the union-bound-over-a-finite-class argument once and for all, in a form that the later missions of this series reuse verbatim.

Difficulty

Theorem 2.2 requires that, for a fixed measurable hypothesis with error greater than $\epsilon$ , the product law gives the event "consistent with all $m$ examples" probability at most $(1 - \epsilon)^m$ , which is the product structure of Measure.pi applied to the event that each coordinate lies in the set where $h$ agrees with $c$ ; the union bound over $H$ and the elementary inequality $(1 - \epsilon)^m \le e^{-\epsilon m}$ finish. Theorem 2.1 adds only the count of binary strings of length at most $K$ and arithmetic with real exponents. The set-cover bound is a discrete induction: an optimal cover of $U$ restricted to the uncovered elements has at most $\mathrm{opt}$ sets, so one of them, hence the greedy choice, covers a $1/\mathrm{opt}$ fraction; the covering clause needs the strict inequality $1 - 1/\mathrm{opt} < e^{-1/\mathrm{opt}}$ . Theorem 2.3 needs that a run of the greedy algorithm never repeats a condition (its satisfied examples are removed), so outputs lie in an explicit finite class, that the first condition of the target list satisfied by a remaining example is useful, and that a complete run is consistent; the bound is then Theorem 2.2.

Formalization scope

Everything is in the sample-complexity sense on the Mission I framework; running time is not modelled and "efficient" is dropped from every statement, which is recorded in the natural-language statements. Theorem 2.2's constant $b$ is $1$ with natural logarithms; Theorem 2.1's constant $a$ is replaced by three explicit sufficient conditions. Hypotheses in the finite class are required to be measurable. The greedy heuristic and the greedy decision-list algorithm are relations (any tie-breaking), and the theorems quantify over every run; the decision-list theorem is stated for every $k$ with the $k$ -conjunctions as conditions, so that its hypothesis is a $k$ -decision list rather than the expansion the book sketches for $k > 1$ . The conjunction count is $3^n + 1$ , including the empty concept that the elimination algorithm outputs on a sample without positive examples. The few-relevant-variables algorithm of §2.3 is not stated (its bound has an unspecified constant and $m$ on both sides). Hypotheses: $0 < \epsilon \le 1$ , $0 < \delta$ (and $\delta < 1$ where $\ln(1/\delta)$ must be nonnegative).

Trivializing readings are excluded: the bad-consistent event is over all of $H$ , the decision-list failure event ranges over every possible output, and the set-cover bound holds for every greedy run. Welcome contributions: the product-law bound for a fixed hypothesis, the union bound over a finset, the string-counting lemma, and the no-repetition lemma for greedy runs.

Selected references

M. J. Kearns, U. V. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994, Chapter 2. doi:10.7551/mitpress/3897.001.0001
A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Occam's razor, Information Processing Letters 24(6), 1987. doi:10.1016/0020-0190(87)90114-1
V. Chvátal, A greedy heuristic for the set-covering problem, Mathematics of Operations Research 4(3), 1979. doi:10.1287/moor.4.3.233
R. L. Rivest, Learning decision lists, Machine Learning 2(3), 1987. doi:10.1007/BF00058680
D. Haussler, Quantifying inductive bias: AI learning algorithms and Valiant's learning framework, Artificial Intelligence 36(2), 1988. doi:10.1016/0004-3702(88)90002-1

7 thms2 active usersReviewed

Completed

Combinatorics Machine Learning Probability·Captain: naimengye

An Introduction to Computational Learning Theory I: The PAC Model, Conjunctions, Rectangles and 3-CNFTextbook

Motivation

Chapter 1 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), introduces Valiant's Probably Approximately Correct model, the framework for the whole book. A learner sees labeled examples of an unknown target concept drawn from an unknown but fixed distribution, and must output a hypothesis that, with probability at least $1 - \delta$ over the sample, misclassifies a fresh example with probability at most $\epsilon$ ; the model is distribution-free, and the hypothesis is judged on the same distribution it was trained on. The chapter's three positive results are the templates for everything that follows. The rectangle game (Theorem 1.1) shows that an infinite class can be learned from a finite sample by exploiting the geometry of the error region. Conjunctions (Theorem 1.2) are learned by the elimination algorithm, whose analysis, a union bound over "bad" literals, is the prototype of every sample-size bound in the book. And 3-CNF formulae (Theorem 1.4) are learned by a change of variables that reduces them to conjunctions, which, set against the intractability of learning 3-term DNF as 3-term DNF (Theorem 1.3), is the reason the final definition of the model lets the hypothesis class differ from the concept class.

Setting

The instance space is a measurable space $X$ , a concept is a function $c : X \to \{0, 1\}$ , and the target distribution $D$ is a probability measure on $X$ . The error of a hypothesis $h$ is $\mathrm{error}(h) = \Pr_{x \sim D}[h(x) \ne c(x)]$ . A sample of $m$ examples is $S = ((x_1, c(x_1)), \dots, (x_m, c(x_m)))$ with the $x_i$ independent draws from $D$ ; a learning algorithm is a function from samples to hypotheses; it has the $(\epsilon, \delta)$ guarantee on a class $C$ if for every $c \in C$ and every $D$ the probability that its hypothesis has error greater than $\epsilon$ is at most $\delta$ ; $C$ is PAC learnable using $H$ if for all $\epsilon, \delta \in (0, 1/2)$ some sample size and algorithm with hypotheses in $H$ achieve the guarantee. For $X = \{0,1\}^n$ a literal is a variable or its negation and a conjunction is a finite set of literals; the elimination algorithm starts from all $2n$ literals and deletes every literal contradicted by a positive example. For $X = \mathbb{R}^2$ the concepts are the closed axis-aligned rectangles and the tightest-fit algorithm returns the smallest rectangle containing the positive examples. A 3-CNF formula is a conjunction of clauses of at most three literals; the expansion $a \mapsto a'$ records for each triple $(u, v, w)$ of literals the value $u \vee v \vee w$ .

Formalization targets

Goal: Theorem 1.2

Conjunctions of boolean literals are PAC learnable by the elimination algorithm: for every target conjunction, every distribution on $\{0,1\}^n$ and $\epsilon, \delta > 0$ , the elimination hypothesis is consistent with every sample labeled by the target, and with

m \ge \frac{2n}{\epsilon}\Big(\ln 2n + \ln\frac{1}{\delta}\Big)

examples its error exceeds $\epsilon$ with probability at most $\delta$ ; hence conjunctions are PAC learnable using conjunctions.

Milestones

Theorem 1.1 (rectangles by the tightest fit, $m \ge (4/\epsilon)\ln(4/\delta)$ ) and Theorem 1.4 (3-CNF formulae by elimination over the $(2n)^3$ expanded variables, the hypothesis being itself a 3-CNF formula).

Significance

Theorem 1.2 is Valiant's original result and the first instance of the two ideas that organize the subject: a hypothesis that is more specific than the target never errs on negative examples, and the error of the hypothesis decomposes as a sum over a polynomial number of "bad" events, each of which is avoided with probability exponentially close to one. Theorem 1.1 is the first learning result for an infinite concept class and the seed of the Vapnik–Chervonenkis theory of Chapter 3. Theorem 1.4 is the first reduction between learning problems and, together with Theorem 1.3, the demonstration that the choice of hypothesis representation can separate tractable from intractable. None of these theorems is machine-checked. Formalizing them fixes, for the rest of the series, the framework in which the error of a hypothesis, the law of a sample and the learnability of a class are stated, so that the Occam, VC-dimension, boosting and noise results of later chapters can be stated on the same objects.

Difficulty

The elimination analysis needs that the hypothesis contains every literal of the target, that its error is at most the sum over its literals $z$ of $p(z) = \Pr[c(a) = 1 \wedge z = 0 \text{ in } a]$ , and that a literal with $p(z) \ge \epsilon/2n$ survives $m$ independent examples with probability at most $(1 - \epsilon/2n)^m$ ; the probabilistic content is the independence of the coordinates of the sample law, which is a product measure, and the inequality $1 - x \le e^{-x}$ . The rectangle analysis is the four-strip argument, which for an arbitrary distribution, possibly with atoms, requires choosing the strip $\{y \ge t^*\}$ with $t^*$ the supremum of the heights at which the strip has weight at least $\epsilon/4$ and using the left-continuity of the weight in the height. The 3-CNF result transports the conjunction bound along the injective expansion: the pushforward of the sample law is the sample law of the expanded distribution, and the error of the composed hypothesis equals the error over the expanded variables. The deduction of PACLearnable from the explicit bounds is a choice of sample size.

Formalization scope

The model is stated in the sample-complexity sense: algorithms are functions of the sample, and the guarantee bounds the outer measure of the failure set under the product law of the sample, which is the strong form of "with probability at least $1 - \delta$ " and requires no measurability of the failure set. Running time, and hence "efficiently", is not modelled, and the hardness Theorem 1.3 is not stated; each theorem carries instead the explicit algorithm and the explicit sample bound of the book's analysis. Concepts on general instance spaces are required to be measurable in the guarantee. The cube is $\{0,1\}^n$ as functions Fin n → Bool; the expanded variables are indexed by the triples of literals, so $N = (2n)^3$ is a Fintype.card. Rectangles are closed, possibly empty; the tightest fit of a sample without positive examples is the empty concept. Hypotheses: $\epsilon > 0$ , $0 < \delta < 1$ ; the sample bounds are as printed, with natural logarithms.

Trivializing readings are excluded: the failure bound is uniform over all distributions and all targets in the class, consistency is asserted for every sample labeled by the target, and the learnability clause quantifies over all $\epsilon, \delta$ . Welcome contributions: the product-law bound $\Pr[\text{a fixed event of probability} \ge p \text{ is missed by all } m \text{ examples}] \le (1 - p)^m$ , the union bound over literals, and the pushforward identity for the expanded sample.

Selected references

M. J. Kearns, U. V. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994, Chapter 1. doi:10.7551/mitpress/3897.001.0001
L. G. Valiant, A theory of the learnable, Communications of the ACM 27(11), 1984. doi:10.1145/1968.1972
A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Learnability and the Vapnik–Chervonenkis dimension, Journal of the ACM 36(4), 1989. doi:10.1145/76359.76371
L. Pitt, L. G. Valiant, Computational limitations on learning from examples, Journal of the ACM 35(4), 1988. doi:10.1145/48014.63140

4 thms2 active usersReviewed

Completed

Machine Learning Probability Theoretical Computer Science·Captain: mikedeng1

Foundations of Machine Learning XIII: The Johnson-Lindenstrauss LemmaTextbook

Motivation

High-dimensional data is often computationally expensive to work with and hard to visualize. The Johnson-Lindenstrauss lemma answers a striking question in this setting: can any finite set of points, no matter how high-dimensional the ambient space, be squeezed into a space of dimension depending only on the number of points (logarithmically) and the desired accuracy, while barely disturbing the distances between them? The answer is yes, and — remarkably — a single, data-independent random construction (a random Gaussian matrix) achieves it with positive probability for any point set. This mission formalizes the lemma and the two probabilistic results its proof is built from.

Setting

For a set $V$ of $m$ points in $\mathbb R^N$ , a map $f:\mathbb R^N\to\mathbb R^k$ is a $(1\pm\epsilon)$ -distance-preserving embedding of $V$ if $(1-\epsilon)\|u-v\|^2\le\|f(u)-f(v)\|^2\le(1+\epsilon)\|u-v\|^2$ for every $u,v\in V$ . The book's proof constructs $f=A/\sqrt k$ from a random matrix $A\in\mathbb R^{k\times N}$ with i.i.d. standard normal ( $N(0,1)$ ) entries, and argues by the probabilistic method: for a fixed pair of points, Lemma 15.3 shows $f$ preserves their squared distance up to $(1\pm\epsilon)$ with probability at least $1-2e^{-(\epsilon^2-\epsilon^3)k/4}$ , because the ratio $\|f(x)\|^2/\|x\|^2$ (for $x$ the difference of the two points) is exactly a $\chi^2_k$ random variable, whose two-sided concentration around its mean $k$ is Lemma 15.2. A union bound over the $O(m^2)$ pairs in $V$ then shows the probability that every pair is simultaneously preserved is still strictly positive — so a map with the desired property must exist, even though no single fixed matrix is exhibited.

Formalization targets

Lemma 15.2 (Chi-squared concentration, milestone). If $Q\sim\chi^2_k$ , then for $0<\epsilon<1/2$ , $P[(1-\epsilon)k\le Q\le(1+\epsilon)k]\ge1-2e^{-(\epsilon^2-\epsilon^3)k/4}$ .

Lemma 15.3 (Gaussian random projection distortion, milestone). For $x\in\mathbb R^N$ , $k<N$ , and $A\in\mathbb R^{k\times N}$ with i.i.d. $N(0,1)$ entries,

P\Big[(1-\epsilon)\|x\|^2\le\big\|\tfrac1{\sqrt k}Ax\big\|^2\le(1+\epsilon)\|x\|^2\Big] \ge1-2e^{-(\epsilon^2-\epsilon^3)k/4}.

Lemma 15.4 — the mission's goal (Johnson-Lindenstrauss). For $0<\epsilon<1/2$ , integer $m>4$ , and $k=20\log(m)/\epsilon^2$ , any set $V$ of $m$ points in $\mathbb R^N$ admits a map $f:\mathbb R^N\to\mathbb R^k$ with $(1-\epsilon)\|u-v\|^2\le\|f(u)-f(v)\|^2\le(1+\epsilon) \|u-v\|^2$ for all $u,v\in V$ .

Significance

This is one of the cleanest instances in the book of the probabilistic method: existence is proved without exhibiting the object, by showing a random construction succeeds with positive probability. The target dimension $k=O(\log m/\epsilon^2)$ is independent of the ambient dimension $N$ — the embedding works no matter how large the original feature space is, which is exactly why the lemma has inspired random-projection methods throughout dimensionality reduction, streaming algorithms, and compressed sensing. Prior art on the Prove2Me platform is not faithful here: HighDimProb.Isoperimetry.johnson_lindenstrauss (Vershynin series) proves a Johnson-Lindenstrauss-type bound, but via a uniformly-random $m$ -dimensional subspace and its orthogonal projection, rescaled by $\sqrt{n/m}$ — a genuinely different construction from this book's explicit i.i.d.-Gaussian-matrix map $f=A/\sqrt k$ , and with different (existentially quantified, unspecified) constants rather than this book's explicit $k=20\log(m)/\epsilon^2$ . The two are classically known to give essentially the same qualitative guarantee, but showing them equivalent would require an independent equivalence proof neither platform item nor this mission undertakes; per the chunk's own brief, the Vershynin theorem is cited here only as related work, not reused as a kind: reference item.

Not formalized here: Theorem 15.1 (the PCA solution), the chapter's other headline result. BRIEF.md explicitly flags PCA and JL as the chapter's two independent capstones, not a proof chain, and recommends dropping PCA if the mission focuses purely on JL. Theorem 15.1's proof is an Eckart-Young-type Frobenius-norm optimization argument over the set of rank- $k$ orthogonal projection matrices — sharing no definitions, hypotheses, or proof technique with the probabilistic-method argument this mission's three items are built from. Formalizing it would mean standing up a second, unrelated piece of mathematics (constrained matrix optimization, singular value decomposition) from scratch for a single additional item; per the captain brief's guidance to leave out, rather than approximate, material disproportionate to the time budget, it is omitted. §15.2 (kernel PCA) and §15.3 (Isomap, LLE, Laplacian eigenmaps) are likewise out of scope, per BRIEF.md's own page-range restriction — applications- heavy manifold-learning material with no numbered result feeding Lemma 15.4's proof.

Difficulty

Lemma 15.2's proof is a genuine Chernoff-bound argument: apply Markov's inequality to $\exp(\lambda Q)$ , substitute the chi-squared distribution's own moment-generating function $(1-2\lambda)^{-k/2}$ , and optimize the resulting bound over $\lambda\in(0,1/2)$ by calculus (the book's own choice $\lambda=\epsilon/(2(1+\epsilon))$ is exactly the minimizer) — not a one-line union of tail bounds, and the same argument must be repeated (with a sign flip) for the lower tail before combining via a union bound. Lemma 15.3's proof needs the non-obvious observation that $T_j=\widehat x_j/\|x\|$ (for $\widehat x=Ax$ ) are themselves i.i.d. standard normal — a consequence of $A$ 's i.i.d. Gaussian entries and $\mathbb E[\widehat x_j^2]=\|x\|^2$ , not immediate from the definitions alone — before the sum of their squares can be recognized as exactly a $\chi^2_k$ variable and Lemma 15.2 applied. Lemma 15.4's own proof, while conceptually simple (a single union bound), needs the specific numerical accounting $2m^2e^{-(\epsilon^2-\epsilon^3)k/4}=2m^{5\epsilon-3}<2m^{-1/2}$ at the chosen $k=20\log(m)/\epsilon^2$ and $\epsilon\le1/2$ to conclude the success probability is strictly positive — a formalization that merely asserted "the union bound gives a positive probability" without this exact accounting would not establish the book's specific, tight constant $k=20\log(m)/\epsilon^2$ .

Formalization scope

SqNorm is the coordinate-wise squared Euclidean norm (∑ᵢ vᵢ²), used in place of Mathlib's EuclideanSpace/PiLp norm typeclass machinery to keep the statements close to the book's own concrete ℝ^N/ℝ^k-coordinate notation. IsChiSquaredMGF states the moment-generating-function characterization of a chi-squared distribution that the proof of Lemma 15.2 itself cites (Eq. C.25), rather than restating the book's own Definition C.7, which sits in an out-of-chapter appendix not read for this mission; this is checked (in SELF_REVIEW.md) to be a faithful, uniquely-determining substitute, since a real random variable's law is determined by its MGF wherever it is finite near 0. IsIIDStandardGaussianMatrix states "i.i.d. standard normal entries" via Mathlib's gaussianReal 0 1 (marginal law) together with iIndepFun (joint independence). The goal theorem's target dimension k is taken as ⌈20 log(m)/ε²⌉ (Nat.ceil) rather than the book's real-valued 20 log(m)/ε², since a map's codomain dimension must be a natural number; this rounding only strengthens (never weakens) the existential conclusion, since the union-bound success probability is monotonically increasing in k. No numerical constant in any of the three items is otherwise altered from the book's own displayed form. A trivializing formalization this mission avoids: stating Lemma 15.4 with an unspecified k = O(log m/ε²) (an asymptotic, not an explicit constant) — per BRIEF.md's own naming of this as one of the series' "explicit-constant" results, k's exact formula 20 log(m)/ε² (up to the ceiling needed for well-typedness) is stated directly.

Selected references

M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 15, §15.4.
W. B. Johnson, J. Lindenstrauss, "Extensions of Lipschitz mappings into a Hilbert space," Contemporary Mathematics 26, 1984, 189-206.
S. Vempala, The Random Projection Method, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 2004.

6 thms2 active usersReviewed

Completed

Machine Learning Probability·Captain: mikedeng1

Support Vector Machines VII: Consistency of Support Vector Machines for RegressionTextbook

Motivation

Chapter 9 asks whether the support vector machine — a regularized empirical risk minimizer $f_{D,\lambda}$ over an RKHS $H$ — is a statistically consistent estimator for regression: does $R_{L,P}(f_{D,\lambda_n}) \to R^*_{L,P}$ as the sample size $n \to \infty$ , for a suitable regularization schedule $\lambda_n \to 0$ ? The chapter's main theorem (Theorem 9.1) answers yes, under an explicit polynomial rate condition on $\lambda_n$ . Its proof reduces the question to bounding how far the empirical regularized solution can be from the population regularized solution, and that reduction bottoms out in a single concentration-of-measure fact: how tightly does an empirical mean of i.i.d. Hilbert-space-valued random variables concentrate around its true mean, given only a bound on one $q$ -th moment (no exponential-moment assumption at all)? That fact is Lemma 9.2, "the following lemma to bound the probability of $|R_{L,P}(f_{D,\lambda}) - R_{L,P}(f_{P,\lambda})| \le \varepsilon$ for $|D| \to \infty$ " — the technical core the whole chapter's consistency argument rests on, and this mission's goal.

Setting

Fix a measurable space $Z$ , a distribution $P$ on $Z$ , a separable Hilbert space $H$ , and a measurable $g : Z \to H$ . Its $q$ -th moment norm, for $q \in (1,\infty)$ , is $\|g\|_q := (\mathbb E_P\|g\|_H^q)^{1/q}$ — the direct Hilbert-space analogue of an ordinary $L^q$ norm. The proof machinery behind concentration results of this kind is symmetrization: replacing a centered i.i.d. sum $\frac1n\sum_i(\xi_i - \mathbb E_P\xi_i)$ by a Rademacher-randomized sum $\frac1n\sum_i \varepsilon_i \xi_i$ , where a Rademacher sequence $\varepsilon_1,\dots,\varepsilon_n$ is a family of independent $\pm1$ -valued random variables, each taking each sign with probability $1/2$ . Once randomized, the sum's $L^p$ -norms (for different $p$ ) become comparable to each other via Kahane's inequality, with a universal constant depending only on the two exponents involved — never on the sample size or the ambient Banach space.

Formalization targets

Goal: Lemma 9.2 (concentration of Hilbert-space-valued sample means)

P^n\!\left(\left\{(z_1,\dots,z_n) \in Z^n : \left\|\frac1n\sum_{i=1}^n g(z_i) - \mathbb E_P g\right\|_H \ge \varepsilon\right\}\right) \le c_q\left(\frac{\|g\|_q}{\varepsilon\, n^{q^*}}\right)^{q}, \qquad q^* := \min\{1/2,\,1-1/q\}

for a universal constant $c_q>0$ depending only on $q$ , every $\varepsilon>0$ and every $n \ge 1$ . This is a genuine generalization of Chebyshev's inequality to Hilbert-space-valued means, sharp enough (via the explicit rate $n^{-q^*}$ ) to drive Theorem 9.1's own polynomial regularization condition $\lambda_n^{p^*} n \to \infty$ .

Milestones (attack order)

Theorem A.8.1 (Symmetrization) — $\mathbb E_P\Psi(\|\frac1n\sum_i(\xi_i-\mathbb E_P\xi_i)\|) \le \mathbb E_P\mathbb E_\nu\Psi(2\|\frac1n\sum_i\varepsilon_i\xi_i\|)$ for convex non-decreasing $\Psi$ , i.i.d. $P$ -integrable $\xi_i$ valued in a separable Banach space, and a Rademacher sequence $\varepsilon_i$ . Directly cited in Lemma 9.2's proof ("Using the symmetrization argument given in Theorem A.8.1...").
Theorem A.8.3 (Kahane's inequality) — for a Rademacher sequence, every two $L^p(\nu)$ and $L^q(\nu)$ norms of $\|\sum_i\varepsilon_ix_i\|$ are comparable via a universal constant $K_{p,q}$ , independent of $n$ and the Banach space $E$ . Directly cited in Lemma 9.2's proof ("If $q\in(1,2]$ , we obtain with Kahane's inequality, see Theorem A.8.3, that...").

Theorem 9.1 itself (BRIEF.md's recommended goal — the full SVM-regression consistency theorem) was not attempted this session; see STATUS.md for the reason and the fallback taken instead.

Significance

Lemma 9.2 is stated and proved once, in the Appendix's general Rademacher-sequence toolkit and this chapter, and then used directly to obtain Theorem 9.1's consistency guarantee: substituting $g :=$ the pointwise SVM "difference process" into Lemma 9.2 converts a purely probabilistic concentration fact into a statement about how close the empirical SVM solution's risk is to the population solution's risk, for every sample size. Because the bound depends on nothing but a single moment $\|g\|_q$ — no boundedness, no sub-Gaussian tail — it is what lets Theorem 9.1 avoid assuming the loss or the label distribution has any exponential tail control, which is essential for regression (where $Y \subset \mathbb R$ need not be bounded, unlike the classification setting of this series' earlier chapters). Symmetrization and Kahane's inequality are themselves standard, reusable tools of empirical process theory (used throughout Chapter 7's entropy-number program, excluded from this series, and Chapter 6's classification oracle inequality).

Difficulty

The published proof of Lemma 9.2 is a short but dense computation: Markov's inequality reduces the tail bound to bounding $\mathbb E_{P^n}\|h\|_H^q$ for the centered mean $h$ ; Theorem A.8.1 symmetrizes; for $q \in (1,2]$ , Theorem A.8.3 (Kahane) converts the $q$ -th moment of the Rademacher sum to its second moment, which an explicit orthogonality computation (the book's Eq. (9.4), $\mathbb E_{\nu^n}\|\sum_i\varepsilon_ix_i\|^2 = \sum_i\|x_i\|^2$ for any fixed $x_1,\dots,x_n$ , an immediate consequence of the Rademacher signs' independence and the Hilbert space's parallelogram identity) reduces to a sum of individual second moments; the case $q>2$ argues analogously with a different exponent split. None of this computation is captured by this mission's two milestones alone — they supply the two cited theorems, not the connecting algebra — so a complete proof of the goal from the milestones as stated still requires reconstructing this argument, exactly as the captain brief's milestones are meant to be (the book's own attack path, not a fully mechanized proof outline).

Formalization scope

$Z$ and $\Theta$ (the Rademacher sequence's own probability space) are arbitrary measurable spaces; $H$ is [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [MeasurableSpace H] [BorelSpace H] [SeparableSpace H] (a separable real Hilbert space with its Borel $\sigma$ -algebra), matching " $H$ be a separable Hilbert space" without narrowing to a concrete space (e.g. $\ell^2$ ) the book itself does not assume. IsRademacherSequence states independence via Mathlib's iIndepFun and the $\pm1$ -probability- $1/2$ condition directly, since no ready-made "Rademacher distribution" object exists in this Mathlib revision (checked by search). $q^* := \min\{1/2, 1-1/q\}$ is substituted algebraically rather than introducing a separate conjugate exponent $q'$ , since $1/q+1/q'=1$ pins $q'$ down uniquely — not a change of content. In Theorem A.8.3, "for all Banach spaces $E$ " quantifies over E : Type (the Type 0 universe) rather than every universe Type*, a disclosed minor restriction with no effect on this mission's own use of the theorem (with $E$ instantiated to a Type* Hilbert space $H$ that is, in every actual application, itself at the Type level).

A trivializing formalization here would drop the "independent" half of IsRademacherSequence (leaving only the marginal $\pm1$ -probability- $1/2$ condition, true even for perfectly correlated signs) or drop the "i.i.d." qualifier on $\xi_1,\dots,\xi_n$ in Theorem A.8.1 (both symmetrization and Kahane's inequality are false, or at least unproven by the book's own argument, without independence) — both are ruled out here by stating iIndepFun explicitly rather than only the marginal distribution conditions.

IsRademacherSequence is reusable beyond this mission: any future formalization of Chapter 7's entropy-number/Rademacher-complexity program, or of Chapter 6's oracle inequality's own use of Rademacher averages, would restate it locally (per Hard Rule 9) from the same book definition. Contributions completing the three sorrys are welcome; Theorem 9.1 itself remains a natural, substantially larger follow-up mission built on top of this one's two milestones together with the RKHS/regularized-risk-minimizer apparatus already available in this series' 04-representer mission (restated locally, per Hard Rule 9).

Selected references

I. Steinwart & A. Christmann, Support Vector Machines, Springer, Information Science and Statistics, 2008. https://doi.org/10.1007/978-0-387-77242-4 (Chapter 9, §§9.1-9.2, pp. 333-337, and Appendix §A.8, pp. 535-537).
J.-P. Kahane, Some Random Series of Functions, 2nd ed., Cambridge University Press, 1985 (Kahane's inequality, Theorem A.8.3's original source).
A. W. van der Vaart & J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996 (Lemma 2.3.1, the source of Theorem A.8.1's proof technique).

4 thms2 active usersReviewed

Completed

Machine Learning Optimization Probability+1·Captain: mikedeng1

High-Dimensional Probability X: Exact Sparse RecoveryTextbook

Motivation

Compressed sensing asks a question that looks impossible at first: can a signal $x\in\mathbb R^n$ be reconstructed exactly from far fewer than $n$ linear measurements $y=Ax\in\mathbb R^m$ , $m\ll n$ ? Classical linear algebra says no — an underdetermined system has infinitely many solutions. But if $x$ is known in advance to be sparse (most of its coordinates are zero), the extra structure makes recovery possible: solving the convex program that minimizes the $\ell_1$ norm of a candidate solution, subject to matching the measurements, recovers $x$ exactly, for a measurement matrix $A$ with a suitable geometric property. This idea, developed by Candès, Romberg, Tao and Donoho in the mid-2000s, underlies modern MRI acceleration, single-pixel cameras, and sparse signal processing generally.

The chapter isolates the exact geometric property a measurement matrix needs — the restricted isometry property (RIP) — and proves, purely by linear algebra with no probability involved, that RIP alone is sufficient for exact recovery by $\ell_1$ minimization. (A companion result, outside this mission, shows random sub-gaussian matrices satisfy RIP with high probability once $m$ is large enough, which is what makes the deterministic guarantee here practically useful; this mission formalizes the deterministic half.)

Setting

For a vector $v$ indexed by a finite set, write $\|v\|_0$ for its number of non-zero coordinates (so $v$ is $s$ -sparse if $\|v\|_0\le s$ ), $\|v\|_1:=\sum_i|v_i|$ for its $\ell_1$ norm, and $\|v\|_2:=\sqrt{\sum_i v_i^2}$ for its Euclidean norm.

An $m\times n$ matrix $A$ satisfies the restricted isometry property (RIP) with parameters $\alpha,\beta,s$ if

\alpha\|v\|_2 \;\le\; \|Av\|_2 \;\le\; \beta\|v\|_2 \qquad\text{for every } s\text{-sparse } v\in\mathbb R^n,

i.e. $A$ acts as an approximate isometry on every $s$ -sparse vector — equivalently (the book's own Exercise 10.5.9), the singular values of every $m\times s$ column-submatrix of $A$ lie in $[\alpha,\beta]$ .

Given a matrix $A$ and measurements $y=Ax$ for an unknown sparse $x$ , the exact-recovery program is

\text{minimize } \|x'\|_1 \quad\text{subject to}\quad y = Ax'.

Formalization targets

Goal (Theorem 10.5.10, RIP implies exact recovery)

\exists\,\hat x = x \quad\text{whenever}\quad \hat x \text{ solves the exact-recovery program for } y=Ax,

precisely: suppose $A$ satisfies RIP with parameters $\alpha,\beta,(1+\lambda)s$ where $\lambda>(\beta/\alpha)^2$ ; then for every $s$ -sparse $x$ , every $\hat x$ that is feasible ( $A\hat x=Ax$ ) and $\ell_1$ -optimal among feasible vectors satisfies $\hat x=x$ . No constant here is hard-coded beyond the book's own explicit threshold $\lambda>(\beta/\alpha)^2$ — the weakest stable form of the claim.

Significance

RIP isolates exactly the geometric mechanism that makes $\ell_1$ -minimization work for sparse recovery: once a matrix is known to satisfy it, exact recovery is a deterministic, provable consequence with no appeal to randomness, no failure probability, and no measurement-count formula to verify beyond the RIP parameters themselves. This clean separation — a purely geometric sufficient condition (RIP), proved separately (in the book's Theorem 10.5.11, outside this mission) to hold with high probability for random sub-gaussian matrices — is the template compressed sensing theory follows throughout: geometric/deterministic guarantee first, probabilistic verification that random constructions meet it second. The theorem is one of the two standard routes (with the direct probabilistic argument of Theorem 10.5.1) to the chapter's central claim that $m=O(s\log n)$ measurements suffice to recover any $s$ -sparse signal in $\mathbb R^n$ — exponentially fewer than the $n$ measurements a naive linear-algebraic argument would need.

The result itself, and the RIP framework, are classical and well-established (Candès-Tao 2005). This mission formalizes the deterministic linear-algebra core of the argument — the statement infrastructure (RIP, sparsity, the exact-recovery program stated as an explicit optimization problem) and the goal theorem — for a solver to close with a proof.

Difficulty

The natural first idea for showing $\hat x=x$ is to try to bound the recovery error $h:=\hat x-x$ directly using $\|Ah\|_2$ (which vanishes, since both $x$ and $\hat x$ are feasible) together with RIP applied to $h$ itself — but $h$ need not be sparse at all: it is the difference of two sparse-ish vectors and can have full support. The actual argument decomposes $h$ 's support into blocks by descending magnitude (the support $I_0$ of $x$ , then the $\lambda s$ largest remaining coordinates $I_1$ , then the next $\lambda s$ , and so on), applies RIP only to the leading block $I_{0,1}=I_0\cup I_1$ (which genuinely has bounded sparsity $\le(1+\lambda)s$ ), and separately bounds the contribution of every later block using the fact that $\hat x$ is $\ell_1$ -optimal (so $\|h_{I_0^c}\|_1\le\|h_{I_0}\|_1$ , the "cone constraint"): each later block's $\ell_2$ norm is controlled by the $\ell_1$ mass of the previous block divided by its size. This is a genuinely multi-step argument combining a purely geometric fact (RIP on one bounded-sparsity block) with a purely combinatorial one (the magnitude-sorted decomposition), and the "obvious" idea of applying RIP to $h$ as a whole does not typecheck, since RIP says nothing about vectors with more than $(1+\lambda)s$ non-zero entries.

Formalization scope

Vectors are plain functions ι → ℝ on a finite index type, not EuclideanSpace ℝ ι: the latter's fixed $\ell_2$ norm instance cannot also host the $\ell_1$ norm the program's objective needs, so both norms (L2Norm, L1Norm) are defined directly by their defining sums on the same underlying type. Sparsity (Sparsity) takes a real-valued threshold s : ℝ, matching that the RIP parameter $(1+\lambda)s$ used by the goal theorem is a real number even at integer base sparsity. A solution $\hat x$ "of the program" is formalized as an explicit argmin membership — feasibility (A.mulVec xhat = A.mulVec x) conjoined with optimality over the exact feasible set (∀ x', A.mulVec x' = A.mulVec x → l1Norm xhat ≤ l1Norm x') — never "there exists an estimator such that", the trivialization risk this chapter's own triage brief flags explicitly (shared with Chapter 3's Max-Cut): an existential reading would prove a different, strictly weaker statement. The conclusion is stated for every such $\hat x$ , not one witness, matching that RIP forces uniqueness.

This mission covers Theorem 10.5.10 only, as the sole item; the probabilistic goal Theorem 10.5.1 (exact recovery for random sub-gaussian measurement matrices, which needs Theorem 10.5.10 together with a separate probabilistic argument, Theorem 10.5.11, that random matrices satisfy RIP), and the Lasso guarantee (Theorem 10.6.1), are both left out for lack of session time: each would need a fresh probabilistic apparatus (independent isotropic sub-gaussian random rows, a failure-probability bound) built from scratch in this chapter's own sub-namespace, with no reusable published definition from an earlier chunk. L2Norm, L1Norm, Sparsity and RIP are reusable by any later chapter or mission needing sparse vectors or the restricted isometry property; solvers' contributions are welcome on completing the proof of Theorem 10.5.10 itself (the magnitude-sorted support decomposition sketched under Difficulty above), and, beyond this mission's current scope, on Theorem 10.5.11 and Theorem 10.5.1.

Selected references

E. J. Candès, T. Tao, Decoding by linear programming, IEEE Transactions on Information Theory 51 (2005), 4203–4215. https://doi.org/10.1109/TIT.2005.858979
D. L. Donoho, Compressed sensing, IEEE Transactions on Information Theory 52 (2006), 1289–1306. https://doi.org/10.1109/TIT.2006.871582
R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 10. https://doi.org/10.1017/9781108231596

5 thms2 active usersReviewed

Completed

Machine Learning Probability·Captain: mikedeng1

High-Dimensional Statistics IV: Dudley's Entropy Integral BoundTextbook

Motivation

Many of the central questions of high-dimensional statistics reduce to bounding the expected supremum of a stochastic process: the maximum correlation of noise with a family of candidate signals, the operator norm of a random matrix, the uniform deviation of an empirical process from its mean. Whenever the index set of the process is infinite or exponentially large, a naive union bound over "all" indices is either vacuous or requires re-deriving a tail bound from scratch for every new problem. Chaining is the general-purpose technique that removes this need: it bounds the expected supremum of a process purely in terms of the geometry of its index set, measured by how many balls of a given radius are needed to cover it. The classical form of this bound is due to Dudley (1967), building on ideas that trace to Kolmogorov; the exposition here follows Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 5.

Setting

Fix an index set $T$ and a collection of zero-mean random variables $\{X_\theta,\theta\in T\}$ . Say this collection is a sub-Gaussian process with respect to a (pseudo)metric $\rho_X$ on $T$ (Definition 5.16) if

\mathbb E\big[e^{\lambda(X_\theta-X_{\theta'})}\big] \;\le\; e^{\lambda^2\rho_X(\theta,\theta')^2/2} \qquad \text{for all } \theta,\theta'\in T,\ \lambda\in\mathbb R.

This single condition covers, as special cases, the canonical Gaussian process $X_\theta = \langle\theta, w\rangle$ for $w$ a standard Gaussian vector (with $\rho_X$ the Euclidean metric) and the Rademacher process built from i.i.d. Rademacher signs.

A $\delta$ -cover of $T$ with respect to a metric $\rho$ is a finite set $\{\theta_1,\dots,\theta_N\}\subset T$ such that every $\theta\in T$ lies within $\rho$ -distance $\delta$ of some $\theta_i$ ; the $\delta$ -covering number $N(\delta;T,\rho)$ is the size of the smallest such cover (Definition 5.1). The quantity $\log N(\delta;T,\rho)$ is the metric entropy of $T$ at scale $\delta$ . Writing $D:=\sup_{\theta,\theta'\in T}\rho_X(\theta,\theta')$ for the diameter of $T$ , the $\delta$ -truncated Dudley entropy integral is

J(\delta; D) \;:=\; \int_\delta^D \sqrt{\log N(u;T)}\,du.

Formalization targets

Goal — Theorem 5.22 (Dudley's entropy integral bound)

\mathbb E\Big[\sup_{\theta,\theta'\in T}(X_\theta-X_{\theta'})\Big] \;\le\; 2\,\mathbb E\Big[\sup_{\substack{\gamma,\gamma'\in T\\\rho_X(\gamma,\gamma')\le\delta}}(X_\gamma-X_{\gamma'})\Big] + 32\,J(\delta/4; D), \qquad \text{for any } \delta\in[0,D].

The bound holds for every zero-mean sub-Gaussian process, with no further structure on $T$ beyond its metric entropy — this is what makes it a general-purpose tool rather than a bound tailored to one model.

Milestone — Proposition 5.17 (one-step discretization bound)

The same conclusion with $32\,J(\delta/4;D)$ replaced by the cruder single-scale term $4\sqrt{D^2\log N(\delta;T)}$ , under the extra technical hypothesis $N(\delta;T)\ge 10$ . This is the one-step precursor whose refinement — iterating the discretization over a geometric sequence of scales instead of applying it once — is exactly what chaining improves.

Milestone — Theorem 5.25 (the Gaussian comparison principle)

A general comparison principle for pairs of centered Gaussian random vectors whose pairwise covariances are ordered coordinatewise and tested against a function with matching sign conditions on its mixed second partial derivatives: $\mathbb E[F(X)]\le\mathbb E[F(Y)]$ . This is the source, by specializing $F$ and the covariance-ordering sets, of both Slepian's inequality and the Sudakov–Fernique comparison, the two workhorse tools of Gaussian process theory used elsewhere in the chapter to obtain sharper, Gaussian-specific bounds than the sub-Gaussian chaining bound above.

Significance

Dudley's bound is the single most-used tool for controlling suprema of stochastic processes in high-dimensional statistics and empirical process theory: Gaussian complexity bounds for convex bodies, operator-norm bounds for random matrices, and uniform laws of large numbers for function classes are all obtained by computing a covering-number bound for the relevant index set and substituting it into Theorem 5.22 (see, for instance, Examples 5.18–5.21 later in the same chapter, and Chapters 13–14 of the book). Its significance is exactly its generality: it converts a purely geometric quantity — how "big" a set is under a metric — into a probabilistic bound, uniformly over every sub-Gaussian process on that set.

Formalizing it. The mathematical proof (interpolation-free, based on chaining and repeated union bounds) is well understood and not itself in question; what this mission produces is a faithful Lean statement of the theorem, its immediate one-step precursor, and the general Gaussian comparison principle that underlies the chapter's complementary (Gaussian-specific) results, each against Mathlib's own measure-theoretic and Gaussian-process infrastructure. All three theorems are currently stated as open goals (:= by sorry); no claim is made here that they are already formalized elsewhere on the platform (a fresh prior-art search for "Dudley," "chaining," "Slepian," "Sudakov," and "Gaussian comparison" returned no faithful matches).

Difficulty

The naive approach — apply Proposition 5.17's one-step discretization once, at whatever scale $\delta$ seems best — cannot see improvement past the cruder $\sqrt{D^2\log N(\delta;T)}$ scaling of the metric entropy at a single resolution. The chaining argument that proves Theorem 5.22 instead telescopes the supremum across a geometric ladder of covers at scales $D2^{-1},D2^{-2},\dots$ , paying for each scale's approximation with a union bound over its own (much smaller, for a small $\delta$ ) covering number, and only then summing the resulting terms into an integral. The difficulty is not any single step of this argument — each step is an elementary sub-Gaussian tail bound — but bookkeeping the composition correctly: the recursive "best approximation at level $m$ of the best approximation at level $m+1$ " chain (Eq. (5.47)) must be built explicitly, and the telescoping sum of $L$ union bounds, each over a set that itself depends on the level $m$ , is what converts into an integral only in the $L\to\infty$ limit as the covers refine to $T$ itself.

Formalization scope

The index set $T$ is formalized as a nonempty Fintype, rather than the book's general totally bounded metric space: this keeps every covering number, diameter, and supremum in this mission a genuine maximum over a finite, nonempty family (realized via ⨆/sInf over finite index types), rather than requiring the full apparatus of totally bounded infinite metric spaces to state the covering-number definition (Definition 5.1) faithfully without risking a vacuous or ill-defined infimum. This is a genuine narrowing of the book's stated generality, disclosed here rather than left implicit — the underlying mathematics of the proof does not depend on finiteness, but a faithful formalization of a general totally bounded space's covering number was judged out of scope for this mission's budget.

The constant $32$ in the goal theorem is kept exactly as stated; the book's own remark that "there is no particular significance to the constant 32, which could be improved with a more careful analysis" is not license to substitute a sharper constant, since doing so would no longer match what this particular proof establishes. Expectations are Bochner integrals against an explicit probability measure Prob, with integrability required as an explicit hypothesis in the sub-Gaussian process definition (SubGaussianProcess) rather than left implicit, since Mathlib's Bochner integral silently returns $0$ for a non-integrable function — a trivializing formalization this mission's definitions and hypotheses rule out.

Theorem 5.25's "centered Gaussian random vector" is formalized using Mathlib's own ProbabilityTheory.HasGaussianLaw predicate (a genuine multivariate Gaussian law, not merely Gaussian marginals) together with an explicit coordinatewise mean-zero hypothesis, and its mixed second partial derivative condition is formalized via iteratedFDeriv ℝ 2 F applied to the relevant pair of standard basis vectors, keeping the sign pattern over the disjoint index sets $A$ and $B$ exact rather than collapsing it to a global convexity assumption on $F$ .

Out of scope for this mission: Sudakov's minoration (the complementary lower bound on the expected supremum of a genuinely Gaussian process, Theorem 5.30, misidentified as "Theorem 5.36" in this mission's planning brief — the correct Sudakov minoration statement is Theorem 5.30, p. 148; Theorem 5.36 is instead a tail-bound generalization of Dudley's bound to $\psi_q$ -Orlicz processes) and the Slepian/Sudakov–Fernique corollaries of Theorem 5.25 (Corollary 5.26, Theorem 5.27) — both natural follow-on work for a later contribution, once the Gaussian comparison principle formalized here is in place.

Selected references

M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019. DOI: 10.1017/9781108627771. Chapter 5.
R. M. Dudley, "The sizes of compact subsets of Hilbert space and continuity of Gaussian processes," Journal of Functional Analysis, 1(3):290–330, 1967.
M. Ledoux and M. Talagrand, Probability in Banach Spaces: Isoperimetry and Processes, Springer, 1991.

9 thms2 active usersReviewed

Completed

Machine Learning Probability Random Matrix Theory·Captain: mikedeng1

High-Dimensional Probability VII: Slepian's Inequality for Gaussian ProcessesTextbook

Motivation

A Gaussian process is a family $(X_t)_{t\in T}$ of jointly Gaussian real random variables indexed by an arbitrary set $T$ — not necessarily time. The canonical example is $X_t = \langle g, t\rangle$ for $t$ ranging over a subset $T\subseteq\mathbb R^n$ and $g$ a standard Gaussian vector in $\mathbb R^n$ ; this single family already encodes questions as varied as the operator norm of a random matrix, the size of a random projection, and the metric complexity of a convex body. In every one of these applications the object of interest reduces to the same quantity: $E\sup_{t\in T} X_t$ , the expected supremum of the process.

Bounding $E\sup_{t\in T} X_t$ directly is hard — computing it exactly is possible only in special cases, such as the reflection principle for Brownian motion. Slepian's inequality (David Slepian, 1962) sidesteps this by comparison: if a second Gaussian process $(Y_t)_{t\in T}$ has matching variances and at-least-as-large pairwise increments as $(X_t)_{t\in T}$ , then $Y$ 's supremum stochastically dominates $X$ 's. This turns a hard direct estimate into a search for a simpler comparison process — the technique that Sudakov and Fernique later sharpened by dropping the equal-variance hypothesis (Theorem 7.2.11), and that Sudakov used to derive a purely geometric lower bound on $E\sup_{t\in T}X_t$ from the covering numbers of $(T,d)$ (Theorem 7.4.1, Sudakov's minoration inequality). Together these results are the entry point to the theory of Gaussian width and generic chaining that occupies the rest of the book (Chapters 7–9, 11), and they underlie sharp bounds on random matrices (Section 7.3), random projections (Chapter 9), and high-dimensional geometry more broadly (Adler and Taylor, Random Fields and Geometry, Springer, 2007; Talagrand, Upper and Lower Bounds for Stochastic Processes, Springer, 2014).

Setting

Fix a probability space $(\Omega,\mathcal F,P)$ . A random process indexed by a set $T$ is a family $(X_t)_{t\in T}$ of real random variables on $\Omega$ . It is a Gaussian process if every finite linear combination $\sum_{t\in T_0} a_t X_t$ ( $T_0\subseteq T$ finite, $a_t\in \mathbb R$ ) is a (possibly degenerate) normal random variable — equivalently, every finite marginal $(X_t)_{t\in T_0}$ is a multivariate Gaussian vector. A process is mean zero if $EX_t = 0$ for every $t$ .

For a mean zero process, the increments $d(t,s) := \lVert X_t - X_s\rVert_{L^2} = (E(X_t - X_s)^2)^{1/2}$ always define a (pseudo)metric on $T$ — the canonical metric — turning the otherwise unstructured index set into a metric space. For a metric space $(T,d)$ and $\varepsilon

0 $, the **covering number**$ N(T,d,\varepsilon) $is the smallest cardinality of a finite subset$ N\subseteq T $such that every point of$ T $is within$ \varepsilon $of some point of$ N $(an$ \varepsilon $-net);$ N(T,d,\varepsilon) := \infty$ if no finite net exists.

Because $T$ need not be countable, $\sup_{t\in T} X_t(\omega)$ need not be a measurable function of $\omega$ . Following the book's own convention, every quantity built from this supremum — $E\sup_{t\in T}X_t$ and $P\{\sup_{t\in T}X_t\ge\tau\}$ — is instead defined through the process's finite-dimensional marginals: as the supremum, over finite nonempty $T_0\subseteq T$ , of $E\max_{t\in T_0}X_t$ (respectively $P\{\max_{t\in T_0}X_t\ge\tau\}$ ). This sidesteps the measurability question entirely, at the cost of the quantity possibly being $+\infty$ .

Formalization targets

Slepian's inequality (Theorem 7.2.1, goal)

Let $(X_t)_{t\in T}$ and $(Y_t)_{t\in T}$ be mean zero Gaussian processes with $EX_t^2 = EY_t^2$ and $E(X_t-X_s)^2 \le E(Y_t-Y_s)^2$ for all $t,s\in T$ . Then for every $\tau\in\mathbb R$ ,

P\{\sup_{t\in T} X_t \ge \tau\} \le P\{\sup_{t\in T} Y_t \ge \tau\},

and consequently $E\sup_{t\in T} X_t \le E\sup_{t\in T} Y_t$ .

Sudakov-Fernique's inequality (Theorem 7.2.11, milestone)

Under only the increment hypothesis $E(X_t-X_s)^2 \le E(Y_t-Y_s)^2$ (no equal-variance hypothesis),

E\sup_{t\in T} X_t \le E\sup_{t\in T} Y_t.

This is the weaker-hypothesis, strictly more applicable form: it is what Sudakov's minoration inequality and the sharp Gaussian random matrix bound of Section 7.3 both invoke.

Sudakov's minoration inequality (Theorem 7.4.1, milestone)

Let $(X_t)_{t\in T}$ be a mean zero Gaussian process with canonical metric $d$ . For every $\varepsilon\ge 0$ at which $N(T,d,\varepsilon)=:N$ is finite,

E\sup_{t\in T} X_t \ge c\,\varepsilon\,\sqrt{\log N}

for an absolute constant $c>0$ . This is the weakest, most stable form of the bound: it names no numerical value for $c$ , so it survives any later sharpening of the constant.

Slepian's inequality, finite-dimensional case (Theorem 7.2.9, milestone)

The vector-indexed special case of Theorem 7.2.1 ( $T$ finite), proved first by Gaussian interpolation and then extended to the general index set.

Significance

The results themselves. Slepian's inequality is the founding comparison theorem for Gaussian processes; Sudakov-Fernique's inequality is its practically indispensable generalization, used routinely to bound suprema of Gaussian processes without needing to track variances explicitly. Sudakov's minoration inequality is the first bridge from the probability of a Gaussian process to the metric geometry of its index set, complementing Dudley's upper bound (Chapter 8) and together giving matching bounds — up to a logarithmic factor, and exactly in many cases of interest — on $E\sup_{t\in T}X_t$ purely from the covering numbers of $(T,d)$ . Downstream, this machinery gives the sharp bound $E\lVert A\rVert \le \sqrt m + \sqrt n$ on Gaussian random matrices (Section 7.3), underlies the Gaussian width used throughout convex geometry and compressed sensing (Chapters 9, 11), and bounds the covering numbers of polytopes and other convex sets (Corollary 7.4.4).

Formalizing it. All three inequalities are proved by the book (Gaussian interpolation and integration by parts for Slepian/Sudakov-Fernique; a direct application of Sudakov-Fernique to a well-chosen comparison process for Sudakov's minoration), so this mission's work is formalizing the statements faithfully and precisely — including the finite-marginal convention needed to make $E\sup_{t\in T}X_t$ and $P\{\sup_{t\in T}X_t\ge\tau\}$ meaningful for an uncountable index set without begging the underlying measurability question. The Gaussian interpolation technique itself (Lemmas 7.2.3, 7.2.5, 7.2.7) is not part of this mission's formalization scope; it is the proof method for the milestones and belongs to solvers closing them.

Difficulty

The obvious first idea — bound $E\sup_t X_t$ by controlling each $X_t$ separately, e.g. via a union bound over a net — throws away exactly the structure Slepian-type comparisons exploit: the joint Gaussianity across $t$ , not marginal tail behavior at each fixed $t$ . A union bound needs a net and a modulus of continuity to begin with; Slepian's and Sudakov-Fernique's inequalities need neither — they compare two processes directly through their covariance structure, which is what makes the technique (Gaussian interpolation: continuously deform the covariance of one process into the other's, and track how a smooth, nearly-indicator functional behaves along the path) work with no assumption on $T$ beyond the two hypotheses stated. The genuine difficulty is the smooth-interpolation argument itself — showing that $E f(Z(u))$ is monotone in $u$ for the right choice of test function $f$ — which is exactly the part left as a milestone for solvers to formalize, not sketched here per the mission format's own rule against proof ideas.

Formalization scope

$E\sup_{t\in T}X_t$ (ProcessESup) is valued in EReal, not ℝ: the finite-marginal supremum a real-valued definition would silently default to the junk value $0$ when the set of finite-marginal expectations is unbounded above — exactly the case the book itself records as $E\sup_{t\in T}X_t=\infty$ (Exercise 7.4.2, a non-relatively-compact index set). P\{\sup_{t\in T}X_t\ge\tau\} (ProcessTailProb) stays real-valued, since it is always bounded in $[0,1]$ and so carries no such risk. Both are defined through finite nonempty subsets of $T$ , per the book's own footnote to Section 7.2; no separability, continuity, or countability assumption is placed on $T$ itself.

Gaussianity is Mathlib's ProbabilityTheory.IsGaussianProcess — every finite restriction of the process has a Gaussian law — which is definitionally the book's Definition 7.1.10 ("every finite linear combination is Gaussian"); mean-zero is stated as an explicit hypothesis alongside it. Integrability of every quantity appearing under an expectation is not stated as a separate hypothesis: Fernique's theorem (already in Mathlib for general Gaussian measures) guarantees a Gaussian process has finite moments of every order, exactly as the book takes for granted.

Sudakov's minoration inequality (Theorem 7.4.1) is formalized for the case the book's own proof actually covers — $N(T,d,\varepsilon)$ finite, taken as a hypothesis = (N : ℕ) rather than as a case split inside the conclusion — since the book itself defers the infinite-covering-number case to a separate, unproved exercise (7.4.2). This keeps $T$ fully general (still possibly uncountable) at every fixed $\varepsilon$ where the net is finite, which rules out a trivializing reading of the theorem: nothing here forces $T$ itself to be finite or countable, only the covering number at the scale $\varepsilon$ in play, which is the book's own hypothesis.

Definitions reusable beyond this mission: ProcessESup, ProcessTailProb, CanonicalMetric, and CoveringNumber are exactly the substrate Chapters 8 ("Dudley's Integral Inequality"), 9 ("The Matrix Deviation Inequality"), and 11 ("Dvoretzky-Milman's Theorem") need for Gaussian width and generic chaining; per this series' plan those missions restate them locally (drafts cannot import another draft's definitions), using this chunk's forms as the faithful reference. Contributions closing the Gaussian-interpolation machinery (Lemmas 7.2.3–7.2.8) as a reusable definitions layer, beyond what any one milestone needs, are welcome.

Selected references

Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018. https://www.math.uci.edu/~rvershyn/papers/HDP-book/HDP-book.pdf
D. Slepian, "The one-sided barrier problem for Gaussian noise", Bell System Technical Journal 41 (1962), 463–501.
V. N. Sudakov, "Gaussian random processes and measures of solid angles in Hilbert space", Soviet Mathematics Doklady 12 (1971), 412–415.
X. Fernique, "Regularité des trajectoires des fonctions aléatoires gaussiennes", in École d'Été de Probabilités de Saint-Flour IV-1974, Springer Lecture Notes in Mathematics 480 (1975), 1–96.
M. Talagrand, Upper and Lower Bounds for Stochastic Processes: Modern Methods and Classical Problems, Springer, 2014.

11 thms2 active usersReviewed

Completed

Operations Research Optimization Probability·Captain: mikedeng1

Introduction to Stochastic Programming VII: Convergence Rates for Sample Average ApproximationTextbook

Motivation

Most stochastic programs cannot be solved exactly: the expectation defining the objective is an integral over a continuous or high-dimensional random parameter, and evaluating it exactly is as hard as the optimization itself. The standard remedy is Monte Carlo: draw a sample of size ν from the random parameter, replace the true expectation by the sample average, and solve the resulting finite-dimensional "sample average approximation" (SAA) instead. This only helps if the SAA's optimal value and optimal solution actually converge to the true problem's as ν → ∞, and if that convergence is fast enough to be useful with a sample size one can actually draw and solve. Birge & Louveaux's Chapter 9, §9.5, states the two central asymptotic results that justify this approach for a general (not necessarily linear, not necessarily two-stage) stochastic program: a central limit theorem describing the SAA optimal value's fluctuations around the truth (Theorem 6, after Shapiro [1991]), and an exponential-rate large-deviation bound on how quickly both the SAA value and the SAA solution concentrate near their true counterparts as the sample grows (Theorem 7, after Dai, Chen & Birge [2000]). This mission formalizes both statements.

Setting

Fix a feasible set X ⊆ ℝⁿ of first-stage decisions and an outcome space Ξ carrying a σ-algebra. The book considers the general stochastic program

z* = inf_{x ∈ X} ∫_Ξ g(x,ξ) P(dξ),                                                        (5.1)

with g : ℝⁿ × Ξ → ℝ an abstract integrand — no longer specialized to the two-stage recourse cost Q(x,ξ) of Chapters 3–7, matching the book's own level of generality at this point in §9.5 — and ξ a random element of (Ξ, 𝓑, P). Given an i.i.d. sample ξ₁, ξ₂, … from P, the sample average approximation of size ν is

zν = inf_{x ∈ X} (1/ν) Σᵢ₌₁^ν g(x,ξᵢ) .                                                    (5.2)

Both z* and zν are attained (an optimal solution x* of (5.1); a random optimal solution xν(ω) of (5.2) at each sample outcome ω). The two chapter results describe, in different regimes, how (zν, xν) relates to (z*, x*) as ν → ∞.

Formalized in this mission: X sits in EuclideanSpace ℝ (Fin n); the sample is a sequence ξ : ℕ → Ω → Ξ on an ambient probability space (Ω, P), independent and identically distributed (Mathlib's iIndepFun/IdentDistrib); z*, x*, zν, xν are given as hypotheses that pin them down as the optimal value and an optimal point of (5.1)/(5.2) (a lower bound over X plus attainment at the named point), rather than computed via sInf/sSup of an image set — Real's extended-real infimum returns the junk value 0 on an unbounded-below or empty set, which would silently misstate the theorems if X, g are only assumed as loosely as the book states them.

Formalization targets

Goal — Chapter 9, Theorem 7 (p. 412)

∀ ε>0, ∃ α>0, ∃ β>0,
  (∀ ν>0, P[|zν − z*| ≥ ε] ≤ α·e^{−βν})
  ∧ (x* the unique optimal solution of (5.1) → ∀ ν≥1, P[‖xν − x*‖ ≥ ε] ≤ α·e^{−βν})

under the moment hypothesis: there exist a>0, θ₀>0, η : Ξ → ℝ with |g(x,ξ)| ≤ a·η(ξ) for all x ∈ X, and E[e^{θ·η(ξ)}] < ∞ for every θ ∈ [0,θ₀]. This is the mission's goal because it is a clean, self-contained existential-constants statement — no algorithm to define, unlike most of the chapter's other convergence results — and because, like Chunk 03's Theorem 6(a), the book's own proof cites an external paper (Dai, Chen & Birge [2000], Theorems 3.1–3.2) and gives no in-text derivation: the statement itself, not a derivation from a preceding numbered result of this book, is the mission's content.

Milestone — Chapter 9, Theorem 6 (p. 411)

X compact, g(x,·) measurable ∀x∈X, g Lipschitz in x with an L²(μ) envelope a,
x0 the unique minimizer of x ↦ E g(x) over X
  ⟹ √ν·[zν − E g(x0)] converges in distribution to N(0, Var g(x0))

Included as a milestone (not used in Theorem 7's proof, which the book does not give — see above) because it is the chapter's other general SAA convergence result, standing on the same setup (5.1)–(5.2), and because Mathlib's MeasureTheory.Function.ConvergenceInDistribution (the TendstoInDistribution predicate) plus Probability.Distributions.Gaussian.Real (gaussianReal) and Mathlib's own i.i.d. central limit theorem (ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub) supply exactly the vocabulary needed to state — not prove — a faithful weak-convergence-to-Gaussian conclusion. Chunk 09's BRIEF.md flagged this as a milestone to attempt "only if your workspace has enough of a weak-convergence/CLT toolkit in Mathlib to state it faithfully"; the toolkit is present (verified directly, not assumed from substrate.md, which predates this rev's addition of ConvergenceInDistribution.lean), so it is included.

Significance

Every practical Monte Carlo solution method for stochastic programming — every discretization, every scenario-reduction heuristic, every "solve on a sample and hope" approach used throughout the rest of the book and the wider literature — rests on exactly these two results: that the SAA converges at all (Theorem 6's CLT gives the asymptotic distribution of the error) and that it converges fast enough to bound the error at a finite, computable sample size (Theorem 7's exponential rate). Formalizing them gives Prove2Me a first foothold in convergence-rate theory for stochastic optimization under sampling, a genre distinct from the concentration-of-measure results already reachable via Mathlib's sub-Gaussian machinery (Probability/Moments/SubGaussian.lean): sub-Gaussian concentration bounds a fixed-size sample's deviation from its own mean, not the rate-in-ν convergence of a nested sequence of optimization problems' values and solutions to a limiting problem's — the object Theorem 7 is actually about.

Difficulty

Theorem 6 needs a functional/uniform argument over the whole feasible set X (not the plain i.i.d. CLT at the single point x0) to control the interaction between sampling noise and the optimization over x; the book states it without proof, citing Shapiro [1991]. Theorem 7's constants α, β are produced by a large-deviation argument specific to the exponential-moment condition, again cited rather than derived in the book. Both are left as sorry; the value of this mission is the faithful statement, matching the difficulty pattern already established for Chunk 03's Theorem 6(a) (a result the book itself only cites).

Formalization scope

Existential constants left abstract, never sharpened or weakened. Theorem 7's α, β are ∃-bound exactly as the book leaves them (trap 8 of reference/FAITHFULNESS_TRAPS.md: the existentials sit outside every quantifier they must be uniform over — in particular outside the ∀ ν). No closed form for α, β in terms of a, θ0, ε is invented.
The book's own typo is corrected, and the correction is flagged. The printed (5.8) reads P[E[zν − z*)] ≥ ε] ≤ αe^{−βν} — an unmatched parenthesis and a stray E[·] around a quantity that is already deterministic. milestones.yaml/MODERATION_NOTES.md quote the typo verbatim; the Lean and natural_language_statement use the unambiguous P[|zν − z*| ≥ ε] the surrounding prose (and every other occurrence of this quantity in the section) plainly intends.
g is left fully abstract, not specialized to the two-stage recourse cost Q(x,ξ) of Chunks 03–07, matching §9.5's own generality and keeping this mission independent of every other chunk's namespace (no cross-chunk import, per missions/README.md's "Prior art" column for this chunk: "none expected").
z*, x*, zν, xν are hypothesis-characterized, not sInf/sSup-defined, to avoid the real extended-value junk-value trap (trap 5) discussed under Setting above.
Measurability of zν, xν is an added hypothesis (hzSAA_meas/hxSAA_meas/hzSAA_meas in Theorem 6), not derivable from the other hypotheses since g is abstract; the book is silent on this technical point, standard for an applied convergence theorem, but Lean's P {ω | …} needs it for the displayed probability to be the actual measure of the event rather than an outer-measure value on a possibly non-measurable set.
Convergence in distribution (Theorem 6) is formalized via Mathlib's TendstoInDistribution, with the limiting Gaussian supplied as an explicit random variable Y on a separate probability space with HasLaw Y (gaussianReal 0 σ²) P' — the same pattern Mathlib's own CLT (tendstoInDistribution_inv_sqrt_mul_sum_sub) uses for its own conclusion.
Trivialization risk (this chapter's own, beyond paper.md's book-wide list item 5). A formalization that quantifies α, β universally, or with an invented closed form, would assert something the book's proof (cited, not given) does not establish; a formalization of Theorem 7 that used a computable sInf-defined zν on a set that is not shown bounded below would let the conclusion hold vacuously via the junk value 0, independent of the genuine large-deviation content — both are excluded by the choices above.

Selected references

Birge, J.R., Louveaux, F. Introduction to Stochastic Programming, 2nd ed., Springer 2011, Chapter 9, §9.5 (pp. 409–412).
Shapiro, A. "Asymptotic properties of statistical estimators in stochastic programming." Annals of Statistics 19 (1991), 1463–1466 — proof of Theorem 6 (their Theorem 3.3).
Dai, L., Chen, C.-H., Birge, J.R. "Convergence properties of two-stage stochastic programming." Journal of Optimization Theory and Applications 106 (2000), 489–509 — proof of Theorem 7 (their Theorems 3.1–3.2).
King, A.J., Rockafellar, R.T. "Asymptotic theory for solutions in statistical estimation and stochastic programming." Mathematics of Operations Research 18 (1993), 148–162 — the general theory of §9.5's opening (Theorem 5), the chapter's third general result, not formalized here (see STATUS.md for why it is out of scope).

2 thms2 active usersReviewed

Completed

Machine Learning Probability Random Matrix Theory·Captain: mikedeng1

High-Dimensional Probability II: Concentration Inequalities for Sums of Independent Random VariablesTextbook

Motivation

The central limit theorem tells us that a normalized sum of independent random variables converges in distribution to a Gaussian. For applications — bounding the failure probability of a randomized algorithm, controlling the error of a Monte Carlo estimator, proving a generalization bound in learning theory — a limiting distribution is not enough: what is needed is a single, explicit, non-asymptotic inequality that holds for every fixed sample size $N$ , not merely as $N \to \infty$ . Hoeffding's inequality (Wassily Hoeffding, 1963) and Bernstein's inequality (Sergei Bernstein, 1920s–1940s, in the form used here due to Vadim Bennett and later authors) are the two archetypal answers: both give an explicit Gaussian-type tail bound for a weighted sum of independent random variables, valid for every $N$ , with all constants made explicit. They are the workhorses behind concentration of measure, high-dimensional statistics, and the non-asymptotic analysis of randomized algorithms; a textbook trying to reach the Johnson–Lindenstrauss lemma, random matrix norms, or the restricted isometry property has to pass through this chapter first, because every one of those results is itself an application of a weighted-sum concentration inequality to a specific choice of random variables.

The central limit theorem's own error term is the obstruction that direct concentration inequalities are built to avoid: the Berry–Esseen theorem (Andrew C. Berry, 1941; Carl-Gustav Esseen, 1942) bounds the normal approximation's error at order $1/\sqrt N$ , which is too slow to recover a genuinely exponential tail bound for finite $N$ . Hoeffding's and Bernstein's inequalities are proved instead by a direct argument — bounding the moment generating function of the sum and optimizing a Markov/Chernoff exponential tilt — that never invokes the central limit theorem or its error term at all.

The sub-gaussian and sub-exponential norms

Fix a probability space $(\Omega, \mathcal F, P)$ . For a real random variable $X$ on $(\Omega, \mathcal F, P)$ , define its sub-gaussian norm

\|X\|_{\psi_2} := \inf\{t > 0 : \mathbb E \exp(X^2/t^2) \text{ is finite and } \le 2\}

and its sub-exponential norm

\|X\|_{\psi_1} := \inf\{t > 0 : \mathbb E \exp(|X|/t) \text{ is finite and } \le 2\}.

In both definitions, the requirement that the exponential moment be finite (i.e. that the moment-generating integrand be integrable), and not merely satisfy " $\le 2$ " as a bare inequality, is essential: without it a moment that is genuinely infinite for a given $t$ would vacuously count as " $\le 2$ " under the Bochner integral's convention that a non-integrable function integrates to $0$ , and every random variable — however heavy-tailed — would trivially have norm $0$ . $X$ is called sub-gaussian (respectively sub-exponential) when this infimum is over a nonempty set, i.e. when some finite $t$ makes the moment finite and at most $2$ . These are genuine norms (up to the identification of almost-surely-equal random variables) on the vector space of random variables for which they are finite, and they are the natural non-asymptotic yardsticks for tail heaviness: $\|X\|_{\psi_2} < \infty$ characterizes a Gaussian-type tail $P\{|X| \ge t\} \le 2\exp(-ct^2/\|X\|_{\psi_2}^2)$ , while $\|X\|_{\psi_1} < \infty$ characterizes an exponential-type tail $P\{|X| \ge t\} \le 2\exp(-ct/\|X\|_{\psi_1})$ . Every bounded random variable — in particular every Bernoulli or Rademacher (symmetric Bernoulli) random variable — is sub-gaussian, and the square of a sub-gaussian random variable is sub-exponential; a genuinely sub-exponential (not sub-gaussian) example is the squared coordinate $g_i^2$ of a standard Gaussian vector, or the exponential distribution itself.

Formalization targets

Goal — Theorem 2.8.2 (Bernstein's inequality, weighted sum). Let $X_1, \dots, X_N$ be independent, mean-zero, sub-exponential random variables on $(\Omega, \mathcal F, P)$ , and let $a = (a_1, \dots, a_N) \in \mathbb R^N$ . Then, for every $t \ge 0$ ,

P\Bigl\{\Bigl|\sum_{i=1}^N a_i X_i\Bigr| \ge t\Bigr\} \;\le\; 2\exp\left[-c\min\left(\frac{t^2}{K^2\|a\|_2^2}, \frac{t}{K\|a\|_\infty}\right)\right],

where $K = \max_i \|X_i\|_{\psi_1}$ and $c > 0$ is an absolute constant that does not depend on $N$ , the $X_i$ , $a$ , or $t$ .

The goal is deliberately the weighted and sub-exponential form, the weakest of the chapter's results that is still stable under the improvements a solver might find: it neither fixes $a_i \equiv 1$ (the unweighted Theorem 2.8.1, a special case) nor restricts to the lighter sub-gaussian tail (Theorem 2.6.3, which follows from a strictly stronger hypothesis). Both weaker theorems, plus Hoeffding's and Chernoff's inequalities, are included as milestones because Bernstein's own proof is built directly from them.

Significance

The result itself. Bernstein's inequality is the two-tail-regime concentration bound: a sub-gaussian tail $\exp(-ct^2/(K\|a\|_2)^2)$ near the mean, transitioning to a heavier sub-exponential tail $\exp(-ct/(K\|a\|_\infty))$ far from it, exactly the behavior one should expect from a mixture of light-tailed terms with one heavy-tailed outlier. It underlies the concentration of quadratic forms (Chapter 6's Hanson–Wright inequality controls $\sum \varepsilon_i \varepsilon_j$ -type terms, which are themselves products of sub-gaussians and hence sub-exponential by Lemma 2.7.7), and it is the standard tool for bounding empirical-process suprema whose summands are not bounded but merely light-tailed.

Formalizing it. No formalization of Bernstein's inequality — in either the weighted or unweighted, or sub-gaussian or sub-exponential form — exists yet on Prove2Me (GET /theorems?q=Bernstein and q=sub-exponential return no relevant hits, checked 2026-09-17). What this mission produces is not just the statement but the machinery underneath it: a working Orlicz-norm treatment of $\psi_1$ and $\psi_2$ that a later mission (the Hanson–Wright inequality, or any future chapter that needs sub-exponential concentration) can build on directly.

Difficulty

The obvious first idea — squaring both sides and applying Chebyshev, as one does to prove the weak law of large numbers — gives only a polynomial tail bound decaying like $1/N$ , far too weak to be useful (this is exactly the point made by the chapter's opening discussion of the coin-tossing example, comparing the linear decay from Chebyshev against the target exponential decay). The central limit theorem promises the right shape of tail asymptotically but, per Berry–Esseen, with an error of order $1/\sqrt N$ that swamps any exponential gain for large deviations — the CLT approximation is simply not valid in the tail regime the inequality needs. The actual argument instead controls the moment generating function of the full sum directly and optimizes an exponential (Chernoff) tilt; this is why the sub-gaussian and sub-exponential norms — MGF-control objects, not moment or tail objects per se — are the right technical vehicle, even though Proposition 2.5.2 and 2.7.1 show all these characterizations are equivalent up to constants. The min of two terms in Bernstein's exponent is not an artifact of a loose proof: it reflects a genuinely two-regime tail (Gaussian near the mean, exponential in the far tail), and collapsing it to a single term in either direction would either be false (dropping the exponential term) or needlessly weak (dropping the Gaussian term, which is what a naive union bound over the worst single term would give).

Formalization scope

Random variables are ℝ-valued functions on an explicit probability space (Ω, mΩ, P) (Ω : Type, MeasurableSpace Ω, P : Measure Ω, [IsProbabilityMeasure P]), matching the book's setup throughout. Independence is Mathlib's ProbabilityTheory.iIndepFun, and tail probabilities are stated with P.real, Mathlib's ℝ-valued measure evaluation, which corresponds directly to the book's $P\{\cdot\}$ .

Both Orlicz norms are defined locally, as genuine infima matching Definitions 2.5.6 and 2.7.5 verbatim (subgaussianNorm, subexponentialNorm, each sInf {t > 0 : Integrable (fun ω => E[...]) P ∧ E[...] ≤ 2}), rather than reused from Mathlib's HasSubgaussianMGF (Mathlib.Probability.Moments.SubGaussian). The Integrable conjunct is not optional dressing: Mathlib's Bochner integral of a non-integrable function is 0 by convention, so a bare E[...] ≤ 2 (without asserting integrability) would be satisfied by every t for which the moment is actually infinite, collapsing the sub-gaussian norm of a standard Gaussian (and, symmetrically, the sub-exponential norm of any heavy-tailed variable) to 0 — a trivializing formalization the mission was moderated to rule out. The same Integrable conjunct appears in every moment hypothesis (general_hoeffding, bernstein_unweighted, bernstein_weighted): ∃ s > 0, Integrable (...) P ∧ ∫ ... ≤ 2, so that the hypothesis is not satisfied vacuously by non-integrable exponential moments either. HasSubgaussianMGF bounds the moment generating function directly with a variance-proxy parameter $\sigma^2$ (E exp(tX) ≤ exp(c t²/2)), which is a different object definitionally from the Orlicz $\psi_2$ norm — equivalent up to a constant factor by the book's own Proposition 2.5.2, but not interchangeable without restating that equivalence — and Mathlib has no sub-exponential analogue at all. Since the goal theorem and two of its milestones need the sub-exponential norm, one consistent convention (the book's own Orlicz norms) is used for both $\psi_1$ and $\psi_2$ throughout the mission, rather than mixing Mathlib's MGF-based sub-gaussian convention with a locally defined sub-exponential one.

Every occurrence of the book's " $c$ is an absolute constant" is formalized as a genuine existential quantifier fixed before the random variables, the vector a, and t are introduced: ∃ c : ℝ, 0 < c ∧ ∀ ..., P.real {...} ≤ 2 * Real.exp (-(c * ...)). No numeral is substituted for c anywhere; a solver's proof may use any positive constant it can establish, exactly mirroring the book's own non-constructive existence claims. The trivializing formalization this rules out is fixing c to a specific small numeral (which would be a strictly stronger, easier, and unfaithful claim) or, in the other direction, weakening the statement by allowing c to depend on N, the $X_i$ , a, or t (which would make the theorem vacuous, since any such bound trivially holds for a small enough $c$ depending on the instance).

Chernoff's inequality (Theorem 2.3.1) needs no Orlicz norm — Bernoulli parameters $p_i$ are given directly via P.real {X i = 1} = p i ∧ P.real {X i = 0} = 1 - p i, and the conclusion uses Real.rpow (^ on ℝ → ℝ → ℝ) for the real exponent $t$ in $(e\mu/t)^t$ . Hoeffding's inequality for symmetric Bernoulli variables (Theorem 2.2.2) is likewise self-contained, needing only the two-point probability hypothesis defining the Rademacher distribution.

Selected references

W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58(301), 1963. https://doi.org/10.2307/2282952
S. Bernstein, The Theory of Probabilities, Gastehizdat Publishing House, Moscow, 1946 (Russian; the inequality is due to Bernstein's earlier 1920s–1930s work, this textbook states the modern sub-exponential form following later expositions).
A. C. Berry, The Accuracy of the Gaussian Approximation to the Sum of Independent Variates, Transactions of the American Mathematical Society 49(1), 1941. https://doi.org/10.2307/1990053
C.-G. Esseen, On the Liapunoff Limit of Error in the Theory of Probability, Arkiv för Matematik, Astronomi och Fysik A28, 1942.
R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 2. https://doi.org/10.1017/9781108231596

7 thms2 active usersReviewed

Completed

Machine Learning Probability Random Matrix Theory·Captain: mikedeng1

High-Dimensional Probability I: Approximate Carathéodory's TheoremTextbook

Motivation

Many arguments in high-dimensional geometry, statistics and computer science need to approximate a point of a convex set by an average of a handful of extreme points, rather than represent it exactly. The classical Carathéodory theorem (1907) answers the exact question: every point of the convex hull of a set $T \subseteq \mathbb{R}^n$ is a convex combination of at most $n+1$ points of $T$ . That bound is tight and grows with the dimension $n$ , which makes it useless whenever $n$ is large — exactly the regime of interest in high-dimensional probability.

B. Maurey's empirical method — an unpublished 1980–81 result reported by G. Pisier, "Remarques sur un résultat non publié de B. Maurey," Séminaire d'Analyse Fonctionnelle 1980–1981 — and later applied by B. Carl to bound covering numbers of operators between Banach spaces (Inequalities of Bernstein-Jackson-type and the degree of compactness of operators in Banach spaces, Ann. Inst. Fourier 35(3), 1985, 79–118), replaces the exact question with an approximate one and removes the dimension dependence entirely: to approximate $x$ to accuracy $\varepsilon$ , the number of points needed depends only on $\varepsilon$ , never on $n$ . Vershynin's High-Dimensional Probability opens with this result as its "Appetizer," using it to illustrate the book's central theme — that randomness is a tool for constructing deterministic combinatorial objects — before any probabilistic machinery has been introduced.

Setting

A convex combination of finitely many points $z_1, \dots, z_m \in \mathbb{R}^n$ is a sum $\sum_{i=1}^m \lambda_i z_i$ with $\lambda_i \ge 0$ and $\sum_i \lambda_i = 1$ . The convex hull $\operatorname{conv}(T)$ of a set $T \subseteq \mathbb{R}^n$ is the set of all convex combinations of all finite collections of points of $T$ . The diameter of $T$ is $\operatorname{diam}(T) = \sup\{\|s-t\|_2 : s, t \in T\}$ , the Euclidean norm throughout.

The classical Carathéodory theorem states that every $x \in \operatorname{conv}(T)$ is a convex combination of at most $n+1$ points of $T$ — with $n+1$ generally unavoidable, attained by a simplex. The question this mission answers is different: given that we are willing to approximate $x$ rather than represent it exactly, and willing to use only combinations with equal coefficients $1/k$ (an average of $k$ points, with repetition allowed), how large must $k$ be as a function of the desired accuracy?

Formalization targets

Goal — Theorem 0.0.2, Approximate Carathéodory's theorem

\text{diam}(T) \le 1,\ x \in \operatorname{conv}(T),\ k \in \mathbb{Z}_{>0} \ \Longrightarrow\ \exists\, x_1,\dots,x_k \in T:\quad \left\| x - \frac{1}{k}\sum_{j=1}^{k} x_j \right\|_2 \le \frac{1}{\sqrt{k}}.

The quantifiers are exactly this order: for every bounded $T$ , every point of its convex hull, and every target $k$ , such an averaging set exists. This is the weakest stable statement carrying the theorem's content — the number of points $k$ does not depend on the dimension $n$ , and the coefficients are forced to be uniform — and it is the form the corollary below invokes directly.

Milestone — Corollary 0.0.4, Covering polytopes by balls

P = \operatorname{conv}(T),\ |T| = N,\ \operatorname{diam}(P) \le 1,\ \varepsilon > 0 \ \Longrightarrow\ \exists\, C,\ |C| \le N^{\lceil 1/\varepsilon^2 \rceil}:\quad P \subseteq \bigcup_{c \in C} \overline{B}(c, \varepsilon).

This is a direct application of the goal to computational geometry's covering problem: how many balls of radius $\varepsilon$ are needed to cover a polytope, and where should they be centered.

Significance

The result itself. The approximate Carathéodory theorem is the prototype of a dimension-free approximation result: whenever a set is bounded, a fixed number of points (depending only on the target accuracy, not the ambient dimension) suffices to approximate any point of its convex hull. This is what makes possible dimension-independent covering-number bounds such as Corollary 0.0.4, which in turn are the starting point for the book's later treatment of entropy, packing and generic chaining (Chapters 4, 7–8). The technique generalizes far beyond $\mathbb{R}^n$ : it underlies covering-number bounds for operators between Banach spaces (Carl's original application) and is a recurring device in learning theory for bounding the size of an $\varepsilon$ -net of a hypothesis class.

Formalizing it. Both results are elementary and already fully proved in the literature; no open mathematical content remains. What this mission contributes is a machine-checked, faithful Lean statement of Maurey's construction and its corollary, phrased over Mathlib's existing convex-hull and metric-diameter machinery, so that later missions in this series (concentration inequalities, Johnson–Lindenstrauss, chaining) can build on a verified base case of "probability constructs a deterministic covering," and so that the empirical method itself becomes a reusable, linked component on the platform. The proof of the goal (via the probabilistic argument sketched by the book: interpret a convex combination as a probability distribution, average $k$ i.i.d. samples, and bound the variance) is left open for solvers.

Difficulty

The identity that makes the proof work — averaging $k$ independent copies of a random vector concentrates around its mean at rate $1/\sqrt{k}$ in mean-square — is a two-line computation once the convex combination is reinterpreted probabilistically. The step that is easy to miss is this reinterpretation itself: nothing in the statement mentions probability, so the "obvious" attack of manipulating the convex-combination weights directly, or trying to construct $x_1,\dots,x_k$ by some explicit combinatorial recipe, does not see a path to a bound independent of $n$ . The probabilistic argument produces the points non-constructively, via an averaging/existence argument (the expected squared distance is small, so some realization achieves it) rather than an explicit formula — a solver has to introduce a probability space and a random vector that does not appear anywhere in the formal statement to be proved.

Formalization scope

Both results are stated over EuclideanSpace ℝ (Fin n) for an explicit dimension n : ℕ, so ‖·‖ is the Euclidean norm and Mathlib's Metric.diam is used directly for $\operatorname{diam}(T) = \sup\{\|s-t\|_2\}$ . The convex hull is Mathlib's convexHull ℝ T; by Mathlib's convexHull_eq, this already coincides with the book's own definition of a convex combination of finitely many points of $T$ , so no bespoke convex-combination definition is introduced — this mission needs no supporting definitions of its own. In the corollary, "a polytope $P$ with $N$ vertices" is formalized, following the book's own proof, as $P = \operatorname{conv}(T)$ for a finite vertex set $T$ with $\#T = N$ , rather than via a separate Polytope structure (which Mathlib does not provide and the book's argument does not need). The covering bound $N^{\lceil 1/\varepsilon^2\rceil}$ is an exponent, not a product with $N$ — matching the book's own proof, which counts the $N^k$ ordered $k$ -tuples of vertices with repetition, $k := \lceil 1/\varepsilon^2\rceil$ ; the typeset " $N\lceil 1/\varepsilon^2\rceil$ " in the corollary statement is the same juxtaposition-as-exponent notation the proof uses for " $N^k$ " one line earlier.

A trivializing formalization is ruled out explicitly: the goal must hold for every integer $k > 0$ and every $x \in \operatorname{conv}(T)$ , not merely some convenient choice — e.g. $k = 1$ together with $x \in T$ trivially satisfies the inequality but proves nothing about the theorem's actual content, that a fixed, dimension-independent $k$ works uniformly over all points of the hull. The formal statement quantifies $T$ , then $x$ , then $k$ , and only then asserts existence of the $x_1,\dots,x_k$ , exactly in that order.

Classical Carathéodory (Theorem 0.0.1, stated for context in the source but not used by either formalized result's proof) is not drafted here: Mathlib already proves the corresponding statement via affine independence (Caratheodory.eq_pos_convex_span_of_mem_convexHull, Analysis/Convex/Caratheodory.lean), from which the book's " $n+1$ points" bound follows via AffineIndependent.card_le_finrank_succ. It is not added as a kind: reference milestone because no corresponding theorem is yet published on the Prove2Me platform to point at (checked 2026-09-17: GET /theorems?q=Caratheodory returns only unrelated tropical-convexity results), and re-drafting existing Mathlib content as a new platform theorem would duplicate rather than reuse it.

Selected references

R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, DOI 10.1017/9781108231596, Appetizer (pp. 1–5).
G. Pisier, "Remarques sur un résultat non publié de B. Maurey," Séminaire d'Analyse Fonctionnelle (Maurey–Schwartz), 1980–1981, exposé no. 5. numdam.org/item/SAF_1980-1981____A5_0
B. Carl, "Inequalities of Bernstein-Jackson-type and the degree of compactness of operators in Banach spaces," Annales de l'Institut Fourier, 35(3), 1985, 79–118. numdam.org/item/AIF_1985__35_3_79_0

2 thms2 active usersReviewed