Statistics

Motivation

Chapter 9 asks whether the support vector machine — a regularized empirical risk minimizer $f_{D,\lambda}$ over an RKHS $H$ — is a statistically consistent estimator for regression: does $R_{L,P}(f_{D,\lambda_n}) \to R^*_{L,P}$ as the sample size $n \to \infty$, for a suitable regularization schedule $\lambda_n \to 0$? The chapter's main theorem (Theorem 9.1) answers yes, under an explicit polynomial rate condition on $\lambda_n$. Its proof reduces the question to bounding how far the empirical regularized solution can be from the population regularized solution, and that reduction bottoms out in a single concentration-of-measure fact: how tightly does an empirical mean of i.i.d. Hilbert-space-valued random variables concentrate around its true mean, given only a bound on one $q$-th moment (no exponential-moment assumption at all)? That fact is Lemma 9.2, "the following lemma to bound the probability of $|R_{L,P}(f_{D,\lambda}) - R_{L,P}(f_{P,\lambda})| \le \varepsilon$ for $|D| \to \infty$" — the technical core the whole chapter's consistency argument rests on, and this mission's goal.

Setting

Fix a measurable space $Z$, a distribution $P$ on $Z$, a separable Hilbert space $H$, and a measurable $g : Z \to H$. Its $q$-th moment norm, for $q \in (1,\infty)$, is $\|g\|_q := (\mathbb E_P\|g\|_H^q)^{1/q}$ — the direct Hilbert-space analogue of an ordinary $L^q$ norm. The proof machinery behind concentration results of this kind is symmetrization: replacing a centered i.i.d. sum $\frac1n\sum_i(\xi_i - \mathbb E_P\xi_i)$ by a Rademacher-randomized sum $\frac1n\sum_i \varepsilon_i \xi_i$, where a Rademacher sequence $\varepsilon_1,\dots,\varepsilon_n$ is a family of independent $\pm1$-valued random variables, each taking each sign with probability $1/2$. Once randomized, the sum's $L^p$-norms (for different $p$) become comparable to each other via Kahane's inequality, with a universal constant depending only on the two exponents involved — never on the sample size or the ambient Banach space.

Formalization targets

Goal: Lemma 9.2 (concentration of Hilbert-space-valued sample means)

$$P^n\!\left(\left\{(z_1,\dots,z_n) \in Z^n : \left\|\frac1n\sum_{i=1}^n g(z_i) - \mathbb E_P g\right\|_H \ge \varepsilon\right\}\right) \le c_q\left(\frac{\|g\|_q}{\varepsilon\, n^{q^*}}\right)^{q}, \qquad q^* := \min\{1/2,\,1-1/q\}$$

for a universal constant $c_q>0$ depending only on $q$, every $\varepsilon>0$ and every $n \ge 1$. This is a genuine generalization of Chebyshev's inequality to Hilbert-space-valued means, sharp enough (via the explicit rate $n^{-q^*}$) to drive Theorem 9.1's own polynomial regularization condition $\lambda_n^{p^*} n \to \infty$.

Milestones (attack order)

1. Theorem A.8.1 (Symmetrization) — $\mathbb E_P\Psi(\|\frac1n\sum_i(\xi_i-\mathbb E_P\xi_i)\|) \le \mathbb E_P\mathbb E_\nu\Psi(2\|\frac1n\sum_i\varepsilon_i\xi_i\|)$ for convex non-decreasing $\Psi$, i.i.d. $P$-integrable $\xi_i$ valued in a separable Banach space, and a Rademacher sequence $\varepsilon_i$. Directly cited in Lemma 9.2's proof ("Using the symmetrization argument given in Theorem A.8.1...").
2. Theorem A.8.3 (Kahane's inequality) — for a Rademacher sequence, every two $L^p(\nu)$ and $L^q(\nu)$ norms of $\|\sum_i\varepsilon_ix_i\|$ are comparable via a universal constant $K_{p,q}$, independent of $n$ and the Banach space $E$. Directly cited in Lemma 9.2's proof ("If $q\in(1,2]$, we obtain with Kahane's inequality, see Theorem A.8.3, that...").

Theorem 9.1 itself (BRIEF.md's recommended goal — the full SVM-regression consistency theorem) was not attempted this session; see STATUS.md for the reason and the fallback taken instead.

Significance

Lemma 9.2 is stated and proved once, in the Appendix's general Rademacher-sequence toolkit and this chapter, and then used directly to obtain Theorem 9.1's consistency guarantee: substituting $g :=$ the pointwise SVM "difference process" into Lemma 9.2 converts a purely probabilistic concentration fact into a statement about how close the empirical SVM solution's risk is to the population solution's risk, for every sample size. Because the bound depends on nothing but a single moment $\|g\|_q$ — no boundedness, no sub-Gaussian tail — it is what lets Theorem 9.1 avoid assuming the loss or the label distribution has any exponential tail control, which is essential for regression (where $Y \subset \mathbb R$ need not be bounded, unlike the classification setting of this series' earlier chapters). Symmetrization and Kahane's inequality are themselves standard, reusable tools of empirical process theory (used throughout Chapter 7's entropy-number program, excluded from this series, and Chapter 6's classification oracle inequality).

Difficulty

The published proof of Lemma 9.2 is a short but dense computation: Markov's inequality reduces the tail bound to bounding $\mathbb E_{P^n}\|h\|_H^q$ for the centered mean $h$; Theorem A.8.1 symmetrizes; for $q \in (1,2]$, Theorem A.8.3 (Kahane) converts the $q$-th moment of the Rademacher sum to its second moment, which an explicit orthogonality computation (the book's Eq. (9.4), $\mathbb E_{\nu^n}\|\sum_i\varepsilon_ix_i\|^2 = \sum_i\|x_i\|^2$ for any fixed $x_1,\dots,x_n$, an immediate consequence of the Rademacher signs' independence and the Hilbert space's parallelogram identity) reduces to a sum of individual second moments; the case $q>2$ argues analogously with a different exponent split. None of this computation is captured by this mission's two milestones alone — they supply the two cited theorems, not the connecting algebra — so a complete proof of the goal from the milestones as stated still requires reconstructing this argument, exactly as the captain brief's milestones are meant to be (the book's own attack path, not a fully mechanized proof outline).

Formalization scope

$Z$ and $\Theta$ (the Rademacher sequence's own probability space) are arbitrary measurable spaces; $H$ is [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [MeasurableSpace H] [BorelSpace H] [SeparableSpace H] (a separable real Hilbert space with its Borel $\sigma$-algebra), matching "$H$ be a separable Hilbert space" without narrowing to a concrete space (e.g. $\ell^2$) the book itself does not assume. IsRademacherSequence states independence via Mathlib's iIndepFun and the $\pm1$-probability-$1/2$ condition directly, since no ready-made "Rademacher distribution" object exists in this Mathlib revision (checked by search). $q^* := \min\{1/2, 1-1/q\}$ is substituted algebraically rather than introducing a separate conjugate exponent $q'$, since $1/q+1/q'=1$ pins $q'$ down uniquely — not a change of content. In Theorem A.8.3, "for all Banach spaces $E$" quantifies over E : Type (the Type 0 universe) rather than every universe Type*, a disclosed minor restriction with no effect on this mission's own use of the theorem (with $E$ instantiated to a Type* Hilbert space $H$ that is, in every actual application, itself at the Type level).

A trivializing formalization here would drop the "independent" half of IsRademacherSequence (leaving only the marginal $\pm1$-probability-$1/2$ condition, true even for perfectly correlated signs) or drop the "i.i.d." qualifier on $\xi_1,\dots,\xi_n$ in Theorem A.8.1 (both symmetrization and Kahane's inequality are false, or at least unproven by the book's own argument, without independence) — both are ruled out here by stating iIndepFun explicitly rather than only the marginal distribution conditions.

IsRademacherSequence is reusable beyond this mission: any future formalization of Chapter 7's entropy-number/Rademacher-complexity program, or of Chapter 6's oracle inequality's own use of Rademacher averages, would restate it locally (per Hard Rule 9) from the same book definition. Contributions completing the three sorrys are welcome; Theorem 9.1 itself remains a natural, substantially larger follow-up mission built on top of this one's two milestones together with the RKHS/regularized-risk-minimizer apparatus already available in this series' 04-representer mission (restated locally, per Hard Rule 9).

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 9, §§9.1-9.2, pp. 333-337, and Appendix §A.8, pp. 535-537).
• J.-P. Kahane, Some Random Series of Functions, 2nd ed., Cambridge University Press, 1985 (Kahane's inequality, Theorem A.8.3's original source).
• A. W. van der Vaart & J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996 (Lemma 2.3.1, the source of Theorem A.8.1's proof technique).

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.

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

Compressed sensing asks a question that looks impossible at first: can a signal $x\in\mathbb R^n$ be reconstructed exactly from far fewer than $n$ linear measurements $y=Ax\in\mathbb R^m$, $m\ll n$? Classical linear algebra says no — an underdetermined system has infinitely many solutions. But if $x$ is known in advance to be sparse (most of its coordinates are zero), the extra structure makes recovery possible: solving the convex program that minimizes the $\ell_1$ norm of a candidate solution, subject to matching the measurements, recovers $x$ exactly, for a measurement matrix $A$ with a suitable geometric property. This idea, developed by Candès, Romberg, Tao and Donoho in the mid-2000s, underlies modern MRI acceleration, single-pixel cameras, and sparse signal processing generally.

The chapter isolates the exact geometric property a measurement matrix needs — the restricted isometry property (RIP) — and proves, purely by linear algebra with no probability involved, that RIP alone is sufficient for exact recovery by $\ell_1$ minimization. (A companion result, outside this mission, shows random sub-gaussian matrices satisfy RIP with high probability once $m$ is large enough, which is what makes the deterministic guarantee here practically useful; this mission formalizes the deterministic half.)

Setting

For a vector $v$ indexed by a finite set, write $\|v\|_0$ for its number of non-zero coordinates (so $v$ is $s$-sparse if $\|v\|_0\le s$), $\|v\|_1:=\sum_i|v_i|$ for its $\ell_1$ norm, and $\|v\|_2:=\sqrt{\sum_i v_i^2}$ for its Euclidean norm.

An $m\times n$ matrix $A$ satisfies the restricted isometry property (RIP) with parameters $\alpha,\beta,s$ if

$$\alpha\|v\|_2 \;\le\; \|Av\|_2 \;\le\; \beta\|v\|_2 \qquad\text{for every } s\text{-sparse } v\in\mathbb R^n,$$

i.e. $A$ acts as an approximate isometry on every $s$-sparse vector — equivalently (the book's own Exercise 10.5.9), the singular values of every $m\times s$ column-submatrix of $A$ lie in $[\alpha,\beta]$.

Given a matrix $A$ and measurements $y=Ax$ for an unknown sparse $x$, the exact-recovery program is

$$\text{minimize } \|x'\|_1 \quad\text{subject to}\quad y = Ax'.$$

Formalization targets

Goal (Theorem 10.5.10, RIP implies exact recovery)

$$\exists\,\hat x = x \quad\text{whenever}\quad \hat x \text{ solves the exact-recovery program for } y=Ax,$$

precisely: suppose $A$ satisfies RIP with parameters $\alpha,\beta,(1+\lambda)s$ where $\lambda>(\beta/\alpha)^2$; then for every $s$-sparse $x$, every $\hat x$ that is feasible ($A\hat x=Ax$) and $\ell_1$-optimal among feasible vectors satisfies $\hat x=x$. No constant here is hard-coded beyond the book's own explicit threshold $\lambda>(\beta/\alpha)^2$ — the weakest stable form of the claim.

Significance

RIP isolates exactly the geometric mechanism that makes $\ell_1$-minimization work for sparse recovery: once a matrix is known to satisfy it, exact recovery is a deterministic, provable consequence with no appeal to randomness, no failure probability, and no measurement-count formula to verify beyond the RIP parameters themselves. This clean separation — a purely geometric sufficient condition (RIP), proved separately (in the book's Theorem 10.5.11, outside this mission) to hold with high probability for random sub-gaussian matrices — is the template compressed sensing theory follows throughout: geometric/deterministic guarantee first, probabilistic verification that random constructions meet it second. The theorem is one of the two standard routes (with the direct probabilistic argument of Theorem 10.5.1) to the chapter's central claim that $m=O(s\log n)$ measurements suffice to recover any $s$-sparse signal in $\mathbb R^n$ — exponentially fewer than the $n$ measurements a naive linear-algebraic argument would need.

The result itself, and the RIP framework, are classical and well-established (Candès-Tao 2005). This mission formalizes the deterministic linear-algebra core of the argument — the statement infrastructure (RIP, sparsity, the exact-recovery program stated as an explicit optimization problem) and the goal theorem — for a solver to close with a proof.

Difficulty

The natural first idea for showing $\hat x=x$ is to try to bound the recovery error $h:=\hat x-x$ directly using $\|Ah\|_2$ (which vanishes, since both $x$ and $\hat x$ are feasible) together with RIP applied to $h$ itself — but $h$ need not be sparse at all: it is the difference of two sparse-ish vectors and can have full support. The actual argument decomposes $h$'s support into blocks by descending magnitude (the support $I_0$ of $x$, then the $\lambda s$ largest remaining coordinates $I_1$, then the next $\lambda s$, and so on), applies RIP only to the leading block $I_{0,1}=I_0\cup I_1$ (which genuinely has bounded sparsity $\le(1+\lambda)s$), and separately bounds the contribution of every later block using the fact that $\hat x$ is $\ell_1$-optimal (so $\|h_{I_0^c}\|_1\le\|h_{I_0}\|_1$, the "cone constraint"): each later block's $\ell_2$ norm is controlled by the $\ell_1$ mass of the previous block divided by its size. This is a genuinely multi-step argument combining a purely geometric fact (RIP on one bounded-sparsity block) with a purely combinatorial one (the magnitude-sorted decomposition), and the "obvious" idea of applying RIP to $h$ as a whole does not typecheck, since RIP says nothing about vectors with more than $(1+\lambda)s$ non-zero entries.

Formalization scope

Vectors are plain functions ι → ℝ on a finite index type, not EuclideanSpace ℝ ι: the latter's fixed $\ell_2$ norm instance cannot also host the $\ell_1$ norm the program's objective needs, so both norms (L2Norm, L1Norm) are defined directly by their defining sums on the same underlying type. Sparsity (Sparsity) takes a real-valued threshold s : ℝ, matching that the RIP parameter $(1+\lambda)s$ used by the goal theorem is a real number even at integer base sparsity. A solution $\hat x$ "of the program" is formalized as an explicit argmin membership — feasibility (A.mulVec xhat = A.mulVec x) conjoined with optimality over the exact feasible set (∀ x', A.mulVec x' = A.mulVec x → l1Norm xhat ≤ l1Norm x') — never "there exists an estimator such that", the trivialization risk this chapter's own triage brief flags explicitly (shared with Chapter 3's Max-Cut): an existential reading would prove a different, strictly weaker statement. The conclusion is stated for every such $\hat x$, not one witness, matching that RIP forces uniqueness.

This mission covers Theorem 10.5.10 only, as the sole item; the probabilistic goal Theorem 10.5.1 (exact recovery for random sub-gaussian measurement matrices, which needs Theorem 10.5.10 together with a separate probabilistic argument, Theorem 10.5.11, that random matrices satisfy RIP), and the Lasso guarantee (Theorem 10.6.1), are both left out for lack of session time: each would need a fresh probabilistic apparatus (independent isotropic sub-gaussian random rows, a failure-probability bound) built from scratch in this chapter's own sub-namespace, with no reusable published definition from an earlier chunk. L2Norm, L1Norm, Sparsity and RIP are reusable by any later chapter or mission needing sparse vectors or the restricted isometry property; solvers' contributions are welcome on completing the proof of Theorem 10.5.10 itself (the magnitude-sorted support decomposition sketched under Difficulty above), and, beyond this mission's current scope, on Theorem 10.5.11 and Theorem 10.5.1.

Selected references

• E. J. Candès, T. Tao, Decoding by linear programming, IEEE Transactions on Information Theory 51 (2005), 4203–4215. https://doi.org/10.1109/TIT.2005.858979
• D. L. Donoho, Compressed sensing, IEEE Transactions on Information Theory 52 (2006), 1289–1306. https://doi.org/10.1109/TIT.2006.871582
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 10. https://doi.org/10.1017/9781108231596

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.

From "larger" to "larger in every direction"

Chapter I's usual stochastic order compares two real-valued random variables by "how large" they tend to be. Chapter VI lifts the same idea to random vectors: $X$ is smaller than $Y$ in the usual multivariate stochastic order if $X$ is less likely than $Y$ to land in any upper set of $\mathbb{R}^n$ — any region defined by "at least this large in every coordinate." This mission formalizes that order and its two founding characterizations: a coupling theorem (the direct $n$-dimensional generalization of Chapter I's own coupling theorem) and a common-source representation, plus two closure properties that make the order usable in practice.

The usual multivariate stochastic order

Let $X$ be a random vector taking values in $\mathbb{R}^n$ on a probability space $(\Omega,\mu)$, and let $Y$ be a random vector taking values in $\mathbb{R}^n$ on a (possibly different) probability space $(\Omega',\nu)$. $X$ is smaller than $Y$ in the usual multivariate stochastic order, written $X \le_{st} Y$, if

$$P\{X\in U\} \le P\{Y\in U\} \quad \text{for every upper set } U\subseteq\mathbb{R}^n,$$

where an upper set is one closed upward under the coordinatewise partial order on $\mathbb{R}^n$ ($x\le y$ iff $x_i\le y_i$ for every $i$). Equivalently, $X\le_{st}Y$ iff $E[\varphi(X)]\le E[\varphi(Y)]$ for every increasing $\varphi:\mathbb{R}^n\to\mathbb{R}$ (increasing with respect to that same coordinatewise order) for which the two expectations exist — the form this mission drafts as the definition, exactly parallel to the univariate order's own equivalent form.

Formalization targets

Goal: the coupling characterization (Theorem 6.B.1)

$$X \le_{st} Y \iff \exists\,(\Omega'',\rho),\ \hat X,\hat Y:\Omega''\to\mathbb{R}^n\text{ with } \hat X=_{st}X,\ \hat Y=_{st}Y,\ P\{\hat X\le\hat Y\}=1.$$

This is the direct $n$-dimensional generalization of Chunk 01's Theorem 1.A.1: a joint law on the random vectors' shared space realizing $X\le_{st}Y$ as an almost-sure coordinatewise inequality between copies. The book does not give this direction's proof here (an explicit construction appears later, in a special case irrelevant to a statements-only mission), and the claim is exactly as citable either way.

Supporting milestones

• Theorem 6.B.2, the common-source restatement: $X\le_{st}Y$ iff there is a real-valued random variable $Z$ and $\mathbb{R}^n$-valued functions $\psi_1\le\psi_2$ (coordinatewise, at every $z\in\mathbb{R}$) with $X=_{st}\psi_1(Z)$, $Y=_{st}\psi_2(Z)$ — the multivariate analogue of Theorem 1.A.2, an immediate restatement of the goal.
• Theorem 6.B.16(b), closure under conjunctions: independent $X_i\le_{st}Y_i$ ($i=1,\dots,m$) give $\psi(X_1,\dots,X_m)\le_{st}\psi(Y_1,\dots,Y_m)$ for any increasing $\psi:\mathbb{R}^k\to\mathbb{R}$ — note the codomain $\mathbb{R}$, so this closure conclusion is itself the univariate order applied to vector-valued inputs. Specializing $\psi$ to a coordinatewise sum gives closure under convolutions.
• Theorem 6.B.16(c), closure under marginalization: $X\le_{st}Y$ implies $X_I\le_{st}Y_I$ for every sub-index set $I\subseteq\{1,\dots,n\}$ — a special case of part (b), included separately for its own simple, widely-used content.

Significance

The usual multivariate stochastic order is the natural tool for comparing random vectors — costs, resource-usage profiles, portfolio returns — that must be ranked simultaneously across several coordinates rather than reduced to a single scalar summary first. It underlies simulation comparisons (via the coupling and common-source characterizations, both constructive), reliability comparisons of multi-component systems (whose component lifetimes are naturally vector-valued), and comparative-statics arguments in queueing and inventory models with several state variables. The closure properties are what make the order compositional: conjunction closure says a vector-by-vector comparison of independent inputs survives any coordinatewise-increasing post-processing, and marginalization closure says a joint comparison restricts consistently to any sub-collection of coordinates — together they are the two properties an analyst reaches for first when reducing a multivariate comparison to a more tractable one.

No platform prior art exists: GET /theorems?q=stochastic+order and q=coupling return zero genuine hits (checked at this book's triage time, re-confirmed this session). This mission restates the usual multivariate stochastic order and its two founding theorems as a self-contained foundation, in the same spirit as Chunk 01's univariate mission but independently drafted, since drafts cannot import each other's Lean.

Difficulty

The chief formalization risk this chapter's own brief flags is conflating "increasing" for $\varphi:\mathbb{R}^n\to\mathbb{R}$ with some order other than the coordinatewise one (a total order via a fixed embedding, or a lexicographic order): the book's order on $\mathbb{R}^n$ is always the componentwise partial order, and Mathlib gives Fin n → ℝ exactly that order by default (its Pi/product order), so Monotone φ for φ : (Fin n → ℝ) → ℝ already means what the book means with no extra predicate to get wrong — but it would be easy to instead encode ℝ^n-valued objects some other way (e.g. a fixed linear functional into ℝ) that silently swaps in a different, weaker order. The second risk is Theorem 6.B.16(b)'s literal codomain: the book states $\psi:\mathbb{R}^k\to\mathbb{R}$ (scalar), so the closure conclusion is a genuinely univariate stochastic-order statement about $\psi$ applied to vector inputs, not a vector-to-vector closure (that is part (a), not drafted here) — stating it as a multivariate conclusion by mistake would silently strengthen a theorem the book does not claim.

Formalization scope

Random vectors are drafted as functions into Fin n → ℝ from arbitrary measurable spaces, which inherit Mathlib's default coordinatewise (Pi) order — the same order the book uses throughout this chapter, requiring no separate order predicate. MultivariateOrder μ ν X Y quantifies over φ : (Fin n → ℝ) → ℝ with Monotone φ in that order and Integrable (φ ∘ X) μ/Integrable (φ ∘ Y) ν stated inside the ∀, exactly matching "for which the expectations exist." Equality in law is ProbabilityTheory.IdentDistrib. Theorem 6.B.2's random variable $Z$ is drafted as $\mathbb{R}$-valued specifically (not an arbitrary-type common source), matching the book's own "for all $z\in\mathbb{R}$" quantification exactly.

Theorem 6.B.16(b) is drafted for a common dimension $n$ across all $X_i,Y_i$ rather than the book's per-$i$ dimension $k_i$: the concatenated input then lives in Fin m → Fin n → ℝ (nested Pi types, carrying the coordinatewise order on $\mathbb{R}^{mn}$ exactly as needed), avoiding a dependent-sum concatenation of vectors of genuinely different lengths that a mission of this size does not justify. This is the "closed under convolutions" special case the book itself names as a corollary of the general statement, not a different claim — but it is a genuine restriction of scope, recorded here rather than silently applied, and the general varying-dimension statement is left for a future pass (see STATUS.md). The theorem's conclusion is stated as the univariate order's own defining inequality on ℝ (∀ x, μ {ω | x < ψ(X_∙ ω)} ≤ ν {ω | x < ψ(Y_∙ ω)}), restated locally rather than importing Chunk 01's UsualOrder, since drafts cannot import another mission's definitions. Theorem 6.B.16(c)'s sub-index set $I\subseteq\{1,\dots,n\}$ of size $k$ is encoded as an injective reindexing r : Fin k → Fin n, with $X_I,Y_I$ drafted as X, Y precomposed coordinatewise with r, matching the book's own subvector notation (6.A.1) exactly.

A trivializing formalization this mission rules out: drafting MultivariateOrder with an order on Fin n → ℝ other than the coordinatewise one (for instance, a fixed linear functional collapsing the vector to a scalar and reusing the univariate order), which would silently state a different, generally weaker order under the same name; and drafting Theorem 6.B.16(b)'s conclusion with a vector-valued (rather than the book's literal scalar-valued) $\psi$, which would silently strengthen a theorem the book states only for real-valued $\psi$. This mission draws on no platform prior art (searches for "stochastic order" and "coupling" as of 2026-09-18 return zero genuine matches). Reusable beyond this mission: the MultivariateOrder definition pattern and its coupling/common-source characterization parallel Chunk 01's univariate pair closely enough that a future chapter needing a multivariate order's own coupling theorem (Chapter VII's multivariate convex order is the direct next instance in this series) 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 6 (Multivariate Stochastic Orders), §6.A–6.B. https://doi.org/10.1007/978-0-387-34675-5
• This series' Chunk 01 (StochasticOrders.Usual), for the univariate usual stochastic order and its coupling/common-source characterizations this chapter directly generalizes.

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