Statistics

From "more spread out" to "more spread out in every direction"

Chapter III's convex order compares two real-valued random variables by "how spread out" they are, holding the mean fixed. Chapter VII lifts the same idea to random vectors: $X$ is smaller than $Y$ in the multivariate convex order if every convex function of $X$ has smaller expectation than the same function of $Y$. This mission formalizes that order, its increasing-convex companion, and their martingale-coupling characterizations — the direct $n$-dimensional generalizations of Chunk 03's and Chunk 04's own goal theorems — plus a cheap mean-equality corollary and a simple standalone scaling result.

The multivariate convex and increasing convex orders

Let $X$ be a random vector taking values in $\mathbb{R}^n$ on $(\Omega,\mu)$, and $Y$ a random vector taking values in $\mathbb{R}^n$ on $(\Omega',\nu)$. $X$ is smaller than $Y$ in the multivariate convex order, $X\le_{cx}Y$, if

$$E[\varphi(X)] \le E[\varphi(Y)] \quad \text{for every convex } \varphi:\mathbb{R}^n\to\mathbb{R} \text{ for which the two expectations exist},$$

and smaller than $Y$ in the increasing convex order, $X\le_{icx}Y$, if the same holds for every $\varphi$ that is both increasing (coordinatewise) and convex. Since each coordinate projection $\varphi_i(x)=x_i$ and its negation are both convex, $X\le_{cx}Y$ forces $E[X]=E[Y]$ componentwise (Eq. 7.A.5) — unlike $\le_{icx}$, which only forces $E[X]\le E[Y]$.

Formalization targets

Goal: the martingale-coupling characterization (Theorem 7.A.1)

$$X \le_{cx} Y \iff \exists\,(\Omega'',\rho),\ \hat X,\hat Y:\Omega''\to\mathbb{R}^n\text{ with } \hat X=_{st}X,\ \hat Y=_{st}Y,\ E[\hat Y\mid\hat X]=\hat X\text{ a.s.}$$

The direct $n$-dimensional generalization of Theorem 3.A.4 (Strassen's martingale coupling, Chunk 03's own goal theorem): a joint law on a common probability space realizing $X\le_{cx}Y$ as a genuine martingale pairing between copies of $X$ and $Y$. The book states no further "Furthermore" strengthening here, unlike the univariate and increasing-convex cases.

Companion: the submartingale-coupling characterization (Theorem 7.A.2, increasing convex case)

$X\le_{icx}Y$ iff there exist $\hat X,\hat Y$ on a common space with $\hat X=_{st}X$, $\hat Y=_{st}Y$, and $\{\hat X,\hat Y\}$ a submartingale, $E[\hat Y\mid\hat X]\ge\hat X$ a.s. — the direct generalization of Theorem 4.A.5's increasing-convex case (Chunk 04's own goal theorem), proved by the book's own cross-reference "by essentially the same method" as the goal. The book's bracketed increasing-concave companion is a genuinely separate statement (swapped conditioning) and is not drafted here for budget (see STATUS.md).

Supporting milestones

• Eq. (7.A.5), the mean-equality corollary: $X\le_{cx}Y\implies E[X]=E[Y]$ (componentwise), provided the expectations exist — a one-line consequence of ConvexOrder's own defining quantifier applied to $\pm$ each coordinate projection.
• Theorem 7.A.9, a simple standalone application: an independent, mean-one random scale factor $U$ always makes a random vector larger in the convex order, $X\le_{cx}UX$.

Significance

The multivariate convex order is the natural tool for comparing the variability of random vectors — portfolios of returns, multi-resource cost vectors, correlated component lifetimes — in a way that respects every direction of the space simultaneously rather than coordinate by coordinate. Its martingale-coupling characterization is the same tool that makes Strassen's theorem useful in the univariate case: it turns the intractable "for every convex $\varphi:\mathbb{R}^n\to\mathbb{R}$" quantifier into a single explicit joint construction, and because it generalizes directly (the book's own proof of Theorem 7.A.4, not drafted here, applies the univariate Theorem 3.A.4 coordinate by coordinate to build the multivariate coupling), it is the natural second data point — after Chunk 03's univariate case and Chunk 06's usual-order case — for what a "coupling-characterization" mission in this book's series looks like once both the order and the dimension vary. Theorem 7.A.9's scaling result is a compact, self-contained illustration of how the order behaves under a common operation (randomized scaling) that appears throughout the book's later risk and insurance examples.

No platform prior art exists: GET /theorems?q=convex+order and q=martingale return only false positives (checked at this book's triage time, re-confirmed this session). This mission restates the multivariate convex and increasing convex orders and their coupling characterizations as a self-contained pair, parallel in structure to Chunks 03 and 04's univariate missions but independently drafted, since drafts cannot import each other's Lean.

Difficulty

The chief formalization risk this chapter's own brief flags is confusing "convex" for $\varphi:\mathbb{R}^n\to\mathbb{R}$ (ordinary convexity, Mathlib's ConvexOn) with a coordinatewise or lattice-based notion — in particular, with Chunk 09's supermodular functions, a different and weaker condition. A second risk is the "increasing" half of IcxOrder: unlike convexity, "increasing" genuinely is the coordinatewise order (matching Chunk 06's convention), so IcxOrder mixes two different kinds of predicate on the same φ (Monotone in the coordinatewise sense, ConvexOn in the ordinary sense) and getting either one wrong silently changes which order is being stated. A third risk, specific to Theorem 7.A.2, is the bracketed icx/icv alternative: as in Chunk 04, the two cases are not symmetric rewrites of each other (the conditioning variable swaps), so a Lean statement conflating them with Or would misstate one case — this mission avoids the risk by drafting only the increasing-convex case and recording the omission explicitly rather than attempting an unsound unification.

Formalization scope

Random vectors are drafted as functions into Fin n → ℝ from arbitrary measurable spaces. ConvexOrder μ ν X Y quantifies over φ : (Fin n → ℝ) → ℝ with ConvexOn ℝ Set.univ φ (ordinary convexity) and Integrable (φ ∘ X) μ/Integrable (φ ∘ Y) ν inside the ∀; IcxOrder adds Monotone φ in Mathlib's default coordinatewise (Pi) order on Fin n → ℝ — the same order Chunk 06's MultivariateOrder uses — as a genuinely separate definition from ConvexOrder, not one derived from the other, since Theorem 7.A.12 (not drafted here) relates the two nontrivially and conflating them would trivialize such a relationship. Equality in law is ProbabilityTheory.IdentDistrib; the martingale/submartingale conditions use Mathlib's conditional-expectation notation ρ[Ŷ | m] =ᵐ[ρ] X̂ (resp. X̂ ≤ᵐ[ρ] ρ[Ŷ | m]) with m generated by X̂, here genuinely Fin n → ℝ-valued (well-defined since Fin n → ℝ is a finite-dimensional, hence complete, normed space over ℝ) — restated locally rather than imported from Chunks 03/06, since drafts cannot import another mission's definitions. Theorem 7.A.9's scaling U·X is Mathlib's scalar multiplication on the ℝ-module Fin n → ℝ.

Two deliberate scope restrictions, recorded rather than silently applied: (1) Theorem 7.A.2 is drafted only for the increasing-convex case, per this chapter's own pitfall 3 (the icv companion's swapped conditioning structure is a genuinely different predicate, not a sign-flipped rewrite, and budget did not justify a fourth definition/theorem pair to draft it separately, unlike Chunk 04 which had budget for both cases of its analogous theorem); (2) Theorem 7.A.5 through 7.A.8's closure properties (mixtures, convolutions, weak limits, the random-sum generalization) are left out entirely — each needs conditional-distribution or convergence-in-distribution machinery this mission's four items do not otherwise require, and none is on the goal's own attack chain.

A trivializing formalization this mission rules out: drafting IcxOrder by deriving it from ConvexOrder and a separate monotonicity wrapper in a way that makes their relationship (Theorem 7.A.12: $X\le_{st}Y\implies X\le_{icx}Y\wedge X\le_{icv}Y$, not drafted here) provable by unfolding rather than by genuine content — the two are kept as independently-quantified predicates for this reason. This mission draws on no platform prior art (searches for "convex order" and "martingale" as of 2026-09-18 return only false positives). Reusable beyond this mission: the ConvexOrder/IcxOrder pattern and their martingale/submartingale coupling shape parallel Chunks 03/04's univariate pair and Chunk 06's multivariate usual-order pair closely enough that a future pass drafting the icv companion, or Chapter VII's later dispersion and transform orders, could restate the same shape with minimal adaptation.

Selected references

• M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007, Chapter 7 (Multivariate Variability and Related Orders), §7.A.1–7.A.2. https://doi.org/10.1007/978-0-387-34675-5
• This series' Chunk 03 (StochasticOrders.Convex) and Chunk 04 (StochasticOrders.MonotoneConvex), for the univariate convex and increasing convex orders and their martingale/submartingale couplings this chapter directly generalizes; Chunk 06 (StochasticOrders.Multivariate), for the multivariate usual stochastic order and its own coupling characterization.

Motivation

Every statistical guarantee for a learning algorithm ultimately rests on a concentration inequality: a bound on how far an empirical average can stray from its expectation. For real-valued averages, Bernstein's inequality (1924, refined through the 20th century) is the classical tool — sharper than Hoeffding's inequality whenever the summands' variance is small compared to their range. Modern learning theory, however, frequently needs to control averages of objects that are not real numbers but elements of a Hilbert space: feature vectors $\Phi(x_i)y_i$, gradients of a loss, or the values a kernel machine's empirical risk functional takes. Steinwart & Christmann, Support Vector Machines (Springer 2008, Information Science and Statistics), Chapter 6, develop exactly the vector-valued extension needed for the book's own SVM consistency proofs: Theorem 6.14, Bernstein's inequality for independent random variables taking values in a separable Hilbert space, and its corollaries.

Setting

Fix a probability space $(\Omega,\mathcal A,P)$ and a separable real Hilbert space $H$. Random variables $\xi_1,\dots,\xi_n : \Omega \to H$ are independent if the family is mutually independent (not merely pairwise), and $\xi_i$ has essential supremum bound $B$, $\|\xi_i\|_\infty \le B$, if $\|\xi_i(\omega)\|_H \le B$ for $P$-almost every $\omega$. Writing $\mathbb E$ for $\mathbb E_P$, the quantities of interest are the mean $\mathbb E\,\xi_i \in H$ (a Bochner integral) and the variance bound $\sigma^2$, an upper bound on $\mathbb E\,\|\xi_i\|_H^2$.

The classical scalar case (Theorem 6.12, itself a refinement of Hoeffding's inequality, Theorem 6.10) bounds $P\big(\frac1n\sum_i \xi_i \ge \varepsilon\big)$ for real-valued, mean-zero, range- and variance-bounded $\xi_i$. The tool behind both the scalar and the vector-valued case is a general exponential-moment inequality (Theorem 6.13) valid for independent, integrable random variables taking values in any separable Banach space $E$:

$$P\Big(\Big\|\sum_{i=1}^n \xi_i\Big\| \ge \varepsilon n\Big) \le \exp\Big(-t\varepsilon n + t\,\mathbb E\Big\|\sum_{i=1}^n \xi_i\Big\| + \sum_{i=1}^n \mathbb E\big(e^{t\|\xi_i\|}-1-t\|\xi_i\|\big)\Big), \qquad \varepsilon,t \ge 0.$$

Formalization targets

Goal: Theorem 6.14 (Bernstein's inequality in Hilbert spaces)

$$P\left(\Big\|\frac1n\sum_{i=1}^n \xi_i\Big\|_H \ge \sqrt{\frac{2\sigma^2\tau}{n}} + \sqrt{\frac{\sigma^2}{n}} + \frac{2B\tau}{3n}\right) \le e^{-\tau}, \qquad \tau>0,$$

for independent, mean-zero $\xi_1,\dots,\xi_n : \Omega \to H$ with $\|\xi_i\|_\infty \le B$ and $\mathbb E\|\xi_i\|_H^2 \le \sigma^2$. This is the weakest stable form of the claim: it is stated for a general separable Hilbert space (not a fixed finite dimension), with the tail written as a sum of three explicit terms rather than folded into an unspecified constant, so it survives specialization to any concrete $H$ without modification.

Supporting facts

Theorem 6.13 (above) is the direct tool Theorem 6.14's own proof invokes ("we will prove the assertion by applying Theorem 6.13"); Theorem 6.12 is the scalar analogue Theorem 6.14 generalizes, included to make the generalization's exact form (three terms, not two) checkable against its source; Corollary 6.15, Hoeffding's inequality in Hilbert spaces, is the immediate mean-free-of-a-variance-bound consequence of Theorem 6.14 obtained by centering, reused directly in the book's own oracle-inequality proof (§6.4).

Significance

Theorem 6.14 is the concentration inequality behind the book's later empirical-process arguments for SVMs: whenever an SVM's analysis needs to bound the deviation of an empirical average of Hilbert-space-valued quantities (feature-map evaluations, loss gradients) from its mean, this is the tool invoked, via Corollary 6.15 in the book's own oracle-inequality derivation. Its distinct contribution over simply applying the scalar Theorem 6.12 coordinate-by-coordinate (which is not available without a fixed, finite orthonormal basis, and even then would produce dimension- dependent bounds) is that the bound here is entirely dimension-free: it depends on $H$ only through the variance bound $\sigma^2$ and the range bound $B$, not through $\dim H$.

The scalar Bernstein inequality is classical (Bernstein 1924, refined by Bennett 1962 and others to the sharper multiplicative form used here); its Banach- and Hilbert-space generalizations (via the martingale-difference / Yurinskii-type argument Theorem 6.13's proof uses) are standard in the empirical-process-theory literature by the time of this book (see, e.g., Pinelis 1994 for closely related Banach-space martingale inequalities). No machine-checked Lean proof of the Hilbert-space form is known to exist on the platform at the time of writing (the platform's own HighDimProb.Concentration.bernstein_unweighted, from the Vershynin series, is a different, sub-exponential-norm scalar statement — see Formalization scope); this mission asks for the book's own bounded-summand, explicit-constant Hilbert-space form.

Difficulty

The natural first attempt generalizes the scalar proof's Markov-inequality argument directly: bound $\mathbb E\,e^{t\|\sum_i\xi_i\|}$ using independence. This breaks immediately because $\|\cdot\|_H$ is not linear, so $e^{t\|\sum_i \xi_i\|}$ does not factor over $i$ the way $e^{t\sum_i \xi_i}$ does in the scalar case — there is no vector-valued analogue of the moment generating function that tensorizes under independence directly. Theorem 6.13's proof resolves this with a martingale-difference decomposition (writing the deviation as a telescoping sum of conditional-expectation differences $X_k$ across the filtration generated by $\xi_1,\dots,\xi_k$) rather than a direct product-of-moment-generating-functions argument, at the cost of needing $E$ separable (for the conditional expectations and the resulting sums to be well-defined and measurable). Deriving Theorem 6.14 from Theorem 6.13 then requires controlling the two extra terms Theorem 6.13 introduces (the mean-norm term and the per-summand correction) using only the Hilbert-space-specific facts $\mathbb E\langle\xi_i,\xi_j\rangle=0$ for $i\ne j$ (from independence and mean-zero) and the scalar bound on $\mathbb E\|\xi_i\|^2$ — which is exactly where the tail's extra $\sqrt{\sigma^2/n}$ term originates, and is not obtainable by naively reusing the scalar Theorem 6.12's two-term optimization over $t$ unchanged.

Formalization scope

$H$ (and, for Theorem 6.13, $E$) is an arbitrary separable real (Hilbert, resp. Banach) space — not fixed to a Euclidean space of any dimension — matching the book's own generality, which is essential since the theorem's dimension-independence is part of its content. $\|\xi_i\|_\infty \le B$ is formalized as the almost-sure bound ∀ᵐ ω ∂P, ‖ξ i ω‖ ≤ B, matching the book's $L^\infty(P)$ convention rather than requiring the bound to hold for literally every $\omega$. Independence is the mutual independence of the whole family (Mathlib's iIndepFun), matching Theorem 6.13's proof, which uses independence of $\xi_k$ from $\sum_{i\ne k}\xi_i$ for every $k$ simultaneously, not merely pairwise independence.

A trivializing formalization would state the conclusion in terms of the scalar random variable $\|\xi_i\|_H$ rather than the vector-valued average's norm $\big\|\frac1n\sum_i \xi_i\big\|_H$ — this would collapse the theorem to an easier scalar statement about a nonnegative random variable and lose the whole point of the vector-valued generalization; it is ruled out here by writing the norm of the sum (not a sum of norms) inside the probability. Likewise, dropping the $\sqrt{\sigma^2/n}$ middle term of the tail bound (present here, absent from the scalar Theorem 6.12) would silently understate the genuine dimension-independent cost of vector-valued concentration; all three terms are kept.

Theorem 6.13's general Banach-space statement, and the scalar Theorem 6.12, are reusable beyond this mission (Theorem 6.13 is the tool any future Banach-space-valued concentration mission in this series would reach for first). The platform's existing HighDimProb.Concentration. bernstein_unweighted/hoeffding_rademacher (Vershynin series) are not reused as kind: reference items here: they use a sub-Gaussian/sub-exponential-Orlicz-norm parameterization and a universal (unspecified) constant, a genuinely different hypothesis structure from this chapter's explicit $L^\infty$-bounded, exact-constant form — reusing them would misrepresent this chapter's own, sharper statement. Completing the four sorrys (Theorems 6.12-6.14, Corollary 6.15) is welcome; the martingale-difference argument behind Theorem 6.13 is the natural starting point, since the other three all reduce to it directly.

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 6, §6.2, pp. 210-217).
• S. Bernstein, "On a modification of Chebyshev's inequality and of the error formula of Laplace," Ann. Sci. Inst. Sav. Ukraine, Sect. Math. 1(4), 1924 (original scalar inequality).
• G. Bennett, "Probability inequalities for the sum of independent random variables," Journal of the American Statistical Association 57(297), 1962, pp. 33-45. https://doi.org/10.1080/01621459.1962.10482149
• I. Pinelis, "Optimum bounds for the distributions of martingales in Banach spaces," Annals of Probability 22(4), 1994, pp. 1679-1706. https://doi.org/10.1214/aop/1176988477

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

Comparing variability, not just location

Chapter I's usual stochastic order compares "how large" two random variables tend to be. A different, equally common question in operations research is "how spread out" a random variable is: two portfolios with the same expected loss can differ sharply in how much that loss varies, and a risk-averse decision maker or a convex cost function cares about exactly that difference. Shaked and Shanthikumar's Stochastic Orders (Springer, 2007) formalizes this comparison as the convex order, the book's mean-preserving-spread order (known outside OR and probability circles as the Rothschild–Stiglitz order from economics). This mission formalizes the order and its central structural result: Strassen's martingale-coupling characterization.

The convex 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 convex order, written $X \le_{cx} Y$, if

$$E[\varphi(X)] \le E[\varphi(Y)] \quad \text{for every convex } \varphi:\mathbb{R}\to\mathbb{R} \text{ for which the two expectations exist.}$$

Convex functions take their relatively largest values on the "extreme" regions outside some interval, so $X \le_{cx} Y$ says $Y$ is more likely than $X$ to take extreme values: $Y$ is "more variable" than $X$. Unlike the usual stochastic order, $X \le_{cx} Y$ forces the two means to agree ($E[X]=E[Y]$, taking $\varphi(x)=\pm x$, both convex) — the convex order compares spread holding location fixed, exactly the mean-preserving-spread reading. Two equivalent forms make it tractable: comparing tail integrals of the survival/distribution functions (Theorem 3.A.1), and comparing mean absolute deviations $E|X-a|$ from every point $a$ (Theorem 3.A.2).

Formalization targets

Goal: Strassen's martingale-coupling characterization (Theorem 3.A.4)

$$X \le_{cx} Y \iff \exists\,(\Omega'',\rho),\ \hat X,\hat Y:\Omega''\to\mathbb{R}\text{ with } \hat X=_{st}X,\ \hat Y=_{st}Y,\ E[\hat Y\mid\hat X]=\hat X\text{ a.s.}$$

Furthermore, $\hat X,\hat Y$ can be chosen so that the conditional law $[\hat Y\mid\hat X=x]$ stochastically increases with $x$ (in $\le_{st}$). This is the convex-order analogue of Chapter I's Theorem 1.A.1: instead of one variable dominating the other pathwise, $Y$'s copy is a fair (martingale) randomization of $X$'s copy whose spread only grows in the conditioning value. The book itself calls the constructive direction "not easy to prove"; this mission states the theorem faithfully, including the "Furthermore" strengthening, without attempting a proof.

Supporting milestones

• Theorem 3.A.1, the tail-integral characterizations: for $X,Y$ with $E[X]=E[Y]$, $X\le_{cx}Y$ iff $\int_x^\infty\bar F(u)\,du\le\int_x^\infty\bar G(u)\,du$ for all $x$, and iff $\int_{-\infty}^x F(u)\,du\le\int_{-\infty}^x G(u)\,du$ for all $x$ — the two integrated forms the book's own sketch of Theorem 3.A.4 uses.
• Theorem 3.A.2, the absolute-deviation characterization: for $X,Y$ with $E[X]=E[Y]$, $X\le_{cx}Y$ iff $E|X-a|\le E|Y-a|$ for every real $a$.
• Theorem 3.A.12(d), closure under convolution: independent $X_i\le_{cx}Y_i$ for $i=1,\dots,m$ gives $\sum_i X_i \le_{cx} \sum_i Y_i$ — the convex-order analogue of Chapter I's Theorem 1.A.3(b).

Significance

The convex order is the standard way operations research and actuarial science formalize "more variable, same average": comparing the riskiness of two portfolios with matched expected return, the effect of aggregation or diversification on total claim size, or the value of information in a stochastic program (where a random variable degenerates to its mean exactly when the decision maker learns everything, the two extremes of a convex-order chain). Strassen's characterization is what turns "compare against every convex function" — an intractable universal quantifier — into a single explicit construction: exhibit one martingale coupling and the comparison is settled for every convex function at once, by Jensen's inequality. This is the technique behind bounding the effect of information or risk aggregation without checking convexity function by function, and the "Furthermore" monotonicity clause is what makes the coupling itself informative about how the spread grows with the conditioning variable, not merely that some fair coupling exists.

Formalizing this theorem fixes, for the whole book series, the exact shape every later coupling theorem for a variability-type order (the increasing convex/concave orders of Chapter IV via a submartingale, the multivariate convex order of Chapter VII) is expected to restate. No proof is attempted; the book's own remark that the constructive direction is "not easy" marks it as a genuine target for a future proof-bearing pass, not a formality.

Difficulty

The definitional trap mirrors Chapter I's: "for every convex $\varphi$" must be a genuine universal quantifier over Mathlib's own convexity predicate, with the existence of both expectations stated as an explicit integrability hypothesis inside the quantifier, not assumed globally or dropped. The coupling theorem doubles the difficulty of Theorem 1.A.1's: the conditional-expectation condition $E[\hat Y\mid\hat X]=\hat X$ a.s. is with respect to the $\sigma$-algebra generated by $\hat X$, not an informal "expected value given $\hat X$", and must use the martingale API's own convention (Mathlib's condExp) precisely. The "Furthermore" clause compounds this: it is a claim about the regular conditional distribution of $\hat Y$ given $\hat X=x$ for every point $x$, not merely the conditional expectation, and dropping it silently (as a "remark" rather than part of the theorem) would understate what Theorem 3.A.4 actually claims — the chapter brief flags this explicitly as a trap, and it is kept as a conjunct of the same existential witness here.

Formalization scope

Random variables are again measurable functions into $\mathbb{R}$ from arbitrary measurable spaces, ConvexOrder μ ν X Y taking $X$ on $(\Omega,\mu)$ and $Y$ on a separate $(\Omega',\nu)$, matching Chapter I's convention and this series' own pattern. Convexity is Mathlib's ConvexOn ℝ Set.univ φ; "equality in law" is again ProbabilityTheory.IdentDistrib. The martingale condition uses Mathlib's conditional-expectation notation ρ[Ŷ | m] =ᵐ[ρ] X̂ with m the $\sigma$-algebra MeasurableSpace.comap X̂ inferInstance generated by X̂ — the martingale API's own convention, not a hand-rolled gloss. The "Furthermore" clause uses Mathlib's ProbabilityTheory.condDistrib, the regular conditional distribution kernel of Ŷ given X̂ (available since ℝ is a standard Borel space), and states "increasing in x in ≤st" via the kernel's survival function being monotone in x at every threshold — restating, locally to this chapter's namespace, the same tail-probability shape Chapter I's UsualOrder uses (drafts cannot import another mission's definitions, per this series' convention). A trivializing formalization is ruled out explicitly: the martingale and monotonicity conjuncts are both kept as genuine content of the existential witness in the goal theorem, not weakened to a bare coupling or dropped as an optional remark.

This mission draws on no platform prior art (searches for "convex order", "Strassen", "martingale", "Jensen" returned only unrelated geometry/algorithm/physics results as of 2026-09-18); Mathlib's Probability/Martingale/* supplies the conditional-expectation and kernel machinery the coupling condition and its "Furthermore" clause are built from, but no platform theorem states the convex order or its coupling characterization itself. Reusable beyond this mission: the condExp/condDistrib-based martingale-coupling pattern is the shape Chapter IV's analogous submartingale coupling (Theorem 4.A.5) and Chapter VII's multivariate convex order (Theorem 7.A.1) are each expected to restate independently.

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
• M. Rothschild and J. E. Stiglitz, "Increasing risk: I. A definition", Journal of Economic Theory, 2(3), 1970, 225–243. https://doi.org/10.1016/0022-0531(70)90038-4

Motivation

Online decision-making problems — multi-armed bandits, contextual bandits, structured bandits, and episodic reinforcement learning — look superficially different but share a common shape: a learner repeatedly acts, observes feedback, and is scored by regret against the best action in hindsight. Foster, Kakade, Qian and Rakhlin's Foundations of Reinforcement Learning and Interactive Decision Making (Foster & Rakhlin, arXiv:2312.16730v1) develops a unifying account of this shape and asks a sharper question than "does this specific algorithm work?": for a given class of possible environments, what is the best regret any algorithm can achieve? The Decision-Estimation Coefficient (DEC), introduced by Foster, Kakade, Qian and Rakhlin (2021, "The Statistical Complexity of Interactive Decision Making") and refined by Foster, Golowich, Qian, Rakhlin and Sekhari (2023), was proposed as the answer: a single real-valued complexity measure of a model class that simultaneously (i) drives a generic optimal-up-to-constants algorithm (Estimation-to-Decisions, E2D), and (ii) lower-bounds the regret of every algorithm. Item (ii) is what turns the DEC from "a complexity measure that happens to work for the algorithms we know" into a genuine characterization of statistical difficulty, in the same sense that minimax rates characterize the difficulty of estimation problems in classical statistics. This mission formalizes that lower bound.

Setting

Chapter 6 of the book (pp. 93–128) introduces Decision Making with Structured Observations (DMSO), a protocol general enough to subsume the contextual-bandit, structured-bandit and episodic tabular-RL protocols of earlier chapters. Over $T$ rounds, the learner selects a decision $\pi_t$ from a decision space $\Pi$; nature draws a reward-observation pair $(r_t, o_t)$ from a fixed, unknown model $M^\star(\cdot \mid \pi_t)$, where a model $M$ maps each decision to a distribution over a reward space $R$ and an observation space $O$. The learner has access to a model class $\mathcal{M}$ containing $M^\star$ (realizability). For $M \in \mathcal{M}$, write $f^M(\pi) := \mathbb{E}_{M,\pi}[r]$ for the mean reward function and $\pi_M := \arg\max_\pi f^M(\pi)$ for the optimal decision; regret is $\mathrm{Reg} := \sum_{t=1}^T f^{M^\star}(\pi_{M^\star}) - \mathbb{E}_{\pi_t \sim p_t}[f^{M^\star}(\pi_t)]$, exactly as in the bandit chapters, now for the general model class.

Because observations, not just mean rewards, now carry information, the DEC needs a way to measure distance between the full conditional distributions $M(\pi)$ and $\hat M(\pi)$, not just between scalars $f^M(\pi)$ and $f^{\hat M}(\pi)$. The chapter uses the squared Hellinger distance $D_H^2$, one of a family of Csiszár $f$-divergences that also includes total variation ($D_{TV}$) and Kullback-Leibler ($D_{KL}$) divergence. For a reference model $\hat M$ and scale $\gamma > 0$, the general Decision-Estimation Coefficient is the min-max game value

$$\mathrm{dec}_\gamma(\mathcal{M}, \hat M) := \inf_{p \in \Delta(\Pi)} \sup_{M \in \mathcal{M}} \mathbb{E}_{\pi \sim p}\bigl[f^M(\pi_M) - f^M(\pi) - \gamma \cdot D_H^2(M(\pi), \hat M(\pi))\bigr],$$

and $\mathrm{dec}_\gamma(\mathcal{M}) := \sup_{\hat M \in \mathrm{co}(\mathcal{M})} \mathrm{dec}_\gamma(\mathcal{M}, \hat M)$. This mission's Lean development (FoundationsRL.GeneralDM) formalizes discrete versions of $D_{TV}$, $D_H^2$, $D_{KL}$ for a finite outcome type, the DMSO regret, and this DEC.

Formalization targets

The goal is Proposition 28 (DEC Lower Bound), p. 105:

$$\exists\, c > 0 \text{ (sufficiently small)} : \forall\, T \text{ with } \mathrm{dec}^c_{\varepsilon_T}(\mathcal{M}) \ge 10\,\varepsilon_T,\; \varepsilon_T := c/\sqrt{T},\; \forall\, \text{algorithm}\; p,\; \exists\, M \in \mathcal{M} : \mathrm{regret}(M, p) \ge \tfrac{1}{20}\, \mathrm{dec}^c_{\varepsilon_T}(\mathcal{M}) \cdot T.$$

Here $\mathrm{dec}^c_\varepsilon$ is the constrained DEC (§6.5.1), a variant of the offset DEC above that hard-constrains the information gain rather than subtracting it — a technical refinement needed to make the lower-bound direction go through — and the "localization condition" $\mathrm{dec}^c_{\varepsilon_T}(\mathcal{M}) \ge 10\varepsilon_T$ is a genuine hypothesis of the proposition, not a footnote. Unlike almost every other target in this series of missions, the statement quantifies over every algorithm rather than naming one: it is a genuine impossibility result. Two supporting divergence facts are included as milestones because the DEC's information-theoretic argument rests on them: Lemma 19 ($D_{TV}^2 \le D_H^2 \le D_{KL}$) and Lemma 20 (a bounded-likelihood-ratio refinement bounding $D_{KL}$ in terms of $D_H^2$). The chapter's own matching upper bound, Proposition 26 (the E2D regret bound for the general DMSO protocol, the direct analogue of Chapter 4's Proposition 13), is included as a milestone to give the reader the matching pair the chapter presents together. Finally, Corollary 1 restates the lower bound in terms of the localized offset DEC (combining Proposition 28 with Proposition 27), included as a milestone showing the lower bound's reach beyond the constrained DEC alone.

Significance

Proposition 28 is what makes the DEC a genuine characterization of the statistical complexity of interactive decision making, rather than merely a sufficient condition for a particular algorithm family to succeed. Combined with the (uncited, technically deeper) matching upper bound for the constrained DEC — Proposition 29, stated but not proved in the book — it shows that for any finite model class, the constrained DEC is necessary and sufficient for low regret up to a $\sqrt{\log|\mathcal{M}|}$ factor in the localization radius: no complexity measure that is substantially different from the DEC can characterize the same problems. This is the general decision-making analogue of how minimax rates pin down statistical estimation, now for interactive protocols with adaptive feedback.

Formalizing the lower bound is new work: no result of this shape exists on the Prove2Me platform (searches for "decision-estimation", "general divergence", "constrained DEC" and "Hellinger" — the last of which surfaces two related-but-distinct affinity/Le Cam bounds from a different mission on bandit lower bounds — return no faithful prior art; see MODERATION_NOTES.md). The formal statement is the boxed proposition; the book gives a self-contained but simplified proof (two named simplifying assumptions, §6.5.3) and cites Foster, Golowich, Qian, Rakhlin & Sekhari (2023) for the unrestricted argument. This mission's Lean items are draft statements (:= by sorry), not proofs; formalizing the proof itself — a two-point adaptive testing argument using the chain rule for KL divergence and a change-of-measure step — is the open contribution this mission proposes.

Difficulty

The obvious first attempt is to try to prove the lower bound by exhibiting one fixed pair of hard models $M, \hat M$, as in classical two-point minimax lower bounds (Le Cam's method, Fano's inequality). This fails here because the decision-making protocol is interactive and adaptive: the algorithm's queries depend on what it has observed, so a model pair chosen obliviously (before seeing the algorithm) cannot in general be made indistinguishable to every algorithm — an adaptive algorithm can be constructed that distinguishes any two fixed models quickly by querying where they differ. The book's proof instead selects the "hard" alternative model $M$ as a function of the algorithm's own strategy (via the constrained DEC's arg max, Eq. (6.36)), so that the pair is hard specifically for the algorithm under consideration, then uses the chain rule for KL divergence plus the change-of-measure identity between the algorithm's induced distributions under $M$ and $\hat M$ to conclude that the algorithm's realized decisions must look similar under both models — hence it cannot get low regret on both simultaneously. Every step of this argument depends on the exact game structure of the constrained DEC, not just its numerical value; a formalization that leaves $\mathrm{dec}^c_\varepsilon$ as an unconstrained real parameter (rather than the actual $\inf$-$\sup$ game with its information-gain constraint) would make the lower bound's conclusion vacuous, since the hypothesis $\mathrm{dec}^c_{\varepsilon_T}(\mathcal{M}) \ge 10\varepsilon_T$ would no longer track any actual property of $\mathcal{M}$.

Formalization scope

The decision space $\Pi$ and the outcome (reward, observation) alphabet $Y$ are both taken as finite types (Fintype); a model $m : \Pi \to Y \to \mathbb{R}$ is a conditional probability vector, and a reward-extraction map $\mathrm{rew} : Y \to \mathbb{R}$ recovers the mean reward $f^m(\pi) = \sum_y m(\pi)(y)\cdot\mathrm{rew}(y)$. hellingerSq, totalVariationDiscrete, klDivDiscrete specialize the book's general dominating-measure divergence formula (Eq. (6.5)) to the counting measure on this finite type; klDivDiscrete returns an ENNReal so its $+\infty$ case (when $P$ is not absolutely continuous w.r.t. $Q$) is represented honestly. The DEC, the constrained DEC and the localized subclass are literal sInf-of-sSup/sSup-of-sSup transcriptions of the book's min-max games — the same convention this series uses for the Chapter-4 DEC — not opaque free real numbers, which rules out the trivializing formalization named above.

Three deviations from this series' usual convention of pinning every constant to the value the book's own proof derives are deliberate and disclosed. First, the numerical constant $c$ in $\varepsilon_T := c/\sqrt{T}$ is explicitly called "not important" by the authors themselves (footnote a, p. 105); it is existentially quantified (∃ c > 0) rather than pinned to a numeral. Second — added at moderation, round 2, 2026-09-19, after the constant was found to be pinned incorrectly — the lower bound's own multiplicative constant is also existentially quantified (∃ c' > 0) rather than pinned to 1/20. The book's printed proof (§6.5.3, pp. 107–110) derives 1/20 (p. 110, not p. 109 as an earlier draft of this mission stated) only under two named simplifying assumptions the theorem's hypotheses do not carry (p. 107, "Simplifications": a class-wide bounded-curvature hypothesis, Eq. (6.34); and a bound on the unaugmented $\sup_{\hat M\in\mathcal M}\mathrm{decc}_\varepsilon(M,\hat M)$ rather than the officially-defined, augmented $\mathrm{decc}_\varepsilon(M) = \sup_{\hat M\in\mathrm{co}(\mathcal M)} \mathrm{decc}_\varepsilon(M\cup\{\hat M\},\hat M)$ this mission's decC implements). Since augmenting either supremum's domain can only raise its value, the printed proof's bound on the narrower, unaugmented quantity does not license a pinned 1/20 against the fully general decC this theorem states; the book itself attributes the proof of the general statement to an external reference (Foster, Golowich, Qian, Rakhlin & Sekhari 2023) not in this document. The existential c' matches the book's own unpinned $\gtrsim$ for Proposition 28 as printed on pp. 105–106. Third, "any algorithm" and $\mathbb{E}[\mathrm{Reg}(T)]$ are formalized, as throughout this series, without a full stochastic-process/history model: regret is a deterministic quantity evaluated at a fixed realized decision-distribution sequence $p : \mathrm{Fin}\,T \to \Pi \to \mathbb{R}$, rather than an expectation over an adaptive, history-dependent algorithm's own randomness. Formalizing the fully adaptive, measure-theoretic version of "any algorithm" — with an explicit filtration and expectation over the induced process law $P_M$ — is future work a solver could add; the current statement is faithful to the book's deterministic-per-realization content but not to its full generality over randomized, history-dependent strategies. The DMSO protocol (Def_FoundationsRL_GeneralDM_Protocol) and the DEC (Def_FoundationsRL_GeneralDM_DEC) are restated locally rather than imported from Chapter 4's mission (FoundationsRL.Structured), since draft items cannot import another chunk's drafts; contributions extending either mission to reuse the other's substrate once both are published are welcome.

Selected references

• Foster, D. J., Kakade, S. M., Qian, J., & Rakhlin, A. (2023). Foundations of Reinforcement Learning and Interactive Decision Making. arXiv:2312.16730.
• Foster, D. J., Kakade, S. M., Qian, J., & Rakhlin, A. (2021). The Statistical Complexity of Interactive Decision Making. arXiv:2112.13487.
• Foster, D. J., Golowich, N., Qian, J., Rakhlin, A., & Sekhari, A. (2023). A Unified Model and Dimension for Interactive Estimation. arXiv:2306.06184.
• Polyanskiy, Y., & Wu, Y. Information Theory: From Coding to Learning. Cambridge University Press (draft edition cited by the book as [68]).

Motivation

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

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

Setting

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

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

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

Formalization targets

Grothendieck's inequality (Theorem 3.5.1)

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

Formalization targets

Goal (Theorem 5.3.1, Johnson-Lindenstrauss Lemma)

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

Spectral clustering recovers group labels from a similarity matrix: compute its leading eigenvectors, embed each point as a row of the eigenvector matrix, and cluster the rows with k-means. It is a standard last step of convex-relaxation methods for clustering, which first estimate a clustering matrix $X$ (with $X_{ij} = 1$ when $i$ and $j$ belong to the same cluster) and then have to turn the estimate back into labels.

Srivastava, Sarkar and Hanasusanto (arXiv:1912.07546v3; Operations Research 71(1), 2023) estimate $X$ by a linear program on a thresholded Gaussian kernel and then round it this way (Algorithm 1, steps 3–4). Their Theorem 2 controls the error of the rounding step in terms of the $\ell_1$ error of the estimate. The argument follows Lei and Rinaldo (Ann. Statist. 43(1), 2015), who analysed spectral clustering for stochastic block models with a polynomial-time $(1+\epsilon)$-approximate k-means step, combined with the Davis–Kahan theorem in the form of Yu, Wang and Samworth (Biometrika 102(2), 2015). The same pattern, "matrix estimation error ⇒ eigenvector error ⇒ misclassification count", recurs throughout the analysis of SDP and spectral methods for community detection and mixture models.

Setting

There are $n$ points and $r$ clusters. A fixed labelling $\varphi : [n] \to [r]$ gives clusters $C_k = \{i : \varphi(i) = k\}$ of sizes $n_k \ge 1$, and $n_{\min} = \min_k n_k$. The true clustering matrix is $X^0_{ij} = 1$ if $\varphi(i) = \varphi(j)$ and $0$ otherwise. Its scaled membership matrix is

$$U^0 = Z^0\,\mathrm{Diag}(1/\sqrt{n_1},\dots,1/\sqrt{n_r}),\qquad U^0_{ik} = \begin{cases} 1/\sqrt{n_k} & \varphi(i) = k,\\ 0 & \text{otherwise.}\end{cases}$$

The estimate $\hat X \in \mathbb R^{n\times n}$ is any symmetric matrix with entries in $[0,1]$. Spectral rounding takes a matrix $\hat U \in \mathbb R^{n\times r}$ of orthonormal eigenvectors of $\hat X$ for its $r$ largest eigenvalues (ties broken arbitrarily), and runs k-means on the rows of $\hat U$. A membership matrix $\Theta \in \mathbb M_{n,r}$ is a $\{0,1\}$-matrix with exactly one $1$ per row; a pair $(\hat\Theta, \hat B)$ with $\hat B \in \mathbb R^{r\times r}$ is a $(1+\epsilon)$-approximate k-means solution on the rows of $\hat U$ if

$$\|\hat U - \hat\Theta\hat B\|_F^2 \le (1+\epsilon)\min_{\Theta\in\mathbb M_{n,r},\, B\in\mathbb R^{r\times r}}\|\hat U - \Theta B\|_F^2 .$$

Let $O$ be an optimal rotation, an orthogonal $r\times r$ matrix minimising $\|\hat U - U^0O\|_F$. With $v_i$ and $\bar v_i$ the rows of $U^0O$ and $\hat\Theta\hat B$, the misclassified set of cluster $k$ is

$$\mathcal S_k = \Big\{ i \in C_k : \|\bar v_i - v_i\| \ge \tfrac{1}{2\sqrt{n_k}} \Big\}.$$

Norms: $\|A\|_1 = \sum_{i,j}|A_{ij}|$ (entrywise), $\|A\|_F^2 = \sum_{i,j}A_{ij}^2$.

Formalization targets

Goal: Theorem 2, (15), without outliers

For every $\hat X$, $\hat U$, $(\hat\Theta,\hat B)$ and optimal $O$ as above and every $\epsilon > 0$,

$$\sum_{k\in[r]}\frac{|\mathcal S_k|}{n_k} \;\le\; 64(2+\epsilon)\,\frac{\|X^0 - \hat X\|_1}{n_{\min}^2}.$$

Milestones

1. Davis–Kahan (Theorem 3, case $s=1$): an eigengap $g$ of a symmetric $\Sigma$ below its top $r$ eigenvalues gives an orthogonal $\hat O$ with $\|U - \hat U\hat O\|_F \le 2^{3/2}\|\hat\Sigma - \Sigma\|_F/g$.
2. Eigenstructure of $X^0$: $U^0$ consists of top-$r$ eigenvectors of $X^0$ with eigenvalues $n_1,\dots,n_r$, and $X^0$ vanishes on the orthogonal complement, so the eigengap is $n_{\min}$.
3. (G.6)(iii): $\|A - B\|_F^2 \le \|A - B\|_1$ for matrices with entries in $[0,1]$.
4. (G.6): $\|\hat U - U^0 O\|_F^2 \le 8\|\hat X - X^0\|_1/n_{\min}^2$.
5. Lemma 5, (G.4) (Lei–Rinaldo): for $V = \Theta^*B^*$ and a $(1+\epsilon)$-approximate k-means solution on any $\hat V$, $\sum_k |\mathcal S_k|\delta_k^2 \le 4(4+2\epsilon)\|V - \hat V\|_F^2$.
6. Centre separation: the rows of $B^* = \mathrm{Diag}(1/\sqrt{n_k})O$ satisfy $\|b^*_l - b^*_k\| = \sqrt{1/n_k + 1/n_l}$.

Companion: permutation recovery

If $64(2+\epsilon)\|X^0 - \hat X\|_1/n_{\min}^2 \le 1$, the k-means labels agree with $\varphi$ up to one permutation of $[r]$ on every point outside $\bigcup_k\mathcal S_k$.

Significance

Inequality (15) separates the analysis of the algorithm into an estimation part (how close $\hat X$ is to $X^0$ in $\ell_1$, Theorem 1 of the paper) and a purely deterministic rounding part. Any estimator of the clustering matrix with entries in $[0,1]$ — the Robust-LP, the SDP relaxations of Peng–Wei or Amini–Levina, a thresholded kernel — inherits a misclassification bound from its $\ell_1$ error through this one statement, with an explicit constant. The companion statement shows that the sets $\mathcal S_k$ really are the misclassified points.

The result is proved on paper; none of it is formalized. Mathlib has the spectral theorem for Hermitian matrices but no eigenspace perturbation bound of Davis–Kahan type, and the platform has no k-means approximation lemma for membership matrices. A machine-checked Davis–Kahan theorem in Frobenius norm and a machine-checked Lei–Rinaldo lemma are reusable well beyond this paper: they are the two standard ingredients of every spectral clustering guarantee for block models and mixtures.

Difficulty

The k-means part is elementary but bookkeeping-heavy: the comparison point in the $(1+\epsilon)$ bound must be a feasible k-means solution, which is why the true embedding $U^0O$ has to factor as a membership matrix times a centre matrix. The main obstacle is the Davis–Kahan step. The naive route through individual eigenvectors fails when eigenvalues of $\hat X$ or of $X^0$ are repeated (here $X^0$ has eigenvalue $n_k$ with multiplicity whenever cluster sizes coincide), and only the subspace is stable; the bound must be stated up to an orthogonal matrix and proved for the whole eigenspace, with no ordering or separation assumption on the eigenvalues of $\hat X$.

Formalization scope

Points are Fin n, clusters Fin r, matrices Matrix ι κ ℝ; the norms are explicit sums, not Mathlib's matrix norm instances. The labelling $\varphi$ is fixed; membership matrices are encoded by assignments $a : [n]\to[r]$, and "$\le (1+\epsilon)\min$" by "$\le (1+\epsilon)\cdot$ the cost of every assignment and every centre matrix". "Top-$r$ eigenvectors" is variational: orthonormal columns, eigenvector equations, and every Rayleigh quotient on the orthogonal complement at most each selected eigenvalue. $n_{\min}$ is a finite minimum and requires $r \ge 1$.

Departures from the printed text, each disclosed in the item concerned:

• No outliers ($m = 0$). The printed Theorem 2 allows outliers; it is false for $m \ge 1$, because the outlier rows of $U^0$ are zero, so the true embedding is not k-means feasible and Lemma 5 does not apply. A counterexample with two clusters of size $M > 256$, one isolated outlier and $\epsilon = 2$ violates (15).
• No probability, no $\bar\epsilon$, no separation condition. (15) is deterministic in $\|X^0 - \hat X\|_1$; the printed probabilistic hypotheses only feed Theorem 1 into the permutation claim.
• The printed $n_{\min} > r$ is replaced by the weaker $n_k \ge 1$.
• Davis–Kahan is stated for the leading eigenspace ($s = 1$), the only case used.
• In Lemma 5 the thresholds are required to satisfy $\delta_k \ge 0$, which the page leaves implicit; for a negative $\delta_k$ the bound (G.4) fails at $\hat V = V$.

The goal quantifies over every optimal rotation $O$, not over some orthogonal matrix chosen afterwards (which could make $\mathcal S_k$ empty), and over every top-eigenvector matrix and every approximate k-means solution; a formalization that fixes $\hat U$ to good eigenvectors, compares only against the true labels, or drops the eigenvalue-dominance clause (allowing bottom eigenvectors) proves a different and partly false statement.

Contributions welcome: Davis–Kahan in Frobenius norm for symmetric real matrices (general $s$ included), the Lei–Rinaldo lemma in full, and the eigenstructure of block-constant matrices.

Selected references

• P. R. Srivastava, P. Sarkar, G. A. Hanasusanto, A Robust Spectral Clustering Algorithm for Sub-Gaussian Mixture Models with Outliers, arXiv:1912.07546v3, 2021; Operations Research 71(1), 2023. https://arxiv.org/abs/1912.07546
• J. Lei, A. Rinaldo, Consistency of spectral clustering in stochastic block models, Annals of Statistics 43(1), 215–237, 2015. https://doi.org/10.1214/14-AOS1274
• Y. Yu, T. Wang, R. J. Samworth, A useful variant of the Davis–Kahan theorem for statisticians, Biometrika 102(2), 315–323, 2015. https://doi.org/10.1093/biomet/asv008
• C. Davis, W. M. Kahan, The rotation of eigenvectors by a perturbation. III, SIAM Journal on Numerical Analysis 7(1), 1–46, 1970. https://doi.org/10.1137/0707001