Probability

Motivation

The book The Principles of Deep Learning Theory by D. A. Roberts and S. Yaida (arXiv:2106.10165) develops a perturbative, physics-style theory of wide deep neural networks. Every later computation in the book, from the statistics of preactivations at initialization to the neural tangent kernel, reduces to Gaussian expectations of polynomials. The single tool that evaluates these expectations is Wick's theorem (eq. 1.45), which the authors ask the reader to "put a box around". This mission formalizes Chapter 1, §1.1 (Gaussian Integrals), culminating in that theorem. It is the first mission of a series formalizing the book, all in the Lean namespace DeepLearningTheory.

Setting

Fix $N \ge 0$ and a symmetric positive-definite real $N\times N$ matrix $K = (K_{\mu\nu})$, the covariance. Write $K^{\mu\nu} = (K^{-1})_{\mu\nu}$ for its inverse. The zero-mean multivariable Gaussian distribution with covariance $K$ (eq. 1.31) has density on $\mathbb{R}^N$

and the expectation of an observable $F$ is $\mathbb{E}[F(z)] = \int d^N z\, p(z) F(z)$ (eqs. 1.36, 1.46), an integral against Lebesgue measure. A pairing of the labels $1,\dots,2m$ is a partition into $m$ unordered pairs; equivalently, a fixed-point-free involution $\sigma$ of $\{1,\dots,2m\}$ pairing $a$ with $\sigma(a)$. There are $(2m-1)!!$ pairings.

Formalization targets

Goal: Wick's theorem (eq. 1.45)

For all indices $\mu_1,\dots,\mu_{2m} \in \{1,\dots,N\}$ (repetitions allowed),

Milestones

1. Eq. (1.30) — the normalization $\int d^N z\, e^{-\frac12 z^\top K^{-1} z} = \sqrt{|2\pi K|}$.
2. Eq. (1.41) — the generating function $\int d^N z\, e^{-\frac12 z^\top K^{-1} z + J\cdot z} = \sqrt{|2\pi K|}\, e^{\frac12 J^\top K J}$ for every source $J \in \mathbb{R}^N$.
3. Odd moments vanish (p. 22, discussion after eq. 1.42).
4. Eq. (1.43) — $\mathbb{E}[z_{\mu_1} z_{\mu_2}] = K_{\mu_1\mu_2}$.
5. Eq. (1.44) — $\mathbb{E}[z_{\mu_1}z_{\mu_2}z_{\mu_3}z_{\mu_4}] = K_{\mu_1\mu_2}K_{\mu_3\mu_4} + K_{\mu_1\mu_3}K_{\mu_2\mu_4} + K_{\mu_1\mu_4}K_{\mu_2\mu_3}$.

Significance

Wick's theorem (also known as Isserlis' theorem, 1918) is used throughout the book: the Gaussianity of the first layer (Chapter 4), the four-point correlators of deep linear networks (Chapter 3), and all perturbative expansions around the infinite-width limit are evaluated by Wick contractions. A machine-checked version stated in the book's own density-based conventions gives later missions of this series a dependable foundation. The result is classical; the work remaining is its formalization in exactly this form. A related statement for general (possibly degenerate) Gaussian measures already exists on the platform as FeynmanWick.wick_theorem_gaussian; the present mission keeps the book's formulation via the explicit density and a positive-definite covariance.

Difficulty

The book's derivation differentiates the generating function (1.41) $2m$ times at $J=0$, which requires justifying differentiation under the integral sign and organizing the combinatorics of the product rule into pairings. Both the analytic step (dominated convergence for Gaussian tails, in $N$ dimensions) and the combinatorial step (a bijection between surviving terms and pairings, with the $1/(2^m m!)$ normalization) are routine on paper but need care in Lean. Computing the normalization (1.30) itself requires diagonalizing $K$ and a linear change of variables.

Formalization scope

• Vectors are functions Fin N → ℝ with Lebesgue measure; $K$ is a Matrix (Fin N) (Fin N) ℝ with K.PosDef (which includes symmetry). The inverse is Mathlib's K⁻¹.
• gaussianDensity K z and gaussExpect K F are exactly the book's $p(z)$ and $\mathbb{E}[F]$; gaussQuadForm K z is $\sum z_\mu K^{\mu\nu} z_\nu$.
• pairings (2m) is the finite set of fixed-point-free involutions of Fin (2m); the product is over labels $a$ with $a<\sigma(a)$, so each pair contributes once.
• Positive definiteness is assumed exactly as in the book; no statement is vacuous since, e.g., $K = I$ satisfies every hypothesis.

Selected references

• D. A. Roberts, S. Yaida (with B. Hanin), The Principles of Deep Learning Theory, Cambridge University Press, 2022. arXiv:2106.10165
• L. Isserlis, On a formula for the product-moment coefficient of any order of a normal frequency distribution in any number of variables, Biometrika 12 (1918). doi:10.1093/biomet/12.1-2.134

Motivation

Chapter 3 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), asks how many random examples suffice to learn a concept from an infinite class. The cardinality bound of Occam's Razor is useless there, yet the rectangle game of Chapter 1 shows that some infinite classes are learnable from a finite sample. The answer is the Vapnik–Chervonenkis dimension: the size of the largest set on which the class realizes every labeling. Sauer's lemma says that a class of VC dimension $d$ realizes only $\Phi_d(m) = \sum_{i \le d}\binom{m}{i} \le (em/d)^d$ labelings on any $m$ points, polynomially many rather than $2^m$, and the ε-net theorem of Blumer, Ehrenfeucht, Haussler and Warmuth turns this into a sample bound: a consistent hypothesis from a class of VC dimension $d$ is probably approximately correct once $m$ is of order $(1/\epsilon)(\log(1/\delta) + d\log(1/\epsilon))$. A matching lower bound shows that $\Omega(d/\epsilon)$ examples are necessary. The chapter thus gives a single combinatorial parameter that characterizes, up to a logarithmic factor, the sample complexity of learning any class in the distribution-free model.

Setting

For a class $C$ of concepts $X \to \{0,1\}$ and a finite $S \subseteq X$, $\Pi_C(S)$ is the set of dichotomies of $S$ realized by $C$; $S$ is shattered if all $2^{|S|}$ are realized; $\mathrm{VCD}(C)$ is the supremum of the sizes of shattered sets, possibly $\infty$; $\Pi_C(m)$ is the largest $|\Pi_C(S)|$ over $|S| = m$; and $\Phi_d(m)$ is defined by $\Phi_d(m) = \Phi_d(m-1) + \Phi_{d-1}(m-1)$, $\Phi_d(0) = \Phi_0(m) = 1$. For a target $c$ the error regions are $c \,\Delta\, h$ for $h$ in the hypothesis class, and a set of points is an ε-net if it meets every error region of weight at least $\epsilon$ under the target distribution $D$. Samples, their product law, consistency and the error of a hypothesis are those of Mission I.

Formalization targets

Goal: Theorems 3.3 and 3.4

Let $H$ be a class of VC dimension at most $d$, well-behaved for the target $c$ (the double-sample event of the proof is null-measurable), and $m \ge 8/\epsilon$. The points of a random sample of $m$ examples of a target $c$ fail to be an ε-net for the error regions $\{c \,\Delta\, h : h \in H\}$ with probability at most

so any algorithm that outputs a hypothesis in $H$ consistent with its sample has error greater than $\epsilon$ with at most that probability; with $m \ge (4/\epsilon)\log_2(2/\delta)$ and $m \ge (8d/\epsilon)\log_2(13/\epsilon)$ the probability is at most $\delta$; and, if $H$ is nonempty, every class contained in $H$ for whose targets $H$ is well-behaved is PAC learnable using $H$.

Milestones

Lemma 3.1 (Sauer's lemma, $\Pi_C(m) \le \Phi_d(m)$); Lemma 3.2 ($\Phi_d(m) = \sum_{i \le d}\binom{m}{i}$); the polynomial bound $\Phi_d(m) \le (em/d)^d$ of p. 57; Theorem 3.5 (the $\Omega(d/\epsilon)$ lower bound, in the two explicit forms of its proof).

Significance

Theorem 3.3 is the fundamental theorem of PAC learning: it replaces $\log|H|$ in Occam's Razor by the VC dimension and thereby covers rectangles, halfspaces, polygons, neural networks with a fixed architecture, and every class whose dichotomies grow polynomially. Its proof, the double sample and random partition argument, is the origin of symmetrization in empirical process theory. Sauer's lemma is a cornerstone of extremal combinatorics with independent proofs by Sauer, Shelah and Vapnik–Chervonenkis, and the lower bound of Theorem 3.5 shows that the upper bound is tight to within $\log(1/\epsilon)$, so the VC dimension genuinely characterizes sample complexity. None of these is machine-checked. Formalizing them puts on the platform the VC dimension, the growth function and the ε-net theorem with explicit constants, stated on the same sample law as the rest of this series, and the first information-theoretic lower bound for learning.

Difficulty

Sauer's lemma is a double induction on $d$ and $m$ through the auxiliary class $C'$ of dichotomies whose two extensions to a distinguished point are both realized, which needs care with the identification of dichotomies of $S$ and of $S \setminus \{x\}$. The ε-net theorem needs: the reduction $\Pr[A] \le 2\Pr[B]$ from a failed ε-net on the first half to a region hit at least $\epsilon m/2$ times by the second half, which is a Chebyshev bound on a binomial variable and is where $m \ge 8/\epsilon$ enters; the exchangeability of the $2m$ draws with a random partition into two halves; the counting bound $\binom{m}{\ell}/\binom{2m}{\ell} \le 2^{-\ell}$; and Sauer's lemma applied to the error regions, whose growth function equals that of $H$. The explicit constants require the numerical inequality $2(2em/d)^d 2^{-\epsilon m/2} \le \delta$ under the two stated conditions. The lower bound is a probabilistic argument with a random target: conditional on the sample, the labels of unseen points are fair coins, so the number of errors on them is binomial and exceeds half its range with probability at least $1/2$; the refined bound scales this construction to a region of weight $16\epsilon$ and uses Markov's inequality to bound the number of draws landing in it. Measurability of the failure sets is avoided by stating outer-measure bounds, except for the double-sample event, which the proof integrates: it is assumed null-measurable (the well-behavedness of Blumer et al., without which the theorem is false for a class of VC dimension $1$ on $\omega_1$). For the lower bound it is avoided by working over a finitely supported distribution on a space with measurable singletons.

Formalization scope

The VC dimension is a supremum in $\mathbb{N} \cup \{\infty\}$, the growth function a supremum in $\mathbb{N}$ (bounded by $2^m$), and $\Phi_d$ the book's recurrence, with its closed form and polynomial bound stated as separate theorems. The goal is stated for a hypothesis class $H$ (Theorem 3.4), Theorem 3.3 being the case $C = H$; it carries the exact bound of the proof, the explicit constants of Blumer et al. in place of the book's $c_0$, the requirement $m \ge 8/\epsilon$ of the proof's Chebyshev step, measurability of the hypotheses and the target, well-behavedness of $H$ for the target, and $0 < \epsilon, \delta < 1$. PAC learnability of the subclasses of $H$ needs $H$ nonempty, since no algorithm outputs hypotheses in the empty class. The lower bound is stated for every deterministic learning function, on an instance space with measurable singletons, for a class shattering some set of $d \ge 1$ points, with the explicit constants derived in the proof sketch ($m \le d/2$: error $\ge 1/8$ with probability $\ge 1/2$; $\epsilon \le 1/16$ and $m \le (d-1)/(64\epsilon)$: error $> \epsilon$ with probability $\ge 1/4$). Running time is not modelled. The composition bound for layered networks (Theorems 3.6 and 3.7) is not stated.

Trivializing readings are excluded: the ε-net event ranges over every hypothesis of $H$, the failure bounds are uniform over all consistent learners, and the lower bound holds for every learning function. Welcome contributions: Sauer's lemma, the closed form and the $(em/d)^d$ bound, the random-partition counting lemma, and the binomial median inequality used in the lower bound.

Selected references

• M. J. Kearns, U. V. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994, Chapter 3. doi:10.7551/mitpress/3897.001.0001
• A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Learnability and the Vapnik–Chervonenkis dimension, Journal of the ACM 36(4), 1989. doi:10.1145/76359.76371
• V. N. Vapnik, A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and its Applications 16(2), 1971. doi:10.1137/1116025
• N. Sauer, On the density of families of sets, Journal of Combinatorial Theory, Series A 13(1), 1972. doi:10.1016/0097-3165(72)90019-2
• A. Ehrenfeucht, D. Haussler, M. Kearns, L. Valiant, A general lower bound on the number of examples needed for learning, Information and Computation 82(3), 1989. doi:10.1016/0890-5401(89)90002-3

Motivation

A decision-maker has $n$ projects, each a Markov reward process, and at every decision time may advance exactly one of them; the others stay frozen. Which project to advance so as to maximize the expected total discounted reward? Posed as a dynamic program the problem has a state space that is the product of the $n$ state spaces, and the size of that product defeats every general method. The index theorem of Gittins and Jones (1974) says the dynamic program is solved exactly by an index policy: there is a real number $\nu(B, x)$, computable for each bandit process $B$ from its own data and its own current state $x$, such that always advancing a process of greatest index is optimal. Chapter 2 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), introduces the index, proves the theorem three times, and works out the properties of the index that the rest of the book, from jobs and superprocesses to restless bandits, is built on: which stopping time attains it, how it is computed, how it moves with the discount factor, and when it collapses to the myopic rule.

The index theorem itself is already on the platform, proved, as BanditAlgorithm.gittins_index_theorem in the Bandit Algorithms series (Lattimore and Szepesvári, Theorem 35.9). This mission cites it and formalizes what Chapter 2 establishes around it.

Setting

A bandit process $B$ (§2.3–2.4) is a Markov reward process on a countable state space $E$: transition probabilities $P(y \mid x)$, a bounded reward $r(x)$ received each time the continuation control is applied in state $x$, and a discount factor $a \in (0, 1)$; the freeze control leaves the state unchanged and yields nothing. The law of the process started at $x$ is $\mathbb{P}_x$ and $x(t)$ is its state at process time $t = 0, 1, 2, \dots$. A stopping time $\tau$ is a past-measurable rule for switching from continuation to freezing, taking values in $\{1, 2, \dots\} \cup \{\infty\}$. For such $\tau$, $R_\tau(B, x) = \mathbb{E}_x[\sum_{t < \tau} a^t r(x(t))]$ is the expected discounted reward and $W_\tau(B, x) = \mathbb{E}_x[\sum_{t < \tau} a^t]$ the expected discounted time; their ratio $\nu_\tau(B, x)$ (2.7) is the equivalent constant reward rate of that portion of $B$. The Gittins index is

and, equivalently, the fair charge (2.5): the greatest rent $\lambda$ per period for which continuing $B$ for one or more periods, paying $\lambda$ each period, can be done without expected loss. A simple family of alternative bandit processes (SFABP) is $n$ such processes with a common discount factor, one of which is continued at each decision time; an index policy continues a process of greatest index. In the Lean development the single-arm model is the platform's (GittinsIndex): the chain law is built by the Ionescu–Tulcea construction, stopping times are adapted $\mathbb{N}\cup\{\infty\}$-valued maps on trajectories, and gittinsIndex P r a x is (2.6).

Formalization targets

Goal: Lemma 2.2, the optimal stopping set

The supremum in (2.6) is attained. For the initial state $\xi$, the attaining stopping rule may be taken to be "stop at the first time $t \ge 1$ at which the state lies in $\Sigma_0$" for any set $\Sigma_0$ with

and every such rule has $\nu_\tau(B, \xi) = \nu(B, \xi)$.

Milestones

Theorem 2.1 as a reference to the proved platform theorem; Eq. (2.5), the fair-charge characterization of the index; the restart-in-state formulation of §2.6.4 as the convergence of the Katehakis–Veinott value iteration; Theorem 2.3, monotonicity in the discount factor; Lemma 2.4, the interchange of two bandit portions; Propositions 2.5–2.8, the monotone-index cases in which the index is the immediate reward, or is attained only after the first step, or only at $\tau = \infty$.

Significance

Lemma 2.2 is the working form of the index: it turns the supremum over all stopping times into a specific rule, the first time the index falls below its starting value, and it is what the interchange proof of §2.7, the modified-forwards-induction policies of §2.6.6, the monotone-index propositions of §2.11 and the treatment of jobs in Chapter 3 all use. The fair-charge form (2.5) is the prevailing-charge proof of the theorem (Weber 1992) and the interpretation that carries over to superprocesses and restless bandits. The restart formulation is how indices are computed in practice (Katehakis and Veinott 1987), and Theorem 2.3 is the first of the comparative statics used throughout Chapters 7 and 8. Lemma 2.4 is the elementary inequality behind the original proof of Gittins and Jones.

Of these, only the index theorem has a machine-checked proof today. Formalizing the rest gives the platform the index as a usable object: a characterization of the optimal stopping rule, a convergent algorithm for it, and the monotonicity facts, all stated against the existing model so that every later mission of this series and every future use of the L&S model can build on them.

Difficulty

The obvious first move for Lemma 2.2, "take the stopping time that achieves the supremum", is what has to be proved: the supremum is over an uncountable family, and attainment comes from the optimal stopping problem with charge $\lambda = \nu(B, \xi)$, whose value function satisfies $\varphi(x) = \max\{0, r(x) - \lambda + a\mathbb{E}[\varphi(x(1)) \mid x(0) = x]\}$, together with the fact that its optimal stopping set is characterized by the strict and non-strict inequalities $\lambda > \nu(B, x)$ and $\lambda \ge \nu(B, x)$. That last step is the content: it identifies the local decision "stop or continue" with a comparison of indices, which is why any set between the two level sets works. On the platform's model this requires the dynamic-programming theory of discounted optimal stopping on a countable space (Theorem 2.10 of the book), the identification of fairChargeProfit with that value function, and the strong Markov property of markovChainMeasure at a trajectory stopping time. Theorem 2.3 needs randomized stopping times (a geometric kill) and the fact that they do not enlarge the supremum. The restart iteration is monotone and bounded but its operator is not a contraction in the restart value, so its limit has to be identified with the restart problem's value directly; that value is $\max(0, \nu/(1-a))$, not $\nu/(1-a)$, because restarting forever is free.

Formalization scope

The state space is a countable type with measurable singletons, so every subset is measurable; rewards are bounded; $a \in (0, 1)$. The chain law, stopping times, the discounted stopped sums and the index are the platform's, unchanged. Expectations are Bochner integrals; with bounded rewards they are finite and no total-function default value enters. IsPositiveStoppingTime fixes $\tau \ge 1$ everywhere, so $W_\tau \ge 1$ and the ratio (2.7) is a genuine quotient. The stopping rule of Lemma 2.2 is the hitting time from time $1$ of a set, with $\infty$ when the set is never hit. The fair-charge profit is a real supremum over the nonempty bounded family of positive stopping times, and (2.5) is stated with the outer supremum over $\{\lambda : \text{profit}(\lambda) \ge 0\}$, a nonempty set bounded above. The restart iteration is stated as a limit, with the value $\max(0, \nu(B, \xi)/(1-a))$: for a nonnegative index this is the book's $\nu/(1-a)$, and the maximum is forced by a one-state example with negative reward. The propositions' hypotheses are almost-sure events under $\mathbb{P}_x$, written as events of measure one.

Two trivializing readings are excluded: the index is never taken over all $\mathbb{N}\cup\{\infty\}$-valued maps but over adapted stopping times, and the stopping set of the goal is not restricted to the two extreme level sets. Contributions welcome: the optimal-stopping dynamic program on markovChainMeasure (value iteration, the strong Markov property at a stopping time), the equivalence of randomized and non-randomized stopping times for the supremum, and the monotone convergence of the restart iteration.

Selected references

• J. Gittins, K. Glazebrook, R. Weber, Multi-armed Bandit Allocation Indices, 2nd ed., Wiley, 2011, Chapter 2. doi:10.1002/9780470980033
• J. C. Gittins, D. M. Jones, A dynamic allocation index for the sequential design of experiments, in Progress in Statistics (Gani, ed.), North-Holland, 1974.
• R. Weber, On the Gittins index for multiarmed bandits, Annals of Applied Probability 2(4), 1992. doi:10.1214/aoap/1177005588
• M. N. Katehakis, A. F. Veinott, The multi-armed bandit problem: decomposition and computation, Mathematics of Operations Research 12(2), 1987. doi:10.1287/moor.12.2.262
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020, Chapter 35. doi:10.1017/9781108571401

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

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:

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]$,

Goal (Theorem 22(a), finite sample guarantees II). Under the same hypotheses, for every $\eta \in (0,1)$ and $\varepsilon \ge \varepsilon_N(\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.

Motivation

Every generalization bound in Chapters 2-11 depends only on the complexity of a fixed hypothesis set $H$ — Rademacher complexity, VC-dimension, growth function — and holds regardless of which algorithm within $H$ actually returns the hypothesis. This is both a strength (broad applicability) and a limitation: it throws away everything specific to how an algorithm searches $H$, and can be uninformative when $H$ itself is large or unbounded (e.g. a regularized objective that implicitly restricts the search without shrinking $H$ as a set). Chapter 14 introduces a fundamentally different route to a generalization bound — a property of the algorithm rather than the hypothesis class — first used by Devroye, Rogers and Wagner for $k$-nearest-neighbor rules and given its modern general form by Bousquet and Elisseeff (2002), whose treatment this chapter follows and (for non-differentiable convex losses) extends.

Setting

A labeled example is $z=(x,y)\in X\times Y$; for a loss function $L:Y'\times Y\to\mathbb R_+$ (where $Y'$ may differ from $Y$, e.g. $Y=\{-1,+1\}$ but $Y'=\mathbb R$ for a real-valued hypothesis), the loss of a hypothesis $h$ at $z$ is $L_z(h)=L(h(x),y)$. Given a learning algorithm $A$ that maps a sample $S$ of size $m$ to a hypothesis $h_S\in H$, the empirical error and generalization error are $\hat R_S(h)=\frac1m\sum_iL_{z_i}(h)$ and $R(h)=\mathbb E_{z\sim D}[L_z(h)]$. Uniform $\beta$-stability (Definition 14.1) says: for any two samples $S$, $S'$ differing by a single point, the algorithm's returned hypotheses satisfy $|L_z(h_S)-L_z(h_{S'})|\le\beta$ for every $z$ — replacing one training point can change the algorithm's loss on any point by at most $\beta$. For the regularized algorithms studied in §14.3, a kernel-based regularization algorithm minimizes $F_S(h)=\hat R_S(h)+ \lambda\|h\|_K^2$ over the RKHS $H$ of a positive-definite kernel $K$, and a loss $L$ is $\sigma$-admissible (Definition 14.3) if $|L(h'(x),y)-L(h(x),y)|\le\sigma|h'(x)-h(x)|$ for all hypotheses $h,h'$ — a Lipschitz-like smoothness condition satisfied by the standard regression and classification losses.

Formalization targets

Proposition 14.4 (milestone). For a PDS kernel $K$ with $K(x,x)\le r^2$ and a convex, $\sigma$-admissible loss $L$, the kernel-based regularization algorithm is $\beta$-stable with

Corollary 14.5 (milestone). For SVR (the $\epsilon$-insensitive loss $L_\epsilon$, bounded by $M$), with probability at least $1-\delta$:

Theorem 14.2 — the mission's goal. For a loss bounded by $M$ and a $\beta$-stable algorithm $A$, with probability at least $1-\delta$ over a sample $S$ of size $m$:

Significance

Theorem 14.2 is the book's demonstration that algorithm-dependent analysis is not merely a special-case curiosity: it is broad enough to cover an entire family (every kernel-based regularization algorithm — KRR, SVR, SVMs, and beyond) uniformly, via a single stability coefficient computation (Proposition 14.4) that is then specialized per algorithm just by plugging in that loss's admissibility constant $\sigma$. Corollary 14.5's SVR bound is the concrete payoff: a fully explicit, dimension-free generalization guarantee for a widely used regression algorithm, with every constant ($r$, $\lambda$, $m$) traceable to the algorithm's own hyperparameters, no VC-dimension or Rademacher-complexity computation required. Unlike Chapters 3-11, whose bounds are oblivious to how $H$ is searched, algorithmic stability is the first tool in the book that can, in principle, certify generalization for a hypothesis class too large or poorly understood for a complexity-based bound to be informative, provided the algorithm itself is stable. No prior art on the Prove2Me platform is faithful: GET /theorems?q=algorithmic+stability, q=uniform+stability return no hits; q=McDiarmid returns only bounded_diff_martingale_two_sided (Boucheron-Lugosi-Massart's own two-sided bounded-differences martingale inequality), which is McDiarmid's inequality's own proof engine (the background result Theorem 14.2's proof applies), not any result of this chapter — a different mathematical object entirely, not reused. All eleven items are drafted fresh.

Not formalized here: Corollary 14.6 (KRR bound), Lemma 14.7 (boundedness of kernel-regularization hypotheses) and Corollary 14.8 (SVM bound). Corollary 14.6 is structurally identical to Corollary 14.5 (a different loss function's admissibility constant plugged into the same Proposition 14.4 + Theorem 14.2 chain) and adds no new formalization content beyond Corollary 14.5, already drafted; Lemma 14.7 and Corollary 14.8 are omitted together, since 14.8's own statement needs 14.7's bound on $|h_S(x)|$ to compute its explicit $M$ (unlike Corollary 14.5, which is given $M$ as a hypothesis) — a genuine additional formalization layer (the reproducing-kernel norm bound $|h_S(x)|\le r\sqrt{B/\lambda}$) disproportionate to a single further corollary within this mission's budget.

Difficulty

The chapter's central technical step is recognizing that $\beta$-stability plus the loss bound $M$ together give exactly the bounded-difference property McDiarmid's inequality needs, applied to $\Phi(S)=R(h_S)-\hat R_S(h_S)$ as a function of the sample: replacing one point of $S$ changes $R(h_S)$ by at most $\beta$ (stability applied to the population loss, an expectation over $z$) and changes $\hat R_S(h_S)$ by at most $\beta+M/m$ (stability on the $m-1$ shared points, plus the full loss bound $M/m$ on the one point that actually changed) — two different, asymmetric arguments that must be combined correctly to get $|\Phi(S)-\Phi(S')|\le 2\beta+M/m$, not merely "stability implies boundedness" asserted directly. Proposition 14.4's own proof (not formalized here beyond its statement) needs a generalized Bregman divergence to handle a possibly non-differentiable convex loss — an extension of Bousquet-Elisseeff's original argument the book credits to itself as novel — via the reproducing-kernel property and Cauchy-Schwarz to convert a divergence bound into a bound on $\|h-h'\|_K$, then back into a pointwise loss bound.

Formalization scope

IsRKHSOf/IsMinimizer are restated locally in Stability, byte-identical to chunk 06-kernels's own copies (a draft item cannot import another chunk's draft module); H is an abstract real inner-product space with an evaluation map ev : H → X → ℝ standing for "elements of H are functions on X", the same device chunk 06's own RKHS formalization uses, since Mathlib's abstract Hilbert spaces are not themselves spaces of functions. UniformlyStable fixes the sample size m as part of the algorithm's type (A : (Fin m → X × Y) → (X → Y')), matching the book's own standing convention of a fixed sample size m throughout the chapter. Proposition 14.4 is stated pairwise — for any two samples differing by one point and any minimizers of their respective regularized objectives, the pointwise loss bound holds — rather than fixing a global choice-function algorithm A, since the book's own proof picks an arbitrary minimizer of each objective without asserting uniqueness; Corollary 14.5 does fix a choice function A (one minimizer per sample), since Theorem 14.2's own statement needs a single algorithm evaluated across the whole product-measure sample space. No numerical constant in any of the three theorems is altered from the book's own displayed form. A trivializing formalization this mission avoids: stating Theorem 14.2 only for the strict per-hypothesis loss bound (∀ h ∈ H, ∀ z, L_z(h) ≤ M) rather than the book's own weaker, algorithm-specific condition (hbound, ∀ S, ∀ z, L_z(A S) ≤ M) — the weaker hypothesis is kept, exactly matching the book's explicit statement that "a weaker condition suffices."

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 14.
• O. Bousquet, A. Elisseeff, "Stability and generalization," Journal of Machine Learning Research 2, 2002, 499-526.
• M. Kearns, D. Ron, "Algorithmic stability and sanity-check bounds for leave-one-out cross-validation," Neural Computation 11(6), 1999, 1427-1453.

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

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$,

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

Maximum entropy (Maxent) models are a widely used family of density-estimation algorithms: given a sample and a set of features, they select the distribution that matches the empirical feature averages while being otherwise as "agnostic" (close to a prior, usually uniform) as possible — a principle that, notably, never requires specifying a parametric family of distributions to search over. This mission formalizes the theorem that explains why this works in practice: Maxent's primal optimization (over distributions, subject to feature-matching constraints) is exactly dual to an unconstrained maximum-likelihood problem over a specific, rich parametric family — the Gibbs distributions — even though the Maxent principle never mentions that family at all.

Setting

For a sample $S=(x_1,\dots,x_m)$ drawn i.i.d. from $D$ over a finite set $X$, and a feature map $\Phi:X\to\mathbb R^N$ with $\|\Phi\|_\infty\le r$, the Maxent principle seeks $p\in\Delta$ (the simplex of distributions over $X$) minimizing the relative entropy $D(p\|p_0)$ to a prior $p_0$, subject to $\|E_{x\sim p}[\Phi(x)]-E_{x\sim\hat D}[\Phi(x)]\|_\infty\le\lambda$ (problem 12.7). Introducing the indicator function $I_K$ ($0$ on $K$, $+\infty$ elsewhere) turns this into the unconstrained primal objective $F(p)=\tilde D(p\|p_0)+I_C(E_p[\Phi])$ (Eq. 12.8), with $C$ the feature-constraint set. A Gibbs distribution with parameter $w\in\mathbb R^N$ is $p_w(x)=p_0(x)e^{w\cdot\Phi(x)}/Z(w)$, $Z(w)$ the partition function (Eq. 12.9); its associated dual objective is $G(w)=\frac1m\sum_i\log\frac{p_w(x_i)}{p_0(x_i)}-\lambda\|w\|_1$ (Eq. 12.10) — note $-\frac1m\sum_i\log p_w(x_i)$ is exactly the empirical log-loss $L_S(w)$, so maximizing $G$ is minimizing an L1-regularized log-loss over the Gibbs family.

Formalization targets

Theorem 12.2 — the mission's goal (Maxent duality). $\sup_{w\in\mathbb R^N}G(w)=\min_pF(p)$. Furthermore, letting $p^*=\arg\min_pF(p)$ and $d^*=\sup_wG(w)$: for any $\epsilon>0$ and any $w$ with $|G(w)-d^*|<\epsilon$, $D(p^*\|p_w)\le\epsilon$.

Theorem 12.3 (Maxent L1-regularization generalization bound, milestone). Fix $\delta>0$. Let $\hat w$ solve the L1-regularized dual (12.12) with $\lambda=2R_m(H)+r\sqrt{\log(2/\delta)/(2m)}$. Then, with probability at least $1-\delta$,

Significance

Theorem 12.2 is one of the most striking dualities in the book: the Maxent principle, phrased purely in terms of closeness to a prior distribution, turns out to always produce a solution in the Gibbs family — not because that family was ever specified, but because relative entropy is the specific measure of closeness whose Fenchel conjugate is the log-partition function. This explains a whole zoo of models (log-linear models, exponential families, Gaussian and bimodal Gibbs distributions from quadratic features) as instances of a single duality theorem, and gives a computationally friendlier route to the (constrained, infinite-if-$X$-is-large) primal problem via the (unconstrained, $N$-dimensional) dual. The theorem's proof is a genuine application of conditional (Fenchel) strong duality, not an unconditional fact — this is, per the chapter's own brief, the sharpest trivialization risk in the entire mission series, since "strong duality always holds for convex problems" is false in general, and a formalization skipping the book's own qualification condition ($\lambda>0$, placing $u_0$ in the interior of the constraint set) would prove a different, potentially-false statement. No prior art on the platform is faithful: GET /theorems?q=maximum+entropy returns no hits, and Mathlib's generic Fenchel-conjugate machinery (Analysis/Convex/Conjugate) does not package the book's own specific qualification conditions as a single reusable theorem matching Theorem B.39 — reusing it inside a proof (not the audited statement) remains available to whoever proves this theorem later.

Not formalized here: Theorem 12.4 (a Bregman-divergence generalization of Theorem 12.2) and Theorem 12.5 (its L2-regularized concrete special case). BRIEF.md itself flags Theorem 12.4 as possibly too heavy and offers Theorem 12.5 as an easier alternative; this mission omits both, since even Theorem 12.5 requires a second, structurally parallel dual-objective-and-minimizer formalization (for L2 rather than L1 regularization) — disproportionate to this mission's budget once Theorem 12.2's own qualification-condition bookkeeping (the heaviest single item in this mission series) is accounted for. §12.1 (density estimation without features: ML/MAP), §12.7 (coordinate descent), and §12.8-12.9 (Bregman-divergence extensions, L2-regularization in general) are likewise out of scope, per BRIEF.md's own page-range restriction.

Difficulty

Theorem 12.2's proof is the book's own explicit application of the Fenchel duality theorem (Theorem B.39, Appendix B) to the specific triple $f(p)=\tilde D(p\|p_0)$, $g(u)=I_C(u)$, $Ap=\sum_xp(x)\Phi(x)$ — every qualification condition (A a bounded linear map, u_0\in A(\mathrm{dom}f)\cap\mathrm{cont}(g), needing \lambda>0 to place u_0 in int(C)) must be checked for this triple, not assumed generically; the conjugate computations themselves (f^*(q)=\log\sum_xp_0(x)e^{q(x)}$ via Lemma B.37, g^(w)=E_{\hat D}[w\cdot\Phi]+\lambda|w|_1 via the dual-norm identity) are specific algebraic derivations, not immediate from abstract duality alone. The second clause's proof needs a further, non-obvious algebraic identity (G(w)-D(p^|p_0)+D(p^|p_w)expanding, via Hölder's inequality applied to the primal feasibility ofp^, to something \le0) that is not a restatement of the first clause but a separate argument built on top of it. Theorem 12.3's proof structurally mirrors chunk 04's SRM bound (bounding L_D(\hat w)-L_S(\hat w)via Hölder's inequality and the Rademacher-complexity feature-concentration bound of Eq. 12.5, then using\hat w`'s optimality twice), but is applied to the log-loss of a Gibbs distribution rather than a generic bounded loss.

Formalization scope

MaxEntPrimalObjective uses EReal (the extended reals) so that the book's own +\infty values (from I_K, \tilde D) are represented exactly, matching the chapter's own explicit use of an extended-real-valued indicator function rather than a soft penalty — a trivializing formalization this mission avoids is silently replacing +\infty with a large real sentinel, which would misstate a convex-analysis object whose entire role in the proof is its infinite value outside the feasible/simplex set. hlam : 0 < lam is a genuine load-bearing hypothesis in the goal theorem, matching the book's own use of \lambda>0 to invoke Theorem B.39's qualification condition — not a free convexity assumption; this is the mission's central faithfulness guard against the chapter's own named trivialization risk. EmpiricalRademacherComplexity/ RademacherComplexity are restated locally, byte-identical to chunks 05-svm/07-boosting's own copies (a draft item cannot import another chunk's draft module). p^* in the goal theorem and \hat w in Theorem 12.3 are both quantified via explicit hypotheses (IsLeast, a minimizer inequality) rather than assumed to exist unconditionally, matching the book's own "let p^*=..."/"let \hat w be a solution of..." phrasing without asserting existence or uniqueness beyond what the book itself asserts. No numerical constant in either theorem is altered from the book's own displayed form.

Selected references

• M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT Press, 2018, Chapter 12, §12.1-12.6.
• E. T. Jaynes, "Information theory and statistical mechanics," Physical Review 106(4), 1957, 620-630.
• S. Della Pietra, V. Della Pietra, J. Lafferty, "Inducing features of random fields," IEEE Transactions on Pattern Analysis and Machine Intelligence 19(4), 1997, 380-393.