Motivation

Weak learning — a base classifier only slightly better than random guessing — is easy to come by; strong learning, in the PAC sense of Chapter 2, is not. Boosting is the technique that turns the first into the second: combine many weak classifiers, each trained on a reweighted version of the sample that emphasizes previously misclassified points, into a single strong ensemble. AdaBoost, the algorithm this chapter studies, does this with a specific, closed-form weighting rule, and comes with two distinct theoretical guarantees: its training error decreases exponentially fast in the number of rounds (Theorem 7.2), and — more surprisingly — its test error can keep improving even after the training error has already reached zero, an empirical phenomenon that Chapter 3's VC-dimension bound cannot explain at all (it predicts overfitting for large numbers of rounds) but that a margin-based analysis, structurally identical to Chapter 5's SVM theory, does (Theorem 7.7). This mission formalizes both routes.

Setting

AdaBoost (Figure 7.1) takes a labeled sample $S=((x_1,y_1),\dots,(x_m,y_m))$ with $y_i\in\{-1,+1\}$ and a base classifier set $H\subseteq\{-1,+1\}^X$, and runs for $T$ rounds. It maintains a distribution $D_t$ over the sample indices, starting uniform ($D_1(i)=1/m$); at round $t$ it selects a base classifier $h_t$ with small $D_t$-weighted error $\varepsilon_t=\Pr_{i\sim D_t}[h_t(x_i)\ne y_i]$, sets $\alpha_t=\frac12\log\frac{1-\varepsilon_t} {\varepsilon_t}$ and $Z_t=2\sqrt{\varepsilon_t(1-\varepsilon_t)}$, and reweights: $D_{t+1}(i)=D_t(i)\exp(-\alpha_ty_ih_t(x_i))/Z_t$. After $T$ rounds it returns $f=\sum_{t=1}^T\alpha_th_t$; its normalized version is $\bar f=f/\sum_t\alpha_t$. Since $\varepsilon_t<1/2$ makes $\alpha_t>0$, $\bar f$ is a genuine convex combination of base classifiers, i.e. a member of the convex hull $\mathrm{conv}(H)=\{\sum_k\mu_kh_k:\mu_k\ge0, h_k\in H,\sum_k\mu_k\le1\}$ (Eq. 7.12). The chapter reuses Chapter 5's confidence-margin apparatus (empirical margin loss $\hat R_{S,\rho}$, Rademacher complexity $\hat R_S$/$R_m$) to analyze $\bar f$'s generalization.

Formalization targets

Theorem 7.2 (AdaBoost empirical error bound, milestone). The empirical (zero-one) error of $f$ satisfies $\hat R_S(f) \le \exp(-2\sum_{t=1}^T(1/2-\varepsilon_t)^2)$, and, if $\gamma\le1/2-\varepsilon_t$ for all $t$, $\hat R_S(f)\le\exp(-2\gamma^2T)$: training error decays exponentially in $T$ whenever every round beats random guessing by a fixed margin (the "edge" $\gamma$).

Lemma 7.4 (milestone). $\hat R_S(\mathrm{conv}(H))=\hat R_S(H)$: the convex hull of a hypothesis set, though generally much larger, has exactly the same empirical Rademacher complexity as the set itself.

Corollary 7.5 (Ensemble Rademacher margin bound, milestone). For $H$ a set of real-valued functions and $\rho>0$, with probability at least $1-\delta$, every $h\in\mathrm{conv}(H)$ satisfies $R(h)\le\hat R_{S,\rho}(h)+\frac2\rho R_m(H)+\sqrt{\log(1/\delta)/(2m)}$ (and the empirical-complexity analogue with an extra additive $3\sqrt{\log(2/\delta)/(2m)}$ term) — this is Theorem 5.8's margin bound applied to $\mathrm{conv}(H)$, then rewritten via Lemma 7.4 so its complexity term is $H$'s own, not the (much larger) convex hull's.

Theorem 7.7 — the mission's goal. Assume $\varepsilon_t<1/2$ for every $t\in[T]$ (so $\alpha_t>0$). Then for any $\rho>0$,

$$\hat R_{S,\rho}(\bar f) \le 2^T\prod_{t=1}^T\sqrt{\varepsilon_t^{1-\rho}(1-\varepsilon_t)^{1+\rho}}.$$

Significance

Theorem 7.7's bound is what makes margin theory a genuine explanation of AdaBoost's empirical behavior: combined with Corollary 7.5 (applied to $\bar f\in\mathrm{conv}(H)$), it shows that if AdaBoost's edge stays bounded away from zero, the empirical margin loss at a fixed $\rho$ decreases exponentially in $T$ while the generalization bound's complexity term does not depend on $T$ at all — so continuing to boost past zero training error can still shrink the true risk, by growing the margin on the training points that are already correctly classified. This resolves the puzzle that opens §7.3.1: AdaBoost's test error is empirically observed to keep decreasing well after its training error hits zero, which the chapter's own earlier VC-dimension bound on $\mathcal F_T$ (Eq. 7.9, growing as $O(dT\log T)$) predicts should eventually overfit, not improve. No prior art on the Prove2Me platform is faithful: GET /theorems?q=boosting and q=AdaBoost return no hits; this chunk's Rademacher-complexity apparatus is restated locally (a draft item cannot import chunk 05-svm's or 03-rademacher-vc's own draft copies) rather than reused, matching the precedent those chunks' own STATUS.md records recommend for every later chunk needing the same machinery.

Not formalized here: Theorem 7.6 (the VC-dimension-based ensemble margin bound, a direct corollary of Corollary 7.5 via chunk 03's VC-dimension apparatus) — restating 03's own machinery a second time for a single further corollary is disproportionate within this mission's budget, and the chapter's actual capstone targets the sharper, dimension-free Rademacher-complexity route (Theorem 7.7) instead. Also out of scope: §7.2.2's coordinate- descent equivalence, §7.2.3's practical (decision-stump) use, and §7.3.4-7.3.5's margin- maximization LP and game-theoretic interpretation — discussion sections with no numbered result feeding the goal's proof.

Difficulty

Theorem 7.2's proof needs the telescoping identity $D_{T+1}(i) = e^{-y_if(x_i)}/(m\prod_tZ_t)$ (Eq. 7.2), obtained by repeatedly unfolding the recursive weight update — a genuine induction on $t$, not a one-line algebraic manipulation — before the elementary inequality $1_{u\le0}\le e^{-u}$ turns the empirical error into a telescoping product of the $Z_t$'s, each of which is then re-expressed in closed form via a case split on $y_ih_t(x_i)=\pm1$. Theorem 7.7's proof reuses the same identity but with an added margin-shift term $\rho\|\alpha\|_1$ inside the exponential, requiring the same telescoping machinery plus a separate accounting of $e^{\rho\sum_t\alpha_t}$ against the product of $[\sqrt{(1-\varepsilon_t)/\varepsilon_t}]^\rho$ factors coming from each $\alpha_t$'s own closed form — a proof that shares its main structural step with Theorem 7.2 but is not a trivial corollary of it. Corollary 7.5's proof is Lemma 7.4 (itself a careful supremum-exchange argument using the dual-norm characterization of $\ell^1$, not a routine calculation) composed with Theorem 5.8, applied to the specific set $\mathrm{conv}(H)$ rather than a generic hypothesis class — a formalization that stated the corollary only for a "sufficiently nice" abstract class, without deriving it from Lemma 7.4's convex-hull identity, would be proving a different, weaker-provenance statement.

Formalization scope

WeightedError, AdaBoostAlpha, AdaBoostNormalizer, AdaBoostDist, AdaBoostEpsilon, AdaBoostEnsemble, AdaBoostNormalizedEnsemble, EmpiricalError and ConvHull are new, capturing AdaBoost as an actual algorithm (a genuine recursion on the round index, closed under Definitions.Def_FoundationsML_Boosting_AdaBoostDist's own recursive equation) rather than an unspecified "boosting procedure" — the trivialization trap BRIEF.md names for this chapter. AdaBoostDist takes the sequence of base classifiers actually selected at each round, h : ℕ → X → ℝ, as external data rather than deriving it via an argmin over H; this is checked in SELF_REVIEW.md to drop no content either milestone or the goal theorem's statement actually needs, since neither invokes h_t's optimality, only the weighted error ε_t it produces under AdaBoost's own distribution D_t. PhiRho, EmpiricalMarginLoss, MarginGeneralizationError, EmpiricalRademacherComplexity and RademacherComplexity are restated locally, byte-identical to chunk 05-svm's own copies of Definitions 5.5, 5.6, 2.1 (specialized), 3.1, 3.2 (a draft item cannot import another chunk's draft module); this duplication collapses once 05-svm and 03-rademacher-vc are uploaded and listed in missions/README.md's "Published definitions" table. No numerical constant in any of the four theorems is altered from the book's own displayed form. A trivializing formalization this mission avoids: stating Theorem 7.2/7.7 for an arbitrary sequence of error rates $\varepsilon_1,\dots,\varepsilon_T$ satisfying $\varepsilon_t<1/2$, disconnected from any actual algorithm — AdaBoostEpsilon instead ties every ε_t to the weighted error AdaBoost's own recursively defined D_t assigns to its own selected h_t, so the bound is provably about this algorithm's error trajectory, not an arbitrary one.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 7.
• 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, 119-139.
• R. E. Schapire, Y. Freund, P. Bartlett, W. S. Lee, "Boosting the margin: a new explanation for the effectiveness of voting methods," The Annals of Statistics 26(5), 1998, 1651-1686.

Motivation

Modern regression problems routinely have far more candidate predictors than observations: genomics with tens of thousands of genes and a few hundred patients, signal recovery from far fewer measurements than the signal's ambient dimension, image reconstruction from an undersampled set of linear projections. In every such setting the classical least-squares estimator is either undetermined or hopelessly noisy, and the ordinary theory of linear regression, built for $n \gg d$, has nothing to say.

The Lasso — $\ell_1$-penalized least squares, introduced by Tibshirani (1996) — is the workhorse response: penalize the least-squares objective by the $\ell_1$-norm of the coefficient vector, which both drives many coordinates exactly to zero and remains a convex, tractable program. What is far from obvious a priori is that this convex relaxation is not just computationally convenient but statistically correct: under a condition on the design matrix, its estimation error is controlled at a rate matching what one could hope for even knowing the true support in advance. Wainwright's High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 7, gives the deterministic backbone of this guarantee — the part of the argument that holds for any noise vector and any design matrix satisfying a single geometric condition, before any probability is introduced.

Setting

Consider the linear model $y = X\theta^* + w$, where $X \in \mathbb R^{n\times d}$ is a known design matrix, $\theta^* \in \mathbb R^d$ is an unknown coefficient vector, and $w \in \mathbb R^n$ is a noise vector, observed together with the response $y \in \mathbb R^n$. Write $\|\theta\|_1 := \sum_{j=1}^d|\theta_j|$ and $\|v\|_\infty := \max_j |v_j|$. The Lagrangian Lasso is the convex program

$$\hat\theta \in \operatorname*{arg\,min}_{\theta \in \mathbb R^d} \left\{ \frac{1}{2n}\|y - X\theta\|_2^2 + \lambda_n \|\theta\|_1 \right\},$$

with regularization parameter $\lambda_n > 0$ chosen by the user.

Say $\theta^*$ is supported on $S \subseteq \{1,\dots,d\}$ if $\theta^*_j = 0$ for every $j \notin S$, and write $|S| = s$ for its sparsity. For a subset $S$ and a constant $\alpha \ge 1$, the cone

$$C_\alpha(S) := \{\Delta \in \mathbb R^d \mid \|\Delta_{S^c}\|_1 \le \alpha \|\Delta_S\|_1\}$$

collects the directions in which an estimation error concentrated near the true support can plausibly point. The matrix $X$ satisfies the restricted eigenvalue (RE) condition over $S$ with parameters $(\kappa,\alpha)$ if

$$\frac{1}{n}\|X\Delta\|_2^2 \ge \kappa \|\Delta\|_2^2 \qquad \text{for all } \Delta \in C_\alpha(S).$$

Ordinarily, when $d > n$, the quadratic cost's Hessian $X^TX/n$ is rank-deficient and has a large flat subspace, so no uniform positive-curvature bound like this can hold over all of $\mathbb R^d$; the RE condition asks for curvature only along the cone $C_\alpha(S)$ that the Lasso's own optimality actually forces its error into.

The companion notion — the restricted nullspace property, $C_1(S) \cap \mathrm{null}(X) = \{0\}$ — is the noiseless analogue: it is exactly the condition under which the $\ell_1$-relaxed basis pursuit program $\min_\theta \|\theta\|_1$ s.t. $X\theta = y$ exactly recovers every $S$-sparse $\theta^*$ from $y = X\theta^*$ (Theorem 7.8). A small pairwise incoherence $\delta_{PW}(X) := \max_{j,k} |\langle X_j,X_k\rangle/n - \mathbb 1[j=k]|$ is one simply-checked sufficient condition for it (Proposition 7.9).

Formalization targets

Goal (Theorem 7.13(a) and its final sentence)

Under (A1) $\theta^*$ supported on $S$, $|S|=s$, and (A2) $X$ satisfies the RE condition over $S$ with parameters $(\kappa,3)$: for any $\hat\theta$ solving the Lagrangian Lasso with $\lambda_n \ge 2\|X^Tw/n\|_\infty$,

$$\|\hat\theta - \theta^*\|_2 \le \frac{3}{\kappa}\sqrt{s}\,\lambda_n, \qquad \|\hat\theta - \theta^*\|_1 \le 4\sqrt{s}\,\|\hat\theta-\theta^*\|_2.$$

Milestones

• Theorem 7.8. The restricted nullspace property is equivalent to exact recovery by basis pursuit for every $S$-sparse vector.
• Proposition 7.9. $\delta_{PW}(X) \le 1/(3s)$ implies the restricted nullspace property for every $S$ with $|S|\le s$.

Significance

The bound is the deterministic core underneath every high-dimensional consistency guarantee for the Lasso: once a statistician checks that a particular random design (Gaussian, sub-Gaussian, or otherwise) satisfies the RE condition with high probability, and bounds $\|X^Tw/n\|_\infty$ using concentration of the noise, this one inequality converts directly into a rate — Wainwright's own Examples 7.14–7.15 do exactly this for the classical Gaussian linear model and for compressed sensing. It also isolates why the Lasso is competitive with an oracle that already knows the support: the rate $\sqrt{s/n}$ (up to log factors, once $\lambda_n$ is instantiated) is the same order one would get regressing only on the $s$ true coordinates.

The theorem is already proved in the source; this mission's contribution is a machine-checked formal statement (and, eventually, proof) of the bound together with its two supporting structural results, in a form that composes with the rest of this book's formalized chapters and with any future formalization of the concentration arguments (Chapters 2–6) that supply $\lambda_n$'s numerical value in specific models.

Difficulty

The proof is short but every step leans on getting the cone membership exactly right. The first hurdle is showing the error $\Delta := \hat\theta - \theta^*$ lands in $C_3(S)$ at all — this needs the Lagrangian basic inequality (from $\hat\theta$'s optimality against $\theta^*$), not the simpler constrained-Lasso argument used for parts (b)/(c), and the constant $3$ (not $1$) comes precisely from the factor of $2$ in the $\lambda_n$ bound combined with Hölder's inequality on the noise term. A tempting shortcut is to assume the uniform curvature bound (7.24), $\|X\Delta\|_2^2/n \ge \kappa\|\Delta\|_2^2$ for all $\Delta \ne 0$ — but in the regime $d > n$ this uniform bound is never satisfiable, since $X^TX/n$ has a $(d-n)$-dimensional null space; the entire point of the restricted eigenvalue condition is to demand curvature only on the cone the optimality argument already produces.

Formalization scope

$X$, $\theta^*$, $\hat\theta$, $w$ are unconstrained vectors/matrices over Fin n/Fin d-indexed reals; $S$ is a Finset (Fin d). The RE condition's constant $\kappa$ is required positive, since the book divides by it throughout the discussion of Theorem 7.13 even though Definition 7.12 itself states the condition schematically; $\alpha=3$ is fixed to the book's own value, not a free parameter of the goal. The $\ell_\infty$- and pairwise-incoherence suprema are real iSups over finite index types, which default to Mathlib's junk value $0$ at dimension $0$ — a degenerate corner with no vector to measure, not a trivializing case of the theorem's actual content. A trivializing formalization would drop the final-sentence $\ell_1$-bound as "a trivial Cauchy–Schwarz corollary" or silently substitute the stronger, later-defined restricted isometry property for the restricted eigenvalue condition; this mission does neither. Parts (b) (constrained Lasso) and (c) (relaxed basis pursuit) of Theorem 7.13, and the primal–dual-witness support-recovery result (Theorem 7.21), are out of this mission's scope; a full-strength companion mission covering them, including the RIP-based Proposition 7.11 and the random-design certification Theorem 7.16, is natural future work.

Selected references

• Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 7. DOI: 10.1017/9781108627771.
• Tibshirani, R. "Regression shrinkage and selection via the Lasso." Journal of the Royal Statistical Society: Series B, 58(1), 1996, 267–288.
• Chen, S. S., Donoho, D. L., Saunders, M. A. "Atomic decomposition by basis pursuit." SIAM Journal on Scientific Computing, 20(1), 1998, 33–61.

From "larger" to "larger in every direction"

Chapter I's usual stochastic order compares two real-valued random variables by "how large" they tend to be. Chapter VI lifts the same idea to random vectors: $X$ is smaller than $Y$ in the usual multivariate stochastic order if $X$ is less likely than $Y$ to land in any upper set of $\mathbb{R}^n$ — any region defined by "at least this large in every coordinate." This mission formalizes that order and its two founding characterizations: a coupling theorem (the direct $n$-dimensional generalization of Chapter I's own coupling theorem) and a common-source representation, plus two closure properties that make the order usable in practice.

The usual multivariate stochastic order

Let $X$ be a random vector taking values in $\mathbb{R}^n$ on a probability space $(\Omega,\mu)$, and let $Y$ be a random vector taking values in $\mathbb{R}^n$ on a (possibly different) probability space $(\Omega',\nu)$. $X$ is smaller than $Y$ in the usual multivariate stochastic order, written $X \le_{st} Y$, if

$$P\{X\in U\} \le P\{Y\in U\} \quad \text{for every upper set } U\subseteq\mathbb{R}^n,$$

where an upper set is one closed upward under the coordinatewise partial order on $\mathbb{R}^n$ ($x\le y$ iff $x_i\le y_i$ for every $i$). Equivalently, $X\le_{st}Y$ iff $E[\varphi(X)]\le E[\varphi(Y)]$ for every increasing $\varphi:\mathbb{R}^n\to\mathbb{R}$ (increasing with respect to that same coordinatewise order) for which the two expectations exist — the form this mission drafts as the definition, exactly parallel to the univariate order's own equivalent form.

Formalization targets

Goal: the coupling characterization (Theorem 6.B.1)

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

This is the direct $n$-dimensional generalization of Chunk 01's Theorem 1.A.1: a joint law on the random vectors' shared space realizing $X\le_{st}Y$ as an almost-sure coordinatewise inequality between copies. The book does not give this direction's proof here (an explicit construction appears later, in a special case irrelevant to a statements-only mission), and the claim is exactly as citable either way.

Supporting milestones

• Theorem 6.B.2, the common-source restatement: $X\le_{st}Y$ iff there is a real-valued random variable $Z$ and $\mathbb{R}^n$-valued functions $\psi_1\le\psi_2$ (coordinatewise, at every $z\in\mathbb{R}$) with $X=_{st}\psi_1(Z)$, $Y=_{st}\psi_2(Z)$ — the multivariate analogue of Theorem 1.A.2, an immediate restatement of the goal.
• Theorem 6.B.16(b), closure under conjunctions: independent $X_i\le_{st}Y_i$ ($i=1,\dots,m$) give $\psi(X_1,\dots,X_m)\le_{st}\psi(Y_1,\dots,Y_m)$ for any increasing $\psi:\mathbb{R}^k\to\mathbb{R}$ — note the codomain $\mathbb{R}$, so this closure conclusion is itself the univariate order applied to vector-valued inputs. Specializing $\psi$ to a coordinatewise sum gives closure under convolutions.
• Theorem 6.B.16(c), closure under marginalization: $X\le_{st}Y$ implies $X_I\le_{st}Y_I$ for every sub-index set $I\subseteq\{1,\dots,n\}$ — a special case of part (b), included separately for its own simple, widely-used content.

Significance

The usual multivariate stochastic order is the natural tool for comparing random vectors — costs, resource-usage profiles, portfolio returns — that must be ranked simultaneously across several coordinates rather than reduced to a single scalar summary first. It underlies simulation comparisons (via the coupling and common-source characterizations, both constructive), reliability comparisons of multi-component systems (whose component lifetimes are naturally vector-valued), and comparative-statics arguments in queueing and inventory models with several state variables. The closure properties are what make the order compositional: conjunction closure says a vector-by-vector comparison of independent inputs survives any coordinatewise-increasing post-processing, and marginalization closure says a joint comparison restricts consistently to any sub-collection of coordinates — together they are the two properties an analyst reaches for first when reducing a multivariate comparison to a more tractable one.

No platform prior art exists: GET /theorems?q=stochastic+order and q=coupling return zero genuine hits (checked at this book's triage time, re-confirmed this session). This mission restates the usual multivariate stochastic order and its two founding theorems as a self-contained foundation, in the same spirit as Chunk 01's univariate mission but independently drafted, since drafts cannot import each other's Lean.

Difficulty

The chief formalization risk this chapter's own brief flags is conflating "increasing" for $\varphi:\mathbb{R}^n\to\mathbb{R}$ with some order other than the coordinatewise one (a total order via a fixed embedding, or a lexicographic order): the book's order on $\mathbb{R}^n$ is always the componentwise partial order, and Mathlib gives Fin n → ℝ exactly that order by default (its Pi/product order), so Monotone φ for φ : (Fin n → ℝ) → ℝ already means what the book means with no extra predicate to get wrong — but it would be easy to instead encode ℝ^n-valued objects some other way (e.g. a fixed linear functional into ℝ) that silently swaps in a different, weaker order. The second risk is Theorem 6.B.16(b)'s literal codomain: the book states $\psi:\mathbb{R}^k\to\mathbb{R}$ (scalar), so the closure conclusion is a genuinely univariate stochastic-order statement about $\psi$ applied to vector inputs, not a vector-to-vector closure (that is part (a), not drafted here) — stating it as a multivariate conclusion by mistake would silently strengthen a theorem the book does not claim.

Formalization scope

Random vectors are drafted as functions into Fin n → ℝ from arbitrary measurable spaces, which inherit Mathlib's default coordinatewise (Pi) order — the same order the book uses throughout this chapter, requiring no separate order predicate. MultivariateOrder μ ν X Y quantifies over φ : (Fin n → ℝ) → ℝ with Monotone φ in that order and Integrable (φ ∘ X) μ/Integrable (φ ∘ Y) ν stated inside the ∀, exactly matching "for which the expectations exist." Equality in law is ProbabilityTheory.IdentDistrib. Theorem 6.B.2's random variable $Z$ is drafted as $\mathbb{R}$-valued specifically (not an arbitrary-type common source), matching the book's own "for all $z\in\mathbb{R}$" quantification exactly.

Theorem 6.B.16(b) is drafted for a common dimension $n$ across all $X_i,Y_i$ rather than the book's per-$i$ dimension $k_i$: the concatenated input then lives in Fin m → Fin n → ℝ (nested Pi types, carrying the coordinatewise order on $\mathbb{R}^{mn}$ exactly as needed), avoiding a dependent-sum concatenation of vectors of genuinely different lengths that a mission of this size does not justify. This is the "closed under convolutions" special case the book itself names as a corollary of the general statement, not a different claim — but it is a genuine restriction of scope, recorded here rather than silently applied, and the general varying-dimension statement is left for a future pass (see STATUS.md). The theorem's conclusion is stated as the univariate order's own defining inequality on ℝ (∀ x, μ {ω | x < ψ(X_∙ ω)} ≤ ν {ω | x < ψ(Y_∙ ω)}), restated locally rather than importing Chunk 01's UsualOrder, since drafts cannot import another mission's definitions. Theorem 6.B.16(c)'s sub-index set $I\subseteq\{1,\dots,n\}$ of size $k$ is encoded as an injective reindexing r : Fin k → Fin n, with $X_I,Y_I$ drafted as X, Y precomposed coordinatewise with r, matching the book's own subvector notation (6.A.1) exactly.

A trivializing formalization this mission rules out: drafting MultivariateOrder with an order on Fin n → ℝ other than the coordinatewise one (for instance, a fixed linear functional collapsing the vector to a scalar and reusing the univariate order), which would silently state a different, generally weaker order under the same name; and drafting Theorem 6.B.16(b)'s conclusion with a vector-valued (rather than the book's literal scalar-valued) $\psi$, which would silently strengthen a theorem the book states only for real-valued $\psi$. This mission draws on no platform prior art (searches for "stochastic order" and "coupling" as of 2026-09-18 return zero genuine matches). Reusable beyond this mission: the MultivariateOrder definition pattern and its coupling/common-source characterization parallel Chunk 01's univariate pair closely enough that a future chapter needing a multivariate order's own coupling theorem (Chapter VII's multivariate convex order is the direct next instance in this series) could restate the same shape with minimal adaptation.

Selected references

• M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007, Chapter 6 (Multivariate Stochastic Orders), §6.A–6.B. https://doi.org/10.1007/978-0-387-34675-5
• This series' Chunk 01 (StochasticOrders.Usual), for the univariate usual stochastic order and its coupling/common-source characterizations this chapter directly generalizes.

Motivation

Many questions in high-dimensional probability reduce to bounding the expected supremum of a random process $(X_t)_{t\in T}$ — the maximum, over an entire indexed family of random variables, of how large any one of them can get. When $T$ is finite this is routine (a union bound over $|T|$ terms suffices), but the interesting cases have $T$ infinite, even uncountable: a supremum over a continuum of test functions, a norm expressed as a supremum over a sphere, or an empirical process indexed by a whole class of functions. A naive union bound is unusable here, since $|T|$ is infinite.

R. M. Dudley's 1967 entropy bound (R. M. Dudley, The sizes of compact subsets of Hilbert space and continuity of Gaussian processes, Journal of Functional Analysis 1 (1967), 290–330) resolved this for Gaussian processes, controlling the expected supremum purely in terms of the metric entropy of $T$ — how many balls of radius $\varepsilon$ are needed to cover $T$, at every scale $\varepsilon$. The technique behind the proof, chaining, builds a sequence of increasingly fine finite approximations to $T$ and telescopes the resulting bounds; it is one of the central tools of the field, reused throughout empirical process theory, statistical learning theory (via Vapnik-Chervonenkis theory), and non-asymptotic random matrix theory. This mission formalizes the chapter's generalization of Dudley's bound beyond Gaussian processes, to any process with sub-gaussian increments, together with the purely combinatorial Sauer-Shelah lemma that the chapter's applications to statistical learning theory build on.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$. A random process is a family $(X_t)_{t\in T}$ of real random variables on $(\Omega,\mathcal F,P)$ indexed by an arbitrary set $T$, with no independence or measurability-of-the-supremum assumed between different $t$'s. Since $\sup_{t\in T}X_t(\omega)$ need not be measurable in $\omega$ for a general index set $T$, its expectation is understood — following the book's own convention, set once in Chapter 7 and reused throughout — through the process's finite-dimensional marginals:

$$\mathbb E\sup_{t\in T}X_t \;:=\; \sup_{T_0\subseteq T\text{ finite, nonempty}}\ \mathbb E\max_{t\in T_0}X_t.$$

Now fix a metric $d$ on $T$, making $(T,d)$ a metric space. The covering number $N(T,d,\varepsilon)$, for $\varepsilon>0$, is the smallest cardinality of a finite $\varepsilon$-net of $T$: a finite set $N\subseteq T$ such that every point of $T$ lies within distance $\varepsilon$ of some point of $N$ (or $N(T,d,\varepsilon):=\infty$ if no finite $\varepsilon$-net exists). The quantity $\log N(T,d,\varepsilon)$ is the metric entropy of $T$ at scale $\varepsilon$: it measures how large $T$ looks when resolved only down to scale $\varepsilon$.

A process $(X_t)_{t\in T}$ has sub-gaussian increments with parameter $K\ge0$ if

$$\|X_t-X_s\|_{\psi_2}\;\le\;K\,d(t,s)\qquad\text{for all }t,s\in T,$$

where $\|\cdot\|_{\psi_2}$ is the sub-gaussian (Orlicz) norm of Chapter 2: the smallest $u>0$ with $\mathbb E\exp((X_t-X_s)^2/u^2)\le2$. This says the increments of the process are controlled by the metric $d$ the way a Gaussian process's increments are controlled by its own canonical metric $d(t,s):=\|X_t-X_s\|_{L^2}$ — but without assuming $(X_t)_{t\in T}$ is Gaussian.

A class of Boolean functions $F$ on a set $\Omega$ shatters a subset $\Lambda\subseteq\Omega$ if every function $g:\Lambda\to\{0,1\}$ arises as the restriction to $\Lambda$ of some $f\in F$. The VC (Vapnik-Chervonenkis) dimension $\mathrm{vc}(F)$ is the largest cardinality of a subset of $\Omega$ shattered by $F$ (or $\infty$ if arbitrarily large finite subsets, or an infinite one, are shattered) — a purely combinatorial measure of how rich the class $F$ is.

Formalization targets

Goal (Theorem 8.1.3, Dudley's integral inequality)

$$\exists\,C>0:\quad\mathbb E\sup_{t\in T}X_t\;\le\;CK\int_0^\infty\sqrt{\log N(T,d,\varepsilon)}\;d\varepsilon$$

for every mean-zero random process $(X_t)_{t\in T}$ on a metric space $(T,d)$ with sub-gaussian increments parameter $K\ge0$, whenever the integral is finite. $C$ is the book's own unnamed absolute constant, never depending on $T$, $K$, or the process. This is the weakest stable form of the claim: no numeral is hard-coded for $C$, and the statement asks only for the shape of the bound, matching what the book actually proves.

Milestone (Theorem 8.3.16, Sauer-Shelah lemma)

$$|F|\;\le\;\sum_{k=0}^{d}\binom nk\;\le\;\left(\frac{en}{d}\right)^{d},\qquad d:=\mathrm{vc}(F),$$

for every class $F$ of Boolean functions on a finite $n$-point set $\Omega$. This is a purely combinatorial fact, with no probability involved, but it is the bridge (via the covering-number bound Theorem 8.3.18, outside this mission's scope) between the chapter's Dudley-inequality engine and its statistical-learning applications — a bound on how large a finite class of Boolean functions can be, in terms of a single combinatorial complexity parameter.

Significance

Dudley's inequality is, in the book's own words, "the main result" of the chaining chapter: it converts a purely geometric quantity — the metric entropy of an index set, computable in many cases from covering-number estimates already available for balls, ellipsoids, and other convex bodies — into a probabilistic control on the size of a random process indexed by that set. This is what lets later chapters (uniform laws of large numbers over function classes, the matrix deviation inequality, the Dvoretzky-Milman theorem on almost-spherical sections of convex bodies) bound suprema over infinite, even uncountable, index sets without ever performing a union bound. The bound is also known to be tight only up to a logarithmic factor in general — Sudakov's minoration inequality (Chapter 7) gives a matching lower bound for Gaussian processes, and the book's own Exercise 8.1.12 exhibits a set where the two bounds genuinely diverge — so the constant $C$ here cannot in general be sharpened away.

The Sauer-Shelah lemma is one of the two founding results of VC theory (together with the Glivenko-Cantelli-type uniform convergence it feeds into), independently discovered by Vapnik and Chervonenkis, Sauer, and Shelah in the early 1970s; it underlies the sample-complexity bounds of statistical learning theory (a hypothesis class with finite VC dimension is PAC-learnable) and, through Theorem 8.3.18, gives one of the two standard routes (the other being direct combinatorial counting) to bounding covering numbers of infinite function classes.

Both results are decades old and have long-established, standard proofs; no open mathematical question is being formalized. What this mission contributes is the machine-checked statement infrastructure — the goal and the Sauer-Shelah milestone, together with the definitions (CoveringNumber, ProcessESup, Shatters, VcDim) a faithful Lean rendering of either result needs — for a solver to close with a proof. No formalization of Dudley's inequality or the Sauer-Shelah lemma is known to exist on the platform prior to this mission.

Difficulty

The natural first idea for bounding $\mathbb E\sup_{t\in T}X_t$ is a single-scale $\varepsilon$-net argument: replace $T$ by a finite $\varepsilon$-net, bound the maximum over the (finite) net by a union bound using the sub-gaussian tail, and separately bound the error of replacing $T$ by the net using the Lipschitz-in-probability control the sub-gaussian-increments hypothesis gives. This works, but it only ever sees $T$ at one fixed resolution $\varepsilon$, and optimizing over $\varepsilon$ afterward gives a bound with an extra $\sqrt{\log(1/\varepsilon)}$-type loss that does not match Dudley's inequality. The actual difficulty is genuinely multi-scale: chaining builds a whole sequence of nets at dyadic scales $\varepsilon=2^{-k}$ simultaneously, connects each point of $T$ to its nearest net point at every scale to form a "chain" of successive approximations back to a single fixed basepoint, and telescopes the resulting sum of increments — turning $X_t$ itself into a sum of differences between successive links of the chain, each individually well controlled by the sub-gaussian hypothesis at its own scale. Passing from the resulting discrete sum over dyadic scales (Theorem 8.1.4) to the continuous integral of the goal is a further, separate technical step.

For the Sauer-Shelah lemma, the natural first idea — bound $|F|$ directly by counting — has no obvious purchase on an arbitrary class of Boolean functions. The actual argument goes through Pajor's lemma, which reduces bounding $|F|$ to counting the shattered subsets of $\Omega$ instead of the functions in $F$ themselves; only then does the cardinality bound $d=\mathrm{vc}(F)$ on shattered sets become directly usable, via a binomial-sum estimate.

Formalization scope

CoveringNumber T ε is ℕ∞-valued (ℕ∞ = WithTop ℕ), defined as the infimum, over the subtype of finite $\varepsilon$-nets of the whole type T (an instance of MetricSpace T), of their cardinality; the infimum of the empty family in this complete lattice is ⊤, reproducing "$N:= \infty$ if no finite net exists" with no case split. ProcessESup is EReal-valued, defined as the supremum over finite nonempty $T_0\subseteq T$ of the Bochner integral of the finite max — EReal, not ℝ, because a real-valued supremum would silently return the junk value $0$ if the family of marginal expectations were unbounded above. Shatters and VcDim are direct transcriptions of Definition 8.3.1, with VcDim valued in ℕ∞ via a supremum of Set.encard over the (always-nonempty, since $\varnothing$ is trivially shattered) subtype of shattered subsets. The goal's mean-zero hypothesis is stated as Integrable (X t) P ∧ ∫ X t = 0 rather than the bare equation, since a non-integrable variable's Bochner integral is 0 in Mathlib by convention regardless of its true mean — a bare-equation hypothesis would let a non-mean-zero, non-integrable process satisfy the theorem vacuously. Two further hypotheses make explicit what the book's own displayed statement treats as understood without spelling out: that $N(T,d,\varepsilon)$ is finite for every $\varepsilon>0$ (total boundedness of $T$), and that the resulting integrand is integrable on $(0,\infty)$ — both hold whenever $T$ is totally bounded, since the integrand vanishes once $\varepsilon\ge\mathrm{diam}(T)$, so neither hypothesis excludes any case the book's own proof does not also need. [Nonempty T] excludes the degenerate empty index set. The absolute constant $C$ is existentially quantified ahead of every type, instance, and hypothesis it is uniform over, and pinned to no numeral, matching "$C$ is an absolute constant" — a formalization hard-coding a specific numeral for $C$ would be invalidated by the next sharper constant in the literature and would not match what the book proves.

A trivializing formalization of the Sauer-Shelah lemma would fix $\mathrm{vc}(F)$ at a hard-coded small value, or drop the second (exponential) inequality in favor of the weaker first one; this mission's statement keeps both inequalities, with $d$ genuinely computed from VcDim, and handles the $d=0$ boundary (where the exponential bound's base involves a division by zero under Lean's x/0=0 convention) explicitly rather than excluding it, since x^0=1 still recovers the book's correct bound $|F|\le1$ there.

This mission covers Theorem 8.1.3 and Theorem 8.3.16 only; Theorem 8.3.18 (covering numbers via VC dimension) and Theorem 8.2.3 (the uniform law of large numbers, the chapter's direct application of Dudley's inequality) are left out, not approximated, for lack of the additional empirical- process measurability machinery — the class of Lipschitz functions of Eq. (8.22), measurability of the resulting empirical process — that a faithful statement of either would need beyond what this mission's items already provide. CoveringNumber and ProcessESup are reusable by any later chapter needing a metric space's covering numbers or a general random process's expected supremum (this book's own Chapters 7, 9, and 11 all use one or both); Shatters and VcDim are reusable by any later development of VC theory or statistical learning theory. Solvers' contributions are welcome on: the chaining argument itself (the mission's hardest open leaf, via the discrete dyadic form of Theorem 8.1.4), Pajor's lemma underlying Sauer-Shelah, and the binomial-sum estimate closing its second inequality.

Selected references

• R. M. Dudley, The sizes of compact subsets of Hilbert space and continuity of Gaussian processes, Journal of Functional Analysis 1 (1967), 290–330. https://doi.org/10.1016/0022-1236(67)90017-1
• N. Sauer, On the density of families of sets, Journal of Combinatorial Theory, Series A 13 (1972), 145–147. https://doi.org/10.1016/0097-3165(72)90019-2
• V. N. Vapnik, A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability & Its Applications 16 (1971), 264–280. https://doi.org/10.1137/1116025
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 8. https://doi.org/10.1017/9781108231596

Motivation

Chapter 2 of Steinwart & Christmann, Support Vector Machines, showed the hinge loss controls the classification loss (Zhang's inequality, Theorem 2.31). That result was special to one target/surrogate pair. Chapter 3 asks the question in general: given any target loss $L_{\mathrm{tar}}$ (the loss whose risk we actually care about) and any surrogate loss $L_{\mathrm{sur}}$ (the loss a learning algorithm actually minimizes, chosen for tractability — convexity, differentiability), when does controlling the excess $L_{\mathrm{sur}}$-risk control the excess $L_{\mathrm{tar}}$-risk? The book's answer factors the question through a purely pointwise object, the calibration function, that depends only on the two losses and a single label distribution — not on the learning problem's ambient space $X$ or the unknown data-generating distribution $P$ at all.

Setting

Fix a measurable space $X$ and a closed label set $Y \subset \mathbb R$. For a loss $L : X \times Y \times \mathbb R \to [0,\infty)$, a distribution $Q$ on $Y$, and $x \in X$, the inner $L$-risk is $C_{L,Q,x}(t) := \int_Y L(x,y,t)\,dQ(y)$ and the minimal inner risk is $C^*_{L,Q,x} := \inf_t C_{L,Q,x}(t)$ (Definition 3.3). Eq. (3.5) rewrites the ordinary $L$-risk of $f$ against a full distribution $P$ on $X \times Y$ as $R_{L,P}(f) = \int_X C_{L,P(\cdot\mid x),x}(f(x))\,dP_X(x)$: the outer risk is an average of inner risks over the $X$-marginal, one inner risk per conditional distribution $P(\cdot\mid x)$. The set of $\varepsilon$-approximate minimizers is $M_{L,Q,x}(\varepsilon) := \{t : C_{L,Q,x}(t) < C^*_{L,Q,x} + \varepsilon\}$ (Definition 3.5).

The calibration function $\delta_{\max}(\varepsilon, Q, x)$ of a pair $(L_{\mathrm{tar}}, L_{\mathrm{sur}})$ (Definition 3.13) is the largest $\delta$ such that every $\delta$-approximate surrogate minimizer is already an $\varepsilon$-approximate target minimizer: $\delta_{\max}( \varepsilon, Q, x) := \inf\{C_{L_{\mathrm{sur}},Q,x}(t) - C^*_{L_{\mathrm{sur}},Q,x} : t \notin M_{L_{\mathrm{tar}},Q,x}(\varepsilon)\}$ when $C^*_{L_{\mathrm{sur}},Q,x} < \infty$, and $\infty$ otherwise. $L_{\mathrm{sur}}$ is $L_{\mathrm{tar}}$-calibrated with respect to a set $\mathcal Q$ of label distributions if $\delta_{\max}(\varepsilon, Q, x) > 0$ for every $\varepsilon \in (0,\infty]$, $Q \in \mathcal Q$, $x$ — one $\delta_{\max}$ working uniformly over the whole class $\mathcal Q$, not just a single fixed distribution.

Formalization targets

Goal: Corollary 3.19 (calibration $\iff$ uniform risk implication, bounded target)

$$L_{\mathrm{sur}}\text{ is }L_{\mathrm{tar}}\text{-calibrated w.r.t. }\mathcal Q \iff \forall \varepsilon \in (0,\infty],\ \forall P \text{ of type } \mathcal Q \text{ with } R^*_{L_{\mathrm{sur}},P}<\infty,\ \exists \delta \in (0,\infty],\ \forall f,$$ $$R_{L_{\mathrm{sur}},P}(f) < R^*_{L_{\mathrm{sur}},P}+\delta \implies R_{L_{\mathrm{tar}},P}(f) < R^*_{L_{\mathrm{tar}},P}+\varepsilon$$

when $L_{\mathrm{tar}}$ is bounded. This is the mission's capstone: a purely pointwise, $P$-independent condition (calibration) is shown equivalent to a whole-class-of-distributions statistical guarantee, not merely necessary for it.

Milestones (attack order)

1. Lemma 3.4 — the Bayes risk is the integral of the minimal inner risks: $R^*_{L,P} = \int_X C^*_{L,P(\cdot\mid x),x}\,dP_X(x)$, and $x \mapsto C^*_{L,P(\cdot\mid x),x}$ is measurable. Foundational: it is what makes minimizing risk pointwise, one conditional distribution at a time, a valid strategy at all.
2. Lemma 3.11 — for $\varepsilon \in (0,\infty]$, $C^*_{L,P(\cdot\mid x),x} < \infty$ for $P_X$-a.a. $x$ iff a measurable $\varepsilon$-approximate minimizer selection $f$ exists. Directly invoked in Theorem 3.17's own proof.
3. Lemma 3.14 — the calibration function traps the surrogate's $\delta_{\max}(\varepsilon)$ -approximate minimizers inside the target's $\varepsilon$-approximate minimizers (and no larger $\delta$ does), plus the pointwise inequality Eq. (3.16), $\delta_{\max}(C_{L_{\mathrm{tar}},Q,x}(t)-C^*_{L_{\mathrm{tar}},Q,x}, Q, x) \le C_{L_{\mathrm{sur}},Q,x}(t)-C^*_{L_{\mathrm{sur}},Q,x}$. Directly invoked in Theorem 3.17's proof ("By part i) of Lemma 3.14...").
4. Theorem 3.17 — for a single fixed $P$, an a.s.-strictly-positive calibration function is necessary for the risk implication (3.18), and sufficient under an added domination condition (Eq. (3.19), a $P_X$-integrable envelope on the excess inner target risk).

Theorem 3.22 (BRIEF.md's originally recommended goal — the fully quantitative uniform calibration inequality, using a Fenchel-Legendre biconjugate) was not attempted; see STATUS.md for the reason and the fallback taken instead.

Significance

Corollary 3.19 is the chapter's answer to "is calibration actually useful, or just necessary?" Theorem 3.17 alone only rules out non-calibrated surrogates; Corollary 3.19 shows that for the two most important bounded target losses in the book — the classification loss and the density-level- detection loss — calibration is exactly the right test, with no gap between necessity and sufficiency. Concretely: the book's Example 3.16 computes that both the least-squares and hinge losses are calibrated surrogates for the classification loss for every $\eta \in [0,1]$, and this corollary is what turns that pointwise computation into the qualitative consistency guarantee "minimizing empirical hinge risk is a statistically sound way to approach the empirical classification risk," ahead of the sharper quantitative form Zhang's inequality already supplies for that one pair (Theorem 2.31) and Theorem 3.22 supplies in general.

Difficulty

The apparatus itself — inner risks, approximate-minimizer sets, the calibration function — is the chapter's real content, and getting the finite/infinite distinction right throughout is the chapter's central technical difficulty: Lemma 3.11's whole point is that "$C^*_{L,P(\cdot\mid x),x}<\infty$ for a.e. $x$" is a genuine dichotomy, not a standing assumption, and the calibration function's own definition branches on exactly this finiteness. A real-valued, junk-at-infinity convention for risks (as used in the 01-loss-functions mission, where losses were always bounded) would silently collapse this dichotomy and trivialize Lemma 3.11 and much of Theorem 3.17's content. The definitions in this mission are built in ENNReal (Lean's $[0,\infty]$) throughout specifically to avoid this trap.

Formalization scope

$X$ is an arbitrary measurable space; label distributions $Q$ range over Measure ℝ with no IsProbabilityMeasure requirement in InnerRisks/CalibrationFunction/Lemma 3.14 — re-reading Lemma 3.14's proof directly (p. 59) found no step that uses $Q$ having total mass $1$, so this hypothesis is dropped as a disclosed generalization there, matching the convention this series already used for Lemma 2.23's convexity hypothesis. Wherever a genuine distribution $P$ on $X \times Y$ is required (Lemma 3.4, Lemma 3.11, Theorem 3.17, Corollary 3.19), $P$ is represented as a pair $(P_X, \kappa)$ — an $X$-marginal $P_X$ and a measurable family $\kappa : X \to \text{Measure } \mathbb R$ of conditional distributions $P(\cdot\mid x)$ — with ∀ x, IsProbabilityMeasure (κ x) added explicitly at each such use site, since the (PX, κ) representation does not force this by its types alone. X being a complete measurable space (required by all four theorem-kind items but Lemma 3.14) is rendered as the disclosed sufficient condition "$\exists$ a probability measure $\mu$ for which $\mu$-null sets have every subset measurable" rather than the book's exact universal-completion equality — see Def_..._IsCompleteMeasurableSpace's own note. $\varepsilon$ ranges over ENNReal throughout, so "$\varepsilon \in [0,\infty]$"/"$(0,\infty]$" need no narrowing, unlike this series' real-valued conventions elsewhere.

A trivializing formalization here would let IsCalibrated/the calibration function be an unconstrained hypothesis disconnected from innerRisk/approxMinimizers, or let κ/PX range freely with no link to outerRisk/bayesRisk as actually defined — both are ruled out since every item's statement is built compositionally from the same innerRisk/minInnerRisk/ approxMinimizers/outerRisk/bayesRisk definitions, traced back to Definitions 3.3, 3.5, 2.2 and 2.3 exactly as the book states them.

Loss, innerRisk/minInnerRisk/approxMinimizers, outerRisk/bayesRisk/IsOfType, and calibrationFunction/IsCalibrated are reusable beyond this mission: this series' 06- classification chunk restates this chapter's apparatus locally (per Hard Rule 9, drafts cannot import each other) when it reuses Chapter 3's calibration ideas for its own oracle inequality. Contributions completing the five sorrys are welcome; Theorem 3.22 itself (the fully quantitative version this mission's BRIEF.md recommended as the primary goal) remains a natural follow-up mission built on top of this one's definitions.

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 3, §§3.1-3.3, pp. 49-65).
• T. Zhang, "Statistical behavior and consistency of classification methods based on convex risk minimization," Annals of Statistics 32(1), 2004, pp. 56-85. https://doi.org/10.1214/aos/1079120130
• P. L. Bartlett, M. I. Jordan & J. D. McAuliffe, "Convexity, classification, and risk bounds," Journal of the American Statistical Association 101(473), 2006, pp. 138-156. https://doi.org/10.1198/016214505000000907

Motivation

Sums of independent random variables are well understood: Bernstein's inequality and its relatives give sharp, non-asymptotic tail bounds for $\sum_i a_i X_i$ whenever the $X_i$ are independent and light-tailed. Many quantities that arise in high-dimensional statistics and random matrix theory, however, are not linear but quadratic in an independent sample — the squared norm of a random vector after a linear transformation, a quadratic-form test statistic, the diagonal of a sample covariance matrix, or the number of edges cut by a random partition in a random graph. A quadratic form $X^\top A X = \sum_{i,j} A_{ij} X_i X_j$ is a sum with dependent terms: $X_iX_j$ and $X_iX_k$ share the factor $X_i$, so classical sum-of-independent-variables tools do not apply directly.

The Hanson-Wright inequality, first obtained by Hanson and Wright (1971) for sub-gaussian variables and later sharpened and popularized in this form by Rudelson and Vershynin (2013, "Hanson-Wright inequality and sub-gaussian concentration," Electronic Communications in Probability), closes this gap: it gives a concentration inequality for $X^\top A X$ around its mean with the same two-regime (sub-gaussian near the center, sub-exponential in the tail) shape as Bernstein's inequality for linear sums. It is now a standard tool wherever quadratic statistics of independent data are analyzed: covariance estimation, compressed sensing, randomized numerical linear algebra, and the analysis of random matrices more broadly draw on it routinely.

Setting

Fix a probability space and let $X = (X_1, \dots, X_n)$ be a random vector whose coordinates $X_1, \dots, X_n$ are independent, mean zero, and sub-gaussian: each $X_i$ has a finite sub-gaussian (Orlicz $\psi_2$) norm $\|X_i\|_{\psi_2}$, the smallest $t > 0$ with $\mathbb E \exp(X_i^2/t^2) \le 2$. Write $K = \max_i \|X_i\|_{\psi_2}$.

Let $A = (A_{ij})_{i,j=1}^n$ be an $n \times n$ real matrix, with no constraint on its diagonal, and form the quadratic form

$$X^\top A X = \sum_{i,j=1}^n A_{ij} X_i X_j.$$

Two matrix norms measure the size of $A$: the Frobenius norm $\|A\|_F = \bigl(\sum_{i,j} A_{ij}^2\bigr)^{1/2}$ (the Euclidean norm of $A$'s entries) and the operator (spectral) norm $\|A\| = \sup_{\|x\|_2=1} \|Ax\|_2$ (the largest singular value of $A$). Always $\|A\| \le \|A\|_F \le \sqrt{n}\,\|A\|$, so the two norms can differ by a factor as large as $\sqrt n$ — the gap between them is exactly what produces the inequality's two regimes below.

Formalization targets

Goal — Theorem 6.2.1 (Hanson-Wright inequality)

$$P\bigl\{\, |X^\top A X - \mathbb E\, X^\top A X| \ge t \,\bigr\} \;\le\; 2 \exp\!\left[-c \min\!\left(\frac{t^2}{K^4 \|A\|_F^2},\ \frac{t}{K^2 \|A\|}\right)\right] \qquad \text{for every } t \ge 0,$$

where $c > 0$ is an absolute constant, not depending on $n$, $X$, $A$, or $t$. Stating the constant only as "some absolute $c$" (rather than pinning it to a numeral) is deliberate: the book's own proof does not track a sharp value, and a goal that only asserts the shape of the bound survives any later improvement to $c$.

Significance

The result itself. Hanson-Wright turns a two-dimensional (in $i,j$) dependency structure into a one-dimensional concentration statement controlled by two scalar quantities, $\|A\|_F$ and $\|A\|$. This is what makes it usable: a practitioner bounding a quadratic statistic need only compute these two norms, not analyze the joint dependency structure of $\{X_iX_j\}$ directly. It specializes to Bernstein's inequality (Chapter 2 of this book) when $A$ is diagonal, and it underlies non-asymptotic guarantees for covariance estimation, the Johnson-Lindenstrauss lemma via a different route, and the concentration of Lipschitz functions of sub-gaussian vectors.

Formalizing it. The published proof of Hanson-Wright is not a single argument but a chain of four steps: a decoupling reduction (Section 6.1), a direct computation for Gaussian chaos (Lemma 6.2.2), a comparison lemma extending the Gaussian bound to general sub-gaussian vectors via a replacement trick (Lemma 6.2.3), and a final assembly that separates the diagonal part (handled by Bernstein's inequality) from the off-diagonal part (handled by decoupling and comparison). This mission formalizes the goal theorem's statement and the first, most reusable link in that chain — the decoupling machinery of Section 6.1, which reduces the analysis of the dependent chaos $X^\top A X$ to the independent-once-conditioned bilinear form $X^\top A X'$ — together with the chapter's separate contraction principle (Section 6.7), a general comparison tool for Rademacher-weighted sums used repeatedly in the book's later chaining chapters. The Gaussian MGF computation and the replacement-trick comparison lemma (Lemmas 6.2.2–6.2.3) are left as future milestones on top of this mission: they require Gaussian rotation invariance and the singular value decomposition of $A$, substantially more machinery than the milestones included here.

Difficulty

The obvious first idea — treat $X^\top A X = \sum_{i,j} A_{ij}X_iX_j$ as if it were a sum of independent terms and apply Bernstein's inequality termwise — fails immediately: the terms $A_{ij}X_iX_j$ for fixed $i$ are not independent across $j$, since they all share the factor $X_i$. Decoupling (Theorem 6.1.1) is the non-obvious fix: it replaces the off-diagonal chaos by a bilinear form $X^\top A X'$ in an independent copy $X'$, which genuinely does become a sum of independent terms once one of the two vectors is conditioned on. The price is a universal constant factor of $4$ and the restriction to diagonal-free matrices, which is exactly why the full Hanson-Wright proof must separate the diagonal contribution to $\mathbb E\,X^\top A X$ (handled directly by Bernstein's inequality, Chapter 2) before decoupling can be applied to what remains.

Formalization scope

Random variables and vectors are real-valued on an explicit probability space $(\Omega, \mathcal F, P)$. The sub-gaussian norm is HighDimProb.Concentration.subgaussianNorm, the Orlicz-$\psi_2$-norm definition already published for this series (01-concentration), reused here as a reference item rather than redefined. $K = \max_i \|X_i\|_{\psi_2}$ is written as a finite supremum over the coordinate index, ⨆ i, subgaussianNorm P (X i); because the index type is always a Fintype (Fin n), this supremum is well-defined and, at the degenerate index $n=0$, reduces to a true (if content-free) instance of the inequality rather than a vacuous or false one. The Frobenius and operator norms of $A$ are this mission's own frobeniusNorm and opNorm, stated directly from their defining formulas rather than through Mathlib's scoped matrix-norm typeclass instances, which are deliberately not global defaults (to avoid a diamond between the two norms) and so are unsuitable for a statement that needs both simultaneously. Every place the goal or a milestone integrates a quantity, that quantity is required Integrable, guarding against Mathlib's convention of returning 0 for the Bochner integral of a non-integrable function — without these hypotheses, a mean-zero or expectation hypothesis could hold vacuously, or a conclusion could hold trivially, for reasons having nothing to do with the book's mathematics.

The formalization deliberately does not restrict $A$'s diagonal in the goal theorem: doing so would collapse Hanson-Wright to a restatement of Bernstein's inequality for the special case of a diagonal matrix, discarding the chapter's actual content, which is handling the off-diagonal, genuinely quadratic dependence between coordinates. The diagonal-free restriction does appear, correctly, in the Decoupling theorem (6.1.1), whose proof needs it.

Reusable beyond this mission: frobeniusNorm and opNorm are needed by any future chapter using matrix norms (Chapter 4's random matrix norms, Chapter 9's matrix deviation inequality); the decoupling theorem and convex decoupling lemma are the standard entry point for any later formalization of chaos concentration; the contraction principle is reused throughout the book's chaining chapters (7 and 8). Welcome contributions include the Gaussian MGF and comparison lemmas (6.2.2–6.2.3) needed to complete a full proof of the goal theorem, and the two-sided version of Bernstein's inequality needed for the diagonal part of that proof.

Selected references

• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018. DOI: 10.1017/9781108231596.
• D. L. Hanson, F. T. Wright, "A bound on tail probabilities for quadratic forms in independent random variables," Annals of Mathematical Statistics 42 (1971), 1079–1083.
• M. Rudelson, R. Vershynin, "Hanson-Wright inequality and sub-gaussian concentration," Electronic Communications in Probability 18 (2013), no. 82, 1–9. https://arxiv.org/abs/1306.2872

Motivation

Binary classification asks for a rule that predicts a label $y \in \{-1,1\}$ from an observation $x$. The natural loss for this task, the classification loss $L_{\mathrm{class}}$, is a step function: minimizing its empirical average over a class of functions $f$ is generally NP-hard, because the objective is non-convex and discontinuous in $f$. Every practical classification algorithm — logistic regression, boosting, and the support vector machine this book is about — sidesteps this by minimizing a convex surrogate loss instead, such as the hinge loss $L_{\mathrm{hinge}}(y,t) := \max\{0, 1-yt\}$, and hoping that a small surrogate risk implies a small classification risk.

Zhang (2004) and Bartlett, Jordan & McAuliffe (2006) put this hope on a rigorous footing: for a wide class of convex surrogates, controlling the excess surrogate risk controls the excess classification risk, with an explicit quantitative relationship. Steinwart & Christmann, Support Vector Machines (Springer 2008, Information Science and Statistics), Chapter 2, develop the special case of the hinge loss in closed form as Theorem 2.31 ("Zhang's inequality"), the sharpest and most self-contained instance of this calibration phenomenon: an exact equality for bounded functions, not merely an inequality.

Setting

Fix a measurable space $(X,\mathcal A)$ and a closed label set $Y \subset \mathbb R$; throughout this mission $Y := \{-1,1\}$. A loss function is a measurable map $L : X \times Y \times \mathbb R \to [0,\infty)$, read as the cost $L(x,y,f(x))$ of predicting $y$ by $f(x)$ when $x$ is observed. Given a distribution $P$ on $X \times Y$, the $L$-risk of a measurable $f : X \to \mathbb R$ is the average cost $R_{L,P}(f) := \int_{X\times Y} L(x,y,f(x))\,dP(x,y)$, and the Bayes risk $R^*_{L,P} := \inf_f R_{L,P}(f)$ is the smallest risk any measurable function can achieve.

The classification loss is $L_{\mathrm{class}}(y,t) := \mathbf 1_{(-\infty,0]}(y \cdot \operatorname{sgn} t)$ — it charges $1$ exactly when the sign of the prediction $t$ disagrees with the label $y$ — where $\operatorname{sgn}$ is the sign function with the book's convention $\operatorname{sgn}(0):=1$. The hinge loss is $L_{\mathrm{hinge}}(y,t) := \max\{0,1-yt\}$, a convex, piecewise-linear upper bound on $L_{\mathrm{class}}$ up to a factor of $2$. Writing $\eta(x) := P(y=1\mid x)$ for the conditional probability of the positive label given $x$, the Bayes classification function is $f^*_{L_{\mathrm{class}},P}(x) := \operatorname{sgn}(2\eta(x)-1)$: it predicts the majority label at $x$.

A loss $L$ can be clipped at $M>0$ if truncating every prediction to $[-M,M]$ never increases the loss: $L(x,y,\widehat t) \le L(x,y,t)$ for the clipped value $\widehat t$ of $t$. Both $L_{\mathrm{class}}$ and $L_{\mathrm{hinge}}$ can be clipped at $M=1$.

Formalization targets

Goal: Zhang's inequality (Theorem 2.31)

$$R_{L_{\mathrm{hinge}},P}(f) - R^*_{L_{\mathrm{hinge}},P} = \int_X |f(x) - f^*_{L_{\mathrm{class}},P}(x)| \cdot |2\eta(x)-1| \, dP_X(x) \qquad (f : X \to [-1,1])$$ $$R_{L_{\mathrm{class}},P}(f) - R^*_{L_{\mathrm{class}},P} \;\le\; R_{L_{\mathrm{hinge}},P}(f) - R^*_{L_{\mathrm{hinge}},P} \qquad (f : X \to \mathbb R)$$

The first target is an exact identity for bounded predictors: the excess hinge risk equals a weighted $L^1$ distance to the Bayes classifier. The second, weaker but unrestricted, statement is what makes the hinge loss a valid classification surrogate for arbitrary real-valued scores: no matter how large $|f|$ grows, the excess classification risk it incurs is bounded by its excess hinge risk. Because the second statement is the one actually used downstream (Chapter 6's oracle inequality composes it with a bound on the excess hinge risk to bound the excess classification risk), it is the weakest stable form of the calibration claim and the natural target to keep in mind when judging whether a variant formalization is still faithful.

Significance

Zhang's inequality is the single fact that licenses every consistency and rate-of-convergence result for SVM classification in the rest of the book (flagged explicitly on p. 38: "we will show in Section 3.4 that the other margin-based losses ... are also reasonable surrogates," and reused directly, e.g., in Chapter 6's oracle inequality via its restatement as Theorem 6.24 in Chapter 6 of this series). Its role is entirely mechanical but load-bearing: every SVM consistency proof reduces to bounding an excess surrogate risk, and Theorem 2.31 is what converts that bound back into a statement about the classification error anyone actually cares about.

The result itself has been known since Zhang (2004) and Bartlett–Jordan–McAuliffe (2006) in more general form (arbitrary convex margin losses, with an explicit "$\psi$-transform" relating excess risks); Theorem 2.31 is the closed-form hinge-loss instance, with the equality (not just an inequality) available because the hinge loss's clipped value is exactly linear in $\eta$. No machine-checked proof of either the general or the hinge-specific statement is known to exist in a public Lean/Mathlib development at the time of writing (see prior-art search below); this mission asks for a formalization of the hinge-specific case exactly as the book states it.

Difficulty

The natural first attempt is to expand both risk differences directly as integrals over $P$ and compare integrands. This works for the equality (bounded $f$), because the hinge loss is piecewise linear in $t$ and the calculation collapses to the algebraic identity $1+f(x)(1-2\eta(x)) = |f(x)-f^*_{L_{\mathrm{class}},P}(x)|\cdot|2\eta(x)-1|$ once $f^*$ is spelled out by cases on the sign of $2\eta(x)-1$. It fails for the inequality on unbounded $f$: neither risk difference has a closed algebraic form once $f$ is allowed to leave $[-1,1]$, and the excess classification risk itself is genuinely discontinuous in $f$. The book's proof resolves this by clipping $f$ first (Lemma 2.23: clipping a convex loss at a minimizer's interval only decreases its risk) and observing the excess classification risk is invariant under clipping — this reduces the general case to the bounded case, at the cost of needing Lemma 2.23 as a genuine prerequisite rather than a routine remark. The remaining pointwise step (Lemma 2.30) is a case-by-case real-variable inequality with no probabilistic content of its own, but gets the boundary case $\eta = 1/2$ (equivalently $2\eta-1=0$, where the book's sign convention $\operatorname{sgn}(0):=1$ is load-bearing) wrong if that convention is not tracked precisely.

Formalization scope

$X$ is an arbitrary measurable space; $Y$ is fixed to $\{-1,1\} \subset \mathbb R$ throughout. A loss is represented as a plain function Loss X := X → ℝ → ℝ → ℝ; nonnegativity and the restriction of the middle argument to $\{-1,1\}$ are supplied as explicit hypotheses at each use site rather than built into the type, since only some lemmas of the chapter need them (Lemma 2.23 needs neither). risk/bayesRisk are ordinary real-valued Bochner integrals/infima, not extended-real-valued as in the book; consequently every assertion that could otherwise degrade to a vacuous 0 - 0 from a non-integrable loss carries an explicit Integrable hypothesis on the relevant loss composed with $f$ — automatic in the book's own setting (bounded losses on a probability space) but not implied by the Lean types alone. $\eta(x) := P(y=1\mid x)$ is represented by its defining disintegration identity, $P(A\times\{1\}) = \int_{x\in A}\eta(x)\,dP_X(x)$ for every measurable $A \subseteq X$, rather than via a general regular-conditional-probability construction — a specific, checkable representation of "the conditional probability of $y=1$ given $x$" rather than a synonym for it.

A trivializing formalization would let $f^*_{L_{\mathrm{class}},P}$ or $\eta$ be an unconstrained hypothesis unconnected to $P$ and $L_{\mathrm{class}}$ (making the goal a tautology about whatever function is supplied); this is ruled out here by deriving $f^*_{L_{\mathrm{class}},P}$ from $\eta$ by the book's own formula $\operatorname{sgn}(2\eta-1)$ and constraining $\eta$ by the disintegration identity above, not taking either as a free unconstrained parameter.

Lemma 2.23, Lemma 2.30, L_class/L_hinge, risk/bayesRisk and CanBeClipped/clip are reusable beyond this mission: Lemma 2.23 and the risk/Bayes-risk vocabulary recur throughout the book (clippability is used again in Section 7.4 and, per this series' README, this chapter's Theorem 2.31 itself is restated inside Chapter 6's oracle inequality). Contributions completing the two milestone proofs and the goal's sorry are welcome; a from-scratch alternative proof avoiding Lemma 2.23 (e.g. by a direct case analysis on $f$ outside $[-1,1]$) would also be a valid solution to the goal, since the milestones are the book's own attack path, not a required lemma structure.

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 2, pp. 21-47).
• T. Zhang, "Statistical behavior and consistency of classification methods based on convex risk minimization," Annals of Statistics 32(1), 2004, pp. 56-85. https://doi.org/10.1214/aos/1079120130
• P. L. Bartlett, M. I. Jordan & J. D. McAuliffe, "Convexity, classification, and risk bounds," Journal of the American Statistical Association 101(473), 2006, pp. 138-156. https://doi.org/10.1198/016214505000000907

Motivation

How many labeled examples does a learning algorithm need to see before its output generalizes well to unseen data? Chapter 2 of Foundations of Machine Learning answers this question for the simplest nontrivial setting — a finite hypothesis set — and in doing so introduces the book's central object, the Probably Approximately Correct (PAC) learning framework: a distribution-free, high-probability guarantee relating a learner's sample size to the accuracy and confidence of its output. Every later chapter's generalization bound (VC-based, Rademacher-based, margin-based) is a variant of the same "probability of a bad event is small" argument this chapter proves in its most elementary form, so getting the chapter's core definitions and its two bracketing theorems (consistent and inconsistent finite-$H$) right is the foundation the rest of the book's guarantees build on.

Setting

A learner sees a sample $S = (x_1,\dots,x_m)$ drawn i.i.d. from a fixed but unknown distribution $D$ on an instance space $X$, labeled by an unknown target concept $c$ drawn from a concept class $C$; a hypothesis $h$ from a fixed hypothesis set $H$ is judged by its generalization error $R(h) = \Pr_{x\sim D}[h(x)\ne c(x)]$ (Definition 2.1) against its empirical error $\hat R_S(h) = \frac1m\sum_i \mathbb 1_{h(x_i)\ne c(x_i)}$ (Definition 2.2) on the observed sample. A concept class is PAC-learnable (Definition 2.3) if some algorithm, given a polynomially-bounded number of samples, returns a hypothesis whose generalization error is at most $\epsilon$ with probability at least $1-\delta$, for every accuracy $\epsilon$ and confidence $\delta$ and every distribution $D$ — the "distribution-free" and "for all target concepts" character of the definition is what makes it a genuine worst-case learning guarantee rather than an average-case one tailored to a particular data-generating process.

Formalization targets

Theorem 2.5 (consistent case, milestone). If $H$ is finite and algorithm $A$ always returns a hypothesis consistent with the target concept on the training sample ($\hat R_S(h_S)=0$), then $\Pr_{S\sim D^m}[R(h_S)\le\epsilon]\ge1-\delta$ whenever $m \ge \frac1\epsilon(\log|H|+\log\frac1\delta)$.

Corollary 2.11 (single-hypothesis Hoeffding bound, milestone). For a fixed hypothesis $h:X\to\{0,1\}$ and any $\delta>0$, with probability at least $1-\delta$, $R(h) \le \hat R_S(h) + \sqrt{\log(2/\delta)/(2m)}$.

Theorem 2.13 (inconsistent case, goal). For a finite hypothesis set $H$ and any $\delta>0$, with probability at least $1-\delta$, simultaneously for every $h\in H$,

$$R(h) \le \hat R_S(h) + \sqrt{\frac{\log|H|+\log(2/\delta)}{2m}}.$$

Significance

Theorem 2.13 is the chapter's capstone because it removes Theorem 2.5's consistency requirement — the typical case in practice, where no hypothesis in $H$ perfectly fits the training data — while paying only an additive $\log|H|$ price inside the square root, via a union bound over $H$ applied to Corollary 2.11's per-hypothesis concentration bound. It is also the template every later generalization bound in the book refines: Chapter 3 replaces $\log|H|$ with the growth function / VC-dimension to handle infinite hypothesis sets, and Chapter 3's Rademacher-complexity bound is the direct machine-independent generalization of the same argument. No prior art on the Prove2Me platform is faithful to this chapter's PAC-learning content (GET /theorems?q=PAC-learnable returns no hits), so all six items are drafted fresh.

Difficulty

Theorem 2.13's own proof is a short combination of two ideas already present in the chapter (Corollary 2.11's Hoeffding bound plus a union bound over $|H|$ hypotheses), but each ingredient carries its own faithfulness burden. Corollary 2.11 needs the sample $S$ and the target hypothesis $h$ kept in the right relationship — $h$ fixed, $S$ random — for the bound to be Hoeffding's inequality and not a vacuous statement about a random hypothesis. Theorem 2.13 needs the $\forall h\in H$ quantifier placed inside the probability event (a single sample $S$ must work for every $h$ at once), not outside it (which would only assert each $h$'s bound holds with high probability for a sample chosen depending on $h$) — the difference between a uniform convergence bound and $|H|$ separate, weaker statements. Definition 2.3's "polynomial function $\mathrm{poly}(\cdot,\cdot,\cdot,\cdot)$" is a genuine formalization judgment call, addressed below.

Formalization scope

GeneralizationError/EmpiricalError are typed generally over $X, Y$ (matching Definition 2.1/2.2's own general statement, "$h : X\to Y$"), since Theorem 2.5 itself is stated for general $Y$, not just $Y=\mathrm{Bool}$; Corollary 2.11 and Theorem 2.13 specialize to $h : X\to\mathrm{Bool}$, matching their own explicit "$h:X\to\{0,1\}$" (Corollary 2.11) and the surrounding inconsistent-case section's restriction to binary classification. The i.i.d. sample $S\sim D^m$ is modeled as the identity random variable on the product-measure space $(\mathrm{Fin}\ m \to X,\ \mathrm{Measure.pi}(\lambda\_.\ D))$ in both Corollary 2.11 and Theorem 2.13, matching the book's own $S\sim D^m$ notation exactly. IsPACLearnable (Definition 2.3) makes "polynomial function" precise as a function bounded above by $K\cdot(a+b+n+s+1)^k$ for some constants $K>0$, $k\in\mathbb N$, uniform in its (nonnegative) arguments — the standard reading of "polynomial in its arguments" in the absence of a ready-made multivariate polynomial-growth predicate in Mathlib; dropping this constraint entirely (stating only "there is some threshold function") would silently weaken Definition 2.3 to a strictly easier notion of learnability, since virtually any finite or well-behaved concept class admits some (possibly super-polynomial) sample-complexity threshold — this is exactly the distinction Example 2.7 (the universal concept class) uses to demonstrate a class that is not PAC-learnable despite admitting a consistent hypothesis set. No numerical constant in Theorem 2.5, Corollary 2.11 or Theorem 2.13 is altered from the book's own; no upper bound on $\delta$ is added anywhere the book itself leaves it unrestricted (the theorems remain true, if vacuous, for $\delta>1$). Not formalized: the "efficiently PAC-learnable" running-time clause of Definition 2.3 (a second, independent polynomial-time condition on $A$ not needed by either milestone or the goal); Corollary 2.10 (the raw two-sided Hoeffding statement Corollary 2.11 is immediately derived from by solving for $\epsilon$, making it redundant with Corollary 2.11 as a formalization target); the axis-aligned-rectangles worked example (Example 2.4–2.9), which illustrates the framework rather than proving a new general result, and the trivializing formalization this chapter invites — reusing Mathlib's rectangle machinery to encode only the specific two-dimensional geometric argument rather than the general finite-$H$ theorems — is exactly what this mission avoids by drafting Theorems 2.5 and 2.13 in their general, hypothesis-set-agnostic form.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 2.
• W. Hoeffding, "Probability inequalities for sums of bounded random variables," Journal of the American Statistical Association 58(301), 1963, 13-30.