High-Dimensional Probability and Statistics

Motivation

Regression is usually taught with a fixed parametric model: linear regression fits a $d$-dimensional coefficient vector, and the estimation error is controlled by $d/n$. Many regression problems in practice have no such finite-dimensional description — the regressor is only known to be, say, convex, monotone, or smooth, and the estimator is a least-squares fit over the (infinite-dimensional) set of functions with that shape. This is nonparametric regression, and the basic question is the same as in the parametric case: how close is the fitted function to the truth, as a function of the sample size $n$? Answering it requires replacing "dimension" with a genuinely functional notion of complexity, since an infinite- dimensional function class can still be small enough to estimate well (a Sobolev ball) or too large to estimate at all. The theory in this mission, due to van de Geer and developed in Chapter 13 of Wainwright (High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019), gives a single non-asymptotic template — the localized Gaussian complexity — that answers this question for an arbitrary star-shaped function class, and recovers the familiar parametric and Sobolev/RKHS rates as special cases.

Setting

Fix $n$ design points $x_1,\dots,x_n$ in an arbitrary covariate space $\mathcal X$ (fixed, not random — this is the fixed-design setting) and observe

$$y_i = f^*(x_i) + \sigma w_i, \qquad i = 1,\dots,n,$$

where $f^*$ is the unknown regression function, $\sigma > 0$ is a known noise level, and $w_1,\dots,w_n$ are i.i.d. standard Gaussian. Given a class $F$ of candidate functions, the nonparametric least-squares estimate is any minimizer

$$\hat f_n \in \arg\min_{f\in F}\ \frac1n\sum_{i=1}^n \big(y_i - f(x_i)\big)^2.$$

Error is measured in the empirical (design-dependent) seminorm $\|g\|_n^2 := \frac1n\sum_{i=1}^n g(x_i)^2$. A class $H$ of functions is star-shaped if $h\in H$ and $\alpha\in[0,1]$ together imply $\alpha h \in H$ — every convex class containing the origin has this property, and it is the minimal structural assumption under which the theory below applies. For a star-shaped class $H$ and radius $\delta>0$, the local Gaussian complexity

$$G_n(\delta; H) := \mathbb E_w\Big[\ \sup_{h\in H,\ \|h\|_n\le\delta}\ \Big|\tfrac1n \sum_{i=1}^n w_i h(x_i)\Big|\ \Big]$$

measures how much a mean-zero Gaussian process can be made to look like a member of $H$ restricted to the ball of radius $\delta$. A critical radius $\delta_n$ is any positive solution of $G_n(\delta;H)/\delta \le \delta/(2\sigma)$; by Lemma 13.6, $\delta\mapsto G_n(\delta;H)/\delta$ is non-increasing on $H$ star-shaped, so this inequality always has a smallest positive solution.

Formalization targets

Lemma 13.6. For any star-shaped $H$, $\delta \mapsto G_n(\delta;H)/\delta$ is non-increasing on $(0,\infty)$, and consequently $G_n(\delta;H)/\delta \le c\delta$ has a smallest positive solution for every $c>0$.

Theorem 13.5 (special case, $f^*\in F$).

$$\mathbb P\big[\|\hat f_n - f^*\|_n^2 \ge 16\,t\delta_n\big] \le e^{-nt\delta_n/(2\sigma^2)} \qquad \text{for all } t \ge \delta_n.$$

Theorem 13.13 (goal — general oracle inequality, $f^*$ not assumed in $F$). With $\delta_n$ solving the critical inequality for $\partial F := F - F$, there are universal constants $(c_0,c_1,c_2)$ such that for all $t\ge\delta_n$,

$$\|\hat f_n-f^*\|_n^2 \le \inf_{\gamma\in(0,1)}\left[\frac{1+\gamma}{1-\gamma}\|f-f^*\|_n^2 +\frac{c_0}{\gamma(1-\gamma)}t\delta_n\right]\quad\text{for all }f\in F,$$

with probability at least $1-c_1e^{-c_2nt\delta_n/\sigma^2}$. The goal is deliberately the statement with unresolved universal constants and an infimum over $\gamma$, rather than any single instantiated bound, so the target survives sharper constant tracking.

Significance

Theorem 13.13 is the "master" result behind essentially every concrete rate in the chapter: orthogonal series regression, convex/monotone regression, and (via the KRR specialization of Section 13.4) kernel ridge regression rates for Sobolev and Gaussian-kernel classes are all obtained by bounding $G_n$ for a particular $F$ and reading off $\delta_n$. Its value is that it isolates exactly the one place where the geometry of $F$ enters — the local Gaussian complexity — while the probabilistic argument (a peeling/chaining argument controlling a localized empirical process) is generic. Formalizing it produces, for the first time on the platform, the statement-level infrastructure (star-shaped classes, local Gaussian complexity, critical radius) that any future mission on a concrete nonparametric-regression rate — kernel ridge regression, convex regression, isotonic regression — can specialize, without re-deriving the oracle inequality from scratch. The proof itself (concentration of Gaussian complexity via Borell-TIS/Gaussian comparison plus a peeling argument over dyadic scales) is not attempted here; only the statement is formalized, as a draft goal for future proof contributions.

Difficulty

The naive route to Theorem 13.13 is to bound $\|\hat f_n - f^*\|_n$ pointwise via the basic inequality $\tfrac12\|\hat f_n-f^*\|_n^2 \le \tfrac{\sigma}{n}\sum_i w_i(\hat f_n(x_i)-f^*(x_i))$ and then bound the right side by $\sigma\,G_n(\delta;\partial F)$ for $\delta = \|\hat f_n-f^*\|_n$ — but $\delta$ is itself random (it depends on the estimate), so this is circular: the bound on the right depends on the very quantity being bounded. The chapter's actual argument resolves this with a peeling device: partition the event space by which dyadic annulus $\|\hat f_n-f^*\|_n$ falls into, and apply a uniform (non-circular) bound on each annulus separately via Gaussian concentration, summing a geometric series of tail probabilities. This is the step every first attempt misses, and it is why the local Gaussian complexity — rather than the simpler global complexity of Chapter 4/5 — is the right object: localizing to radius $\delta$ is what makes the per-annulus bound tight enough for the final sum to converge.

Formalization scope

Design points are an arbitrary type X (no topology or metric structure is needed for the statements themselves); the least-squares estimate is represented as a Prop (IsLeastSquaresEstimate) picking out any function achieving the empirical minimum, matching the book's "any minimizer" phrasing rather than assuming uniqueness. The local Gaussian complexity is defined as an expectation over an explicit i.i.d.-standard-Gaussian noise vector on an abstract probability space, with the inner supremum taken over the subtype of the radius-restricted slice of the class — this is well-defined (not the junk value 0 of an unbounded Set ℝ supremum) whenever the slice is nonempty, which holds automatically for any nonempty star-shaped class (taking $\alpha=0$ exhibits $0$ in the class). Since neither X nor H carries a topology, separability or countability constraint, SatisfiesCriticalInequality adds an explicit Integrable hypothesis on that same supremum (added in revision), guarding against Mathlib's Bochner integral silently returning the junk value 0 for a non-measurable integrand — a value that would otherwise trivially satisfy the critical inequality for every positive δ, regardless of the function class's actual local complexity. The trivializing formalization to rule out here is stating Theorem 13.13's universal constants after the quantification over the function class and sample size, which would let $(c_0,c_1,c_2)$ secretly depend on the instance and make the "universal" claim vacuous; this mission places the constant quantifiers first, before the class, design and noise data they must not depend on. A complete downstream development would add: the concentration-of-Gaussian-complexity step (Borell–TIS or a comparable tail bound), the peeling argument, and the metric-entropy / Dudley-integral machinery of Section 13.2.1 for bounding $G_n$ explicitly on concrete classes (Sobolev balls, RKHS balls) — none of which is attempted here.

Selected references

• M. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Chapter 13. https://doi.org/10.1017/9781108627771
• S. van de Geer, Empirical Processes in M-Estimation, Cambridge University Press, 2000.
• S. van de Geer, "Estimating a regression function," Annals of Statistics, 18(2):907-924, 1990. https://doi.org/10.1214/aos/1176347627

Motivation

Every consistency guarantee for an empirical-risk-minimization procedure — the Lasso, kernel ridge regression, maximum likelihood — ultimately rests on relating an empirical average to its population expectation, uniformly over the class of candidate functions or parameters being searched. Chapter 4 established the classical form of this connection: a uniform law of large numbers, bounding $\sup_{f\in F}|\|f\|_n^2-\|f\|_2^2|$ by an absolute quantity governed by the (unlocalized) complexity of $F$. Such a bound is often wasteful: it treats a function with small population norm the same as one with large population norm, when intuitively the empirical and population norms of a small function should already agree closely. This mission formalizes the sharper, localized form of this uniform law — the same localization principle Chapter 13 used for nonparametric least squares, now applied directly to the empirical-versus-population norm comparison itself, giving relative rather than absolute control and recovering optimal convergence rates that the unlocalized theory misses.

Setting

Fix a probability distribution $P$ over a covariate space $X$ and $n$ i.i.d. samples $x_1,\dots,x_n\sim P$. For $f:X\to\mathbb R$, the population norm is $\|f\|_2^2:=\int_Xf(x)^2\,P(dx)$ and the empirical norm is $\|f\|_n^2:=\frac1n\sum_{i=1}^nf(x_i)^2$; by linearity of expectation, $\mathbb E[\|f\|_n^2]=\|f\|_2^2$, so the question is how tightly $\|f\|_n^2$ concentrates around $\|f\|_2^2$, uniformly over a function class $F$. A class $F$ is star-shaped around the origin if $f\in F,\alpha\in[0,1]\implies\alpha f\in F$, and $b$-uniformly bounded if $\|f\|_\infty\le b$ for every $f\in F$. The relevant complexity measure is the population localized Rademacher complexity

$$R_n(\delta;F) := \mathbb E_{\varepsilon,x}\Big[\ \sup_{f\in F,\ \|f\|_2\le\delta}\ \Big| \tfrac1n\sum_{i=1}^n\varepsilon_if(x_i)\Big|\ \Big],$$

where $\varepsilon_1,\dots,\varepsilon_n$ are i.i.d. Rademacher signs independent of the samples — note that, unlike Chapter 13's Gaussian complexity for fixed design points, this expectation integrates out the randomness of the samples themselves, since this chapter treats $\{x_i\}$ as genuinely random throughout. A critical radius $\delta_n$ is any positive solution of $R_n(\delta;F)\le\delta^2/b$.

Formalization targets

Theorem 14.1 (goal). Given $F$ star-shaped and $b$-uniformly bounded, and $\delta_n$ solving the critical inequality, for any $t\ge\delta_n$,

$$\Big|\|f\|_n^2-\|f\|_2^2\Big|\le\frac12\|f\|_2^2+\frac{t^2}2 \qquad\text{for all }f\in F,$$

with probability at least $1-c_1e^{-c_2nt^2/b^2}$; and if additionally $n\delta_n^2\ge\frac2{c_2}\log(4\log(1/\delta_n))$,

$$\big|\|f\|_n-\|f\|_2\big|\le c_0\delta_n \qquad\text{for all }f\in F,$$

with probability at least $1-c_1'e^{-c_2'n\delta_n^2/b^2}$.

Significance

Theorem 14.1 is the technical engine behind two of the book's other sharp results: Example 14.2's derivation of the optimal $n^{-1/2}$ rate for bounded quadratic function classes (where the unlocalized analogue of this theorem only achieves the slower $n^{-1/4}$ rate), and, more broadly, every later argument in the book that needs to translate an empirical-norm guarantee (as produced directly by an M-estimator's optimality, e.g. Chapter 13's nonparametric least-squares bounds) into a population-norm guarantee, or vice versa. The gap between the "absolute" uniform law of Chapter 4 and the "relative" one here is exactly the difference between a bound that is only informative for functions of order-one population norm, and one that remains sharp arbitrarily close to the origin — which is precisely where a consistent estimator's error eventually lives. Formalizing the statement produces, for the first time on the platform, the localized-Rademacher-complexity vocabulary at the population level (as opposed to Chapter 13's fixed-design Gaussian-complexity version), reusable by any future mission needing to pass between empirical and population norms.

Difficulty

The naive approach — apply Hoeffding's inequality to $|\|f\|_n^2-\|f\|_2^2|$ for a fixed $f$, then union-bound (or apply the unlocalized Rademacher-complexity uniform law of Chapter 4) over $F$ — gives a bound whose complexity term does not shrink as $\|f\|_2\to0$, since it uses the complexity of all of $F$ regardless of a given function's own size. This is exactly the sub-optimality Example 14.2 exhibits concretely: the naive bound gives rate $n^{-1/4}$ where the truth is $n^{-1/2}$. The fix is not merely technical bookkeeping — it requires a genuine peeling argument over dyadic norm-scales (exactly as in Chapter 13's proof of Theorem 13.13), applying the localized complexity $R_n(\delta;F)$ at the scale $\delta=\|f\|_2$ appropriate to each individual $f$, and controlling the resulting geometric sum of tail probabilities across scales. A reader's first instinct — bound $\|f\|_2$ in terms of $\|f\|_n$ and substitute — is circular, since $\|f\|_n$ is itself the random quantity being controlled.

Formalization scope

The covariate space X carries an arbitrary MeasurableSpace structure (no topology needed for the statement); the sample sequence and the Rademacher signs are both represented as families of measurable functions on a shared probability space Ω, with their joint independence stated as a single IndepFun between the two vector-valued sequences (rather than building a combined-index iIndepFun), since it is the two sequences — not each pair of individual variables — whose independence the book invokes. The two conclusions of Theorem 14.1 are stated as a conjunction with the second gated behind its own extra hypothesis, never collapsed into a single implication, since the book's own statement keeps them syntactically and logically distinct (the second requires a strictly stronger and additional condition on top of the first's). The universal constants (c1,c2,c0,c1',c2') are quantified before every instance object, so they cannot secretly depend on the function class, sample size, or radius. Every f ∈ F is required measurable (hF_meas, added in revision): the book's own framing implicitly restricts to measurable, square-integrable f throughout (p. 454), and without this hypothesis the population norm popNormSq, which appears directly in the goal's conclusion, could silently take Mathlib's Bochner-integral junk value 0 for a non-measurable, pointwise-bounded member of a star-shaped, uniformly-bounded F. The trivializing formalization ruled out here is stating the localization constraint at the empirical rather than population norm in popRademacherComplexity — this chapter's whole point (contrast Chapter 13's Gn, correctly localized at the empirical norm since there the design is fixed) is that $R_n(\delta;F)$'s localization is a population-level object, precisely because the samples are random here. Welcome future contributions: Corollary 14.3's covering-number sufficient condition for the empirical version of the critical inequality, and Theorem 14.20's Lipschitz/strongly-convex cost-function uniform law, both deferred from this mission (see STATUS.md) as they need substantial additional apparatus (metric entropy integrals; cost functions and strong convexity) beyond what Theorem 14.1 itself requires.

Selected references

• M. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019, Chapter 14. https://doi.org/10.1017/9781108627771
• P. Bartlett, O. Bousquet and S. Mendelson, "Local Rademacher complexities," Annals of Statistics, 33(4):1497-1537, 2005. https://doi.org/10.1214/009053605000000282
• V. Koltchinskii, "Local Rademacher complexities and oracle inequalities in risk minimization," Annals of Statistics, 34(6):2593-2656, 2006. https://doi.org/10.1214/009053606000001019

Motivation

Estimating a $d\times d$ covariance matrix $\Sigma$ from $n$ samples is a canonical high-dimensional problem: the natural estimator, the sample covariance $\hat\Sigma$, is consistent in operator norm only when $n\gtrsim d$, which fails outright in the regime $d\gg n$ common to modern applications. When $\Sigma$ is additionally known to be sparse — few nonzero entries per row — a simple fix restores consistency even when $d\gg n$: threshold every entry of $\hat\Sigma$ below a data-dependent level to zero. This mission formalizes the matrix concentration machinery behind that fix and the resulting guarantee, following Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 6.

Setting

For a random matrix $Q$, the matrix variance is $\mathrm{var}(Q):=\mathbb E[Q^2]-(\mathbb E[Q])^2$, and the Loewner order $A\preceq B$ on symmetric matrices means $B-A$ is positive semidefinite. A zero-mean symmetric random matrix $Q$ satisfies Bernstein's condition (Definition 6.10) with parameter $b>0$ if $\mathbb E[Q^j]\preceq\tfrac12 j!\,b^{j-2}\mathrm{var}(Q)$ for $j=3,4,\dots$ — the matrix analogue of the scalar Bernstein condition of Chapter 2. The operator (spectral) norm $|\!|\!|M|\!|\!|_2$ is $M$'s largest singular value.

Given a threshold $\lambda>0$, the hard-thresholding operator is $T_\lambda(u):=u\cdot \mathbb 1[|u|>\lambda]$, extended entrywise to matrices (Eq. (6.52)). A covariance matrix $\Sigma$'s sparsity pattern is captured by its adjacency matrix $A_{j\ell}:=\mathbb 1[\Sigma_{j\ell}\neq0]$ (p. 181); $|\!|\!|A|\!|\!|_2\le d$ always, with equality only when $\Sigma$ has no zero entries, and $|\!|\!|A|\!|\!|_2\le s$ whenever $\Sigma$ has at most $s$ nonzero entries per row.

Formalization targets

Goal — Theorem 6.23 (thresholding-based covariance estimation)

Let $\{x_i\}_{i=1}^n$ be i.i.d. zero-mean random vectors with covariance $\Sigma$, each coordinate sub-Gaussian with parameter at most $\sigma$. If $n>\log d$, then for any $\delta>0$, the thresholded sample covariance $T_{\lambda_n}(\hat\Sigma)$ with $\lambda_n/\sigma^2 = 8\sqrt{\log d/n}+\delta$ satisfies

$$\mathbb P\big[\,|\!|\!|T_{\lambda_n}(\hat\Sigma)-\Sigma|\!|\!|_2 \ge 2|\!|\!|A|\!|\!|_2\lambda_n\,\big] \;\le\; 8e^{-\frac{n}{16}\min\{\delta,\delta^2\}}.$$

The error scales with the graph sparsity $|\!|\!|A|\!|\!|_2$, not with $d$ directly — the whole point of thresholding when the ambient dimension is much larger than the sample size.

Milestone — Theorem 6.17 (the matrix Bernstein bound)

For independent, zero-mean, symmetric random matrices $\{Q_i\}$ satisfying Bernstein's condition with parameter $b$,

$$\mathbb P\Big[\frac1n\Big|\!\Big|\!\Big|\sum_{i=1}^n Q_i\Big|\!\Big|\!\Big|_2 \ge \delta\Big] \;\le\; 2\,\mathrm{rank}\Big(\sum_{i=1}^n\mathrm{var}(Q_i)\Big)\exp\Big(-\frac{n\delta^2}{2(\sigma^2+b\delta)}\Big).$$

This is the general matrix concentration tool the whole chapter builds toward; Theorem 6.23 is one of its corollaries.

Milestone — Eq. (6.54) (the deterministic thresholding bound)

For any $\lambda_n$ with $\|\hat\Sigma-\Sigma\|_{\max}\le\lambda_n$, $|\!|\!|T_{\lambda_n}(\hat\Sigma)-\Sigma|\!|\!|_2\le2|\!|\!|A|\!|\!|_2\lambda_n$ — a purely deterministic fact, with no probability involved, that reduces Theorem 6.23's proof to a single probabilistic input: controlling $\|\hat\Sigma-\Sigma\|_{\max}$.

Significance

Theorem 6.17 is the workhorse of the whole chapter: besides Theorem 6.23, it also underlies Corollary 6.20's operator-norm bound for the unstructured sample covariance matrix (used in turn for the two example ensembles in Section 6.4.5), by taking $Q_i:=x_ix_i^T-\Sigma$. Theorem 6.23 itself is the standard justification for thresholding-based covariance estimators used throughout high-dimensional statistics whenever the sparsity pattern of $\Sigma$, though unknown, is believed to be structured.

Formalizing it. No faithful prior art exists on the platform for the matrix Bernstein bound or covariance thresholding (a fresh search for "matrix Bernstein," "Bernstein condition matrix," "thresholding covariance," and "sparse covariance" returned no hits). The existing RademacherWigner.* items formalize spectral-edge and empirical-spectral-distribution bounds for the Wigner ensemble specifically (a symmetric matrix with i.i.d. entries) — a narrower, different random-matrix model from the general Bernstein-condition matrices this chapter treats, and not reused here. All three theorems are drafted as open goals (:= by sorry).

Difficulty

The naive approach to a matrix tail bound — apply the scalar Chernoff/Bernstein technique directly to the operator norm — fails because the operator norm is not a linear functional of $Q$, so the scalar moment generating function bound does not translate directly. The resolution (Lemma 6.13, not itself part of this mission) instead bounds the trace of the matrix exponential of the sum, which is linear-algebraically tractable via the Golden–Thompson-type inequality and the union bound over the (at most $\mathrm{rank}(\bar V)$) nonzero eigenvalue directions of the aggregate variance $\bar V=\sum_i\mathrm{var}(Q_i)$ — this is exactly why the bound's prefactor is $\mathrm{rank}(\bar V)$, not the ambient dimension $d$: a low-rank aggregate variance (e.g. from a highly structured collection of matrices) yields a much tighter bound than a naive union bound over all $d$ eigen-directions would. Theorem 6.23's own difficulty is entirely in the reduction to Theorem 6.17 plus Eq. (6.54): checking that $Q_i:=x_ix_i^T-\Sigma$ satisfies the Bernstein condition with the stated parameters, and that $\|\hat\Sigma-\Sigma\|_{\max}$ concentrates at the stated rate via a union bound over the $O(d^2)$ matrix entries.

Formalization scope

"Symmetric" is realized via Mathlib's Matrix.IsSymm; the Loewner order via (B-A).PosSemidef. The matrix moment generating function itself (ΨQ(λ):=E[e^{λQ}]) is not formalized, since none of this mission's three theorem statements need it directly — Bernstein's condition (Definition 6.10) is stated purely in terms of polynomial moments $\mathbb E[Q^j]$, avoiding the substantial extra machinery (Mathlib's NormedSpace.exp for matrices) that a faithful matrix-exponential definition would require, at no cost to faithfulness for the three statements actually drafted.

Independence of $\{Q_i\}$/$\{x_i\}$ is realized via Mathlib's iIndepFun; this required adding a local MeasurableSpace (Matrix (Fin d) (Fin d) ℝ) instance in the workspace, since Matrix is a def, not an abbrev, over the underlying Pi type, so Lean's instance search does not automatically find the Pi-type MeasurableSpace instance for it. "Identically distributed" is realized via Mathlib's IdentDistrib against a fixed reference index. "Each component sub-Gaussian" is restated locally as an explicit MGF bound at the reference index, per this book's cross-chapter rule against importing another chapter's draft definitions.

If a statement admits a trivializing formalization: the rank(...) prefactor of Theorem 6.17 is kept exactly, not replaced by the ambient dimension $d$ (which would be a strictly weaker, non-trivializing but unfaithful simplification, since the bound's whole point is that rank(...) ≤ d can be much smaller). ‖·‖_max and opNorm at d=0 return Mathlib's junk value 0 (harmless: no matrix entries or singular values exist at that degenerate size either).

Out of scope for this mission: Theorem 6.15 (the sub-Gaussian-tail matrix concentration result that precedes Theorem 6.17 in the same section) and Corollary 6.20 (the unstructured covariance-estimation corollary) — both natural follow-on work, cut for this chunk's time budget; see STATUS.md.

Selected references

• M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019. DOI: 10.1017/9781108627771. Chapter 6.
• J. A. Tropp, "User-friendly tail bounds for sums of random matrices," Foundations of Computational Mathematics, 12(4):389–434, 2012.