Machine Learning

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

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

Linear methods like SVMs work only when the classes are linearly separable, but most real data is not. Chapter 6 shows how to get non-linear decision boundaries for free: replace the input space's inner product with a kernel $K$ that implicitly computes an inner product in a (possibly very high- or infinite-dimensional) feature space, without ever explicitly computing the feature mapping. This works for any positive definite symmetric (PDS) kernel — and the chapter's central theorem shows that such a kernel always induces a genuine Hilbert space (the reproducing kernel Hilbert space, RKHS) in which the kernel is literally an inner product. The chapter's capstone, the representer theorem, then shows that a broad class of optimization problems over this (possibly infinite-dimensional) Hilbert space always has a solution expressible as a finite linear combination of kernel evaluations at the training points — turning an infinite-dimensional problem into a finite, $m$-dimensional one.

Setting

A kernel $K:X\times X\to\mathbb R$ is PDS (Definition 6.3) if for every finite sample $\{x_1,\dots,x_m\}\subseteq X$, the Gram matrix $[K(x_i,x_j)]$ is symmetric positive semidefinite. Theorem 6.8 shows every PDS kernel is an inner product $K(x,x')=\langle \Phi(x),\Phi(x')\rangle$ in some Hilbert space $H$ (the RKHS), which further has the reproducing property $h(x)=\langle h,K(x,\cdot)\rangle$ for every $h\in H$ — evaluating $h$ at a point is itself an inner product with the kernel section at that point. Theorem 6.10 shows PDS kernels are closed under sum, product, tensor product, pointwise limit, and power-series composition, letting complex kernels (Gaussian, and many others) be built from simple ones (polynomial kernels) without re-verifying positive-semidefiniteness from scratch. Section 6.3's representer theorem (Theorem 6.11) then considers minimizing, over $h\in H$, an objective $F(h)=G(\|h\|_H)+L(h(x_1),\dots,h(x_m))$ that depends on $h$ only through its norm and its values at $m$ fixed points.

Formalization targets

Theorem 6.8 (RKHS existence, milestone). For a PDS kernel $K$, there exist a Hilbert space $H$ and $\Phi:X\to H$ with $K(x,x')=\langle\Phi(x),\Phi(x')\rangle$, and $H$ has the reproducing property $h(x)=\langle h,K(x,\cdot)\rangle$ for all $h\in H$, $x\in X$.

Theorem 6.10 (closure properties, milestone). PDS kernels are closed under sum, product, tensor product, pointwise limit, and power-series composition with non-negative coefficients.

Theorem 6.11 — the mission's goal. For any non-decreasing $G:\mathbb R\to\mathbb R$ and any loss $L:\mathbb R^m\to\mathbb R\cup\{+\infty\}$, $\mathrm{argmin}_{h\in H} G(\|h\|_H)+ L(h(x_1),\dots,h(x_m))$ admits a solution $h^\star=\sum_{i=1}^m\alpha_i K(x_i,\cdot)$; if $G$ is increasing, every solution has this form.

Significance

Theorem 6.11 is the chapter's payoff and one of the most widely used structural results in kernel methods: it explains, in one general statement covering SVMs, kernel ridge regression, Gaussian process MAP estimation and many other algorithms simultaneously, why the dual (finite, $m$-coefficient) formulation always suffices — the RKHS's infinite dimensionality never has to be confronted directly. Theorem 6.8 is the structural fact the whole chapter (and every later kernelized algorithm in the book, chapters 9-11, 15) depends on: without it, "PDS kernel" would be a purely combinatorial condition on Gram matrices with no guarantee it corresponds to any actual inner product. No prior art on the Prove2Me platform is faithful to any of this chapter's content: GET /theorems?q=Representer theorem and q=reproducing kernel return no faithful match (one unrelated hit concerns a Gaussian-measure reproducing kernel in a different, probabilistic context, not this chapter's PDS-kernel/RKHS construction). All six items are drafted fresh.

Difficulty

Theorem 6.8's proof is a genuine construction: define $H_0$ as finite linear combinations of kernel sections $\Phi(x)=K(x,\cdot)$, define an inner product on $H_0$ using $K$ itself, verify it is well-defined (independent of the representation), positive semidefinite (via the PDS hypothesis), and — via the Cauchy-Schwarz-for-PDS-kernels lemma (Lemma 6.7) — actually positive definite, then complete $H_0$ to a genuine Hilbert space $H$ in which it is dense, and finally extend the reproducing property from the dense subspace $H_0$ to all of $H$ by a continuity argument. This is substantial analysis, not a restatement. Theorem 6.11's proof uses the orthogonal decomposition $H=H_1\oplus H_1^\perp$ (where $H_1=\mathrm{span}\{K(x_i, \cdot)\}$) and the reproducing property to show the orthogonal component $h^\perp$ never helps and, when $G$ is strictly increasing, strictly hurts — a short argument, but one that depends essentially on Theorem 6.8's reproducing property holding for the specific $H$ constructed, not just any Hilbert space with the kernel as its inner product.

Formalization scope

IsPDS uses the book's own second SPSD characterization (c^T K c ≥ 0 for every finite sample and coefficient vector c) rather than the non-negative-eigenvalues characterization, avoiding spectral theory for a Prop-valued definition; the book states the two are equivalent. IsRKHSOf and IsMinimizer are formalization scaffolding, not book-numbered definitions: IsRKHSOf packages Theorem 6.8's own two displayed equations (6.8, 6.9) as a reusable predicate shared between Theorem 6.8 (its conclusion) and Theorem 6.11 (its "H its corresponding RKHS" hypothesis), using an explicit evaluation map ev : H → X → ℝ to stand in for "elements of H are functions on X," since Mathlib's abstract Hilbert spaces are not themselves spaces of functions; IsMinimizer packages argmin. Both X in Theorem 6.8's existential and Theorem 6.11's ambient type are plain Type rather than Type*, avoiding universe-polymorphic quantification over the constructed Hilbert space's own type — a harmless simplification, since every application in this book instantiates X at a concrete, small type (typically $\mathbb R^N$ or a finite set). Theorem 6.11's loss codomain ℝ ∪ {+∞} is WithTop ℝ, not EReal (which would also admit -∞, an unstated generalization the book's own display does not license, since EReal's ⊤+⊥=⊥ collapse is a genuine faithfulness risk the book's own L:\mathbb R^m\to\mathbb R\cup\{+\infty\} avoids by construction). WithTop ℝ on its own does not avoid every collapse, though: an unconstrained L may be the constant function ⊤ (a legal instance of ℝ∪\{+\infty\}), forcing the objective identically ⊤ and every point to vacuously minimize it, which would make the theorem's second conjunct false. An added hypothesis, ∃ h₀, F h₀ ≠ ⊤, makes explicit the book's own implicit assumption that the objective is finite somewhere — see the Formalization scope note below. Theorem 6.11's two clauses are otherwise kept exactly as distinct as the book states them: existence needs only Monotone G (non-decreasing); "any solution has this form" needs StrictMono G (increasing) as an added hypothesis on the second conjunct only — per this chunk's own BRIEF.md, the crux of the theorem, and the trap this mission is most careful to avoid collapsing. Theorem 6.10's five closure clauses are stated as one conjunction (matching the book's single theorem, not five separate items); the power-series clause keeps the book's own radius-of-convergence domain restriction and adds an explicit summability hypothesis guarding the ∑' term.

Not formalized: Theorem 6.2 (Mercer's condition) — not needed by the goal's own proof chain (it is an equivalent characterization of PDS mentioned before the RKHS construction, not a premise Theorem 6.8's or 6.11's proof invokes) and its own hypotheses (compact $X\subset \mathbb R^N$, continuous $K$, an eigenfunction expansion of a compact self-adjoint integral operator) are real analytic content this mission's budget does not include; Lemma 6.7 (Cauchy-Schwarz for PDS kernels) and Lemma 6.9 (normalized PDS kernels) — supporting lemmas for Theorem 6.8's proof, not independently numbered results the goal cites; Theorem 6.12/Corollary 6.13 (Rademacher complexity/margin bounds for kernel-based hypotheses) — the chapter's optional further milestone, connecting to chunks 03/05's machinery, cut for budget; §6.5-6.8 (sequence kernels, weighted transducers, rational kernels, Bochner's theorem, approximate feature maps) — explicitly out of scope per this chunk's own BRIEF.md, a distinct, applications-heavy topic.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 6, §6.1-6.4.
• B. Schölkopf, R. Herbrich, A. J. Smola, "A generalized representer theorem," COLT 2001, Lecture Notes in Computer Science 2111, 2001, 416-426.
• N. Aronszajn, "Theory of reproducing kernels," Transactions of the American Mathematical Society 68(3), 1950, 337-404.

Motivation

Chapter 2 of Steinwart & Christmann, Support Vector Machines, showed the hinge loss controls the classification loss (Zhang's inequality, Theorem 2.31). That result was special to one target/surrogate pair. Chapter 3 asks the question in general: given any target loss $L_{\mathrm{tar}}$ (the loss whose risk we actually care about) and any surrogate loss $L_{\mathrm{sur}}$ (the loss a learning algorithm actually minimizes, chosen for tractability — convexity, differentiability), when does controlling the excess $L_{\mathrm{sur}}$-risk control the excess $L_{\mathrm{tar}}$-risk? The book's answer factors the question through a purely pointwise object, the calibration function, that depends only on the two losses and a single label distribution — not on the learning problem's ambient space $X$ or the unknown data-generating distribution $P$ at all.

Setting

Fix a measurable space $X$ and a closed label set $Y \subset \mathbb R$. For a loss $L : X \times Y \times \mathbb R \to [0,\infty)$, a distribution $Q$ on $Y$, and $x \in X$, the inner $L$-risk is $C_{L,Q,x}(t) := \int_Y L(x,y,t)\,dQ(y)$ and the minimal inner risk is $C^*_{L,Q,x} := \inf_t C_{L,Q,x}(t)$ (Definition 3.3). Eq. (3.5) rewrites the ordinary $L$-risk of $f$ against a full distribution $P$ on $X \times Y$ as $R_{L,P}(f) = \int_X C_{L,P(\cdot\mid x),x}(f(x))\,dP_X(x)$: the outer risk is an average of inner risks over the $X$-marginal, one inner risk per conditional distribution $P(\cdot\mid x)$. The set of $\varepsilon$-approximate minimizers is $M_{L,Q,x}(\varepsilon) := \{t : C_{L,Q,x}(t) < C^*_{L,Q,x} + \varepsilon\}$ (Definition 3.5).

The calibration function $\delta_{\max}(\varepsilon, Q, x)$ of a pair $(L_{\mathrm{tar}}, L_{\mathrm{sur}})$ (Definition 3.13) is the largest $\delta$ such that every $\delta$-approximate surrogate minimizer is already an $\varepsilon$-approximate target minimizer: $\delta_{\max}( \varepsilon, Q, x) := \inf\{C_{L_{\mathrm{sur}},Q,x}(t) - C^*_{L_{\mathrm{sur}},Q,x} : t \notin M_{L_{\mathrm{tar}},Q,x}(\varepsilon)\}$ when $C^*_{L_{\mathrm{sur}},Q,x} < \infty$, and $\infty$ otherwise. $L_{\mathrm{sur}}$ is $L_{\mathrm{tar}}$-calibrated with respect to a set $\mathcal Q$ of label distributions if $\delta_{\max}(\varepsilon, Q, x) > 0$ for every $\varepsilon \in (0,\infty]$, $Q \in \mathcal Q$, $x$ — one $\delta_{\max}$ working uniformly over the whole class $\mathcal Q$, not just a single fixed distribution.

Formalization targets

Goal: Corollary 3.19 (calibration $\iff$ uniform risk implication, bounded target)

$$L_{\mathrm{sur}}\text{ is }L_{\mathrm{tar}}\text{-calibrated w.r.t. }\mathcal Q \iff \forall \varepsilon \in (0,\infty],\ \forall P \text{ of type } \mathcal Q \text{ with } R^*_{L_{\mathrm{sur}},P}<\infty,\ \exists \delta \in (0,\infty],\ \forall f,$$ $$R_{L_{\mathrm{sur}},P}(f) < R^*_{L_{\mathrm{sur}},P}+\delta \implies R_{L_{\mathrm{tar}},P}(f) < R^*_{L_{\mathrm{tar}},P}+\varepsilon$$

when $L_{\mathrm{tar}}$ is bounded. This is the mission's capstone: a purely pointwise, $P$-independent condition (calibration) is shown equivalent to a whole-class-of-distributions statistical guarantee, not merely necessary for it.

Milestones (attack order)

1. Lemma 3.4 — the Bayes risk is the integral of the minimal inner risks: $R^*_{L,P} = \int_X C^*_{L,P(\cdot\mid x),x}\,dP_X(x)$, and $x \mapsto C^*_{L,P(\cdot\mid x),x}$ is measurable. Foundational: it is what makes minimizing risk pointwise, one conditional distribution at a time, a valid strategy at all.
2. Lemma 3.11 — for $\varepsilon \in (0,\infty]$, $C^*_{L,P(\cdot\mid x),x} < \infty$ for $P_X$-a.a. $x$ iff a measurable $\varepsilon$-approximate minimizer selection $f$ exists. Directly invoked in Theorem 3.17's own proof.
3. Lemma 3.14 — the calibration function traps the surrogate's $\delta_{\max}(\varepsilon)$ -approximate minimizers inside the target's $\varepsilon$-approximate minimizers (and no larger $\delta$ does), plus the pointwise inequality Eq. (3.16), $\delta_{\max}(C_{L_{\mathrm{tar}},Q,x}(t)-C^*_{L_{\mathrm{tar}},Q,x}, Q, x) \le C_{L_{\mathrm{sur}},Q,x}(t)-C^*_{L_{\mathrm{sur}},Q,x}$. Directly invoked in Theorem 3.17's proof ("By part i) of Lemma 3.14...").
4. Theorem 3.17 — for a single fixed $P$, an a.s.-strictly-positive calibration function is necessary for the risk implication (3.18), and sufficient under an added domination condition (Eq. (3.19), a $P_X$-integrable envelope on the excess inner target risk).

Theorem 3.22 (BRIEF.md's originally recommended goal — the fully quantitative uniform calibration inequality, using a Fenchel-Legendre biconjugate) was not attempted; see STATUS.md for the reason and the fallback taken instead.

Significance

Corollary 3.19 is the chapter's answer to "is calibration actually useful, or just necessary?" Theorem 3.17 alone only rules out non-calibrated surrogates; Corollary 3.19 shows that for the two most important bounded target losses in the book — the classification loss and the density-level- detection loss — calibration is exactly the right test, with no gap between necessity and sufficiency. Concretely: the book's Example 3.16 computes that both the least-squares and hinge losses are calibrated surrogates for the classification loss for every $\eta \in [0,1]$, and this corollary is what turns that pointwise computation into the qualitative consistency guarantee "minimizing empirical hinge risk is a statistically sound way to approach the empirical classification risk," ahead of the sharper quantitative form Zhang's inequality already supplies for that one pair (Theorem 2.31) and Theorem 3.22 supplies in general.

Difficulty

The apparatus itself — inner risks, approximate-minimizer sets, the calibration function — is the chapter's real content, and getting the finite/infinite distinction right throughout is the chapter's central technical difficulty: Lemma 3.11's whole point is that "$C^*_{L,P(\cdot\mid x),x}<\infty$ for a.e. $x$" is a genuine dichotomy, not a standing assumption, and the calibration function's own definition branches on exactly this finiteness. A real-valued, junk-at-infinity convention for risks (as used in the 01-loss-functions mission, where losses were always bounded) would silently collapse this dichotomy and trivialize Lemma 3.11 and much of Theorem 3.17's content. The definitions in this mission are built in ENNReal (Lean's $[0,\infty]$) throughout specifically to avoid this trap.

Formalization scope

$X$ is an arbitrary measurable space; label distributions $Q$ range over Measure ℝ with no IsProbabilityMeasure requirement in InnerRisks/CalibrationFunction/Lemma 3.14 — re-reading Lemma 3.14's proof directly (p. 59) found no step that uses $Q$ having total mass $1$, so this hypothesis is dropped as a disclosed generalization there, matching the convention this series already used for Lemma 2.23's convexity hypothesis. Wherever a genuine distribution $P$ on $X \times Y$ is required (Lemma 3.4, Lemma 3.11, Theorem 3.17, Corollary 3.19), $P$ is represented as a pair $(P_X, \kappa)$ — an $X$-marginal $P_X$ and a measurable family $\kappa : X \to \text{Measure } \mathbb R$ of conditional distributions $P(\cdot\mid x)$ — with ∀ x, IsProbabilityMeasure (κ x) added explicitly at each such use site, since the (PX, κ) representation does not force this by its types alone. X being a complete measurable space (required by all four theorem-kind items but Lemma 3.14) is rendered as the disclosed sufficient condition "$\exists$ a probability measure $\mu$ for which $\mu$-null sets have every subset measurable" rather than the book's exact universal-completion equality — see Def_..._IsCompleteMeasurableSpace's own note. $\varepsilon$ ranges over ENNReal throughout, so "$\varepsilon \in [0,\infty]$"/"$(0,\infty]$" need no narrowing, unlike this series' real-valued conventions elsewhere.

A trivializing formalization here would let IsCalibrated/the calibration function be an unconstrained hypothesis disconnected from innerRisk/approxMinimizers, or let κ/PX range freely with no link to outerRisk/bayesRisk as actually defined — both are ruled out since every item's statement is built compositionally from the same innerRisk/minInnerRisk/ approxMinimizers/outerRisk/bayesRisk definitions, traced back to Definitions 3.3, 3.5, 2.2 and 2.3 exactly as the book states them.

Loss, innerRisk/minInnerRisk/approxMinimizers, outerRisk/bayesRisk/IsOfType, and calibrationFunction/IsCalibrated are reusable beyond this mission: this series' 06- classification chunk restates this chapter's apparatus locally (per Hard Rule 9, drafts cannot import each other) when it reuses Chapter 3's calibration ideas for its own oracle inequality. Contributions completing the five sorrys are welcome; Theorem 3.22 itself (the fully quantitative version this mission's BRIEF.md recommended as the primary goal) remains a natural follow-up mission built on top of this one's definitions.

Selected references

• I. Steinwart & A. Christmann, Support Vector Machines, Springer, Information Science and Statistics, 2008. https://doi.org/10.1007/978-0-387-77242-4 (Chapter 3, §§3.1-3.3, pp. 49-65).
• T. Zhang, "Statistical behavior and consistency of classification methods based on convex risk minimization," Annals of Statistics 32(1), 2004, pp. 56-85. https://doi.org/10.1214/aos/1079120130
• P. L. Bartlett, M. I. Jordan & J. D. McAuliffe, "Convexity, classification, and risk bounds," Journal of the American Statistical Association 101(473), 2006, pp. 138-156. https://doi.org/10.1198/016214505000000907

Motivation

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

Chapters 2 and 3 bound the estimation error of a hypothesis chosen from a fixed hypothesis set $H$, but the choice of $H$ itself is left open: a richer $H$ lowers the approximation error (how close $H$ comes to the Bayes classifier) at the price of a looser generalization bound, and a poorer $H$ does the reverse. Chapter 4 is the book's answer to this trade-off. It first shows that Empirical Risk Minimization (ERM) alone cannot resolve it — ERM ignores the complexity of $H$ entirely — and then develops Structural Risk Minimization (SRM): decompose a rich hypothesis set into a nested countable union $H=\bigcup_{k\ge1}H_k$ of increasingly complex pieces, and let the learning algorithm balance empirical fit against a complexity penalty for each $H_k$ automatically. The chapter closes by showing how the same balance can be achieved computationally through convex surrogate losses, whose minimization is tractable where minimizing the zero-one loss directly is not.

Setting

For a hypothesis $h$ chosen from $H$, the excess error $R(h)-R^*$ decomposes into an estimation term $R(h)-\inf_{h\in H}R(h)$ and an approximation term $\inf_{h\in H}R(h)-R^*$ (Eq. 4.1). Proposition 4.1 bounds ERM's estimation error by twice the uniform deviation $\sup_{h\in H}|R(h)-\hat R_S(h)|$. For a nested family $(H_k)_{k\ge1}$ and $h\in H$, $k(h)$ denotes the least index with $h\in H_{k(h)}$; SRM selects $h_S^{SRM}$ by minimizing $F_k(h)=\hat R_S(h)+R_m(H_k)+\sqrt{\log k/m}$ jointly over $k\ge1$ and $h\in H_k$, where $R_m(H_k)$ is $H_k$'s Rademacher complexity (Definitions 3.1/3.2, restated locally in this chunk's ModelSelection namespace). Theorem 4.2 is the resulting learning guarantee. Section 4.4 develops a competing model-selection procedure, cross-validation, and Theorem 4.4 directly compares its guarantee to SRM's on a held-out split of the sample. Section 4.7 turns to real-valued scoring functions $h:X\to\mathbb R$ with sign convention $f_h(x)=\mathrm{sign}(h(x))$ and a convex non-decreasing surrogate $\Phi$ of the zero-one loss; the Bayes scoring function $h^*(x)=\eta(x)-\tfrac12$ (Eq. 4.9) and the $\Phi$-loss $L_\Phi$ (Eq. 4.10) let Theorem 4.7 bound the true excess error by a power of the surrogate's own excess loss.

Formalization targets

Proposition 4.1 (ERM bound, milestone). For any sample $S$, $\Pr[R(h_S^{ERM}) - \inf_{h\in H}R(h) > \epsilon] \le \Pr[\sup_{h\in H}|R(h)-\hat R_S(h)| > \epsilon/2]$.

Theorem 4.2 — the mission's goal. For a nested countable union $H=\bigcup_{k\ge1}H_k$ and $h_S^{SRM}$ minimizing $F_k(h)$ over the whole union, for any $\delta>0$, with probability at least $1-\delta$:

$$R(h_S^{SRM}) \le \inf_{h\in H}\Big[R(h)+2R_m(H_{k(h)})+\sqrt{\tfrac{\log k(h)}m}\Big] + \sqrt{\tfrac{2\log(3/\delta)}m}.$$

Theorem 4.4 (Cross-validation versus SRM, milestone). Splitting a sample of size $m$ into $S_1$ (size $(1-\alpha)m$, training) and $S_2$ (size $\alpha m$, validation), for any $\delta>0$, with probability at least $1-\delta$:

$$R(h_S^{CV}) - R(h_{S_1}^{SRM}) \le 2\sqrt{\tfrac{\log\max(k(h_S^{CV}),k(h_{S_1}^{SRM}))}{\alpha m}} + 2\sqrt{\tfrac{\log(4/\delta)}{2\alpha m}}.$$

Theorem 4.7 (Convex-surrogate excess-error bound, milestone). For $\Phi$ convex and non-decreasing with $s\ge1,c>0$ satisfying $|h^*(x)|^s \le c^s(L_\Phi(x,0)-L_\Phi(x,h^*_\Phi(x)))$ for all $x$: $R(h)-R^* \le 2c(L_\Phi(h)-L^*_\Phi)^{1/s}$.

Significance

Theorem 4.2 is the chapter's headline result and the theoretical justification for regularization-based learning: it shows that a single algorithm, without knowing in advance which $H_k$ contains a good hypothesis, achieves a guarantee that is — up to the $\sqrt{\log k(h)/m}$ penalty — as favorable as if an oracle had revealed the best-in-class index in advance (Eq. 4.6). It is also the chapter's genuine new content beyond chunk 03-rademacher-vc's single-hypothesis-set bound: the countable union bound (a 1/k²-weighted union over $k\ge1$ converging to $\pi^2/6$, hence the $\log 3$ appearing in place of $\log 2$) is not a restatement of Theorem 3.3 but a distinct argument, and the goal's inf over the whole nested family is what makes SRM a model-selection method rather than a bound for one fixed $k$. Theorem 4.4 is the chapter's only head-to-head comparison between two competing model-selection procedures, on two genuinely different samples. Theorem 4.7 is the bridge between the learning-theoretic guarantees of chapters 2-4 and the actually-implemented convex optimization problems of chapters 5 (SVM), 6 (kernels) and beyond, all of which minimize a convex surrogate rather than the zero-one loss directly. No prior art exists on the platform: GET /theorems?q=structural%20risk%20minimization and GET /theorems?q=model%20selection both return zero hits.

Difficulty

Theorem 4.2's proof genuinely uses the union bound over a countably infinite family indexed by $k\ge1$ with weight $1/k^2$ converging to $\pi^2/6 < 2$ (Eq. 4.5) — this is the chapter's distinct new technique, not an application of chunk 03's finite/VC-dimension machinery to a single $H_k$; a formalization that stated the bound only for one fixed $k$, or dropped the inf over the whole union in favor of a single best-in-class $h^*$, would be Theorem 4.2's named trivializing formalization (BRIEF.md's pitfall note) rather than the theorem itself. Theorem 4.4 requires keeping two distinct samples ($S_1$, $S_2$, of different, precisely related sizes) and two distinct hypotheses ($h_S^{CV}$, $h_{S_1}^{SRM}$) apart throughout; conflating them collapses the comparison to a tautology. Theorem 4.7's difficulty is in its setup, not its statement: the Bayes scoring function, the $\Phi$-loss, and the pointwise $\Phi$-minimizer $h^*_\Phi$ (which the book allows to take the extended values $\pm\infty$ at the degenerate points $\eta(x)\in\{0,1\}$) all need care to state without silently altering the theorem's content.

Formalization scope

GeneralizationError, EmpiricalError, EmpiricalRademacherComplexity and RademacherComplexity are restated locally in this chunk's ModelSelection namespace (identical in content to chunk 03-rademacher-vc's own copies), since a draft item cannot import another chunk's draft module. LeastIndex H h (k(h)) is Nat.sInf {k | 1 ≤ k ∧ h ∈ H k}; every theorem using it carries the standing hypothesis that h lies in the relevant union, guarding against trap 5 (Nat.sInf of an empty set). Theorem 4.2's hSRM and Proposition 4.1's hERM are hypothesis-supplied functions satisfying the book's optimality property, not constructed via choice over an unconstrained H; H.Nonempty (Proposition 4.1) and (⋃ k ≥ 1, Hk k).Nonempty (Theorem 4.2) guard the outer sInf/inf terms against trap 5. Theorem 4.7's $h^*_\Phi$ is formalized as a real-valued function satisfying the pointwise minimization property for all $x$; the book's own extended-real convention ($h^*_\Phi(x)=\pm\infty$ exactly where $\eta(x)\in\{0,1\}$) is outside this formalization — disclosed here and in MODERATION_NOTES.md — since no real number satisfies the minimizing property at those degenerate points, the theorem as stated applies precisely to the case a real-valued $h^*_\Phi$ can be supplied, which is the book's own generic case. No numerical constant is altered from the book in any of the four theorems: 2 and log(3/δ) in Theorem 4.2, 2 (twice) and log(4/δ) in Theorem 4.4, and 2c and the exponent 1/s in Theorem 4.7 are exactly as displayed.

Not formalized: the discussion of computing $k^*$ via binary search (a computational, not a statistical, result); $n$-fold and leave-one-out cross-validation (Section 4.5, a practical variant of Theorem 4.4's two-sample cross-validation without its own numbered generalization bound); regularization-based algorithms (Section 4.6, the uncountable-union extension of SRM, which the book itself only sketches without a numbered theorem); Lemma 4.5 and Proposition 4.6 (intermediate results establishing that $h^*_\Phi$ induces the same classifier as $h^*$, needed for Theorem 4.7's proof but not part of its statement); and the worked examples for the hinge, exponential and logistic losses (instantiations of Theorem 4.7's $s,c$, not separate theorems). Drafting only these worked instantiations in place of Theorem 4.7's general statement would be a trivializing formalization for this chapter.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 4.
• V. Vapnik, Statistical Learning Theory, Wiley-Interscience, 1998 (structural risk minimization).
• T. Zhang, "Statistical behavior and consistency of classification methods based on convex risk minimization," Annals of Statistics 32(1), 2003 (Theorem 4.7's origin).

Motivation

Every method in Chapters 2-4 of this series solves a projection or proximal subproblem at every step — a Euclidean projection, or a Bregman-divergence prox-mapping — which can itself be as hard as the original problem when $X$ is a complicated feasible set (a spectrahedron, a flow polytope, a matroid base polytope). The conditional gradient method (Frank & Wolfe, 1956) sidesteps this entirely: instead of a projection, each step calls a linear optimization (LO) oracle — minimize a linear function over $X$ — which is frequently far cheaper (over a spectrahedron, this reduces to a single eigenvector computation; over many combinatorial polytopes, to a greedy algorithm). This is the origin of the modern "projection-free" family of optimization methods widely used at the scale where projections are the bottleneck.

Setting

Fix a nonempty compact convex set $X$ in a real normed space $E$ and a convex $f:X\to \mathbb R$ with $L$-Lipschitz gradient (Eq. (7.1.4)): $\|f'(x)-f'(y)\|_*\le L\|x-y\|$. The classic conditional gradient (CndG) method, Algorithm 7.1, sets $x_0\in X$, $y_0=x_0$, and for $k=1,2,\dots$: calls the LO oracle $x_k\in\arg\min_{z\in X}\langle f'(y_{k-1}),z\rangle$, then sets $y_k=(1-\alpha_k)y_{k-1}+\alpha_kx_k$ for a stepsize $\alpha_k\in[0,1]$, either the fixed schedule $\alpha_k=2/(k+1)$ (Eq. (7.1.9)) or exact line search (Eq. (7.1.10)).

Section 7.1.1.2 extends this to bilinear saddle-point problems, where $f$ itself is the (generally nonsmooth) function $f(x)=\max_{y\in Y}\{\langle Ax,y\rangle-\hat f(y)\}$ (Eq. (7.1.5)) for a compact convex $Y$ and linear operator $A$. Since $f$ is nonsmooth, the method is applied instead to a family of smooth approximations $f_\eta$ built from a strongly convex $\omega$ on $Y$ (Eq. (7.1.21)-(7.1.23)), with the smoothing parameter $\eta_k$ allowed to vary across iterations rather than being fixed in advance.

Formalization targets

Goal — Theorem 7.1

$$f(y_k) - f^* \le \frac{2L}{k(k+1)}\sum_{i=1}^k\|x_i-y_{i-1}\|^2.$$

Supporting milestones, in attack order

• Lemma 7.1: the smoothed objective family $f_\eta$ is monotone nondecreasing in $\eta\ge0$ — the one-line fact ($V(y)-D_Y^2\le0$ pointwise) that licenses a variable, decreasing smoothing schedule $\eta_k$ rather than a schedule fixed in advance from knowledge of the target accuracy.
• Theorem 7.2: the saddle-point counterpart of the goal theorem, running the same CndG algorithm on the smoothed gradients $f_{\eta_k}'$ instead of $f'$ directly, with the explicit rate $f(y_k)-f^*\le\frac{2}{k(k+1)}\sum_{i=1}^k[i\eta_iD_Y^2+\frac{\|A\|^2}{\sigma_v\eta_i} \|x_i-y_{i-1}\|^2]$.

Every constant here is exactly the book's; the goal theorem's bound is left in terms of the actual step distances $\sum\|x_i-y_{i-1}\|^2$, not a diameter-based simplification (see Difficulty).

Significance

This mission formalizes the founding convergence result of the entire projection-free family (Frank-Wolfe methods), which has become central to large-scale machine learning precisely because its per-iteration cost can be orders of magnitude below that of a projection-based method on structured feasible sets. Theorem 7.1's specific form — a rate depending on the realized step distances rather than a fixed diameter — is also the more informative, tighter statement (the book's own remarks show it recovers the classical diameter-based $O(LD_X^2/\varepsilon)$ complexity as a corollary, but also explains why the rate can be much better in practice when the iterates settle near an extreme point).

No result matching conditional gradient / Frank-Wolfe methods exists on the platform as of 2026-09-18 (q=Frank-Wolfe and q=conditional gradient both return zero hits — see Prior art in MODERATION_NOTES.md).

Difficulty

The chief formalization difficulty is representing "with the stepsize policy in (7.1.9) or (7.1.10)" faithfully without either restricting to one policy (weaker than the book's stated theorem) or introducing an awkward disjunction of two separate algorithm definitions. The book's own proof resolves this by a single observation used for both policies at once: $f(y_k)\le f(\tilde y_k)$ for $\tilde y_k$ the point the fixed schedule $\gamma_k=2/(k+1)$ would have produced — trivially by equality under (7.1.9), or because $y_k$ is chosen to minimize $f$ over the entire line segment under (7.1.10), of which $\tilde y_k$ is one point. This mission's hyk_le hypothesis states exactly this shared consequence, which is genuinely what the proof uses and genuinely covers both policies, rather than picking one arbitrarily.

A second difficulty is not collapsing $\sum_{i=1}^k\|x_i-y_{i-1}\|^2$ into a diameter bound $kD_X^2$ inside the milestone itself — the book's own remarks perform that substitution as a separate, weaker corollary (Eq. (7.1.19)) after stating Theorem 7.1 in its sharper form; folding the substitution into the goal statement itself would silently prove a different, weaker theorem.

Formalization scope

conditional_gradient_rate and saddle_point_cndg_rate state the LO oracle's exactness (x k ∈ Argmin_{z∈X}⟨fGrad(y(k-1)),z⟩) as a pointwise hypothesis rather than deriving it from IsCompact X via an existence lemma — matching the pointwise-hypothesis convention this series uses throughout for argmin-defined algorithmic steps (chunk 03-deterministic's mirror-descent updates, chunk 04-stochastic's stochastic mirror-descent update). X compact convex is still included as a hypothesis, matching the book's own standing assumption on the problem class, even though it is not itself needed to derive the stated conclusion from the other hypotheses.

smoothed_objective_monotone and saddle_point_cndg_rate realize $f_\eta$/$f$ via sSup of the image of $Y$ under the pointwise saddle-point objective, matching the book's own max_{y∈Y}{...} definition (Eq. (7.1.5), (7.1.23)) directly rather than introducing a separate Def_ file for a "bilinear saddle-point objective" structure — no other item in this mission reuses that definition verbatim, so per this series' convention (no shared substrate bundled into a structure unless reused), it is inlined at each use.

A trivializing formalization this mission rules out: stating the LO oracle via an $\varepsilon$-approximate minimizer ((fGrad (y(k-1))) (x k) ≤ (fGrad (y(k-1))) z + ε for some ε) rather than an exact one — this is explicitly a different, weaker algorithm the book does not analyze in Theorem 7.1/7.2 (the book studies approximate LO oracles separately, later in the chapter, not selected here).

Left out of scope, for time: Theorem 7.7 (the matching lower complexity bound for LO-oracle methods, Eq. (7.1.60)) — formalizing it faithfully requires first modeling the abstract class of "LCP methods" (any algorithm restricted to LO-oracle calls) as a universally-quantified object, a substantially different and more involved formalization task than the two upper-bound convergence theorems selected here; named per Hard Rule 7 rather than approximated. The d(x)=\sum x_i\log x_i entropy-smoothing remark and the primal/primal-dual averaging CndG variants (§7.1.2, not covered by this mission's page range) are likewise not attempted.

Selected references

• G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, Springer 2020, Chapter 7, §7.1.1. https://doi.org/10.1007/978-3-030-39568-1
• M. Frank, P. Wolfe, "An algorithm for quadratic programming," Naval Research Logistics Quarterly, 3(1-2), 1956, pp. 95-110.
• M. Jaggi, "Revisiting Frank-Wolfe: projection-free sparse convex optimization," ICML, 2013 (the modern machine-learning revival of the method).

Motivation

Empirical-risk-minimization objectives in machine learning are finite sums: $\Psi(x) = \frac{1}{m}\sum_{i=1}^m f_i(x) + h(x)$, one smooth term $f_i$ per training example (or per worker, in a distributed setting), plus a simple nonsmooth regularizer $h$. Chapter 4's basic stochastic mirror descent handles this by sampling a single random component gradient $\nabla f_{i_t}(x)$ as an unbiased estimator of $\nabla f(x)$ — but that estimator's variance is a constant throughout the algorithm, which caps the achievable convergence rate. Variance-reduced mirror descent asks a sharper question: can an unbiased finite-sum gradient estimator be built whose variance itself vanishes as the algorithm approaches the optimum? The answer — periodic full-gradient snapshots combined with single-component corrections — is the SVRG-style idea this mission formalizes in Lan's general-norm mirror-descent framework, with an explicit, sampling-distribution-dependent constant rather than a generic $O(\cdot)$.

Setting

Fix a closed convex set $X$ in a real normed space $E$, and the finite-sum composite problem $\min_{x\in X}\{\Psi(x):=f(x)+h(x)\}$ (Eq. (5.3.1)), where $f(x)=\frac1m\sum_{i=1}^m f_i(x)$ is the average of $m$ smooth convex component functions, each with $L_i$-Lipschitz gradient $\nabla f_i$ ($\|\nabla f_i(x)-\nabla f_i(y)\|_*\le L_i\|x-y\|$), and $h$ is a simple, possibly nondifferentiable convex function. $f$ is possibly $\mu$-strongly convex, $\mu\ge0$ (Eq. (5.3.2)); this mission's goal takes $\mu=0$ (§5.3.1, "Smooth Problems Without Strong Convexity"). A fixed probability distribution $Q=\{q_1,\dots,q_m\}$ on the component indices governs the algorithm's random sampling, and

$$L_Q := \frac{1}{m}\max_{i=1,\dots,m}\frac{L_i}{q_i}$$

is the section's key aggregate smoothness constant (Eq. (5.3.4)), replacing the plain average $L$ wherever component-wise variance enters the analysis. Variance-reduced mirror descent (Algorithm 5.6) is a multi-epoch method: each epoch of length $T_s$ recomputes a full gradient $\nabla f(\tilde x)$ at a snapshot point $\tilde x$, then runs $T_s$ inner iterations using the estimator $G_t := \big(\nabla f_{i_t}(x_t)-\nabla f_{i_t}(\tilde x)\big)/(q_{i_t}m) + \nabla f(\tilde x)$ and the mirror-descent-with-composite-term update $x_{t+1}:=\arg\min_{x\in X}\{\gamma[\langle G_t,x\rangle+h(x)]+V(x_t,x)\}$, where $V$ is the Bregman divergence of a fixed distance-generating function, exactly as in Chapters 3-4.

Formalization targets

Goal — Corollary 5.8

With $\theta=1$, $\gamma=1/(16L_Q)$, and the doubling epoch schedule $T_1=7$, $T_s=2T_{s-1}$ (Eq. (5.3.17)),

$$\mathbb E[\Psi(\bar x_S)-\Psi(x^*)] \le \frac{8}{2^{S-1}}\left[\frac{11}{4}\big(\Psi(x_0)-\Psi(x^*)\big)+16L_Q\,V(x_0,x^*)\right]$$

for every epoch count $S\ge1$, where $\bar x_S$ is the weighted average of the epoch snapshots (Eq. (5.3.16)).

Supporting milestones, in attack order

• Lemma 5.12 — the per-component gradient-variation bound $\frac1m\sum_i\frac1{mq_i}\|\nabla f_i(x)-\nabla f_i(x^*)\|_*^2 \le 2L_Q[\Psi(x)-\Psi(x^*)]$, the basic smoothness consequence from which the estimator's variance bound is built.
• Lemma 5.13 — unbiasedness ($\mathbb E[\delta_t]=0$) and two variance bounds ($\mathbb E[\|\delta_t\|_*^2]\le 2L_Q[\dots]$ and $\le 4L_Q[\dots]$) for the variance-reduced estimator's error $\delta_t:=G_t-\nabla f(x_t)$.
• Lemma 5.14 — the one-step progress bound combining Lemma 5.13's variance control with the mirror-descent update's three-point inequality.
• Theorem 5.6 — the general epoch-level convergence bound (with an arbitrary epoch-length schedule $T_s$ and stepsize $\gamma$ satisfying $4L_Q\gamma\le1$) that Corollary 5.8 instantiates.

Every constant is exactly the book's: $L_Q$'s own sampling-distribution-dependent definition (never specialized to uniform $q_i=1/m$), and Corollary 5.8's explicit $8/2^{S-1}$, $11/4$, $16L_Q$ — not a generic $O(\cdot)$ — are all taken verbatim.

Significance

This is the series' first genuinely finite-sum result: unlike Chapters 3-4's single abstract objective $f$, here $f$ is structurally a named average of $m$ component functions, and the sampling distribution $\{q_i\}$ over those components is a first-class free parameter of both the algorithm and the analysis (not fixed to uniform sampling) — $L_Q$ itself depends on this choice, and a formalization that hard-codes $q_i=1/m$ would understate what Lemma 5.12's own proof needs. Getting Theorem 5.6/Corollary 5.8 right also requires keeping two nested indices straight: inner iterations $t$ within an epoch, and outer epoch counts $s$, with the convergence bound stated in terms of the epoch count $S$ alone — and keeping the two "gap" quantities $\Psi(x_0)-\Psi(x^*)$ (an objective-value gap) and $V(x_0,x^*)$ (a Bregman-divergence gap) distinct throughout, since they enter Corollary 5.8's final bound with different explicit coefficients ($11/4$ vs. $16L_Q$) and neither generically bounds the other.

No result on the platform models a finite-sum objective with $m$ named component functions sampled by a general index distribution $\{q_i\}$, a variance-reduction snapshot/anchor point, or this specific SVRG-style estimator, as of 2026-09-18 (q=finite sum, q=variance reduction, q=SVRG, q=component function, q=variance reduced gradient, q=mirror descent finite sum — see Prior art below).

Difficulty

The central difficulty is Theorem 5.6's own epoch-weight sequence $w_s$: the book defines $w_s:=(1-4L_Q\gamma)(T_{s-1}-1)-4L_Q\gamma T_s$ explicitly only for $s\ge2$ (Eq. (5.3.14)), yet the displayed sums $\sum_{s=1}^S w_s$ in (5.3.15)-(5.3.16) run from $s=1$. A 2026-09-19 revision found that this, combined with the epoch snapshot $\tilde x_s$ being constrained only by membership in $X$ and not tied to the algorithm's own dynamics, made the originally drafted statements false, not merely incomplete: an adversarial, unboundedly-large-$\Psi$, $\omega$-independent $\tilde x_1$ together with $w_1\to\infty$ violates the stated conclusion. The fix restores the connection via an auxiliary epoch-boundary sequence and the per-epoch progress inequality Theorem 5.6's own proof derives from Lemma 5.14 (see epoch_convergence_bound's hepoch hypothesis), and resolves $w_1$ by extending (5.3.14)'s domain to $s\ge1$ via a fixed "epoch 0" length $T_0$ — w_1 is no longer left free beyond positivity. finite_sum_variance_reduced_rate instantiates $T_0:=T_1/2=3.5$ concretely, reproducing the arithmetic Corollary 5.8's own proof is internally consistent with ($w_1 = 3/4(3.5-1)-1/4\cdot7 = 1/8$, matching the closed form $(1/8)T_1-3/4=1/8$) — this was previously only a documented-but-unresolved observation, not yet a stated hypothesis.

Formalization scope

All five items are stated over a general real normed space [NormedAddCommGroup E] [NormedSpace ℝ E], matching the mirror-descent chunks' general-norm convention (never specialized to Euclidean space or squared distance) — $V$ is a free two-point function throughout, and each $\nabla f_i$, $\nabla f$, $G_t$ are continuous linear functionals E →L[ℝ] ℝ, whose Mathlib operator norm supplies the dual norm $\|\cdot\|_*$ with no separate definition needed. This is the trivializing formalization this mission rules out: hard-coding $q_i=1/m$ (uniform sampling) or $V(x,y)=\frac12 \|x-y\|^2$ (Euclidean Bregman divergence) would understate both $L_Q$'s dependence on the sampling distribution (the whole point of Lemma 5.12's bound) and the general-norm apparatus the rest of this book series shares.

Ψ(x_0)-Ψ(x^*) and V(x_0,x^*) are kept as two syntactically distinct terms throughout — never conflated or bounded one by the other — matching Corollary 5.8's own two separate coefficients. Corollary 5.8's own explicit constants ($8/2^{S-1}$, $11/4$, $16L_Q$) are stated verbatim rather than left as an unspecified $O(\cdot)$, per Hard Rule 6.

Left out of scope, for time: the gradient-computation-count complexity bound (Eq. (5.3.19), an $O(\cdot)$ statement about total oracle calls, not a convergence-rate inequality on $\Psi$) and §5.3.2's strongly-convex case (Theorem 5.7, a geometric-decay bound $\Delta_s\le\rho\Delta_{s-1}$ under $\mu>0$) are natural continuations reusing this mission's variance_reduced_progress_bound milestone, not attempted here.

Prior art

q=finite sum, q=variance reduction, q=SVRG, q=component function, q=variance reduced gradient, and q=mirror descent finite sum were all searched on 2026-09-18. The only topically-adjacent hit across all six queries is ShiOptRates.Stochastic.variance_purchase_ classical ("Classical variance reduction is cost-neutral..."), which models plain minibatch SGD on a smooth objective with an i.i.d.-noise oracle characterized by a single scalar variance $\hat\sigma^2$ and a minibatch-size trade-off — no finite-sum structure with $m$ named component functions, no sampling distribution $\{q_i\}$, no snapshot/anchor point $\tilde x$, and a different question (cost-neutrality of minibatch size vs. this mission's convergence rate for a fixed variance-reduction scheme). Not reused; every item in this mission is drafted fresh.

Selected references

• G. Lan, First-Order and Stochastic Optimization Methods for Machine Learning, Springer Series in the Data Sciences, Springer 2020, Chapter 5, §5.3. https://doi.org/10.1007/978-3-030-39568-1
• R. Johnson, T. Zhang, "Accelerating stochastic gradient descent using predictive variance reduction," Advances in Neural Information Processing Systems (NeurIPS), 2013 (the SVRG estimator this section's gradient estimator generalizes to the composite mirror-descent setting).
• A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, "Robust stochastic approximation approach to stochastic programming," SIAM Journal on Optimization, 19(4), 2009, pp. 1574-1609.