Statistics

Motivation

Every generalization bound presented so far in this series is for classification, where the error of a prediction is binary (correct or not). Regression asks a different question: predictions are real-valued, and error is measured by the magnitude of the deviation from the true label, via a loss function L. Chapter 11 develops generalization theory for bounded regression, showing that the same two complexity measures used for classification — Rademacher complexity and a VC-dimension analogue — extend naturally, once the loss function itself is folded into the machinery via a Lipschitz-contraction argument (Rademacher route) or a reduction to classification via level-set thresholding (pseudo-dimension route).

Setting

A regression hypothesis h:X→ℝ is scored by a loss L:ℝ×ℝ→ℝ against a joint distribution D on X×ℝ (the stochastic scenario, since regression labels are rarely exactly reproducible); R(h) = E_{(x,y)~D}[L(h(x),y)] (Eq. 11.1) and R̂_S(h) = (1/m)∑L(h(x_i),y_i) (Eq. 11.2). For a finite hypothesis set, Theorem 11.1 gives a Hoeffding/union-bound guarantee directly, the regression analogue of chunk 02-pac's finite-hypothesis bound. For infinite H, §11.2.2 develops a Rademacher-complexity route: Proposition 11.2 shows that if L is µ-Lipschitz in its first (predicted-value) argument, the Rademacher complexity of the loss-composed family G = {(x,y)↦L(h(x),y) : h∈H} is controlled by µ times H's own Rademacher complexity, via Talagrand's contraction lemma (chunk 05-svm's Lemma 5.7); Theorem 11.3 combines this with chunk 03's Theorem 3.3 to give the chapter's headline bound. §11.2.3 develops an independent, purely combinatorial route: pseudo-dimension (Definition 11.5), a real-valued analogue of VC-dimension defined via threshold-witnessed shattering (Definition 11.4, restated via its own Eq. 11.3 as the VC-dimension of a thresholded indicator family); Theorem 11.8 gives a pseudo-dimension generalization bound by reducing regression to a family of classification problems (one per threshold t), using the tail-integral identity Eq. 11.5.

Formalization targets

Theorem 11.1 (milestone). For L bounded by M and H finite: for any δ>0, with probability at least 1-δ, for all h∈H: R(h) ≤ R̂_S(h) + M√((log|H|+log(1/δ))/(2m)).

Proposition 11.2 (milestone). For L non-negative, bounded by M, µ-Lipschitz in its first argument: for any sample S, R̂_S(G) ≤ µR̂_S(H).

Theorem 11.3 — the mission's goal. Under Proposition 11.2's hypotheses on L: for any δ>0, with probability at least 1-δ, for all h∈H: E[L(h(x),y)] ≤ (1/m)∑L(h(x_i),y_i) + 2µR_m(H) + M√(log(1/δ)/(2m)), and also with 2µR̂_S(H) + 3M√(log(2/δ)/(2m)).

Theorem 11.8 (milestone). For Pdim(G)=d, L non-negative bounded by M: for any δ>0, with probability at least 1-δ over a sample of size m, for all h∈H: R(h) ≤ R̂_S(h) + M√(2d log(em/d)/m) + M√(log(1/δ)/(2m)).

Significance

Theorem 11.3 is the chapter's own choice of headline result (§11.2's stated goal is to show "how the Rademacher complexity bounds of theorem 3.3 can be used to derive generalization bounds for regression"), and its proof genuinely reuses two pieces of prior machinery from this series — chunk 03's Theorem 3.3 and chunk 05's Talagrand's-lemma-style contraction — combined via a new observation (Proposition 11.2) specific to loss-composed families, not a restatement of either. Theorem 11.8 is the chapter's second, structurally independent technique: its em/d bound parallels chunk 03's Corollary 3.19 (both ultimately reduce to a VC-dimension-style growth-function argument), but the reduction itself — regression to a continuum of threshold classification problems, via the Lebesgue-integral tail identity Eq. (11.5) applied to |R(h)-R̂_S(h)| — is genuinely new content for this book, and pseudo-dimension has no prior art on the platform or in Mathlib. No prior art exists for this chapter's overall content either: GET /theorems?q=generalization%20bound%20regression and GET /theorems?q=pseudo-dimension both return zero hits.

Difficulty

Proposition 11.2's proof needs Talagrand's contraction lemma applied with the Lipschitz constant taken in the first argument of L only — the predicted value h(x_i), holding the true label y_i fixed — exactly the pitfall BRIEF.md names: a loss Lipschitz in the wrong argument, or in both arguments jointly, would not license this step. Theorem 11.8's proof is the chapter's most involved: it defines, for every h∈H and threshold t≥0, a classifier c(h,t):(x,y)↦1_{L(h(x),y)>t}, bounds |R(h)-R̂_S(h)| by M·sup_{t∈[0,M]}|R(c(h,t))- R̂_S(c(h,t))| via the tail-integral identity, and then applies a VC-dimension-style classification bound (Corollary 3.19) to the family of thresholded classifiers — whose VC-dimension is, by Eq. (11.3), exactly Pdim(G) by construction. A formalization that conflated pseudo-dimension with ordinary VC-dimension, or reused chunk 03's HasVCDim definition by relabeling, would misrepresent this chapter's genuinely different (real-valued, threshold-witnessed) combinatorial notion — precisely the pitfall BRIEF.md flags.

Formalization scope

Y := ℝ throughout (the book's own "Y a measurable subset of ℝ"), a harmless simplification consistent with every hypothesis, loss and Lipschitz condition in this chapter being stated for real-valued scores and labels. EmpiricalRademacherComplexity/ RademacherComplexity restate chunk 03-rademacher-vc's Definitions 3.1/3.2 locally, since a draft item cannot import another chunk's draft module. Shatters/PseudoDim are formalized via the book's own equivalent reformulation (Eq. 11.3, the thresholded-indicator form), rather than the sign-function form of Definition 11.4 directly, since the two coincide except at a measure-zero boundary the book itself does not address; PseudoDim mirrors chunk 03's HasVCDim Prop-valued pattern (does not cover Pdim(G)=+∞; every consuming theorem takes it as an explicit hypothesis) but is a structurally distinct definition built on Shatters, never a relabeling of HasVCDim, per BRIEF.md's pitfall note. Proposition 11.2's and Theorem 11.3's Lipschitz hypothesis (hLlip) is stated with the true label y' universally quantified outside the two-point comparison y1, y2 (the predicted values), matching "for any fixed y' ∈ Y, y ↦ L(y,y') is µ-Lipschitz" exactly — Lipschitzness in the first argument only, per BRIEF.md's pitfall note. RademacherComplexity (Measure.map Prod.fst D) H m gives the book's R_m(H) (H's Rademacher complexity under the marginal sampling distribution of the inputs x, i.e. D's first marginal). No numerical constant is altered from the book in any of the four theorems.

Not formalized: the L_p-loss worked example following Theorem 11.3's proof (an instantiation of the general theorem for a specific loss family, not a separate numbered theorem); Theorem 11.6 and Theorem 11.7 (worked pseudo-dimension examples for hyperplanes and vector spaces, background/illustration rather than the chapter's general machinery — drafting only these examples instead of the general Theorem 11.8 would be this chapter's trivializing formalization); the two-sided variant of Theorem 11.1 mentioned immediately after its proof (an unnumbered remark, not a separately displayed/numbered theorem); and all of §11.3 (linear regression, kernel ridge regression, SVR, Lasso and their online variants), which is applications-heavy per BRIEF.md's chapter restriction to §11.1-11.2.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 11 (§11.1-11.2).
• D. Haussler, "Decision theoretic generalizations of the PAC model for neural net and other learning applications," Information and Computation 100(1), 1992 (pseudo-dimension's origin).
• D. Pollard, Convergence of Stochastic Processes, Springer, 1984 (the tail-integral identity Eq. 11.5's classical antecedent).

Motivation

Every generalization bound in chapters 2-5 is for binary classification. Most real-world classification problems have more than two classes, and the number of classes can itself be in the hundreds or thousands (topic classification, speech recognition). Chapter 9 extends the margin-based generalization theory of chapter 5 (SVMs) to this multi-class, mono-label setting, using the same Rademacher-complexity machinery as chunk 03-rademacher-vc, but with a new combinatorial ingredient — bounding the Rademacher complexity of a family built by taking a pointwise maximum over several hypothesis sets — needed because a multi-class prediction is itself an argmax over per-class scores.

Setting

A multi-class hypothesis is a scoring function $h:X\times Y\to\mathbb R$ with $Y=\{1,\dots,k\}$ (mono-label case); the predicted label is $\arg\max_y h(x,y)$, and the margin $\rho_h(x,y)=h(x,y)-\max_{y'\ne y}h(x,y')$ (p. 215) is negative exactly when $h$ misclassifies $(x,y)$. The empirical margin loss $\hat R_{S,\rho}(h)$ (Eq. 9.5) uses the same margin-loss function $\Phi_\rho$ (Definition 5.5) as chunk 05-svm, restated locally here. $\Pi_1(H) = \{x\mapsto h(x,y):y\in Y,h\in H\}$ (p. 217) projects a multi-class hypothesis set onto ordinary real-valued functions on $X$ — the object the chapter's Rademacher-complexity bound actually controls, since $H\subseteq\mathbb R^{X\times Y}$ has no norm of its own without such a projection. Lemma 9.1 is a purely combinatorial tool: the empirical Rademacher complexity of a family built by taking the pointwise max over $l$ hypothesis sets is bounded by the sum of their individual empirical Rademacher complexities — used to control the argmax structure of a multi-class prediction. Theorem 9.2 combines this with chunk 03's Rademacher-complexity generalization machinery (Theorem 3.3) to give the chapter's margin bound. Proposition 9.3 and Corollary 9.4 specialize this to kernel-based hypotheses, where each class has its own weight vector in a reproducing kernel Hilbert space and the $k$ weight vectors are jointly constrained by an $L^p$-type group norm $\|W\|_{H,p}\le\Lambda$.

Formalization targets

Lemma 9.1 (milestone). For $F_1,\dots,F_l$ hypothesis sets in $\mathbb R^X$, $l\ge1$, and $G=\{\max\{h_1,\dots,h_l\}:h_i\in F_i\}$: $\hat R_S(G)\le\sum_{j=1}^l\hat R_S(F_j)$.

Theorem 9.2 — the mission's goal. For $H\subseteq\mathbb R^{X\times Y}$, $Y=\{1,\dots,k\}$, fix $\rho>0$. For any $\delta>0$, with probability at least $1-\delta$, for all $h\in H$:

$$R(h) \le \hat R_{S,\rho}(h) + \tfrac{4k}\rho R_m(\Pi_1(H)) + \sqrt{\tfrac{\log(1/\delta)} {2m}}.$$

Proposition 9.3 (milestone). For a PDS kernel $K$ with feature map $\Phi$ and $K(x,x)\le r^2$: $R_m(\Pi_1(H_{K,p})) \le \sqrt{r^2\Lambda^2/m}$.

Corollary 9.4 (milestone). Under Proposition 9.3's hypotheses, fix $\rho>0$. For any $\delta>0$, with probability at least $1-\delta$, for all $h\in H_{K,p}$: $R(h) \le \hat R_{S,\rho}(h) + 4k\sqrt{r^2\Lambda^2/\rho^2/m} + \sqrt{\log(1/\delta)/(2m)}$.

Significance

Theorem 9.2 is the multi-class generalization of chunk 05-svm's Theorem 5.8, and its proof is the chapter's genuine new technique rather than a restatement: it needs a $k$-way application of Lemma 9.1 (once for the argmax structure of the margin, once summing over the $k$ possible labels), which is exactly where the $4k$ factor comes from. Corollary 9.4 is the direct theoretical basis for the multi-class SVM algorithm the chapter derives next (§9.3.1): the displayed dual optimization problem literally minimizes the right-hand side of the corollary's bound. No prior art exists on the platform: GET /theorems?q=multi-class%20classification returns zero hits, and chunk 03's Rademacher-complexity machinery (needed by the proof route) is a draft, not reusable, per the "drafts cannot import drafts" rule.

Difficulty

Lemma 9.1's proof is a genuine two-function argument (max as $\tfrac12(h_1+h_2+|h_1-h_2|)$, Talagrand's lemma applied to $|\cdot|$) generalized to $l$ functions by induction, not a one-line consequence of chunk 03's single-hypothesis-set bound. Theorem 9.2's own proof (PDF pp. 234-236) is the chapter's most involved: it introduces an auxiliary margin function $\rho_{\theta,h}$ with a free parameter $\theta$ later fixed to $2\rho$, splits the resulting Rademacher complexity into a "diagonal" term (bounded via a further one-hot decomposition across the $k$ classes, giving the first factor of $k$) and a "off-diagonal" term bounded via Lemma 9.1 (giving the second factor, folded into the same $4k$ constant). A formalization that stated Theorem 9.2 for $H$ itself rather than $\Pi_1(H)$, or that treated $k$ as an unrelated free constant rather than the actual number of classes, would misstate the theorem — precisely the pitfall BRIEF.md names for this chapter. Proposition 9.3's proof is a clean Cauchy-Schwarz/Jensen argument in the RKHS but needs the $L^p$-group-norm hypothesis class $H_{K,p}$ stated with its exact footnote definition (PDF p. 236), not a simplified $p=2$ special case.

Formalization scope

GeneralizationError, EmpiricalRademacherComplexity and RademacherComplexity are restated locally in this chunk's MultiClass namespace (the last two identical in content to chunk 03-rademacher-vc's own copies); MarginLossFunction restates chunk 05-svm's Definition 5.5 (the same function, needed here for this chapter's own EmpiricalMarginLoss); IsPDS restates chunk 06-kernels's PDS-kernel definition. All are duplicated rather than imported since a draft item cannot import another chunk's draft module, and none of 03, 05, 06 is listed as reusable in missions/README.md's "Published definitions" table at the time of this session. GeneralizationError is formalized via the book's own established equivalence "$h$ misclassifies $(x,y)$ iff $\rho_h(x,y)\le0$" (the form Theorem 9.2's own proof displays and works with), rather than via an explicit argmax classifier construction — checked as faithful, not a weakening, since it is exactly the quantity the chapter's proof bounds. MarginFunction's ⨆_{y'≠y} is a real supremum rather than a Finset.sup', avoiding a nonempty-finset side proof at definition time; every consuming theorem supplies 2 ≤ k (Y = Fin k) to guard it against trap 5. MaxFamily's index type is Fintype+Nonempty rather than a Finset-cardinality parameter l, a harmless generalization matching "l ≥ 1 hypothesis sets" via Nonempty. IsPDS's feature map Φ and its defining property K(x,y) = ⟪Φ(x),Φ(y)⟫ are supplied as hypotheses to the two kernel theorems rather than as a separate "feature mapping associated to a kernel" definition — the book itself treats this as a given correspondence, not a construction. No numerical constant is altered: 4k/ρ and log(1/δ) in Theorem 9.2, r²Λ²/m in Proposition 9.3, and 4k and r²Λ²/ρ²/m in Corollary 9.4 are exactly as displayed.

Not formalized: §9.1's discussion of the multi-label case (Eq. 9.2/9.3, the Hamming-distance risk) and Eq. 9.4 (empirical Hamming error) — background for a case this chapter's own generalization-bound section (§9.2) does not cover (the mono-label case only); the multi-class SVM primal/dual optimization problems (§9.3.1, an algorithm derived from Corollary 9.4, not a generalization-theoretic theorem); AdaBoost.MH (§9.3.2, a boosting algorithm, analyzed via a convex-surrogate argument rather than the Rademacher-complexity route this mission formalizes); and the uniform-over-$\rho$ extension mentioned at the end of the Theorem 9.2 proof (an unnumbered remark referencing Theorem 5.9's technique from a different chapter, not restated here). Drafting only the algorithmic consequences (the multi-class SVM's optimization problem) in place of the generalization bounds themselves would be this chapter's trivializing formalization.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 9.
• V. Koltchinskii, D. Panchenko, "Empirical margin distributions and bounding the generalization error of combined classifiers," Annals of Statistics 30(1), 2002 (Lemma 9.1's technique).
• K. Crammer, Y. Singer, "On the algorithmic implementation of multiclass kernel-based vector machines," JMLR 2, 2001 (the multi-class SVM algorithm §9.3.1 derives).

Motivation

Every guarantee in the preceding chapters assumes a fixed distribution and i.i.d. sampling. On-line learning drops both assumptions: an algorithm processes one example at a time, in an adversarial (worst-case) sequence, and is judged by regret against the best fixed comparator in hindsight rather than by generalization error. This chapter develops the theory for this setting — mistake bounds and regret bounds for prediction with expert advice, a margin-based mistake bound for the Perceptron — and then closes a conceptual gap: since on-line algorithms need no distributional assumption, can their guarantees be converted into ordinary distributional (batch) generalization guarantees when the data does happen to be i.i.d.? The on-line-to-batch conversion theorem answers yes, using nothing but an Azuma's-inequality martingale argument on the sequence of hypotheses the algorithm actually produces.

Setting

At round t, an on-line algorithm receives x_t, predicts ŷ_t, receives the true label y_t, and incurs loss L(ŷ_t,y_t); its regret R_T (Eq. 8.1) compares its cumulative loss to the best fixed action's in hindsight. §8.2 develops this for prediction with expert advice: the Halving algorithm (realizable case), Weighted Majority and its randomized version RWM (zero-one loss, Theorem 8.4's L_T ≤ log(N)/(1-β) + (2-β)L_T^min, proved by the chapter's recurring potential-function technique applied to W_t = ∑_i w_{t,i}), and the Exponential Weighted Average algorithm (convex losses). §8.3.1 analyzes the Perceptron, a linear classification algorithm whose margin-based mistake bound (Theorem 8.8, separable case; the non-separable Theorem 8.11, restated here, in terms of an arbitrary comparator v's hinge losses) depends only on the normalized margin, not the ambient dimension. §8.4 shows that averaging the hypotheses h_1,…,h_T an on-line algorithm produces while processing an i.i.d. sample S yields a hypothesis with controlled true risk: Lemma 8.14 bounds the average of the per-round risks R(h_t) by the average on-line loss via a martingale argument on V_t = R(h_t) - L(h_t(x_t),y_t), and Theorem 8.15 upgrades this, via the loss's convexity, to a bound on the risk of the averaged hypothesis (1/T)∑h_t.

Formalization targets

Theorem 8.4 (milestone). Fix β∈[1/2,1). For any T≥1: L_T ≤ log(N)/(1-β) + (2-β)L_T^min; for β=max{1/2,1-√(log(N)/T)}: L_T ≤ L_T^min + 2√(T log N).

Theorem 8.11 (milestone). M ≤ inf_{ρ>0,‖v‖₂≤1}[(r/ρ+√(r²/ρ²+4‖l_ρ‖₁))/2]², where l_ρ=(l_t)_{t∈I}, l_t=max{0,1-y_t(v·x_t)/ρ}.

Lemma 8.14 (milestone). For any δ>0, with probability at least 1-δ: (1/T)∑_tR(h_t) ≤ (1/T)∑_tL(h_t(x_t),y_t) + M√(2log(1/δ)/T).

Theorem 8.15 — the mission's goal (first inequality). Under Lemma 8.14's hypotheses, with L additionally convex in its first argument: for any δ>0, with probability at least 1-δ: R((1/T)∑_th_t) ≤ (1/T)∑_tL(h_t(x_t),y_t) + M√(2log(1/δ)/T).

Significance

Theorem 8.15 is the chapter's conceptual capstone: it is the only bridge in the whole book between the adversarial on-line-learning framework and the distributional PAC/statistical framework every other chapter develops, and its proof needs nothing beyond Lemma 8.14 plus convexity — no new machinery, just the right observation about the loss's structure. Theorem 8.4 is the chapter's cleanest instance of its recurring potential-function proof technique (reused, with variations, for Theorems 8.3, 8.6 and 8.7), and — checked against the platform's existing OnlineConvexOpt.Introduction.randomized_weighted_majority_mistake_bound (Hazan series) — a genuinely different result from what is already on the platform: that lemma bounds a mistake count with a (1+ε) multiplier, this bounds the RWM algorithm's own weighted-mixture loss with a 1/(1-β) term and a distinct optimal-β substitution, confirming BRIEF.md's assessment that the two are close but not interchangeable. Theorem 8.11 is the non-realizable generalization of the separable-case Perceptron bound (Theorem 8.8) that motivates soft-margin algorithms generally, expressed via an arbitrary comparator's hinge loss rather than assuming perfect separability. No prior art exists for the chapter's other content: GET /theorems?q=online%20to%20batch returns zero hits, and GET /theorems?q=perceptron returns only an unrelated neural-network topology result.

Difficulty

Theorem 8.4's proof (mirrored by Theorem 8.3's WM analogue) derives matching upper and lower bounds on the potential W_t, combines them via a logarithm, and substitutes a specific optimal β found by differentiating the resulting bound — a genuine two-step optimization argument, not a direct algebraic identity. Theorem 8.11's proof solves a quadratic inequality in √M after summing the hinge-loss-defining inequalities over the update set I and invoking the Cauchy-Schwarz step already used in Theorem 8.8's proof; keeping the inf over both ρ and v in the statement (not fixing them, per BRIEF.md's pitfall note) is what makes this a genuine bound rather than a bound for one arbitrary choice. Lemma 8.14's proof is an application of Azuma's inequality (the book's own Theorem D.7) to the martingale difference sequence V_t = R(h_t) - L(h_t(x_t),y_t), which requires h_t to be measurable with respect to the history strictly before round t — the on-line algorithm's hypothesis at round t must not depend on the pair drawn at that same round, per BRIEF.md's pitfall note. Theorem 8.15's step beyond Lemma 8.14 is the passage from the average of T individual risks to the risk of the averaged hypothesis, licensed by Jensen's inequality under the loss's convexity in its first argument — dropping convexity breaks exactly this step, not merely weakening a constant.

Formalization scope

GeneralizationError restates chunk 11-regression's Eq. (11.1) convention locally (Y := ℝ, consistent with that chunk's own harmless simplification), needed here since Theorem 8.15 requires averaging hypotheses into a single real-valued function. OnlineHypothesis A S t is formalized so that its type signature itself enforces history-adaptedness: the on-line algorithm A : (n:ℕ) → (Fin n → X × ℝ) → (X → ℝ) is a function of the prefix of the sample seen so far, and OnlineHypothesis A S t applies it only to S's first t pairs — this is what licenses Azuma's inequality's martingale-difference argument (the conditional-mean-zero property of V_t), per BRIEF.md's pitfall note. Revision (2026-09-19), correcting an earlier claim in this section: history-adaptedness does not by itself guard against GeneralizationError's Bochner integral silently junking to 0 for a non-measurable hypothesis (a distinct property — whether h_t, as a function of x, is Measurable — from whether h_t depends on round t's own draw). Moderation found this a live gap in both Lemma 8.14 and Theorem 8.15's drafted statements; both now carry an explicit hAmeas/hLmeas hypothesis in addition to the history-adapted type signature. RWM's w_{t,i}, W_t, p_{t,i}, L_t, L_T, L_{T,i}, L_T^min are modeled as their own recursively-defined algorithm state (mirroring, but never substituting into, chunk 07-boosting's AdaBoost pattern), matching this chapter's own loss-based (not mistake-count) quantities, per BRIEF.md's pitfall note distinguishing them from AdaBoost's and RWM-mistake variants. The Perceptron's w_t, update-index set I, and M = |I| are modeled the same way, using Eq. (8.23)'s equivalent sign-agreement update rule (the book's own reformulation of Figure 8.6's sgn-based rule). Theorem 8.11's inf_{ρ>0,‖v‖₂≤1} is a genuine nested restricted infimum (⨅ ρ ∈ Set.Ioi 0, ⨅ v ∈ Metric.closedBall 0 1, …), not a bound instantiated at fixed ρ, v, per BRIEF.md's explicit pitfall note. No numerical constant is altered from the book in any of the four theorems.

Not formalized: Theorems 8.1-8.3 (Halving and WM mistake bounds — the chapter's warm-up results, superseded in content by the more general RWM/EWA theorems that follow), Theorem 8.5 (a matching lower bound, a distinct impossibility result rather than an algorithm's guarantee), Theorems 8.6-8.7 (Exponential Weighted Average regret bounds — a third algorithm with its own potential-function proof, out of scope per BRIEF.md's restriction to §8.2's Halving/WM/RWM), Theorems 8.8-8.10 (the Perceptron's separable-case bound and its leave-one-out-based expected generalization bounds, both superseded in generality by Theorem 8.11 for this mission's purposes), Theorem 8.12 (Perceptron's L²-norm hinge-loss bound, the book's own note that it is implied by, and looser than, Theorem 8.11's L¹-norm bound), the dual/kernel Perceptron (an equivalent reformulation, not new generalization content), and Theorem 8.15's second displayed inequality (a regret-form corollary depending on the regret decomposition of the surrounding discussion, not drafted per BRIEF.md's own recommendation to commit to the first inequality as the goal). §8.3.2 (Winnow) and §8.5 (the game-theoretic connection) are out of scope per BRIEF.md's chapter restriction.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 8 (§8.2, §8.3.1, §8.4).
• N. Littlestone, M. K. Warmuth, "The weighted majority algorithm," Information and Computation 108(2), 1994 (WM/RWM's origin).
• F. Rosenblatt, "The perceptron: a probabilistic model for information storage and organization in the brain," Psychological Review 65(6), 1958 (the Perceptron algorithm).
• Y. Freund, R. E. Schapire, "Large margin classification using the perceptron algorithm," Machine Learning 37(3), 1999 (Theorem 8.11's hinge-loss mistake bound).

Motivation

Many estimation problems are naturally posed over matrices rather than vectors: recommender systems (Netflix-style matrix completion), multivariate regression with correlated responses, vector autoregressive time series, and phase retrieval all reduce to estimating an unknown matrix $\Theta^*$ that is low-rank, or well approximated by one. A rank constraint alone makes the natural least-squares estimator non-convex and generally intractable; replacing it with the nuclear norm — the sum of the matrix's singular values, the tightest convex surrogate for rank — yields a tractable semidefinite program. Wainwright's High-Dimensional Statistics (2019), Chapter 10, shows that this substitution costs nothing statistically: nuclear-norm-regularized least squares achieves error rates matching what one could hope for even knowing the rank in advance, by specializing Chapter 9's general decomposable-regularizer framework (mission 09-decomposability) directly to the nuclear norm.

Setting

For matrices $A,B\in\mathbb R^{d_1\times d_2}$, the trace inner product is $\langle\!\langle A,B\rangle\!\rangle := \mathrm{trace}(A^TB) = \sum_{j_1,j_2}A_{j_1j_2}B_{j_1j_2}$ (Eq. 10.1), inducing the Frobenius norm $\|\!|A|\!\|_F$. Given design matrices $X_1,\dots,X_n\in\mathbb R^{d_1\times d_2}$ and responses $y_i=\langle\!\langle X_i,\Theta^*\rangle\!\rangle+w_i$, the observation operator $\mathcal X_n(\Theta):=(\langle\!\langle X_i,\Theta\rangle\!\rangle)_{i=1}^n$ and its adjoint $\mathcal X_n^*(u):=\sum_iu_iX_i$ (Eqs. 10.2-10.3) are the matrix analogs of a vector design matrix and its transpose. The nuclear norm $\|\!|\Theta|\!\|_{\mathrm{nuc}}:=\sum_j\sigma_j(\Theta)$ (Eq. 10.5) — the sum of singular values — is a decomposable regularizer (in the sense of Chapter 9) with respect to the subspace pair spanned by the top singular vectors of any target matrix, and its dual norm (Table 9.1) is the $\ell_2$-operator (spectral) norm $\|\!|\cdot|\!\|_2$. The estimator under study is nuclear-norm-regularized least squares,

$$\hat\Theta \in \operatorname*{arg\,min}_{\Theta\in\mathbb R^{d_1\times d_2}} \left\{ \frac{1}{2n}\|y-\mathcal X_n(\Theta)\|_2^2 + \lambda_n\|\!|\Theta|\!\|_{\mathrm{nuc}} \right\} \tag{10.16}$$

with $\lambda_n>0$ user-chosen.

Formalization targets

Goal (Proposition 10.6)

Suppose $\mathcal X_n$ satisfies the restricted strong convexity condition (10.17), $\|\mathcal X_n(\Delta)\|_2^2/(2n) \ge \kappa/2\|\!|\Delta|\!\|_F^2 - c_0\frac{d_1+d_2}{n}\|\!|\Delta|\!\|_{\mathrm{nuc}}^2$ for all $\Delta$, with $\kappa>0$, $c_0\ge 0$. Conditioned on the good event $\mathcal G(\lambda_n)=\{\|\!|\frac1n\sum_iw_iX_i|\!\|_2 \le\lambda_n/2\}$, any optimal $\hat\Theta$ satisfies, for any $r\in\{1,\dots,d'\}$ with $r\le\kappa n/(128c_0(d_1+d_2))$,

$$\|\!|\hat\Theta-\Theta^*|\!\|_F^2 \le \frac{9}{2}\frac{\lambda_n^2}{\kappa^2}r + \frac{1}{\kappa}\left\{2\lambda_n\sum_{j=r+1}^{d'}\sigma_j(\Theta^*) + \frac{32c_0(d_1+d_2)}{n}\left(\sum_{j=r+1}^{d'}\sigma_j(\Theta^*)\right)^2\right\}.$$

Milestone (Proposition 10.7)

Under the alternative $\Phi^*$-curvature condition (10.20) (a curvature bound on the gradient map rather than the Taylor error), with $\mathrm{rank}(\Theta^*)<\kappa/(64\tau_n)$: conditioned on $\mathcal G(\lambda_n)=\{\|\!|\frac1n\mathcal X_n^*(w)|\!\|_2\le\lambda_n/2\}$, any optimal $\hat\Theta$ satisfies $\|\!|\hat\Theta-\Theta^*|\!\|_2 \le 3\sqrt2\,\lambda_n/\kappa$ — an operator-norm bound the book notes is, in conjunction with the cone-like constraint (10.15), strictly stronger than Proposition 10.6's Frobenius-norm bound.

Significance

Proposition 10.6 is this chapter's direct payoff from Chapter 9's general machinery: it shows that the deterministic backbone of the Lasso's guarantee (mission 07-sparse-linear) extends essentially verbatim to the matrix setting, with the sparsity level $s$ replaced by the target rank $r$ and the ambient dimension $d$ replaced by $d_1+d_2$ — exactly the "degrees of freedom" scaling one would predict by counting the parameters needed to specify a rank-$r$ matrix. Every one of the chapter's later corollaries (matrix compressed sensing, multivariate regression, matrix completion) is obtained by verifying the restricted strong convexity condition (10.17) holds with high probability for a specific random design, then reading the rate directly off Proposition 10.6 — the same two-step recipe Chapter 9's own Theorem 9.19 established abstractly. Proposition 10.7's operator-norm bound is what subsequently controls the individual singular values of the estimation error, needed for exact-rank-recovery guarantees.

Difficulty

Both results are direct specializations of Chapter 9's general oracle inequalities (Theorem 9.19 and Theorem 9.24 respectively) to the nuclear norm as regularizer and the Frobenius/operator norm pair, so their formalization difficulty lies almost entirely in getting the matrix-specific objects right rather than in new proof machinery: the nuclear norm requires an actual notion of singular values (realized via the eigenvalues of the Gram matrix $\Theta^T\Theta$, using Mathlib's Hermitian-matrix spectral theorem), the operator norm requires the correct rectangular generalization of the symmetric-matrix Rayleigh-quotient characterization used in mission 08-pca, and the restricted-strong-convexity and curvature conditions must be instantiated against the correctly-adjointed observation operator $\mathcal X_n^*$. A further subtlety is keeping Proposition 10.6's Frobenius-norm conclusion and Proposition 10.7's operator-norm conclusion cleanly distinct — the book itself warns against conflating the norms used across different chapters of Part II (the vector $\ell_2$-norm of chunks 07-sparse-linear/08-pca versus the matrix Frobenius and operator norms here).

Formalization scope

Scope cut, disclosed here and in STATUS.md. BRIEF.md recommends Corollary 10.10 (the sample-complexity bound for the $\Sigma$-Gaussian random matrix ensemble) as the goal theorem. Corollary 10.10 is a genuinely probabilistic statement — it asserts a bound holding "with probability at least $1-2e^{-2n\delta^2}$" over $n$ i.i.d. draws of design matrices from a $\Sigma$-Gaussian ensemble (Theorem 10.8's own high-probability restricted-strong-convexity certification for that ensemble) — and formalizing it faithfully would require a genuine multivariate-Gaussian-measure infrastructure on matrix space (a probability space, an i.i.d. sequence of $\Sigma$-covariance-structured Gaussian matrices, and Mathlib's measure-theoretic probability API) that is disproportionate to this mission's time budget, and orthogonal to what Chapter 10 itself contributes (the chapter's own text stresses that Propositions 10.6 and 10.7 are the chapter's deterministic core, with probability entering only in Section 10.3's ensemble-specific certification — precisely mirroring chunk 09-decomposability's own "Theorem 9.19 is actually a deterministic result" framing). This mission instead takes Proposition 10.6 as its goal — explicitly named in BRIEF.md's own candidate list as "the nuclear-norm oracle inequality, an explicit corollary of Theorem 9.19" — the natural, tractable, still highly citable deterministic title result of Section 10.2, together with its companion Proposition 10.7. Theorem 10.8 (the $\Sigma$-Gaussian ensemble's RSC certification), Corollary 10.9 (noiseless exact recovery) and Corollary 10.10 itself are left for a future mission with a dedicated probability-theory budget. The cone-like constraint (Eq. 10.15) — whose own faithful statement requires the same explicit subspace-pair machinery ($\mathcal M(U_r,V_r),\bar{\mathcal M}(U_r,V_r)$) chunk 09-decomposability built for the general theory — is similarly left out, since Propositions 10.6 and 10.7's own numbered statements never expose these subspaces directly (only their proofs do, via instantiating Theorem 9.19/9.24). singularValues and nuclearNorm are noncomputable, defined via Mathlib's Hermitian-matrix eigenvalue spectral theorem; c0 ≥ 0 and λn > 0 are made explicit, matching this book's running conventions for RSC tolerance constants and regularization weights (see MODERATION_NOTES.md).

Selected references

• Wainwright, M. J. High-Dimensional Statistics: A Non-Asymptotic Viewpoint. Cambridge University Press, 2019. Chapter 10. DOI: 10.1017/9781108627771.
• Negahban, S., Wainwright, M. J. "Estimation of (near) low-rank matrices with noise and high-dimensional scaling." Annals of Statistics, 39(2), 2011, 1069–1097.
• Recht, B., Fazel, M., Parrilo, P. A. "Guaranteed minimum-rank solutions of linear matrix equations via nuclear norm minimization." SIAM Review, 52(3), 2010, 471–501.

Motivation

Weak learning — a base classifier only slightly better than random guessing — is easy to come by; strong learning, in the PAC sense of Chapter 2, is not. Boosting is the technique that turns the first into the second: combine many weak classifiers, each trained on a reweighted version of the sample that emphasizes previously misclassified points, into a single strong ensemble. AdaBoost, the algorithm this chapter studies, does this with a specific, closed-form weighting rule, and comes with two distinct theoretical guarantees: its training error decreases exponentially fast in the number of rounds (Theorem 7.2), and — more surprisingly — its test error can keep improving even after the training error has already reached zero, an empirical phenomenon that Chapter 3's VC-dimension bound cannot explain at all (it predicts overfitting for large numbers of rounds) but that a margin-based analysis, structurally identical to Chapter 5's SVM theory, does (Theorem 7.7). This mission formalizes both routes.

Setting

AdaBoost (Figure 7.1) takes a labeled sample $S=((x_1,y_1),\dots,(x_m,y_m))$ with $y_i\in\{-1,+1\}$ and a base classifier set $H\subseteq\{-1,+1\}^X$, and runs for $T$ rounds. It maintains a distribution $D_t$ over the sample indices, starting uniform ($D_1(i)=1/m$); at round $t$ it selects a base classifier $h_t$ with small $D_t$-weighted error $\varepsilon_t=\Pr_{i\sim D_t}[h_t(x_i)\ne y_i]$, sets $\alpha_t=\frac12\log\frac{1-\varepsilon_t} {\varepsilon_t}$ and $Z_t=2\sqrt{\varepsilon_t(1-\varepsilon_t)}$, and reweights: $D_{t+1}(i)=D_t(i)\exp(-\alpha_ty_ih_t(x_i))/Z_t$. After $T$ rounds it returns $f=\sum_{t=1}^T\alpha_th_t$; its normalized version is $\bar f=f/\sum_t\alpha_t$. Since $\varepsilon_t<1/2$ makes $\alpha_t>0$, $\bar f$ is a genuine convex combination of base classifiers, i.e. a member of the convex hull $\mathrm{conv}(H)=\{\sum_k\mu_kh_k:\mu_k\ge0, h_k\in H,\sum_k\mu_k\le1\}$ (Eq. 7.12). The chapter reuses Chapter 5's confidence-margin apparatus (empirical margin loss $\hat R_{S,\rho}$, Rademacher complexity $\hat R_S$/$R_m$) to analyze $\bar f$'s generalization.

Formalization targets

Theorem 7.2 (AdaBoost empirical error bound, milestone). The empirical (zero-one) error of $f$ satisfies $\hat R_S(f) \le \exp(-2\sum_{t=1}^T(1/2-\varepsilon_t)^2)$, and, if $\gamma\le1/2-\varepsilon_t$ for all $t$, $\hat R_S(f)\le\exp(-2\gamma^2T)$: training error decays exponentially in $T$ whenever every round beats random guessing by a fixed margin (the "edge" $\gamma$).

Lemma 7.4 (milestone). $\hat R_S(\mathrm{conv}(H))=\hat R_S(H)$: the convex hull of a hypothesis set, though generally much larger, has exactly the same empirical Rademacher complexity as the set itself.

Corollary 7.5 (Ensemble Rademacher margin bound, milestone). For $H$ a set of real-valued functions and $\rho>0$, with probability at least $1-\delta$, every $h\in\mathrm{conv}(H)$ satisfies $R(h)\le\hat R_{S,\rho}(h)+\frac2\rho R_m(H)+\sqrt{\log(1/\delta)/(2m)}$ (and the empirical-complexity analogue with an extra additive $3\sqrt{\log(2/\delta)/(2m)}$ term) — this is Theorem 5.8's margin bound applied to $\mathrm{conv}(H)$, then rewritten via Lemma 7.4 so its complexity term is $H$'s own, not the (much larger) convex hull's.

Theorem 7.7 — the mission's goal. Assume $\varepsilon_t<1/2$ for every $t\in[T]$ (so $\alpha_t>0$). Then for any $\rho>0$,

$$\hat R_{S,\rho}(\bar f) \le 2^T\prod_{t=1}^T\sqrt{\varepsilon_t^{1-\rho}(1-\varepsilon_t)^{1+\rho}}.$$

Significance

Theorem 7.7's bound is what makes margin theory a genuine explanation of AdaBoost's empirical behavior: combined with Corollary 7.5 (applied to $\bar f\in\mathrm{conv}(H)$), it shows that if AdaBoost's edge stays bounded away from zero, the empirical margin loss at a fixed $\rho$ decreases exponentially in $T$ while the generalization bound's complexity term does not depend on $T$ at all — so continuing to boost past zero training error can still shrink the true risk, by growing the margin on the training points that are already correctly classified. This resolves the puzzle that opens §7.3.1: AdaBoost's test error is empirically observed to keep decreasing well after its training error hits zero, which the chapter's own earlier VC-dimension bound on $\mathcal F_T$ (Eq. 7.9, growing as $O(dT\log T)$) predicts should eventually overfit, not improve. No prior art on the Prove2Me platform is faithful: GET /theorems?q=boosting and q=AdaBoost return no hits; this chunk's Rademacher-complexity apparatus is restated locally (a draft item cannot import chunk 05-svm's or 03-rademacher-vc's own draft copies) rather than reused, matching the precedent those chunks' own STATUS.md records recommend for every later chunk needing the same machinery.

Not formalized here: Theorem 7.6 (the VC-dimension-based ensemble margin bound, a direct corollary of Corollary 7.5 via chunk 03's VC-dimension apparatus) — restating 03's own machinery a second time for a single further corollary is disproportionate within this mission's budget, and the chapter's actual capstone targets the sharper, dimension-free Rademacher-complexity route (Theorem 7.7) instead. Also out of scope: §7.2.2's coordinate- descent equivalence, §7.2.3's practical (decision-stump) use, and §7.3.4-7.3.5's margin- maximization LP and game-theoretic interpretation — discussion sections with no numbered result feeding the goal's proof.

Difficulty

Theorem 7.2's proof needs the telescoping identity $D_{T+1}(i) = e^{-y_if(x_i)}/(m\prod_tZ_t)$ (Eq. 7.2), obtained by repeatedly unfolding the recursive weight update — a genuine induction on $t$, not a one-line algebraic manipulation — before the elementary inequality $1_{u\le0}\le e^{-u}$ turns the empirical error into a telescoping product of the $Z_t$'s, each of which is then re-expressed in closed form via a case split on $y_ih_t(x_i)=\pm1$. Theorem 7.7's proof reuses the same identity but with an added margin-shift term $\rho\|\alpha\|_1$ inside the exponential, requiring the same telescoping machinery plus a separate accounting of $e^{\rho\sum_t\alpha_t}$ against the product of $[\sqrt{(1-\varepsilon_t)/\varepsilon_t}]^\rho$ factors coming from each $\alpha_t$'s own closed form — a proof that shares its main structural step with Theorem 7.2 but is not a trivial corollary of it. Corollary 7.5's proof is Lemma 7.4 (itself a careful supremum-exchange argument using the dual-norm characterization of $\ell^1$, not a routine calculation) composed with Theorem 5.8, applied to the specific set $\mathrm{conv}(H)$ rather than a generic hypothesis class — a formalization that stated the corollary only for a "sufficiently nice" abstract class, without deriving it from Lemma 7.4's convex-hull identity, would be proving a different, weaker-provenance statement.

Formalization scope

WeightedError, AdaBoostAlpha, AdaBoostNormalizer, AdaBoostDist, AdaBoostEpsilon, AdaBoostEnsemble, AdaBoostNormalizedEnsemble, EmpiricalError and ConvHull are new, capturing AdaBoost as an actual algorithm (a genuine recursion on the round index, closed under Definitions.Def_FoundationsML_Boosting_AdaBoostDist's own recursive equation) rather than an unspecified "boosting procedure" — the trivialization trap BRIEF.md names for this chapter. AdaBoostDist takes the sequence of base classifiers actually selected at each round, h : ℕ → X → ℝ, as external data rather than deriving it via an argmin over H; this is checked in SELF_REVIEW.md to drop no content either milestone or the goal theorem's statement actually needs, since neither invokes h_t's optimality, only the weighted error ε_t it produces under AdaBoost's own distribution D_t. PhiRho, EmpiricalMarginLoss, MarginGeneralizationError, EmpiricalRademacherComplexity and RademacherComplexity are restated locally, byte-identical to chunk 05-svm's own copies of Definitions 5.5, 5.6, 2.1 (specialized), 3.1, 3.2 (a draft item cannot import another chunk's draft module); this duplication collapses once 05-svm and 03-rademacher-vc are uploaded and listed in missions/README.md's "Published definitions" table. No numerical constant in any of the four theorems is altered from the book's own displayed form. A trivializing formalization this mission avoids: stating Theorem 7.2/7.7 for an arbitrary sequence of error rates $\varepsilon_1,\dots,\varepsilon_T$ satisfying $\varepsilon_t<1/2$, disconnected from any actual algorithm — AdaBoostEpsilon instead ties every ε_t to the weighted error AdaBoost's own recursively defined D_t assigns to its own selected h_t, so the bound is provably about this algorithm's error trajectory, not an arbitrary one.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 7.
• Y. Freund, R. E. Schapire, "A decision-theoretic generalization of on-line learning and an application to boosting," Journal of Computer and System Sciences 55(1), 1997, 119-139.
• R. E. Schapire, Y. Freund, P. Bartlett, W. S. Lee, "Boosting the margin: a new explanation for the effectiveness of voting methods," The Annals of Statistics 26(5), 1998, 1651-1686.

Motivation

Random matrices with independent rows are the workhorse of high-dimensional statistics and compressed sensing: sample covariance matrices, sub-sampled measurement operators, and randomized sketches are all of this form. A basic question about such a matrix $A$ is how close $\|Ax\|_2$ stays to its typical size $\mathbb E\|Ax\|_2\approx\sqrt m\|x\|_2$ — not just for one fixed $x$, but simultaneously for every $x$ in some set $T$ of interest (a sphere, a cone, the difference set of a data cloud). A bound that holds only pointwise in $x$ is of limited use, since most applications need to reason about the worst case over an entire geometric set at once.

This chapter proves such a uniform bound — the matrix deviation inequality — for matrices with independent, isotropic, sub-gaussian rows, controlling the deviation by a single geometric parameter of $T$, its Gaussian complexity. The result is a direct descendant of the chaining machinery of Chapter 8 (via Talagrand's comparison inequality, Chapter 8.6) and, in this book's own account, subsumes several results proved earlier by other methods — two-sided bounds on random matrices, the Johnson-Lindenstrauss lemma for infinite sets — while also yielding two new consequences central to high-dimensional convex geometry: the $M^*$ bound and the Escape theorem, both controlling how a random subspace intersects a fixed geometric set.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$. A random vector $X$ in $\mathbb R^n$ is isotropic if its covariance matrix is the identity, $\Sigma(X)=\mathbb E[XX^\top]=I_n$ — equivalently (the book's own Lemma 3.2.3), $\mathbb E\langle X,x\rangle^2=\|x\|_2^2$ for every $x\in\mathbb R^n$. The sub-gaussian norm of a random vector $X$ is $\|X\|_{\psi_2}:=\sup_{x\in S^{n-1}}\|\langle X,x\rangle\|_{\psi_2}$, the supremum over the unit sphere of the scalar sub-gaussian (Orlicz $\psi_2$) norm of its one-dimensional marginals; $X$ is sub-gaussian when this is finite.

Fix a standard Gaussian random vector $g\sim N(0,I_n)$ in $\mathbb R^n$ (a vector whose coordinates in any orthonormal basis are independent standard normal). For a subset $T\subseteq\mathbb R^n$, the Gaussian width and Gaussian complexity of $T$ are

$$w(T) := \mathbb E\sup_{x\in T}\langle g,x\rangle, \qquad \gamma(T) := \mathbb E\sup_{x\in T}|\langle g,x\rangle|,$$

two closely related measures of the geometric size of $T$ — "cousins" that agree up to a factor of $2$ whenever $T$ contains the origin, and agree exactly when $T$ is origin-symmetric.

Formalization targets

Goal (Theorem 9.1.1, Matrix deviation inequality)

$$\exists\,C>0:\quad \mathbb E\sup_{x\in T}\bigl|\,\|Ax\|_2-\sqrt m\|x\|_2\,\bigr| \;\le\; CK^2\gamma(T)$$

for every $m\times n$ matrix $A$ whose rows $A_1,\dots,A_m$ are independent, isotropic, sub-gaussian random vectors with $K:=\max_i\|A_i\|_{\psi_2}$, and every $T\subseteq\mathbb R^n$ (whenever $\gamma(T)$ is finite). $C$ is the book's own unnamed absolute constant, hard-coded to no numeral — the weakest stable form of the claim.

Milestone (Theorem 9.4.2, the $M^*$ bound)

$$\mathbb E\,\mathrm{diam}(T\cap\ker A) \;\le\; \frac{CK^2w(T)}{\sqrt m}$$

for the same class of matrices $A$ and any bounded $T\subseteq\mathbb R^n$, where $\ker A$ is the (random) kernel of $A$, a subspace of codimension at most $m$. A direct one-paragraph consequence of the goal theorem (apply it to $T-T$, then restrict to $\ker A$, where $\|Ax-Ay\|_2$ vanishes).

Significance

The matrix deviation inequality converts a purely algebraic quantity — how close $\|Ax\|_2$ stays to $\sqrt m\|x\|_2$ — into a single geometric parameter of the index set $T$, letting it subsume, via specializations of $T$, results that were previously proved by separate ad hoc arguments: two-sided singular value bounds on random matrices ($T$ a sphere), Johnson-Lindenstrauss-type embeddings for possibly infinite point sets ($T$ a difference set), and covariance estimation. The $M^*$ bound is one of the two classical consequences the book develops fresh from the inequality (the other, the Escape theorem, is outside this mission's scope): it answers, quantitatively, how large a random affine section of a fixed convex body typically is, a question at the heart of the local theory of Banach spaces and of compressed sensing's recovery guarantees (Chapter 10 builds directly on this chapter's machinery). Both results have long-standing, well-understood classical proofs; this mission formalizes their statements, not open research.

Difficulty

The natural first idea — bound $\|Ax\|_2-\sqrt m\|x\|_2$ pointwise for a fixed $x$ using concentration of the norm of a sub-gaussian random vector, then take a union bound over $T$ — only works when $T$ is finite, and gives a bound that scales with $\log|T|$ rather than with the actual geometric size of $T$. The book's actual route treats $X_x:=\|Ax\|_2-\sqrt m\|x\|_2$, indexed by $x\in\mathbb R^n$, as a genuine random process and shows it has sub-gaussian increments ($\|X_x-X_y\|_{\psi_2}\le CK^2\|x-y\|_2$) — itself a nontrivial fact proved in stages (first for a single unit vector via concentration of the norm, Theorem 3.1.1; then for a pair of unit vectors via a squared-process argument; only then in full generality) — and then invokes Talagrand's comparison inequality (a consequence of the chaining machinery of Chapter 8) to pass from sub-gaussian increments directly to a bound in terms of Gaussian complexity, without ever performing a union bound over $T$ itself.

Formalization scope

A is represented by its rows, A : Fin m → Ω → EuclideanSpace ℝ (Fin n), with ‖Ax‖₂ recovered as Real.sqrt (∑ i, ⟨Aᵢ,x⟩²) rather than constructing A as a Matrix/LinearMap — this matches the book's own row-by-row hypotheses exactly and is what both theorems' own proofs use directly. IsIsotropic is formalized via the book's basis-free Lemma 3.2.3 characterization (E⟨X,x⟩² = ‖x‖² for every x) rather than the matrix equation Σ(X)=Iₙ, avoiding a fixed-basis covariance-matrix construction the rest of this chunk's definitions do not otherwise need. SubgaussianVectorNorm reuses the published scalar subgaussianNorm. GaussianWidth and GaussianComplexity realize the standard Gaussian vector g ∼ N(0,Iₙ) as the identity map on Mathlib's own standard Gaussian measure on a finite-dimensional inner product space (ProbabilityTheory.stdGaussian), and both, together with the goal's own left-hand side, use a locally-defined finite-marginal expected-supremum convention (ExpSup, EReal-valued) matching the book's own footnote-3 convention (Section 7.2), reused throughout the series. Both theorems' right-hand sides presuppose their respective geometric parameter ($\gamma(T)$ or $w(T)$) is a finite real number; since both are EReal-valued in general, each theorem takes an explicit real witness together with a proof that it equals the true value — the same finiteness-disclosure pattern 07-chaining's Dudley inequality uses for its own right-hand integral, needed here for exactly the same reason (the book's own display does not spell out why the quantity is finite, true whenever $T$ is bounded, as in every application). $C$ (and, in the milestone, the same $C$ again — the two are not asserted equal, matching that the book states them as two separate "absolute constants") is existentially quantified before every type, instance and hypothesis it is uniform over. The $M^*$ bound milestone (m_star_bound) additionally carries the hypothesis $m > 0$: its conclusion divides by $\sqrt m$, and without this hypothesis Lean's real-division convention ($x/0=0$) makes the right-hand side $0$ at $m=0$ regardless of $C, K, w(T)$ — false whenever $T$ has positive diameter, not merely a weaker or vacuous claim. The book's own proof ("Dividing by $\sqrt m$ yields …", p. 241) already implicitly assumes $m \ge 1$, matching every other use of $m$ in the chapter as a positive count of measurement rows.

A trivializing formalization would fix $T$ to be a finite set, collapsing the goal to the elementary union-bound case the book explicitly contrasts its own more general statement against (Section 9.1's opening paragraph: "we may choose an arbitrary subset $T\subseteq\mathbb R^n$"); this mission's goal quantifies over an arbitrary Set (EuclideanSpace ℝ (Fin n)) to rule that out.

This mission covers Theorem 9.1.1 and Theorem 9.4.2 only; Theorem 9.4.7 (the Escape theorem) and Theorem 9.2.4 (covariance estimation for lower-dimensional distributions), both named as candidate milestones, are left out for lack of session time given the substantial shared infrastructure this chapter needed from scratch. ExpSup, IsIsotropic, SubgaussianVectorNorm, GaussianWidth and GaussianComplexity are reusable by any later chapter needing an isotropic or sub-gaussian random vector, or a Gaussian-width-type quantity (Chapters 4, 10, 11 of this same book series all use one or more of these notions). Solvers' contributions are welcome on: Theorem 9.1.3 (the sub-gaussian increments of the deviation process, the technical heart of the goal's proof), Talagrand's comparison inequality itself (outside this mission, in 07-chaining's companion chapter), and the one-paragraph reduction from the goal to the $M^*$ bound.

Selected references

• S. Mendelson, A. Pajor, N. Tomczak-Jaegermann, Reconstruction and subgaussian operators in asymptotic geometric analysis, Geometric and Functional Analysis 17 (2007), 1248–1282. https://doi.org/10.1007/s00039-007-0618-7
• V. D. Milman, A new proof of A. Dvoretzky's theorem on cross-sections of convex bodies, Funkcional. Anal. i Priložen. 5 (1971), 28–37.
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 9. https://doi.org/10.1017/9781108231596

Motivation

Many questions in high-dimensional probability reduce to bounding the expected supremum of a random process $(X_t)_{t\in T}$ — the maximum, over an entire indexed family of random variables, of how large any one of them can get. When $T$ is finite this is routine (a union bound over $|T|$ terms suffices), but the interesting cases have $T$ infinite, even uncountable: a supremum over a continuum of test functions, a norm expressed as a supremum over a sphere, or an empirical process indexed by a whole class of functions. A naive union bound is unusable here, since $|T|$ is infinite.

R. M. Dudley's 1967 entropy bound (R. M. Dudley, The sizes of compact subsets of Hilbert space and continuity of Gaussian processes, Journal of Functional Analysis 1 (1967), 290–330) resolved this for Gaussian processes, controlling the expected supremum purely in terms of the metric entropy of $T$ — how many balls of radius $\varepsilon$ are needed to cover $T$, at every scale $\varepsilon$. The technique behind the proof, chaining, builds a sequence of increasingly fine finite approximations to $T$ and telescopes the resulting bounds; it is one of the central tools of the field, reused throughout empirical process theory, statistical learning theory (via Vapnik-Chervonenkis theory), and non-asymptotic random matrix theory. This mission formalizes the chapter's generalization of Dudley's bound beyond Gaussian processes, to any process with sub-gaussian increments, together with the purely combinatorial Sauer-Shelah lemma that the chapter's applications to statistical learning theory build on.

Setting

Fix a probability space $(\Omega,\mathcal F,P)$. A random process is a family $(X_t)_{t\in T}$ of real random variables on $(\Omega,\mathcal F,P)$ indexed by an arbitrary set $T$, with no independence or measurability-of-the-supremum assumed between different $t$'s. Since $\sup_{t\in T}X_t(\omega)$ need not be measurable in $\omega$ for a general index set $T$, its expectation is understood — following the book's own convention, set once in Chapter 7 and reused throughout — through the process's finite-dimensional marginals:

$$\mathbb E\sup_{t\in T}X_t \;:=\; \sup_{T_0\subseteq T\text{ finite, nonempty}}\ \mathbb E\max_{t\in T_0}X_t.$$

Now fix a metric $d$ on $T$, making $(T,d)$ a metric space. The covering number $N(T,d,\varepsilon)$, for $\varepsilon>0$, is the smallest cardinality of a finite $\varepsilon$-net of $T$: a finite set $N\subseteq T$ such that every point of $T$ lies within distance $\varepsilon$ of some point of $N$ (or $N(T,d,\varepsilon):=\infty$ if no finite $\varepsilon$-net exists). The quantity $\log N(T,d,\varepsilon)$ is the metric entropy of $T$ at scale $\varepsilon$: it measures how large $T$ looks when resolved only down to scale $\varepsilon$.

A process $(X_t)_{t\in T}$ has sub-gaussian increments with parameter $K\ge0$ if

$$\|X_t-X_s\|_{\psi_2}\;\le\;K\,d(t,s)\qquad\text{for all }t,s\in T,$$

where $\|\cdot\|_{\psi_2}$ is the sub-gaussian (Orlicz) norm of Chapter 2: the smallest $u>0$ with $\mathbb E\exp((X_t-X_s)^2/u^2)\le2$. This says the increments of the process are controlled by the metric $d$ the way a Gaussian process's increments are controlled by its own canonical metric $d(t,s):=\|X_t-X_s\|_{L^2}$ — but without assuming $(X_t)_{t\in T}$ is Gaussian.

A class of Boolean functions $F$ on a set $\Omega$ shatters a subset $\Lambda\subseteq\Omega$ if every function $g:\Lambda\to\{0,1\}$ arises as the restriction to $\Lambda$ of some $f\in F$. The VC (Vapnik-Chervonenkis) dimension $\mathrm{vc}(F)$ is the largest cardinality of a subset of $\Omega$ shattered by $F$ (or $\infty$ if arbitrarily large finite subsets, or an infinite one, are shattered) — a purely combinatorial measure of how rich the class $F$ is.

Formalization targets

Goal (Theorem 8.1.3, Dudley's integral inequality)

$$\exists\,C>0:\quad\mathbb E\sup_{t\in T}X_t\;\le\;CK\int_0^\infty\sqrt{\log N(T,d,\varepsilon)}\;d\varepsilon$$

for every mean-zero random process $(X_t)_{t\in T}$ on a metric space $(T,d)$ with sub-gaussian increments parameter $K\ge0$, whenever the integral is finite. $C$ is the book's own unnamed absolute constant, never depending on $T$, $K$, or the process. This is the weakest stable form of the claim: no numeral is hard-coded for $C$, and the statement asks only for the shape of the bound, matching what the book actually proves.

Milestone (Theorem 8.3.16, Sauer-Shelah lemma)

$$|F|\;\le\;\sum_{k=0}^{d}\binom nk\;\le\;\left(\frac{en}{d}\right)^{d},\qquad d:=\mathrm{vc}(F),$$

for every class $F$ of Boolean functions on a finite $n$-point set $\Omega$. This is a purely combinatorial fact, with no probability involved, but it is the bridge (via the covering-number bound Theorem 8.3.18, outside this mission's scope) between the chapter's Dudley-inequality engine and its statistical-learning applications — a bound on how large a finite class of Boolean functions can be, in terms of a single combinatorial complexity parameter.

Significance

Dudley's inequality is, in the book's own words, "the main result" of the chaining chapter: it converts a purely geometric quantity — the metric entropy of an index set, computable in many cases from covering-number estimates already available for balls, ellipsoids, and other convex bodies — into a probabilistic control on the size of a random process indexed by that set. This is what lets later chapters (uniform laws of large numbers over function classes, the matrix deviation inequality, the Dvoretzky-Milman theorem on almost-spherical sections of convex bodies) bound suprema over infinite, even uncountable, index sets without ever performing a union bound. The bound is also known to be tight only up to a logarithmic factor in general — Sudakov's minoration inequality (Chapter 7) gives a matching lower bound for Gaussian processes, and the book's own Exercise 8.1.12 exhibits a set where the two bounds genuinely diverge — so the constant $C$ here cannot in general be sharpened away.

The Sauer-Shelah lemma is one of the two founding results of VC theory (together with the Glivenko-Cantelli-type uniform convergence it feeds into), independently discovered by Vapnik and Chervonenkis, Sauer, and Shelah in the early 1970s; it underlies the sample-complexity bounds of statistical learning theory (a hypothesis class with finite VC dimension is PAC-learnable) and, through Theorem 8.3.18, gives one of the two standard routes (the other being direct combinatorial counting) to bounding covering numbers of infinite function classes.

Both results are decades old and have long-established, standard proofs; no open mathematical question is being formalized. What this mission contributes is the machine-checked statement infrastructure — the goal and the Sauer-Shelah milestone, together with the definitions (CoveringNumber, ProcessESup, Shatters, VcDim) a faithful Lean rendering of either result needs — for a solver to close with a proof. No formalization of Dudley's inequality or the Sauer-Shelah lemma is known to exist on the platform prior to this mission.

Difficulty

The natural first idea for bounding $\mathbb E\sup_{t\in T}X_t$ is a single-scale $\varepsilon$-net argument: replace $T$ by a finite $\varepsilon$-net, bound the maximum over the (finite) net by a union bound using the sub-gaussian tail, and separately bound the error of replacing $T$ by the net using the Lipschitz-in-probability control the sub-gaussian-increments hypothesis gives. This works, but it only ever sees $T$ at one fixed resolution $\varepsilon$, and optimizing over $\varepsilon$ afterward gives a bound with an extra $\sqrt{\log(1/\varepsilon)}$-type loss that does not match Dudley's inequality. The actual difficulty is genuinely multi-scale: chaining builds a whole sequence of nets at dyadic scales $\varepsilon=2^{-k}$ simultaneously, connects each point of $T$ to its nearest net point at every scale to form a "chain" of successive approximations back to a single fixed basepoint, and telescopes the resulting sum of increments — turning $X_t$ itself into a sum of differences between successive links of the chain, each individually well controlled by the sub-gaussian hypothesis at its own scale. Passing from the resulting discrete sum over dyadic scales (Theorem 8.1.4) to the continuous integral of the goal is a further, separate technical step.

For the Sauer-Shelah lemma, the natural first idea — bound $|F|$ directly by counting — has no obvious purchase on an arbitrary class of Boolean functions. The actual argument goes through Pajor's lemma, which reduces bounding $|F|$ to counting the shattered subsets of $\Omega$ instead of the functions in $F$ themselves; only then does the cardinality bound $d=\mathrm{vc}(F)$ on shattered sets become directly usable, via a binomial-sum estimate.

Formalization scope

CoveringNumber T ε is ℕ∞-valued (ℕ∞ = WithTop ℕ), defined as the infimum, over the subtype of finite $\varepsilon$-nets of the whole type T (an instance of MetricSpace T), of their cardinality; the infimum of the empty family in this complete lattice is ⊤, reproducing "$N:= \infty$ if no finite net exists" with no case split. ProcessESup is EReal-valued, defined as the supremum over finite nonempty $T_0\subseteq T$ of the Bochner integral of the finite max — EReal, not ℝ, because a real-valued supremum would silently return the junk value $0$ if the family of marginal expectations were unbounded above. Shatters and VcDim are direct transcriptions of Definition 8.3.1, with VcDim valued in ℕ∞ via a supremum of Set.encard over the (always-nonempty, since $\varnothing$ is trivially shattered) subtype of shattered subsets. The goal's mean-zero hypothesis is stated as Integrable (X t) P ∧ ∫ X t = 0 rather than the bare equation, since a non-integrable variable's Bochner integral is 0 in Mathlib by convention regardless of its true mean — a bare-equation hypothesis would let a non-mean-zero, non-integrable process satisfy the theorem vacuously. Two further hypotheses make explicit what the book's own displayed statement treats as understood without spelling out: that $N(T,d,\varepsilon)$ is finite for every $\varepsilon>0$ (total boundedness of $T$), and that the resulting integrand is integrable on $(0,\infty)$ — both hold whenever $T$ is totally bounded, since the integrand vanishes once $\varepsilon\ge\mathrm{diam}(T)$, so neither hypothesis excludes any case the book's own proof does not also need. [Nonempty T] excludes the degenerate empty index set. The absolute constant $C$ is existentially quantified ahead of every type, instance, and hypothesis it is uniform over, and pinned to no numeral, matching "$C$ is an absolute constant" — a formalization hard-coding a specific numeral for $C$ would be invalidated by the next sharper constant in the literature and would not match what the book proves.

A trivializing formalization of the Sauer-Shelah lemma would fix $\mathrm{vc}(F)$ at a hard-coded small value, or drop the second (exponential) inequality in favor of the weaker first one; this mission's statement keeps both inequalities, with $d$ genuinely computed from VcDim, and handles the $d=0$ boundary (where the exponential bound's base involves a division by zero under Lean's x/0=0 convention) explicitly rather than excluding it, since x^0=1 still recovers the book's correct bound $|F|\le1$ there.

This mission covers Theorem 8.1.3 and Theorem 8.3.16 only; Theorem 8.3.18 (covering numbers via VC dimension) and Theorem 8.2.3 (the uniform law of large numbers, the chapter's direct application of Dudley's inequality) are left out, not approximated, for lack of the additional empirical- process measurability machinery — the class of Lipschitz functions of Eq. (8.22), measurability of the resulting empirical process — that a faithful statement of either would need beyond what this mission's items already provide. CoveringNumber and ProcessESup are reusable by any later chapter needing a metric space's covering numbers or a general random process's expected supremum (this book's own Chapters 7, 9, and 11 all use one or both); Shatters and VcDim are reusable by any later development of VC theory or statistical learning theory. Solvers' contributions are welcome on: the chaining argument itself (the mission's hardest open leaf, via the discrete dyadic form of Theorem 8.1.4), Pajor's lemma underlying Sauer-Shelah, and the binomial-sum estimate closing its second inequality.

Selected references

• R. M. Dudley, The sizes of compact subsets of Hilbert space and continuity of Gaussian processes, Journal of Functional Analysis 1 (1967), 290–330. https://doi.org/10.1016/0022-1236(67)90017-1
• N. Sauer, On the density of families of sets, Journal of Combinatorial Theory, Series A 13 (1972), 145–147. https://doi.org/10.1016/0097-3165(72)90019-2
• V. N. Vapnik, A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability & Its Applications 16 (1971), 264–280. https://doi.org/10.1137/1116025
• R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data Science, Cambridge University Press, 2018, Chapter 8. https://doi.org/10.1017/9781108231596

Comparing location and spread together

Chapter I's usual stochastic order compares "how large" two random variables tend to be; Chapter III's convex order compares "how spread out" they are, holding the mean fixed. Chapter IV's increasing convex and increasing concave orders combine the two: $X \le_{icx} Y$ says $X$ is both smaller and less variable than $Y$ in a single comparison, without forcing equal means. These are the orders a decision-maker with risk-averse (concave-utility) or risk-loving (convex-cost) preferences actually uses to rank random outcomes, since expected utility is exactly an expectation of an increasing concave or convex function. This mission formalizes both orders and their coupling characterization: the submartingale/supermartingale analogue, one chapter over, of Chapter III's Strassen martingale coupling for the plain convex order.

The increasing convex and increasing concave orders

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

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

and smaller than $Y$ in the increasing concave order, $X \le_{icv} Y$, if the same holds for every increasing concave $\varphi$. Taking $\varphi(x)=x$ (increasing and both convex and concave) gives $E[X]\le E[Y]$ under either order — unlike the convex order, no equality of means is forced. Two equivalent tail-integral characterizations (Theorem 4.A.2) make the orders tractable: $X\le_{icx}Y$ iff $\int_x^\infty \bar F(u)\,du \le \int_x^\infty \bar G(u)\,du$ for every $x$, and $X\le_{icv}Y$ iff $\int_{-\infty}^x F(u)\,du \ge \int_{-\infty}^x G(u)\,du$ for every $x$, where $\bar F,\bar G$ and $F,G$ are the survival and distribution functions.

Formalization targets

Goal: the submartingale-coupling characterization (Theorem 4.A.5, increasing convex case)

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

Furthermore, $\hat X,\hat Y$ can be chosen so that $[\hat Y\mid\hat X=x]$ stochastically increases with $x$ (in $\le_{st}$). This is the increasing-convex analogue of Chapter III's Theorem 3.A.4: instead of a martingale, $\{\hat X,\hat Y\}$ need only be a submartingale — the copy of $Y$ is, conditionally on the copy of $X$, at least a fair randomization of it. The book states its proof is "similar to the proof of Theorem 3.A.4" and calls the constructive direction "not easy to prove"; this mission states the theorem faithfully, including the "Furthermore" strengthening, without attempting a proof.

Companion: the supermartingale-coupling characterization (Theorem 4.A.5, increasing concave case)

The same theorem's other bracketed case: $X \le_{icv} Y$ iff there exist $\hat X,\hat Y$ on a common space with $\hat X=_{st}X$, $\hat Y=_{st}Y$, and $\{\hat Y,\hat X\}$ a supermartingale, $E[\hat X\mid\hat Y]\le\hat Y$ a.s. — note the swapped roles of $\hat X$ and $\hat Y$ in the conditioning relative to the increasing-convex case, not merely a flipped inequality. Drafted as a separate Lean theorem from the goal (see Formalization scope), since the two conditioning structures are genuinely different predicates, not sign-flipped rewrites of one another.

Supporting milestones

• Theorem 4.A.1, the duality relation: $X\le_{icx}Y \iff -X\ge_{icv}-Y$, and $X\le_{icv}Y\iff -X\ge_{icx}-Y$ — the increasing-order analogue of Theorem 3.A.12(a)'s duality for the plain convex order.
• Theorem 4.A.2, the tail-integral characterizations above, for integrable $X,Y$.
• Theorem 4.A.8(d), closure under convolution: independent $X_i\le_{icx}Y_i$ (resp. $\le_{icv}$) for $i=1,\dots,m$ gives $\sum_i X_i \le_{icx} \sum_i Y_i$ (resp. $\le_{icv}$) — the increasing-order analogue of Chapter III's Theorem 3.A.12(d), which the book itself says "can be proven as in Theorem 3.A.12."

Significance

The increasing convex and concave orders are the natural language of expected-utility comparisons: a risk-averse agent with concave utility $u$ prefers $Y$ to $X$ exactly when $X\le_{icv}Y$ implies $E[u(X)]\le E[u(Y)]$ for every increasing concave $u$ — the order is defined precisely so that "every risk-averse agent with increasing utility agrees" collapses to one comparison. In operations research this underlies stochastic dominance of the second kind in portfolio and inventory models, and the increasing-convex order similarly formalizes "second-order stochastic dominance for costs" used to compare random cost/loss distributions under risk-loving or regret-averse preferences. The submartingale-coupling characterization is what turns the intractable "for every increasing convex $\varphi$" quantifier into a single explicit construction, exactly as Strassen's theorem does for the plain convex order — and, being the direct chapter-IV successor to Chapter III's coupling theorem in this series, it fixes the second data point for what a "coupling-characterization" mission in this book's series looks like when the order being characterized is not symmetric between the two variables' roles.

No platform prior art exists: GET /theorems?q=increasing+convex, q=increasing+concave, and q=submartingale return zero genuinely matching hits (the one submartingale hit, a bandit subgaussian maximal inequality, uses Doob's inequality for a concentration bound, not this order). This mission restates the increasing convex/concave orders and their coupling characterization as a foundational, self-contained pair of definitions, parallel in structure to Chunk 03's convex-order mission but independently drafted (drafts cannot import each other's Lean).

Difficulty

The chief formalization risk is the one this chapter's own brief flags explicitly: the book states Theorem 4.A.5 as a single statement with bracketed alternatives ("$X\le_{icx}Y$ [$X\le_{icv}Y$] iff … $\{\hat X,\hat Y\}$ is a submartingale [$\{\hat Y,\hat X\}$ is a supermartingale] …"), and the two cases are not symmetric rewrites of each other — the conditioning variable in E[Ŷ|X̂]≥X̂ swaps to E[X̂|Ŷ]≤Ŷ in the concave case, not just a flipped inequality on the same conditioning. A Lean statement that tried to unify both cases with a single Or or a naive sign-flip would either conflate two different predicates or silently state the wrong condition for one of the two cases. The duality theorem (4.A.1) compounds this risk in the other direction: its content is exactly that $\le_{icx}$ and $\ge_{icv}$ are related (by negating the variables), so a formalization that makes this equivalence provable by unfolding definitions (rather than as a genuine ↔ between two independently-stated predicates) would trivialize the one theorem whose entire content is that relationship.

Formalization scope

Random variables are measurable functions into $\mathbb{R}$ from arbitrary measurable spaces, matching this series' convention; IcxOrder μ ν X Y and IcvOrder μ ν X Y are drafted as two separate definitions (not one order parametrized by an Or of function classes), each quantifying over Monotone φ ∧ ConvexOn ℝ Set.univ φ (resp. ConcaveOn) with the two expectations' existence stated as explicit Integrable hypotheses inside the ∀, exactly as Chunk 03's ConvexOrder. Equality in law is ProbabilityTheory.IdentDistrib. The goal's submartingale condition uses Mathlib's conditional-expectation notation X̂ ≤ᵐ[ρ] ρ[Ŷ | m] with m the σ-algebra generated by X̂; its companion's supermartingale condition uses ρ[X̂ | m'] ≤ᵐ[ρ] Ŷ with m' generated by Ŷ instead — the conditioning variable is genuinely swapped between the two theorems, matching the book's own bracket ordering {X̂,Ŷ} vs. {Ŷ,X̂}. The "Furthermore" clause in both is kept (not dropped), via Mathlib's ProbabilityTheory.condDistrib, restated as the relevant conditional-distribution kernel's survival function being monotone at every threshold — the same shape Chapter I's UsualOrder and Chunk 03's goal theorem use, necessarily restated locally since drafts cannot import another mission's definitions.

Theorem 4.A.1 (duality) and Theorem 4.A.8(d) (convolution closure) are each drafted as a single Lean theorem with two independent conjuncts (an ∧ of two ↔s, or of two implications), one per bracketed case, since the book states both cases as the two halves of one theorem sharing every hypothesis — this is not the same shape as the goal/companion split, where the two cases have genuinely different internal structure (the swapped conditioning) rather than a shared statement instantiated at two function classes. A trivializing formalization this mission rules out: stating Theorem 4.A.1's duality by relabeling IcvOrder as IcxOrder applied to negated arguments (making the equivalence a rfl or single simp unfolding) rather than keeping the two orders as independently-defined predicates whose relationship is the theorem's actual content.

This mission draws on no platform prior art (searches for "increasing convex", "increasing concave", and "submartingale" as of 2026-09-18 return zero genuine matches — the sole submartingale hit is an unrelated bandit concentration inequality via Doob's inequality). Reusable beyond this mission: the IcxOrder/IcvOrder definition pattern and the submartingale/supermartingale coupling shape parallel Chunk 03's ConvexOrder martingale-coupling pattern closely enough that a future chapter needing "coupling characterization of a location-and-spread order" (none of the remaining chapters currently in this series' first wave) 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 4 (Univariate Monotone Convex and Related Orders), §4.A. https://doi.org/10.1007/978-0-387-34675-5
• This series' Chunk 03 (StochasticOrders.Convex), for the plain convex order and Strassen's martingale coupling this chapter's submartingale/supermartingale coupling directly generalizes.