Machine Learning

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

The support vector machine and every other kernel method (Gaussian processes, kernel ridge regression, kernel PCA) is specified by choosing a kernel: a function $k(x,x')$ measuring similarity between two inputs, used in place of an inner product on the raw data. This lets a linear algorithm implicitly work in a very high- or infinite-dimensional feature space without ever computing a feature vector explicitly (the "kernel trick"). The definition of a kernel most directly tied to this trick — $k(x,x') = \langle \Phi(x),\Phi(x')\rangle$ for some feature map $\Phi$ into a Hilbert space — is exactly the definition that makes verifying a candidate similarity function is a valid kernel hard: it asks for an explicit Hilbert space and map that in practice nobody wants to construct by hand.

Schoenberg's theorem (1938, for a special class of functions on the sphere) and the general theory developed by Aronszajn and others through the mid-20th century established the alternative used ever since: a function is a kernel exactly when it is symmetric and positive definite, a checkable condition on finite point sets alone. Steinwart & Christmann, Support Vector Machines (Springer 2008, Information Science and Statistics), Theorem 4.16 gives the modern, self-contained real-Hilbert-space proof of this equivalence, and it is the theorem every later construction in the book's kernel chapter (sums, products, limits, and the specific kernel families used in practice) rests on.

Setting

Fix a non-empty set $X$ (the input space; no further structure is assumed). A function $k : X \times X \to \mathbb R$ is a kernel on $X$ if there exist a real Hilbert space $H$ and a feature map $\Phi : X \to H$ such that

$$k(x,x') = \langle \Phi(x), \Phi(x') \rangle_H \qquad \text{for all } x, x' \in X.$$

Neither $H$ nor $\Phi$ are determined by $k$: for $X = \mathbb R$, $k(x,x') := xx'$ admits both the identity map on $\mathbb R$ and $\Phi(x) := (x/\sqrt2, x/\sqrt2) \in \mathbb R^2$ as feature maps.

Separately, $k$ is symmetric if $k(x,x') = k(x',x)$ for all $x,x'$, and positive definite if, for every $n \in \mathbb N$, every $\alpha_1,\dots,\alpha_n \in \mathbb R$, and every $x_1,\dots,x_n \in X$,

$$\sum_{i=1}^n \sum_{j=1}^n \alpha_i \alpha_j\, k(x_j,x_i) \ge 0,$$

equivalently: the $n \times n$ Gram matrix $(k(x_j,x_i))_{i,j}$ is positive semidefinite for every finite point set. This condition mentions only $X$, $\mathbb R$, and finite sums — no Hilbert space at all.

Formalization targets

Goal: Theorem 4.16

$$k \text{ is a kernel on } X \iff k \text{ is symmetric and positive definite.}$$

The forward direction is elementary (a two-line computation from the feature-map definition, recorded in the book just before the theorem statement). The goal is the full equivalence, including the converse: a symmetric, positive definite function, given with no reference to any ambient Hilbert space at all, is nonetheless a kernel.

Supporting facts: Lemma 4.5 and Corollary 4.17

$$k, k_1, k_2 \text{ kernels},\ \alpha \ge 0 \implies \alpha k,\ k_1 + k_2 \text{ are kernels (Lemma 4.5)},$$ $$k_n \to k \text{ pointwise},\ \text{each } k_n \text{ a kernel} \implies k \text{ is a kernel (Corollary 4.17)}.$$

Neither is a hypothesis Theorem 4.16's own proof consumes; both are included as further chapter results built on the same two definitions, chosen because they are the tools the book uses immediately afterward to construct concrete kernels (polynomial kernels, kernels given by convergent power series) without exhibiting a feature map for each one by hand, and because Corollary 4.17's one-line proof ("every $k_n$ is symmetric and satisfies (4.5); therefore so is the pointwise limit $k$") only makes sense once Theorem 4.16 is available as the bridge back to "is a kernel".

Significance

Theorem 4.16 is the single result that turns "is a kernel" from an existential, non-constructive question (does some Hilbert space and feature map exist?) into a universal, checkable one (does a finite-dimensional matrix inequality hold for every finite point set?). Every kernel actually used in the book from this point on — polynomial kernels, the Gaussian RBF kernel, kernels built from Taylor or Fourier series — is verified to be a kernel via this characterization, not by exhibiting a feature map directly (an infinite-dimensional one, in most of these cases). Lemma 4.5 and Corollary 4.17 are the two closure properties that make positive-definiteness verification compositional: a new kernel is usually built as a sum, nonnegative multiple, product, or limit of kernels already known to be positive definite, rather than checked from scratch.

The result itself is classical (Schoenberg 1938 for the special case relevant to distance-based kernels on spheres; the general Hilbert-space statement is standard by the mid-20th century, see Aronszajn 1950's RKHS paper and Berg–Christensen–Ressel's monograph). No machine-checked Lean proof of this specific real-Hilbert-space equivalence is known to exist on the platform at the time of writing (see prior-art search below); this mission asks for its formalization exactly as the book states and proves it, via the explicit pre-Hilbert-space-of-finite-combinations construction rather than any other known proof of the same fact (e.g. via Riesz representation).

Difficulty

The forward direction (kernel $\Rightarrow$ symmetric and positive definite) is immediate once a feature map is given. The converse is not: starting from only the two finite, algebraic conditions, the proof must manufacture a Hilbert space and a feature map out of nothing but $k$ and $X$. The book's construction — the space $H_{\mathrm{pre}}$ of finite linear combinations $\sum_i \alpha_i k(\cdot,x_i)$, with inner product $\langle f,g\rangle := \sum_{i,j} \alpha_i\beta_j k(x_j',x_i)$ — requires checking, in order, that this inner product is well-defined independently of how $f$ and $g$ are represented as such combinations (using the reproducing-type identity $\langle f,g\rangle = \sum_j \beta_j f(x_j')$), that it is positive definite as an actual inner product (not just on the Gram-matrix diagonal, i.e. $\langle f,f \rangle = 0 \Rightarrow f = 0$ as a function, which uses a Cauchy–Schwarz argument on $H_{\mathrm{pre}}$ itself before $H_{\mathrm{pre}}$ is known to be an inner product space), and only then completing $H_{\mathrm{pre}}$ to an honest Hilbert space. Each of these three steps individually looks routine, but the middle one is circular-looking on a first reading (using an inner-product inequality to prove the pairing is an inner product) and is the step every attempted shortcut skips.

Formalization scope

$X$ is an arbitrary non-empty type (Nonempty X), matching Definition 4.1's own standing hypothesis; no additional topological or measurable structure is imposed, since none is used by either the definitions or Theorem 4.16's proof. IsKernel existentially quantifies over a Type Hilbert space (NormedAddCommGroup, real InnerProductSpace, CompleteSpace) and a feature map, matching Definition 4.1 specialized to the real field $\mathbb K = \mathbb R$; the complex case of Definition 4.1 is out of scope, since Theorem 4.16 itself is stated only for real-valued $k$. PositiveDefinite and Symmetric (Definition 4.15) quantify over an arbitrary finite family via Fin n → X / Fin n → ℝ for n : ℕ, exactly the book's "for all $n$, $\alpha_1,\dots,\alpha_n$, $x_1,\dots,x_n$".

A trivializing formalization would fix a specific small Hilbert space (e.g. $\mathbb R^d$ for a fixed $d$) in IsKernel's existential rather than an arbitrary one, which would make the "if" direction of Theorem 4.16 false in general (a positive definite kernel's minimal feature space can be infinite-dimensional) or silently restrict the theorem's scope; this is ruled out here by existentially quantifying over an unconstrained Hilbert space type.

IsKernel, Symmetric, and PositiveDefinite are reusable well beyond this mission: every later kernel construction in the book (polynomial kernels, Lemma 4.6's product kernels, the reproducing kernel Hilbert space of Section 4.2) is stated in terms of them. Completing the two milestone proofs and the goal's own sorry (the $H_{\mathrm{pre}}$ construction above) is welcome; a from-scratch formalization of Lemma 4.6 (products of kernels, needing the completed tensor product of two Hilbert spaces) or of the chapter's other named kernel families would be natural, faithful extensions of this mission but are out of scope for it.

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 4, §4.1, pp. 111-119).
• N. Aronszajn, "Theory of Reproducing Kernels," Transactions of the American Mathematical Society 68(3), 1950, pp. 337-404. https://doi.org/10.2307/1990404
• I. J. Schoenberg, "Metric spaces and positive definite functions," Transactions of the American Mathematical Society 44(3), 1938, pp. 522-536. https://doi.org/10.2307/1989894
• C. Berg, J. P. R. Christensen & P. Ressel, Harmonic Analysis on Semigroups: Theory of Positive Definite and Related Functions, Springer GTM 100, 1984. https://doi.org/10.1007/978-1-4612-1128-0

Motivation

Support vector machines were, for two decades, the workhorse of applied classification, and the reason offered for their success was always geometric: SVMs maximize the margin between the two classes. Chapter 3's VC-dimension bound cannot explain why this should help — for linear hypotheses in $\mathbb R^N$ its bound depends on $N+1$ and is uninformative whenever the feature dimension is large relative to the sample size, exactly the regime (kernel-induced or high-dimensional features) where SVMs are most often used. Chapter 5 answers the question this leaves open: a generalization bound for a real-valued hypothesis, stated in terms of its margin on the training sample, that does not depend on the ambient dimension at all. This is also the template every later chapter's margin bound specializes (multi-class classification, ranking, and, indirectly, boosting all reuse the same Rademacher-complexity-of-a-Lipschitz-loss argument developed here).

Setting

A hypothesis here is a real-valued function $h:X\to\mathbb R$, not (as in Chapters 2-3) a function into $\{-1,+1\}$: for a labeled point $(x,y)$ with $y\in\{-1,+1\}$, the sign of $h(x)$ gives the prediction and $|h(x)|$ is read as the classifier's confidence. The confidence margin of $h$ at $(x,y)$ is $y\,h(x)$; it is positive exactly when $h$ classifies $x$ correctly. For $\rho>0$, the $\rho$-margin loss $\Phi_\rho:\mathbb R\to\mathbb R$ (Definition 5.5) is

$$\Phi_\rho(x) = \min\Big(1,\max\Big(0,1-\frac x\rho\Big)\Big),$$

equal to $1$ when $x\le 0$ (misclassified), $0$ when $x\ge\rho$ (classified with confidence at least $\rho$), and interpolating linearly in between; it is $1/\rho$-Lipschitz. The empirical margin loss on a sample $S=(x_1,\dots,x_m)$ with labels $y_1,\dots,y_m$ (Definition 5.6) is $\hat R_{S,\rho}(h) = \frac1m\sum_{i=1}^m\Phi_\rho(y_ih(x_i))$ — the fraction of training points misclassified or classified with confidence below $\rho$, a strictly stronger requirement than plain misclassification. The (population) generalization error is $R(h)=\Pr_{(x,y)\sim D}[y\,h(x)\le 0]$. Rademacher complexity, $\hat R_S(H)$ and $R_m(H)$ (Definitions 3.1-3.2, restated here since chunk 03-rademacher-vc's own copies are still drafts), measure how well a real-valued hypothesis class $H$ correlates with random sign noise on a sample, and are the vehicle through which the margin bound's complexity term is expressed.

Formalization targets

Lemma 5.7 (Talagrand's lemma, milestone). For $l$-Lipschitz $\Phi_1,\dots,\Phi_m:\mathbb R\to\mathbb R$ and any hypothesis set $H$ of real-valued functions,

$$\frac1m\,\mathbb E_\sigma\Big[\sup_{h\in H}\sum_{i=1}^m\sigma_i(\Phi_i\circ h)(x_i)\Big] \le l\,\hat R_S(H).$$

Theorem 5.10 (Rademacher complexity of bounded-norm linear hypotheses, milestone). For $S\subseteq\{x:\|x\|\le r\}$ and $H=\{x\mapsto w\cdot x:\|w\|\le\Lambda\}$,

$$\hat R_S(H) \le \sqrt{r^2\Lambda^2/m}.$$

Corollary 5.11 (margin bound for linear hypotheses, milestone). For the same $H$ and $X\subseteq\{x:\|x\|\le r\}$, fixing $\rho>0$, with probability at least $1-\delta$,

$$R(h) \le \hat R_{S,\rho}(h) + 2\sqrt{\frac{r^2\Lambda^2/\rho^2}{m}} + \sqrt{\frac{\log(1/\delta)}{2m}} \quad\text{for all } h\in H.$$

Theorem 5.8 — the mission's goal. For any set $H$ of real-valued functions and $\rho>0$, with probability at least $1-\delta$, both

$$R(h) \le \hat R_{S,\rho}(h) + \frac2\rho R_m(H) + \sqrt{\frac{\log(1/\delta)}{2m}}$$ $$R(h) \le \hat R_{S,\rho}(h) + \frac2\rho \hat R_S(H) + 3\sqrt{\frac{\log(2/\delta)}{2m}}$$

hold simultaneously for all $h\in H$.

Significance

Theorem 5.8 is genuinely dimension-free: unlike Chapter 3's VC-dimension bound (5.36 in the book, restated from Corollary 3.19), it holds regardless of the ambient feature dimension $N$, depending instead only on the hypothesis class's Rademacher complexity and the chosen margin $\rho$. Specialized to bounded-norm linear hypotheses (Corollary 5.11), this gives the theoretical justification most often cited for SVMs and every other margin-maximization algorithm: whenever the training data admits a large geometric margin, the empirical margin loss at that margin is small (often zero, in the separable case) and the bound is tight regardless of $N$. Every later chapter's own margin bound (multi-class in Chapter 9, ranking in Chapter 10) is a direct structural descendant of Theorem 5.8's proof technique. No prior art on the Prove2Me platform is faithful: GET /theorems?q=support+vector+machine and q=margin+bound return no hits on this book's model (the two q=margin+bound hits found, both from the Aether Catalog, state a different comparison — a VC-type bound is eventually worse than a fixed Rademacher-type bound as a function of dimension — not Theorem 5.8 itself); q=Talagrand and q=contraction+principle return several hits (Ledoux/Talagrand convex-distance concentration, Rudin's Banach-space contraction-mapping theorem, a generic Rademacher-sign contraction lemma for quadratic sums) but every one states either a different mathematical object (metric-space fixed points, Talagrand's concentration inequality on product spaces) or a different idiom (squared vs. linear coordinate sums) from Lemma 5.7's function-composition contraction — none reused. All nine items are drafted fresh.

Not formalized here: Theorem 5.4 (the SVM sparsity/leave-one-out bound). It is listed as a candidate milestone in BRIEF.md, but its statement and proof depend on the primal/dual SVM optimization problem itself (the Lagrangian, KKT conditions, and the resulting definition of a "support vector" as a training point with nonzero dual coefficient) — a materially different, non-margin-based proof technique (leave-one-out stability of the trained hypothesis, via Lemma 5.3) that shares no definitions with the margin-bound family this mission's goal and other milestones are built on. Formalizing it faithfully would require standing up the SVM primal/dual formalism (Lagrangian, complementary slackness, the "support vector" predicate itself) from scratch, which is disproportionate to a single additional milestone within this mission's budget; per the captain brief's guidance to leave out, rather than approximate, a statement that cannot be made faithful in the time available, it is omitted.

Difficulty

The proof of Theorem 5.8 needs the empirical margin loss's zero-one-loss upper bound ($\mathbb 1_{u\le 0}\le\Phi_\rho(u)$) applied before invoking Theorem 3.3's Rademacher generalization bound on the composed class $\tilde{\tilde H}=\{\Phi_\rho\circ f: f\in\tilde H\}$, $\tilde H=\{(x,y)\mapsto y\,h(x):h\in H\}$ — reversing this order (bounding $R(h)$ by a Rademacher complexity computed on the zero-one loss directly) does not work, because the zero-one loss is not Lipschitz. Talagrand's lemma is exactly what lets the $1/\rho$-Lipschitz surrogate $\Phi_\rho$ be pulled outside the Rademacher complexity, at the cost of a factor $1/\rho$ and no worse; its own proof is an induction removing one Rademacher variable at a time, using a two-point supremum argument (fixing $\epsilon>0$, choosing near-optimal $h_1,h_2$) that does not simplify to anything less than genuine care with suprema of non-smooth objects — a formalization attempting to replace this with a naive linearity-of-expectation argument would be proving a false or vacuous statement, since $\sup$ does not commute with linear combinations. Theorem 5.10's bound needs the Cauchy-Schwarz and Jensen inequalities used in the particular order the book uses them (Cauchy-Schwarz on the empirical sup, then Jensen on the expectation of a norm, then the independence of the $\sigma_i$s) — the bound $\hat R_S(H)\le r\Lambda/\sqrt m$ does not follow from either inequality alone.

Formalization scope

EmpiricalRademacherComplexity/RademacherComplexity are restated locally in SVM, byte-identical to chunk 03-rademacher-vc's own copies (a draft item cannot import another chunk's draft module); this duplication collapses once 03-rademacher-vc is uploaded and listed in missions/README.md's "Published definitions" table. MarginGeneralizationError is a new, real-valued-hypothesis specialization of Definition 2.1 (R(h) = P[y h(x) ≤ 0]), distinct from every earlier chunk's {-1,+1}-valued GeneralizationError, since no earlier chunk's own copy matches this chapter's real-valued convention. PhiRho/EmpiricalMarginLoss are new. The goal theorem (margin_bound_binary_classification) states H's own Rademacher complexity computed on the marginal X-distribution (D.map Prod.fst), matching the book's final displayed form — the proof's intermediate step (the lifted class $\tilde H=\{(x,y)\mapsto y h(x)\}$ having the same Rademacher complexity as $H$ itself, since $y\in\{-1,+1\}$) is not separately drafted, only the theorem's statement. Theorem 5.10/Corollary 5.11 generalize the book's ambient $\mathbb R^N$ to an arbitrary real inner-product space X ([NormedAddCommGroup X] [InnerProductSpace ℝ X]), a harmless generalization since the book's proof (Cauchy-Schwarz, Jensen, orthogonality of Rademacher signs) uses only the inner-product structure, never finite dimension; [BorelSpace X] is added to Corollary 5.11's statement to make the measurable structure under which MarginGeneralizationError is well-posed explicit, since every x ↦ ⟨w, x⟩ is automatically Borel-measurable — not a substantive restriction, the book never discusses measurability of linear functionals. 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 5.8 only for a Finset/finite H (which would make it a disguised instance of Chapter 2's finite-hypothesis bound rather than the chapter's genuinely new, complexity-based argument) — H : Set (X → ℝ) is left fully general, exactly as the book states it.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 5.
• C. Cortes, V. Vapnik, "Support-vector networks," Machine Learning 20(3), 1995, 273-297.
• M. Talagrand, "Sharper bounds for Gaussian and empirical processes," The Annals of Probability 22(1), 1994, 28-76.
• P. Bartlett, S. Mendelson, "Rademacher and Gaussian complexities: risk bounds and structural results," Journal of Machine Learning Research 3, 2002, 463-482.

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

Many statistical estimators are defined by minimizing an empirical average over a class of candidate models — empirical risk minimization, maximum likelihood, and binary classification all fit this template. Analyzing such an estimator's excess risk reduces, in each case, to controlling how far the empirical average of a whole class of functions can deviate from its population expectation, not just a single fixed function — a much stronger requirement than the ordinary law of large numbers, which only controls one function at a time. This mission formalizes the central non-asymptotic tool for this problem, the Rademacher complexity-based uniform law, following Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 4.

Setting

Let $F$ be a class of real-valued functions with a common domain, indexed as $F=\{f_j, j\in\iota\}$, and let $X_1,\dots,X_n$ be i.i.d. samples from a distribution $P$. The empirical process deviation (Eq. (4.7)) is

$$\|\mathbb P_n-P\|_F \;:=\; \sup_{f\in F}\Big|\frac1n\sum_{i=1}^n f(X_i) - \mathbb E[f(X)]\Big|.$$

Given an independent Rademacher sequence $\varepsilon_1,\dots,\varepsilon_n$ (each $\varepsilon_i=\pm1$ equiprobably), the symmetrized process (Eq. (4.19)) and the Rademacher complexity (Eq. (4.13)) of $F$ are

$$\|S_n\|_F := \sup_{f\in F}\Big|\frac1n\sum_{i=1}^n\varepsilon_if(X_i)\Big|, \qquad R_n(F) := \mathbb E_{X,\varepsilon}[\|S_n\|_F].$$

A class $F$ is $b$-uniformly bounded if $\|f\|_\infty\le b$ for every $f\in F$.

Formalization targets

Goal — Theorem 4.10 (a uniform law via Rademacher complexity)

For any $b$-uniformly bounded class $F$, any $n\ge1$, and any $\delta\ge0$,

$$\|\mathbb P_n-P\|_F \;\le\; 2R_n(F)+\delta$$

with $P$-probability at least $1-\exp(-n\delta^2/2b^2)$.

Milestone — Proposition 4.11 (symmetrization sandwich)

For any convex non-decreasing $\Phi$, $\mathbb E[\Phi(\tfrac12\|S_n\|_{\bar F})] \le \mathbb E[\Phi(\|\mathbb P_n-P\|_F)] \le \mathbb E[\Phi(2\|S_n\|_F)]$, where $\bar F$ is the recentered class. This generalizes the specific symmetrization step used in Theorem 4.10's own proof (the case $\Phi(t)=t$) to an entire family of moment comparisons.

Milestone — Eq. (4.16) (concentration around the mean)

For a $b$-uniformly bounded, i.i.d.-sampled class $F$, $\|\mathbb P_n-P\|_F - \mathbb E[\|\mathbb P_n-P\|_F] \le t$ with $P$-probability at least $1-e^{-nt^2/2b^2}$, obtained via the bounded-differences method. Combined with Proposition 4.11's bound on $\mathbb E[\|\mathbb P_n-P\|_F]$ by $2R_n(F)$, this is exactly Theorem 4.10's proof.

Significance

Theorem 4.10 is the general-purpose engine behind the classical Glivenko–Cantelli theorem (recovered by taking $F$ to be the class of half-line indicator functions, Example 4.6) and behind uniform convergence guarantees for empirical risk minimization more broadly (Section 4.1.2): whenever a task can be reduced to bounding the Rademacher complexity of a specific function class — a purely combinatorial/geometric quantity independent of any particular statistical model — Theorem 4.10 converts that bound directly into a high-probability uniform convergence guarantee. Proposition 4.11 is separately significant as the general symmetrization principle from which Theorem 4.10's specific bound, and many similar bounds throughout empirical process theory, are instances.

Formalizing it. No faithful prior art exists on the platform: a fresh search for "uniform law," "symmetrization," "Rademacher complexity," "Glivenko-Cantelli," and "empirical process" found only unrelated hits and the existing RademacherSymmetrization.*/RademacherMassart.* items, which are specific to finite function classes (Finset (X → ℝ)) — a strictly narrower setting than Theorem 4.10's fully general (possibly infinite) function classes, and not reused here. All three theorems are drafted as open goals (:= by sorry).

Difficulty

The naive approach to bounding $\|\mathbb P_n-P\|_F$ — apply a scalar concentration bound to each $f\in F$ individually and union-bound over $F$ — fails outright when $F$ is infinite (there is no union bound to take). The two-step resolution captured by this mission's milestones avoids this entirely: first, $\|\mathbb P_n-P\|_F$ itself, viewed as a single function of the $n$ samples, is shown to concentrate sharply around its own mean via the bounded-differences method (no union bound over $F$ needed — the argument treats $\sup_{f\in F}(\cdots)$ as one Lipschitz function of the samples). Second, the mean $\mathbb E[\|\mathbb P_n-P\|_F]$ itself, a single deterministic number, is bounded via symmetrization: introducing an independent "ghost sample" $Y_i$ with the same law as $X_i$ converts the un-symmetric quantity $\mathbb E[\sup_f|(1/n)\sum f(X_i)-\mathbb E f|]$ into the manifestly symmetric $\mathbb E[\sup_f|(1/n)\sum\varepsilon_i (f(X_i)-f(Y_i))|]$, and it is only after this symmetrization that the supremum over $F$ becomes tractable via the geometry of $F$ (its Rademacher complexity) rather than requiring $F$ finite.

Formalization scope

The function class $F$ is realized as the range of an index family $f:\iota\to D\to\mathbb R$ rather than a Set (D → ℝ), matching the standard representation of a (possibly infinite) function class by an index type; ι carries no finiteness assumption, matching the book's own full generality (in contrast to the platform's existing RademacherSymmetrization/ RademacherMassart items, which are finite-class-specific). The population expectation $\mathbb E[f(X)]$ is realized via an explicit population variable $X_0$ sharing the samples' common law, rather than a separately axiomatized abstract distribution object. The Rademacher sequence and the samples are packaged into one jointly independent family Z : ℕ → Ω → D × ℝ with an explicit hypothesis that the two coordinates are themselves independent at each index — capturing "$\varepsilon$ independent of $X$, both i.i.d." exactly, without a bespoke joint-independence predicate.

Theorem 4.10's own qualitative corollary ("consequently, $\|\mathbb P_n-P\|_F\xrightarrow{a.s.}0$ whenever $R_n(F)=o(1)$") is not included in the goal's conclusion: it concerns an infinite sequence of samples and asymptotic convergence via the Borel–Cantelli lemma, a substantially different formal object (requiring Filter.Tendsto over ℕ→∞ and ∀ᵐ almost-sure convergence) from the single-$n$ non-asymptotic tail bound (4.14) this mission's goal states, and is left as natural follow-on work, alongside a direct formalization of the classical Glivenko–Cantelli theorem (Theorem 4.4) as a corollary.

Lemma 4.14 (the polynomial-discrimination route to bounding Rademacher complexity for VC-type classes) is out of scope for this mission: its displayed inequality is extracted with heavily garbled math layout from the source PDF (a known, disclosed limitation of this book's text extraction at that specific page), and confirming it character-for-character against the rendered page image was judged out of budget for this chunk relative to Proposition 4.11 and Eq. (4.16), both of which are directly load-bearing in Theorem 4.10's own proof and extracted cleanly.

Selected references

• M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019. DOI: 10.1017/9781108627771. Chapter 4.
• M. Ledoux and M. Talagrand, Probability in Banach Spaces: Isoperimetry and Processes, Springer, 1991 (the symmetrization technique).
• V. N. Vapnik and A. Y. Chervonenkis, "On the uniform convergence of relative frequencies of events to their probabilities," Theory of Probability and Its Applications, 16(2):264–280, 1971.

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