All missions

Motivation

Principal component analysis (PCA) is one of the oldest and most widely used tools in multivariate statistics: given data with covariance matrix $\Sigma$, project onto the top eigenvector(s) of $\Sigma$ to find the directions of maximal variance. In practice one never observes $\Sigma$ itself, only a perturbed version — a sample covariance matrix $\hat\Sigma = \Sigma + P$, with $P$ the (random) estimation error. The natural question, asked since at least Davis and Kahan (1970) and Wedin (1972), is: how close is the top eigenvector of $\hat\Sigma$ to that of $\Sigma$? Wainwright's High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 8, gives a self-contained, sharp, non-asymptotic answer, phrased entirely in terms of two deterministic quantities: the eigengap of $\Sigma$, and a single scalar summarizing how the perturbation $P$ couples to the top eigendirection.

Unlike most of the results in this book series, this one is a statement of pure linear algebra: no probability, no concentration inequality, no sample size is needed to state or prove it. Randomness enters only afterward, when $P$ is instantiated as an actual sampling error and bounded using the machinery of earlier chapters (Corollary 8.7, out of this mission's scope).

Setting

Let $\Sigma \in \mathbb R^{d\times d}$ be a symmetric positive semidefinite matrix. Say $\theta \in \mathbb R^d$ is a maximal unit eigenvector of $\Sigma$ if $\|\theta\|_2=1$ and $\theta$ maximizes the Rayleigh quotient $\langle\theta,\Sigma\theta\rangle$ over the whole unit sphere $\mathcal S^{d-1}$ — the variational characterization of the top eigenvector/eigenvalue pair, matching Eq. (8.14) of the book. Write $\gamma_1(\Sigma) := \langle\theta^*,\Sigma\theta^*\rangle$ for the corresponding top eigenvalue. Say $\Sigma$ has eigengap $\nu>0$ at $\theta^*$ if every unit vector $v$ orthogonal to $\theta^*$ satisfies $\langle v,\Sigma v\rangle \le \gamma_1(\Sigma) - \nu$ — the Courant-Fischer variational form of the book's $\nu := \gamma_1(\Sigma)-\gamma_2(\Sigma)$.

For a symmetric perturbation matrix $P \in \mathbb R^{d\times d}$, write $|\!|\!|P|\!|\!|_2 := \sup_{\|v\|_2=1}|\langle v,Pv\rangle|$ for its $\ell_2$-operator norm, and

$$\tilde p \;:=\; P\theta^* - \langle P\theta^*,\theta^*\rangle\,\theta^*$$

for the component of $P\theta^*$ orthogonal to $\theta^*$ — the piece of the perturbation that actually couples the top eigendirection to the rest of the space (Eq. (8.11)). Note $\|\tilde p\|_2$ can be far smaller than $|\!|\!|P|\!|\!|_2$: a perturbation can be large in every direction yet barely move the top eigenvector, if its interaction with $\theta^*$ specifically is small.

Formalization targets

Goal (Theorem 8.5)

Let $\Sigma$ be symmetric positive semidefinite with maximal unit eigenvector $\theta^*$ and eigengap $\nu>0$. For any symmetric $P$ with $|\!|\!|P|\!|\!|_2 < \nu/2$, and any maximal unit eigenvector $\hat\theta$ of $\hat\Sigma := \Sigma+P$ with $\langle\hat\theta,\theta^*\rangle \ge 0$,

$$\|\hat\theta - \theta^*\|_2 \;\le\; \frac{2\|\tilde p\|_2}{\nu - 2|\!|\!|P|\!|\!|_2}.$$

Milestone (Lemma 8.6, the PCA basic inequality)

Under the same eigengap hypothesis, with $\Psi(\Delta;P) := \langle\Delta,P\Delta\rangle

• 2\langle\Delta,P\theta^\rangle$and$\Delta := \hat\theta-\theta^$,

$$\nu\bigl(1-\langle\hat\theta,\theta^*\rangle^2\bigr) \;\le\; |\Psi(\Delta;P)|.$$

Significance

The bound isolates exactly what drives eigenvector instability: not the raw size of the perturbation but its projection onto the top eigendirection, rescaled by the inverse eigengap. This explains, in one inequality, the qualitative phenomenon Example 8.4 illustrates numerically (a tiny perturbation can move the eigenvector far when the eigengap is small) and quantifies exactly how far. It is the deterministic engine behind every consistency result for PCA in the rest of the chapter: Corollary 8.7 (rates for the spiked covariance model) and the sparse-PCA guarantee (Theorem 8.10) both specialize this same bound, after bounding $\|\tilde p\|_2$ and $|\!|\!|P|\!|\!|_2$ using concentration for a specific random design. It is also a sharp instance of the general Davis-Kahan-type perturbation theory for symmetric matrices, phrased with an explicit, non-asymptotic constant rather than an $O(\cdot)$.

The theorem is already proved in the source; this mission's contribution is a machine-checked formal statement (and, eventually, proof) of the bound and its supporting basic inequality, composing with any future formalization of the chapter's probabilistic corollaries.

Difficulty

The proof is genuinely variational, not spectral: it never diagonalizes $\Sigma$ or $\hat\Sigma$, only uses that $\theta^*$ and $\hat\theta$ are optimal for their respective Rayleigh-quotient maximizations. The one place a naive argument fails is in bounding $|\Psi(\Delta;P)|$ itself (the proof of Lemma 8.6): a direct Cauchy-Schwarz bound on $\langle\Delta,P\Delta\rangle$ using $|\!|\!|P|\!|\!|_2$ alone would produce a bound in terms of $|\!|\!|P|\!|\!|_2$ throughout, not the sharper $\|\tilde p\|_2$ the theorem actually delivers; getting the sharper dependence requires decomposing $\Delta$ along $\theta^*$ and its orthogonal complement and tracking the two pieces separately (the $\varrho$, $z$ decomposition on p. 244). The sharpness of the threshold $|\!|\!|P|\!|\!|_2 < \nu/2$ is also not a proof artifact: the book's own $2\times 2$ example ($\Sigma=\mathrm{diag}(2,1)$, $P=\mathrm{diag}(-1/2,1/2)$) shows the perturbed matrix can lose a unique maximal eigenvector exactly at $|\!|\!|P|\!|\!|_2 = \nu/2$.

Formalization scope

$\Sigma$, $P$, $\hat\Sigma=\Sigma+P$ are Matrix (Fin d) (Fin d) ℝ; "symmetric" is M.transpose = M; "positive semidefinite" is the quadratic-form condition $\langle v, \Sigma v\rangle \ge 0$ for all $v$, stated directly rather than via a Mathlib PosSemidef typeclass. "Maximal unit eigenvector" and "eigengap" are both given their variational (Rayleigh-quotient) characterizations rather than defined through Mathlib's enumerated matrix-eigenvalue API — mathematically equivalent to the book's spectral definitions by the Courant-Fischer theorem, and the same characterization the book's own proof works with throughout (Eq. (8.14)). The operator norm $|\!|\!|\cdot|\!|\!|_2$ is likewise realized variationally, valid because this mission only ever applies it to symmetric matrices, exactly as the book does in this chapter. $\tilde p$ is realized as a basis-independent vector in $\mathbb R^d$ (the component of $P\theta^*$ orthogonal to $\theta^*$) rather than the book's basis-dependent $\mathbb R^{d-1}$ representative; its $\ell_2$-norm — the only quantity the theorem's conclusion uses — is identical either way.

Deliberate scope decision, disclosed here rather than silently: the book's own Theorem 8.5 concludes that $\hat\Sigma$ "has a unique maximal eigenvector $\hat\theta$" satisfying the bound — asserting both existence and uniqueness as part of the theorem, on top of the quantitative bound. This mission formalizes only the quantitative bound, for an arbitrary maximal unit eigenvector $\hat\theta$ of $\hat\Sigma$ satisfying the sign condition $\langle\hat\theta,\theta^*\rangle\ge0$ — exactly what the book's own proof establishes (the proof never separately argues existence or uniqueness; both are consequences that could be derived from the bound together with a compactness argument for existence, left to a future extension) and exactly what every downstream use in the chapter (Examples, Corollary 8.7) actually invokes. A trivializing formalization would instead drop the sharp threshold $|\!|\!|P|\!|\!|_2 < \nu/2$ to ≤, or conflate the general operator norm with the symmetric-matrix Rayleigh-quotient characterization for a non-symmetric $P$; this mission does neither. Corollary 8.7 (spiked covariance rates) and Theorem 8.10 (sparse PCA, needing the uniform deviation condition of Eq. (8.26)) are out of this mission's scope; a companion mission formalizing them on top of this one's pca_eigenvector_perturbation_bound is natural future work, together with a proof of existence of a maximal unit eigenvector via compactness of the sphere.

Selected references

• Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 8. DOI: 10.1017/9781108627771.
• Davis, C., Kahan, W. M. "The rotation of eigenvectors by a perturbation. III." SIAM Journal on Numerical Analysis, 7(1), 1970, 1–46.
• Wedin, P.-Å. "Perturbation bounds in connection with singular value decomposition." BIT Numerical Mathematics, 12(1), 1972, 99–111.

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

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

Formalization targets

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

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

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

Selected references

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

Motivation

Support vector machines (SVMs) are trained by solving a regularized empirical risk minimization problem over a reproducing kernel Hilbert space (RKHS) — a space that is typically infinite-dimensional. On its face, this looks computationally hopeless: how can a computer search an infinite-dimensional space for a minimizer? The representer theorem is the result that makes SVM training tractable at all: it shows that no matter how large the RKHS is, the minimizer of the SVM objective for a sample of size $n$ always lies in the $n$-dimensional subspace spanned by the kernel evaluated at the $n$ sample points. This turns an infinite- dimensional optimization problem into a finite-dimensional one before a single line of an optimization algorithm is written, and it is the reason every practical SVM solver (from the original sequential minimal optimization algorithm onward) searches only over $n$ coefficients rather than over an abstract function space.

The theorem in this mission — Theorem 5.5 of Steinwart and Christmann, Support Vector Machines (Springer, 2008) — is stated for general convex losses and general kernels, subsuming the classification-SVM and regression-SVM special cases that appear throughout the machine learning literature. Its lineage traces to Kimeldorf and Wahba's 1971 representer theorem for spline-smoothing problems; the book's own version (attributed to a 1971 result, generalized here to arbitrary convex losses and RKHSs) is the general form used throughout the rest of the book.

Setting

Fix a nonempty set $X$ (the input space) and a loss function $L : X \times \mathbb R \times \mathbb R \to [0,\infty)$: a measurable map where $L(x,y,t)$ is the cost of predicting label $y$ by value $t$ when the input is $x$. $L$ is convex if $L(x,y,\cdot)$ is convex for every fixed $x,y$.

A reproducing kernel Hilbert space (RKHS) over $X$ is a real Hilbert space $H$ of real-valued functions on $X$ that carries a kernel $k : X \times X \to \mathbb R$ with two properties: $k(\cdot,x) \in H$ for every $x \in X$, and the reproducing property $f(x) = \langle f, k(\cdot,x)\rangle_H$ holds for every $f \in H$ and $x \in X$. Intuitively, $k$ lets you evaluate any $f \in H$ at a point $x$ by taking an inner product with the fixed function $k(\cdot,x)$ — this is what makes $H$ a space of genuine, pointwise-evaluable functions rather than an abstract Hilbert space.

Given a finite sample $D := ((x_1,y_1),\dots,(x_n,y_n)) \in (X \times \mathbb R)^n$, the empirical $L$-risk of $f : X \to \mathbb R$ is $R_{L,D}(f) := \tfrac1n\sum_{i=1}^n L(x_i,y_i,f(x_i))$. For a regularization parameter $\lambda > 0$, the SVM training problem asks for a minimizer of the regularized empirical risk

$$f \mapsto \lambda\|f\|_H^2 + R_{L,D}(f)$$

over all of $H$. A minimizer of this objective is called an empirical SVM solution $f_{D,\lambda}$.

Formalization targets

Goal — Theorem 5.5 (Representer theorem)

$$\exists! \, f_{D,\lambda} \in H : \quad \lambda\|f_{D,\lambda}\|_H^2 + R_{L,D}(f_{D,\lambda}) = \min_{f \in H} \Bigl(\lambda\|f\|_H^2 + R_{L,D}(f)\Bigr), \qquad f_{D,\lambda}(x) = \sum_{i=1}^n \alpha_i\, k(x,x_i) \; \text{ for some } \alpha_1,\dots,\alpha_n \in \mathbb R.$$

The theorem asserts both halves at once: the regularized empirical risk has a unique minimizer over the (possibly infinite-dimensional) $H$, and that unique minimizer is representable as a finite linear combination of the kernel functions at the sample points. Neither the coefficients $\alpha_i$ nor the finite-dimensional subspace they live in are fixed in advance by the statement; only their existence is asserted, so a stronger claim (e.g. uniqueness or an explicit formula for the $\alpha_i$) would be a different, harder theorem not proved here.

Supporting milestones (the general, population-level analogue)

The book develops the representer theorem's existence-and-uniqueness clause by first proving it for the corresponding population problem — minimizing $f \mapsto \lambda\|f\|_H^2 + R_{L,P}(f)$ over a distribution $P$ rather than a finite sample — and then adapting the same two arguments to the empirical case:

• Lemma 5.1 (uniqueness): for a convex loss and an RKHS $H$ with $R_{L,P}(f) < \infty$ for some $f \in H$, the regularized population risk has at most one minimizer over $H$, for every $\lambda > 0$.
• Theorem 5.2 (existence): for a convex, $P$-integrable Nemitski loss and the RKHS of a bounded kernel, the regularized population risk has at least one minimizer, for every $\lambda > 0$.
• Theorem 5.6 (non-triviality): under the same hypotheses as Theorem 5.2, if $H$ can beat the risk of the zero function ($\inf_{f \in H} R_{L,P}(f) < R_{L,P}(0)$), then every minimizer is nonzero, for every $\lambda > 0$.

Significance

The representer theorem is the single fact that turns kernel-based learning from a theoretical curiosity into a practical algorithm family: every popular SVM solver (SMO, coordinate descent, interior-point methods for the dual) is, at bottom, a method for finding the $n$ coefficients $\alpha_1,\dots,\alpha_n$ the theorem guarantees exist, not for searching $H$ directly. The representation also underlies the "kernel trick": since the objective and the solution both depend on $H$ only through inner products $\langle k(\cdot,x_i), k(\cdot,x_j)\rangle_H = k(x_i,x_j)$, an SVM can be trained and evaluated without ever computing with elements of $H$ explicitly, using only the $n \times n$ Gram matrix of kernel values.

Formalizing this theorem means formalizing the existence-and-uniqueness argument (Lemma 5.1's strict-convexity computation for the midpoint of two hypothetical minimizers, together with the weak-compactness argument used for existence) and the orthogonal-projection argument for the representation clause (projecting any candidate minimizer onto the finite-dimensional span of the kernel functions at the sample points strictly improves — or leaves unchanged — both the norm term and the risk term, so an optimal solution can always be chosen inside that span). No part of this argument has a machine-checked Lean proof in Mathlib or elsewhere at the time of writing; only the underlying general-purpose tools (Hilbert-space projections, convexity of norms) are already in Mathlib.

Difficulty

The natural first idea for the representation clause is to try to exhibit the coefficients $\alpha_i$ directly, e.g. by writing down the dual optimization problem and reading off its KKT multipliers. This is exactly backwards: the book's proof (and any faithful one) derives the representation before knowing anything about a dual problem, purely from the orthogonal decomposition $H = H|_{X'} \oplus H|_{X'}^\perp$ of $H$ into the span $H|_{X'}$ of the sample's kernel functions and its orthogonal complement. The key insight — one that a solver who reaches for duality first will miss — is that projecting any $f \in H$ onto $H|_{X'}$ leaves the empirical risk exactly unchanged (since $R_{L,D}$ only sees $f$'s values at the sample points, and the reproducing property shows those values are unaffected by throwing away the $H|_{X'}^\perp$ component) while weakly decreasing the norm term, so the infimum over all of $H$ is already attained inside the finite-dimensional $H|_{X'}$.

For the existence-and-uniqueness clause, the difficulty is genuinely functional-analytic rather than algorithmic: existence needs a compactness argument in a space with no compact balls (Theorem 5.2 gets around this via lower semicontinuity and boundedness of the sublevel set, not via any finite-dimensional trick), and uniqueness needs the parallelogram-law strict convexity of the Hilbert norm, not merely convexity of the loss.

Formalization scope

$H$ is represented as an arbitrary real Hilbert space together with an injective linear evaluation map into $X \to \mathbb R$ (so that $H$ is genuinely realized as a space of functions, not an abstract Hilbert space with no relation to $X$), and a kernel $k$ satisfying the reproducing property with respect to that evaluation map (IsRKHSOfKernel). This is an equivalent, operative rendering of "$H$ is the RKHS of the kernel $k$" (Definition 4.18 together with Lemma 4.19 of the book), chosen because it is exactly the form the chapter's own proofs use; it is restated inside this chunk's own InfiniteSample sub-namespace rather than imported from the Kernels chapter's mission, since drafts in this series cannot import one another.

The population risk $R_{L,P}$ is formalized as a lower Lebesgue integral into $[0,\infty]$ (ENNReal), which is always well-defined for a nonnegative integrand with no integrability hypothesis — matching the book's own remark that "the integral always exists, although it is not necessarily finite." The empirical risk $R_{L,D}$, by contrast, is a manifestly finite average over the $n$ sample points and is formalized as an ordinary real number. The sample size $n$ is required positive ($n \ge 1$), matching the book's implicit convention that the empirical measure $\bar D := \tfrac1n\sum_i \delta_{(x_i,y_i)}$ presupposes a nonempty sample.

A trivializing formalization of the representer theorem would state only the representation clause $f_{D,\lambda}(x) = \sum_i \alpha_i k(x,x_i)$ while assuming the existence of "the" solution $f_{D,\lambda}$ as a hypothesis; this begs the question, since the book's own proof establishes existence and uniqueness as part of the theorem, not as a standing assumption. This mission's goal keeps both clauses bundled into one ∃! statement for exactly this reason.

The infrastructure needed — a general convex loss, a Nemitski-loss integrability condition, and the RKHS/reproducing-kernel bundle — is restated locally here and is reusable, with the same caveat about not being importable across this series' independently drafted chapters, by any later mission (e.g. this book's own Chapters 6, 8 and 9) that needs the same objects. Contributed proofs are welcome for either the existence/uniqueness argument (Lemma 5.1/Theorem 5.2's techniques) or the orthogonal-projection representation argument; the two are largely independent and could be solved separately.

Selected references

• I. Steinwart and A. Christmann, Support Vector Machines, Springer Series in Information Science and Statistics, Springer, 2008. https://doi.org/10.1007/978-0-387-77242-4
• G. Kimeldorf and G. Wahba, "Some results on Tchebycheffian spline functions," Journal of Mathematical Analysis and Applications, 33(1):82–95, 1971. https://doi.org/10.1016/0022-247X(71)90184-3
• B. Schölkopf, R. Herbrich, and A. J. Smola, "A generalized representer theorem," in Computational Learning Theory (COLT 2001), Lecture Notes in Computer Science, vol. 2111, Springer, 2001, pp. 416–426. https://doi.org/10.1007/3-540-44581-1_27

Comparing distributions by their Laplace transforms

Many of the orders in Shaked and Shanthikumar's Stochastic Orders (Springer, 2007) are built by fixing a class of test functions $\varphi$ and declaring $X \le Y$ whenever $E[\varphi(X)] \le E[\varphi(Y)]$ for every $\varphi$ in that class: all increasing functions give the usual stochastic order, all convex functions give the convex order. This mission formalizes the order obtained from the single function $\varphi_s(x) = -e^{-sx}$, $s > 0$ — the Laplace transform order — together with its principal alternative characterization and three of its closure properties. Unlike almost every other order in the book, this one has essentially no dependence on material from earlier chapters, which is why it is a natural standalone mission.

The Laplace transform order

Let $X$ be a real-valued random variable on a probability space $(\Omega,\mu)$, and let $Y$ be a real-valued random variable on a (possibly different) probability space $(\Omega',\nu)$. $X$ is smaller than $Y$ in the Laplace transform order, written $X \le_{Lt} Y$, if

$$E[e^{-sX}] \ge E[e^{-sY}] \quad \text{for every } s > 0.$$

The order is meant for nonnegative random variables: the book's own standing convention for the whole of §5.A is that every random variable mentioned is nonnegative, since otherwise $E[e^{-sX}]$ need not even be finite. Every theorem below carries that hypothesis explicitly rather than folding it into the order's own definition, so the definition itself is stated exactly as broadly as the book's raw equation (5.A.1) is — a comparison of two expectations, for two random variables that need not share a probability space, since $\le_{Lt}$ is a comparison of distributions.

A second definition supports one of the milestones: a function $\varphi : [0,\infty) \to \mathbb{R}$ is completely monotone if all its derivatives exist and $(-1)^n\varphi^{(n)}(x) \ge 0$ for every $x > 0$ and every $n = 0, 1, 2, \dots$. Every $\varphi_s(x) = e^{-sx}$, $s > 0$, is completely monotone, which is what connects the raw definition of $\le_{Lt}$ to its function-class characterization below.

Formalization targets

Goal: the integrated-survival-function characterization (Theorem 5.A.1)

$$X \le_{Lt} Y \iff \int_0^\infty e^{-sx}\bar F(x)\,dx \le \int_0^\infty e^{-sx}\bar G(x)\,dx \quad \text{for every } s > 0,$$

where $\bar F(x) = P\{X>x\}$ and $\bar G(x) = P\{Y>x\}$ are the survival functions of $X$ and $Y$. This is the book's principal restatement of the order, obtained from the identity $\int_0^\infty e^{-sx}\bar F(x)\,dx = s^{-1}(1-E[e^{-sX}])$: instead of comparing the raw Laplace transforms of $X$ and $Y$ themselves, it compares the Laplace transforms of their survival functions, weighted the same way. It is the natural goal for a standalone chapter mission: the chapter's own defining equation plus one elementary identity is exactly the book's own proof, and it is the form of the order that the chapter's closure properties are stated against.

Supporting milestones

• Eq. (5.A.5), the mean inequality: $X \le_{Lt} Y \implies E[X] \le E[Y]$, provided the expectations exist — obtained by dividing the defining inequality by $s$ and letting $s \downarrow 0$.
• Theorem 5.A.3, the function-class characterization: $X \le_{Lt} Y$ iff $E[\varphi(X)] \ge E[\varphi(Y)]$ for every completely monotone $\varphi$, provided the expectations exist — the order's analogue of "all increasing functions" for $\le_{st}$ or "all convex functions" for $\le_{cx}$.
• Theorem 5.A.7(a), closure under functions with a completely monotone derivative: $X \le_{Lt} Y$ and $g$ positive with $g'$ completely monotone gives $g(X) \le_{Lt} g(Y)$.
• Theorem 5.A.7(d), the convolution corollary: independent $X_i \le_{Lt} Y_i$, $i=1,\dots,m$, gives $\sum_i X_i \le_{Lt} \sum_i Y_i$.

Significance

The Laplace transform order is the natural comparison for nonnegative quantities that arise as sums or mixtures of exponential-type random variables — waiting times, workloads, service completion times — precisely because it is preserved under convolution (Theorem 5.A.7(d)) and under the broad class of transformations with a completely monotone derivative (Theorem 5.A.7(a)), which includes every concave power $x^p$, $0<p\le 1$. It sits strictly between the convex-type orders and weaker moment comparisons: Eq. (5.A.5) shows it implies ordered means, but (unlike $\le_{cx}$) it does not require equal means, and (unlike $\le_{icx}$) it is not implied by a pointwise comparison of integrated tails alone — it is its own, genuinely different order, useful whenever a modeler's comparison naturally arises through Laplace-transform (equivalently, moment-generating-function-at- negative-argument) calculations rather than through a coupling or a tail-probability argument. Theorem 5.A.3's function-class form is the bridge that lets the order be verified either way: by a single-parameter family of exponential test functions, or by the full class of completely monotone functions of which they are the extreme rays.

Difficulty

The chapter's own first warning applies directly: the order's every characterization requires $X,Y \ge 0$, and dropping that hypothesis anywhere — as opposed to carrying it explicitly on each theorem, per this mission's convention — would silently change which statements are even well-posed, since $E[e^{-sX}]$ can diverge for $X$ unbounded below. The quantifier "$\forall s > 0$" in both the raw definition and Theorem 5.A.1 ranges over the whole positive half-line, not a bounded or discretized set of test points; narrowing it would produce a strictly weaker order. In CompletelyMonotone, the phrase "all its derivatives exist" is a genuine hypothesis, not a formality: stating only the sign condition on iteratedDeriv n φ x without also requiring φ to be C^∞ would let the definition be satisfied vacuously wherever a derivative fails to exist (a classic junk-value trap), which is why the mission's definition bundles smoothness explicitly. Theorem 5.A.7(a)'s "$g$ positive" is a hypothesis on $g$'s values at the nonnegative reals that $X$ and $Y$ actually take, not on all of $\mathbb{R}$, and must not be silently strengthened to "$g$ everywhere positive" or weakened to "$g$ nonnegative" (which would let $g$ vanish and break the order's need for $e^{-sg(X)}$ to be well-behaved).

Formalization scope

LaplaceOrder μ ν X Y takes $X : \Omega \to \mathbb{R}$ on $(\Omega,\mu)$ and $Y : \Omega' \to \mathbb{R}$ on a separate $(\Omega',\nu)$, matching the series' convention (e.g. StochasticOrders.Usual.UsualOrder) that the order compares distributions, not jointly defined variables. Nonnegativity of $X$ and $Y$ is an explicit hypothesis ∀ ω, 0 ≤ X ω / ∀ ω, 0 ≤ Y ω on every theorem, never built into LaplaceOrder itself. CompletelyMonotone φ is ContDiff ℝ ⊤ φ ∧ ∀ n x, 0 < x → 0 ≤ (-1)^n * iteratedDeriv n φ x — the smoothness conjunct guards the junk-value trap described above. The survival function $\bar F(x) = P\{X>x\}$ in the goal theorem is formalized inline as (μ {ω | x < X ω}).toReal, valid since μ is a probability measure (so the underlying ENNReal value is finite and the conversion to ℝ loses no information); the integral $\int_0^\infty$ is Bochner integration over Set.Ici (0 : ℝ). "Provided the expectations exist" becomes explicit Integrable hypotheses per statement (on $X$, $Y$ themselves for Eq. 5.A.5; on $\varphi \circ X$, $\varphi \circ Y$ for each $\varphi$ in Theorem 5.A.3), rather than a blanket integrability assumption that would understate which expectations the book actually needs. Independence in the convolution corollary is ProbabilityTheory.iIndepFun, one family per side, as in Chunk 01's own convolution corollary. A trivializing formalization is ruled out: $\le_{Lt}$ is not restated as a comparison of one moment or of the raw random variables' means, and the "universal function class" of Theorem 5.A.3 is exactly the completely monotone functions the book names, not a fixed finite subfamily or a narrowed subclass (e.g. only the exponentials themselves, which would make Theorem 5.A.3 a restatement of the definition rather than its own theorem).

This mission draws on no platform prior art: repeated searches for "Laplace transform" and "completely monotone" during this session return only unrelated analytic-number-theory formalizations (a Langlands–Tunnell Laplace–Mellin transform identity) and no hits at all, respectively — confirming BRIEF.md's expectation that this subarea is untouched on the platform. It is one of nine missions in a series covering the whole book; per the series' own convention, its definitions are not imported by any other chapter's mission, and it does not import any other chapter's definitions in turn (the chapter itself has essentially no cross-chapter dependence, the reason it was flagged as the series' most self-contained chunk).

Selected references

• M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

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

The support vector machine and every other kernel method (Gaussian processes, kernel ridge regression, kernel PCA) is specified by choosing a kernel: a function $k(x,x')$ measuring similarity between two inputs, used in place of an inner product on the raw data. This lets a linear algorithm implicitly work in a very high- or infinite-dimensional feature space without ever computing a feature vector explicitly (the "kernel trick"). The definition of a kernel most directly tied to this trick — $k(x,x') = \langle \Phi(x),\Phi(x')\rangle$ for some feature map $\Phi$ into a Hilbert space — is exactly the definition that makes verifying a candidate similarity function is a valid kernel hard: it asks for an explicit Hilbert space and map that in practice nobody wants to construct by hand.

Schoenberg's theorem (1938, for a special class of functions on the sphere) and the general theory developed by Aronszajn and others through the mid-20th century established the alternative used ever since: a function is a kernel exactly when it is symmetric and positive definite, a checkable condition on finite point sets alone. Steinwart & Christmann, Support Vector Machines (Springer 2008, Information Science and Statistics), Theorem 4.16 gives the modern, self-contained real-Hilbert-space proof of this equivalence, and it is the theorem every later construction in the book's kernel chapter (sums, products, limits, and the specific kernel families used in practice) rests on.

Setting

Fix a non-empty set $X$ (the input space; no further structure is assumed). A function $k : X \times X \to \mathbb R$ is a kernel on $X$ if there exist a real Hilbert space $H$ and a feature map $\Phi : X \to H$ such that

$$k(x,x') = \langle \Phi(x), \Phi(x') \rangle_H \qquad \text{for all } x, x' \in X.$$

Neither $H$ nor $\Phi$ are determined by $k$: for $X = \mathbb R$, $k(x,x') := xx'$ admits both the identity map on $\mathbb R$ and $\Phi(x) := (x/\sqrt2, x/\sqrt2) \in \mathbb R^2$ as feature maps.

Separately, $k$ is symmetric if $k(x,x') = k(x',x)$ for all $x,x'$, and positive definite if, for every $n \in \mathbb N$, every $\alpha_1,\dots,\alpha_n \in \mathbb R$, and every $x_1,\dots,x_n \in X$,

$$\sum_{i=1}^n \sum_{j=1}^n \alpha_i \alpha_j\, k(x_j,x_i) \ge 0,$$

equivalently: the $n \times n$ Gram matrix $(k(x_j,x_i))_{i,j}$ is positive semidefinite for every finite point set. This condition mentions only $X$, $\mathbb R$, and finite sums — no Hilbert space at all.

Formalization targets

Goal: Theorem 4.16

$$k \text{ is a kernel on } X \iff k \text{ is symmetric and positive definite.}$$

The forward direction is elementary (a two-line computation from the feature-map definition, recorded in the book just before the theorem statement). The goal is the full equivalence, including the converse: a symmetric, positive definite function, given with no reference to any ambient Hilbert space at all, is nonetheless a kernel.

Supporting facts: Lemma 4.5 and Corollary 4.17

$$k, k_1, k_2 \text{ kernels},\ \alpha \ge 0 \implies \alpha k,\ k_1 + k_2 \text{ are kernels (Lemma 4.5)},$$ $$k_n \to k \text{ pointwise},\ \text{each } k_n \text{ a kernel} \implies k \text{ is a kernel (Corollary 4.17)}.$$

Neither is a hypothesis Theorem 4.16's own proof consumes; both are included as further chapter results built on the same two definitions, chosen because they are the tools the book uses immediately afterward to construct concrete kernels (polynomial kernels, kernels given by convergent power series) without exhibiting a feature map for each one by hand, and because Corollary 4.17's one-line proof ("every $k_n$ is symmetric and satisfies (4.5); therefore so is the pointwise limit $k$") only makes sense once Theorem 4.16 is available as the bridge back to "is a kernel".

Significance

Theorem 4.16 is the single result that turns "is a kernel" from an existential, non-constructive question (does some Hilbert space and feature map exist?) into a universal, checkable one (does a finite-dimensional matrix inequality hold for every finite point set?). Every kernel actually used in the book from this point on — polynomial kernels, the Gaussian RBF kernel, kernels built from Taylor or Fourier series — is verified to be a kernel via this characterization, not by exhibiting a feature map directly (an infinite-dimensional one, in most of these cases). Lemma 4.5 and Corollary 4.17 are the two closure properties that make positive-definiteness verification compositional: a new kernel is usually built as a sum, nonnegative multiple, product, or limit of kernels already known to be positive definite, rather than checked from scratch.

The result itself is classical (Schoenberg 1938 for the special case relevant to distance-based kernels on spheres; the general Hilbert-space statement is standard by the mid-20th century, see Aronszajn 1950's RKHS paper and Berg–Christensen–Ressel's monograph). No machine-checked Lean proof of this specific real-Hilbert-space equivalence is known to exist on the platform at the time of writing (see prior-art search below); this mission asks for its formalization exactly as the book states and proves it, via the explicit pre-Hilbert-space-of-finite-combinations construction rather than any other known proof of the same fact (e.g. via Riesz representation).

Difficulty

The forward direction (kernel $\Rightarrow$ symmetric and positive definite) is immediate once a feature map is given. The converse is not: starting from only the two finite, algebraic conditions, the proof must manufacture a Hilbert space and a feature map out of nothing but $k$ and $X$. The book's construction — the space $H_{\mathrm{pre}}$ of finite linear combinations $\sum_i \alpha_i k(\cdot,x_i)$, with inner product $\langle f,g\rangle := \sum_{i,j} \alpha_i\beta_j k(x_j',x_i)$ — requires checking, in order, that this inner product is well-defined independently of how $f$ and $g$ are represented as such combinations (using the reproducing-type identity $\langle f,g\rangle = \sum_j \beta_j f(x_j')$), that it is positive definite as an actual inner product (not just on the Gram-matrix diagonal, i.e. $\langle f,f \rangle = 0 \Rightarrow f = 0$ as a function, which uses a Cauchy–Schwarz argument on $H_{\mathrm{pre}}$ itself before $H_{\mathrm{pre}}$ is known to be an inner product space), and only then completing $H_{\mathrm{pre}}$ to an honest Hilbert space. Each of these three steps individually looks routine, but the middle one is circular-looking on a first reading (using an inner-product inequality to prove the pairing is an inner product) and is the step every attempted shortcut skips.

Formalization scope

$X$ is an arbitrary non-empty type (Nonempty X), matching Definition 4.1's own standing hypothesis; no additional topological or measurable structure is imposed, since none is used by either the definitions or Theorem 4.16's proof. IsKernel existentially quantifies over a Type Hilbert space (NormedAddCommGroup, real InnerProductSpace, CompleteSpace) and a feature map, matching Definition 4.1 specialized to the real field $\mathbb K = \mathbb R$; the complex case of Definition 4.1 is out of scope, since Theorem 4.16 itself is stated only for real-valued $k$. PositiveDefinite and Symmetric (Definition 4.15) quantify over an arbitrary finite family via Fin n → X / Fin n → ℝ for n : ℕ, exactly the book's "for all $n$, $\alpha_1,\dots,\alpha_n$, $x_1,\dots,x_n$".

A trivializing formalization would fix a specific small Hilbert space (e.g. $\mathbb R^d$ for a fixed $d$) in IsKernel's existential rather than an arbitrary one, which would make the "if" direction of Theorem 4.16 false in general (a positive definite kernel's minimal feature space can be infinite-dimensional) or silently restrict the theorem's scope; this is ruled out here by existentially quantifying over an unconstrained Hilbert space type.

IsKernel, Symmetric, and PositiveDefinite are reusable well beyond this mission: every later kernel construction in the book (polynomial kernels, Lemma 4.6's product kernels, the reproducing kernel Hilbert space of Section 4.2) is stated in terms of them. Completing the two milestone proofs and the goal's own sorry (the $H_{\mathrm{pre}}$ construction above) is welcome; a from-scratch formalization of Lemma 4.6 (products of kernels, needing the completed tensor product of two Hilbert spaces) or of the chapter's other named kernel families would be natural, faithful extensions of this mission but are out of scope for it.

Selected references

• I. Steinwart & A. Christmann, Support Vector Machines, Springer, Information Science and Statistics, 2008. https://doi.org/10.1007/978-0-387-77242-4 (Chapter 4, §4.1, pp. 111-119).
• N. Aronszajn, "Theory of Reproducing Kernels," Transactions of the American Mathematical Society 68(3), 1950, pp. 337-404. https://doi.org/10.2307/1990404
• I. J. Schoenberg, "Metric spaces and positive definite functions," Transactions of the American Mathematical Society 44(3), 1938, pp. 522-536. https://doi.org/10.2307/1989894
• C. Berg, J. P. R. Christensen & P. Ressel, Harmonic Analysis on Semigroups: Theory of Positive Definite and Related Functions, Springer GTM 100, 1984. https://doi.org/10.1007/978-1-4612-1128-0

Motivation

Support vector machines were, for two decades, the workhorse of applied classification, and the reason offered for their success was always geometric: SVMs maximize the margin between the two classes. Chapter 3's VC-dimension bound cannot explain why this should help — for linear hypotheses in $\mathbb R^N$ its bound depends on $N+1$ and is uninformative whenever the feature dimension is large relative to the sample size, exactly the regime (kernel-induced or high-dimensional features) where SVMs are most often used. Chapter 5 answers the question this leaves open: a generalization bound for a real-valued hypothesis, stated in terms of its margin on the training sample, that does not depend on the ambient dimension at all. This is also the template every later chapter's margin bound specializes (multi-class classification, ranking, and, indirectly, boosting all reuse the same Rademacher-complexity-of-a-Lipschitz-loss argument developed here).

Setting

A hypothesis here is a real-valued function $h:X\to\mathbb R$, not (as in Chapters 2-3) a function into $\{-1,+1\}$: for a labeled point $(x,y)$ with $y\in\{-1,+1\}$, the sign of $h(x)$ gives the prediction and $|h(x)|$ is read as the classifier's confidence. The confidence margin of $h$ at $(x,y)$ is $y\,h(x)$; it is positive exactly when $h$ classifies $x$ correctly. For $\rho>0$, the $\rho$-margin loss $\Phi_\rho:\mathbb R\to\mathbb R$ (Definition 5.5) is

$$\Phi_\rho(x) = \min\Big(1,\max\Big(0,1-\frac x\rho\Big)\Big),$$

equal to $1$ when $x\le 0$ (misclassified), $0$ when $x\ge\rho$ (classified with confidence at least $\rho$), and interpolating linearly in between; it is $1/\rho$-Lipschitz. The empirical margin loss on a sample $S=(x_1,\dots,x_m)$ with labels $y_1,\dots,y_m$ (Definition 5.6) is $\hat R_{S,\rho}(h) = \frac1m\sum_{i=1}^m\Phi_\rho(y_ih(x_i))$ — the fraction of training points misclassified or classified with confidence below $\rho$, a strictly stronger requirement than plain misclassification. The (population) generalization error is $R(h)=\Pr_{(x,y)\sim D}[y\,h(x)\le 0]$. Rademacher complexity, $\hat R_S(H)$ and $R_m(H)$ (Definitions 3.1-3.2, restated here since chunk 03-rademacher-vc's own copies are still drafts), measure how well a real-valued hypothesis class $H$ correlates with random sign noise on a sample, and are the vehicle through which the margin bound's complexity term is expressed.

Formalization targets

Lemma 5.7 (Talagrand's lemma, milestone). For $l$-Lipschitz $\Phi_1,\dots,\Phi_m:\mathbb R\to\mathbb R$ and any hypothesis set $H$ of real-valued functions,

$$\frac1m\,\mathbb E_\sigma\Big[\sup_{h\in H}\sum_{i=1}^m\sigma_i(\Phi_i\circ h)(x_i)\Big] \le l\,\hat R_S(H).$$

Theorem 5.10 (Rademacher complexity of bounded-norm linear hypotheses, milestone). For $S\subseteq\{x:\|x\|\le r\}$ and $H=\{x\mapsto w\cdot x:\|w\|\le\Lambda\}$,

$$\hat R_S(H) \le \sqrt{r^2\Lambda^2/m}.$$

Corollary 5.11 (margin bound for linear hypotheses, milestone). For the same $H$ and $X\subseteq\{x:\|x\|\le r\}$, fixing $\rho>0$, with probability at least $1-\delta$,

$$R(h) \le \hat R_{S,\rho}(h) + 2\sqrt{\frac{r^2\Lambda^2/\rho^2}{m}} + \sqrt{\frac{\log(1/\delta)}{2m}} \quad\text{for all } h\in H.$$

Theorem 5.8 — the mission's goal. For any set $H$ of real-valued functions and $\rho>0$, with probability at least $1-\delta$, both

$$R(h) \le \hat R_{S,\rho}(h) + \frac2\rho R_m(H) + \sqrt{\frac{\log(1/\delta)}{2m}}$$ $$R(h) \le \hat R_{S,\rho}(h) + \frac2\rho \hat R_S(H) + 3\sqrt{\frac{\log(2/\delta)}{2m}}$$

hold simultaneously for all $h\in H$.

Significance

Theorem 5.8 is genuinely dimension-free: unlike Chapter 3's VC-dimension bound (5.36 in the book, restated from Corollary 3.19), it holds regardless of the ambient feature dimension $N$, depending instead only on the hypothesis class's Rademacher complexity and the chosen margin $\rho$. Specialized to bounded-norm linear hypotheses (Corollary 5.11), this gives the theoretical justification most often cited for SVMs and every other margin-maximization algorithm: whenever the training data admits a large geometric margin, the empirical margin loss at that margin is small (often zero, in the separable case) and the bound is tight regardless of $N$. Every later chapter's own margin bound (multi-class in Chapter 9, ranking in Chapter 10) is a direct structural descendant of Theorem 5.8's proof technique. No prior art on the Prove2Me platform is faithful: GET /theorems?q=support+vector+machine and q=margin+bound return no hits on this book's model (the two q=margin+bound hits found, both from the Aether Catalog, state a different comparison — a VC-type bound is eventually worse than a fixed Rademacher-type bound as a function of dimension — not Theorem 5.8 itself); q=Talagrand and q=contraction+principle return several hits (Ledoux/Talagrand convex-distance concentration, Rudin's Banach-space contraction-mapping theorem, a generic Rademacher-sign contraction lemma for quadratic sums) but every one states either a different mathematical object (metric-space fixed points, Talagrand's concentration inequality on product spaces) or a different idiom (squared vs. linear coordinate sums) from Lemma 5.7's function-composition contraction — none reused. All nine items are drafted fresh.

Not formalized here: Theorem 5.4 (the SVM sparsity/leave-one-out bound). It is listed as a candidate milestone in BRIEF.md, but its statement and proof depend on the primal/dual SVM optimization problem itself (the Lagrangian, KKT conditions, and the resulting definition of a "support vector" as a training point with nonzero dual coefficient) — a materially different, non-margin-based proof technique (leave-one-out stability of the trained hypothesis, via Lemma 5.3) that shares no definitions with the margin-bound family this mission's goal and other milestones are built on. Formalizing it faithfully would require standing up the SVM primal/dual formalism (Lagrangian, complementary slackness, the "support vector" predicate itself) from scratch, which is disproportionate to a single additional milestone within this mission's budget; per the captain brief's guidance to leave out, rather than approximate, a statement that cannot be made faithful in the time available, it is omitted.

Difficulty

The proof of Theorem 5.8 needs the empirical margin loss's zero-one-loss upper bound ($\mathbb 1_{u\le 0}\le\Phi_\rho(u)$) applied before invoking Theorem 3.3's Rademacher generalization bound on the composed class $\tilde{\tilde H}=\{\Phi_\rho\circ f: f\in\tilde H\}$, $\tilde H=\{(x,y)\mapsto y\,h(x):h\in H\}$ — reversing this order (bounding $R(h)$ by a Rademacher complexity computed on the zero-one loss directly) does not work, because the zero-one loss is not Lipschitz. Talagrand's lemma is exactly what lets the $1/\rho$-Lipschitz surrogate $\Phi_\rho$ be pulled outside the Rademacher complexity, at the cost of a factor $1/\rho$ and no worse; its own proof is an induction removing one Rademacher variable at a time, using a two-point supremum argument (fixing $\epsilon>0$, choosing near-optimal $h_1,h_2$) that does not simplify to anything less than genuine care with suprema of non-smooth objects — a formalization attempting to replace this with a naive linearity-of-expectation argument would be proving a false or vacuous statement, since $\sup$ does not commute with linear combinations. Theorem 5.10's bound needs the Cauchy-Schwarz and Jensen inequalities used in the particular order the book uses them (Cauchy-Schwarz on the empirical sup, then Jensen on the expectation of a norm, then the independence of the $\sigma_i$s) — the bound $\hat R_S(H)\le r\Lambda/\sqrt m$ does not follow from either inequality alone.

Formalization scope

EmpiricalRademacherComplexity/RademacherComplexity are restated locally in SVM, byte-identical to chunk 03-rademacher-vc's own copies (a draft item cannot import another chunk's draft module); this duplication collapses once 03-rademacher-vc is uploaded and listed in missions/README.md's "Published definitions" table. MarginGeneralizationError is a new, real-valued-hypothesis specialization of Definition 2.1 (R(h) = P[y h(x) ≤ 0]), distinct from every earlier chunk's {-1,+1}-valued GeneralizationError, since no earlier chunk's own copy matches this chapter's real-valued convention. PhiRho/EmpiricalMarginLoss are new. The goal theorem (margin_bound_binary_classification) states H's own Rademacher complexity computed on the marginal X-distribution (D.map Prod.fst), matching the book's final displayed form — the proof's intermediate step (the lifted class $\tilde H=\{(x,y)\mapsto y h(x)\}$ having the same Rademacher complexity as $H$ itself, since $y\in\{-1,+1\}$) is not separately drafted, only the theorem's statement. Theorem 5.10/Corollary 5.11 generalize the book's ambient $\mathbb R^N$ to an arbitrary real inner-product space X ([NormedAddCommGroup X] [InnerProductSpace ℝ X]), a harmless generalization since the book's proof (Cauchy-Schwarz, Jensen, orthogonality of Rademacher signs) uses only the inner-product structure, never finite dimension; [BorelSpace X] is added to Corollary 5.11's statement to make the measurable structure under which MarginGeneralizationError is well-posed explicit, since every x ↦ ⟨w, x⟩ is automatically Borel-measurable — not a substantive restriction, the book never discusses measurability of linear functionals. No numerical constant in any of the four theorems is altered from the book's own displayed form. A trivializing formalization this mission avoids: stating Theorem 5.8 only for a Finset/finite H (which would make it a disguised instance of Chapter 2's finite-hypothesis bound rather than the chapter's genuinely new, complexity-based argument) — H : Set (X → ℝ) is left fully general, exactly as the book states it.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 5.
• C. Cortes, V. Vapnik, "Support-vector networks," Machine Learning 20(3), 1995, 273-297.
• M. Talagrand, "Sharper bounds for Gaussian and empirical processes," The Annals of Probability 22(1), 1994, 28-76.
• P. Bartlett, S. Mendelson, "Rademacher and Gaussian complexities: risk bounds and structural results," Journal of Machine Learning Research 3, 2002, 463-482.