Statistics · Prove2Me

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

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

Operations Research Probability Stochastic Systems·Captain: mikedeng1

Stochastic Orders I: The Usual Stochastic Order and Its Coupling CharacterizationTextbook

Comparing random outcomes without comparing numbers

Operations research and applied probability are full of questions of the shape "is X riskier, larger, or later than Y?" when X and Y are random: two queueing disciplines' waiting times, two inventory policies' shortfall, two insurance portfolios' claim size. Comparing their means answers a weaker question than the modeler usually wants, since two distributions can share a mean while one is uniformly the "worse" one to face. Shaked and Shanthikumar's Stochastic Orders (Springer, 2007) is the standard reference for the family of orders built to make "X is stochastically no larger than Y" precise, and this mission formalizes the foundational member of that family: the usual stochastic order, together with its central structural theorem.

The usual stochastic order

Let $X$ be a real-valued random variable on a probability space $(\Omega,\mu)$ , and let $Y$ be a real-valued random variable on a (possibly different) probability space $(\Omega',\nu)$ . $X$ is smaller than $Y$ in the usual stochastic order, written $X \le_{st} Y$ , if

P\{X > x\} \le P\{Y > x\} \quad \text{for every } x \in (-\infty,\infty).

Equivalently, $P\{X \le x\} \ge P\{Y \le x\}$ for every $x$ : $Y$ 's cumulative distribution function never exceeds $X$ 's. Two features of the definition matter for everything that follows. First, it is a comparison of distributions, not of jointly defined variables — $X$ and $Y$ need not live on the same probability space, and the order depends only on their laws. Second, the inequality must hold for every threshold $x$ simultaneously; it is not a comparison of two summary statistics such as means or medians, and a distribution can fail $X \le_{st} Y$ even while $E[X] \le E[Y]$ .

A closely related order compares residual lifetimes rather than raw tail probabilities. $X$ is smaller than $Y$ in the hazard rate order, written $X \le_{hr} Y$ , if the survival functions $\bar F(x) = P\{X>x\}$ , $\bar G(x) = P\{Y>x\}$ satisfy $\bar F(x)\bar G(y) \ge \bar F(y)\bar G(x)$ for all $x \le y$ — the general, density-free form of the condition that for absolutely continuous distributions reduces to a pointwise comparison of hazard rates $r(t) = f(t)/\bar F(t)$ . It is one of several stronger orders (alongside the likelihood ratio order) that the book shows all imply $\le_{st}$ , and it is the mission's second definition.

Formalization targets

Goal: the coupling characterization (Theorem 1.A.1)

X \le_{st} Y \iff \exists\,(\Omega'',\rho),\ \hat X,\hat Y : \Omega'' \to \mathbb{R} \text{ with } \hat X =_{st} X,\ \hat Y =_{st} Y,\ \text{and } P\{\hat X \le \hat Y\} = 1.

This is the order's Strassen-type coupling theorem: $X \le_{st} Y$ holds exactly when copies of $X$ and $Y$ can be realized on one common probability space so that, almost surely, the copy of $X$ never exceeds the copy of $Y$ . It is the weakest possible statement with this shape (existence of some coupling on some space, not a canonical one), and it is the archetype every later chapter's own coupling theorem — for the hazard rate order, the convex order (via a martingale coupling), the multivariate orders — restates for its own comparison.

Supporting milestones

Theorem 1.A.2, the same characterization restated via a common random source: $X \le_{st} Y$ iff there is a random variable $Z$ and functions $\psi_1 \le \psi_2$ with $X =_{st} \psi_1(Z)$ and $Y =_{st} \psi_2(Z)$ .
Theorem 1.A.3(a), closure under monotone transformations: $X \le_{st} Y$ and $g$ increasing gives $g(X) \le_{st} g(Y)$ (reversed for $g$ decreasing).
Theorem 1.A.3(b), closure under increasing functions of independent families and, as its corollary, under convolution: independent $X_i \le_{st} Y_i$ and $\psi$ increasing gives $\psi(X_1,\dots,X_m) \le_{st} \psi(Y_1,\dots,Y_m)$ , in particular $\sum_i X_i \le_{st} \sum_i Y_i$ .
Theorem 1.B.1, the first link of the book's implication chain: $X \le_{hr} Y \implies X \le_{st} Y$ .

Significance

The usual stochastic order is the weakest and most widely used of the book's orders, and the coupling theorem is the tool that makes it tractable: comparing tail probabilities for every threshold is an infinite family of inequalities, while exhibiting one coupling on one space settles the comparison in a single stroke. This is the technique behind, among many applications in the book and the wider literature, comparing waiting times across queueing disciplines, bounding the effect of parameter uncertainty on a risk measure, and proving monotonicity results for Markov chains by coupling their sample paths. The closure properties (Theorem 1.A.3) are what let such comparisons survive composition with a monotone payoff function or a sum of independent components — exactly the operations a queueing or inventory model performs on its primitives.

Formalizing this theorem establishes, in one place, both the statement and the exact shape of its existential witness (a genuine ∃ over a probability space and two identically distributed random variables, not merely two abstractly-known-to-exist objects), which is the piece every later chapter's own coupling theorem in this series needs to get right independently. No proof is attempted in this mission; the book's own three-line construction ( $\hat X = F^{-1}(U)$ , $\hat Y = G^{-1}(U)$ for a uniform $U$ ) is a natural target for a future proof-bearing pass.

Difficulty

The definitional trap is the "for all $x$ " in $\le_{st}$ : it is tempting to shortcut it into a comparison of one summary statistic (a mean, an essential supremum, a specific quantile), which is uniformly weaker and would make Theorem 1.A.1 either false or a different, easier theorem. The coupling theorem itself has a second trap in its existential structure: the common probability space $(\Omega'',\rho)$ must be genuinely quantified — fixed neither to $\Omega$ nor $\Omega'$ in advance — and " $\hat X =_{st} X$ " is equality of the two random variables' laws, not almost-sure equality of $\hat X$ and $X$ themselves (they typically do not share a domain before the construction). Theorem 1.A.3(b)'s general statement, for an arbitrary increasing $\psi:\mathbb{R}^m \to \mathbb{R}$ on independent families, is easy to understate as only its convolution corollary; the book gives both, and the general statement is the one with the actual content (the sum is recovered by taking $\psi$ to be the coordinate sum, itself increasing).

Formalization scope

Random variables are represented as measurable functions into $\mathbb{R}$ from arbitrary measurable spaces, and "equality in law" is Mathlib's native ProbabilityTheory.IdentDistrib, which is defined for two (possibly different) probability spaces and requires almost-everywhere measurability rather than fixing an ambient space in advance — matching the book's own treatment of $X \le_{st} Y$ as a comparison between distributions. UsualOrder μ ν X Y and HazardRateOrder μ ν X Y both take $X:\Omega\to\mathbb{R}$ on $(\Omega,\mu)$ and $Y:\Omega'\to\mathbb{R}$ on a separate $(\Omega',\nu)$ , so no theorem here can be trivialized by silently forcing $X$ and $Y$ onto one shared space. HazardRateOrder is stated via the survival-function cross-product inequality (Eq. 1.B.4), the form that needs no absolute-continuity hypothesis, rather than via a derivative-based hazard rate, so it applies to the same general random variables as UsualOrder without an extra regularity hypothesis the book itself does not require at this level of generality. Independence in Theorem 1.A.3(b) is Mathlib's ProbabilityTheory.iIndepFun; the random variable $Z$ of Theorem 1.A.2 is left valued in an arbitrary measurable space, matching the book's unrestricted statement, rather than narrowed to $\mathbb{R}$ -valued for convenience. A trivializing formalization is ruled out explicitly: $\le_{st}$ is not formalized as a comparison of means, medians, or any single moment, and the coupling theorems' ∃ is a genuine existential over a probability space, not a hypothesis smuggling in the witness's existence.

This mission draws on no platform prior art (repeated searches for "stochastic order", "coupling", "Strassen" and "identically distributed" turned up nothing on-topic as of 2026-09-18); it is the first mission in a nine-chapter series covering the whole book, and its own definitions are not imported by later chapters — each restates locally what it needs, per the series' own convention that draft items cannot import another draft's definitions. Reusable beyond this mission: the UsualOrder/HazardRateOrder shape (parametrizing over two separate probability spaces) is the pattern every later chapter's own order definition follows.

Selected references

M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

7 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 Random Matrix Theory·Captain: mikedeng1

High-Dimensional Statistics V: Thresholding-Based Covariance EstimationTextbook

Motivation

Estimating a $d\times d$ covariance matrix $\Sigma$ from $n$ samples is a canonical high-dimensional problem: the natural estimator, the sample covariance $\hat\Sigma$ , is consistent in operator norm only when $n\gtrsim d$ , which fails outright in the regime $d\gg n$ common to modern applications. When $\Sigma$ is additionally known to be sparse — few nonzero entries per row — a simple fix restores consistency even when $d\gg n$ : threshold every entry of $\hat\Sigma$ below a data-dependent level to zero. This mission formalizes the matrix concentration machinery behind that fix and the resulting guarantee, following Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 6.

Setting

For a random matrix $Q$ , the matrix variance is $\mathrm{var}(Q):=\mathbb E[Q^2]-(\mathbb E[Q])^2$ , and the Loewner order $A\preceq B$ on symmetric matrices means $B-A$ is positive semidefinite. A zero-mean symmetric random matrix $Q$ satisfies Bernstein's condition (Definition 6.10) with parameter $b>0$ if $\mathbb E[Q^j]\preceq\tfrac12 j!\,b^{j-2}\mathrm{var}(Q)$ for $j=3,4,\dots$ — the matrix analogue of the scalar Bernstein condition of Chapter 2. The operator (spectral) norm $|\!|\!|M|\!|\!|_2$ is $M$ 's largest singular value.

Given a threshold $\lambda>0$ , the hard-thresholding operator is $T_\lambda(u):=u\cdot \mathbb 1[|u|>\lambda]$ , extended entrywise to matrices (Eq. (6.52)). A covariance matrix $\Sigma$ 's sparsity pattern is captured by its adjacency matrix $A_{j\ell}:=\mathbb 1[\Sigma_{j\ell}\neq0]$ (p. 181); $|\!|\!|A|\!|\!|_2\le d$ always, with equality only when $\Sigma$ has no zero entries, and $|\!|\!|A|\!|\!|_2\le s$ whenever $\Sigma$ has at most $s$ nonzero entries per row.

Formalization targets

Goal — Theorem 6.23 (thresholding-based covariance estimation)

Let $\{x_i\}_{i=1}^n$ be i.i.d. zero-mean random vectors with covariance $\Sigma$ , each coordinate sub-Gaussian with parameter at most $\sigma$ . If $n>\log d$ , then for any $\delta>0$ , the thresholded sample covariance $T_{\lambda_n}(\hat\Sigma)$ with $\lambda_n/\sigma^2 = 8\sqrt{\log d/n}+\delta$ satisfies

\mathbb P\big[\,|\!|\!|T_{\lambda_n}(\hat\Sigma)-\Sigma|\!|\!|_2 \ge 2|\!|\!|A|\!|\!|_2\lambda_n\,\big] \;\le\; 8e^{-\frac{n}{16}\min\{\delta,\delta^2\}}.

The error scales with the graph sparsity $|\!|\!|A|\!|\!|_2$ , not with $d$ directly — the whole point of thresholding when the ambient dimension is much larger than the sample size.

Milestone — Theorem 6.17 (the matrix Bernstein bound)

For independent, zero-mean, symmetric random matrices $\{Q_i\}$ satisfying Bernstein's condition with parameter $b$ ,

\mathbb P\Big[\frac1n\Big|\!\Big|\!\Big|\sum_{i=1}^n Q_i\Big|\!\Big|\!\Big|_2 \ge \delta\Big] \;\le\; 2\,\mathrm{rank}\Big(\sum_{i=1}^n\mathrm{var}(Q_i)\Big)\exp\Big(-\frac{n\delta^2}{2(\sigma^2+b\delta)}\Big).

This is the general matrix concentration tool the whole chapter builds toward; Theorem 6.23 is one of its corollaries.

Milestone — Eq. (6.54) (the deterministic thresholding bound)

For any $\lambda_n$ with $\|\hat\Sigma-\Sigma\|_{\max}\le\lambda_n$ , $|\!|\!|T_{\lambda_n}(\hat\Sigma)-\Sigma|\!|\!|_2\le2|\!|\!|A|\!|\!|_2\lambda_n$ — a purely deterministic fact, with no probability involved, that reduces Theorem 6.23's proof to a single probabilistic input: controlling $\|\hat\Sigma-\Sigma\|_{\max}$ .

Significance

Theorem 6.17 is the workhorse of the whole chapter: besides Theorem 6.23, it also underlies Corollary 6.20's operator-norm bound for the unstructured sample covariance matrix (used in turn for the two example ensembles in Section 6.4.5), by taking $Q_i:=x_ix_i^T-\Sigma$ . Theorem 6.23 itself is the standard justification for thresholding-based covariance estimators used throughout high-dimensional statistics whenever the sparsity pattern of $\Sigma$ , though unknown, is believed to be structured.

Formalizing it. No faithful prior art exists on the platform for the matrix Bernstein bound or covariance thresholding (a fresh search for "matrix Bernstein," "Bernstein condition matrix," "thresholding covariance," and "sparse covariance" returned no hits). The existing RademacherWigner.* items formalize spectral-edge and empirical-spectral-distribution bounds for the Wigner ensemble specifically (a symmetric matrix with i.i.d. entries) — a narrower, different random-matrix model from the general Bernstein-condition matrices this chapter treats, and not reused here. All three theorems are drafted as open goals (:= by sorry).

Difficulty

The naive approach to a matrix tail bound — apply the scalar Chernoff/Bernstein technique directly to the operator norm — fails because the operator norm is not a linear functional of $Q$ , so the scalar moment generating function bound does not translate directly. The resolution (Lemma 6.13, not itself part of this mission) instead bounds the trace of the matrix exponential of the sum, which is linear-algebraically tractable via the Golden–Thompson-type inequality and the union bound over the (at most $\mathrm{rank}(\bar V)$ ) nonzero eigenvalue directions of the aggregate variance $\bar V=\sum_i\mathrm{var}(Q_i)$ — this is exactly why the bound's prefactor is $\mathrm{rank}(\bar V)$ , not the ambient dimension $d$ : a low-rank aggregate variance (e.g. from a highly structured collection of matrices) yields a much tighter bound than a naive union bound over all $d$ eigen-directions would. Theorem 6.23's own difficulty is entirely in the reduction to Theorem 6.17 plus Eq. (6.54): checking that $Q_i:=x_ix_i^T-\Sigma$ satisfies the Bernstein condition with the stated parameters, and that $\|\hat\Sigma-\Sigma\|_{\max}$ concentrates at the stated rate via a union bound over the $O(d^2)$ matrix entries.

Formalization scope

"Symmetric" is realized via Mathlib's Matrix.IsSymm; the Loewner order via (B-A).PosSemidef. The matrix moment generating function itself (ΨQ(λ):=E[e^{λQ}]) is not formalized, since none of this mission's three theorem statements need it directly — Bernstein's condition (Definition 6.10) is stated purely in terms of polynomial moments $\mathbb E[Q^j]$ , avoiding the substantial extra machinery (Mathlib's NormedSpace.exp for matrices) that a faithful matrix-exponential definition would require, at no cost to faithfulness for the three statements actually drafted.

Independence of $\{Q_i\}$ / $\{x_i\}$ is realized via Mathlib's iIndepFun; this required adding a local MeasurableSpace (Matrix (Fin d) (Fin d) ℝ) instance in the workspace, since Matrix is a def, not an abbrev, over the underlying Pi type, so Lean's instance search does not automatically find the Pi-type MeasurableSpace instance for it. "Identically distributed" is realized via Mathlib's IdentDistrib against a fixed reference index. "Each component sub-Gaussian" is restated locally as an explicit MGF bound at the reference index, per this book's cross-chapter rule against importing another chapter's draft definitions.

If a statement admits a trivializing formalization: the rank(...) prefactor of Theorem 6.17 is kept exactly, not replaced by the ambient dimension $d$ (which would be a strictly weaker, non-trivializing but unfaithful simplification, since the bound's whole point is that rank(...) ≤ d can be much smaller). ‖·‖_max and opNorm at d=0 return Mathlib's junk value 0 (harmless: no matrix entries or singular values exist at that degenerate size either).

Out of scope for this mission: Theorem 6.15 (the sub-Gaussian-tail matrix concentration result that precedes Theorem 6.17 in the same section) and Corollary 6.20 (the unstructured covariance-estimation corollary) — both natural follow-on work, cut for this chunk's time budget; see STATUS.md.

Selected references

M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019. DOI: 10.1017/9781108627771. Chapter 6.
J. A. Tropp, "User-friendly tail bounds for sums of random matrices," Foundations of Computational Mathematics, 12(4):389–434, 2012.

12 thms2 active usersReviewed

Completed

Machine Learning Probability Theoretical Computer Science·Captain: mikedeng1

Foundations of Machine Learning IX: Ranking and the Margin BoundTextbook

Motivation

Ranking is the learning problem behind search engines, recommendation systems and fraud-alert triage: what matters is not a single classification decision but the relative order the system assigns to a set of items, because a user or analyst can only act on the very top of a ranked list. Chapter 10 develops margin-based generalization theory for the score-based ranking setting, transplanting chunk 05-svm's single-sample Rademacher-complexity machinery to a genuinely two-sample structure: a ranking example is a pair of points, one drawn from each of two positions, and the chapter's bound must therefore control two marginal complexities rather than one. It also introduces RankBoost, the ranking analogue of AdaBoost, with a boosting-style empirical-error guarantee proved by the same normalization-factor telescoping argument as chunk 07's AdaBoost bound, adapted to RankBoost's own pairwise per-round quantities.

Setting

A ranking example is a pair (x,x') drawn from a distribution D over X×X, labeled by a preference function f; restricted to {-1,+1} labels (the simplification §10.2 adopts), a scoring function h:X→ℝ misranks (x,x') when f(x,x')(h(x')-h(x)) ≤ 0 (Eq. 10.1/10.2). The empirical margin loss R̂_{S,ρ}(h) (Eq. 10.3) uses the same Φ_ρ (Definition 5.5) as chunk 05-svm, restated locally here. Writing S1, S2 for the two coordinate projections of a pair sample S, and D1, D2 for the corresponding marginals of D, R_m^{D1}(H) and R_m^{D2}(H) are the Rademacher complexities of H under each marginal (p. 241). Theorem 10.1 bounds R(h) in terms of these two Rademacher-complexity terms, both in their population form (R_m^{D1}, R_m^{D2}) and their empirical form (R̂_{S1}, R̂_{S2}), via chunk 03's Theorem 3.3 applied through an auxiliary hypothesis family H̃ = {((x,x'),y) ↦ y[h(x')-h(x)]}. Corollary 10.2 specializes this to kernel-based linear scoring hypotheses; §10.4 introduces RankBoost (Figure 10.1), whose per-round weighted pairwise-outcome fractions ε_t^+, ε_t^- (Eq. 10.11) play the role AdaBoost's single ε_t plays in chunk 07, and Theorem 10.3 bounds RankBoost's empirical error in terms of them. Corollary 10.4 combines Theorem 10.1 with Lemma 7.4 (the convex hull of H has the same empirical Rademacher complexity as H, restated as a standing fact of the boosting series) to give RankBoost's own margin-based guarantee.

Formalization targets

Theorem 10.1 — the mission's goal. For H a set of real-valued functions, ρ>0, δ>0, with probability at least 1-δ, for all h∈H:

R(h) \le \hat R_{S,\rho}(h) + \tfrac2\rho(R_m^{D_1}(H)+R_m^{D_2}(H)) + \sqrt{\tfrac{\log(1/\delta)}{2m}}

R(h) \le \hat R_{S,\rho}(h) + \tfrac2\rho(\hat R_{S_1}(H)+\hat R_{S_2}(H)) + 3\sqrt{\tfrac{\log(2/\delta)}{2m}}.

Corollary 10.2 (milestone). For a PDS kernel K with r an upper bound on K(x,x), feature map Φ, and H = {x↦w·Φ(x) : ‖w‖≤Λ}, fixed ρ>0: R(h) ≤ R̂_{S,ρ}(h) + 4√(r²Λ²/ρ²/m) + √(log(1/δ)/(2m)).

Theorem 10.3 (milestone). RankBoost's empirical error verifies R̂_S(f) ≤ exp(-2∑_t((ε_t^+-ε_t^-)/2)²), and ≤ exp(-2γ²T) if the edge is uniformly at least γ>0.

Corollary 10.4 (milestone). Theorem 10.1's first bound, applied to h∈conv(H).

Significance

Theorem 10.1's proof is the chapter's genuine new technique, not a restatement of chunk 05's Theorem 5.8: the two-sample decomposition (splitting the supremum over H̃ into a term on x' alone and a term on x alone, each bounded by the Rademacher complexity under its own marginal) is what the 2/ρ · (R_m^{D1}+R_m^{D2}) structure expresses, and collapsing it to a single-sample bound would either be false or silently assume D1=D2 (which only holds for a symmetric D, an assumption the theorem does not make). Corollary 10.2 is the direct theoretical basis for the ranking SVM algorithm §10.3 derives. Theorem 10.3 mirrors chunk 07-boosting's Theorem 7.2 almost line for line in its proof technique (the same telescoping product of normalization factors Z_t), but with genuinely different per-round quantities (ε_t^+, ε_t^- rather than a single ε_t) that must not be conflated with AdaBoost's own, per BRIEF.md's pitfall note. Corollary 10.4 is what makes RankBoost's output (a linear, not convex, combination — normalized by ‖α‖_1) provably generalize independently of the number of boosting rounds T, the ranking analogue of chunk 07's Corollary 7.5. No prior art exists on the platform: GET /theorems?q=ranking%20loss returns zero hits.

Difficulty

Theorem 10.1's proof needs the two-sample structure carried through explicitly: H̃'s Rademacher complexity splits, via the sub-additivity of sup and the fact that y_iσ_i and σ_i have the same distribution, into a term on S2 alone and a term on S1 alone — treating a ranking sample as an ordinary single sample (chunk 03's single-hypothesis-set machinery applied naively) would drop this structure entirely and is exactly the pitfall BRIEF.md names. Theorem 10.3's proof requires Z_t = ε_t^0 + 2√(ε_t^+ε_t^-) be bounded via the identity 4ε_t^+ε_t^- = (1-ε_t^0)^2 - (ε_t^+-ε_t^-)^2 and the inequality 1-x ≤ e^{-x} — the same telescoping-normalizer technique as AdaBoost's Theorem 7.2, but RankBoost's own D_t, ε_t^+, ε_t^- genuinely differ (they are defined via pairwise outcomes y_i(h(x'_i)-h(x_i)) ∈ {-1,0,+1}, not a single-point disagreement h(x_i)≠y_i) and must be modeled as their own recursively-defined algorithm state, not obtained by substitution into chunk 07's AdaBoost Lean.

Formalization scope

MarginLossFunction restates chunk 05-svm's Definition 5.5; EmpiricalRademacherComplexity/ RademacherComplexity restate chunk 03-rademacher-vc's Definitions 3.1/3.2; IsPDS restates chunk 06-kernels's PDS-kernel definition; ConvHull restates chunk 07-boosting's convex-hull definition — all duplicated rather than imported since a draft item cannot import another chunk's draft module, and none is listed as reusable in missions/README.md's "Published definitions" table at the time of this session. D1, D2 are computed directly as Measure.map Prod.fst D/Measure.map Prod.snd D rather than posited via a separate marginal hypothesis, so the theorem statement itself pins down that they are genuinely the marginals of the sampling distribution D, not independent parameters. Corollary 10.2's r is an explicit upper bound on K(x,x) (hrK : ∀ x, K x x ≤ r) rather than a literal sSup, per BRIEF.md's pitfall note about the possibly-infinite supremum — the theorem's conclusion is monotonic in r, so this is not a weakening. RankBoost's D_t, ε_t^+, ε_t^-, α_t, Z_t and returned function f are modeled as their own recursively-defined algorithm state (mirroring chunk 07's AdaBoostDist/AdaBoostEpsilon/AdaBoostEnsemble pattern exactly, but built from RankBoost's own pairwise-outcome quantities, never by substituting into the AdaBoost Lean, per BRIEF.md's pitfall note) — RankBoostEpsilonPlus/RankBoostEpsilonMinus are already tied to RankBoost's own D_t and selected base ranker, so Theorem 10.3 needs no separate hypothesis connecting them (the same trivialization guard chunk 07's own Theorem 7.2 documents). No numerical constant is altered from the book in any of the four theorems.

Not formalized: §10.3's ranking-SVM primal/dual optimization problems (an algorithm derived from Corollary 10.2, not a generalization-theoretic result); §10.4.2 (RankBoost as coordinate descent, an algorithmic-equivalence argument, not a generalization bound); §10.5 (bipartite ranking, its own distinct problem formulation with a different generalization error, Eq. 10.20, explicitly out of scope per BRIEF.md); §10.6-10.7 (preference-based ranking, other criteria), out of scope per BRIEF.md. The uniform-over-ρ extension mentioned after both Theorem 10.1's and Corollary 10.2's proofs (referencing Theorem 5.9's technique from a different chapter) is not drafted, matching chunk 09-multiclass's identical scope decision for the analogous remark.

Selected references

M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 10 (§10.1-10.4).
Y. Freund, R. Iyer, R. E. Schapire, Y. Singer, "An efficient boosting algorithm for combining preferences," JMLR 4, 2003 (RankBoost's origin).
C. Cortes, M. Mohri, "AUC optimization vs. error rate minimization," NeurIPS 2003 (the ranking-SVM connection §10.3 develops).

20 thms2 active usersReviewed

Completed

Machine Learning Probability·Captain: mikedeng1

High-Dimensional Statistics XIV: Fano's Method for Minimax Lower BoundsTextbook

Motivation

Every convergence-rate result in the preceding chapters is an upper bound: some specific estimator (the Lasso, PCA, kernel ridge regression) achieves a given error rate. A natural and much harder question is the complementary one: is that rate actually the best any procedure could achieve, no matter its computational cost? Answering this requires a theory of lower bounds that holds simultaneously for every conceivable estimator — a fundamentally different kind of argument from constructing and analyzing one particular algorithm. Wainwright's High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 15, develops this theory, unifying classical techniques (Le Cam, Assouad, Fano) under one reduction: converting continuous estimation into discrete hypothesis testing.

Setting

Let $\mathcal X$ be a sample space and $\mathcal P$ a class of probability distributions on $\mathcal X$ . A functional $\theta: \mathcal P \to \Omega$ assigns each distribution a parameter of interest. An estimator is a measurable map $\hat\theta: \mathcal X \to \Omega$ . Fix a semi-metric $\rho:\Omega\times\Omega\to[0,\infty)$ — symmetric, triangle-inequality-satisfying, $\rho(\theta,\theta)=0$ , but possibly $\rho(\theta,\theta')=0$ for $\theta\ne\theta'$ — and an increasing $\Phi:[0,\infty)\to[0,\infty)$ . The minimax risk is

\mathfrak M\bigl(\theta(\mathcal P); \Phi\circ\rho\bigr) \;:=\; \inf_{\hat\theta} \sup_{P\in \mathcal P} \mathbb E_P\bigl[\Phi\bigl(\rho(\hat\theta, \theta(P))\bigr)\bigr],

the smallest worst-case expected loss achievable by any measurable estimator (Eq. (15.2)).

Given a 2δ-separated set $\{\theta_1,\dots,\theta_M\} \subseteq \theta(\mathcal P)$ (every pair satisfies $\rho(\theta_j,\theta_k)\ge 2\delta$ ) with representative distributions $P_{\theta_1},\dots,P_{\theta_M}$ , Wainwright constructs a testing problem: sample $J$ uniformly from $[M]$ , then $Z\sim P_{\theta_J}$ ; write $Q$ for the resulting joint law of $(J,Z)$ . A test function $\psi:\mathcal X\to[M]$ attempts to recover $J$ from $Z$ ; its error probability is $Q[\psi(Z)\ne J]$ .

Formalization targets

Goal (Proposition 15.1, "From estimation to testing")

For any increasing $\Phi$ and any 2δ-separated set with its induced joint testing measure $Q$ ,

\mathfrak M\bigl(\theta(\mathcal P); \Phi\circ\rho\bigr) \;\ge\; \Phi(\delta) \inf_{\psi} Q\bigl[\psi(Z)\ne J\bigr].

This mission formalizes Proposition 15.1 alone (see Formalization scope below for why, and what a follow-up mission would add to reach Fano's method proper, Proposition 15.12).

Significance

Proposition 15.1 is the single reduction every subsequent technique in the chapter specializes: Le Cam's two-point method (Lemma 15.9, $M=2$ , bounding the testing error via total variation distance), Fano's method (Proposition 15.12, bounding it via mutual information $I(Z;J)$ and Fano's inequality), and Assouad's method (a different, hypercube-based packing). Formalizing it in full generality — general $\Phi$ , general semi-metric, general $M$ -ary packing set — gives a single reusable lemma that a future mission proving any of these specific bounds can build on directly, rather than re-deriving the reduction each time.

The theorem is already proved in the source; this mission's contribution is a machine-checked formal statement (and, eventually, proof) of the reduction, in a form composing with any future formalization of the chapter's testing-error bounds (total variation, Fano, or otherwise).

Difficulty

The proof combines two ingredients that must each be kept in their sharpest form: Markov's inequality applied to $\Phi(\rho(\hat\theta,\theta))$ (which only needs $\Phi$ increasing, not convex or any specific shape — a premature specialization to $\Phi(t)=t^2$ would silently prove a weaker, less reusable statement), and the reduction of any estimator to a test via nearest- packing-point assignment (Eq. (15.4)), which uses the triangle inequality on $\rho$ in a specific direction (bounding $\rho(\theta_k,\hat\theta)$ from below via $\rho(\theta_j,\theta_k)$ and $\rho(\theta_j,\hat\theta)$ ) to show that a small estimation error forces the induced test to be correct. Getting the direction and strictness of every inequality right — non-strict separation, but strict distance in the "test is correct" event — is where a naive restatement goes wrong.

Formalization scope

$\mathcal X$ , $\Omega$ are arbitrary measurable spaces; the distribution class $\mathcal P$ is realized as an indexed family measure : Idx → Measure 𝒳 rather than a bare set of measures, composing directly with θ : Idx → Ω. The semi-metric $\rho$ is a bare function with explicit nonnegativity/reflexivity/symmetry/triangle-inequality hypotheses, matching the book's own footnote definition, rather than Mathlib's PseudoMetricSpace typeclass (kept self-contained, no extra instance machinery). The minimax risk is valued in ENNReal via the lower Lebesgue integral ∫⁻, not the Bochner integral, specifically to avoid the non-integrable-loss junk value 0 that a Bochner-integral formalization would silently introduce — a trivializing formalization would use ∫ (Bochner) here, letting a non-integrable loss vanish and making the inequality easier to satisfy than the book's actual claim; this mission does not do that. The joint testing measure $Q$ is characterized by its slice-measure equations directly on the product space $[M]\times\mathcal X$ , avoiding Mathlib's general conditional/disintegration machinery while remaining exactly equivalent to " $J$ uniform, $Z\mid J=j\sim P_{\theta_j}$ ".

Disclosed major scope decision. BRIEF.md recommended Proposition 15.12 (the Fano bound itself, Φ(δ)(1 - (I(Z;J)+\log 2)/\log M)) as this mission's goal. That statement requires, in addition to everything above, a formalized notion of mutual information $I(Z;J)$ between a finite-valued and a general (possibly continuous) random variable, and its use of a Fano-type inequality (Eq. (15.31), itself deferred by the book to "Section 15.4" and not fully quoted in the brief). Building a faithful mutual-information formalization general enough for this setting (finite $J$ , arbitrary measurable $Z$ ) — matching Mathlib's or this repo's existing, narrower information-theoretic developments (SourceCoding.*, built for a different, channel-coding purpose per BRIEF.md's own prior-art note) or building one from scratch — is substantially more than this session's remaining budget after building and self-reviewing 08-pca and 07-sparse-linear. This mission instead formalizes Proposition 15.1, the foundational reduction Proposition 15.12 itself specializes (via a particular bound on $\inf_\psi Q[\psi(Z)\ne J]$ ), so that a follow-up mission can add the mutual-information/Fano step on top of HighDimStat.Minimax.estimation_to_testing without redoing this reduction. This mission's name, fixed from missions/README.md, still names "Fano's Method" as the series slot this chunk occupies; its actual content is the reduction step every method in that family (including Fano's) shares — recorded explicitly here and in STATUS.md, not left implicit.

Selected references

Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 15. DOI: 10.1017/9781108627771.
Le Cam, L. "Convergence of estimates under dimensionality restrictions." Annals of Statistics, 1(1), 1973, 38–53.
Fano, R. M. Transmission of Information: A Statistical Theory of Communications. MIT Press, 1961.
Yu, B. "Assouad, Fano, and Le Cam." In Festschrift for Lucien Le Cam, Springer, 1997, 423–435.

4 thms2 active usersReviewed

Machine Learning Probability·Captain: mikedeng1

High-Dimensional Statistics XII: An Oracle Inequality for Nonparametric Least SquaresTextbook

Motivation

Regression is usually taught with a fixed parametric model: linear regression fits a $d$ -dimensional coefficient vector, and the estimation error is controlled by $d/n$ . Many regression problems in practice have no such finite-dimensional description — the regressor is only known to be, say, convex, monotone, or smooth, and the estimator is a least-squares fit over the (infinite-dimensional) set of functions with that shape. This is nonparametric regression, and the basic question is the same as in the parametric case: how close is the fitted function to the truth, as a function of the sample size $n$ ? Answering it requires replacing "dimension" with a genuinely functional notion of complexity, since an infinite- dimensional function class can still be small enough to estimate well (a Sobolev ball) or too large to estimate at all. The theory in this mission, due to van de Geer and developed in Chapter 13 of Wainwright (High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019), gives a single non-asymptotic template — the localized Gaussian complexity — that answers this question for an arbitrary star-shaped function class, and recovers the familiar parametric and Sobolev/RKHS rates as special cases.

Setting

Fix $n$ design points $x_1,\dots,x_n$ in an arbitrary covariate space $\mathcal X$ (fixed, not random — this is the fixed-design setting) and observe

y_i = f^*(x_i) + \sigma w_i, \qquad i = 1,\dots,n,

where $f^*$ is the unknown regression function, $\sigma > 0$ is a known noise level, and $w_1,\dots,w_n$ are i.i.d. standard Gaussian. Given a class $F$ of candidate functions, the nonparametric least-squares estimate is any minimizer

\hat f_n \in \arg\min_{f\in F}\ \frac1n\sum_{i=1}^n \big(y_i - f(x_i)\big)^2.

Error is measured in the empirical (design-dependent) seminorm $\|g\|_n^2 := \frac1n\sum_{i=1}^n g(x_i)^2$ . A class $H$ of functions is star-shaped if $h\in H$ and $\alpha\in[0,1]$ together imply $\alpha h \in H$ — every convex class containing the origin has this property, and it is the minimal structural assumption under which the theory below applies. For a star-shaped class $H$ and radius $\delta>0$ , the local Gaussian complexity

G_n(\delta; H) := \mathbb E_w\Big[\ \sup_{h\in H,\ \|h\|_n\le\delta}\ \Big|\tfrac1n \sum_{i=1}^n w_i h(x_i)\Big|\ \Big]

measures how much a mean-zero Gaussian process can be made to look like a member of $H$ restricted to the ball of radius $\delta$ . A critical radius $\delta_n$ is any positive solution of $G_n(\delta;H)/\delta \le \delta/(2\sigma)$ ; by Lemma 13.6, $\delta\mapsto G_n(\delta;H)/\delta$ is non-increasing on $H$ star-shaped, so this inequality always has a smallest positive solution.

Formalization targets

Lemma 13.6. For any star-shaped $H$ , $\delta \mapsto G_n(\delta;H)/\delta$ is non-increasing on $(0,\infty)$ , and consequently $G_n(\delta;H)/\delta \le c\delta$ has a smallest positive solution for every $c>0$ .

Theorem 13.5 (special case, $f^*\in F$ ).

\mathbb P\big[\|\hat f_n - f^*\|_n^2 \ge 16\,t\delta_n\big] \le e^{-nt\delta_n/(2\sigma^2)} \qquad \text{for all } t \ge \delta_n.

Theorem 13.13 (goal — general oracle inequality, $f^*$ not assumed in $F$ ). With $\delta_n$ solving the critical inequality for $\partial F := F - F$ , there are universal constants $(c_0,c_1,c_2)$ such that for all $t\ge\delta_n$ ,

\|\hat f_n-f^*\|_n^2 \le \inf_{\gamma\in(0,1)}\left[\frac{1+\gamma}{1-\gamma}\|f-f^*\|_n^2 +\frac{c_0}{\gamma(1-\gamma)}t\delta_n\right]\quad\text{for all }f\in F,

with probability at least $1-c_1e^{-c_2nt\delta_n/\sigma^2}$ . The goal is deliberately the statement with unresolved universal constants and an infimum over $\gamma$ , rather than any single instantiated bound, so the target survives sharper constant tracking.

Significance

Theorem 13.13 is the "master" result behind essentially every concrete rate in the chapter: orthogonal series regression, convex/monotone regression, and (via the KRR specialization of Section 13.4) kernel ridge regression rates for Sobolev and Gaussian-kernel classes are all obtained by bounding $G_n$ for a particular $F$ and reading off $\delta_n$ . Its value is that it isolates exactly the one place where the geometry of $F$ enters — the local Gaussian complexity — while the probabilistic argument (a peeling/chaining argument controlling a localized empirical process) is generic. Formalizing it produces, for the first time on the platform, the statement-level infrastructure (star-shaped classes, local Gaussian complexity, critical radius) that any future mission on a concrete nonparametric-regression rate — kernel ridge regression, convex regression, isotonic regression — can specialize, without re-deriving the oracle inequality from scratch. The proof itself (concentration of Gaussian complexity via Borell-TIS/Gaussian comparison plus a peeling argument over dyadic scales) is not attempted here; only the statement is formalized, as a draft goal for future proof contributions.

Difficulty

The naive route to Theorem 13.13 is to bound $\|\hat f_n - f^*\|_n$ pointwise via the basic inequality $\tfrac12\|\hat f_n-f^*\|_n^2 \le \tfrac{\sigma}{n}\sum_i w_i(\hat f_n(x_i)-f^*(x_i))$ and then bound the right side by $\sigma\,G_n(\delta;\partial F)$ for $\delta = \|\hat f_n-f^*\|_n$ — but $\delta$ is itself random (it depends on the estimate), so this is circular: the bound on the right depends on the very quantity being bounded. The chapter's actual argument resolves this with a peeling device: partition the event space by which dyadic annulus $\|\hat f_n-f^*\|_n$ falls into, and apply a uniform (non-circular) bound on each annulus separately via Gaussian concentration, summing a geometric series of tail probabilities. This is the step every first attempt misses, and it is why the local Gaussian complexity — rather than the simpler global complexity of Chapter 4/5 — is the right object: localizing to radius $\delta$ is what makes the per-annulus bound tight enough for the final sum to converge.

Formalization scope

Design points are an arbitrary type X (no topology or metric structure is needed for the statements themselves); the least-squares estimate is represented as a Prop (IsLeastSquaresEstimate) picking out any function achieving the empirical minimum, matching the book's "any minimizer" phrasing rather than assuming uniqueness. The local Gaussian complexity is defined as an expectation over an explicit i.i.d.-standard-Gaussian noise vector on an abstract probability space, with the inner supremum taken over the subtype of the radius-restricted slice of the class — this is well-defined (not the junk value 0 of an unbounded Set ℝ supremum) whenever the slice is nonempty, which holds automatically for any nonempty star-shaped class (taking $\alpha=0$ exhibits $0$ in the class). Since neither X nor H carries a topology, separability or countability constraint, SatisfiesCriticalInequality adds an explicit Integrable hypothesis on that same supremum (added in revision), guarding against Mathlib's Bochner integral silently returning the junk value 0 for a non-measurable integrand — a value that would otherwise trivially satisfy the critical inequality for every positive δ, regardless of the function class's actual local complexity. The trivializing formalization to rule out here is stating Theorem 13.13's universal constants after the quantification over the function class and sample size, which would let $(c_0,c_1,c_2)$ secretly depend on the instance and make the "universal" claim vacuous; this mission places the constant quantifiers first, before the class, design and noise data they must not depend on. A complete downstream development would add: the concentration-of-Gaussian-complexity step (Borell–TIS or a comparable tail bound), the peeling argument, and the metric-entropy / Dudley-integral machinery of Section 13.2.1 for bounding $G_n$ explicitly on concrete classes (Sobolev balls, RKHS balls) — none of which is attempted here.

Selected references

M. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Chapter 13. https://doi.org/10.1017/9781108627771
S. van de Geer, Empirical Processes in M-Estimation, Cambridge University Press, 2000.
S. van de Geer, "Estimating a regression function," Annals of Statistics, 18(2):907-924, 1990. https://doi.org/10.1214/aos/1176347627

4 thms2 active usersReviewed

Functional Analysis Machine Learning Probability·Captain: mikedeng1

High-Dimensional Statistics XI: The Moore-Aronszajn TheoremTextbook

Motivation

Many statistical problems — nonparametric regression, density estimation, dimension reduction, testing — are naturally posed as optimization over a space of functions rather than a finite-dimensional parameter vector. Hilbert spaces provide the right generality: they carry an inner product and a norm, so notions of projection, orthogonality and least-squares fitting all make sense, exactly as in ordinary Euclidean space, even though the "vectors" are now functions. Reproducing kernel Hilbert spaces (RKHSs) are the particular class of function-valued Hilbert spaces that make this program computationally tractable: they are generated by a single bivariate kernel function, and every RKHS computation reduces to evaluating that kernel, never to manipulating an infinite-dimensional object directly (the "kernel trick"). Wainwright's High-Dimensional Statistics (2019), Chapter 12, develops the foundational correspondence between kernels and Hilbert spaces that makes this possible, and this mission formalizes its two central theorems.

Setting

A Hilbert space is a complete inner product space (Definitions 12.1–12.2); this mission uses Mathlib's own NormedAddCommGroup/InnerProductSpace ℝ/CompleteSpace typeclasses for this notion throughout. A linear functional $L:H\to\mathbb R$ is bounded if $|L(f)|\le M\|f\|_H$ for some $M<\infty$ and all $f\in H$ ; the Riesz representation theorem (Theorem 12.5) says every such functional is $L(f)=\langle f,g\rangle_H$ for a unique $g\in H$ .

A bivariate function $K:X\times X\to\mathbb R$ is a positive semidefinite (PSD) kernel (Definition 12.6) if it is symmetric and every finite Gram matrix $(K(x_i,x_j))_{i,j=1}^n$ is positive semidefinite — the natural generalization of a PSD matrix to a (possibly infinite) index set $X$ , with no topological structure on $X$ required. A reproducing kernel Hilbert space (RKHS) for a kernel $K$ is a Hilbert space $H$ of functions on $X$ such that, for every $x\in X$ , the function $K(\cdot,x)$ belongs to $H$ and

\langle f, K(\cdot,x)\rangle_H = f(x) \qquad \text{for all } f\in H \tag{12.3}

— the reproducing property. Equivalently (Definition 12.12), $H$ is an RKHS exactly when every evaluation functional $f\mapsto f(x)$ is bounded on $H$ .

Formalization targets

Goal (Theorem 12.11, the Moore-Aronszajn theorem)

Given any PSD kernel function $K$ on any set $X$ , there is a Hilbert space $H$ (embedded into functions on $X$ ) in which $K$ satisfies the reproducing property (12.3) — and this Hilbert space is unique: any two Hilbert spaces with this property for the same $K$ are linearly isometric via an isometry intertwining their embeddings into functions on $X$ .

Milestones

Theorem 12.5 (Riesz representation). Every bounded linear functional on a Hilbert space $H$ has a unique representer $g\in H$ : $L(f)=\langle f,g\rangle_H$ for all $f$ . Used inside the proof of Theorem 12.13 to produce the representer $R_x$ of each evaluation functional.
Theorem 12.13 (the converse correspondence). Given any Hilbert space $H$ of functions on $X$ in which every evaluation functional is bounded, there is a unique PSD kernel $K$ satisfying the reproducing property for $H$ — completing the Moore-Aronszajn equivalence between PSD kernels and Hilbert spaces with bounded evaluation functionals.
Theorem 12.20 (Mercer's theorem). Under compactness of $X$ , continuity of $K$ , and the Hilbert-Schmidt condition $\int_{X\times X}K^2\,dP\,dP<\infty$ , the integral operator $T_K(f)(x)=\int_XK(x,z)f(z)\,dP(z)$ has an orthonormal eigenbasis $(\varphi_j)$ of $L^2(X;P)$ with non-negative eigenvalues $(\mu_j)$ , and $K(x,z)=\sum_j\mu_j\varphi_j(x)\varphi_j(z)$ , with the series converging absolutely and uniformly.

Significance

Theorem 12.11 is the theorem that makes the entire RKHS apparatus well-posed: every time a statistician writes down a kernel — linear, polynomial, Gaussian — Theorem 12.11 guarantees that a canonical Hilbert space of functions exists in which that kernel reproduces, so that optimizing over "the RKHS associated with $K$ " is a well-defined problem, not merely a suggestive shorthand. Theorem 12.13's converse shows the correspondence is exact — the class of kernel-generated Hilbert spaces is exactly the class of function spaces with bounded evaluation, the class relevant to any statistical application that samples a function at finitely many points. Together, these two results are the foundation the book's own later chapters build directly on: Chapter 13's nonparametric least-squares oracle inequality, and Chapter 14's kernel density estimation, both work by optimizing over an RKHS and are only well-posed because of this correspondence. Mercer's theorem, in turn, is what connects the RKHS viewpoint back to the earlier feature-map viewpoint of Chapter 12.2.2 (Eq. 12.2): the eigenfunctions $(\sqrt{\mu_j}\varphi_j)_j$ give an explicit feature map into $\ell^2(\mathbb N)$ realizing $K$ , and its expansion is what later underlies the book's discussion of kernel PCA and of RKHS balls as ellipsoids in $\ell^2(\mathbb N)$ -coordinates.

Difficulty

The formalization difficulty is concentrated in getting the type of the existence-and- uniqueness claim right, not in any single hypothesis. A Hilbert space is not naturally a subtype of a fixed ambient space in Lean, so "the Hilbert space $H$ " of Theorem 12.11 is formalized as an abstract type together with its own NormedAddCommGroup/InnerProductSpace ℝ/CompleteSpace instances, connected to "a space of functions on $X$ " via an injective linear embedding into $X\to\mathbb R$ — and uniqueness must then be stated as an isometric equivalence between any two witnessing Hilbert spaces that respects this embedding, the faithful rendering of the book's own proof, which literally shows two candidate Hilbert spaces are equal as sets of functions. A second subtlety is keeping Theorem 12.11's hypotheses (a bare PSD kernel, no topology on $X$ ) cleanly separated from Mercer's theorem's additional compactness, continuity and measure-theoretic apparatus — the two theorems are frequently conflated informally, but the book is explicit that Theorem 12.11 needs none of Mercer's structure.

Formalization scope

$X$ is an unconstrained Type* for Theorem 12.5, 12.11 and 12.13 — no topology, matching the book's own generality. Mercer's theorem (Theorem 12.20) additionally requires [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] and a finite measure P, matching its own compactness/continuity/measure-theoretic hypotheses exactly, never applied outside that scope. The integral operator $T_K$ of Eq. (12.11a) is presented as an abstract linear map on Lp ℝ 2 P tied to the defining integral formula via an explicit hypothesis, rather than constructed as a def, since constructing it as a genuine well-defined operator (needing integrability and a.e.-measurability arguments) is proof content, not definitional content, and this mission's definitions file is sorry-free by convention. Mercer's orthonormal-basis index type is existentially quantified over a countable ι (∃ (ι : Type) (_ : Countable ι), ...) rather than fixed to ℕ, since L²(X;P) can be finite-dimensional for finite X (Example 12.18/12.21), where no infinite orthonormal basis exists; the uniform-convergence conjunct is correspondingly quantified over every bijection e : ℕ ≃ ι (vacuous when ι is finite, a genuine order-independent claim when ι is countably infinite). A trivializing formalization of this chapter would state only existence in Theorem 12.11 and drop uniqueness (explicitly warned against by this chapter's own brief), or state Mercer's convergence merely pointwise or in $L^2$ rather than absolutely and uniformly; this mission avoids both. Out of scope: the constructive proof detail of Theorem 12.11 (the explicit span-and-complete construction is proof content, not part of the statement), the chapter's worked kernel examples (linear, polynomial, Gaussian kernels, Examples 12.7–12.9), and the further consequences of Mercer's theorem (Corollary 12.26 on RKHS-ball ellipsoids, the feature-map connection of Eq. 12.14) — all natural follow-on work for a future mission on kernel-based nonparametric regression (Chapter 13, mission 13-nonparametric-ls), which restates whatever RKHS objects it needs locally rather than importing this mission's draft, per this book's series-wide convention.

Selected references

Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 12. DOI: 10.1017/9781108627771.
Aronszajn, N. "Theory of reproducing kernels." Transactions of the American Mathematical Society, 68(3), 1950, 337–404.
Mercer, J. "Functions of positive and negative type, and their connection with the theory of integral equations." Philosophical Transactions of the Royal Society A, 209, 1909, 415–446.

5 thms2 active usersReviewed

Machine Learning Probability·Captain: mikedeng1

High-Dimensional Statistics VIII: Oracle Inequalities for Decomposable RegularizersTextbook

Motivation

Chapters 2 through 8 of Wainwright's High-Dimensional Statistics build up sharp error bounds for a sequence of specific high-dimensional models — sparse linear regression via the Lasso (Chapter 7), sparse principal components (Chapter 8) — each proved from scratch with techniques tailored to that model's own penalty and loss. Chapter 9 steps back and asks what made all of those arguments work, and isolates the answer into two structural ingredients: a decomposable regularizer, whose triangle inequality is tight across a well-chosen subspace pair, and a restricted curvature condition on the loss, holding only on the cone that decomposability forces the estimation error into. Once these two ingredients are checked for a particular model, a single, already-proved oracle inequality hands back the error bound — no further optimization-theoretic argument is needed. This mission formalizes that oracle inequality itself, together with its two supporting theorems, as the reusable core the book's later chapters (nuclear-norm matrix regression in Chapter 10, graphical model selection in Chapter 11, group-sparse and overlap-group Lassos) each specialize.

Setting

Let $\Omega$ be a finite-dimensional real inner product space (e.g. $\mathbb R^d$ , or a matrix space with the Frobenius inner product), and consider the regularized M-estimator

\hat\theta \in \operatorname*{arg\,min}_{\theta\in\Omega} \Big\{ L_n(\theta) + \lambda_n\Phi(\theta) \Big\},

where $L_n:\Omega\to\mathbb R$ is a convex empirical cost function, $\Phi:\Omega\to[0,\infty)$ is a norm-based regularizer, and $\lambda_n>0$ is a user-chosen regularization weight. Write $\theta^*$ for the true parameter and $\Delta:=\hat\theta-\theta^*$ for the estimation error.

A pair of subspaces $\mathcal M\subseteq\bar{\mathcal M}$ of $\Omega$ — the model subspace and its (possibly larger) closure — has an associated perturbation subspace $\bar{\mathcal M}^\perp$ , the orthogonal complement of $\bar{\mathcal M}$ . The regularizer $\Phi$ is decomposable with respect to $(\mathcal M,\bar{\mathcal M})$ if the triangle inequality $\Phi(\alpha+\beta)\le\Phi(\alpha)+\Phi(\beta)$ is an equality whenever $\alpha\in\mathcal M$ and $\beta\in\bar{\mathcal M}^\perp$ — the regularizer penalizes deviations away from the model subspace exactly as much as it possibly could. The canonical example is the $\ell_1$ -norm with $\mathcal M=\bar{\mathcal M}$ the subspace of vectors supported on a fixed index set $S$ .

Writing $\Phi^*(v):=\sup_{\Phi(u)\le 1}\langle u,v\rangle$ for the dual norm, the good event $\mathcal G(\lambda_n):=\{\Phi^*(\nabla L_n(\theta^*))\le\lambda_n/2\}$ says the regularization weight dominates the dual norm of the score function at the truth — the non-probabilistic conditioning hypothesis every result in this chapter is stated under. The subspace Lipschitz constant $\Psi(S):=\sup_{u\in S\setminus\{0\}}\Phi(u)/\|u\|$ measures the worst-case price of converting between the regularizer $\Phi$ and the error norm $\|\cdot\|$ on a subspace $S$ .

Formalization targets

Goal (Theorem 9.19, "Bounds for general models")

Under (A1) $L_n$ convex, satisfying restricted strong convexity (RSC) with curvature $\kappa>0$ , radius $R$ and tolerance $\tau_n^2$ — $E_n(\Delta):=L_n(\theta^*+\Delta)-L_n(\theta^*) -\langle\nabla L_n(\theta^*),\Delta\rangle \ge \frac{\kappa}{2}\|\Delta\|^2-\tau_n^2\Phi^2(\Delta)$ for $\|\Delta\|\le R$ — and (A2) $\Phi$ decomposable with respect to $(\mathcal M,\bar{\mathcal M})$ : conditioned on $\mathcal G(\lambda_n)$ , any optimal $\hat\theta$ satisfies

\text{(a)}\quad \Phi(\hat\theta-\theta^*) \le 4\big(\Psi(\bar{\mathcal M})\, \|\hat\theta-\theta^*\| + \Phi(\theta^*_{\mathcal M^\perp})\big),

and, whenever $\tau_n^2\Psi^2(\bar{\mathcal M})\le\kappa/64$ and $\varepsilon_n(\mathcal M,\bar{\mathcal M})\le R$ ,

\text{(b)}\quad \|\hat\theta-\theta^*\|^2 \le \varepsilon_n^2(\mathcal M,\bar{\mathcal M}) := \frac{9\lambda_n^2}{\kappa^2}\Psi^2(\bar{\mathcal M}) + \frac{8}{\kappa}\Big(\lambda_n\Phi(\theta^*_{\mathcal M^\perp}) + 16\tau_n^2\Phi^2(\theta^*_{\mathcal M^\perp})\Big).

Milestones

Proposition 9.13. Under (A2) alone, conditioned on $\mathcal G(\lambda_n)$ , the error $\Delta=\hat\theta-\theta^*$ lies in the cone $\mathbb C_{\theta^*}(\mathcal M,\bar{\mathcal M}):=\{\Delta\mid\Phi(\Delta_{\bar{\mathcal M}^\perp})\le 3\Phi(\Delta_{\bar{\mathcal M}})+4\Phi(\theta^*_{\mathcal M^\perp})\}$ — the purely geometric fact Theorem 9.19's curvature argument is built on.
Corollary 9.20. When $\theta^*\in\mathcal M$ exactly, the approximation-error term of $\varepsilon_n^2$ vanishes and Theorem 9.19 collapses to $\Phi(\hat\theta-\theta^*)\le\frac{6\lambda_n}{\kappa}\Psi^2(\bar{\mathcal M})$ , $\|\hat\theta-\theta^*\|^2\le\frac{9\lambda_n^2}{\kappa^2}\Psi^2(\bar{\mathcal M})$ — the form used directly against every concrete model in the rest of the book.
Theorem 9.24. Under an alternative, gradient-based curvature condition ( $\Phi^*$ -curvature, Definition 9.22) and $\theta^*\in\mathcal M$ , the dual-norm error is controlled directly: $\Phi^*(\hat\theta-\theta^*)\le 3\lambda_n/\kappa$ .

Significance

Theorem 9.19 is the book's own claimed unifying result: as it remarks explicitly, the theorem is a deterministic implication, and every later probabilistic corollary in Parts II and III of the book is obtained by (i) checking that a specific loss/regularizer pair is decomposable with respect to a natural subspace pair for the problem at hand, (ii) certifying the RSC condition with high probability for that loss (via concentration arguments from Chapters 2–6), and (iii) choosing $\lambda_n$ large enough that the good event holds with high probability — then reading off the rate directly from $\varepsilon_n^2(\mathcal M,\bar{\mathcal M})$ . Chapter 7's Lasso bound (Theorem 7.13, mission 07-sparse-linear) is exactly Corollary 9.20 specialized to $\Phi=\|\cdot\|_1$ and $\mathcal M$ the subspace of $s$ -sparse vectors — but Chapter 9 proves it once, in a form that Chapter 10's nuclear-norm-regularized low-rank matrix regression (mission 10-matrix-rank), Chapter 11's graphical model selection, and the chapter's own group-Lasso and overlap-group-Lasso examples all instantiate without re-deriving the optimization argument.

Difficulty

The formalization difficulty here is almost entirely conceptual rather than syntactic: getting the two-subspace apparatus $(\mathcal M,\bar{\mathcal M})$ exactly right. The book explicitly allows $\bar{\mathcal M}$ to be a strict superset of $\mathcal M$ (needed for the nuclear norm in Chapter 10, where the naive choice $\mathcal M=\bar{\mathcal M}$ fails to be decomposable at all), so every definition and theorem in this mission is parameterized by the pair, not by a single subspace — and three genuinely different projections appear across the statements: the error vector's projection onto $\bar{\mathcal M}$ and onto $\bar{\mathcal M}^\perp$ (both keep the bar), versus the true parameter's projection onto $\mathcal M^\perp$ (the complement of the small, unbarred subspace). A further subtlety specific to this printed source: several of the book's own displayed equations for $\Psi(\cdot)$ in Theorem 9.19 and Corollary 9.20 lose the overbar on $\bar{\mathcal M}$ in PDF text extraction (a rendering artifact, not a mathematical ambiguity); resolving which subspace is meant required reading the surrounding proof text line by line, since only $\Psi(\bar{\mathcal M})$ — not $\Psi(\mathcal M)$ — is mathematically consistent with how the constant is derived and used (see MODERATION_NOTES.md).

Formalization scope

$\Omega$ is [NormedAddCommGroup Ω] [InnerProductSpace ℝ Ω] [FiniteDimensional ℝ Ω], matching the book's implicit assumption of a finite-dimensional inner-product parameter space throughout this part of the book. The regularizer's norm axioms (IsRegularizerNorm), the dual norm, and the subspace Lipschitz constant are all defined via sSup/sInf-free explicit formulas or sSup over an explicitly-described set (never an unconstrained supremum over all of $\Omega$ ), so no faithfulness trap from an unbounded or empty supremum arises (see MODERATION_NOTES.md's trap table). κ > 0 and λ_n > 0 are made explicit hypotheses of every theorem, matching Definition 9.15's own stated positivity of $\kappa$ and the chapter's running convention that $\lambda_n$ is a positive regularization weight — never a narrowing of the theorem's actual scope. A trivializing formalization of this chapter would either collapse the two-subspace machinery to a single subspace $\mathcal M=\bar{\mathcal M}$ (which is faithful only for the $\ell_1$ /group-Lasso examples, not the general theorem, and not what Chapter 10 needs) or silently drop the second conjunct of Theorem 9.19's conclusion (part (b), the actual quantitative rate) in favor of only the qualitative part (a); this mission formalizes the full two-subspace statement and both conjuncts of the goal theorem. Out of scope: the chapter's worked examples (sparse GLMs, Corollary 9.26; group Lasso; nuclear-norm matrix regression) that specialize the goal to concrete models — Chapter 10's own mission (10-matrix-rank) restates the needed instance of this framework locally rather than importing this mission's draft, per this book's series-wide convention that no draft imports another chunk's draft. Also out of scope: the RSC-implies-restricted-eigenvalue correspondence (Example 9.16) and the $\mu_n(\Phi^*)$ -based general RSC certification (Theorem 9.36, Section 9.8), both purely probabilistic results that lie outside this chapter's own deterministic core.

Selected references

Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 9. DOI: 10.1017/9781108627771.
Negahban, S. N., Ravikumar, P., Wainwright, M. J., Yu, B. "A unified framework for high-dimensional analysis of M-estimators with decomposable regularizers." Statistical Science, 27(4), 2012, 538–557.
Tibshirani, R. "Regression shrinkage and selection via the Lasso." Journal of the Royal Statistical Society: Series B, 58(1), 1996, 267–288.

5 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 Probability·Captain: mikedeng1

High-Dimensional Statistics VII: Eigenvector Perturbation for High-Dimensional PCATextbook

Motivation

Principal component analysis (PCA) is one of the oldest and most widely used tools in multivariate statistics: given data with covariance matrix $\Sigma$ , project onto the top eigenvector(s) of $\Sigma$ to find the directions of maximal variance. In practice one never observes $\Sigma$ itself, only a perturbed version — a sample covariance matrix $\hat\Sigma = \Sigma + P$ , with $P$ the (random) estimation error. The natural question, asked since at least Davis and Kahan (1970) and Wedin (1972), is: how close is the top eigenvector of $\hat\Sigma$ to that of $\Sigma$ ? Wainwright's High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 8, gives a self-contained, sharp, non-asymptotic answer, phrased entirely in terms of two deterministic quantities: the eigengap of $\Sigma$ , and a single scalar summarizing how the perturbation $P$ couples to the top eigendirection.

Unlike most of the results in this book series, this one is a statement of pure linear algebra: no probability, no concentration inequality, no sample size is needed to state or prove it. Randomness enters only afterward, when $P$ is instantiated as an actual sampling error and bounded using the machinery of earlier chapters (Corollary 8.7, out of this mission's scope).

Setting

Let $\Sigma \in \mathbb R^{d\times d}$ be a symmetric positive semidefinite matrix. Say $\theta \in \mathbb R^d$ is a maximal unit eigenvector of $\Sigma$ if $\|\theta\|_2=1$ and $\theta$ maximizes the Rayleigh quotient $\langle\theta,\Sigma\theta\rangle$ over the whole unit sphere $\mathcal S^{d-1}$ — the variational characterization of the top eigenvector/eigenvalue pair, matching Eq. (8.14) of the book. Write $\gamma_1(\Sigma) := \langle\theta^*,\Sigma\theta^*\rangle$ for the corresponding top eigenvalue. Say $\Sigma$ has eigengap $\nu>0$ at $\theta^*$ if every unit vector $v$ orthogonal to $\theta^*$ satisfies $\langle v,\Sigma v\rangle \le \gamma_1(\Sigma) - \nu$ — the Courant-Fischer variational form of the book's $\nu := \gamma_1(\Sigma)-\gamma_2(\Sigma)$ .

For a symmetric perturbation matrix $P \in \mathbb R^{d\times d}$ , write $|\!|\!|P|\!|\!|_2 := \sup_{\|v\|_2=1}|\langle v,Pv\rangle|$ for its $\ell_2$ -operator norm, and

\tilde p \;:=\; P\theta^* - \langle P\theta^*,\theta^*\rangle\,\theta^*

for the component of $P\theta^*$ orthogonal to $\theta^*$ — the piece of the perturbation that actually couples the top eigendirection to the rest of the space (Eq. (8.11)). Note $\|\tilde p\|_2$ can be far smaller than $|\!|\!|P|\!|\!|_2$ : a perturbation can be large in every direction yet barely move the top eigenvector, if its interaction with $\theta^*$ specifically is small.

Formalization targets

Goal (Theorem 8.5)

Let $\Sigma$ be symmetric positive semidefinite with maximal unit eigenvector $\theta^*$ and eigengap $\nu>0$ . For any symmetric $P$ with $|\!|\!|P|\!|\!|_2 < \nu/2$ , and any maximal unit eigenvector $\hat\theta$ of $\hat\Sigma := \Sigma+P$ with $\langle\hat\theta,\theta^*\rangle \ge 0$ ,

\|\hat\theta - \theta^*\|_2 \;\le\; \frac{2\|\tilde p\|_2}{\nu - 2|\!|\!|P|\!|\!|_2}.

Milestone (Lemma 8.6, the PCA basic inequality)

Under the same eigengap hypothesis, with $\Psi(\Delta;P) := \langle\Delta,P\Delta\rangle

2\langle\Delta,P\theta^\rangle $and$ \Delta := \hat\theta-\theta^$,

\nu\bigl(1-\langle\hat\theta,\theta^*\rangle^2\bigr) \;\le\; |\Psi(\Delta;P)|.

Significance

The bound isolates exactly what drives eigenvector instability: not the raw size of the perturbation but its projection onto the top eigendirection, rescaled by the inverse eigengap. This explains, in one inequality, the qualitative phenomenon Example 8.4 illustrates numerically (a tiny perturbation can move the eigenvector far when the eigengap is small) and quantifies exactly how far. It is the deterministic engine behind every consistency result for PCA in the rest of the chapter: Corollary 8.7 (rates for the spiked covariance model) and the sparse-PCA guarantee (Theorem 8.10) both specialize this same bound, after bounding $\|\tilde p\|_2$ and $|\!|\!|P|\!|\!|_2$ using concentration for a specific random design. It is also a sharp instance of the general Davis-Kahan-type perturbation theory for symmetric matrices, phrased with an explicit, non-asymptotic constant rather than an $O(\cdot)$ .

The theorem is already proved in the source; this mission's contribution is a machine-checked formal statement (and, eventually, proof) of the bound and its supporting basic inequality, composing with any future formalization of the chapter's probabilistic corollaries.

Difficulty

The proof is genuinely variational, not spectral: it never diagonalizes $\Sigma$ or $\hat\Sigma$ , only uses that $\theta^*$ and $\hat\theta$ are optimal for their respective Rayleigh-quotient maximizations. The one place a naive argument fails is in bounding $|\Psi(\Delta;P)|$ itself (the proof of Lemma 8.6): a direct Cauchy-Schwarz bound on $\langle\Delta,P\Delta\rangle$ using $|\!|\!|P|\!|\!|_2$ alone would produce a bound in terms of $|\!|\!|P|\!|\!|_2$ throughout, not the sharper $\|\tilde p\|_2$ the theorem actually delivers; getting the sharper dependence requires decomposing $\Delta$ along $\theta^*$ and its orthogonal complement and tracking the two pieces separately (the $\varrho$ , $z$ decomposition on p. 244). The sharpness of the threshold $|\!|\!|P|\!|\!|_2 < \nu/2$ is also not a proof artifact: the book's own $2\times 2$ example ( $\Sigma=\mathrm{diag}(2,1)$ , $P=\mathrm{diag}(-1/2,1/2)$ ) shows the perturbed matrix can lose a unique maximal eigenvector exactly at $|\!|\!|P|\!|\!|_2 = \nu/2$ .

Formalization scope

$\Sigma$ , $P$ , $\hat\Sigma=\Sigma+P$ are Matrix (Fin d) (Fin d) ℝ; "symmetric" is M.transpose = M; "positive semidefinite" is the quadratic-form condition $\langle v, \Sigma v\rangle \ge 0$ for all $v$ , stated directly rather than via a Mathlib PosSemidef typeclass. "Maximal unit eigenvector" and "eigengap" are both given their variational (Rayleigh-quotient) characterizations rather than defined through Mathlib's enumerated matrix-eigenvalue API — mathematically equivalent to the book's spectral definitions by the Courant-Fischer theorem, and the same characterization the book's own proof works with throughout (Eq. (8.14)). The operator norm $|\!|\!|\cdot|\!|\!|_2$ is likewise realized variationally, valid because this mission only ever applies it to symmetric matrices, exactly as the book does in this chapter. $\tilde p$ is realized as a basis-independent vector in $\mathbb R^d$ (the component of $P\theta^*$ orthogonal to $\theta^*$ ) rather than the book's basis-dependent $\mathbb R^{d-1}$ representative; its $\ell_2$ -norm — the only quantity the theorem's conclusion uses — is identical either way.

Deliberate scope decision, disclosed here rather than silently: the book's own Theorem 8.5 concludes that $\hat\Sigma$ "has a unique maximal eigenvector $\hat\theta$ " satisfying the bound — asserting both existence and uniqueness as part of the theorem, on top of the quantitative bound. This mission formalizes only the quantitative bound, for an arbitrary maximal unit eigenvector $\hat\theta$ of $\hat\Sigma$ satisfying the sign condition $\langle\hat\theta,\theta^*\rangle\ge0$ — exactly what the book's own proof establishes (the proof never separately argues existence or uniqueness; both are consequences that could be derived from the bound together with a compactness argument for existence, left to a future extension) and exactly what every downstream use in the chapter (Examples, Corollary 8.7) actually invokes. A trivializing formalization would instead drop the sharp threshold $|\!|\!|P|\!|\!|_2 < \nu/2$ to ≤, or conflate the general operator norm with the symmetric-matrix Rayleigh-quotient characterization for a non-symmetric $P$ ; this mission does neither. Corollary 8.7 (spiked covariance rates) and Theorem 8.10 (sparse PCA, needing the uniform deviation condition of Eq. (8.26)) are out of this mission's scope; a companion mission formalizing them on top of this one's pca_eigenvector_perturbation_bound is natural future work, together with a proof of existence of a maximal unit eigenvector via compactness of the sphere.

Selected references

Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 8. DOI: 10.1017/9781108627771.
Davis, C., Kahan, W. M. "The rotation of eigenvectors by a perturbation. III." SIAM Journal on Numerical Analysis, 7(1), 1970, 1–46.
Wedin, P.-Å. "Perturbation bounds in connection with singular value decomposition." BIT Numerical Mathematics, 12(1), 1972, 99–111.

8 thms2 active usersReviewed