All missions

Motivation

Support vector machines (SVMs) are trained by solving a regularized empirical risk minimization problem over a reproducing kernel Hilbert space (RKHS) — a space that is typically infinite-dimensional. On its face, this looks computationally hopeless: how can a computer search an infinite-dimensional space for a minimizer? The representer theorem is the result that makes SVM training tractable at all: it shows that no matter how large the RKHS is, the minimizer of the SVM objective for a sample of size $n$ always lies in the $n$-dimensional subspace spanned by the kernel evaluated at the $n$ sample points. This turns an infinite- dimensional optimization problem into a finite-dimensional one before a single line of an optimization algorithm is written, and it is the reason every practical SVM solver (from the original sequential minimal optimization algorithm onward) searches only over $n$ coefficients rather than over an abstract function space.

The theorem in this mission — Theorem 5.5 of Steinwart and Christmann, Support Vector Machines (Springer, 2008) — is stated for general convex losses and general kernels, subsuming the classification-SVM and regression-SVM special cases that appear throughout the machine learning literature. Its lineage traces to Kimeldorf and Wahba's 1971 representer theorem for spline-smoothing problems; the book's own version (attributed to a 1971 result, generalized here to arbitrary convex losses and RKHSs) is the general form used throughout the rest of the book.

Setting

Fix a nonempty set $X$ (the input space) and a loss function $L : X \times \mathbb R \times \mathbb R \to [0,\infty)$: a measurable map where $L(x,y,t)$ is the cost of predicting label $y$ by value $t$ when the input is $x$. $L$ is convex if $L(x,y,\cdot)$ is convex for every fixed $x,y$.

A reproducing kernel Hilbert space (RKHS) over $X$ is a real Hilbert space $H$ of real-valued functions on $X$ that carries a kernel $k : X \times X \to \mathbb R$ with two properties: $k(\cdot,x) \in H$ for every $x \in X$, and the reproducing property $f(x) = \langle f, k(\cdot,x)\rangle_H$ holds for every $f \in H$ and $x \in X$. Intuitively, $k$ lets you evaluate any $f \in H$ at a point $x$ by taking an inner product with the fixed function $k(\cdot,x)$ — this is what makes $H$ a space of genuine, pointwise-evaluable functions rather than an abstract Hilbert space.

Given a finite sample $D := ((x_1,y_1),\dots,(x_n,y_n)) \in (X \times \mathbb R)^n$, the empirical $L$-risk of $f : X \to \mathbb R$ is $R_{L,D}(f) := \tfrac1n\sum_{i=1}^n L(x_i,y_i,f(x_i))$. For a regularization parameter $\lambda > 0$, the SVM training problem asks for a minimizer of the regularized empirical risk

$$f \mapsto \lambda\|f\|_H^2 + R_{L,D}(f)$$

over all of $H$. A minimizer of this objective is called an empirical SVM solution $f_{D,\lambda}$.

Formalization targets

Goal — Theorem 5.5 (Representer theorem)

$$\exists! \, f_{D,\lambda} \in H : \quad \lambda\|f_{D,\lambda}\|_H^2 + R_{L,D}(f_{D,\lambda}) = \min_{f \in H} \Bigl(\lambda\|f\|_H^2 + R_{L,D}(f)\Bigr), \qquad f_{D,\lambda}(x) = \sum_{i=1}^n \alpha_i\, k(x,x_i) \; \text{ for some } \alpha_1,\dots,\alpha_n \in \mathbb R.$$

The theorem asserts both halves at once: the regularized empirical risk has a unique minimizer over the (possibly infinite-dimensional) $H$, and that unique minimizer is representable as a finite linear combination of the kernel functions at the sample points. Neither the coefficients $\alpha_i$ nor the finite-dimensional subspace they live in are fixed in advance by the statement; only their existence is asserted, so a stronger claim (e.g. uniqueness or an explicit formula for the $\alpha_i$) would be a different, harder theorem not proved here.

Supporting milestones (the general, population-level analogue)

The book develops the representer theorem's existence-and-uniqueness clause by first proving it for the corresponding population problem — minimizing $f \mapsto \lambda\|f\|_H^2 + R_{L,P}(f)$ over a distribution $P$ rather than a finite sample — and then adapting the same two arguments to the empirical case:

• Lemma 5.1 (uniqueness): for a convex loss and an RKHS $H$ with $R_{L,P}(f) < \infty$ for some $f \in H$, the regularized population risk has at most one minimizer over $H$, for every $\lambda > 0$.
• Theorem 5.2 (existence): for a convex, $P$-integrable Nemitski loss and the RKHS of a bounded kernel, the regularized population risk has at least one minimizer, for every $\lambda > 0$.
• Theorem 5.6 (non-triviality): under the same hypotheses as Theorem 5.2, if $H$ can beat the risk of the zero function ($\inf_{f \in H} R_{L,P}(f) < R_{L,P}(0)$), then every minimizer is nonzero, for every $\lambda > 0$.

Significance

The representer theorem is the single fact that turns kernel-based learning from a theoretical curiosity into a practical algorithm family: every popular SVM solver (SMO, coordinate descent, interior-point methods for the dual) is, at bottom, a method for finding the $n$ coefficients $\alpha_1,\dots,\alpha_n$ the theorem guarantees exist, not for searching $H$ directly. The representation also underlies the "kernel trick": since the objective and the solution both depend on $H$ only through inner products $\langle k(\cdot,x_i), k(\cdot,x_j)\rangle_H = k(x_i,x_j)$, an SVM can be trained and evaluated without ever computing with elements of $H$ explicitly, using only the $n \times n$ Gram matrix of kernel values.

Formalizing this theorem means formalizing the existence-and-uniqueness argument (Lemma 5.1's strict-convexity computation for the midpoint of two hypothetical minimizers, together with the weak-compactness argument used for existence) and the orthogonal-projection argument for the representation clause (projecting any candidate minimizer onto the finite-dimensional span of the kernel functions at the sample points strictly improves — or leaves unchanged — both the norm term and the risk term, so an optimal solution can always be chosen inside that span). No part of this argument has a machine-checked Lean proof in Mathlib or elsewhere at the time of writing; only the underlying general-purpose tools (Hilbert-space projections, convexity of norms) are already in Mathlib.

Difficulty

The natural first idea for the representation clause is to try to exhibit the coefficients $\alpha_i$ directly, e.g. by writing down the dual optimization problem and reading off its KKT multipliers. This is exactly backwards: the book's proof (and any faithful one) derives the representation before knowing anything about a dual problem, purely from the orthogonal decomposition $H = H|_{X'} \oplus H|_{X'}^\perp$ of $H$ into the span $H|_{X'}$ of the sample's kernel functions and its orthogonal complement. The key insight — one that a solver who reaches for duality first will miss — is that projecting any $f \in H$ onto $H|_{X'}$ leaves the empirical risk exactly unchanged (since $R_{L,D}$ only sees $f$'s values at the sample points, and the reproducing property shows those values are unaffected by throwing away the $H|_{X'}^\perp$ component) while weakly decreasing the norm term, so the infimum over all of $H$ is already attained inside the finite-dimensional $H|_{X'}$.

For the existence-and-uniqueness clause, the difficulty is genuinely functional-analytic rather than algorithmic: existence needs a compactness argument in a space with no compact balls (Theorem 5.2 gets around this via lower semicontinuity and boundedness of the sublevel set, not via any finite-dimensional trick), and uniqueness needs the parallelogram-law strict convexity of the Hilbert norm, not merely convexity of the loss.

Formalization scope

$H$ is represented as an arbitrary real Hilbert space together with an injective linear evaluation map into $X \to \mathbb R$ (so that $H$ is genuinely realized as a space of functions, not an abstract Hilbert space with no relation to $X$), and a kernel $k$ satisfying the reproducing property with respect to that evaluation map (IsRKHSOfKernel). This is an equivalent, operative rendering of "$H$ is the RKHS of the kernel $k$" (Definition 4.18 together with Lemma 4.19 of the book), chosen because it is exactly the form the chapter's own proofs use; it is restated inside this chunk's own InfiniteSample sub-namespace rather than imported from the Kernels chapter's mission, since drafts in this series cannot import one another.

The population risk $R_{L,P}$ is formalized as a lower Lebesgue integral into $[0,\infty]$ (ENNReal), which is always well-defined for a nonnegative integrand with no integrability hypothesis — matching the book's own remark that "the integral always exists, although it is not necessarily finite." The empirical risk $R_{L,D}$, by contrast, is a manifestly finite average over the $n$ sample points and is formalized as an ordinary real number. The sample size $n$ is required positive ($n \ge 1$), matching the book's implicit convention that the empirical measure $\bar D := \tfrac1n\sum_i \delta_{(x_i,y_i)}$ presupposes a nonempty sample.

A trivializing formalization of the representer theorem would state only the representation clause $f_{D,\lambda}(x) = \sum_i \alpha_i k(x,x_i)$ while assuming the existence of "the" solution $f_{D,\lambda}$ as a hypothesis; this begs the question, since the book's own proof establishes existence and uniqueness as part of the theorem, not as a standing assumption. This mission's goal keeps both clauses bundled into one ∃! statement for exactly this reason.

The infrastructure needed — a general convex loss, a Nemitski-loss integrability condition, and the RKHS/reproducing-kernel bundle — is restated locally here and is reusable, with the same caveat about not being importable across this series' independently drafted chapters, by any later mission (e.g. this book's own Chapters 6, 8 and 9) that needs the same objects. Contributed proofs are welcome for either the existence/uniqueness argument (Lemma 5.1/Theorem 5.2's techniques) or the orthogonal-projection representation argument; the two are largely independent and could be solved separately.

Selected references

• I. Steinwart and A. Christmann, Support Vector Machines, Springer Series in Information Science and Statistics, Springer, 2008. https://doi.org/10.1007/978-0-387-77242-4
• G. Kimeldorf and G. Wahba, "Some results on Tchebycheffian spline functions," Journal of Mathematical Analysis and Applications, 33(1):82–95, 1971. https://doi.org/10.1016/0022-247X(71)90184-3
• B. Schölkopf, R. Herbrich, and A. J. Smola, "A generalized representer theorem," in Computational Learning Theory (COLT 2001), Lecture Notes in Computer Science, vol. 2111, Springer, 2001, pp. 416–426. https://doi.org/10.1007/3-540-44581-1_27

Comparing distributions by their Laplace transforms

Many of the orders in Shaked and Shanthikumar's Stochastic Orders (Springer, 2007) are built by fixing a class of test functions $\varphi$ and declaring $X \le Y$ whenever $E[\varphi(X)] \le E[\varphi(Y)]$ for every $\varphi$ in that class: all increasing functions give the usual stochastic order, all convex functions give the convex order. This mission formalizes the order obtained from the single function $\varphi_s(x) = -e^{-sx}$, $s > 0$ — the Laplace transform order — together with its principal alternative characterization and three of its closure properties. Unlike almost every other order in the book, this one has essentially no dependence on material from earlier chapters, which is why it is a natural standalone mission.

The Laplace transform order

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

$$E[e^{-sX}] \ge E[e^{-sY}] \quad \text{for every } s > 0.$$

The order is meant for nonnegative random variables: the book's own standing convention for the whole of §5.A is that every random variable mentioned is nonnegative, since otherwise $E[e^{-sX}]$ need not even be finite. Every theorem below carries that hypothesis explicitly rather than folding it into the order's own definition, so the definition itself is stated exactly as broadly as the book's raw equation (5.A.1) is — a comparison of two expectations, for two random variables that need not share a probability space, since $\le_{Lt}$ is a comparison of distributions.

A second definition supports one of the milestones: a function $\varphi : [0,\infty) \to \mathbb{R}$ is completely monotone if all its derivatives exist and $(-1)^n\varphi^{(n)}(x) \ge 0$ for every $x > 0$ and every $n = 0, 1, 2, \dots$. Every $\varphi_s(x) = e^{-sx}$, $s > 0$, is completely monotone, which is what connects the raw definition of $\le_{Lt}$ to its function-class characterization below.

Formalization targets

Goal: the integrated-survival-function characterization (Theorem 5.A.1)

$$X \le_{Lt} Y \iff \int_0^\infty e^{-sx}\bar F(x)\,dx \le \int_0^\infty e^{-sx}\bar G(x)\,dx \quad \text{for every } s > 0,$$

where $\bar F(x) = P\{X>x\}$ and $\bar G(x) = P\{Y>x\}$ are the survival functions of $X$ and $Y$. This is the book's principal restatement of the order, obtained from the identity $\int_0^\infty e^{-sx}\bar F(x)\,dx = s^{-1}(1-E[e^{-sX}])$: instead of comparing the raw Laplace transforms of $X$ and $Y$ themselves, it compares the Laplace transforms of their survival functions, weighted the same way. It is the natural goal for a standalone chapter mission: the chapter's own defining equation plus one elementary identity is exactly the book's own proof, and it is the form of the order that the chapter's closure properties are stated against.

Supporting milestones

• Eq. (5.A.5), the mean inequality: $X \le_{Lt} Y \implies E[X] \le E[Y]$, provided the expectations exist — obtained by dividing the defining inequality by $s$ and letting $s \downarrow 0$.
• Theorem 5.A.3, the function-class characterization: $X \le_{Lt} Y$ iff $E[\varphi(X)] \ge E[\varphi(Y)]$ for every completely monotone $\varphi$, provided the expectations exist — the order's analogue of "all increasing functions" for $\le_{st}$ or "all convex functions" for $\le_{cx}$.
• Theorem 5.A.7(a), closure under functions with a completely monotone derivative: $X \le_{Lt} Y$ and $g$ positive with $g'$ completely monotone gives $g(X) \le_{Lt} g(Y)$.
• Theorem 5.A.7(d), the convolution corollary: independent $X_i \le_{Lt} Y_i$, $i=1,\dots,m$, gives $\sum_i X_i \le_{Lt} \sum_i Y_i$.

Significance

The Laplace transform order is the natural comparison for nonnegative quantities that arise as sums or mixtures of exponential-type random variables — waiting times, workloads, service completion times — precisely because it is preserved under convolution (Theorem 5.A.7(d)) and under the broad class of transformations with a completely monotone derivative (Theorem 5.A.7(a)), which includes every concave power $x^p$, $0<p\le 1$. It sits strictly between the convex-type orders and weaker moment comparisons: Eq. (5.A.5) shows it implies ordered means, but (unlike $\le_{cx}$) it does not require equal means, and (unlike $\le_{icx}$) it is not implied by a pointwise comparison of integrated tails alone — it is its own, genuinely different order, useful whenever a modeler's comparison naturally arises through Laplace-transform (equivalently, moment-generating-function-at- negative-argument) calculations rather than through a coupling or a tail-probability argument. Theorem 5.A.3's function-class form is the bridge that lets the order be verified either way: by a single-parameter family of exponential test functions, or by the full class of completely monotone functions of which they are the extreme rays.

Difficulty

The chapter's own first warning applies directly: the order's every characterization requires $X,Y \ge 0$, and dropping that hypothesis anywhere — as opposed to carrying it explicitly on each theorem, per this mission's convention — would silently change which statements are even well-posed, since $E[e^{-sX}]$ can diverge for $X$ unbounded below. The quantifier "$\forall s > 0$" in both the raw definition and Theorem 5.A.1 ranges over the whole positive half-line, not a bounded or discretized set of test points; narrowing it would produce a strictly weaker order. In CompletelyMonotone, the phrase "all its derivatives exist" is a genuine hypothesis, not a formality: stating only the sign condition on iteratedDeriv n φ x without also requiring φ to be C^∞ would let the definition be satisfied vacuously wherever a derivative fails to exist (a classic junk-value trap), which is why the mission's definition bundles smoothness explicitly. Theorem 5.A.7(a)'s "$g$ positive" is a hypothesis on $g$'s values at the nonnegative reals that $X$ and $Y$ actually take, not on all of $\mathbb{R}$, and must not be silently strengthened to "$g$ everywhere positive" or weakened to "$g$ nonnegative" (which would let $g$ vanish and break the order's need for $e^{-sg(X)}$ to be well-behaved).

Formalization scope

LaplaceOrder μ ν X Y takes $X : \Omega \to \mathbb{R}$ on $(\Omega,\mu)$ and $Y : \Omega' \to \mathbb{R}$ on a separate $(\Omega',\nu)$, matching the series' convention (e.g. StochasticOrders.Usual.UsualOrder) that the order compares distributions, not jointly defined variables. Nonnegativity of $X$ and $Y$ is an explicit hypothesis ∀ ω, 0 ≤ X ω / ∀ ω, 0 ≤ Y ω on every theorem, never built into LaplaceOrder itself. CompletelyMonotone φ is ContDiff ℝ ⊤ φ ∧ ∀ n x, 0 < x → 0 ≤ (-1)^n * iteratedDeriv n φ x — the smoothness conjunct guards the junk-value trap described above. The survival function $\bar F(x) = P\{X>x\}$ in the goal theorem is formalized inline as (μ {ω | x < X ω}).toReal, valid since μ is a probability measure (so the underlying ENNReal value is finite and the conversion to ℝ loses no information); the integral $\int_0^\infty$ is Bochner integration over Set.Ici (0 : ℝ). "Provided the expectations exist" becomes explicit Integrable hypotheses per statement (on $X$, $Y$ themselves for Eq. 5.A.5; on $\varphi \circ X$, $\varphi \circ Y$ for each $\varphi$ in Theorem 5.A.3), rather than a blanket integrability assumption that would understate which expectations the book actually needs. Independence in the convolution corollary is ProbabilityTheory.iIndepFun, one family per side, as in Chunk 01's own convolution corollary. A trivializing formalization is ruled out: $\le_{Lt}$ is not restated as a comparison of one moment or of the raw random variables' means, and the "universal function class" of Theorem 5.A.3 is exactly the completely monotone functions the book names, not a fixed finite subfamily or a narrowed subclass (e.g. only the exponentials themselves, which would make Theorem 5.A.3 a restatement of the definition rather than its own theorem).

This mission draws on no platform prior art: repeated searches for "Laplace transform" and "completely monotone" during this session return only unrelated analytic-number-theory formalizations (a Langlands–Tunnell Laplace–Mellin transform identity) and no hits at all, respectively — confirming BRIEF.md's expectation that this subarea is untouched on the platform. It is one of nine missions in a series covering the whole book; per the series' own convention, its definitions are not imported by any other chapter's mission, and it does not import any other chapter's definitions in turn (the chapter itself has essentially no cross-chapter dependence, the reason it was flagged as the series' most self-contained chunk).

Selected references

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

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