Probability

Motivation

Regularization — adding a penalty on model complexity to an empirical risk minimization objective — is one of the oldest and most reliably effective tools in statistical learning: ridge regression, LASSO, and margin-based support vector machines all fit this template. For decades the regularization weight and penalty function were chosen heuristically or by cross-validation, with only asymptotic or worst-case generalization bounds explaining why they help. Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter on Wasserstein distributionally robust optimization (DRO) gives regularization a different, non-asymptotic justification: a decision rule that is robust to adversarial perturbations of its training data, measured in Wasserstein distance, is exactly a regularized empirical risk minimizer — no approximation, no asymptotics. This mission formalizes the general form of that equivalence, Theorem 10 (p. 14), which underlies every regularization-by-robustification result the chapter derives for classification and regression alike.

Setting

Fix a normed space $\Xi = \mathbb{R}^m$, a convex loss function $\ell : \Xi \to \mathbb{R}$, a radius $\varepsilon \ge 0$, and $N$ training samples $\hat\xi_1,\dots,\hat\xi_N \in \Xi$ ($N \ge 1$). The empirical distribution is $\hat P_N = \frac{1}{N}\sum_{i=1}^N \delta_{\hat\xi_i}$. The worst-case risk of $\ell$ at radius $\varepsilon$ (eq. (6), p. 6) is

$$R_{\varepsilon,p}(\hat P_N,\ell) = \sup_{Q \in B_{\varepsilon,p}(\hat P_N)} E_Q[\ell(\xi)],$$

where $B_{\varepsilon,p}(\hat P_N)$ is the type-$p$ Wasserstein ball of radius $\varepsilon$ around $\hat P_N$ (Definition 1, p. 3) — the set of probability measures on $\Xi$ within Wasserstein distance $\varepsilon$ of the empirical distribution, under a norm $\|\cdot\|$ on $\Xi$ and its transportation exponent $p$. The Lipschitz modulus $\mathrm{Lip}(\ell) = \sup_{\xi\ne\xi'} \frac{|\ell(\xi)-\ell(\xi')|}{\|\xi-\xi'\|}$ (possibly $+\infty$) measures how fast $\ell$ can grow.

Formalization targets

Goal (Theorem 10, convex loss and $p=1$). If $\ell$ is convex and $p=1$, then the worst-case risk of $\ell$ over the type-1 Wasserstein ball around the empirical distribution coincides with the Lipschitz-regularized empirical loss:

$$R_{\varepsilon,1}(\hat P_N,\ell) = R(\hat P_N,\ell) + \varepsilon \cdot \mathrm{Lip}(\ell),$$

where $R(\hat P_N,\ell) = \frac{1}{N}\sum_{i=1}^N \ell(\hat\xi_i)$ is the ordinary empirical risk. The left side is the worst-case expected loss under adversarial perturbations of the training data of bounded aggregate Wasserstein cost; the right side is the ordinary empirical risk plus a regularization term proportional to the perturbation radius $\varepsilon$ and the loss's own Lipschitz modulus — no approximation, an exact equality for every convex $\ell$.

Significance

This is the single result underlying every specific regularization-by-robustification corollary the chapter derives — the $\ell_2$-regularized SVM and its $\ell_1$/$\ell_\infty$ variants, regularized logistic regression, and the regression analogue with a Lipschitz loss (Proposition 3) — because each of those is obtained by substituting a specific convex, Lipschitz loss (hinge, logloss, a linear-model margin loss) for the general $\ell$ here and reading off $\mathrm{Lip}(\ell)$ in closed form. Theorem 10 is exact ($p=1$, Ξ = R^m) precisely because a type-1 transportation cost is dual to the Lipschitz modulus (a consequence of the Kantorovich- Rubinstein duality this book's earlier duality theorems establish), whereas the corresponding statement for $p \ge 2$ (Theorem 11 elsewhere in the chapter) needs a strictly stronger hypothesis on $\ell$. Formalizing Theorem 10 fixes, machine-checkably, the exact scope of the equivalence — which losses qualify (convex, no boundedness or smoothness needed), which transportation exponent is required ($p=1$, not any $p\ge1$), and that the equality is exact, not an upper or lower bound — the single fact every classification- and regression-specific robustification corollary in the chapter cites without re-deriving.

Difficulty

The natural first attempt treats the worst-case risk as an instance of the general finite convex reduction (Theorem 8, which needs $\ell$ or a related concave/convex-conjugate structure and applies for a general norm exponent $p,q$ with $1/p+1/q=1$) and specializes it to $p=1$. This is not the paper's own route for Theorem 10: at $p=1$ the dual exponent $q=\infty$, and the general finite-convex-program reduction (11) degenerates in a way that is more naturally derived directly from the type-1 Wasserstein distance's own dual (Kantorovich-Rubinstein) representation — a Lipschitz test function pairs exactly with a type-1 transportation cost, which is why the answer is Lipschitz-regularization and not some other penalty. The Lean statement records only the final equality (the proof itself, via Theorem 8 or the direct Kantorovich-Rubinstein route, is left as sorry, as required for a draft item), but the choice of which milestones would support that proof is exactly this: the type-1/Lipschitz-modulus duality is a structurally different argument from the finite-convex-program machinery Theorem 8 needs for other $p$, which is why this chapter's earlier draft mistakenly tried to reach a specialization of Theorem 10 (Proposition 2, restated for a labeled, $\kappa=\infty$ ambiguity set) through a finite-atom shortcut that does not actually capture the general type-1 ball Theorem 10's own proof needs — see Formalization scope.

Formalization scope

$\Xi$ is EuclideanSpace ℝ (Fin m) (fixed to Set.univ, matching the theorem's own "Ξ = R^m" hypothesis) with an arbitrary fixed norm as a type-class parameter, not specialized to Euclidean. The worst-case risk, Wasserstein distance, ambiguity set, nominal risk, empirical distribution and Lipschitz modulus are all redefined locally in this chapter's own namespace, verbatim restatements of 01-duality's own drafts of the same objects (identical EReal/ENNReal/Integrable conventions), because 01-duality is not yet a published mission (CAPTAIN_ADDENDUM_WAVE2.md rule 5); a later upload can retire the duplication once it is live. hN : 0 < N excludes the empty-sample case the paper's own "N training samples" presupposes; hℓ : Integrable ℓ (empiricalDistribution ξhat) guards the empirical risk's Bochner integral (automatically satisfied under any real-valued ℓ since the empirical distribution is a finite convex combination of Dirac masses, but stated explicitly rather than assumed silently). No constant is pinned to a numeral. This mission originally targeted Proposition 2 (regularization by robustification for classification, p. 25), a specialization of Theorem 10 to a labeled, κ=∞ input-output ambiguity set — but that draft's κ=∞ ambiguity set restricted admissible perturbations to a finite family of exactly N atoms, each sample's entire mass moving as one indivisible unit, which is a strict, non-faithful subset of the true κ=∞ Wasserstein ball (splitting a sample's mass across several destinations is a legitimate, and for a convex loss strictly more powerful, perturbation by Jensen's inequality). This made the goal theorem false for at least one of the three loss functions (Table 1) the mission itself certified as covered (logloss), not merely narrower than the paper's claim — moderation caught this and required either a faithful general-ambiguity-set reformulation or retargeting the goal. This mission takes the latter: Theorem 10 itself, already correctly and generally stated using the unrestricted Wasserstein ball throughout, is now the goal, with no further milestone (no other numbered result in this chunk's scope is needed for Theorem 10's own statement beyond the shared definitions above). A future mission in this series can revisit Proposition 2/3 with a properly general labeled ambiguity set once that construction (label-pinned marginal plus an aggregate coupling condition on the input coordinate, rather than a finite atom family) is built.

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research. https://doi.org/10.1287/educ.2019.0198
• Shafieezadeh-Abadeh, S., Esfahani, P. M., & Kuhn, D. (2015). Distributionally robust logistic regression. Advances in Neural Information Processing Systems, 28.
• Blanchet, J., Kang, Y., & Murthy, K. (2019). Robust Wasserstein profile inference and applications to machine learning. Journal of Applied Probability, 56(3), 830–857.

Motivation

A decision maker who solves a distributionally robust optimization (DRO) problem over a Wasserstein ball chooses a radius $\varepsilon$ by hand, and it is natural to ask what guarantee that choice actually buys: how large must $\varepsilon$ be, as a function of the sample size $N$ and a desired confidence level, before the resulting worst-case risk is provably not an underestimate of the true (unknown-distribution) risk? Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter answers this for the mean-covariance relaxation of Wasserstein DRO introduced via the Gelbrich hull (Section 2.3): Theorem 21 gives a concentration inequality for how fast the sample mean and covariance approach the true mean and covariance, and Theorem 22 turns that concentration bound into a finite-sample statistical guarantee for the Gelbrich risk itself. This mission formalizes both.

Setting

Fix $m \in \mathbb{N}$. Let $P$ be the unknown true distribution on $\mathbb{R}^m$ with mean vector $\mu$ and covariance matrix $\Sigma \in S^m_+$, and suppose $P$ is light-tailed: there exist $\alpha > 2$ and $A > 0$ with $E_P[\exp(\|\xi\|_2^\alpha)] \le A$. Let $\hat\xi_1,\dots,\hat \xi_N$ be $N$ independent, identically distributed samples from $P$; write $P^N$ for their joint law (the $N$-fold product measure) and $\hat\mu, \hat\Sigma$ for the resulting sample mean and sample covariance, i.e. the mean and covariance of the empirical distribution $\hat P_N = \frac{1}{N}\sum_i \delta_{\hat\xi_i}$. Recall from the Gelbrich construction the mean-covariance uncertainty set $U_\varepsilon(\hat\mu,\hat\Sigma) = \{(\mu,\Sigma) \in \mathbb{R}^m \times S^m_+ : \|\hat\mu-\mu\|_2^2 + \mathrm{Tr}[\hat\Sigma+\Sigma-2(\hat\Sigma^{1/2} \Sigma\hat\Sigma^{1/2})^{1/2}] \le \varepsilon^2\}$, and the Gelbrich risk $R_\varepsilon(\hat\mu,\hat\Sigma,\ell) = \sup_{Q \in G_\varepsilon(\hat\mu,\hat\Sigma)} E_Q[\ell(\xi)]$ of a loss function $\ell$ over the Gelbrich hull $G_\varepsilon(\hat\mu,\hat \Sigma)$.

Formalization targets

Milestone (Theorem 21, concentration inequalities II). There is $c > 1$, depending on $P$ only through $\mu,\Sigma,\alpha,A,m$ (not on any finer feature of $P$), such that for every $\eta \in (0,1]$,

$$P^N\big[(\mu,\Sigma) \in U_\varepsilon(\hat\mu,\hat\Sigma)\big] \ge 1-\eta \quad \text{whenever} \quad \varepsilon \ge \varepsilon_N(\eta) := \frac{\log(c/\eta)}{\sqrt N}.$$

Goal (Theorem 22(a), finite sample guarantees II). Under the same hypotheses, for every $\eta \in (0,1)$ and $\varepsilon \ge \varepsilon_N(\eta)$,

$$P^N\Big\{R(P,\ell) \le R_\varepsilon(\hat\mu,\hat\Sigma,\ell) \;\; \forall \ell \in L\Big\} \ge 1-\eta.$$

With probability at least $1-\eta$ over the draw of the training sample, the Gelbrich risk computed from that sample upper-bounds the true risk of every admissible loss function simultaneously — not just of one fixed $\ell$ chosen in advance. (The paper's part (b), the analogous guarantee $P^N\{R(P,\ell^\star) \le R_\varepsilon(\hat\mu,\hat\Sigma,\ell^\star)\} \ge 1-\eta$ for the specific optimizer $\ell^\star$ of the Gelbrich risk minimization problem, is not formalized in this mission — see Formalization scope.)

Significance

Theorem 22 is what makes the Gelbrich-risk relaxation of Wasserstein DRO more than a computational convenience: it certifies that solving the tractable Gelbrich risk minimization problem gives a decision whose true out-of-sample risk is, with high probability, no worse than the value the solver reports — a genuine confidence guarantee, not merely an approximation of the Wasserstein worst-case risk. Theorem 21's rate, $\varepsilon_N(\eta) = O(N^{-1/2})$, is also of independent interest: it is dimension-free (no curse of dimensionality), in contrast to the paper's earlier general-distribution concentration result (Theorem 18, out of scope for this mission) whose rate degrades with $m$. Formalizing Theorem 21 fixes, machine-checkably, the exact functional form of $\varepsilon_N(\eta)$ and the precise sense in which $c$ is "distribution-free" given $(\mu,\Sigma,\alpha,A,m)$ — a subtlety easy to state informally but easy to get wrong formally (see Difficulty).

Difficulty

The central formalization difficulty is not proving the theorems (both are left as sorry in this draft) but stating the existential constant $c$ correctly. The paper says $c$ "depends on $P$ only through $\mu,\Sigma,\alpha,A,m$" — informally, a promise that $c$ is uniform across every distribution $P$ sharing those five parameters, not merely that some $c$ exists for each $P$ separately (a vacuously true, much weaker statement obtained by naively quantifying $c$ after $P$). The correct encoding places $\exists c$ before the universal quantifier over $P$: for fixed $(\mu,\Sigma,\alpha,A,m)$, one $c$ must work for every $P$ with that mean, covariance, and tail bound. Getting this quantifier order backwards silently converts a genuine finite-sample guarantee into a triviality (FAITHFULNESS_TRAPS.md trap 8).

Formalization scope

Distributions live on EuclideanSpace ℝ (Fin m); $P^N$, the law of $N$ iid samples, is the $N$-fold product measure MeasureTheory.Measure.pi (fun _ => P) on Fin N → EuclideanSpace ℝ (Fin m) — an event about the random sample sequence is a set of such tuples, and "$P^N[\text{event}] \ge 1-\eta$" is that product measure's mass on the event set. All risk and uncertainty-set definitions (meanVector, covarianceMatrix, meanCovarianceUncertaintySet, gelbrichHull, gelbrichRisk, nominalRisk, empiricalDistribution) are redefined locally in this chapter's own namespace, matching 02-gelbrich's conventions exactly, since neither 01-duality nor 02-gelbrich is yet a published mission (CAPTAIN_ADDENDUM_WAVE2.md rule 5); a later upload can retire the duplication once those missions are live. The existential constant c is placed before the universal quantifier over P in both theorems, exactly capturing "depends on P only through µ,Σ,α,A,m" — see Difficulty. Only Theorem 22's part (a) (the uniform bound over a loss class L) is formalized; part (b) — the bound for the specific optimizer ℓ* of the Gelbrich risk minimization problem (19) — is left out, because it requires first formalizing "ℓ* is an optimizer of problem (19)" as an object (an infimum-attaining selection over a data-dependent optimization problem), which is additional infrastructure this mission's time budget did not cover; formalizing it as an unconditional bound over an arbitrary data-dependent ℓ* (dropping the optimality hypothesis) would be unfaithful — the guarantee genuinely depends on ℓ* being an optimizer, not an arbitrary measurable function of the sample. The goal theorem also carries hΞ, stating Ξ contains the support of P (the paper's own standing assumption, p. 6, for every later use of Ξ), and hLInt, an Integrable ℓ P guard for every ℓ ∈ L, matching Assumption 1 (p. 9); both were added after moderation found the goal's original statement, without them, admitted a counter-instance (Ξ = ∅ collapses the Gelbrich hull to empty and the risk supremum to ⊥, making the guarantee provably false rather than merely undisclosed). Theorem 18 (the general, dimension- dependent concentration inequality with its piecewise ε_N(η) formula) and Theorems 19/20/23 (its downstream guarantees and the asymptotic-consistency results) are out of scope for this mission, which targets the Gelbrich-risk branch (Theorems 21/22) specifically.

Selected references

• Kuhn, D., Mohajerin Esfahani, P., Nguyen, V. A., & Shafieezadeh-Abadeh, S. (2019). Wasserstein Distributionally Robust Optimization: Theory and Applications in Machine Learning. INFORMS TutORials in Operations Research. https://doi.org/10.1287/educ.2019.0198
• Fournier, N., & Guillin, A. (2015). On the rate of convergence in Wasserstein distance of the empirical measure. Probability Theory and Related Fields, 162(3), 707–738.
• Gao, R., & Kleywegt, A. J. (2023). Distributionally robust stochastic optimization with Wasserstein distance. Mathematics of Operations Research, 48(2), 603–655.

Comparing random outcomes without comparing numbers

Operations research and applied probability are full of questions of the shape "is X riskier, larger, or later than Y?" when X and Y are random: two queueing disciplines' waiting times, two inventory policies' shortfall, two insurance portfolios' claim size. Comparing their means answers a weaker question than the modeler usually wants, since two distributions can share a mean while one is uniformly the "worse" one to face. Shaked and Shanthikumar's Stochastic Orders (Springer, 2007) is the standard reference for the family of orders built to make "X is stochastically no larger than Y" precise, and this mission formalizes the foundational member of that family: the usual stochastic order, together with its central structural theorem.

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

$$P\{X > x\} \le P\{Y > x\} \quad \text{for every } x \in (-\infty,\infty).$$

Equivalently, $P\{X \le x\} \ge P\{Y \le x\}$ for every $x$: $Y$'s cumulative distribution function never exceeds $X$'s. Two features of the definition matter for everything that follows. First, it is a comparison of distributions, not of jointly defined variables — $X$ and $Y$ need not live on the same probability space, and the order depends only on their laws. Second, the inequality must hold for every threshold $x$ simultaneously; it is not a comparison of two summary statistics such as means or medians, and a distribution can fail $X \le_{st} Y$ even while $E[X] \le E[Y]$.

A closely related order compares residual lifetimes rather than raw tail probabilities. $X$ is smaller than $Y$ in the hazard rate order, written $X \le_{hr} Y$, if the survival functions $\bar F(x) = P\{X>x\}$, $\bar G(x) = P\{Y>x\}$ satisfy $\bar F(x)\bar G(y) \ge \bar F(y)\bar G(x)$ for all $x \le y$ — the general, density-free form of the condition that for absolutely continuous distributions reduces to a pointwise comparison of hazard rates $r(t) = f(t)/\bar F(t)$. It is one of several stronger orders (alongside the likelihood ratio order) that the book shows all imply $\le_{st}$, and it is the mission's second definition.

Formalization targets

Goal: the coupling characterization (Theorem 1.A.1)

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

This is the order's Strassen-type coupling theorem: $X \le_{st} Y$ holds exactly when copies of $X$ and $Y$ can be realized on one common probability space so that, almost surely, the copy of $X$ never exceeds the copy of $Y$. It is the weakest possible statement with this shape (existence of some coupling on some space, not a canonical one), and it is the archetype every later chapter's own coupling theorem — for the hazard rate order, the convex order (via a martingale coupling), the multivariate orders — restates for its own comparison.

Supporting milestones

• Theorem 1.A.2, the same characterization restated via a common random source: $X \le_{st} Y$ iff there is a random variable $Z$ and functions $\psi_1 \le \psi_2$ with $X =_{st} \psi_1(Z)$ and $Y =_{st} \psi_2(Z)$.
• Theorem 1.A.3(a), closure under monotone transformations: $X \le_{st} Y$ and $g$ increasing gives $g(X) \le_{st} g(Y)$ (reversed for $g$ decreasing).
• Theorem 1.A.3(b), closure under increasing functions of independent families and, as its corollary, under convolution: independent $X_i \le_{st} Y_i$ and $\psi$ increasing gives $\psi(X_1,\dots,X_m) \le_{st} \psi(Y_1,\dots,Y_m)$, in particular $\sum_i X_i \le_{st} \sum_i Y_i$.
• Theorem 1.B.1, the first link of the book's implication chain: $X \le_{hr} Y \implies X \le_{st} Y$.

Significance

The usual stochastic order is the weakest and most widely used of the book's orders, and the coupling theorem is the tool that makes it tractable: comparing tail probabilities for every threshold is an infinite family of inequalities, while exhibiting one coupling on one space settles the comparison in a single stroke. This is the technique behind, among many applications in the book and the wider literature, comparing waiting times across queueing disciplines, bounding the effect of parameter uncertainty on a risk measure, and proving monotonicity results for Markov chains by coupling their sample paths. The closure properties (Theorem 1.A.3) are what let such comparisons survive composition with a monotone payoff function or a sum of independent components — exactly the operations a queueing or inventory model performs on its primitives.

Formalizing this theorem establishes, in one place, both the statement and the exact shape of its existential witness (a genuine ∃ over a probability space and two identically distributed random variables, not merely two abstractly-known-to-exist objects), which is the piece every later chapter's own coupling theorem in this series needs to get right independently. No proof is attempted in this mission; the book's own three-line construction ($\hat X = F^{-1}(U)$, $\hat Y = G^{-1}(U)$ for a uniform $U$) is a natural target for a future proof-bearing pass.

Difficulty

The definitional trap is the "for all $x$" in $\le_{st}$: it is tempting to shortcut it into a comparison of one summary statistic (a mean, an essential supremum, a specific quantile), which is uniformly weaker and would make Theorem 1.A.1 either false or a different, easier theorem. The coupling theorem itself has a second trap in its existential structure: the common probability space $(\Omega'',\rho)$ must be genuinely quantified — fixed neither to $\Omega$ nor $\Omega'$ in advance — and "$\hat X =_{st} X$" is equality of the two random variables' laws, not almost-sure equality of $\hat X$ and $X$ themselves (they typically do not share a domain before the construction). Theorem 1.A.3(b)'s general statement, for an arbitrary increasing $\psi:\mathbb{R}^m \to \mathbb{R}$ on independent families, is easy to understate as only its convolution corollary; the book gives both, and the general statement is the one with the actual content (the sum is recovered by taking $\psi$ to be the coordinate sum, itself increasing).

Formalization scope

Random variables are represented as measurable functions into $\mathbb{R}$ from arbitrary measurable spaces, and "equality in law" is Mathlib's native ProbabilityTheory.IdentDistrib, which is defined for two (possibly different) probability spaces and requires almost-everywhere measurability rather than fixing an ambient space in advance — matching the book's own treatment of $X \le_{st} Y$ as a comparison between distributions. UsualOrder μ ν X Y and HazardRateOrder μ ν X Y both take $X:\Omega\to\mathbb{R}$ on $(\Omega,\mu)$ and $Y:\Omega'\to\mathbb{R}$ on a separate $(\Omega',\nu)$, so no theorem here can be trivialized by silently forcing $X$ and $Y$ onto one shared space. HazardRateOrder is stated via the survival-function cross-product inequality (Eq. 1.B.4), the form that needs no absolute-continuity hypothesis, rather than via a derivative-based hazard rate, so it applies to the same general random variables as UsualOrder without an extra regularity hypothesis the book itself does not require at this level of generality. Independence in Theorem 1.A.3(b) is Mathlib's ProbabilityTheory.iIndepFun; the random variable $Z$ of Theorem 1.A.2 is left valued in an arbitrary measurable space, matching the book's unrestricted statement, rather than narrowed to $\mathbb{R}$-valued for convenience. A trivializing formalization is ruled out explicitly: $\le_{st}$ is not formalized as a comparison of means, medians, or any single moment, and the coupling theorems' ∃ is a genuine existential over a probability space, not a hypothesis smuggling in the witness's existence.

This mission draws on no platform prior art (repeated searches for "stochastic order", "coupling", "Strassen" and "identically distributed" turned up nothing on-topic as of 2026-09-18); it is the first mission in a nine-chapter series covering the whole book, and its own definitions are not imported by later chapters — each restates locally what it needs, per the series' own convention that draft items cannot import another draft's definitions. Reusable beyond this mission: the UsualOrder/HazardRateOrder shape (parametrizing over two separate probability spaces) is the pattern every later chapter's own order definition follows.

Selected references

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

Motivation

High-dimensional data is often computationally expensive to work with and hard to visualize. The Johnson-Lindenstrauss lemma answers a striking question in this setting: can any finite set of points, no matter how high-dimensional the ambient space, be squeezed into a space of dimension depending only on the number of points (logarithmically) and the desired accuracy, while barely disturbing the distances between them? The answer is yes, and — remarkably — a single, data-independent random construction (a random Gaussian matrix) achieves it with positive probability for any point set. This mission formalizes the lemma and the two probabilistic results its proof is built from.

Setting

For a set $V$ of $m$ points in $\mathbb R^N$, a map $f:\mathbb R^N\to\mathbb R^k$ is a $(1\pm\epsilon)$-distance-preserving embedding of $V$ if $(1-\epsilon)\|u-v\|^2\le\|f(u)-f(v)\|^2\le(1+\epsilon)\|u-v\|^2$ for every $u,v\in V$. The book's proof constructs $f=A/\sqrt k$ from a random matrix $A\in\mathbb R^{k\times N}$ with i.i.d. standard normal ($N(0,1)$) entries, and argues by the probabilistic method: for a fixed pair of points, Lemma 15.3 shows $f$ preserves their squared distance up to $(1\pm\epsilon)$ with probability at least $1-2e^{-(\epsilon^2-\epsilon^3)k/4}$, because the ratio $\|f(x)\|^2/\|x\|^2$ (for $x$ the difference of the two points) is exactly a $\chi^2_k$ random variable, whose two-sided concentration around its mean $k$ is Lemma 15.2. A union bound over the $O(m^2)$ pairs in $V$ then shows the probability that every pair is simultaneously preserved is still strictly positive — so a map with the desired property must exist, even though no single fixed matrix is exhibited.

Formalization targets

Lemma 15.2 (Chi-squared concentration, milestone). If $Q\sim\chi^2_k$, then for $0<\epsilon<1/2$, $P[(1-\epsilon)k\le Q\le(1+\epsilon)k]\ge1-2e^{-(\epsilon^2-\epsilon^3)k/4}$.

Lemma 15.3 (Gaussian random projection distortion, milestone). For $x\in\mathbb R^N$, $k<N$, and $A\in\mathbb R^{k\times N}$ with i.i.d. $N(0,1)$ entries,

$$P\Big[(1-\epsilon)\|x\|^2\le\big\|\tfrac1{\sqrt k}Ax\big\|^2\le(1+\epsilon)\|x\|^2\Big] \ge1-2e^{-(\epsilon^2-\epsilon^3)k/4}.$$

Lemma 15.4 — the mission's goal (Johnson-Lindenstrauss). For $0<\epsilon<1/2$, integer $m>4$, and $k=20\log(m)/\epsilon^2$, any set $V$ of $m$ points in $\mathbb R^N$ admits a map $f:\mathbb R^N\to\mathbb R^k$ with $(1-\epsilon)\|u-v\|^2\le\|f(u)-f(v)\|^2\le(1+\epsilon) \|u-v\|^2$ for all $u,v\in V$.

Significance

This is one of the cleanest instances in the book of the probabilistic method: existence is proved without exhibiting the object, by showing a random construction succeeds with positive probability. The target dimension $k=O(\log m/\epsilon^2)$ is independent of the ambient dimension $N$ — the embedding works no matter how large the original feature space is, which is exactly why the lemma has inspired random-projection methods throughout dimensionality reduction, streaming algorithms, and compressed sensing. Prior art on the Prove2Me platform is not faithful here: HighDimProb.Isoperimetry.johnson_lindenstrauss (Vershynin series) proves a Johnson-Lindenstrauss-type bound, but via a uniformly-random $m$-dimensional subspace and its orthogonal projection, rescaled by $\sqrt{n/m}$ — a genuinely different construction from this book's explicit i.i.d.-Gaussian-matrix map $f=A/\sqrt k$, and with different (existentially quantified, unspecified) constants rather than this book's explicit $k=20\log(m)/\epsilon^2$. The two are classically known to give essentially the same qualitative guarantee, but showing them equivalent would require an independent equivalence proof neither platform item nor this mission undertakes; per the chunk's own brief, the Vershynin theorem is cited here only as related work, not reused as a kind: reference item.

Not formalized here: Theorem 15.1 (the PCA solution), the chapter's other headline result. BRIEF.md explicitly flags PCA and JL as the chapter's two independent capstones, not a proof chain, and recommends dropping PCA if the mission focuses purely on JL. Theorem 15.1's proof is an Eckart-Young-type Frobenius-norm optimization argument over the set of rank-$k$ orthogonal projection matrices — sharing no definitions, hypotheses, or proof technique with the probabilistic-method argument this mission's three items are built from. Formalizing it would mean standing up a second, unrelated piece of mathematics (constrained matrix optimization, singular value decomposition) from scratch for a single additional item; per the captain brief's guidance to leave out, rather than approximate, material disproportionate to the time budget, it is omitted. §15.2 (kernel PCA) and §15.3 (Isomap, LLE, Laplacian eigenmaps) are likewise out of scope, per BRIEF.md's own page-range restriction — applications- heavy manifold-learning material with no numbered result feeding Lemma 15.4's proof.

Difficulty

Lemma 15.2's proof is a genuine Chernoff-bound argument: apply Markov's inequality to $\exp(\lambda Q)$, substitute the chi-squared distribution's own moment-generating function $(1-2\lambda)^{-k/2}$, and optimize the resulting bound over $\lambda\in(0,1/2)$ by calculus (the book's own choice $\lambda=\epsilon/(2(1+\epsilon))$ is exactly the minimizer) — not a one-line union of tail bounds, and the same argument must be repeated (with a sign flip) for the lower tail before combining via a union bound. Lemma 15.3's proof needs the non-obvious observation that $T_j=\widehat x_j/\|x\|$ (for $\widehat x=Ax$) are themselves i.i.d. standard normal — a consequence of $A$'s i.i.d. Gaussian entries and $\mathbb E[\widehat x_j^2]=\|x\|^2$, not immediate from the definitions alone — before the sum of their squares can be recognized as exactly a $\chi^2_k$ variable and Lemma 15.2 applied. Lemma 15.4's own proof, while conceptually simple (a single union bound), needs the specific numerical accounting $2m^2e^{-(\epsilon^2-\epsilon^3)k/4}=2m^{5\epsilon-3}<2m^{-1/2}$ at the chosen $k=20\log(m)/\epsilon^2$ and $\epsilon\le1/2$ to conclude the success probability is strictly positive — a formalization that merely asserted "the union bound gives a positive probability" without this exact accounting would not establish the book's specific, tight constant $k=20\log(m)/\epsilon^2$.

Formalization scope

SqNorm is the coordinate-wise squared Euclidean norm (∑ᵢ vᵢ²), used in place of Mathlib's EuclideanSpace/PiLp norm typeclass machinery to keep the statements close to the book's own concrete ℝ^N/ℝ^k-coordinate notation. IsChiSquaredMGF states the moment-generating-function characterization of a chi-squared distribution that the proof of Lemma 15.2 itself cites (Eq. C.25), rather than restating the book's own Definition C.7, which sits in an out-of-chapter appendix not read for this mission; this is checked (in SELF_REVIEW.md) to be a faithful, uniquely-determining substitute, since a real random variable's law is determined by its MGF wherever it is finite near 0. IsIIDStandardGaussianMatrix states "i.i.d. standard normal entries" via Mathlib's gaussianReal 0 1 (marginal law) together with iIndepFun (joint independence). The goal theorem's target dimension k is taken as ⌈20 log(m)/ε²⌉ (Nat.ceil) rather than the book's real-valued 20 log(m)/ε², since a map's codomain dimension must be a natural number; this rounding only strengthens (never weakens) the existential conclusion, since the union-bound success probability is monotonically increasing in k. No numerical constant in any of the three items is otherwise altered from the book's own displayed form. A trivializing formalization this mission avoids: stating Lemma 15.4 with an unspecified k = O(log m/ε²) (an asymptotic, not an explicit constant) — per BRIEF.md's own naming of this as one of the series' "explicit-constant" results, k's exact formula 20 log(m)/ε² (up to the ceiling needed for well-typedness) is stated directly.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 15, §15.4.
• W. B. Johnson, J. Lindenstrauss, "Extensions of Lipschitz mappings into a Hilbert space," Contemporary Mathematics 26, 1984, 189-206.
• S. Vempala, The Random Projection Method, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, 2004.

Motivation

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

Setting

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

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

Formalization targets

Goal — Theorem 6.23 (thresholding-based covariance estimation)

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

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

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

Milestone — Theorem 6.17 (the matrix Bernstein bound)

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

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

Ranking is the learning problem behind search engines, recommendation systems and fraud-alert triage: what matters is not a single classification decision but the relative order the system assigns to a set of items, because a user or analyst can only act on the very top of a ranked list. Chapter 10 develops margin-based generalization theory for the score-based ranking setting, transplanting chunk 05-svm's single-sample Rademacher-complexity machinery to a genuinely two-sample structure: a ranking example is a pair of points, one drawn from each of two positions, and the chapter's bound must therefore control two marginal complexities rather than one. It also introduces RankBoost, the ranking analogue of AdaBoost, with a boosting-style empirical-error guarantee proved by the same normalization-factor telescoping argument as chunk 07's AdaBoost bound, adapted to RankBoost's own pairwise per-round quantities.

Setting

A ranking example is a pair (x,x') drawn from a distribution D over X×X, labeled by a preference function f; restricted to {-1,+1} labels (the simplification §10.2 adopts), a scoring function h:X→ℝ misranks (x,x') when f(x,x')(h(x')-h(x)) ≤ 0 (Eq. 10.1/10.2). The empirical margin loss R̂_{S,ρ}(h) (Eq. 10.3) uses the same Φ_ρ (Definition 5.5) as chunk 05-svm, restated locally here. Writing S1, S2 for the two coordinate projections of a pair sample S, and D1, D2 for the corresponding marginals of D, R_m^{D1}(H) and R_m^{D2}(H) are the Rademacher complexities of H under each marginal (p. 241). Theorem 10.1 bounds R(h) in terms of these two Rademacher-complexity terms, both in their population form (R_m^{D1}, R_m^{D2}) and their empirical form (R̂_{S1}, R̂_{S2}), via chunk 03's Theorem 3.3 applied through an auxiliary hypothesis family H̃ = {((x,x'),y) ↦ y[h(x')-h(x)]}. Corollary 10.2 specializes this to kernel-based linear scoring hypotheses; §10.4 introduces RankBoost (Figure 10.1), whose per-round weighted pairwise-outcome fractions ε_t^+, ε_t^- (Eq. 10.11) play the role AdaBoost's single ε_t plays in chunk 07, and Theorem 10.3 bounds RankBoost's empirical error in terms of them. Corollary 10.4 combines Theorem 10.1 with Lemma 7.4 (the convex hull of H has the same empirical Rademacher complexity as H, restated as a standing fact of the boosting series) to give RankBoost's own margin-based guarantee.

Formalization targets

Theorem 10.1 — the mission's goal. For H a set of real-valued functions, ρ>0, δ>0, with probability at least 1-δ, for all h∈H:

$$R(h) \le \hat R_{S,\rho}(h) + \tfrac2\rho(R_m^{D_1}(H)+R_m^{D_2}(H)) + \sqrt{\tfrac{\log(1/\delta)}{2m}}$$ $$R(h) \le \hat R_{S,\rho}(h) + \tfrac2\rho(\hat R_{S_1}(H)+\hat R_{S_2}(H)) + 3\sqrt{\tfrac{\log(2/\delta)}{2m}}.$$

Corollary 10.2 (milestone). For a PDS kernel K with r an upper bound on K(x,x), feature map Φ, and H = {x↦w·Φ(x) : ‖w‖≤Λ}, fixed ρ>0: R(h) ≤ R̂_{S,ρ}(h) + 4√(r²Λ²/ρ²/m) + √(log(1/δ)/(2m)).

Theorem 10.3 (milestone). RankBoost's empirical error verifies R̂_S(f) ≤ exp(-2∑_t((ε_t^+-ε_t^-)/2)²), and ≤ exp(-2γ²T) if the edge is uniformly at least γ>0.

Corollary 10.4 (milestone). Theorem 10.1's first bound, applied to h∈conv(H).

Significance

Theorem 10.1's proof is the chapter's genuine new technique, not a restatement of chunk 05's Theorem 5.8: the two-sample decomposition (splitting the supremum over H̃ into a term on x' alone and a term on x alone, each bounded by the Rademacher complexity under its own marginal) is what the 2/ρ · (R_m^{D1}+R_m^{D2}) structure expresses, and collapsing it to a single-sample bound would either be false or silently assume D1=D2 (which only holds for a symmetric D, an assumption the theorem does not make). Corollary 10.2 is the direct theoretical basis for the ranking SVM algorithm §10.3 derives. Theorem 10.3 mirrors chunk 07-boosting's Theorem 7.2 almost line for line in its proof technique (the same telescoping product of normalization factors Z_t), but with genuinely different per-round quantities (ε_t^+, ε_t^- rather than a single ε_t) that must not be conflated with AdaBoost's own, per BRIEF.md's pitfall note. Corollary 10.4 is what makes RankBoost's output (a linear, not convex, combination — normalized by ‖α‖_1) provably generalize independently of the number of boosting rounds T, the ranking analogue of chunk 07's Corollary 7.5. No prior art exists on the platform: GET /theorems?q=ranking%20loss returns zero hits.

Difficulty

Theorem 10.1's proof needs the two-sample structure carried through explicitly: H̃'s Rademacher complexity splits, via the sub-additivity of sup and the fact that y_iσ_i and σ_i have the same distribution, into a term on S2 alone and a term on S1 alone — treating a ranking sample as an ordinary single sample (chunk 03's single-hypothesis-set machinery applied naively) would drop this structure entirely and is exactly the pitfall BRIEF.md names. Theorem 10.3's proof requires Z_t = ε_t^0 + 2√(ε_t^+ε_t^-) be bounded via the identity 4ε_t^+ε_t^- = (1-ε_t^0)^2 - (ε_t^+-ε_t^-)^2 and the inequality 1-x ≤ e^{-x} — the same telescoping-normalizer technique as AdaBoost's Theorem 7.2, but RankBoost's own D_t, ε_t^+, ε_t^- genuinely differ (they are defined via pairwise outcomes y_i(h(x'_i)-h(x_i)) ∈ {-1,0,+1}, not a single-point disagreement h(x_i)≠y_i) and must be modeled as their own recursively-defined algorithm state, not obtained by substitution into chunk 07's AdaBoost Lean.

Formalization scope

MarginLossFunction restates chunk 05-svm's Definition 5.5; EmpiricalRademacherComplexity/ RademacherComplexity restate chunk 03-rademacher-vc's Definitions 3.1/3.2; IsPDS restates chunk 06-kernels's PDS-kernel definition; ConvHull restates chunk 07-boosting's convex-hull definition — all duplicated rather than imported since a draft item cannot import another chunk's draft module, and none is listed as reusable in missions/README.md's "Published definitions" table at the time of this session. D1, D2 are computed directly as Measure.map Prod.fst D/Measure.map Prod.snd D rather than posited via a separate marginal hypothesis, so the theorem statement itself pins down that they are genuinely the marginals of the sampling distribution D, not independent parameters. Corollary 10.2's r is an explicit upper bound on K(x,x) (hrK : ∀ x, K x x ≤ r) rather than a literal sSup, per BRIEF.md's pitfall note about the possibly-infinite supremum — the theorem's conclusion is monotonic in r, so this is not a weakening. RankBoost's D_t, ε_t^+, ε_t^-, α_t, Z_t and returned function f are modeled as their own recursively-defined algorithm state (mirroring chunk 07's AdaBoostDist/AdaBoostEpsilon/AdaBoostEnsemble pattern exactly, but built from RankBoost's own pairwise-outcome quantities, never by substituting into the AdaBoost Lean, per BRIEF.md's pitfall note) — RankBoostEpsilonPlus/RankBoostEpsilonMinus are already tied to RankBoost's own D_t and selected base ranker, so Theorem 10.3 needs no separate hypothesis connecting them (the same trivialization guard chunk 07's own Theorem 7.2 documents). No numerical constant is altered from the book in any of the four theorems.

Not formalized: §10.3's ranking-SVM primal/dual optimization problems (an algorithm derived from Corollary 10.2, not a generalization-theoretic result); §10.4.2 (RankBoost as coordinate descent, an algorithmic-equivalence argument, not a generalization bound); §10.5 (bipartite ranking, its own distinct problem formulation with a different generalization error, Eq. 10.20, explicitly out of scope per BRIEF.md); §10.6-10.7 (preference-based ranking, other criteria), out of scope per BRIEF.md. The uniform-over-ρ extension mentioned after both Theorem 10.1's and Corollary 10.2's proofs (referencing Theorem 5.9's technique from a different chapter) is not drafted, matching chunk 09-multiclass's identical scope decision for the analogous remark.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 10 (§10.1-10.4).
• Y. Freund, R. Iyer, R. E. Schapire, Y. Singer, "An efficient boosting algorithm for combining preferences," JMLR 4, 2003 (RankBoost's origin).
• C. Cortes, M. Mohri, "AUC optimization vs. error rate minimization," NeurIPS 2003 (the ranking-SVM connection §10.3 develops).

Motivation

Every convergence-rate result in the preceding chapters is an upper bound: some specific estimator (the Lasso, PCA, kernel ridge regression) achieves a given error rate. A natural and much harder question is the complementary one: is that rate actually the best any procedure could achieve, no matter its computational cost? Answering this requires a theory of lower bounds that holds simultaneously for every conceivable estimator — a fundamentally different kind of argument from constructing and analyzing one particular algorithm. Wainwright's High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 15, develops this theory, unifying classical techniques (Le Cam, Assouad, Fano) under one reduction: converting continuous estimation into discrete hypothesis testing.

Setting

Let $\mathcal X$ be a sample space and $\mathcal P$ a class of probability distributions on $\mathcal X$. A functional $\theta: \mathcal P \to \Omega$ assigns each distribution a parameter of interest. An estimator is a measurable map $\hat\theta: \mathcal X \to \Omega$. Fix a semi-metric $\rho:\Omega\times\Omega\to[0,\infty)$ — symmetric, triangle-inequality-satisfying, $\rho(\theta,\theta)=0$, but possibly $\rho(\theta,\theta')=0$ for $\theta\ne\theta'$ — and an increasing $\Phi:[0,\infty)\to[0,\infty)$. The minimax risk is

$$\mathfrak M\bigl(\theta(\mathcal P); \Phi\circ\rho\bigr) \;:=\; \inf_{\hat\theta} \sup_{P\in \mathcal P} \mathbb E_P\bigl[\Phi\bigl(\rho(\hat\theta, \theta(P))\bigr)\bigr],$$

the smallest worst-case expected loss achievable by any measurable estimator (Eq. (15.2)).

Given a 2δ-separated set $\{\theta_1,\dots,\theta_M\} \subseteq \theta(\mathcal P)$ (every pair satisfies $\rho(\theta_j,\theta_k)\ge 2\delta$) with representative distributions $P_{\theta_1},\dots,P_{\theta_M}$, Wainwright constructs a testing problem: sample $J$ uniformly from $[M]$, then $Z\sim P_{\theta_J}$; write $Q$ for the resulting joint law of $(J,Z)$. A test function $\psi:\mathcal X\to[M]$ attempts to recover $J$ from $Z$; its error probability is $Q[\psi(Z)\ne J]$.

Formalization targets

Goal (Proposition 15.1, "From estimation to testing")

For any increasing $\Phi$ and any 2δ-separated set with its induced joint testing measure $Q$,

$$\mathfrak M\bigl(\theta(\mathcal P); \Phi\circ\rho\bigr) \;\ge\; \Phi(\delta) \inf_{\psi} Q\bigl[\psi(Z)\ne J\bigr].$$

This mission formalizes Proposition 15.1 alone (see Formalization scope below for why, and what a follow-up mission would add to reach Fano's method proper, Proposition 15.12).

Significance

Proposition 15.1 is the single reduction every subsequent technique in the chapter specializes: Le Cam's two-point method (Lemma 15.9, $M=2$, bounding the testing error via total variation distance), Fano's method (Proposition 15.12, bounding it via mutual information $I(Z;J)$ and Fano's inequality), and Assouad's method (a different, hypercube-based packing). Formalizing it in full generality — general $\Phi$, general semi-metric, general $M$-ary packing set — gives a single reusable lemma that a future mission proving any of these specific bounds can build on directly, rather than re-deriving the reduction each time.

The theorem is already proved in the source; this mission's contribution is a machine-checked formal statement (and, eventually, proof) of the reduction, in a form composing with any future formalization of the chapter's testing-error bounds (total variation, Fano, or otherwise).

Difficulty

The proof combines two ingredients that must each be kept in their sharpest form: Markov's inequality applied to $\Phi(\rho(\hat\theta,\theta))$ (which only needs $\Phi$ increasing, not convex or any specific shape — a premature specialization to $\Phi(t)=t^2$ would silently prove a weaker, less reusable statement), and the reduction of any estimator to a test via nearest- packing-point assignment (Eq. (15.4)), which uses the triangle inequality on $\rho$ in a specific direction (bounding $\rho(\theta_k,\hat\theta)$ from below via $\rho(\theta_j,\theta_k)$ and $\rho(\theta_j,\hat\theta)$) to show that a small estimation error forces the induced test to be correct. Getting the direction and strictness of every inequality right — non-strict separation, but strict distance in the "test is correct" event — is where a naive restatement goes wrong.

Formalization scope

$\mathcal X$, $\Omega$ are arbitrary measurable spaces; the distribution class $\mathcal P$ is realized as an indexed family measure : Idx → Measure 𝒳 rather than a bare set of measures, composing directly with θ : Idx → Ω. The semi-metric $\rho$ is a bare function with explicit nonnegativity/reflexivity/symmetry/triangle-inequality hypotheses, matching the book's own footnote definition, rather than Mathlib's PseudoMetricSpace typeclass (kept self-contained, no extra instance machinery). The minimax risk is valued in ENNReal via the lower Lebesgue integral ∫⁻, not the Bochner integral, specifically to avoid the non-integrable-loss junk value 0 that a Bochner-integral formalization would silently introduce — a trivializing formalization would use ∫ (Bochner) here, letting a non-integrable loss vanish and making the inequality easier to satisfy than the book's actual claim; this mission does not do that. The joint testing measure $Q$ is characterized by its slice-measure equations directly on the product space $[M]\times\mathcal X$, avoiding Mathlib's general conditional/disintegration machinery while remaining exactly equivalent to "$J$ uniform, $Z\mid J=j\sim P_{\theta_j}$".

Disclosed major scope decision. BRIEF.md recommended Proposition 15.12 (the Fano bound itself, Φ(δ)(1 - (I(Z;J)+\log 2)/\log M)) as this mission's goal. That statement requires, in addition to everything above, a formalized notion of mutual information $I(Z;J)$ between a finite-valued and a general (possibly continuous) random variable, and its use of a Fano-type inequality (Eq. (15.31), itself deferred by the book to "Section 15.4" and not fully quoted in the brief). Building a faithful mutual-information formalization general enough for this setting (finite $J$, arbitrary measurable $Z$) — matching Mathlib's or this repo's existing, narrower information-theoretic developments (SourceCoding.*, built for a different, channel-coding purpose per BRIEF.md's own prior-art note) or building one from scratch — is substantially more than this session's remaining budget after building and self-reviewing 08-pca and 07-sparse-linear. This mission instead formalizes Proposition 15.1, the foundational reduction Proposition 15.12 itself specializes (via a particular bound on $\inf_\psi Q[\psi(Z)\ne J]$), so that a follow-up mission can add the mutual-information/Fano step on top of HighDimStat.Minimax.estimation_to_testing without redoing this reduction. This mission's name, fixed from missions/README.md, still names "Fano's Method" as the series slot this chunk occupies; its actual content is the reduction step every method in that family (including Fano's) shares — recorded explicitly here and in STATUS.md, not left implicit.

Selected references

• Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 15. DOI: 10.1017/9781108627771.
• Le Cam, L. "Convergence of estimates under dimensionality restrictions." Annals of Statistics, 1(1), 1973, 38–53.
• Fano, R. M. Transmission of Information: A Statistical Theory of Communications. MIT Press, 1961.
• Yu, B. "Assouad, Fano, and Le Cam." In Festschrift for Lucien Le Cam, Springer, 1997, 423–435.

Ordering how strongly two variables move together

The first eight chapters of Shaked and Shanthikumar's Stochastic Orders (Springer, 2007) compare single random variables — location, variability, convexity. Chapter IX turns to a different question: given two coordinates of a random vector, how strongly do they tend to move together? "Large values of $X_1$ go with large values of $X_2$" is a qualitative property (positive dependence); comparing how much two bivariate distributions exhibit it, holding their individual marginals fixed, is what this chapter's positive dependence orders make precise. This mission formalizes the two central ones — the PQD order and the supermodular order — and the supermodular order's closure properties, the chapter's own capstone result.

The PQD and supermodular orders

Let $X=(X_1,\dots,X_n)$ and $Y=(Y_1,\dots,Y_n)$ be two random vectors, with joint survival function $\bar F(x)=P\{X_1>x_1,\dots,X_n>x_n\}$ and joint distribution function $F(x)=P\{X_1\le x_1,\dots,X_n\le x_n\}$ (similarly $\bar G, G$ for $Y$). $X$ is smaller than $Y$ in the PQD order, written $X\le_{PQD}Y$, if

$$\bar F(x)\le\bar G(x)\ \text{ and }\ F(x)\le G(x) \quad\text{for every }x\in\mathbb{R}^n.$$

(It follows, though it need not be assumed, that $X$ and $Y$ then share the same univariate marginals — the two inequalities together pin the marginals down, unlike a single one alone.) This is Lehmann's positive-quadrant-dependence order in its general multivariate form: $Y$'s coordinates cluster together, in both the upper and lower "quadrants," at least as strongly as $X$'s.

A function $\varphi:\mathbb{R}^n\to\mathbb{R}$ is supermodular if $\varphi(x)+\varphi(y)\le\varphi(x\wedge y)+\varphi(x\vee y)$ for the coordinatewise meet/join — the function-level notion the platform's Topkis/Supermodularity series already formalizes for games and lattices, reused here directly. $X$ is smaller than $Y$ in the supermodular order, written $X\le_{sm}Y$, if $E[\varphi(X)]\le E[\varphi(Y)]$ for every supermodular $\varphi$ for which the two expectations exist. Because the indicator of any upper or lower orthant is itself supermodular, $X\le_{sm}Y\implies X\le_{PQD}Y$ (Eq. 9.A.17): the supermodular order is strictly finer than the PQD order, and for $n=2$ the two coincide.

Formalization targets

Goal: closure properties of the supermodular order (Theorem 9.A.9(a),(c))

$$(X_1,\dots,X_n)\le_{sm}(Y_1,\dots,Y_n) \implies (g_1(X_1),\dots,g_n(X_n))\le_{sm}(g_1(Y_1),\dots,g_n(Y_n))$$

whenever every $g_i$ is increasing, or every $g_i$ is decreasing (part a); and

$$X\le_{sm}Y \implies X_I\le_{sm}Y_I \quad\text{for every } I\subseteq\{1,\dots,n\}$$

(part c, closure under marginalization). These are two of Theorem 9.A.9's five closure properties — the theorem the brief for this mission recommends as its goal — chosen as the ones that need no further definitional machinery beyond the orders themselves (composition and a coordinate projection, both plain pushforwards of the vector's law).

Supporting milestone

• Theorem 9.A.4, the general multivariate closure of the PQD order under independent pairing: if $X\le_{PQD}Y$, $U\le_{PQD}V$, with $X,U$ independent and $Y,V$ independent, then $(\varphi_1(X_1,U_1),\dots,\varphi_n(X_n,U_n))\le_{PQD}(\varphi_1(Y_1,V_1),\dots,\varphi_n(Y_n,V_n))$ for all increasing $\varphi_i$ — the closure property the chapter opens with (as Theorem 9.A.1, the bivariate case), generalized to $n$ dimensions.

Significance

Positive dependence orders formalize a comparison operations research and risk management need constantly but rarely state precisely: two portfolios, insurance lines, or queueing networks with identical individual risk profiles can still differ sharply in how their components co-move, and that co-movement — not the marginals — is often what drives tail risk, correlated failures, or aggregate variability. The supermodular order is the standard tool for comparing this directly: Theorem 9.A.9's closure properties are what let a comparison established for primitive components survive the operations a model actually performs on them — relabeling by a monotone transform (part a), reading off a subset of coordinates (part c), combining independent sub-vectors (part b), conditioning on a covariate (part d), or passing to a distributional limit (part e). Chapter VI's multivariate stochastic order and Chapter VII's multivariate convex order are the two other multivariate orders in the book; the supermodular order is the one built specifically to compare dependence structure rather than location or spread, and it connects directly to the platform's existing Topkis/Supermodularity series, whose function-level predicate this mission reuses rather than restates.

Formalizing Theorem 9.A.9 fixes the exact shape a supermodular-order closure claim takes when built as a pushforward of the vector's law — the natural Mathlib-idiomatic rendering once the order is stated on laws rather than on variables tied to a fixed ambient space — for any future mission in this series or elsewhere that needs to state a closure property of a vector-valued stochastic order. No proof is attempted; both drafted parts of Theorem 9.A.9 have short book proofs (part (a) from the fact that composing a supermodular function with all-increasing or all-decreasing coordinate maps is again supermodular; part (c) the book calls "easy to prove"), making them plausible future proof targets.

Difficulty

The chapter's central definitional trap is that the PQD order's defining condition — even in its general multivariate form — determines the marginals as a consequence of the two joint inequalities holding together, not as a separate hypothesis to add; adding same-marginals as an extra explicit condition on top of Eqs. (9.A.13)-(9.A.14) would not be false, but it would present as a hypothesis something the theorem's own two conditions already force. A second trap is specific to Theorem 9.A.9(a): the $g_i$ must be uniformly increasing or uniformly decreasing across all coordinates, not an arbitrary per-coordinate mix — a mixed-monotonicity version is a materially different, unproven claim, since it is exactly the all-same-direction condition that keeps a composition with a supermodular function supermodular. A third, more basic trap common to every function-class order in this book: "for every supermodular $\varphi$" must be a genuine universal quantifier with the two expectations' existence stated as an explicit hypothesis, not a global assumption or a specific test function standing in for the whole class.

Formalization scope

Unlike the univariate orders formalized elsewhere in this series (which take random variables $X:\Omega\to\mathbb{R}$, $Y:\Omega'\to\mathbb{R}$ on two possibly-different probability spaces), PQDOrder and SupermodularOrder here are stated directly on the two vectors' laws — measures $P,Q$ on $\iota\to\mathbb{R}$ for a finite index type $\iota$ — since the book's own comparisons never reference a joint law of $X$ and $Y$ together, only their separate distributions. This is also what lets Theorem 9.A.9(a)'s coordinatewise composition and (c)'s marginalization be stated as plain pushforwards (Measure.map) of one law, without carrying an ambient sample space through the statement. The index type is left an arbitrary finite type (Fintype ι, not fixed to Fin n) so the same two declarations serve both a full $n$-vector and any marginal sub-vector obtained by restricting to a subset $I$ of coordinates — the shape Theorem 9.A.9(c) itself needs. Supermodularity reuses the platform's own Supermodularity.Monotonicity.SupermodularOn (from the Topkis series, via a kind: reference item) with its relativizing set argument fixed to Set.univ, its plain unrelativized form — checked to match the book's φ(x)+φ(y)≤φ(x∧y)+φ(x∨y) on ι → ℝ's own coordinatewise lattice structure exactly, not a games- or player-scoped variant. Independence in Theorem 9.A.4 is formalized by taking the joint law of the two independent vectors to be the product measure of their marginals — the standard way to construct an independent coupling with prescribed marginals — rather than adding a separate independence hypothesis about pre-existing random variables. Measurable hypotheses are added on every map a Measure.map is taken along, guarding against the pushforward's junk-zero-measure convention for a non-measurable map; none narrows what the book's own theorems claim, since every map used (a monotone/antitone composition, a coordinate projection) is genuinely measurable. A trivializing formalization is ruled out explicitly: the supermodular quantifier ranges over the reused, already-audited Topkis predicate rather than a hand-rolled or restricted one, and the "for all increasing $\varphi_i$" of Theorem 9.A.4 is a genuine universal over jointly-monotone functions of two arguments, not a fixed example.

This mission draws on the platform's own Topkis/Supermodularity series for its supermodular function-level building block (Supermodularity.Monotonicity.SupermodularOn, reused as a reference item — the strongest prior-art connection of the whole nine-chapter series, per the series plan) but on no prior art for the orders themselves (repeated searches for "PQD", "positive dependence", "Fréchet bound" and "supermodular" returned nothing on-topic beyond the Topkis series as of 2026-09-18). Reusable beyond this mission: the laws-only, arbitrary-Fintype- index formalization pattern is available to any later mission in this series needing a multivariate order (Chapter VI's multivariate stochastic order, Chapter VII's multivariate convex order) that wants marginalization or coordinatewise composition stated as plain pushforwards.

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
• E. L. Lehmann, "Some concepts of dependence", Annals of Mathematical Statistics, 37(5), 1966, 1137–1153. https://doi.org/10.1214/aoms/1177699260

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).

Counting terms and comparing the resulting sums

Chapters III and IV formalize what it means for one random variable to be "more spread out" or "larger and more spread out" than another. Chapter VIII asks a different kind of question: if the number of terms in a sum of i.i.d. random variables is itself random, and one count is larger than another in one of these orders, does the resulting random sum inherit the comparison? This mission formalizes the chapter's own answer — Theorem 8.A.13 — a clean, self-contained closure result that needs only the icx/icv/cx orders from Chunks 03/04 (restated locally) and one nonnegative-integer-valued index, without the heavier parametric-family apparatus (SICX, SICV, SIL, and the stochastic-convexity-of-a-family notions) that occupies most of the rest of the chapter.

The icx/icv/cx orders, restated for this chapter

This chapter restates the univariate increasing convex, increasing concave and convex orders (Chunks 04 and 03's own subjects) locally, since drafts cannot import another mission's definitions: for random variables $X,Y$, $X\le_{icx}Y$ [$X\le_{icv}Y$] if $E[\varphi(X)]\le E[\varphi(Y)]$ for every increasing convex [concave] $\varphi:\mathbb{R}\to\mathbb{R}$ for which the expectations exist, and $X\le_{cx}Y$ if the same holds for every convex $\varphi$ (dropping "increasing"). Theorem 8.A.13 applies these same three orders to nonnegative-integer-valued random variables $M,N$ — a special case of the real-valued order (after the coercion $\mathbb{N}\to\mathbb{R}$), not a separate discrete order, per this chapter's own pitfall 1.

Formalization target

Goal: closure of the icx/icv/cx orders under random sums (Theorem 8.A.13)

Let $\{Y_k, k\in\mathbb{N}_{++}\}$ be i.i.d. nonnegative random variables, independent of the two nonnegative discrete random variables $M$ and $N$. Then

$$M\le_{icx}[\le_{icv}]\,N \implies \sum_{k=1}^{M}Y_k \le_{icx}[\le_{icv}]\sum_{k=1}^{N}Y_k, \qquad M\le_{cx}N \implies \sum_{k=1}^{M}Y_k \le_{cx}\sum_{k=1}^{N}Y_k.$$

Comparing the number of terms propagates to a comparison of the resulting random sums. This is "an application of these notions in establishing a stochastic inequality," in the book's own words right before the theorem — the formal content behind Example 8.A.2's claim that a homogeneous Poisson process is SIL, via the semigroup property of Example 8.A.7 (neither a numbered theorem, so neither is drafted as a milestone here — cited as background only, per CAPTAIN_BRIEF.md rule 5).

The book's proof defines $\psi(n) = E[\varphi(\sum_{k=1}^n Y_k)]$ for an increasing convex [concave] $\varphi$ and observes (via the unnumbered Example 8.A.4) that $\psi$ is itself increasing and convex [concave] in $n$; the icx/icv order on $M,N$ then transfers directly to $\psi(M)$ vs. $\psi(N)$, giving part (a). Part (b) follows from part (a) together with the equal-means fact $E[\sum_{k=1}^M Y_k]=E[\sum_{k=1}^N Y_k]$ under $M\le_{cx}N$ (Theorem 4.A.35, a Chapter 4 result not restated in this mission).

Significance

Random sums are the natural model for aggregate risk, total service time, or total demand when the number of contributing terms is itself uncertain — the number of claims in an insurance period, the number of customers served, the number of jobs in a batch. Theorem 8.A.13 is the tool that lets an analyst reduce a comparison of two such aggregates to a comparison of the (often much simpler) counting processes that generate them, without having to reason about the joint distribution of the sums directly. It is also the concrete instance, stripped of the rest of the chapter's parametric-family machinery, of a pattern that recurs throughout the book: an order on an index set (here, the count $M$ vs. $N$) transferring through a monotone/convex construction (here, summation) to an order on the resulting random variables — the same shape Chunk 06's Theorem 6.B.16(b) and Chunk 07's Theorem 7.A.9 each illustrate in their own settings.

No platform prior art exists: GET /theorems?q=random+sum, q=compound+distribution, q=Poisson+process, and q=renewal return nothing usable (the last returns only MarkovMixing/CLT-adjacent hits, not classical renewal or compound-sum results, confirmed at triage time and re-checked this session). This mission restates the icx/icv/cx orders and their random-sum closure as a self-contained result, independently drafted since drafts cannot import Chunks 03/04's Lean.

Difficulty

The chief formalization risk is treating $M\le_{icx}N$ as a separate "discrete" order rather than the same real-valued order applied to $\mathbb{N}$-valued random variables after coercion — this chapter's own pitfall 1. A second risk is drafting $\sum_{k=1}^{M}Y_k$ as a fixed-length sum with $M$ substituted in afterward, rather than a genuine random (randomly-stopped) sum where $M$ is itself random and independent of the $\{Y_k\}$ sequence — this chapter's own pitfall 2; the independence hypothesis has to be carried explicitly, not left as an unstated convention. A third risk, common to every bracketed theorem in this series, is conflating the icx and icv cases of part (a) into a single Or-joined statement rather than two clearly distinguished conjuncts — this chapter's own pitfall 3.

A different kind of risk, specific to this chapter, is scope creep into the parametric-family apparatus (SI, SCX, SICX, SIL, and the "family indexed by $\theta\in\Theta$" definitions) that occupies most of Chapter 8: as BRIEF.md's own Setup note observes, that apparatus is heavier than the rest of the book (a family, a parameter set, and several bracketed cases per definition), and a trivializing risk specific to it — flagged in this chapter's pitfall 4 — is a family predicate that is vacuously true for a degenerate parametrization (e.g. $\Theta$ a singleton). This mission avoids that risk entirely by choosing the one clean, self-contained closure theorem in the chapter that needs none of it.

Formalization scope

The icx/icv/cx orders are restated locally (IcxOrder, IcvOrder, ConvexOrder, univariate, real-valued), exactly matching Chunks 04 and 03's own shapes, since drafts cannot import another mission's definitions. $M,N:\Omega\to\mathbb{N}$ are nonnegative-integer-valued; the orders are applied to them via the coercion fun ω => (M ω : ℝ) (resp. N), matching pitfall 1 exactly — no separate discrete-order predicate is introduced. The i.i.d. sequence is drafted as Y : ℕ → Ω → ℝ (indexing Y 0, Y 1, … for the book's Y_1, Y_2, …, a one-step reindexing noted explicitly rather than left implicit), with iIndepFun Y μ for mutual independence and IdentDistrib (Y j) (Y k) μ μ for every j, k for identical distribution, plus 0 ≤ᵐ[μ] Y k for nonnegativity. The random sum itself is ∑ k ∈ Finset.range (M ω), Y k ω — a genuine randomly-stopped sum, per pitfall 2 — and independence of $\{Y_k\}$ from $(M,N)$ jointly is IndepFun (fun ω => (M ω, N ω)) (fun ω k => Y k ω) μ, treating the whole sequence as one ℕ → ℝ-valued random element, stated as an explicit hypothesis rather than an implicit convention. The theorem's three conjuncts (icx, icv, cx) mirror the book's own single Theorem 8.A.13, whose part (a) bundles the icx/icv brackets and whose part (b) states the cx case separately, per pitfall 3.

A trivializing formalization this mission rules out: substituting M into a fixed-length Finset.range n sum after the fact (erasing the random-stopping structure that makes this a random-sum theorem at all) rather than genuinely summing over Finset.range (M ω), and treating M ≤icx N as anything other than the same real-valued order Chunks 03/04 define, applied after coercion. This mission draws on no platform prior art (searches for "random sum", "compound distribution", "Poisson process" and "renewal" as of 2026-09-18 return nothing usable). Unlike every other chapter in this series so far, this mission has no milestone theorems: every other numbered result near the goal in this chapter needs the parametric-family apparatus this mission deliberately avoids, and the un-numbered facts the goal's own proof cites (Example 8.A.4's potential-function monotonicity, Example 8.A.7's semigroup property) cannot be milestones per CAPTAIN_BRIEF.md rule 5 — see STATUS.md for the full accounting.

Selected references

• M. Shaked and J. G. Shanthikumar, Stochastic Orders, Springer Series in Statistics, Springer, 2007, Chapter 8 (Stochastic Convexity and Concavity), §8.A.1–8.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/concave orders this chapter restates locally.