High-Dimensional Probability and Statistics

Motivation

Many arguments in high-dimensional geometry, statistics and computer science need to approximate a point of a convex set by an average of a handful of extreme points, rather than represent it exactly. The classical Carathéodory theorem (1907) answers the exact question: every point of the convex hull of a set $T \subseteq \mathbb{R}^n$ is a convex combination of at most $n+1$ points of $T$. That bound is tight and grows with the dimension $n$, which makes it useless whenever $n$ is large — exactly the regime of interest in high-dimensional probability.

B. Maurey's empirical method — an unpublished 1980–81 result reported by G. Pisier, "Remarques sur un résultat non publié de B. Maurey," Séminaire d'Analyse Fonctionnelle 1980–1981 — and later applied by B. Carl to bound covering numbers of operators between Banach spaces (Inequalities of Bernstein-Jackson-type and the degree of compactness of operators in Banach spaces, Ann. Inst. Fourier 35(3), 1985, 79–118), replaces the exact question with an approximate one and removes the dimension dependence entirely: to approximate $x$ to accuracy $\varepsilon$, the number of points needed depends only on $\varepsilon$, never on $n$. Vershynin's High-Dimensional Probability opens with this result as its "Appetizer," using it to illustrate the book's central theme — that randomness is a tool for constructing deterministic combinatorial objects — before any probabilistic machinery has been introduced.

Setting

A convex combination of finitely many points $z_1, \dots, z_m \in \mathbb{R}^n$ is a sum $\sum_{i=1}^m \lambda_i z_i$ with $\lambda_i \ge 0$ and $\sum_i \lambda_i = 1$. The convex hull $\operatorname{conv}(T)$ of a set $T \subseteq \mathbb{R}^n$ is the set of all convex combinations of all finite collections of points of $T$. The diameter of $T$ is $\operatorname{diam}(T) = \sup\{\|s-t\|_2 : s, t \in T\}$, the Euclidean norm throughout.

The classical Carathéodory theorem states that every $x \in \operatorname{conv}(T)$ is a convex combination of at most $n+1$ points of $T$ — with $n+1$ generally unavoidable, attained by a simplex. The question this mission answers is different: given that we are willing to approximate $x$ rather than represent it exactly, and willing to use only combinations with equal coefficients $1/k$ (an average of $k$ points, with repetition allowed), how large must $k$ be as a function of the desired accuracy?

Formalization targets

Goal — Theorem 0.0.2, Approximate Carathéodory's theorem

$$\text{diam}(T) \le 1,\ x \in \operatorname{conv}(T),\ k \in \mathbb{Z}_{>0} \ \Longrightarrow\ \exists\, x_1,\dots,x_k \in T:\quad \left\| x - \frac{1}{k}\sum_{j=1}^{k} x_j \right\|_2 \le \frac{1}{\sqrt{k}}.$$

The quantifiers are exactly this order: for every bounded $T$, every point of its convex hull, and every target $k$, such an averaging set exists. This is the weakest stable statement carrying the theorem's content — the number of points $k$ does not depend on the dimension $n$, and the coefficients are forced to be uniform — and it is the form the corollary below invokes directly.

Milestone — Corollary 0.0.4, Covering polytopes by balls

$$P = \operatorname{conv}(T),\ |T| = N,\ \operatorname{diam}(P) \le 1,\ \varepsilon > 0 \ \Longrightarrow\ \exists\, C,\ |C| \le N^{\lceil 1/\varepsilon^2 \rceil}:\quad P \subseteq \bigcup_{c \in C} \overline{B}(c, \varepsilon).$$

This is a direct application of the goal to computational geometry's covering problem: how many balls of radius $\varepsilon$ are needed to cover a polytope, and where should they be centered.

Significance

The result itself. The approximate Carathéodory theorem is the prototype of a dimension-free approximation result: whenever a set is bounded, a fixed number of points (depending only on the target accuracy, not the ambient dimension) suffices to approximate any point of its convex hull. This is what makes possible dimension-independent covering-number bounds such as Corollary 0.0.4, which in turn are the starting point for the book's later treatment of entropy, packing and generic chaining (Chapters 4, 7–8). The technique generalizes far beyond $\mathbb{R}^n$: it underlies covering-number bounds for operators between Banach spaces (Carl's original application) and is a recurring device in learning theory for bounding the size of an $\varepsilon$-net of a hypothesis class.

Formalizing it. Both results are elementary and already fully proved in the literature; no open mathematical content remains. What this mission contributes is a machine-checked, faithful Lean statement of Maurey's construction and its corollary, phrased over Mathlib's existing convex-hull and metric-diameter machinery, so that later missions in this series (concentration inequalities, Johnson–Lindenstrauss, chaining) can build on a verified base case of "probability constructs a deterministic covering," and so that the empirical method itself becomes a reusable, linked component on the platform. The proof of the goal (via the probabilistic argument sketched by the book: interpret a convex combination as a probability distribution, average $k$ i.i.d. samples, and bound the variance) is left open for solvers.

Difficulty

The identity that makes the proof work — averaging $k$ independent copies of a random vector concentrates around its mean at rate $1/\sqrt{k}$ in mean-square — is a two-line computation once the convex combination is reinterpreted probabilistically. The step that is easy to miss is this reinterpretation itself: nothing in the statement mentions probability, so the "obvious" attack of manipulating the convex-combination weights directly, or trying to construct $x_1,\dots,x_k$ by some explicit combinatorial recipe, does not see a path to a bound independent of $n$. The probabilistic argument produces the points non-constructively, via an averaging/existence argument (the expected squared distance is small, so some realization achieves it) rather than an explicit formula — a solver has to introduce a probability space and a random vector that does not appear anywhere in the formal statement to be proved.

Formalization scope

Both results are stated over EuclideanSpace ℝ (Fin n) for an explicit dimension n : ℕ, so ‖·‖ is the Euclidean norm and Mathlib's Metric.diam is used directly for $\operatorname{diam}(T) = \sup\{\|s-t\|_2\}$. The convex hull is Mathlib's convexHull ℝ T; by Mathlib's convexHull_eq, this already coincides with the book's own definition of a convex combination of finitely many points of $T$, so no bespoke convex-combination definition is introduced — this mission needs no supporting definitions of its own. In the corollary, "a polytope $P$ with $N$ vertices" is formalized, following the book's own proof, as $P = \operatorname{conv}(T)$ for a finite vertex set $T$ with $\#T = N$, rather than via a separate Polytope structure (which Mathlib does not provide and the book's argument does not need). The covering bound $N^{\lceil 1/\varepsilon^2\rceil}$ is an exponent, not a product with $N$ — matching the book's own proof, which counts the $N^k$ ordered $k$-tuples of vertices with repetition, $k := \lceil 1/\varepsilon^2\rceil$; the typeset "$N\lceil 1/\varepsilon^2\rceil$" in the corollary statement is the same juxtaposition-as-exponent notation the proof uses for "$N^k$" one line earlier.

A trivializing formalization is ruled out explicitly: the goal must hold for every integer $k > 0$ and every $x \in \operatorname{conv}(T)$, not merely some convenient choice — e.g. $k = 1$ together with $x \in T$ trivially satisfies the inequality but proves nothing about the theorem's actual content, that a fixed, dimension-independent $k$ works uniformly over all points of the hull. The formal statement quantifies $T$, then $x$, then $k$, and only then asserts existence of the $x_1,\dots,x_k$, exactly in that order.

Classical Carathéodory (Theorem 0.0.1, stated for context in the source but not used by either formalized result's proof) is not drafted here: Mathlib already proves the corresponding statement via affine independence (Caratheodory.eq_pos_convex_span_of_mem_convexHull, Analysis/Convex/Caratheodory.lean), from which the book's "$n+1$ points" bound follows via AffineIndependent.card_le_finrank_succ. It is not added as a kind: reference milestone because no corresponding theorem is yet published on the Prove2Me platform to point at (checked 2026-09-17: GET /theorems?q=Caratheodory returns only unrelated tropical-convexity results), and re-drafting existing Mathlib content as a new platform theorem would duplicate rather than reuse it.

Selected references

• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, DOI 10.1017/9781108231596, Appetizer (pp. 1–5).
• G. Pisier, "Remarques sur un résultat non publié de B. Maurey," Séminaire d'Analyse Fonctionnelle (Maurey–Schwartz), 1980–1981, exposé no. 5. numdam.org/item/SAF_1980-1981____A5_0
• B. Carl, "Inequalities of Bernstein-Jackson-type and the degree of compactness of operators in Banach spaces," Annales de l'Institut Fourier, 35(3), 1985, 79–118. numdam.org/item/AIF_1985__35_3_79_0

Motivation

The central limit theorem tells us that a normalized sum of independent random variables converges in distribution to a Gaussian. For applications — bounding the failure probability of a randomized algorithm, controlling the error of a Monte Carlo estimator, proving a generalization bound in learning theory — a limiting distribution is not enough: what is needed is a single, explicit, non-asymptotic inequality that holds for every fixed sample size $N$, not merely as $N \to \infty$. Hoeffding's inequality (Wassily Hoeffding, 1963) and Bernstein's inequality (Sergei Bernstein, 1920s–1940s, in the form used here due to Vadim Bennett and later authors) are the two archetypal answers: both give an explicit Gaussian-type tail bound for a weighted sum of independent random variables, valid for every $N$, with all constants made explicit. They are the workhorses behind concentration of measure, high-dimensional statistics, and the non-asymptotic analysis of randomized algorithms; a textbook trying to reach the Johnson–Lindenstrauss lemma, random matrix norms, or the restricted isometry property has to pass through this chapter first, because every one of those results is itself an application of a weighted-sum concentration inequality to a specific choice of random variables.

The central limit theorem's own error term is the obstruction that direct concentration inequalities are built to avoid: the Berry–Esseen theorem (Andrew C. Berry, 1941; Carl-Gustav Esseen, 1942) bounds the normal approximation's error at order $1/\sqrt N$, which is too slow to recover a genuinely exponential tail bound for finite $N$. Hoeffding's and Bernstein's inequalities are proved instead by a direct argument — bounding the moment generating function of the sum and optimizing a Markov/Chernoff exponential tilt — that never invokes the central limit theorem or its error term at all.

The sub-gaussian and sub-exponential norms

Fix a probability space $(\Omega, \mathcal F, P)$. For a real random variable $X$ on $(\Omega, \mathcal F, P)$, define its sub-gaussian norm

$$\|X\|_{\psi_2} := \inf\{t > 0 : \mathbb E \exp(X^2/t^2) \text{ is finite and } \le 2\}$$

and its sub-exponential norm

$$\|X\|_{\psi_1} := \inf\{t > 0 : \mathbb E \exp(|X|/t) \text{ is finite and } \le 2\}.$$

In both definitions, the requirement that the exponential moment be finite (i.e. that the moment-generating integrand be integrable), and not merely satisfy "$\le 2$" as a bare inequality, is essential: without it a moment that is genuinely infinite for a given $t$ would vacuously count as "$\le 2$" under the Bochner integral's convention that a non-integrable function integrates to $0$, and every random variable — however heavy-tailed — would trivially have norm $0$. $X$ is called sub-gaussian (respectively sub-exponential) when this infimum is over a nonempty set, i.e. when some finite $t$ makes the moment finite and at most $2$. These are genuine norms (up to the identification of almost-surely-equal random variables) on the vector space of random variables for which they are finite, and they are the natural non-asymptotic yardsticks for tail heaviness: $\|X\|_{\psi_2} < \infty$ characterizes a Gaussian-type tail $P\{|X| \ge t\} \le 2\exp(-ct^2/\|X\|_{\psi_2}^2)$, while $\|X\|_{\psi_1} < \infty$ characterizes an exponential-type tail $P\{|X| \ge t\} \le 2\exp(-ct/\|X\|_{\psi_1})$. Every bounded random variable — in particular every Bernoulli or Rademacher (symmetric Bernoulli) random variable — is sub-gaussian, and the square of a sub-gaussian random variable is sub-exponential; a genuinely sub-exponential (not sub-gaussian) example is the squared coordinate $g_i^2$ of a standard Gaussian vector, or the exponential distribution itself.

Formalization targets

Goal — Theorem 2.8.2 (Bernstein's inequality, weighted sum). Let $X_1, \dots, X_N$ be independent, mean-zero, sub-exponential random variables on $(\Omega, \mathcal F, P)$, and let $a = (a_1, \dots, a_N) \in \mathbb R^N$. Then, for every $t \ge 0$,

$$P\Bigl\{\Bigl|\sum_{i=1}^N a_i X_i\Bigr| \ge t\Bigr\} \;\le\; 2\exp\left[-c\min\left(\frac{t^2}{K^2\|a\|_2^2}, \frac{t}{K\|a\|_\infty}\right)\right],$$

where $K = \max_i \|X_i\|_{\psi_1}$ and $c > 0$ is an absolute constant that does not depend on $N$, the $X_i$, $a$, or $t$.

The goal is deliberately the weighted and sub-exponential form, the weakest of the chapter's results that is still stable under the improvements a solver might find: it neither fixes $a_i \equiv 1$ (the unweighted Theorem 2.8.1, a special case) nor restricts to the lighter sub-gaussian tail (Theorem 2.6.3, which follows from a strictly stronger hypothesis). Both weaker theorems, plus Hoeffding's and Chernoff's inequalities, are included as milestones because Bernstein's own proof is built directly from them.

Significance

The result itself. Bernstein's inequality is the two-tail-regime concentration bound: a sub-gaussian tail $\exp(-ct^2/(K\|a\|_2)^2)$ near the mean, transitioning to a heavier sub-exponential tail $\exp(-ct/(K\|a\|_\infty))$ far from it, exactly the behavior one should expect from a mixture of light-tailed terms with one heavy-tailed outlier. It underlies the concentration of quadratic forms (Chapter 6's Hanson–Wright inequality controls $\sum \varepsilon_i \varepsilon_j$-type terms, which are themselves products of sub-gaussians and hence sub-exponential by Lemma 2.7.7), and it is the standard tool for bounding empirical-process suprema whose summands are not bounded but merely light-tailed.

Formalizing it. No formalization of Bernstein's inequality — in either the weighted or unweighted, or sub-gaussian or sub-exponential form — exists yet on Prove2Me (GET /theorems?q=Bernstein and q=sub-exponential return no relevant hits, checked 2026-09-17). What this mission produces is not just the statement but the machinery underneath it: a working Orlicz-norm treatment of $\psi_1$ and $\psi_2$ that a later mission (the Hanson–Wright inequality, or any future chapter that needs sub-exponential concentration) can build on directly.

Difficulty

The obvious first idea — squaring both sides and applying Chebyshev, as one does to prove the weak law of large numbers — gives only a polynomial tail bound decaying like $1/N$, far too weak to be useful (this is exactly the point made by the chapter's opening discussion of the coin-tossing example, comparing the linear decay from Chebyshev against the target exponential decay). The central limit theorem promises the right shape of tail asymptotically but, per Berry–Esseen, with an error of order $1/\sqrt N$ that swamps any exponential gain for large deviations — the CLT approximation is simply not valid in the tail regime the inequality needs. The actual argument instead controls the moment generating function of the full sum directly and optimizes an exponential (Chernoff) tilt; this is why the sub-gaussian and sub-exponential norms — MGF-control objects, not moment or tail objects per se — are the right technical vehicle, even though Proposition 2.5.2 and 2.7.1 show all these characterizations are equivalent up to constants. The min of two terms in Bernstein's exponent is not an artifact of a loose proof: it reflects a genuinely two-regime tail (Gaussian near the mean, exponential in the far tail), and collapsing it to a single term in either direction would either be false (dropping the exponential term) or needlessly weak (dropping the Gaussian term, which is what a naive union bound over the worst single term would give).

Formalization scope

Random variables are ℝ-valued functions on an explicit probability space (Ω, mΩ, P) (Ω : Type, MeasurableSpace Ω, P : Measure Ω, [IsProbabilityMeasure P]), matching the book's setup throughout. Independence is Mathlib's ProbabilityTheory.iIndepFun, and tail probabilities are stated with P.real, Mathlib's ℝ-valued measure evaluation, which corresponds directly to the book's $P\{\cdot\}$.

Both Orlicz norms are defined locally, as genuine infima matching Definitions 2.5.6 and 2.7.5 verbatim (subgaussianNorm, subexponentialNorm, each sInf {t > 0 : Integrable (fun ω => E[...]) P ∧ E[...] ≤ 2}), rather than reused from Mathlib's HasSubgaussianMGF (Mathlib.Probability.Moments.SubGaussian). The Integrable conjunct is not optional dressing: Mathlib's Bochner integral of a non-integrable function is 0 by convention, so a bare E[...] ≤ 2 (without asserting integrability) would be satisfied by every t for which the moment is actually infinite, collapsing the sub-gaussian norm of a standard Gaussian (and, symmetrically, the sub-exponential norm of any heavy-tailed variable) to 0 — a trivializing formalization the mission was moderated to rule out. The same Integrable conjunct appears in every moment hypothesis (general_hoeffding, bernstein_unweighted, bernstein_weighted): ∃ s > 0, Integrable (...) P ∧ ∫ ... ≤ 2, so that the hypothesis is not satisfied vacuously by non-integrable exponential moments either. HasSubgaussianMGF bounds the moment generating function directly with a variance-proxy parameter $\sigma^2$ (E exp(tX) ≤ exp(c t²/2)), which is a different object definitionally from the Orlicz $\psi_2$ norm — equivalent up to a constant factor by the book's own Proposition 2.5.2, but not interchangeable without restating that equivalence — and Mathlib has no sub-exponential analogue at all. Since the goal theorem and two of its milestones need the sub-exponential norm, one consistent convention (the book's own Orlicz norms) is used for both $\psi_1$ and $\psi_2$ throughout the mission, rather than mixing Mathlib's MGF-based sub-gaussian convention with a locally defined sub-exponential one.

Every occurrence of the book's "$c$ is an absolute constant" is formalized as a genuine existential quantifier fixed before the random variables, the vector a, and t are introduced: ∃ c : ℝ, 0 < c ∧ ∀ ..., P.real {...} ≤ 2 * Real.exp (-(c * ...)). No numeral is substituted for c anywhere; a solver's proof may use any positive constant it can establish, exactly mirroring the book's own non-constructive existence claims. The trivializing formalization this rules out is fixing c to a specific small numeral (which would be a strictly stronger, easier, and unfaithful claim) or, in the other direction, weakening the statement by allowing c to depend on N, the $X_i$, a, or t (which would make the theorem vacuous, since any such bound trivially holds for a small enough $c$ depending on the instance).

Chernoff's inequality (Theorem 2.3.1) needs no Orlicz norm — Bernoulli parameters $p_i$ are given directly via P.real {X i = 1} = p i ∧ P.real {X i = 0} = 1 - p i, and the conclusion uses Real.rpow (^ on ℝ → ℝ → ℝ) for the real exponent $t$ in $(e\mu/t)^t$. Hoeffding's inequality for symmetric Bernoulli variables (Theorem 2.2.2) is likewise self-contained, needing only the two-point probability hypothesis defining the Rademacher distribution.

Selected references

• W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of the American Statistical Association 58(301), 1963. https://doi.org/10.2307/2282952
• S. Bernstein, The Theory of Probabilities, Gastehizdat Publishing House, Moscow, 1946 (Russian; the inequality is due to Bernstein's earlier 1920s–1930s work, this textbook states the modern sub-exponential form following later expositions).
• A. C. Berry, The Accuracy of the Gaussian Approximation to the Sum of Independent Variates, Transactions of the American Mathematical Society 49(1), 1941. https://doi.org/10.2307/1990053
• C.-G. Esseen, On the Liapunoff Limit of Error in the Theory of Probability, Arkiv för Matematik, Astronomi och Fysik A28, 1942.
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 2. https://doi.org/10.1017/9781108231596

Motivation

Any dataset of $N$ points can be described exactly by embedding it in $\mathbb R^n$ for $n$ large enough — but a large $n$ is expensive: nearest-neighbor search, clustering, and streaming algorithms all scale with the ambient dimension, not with $N$. The question that opens this mission is whether the dimension can be cut down while leaving the data's geometry — the pairwise distances between points — essentially untouched.

Johnson and Lindenstrauss answered this in 1984, while studying extensions of Lipschitz maps into Hilbert space (W. Johnson, J. Lindenstrauss, Extensions of Lipschitz mappings into a Hilbert space, Contemp. Math. 26 (1984), 189–206): $N$ points in any Euclidean space, of any dimension $n$, can be mapped by a single linear map into a space of dimension only $O(\varepsilon^{-2}\log N)$, distorting every pairwise distance by at most a factor of $1\pm\varepsilon$. The map does not depend on the data beyond its cardinality — a single random object works simultaneously for the whole point set with high probability. This is now one of the standard tools of randomized dimension reduction, cited across nearest-neighbor search, streaming linear algebra, compressed sensing, and machine learning pipelines that need to shrink feature dimension before a downstream algorithm runs.

Setting

Fix a probability space $(\Omega,\mathcal F,\mathrm{Prob})$. A random orthogonal projection of rank $m$ in $\mathbb R^n$ is a map $P:\Omega\to(\mathbb R^n\to\mathbb R^n)$, continuous and linear for each $\omega$, such that almost surely $P_\omega$ is idempotent ($P_\omega\circ P_\omega = P_\omega$), self-adjoint, and has range of dimension $m$ — i.e. $P_\omega$ is the orthogonal projection onto some $m$-dimensional subspace $E_\omega\subset\mathbb R^n$. It is uniformly distributed in the Grassmannian $G_{n,m}$ (written $E\sim\mathrm{Unif}(G_{n,m})$) when its law is rotation invariant: for every orthogonal transformation $U$ of $\mathbb R^n$, the conjugated map $\omega\mapsto U\circ P_\omega\circ U^{-1}$ has the same law as $P$. Conjugating a projection by $U$ is exactly the projection onto the image of its range under $U$, so this says the law of the random subspace $E=\mathrm{range}(P)$ is invariant under the full orthogonal group — the operational definition Vershynin himself uses for a "uniformly distributed" random subspace, since no coordinate-free formula for such a subspace's law is given directly.

A companion notion drives the proof: a random vector $X$ is uniform on the Euclidean sphere of radius $r$, $X\sim\mathrm{Unif}(r\,S^{n-1})$, when it lies on that sphere almost surely and its law is likewise rotation invariant. And a real random variable $Y$ is sub-gaussian with sub-gaussian ($\psi_2$) norm $\|Y\|_{\psi_2} := \inf\{t>0:\mathbb E\exp(Y^2/t^2)\le 2\}$, the standard non-asymptotic measure of how light-tailed $Y$'s distribution is (a bounded or Gaussian random variable has finite $\psi_2$ norm; the tail probability $\mathbb P\{|Y|\ge s\}$ then decays at least as fast as $2\exp(-cs^2/\|Y\|_{\psi_2}^2)$).

Formalization targets

Goal (Theorem 5.3.1, Johnson-Lindenstrauss Lemma)

$$\exists\,C,c>0:\quad m\ge\frac{C}{\varepsilon^2}\log|X| \;\Longrightarrow\; \mathrm{Prob}\Bigl\{\forall x,y\in X:\ (1-\varepsilon)\|x-y\|_2\le \bigl\|\sqrt{\tfrac nm}\,P_\omega(x-y)\bigr\|_2\le(1+\varepsilon)\|x-y\|_2\Bigr\} \;\ge\;1-2\exp(-c\varepsilon^2 m)$$

for every finite $X\subset\mathbb R^n$, every $\varepsilon>0$, and every random orthogonal projection $P$ of rank $m$ uniformly distributed in $G_{n,m}$. The universal quantifier over pairs $x,y\in X$ sits inside the single probability event — this is the union-bound content that makes the statement a genuine simultaneous guarantee for the whole point set, not a restatement of the single-vector lemma below for one fixed pair. Both constants are the book's own unnamed absolute constants, never depending on $n$, $m$, $N=|X|$, or $\varepsilon$; this is the weakest stable form of the claim (no numeral is hard-coded for $C$ or $c$), matching the book's own statement exactly.

Significance

The lemma gives a universal, data-oblivious dimension-reduction guarantee: the target dimension $m=O(\varepsilon^{-2}\log N)$ depends only on the number of points and the desired distortion, never on the ambient dimension $n$ or on the geometry of the specific point set. This is what makes it usable as a black-box preprocessing step ahead of an algorithm whose cost scales with $n$ — the projection is drawn once, without looking at the data, and works with high probability for every pairwise distance simultaneously. The bound is also known to be essentially optimal in $N$: Alon (Problems and results in extremal combinatorics, Discrete Math. 273 (2003)) showed a lower bound of $\Omega(\varepsilon^{-2}\log N/\log(1/\varepsilon))$ on the target dimension, so the $\log N$ dependence cannot be removed.

The theorem itself has been proved for decades and admits several proof strategies (this book's route through Lipschitz concentration on the sphere; the original volume/measure-concentration argument; later "sparse" or structured variants of the projection for faster computation). This mission formalizes the classical dense-Gaussian-projection proof route as Vershynin presents it, building the sphere-concentration engine (Theorem 5.1.4) and the single-vector projection lemma (Lemma 5.3.2) that the union-bound argument for the goal rests on. No machine-checked formal proof of this chain is known to exist on the platform prior to this mission (see Formalization scope below); what is contributed is the statement infrastructure — the goal and its two direct supporting lemmas, stated with explicit, unpinned absolute constants — for solvers to close.

Difficulty

The natural first idea — bound the distortion of a single fixed vector under a random projection, then take a union bound over the $\binom N2$ pairwise differences — is exactly the strategy Lemma 5.3.2 and the goal use, but it does not by itself explain why the single-vector concentration bound (Lemma 5.3.2(b)) holds with the stated sub-gaussian-type tail. That bound is not elementary: it reduces to a uniform concentration statement for an arbitrary Lipschitz function of a uniformly random point on a high-dimensional sphere (Theorem 5.1.4), since $\|Pz\|_2$, viewed as a function of a rotated copy of $z$, is a $1$-Lipschitz function on the sphere. Proving that every Lipschitz function concentrates — not just linear ones, for which sub-gaussianity was already established in Chapter 3 — needs a genuinely different tool: comparing the sub-level sets of an arbitrary Lipschitz function to spherical caps via an isoperimetric inequality on the sphere. This geometric input is what makes the concentration phenomenon behind Johnson-Lindenstrauss a dimension-free fact rather than a special property of coordinate projections.

Formalization scope

$X$ is a Finset of points in EuclideanSpace ℝ (Fin n), matching "a set of $N$ points"; $N$ is read off as X.card. The random subspace $E\in G_{n,m}$ is represented throughout by the orthogonal projection $P$ onto it (IsUniformProjection), following the book's own statements, which are phrased in terms of $P$ rather than $E$; the scaled map $Q=\sqrt{n/m}\,P$ of the goal is written Real.sqrt (n/m) • P ω applied to x - y, using linearity of $P_\omega$ to realize $Qx-Qy = Q(x-y)$. Both "uniform on the sphere" and "uniform in the Grassmannian" are defined operationally by rotation invariance of the underlying law, since Mathlib has no ready-made normalized surface measure on a general-radius Euclidean sphere or Haar-measure construction on the Grassmannian/orthogonal group to build a canonical uniform object from; rotation invariance uniquely determines the corresponding measure among those supported on the relevant set, so the operational and constructive definitions coincide extensionally. Every "absolute constant" in the book ($C$ in Theorem 5.3.1's sample-complexity hypothesis, $c$ in every failure-probability bound, and the sub-gaussian constant $C$ of Theorem 5.1.4) is existentially quantified ahead of the dimension, sample size, and every other object, and pinned to no numeral — a formalization that hard-coded a specific numeral for any of these would be invalidated by the next sharper constant in the literature and would not match what the book actually proves.

A trivializing formalization is one that states the conclusion for a single fixed pair $x,y$ rather than universally over all pairs inside one event; that would collapse the union-bound content that makes this a dimension-reduction statement for a whole point set (with $N$ points), rather than a restatement of the single-vector Lemma 5.3.2(b). This mission's goal statement is built to rule that out explicitly (see Formalization targets above).

Reusable infrastructure: subgaussianNorm (the Orlicz $\psi_2$ norm, restated per Vershynin Definition 2.5.6) and the rotation-invariance idiom for "uniformly distributed" random geometric objects are of independent interest to any later chapter needing sub-gaussian random vectors or random subspaces/projections (e.g. Chapters 4, 6, 7, 9, 11 of this same book series). Solvers' contributions are welcome on: the isoperimetric inequality on the sphere and its use to prove Theorem 5.1.4 (the mission's hardest open leaf); the coordinate-projection computation underlying Lemma 5.3.2(a); and the concentration-plus-union-bound argument closing the goal from the three supporting lemmas.

Selected references

• W. Johnson, J. Lindenstrauss, Extensions of Lipschitz mappings into a Hilbert space, Contemporary Mathematics 26 (1984), 189–206.
• N. Alon, Problems and results in extremal combinatorics, I, Discrete Mathematics 273 (2003), 31–53. https://doi.org/10.1016/S0012-365X(03)00227-9
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 5. https://doi.org/10.1017/9781108231596

Motivation

Many hard combinatorial optimization problems — finding the maximum cut of a graph, deciding the ground state of an Ising spin system, bounding the correlation of a physical system — can be written as maximizing a bilinear form over sign vectors $x_i \in \{-1, 1\}$. Exhaustive search over $2^n$ sign patterns is intractable, so practitioners relax the problem: replace each sign $x_i$ by a unit vector $X_i$ in a higher-dimensional space and optimize the resulting inner products instead. This relaxation, a semidefinite program, is convex and solvable in polynomial time. The question is how much is lost in the relaxation — whether its optimal value can be far from the true, combinatorial optimum.

Grothendieck's inequality, proved by Alexander Grothendieck in 1953 in the context of Banach space theory (Résumé de la théorie métrique des produits tensoriels topologiques, Bol. Soc. Mat. São Paulo 8 (1953), 1–79), answers this for a broad class of such relaxations: replacing signs by unit vectors in an arbitrary Hilbert space changes the optimal value by at most an absolute, dimension-free constant factor. The inequality has since become a standard tool across combinatorial optimization, Banach space geometry, and (via the Goemans-Williamson algorithm for maximum cut, Section 3.6 of the source) approximation algorithms; see U. Haagerup, The Grothendieck inequality for bilinear forms on $C^*$-algebras, Adv. Math. 56 (1985) for the tightest known constant, and Alon–Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35 (2006), for the algorithmic connection this mission's Theorem 3.5.6 sets up.

Setting

Fix positive integers $m, n$. Consider a real $m \times n$ matrix $A = (a_{ij})$. Say $A$ is normalized if for every choice of numbers $x_1, \dots, x_m, y_1, \dots, y_n \in \{-1, 1\}$,

$$\Bigl| \sum_{i=1}^m \sum_{j=1}^n a_{ij}\, x_i y_j \Bigr| \;\le\; 1.$$

This says $A$, viewed as a bilinear form on $\{-1,1\}^m \times \{-1,1\}^n$, has sup-norm at most $1$. Now let $H$ be any real Hilbert space — a real vector space equipped with an inner product $\langle \cdot, \cdot \rangle$ complete in the induced norm — and consider vectors $u_1, \dots, u_m \in H$ and $v_1, \dots, v_n \in H$, each of unit norm $\|u_i\| = \|v_j\| = 1$. Replacing the scalar product $x_i y_j$ by the inner product $\langle u_i, v_j \rangle$ in the same bilinear form gives $\sum_{i,j} a_{ij} \langle u_i, v_j \rangle$, a real number depending on the choice of $H$ and of the unit vectors. The question is how large this can be, uniformly over every such choice.

Formalization targets

Grothendieck's inequality (Theorem 3.5.1)

$$A \text{ normalized} \;\Longrightarrow\; \Bigl| \sum_{i,j} a_{ij}\, \langle u_i, v_j\rangle \Bigr| \;\le\; K$$

for every real Hilbert space $H$ and unit vectors $u_i, v_j \in H$, where $K$ is a constant depending on neither $A$, its dimensions, nor $H$. This mission's goal formalizes the book's own first-pass bound $K \le 288$ (Section 3.5), proved by a Gaussian truncation argument; it does not fix a numeral for $K$, only that some absolute constant works, matching the shape of the true statement rather than a specific numeral that a sharper argument (the book's own Section 3.7 gives $K \le 1.783$) would immediately obsolete. See Formalization scope below for why this is the goal, not the sharper bound.

Significance

The result itself. Grothendieck's inequality is the single fact that makes semidefinite relaxation a provably good algorithmic strategy rather than a heuristic: whatever the true, hard-to-compute combinatorial optimum of a $\{-1,1\}$-valued bilinear optimization is, the tractable Hilbert-space relaxation cannot overshoot it by more than the constant $K$. Milestone Theorem 3.5.6 makes this concrete for positive-semidefinite matrices, showing the semidefinite relaxation SDP$(A)$ of the integer program INT$(A)$ satisfies INT$(A) \le$ SDP$(A) \le 2K \cdot$ INT$(A)$ — the guarantee underlying the Goemans-Williamson 0.878-approximation algorithm for maximum cut (Theorem 3.6.5 of the source, out of scope for this mission; see Formalization scope).

Formalizing it. The inequality and its two chapter milestones are proved but not previously formalized on this platform (checked by concept search for "Grothendieck", "semidefinite", "positive-semidefinite", and "max-cut" — no hits beyond the unrelated Grothendieck-Teichmüller group). What remains after this mission is the sharper $K \le 1.783$ argument of Section 3.7 (the "kernel trick"), a separate, heavier development building on positive-definite kernels, and full proofs of every milestone below (currently open sorry goals).

Difficulty

The statement of Grothendieck's inequality contains no randomness, yet every known elementary proof is probabilistic; this is itself a striking feature of the result. The obvious approach — bound $\sum_{i,j} a_{ij}\langle u_i,v_j\rangle$ directly by exploiting the normalization hypothesis on $A$ — fails because the normalization hypothesis only controls $A$ against sign vectors, and there is no way to project an arbitrary unit vector in a Hilbert space onto $\{-1,1\}$ without losing information. The book's proof instead represents each unit vector $u_i, v_j$ via a scalar Gaussian random variable $\langle g, u_i\rangle$ for a single Gaussian vector $g$, recovering the inner products in expectation (Exercise 3.3.5); but these Gaussian variables are unbounded, so the normalization hypothesis (which bounds $A$ against bounded $\pm 1$ inputs) cannot be applied to them directly. The core technical step is a truncation argument: splitting each Gaussian variable into a bounded part and a small-$L^2$-norm unbounded remainder, applying the hypothesis to the bounded parts, and bounding the remainder terms by treating them as elements of the Hilbert space $L^2$ and invoking the very inequality being proved (Theorem 3.5.1 itself, applied with $H = L^2$) as a self-referential bootstrap — this is why the proof fixes $K$ as the smallest valid constant before starting, rather than building it up from scratch.

Formalization scope

The goal and both milestones work with the real matrix and real inner product space directly; H is required to be a complete real inner product space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace), matching the book's "any Hilbert space." No dimension bound on $H$ is imposed — the inequality's content is exactly that $K$ does not grow with $\dim H$.

This mission does not formalize the sharper $K \le 1.783$ bound of Section 3.7, nor Theorem 3.6.5 (the 0.878-approximation guarantee for maximum cut via randomized rounding): the latter's statement quantifies over "the result of a randomized rounding of the solution of the semidefinite program," which would drag a specific algorithm into the audited statement rather than keeping it a self-contained mathematical claim (the statement/proof-separation trap this series' triage rubric flags). Grothendieck's identity (Lemma 3.6.6), the key fact behind that rounding step, is included on its own as a milestone, stated with an explicit, named random sign variable rather than an opaque "rounding procedure."

A trivializing formalization would state the goal with $K$ allowed to depend on $A$, $m$, $n$, or $H$ — every such bound is easy (e.g. $K = \sum_{ij} |a_{ij}|$) and carries none of the theorem's content; the Lean statement rules this out by quantifying $K$ before every other object. $\mathrm{INT}(A)$ and $\mathrm{SDP}(A)$ (Theorem 3.5.6) are defined from scratch in this chunk's namespace, using Matrix.PosSemidef from Mathlib for the positive-semidefiniteness hypothesis (which bundles the real-symmetric condition); Mathlib has no ready-made SDP-value construction to reuse. The sub-gaussian (Orlicz $\psi_2$) norm used by Theorem 3.1.1 is reused, unchanged, from the 01-concentration mission in this series (HighDimProb.Concentration.SubgaussianNorm) rather than redefined.

Selected references

• A. Grothendieck, Résumé de la théorie métrique des produits tensoriels topologiques, Bol. Soc. Mat. São Paulo 8 (1953), 1–79.
• U. Haagerup, The Grothendieck inequality for bilinear forms on $C^*$-algebras, Adv. Math. 56 (1985), 93–116.
• N. Alon, A. Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35 (2006), 787–803.
• M. X. Goemans, D. P. Williamson, Improved approximation algorithms for maximum cut and satisfiability problems using semidefinite programming, J. ACM 42 (1995), 1115–1145.
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 3, DOI 10.1017/9781108231596.

Motivation

A recurring question in high-dimensional statistics is how tightly a scalar quantity built from many random inputs concentrates around its mean, even as the number of inputs grows without bound. Two classical answers organize the whole toolkit: martingale methods, which control a sum of dependent increments one conditional step at a time, and Gaussian-specific isoperimetry, which shows that essentially any regular (Lipschitz) function of a high-dimensional Gaussian vector concentrates as tightly as a single Gaussian coordinate, regardless of dimension. This mission formalizes one representative theorem from each line: the general martingale Bernstein bound (Wainwright, High-Dimensional Statistics, 2019, Theorem 2.19) and the Gaussian concentration of Lipschitz functions (Theorem 2.26), following Chapter 2 of the same book.

Setting

A random variable $X$ with mean $\mu=\mathbb E[X]$ is sub-Gaussian with parameter $\sigma$ (Definition 2.2) if $\mathbb E[e^{\lambda(X-\mu)}]\le e^{\sigma^2\lambda^2/2}$ for all $\lambda\in\mathbb R$; it is sub-exponential with parameters $(\nu,\alpha)$ (Definition 2.7, a strictly milder condition) if the same bound holds only for $|\lambda|<1/\alpha$, with the convention $1/0=+\infty$ so that $\alpha=0$ recovers the sub-Gaussian case exactly.

A sequence $\{D_k\}_{k\ge1}$, adapted to a filtration $\{\mathcal F_k\}$, is a martingale difference sequence if each $D_k$ is $\mathcal F_k$-measurable and $\mathbb E[D_k\mid\mathcal F_{k-1}]=0$. Such sequences arise throughout statistics via the Doob martingale construction: given a function $f$ of independent variables $X_1,\dots,X_n$, setting $D_k:=\mathbb E[f(X)\mid X_1,\dots,X_k]-\mathbb E[f(X)\mid X_1,\dots,X_{k-1}]$ telescopes to $f(X)-\mathbb E[f(X)]=\sum_k D_k$, converting a deviation question about $f(X)$ into a martingale concentration question.

A function $f:\mathbb R^n\to\mathbb R$ is $L$-Lipschitz with respect to the Euclidean norm if $|f(x)-f(y)|\le L\|x-y\|_2$ for all $x,y$ (Eq. (2.38)).

Formalization targets

Goal — Theorem 2.26 (Gaussian concentration of Lipschitz functions)

Let $(X_1,\dots,X_n)$ be i.i.d. standard Gaussian and $f$ be $L$-Lipschitz with respect to the Euclidean norm. Then $f(X)-\mathbb E[f(X)]$ is sub-Gaussian with parameter at most $L$, and hence

$$\mathbb P[|f(X)-\mathbb E[f(X)]|\ge t] \;\le\; 2e^{-t^2/2L^2} \qquad \text{for all } t\ge 0.$$

The bound is dimension-free: it depends on $n$ only through $f$'s Lipschitz constant, not the ambient dimension itself.

Milestone — Lemma 2.27 (Gaussian interpolation identity)

For any differentiable $f$ and convex $\varphi$, $\mathbb E[\varphi(f(X)-\mathbb E[f(X)])] \le \mathbb E[\varphi(\tfrac\pi2\langle\nabla f(X),Y\rangle)]$ for $X,Y\sim N(0,I_n)$ independent — the interpolation identity Theorem 2.26's proof is built on.

Milestone — Theorem 2.19 (martingale Bernstein bound)

Given a martingale difference sequence with a per-index sub-exponential conditional moment-generating-function bound $\mathbb E[e^{\lambda D_k}\mid\mathcal F_{k-1}]\le e^{\lambda^2\nu_k^2/2}$ for $|\lambda|<1/\alpha_k$, the sum $\sum_k D_k$ is itself sub-exponential with parameters $\big(\sqrt{\sum_k\nu_k^2},\ \max_k\alpha_k\big)$, and satisfies the two-regime concentration inequality of Eq. (2.28): sub-Gaussian for small deviations, sub-exponential for large ones. This is the chapter's central general-purpose martingale concentration tool.

Significance

Theorem 2.19 is the source of two of the most-cited concentration inequalities in the field — the Azuma–Hoeffding inequality (Corollary 2.20) and the bounded-differences/McDiarmid inequality (Corollary 2.21), both already faithfully covered elsewhere on the platform (azuma_hoeffding_two_sided, bounded_diff_martingale_two_sided) and included here as kind: reference milestones rather than redrafted. Theorem 2.26's Gaussian Lipschitz concentration is separately significant: it is the tool behind dimension-free operator-norm bounds for random matrices, concentration of the empirical spectral distribution, and much of the machinery of Chapters 5 and 6 of the same book.

Formalizing it. No faithful prior art exists on the platform for either the martingale Bernstein bound or Lipschitz-Gaussian concentration itself (a fresh search for "martingale Bernstein," "sub-exponential martingale," "Gaussian interpolation," and "Lipschitz concentration" returned no hits; the existing Vershynin-book item HighDimProb.Isoperimetry.lipschitz_concentration_sphere concentrates a Lipschitz function on the sphere, a different underlying space and a different proof from Theorem 2.26's Gaussian vector). Both goal-adjacent theorems and the Gaussian interpolation lemma are drafted here as open goals (:= by sorry); the two Azuma–Hoeffding/bounded-differences corollaries are reused from the platform's existing, already-proved formalizations.

Difficulty

The naive approach to Theorem 2.26 — try to bound $f(X)-\mathbb E[f(X)]$ directly via a Lipschitz-type argument in $\mathbb R^n$ — has no obvious route to a dimension-free bound, since a union bound over coordinates (or over an $\varepsilon$-net of the domain) picks up a factor that grows with $n$. The resolution, Lemma 2.27's interpolation identity, instead exploits a special structural fact about the Gaussian distribution — its rotation invariance — to replace the nonlinear quantity $f(X)-\mathbb E[f(X)]$ with the linear, and hence exactly computable, Gaussian quantity $\langle\nabla f(X),Y\rangle$, at the mild cost of a non-optimal constant. Theorem 2.19's difficulty is bookkeeping rather than a conceptual obstruction: the recursive conditioning step (Eq. (2.29)) must be iterated exactly $n$ times while keeping track of the interplay between the two parameters $\nu_k,\alpha_k$ per difference, and Proposition 2.9's two-regime tail bound (small-deviation sub-Gaussian behavior, large-deviation sub-exponential behavior) must be carried through unchanged into the final statement — dropping either regime understates what the theorem proves.

Formalization scope

Expectations are Bochner integrals against an explicit probability measure, with integrability required as an explicit hypothesis in IsSubGaussian and IsSubExponential (Mathlib's Bochner integral silently returns $0$ for a non-integrable function, which this mission's definitions rule out as a trivializing formalization). The sub-exponential condition's domain restriction |λ| < 1/α is realized as the disjunction α = 0 ∨ |λ| < 1/α, since Lean's real division convention 1/0 = 0 is exactly backwards from the book's own stated 1/0 = +\infty convention for the degenerate sub-Gaussian case.

"$X,Y\sim N(0,I_n)$ independent" (Lemma 2.27, Theorem 2.26) is formalized via Mathlib's HasGaussianLaw predicate together with explicit coordinatewise mean-zero and identity-covariance hypotheses, which together pin down the standard multivariate normal law, plus IndepFun. The inner product $\langle\nabla f(X),Y\rangle$ is realized as fderiv ℝ f (X ω) (Y ω), the Fréchet derivative applied to $Y(\omega)$ — equal to $\langle\nabla f(X(\omega)),Y(\omega)\rangle$ by the Riesz representation of the gradient on a Hilbert space, avoiding the need to separately construct a gradient vector field.

Theorem 2.19's printed parameter pair for part (a), "$(\sum_k\nu_k^2,\alpha_*)$," is formalized as $(\sqrt{\sum_k\nu_k^2},\alpha_*)$: Definition 2.7 parametrizes the sub-exponential MGF bound by $\nu$ (with $\nu^2$ appearing in the exponent), so a literal transcription of the printed pair's first entry would silently square the effective parameter and make part (a), read literally, inconsistent with part (b)'s own tail-bound formula (which the book derives from part (a) via the general sub-exponential tail bound, Proposition 2.9). The corrected pairing is the one the book's own proof actually establishes; see MODERATION_NOTES.md for the full derivation.

Out of scope for this mission: Proposition 2.5 (plain Hoeffding for a sum of independent sub-Gaussians), used in the book only as background for Theorem 2.26's proof and not redrafted, since the goal theorem's own statement does not depend on it once Lemma 2.27 is in hand.

Selected references

• M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019. DOI: 10.1017/9781108627771. Chapter 2.
• K. Azuma, "Weighted sums of certain dependent random variables," Tôhoku Mathematical Journal, 19:357–367, 1967.
• W. Hoeffding, "Probability inequalities for sums of bounded random variables," Journal of the American Statistical Association, 58:13–30, 1963.

Motivation

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

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

Setting

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

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

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

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

Formalization targets

Goal — Theorem 6.2.1 (Hanson-Wright inequality)

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

A Gaussian process is a family $(X_t)_{t\in T}$ of jointly Gaussian real random variables indexed by an arbitrary set $T$ — not necessarily time. The canonical example is $X_t = \langle g, t\rangle$ for $t$ ranging over a subset $T\subseteq\mathbb R^n$ and $g$ a standard Gaussian vector in $\mathbb R^n$; this single family already encodes questions as varied as the operator norm of a random matrix, the size of a random projection, and the metric complexity of a convex body. In every one of these applications the object of interest reduces to the same quantity: $E\sup_{t\in T} X_t$, the expected supremum of the process.

Bounding $E\sup_{t\in T} X_t$ directly is hard — computing it exactly is possible only in special cases, such as the reflection principle for Brownian motion. Slepian's inequality (David Slepian, 1962) sidesteps this by comparison: if a second Gaussian process $(Y_t)_{t\in T}$ has matching variances and at-least-as-large pairwise increments as $(X_t)_{t\in T}$, then $Y$'s supremum stochastically dominates $X$'s. This turns a hard direct estimate into a search for a simpler comparison process — the technique that Sudakov and Fernique later sharpened by dropping the equal-variance hypothesis (Theorem 7.2.11), and that Sudakov used to derive a purely geometric lower bound on $E\sup_{t\in T}X_t$ from the covering numbers of $(T,d)$ (Theorem 7.4.1, Sudakov's minoration inequality). Together these results are the entry point to the theory of Gaussian width and generic chaining that occupies the rest of the book (Chapters 7–9, 11), and they underlie sharp bounds on random matrices (Section 7.3), random projections (Chapter 9), and high-dimensional geometry more broadly (Adler and Taylor, Random Fields and Geometry, Springer, 2007; Talagrand, Upper and Lower Bounds for Stochastic Processes, Springer, 2014).

Setting

Fix a probability space $(\Omega,\mathcal F,P)$. A random process indexed by a set $T$ is a family $(X_t)_{t\in T}$ of real random variables on $\Omega$. It is a Gaussian process if every finite linear combination $\sum_{t\in T_0} a_t X_t$ ($T_0\subseteq T$ finite, $a_t\in \mathbb R$) is a (possibly degenerate) normal random variable — equivalently, every finite marginal $(X_t)_{t\in T_0}$ is a multivariate Gaussian vector. A process is mean zero if $EX_t = 0$ for every $t$.

For a mean zero process, the increments $d(t,s) := \lVert X_t - X_s\rVert_{L^2} = (E(X_t - X_s)^2)^{1/2}$ always define a (pseudo)metric on $T$ — the canonical metric — turning the otherwise unstructured index set into a metric space. For a metric space $(T,d)$ and $\varepsilon

0$, the **covering number**$N(T,d,\varepsilon)$is the smallest cardinality of a finite subset$N\subseteq T$such that every point of$T$is within$\varepsilon$of some point of$N$(an$\varepsilon$-net);$N(T,d,\varepsilon) := \infty$ if no finite net exists.

Because $T$ need not be countable, $\sup_{t\in T} X_t(\omega)$ need not be a measurable function of $\omega$. Following the book's own convention, every quantity built from this supremum — $E\sup_{t\in T}X_t$ and $P\{\sup_{t\in T}X_t\ge\tau\}$ — is instead defined through the process's finite-dimensional marginals: as the supremum, over finite nonempty $T_0\subseteq T$, of $E\max_{t\in T_0}X_t$ (respectively $P\{\max_{t\in T_0}X_t\ge\tau\}$). This sidesteps the measurability question entirely, at the cost of the quantity possibly being $+\infty$.

Formalization targets

Slepian's inequality (Theorem 7.2.1, goal)

Let $(X_t)_{t\in T}$ and $(Y_t)_{t\in T}$ be mean zero Gaussian processes with $EX_t^2 = EY_t^2$ and $E(X_t-X_s)^2 \le E(Y_t-Y_s)^2$ for all $t,s\in T$. Then for every $\tau\in\mathbb R$,

$$P\{\sup_{t\in T} X_t \ge \tau\} \le P\{\sup_{t\in T} Y_t \ge \tau\},$$

and consequently $E\sup_{t\in T} X_t \le E\sup_{t\in T} Y_t$.

Sudakov-Fernique's inequality (Theorem 7.2.11, milestone)

Under only the increment hypothesis $E(X_t-X_s)^2 \le E(Y_t-Y_s)^2$ (no equal-variance hypothesis),

$$E\sup_{t\in T} X_t \le E\sup_{t\in T} Y_t.$$

This is the weaker-hypothesis, strictly more applicable form: it is what Sudakov's minoration inequality and the sharp Gaussian random matrix bound of Section 7.3 both invoke.

Sudakov's minoration inequality (Theorem 7.4.1, milestone)

Let $(X_t)_{t\in T}$ be a mean zero Gaussian process with canonical metric $d$. For every $\varepsilon\ge 0$ at which $N(T,d,\varepsilon)=:N$ is finite,

$$E\sup_{t\in T} X_t \ge c\,\varepsilon\,\sqrt{\log N}$$

for an absolute constant $c>0$. This is the weakest, most stable form of the bound: it names no numerical value for $c$, so it survives any later sharpening of the constant.

Slepian's inequality, finite-dimensional case (Theorem 7.2.9, milestone)

The vector-indexed special case of Theorem 7.2.1 ($T$ finite), proved first by Gaussian interpolation and then extended to the general index set.

Significance

The results themselves. Slepian's inequality is the founding comparison theorem for Gaussian processes; Sudakov-Fernique's inequality is its practically indispensable generalization, used routinely to bound suprema of Gaussian processes without needing to track variances explicitly. Sudakov's minoration inequality is the first bridge from the probability of a Gaussian process to the metric geometry of its index set, complementing Dudley's upper bound (Chapter 8) and together giving matching bounds — up to a logarithmic factor, and exactly in many cases of interest — on $E\sup_{t\in T}X_t$ purely from the covering numbers of $(T,d)$. Downstream, this machinery gives the sharp bound $E\lVert A\rVert \le \sqrt m + \sqrt n$ on Gaussian random matrices (Section 7.3), underlies the Gaussian width used throughout convex geometry and compressed sensing (Chapters 9, 11), and bounds the covering numbers of polytopes and other convex sets (Corollary 7.4.4).

Formalizing it. All three inequalities are proved by the book (Gaussian interpolation and integration by parts for Slepian/Sudakov-Fernique; a direct application of Sudakov-Fernique to a well-chosen comparison process for Sudakov's minoration), so this mission's work is formalizing the statements faithfully and precisely — including the finite-marginal convention needed to make $E\sup_{t\in T}X_t$ and $P\{\sup_{t\in T}X_t\ge\tau\}$ meaningful for an uncountable index set without begging the underlying measurability question. The Gaussian interpolation technique itself (Lemmas 7.2.3, 7.2.5, 7.2.7) is not part of this mission's formalization scope; it is the proof method for the milestones and belongs to solvers closing them.

Difficulty

The obvious first idea — bound $E\sup_t X_t$ by controlling each $X_t$ separately, e.g. via a union bound over a net — throws away exactly the structure Slepian-type comparisons exploit: the joint Gaussianity across $t$, not marginal tail behavior at each fixed $t$. A union bound needs a net and a modulus of continuity to begin with; Slepian's and Sudakov-Fernique's inequalities need neither — they compare two processes directly through their covariance structure, which is what makes the technique (Gaussian interpolation: continuously deform the covariance of one process into the other's, and track how a smooth, nearly-indicator functional behaves along the path) work with no assumption on $T$ beyond the two hypotheses stated. The genuine difficulty is the smooth-interpolation argument itself — showing that $E f(Z(u))$ is monotone in $u$ for the right choice of test function $f$ — which is exactly the part left as a milestone for solvers to formalize, not sketched here per the mission format's own rule against proof ideas.

Formalization scope

$E\sup_{t\in T}X_t$ (ProcessESup) is valued in EReal, not ℝ: the finite-marginal supremum a real-valued definition would silently default to the junk value $0$ when the set of finite-marginal expectations is unbounded above — exactly the case the book itself records as $E\sup_{t\in T}X_t=\infty$ (Exercise 7.4.2, a non-relatively-compact index set). P\{\sup_{t\in T}X_t\ge\tau\} (ProcessTailProb) stays real-valued, since it is always bounded in $[0,1]$ and so carries no such risk. Both are defined through finite nonempty subsets of $T$, per the book's own footnote to Section 7.2; no separability, continuity, or countability assumption is placed on $T$ itself.

Gaussianity is Mathlib's ProbabilityTheory.IsGaussianProcess — every finite restriction of the process has a Gaussian law — which is definitionally the book's Definition 7.1.10 ("every finite linear combination is Gaussian"); mean-zero is stated as an explicit hypothesis alongside it. Integrability of every quantity appearing under an expectation is not stated as a separate hypothesis: Fernique's theorem (already in Mathlib for general Gaussian measures) guarantees a Gaussian process has finite moments of every order, exactly as the book takes for granted.

Sudakov's minoration inequality (Theorem 7.4.1) is formalized for the case the book's own proof actually covers — $N(T,d,\varepsilon)$ finite, taken as a hypothesis = (N : ℕ) rather than as a case split inside the conclusion — since the book itself defers the infinite-covering-number case to a separate, unproved exercise (7.4.2). This keeps $T$ fully general (still possibly uncountable) at every fixed $\varepsilon$ where the net is finite, which rules out a trivializing reading of the theorem: nothing here forces $T$ itself to be finite or countable, only the covering number at the scale $\varepsilon$ in play, which is the book's own hypothesis.

Definitions reusable beyond this mission: ProcessESup, ProcessTailProb, CanonicalMetric, and CoveringNumber are exactly the substrate Chapters 8 ("Dudley's Integral Inequality"), 9 ("The Matrix Deviation Inequality"), and 11 ("Dvoretzky-Milman's Theorem") need for Gaussian width and generic chaining; per this series' plan those missions restate them locally (drafts cannot import another draft's definitions), using this chunk's forms as the faithful reference. Contributions closing the Gaussian-interpolation machinery (Lemmas 7.2.3–7.2.8) as a reusable definitions layer, beyond what any one milestone needs, are welcome.

Selected references

• Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018. https://www.math.uci.edu/~rvershyn/papers/HDP-book/HDP-book.pdf
• D. Slepian, "The one-sided barrier problem for Gaussian noise", Bell System Technical Journal 41 (1962), 463–501.
• V. N. Sudakov, "Gaussian random processes and measures of solid angles in Hilbert space", Soviet Mathematics Doklady 12 (1971), 412–415.
• X. Fernique, "Regularité des trajectoires des fonctions aléatoires gaussiennes", in École d'Été de Probabilités de Saint-Flour IV-1974, Springer Lecture Notes in Mathematics 480 (1975), 1–96.
• M. Talagrand, Upper and Lower Bounds for Stochastic Processes: Modern Methods and Classical Problems, Springer, 2014.

Motivation

Many of the central questions of high-dimensional statistics reduce to bounding the expected supremum of a stochastic process: the maximum correlation of noise with a family of candidate signals, the operator norm of a random matrix, the uniform deviation of an empirical process from its mean. Whenever the index set of the process is infinite or exponentially large, a naive union bound over "all" indices is either vacuous or requires re-deriving a tail bound from scratch for every new problem. Chaining is the general-purpose technique that removes this need: it bounds the expected supremum of a process purely in terms of the geometry of its index set, measured by how many balls of a given radius are needed to cover it. The classical form of this bound is due to Dudley (1967), building on ideas that trace to Kolmogorov; the exposition here follows Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 5.

Setting

Fix an index set $T$ and a collection of zero-mean random variables $\{X_\theta,\theta\in T\}$. Say this collection is a sub-Gaussian process with respect to a (pseudo)metric $\rho_X$ on $T$ (Definition 5.16) if

$$\mathbb E\big[e^{\lambda(X_\theta-X_{\theta'})}\big] \;\le\; e^{\lambda^2\rho_X(\theta,\theta')^2/2} \qquad \text{for all } \theta,\theta'\in T,\ \lambda\in\mathbb R.$$

This single condition covers, as special cases, the canonical Gaussian process $X_\theta = \langle\theta, w\rangle$ for $w$ a standard Gaussian vector (with $\rho_X$ the Euclidean metric) and the Rademacher process built from i.i.d. Rademacher signs.

A $\delta$-cover of $T$ with respect to a metric $\rho$ is a finite set $\{\theta_1,\dots,\theta_N\}\subset T$ such that every $\theta\in T$ lies within $\rho$-distance $\delta$ of some $\theta_i$; the $\delta$-covering number $N(\delta;T,\rho)$ is the size of the smallest such cover (Definition 5.1). The quantity $\log N(\delta;T,\rho)$ is the metric entropy of $T$ at scale $\delta$. Writing $D:=\sup_{\theta,\theta'\in T}\rho_X(\theta,\theta')$ for the diameter of $T$, the $\delta$-truncated Dudley entropy integral is

$$J(\delta; D) \;:=\; \int_\delta^D \sqrt{\log N(u;T)}\,du.$$

Formalization targets

Goal — Theorem 5.22 (Dudley's entropy integral bound)

$$\mathbb E\Big[\sup_{\theta,\theta'\in T}(X_\theta-X_{\theta'})\Big] \;\le\; 2\,\mathbb E\Big[\sup_{\substack{\gamma,\gamma'\in T\\\rho_X(\gamma,\gamma')\le\delta}}(X_\gamma-X_{\gamma'})\Big] + 32\,J(\delta/4; D), \qquad \text{for any } \delta\in[0,D].$$

The bound holds for every zero-mean sub-Gaussian process, with no further structure on $T$ beyond its metric entropy — this is what makes it a general-purpose tool rather than a bound tailored to one model.

Milestone — Proposition 5.17 (one-step discretization bound)

The same conclusion with $32\,J(\delta/4;D)$ replaced by the cruder single-scale term $4\sqrt{D^2\log N(\delta;T)}$, under the extra technical hypothesis $N(\delta;T)\ge 10$. This is the one-step precursor whose refinement — iterating the discretization over a geometric sequence of scales instead of applying it once — is exactly what chaining improves.

Milestone — Theorem 5.25 (the Gaussian comparison principle)

A general comparison principle for pairs of centered Gaussian random vectors whose pairwise covariances are ordered coordinatewise and tested against a function with matching sign conditions on its mixed second partial derivatives: $\mathbb E[F(X)]\le\mathbb E[F(Y)]$. This is the source, by specializing $F$ and the covariance-ordering sets, of both Slepian's inequality and the Sudakov–Fernique comparison, the two workhorse tools of Gaussian process theory used elsewhere in the chapter to obtain sharper, Gaussian-specific bounds than the sub-Gaussian chaining bound above.

Significance

Dudley's bound is the single most-used tool for controlling suprema of stochastic processes in high-dimensional statistics and empirical process theory: Gaussian complexity bounds for convex bodies, operator-norm bounds for random matrices, and uniform laws of large numbers for function classes are all obtained by computing a covering-number bound for the relevant index set and substituting it into Theorem 5.22 (see, for instance, Examples 5.18–5.21 later in the same chapter, and Chapters 13–14 of the book). Its significance is exactly its generality: it converts a purely geometric quantity — how "big" a set is under a metric — into a probabilistic bound, uniformly over every sub-Gaussian process on that set.

Formalizing it. The mathematical proof (interpolation-free, based on chaining and repeated union bounds) is well understood and not itself in question; what this mission produces is a faithful Lean statement of the theorem, its immediate one-step precursor, and the general Gaussian comparison principle that underlies the chapter's complementary (Gaussian-specific) results, each against Mathlib's own measure-theoretic and Gaussian-process infrastructure. All three theorems are currently stated as open goals (:= by sorry); no claim is made here that they are already formalized elsewhere on the platform (a fresh prior-art search for "Dudley," "chaining," "Slepian," "Sudakov," and "Gaussian comparison" returned no faithful matches).

Difficulty

The naive approach — apply Proposition 5.17's one-step discretization once, at whatever scale $\delta$ seems best — cannot see improvement past the cruder $\sqrt{D^2\log N(\delta;T)}$ scaling of the metric entropy at a single resolution. The chaining argument that proves Theorem 5.22 instead telescopes the supremum across a geometric ladder of covers at scales $D2^{-1},D2^{-2},\dots$, paying for each scale's approximation with a union bound over its own (much smaller, for a small $\delta$) covering number, and only then summing the resulting terms into an integral. The difficulty is not any single step of this argument — each step is an elementary sub-Gaussian tail bound — but bookkeeping the composition correctly: the recursive "best approximation at level $m$ of the best approximation at level $m+1$" chain (Eq. (5.47)) must be built explicitly, and the telescoping sum of $L$ union bounds, each over a set that itself depends on the level $m$, is what converts into an integral only in the $L\to\infty$ limit as the covers refine to $T$ itself.

Formalization scope

The index set $T$ is formalized as a nonempty Fintype, rather than the book's general totally bounded metric space: this keeps every covering number, diameter, and supremum in this mission a genuine maximum over a finite, nonempty family (realized via ⨆/sInf over finite index types), rather than requiring the full apparatus of totally bounded infinite metric spaces to state the covering-number definition (Definition 5.1) faithfully without risking a vacuous or ill-defined infimum. This is a genuine narrowing of the book's stated generality, disclosed here rather than left implicit — the underlying mathematics of the proof does not depend on finiteness, but a faithful formalization of a general totally bounded space's covering number was judged out of scope for this mission's budget.

The constant $32$ in the goal theorem is kept exactly as stated; the book's own remark that "there is no particular significance to the constant 32, which could be improved with a more careful analysis" is not license to substitute a sharper constant, since doing so would no longer match what this particular proof establishes. Expectations are Bochner integrals against an explicit probability measure Prob, with integrability required as an explicit hypothesis in the sub-Gaussian process definition (SubGaussianProcess) rather than left implicit, since Mathlib's Bochner integral silently returns $0$ for a non-integrable function — a trivializing formalization this mission's definitions and hypotheses rule out.

Theorem 5.25's "centered Gaussian random vector" is formalized using Mathlib's own ProbabilityTheory.HasGaussianLaw predicate (a genuine multivariate Gaussian law, not merely Gaussian marginals) together with an explicit coordinatewise mean-zero hypothesis, and its mixed second partial derivative condition is formalized via iteratedFDeriv ℝ 2 F applied to the relevant pair of standard basis vectors, keeping the sign pattern over the disjoint index sets $A$ and $B$ exact rather than collapsing it to a global convexity assumption on $F$.

Out of scope for this mission: Sudakov's minoration (the complementary lower bound on the expected supremum of a genuinely Gaussian process, Theorem 5.30, misidentified as "Theorem 5.36" in this mission's planning brief — the correct Sudakov minoration statement is Theorem 5.30, p. 148; Theorem 5.36 is instead a tail-bound generalization of Dudley's bound to $\psi_q$-Orlicz processes) and the Slepian/Sudakov–Fernique corollaries of Theorem 5.25 (Corollary 5.26, Theorem 5.27) — both natural follow-on work for a later contribution, once the Gaussian comparison principle formalized here is in place.

Selected references

• M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019. DOI: 10.1017/9781108627771. Chapter 5.
• R. M. Dudley, "The sizes of compact subsets of Hilbert space and continuity of Gaussian processes," Journal of Functional Analysis, 1(3):290–330, 1967.
• M. Ledoux and M. Talagrand, Probability in Banach Spaces: Isoperimetry and Processes, Springer, 1991.

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

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

Formalization targets

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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