High-Dimensional Probability and Statistics

Motivation

Random matrices with independent entries appear whenever a system is measured through many noisy, roughly independent channels: shot noise in a sensor array, edges in an Erdős–Rényi-type random graph, or the design matrix of a linear model with independent covariates. A basic question about any such matrix $A$ is how far it can stretch a vector — its operator norm $\|A\|$ — since this single number controls the stability of every linear statistic computed from $A$: least-squares estimates, spectral clustering, covariance estimation, and random projections all reduce, at some point, to bounding $\|A\|$.

The theory traces to Marchenko and Pastur's 1967 asymptotic law for the spectrum of large random matrices, and to Bai and Yin's 1988 almost-sure limit $\|A\|/\sqrt n \to 2$ for $n \times n$ matrices with i.i.d. mean-zero, unit-variance entries. Those results are asymptotic: they say what happens as the dimension $n \to \infty$, for a fixed matrix shape. The result formalized here, Theorem 4.4.5 of Vershynin's High-Dimensional Probability (2018) (DOI 10.1017/9781108231596), belongs to the more recent non-asymptotic strand of the theory: it gives an explicit, dimension-free bound that holds at every fixed $m, n$, with an explicit failure probability — the form of statement needed for finite-sample guarantees in statistics and data science, rather than limiting behavior.

Setting

Let $A$ be an $m \times n$ real matrix. Equip $\mathbb R^n$ and $\mathbb R^m$ with the Euclidean norm $\|\cdot\|_2$; $A$ acts as a linear map $\ell_2^n \to \ell_2^m$. Its operator norm (§4.1.2) is

$$\|A\| \;:=\; \max_{x \in S^{n-1}} \|Ax\|_2 ,$$

the largest factor by which $A$ can stretch a unit vector; equivalently, the largest singular value of $A$.

A real random variable $X$ is sub-gaussian with the mission's own convention (matching the Orlicz $\psi_2$ norm this series already carries as a published definition, HighDimProb.Concentration.subgaussianNorm) if

$$\|X\|_{\psi_2} \;:=\; \inf\{t > 0 : \mathbb E \exp(X^2/t^2) \le 2\} \;<\; \infty .$$

Bounded random variables and Gaussians are sub-gaussian; a Bernoulli($p$) variable and a $\pm 1$-valued coin flip both qualify, which is why the theorem below directly covers random matrices with i.i.d. Rademacher or Gaussian entries as special cases.

The mission's proof technique is the ε-net argument, developed in §4.2 and used nowhere before this chapter of the book: a metric space $(T,d)$, a subset $K \subseteq T$, and $\varepsilon > 0$ give rise to an ε-net $N \subseteq K$ — a finite set such that every point of $K$ is within $\varepsilon$ of some point of $N$ — and a covering number $N(K, d, \varepsilon)$, the smallest cardinality of such a net. The technique reduces a statement that must hold uniformly over an infinite (compact) set to a statement about finitely many points, paid for by a union bound whose cost is controlled by the covering number.

Formalization targets

Goal (Theorem 4.4.5)

$$\exists\, C > 0 \;\text{such that}\; \forall\, t > 0,\quad \mathrm{Prob}\bigl\{\, \|A\| \le CK(\sqrt m + \sqrt n + t) \,\bigr\} \;\ge\; 1 - 2\exp(-t^2),$$

for any $m \times n$ random matrix $A$ with independent, mean-zero, sub-gaussian entries $A_{ij}$ and $K = \max_{i,j} \|A_{ij}\|_{\psi_2}$. This is the weakest stable form of the bound — it fixes no numerical value for $C$, only its existence and absoluteness (independence from $m$, $n$, $A$, $t$), so later refinements of the constant do not invalidate it.

Significance

The result itself. The bound $\|A\| \lesssim \sqrt m + \sqrt n$ is sharp up to the constant: for entries of unit variance, $\mathbb E\|A\| \ge \tfrac14(\sqrt m + \sqrt n)$ for large $m, n$ (the book's Exercise 4.4.7), so no non-asymptotic bound of this shape can be improved beyond constants. It is the entry point to the rest of the book's random matrix theory: Corollary 4.4.8 specializes it to symmetric matrices, and it underlies the community-detection (§4.5) and covariance-estimation (§4.7) applications later in the same chapter, neither of which is part of this mission.

Formalizing it. The theorem is a classical, fully proved result; nothing about its truth is open. What this mission contributes is a machine-checked formal statement — together with the two pieces of chapter infrastructure its own textbook proof names by number (Corollary 4.2.13, Exercise 4.4.3(a)) — and a third, self-contained application of the same covering-number machinery (Theorem 4.3.5) that exercises the shared IsEpsNet/coveringNumber definitions on a different metric space (the Hamming cube), independently of the Euclidean case. Mathlib and the Prove2Me platform currently have no ε-net, covering-number, or packing-number infrastructure (checked by q=random matrix, q=operator norm, q=covering number, q=net on the platform, and by filename search in Mathlib): this mission is the first to introduce it, restated inside its own namespace since it is not otherwise available to build on.

Difficulty

The obvious first approach is to bound $\|A\| = \max_{x \in S^{n-1}} \|Ax\|_2$ directly by union-bounding a concentration inequality over the sphere $S^{n-1}$. This fails outright: $S^{n-1}$ is infinite (indeed uncountable) for $n \ge 2$, so no union bound over its points can converge — the naive approach gives $\infty \cdot (\text{tail probability})$. The ε-net argument is the fix, but it is not just "discretize and hope": the reduction from the sphere to a finite net (quadratic_form_on_net, Exercise 4.4.3(a)) loses a multiplicative factor $1/(1-2\varepsilon)$ that must be tracked, and the net's cardinality (covering_numbers_of_euclidean_ball_and_sphere, Corollary 4.2.13) is exponential in the dimension ($9^n$ at $\varepsilon = 1/4$) — so the per-point tail probability from Hoeffding-type concentration must itself decay fast enough (quadratically in the exponent) to survive multiplying by $9^{m+n}$ many points. Getting the union bound to close requires choosing the threshold $u$ in the tail bound proportionally to $\sqrt m + \sqrt n + t$, not to $t$ alone — the $\sqrt m + \sqrt n$ term is exactly what pays for the net's exponential size.

Formalization scope

$A$ is represented as Ω → Matrix (Fin m) (Fin n) ℝ; its entries A ω i j are the individual real random variables. Independence of the $mn$ entries is iIndepFun over the index type Fin m × Fin n; mean-zero is the vanishing of each entry's Bochner integral. The operator norm is the norm of the associated continuous linear map between EuclideanSpace ℝ (Fin n) and EuclideanSpace ℝ (Fin m) (matrixOpNorm, every linear map between finite-dimensional normed spaces being automatically continuous), matching the book's maxₓ∈Sⁿ⁻¹ ‖Ax‖₂ exactly. The sub-gaussian norm $K$ reuses this series' own published definition, HighDimProb.Concentration.subgaussianNorm, rather than a re-derivation. Covering numbers (coveringNumber) are restricted to finite (Finset) ε-nets, the only kind this chapter uses; this is a deliberate restriction, not a general-purpose covering-number formalization, and is disclosed as such. A hard-coded numeral for $C$, or an unquantified "with high probability" in place of the explicit failure probability $2\exp(-t^2)$, would each trivialize the statement and is ruled out: $C$ is existentially bound ahead of every other quantifier, and $t > 0$ is a free parameter with its own explicit bound, exactly as the book states it.

Definitions reusable beyond this mission: IsEpsNet and coveringNumber are stated for a general PseudoMetricSpace and apply unchanged to any later chapter's covering-number needs (e.g. Chapter 8's VC-dimension covering numbers), though per this series' rule that drafts cannot import drafts, a later chunk would restate rather than import them until this mission is published. matrixOpNorm is likewise chapter-agnostic. Contributions completing the sorry proofs of any of the four theorem items are welcome and independent of one another; the covering number and net-reduction items (covering_numbers_of_euclidean_ball_and_sphere, quadratic_form_on_net) are the standard prerequisites for the goal's own volumetric/ε-net proof.

Selected references

• Vershynin, R. High-Dimensional Probability: An Introduction with Applications in Data Science. Cambridge University Press, 2018. DOI 10.1017/9781108231596
• Bai, Z. D., Yin, Y. Q. "Necessary and sufficient conditions for almost sure convergence of the largest eigenvalue of a Wigner matrix." Annals of Probability 16 (1988), 1729–1741.
• Marchenko, V. A., Pastur, L. A. "Distribution of eigenvalues for some sets of random matrices." Mathematics of the USSR-Sbornik 1 (1967), 457–483.

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

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

Goal (Theorem 8.1.3, Dudley's integral inequality)

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

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

Milestone (Theorem 8.3.16, Sauer-Shelah lemma)

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

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

Significance

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

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

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

Difficulty

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

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

Formalization scope

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

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

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

Selected references

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

Motivation

Random matrices with independent rows are the workhorse of high-dimensional statistics and compressed sensing: sample covariance matrices, sub-sampled measurement operators, and randomized sketches are all of this form. A basic question about such a matrix $A$ is how close $\|Ax\|_2$ stays to its typical size $\mathbb E\|Ax\|_2\approx\sqrt m\|x\|_2$ — not just for one fixed $x$, but simultaneously for every $x$ in some set $T$ of interest (a sphere, a cone, the difference set of a data cloud). A bound that holds only pointwise in $x$ is of limited use, since most applications need to reason about the worst case over an entire geometric set at once.

This chapter proves such a uniform bound — the matrix deviation inequality — for matrices with independent, isotropic, sub-gaussian rows, controlling the deviation by a single geometric parameter of $T$, its Gaussian complexity. The result is a direct descendant of the chaining machinery of Chapter 8 (via Talagrand's comparison inequality, Chapter 8.6) and, in this book's own account, subsumes several results proved earlier by other methods — two-sided bounds on random matrices, the Johnson-Lindenstrauss lemma for infinite sets — while also yielding two new consequences central to high-dimensional convex geometry: the $M^*$ bound and the Escape theorem, both controlling how a random subspace intersects a fixed geometric set.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$. A random vector $X$ in $\mathbb R^n$ is isotropic if its covariance matrix is the identity, $\Sigma(X)=\mathbb E[XX^\top]=I_n$ — equivalently (the book's own Lemma 3.2.3), $\mathbb E\langle X,x\rangle^2=\|x\|_2^2$ for every $x\in\mathbb R^n$. The sub-gaussian norm of a random vector $X$ is $\|X\|_{\psi_2}:=\sup_{x\in S^{n-1}}\|\langle X,x\rangle\|_{\psi_2}$, the supremum over the unit sphere of the scalar sub-gaussian (Orlicz $\psi_2$) norm of its one-dimensional marginals; $X$ is sub-gaussian when this is finite.

Fix a standard Gaussian random vector $g\sim N(0,I_n)$ in $\mathbb R^n$ (a vector whose coordinates in any orthonormal basis are independent standard normal). For a subset $T\subseteq\mathbb R^n$, the Gaussian width and Gaussian complexity of $T$ are

$$w(T) := \mathbb E\sup_{x\in T}\langle g,x\rangle, \qquad \gamma(T) := \mathbb E\sup_{x\in T}|\langle g,x\rangle|,$$

two closely related measures of the geometric size of $T$ — "cousins" that agree up to a factor of $2$ whenever $T$ contains the origin, and agree exactly when $T$ is origin-symmetric.

Formalization targets

Goal (Theorem 9.1.1, Matrix deviation inequality)

$$\exists\,C>0:\quad \mathbb E\sup_{x\in T}\bigl|\,\|Ax\|_2-\sqrt m\|x\|_2\,\bigr| \;\le\; CK^2\gamma(T)$$

for every $m\times n$ matrix $A$ whose rows $A_1,\dots,A_m$ are independent, isotropic, sub-gaussian random vectors with $K:=\max_i\|A_i\|_{\psi_2}$, and every $T\subseteq\mathbb R^n$ (whenever $\gamma(T)$ is finite). $C$ is the book's own unnamed absolute constant, hard-coded to no numeral — the weakest stable form of the claim.

Milestone (Theorem 9.4.2, the $M^*$ bound)

$$\mathbb E\,\mathrm{diam}(T\cap\ker A) \;\le\; \frac{CK^2w(T)}{\sqrt m}$$

for the same class of matrices $A$ and any bounded $T\subseteq\mathbb R^n$, where $\ker A$ is the (random) kernel of $A$, a subspace of codimension at most $m$. A direct one-paragraph consequence of the goal theorem (apply it to $T-T$, then restrict to $\ker A$, where $\|Ax-Ay\|_2$ vanishes).

Significance

The matrix deviation inequality converts a purely algebraic quantity — how close $\|Ax\|_2$ stays to $\sqrt m\|x\|_2$ — into a single geometric parameter of the index set $T$, letting it subsume, via specializations of $T$, results that were previously proved by separate ad hoc arguments: two-sided singular value bounds on random matrices ($T$ a sphere), Johnson-Lindenstrauss-type embeddings for possibly infinite point sets ($T$ a difference set), and covariance estimation. The $M^*$ bound is one of the two classical consequences the book develops fresh from the inequality (the other, the Escape theorem, is outside this mission's scope): it answers, quantitatively, how large a random affine section of a fixed convex body typically is, a question at the heart of the local theory of Banach spaces and of compressed sensing's recovery guarantees (Chapter 10 builds directly on this chapter's machinery). Both results have long-standing, well-understood classical proofs; this mission formalizes their statements, not open research.

Difficulty

The natural first idea — bound $\|Ax\|_2-\sqrt m\|x\|_2$ pointwise for a fixed $x$ using concentration of the norm of a sub-gaussian random vector, then take a union bound over $T$ — only works when $T$ is finite, and gives a bound that scales with $\log|T|$ rather than with the actual geometric size of $T$. The book's actual route treats $X_x:=\|Ax\|_2-\sqrt m\|x\|_2$, indexed by $x\in\mathbb R^n$, as a genuine random process and shows it has sub-gaussian increments ($\|X_x-X_y\|_{\psi_2}\le CK^2\|x-y\|_2$) — itself a nontrivial fact proved in stages (first for a single unit vector via concentration of the norm, Theorem 3.1.1; then for a pair of unit vectors via a squared-process argument; only then in full generality) — and then invokes Talagrand's comparison inequality (a consequence of the chaining machinery of Chapter 8) to pass from sub-gaussian increments directly to a bound in terms of Gaussian complexity, without ever performing a union bound over $T$ itself.

Formalization scope

A is represented by its rows, A : Fin m → Ω → EuclideanSpace ℝ (Fin n), with ‖Ax‖₂ recovered as Real.sqrt (∑ i, ⟨Aᵢ,x⟩²) rather than constructing A as a Matrix/LinearMap — this matches the book's own row-by-row hypotheses exactly and is what both theorems' own proofs use directly. IsIsotropic is formalized via the book's basis-free Lemma 3.2.3 characterization (E⟨X,x⟩² = ‖x‖² for every x) rather than the matrix equation Σ(X)=Iₙ, avoiding a fixed-basis covariance-matrix construction the rest of this chunk's definitions do not otherwise need. SubgaussianVectorNorm reuses the published scalar subgaussianNorm. GaussianWidth and GaussianComplexity realize the standard Gaussian vector g ∼ N(0,Iₙ) as the identity map on Mathlib's own standard Gaussian measure on a finite-dimensional inner product space (ProbabilityTheory.stdGaussian), and both, together with the goal's own left-hand side, use a locally-defined finite-marginal expected-supremum convention (ExpSup, EReal-valued) matching the book's own footnote-3 convention (Section 7.2), reused throughout the series. Both theorems' right-hand sides presuppose their respective geometric parameter ($\gamma(T)$ or $w(T)$) is a finite real number; since both are EReal-valued in general, each theorem takes an explicit real witness together with a proof that it equals the true value — the same finiteness-disclosure pattern 07-chaining's Dudley inequality uses for its own right-hand integral, needed here for exactly the same reason (the book's own display does not spell out why the quantity is finite, true whenever $T$ is bounded, as in every application). $C$ (and, in the milestone, the same $C$ again — the two are not asserted equal, matching that the book states them as two separate "absolute constants") is existentially quantified before every type, instance and hypothesis it is uniform over. The $M^*$ bound milestone (m_star_bound) additionally carries the hypothesis $m > 0$: its conclusion divides by $\sqrt m$, and without this hypothesis Lean's real-division convention ($x/0=0$) makes the right-hand side $0$ at $m=0$ regardless of $C, K, w(T)$ — false whenever $T$ has positive diameter, not merely a weaker or vacuous claim. The book's own proof ("Dividing by $\sqrt m$ yields …", p. 241) already implicitly assumes $m \ge 1$, matching every other use of $m$ in the chapter as a positive count of measurement rows.

A trivializing formalization would fix $T$ to be a finite set, collapsing the goal to the elementary union-bound case the book explicitly contrasts its own more general statement against (Section 9.1's opening paragraph: "we may choose an arbitrary subset $T\subseteq\mathbb R^n$"); this mission's goal quantifies over an arbitrary Set (EuclideanSpace ℝ (Fin n)) to rule that out.

This mission covers Theorem 9.1.1 and Theorem 9.4.2 only; Theorem 9.4.7 (the Escape theorem) and Theorem 9.2.4 (covariance estimation for lower-dimensional distributions), both named as candidate milestones, are left out for lack of session time given the substantial shared infrastructure this chapter needed from scratch. ExpSup, IsIsotropic, SubgaussianVectorNorm, GaussianWidth and GaussianComplexity are reusable by any later chapter needing an isotropic or sub-gaussian random vector, or a Gaussian-width-type quantity (Chapters 4, 10, 11 of this same book series all use one or more of these notions). Solvers' contributions are welcome on: Theorem 9.1.3 (the sub-gaussian increments of the deviation process, the technical heart of the goal's proof), Talagrand's comparison inequality itself (outside this mission, in 07-chaining's companion chapter), and the one-paragraph reduction from the goal to the $M^*$ bound.

Selected references

• S. Mendelson, A. Pajor, N. Tomczak-Jaegermann, Reconstruction and subgaussian operators in asymptotic geometric analysis, Geometric and Functional Analysis 17 (2007), 1248–1282. https://doi.org/10.1007/s00039-007-0618-7
• V. D. Milman, A new proof of A. Dvoretzky's theorem on cross-sections of convex bodies, Funkcional. Anal. i Priložen. 5 (1971), 28–37.
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 9. https://doi.org/10.1017/9781108231596

Motivation

A striking fact discovered by Dvoretzky in the 1960s (conjectured by Grothendieck, and sharpened into its modern quantitative form by Milman in 1971) is that every high-dimensional convex body, however irregular, contains a round slice: a random low-dimensional section (or projection) of any bounded convex set in $\mathbb R^n$ is, with high probability, close to a Euclidean ball — provided the dimension of the slice is small enough relative to a single geometric parameter of the body. This is remarkable because it holds for every bounded set, arbitrarily irregular; no special structure is assumed beyond boundedness. This chapter proves the theorem in its Gaussian form, as a culmination of every geometric and probabilistic tool the book develops: chaining and Dudley's inequality (Chapter 8), the matrix deviation inequality (Chapter 9), and Gaussian width and the stable dimension (Chapter 7) all combine into a single closing argument.

Setting

Fix a subset $T\subseteq\mathbb R^n$. For a standard Gaussian vector $g\sim N(0,I_n)$, the Gaussian width of $T$ is $w(T) := \mathbb E\sup_{x\in T}\langle g,x\rangle$ (Chapter 7), and the stable dimension of a bounded $T$ is $d(T) := w(T)^2/\mathrm{diam}(T)^2$ up to an absolute constant factor (Definition 7.6.2) — a robust substitute for the ordinary linear-algebraic dimension of $T$, which can jump discontinuously under a small perturbation of $T$, unlike $d(T)$.

An $m\times n$ Gaussian random matrix with i.i.d. $N(0,1)$ entries is a random matrix $A$ each of whose $mn$ entries is an independent standard normal random variable.

Formalization targets

Goal (Theorem 11.3.3, Dvoretzky-Milman's theorem, Gaussian form)

$$\exists\,c>0:\quad m\le c\varepsilon^2 d(T) \;\Longrightarrow\; \mathbb P\bigl[(1-\varepsilon)B \subseteq \mathrm{conv}(AT) \subseteq (1+\varepsilon)B\bigr] \ge 0.99$$

for every $m\times n$ Gaussian random matrix $A$ with i.i.d. $N(0,1)$ entries, every bounded $T\subseteq\mathbb R^n$ containing the origin, and every $\varepsilon\in(0,1)$, where $B$ is the Euclidean ball of radius $w(T)$ centered at the origin. The probability $0.99$ is the book's own literal numeral, not a free parameter — this is the theorem the book actually states, not a family of theorems indexed by a confidence level.

Significance

Dvoretzky-Milman's theorem is one of the foundational results of the local theory of Banach spaces (asymptotic geometric analysis): it says every $n$-dimensional normed space contains an almost-Euclidean subspace of dimension proportional to (a geometric invariant closely related to) $\log n$ in the worst case, and much larger for spaces whose unit ball is already well-behaved (the stable dimension of the cube $[-1,1]^n$, for instance, is proportional to $n$ itself — Example 11.3.6). This underlies results throughout convex geometry, compressed sensing, and high-dimensional statistics wherever a random low-dimensional projection needs to be shown to preserve geometric structure. The book's own framing makes clear why this chapter is placed last: the theorem's proof is a genuine capstone, invoking Chevet's inequality (itself built from the matrix deviation inequality of Chapter 9, which is built from chaining, Chapter 8) as its main technical tool.

The theorem and its proof are classical (Milman 1971; this book's specific route via Chevet's inequality is a standard modern exposition). This mission formalizes the goal theorem's statement — including its two supporting geometric quantities, Gaussian width and stable dimension, and the notion of a Gaussian random matrix — as a complete, faithful target for a solver, in the book's own sub-namespace built for this chapter (no dependency here is reusable from an earlier chunk, since none of this book series' Chapter 7 or Chapter 9 definitions has yet been published).

Difficulty

The natural first idea — bound $\mathrm{conv}(AT)$ directly using concentration of $\|Ax\|_2$ for each fixed $x\in T$ — runs into exactly the uniform-supremum obstacle the whole book has been building tools to overcome: a bound that holds for one $x$ at a time, even with a union bound over a net of $T$, does not obviously extend to the full convex hull without first controlling $\sup_{x\in T}|\langle Ax,y\rangle - w(T)\|y\|_2|$ uniformly over both $x\in T$ and $y$ on the unit sphere of the target space — a two-parameter supremum. The book's actual route goes through Chevet's inequality, itself proved using the matrix deviation inequality's own chaining-based argument, to control this two-sided supremum, and then converts the resulting inequality into the containment $(1-\varepsilon)B\subseteq\mathrm{conv}(AT)\subseteq(1+\varepsilon)B$ via a support- function duality argument (a convex body is pinned down by its support function, so bounding $\sup_{x\in T}\langle Ax,y\rangle$ uniformly over $y$ on the sphere is exactly what is needed).

Formalization scope

A is Ω → Matrix (Fin m) (Fin n) ℝ with an explicit IsGaussianMatrix hypothesis (entries i.i.d. $N(0,1)$, formalized entrywise with joint independence). conv(AT) is convexHull ℝ of the image of T under A's mulVec, round-tripped through EuclideanSpace's continuous linear equivalence with the underlying function type. w(T) reuses this mission series' ExpSup/GaussianWidth convention (redefined locally, per the drafts-cannot-import-drafts rule, following the same ProbabilityTheory.stdGaussian-based realization of a standard Gaussian vector as 08-matrix-deviation). The stable dimension $d(T)$ is formalized directly as $w(T)^2/ \mathrm{diam}(T)^2$ rather than via the book's literal (but only asymptotically equivalent, per Exercise 7.6.1) definition through a squared Gaussian width $h(T-T)^2$ — the goal theorem's own proof uses only the inequality direction of that equivalence, and the goal's hypothesis already carries an unpinned absolute constant that absorbs the equivalence constant, so this substitution preserves the theorem's exact truth content (see StableDimension's own doc-comment and MODERATION_NOTES.md for the full argument) rather than approximating it.

Ball-center deviation, disclosed. The book's printed theorem statement carries no hypothesis that $T$ contains the origin; its proof opens by translating $T$ so that it does ("Translating $T$ if necessary, we can assume that $T$ contains the origin"), and Remark 11.3.4 then confirms the ball is centered at the origin in that case. This mission states the WLOG-reduced case directly — adding $0\in T$ as an explicit hypothesis — rather than also formalizing the translation argument that recovers the fully general (untranslated) statement. This is disclosed as a genuine narrowing of the literal printed statement, though not of what the book's own proof actually establishes.

This mission covers Theorem 11.3.3 only, with no milestones: BRIEF.md explicitly instructs that if the chapter's full proof chain (general matrix deviation inequality, Chevet's inequality, random projections of sets — Theorems 11.1.5, 11.2.4, 11.3.1) proves too heavy for the session, milestones should be cut rather than the goal substituted. All three are left out, not approximated, given this chapter's five from-scratch definitions already needed for the goal's own statement. ExpSup, GaussianWidth, StableDimension and IsGaussianMatrix are reusable by any later development needing Gaussian width, the stable dimension, or a Gaussian random matrix. Solvers' contributions are welcome on the goal theorem itself and, beyond this mission's current scope, on the three named milestones.

Selected references

• A. Dvoretzky, Some results on convex bodies and Banach spaces, Proc. Internat. Sympos. Linear Spaces (Jerusalem, 1960), 123–160.
• V. D. Milman, A new proof of A. Dvoretzky's theorem on cross-sections of convex bodies, Funkcional. Anal. i Priložen. 5 (1971), 28–37.
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 11. https://doi.org/10.1017/9781108231596

Motivation

Chapters 2 through 8 of Wainwright's High-Dimensional Statistics build up sharp error bounds for a sequence of specific high-dimensional models — sparse linear regression via the Lasso (Chapter 7), sparse principal components (Chapter 8) — each proved from scratch with techniques tailored to that model's own penalty and loss. Chapter 9 steps back and asks what made all of those arguments work, and isolates the answer into two structural ingredients: a decomposable regularizer, whose triangle inequality is tight across a well-chosen subspace pair, and a restricted curvature condition on the loss, holding only on the cone that decomposability forces the estimation error into. Once these two ingredients are checked for a particular model, a single, already-proved oracle inequality hands back the error bound — no further optimization-theoretic argument is needed. This mission formalizes that oracle inequality itself, together with its two supporting theorems, as the reusable core the book's later chapters (nuclear-norm matrix regression in Chapter 10, graphical model selection in Chapter 11, group-sparse and overlap-group Lassos) each specialize.

Setting

Let $\Omega$ be a finite-dimensional real inner product space (e.g. $\mathbb R^d$, or a matrix space with the Frobenius inner product), and consider the regularized M-estimator

$$\hat\theta \in \operatorname*{arg\,min}_{\theta\in\Omega} \Big\{ L_n(\theta) + \lambda_n\Phi(\theta) \Big\},$$

where $L_n:\Omega\to\mathbb R$ is a convex empirical cost function, $\Phi:\Omega\to[0,\infty)$ is a norm-based regularizer, and $\lambda_n>0$ is a user-chosen regularization weight. Write $\theta^*$ for the true parameter and $\Delta:=\hat\theta-\theta^*$ for the estimation error.

A pair of subspaces $\mathcal M\subseteq\bar{\mathcal M}$ of $\Omega$ — the model subspace and its (possibly larger) closure — has an associated perturbation subspace $\bar{\mathcal M}^\perp$, the orthogonal complement of $\bar{\mathcal M}$. The regularizer $\Phi$ is decomposable with respect to $(\mathcal M,\bar{\mathcal M})$ if the triangle inequality $\Phi(\alpha+\beta)\le\Phi(\alpha)+\Phi(\beta)$ is an equality whenever $\alpha\in\mathcal M$ and $\beta\in\bar{\mathcal M}^\perp$ — the regularizer penalizes deviations away from the model subspace exactly as much as it possibly could. The canonical example is the $\ell_1$-norm with $\mathcal M=\bar{\mathcal M}$ the subspace of vectors supported on a fixed index set $S$.

Writing $\Phi^*(v):=\sup_{\Phi(u)\le 1}\langle u,v\rangle$ for the dual norm, the good event $\mathcal G(\lambda_n):=\{\Phi^*(\nabla L_n(\theta^*))\le\lambda_n/2\}$ says the regularization weight dominates the dual norm of the score function at the truth — the non-probabilistic conditioning hypothesis every result in this chapter is stated under. The subspace Lipschitz constant $\Psi(S):=\sup_{u\in S\setminus\{0\}}\Phi(u)/\|u\|$ measures the worst-case price of converting between the regularizer $\Phi$ and the error norm $\|\cdot\|$ on a subspace $S$.

Formalization targets

Goal (Theorem 9.19, "Bounds for general models")

Under (A1) $L_n$ convex, satisfying restricted strong convexity (RSC) with curvature $\kappa>0$, radius $R$ and tolerance $\tau_n^2$ — $E_n(\Delta):=L_n(\theta^*+\Delta)-L_n(\theta^*) -\langle\nabla L_n(\theta^*),\Delta\rangle \ge \frac{\kappa}{2}\|\Delta\|^2-\tau_n^2\Phi^2(\Delta)$ for $\|\Delta\|\le R$ — and (A2) $\Phi$ decomposable with respect to $(\mathcal M,\bar{\mathcal M})$: conditioned on $\mathcal G(\lambda_n)$, any optimal $\hat\theta$ satisfies

$$\text{(a)}\quad \Phi(\hat\theta-\theta^*) \le 4\big(\Psi(\bar{\mathcal M})\, \|\hat\theta-\theta^*\| + \Phi(\theta^*_{\mathcal M^\perp})\big),$$

and, whenever $\tau_n^2\Psi^2(\bar{\mathcal M})\le\kappa/64$ and $\varepsilon_n(\mathcal M,\bar{\mathcal M})\le R$,

$$\text{(b)}\quad \|\hat\theta-\theta^*\|^2 \le \varepsilon_n^2(\mathcal M,\bar{\mathcal M}) := \frac{9\lambda_n^2}{\kappa^2}\Psi^2(\bar{\mathcal M}) + \frac{8}{\kappa}\Big(\lambda_n\Phi(\theta^*_{\mathcal M^\perp}) + 16\tau_n^2\Phi^2(\theta^*_{\mathcal M^\perp})\Big).$$

Milestones

• Proposition 9.13. Under (A2) alone, conditioned on $\mathcal G(\lambda_n)$, the error $\Delta=\hat\theta-\theta^*$ lies in the cone $\mathbb C_{\theta^*}(\mathcal M,\bar{\mathcal M}):=\{\Delta\mid\Phi(\Delta_{\bar{\mathcal M}^\perp})\le 3\Phi(\Delta_{\bar{\mathcal M}})+4\Phi(\theta^*_{\mathcal M^\perp})\}$ — the purely geometric fact Theorem 9.19's curvature argument is built on.
• Corollary 9.20. When $\theta^*\in\mathcal M$ exactly, the approximation-error term of $\varepsilon_n^2$ vanishes and Theorem 9.19 collapses to $\Phi(\hat\theta-\theta^*)\le\frac{6\lambda_n}{\kappa}\Psi^2(\bar{\mathcal M})$, $\|\hat\theta-\theta^*\|^2\le\frac{9\lambda_n^2}{\kappa^2}\Psi^2(\bar{\mathcal M})$ — the form used directly against every concrete model in the rest of the book.
• Theorem 9.24. Under an alternative, gradient-based curvature condition ($\Phi^*$-curvature, Definition 9.22) and $\theta^*\in\mathcal M$, the dual-norm error is controlled directly: $\Phi^*(\hat\theta-\theta^*)\le 3\lambda_n/\kappa$.

Significance

Theorem 9.19 is the book's own claimed unifying result: as it remarks explicitly, the theorem is a deterministic implication, and every later probabilistic corollary in Parts II and III of the book is obtained by (i) checking that a specific loss/regularizer pair is decomposable with respect to a natural subspace pair for the problem at hand, (ii) certifying the RSC condition with high probability for that loss (via concentration arguments from Chapters 2–6), and (iii) choosing $\lambda_n$ large enough that the good event holds with high probability — then reading off the rate directly from $\varepsilon_n^2(\mathcal M,\bar{\mathcal M})$. Chapter 7's Lasso bound (Theorem 7.13, mission 07-sparse-linear) is exactly Corollary 9.20 specialized to $\Phi=\|\cdot\|_1$ and $\mathcal M$ the subspace of $s$-sparse vectors — but Chapter 9 proves it once, in a form that Chapter 10's nuclear-norm-regularized low-rank matrix regression (mission 10-matrix-rank), Chapter 11's graphical model selection, and the chapter's own group-Lasso and overlap-group-Lasso examples all instantiate without re-deriving the optimization argument.

Difficulty

The formalization difficulty here is almost entirely conceptual rather than syntactic: getting the two-subspace apparatus $(\mathcal M,\bar{\mathcal M})$ exactly right. The book explicitly allows $\bar{\mathcal M}$ to be a strict superset of $\mathcal M$ (needed for the nuclear norm in Chapter 10, where the naive choice $\mathcal M=\bar{\mathcal M}$ fails to be decomposable at all), so every definition and theorem in this mission is parameterized by the pair, not by a single subspace — and three genuinely different projections appear across the statements: the error vector's projection onto $\bar{\mathcal M}$ and onto $\bar{\mathcal M}^\perp$ (both keep the bar), versus the true parameter's projection onto $\mathcal M^\perp$ (the complement of the small, unbarred subspace). A further subtlety specific to this printed source: several of the book's own displayed equations for $\Psi(\cdot)$ in Theorem 9.19 and Corollary 9.20 lose the overbar on $\bar{\mathcal M}$ in PDF text extraction (a rendering artifact, not a mathematical ambiguity); resolving which subspace is meant required reading the surrounding proof text line by line, since only $\Psi(\bar{\mathcal M})$ — not $\Psi(\mathcal M)$ — is mathematically consistent with how the constant is derived and used (see MODERATION_NOTES.md).

Formalization scope

$\Omega$ is [NormedAddCommGroup Ω] [InnerProductSpace ℝ Ω] [FiniteDimensional ℝ Ω], matching the book's implicit assumption of a finite-dimensional inner-product parameter space throughout this part of the book. The regularizer's norm axioms (IsRegularizerNorm), the dual norm, and the subspace Lipschitz constant are all defined via sSup/sInf-free explicit formulas or sSup over an explicitly-described set (never an unconstrained supremum over all of $\Omega$), so no faithfulness trap from an unbounded or empty supremum arises (see MODERATION_NOTES.md's trap table). κ > 0 and λ_n > 0 are made explicit hypotheses of every theorem, matching Definition 9.15's own stated positivity of $\kappa$ and the chapter's running convention that $\lambda_n$ is a positive regularization weight — never a narrowing of the theorem's actual scope. A trivializing formalization of this chapter would either collapse the two-subspace machinery to a single subspace $\mathcal M=\bar{\mathcal M}$ (which is faithful only for the $\ell_1$/group-Lasso examples, not the general theorem, and not what Chapter 10 needs) or silently drop the second conjunct of Theorem 9.19's conclusion (part (b), the actual quantitative rate) in favor of only the qualitative part (a); this mission formalizes the full two-subspace statement and both conjuncts of the goal theorem. Out of scope: the chapter's worked examples (sparse GLMs, Corollary 9.26; group Lasso; nuclear-norm matrix regression) that specialize the goal to concrete models — Chapter 10's own mission (10-matrix-rank) restates the needed instance of this framework locally rather than importing this mission's draft, per this book's series-wide convention that no draft imports another chunk's draft. Also out of scope: the RSC-implies-restricted-eigenvalue correspondence (Example 9.16) and the $\mu_n(\Phi^*)$-based general RSC certification (Theorem 9.36, Section 9.8), both purely probabilistic results that lie outside this chapter's own deterministic core.

Selected references

• Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 9. DOI: 10.1017/9781108627771.
• Negahban, S. N., Ravikumar, P., Wainwright, M. J., Yu, B. "A unified framework for high-dimensional analysis of M-estimators with decomposable regularizers." Statistical Science, 27(4), 2012, 538–557.
• Tibshirani, R. "Regression shrinkage and selection via the Lasso." Journal of the Royal Statistical Society: Series B, 58(1), 1996, 267–288.

Motivation

Many estimation problems are naturally posed over matrices rather than vectors: recommender systems (Netflix-style matrix completion), multivariate regression with correlated responses, vector autoregressive time series, and phase retrieval all reduce to estimating an unknown matrix $\Theta^*$ that is low-rank, or well approximated by one. A rank constraint alone makes the natural least-squares estimator non-convex and generally intractable; replacing it with the nuclear norm — the sum of the matrix's singular values, the tightest convex surrogate for rank — yields a tractable semidefinite program. Wainwright's High-Dimensional Statistics (2019), Chapter 10, shows that this substitution costs nothing statistically: nuclear-norm-regularized least squares achieves error rates matching what one could hope for even knowing the rank in advance, by specializing Chapter 9's general decomposable-regularizer framework (mission 09-decomposability) directly to the nuclear norm.

Setting

For matrices $A,B\in\mathbb R^{d_1\times d_2}$, the trace inner product is $\langle\!\langle A,B\rangle\!\rangle := \mathrm{trace}(A^TB) = \sum_{j_1,j_2}A_{j_1j_2}B_{j_1j_2}$ (Eq. 10.1), inducing the Frobenius norm $\|\!|A|\!\|_F$. Given design matrices $X_1,\dots,X_n\in\mathbb R^{d_1\times d_2}$ and responses $y_i=\langle\!\langle X_i,\Theta^*\rangle\!\rangle+w_i$, the observation operator $\mathcal X_n(\Theta):=(\langle\!\langle X_i,\Theta\rangle\!\rangle)_{i=1}^n$ and its adjoint $\mathcal X_n^*(u):=\sum_iu_iX_i$ (Eqs. 10.2-10.3) are the matrix analogs of a vector design matrix and its transpose. The nuclear norm $\|\!|\Theta|\!\|_{\mathrm{nuc}}:=\sum_j\sigma_j(\Theta)$ (Eq. 10.5) — the sum of singular values — is a decomposable regularizer (in the sense of Chapter 9) with respect to the subspace pair spanned by the top singular vectors of any target matrix, and its dual norm (Table 9.1) is the $\ell_2$-operator (spectral) norm $\|\!|\cdot|\!\|_2$. The estimator under study is nuclear-norm-regularized least squares,

$$\hat\Theta \in \operatorname*{arg\,min}_{\Theta\in\mathbb R^{d_1\times d_2}} \left\{ \frac{1}{2n}\|y-\mathcal X_n(\Theta)\|_2^2 + \lambda_n\|\!|\Theta|\!\|_{\mathrm{nuc}} \right\} \tag{10.16}$$

with $\lambda_n>0$ user-chosen.

Formalization targets

Goal (Proposition 10.6)

Suppose $\mathcal X_n$ satisfies the restricted strong convexity condition (10.17), $\|\mathcal X_n(\Delta)\|_2^2/(2n) \ge \kappa/2\|\!|\Delta|\!\|_F^2 - c_0\frac{d_1+d_2}{n}\|\!|\Delta|\!\|_{\mathrm{nuc}}^2$ for all $\Delta$, with $\kappa>0$, $c_0\ge 0$. Conditioned on the good event $\mathcal G(\lambda_n)=\{\|\!|\frac1n\sum_iw_iX_i|\!\|_2 \le\lambda_n/2\}$, any optimal $\hat\Theta$ satisfies, for any $r\in\{1,\dots,d'\}$ with $r\le\kappa n/(128c_0(d_1+d_2))$,

$$\|\!|\hat\Theta-\Theta^*|\!\|_F^2 \le \frac{9}{2}\frac{\lambda_n^2}{\kappa^2}r + \frac{1}{\kappa}\left\{2\lambda_n\sum_{j=r+1}^{d'}\sigma_j(\Theta^*) + \frac{32c_0(d_1+d_2)}{n}\left(\sum_{j=r+1}^{d'}\sigma_j(\Theta^*)\right)^2\right\}.$$

Milestone (Proposition 10.7)

Under the alternative $\Phi^*$-curvature condition (10.20) (a curvature bound on the gradient map rather than the Taylor error), with $\mathrm{rank}(\Theta^*)<\kappa/(64\tau_n)$: conditioned on $\mathcal G(\lambda_n)=\{\|\!|\frac1n\mathcal X_n^*(w)|\!\|_2\le\lambda_n/2\}$, any optimal $\hat\Theta$ satisfies $\|\!|\hat\Theta-\Theta^*|\!\|_2 \le 3\sqrt2\,\lambda_n/\kappa$ — an operator-norm bound the book notes is, in conjunction with the cone-like constraint (10.15), strictly stronger than Proposition 10.6's Frobenius-norm bound.

Significance

Proposition 10.6 is this chapter's direct payoff from Chapter 9's general machinery: it shows that the deterministic backbone of the Lasso's guarantee (mission 07-sparse-linear) extends essentially verbatim to the matrix setting, with the sparsity level $s$ replaced by the target rank $r$ and the ambient dimension $d$ replaced by $d_1+d_2$ — exactly the "degrees of freedom" scaling one would predict by counting the parameters needed to specify a rank-$r$ matrix. Every one of the chapter's later corollaries (matrix compressed sensing, multivariate regression, matrix completion) is obtained by verifying the restricted strong convexity condition (10.17) holds with high probability for a specific random design, then reading the rate directly off Proposition 10.6 — the same two-step recipe Chapter 9's own Theorem 9.19 established abstractly. Proposition 10.7's operator-norm bound is what subsequently controls the individual singular values of the estimation error, needed for exact-rank-recovery guarantees.

Difficulty

Both results are direct specializations of Chapter 9's general oracle inequalities (Theorem 9.19 and Theorem 9.24 respectively) to the nuclear norm as regularizer and the Frobenius/operator norm pair, so their formalization difficulty lies almost entirely in getting the matrix-specific objects right rather than in new proof machinery: the nuclear norm requires an actual notion of singular values (realized via the eigenvalues of the Gram matrix $\Theta^T\Theta$, using Mathlib's Hermitian-matrix spectral theorem), the operator norm requires the correct rectangular generalization of the symmetric-matrix Rayleigh-quotient characterization used in mission 08-pca, and the restricted-strong-convexity and curvature conditions must be instantiated against the correctly-adjointed observation operator $\mathcal X_n^*$. A further subtlety is keeping Proposition 10.6's Frobenius-norm conclusion and Proposition 10.7's operator-norm conclusion cleanly distinct — the book itself warns against conflating the norms used across different chapters of Part II (the vector $\ell_2$-norm of chunks 07-sparse-linear/08-pca versus the matrix Frobenius and operator norms here).

Formalization scope

Scope cut, disclosed here and in STATUS.md. BRIEF.md recommends Corollary 10.10 (the sample-complexity bound for the $\Sigma$-Gaussian random matrix ensemble) as the goal theorem. Corollary 10.10 is a genuinely probabilistic statement — it asserts a bound holding "with probability at least $1-2e^{-2n\delta^2}$" over $n$ i.i.d. draws of design matrices from a $\Sigma$-Gaussian ensemble (Theorem 10.8's own high-probability restricted-strong-convexity certification for that ensemble) — and formalizing it faithfully would require a genuine multivariate-Gaussian-measure infrastructure on matrix space (a probability space, an i.i.d. sequence of $\Sigma$-covariance-structured Gaussian matrices, and Mathlib's measure-theoretic probability API) that is disproportionate to this mission's time budget, and orthogonal to what Chapter 10 itself contributes (the chapter's own text stresses that Propositions 10.6 and 10.7 are the chapter's deterministic core, with probability entering only in Section 10.3's ensemble-specific certification — precisely mirroring chunk 09-decomposability's own "Theorem 9.19 is actually a deterministic result" framing). This mission instead takes Proposition 10.6 as its goal — explicitly named in BRIEF.md's own candidate list as "the nuclear-norm oracle inequality, an explicit corollary of Theorem 9.19" — the natural, tractable, still highly citable deterministic title result of Section 10.2, together with its companion Proposition 10.7. Theorem 10.8 (the $\Sigma$-Gaussian ensemble's RSC certification), Corollary 10.9 (noiseless exact recovery) and Corollary 10.10 itself are left for a future mission with a dedicated probability-theory budget. The cone-like constraint (Eq. 10.15) — whose own faithful statement requires the same explicit subspace-pair machinery ($\mathcal M(U_r,V_r),\bar{\mathcal M}(U_r,V_r)$) chunk 09-decomposability built for the general theory — is similarly left out, since Propositions 10.6 and 10.7's own numbered statements never expose these subspaces directly (only their proofs do, via instantiating Theorem 9.19/9.24). singularValues and nuclearNorm are noncomputable, defined via Mathlib's Hermitian-matrix eigenvalue spectral theorem; c0 ≥ 0 and λn > 0 are made explicit, matching this book's running conventions for RSC tolerance constants and regularization weights (see MODERATION_NOTES.md).

Selected references

• Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 10. DOI: 10.1017/9781108627771.
• Negahban, S., Wainwright, M. J. "Estimation of (near) low-rank matrices with noise and high-dimensional scaling." Annals of Statistics, 39(2), 2011, 1069–1097.
• Recht, B., Fazel, M., Parrilo, P. A. "Guaranteed minimum-rank solutions of linear matrix equations via nuclear norm minimization." SIAM Review, 52(3), 2010, 471–501.

Motivation

Many high-dimensional data sets — gene-expression profiles, sensor networks, social interactions — come with no natural ordering of variables, only pairwise dependencies whose structure is itself the object of interest. A graphical model encodes these dependencies as an undirected graph: vertices are variables, and edges mark direct (conditional) dependence. Recovering the graph from samples — graphical model selection — is a combinatorial problem masquerading as a statistical one: there are $2^{\binom{d}{2}}$ candidate graphs on $d$ vertices, far too many to search directly. For Gaussian data, however, graph structure is exactly the sparsity pattern of the inverse covariance (precision) matrix, which turns graph selection into $d$ coupled sparse-regression problems — one per vertex — each of which the Lasso theory of Chapter 7 already knows how to solve. This mission formalizes the theorem, due to Meinshausen and Bühlmann (2006), that shows this reduction actually works: solving $d$ independent Lasso problems and combining the results recovers the exact graph with high probability, at a sample complexity governed by the same kind of incoherence condition that governs Lasso support recovery itself.

Setting

An undirected graphical model on a finite vertex set $V$ pairs a graph $G=(V,E)$ with a random vector $X=(X_j)_{j\in V}$. Two equivalent structural properties connect $X$ to $G$ (Theorem 11.8, Hammersley-Clifford): $X$ factorizes according to $G$ if its density is a product of nonnegative functions, one per clique of $G$, each depending only on the variables in that clique (Definition 11.1); $X$ is Markov with respect to $G$ if, for every vertex cutset $S$ separating $V$ into disjoint pieces $A$ and $B$, the sub-vectors $X_A$ and $X_B$ are conditionally independent given $X_S$ (Definition 11.5). For a strictly positive density, these are the same condition.

For a zero-mean $d$-dimensional Gaussian vector with covariance $\Sigma^*$ and precision matrix $\Theta^*=(\Sigma^*)^{-1}$, the graph structure is exactly the support of $\Theta^*$: $(j,k)\in E \iff \Theta^*_{jk}\ne0$. The neighborhood $N(j):=\{k\mid(j,k)\in E\}$ of each vertex is itself a vertex cutset (separating $\{j\}$ from everything else), so the conditional independence $X_j\perp X_{V\setminus N^+(j)}\mid X_{N(j)}$ holds, and — by standard Gaussian conditioning — $X_j$ decomposes as a linear function of $X_{V\setminus\{j\}}$ plus independent Gaussian noise, with regression coefficients supported exactly on $N(j)$. Neighborhood regression exploits this directly: for each vertex $j$, solve the Lasso

$$\hat\theta_j \in \arg\min_{\theta\in\mathbb R^{d-1}}\ \frac1{2n}\|X_j-X_{\setminus\{j\}}\theta\|_2^2 +\lambda_n\|\theta\|_1,$$

read off $\hat N(j):=\{k\mid\hat\theta_{j,k}\ne0\}$, and combine the $d$ per-vertex estimates into a single edge set via the OR rule ($(j,k)\in\hat E_{\mathrm{OR}}$ iff $k\in\hat N(j)$ or $j\in\hat N(k)$) or the more conservative AND rule (iff both hold). The relevant incoherence condition, analogous to Chapter 7's, is stated for a positive definite matrix $\Gamma$ and subset $S$: $\Gamma$ is $\alpha$-incoherent with respect to $S$ if $\max_{k\notin S}\|\Gamma_{kS}(\Gamma_{SS})^{-1}\|_1\le1-\alpha$.

Formalization targets

Theorem 11.8 (Hammersley-Clifford). Factorizes G p ↔ IsMarkov G X P for any strictly positive density $p$.

Theorem 11.12 (goal — graph selection consistency). Suppose for every $j$, $\Sigma^*_{\setminus\{j\}}$ is $\alpha$-incoherent with respect to $N(j)$, and $|\!|\!|(\Sigma^*_{N(j),N(j)})^{-1}|\!|\!|_\infty\le b$. With $\lambda_n=c_0\frac1\alpha(\sqrt{\log d/n}+\delta)$, the neighborhood-Lasso estimate combined via either rule satisfies, with probability at least $1-c_2e^{-c_3n\min(\delta^2,1/m)}$:

$$\hat E\subseteq E \qquad\text{and}\qquad \forall (j,k):\ |\Theta^*_{jk}|\ge7b\lambda_n \implies (j,k)\in\hat E.$$

Significance

Theorem 11.12 is the statistical justification for one of the two standard approaches to Gaussian graphical model selection (the other being the penalized-likelihood "graphical Lasso" of §11.2.1). Its significance is computational as much as statistical: rather than solving one $d$-dimensional penalized-likelihood problem, neighborhood regression solves $d$ independent, embarrassingly parallel Lasso problems, each of dimension $d-1$ — a substantial practical advantage at scale, with (as this theorem shows) no loss in statistical guarantee. Formalizing it produces, for the first time on the platform, statement-level infrastructure for undirected graphical models (Hammersley-Clifford, the Markov property via vertex cutsets, neighborhood structure) together with the random-design analogue of the Lasso support-recovery machinery — a genuinely different technical regime from Chapter 7's fixed-design Lasso theory, since here the "design matrix" $X_{\setminus\{j\}}$ is itself Gaussian and statistically coupled to the response $X_j$ through the very covariance structure being estimated. As with the other missions in this series, only the statements are formalized here; the proofs (an extension of the primal-dual witness technique to random design, per the book's own proof sketch) are left as the draft goal for future proof contributions.

Difficulty

The proof of Theorem 7.21 (Chapter 7's Lasso support-recovery guarantee) is for a deterministic design matrix, with all randomness confined to the additive noise. Here the "design" $X_{\setminus\{j\}}$ is itself random and Gaussian, and — critically — it is statistically dependent on the very quantity ($N(j)$, encoded in $\Theta^*$'s support) the Lasso is trying to recover, since $X_{\setminus\{j\}}$'s own covariance structure is exactly what the incoherence condition constrains. The naive approach of just conditioning on the realized design matrix and invoking Theorem 7.21 fails, because the deterministic-design incoherence condition would then need to hold for the sample covariance $\Gamma=\frac1n X_{\setminus\{j\}}^TX_{\setminus\{j\}}$, not the population covariance $\Sigma^*_{\setminus\{j\}}$ that is actually assumed — and controlling the gap between sample and population incoherence under the joint (not fixed) randomness of predictors and response is exactly the extra step the book's proof needs, handled via an extension of the primal-dual witness technique that tracks both sources of randomness together.

Formalization scope

The vertex set V is an arbitrary finite type; the covariate space for X is ℝ throughout (all variables jointly Gaussian). The Gaussian design is characterized via its one-dimensional projections (every linear combination is univariate Gaussian with the matching variance) rather than via Mathlib's multivariate-Gaussian machinery directly, to keep the definition self-contained. IsAlphaIncoherent's ambient index set is realized as a subset of the full vertex type rather than as a literal submatrix, since the book's condition never references an entry outside it. The theorem states the conclusion jointly for both the OR-rule and AND-rule estimated edge sets on one shared high-probability event, matching "based on either rule" literally rather than picking one. The trivializing formalization ruled out here is treating the neighborhood-Lasso estimate as a fixed-design Lasso problem (silently dropping the joint randomness of predictors and response) — every design realization in this formalization is the actual random vector Xdes i ω, not a deterministic parameter, and the Gaussian design hypothesis (IsIIDGaussianDesign) is stated over the same probability space Ω as the least-squares residual. Theorem 11.8 (Hammersley–Clifford) is formalized only for the continuous case — a random vector with a density with respect to Lebesgue measure — matching what the Gaussian goal (Theorem 11.12) actually needs; the book's own Definition 11.1 also permits a discrete (counting-measure) density, with the Ising model (Example 11.4) as a worked instance, which this mission does not cover. Contributions welcome: the graphical Lasso's own guarantees (Propositions 11.9, 11.10, deferred from this mission — see STATUS.md), and the proof of Theorem 11.12 itself via the primal-dual witness extension the book sketches.

Selected references

• M. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Chapter 11. https://doi.org/10.1017/9781108627771
• N. Meinshausen and P. Bühlmann, "High-dimensional graphs and variable selection with the Lasso," Annals of Statistics, 34(3):1436-1462, 2006. https://doi.org/10.1214/009053606000000281
• J. Hammersley and P. Clifford, "Markov fields on finite graphs and lattices," unpublished manuscript, 1971.

Motivation

Many statistical problems — nonparametric regression, density estimation, dimension reduction, testing — are naturally posed as optimization over a space of functions rather than a finite-dimensional parameter vector. Hilbert spaces provide the right generality: they carry an inner product and a norm, so notions of projection, orthogonality and least-squares fitting all make sense, exactly as in ordinary Euclidean space, even though the "vectors" are now functions. Reproducing kernel Hilbert spaces (RKHSs) are the particular class of function-valued Hilbert spaces that make this program computationally tractable: they are generated by a single bivariate kernel function, and every RKHS computation reduces to evaluating that kernel, never to manipulating an infinite-dimensional object directly (the "kernel trick"). Wainwright's High-Dimensional Statistics (2019), Chapter 12, develops the foundational correspondence between kernels and Hilbert spaces that makes this possible, and this mission formalizes its two central theorems.

Setting

A Hilbert space is a complete inner product space (Definitions 12.1–12.2); this mission uses Mathlib's own NormedAddCommGroup/InnerProductSpace ℝ/CompleteSpace typeclasses for this notion throughout. A linear functional $L:H\to\mathbb R$ is bounded if $|L(f)|\le M\|f\|_H$ for some $M<\infty$ and all $f\in H$; the Riesz representation theorem (Theorem 12.5) says every such functional is $L(f)=\langle f,g\rangle_H$ for a unique $g\in H$.

A bivariate function $K:X\times X\to\mathbb R$ is a positive semidefinite (PSD) kernel (Definition 12.6) if it is symmetric and every finite Gram matrix $(K(x_i,x_j))_{i,j=1}^n$ is positive semidefinite — the natural generalization of a PSD matrix to a (possibly infinite) index set $X$, with no topological structure on $X$ required. A reproducing kernel Hilbert space (RKHS) for a kernel $K$ is a Hilbert space $H$ of functions on $X$ such that, for every $x\in X$, the function $K(\cdot,x)$ belongs to $H$ and

$$\langle f, K(\cdot,x)\rangle_H = f(x) \qquad \text{for all } f\in H \tag{12.3}$$

— the reproducing property. Equivalently (Definition 12.12), $H$ is an RKHS exactly when every evaluation functional $f\mapsto f(x)$ is bounded on $H$.

Formalization targets

Goal (Theorem 12.11, the Moore-Aronszajn theorem)

Given any PSD kernel function $K$ on any set $X$, there is a Hilbert space $H$ (embedded into functions on $X$) in which $K$ satisfies the reproducing property (12.3) — and this Hilbert space is unique: any two Hilbert spaces with this property for the same $K$ are linearly isometric via an isometry intertwining their embeddings into functions on $X$.

Milestones

• Theorem 12.5 (Riesz representation). Every bounded linear functional on a Hilbert space $H$ has a unique representer $g\in H$: $L(f)=\langle f,g\rangle_H$ for all $f$. Used inside the proof of Theorem 12.13 to produce the representer $R_x$ of each evaluation functional.
• Theorem 12.13 (the converse correspondence). Given any Hilbert space $H$ of functions on $X$ in which every evaluation functional is bounded, there is a unique PSD kernel $K$ satisfying the reproducing property for $H$ — completing the Moore-Aronszajn equivalence between PSD kernels and Hilbert spaces with bounded evaluation functionals.
• Theorem 12.20 (Mercer's theorem). Under compactness of $X$, continuity of $K$, and the Hilbert-Schmidt condition $\int_{X\times X}K^2\,dP\,dP<\infty$, the integral operator $T_K(f)(x)=\int_XK(x,z)f(z)\,dP(z)$ has an orthonormal eigenbasis $(\varphi_j)$ of $L^2(X;P)$ with non-negative eigenvalues $(\mu_j)$, and $K(x,z)=\sum_j\mu_j\varphi_j(x)\varphi_j(z)$, with the series converging absolutely and uniformly.

Significance

Theorem 12.11 is the theorem that makes the entire RKHS apparatus well-posed: every time a statistician writes down a kernel — linear, polynomial, Gaussian — Theorem 12.11 guarantees that a canonical Hilbert space of functions exists in which that kernel reproduces, so that optimizing over "the RKHS associated with $K$" is a well-defined problem, not merely a suggestive shorthand. Theorem 12.13's converse shows the correspondence is exact — the class of kernel-generated Hilbert spaces is exactly the class of function spaces with bounded evaluation, the class relevant to any statistical application that samples a function at finitely many points. Together, these two results are the foundation the book's own later chapters build directly on: Chapter 13's nonparametric least-squares oracle inequality, and Chapter 14's kernel density estimation, both work by optimizing over an RKHS and are only well-posed because of this correspondence. Mercer's theorem, in turn, is what connects the RKHS viewpoint back to the earlier feature-map viewpoint of Chapter 12.2.2 (Eq. 12.2): the eigenfunctions $(\sqrt{\mu_j}\varphi_j)_j$ give an explicit feature map into $\ell^2(\mathbb N)$ realizing $K$, and its expansion is what later underlies the book's discussion of kernel PCA and of RKHS balls as ellipsoids in $\ell^2(\mathbb N)$-coordinates.

Difficulty

The formalization difficulty is concentrated in getting the type of the existence-and- uniqueness claim right, not in any single hypothesis. A Hilbert space is not naturally a subtype of a fixed ambient space in Lean, so "the Hilbert space $H$" of Theorem 12.11 is formalized as an abstract type together with its own NormedAddCommGroup/InnerProductSpace ℝ/CompleteSpace instances, connected to "a space of functions on $X$" via an injective linear embedding into $X\to\mathbb R$ — and uniqueness must then be stated as an isometric equivalence between any two witnessing Hilbert spaces that respects this embedding, the faithful rendering of the book's own proof, which literally shows two candidate Hilbert spaces are equal as sets of functions. A second subtlety is keeping Theorem 12.11's hypotheses (a bare PSD kernel, no topology on $X$) cleanly separated from Mercer's theorem's additional compactness, continuity and measure-theoretic apparatus — the two theorems are frequently conflated informally, but the book is explicit that Theorem 12.11 needs none of Mercer's structure.

Formalization scope

$X$ is an unconstrained Type* for Theorem 12.5, 12.11 and 12.13 — no topology, matching the book's own generality. Mercer's theorem (Theorem 12.20) additionally requires [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] and a finite measure P, matching its own compactness/continuity/measure-theoretic hypotheses exactly, never applied outside that scope. The integral operator $T_K$ of Eq. (12.11a) is presented as an abstract linear map on Lp ℝ 2 P tied to the defining integral formula via an explicit hypothesis, rather than constructed as a def, since constructing it as a genuine well-defined operator (needing integrability and a.e.-measurability arguments) is proof content, not definitional content, and this mission's definitions file is sorry-free by convention. Mercer's orthonormal-basis index type is existentially quantified over a countable ι (∃ (ι : Type) (_ : Countable ι), ...) rather than fixed to ℕ, since L²(X;P) can be finite-dimensional for finite X (Example 12.18/12.21), where no infinite orthonormal basis exists; the uniform-convergence conjunct is correspondingly quantified over every bijection e : ℕ ≃ ι (vacuous when ι is finite, a genuine order-independent claim when ι is countably infinite). A trivializing formalization of this chapter would state only existence in Theorem 12.11 and drop uniqueness (explicitly warned against by this chapter's own brief), or state Mercer's convergence merely pointwise or in $L^2$ rather than absolutely and uniformly; this mission avoids both. Out of scope: the constructive proof detail of Theorem 12.11 (the explicit span-and-complete construction is proof content, not part of the statement), the chapter's worked kernel examples (linear, polynomial, Gaussian kernels, Examples 12.7–12.9), and the further consequences of Mercer's theorem (Corollary 12.26 on RKHS-ball ellipsoids, the feature-map connection of Eq. 12.14) — all natural follow-on work for a future mission on kernel-based nonparametric regression (Chapter 13, mission 13-nonparametric-ls), which restates whatever RKHS objects it needs locally rather than importing this mission's draft, per this book's series-wide convention.

Selected references

• Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 12. DOI: 10.1017/9781108627771.
• Aronszajn, N. "Theory of reproducing kernels." Transactions of the American Mathematical Society, 68(3), 1950, 337–404.
• Mercer, J. "Functions of positive and negative type, and their connection with the theory of integral equations." Philosophical Transactions of the Royal Society A, 209, 1909, 415–446.