Statistics

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

Comparing location and spread together

Chapter I's usual stochastic order compares "how large" two random variables tend to be; Chapter III's convex order compares "how spread out" they are, holding the mean fixed. Chapter IV's increasing convex and increasing concave orders combine the two: $X \le_{icx} Y$ says $X$ is both smaller and less variable than $Y$ in a single comparison, without forcing equal means. These are the orders a decision-maker with risk-averse (concave-utility) or risk-loving (convex-cost) preferences actually uses to rank random outcomes, since expected utility is exactly an expectation of an increasing concave or convex function. This mission formalizes both orders and their coupling characterization: the submartingale/supermartingale analogue, one chapter over, of Chapter III's Strassen martingale coupling for the plain convex order.

The increasing convex and increasing concave orders

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 increasing convex order, written $X \le_{icx} Y$, if

$$E[\varphi(X)] \le E[\varphi(Y)] \quad \text{for every increasing convex } \varphi:\mathbb{R}\to\mathbb{R} \text{ for which the two expectations exist,}$$

and smaller than $Y$ in the increasing concave order, $X \le_{icv} Y$, if the same holds for every increasing concave $\varphi$. Taking $\varphi(x)=x$ (increasing and both convex and concave) gives $E[X]\le E[Y]$ under either order — unlike the convex order, no equality of means is forced. Two equivalent tail-integral characterizations (Theorem 4.A.2) make the orders tractable: $X\le_{icx}Y$ iff $\int_x^\infty \bar F(u)\,du \le \int_x^\infty \bar G(u)\,du$ for every $x$, and $X\le_{icv}Y$ iff $\int_{-\infty}^x F(u)\,du \ge \int_{-\infty}^x G(u)\,du$ for every $x$, where $\bar F,\bar G$ and $F,G$ are the survival and distribution functions.

Formalization targets

Goal: the submartingale-coupling characterization (Theorem 4.A.5, increasing convex case)

$$X \le_{icx} Y \iff \exists\,(\Omega'',\rho),\ \hat X,\hat Y:\Omega''\to\mathbb{R}\text{ with } \hat X=_{st}X,\ \hat Y=_{st}Y,\ E[\hat Y\mid\hat X]\ge\hat X\text{ a.s.}$$

Furthermore, $\hat X,\hat Y$ can be chosen so that $[\hat Y\mid\hat X=x]$ stochastically increases with $x$ (in $\le_{st}$). This is the increasing-convex analogue of Chapter III's Theorem 3.A.4: instead of a martingale, $\{\hat X,\hat Y\}$ need only be a submartingale — the copy of $Y$ is, conditionally on the copy of $X$, at least a fair randomization of it. The book states its proof is "similar to the proof of Theorem 3.A.4" and calls the constructive direction "not easy to prove"; this mission states the theorem faithfully, including the "Furthermore" strengthening, without attempting a proof.

Companion: the supermartingale-coupling characterization (Theorem 4.A.5, increasing concave case)

The same theorem's other bracketed case: $X \le_{icv} Y$ iff there exist $\hat X,\hat Y$ on a common space with $\hat X=_{st}X$, $\hat Y=_{st}Y$, and $\{\hat Y,\hat X\}$ a supermartingale, $E[\hat X\mid\hat Y]\le\hat Y$ a.s. — note the swapped roles of $\hat X$ and $\hat Y$ in the conditioning relative to the increasing-convex case, not merely a flipped inequality. Drafted as a separate Lean theorem from the goal (see Formalization scope), since the two conditioning structures are genuinely different predicates, not sign-flipped rewrites of one another.

Supporting milestones

• Theorem 4.A.1, the duality relation: $X\le_{icx}Y \iff -X\ge_{icv}-Y$, and $X\le_{icv}Y\iff -X\ge_{icx}-Y$ — the increasing-order analogue of Theorem 3.A.12(a)'s duality for the plain convex order.
• Theorem 4.A.2, the tail-integral characterizations above, for integrable $X,Y$.
• Theorem 4.A.8(d), closure under convolution: independent $X_i\le_{icx}Y_i$ (resp. $\le_{icv}$) for $i=1,\dots,m$ gives $\sum_i X_i \le_{icx} \sum_i Y_i$ (resp. $\le_{icv}$) — the increasing-order analogue of Chapter III's Theorem 3.A.12(d), which the book itself says "can be proven as in Theorem 3.A.12."

Significance

The increasing convex and concave orders are the natural language of expected-utility comparisons: a risk-averse agent with concave utility $u$ prefers $Y$ to $X$ exactly when $X\le_{icv}Y$ implies $E[u(X)]\le E[u(Y)]$ for every increasing concave $u$ — the order is defined precisely so that "every risk-averse agent with increasing utility agrees" collapses to one comparison. In operations research this underlies stochastic dominance of the second kind in portfolio and inventory models, and the increasing-convex order similarly formalizes "second-order stochastic dominance for costs" used to compare random cost/loss distributions under risk-loving or regret-averse preferences. The submartingale-coupling characterization is what turns the intractable "for every increasing convex $\varphi$" quantifier into a single explicit construction, exactly as Strassen's theorem does for the plain convex order — and, being the direct chapter-IV successor to Chapter III's coupling theorem in this series, it fixes the second data point for what a "coupling-characterization" mission in this book's series looks like when the order being characterized is not symmetric between the two variables' roles.

No platform prior art exists: GET /theorems?q=increasing+convex, q=increasing+concave, and q=submartingale return zero genuinely matching hits (the one submartingale hit, a bandit subgaussian maximal inequality, uses Doob's inequality for a concentration bound, not this order). This mission restates the increasing convex/concave orders and their coupling characterization as a foundational, self-contained pair of definitions, parallel in structure to Chunk 03's convex-order mission but independently drafted (drafts cannot import each other's Lean).

Difficulty

The chief formalization risk is the one this chapter's own brief flags explicitly: the book states Theorem 4.A.5 as a single statement with bracketed alternatives ("$X\le_{icx}Y$ [$X\le_{icv}Y$] iff … $\{\hat X,\hat Y\}$ is a submartingale [$\{\hat Y,\hat X\}$ is a supermartingale] …"), and the two cases are not symmetric rewrites of each other — the conditioning variable in E[Ŷ|X̂]≥X̂ swaps to E[X̂|Ŷ]≤Ŷ in the concave case, not just a flipped inequality on the same conditioning. A Lean statement that tried to unify both cases with a single Or or a naive sign-flip would either conflate two different predicates or silently state the wrong condition for one of the two cases. The duality theorem (4.A.1) compounds this risk in the other direction: its content is exactly that $\le_{icx}$ and $\ge_{icv}$ are related (by negating the variables), so a formalization that makes this equivalence provable by unfolding definitions (rather than as a genuine ↔ between two independently-stated predicates) would trivialize the one theorem whose entire content is that relationship.

Formalization scope

Random variables are measurable functions into $\mathbb{R}$ from arbitrary measurable spaces, matching this series' convention; IcxOrder μ ν X Y and IcvOrder μ ν X Y are drafted as two separate definitions (not one order parametrized by an Or of function classes), each quantifying over Monotone φ ∧ ConvexOn ℝ Set.univ φ (resp. ConcaveOn) with the two expectations' existence stated as explicit Integrable hypotheses inside the ∀, exactly as Chunk 03's ConvexOrder. Equality in law is ProbabilityTheory.IdentDistrib. The goal's submartingale condition uses Mathlib's conditional-expectation notation X̂ ≤ᵐ[ρ] ρ[Ŷ | m] with m the σ-algebra generated by X̂; its companion's supermartingale condition uses ρ[X̂ | m'] ≤ᵐ[ρ] Ŷ with m' generated by Ŷ instead — the conditioning variable is genuinely swapped between the two theorems, matching the book's own bracket ordering {X̂,Ŷ} vs. {Ŷ,X̂}. The "Furthermore" clause in both is kept (not dropped), via Mathlib's ProbabilityTheory.condDistrib, restated as the relevant conditional-distribution kernel's survival function being monotone at every threshold — the same shape Chapter I's UsualOrder and Chunk 03's goal theorem use, necessarily restated locally since drafts cannot import another mission's definitions.

Theorem 4.A.1 (duality) and Theorem 4.A.8(d) (convolution closure) are each drafted as a single Lean theorem with two independent conjuncts (an ∧ of two ↔s, or of two implications), one per bracketed case, since the book states both cases as the two halves of one theorem sharing every hypothesis — this is not the same shape as the goal/companion split, where the two cases have genuinely different internal structure (the swapped conditioning) rather than a shared statement instantiated at two function classes. A trivializing formalization this mission rules out: stating Theorem 4.A.1's duality by relabeling IcvOrder as IcxOrder applied to negated arguments (making the equivalence a rfl or single simp unfolding) rather than keeping the two orders as independently-defined predicates whose relationship is the theorem's actual content.

This mission draws on no platform prior art (searches for "increasing convex", "increasing concave", and "submartingale" as of 2026-09-18 return zero genuine matches — the sole submartingale hit is an unrelated bandit concentration inequality via Doob's inequality). Reusable beyond this mission: the IcxOrder/IcvOrder definition pattern and the submartingale/supermartingale coupling shape parallel Chunk 03's ConvexOrder martingale-coupling pattern closely enough that a future chapter needing "coupling characterization of a location-and-spread order" (none of the remaining chapters currently in this series' first wave) could restate the same shape with minimal adaptation.

Selected references

• M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007, Chapter 4 (Univariate Monotone Convex and Related Orders), §4.A. https://doi.org/10.1007/978-0-387-34675-5
• This series' Chunk 03 (StochasticOrders.Convex), for the plain convex order and Strassen's martingale coupling this chapter's submartingale/supermartingale coupling directly generalizes.

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

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