The science of systems that learn from data and experience. Its scope runs from the statistical and mathematical foundations of learning, including generalization, expressivity, and computational limits, through the design of learning algorithms, deep learning, reinforcement learning, and probabilistic methods, to the empirical study of large models and the trustworthiness, interpretability, and societal impact of learned systems.
The Principles of Deep Learning Theory III: Preactivation Statistics in the First Two LayersTextbook
Motivation
Chapter 4 of The Principles of Deep Learning Theory by D. A. Roberts and S. Yaida (arXiv:2106.10165) begins the analysis of general multilayer perceptrons (MLPs) with a nonlinear activation function σ at initialization. The first layer is exactly Gaussian; the second layer is the first place where non-Gaussianity appears, as a connected four-point correlator suppressed by 1/n1 and governed by the four-point vertexV(2). This mission formalizes §§4.1–4.2, which are exact at any width. It is the third mission in a series formalizing the book (namespace DeepLearningTheory) and reuses the definitions of Mission II (Deep Linear Networks at Initialization).
Setting
An MLP with widths n0,n1,n2,… and activation σ:R→R maps inputs xα∈Rn0 to preactivations
(eqs. 4.2, 4.30). At initialization all biases and weights are independent centered Gaussians with E[bi(ℓ)bj(ℓ)]=δijCb(ℓ) and E[Wi1j1(ℓ)Wi2j2(ℓ)]=δi1i2δj1j2CW(ℓ)/nℓ−1 (eqs. 4.3–4.4). The first-layer metric is Gα1α2(1)=Cb(1)+CW(1)n01∑jxj;α1xj;α2 (eq. 4.8), and ⟨F(zα1,…,zαm)⟩g denotes the expectation over a centered Gaussian vector (zα) with covariance g (eq. 4.25), with σα≡σ(zα).
Eq. (4.9) — first-layer four-point correlator is the Wick value.
Eq. (4.23) — the first-layer preactivations are exactly Gaussian with covariance δi1i2Gα1α2(1).
Eqs. (4.27), (4.28), (4.29) — activation correlators in the first layer as Gaussian expectations.
Eq. (4.40) — two-point correlator of the second-layer metric fluctuation.
Eq. (4.41) — second-layer two-point correlator.
Significance
These identities are the base case of the book's recursion (Chapter 4.3 onward) for the kernel and four-point vertex in deeper layers, and they show concretely that a finite-width network is not a Gaussian process: the 1/n1 connected correlator is generically nonzero for nonlinear σ. The results are exact computations in the book; this mission formalizes them.
Difficulty
The second layer is a Gaussian conditional on the first layer, with a random covariance (the stochastic metric, eq. 4.36). Turning this into unconditional correlators requires conditioning on the first-layer preactivations, independence of different first-layer neurons, and the identification of first-layer activation correlators with Gaussian expectations over the metric G(1), which may be degenerate (e.g. repeated inputs). Integrability of σ against Gaussians must be controlled.
Formalization scope
Definitions from Mission II are reused: kron, inputKernel, WeightIndex. New definitions: mlpPreact (zi(ℓ)(x)), IsMLPInit (independent Gaussian biases and weights with layer-dependent Cb(ℓ),CW(ℓ)), firstLayerMetric (G(1) on finitely many inputs), gaussAvg (⟨⋅⟩g, via Mathlib's multivariateGaussian, which handles singular positive-semidefinite g), and HasPolyGrowth.
Statements about activations assume σ measurable with polynomial growth, the standing convention guaranteeing that all Gaussian averages are finite; this covers ReLU, tanh, sigmoid, GELU, SWISH and the perceptron step function.
The sample set is Fin D (for the specific statements, D=2 or 4 inputs, possibly repeated). n1>0 is assumed where the formulas divide by n1.
Selected references
D. A. Roberts, S. Yaida (with B. Hanin), The Principles of Deep Learning Theory, Cambridge University Press, 2022, Chapter 4. arXiv:2106.10165
Chapter 13 showed that convex-Lipschitz-bounded and convex-smooth-bounded problems are learnable by regularized loss minimization; Chapter 14 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) shows how to learn them with the simplest possible algorithm. Gradient descent moves against the gradient with a fixed step size and outputs the average of its iterates; its analysis (Lemma 14.1) is a single telescoping identity that bounds ∑t⟨w(t)−w⋆,vt⟩ for any sequence of directions vt, and this generality is the whole point. It gives the rate Bρ/T for convex Lipschitz functions (Corollary 14.2), extends to nondifferentiable functions through subgradients (Definition 14.4, Lemmas 14.3 and 14.7), and, because it never used that the directions were gradients, extends to stochastic gradient descent, in which each direction is random with a subgradient as its conditional expectation (Theorem 14.8). Applied to the risk LD(w) with a fresh example at each step, SGD is a learning algorithm whose sample complexity is the iteration count: B2ρ2/ϵ2 examples for convex-Lipschitz-bounded problems (Corollary 14.12) and 12B2β/ϵ2 for convex-smooth-bounded ones (Theorem 14.13, Corollary 14.14). A projected, decreasing-step variant for strongly convex objectives has rate (ρ2/(2λT))(1+logT) (Theorem 14.11).
Setting
Hypotheses are vectors in Rd; convex, Lipschitz and smooth losses, convex-Lipschitz-bounded and convex-smooth-bounded problems, and strong convexity are those of Mission IX. A vector v is a subgradient of f at w if f(u)≥f(w)+⟨u−w,v⟩ for all u. The iterates of an update rule w(1)=0, w(t+1)=w(t)−ηvt are indexed from 0, and the output after T steps is wˉ=T1∑t<Tw(t). The randomness of SGD is modelled as the chapter uses it in §14.5: a sample z0,…,zT−1 drawn i.i.d. from D and an oracle g with vt=g(w(t),zt), where g is a stochastic subgradient oracle for f if Ez∼Dg(w,z)∈∂f(w) for every w. This is the book's condition E[vt∣w(t)]∈∂f(w(t)) in the case where the direction depends on the past only through w(t) and on fresh randomness, which is what every application in the book does; the expectation E[f(wˉ)] is then an integral over DT. For learning, g(w,z) is a subgradient of ℓ(⋅,z) at w, so that Ezg(w,z) is a subgradient of LD at w (14.13). The projection of w onto a convex set H is a nearest point of H, and the strongly convex variant projects after each step with step size 1/(λt).
Formalization targets
Goal: Theorem 14.8
For a convex f, B,ρ>0, a measurable oracle g with Ezg(w,z)∈∂f(w) and ∥g(w,z)∥≤ρ, any w⋆ with ∥w⋆∥≤B, T≥1 and η=B/(ρT): E[f(wˉ)]−f(w⋆)≤Bρ/T; and for every ϵ>0, T≥B2ρ2/ϵ2 gives E[f(wˉ)]−f(w⋆)≤ϵ.
Milestones
Lemma 14.1. For any directions, ∑t<T⟨w(t)−w⋆,vt⟩≤∥w⋆∥2/(2η)+(η/2)∑t<T∥vt∥2; with ∥vt∥≤ρ, ∥w⋆∥≤B and η=B/(ρT) the average is at most Bρ/T.
Corollary 14.2. Subgradient descent on a convex ρ-Lipschitz f with η=B/(ρT) has f(wˉ)−f(w⋆)≤Bρ/T for every ∥w⋆∥≤B, and T≥B2ρ2/ϵ2 gives ϵ.
Lemma 14.7. A convex f on Rd is ρ-Lipschitz iff all its subgradients have norm at most ρ.
Lemma 14.9. For the projection v of w onto a convex H and u∈H, ∥w−u∥2≥∥v−u∥2.
Theorem 14.11. For λ-strongly convex f, a closed convex H, an oracle with Ez∥g(w,z)∥2≤ρ2 and any w⋆∈H, the projected variant with ηt=1/(λt) has E[f(wˉ)]−f(w⋆)≤(ρ2/(2λT))(1+logT).
Corollary 14.12. SGD on the risk of a convex-Lipschitz-bounded problem with T≥B2ρ2/ϵ2 examples has E[LD(wˉ)]≤LD(w)+ϵ for every w∈H.
Theorem 14.13. For convex, β-smooth, nonnegative losses and ηβ<1, SGD with gradient directions has E[LD(wˉ)]≤1−ηβ1(LD(w⋆)+∥w⋆∥2/(2ηT)).
Corollary 14.14. For a convex-smooth-bounded problem with ℓ(0,z)≤1 and any ϵ>0, SGD with η=1/(β(1+3/ϵ)) and T≥12B2β/ϵ2 has E[LD(wˉ)]≤LD(w)+ϵ for every w∈H.
Further items: Lemma 14.3, Claims 14.5, 14.6 and 14.10, and the hinge-loss subgradient of Example 14.2.
Significance
SGD is the algorithm behind most of modern machine learning, and Theorem 14.8 is its basic guarantee: dimension-free, independent of the form of f beyond convexity, and with a sample complexity matching the regularization bound of Chapter 13 up to a constant. Lemma 14.1 isolates the deterministic identity that makes both gradient descent and its stochastic version work, and Lemma 14.7 is the bridge between the Lipschitz assumption of Chapter 12 and the bounded directions the analysis needs. The learning corollaries make the point that runs through Part II of the book: for convex problems, optimization and learning are the same activity, and one pass over the data suffices.
Nothing here is machine-checked. The chapter's statements are essentially correct, and the formalization records the reading choices rather than corrections: the i.i.d.-oracle model of the randomness, the subgradient form of gradient descent, the bound at every point of the ball rather than at a minimizer, and, in Corollary 14.14, the assumptions ϵ≤1 and 0∈H under which the derivation from Theorem 14.13 goes through.
Difficulty
Lemma 14.1 is a completed square and a telescoping sum and is the intended entry point; the Bρ/T clause is the substitution of η. Corollary 14.2 is Lemma 14.1 with Jensen's inequality for the average and the subgradient inequality at each iterate, plus Lemma 14.7 to bound the directions. The subgradient facts need convex analysis: Lemma 14.3 in the direction "convex implies subgradients exist" is the supporting hyperplane theorem on Rd, which Mathlib does not offer directly; Claim 14.5 uses the first-order characterization of convexity for differentiable functions; Lemma 14.7's "Lipschitz implies bounded subgradients" is the book's one-line argument along u=w+ϵv/∥v∥. Theorem 14.8 is Lemma 14.1 plus the conditioning argument of the book, which in the i.i.d.-oracle model is Fubini on the product DT: the iterate w(t) is a measurable function of z0,…,zt−1, and integrating ⟨w(t)−w⋆,g(w(t),zt)⟩ over zt first gives ⟨w(t)−w⋆,Ezg(w(t),z)⟩≥f(w(t))−f(w⋆). Theorem 14.11 adds the projection lemma, the strong-convexity inequality of Claim 14.10, the telescoping of 2λt(at−at+1)−2λat and the harmonic sum ∑t≤T1/t≤1+logT; the second-moment hypothesis makes E∥w(t)−w⋆∥2 finite inductively. Corollary 14.12 is Theorem 14.8 for f=LD with the oracle of (14.13), which requires exchanging a subgradient inequality with the integral over z. Theorem 14.13 replaces the Lipschitz bound by self-boundedness, ∥∇ℓ∥2≤2βℓ, and rearranges; Corollary 14.14 is its arithmetic under the added assumptions. In all expectation statements the measurability of the iterates in the sample, from the measurability of the oracle, is a routine but necessary lemma.
Formalization scope
Iterates are defined by structural recursion, so no argmin is chosen; the sample-driven SGD stops after T updates; the projection onto H is a chosen nearest point, unique for closed convex H. Bounds are stated for every w⋆ in the ball (or in H) rather than for a minimizer, which is what the proofs give and is stronger. The oracle bound ∥g(w,z)∥≤ρ is required surely (the book: with probability 1); the almost-sure version is a routine extension. The second-moment hypothesis of Theorem 14.11 is a lower Lebesgue integral, so that a non-integrable oracle cannot satisfy it vacuously. The learning corollaries assume a measurable loss, nonnegative and bounded at the origin, so that the risks are genuine integrals, and a measurable selector of subgradients. Variable step sizes (§14.4.2), other averaging schemes (§14.4.3), SGD for regularized loss minimization (§14.5.3) and the exercises are not stated.
Trivializing readings are excluded: the expectations are over the product law of the examples with measurable integrands, the subgradient conditions are pointwise inequalities, and the iteration counts are the book's. Welcome contributions: Lemma 14.1 as a reusable telescoping lemma, the measurability of the SGD iterates, and the Fubini step that turns an oracle condition into the inequality (14.10).
Selected references
S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 14. doi:10.1017/CBO9781107298019
H. Robbins, S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22(3), 1951. doi:10.1214/aoms/1177729586
M. Zinkevich, Online convex programming and generalized infinitesimal gradient ascent, Proceedings of ICML, 2003.
A. Nemirovski, A. Juditsky, G. Lan, A. Shapiro, Robust stochastic approximation approach to stochastic programming, SIAM Journal on Optimization 19(4), 2009. doi:10.1137/070704277
S. Shalev-Shwartz, Online learning and online convex optimization, Foundations and Trends in Machine Learning 4(2), 2012. doi:10.1561/2200000018
Understanding Machine Learning IX: Convex Learning Problems, Regularization and StabilityTextbook
Motivation
Chapters 12 and 13 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) leave binary classification for the general framework in which a hypothesis is a vector w∈Rd and the loss ℓ(w,z) is a convex function of w. Convexity makes the ERM problem tractable (Lemma 12.11), but Examples 12.8 and 12.9 show that convexity, even with a bounded class, does not by itself make a problem learnable: one-dimensional linear regression with the squared loss defeats every learner. The chapter therefore isolates two families, the convex-Lipschitz-bounded and the convex-smooth-bounded problems (Definitions 12.12 and 12.13), and Chapter 13 proves that both are learnable, not by ERM but by Regularized Loss Minimization with Tikhonov regularization, A(S)∈argminwLS(w)+λ∥w∥2. The proof goes through a new idea: stability. Theorem 13.2 expresses the expected overfitting E[LD(A(S))−LS(A(S))] exactly as the expected effect of replacing one training example, strong convexity of the regularized objective bounds that effect (Lemma 13.5, Corollaries 13.6 and 13.7), and balancing the regularization against the fit gives oracle inequalities (Corollaries 13.8 and 13.10) and sample-complexity guarantees (Corollaries 13.9 and 13.11), with ridge regression as the worked example (Theorem 13.1).
Setting
Hypotheses are vectors in Rd with the Euclidean norm, as in Mission VI; risk, empirical risk, the product law of a sample and agnostic PAC learnability are those of Mission I. A problem is convex when H is convex and every ℓ(⋅,z) is convex; it is convex-Lipschitz-bounded with parameters ρ,B when moreover ∥w∥≤B on H and every ℓ(⋅,z) is ρ-Lipschitz on Rd, and convex-smooth-bounded with parameters β,B when every ℓ(⋅,z) is nonnegative and differentiable with a β-Lipschitz gradient. Lipschitzness and smoothness are required on all of Rd because the RLM rule is unconstrained and its outputs need not lie in H. The RLM rule is a relation: w is an output on S if it minimizes LS(w)+λ∥w∥2 over Rd, and a learner implements the rule if all its outputs are minimizers. For the losses of the chapter the minimizer exists and is unique. Given S=(z1,…,zm) and a further example z′, S(i) is S with zi replaced by z′; a learner is on-average-replace-one-stable with rate ϵ(m) if E(S,z′)∼Dm+1,i∼U(m)[ℓ(A(S(i)),zi)−ℓ(A(S),zi)]≤ϵ(m) for every distribution. Strong convexity is Mathlib's StrongConvexOn, which is Definition 13.4 verbatim.
Expectations over samples are integrals against product laws. For them to be genuine, the theorems about arbitrary learners assume a jointly measurable loss bounded by a constant and a measurable learner, and the theorems about RLM assume a jointly measurable, nonnegative loss bounded at the origin and a measurable learner; for RLM the latter is automatic, since the minimizer is unique.
Formalization targets
Goal: Corollary 13.9
For a convex-Lipschitz-bounded problem with parameters ρ,B>0 and the RLM learner with λ(m)=2ρ2/(B2m): for every distribution, every m≥1 and every w∈H, ES[LD(A(S))]≤LD(w)+ρB8/m; hence for every ϵ>0 and m≥8ρ2B2/ϵ2, ES[LD(A(S))]≤LD(w)+ϵ.
Milestones
Examples 12.8–12.9. Linear regression on R with the squared loss is not agnostic PAC learnable, over H=R or over H=[−1,1].
Theorem 13.2. For any measurable learner and m≥1, ES[LD(A(S))−LS(A(S))] equals the replace-one expectation of (13.6).
Lemma 13.5.λ∥w∥2 is 2λ-strongly convex; a strongly convex function plus a convex one is strongly convex; at a minimizer u of a λ-strongly convex f, f(w)−f(u)≥2λ∥w−u∥2.
Corollary 13.6. For a convex ρ-Lipschitz loss and λ>0, RLM satisfies ℓ(A(S(i)),zi)−ℓ(A(S),zi)≤2ρ2/(λm) for every S,z′,i, is stable with that rate, and has ES[LD(A(S))−LS(A(S))]≤2ρ2/(λm).
Corollary 13.7. For a convex, nonnegative, β-smooth loss and λ≥2β/m, the replace-one expectation is at most (48β/(λm))E[LS(A(S))], and at most 48βC/(λm) if ℓ(0,z)≤C.
Corollary 13.8.ES[LD(A(S))]≤LD(w∗)+λ∥w∗∥2+2ρ2/(λm) for every w∗.
Corollary 13.11. A convex-smooth-bounded problem with ℓ(0,z)≤1 is learned by RLM with λ=ϵ/(3B2) once m≥150βB2/ϵ2.
Theorem 13.1. Ridge regression on the unit ball with labels in [−1,1], λ=ϵ/(3B2) and m≥150B2/ϵ2 has ES[LD(A(S))]≤min∥w∥≤BLD(w)+ϵ.
Further items: Lemma 12.11, the hinge loss as a convex surrogate of the 0–1 loss, the stability-implies-no-overfitting remark of §13.2, and the ridge regression system (13.4)–(13.5).
Significance
Stability is the third route to learnability in the book after uniform convergence and nonuniform learnability, and the only one that applies to convex-Lipschitz-bounded problems in general, for which uniform convergence can fail (the book's Exercise 13.2). The chain from strong convexity through replace-one stability to oracle inequalities is the template for the analysis of every regularized learner, and Theorem 13.2 is an exact identity, not a bound. Ridge regression, support vector machines (Chapter 15) and the regularized algorithms of later chapters are all instances.
Nothing here is machine-checked. The sample sizes of Corollary 13.11 and Theorem 13.1 are the book's 150. Chaining Corollary 13.10 as printed would need 216, but the derivation of Corollary 13.7 actually gives the stability rate 20β/(λm), with which 90 suffices.
Difficulty
Lemma 12.11 and the hinge surrogate are direct. Lemma 13.5 is elementary but part (3) needs the limit α→0 of the strong-convexity inequality at a minimizer. Examples 12.8–12.9 require constructing the two finitely supported distributions of the book and computing the risk of a fixed output on each; the probability that all m examples are of the second type is at least 0.99 under both, and the deterministic learner's output on that sample decides which distribution defeats it. Theorem 13.2 is the exchangeability argument of the book: E[ℓ(A(S),z′)]=E[ℓ(A(S(i)),zi)] because swapping zi and z′ preserves the product law; the formal work is the measure-preserving transposition on Zm+1 and the integrability of the functions involved. Corollaries 13.6 and 13.7 follow the book's pointwise derivation from (13.7) to (13.11) and (13.12) to (13.14), where the smooth case uses the self-boundedness ∥∇ℓ∥2≤2βℓ of nonnegative smooth functions and the inequality (a+b)2≤3(a2+b2); passing to expectations then uses Theorem 13.2 and, for the smooth case, the symmetry E[ℓ(A(S(i)),z′)]=E[ℓ(A(S),zi)]. Corollaries 13.8 to 13.11 are the arithmetic of the book once (13.16), E[LS(A(S))]≤LD(w∗)+λ∥w∗∥2, is in hand, with the corrected constant for 13.11. The ridge system is the gradient condition for a strongly convex quadratic, and Theorem 13.1 is Corollary 13.11 applied to 21(⟨w,x⟩−y)2, which is ∥x∥2-smooth with ℓ(0,z)=y2/2≤1/2 on the support. In every expectation statement the measurability of S↦A(S) for the RLM rule, which the theorems take as a hypothesis, is provable from uniqueness of the minimizer and is worth a lemma.
Formalization scope
Losses are real-valued functions of a vector and an example; Lipschitz and smoothness conditions are global on Rd. The RLM rule is a minimizer relation with the regularization parameter as an explicit argument, and Corollary 13.9's learner uses a parameter depending on m. Stability quantifies over m≥1 and averages over the replaced index. Expectation statements carry measurability hypotheses that make every integral genuine, and the theorems about arbitrary learners assume a bounded loss. The minimum over H is stated as "for every w∈H", so no minimizer is needed. Definitions 12.1–12.9 and Claims 12.4–12.9 (general convex analysis) are not restated, nor are Examples 12.10–12.11, the discussion of §12.3 beyond the surrogate property, Remark 13.1, and Exercises 12.1–12.4 and 13.1–13.2.
Trivializing readings are excluded: the nonlearnability examples are stated as negations of the framework's learnability, the stability identity is an equality with both sides genuine integrals, and the constants of the oracle inequalities are the book's. Welcome contributions: the transposition invariance of product laws behind Theorem 13.2, the bound ∥A(S)∥2≤LS(0)/λ for RLM outputs, the measurability of the RLM minimizer, and the self-boundedness inequality (12.6).
Selected references
S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapters 12 and 13. doi:10.1017/CBO9781107298019
O. Bousquet, A. Elisseeff, Stability and generalization, Journal of Machine Learning Research 2, 2002.
S. Shalev-Shwartz, O. Shamir, N. Srebro, K. Sridharan, Learnability, stability and uniform convergence, Journal of Machine Learning Research 11, 2010.
A. N. Tikhonov, On the stability of inverse problems, Doklady Akademii Nauk SSSR 39(5), 1943.
Flow Matching Theorem 1: Marginal Continuity EquationResearch Paper
From conditional motion to a marginal probability path
Flow matching models a changing probability distribution using a time-dependent velocity field. A conditional model specifies a density and a velocity separately for each conditioning point. The mathematical question is whether those conditional descriptions determine a velocity for the mixture distribution. This mission concerns the continuity-equation formulation of Theorem 1 of Lipman, Chen, Ben-Hamu, Nickel, and Le, Flow Matching for Generative Modeling (ICLR 2023). The source is arXiv:2210.02747v2, Section 3.1 and Appendix A.
Densities, velocities, and probability flux
Fix a natural number d and let E=Rd. The conditioning distributionQ is a Borel probability measure on E. At time t, position x, and conditioning point z, write ρ(t,x,z) for the conditional density and v(t,x,z)∈E for the conditional velocity. The variable x is integrated against Lebesgue measure; z is integrated against Q. These roles remain distinct even though both variables take values in the same space.
The conditional flux is F(t,x,z)=ρ(t,x,z)v(t,x,z). The marginal density, marginal flux, and marginal velocity are defined by
These definitions express equations (6) and (8) using a probability measure rather than a data-density function. This representation also allows discrete conditioning distributions. Every conditional density is strictly positive and normalized on 0≤t≤1, jointly measurable in (x,z), and integrable in z at each fixed (t,x).
The divergence of a differentiable vector field is the sum of the diagonal entries of its derivative. A density and velocity satisfy the classical continuity equation when their flux is spatially differentiable and the density has time derivative equal to minus that divergence.
Formalization targets
The goal asserts that p(t,⋅) is a positive probability density for every t∈[0,1] and that
∂tp(t,x)+divx(p(t,x)u(t,x))=0(0<t<1,x∈E).
The hypotheses require the conditional continuity equation for Q-almost every conditioning point, at each interior time and spatial point. They also specify a sufficient local domination package for differentiation under the integral. This is an explicit classical interpretation of the regularity qualification in the proof of Theorem 1.
Four supporting targets isolate the mathematical assertions used by this formulation: the probability-density property of equation (6); time differentiation under the conditioning integral; spatial divergence under the conditioning integral; and the velocity/flux identity corresponding to equation (8). The source contains these equations and operations rather than separately numbered supporting lemmas, so the milestone titles identify the relevant equation or proof passage.
What completing the formalization provides
The deliverable is a checked interface for passing from a measurable family of conditional continuity equations to the continuity equation of its mixture. It records which variables are differentiated, which measure is used for averaging, where positivity is needed, and which assumptions justify each analytic operation. The time and spatial differentiation lemmas are stated for general measures and integrands, making them reusable outside this particular probability model.
The mathematical result is already proved in the cited paper. The uploaded theorem items are open formalization targets, with explicit proof placeholders. Successful local compilation checks their types and imports; it does not establish their conclusions. The definition module contains no proof placeholders.
Analytic obligations
Pointwise differentiability of every conditional function does not by itself justify differentiating an integral over the conditioning variable. The regularity predicates therefore require a neighborhood independent of that variable, an integrable bound for the derivative norm throughout that neighborhood, and almost-everywhere measurability of the integrand and derivative. Time and space receive separate predicates because their derivatives take values in different spaces.
There is also a distinction between density normalization in x and integrability in z at a fixed position. The formal assumptions record both. A probability measure on the conditioning space does not make every measurable function integrable. These conditions prevent the totalized Bochner integral from silently supplying a default value where an intended integral fails to exist.
Formalization scope
Space is represented by Fin d → ℝ, with its standard finite-product Borel structure and Lebesgue measure. Its norm is the standard product norm used by mathlib. All finite dimensions, including dimension zero, are included. Time-dependent functions are defined on all real times, while density assumptions apply on the closed unit interval and derivative conclusions apply on its interior. No endpoint time derivative is asserted.
The regularity package is one sufficient realization of the source's Leibniz-rule assumption, not a claim to the weakest possible hypotheses. Conditional continuity equations may hold almost everywhere in the conditioning variable; their exceptional sets may depend on the fixed time and position. Spatial differentiability of the marginal flux is part of the conclusion, so the equation cannot be satisfied merely through the default value of an undefined derivative.
The target is the PDE formulation. It does not assert existence of a global ODE flow, uniqueness of transported measures, or equality with a flow pushforward. Those require a separate transport development. It also asserts no endpoint approximation to a data distribution and no theorem about optimization, neural networks, or Gaussian paths. No marginal continuity equation or differentiation–integration interchange is assumed as an input.
Required infrastructure consists of Bochner integration, finite-dimensional differentiation, finite sums of derivative coordinates, and product-measure integration. Contributions may prove the supporting targets or the goal directly while preserving their statements and the distinction between classical PDE and flow-transport claims.
Selected references
Yaron Lipman, Ricky T. Q. Chen, Heli Ben-Hamu, Maximilian Nickel, and Matt Le. Flow Matching for Generative Modeling. ICLR 2023. arXiv:2210.02747v2, Section 2, Section 3.1, Theorem 1, equations (6), (8), and (26), and Appendix A's proof of Theorem 1.
Understanding Machine Learning VII: Boosting and AdaBoostTextbook
Motivation
Boosting answers a question raised by Kearns and Valiant: can a learner that is only slightly better than random guessing be turned into one that is arbitrarily accurate? Chapter 10 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) defines γ-weak learnability (Definition 10.1), the PAC requirement with the accuracy ϵ replaced by the fixed value 1/2−γ, and presents AdaBoost, the algorithm of Freund and Schapire that, given weak hypotheses, reweights the training set round by round and outputs a weighted majority vote. The chapter's main result (Theorem 10.2) is that the training error of AdaBoost's output decreases as e−2γ2T in the number of rounds. Since the output is a halfspace over the predictions of T base hypotheses, the chapter then bounds the VC-dimension of that class (Lemma 10.3), so that the number of rounds becomes a knob for the bias–complexity tradeoff. Example 10.1 shows a concrete weak learner, ERM over decision stumps for the class of 3-piece classifiers on the line, and the chapter remarks that, statistically, weak learnability is no easier than strong learnability: a class of infinite VC-dimension is not weakly learnable either.
Setting
The framework is that of Missions I and IV: binary classification over a domain X with the 0–1 loss, distributions D over X with a labeling function f, learners as functions of the sample, the VC-dimension, and ERM. Labels and hypotheses are Boolean, with ±1 values obtained through sgn(true)=1, sgn(false)=−1, and sign(z) is true exactly when z>0. A γ-weak learner for H with the function mH:(0,1)→N returns, for every δ, every D and every measurable f realizable by H, a hypothesis with L(D,f)(h)≤1/2−γ with probability at least 1−δ once m≥mH(δ); the failure event is bounded in outer measure as in Definition 3.1.
AdaBoost is formalized as a deterministic function of the sample S=(x1,y1),…,(xm,ym) and of the sequence of weak hypotheses h0,h1,… that the weak learner returned. The distributions are defined by recursion: D(0) is uniform, ϵt=∑iDi(t)1[ht(xi)=yi], wt=21log(1/ϵt−1), and Di(t+1)∝Di(t)exp(−wtyiht(xi)); the output after T rounds is x↦sign(∑t<Twtht(x)). Rounds are indexed from 0, so D(0) is the book's D(1). The class L(B,T) of Equation (10.4) consists of the functions x↦sign(∑t=1Twtht(x)) with ht∈B. Decision stumps over R are the threshold functions x↦[θ<x] and their negations x↦[x≤θ]; a 3-piece classifier is b outside [θ1,θ2] and −b inside, with θ1<θ2.
Formalization targets
Goal: Theorem 10.2
If γ>0 and every round t<T has 0<ϵt≤1/2−γ, then the empirical 0–1 risk of AdaBoost's output after T rounds is at most exp(−2γ2T).
Milestones
§10.1. A class of infinite VC-dimension is not γ-weak-learnable for any γ>0 (domain with measurable singletons, measurable hypotheses).
Example 10.1. There is one sample-size function with which every ERM learner over the decision stumps is a 1/12-weak learner for the 3-piece classifiers.
Exercise 10.3. For a nonempty sample and ϵt∈(0,1), the error of ht under D(t+1) is exactly 1/2.
Lemma 10.3. If T≥3 and VCdim(B)=d≥3, then VCdim(L(B,T))≤T(d+1)(3log(T(d+1))+2).
Further item: Exercise 10.4 (1), VCdim(B)≤VCdim(L(B,T)) for T≥1.
Significance
Theorem 10.2 is the reason AdaBoost works and the template for every analysis of boosting: a potential function, here m1∑ie−yift(xi), bounds the 0–1 training error and contracts by the factor 2ϵt(1−ϵt)≤1−4γ2 at every round. Lemma 10.3 supplies the other half of the picture, an estimation-error bound growing only like T⋅VCdim(B) up to logarithms, so that Theorem 6.8 turns the pair into a generalization guarantee for boosting. The remark of §10.1 places weak learning in the statistical landscape of Part I: the VC-dimension characterizes it too, and the gain of boosting is computational.
Nothing here is machine-checked. Two points where the book's text needs care are built into the statements. The weight wt is undefined when ϵt=0, and the algorithm's normalization then divides 0 by 0; in Lean the logarithm of a negative number is 0, so with ϵt=0 the formal algorithm would ignore a perfect weak hypothesis and the bound could fail. The theorems therefore assume ϵt>0, which is the case in which the book's formulas are defined. And the book's derivation of "infinite VC-dimension implies not weakly learnable" from the lower bound of Theorem 6.8 at ϵ=1/2−γ uses that bound outside the range in which Chapter 28 proves it; the statement itself is true, by the km-point form of the No-Free-Lunch argument (Exercise 5.3 of Mission III) and Lemma B.1.
Difficulty
Exercise 10.4 (1) is a one-line embedding of B into L(B,T) with the weights (1,0,…,0) and is the entry point. Exercise 10.3 is the computation of the book: after the update, the weight of the mistakes of ht is ewtϵt and the weight of the correct examples is e−wt(1−ϵt), and with ewt=(1−ϵt)/ϵt these are equal. Theorem 10.2 needs, by induction on the round, the closed form Di(t)=e−yift(xi)/∑je−yjft(xj) of the distribution, the pointwise bound 1[sign(f(x))=y]≤e−yf(x) for the sign convention used, the telescoping product (10.2), the identity Zt+1/Zt=2ϵt(1−ϵt), the monotonicity of a(1−a) on [0,1/2] and 1−a≤e−a. Lemma 10.3 counts dichotomies: Sauer's lemma bounds the restrictions of B to a shattered set by (em/d)d, choosing T of them gives (em/d)dT, the halfspaces of RT contribute (em/T)T by Theorem 9.2, and the inequality 2m≤m(d+1)T is solved with Lemma A.1; the finite-VC lower bound m≤d+1 handles small m, and the numeric slack of the book's chain must be checked. Example 10.1 combines a geometric observation, that one of the three regions of a 3-piece classifier has mass at most 1/3 and a stump agrees with the other two, with the agnostic guarantee for ERM over the stumps from Theorem 6.7, applied with accuracy 1/12; the best stump may only approach error 1/3 because constant functions are not stumps, and the slack absorbs this. The §10.1 remark is the argument sketched above.
Formalization scope
AdaBoost is a function of the sample and of the returned weak hypotheses; the weak learner's randomness and its failure probability (Remark 10.2) are not modelled, and Theorem 10.2 is the deterministic statement the book proves. Rounds are indexed from 0. The output uses sign(0)= negative, consistently with Mission VI. The class L(B,T) is a set of functions, so Lemma 10.3 is a statement about the VC-dimension of Mission IV, with the bound taken in N∪{∞} through the integer part of the real right-hand side and the natural logarithm. Decision stumps are closed under negation, as the book's sign(x−θ)⋅b; constant functions are not stumps. The efficient ERM for decision stumps (§10.1.1), the face-recognition features (§10.4), Exercises 10.1, 10.2, 10.4 (2)–(3) and 10.5 are not stated. The claims of §10.3 that piecewise-constant classifiers with T pieces lie in L(stumps,T) and that this class shatters T+1 points depend on treating sign(x−(−∞)) as a stump and on the sign convention; with real thresholds, L(stumps,2) does not shatter three points under either convention, so these claims are not stated.
Trivializing readings are excluded: the weak-error hypotheses are strict where the book's formulas require it, the VC bounds are in N∪{∞}, and the weak-learner guarantee quantifies over all distributions and all realizable labelings. Welcome contributions: the closed form of D(t), the contraction identity for Zt+1/Zt, and the dichotomy count behind Lemma 10.3.
Selected references
S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 10. doi:10.1017/CBO9781107298019
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. doi:10.1006/jcss.1997.1504
R. E. Schapire, The strength of weak learnability, Machine Learning 5(2), 1990. doi:10.1007/BF00116037
M. Kearns, L. Valiant, Cryptographic limitations on learning Boolean formulae and finite automata, Journal of the ACM 41(1), 1994. doi:10.1145/174644.174647
R. E. Schapire, Y. Freund, Boosting: Foundations and Algorithms, MIT Press, 2012.
Understanding Machine Learning VI: Linear Predictors, the Perceptron and Least SquaresTextbook
Motivation
Part II of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) turns from the theory of learnability to hypothesis classes that can actually be learned by algorithms, and it starts with the family that almost every practical method is built on: linear predictors. Chapter 9 introduces the affine functions Ld and the three classes obtained by composing them with a link: halfspaces for classification, linear regression for real-valued prediction, and logistic regression in between. For each class it gives an ERM algorithm and the guarantee that goes with it. For halfspaces in the separable case the algorithm is Rosenblatt's Perceptron, and the guarantee is the classical mistake bound (Theorem 9.1): the number of updates is at most (RB)2, where R bounds the data and B is the norm of the smallest vector separating it with margin one. The chapter then computes the VC-dimension of halfspaces (Theorems 9.2 and 9.3), which by the fundamental theorem of Mission IV makes them learnable, derives the Least Squares normal equations for regression, and observes that the logistic loss is convex, the property later chapters exploit.
Setting
Vectors live in Rd with its Euclidean inner product and norm. The affine functions are hw,b(x)=⟨w,x⟩+b, homogenous when b=0; a halfspace hypothesis is x↦sign(⟨w,x⟩+b), formalized as a Boolean predictor that is true exactly when ⟨w,x⟩+b>0 (the book leaves sign(0) unspecified; the VC computations do not depend on the convention). A sample (x1,y1),…,(xm,ym) with labels yi∈{±1} is separable if some w has yi⟨w,xi⟩>0 for all i; the constants of Theorem 9.1 are B=inf{∥w∥:∀i,yi⟨w,xi⟩≥1} and R=maxi∥xi∥. The Batch Perceptron starts at w(0)=0 and, while some example has yi⟨w(t),xi⟩≤0, adds yixi; since the algorithm may pick any mistaken example, a run is any sequence of updates obeying this rule, and the theorem is stated for all runs. For regression the loss is (h(x)−y)2 and the Least Squares system is Aw=b with A=∑ixixi⊤, written as the linear map w↦∑i⟨xi,w⟩xi, and b=∑iyixi. The logistic function is φsig(z)=1/(1+e−z) and the logistic loss is log(1+exp(−y⟨w,x⟩)). The learning-theoretic notions (ERM, PAC and agnostic PAC learnability, VC-dimension) are those of Missions I and IV.
Formalization targets
Goal: Theorem 9.1 (Perceptron convergence)
For a separable sample with labels in {±1}, every run of the Batch Perceptron of T iterations satisfies T≤(RB)2, and some run of at most (RB)2 iterations ends with yi⟨w(T),xi⟩>0 for every i.
Milestones
Equation (9.1). A sample is separable if and only if some w satisfies yi⟨w,xi⟩≥1 for all i.
Theorem 9.2. The VC-dimension of the homogenous halfspaces in Rd is d.
Theorem 9.3. The VC-dimension of the halfspaces in Rd is d+1.
Least Squares (9.6). The system Aw=b always has a solution, and w solves it if and only if hw is an ERM hypothesis for the squared loss over the homogenous linear predictors.
Further items: Exercise 9.3, the tightness of Theorem 9.1 (for every m a sample with R≤1, (BR)2≤m and a run of exactly m updates); the learnability of halfspaces by ERM, a consequence of Theorem 9.3 and the fundamental theorem; Exercise 9.2, A is invertible iff the xi span Rd; and the convexity of the logistic loss in w.
Significance
The Perceptron bound is one of the oldest results of learning theory (Novikoff 1962) and the model for every mistake bound in the online-learning chapters: it is independent of the dimension and of the number of examples, depending only on the geometry of the data through R and B. Theorems 9.2 and 9.3 are the first VC-dimension computations of a class used in practice and give, through Theorem 6.8, the sample complexity Θ((d+log(1/δ))/ϵ) of learning halfspaces. The normal equations are the algorithmic content of linear regression, and the convexity of the logistic loss is why logistic regression is tractable in the nonseparable case, where ERM for halfspaces with the 0–1 loss is hard.
Nothing here is machine-checked in this form. Mathlib has the inner-product geometry, the Cauchy–Schwarz inequality, linear algebra of finite-dimensional spaces and convexity of compositions, but neither the Perceptron nor the VC-dimension of halfspaces.
Difficulty
Equation (9.1) is a rescaling and the intended entry point. The convexity of the logistic loss is the composition of the convex function log(1+e−t) with the linear map w↦y⟨w,x⟩. Exercise 9.2 is the identification of the kernel of ∑i⟨xi,⋅⟩xi with the orthogonal complement of the span. The normal equations require showing that a convex quadratic is minimized exactly where its gradient vanishes, and that b lies in the range of A, which is the span of the xi. Theorem 9.1 is the book's proof: by induction on the run, ⟨w∗,w(T)⟩≥T and ∥w(T)∥2≤TR2 for any feasible w∗, then Cauchy–Schwarz, and finally the passage from a feasible w∗ to the infimum B; the existence clause follows because a run can be extended as long as the stopping condition fails and all runs are bounded. Theorem 9.2 is the linear-dependence argument of the book, with a case analysis on the signs of the coefficients and on which side is nonempty, and the shattering of the standard basis; Theorem 9.3 lifts it to Rd+1 by appending a constant coordinate. The learnability of halfspaces is Theorem 6.7 applied to a class that must be shown measurable, nonempty, of finite VC-dimension and pointwise separable; the last needs rational approximations (wn,bn) in which the offset moves below b more slowly than wn approaches w, so that boundary points keep their label.
Formalization scope
Halfspaces are Boolean predictors with sign(0) negative; the classes are sets of functions, so the VC-dimension is that of Mission IV. The Perceptron is a relation on sequences, not a program: this captures the algorithm's freedom to choose any mistaken example and makes the bound apply to all implementations. B is an infimum, which is attained (the feasible set is closed and the norm is coercive), but the theorem does not need attainment. R is a real supremum over the finite index set, equal to 0 for the empty sample, where every run has length 0. The Least Squares statement is about the homogenous class and the sample i↦(xi,yi), with ERM in the sense of Mission I; the bias term is handled by the book's reduction, appending a constant coordinate, and is not formalized separately. The learnability item states qualitative learnability and the ERM guarantee with an unspecified sample-complexity function; the quantitative rate is Theorem 6.8 of Mission IV. Linear programming (§9.1.1), the pseudo-inverse (§9.2.1), polynomial regression (§9.2.2), Exercises 9.1 and 9.4–9.6 are not stated.
Trivializing readings are excluded: labels are constrained to ±1, runs must start at 0 and update only on mistakes, the VC equalities are in N∪{∞}, and the ERM equivalence is a biconditional. Welcome contributions: the two Perceptron invariants as separate lemmas, the shattering of the standard basis, and the pointwise separability of halfspaces.
Selected references
S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 9. doi:10.1017/CBO9781107298019
F. Rosenblatt, The perceptron: a probabilistic model for information storage and organization in the brain, Psychological Review 65(6), 1958. doi:10.1037/h0042519
A. B. J. Novikoff, On convergence proofs on perceptrons, Proceedings of the Symposium on the Mathematical Theory of Automata 12, 1962.
S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6, 1954. doi:10.4153/CJM-1954-037-2
S. Ben-David, H. U. Simon, Efficient learning of linear perceptrons, Advances in Neural Information Processing Systems 13, 2001.
The fundamental theorem of Mission IV says that a class of binary classifiers is PAC learnable exactly when its VC-dimension is finite. That leaves out classes one would like to learn, such as all polynomial classifiers over the line, whose VC-dimension is infinite although each degree separately is learnable. Chapter 7 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) relaxes the definition. In nonuniform learnability (Definition 7.1) the sample size may depend on the hypothesis the learner is competing with: the learner must, for every h∈H, eventually do as well as h up to ϵ, but how soon may depend on h. The chapter's main result (Theorem 7.2) characterizes the nonuniformly learnable classes of binary classifiers as the countable unions of agnostic PAC learnable classes. The learning rule behind it is Structural Risk Minimization (SRM): write H=⋃nHn, weight the pieces, and minimize the empirical risk plus a confidence term that grows with the index (Theorems 7.3–7.5). Applied to a countable class described by a prefix-free code, SRM becomes the Minimum Description Length rule and yields a quantitative form of Occam's razor (Lemma 7.6, Theorem 7.7). The chapter closes the circle with a No-Free-Lunch result for the relaxed notion (Remark 7.2, Exercise 7.5).
Setting
The framework is that of Missions I, II and IV: examples in a domain Z, a hypothesis type with a class H, a loss ℓ, risk LD and empirical risk LS, learners as functions of the sample, the uniform convergence property with an explicit rate mHUC, agnostic PAC learnability, and for binary classification the 0–1 loss, the VC-dimension and pointwise separability. The new module adds Definition 7.1 with an explicit rate mNUL and, as in Definition 3.4, learners whose outputs lie in H; the same notion for a family of learners indexed by the confidence δ, since the SRM and MDL rules take δ as an input; the rate ϵn(m,δ)=inf{ϵ∈(0,1):mHnUC(ϵ,δ)≤m} of Equation (7.1), which is meaningful only when that set is nonempty; the index n(h)=min{n:h∈Hn} of Equation (7.4); the SRM rule as a minimizer of LS(h)+ϵn(h)(m,w(n(h))δ) over the admissible hypotheses, those whose index has positive weight and a defined rate; prefix-free description languages d:H→{0,1}∗ and the MDL rule; and shattering of an infinite set.
Formalization targets
Goal: Theorem 7.2
For a class H of measurable binary classifiers over a domain with measurable singletons, every subclass of which is pointwise separable, H is nonuniformly learnable if and only if there are classes Hn with ⋃nHn=H, each agnostic PAC learnable.
Milestones
Theorem 7.3. If H=⋃nHn is nonempty and each Hn has the uniform convergence property, then H is nonuniformly learnable (general loss).
Theorem 7.4. For weights w(n)∈[0,1] with partial sums at most 1, uniformly convergent pieces Hn with rates mHnUC, δ∈(0,1), any D and any m: with probability at least 1−δ, for every n with w(n)>0 at which ϵn(m,w(n)δ) is defined and every h∈Hn, ∣LD(h)−LS(h)∣≤ϵn(m,w(n)δ).
Theorem 7.5. With w(n)=6/(π2n2) and H0=∅, every family of learners implementing the SRM rule satisfies the nonuniform guarantee with rate mNUL(ϵ,δ,h)=mHn(h)UC(ϵ/2,6δ/(πn(h))2).
Lemma 7.6 (Kraft). For a prefix-free set S of binary strings, every finite subfamily satisfies ∑σ2−∣σ∣≤1.
Theorem 7.7. For a prefix-free description language on a class with a [0,1]-valued loss, m≥1 and δ>0: with probability at least 1−δ, every h∈H satisfies LD(h)≤LS(h)+(∣h∣+ln(2/δ))/(2m).
Further items: nonuniform learnability is implied by agnostic PAC learnability (§7.1); a nonuniformly learnable class of binary classifiers is a countable union of classes of finite VC-dimension (Exercise 7.5 (1)–(2)); a class shattering an infinite set admits no countable cover by classes of finite VC-dimension (Exercise 7.5 (3)) and is not nonuniformly learnable; over an infinite domain the class of all measurable classifiers is not nonuniformly learnable (Remark 7.2).
Significance
Theorem 7.2 is the second characterization theorem of the book's Part I and the one that explains why model selection works: any class that can be stratified into learnable pieces is learnable in the nonuniform sense, with the price of not knowing the index paid in sample size rather than in principle. SRM is the abstract form of every penalized learning rule, and the MDL bound of Theorem 7.7 is the cleanest instance, a bound in which the only property of the hypothesis that matters is the length of its description. Remark 7.2 shows the relaxation is not free: even nonuniformly, no learner handles all classifiers over an infinite domain.
Nothing here is machine-checked. The chapter's arguments are short but they combine everything before them: Hoeffding, the union bound with weights, the VC lower bound of Corollary 6.4 and the fundamental theorem. Three places where the book's statements need care are recorded in the formalization: the rate ϵn is an infimum that may be undefined for small m; the SRM rule takes δ as an input and so is a family of learners; and the fundamental theorem's uniform-convergence direction needs a measurability condition, which appears in Theorem 7.2 as hereditary pointwise separability.
Difficulty
The relaxation remark is a direct comparison of two definitions. Kraft's inequality is the coin-tossing argument of the book or an induction on the maximal length: it is the intended entry point. Theorem 7.4 is Theorem 7.3's engine: for each index and each ϵ in the set of Equation (7.1), the uniform convergence property bounds the failure by w(n)δ; the passage from "every ϵ in the set" to the infimum uses continuity of the outer measure along an increasing union; the union over n uses countable subadditivity and the partial-sum condition. Theorem 7.5 is Theorem 7.4 on the good event together with the two inequalities of the book's proof, using that the target is admissible when m≥mHn(h)UC(ϵ/2,w(n(h))δ) and that admissibility of the SRM output gives the bound for it. Theorem 7.3 asks for a single learner: SRM with a confidence schedule δm→0 chosen so that, for each fixed index, the rate at level δm eventually falls below any ϵ, together with an approximate minimizer within 1/m; the target hypothesis is admissible for m large. Theorem 7.7 is Theorem 7.4 with singleton pieces and the weights 2−∣h∣, a one-sided Hoeffding bound for each h, and Kraft's inequality. Exercise 7.5 (3) is the combinatorial construction of the book's hint, disjoint finite subsets Kn of the shattered set with ∣Kn∣>VCdim(Hn) and a labeling that no Hn realizes. The first half of Theorem 7.2 is Corollary 6.4 applied to the nonuniform learner at fixed ϵ0,δ0, with constants chosen so that the two probability bounds actually contradict; the second half is the fundamental theorem on each piece followed by Theorem 7.3.
Formalization scope
Learners output hypotheses in H, in Definition 7.1 as in Definition 3.4. The rate ϵn is an infimum over the set of Equation (7.1), and every statement that uses it is guarded by the nonemptiness of that set; the weight w(n) may be 0, and H0=∅ encodes the book's indices 1,2,…. The SRM rule minimizes over admissible hypotheses, and an SRM family is one that returns an admissible minimizer whenever some hypothesis is admissible, which is the book's assumption that the argmin is attained (automatic for the 0–1 loss). Theorem 7.4's sum condition is on partial sums, and Kraft's inequality is on finite subfamilies, so no divergent series is silently zero. Theorem 7.7 assumes a [0,1]-valued loss and m≥1. The binary-classification results assume measurable singletons and measurable hypotheses; Theorem 7.2 also assumes every subclass pointwise separable, which every class over a countable domain satisfies. Definition 7.8 (consistency) and the Memorize algorithm of §7.4 are not stated.
Trivializing readings are excluded: outputs in H keep the risk an honest integral, the rate is never a junk infimum of the empty set, and the failure events are bounded in outer measure. Welcome contributions: a reusable weighted union bound over a countable family of uniform-convergence events, the continuity argument for the infimum rate, and the shattered-set combinatorics of Exercise 7.5.
Selected references
S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 7. doi:10.1017/CBO9781107298019
Understanding Machine Learning III: The No-Free-Lunch TheoremTextbook
Motivation
Missions I and II of this series showed that finite hypothesis classes are learnable, with and without the realizability assumption, by empirical risk minimization. Chapter 5 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) asks the converse question: is prior knowledge, in the form of a restricted hypothesis class, really necessary? Could there be a universal learner, an algorithm that, given enough examples from any distribution, outputs a predictor of low risk? The No-Free-Lunch theorem (Theorem 5.1) answers no: for binary classification with the 0–1 loss over a domain X, for every learning algorithm and every training-set size m smaller than ∣X∣/2 there is a distribution on which the learner fails with probability at least 1/7, even though that distribution is perfectly predictable by some function f, so that another learner (ERM over {f}) succeeds. The consequence for the framework is Corollary 5.2: over an infinite domain, the class of all functions is not PAC learnable. This is the first lower bound of the book and the reason the rest of it is about the complexity of hypothesis classes rather than about universal algorithms.
Setting
The framework is the UnderstandingML_Framework module of Mission I, cited as a reference. Binary classification over a domain X uses examples in X×{0,1}, hypotheses h:X→{0,1} and the 0–1 loss, so the risk of h under a distribution D over X×{0,1} is LD(h)=D({(x,y):h(x)=y}), computed as the integral of the 0–1 loss. A learner is a function from samples of each size to hypotheses, and a sample of size m has the law Dm. PAC learnability of a class H (Definition 3.1) requires a sample-complexity function mH and a learner A such that for every ϵ,δ∈(0,1), every distribution D over X and every measurable labeling function f realizable by H, samples of size m≥mH(ϵ,δ) yield L(D,f)(A(S))≤ϵ with probability at least 1−δ.
Two conventions specific to this mission. The domain X is assumed to have measurable singletons (the book's Remark 3.1 assumes away measurability issues); this makes the finitely supported distributions of the proof honest probability measures and makes every LD(h) under them a genuine integral. And "m smaller than ∣X∣/2" is written 2m<∣X∣ in the extended natural numbers, so that an infinite domain satisfies it for every m.
Formalization targets
Goal: Theorem 5.1 (No-Free-Lunch)
Let A be any learning algorithm for binary classification with respect to the 0–1 loss over a domain X with measurable singletons, and let m be a training-set size with 2m<∣X∣. Then there exists a probability distribution D over X×{0,1} such that
there is a measurable f:X→{0,1} with LD(f)=0;
there is a measurable set E of samples of size m with Dm(E)≥1/7 on which LD(A(S))≥1/8.
Milestones
Lemma B.1 (Appendix B). If Z takes values in [0,1] and E[Z]=μ, then for every a∈(0,1), P[Z>1−a]≥(μ−(1−a))/a, and consequently P[Z>a]≥(μ−a)/(1−a)≥μ−a.
Equation (5.2). Under the hypotheses of Theorem 5.1 there are D and a measurable f with LD(f)=0 and ES∼Dm[LD(A(S))]≥1/4.
Corollary 5.2. For an infinite domain X with measurable singletons, the class of all functions X→{0,1} is not PAC learnable.
Two further items: Exercise 5.1, the passage from an expectation of at least 1/4 to a probability of at least 1/7 of exceeding 1/8 for a [0,1]-valued variable; and Exercise 5.3, the k-fold version of Equation (5.2), with bound 1/2−1/(2k) when km≤∣X∣, k≥2 and X is nonempty.
Significance
The No-Free-Lunch theorem is the book's first impossibility result and the conceptual pivot of Part I: it shows that learnability is a property of the pair (hypothesis class, learner) and not of the learner alone, and it motivates the bias–complexity tradeoff of §5.2 and the VC-dimension of Chapter 6, whose lower bound (Theorem 6.7, the "only if" direction of the fundamental theorem) is proved by the same symmetrization argument. Corollary 5.2 is the statement that the class of all functions has infinite sample complexity, the negative half of the characterization of learnable classes.
Nothing here is machine-checked. The proof is combinatorial and elementary but has real content for a formalization: a finite subset C of the domain, the 22m labelings of C, the uniform distribution on C labeled by each of them, an exchange of a maximum, an average and a minimum over labelings and sample sequences, and a pairing argument on labelings that differ at exactly one unseen point. Lemma B.1 is a reverse Markov inequality for bounded variables that later chapters also use.
Difficulty
Lemma B.1 is Markov's inequality applied to 1−Z and is the entry point; Exercise 5.1 is its instance with a=1/8 and μ≥1/4, giving (1/4−1/8)/(7/8)=1/7, together with the inclusion of {θ>1/8} in {θ≥1/8}. Theorem 5.1 follows from Equation (5.2) and Exercise 5.1 once one knows that S↦LD(A(S)) is, under the finitely supported Dm, almost everywhere equal to a measurable function with values in [0,1]; the set E is the intersection of the event with the finite support of Dm, which is measurable because singletons are. Equation (5.2) is the heart of the mission. One picks C⊆X of size 2m (available because 2m<∣X∣), lets Di be uniform on C labeled by the i-th function fi:C→{0,1} extended by 0 off C, and computes ES∼Dim[LDi(A(S))] as an average over the (2m)m sequences of instances, which requires identifying Dim as a finitely supported measure on sequences, that is, the product of finitely supported measures. The inequalities (5.4)–(5.6) exchange max, average and min and restrict to the unseen points, and the pairing argument shows that for each unseen point the average over i of the indicator that A errs on it is exactly 1/2. Exercise 5.3 is the same argument with ∣C∣=km, where at least (k−1)m points are unseen. Corollary 5.2 takes ϵ<1/8, δ<1/7, m=mH(ϵ,δ) and a set C of size 2m in the infinite domain, and derives the contradiction from Theorem 5.1 via the identification of LD for D uniform on C labeled by f with the true error L(DX,f) of Definition 3.1, where DX is uniform on C; the case m=0 is handled separately with a single point.
Formalization scope
The items are stated in the joint-distribution form of the book's Chapter 5, with D over X×{0,1} and LD the risk under the 0–1 loss, rather than in the (D,f) form of Definition 3.1; Corollary 5.2 is the bridge and is stated with the framework's PACLearnable. Witness labeling functions are required to be measurable, because a non-measurable f would make LD(f)=0 true by Lean's convention for non-integrable functions rather than by content. Clause (2) of Theorem 5.1 is stated in the inner form (a measurable set of probability at least 1/7 inside the event) rather than as a lower bound on the outer measure of the event, which for a non-measurable event would be the weaker statement. The size condition uses ENat.card, so infinite domains satisfy it. Learners are deterministic functions of the sample; the book's argument goes through for randomized learners by averaging, but the framework does not model them.
Trivializing readings are excluded: the distribution must be a probability measure, the failing set must be measurable with an honest lower bound, and the witness f must be measurable. Welcome contributions: the finitely supported product law on sequences, the averaging identity (5.3), and the pairing argument on labelings of C.
Selected references
S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 5 and Appendix B. doi:10.1017/CBO9781107298019
D. H. Wolpert, W. G. Macready, No free lunch theorems for optimization, IEEE Transactions on Evolutionary Computation 1(1), 1997. doi:10.1109/4235.585893
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
V. N. Vapnik, Statistical Learning Theory, Wiley, 1998.
Understanding Machine Learning II: Learning via Uniform ConvergenceTextbook
Motivation
Mission I of this series set up the statistical learning framework of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019) and proved, in the book's Chapters 2 and 3, that finite classes are PAC learnable under the realizability assumption. Chapter 4 removes that assumption. Its idea is the one that organizes the rest of the theory: if the empirical risks LS(h) of all hypotheses in H are simultaneously close to their true risks LD(h), then minimizing LS over H is nearly as good as minimizing LD over H, whatever the distribution D is. A sample with that property is called ϵ-representative (Definition 4.1), and a class for which representative samples are guaranteed at some sample size is said to have the uniform convergence property (Definition 4.3). Lemma 4.2 turns representativeness into a guarantee for ERM, Corollary 4.4 turns uniform convergence into agnostic PAC learnability, Hoeffding's inequality (Lemma 4.5) gives uniform convergence for a single hypothesis, and a union bound gives it for a finite class: Corollary 4.6, the capstone, says every finite class with a loss in [0,1] is agnostic PAC learnable by ERM with sample complexity ⌈2log(2∣H∣/δ)/ϵ2⌉.
Setting
The framework is the UnderstandingML_Framework module of Mission I, cited here as a reference. A domain Z is a measurable space, hypotheses form a type with a class H, and a loss ℓ:H×Z→R is given. The risk is LD(h)=Ez∼Dℓ(h,z), the empirical risk on S=(z1,…,zm) is LS(h)=m1∑iℓ(h,zi), and a sample of size m has the product law Dm. A hypothesis is an ERM hypothesis for S if it lies in H and minimizes LS over H; a learner is a function from samples of each size to hypotheses, and an ERM learner returns an ERM hypothesis on every sample.
S is ϵ-representative with respect to H, ℓ and D if ∣LS(h)−LD(h)∣≤ϵ for every h∈H. H has the uniform convergence property with the function mHUC if for every ϵ,δ∈(0,1) and every distribution D over Z, a sample of m≥mHUC(ϵ,δ) i.i.d. examples is ϵ-representative with probability at least 1−δ. H is agnostic PAC learnable with the function mH and the learner A if A returns hypotheses in H and, for every ϵ,δ∈(0,1), every D and every m≥mH(ϵ,δ), LD(A(S))≤minh′∈HLD(h′)+ϵ with probability at least 1−δ over S∼Dm. As in Mission I, "with probability at least 1−δ" is an upper bound δ on the outer measure of the failure event, "minh′∈HLD(h′)+ϵ<LD(h)" is written as "∃h′∈H, LD(h′)+ϵ<LD(h)", and sample-complexity functions are carried explicitly rather than as minimal functions.
Formalization targets
Goal: Corollary 4.6
Let H be a finite hypothesis class, Z a domain and ℓ:H×Z→[0,1] a loss function whose sections ℓ(h,⋅) are measurable. Then
H has the uniform convergence property with the function mHUC(ϵ,δ)=⌈log(2∣H∣/δ)/(2ϵ2)⌉;
every ERM learner for H is an agnostic PAC learner with the function mH(ϵ,δ)=⌈2log(2∣H∣/δ)/ϵ2⌉, which is mHUC(ϵ/2,δ);
if H is nonempty, H is agnostic PAC learnable.
Milestones
Lemma 4.2. If S is ϵ/2-representative and hS is an ERM hypothesis for S, then LD(hS)≤LD(h)+ϵ for every h∈H.
Corollary 4.4. If H has the uniform convergence property with mHUC, then every ERM learner for H is an agnostic PAC learner with the function (ϵ,δ)↦mHUC(ϵ/2,δ), and H is agnostic PAC learnable as soon as an ERM learner exists.
Lemma 4.5 (Hoeffding's inequality). For a probability measure D, a measurable θ with a≤θ≤b almost surely and mean μ=∫θdD, and ϵ>0,
Dm[m1∑i=1mθ(ωi)−μ>ϵ]≤2exp(−2mϵ2/(b−a)2).
Significance
Chapter 4 is where the book's account of learnability becomes distribution-free in the agnostic sense: nothing is assumed about D beyond being a probability distribution, and the guarantee is relative to the best hypothesis in the class. Lemma 4.2 and Corollary 4.4 are the reduction that every later generalization bound in the book (VC dimension, Rademacher complexity, covering numbers, compression) plugs into: prove uniform convergence, get ERM learnability. Corollary 4.6 is the first instance, and its log∣H∣/ϵ2 dependence, against the log∣H∣/ϵ of the realizable case, is the standard illustration of the price of agnosticism. Hoeffding's inequality is stated in the form the book uses everywhere afterward, for the product law of one distribution, with an almost-sure range bound and the mean written as an integral.
Nothing here is machine-checked. Mathlib has no Hoeffding inequality for sums of i.i.d. bounded variables on a product measure in this form, so Lemma 4.5 is a genuine contribution; its proof in the book's Appendix B goes through Hoeffding's lemma on the moment generating function of a bounded centered variable and the Chernoff bounding method, both of which will be needed by the concentration results of later missions.
Difficulty
Lemma 4.2 is three inequalities on real numbers and is the intended entry point. Corollary 4.4 is Lemma 4.2 applied on the complement of the failure event of uniform convergence at ϵ/2: the failure set of the learner is contained in the failure set of representativeness, and outer measure is monotone. Hoeffding's inequality is the substantial item: one needs the moment generating function bound Eeλ(θ−μ)≤eλ2(b−a)2/8 (Lemma B.7 of the book, by convexity of the exponential on [a,b]), independence of the coordinates under Measure.pi to factor the expectation of the product, Markov's inequality, and the optimization over λ; the two tails are treated separately and added. The degenerate cases are genuine: for m=0 the bound is 2 and the claim holds trivially, and for a=b Lean's convention x/0=0 makes the bound 2 again. Corollary 4.6 combines Hoeffding for each h∈H with a union bound over the finite class and an arithmetic step showing that m≥log(2∣H∣/δ)/(2ϵ2) gives 2∣H∣e−2mϵ2≤δ; the empty class makes the uniform convergence clause vacuous. The second and third clauses of the goal then follow from Corollary 4.4, the third by exhibiting an ERM learner, which exists for a nonempty finite class by choosing a minimizer of LS.
Formalization scope
The four items live in the general loss framework, not the binary-classification special case, because the chapter is stated for an arbitrary loss; Mission I's IsRepresentative and HasUniformConvergenceWith already carry the chapter's definitions, so no new definition module is introduced. Losses in Corollary 4.6 are real-valued with the range condition ℓ(h,z)∈[0,1] for every z and measurability of ℓ(h,⋅) for h∈H, which is what the book's "ℓ:H×Z→[0,1]" and Remark 3.1 give. The book's "mH(ϵ,δ)≤⋯" is stated as "the guarantee holds with the function ⌈⋯⌉", the same convention as Mission I. In Corollary 4.4 the ERM clause is universal over ERM learners, matching "the ERM paradigm is a successful agnostic PAC learner" for every choice of minimizer; the existence of an ERM learner is a separate hypothesis for the learnability clause because a class with no minimizers on some sample has no ERM rule. Hoeffding's inequality is on i.i.d. coordinates of Measure.pi; the book's "E[θi]=μ" is the definition of μ rather than an assumption.
Trivializing readings are excluded: the failure events are bounded in outer measure, so measurability of the events is not a loophole; representativeness is required for every h∈H; the sample-complexity functions are the book's, with ceilings. Welcome contributions: Hoeffding's lemma on bounded centered variables, the factorization of the moment generating function under Measure.pi, and a reusable union bound over a finite class.
Selected references
S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 4 and Appendix B. doi:10.1017/CBO9781107298019
W. Hoeffding, Probability inequalities for sums of bounded random variables, Journal of the American Statistical Association 58(301), 1963. doi:10.1080/01621459.1963.10500830
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
S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013, Chapter 2. doi:10.1093/acprof:oso/9780199535255.001.0001
Understanding Machine Learning I: The Statistical Learning Framework, ERM and Finite ClassesTextbook
Motivation
Chapters 2 and 3 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (Cambridge University Press, 2014, doi:10.1017/CBO9781107298019), set up the framework in which the whole book asks what learning is. A learner sees a sample drawn independently from an unknown distribution over examples, chooses a hypothesis from a class fixed in advance, and is judged by its risk, the expected loss on a fresh example. The natural rule is Empirical Risk Minimization: pick a hypothesis that does best on the sample. Chapter 2 shows that ERM over an unrestricted class overfits, that restricting the class is what makes learning possible, and that a finite class never overfits once the sample is larger than log(∣H∣/δ)/ϵ (Corollary 2.3). Chapter 3 turns this into a definition, Probably Approximately Correct learnability with its sample-complexity function mH(ϵ,δ), restates the finite-class result as Corollary 3.2, and then generalizes in two directions that the rest of the book lives in: the agnostic model, in which no hypothesis need be perfect and the learner competes with the best hypothesis in the class, and general loss functions, which cover regression, multiclass prediction and unsupervised tasks. Chapter 4 adds the notion of an ε-representative sample and of uniform convergence, the tool by which the finite-class result extends to the agnostic case; its definitions are included here since they complete the framework.
Setting
A domain Z of examples, a class H of hypotheses and a loss ℓ:H×Z→R. The risk of h under a distribution D is LD(h)=Ez∼Dℓ(h,z) and its empirical risk on S=(z1,…,zm) is LS(h)=m1∑iℓ(h,zi); a sample is drawn i.i.d., S∼Dm; an ERM hypothesis minimizes LS over H; a learning algorithm maps samples of each size to hypotheses. In binary classification the examples are (x,f(x)) with x∼D over X and f a labeling function, and the true error is L(D,f)(h)=D({x:h(x)=f(x)}); the realizability assumption says some h⋆∈H has L(D,f)(h⋆)=0. H is PAC learnable if some sample-complexity function mH and algorithm guarantee, for all ϵ,δ∈(0,1), all D and all realizable f, true error at most ϵ with probability at least 1−δ from m≥mH(ϵ,δ) examples; agnostic PAC learnability with respect to a loss asks instead for LD(h)≤minh′∈HLD(h′)+ϵ for every distribution over Z.
Formalization targets
Goal: Corollary 3.2
Every finite hypothesis class is PAC learnable with sample complexity
mH(ϵ,δ)≤⌈ϵlog(∣H∣/δ)⌉,
by the ERM rule: for a nonempty finite class of measurable hypotheses there is an ERM learner satisfying the PAC guarantee with that sample-complexity function.
Milestone
Corollary 2.3: under realizability, with m≥log(∣H∣/δ)/ϵ examples, every ERM hypothesis has true error at most ϵ with probability at least 1−δ.
Significance
Corollaries 2.3 and 3.2 are the first learning theorem of the book and the template for all later sample-complexity bounds: a bad hypothesis is consistent with an i.i.d. sample with probability at most (1−ϵ)m≤e−ϵm, and a union bound over the class turns this into a guarantee that holds uniformly over all distributions and all realizable labelings. Everything that follows, uniform convergence for finite classes, the fundamental theorem for classes of finite VC dimension, structural risk minimization, replaces the count ∣H∣ by a finer measure of the class's complexity but keeps the argument. None of this is machine-checked. The mission fixes on the platform the objects that the rest of the series uses without change: risks, empirical risks, the product law of a sample, the ERM relation, and the four learnability notions of Definitions 3.1, 3.4, 4.1 and 4.3.
Difficulty
The milestone needs that, for a fixed measurable hypothesis whose true error exceeds ϵ, the product law gives the event "zero empirical risk" probability at most (1−ϵ)m; this is the product structure of Measure.pi on the event that each labeled example lies in the measurable set where the hypothesis agrees with f, followed by 1−ϵ≤e−ϵ, the union bound over the finite class and the observation that under realizability every ERM hypothesis has zero empirical risk, so a bad ERM hypothesis is a consistent bad hypothesis. The goal packages this as a learner: existence of an ERM hypothesis for every sample (a finite nonempty class has a minimizer), and the arithmetic of the ceiling.
Formalization scope
The framework is the book's, with the risk as a Bochner integral, the sample law as a product measure, ERM as a relation and learners as deterministic functions of the sample; failure probabilities are stated as upper bounds on the outer measure of the failure set, the strong form of "with probability at least 1−δ"; the comparison with minh′∈HLD(h′) is written without an infimum. Sample-complexity functions are carried explicitly: the book's mH as the minimal such function is not defined, and "mH≤f" is stated as "the learner satisfies the guarantee with the function f". Hypotheses and labeling functions are assumed measurable (Remark 3.1). The union bound (Lemma 2.2) is Mathlib's measure_union_le and is not an item. Hypotheses: ϵ>0, δ∈(0,1), H finite (and nonempty for the learner to exist).
Trivializing readings are excluded: the milestone's failure event ranges over every ERM hypothesis, and the goal quantifies over all distributions, all realizable labelings and all ϵ,δ. Welcome contributions: the product-law bound for a fixed hypothesis and the union bound over a finset, which every later mission of the series reuses.
Selected references
S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapters 2–4. doi:10.1017/CBO9781107298019
L. G. Valiant, A theory of the learnable, Communications of the ACM 27(11), 1984. doi:10.1145/1968.1972
D. Haussler, Decision theoretic generalizations of the PAC model for neural net and other learning applications, Information and Computation 100(1), 1992. doi:10.1016/0890-5401(92)90010-D
An Introduction to Computational Learning Theory II: Occam's Razor, Set Cover and Decision ListsTextbook
Motivation
Chapter 2 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), gives a formal justification of Occam's Razor inside the PAC model. An Occam algorithm is judged not by the predictive power of its hypothesis but by how succinctly the hypothesis explains the sample before it: it must be consistent with the data and short, in the sense that its representation has fewer bits than the data it reproduces. The chapter's theorems say that, when the examples are drawn independently from a fixed distribution, such compression automatically yields prediction: a consistent hypothesis drawn from a small class is, with high probability, accurate on unseen examples. This turns the design of PAC learning algorithms into a combinatorial task, finding a short consistent hypothesis, and the chapter demonstrates the method three times: it shaves a logarithmic factor off the conjunction bound of Chapter 1, it learns conjunctions with few relevant variables through the greedy set-cover heuristic, and it learns Rivest's decision lists, a class strictly more expressive than k-CNF and k-DNF, by a greedy algorithm whose correctness is a one-line consequence of consistency.
Setting
The framework is that of Mission I: a measurable instance space, concepts as boolean functions, a target distribution D, the product law of a sample of m labeled examples, the error error(h)=Prx∼D[h(x)=c(x)], and consistency of a hypothesis with a sample. Hypotheses may be represented by binary strings through a representation map, with size the bit length; an (α,β)-Occam algorithm outputs a consistent hypothesis of size at most (n⋅size(c))αmβ with 0≤β<1. The set cover problem asks for a minimum subcollection of a collection S of subsets of a finite universe U that covers U; the greedy heuristic repeatedly picks the set covering the most uncovered elements. A k-decision list is a sequence of conditions, each a conjunction of at most k literals, with a bit attached to each and a default bit; it evaluates to the bit of the first satisfied condition. The greedy decision-list algorithm repeatedly finds a useful condition, one satisfied by some remaining examples all of which carry the same label, appends it with that label and removes those examples.
For a finite hypothesis class H, a target c, a distribution D and 0<ϵ≤1, the probability that a sample of m examples is consistent with some h∈H of error greater than ϵ is at most ∣H∣(1−ϵ)m; hence
m≥ϵ1(ln∣H∣+lnδ1)
makes this probability at most δ, and any algorithm that outputs a consistent hypothesis from H has error greater than ϵ with probability at most ∣H∣(1−ϵ)m.
Milestones
Theorem 2.1 (an (α,β)-Occam algorithm is a PAC algorithm, with explicit sample-size conditions in place of the constant a); the greedy set-cover bound of §2.3 (∣Ui∣≤(1−1/opt)i∣U∣ and optln∣U∣ sets cover); the improved conjunction bound of §2.2; Theorem 2.3 (k-decision lists are PAC learnable by the greedy algorithm, which never fails and whose outputs are consistent).
Significance
Theorem 2.2 is the single most used tool of the subject: every finite-class sample bound, including the ones for conjunctions, decision lists, k-CNF and the discretized geometric classes, is an instance of it, and the Vapnik–Chervonenkis theory of Chapter 3 is its extension to infinite classes with the growth function in place of ∣H∣. Theorem 2.1 is the philosophical statement, that succinct explanation implies prediction, and its converse (Exercise 2.3, and more strongly the boosting theorem of Chapter 4) makes Occam learning equivalent to PAC learning. The greedy set-cover bound is Chvátal's classical approximation guarantee, used in the book for learning with few relevant variables and again in later chapters. Theorem 2.3 is Rivest's result, and its proof exhibits the pattern "consistency by construction plus a counting bound" in its purest form. None of these is machine-checked. Their formalization gives the platform the union-bound-over-a-finite-class argument once and for all, in a form that the later missions of this series reuse verbatim.
Difficulty
Theorem 2.2 requires that, for a fixed measurable hypothesis with error greater than ϵ, the product law gives the event "consistent with all m examples" probability at most (1−ϵ)m, which is the product structure of Measure.pi applied to the event that each coordinate lies in the set where h agrees with c; the union bound over H and the elementary inequality (1−ϵ)m≤e−ϵm finish. Theorem 2.1 adds only the count of binary strings of length at most K and arithmetic with real exponents. The set-cover bound is a discrete induction: an optimal cover of U restricted to the uncovered elements has at most opt sets, so one of them, hence the greedy choice, covers a 1/opt fraction; the covering clause needs the strict inequality 1−1/opt<e−1/opt. Theorem 2.3 needs that a run of the greedy algorithm never repeats a condition (its satisfied examples are removed), so outputs lie in an explicit finite class, that the first condition of the target list satisfied by a remaining example is useful, and that a complete run is consistent; the bound is then Theorem 2.2.
Formalization scope
Everything is in the sample-complexity sense on the Mission I framework; running time is not modelled and "efficient" is dropped from every statement, which is recorded in the natural-language statements. Theorem 2.2's constant b is 1 with natural logarithms; Theorem 2.1's constant a is replaced by three explicit sufficient conditions. Hypotheses in the finite class are required to be measurable. The greedy heuristic and the greedy decision-list algorithm are relations (any tie-breaking), and the theorems quantify over every run; the decision-list theorem is stated for every k with the k-conjunctions as conditions, so that its hypothesis is a k-decision list rather than the expansion the book sketches for k>1. The conjunction count is 3n+1, including the empty concept that the elimination algorithm outputs on a sample without positive examples. The few-relevant-variables algorithm of §2.3 is not stated (its bound has an unspecified constant and m on both sides). Hypotheses: 0<ϵ≤1, 0<δ (and δ<1 where ln(1/δ) must be nonnegative).
Trivializing readings are excluded: the bad-consistent event is over all of H, the decision-list failure event ranges over every possible output, and the set-cover bound holds for every greedy run. Welcome contributions: the product-law bound for a fixed hypothesis, the union bound over a finset, the string-counting lemma, and the no-repetition lemma for greedy runs.
Selected references
M. J. Kearns, U. V. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994, Chapter 2. doi:10.7551/mitpress/3897.001.0001
A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Occam's razor, Information Processing Letters 24(6), 1987. doi:10.1016/0020-0190(87)90114-1
V. Chvátal, A greedy heuristic for the set-covering problem, Mathematics of Operations Research 4(3), 1979. doi:10.1287/moor.4.3.233
R. L. Rivest, Learning decision lists, Machine Learning 2(3), 1987. doi:10.1007/BF00058680
D. Haussler, Quantifying inductive bias: AI learning algorithms and Valiant's learning framework, Artificial Intelligence 36(2), 1988. doi:10.1016/0004-3702(88)90002-1
An Introduction to Computational Learning Theory I: The PAC Model, Conjunctions, Rectangles and 3-CNFTextbook
Motivation
Chapter 1 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), introduces Valiant's Probably Approximately Correct model, the framework for the whole book. A learner sees labeled examples of an unknown target concept drawn from an unknown but fixed distribution, and must output a hypothesis that, with probability at least 1−δ over the sample, misclassifies a fresh example with probability at most ϵ; the model is distribution-free, and the hypothesis is judged on the same distribution it was trained on. The chapter's three positive results are the templates for everything that follows. The rectangle game (Theorem 1.1) shows that an infinite class can be learned from a finite sample by exploiting the geometry of the error region. Conjunctions (Theorem 1.2) are learned by the elimination algorithm, whose analysis, a union bound over "bad" literals, is the prototype of every sample-size bound in the book. And 3-CNF formulae (Theorem 1.4) are learned by a change of variables that reduces them to conjunctions, which, set against the intractability of learning 3-term DNF as 3-term DNF (Theorem 1.3), is the reason the final definition of the model lets the hypothesis class differ from the concept class.
Setting
The instance space is a measurable space X, a concept is a function c:X→{0,1}, and the target distribution D is a probability measure on X. The error of a hypothesis h is error(h)=Prx∼D[h(x)=c(x)]. A sample of m examples is S=((x1,c(x1)),…,(xm,c(xm))) with the xi independent draws from D; a learning algorithm is a function from samples to hypotheses; it has the (ϵ,δ) guarantee on a class C if for every c∈C and every D the probability that its hypothesis has error greater than ϵ is at most δ; C is PAC learnable using H if for all ϵ,δ∈(0,1/2) some sample size and algorithm with hypotheses in H achieve the guarantee. For X={0,1}n a literal is a variable or its negation and a conjunction is a finite set of literals; the elimination algorithm starts from all 2n literals and deletes every literal contradicted by a positive example. For X=R2 the concepts are the closed axis-aligned rectangles and the tightest-fit algorithm returns the smallest rectangle containing the positive examples. A 3-CNF formula is a conjunction of clauses of at most three literals; the expansion a↦a′ records for each triple (u,v,w) of literals the value u∨v∨w.
Formalization targets
Goal: Theorem 1.2
Conjunctions of boolean literals are PAC learnable by the elimination algorithm: for every target conjunction, every distribution on {0,1}n and ϵ,δ>0, the elimination hypothesis is consistent with every sample labeled by the target, and with
m≥ϵ2n(ln2n+lnδ1)
examples its error exceeds ϵ with probability at most δ; hence conjunctions are PAC learnable using conjunctions.
Milestones
Theorem 1.1 (rectangles by the tightest fit, m≥(4/ϵ)ln(4/δ)) and Theorem 1.4 (3-CNF formulae by elimination over the (2n)3 expanded variables, the hypothesis being itself a 3-CNF formula).
Significance
Theorem 1.2 is Valiant's original result and the first instance of the two ideas that organize the subject: a hypothesis that is more specific than the target never errs on negative examples, and the error of the hypothesis decomposes as a sum over a polynomial number of "bad" events, each of which is avoided with probability exponentially close to one. Theorem 1.1 is the first learning result for an infinite concept class and the seed of the Vapnik–Chervonenkis theory of Chapter 3. Theorem 1.4 is the first reduction between learning problems and, together with Theorem 1.3, the demonstration that the choice of hypothesis representation can separate tractable from intractable. None of these theorems is machine-checked. Formalizing them fixes, for the rest of the series, the framework in which the error of a hypothesis, the law of a sample and the learnability of a class are stated, so that the Occam, VC-dimension, boosting and noise results of later chapters can be stated on the same objects.
Difficulty
The elimination analysis needs that the hypothesis contains every literal of the target, that its error is at most the sum over its literals z of p(z)=Pr[c(a)=1∧z=0 in a], and that a literal with p(z)≥ϵ/2n survives m independent examples with probability at most (1−ϵ/2n)m; the probabilistic content is the independence of the coordinates of the sample law, which is a product measure, and the inequality 1−x≤e−x. The rectangle analysis is the four-strip argument, which for an arbitrary distribution, possibly with atoms, requires choosing the strip {y≥t∗} with t∗ the supremum of the heights at which the strip has weight at least ϵ/4 and using the left-continuity of the weight in the height. The 3-CNF result transports the conjunction bound along the injective expansion: the pushforward of the sample law is the sample law of the expanded distribution, and the error of the composed hypothesis equals the error over the expanded variables. The deduction of PACLearnable from the explicit bounds is a choice of sample size.
Formalization scope
The model is stated in the sample-complexity sense: algorithms are functions of the sample, and the guarantee bounds the outer measure of the failure set under the product law of the sample, which is the strong form of "with probability at least 1−δ" and requires no measurability of the failure set. Running time, and hence "efficiently", is not modelled, and the hardness Theorem 1.3 is not stated; each theorem carries instead the explicit algorithm and the explicit sample bound of the book's analysis. Concepts on general instance spaces are required to be measurable in the guarantee. The cube is {0,1}n as functions Fin n → Bool; the expanded variables are indexed by the triples of literals, so N=(2n)3 is a Fintype.card. Rectangles are closed, possibly empty; the tightest fit of a sample without positive examples is the empty concept. Hypotheses: ϵ>0, 0<δ<1; the sample bounds are as printed, with natural logarithms.
Trivializing readings are excluded: the failure bound is uniform over all distributions and all targets in the class, consistency is asserted for every sample labeled by the target, and the learnability clause quantifies over all ϵ,δ. Welcome contributions: the product-law bound Pr[a fixed event of probability≥p is missed by all m examples]≤(1−p)m, the union bound over literals, and the pushforward identity for the expanded sample.
Selected references
M. J. Kearns, U. V. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994, Chapter 1. doi:10.7551/mitpress/3897.001.0001
L. G. Valiant, A theory of the learnable, Communications of the ACM 27(11), 1984. doi:10.1145/1968.1972
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
L. Pitt, L. G. Valiant, Computational limitations on learning from examples, Journal of the ACM 35(4), 1988. doi:10.1145/48014.63140
Wasserstein Distributionally Robust Optimization V: The Wasserstein Shrinkage Estimator and Robust MMSE EstimationTextbook
Motivation
Minimum mean square error (MMSE) estimation — predicting a signal x from a noisy observation
y by minimizing expected squared prediction error — underlies linear systems theory, linear
regression, Kalman filtering, and multiple-input multiple-output signal processing. Its classical
solution assumes the joint distribution of (x,y) is known exactly; in practice it is estimated
from data, and the estimator inherits sampling error and model risk. Kuhn, Mohajerin Esfahani,
Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter shows that hedging the MMSE
objective against every distribution in a Wasserstein ball around the empirical distribution
— an infinite-dimensional worst case over an intractable set of measures, a priori — collapses
to a tractable, finite-dimensional convex semidefinite program (Theorem 25, p. 29), building on
the Gelbrich-hull machinery of Section 2.3. This mission formalizes that reduction.
Setting
Fix mx,my∈N and let ξ=(x,y)∈Rmx×Rmy
be a random vector: x the signal to be estimated, y the observation. An estimator is a
measurable function ψ:Rmy→Rmx; write Ψ for the family of
all estimators. The distribution of ξ is only known to lie in a type-2 Wasserstein ball
Bε,2(P^N) centered at an elliptical nominal distribution P^N=Eg(μ^,Σ^) with nominal mean μ^∈Rm (m=mx+my), nominal
covariance Σ^∈S+m, and density generator g. The distributionally robust MMSE
estimation problem is
ψ∈ΨinfQ∈Bε,2(P^N)supEQ[∥x−ψ(y)∥22].(35)
Writing Σ^=(Σ^xxΣ^yxΣ^xyΣ^yy) blockwise, the nonlinear convex SDP
is the finite-dimensional relaxation the chapter builds toward.
Formalization targets
Goal (Theorem 25, distributionally robust MMSE estimator). If Σ^≻0, then the
optimal value of problem (35) equals the optimal value of SDP (36). Moreover, if S⋆ is
optimal in (36) with Syy⋆ invertible, then the affine function
ψ⋆(y)=Sxy⋆(Syy⋆)−1(y−μ^y)+μ^x
attains the outer infimum of (35) — it is a distributionally robust MMSE estimator, exhibited in
closed form from an SDP optimizer.
Significance
Theorem 25 reduces an a priori infinite-dimensional, worst-case functional optimization problem
(an infimum over all measurable estimators of a supremum over all distributions within a
Wasserstein ball) to a finite convex program with one linear matrix inequality, one Loewner-order
lower bound, and one trace/matrix-square-root constraint — solvable in polynomial time, with the
optimal estimator recovered in closed form from the SDP's optimal block matrix. It shows that
robustifying MMSE estimation against distributional ambiguity does not sacrifice tractability:
the resulting estimator remains affine, the same functional form as the classical (non-robust)
best linear unbiased estimator, only with its coefficients drawn from a regularized covariance
estimate rather than the raw sample covariance. Formalizing it fixes, machine-checkably, the exact
shape of that regularization — which SDP constraints are load-bearing (the Loewner lower bound in
particular rules out a numerically unstable near-singular Syy) and which conditions
(Σ^≻0, Syy⋆ invertible) the closed-form estimator formula actually needs.
Difficulty
The paper's own remark (p. 29) names the two nontrivial steps: first, "establishing a minimax
theorem for (35) and exploiting the properties of elliptical distributions" to show the outer
infimum is attained by an affine estimator — a priori (35) ranges over all measurable ψ,
and there is no obvious reason the worst case forces linearity. Second, "combining this structural
insight with Theorem 16" (the SDP-representability result for indefinite quadratic losses under
an elliptical nominal distribution, itself a nontrivial closed-form reduction of an
infinite-dimensional worst-case risk) to convert the now-restricted problem over affine estimators
into the finite SDP (36). Neither step is a routine consequence of the ambiguity-set definitions
alone; each requires structural facts about elliptical distributions and quadratic losses proved
earlier in the chapter.
Formalization scope
The signal-observation space is EuclideanSpace ℝ (Fin mx ⊕ Fin my), with x and y recovered
as the two summand projections; the block matrix S is Matrix (Fin mx ⊕ Fin my) (Fin mx ⊕ Fin my) ℝ, and Matrix.toBlocks₁₁/toBlocks₁₂/toBlocks₂₁/toBlocks₂₂ give its four blocks. The
constraint "Sxy=Syx⊤" is not stated as a separate hypothesis: it follows
automatically once S is symmetric (implied by S.PosSemidef), so encoding the feasible set from
a single symmetric S rather than four independently-quantified blocks makes it structurally
impossible to drop — see pitfall 4 of BRIEF.md. The outer infimum of problem (35) ranges only
over measurableψ (Measurable ψ on the binder), matching the paper's own definition of
Ψ as "the family of all possible measurable estimators" (p. 29) exactly. λ_min(Σ̂) is taken
as a hypothesis parameter
characterized by the two properties that make it the minimum ("≤ every eigenvalue of Σ̂, and
attained by some eigenvalue"), rather than invoking a specific Mathlib min-eigenvalue API by name.
S_{yy}⁻¹ uses the ordinary matrix inverse (junk zero matrix when singular), matching the paper's
literal notation; S^\star_{yy} invertible is stated as an added hypothesis, not present
verbatim on the page, because the paper leaves the formula's well-definedness implicit — disclosed
per pitfall 5 rather than silently assumed away. The paper's own "which is always solvable"
clause is not asserted: Theorem 25 states, as part of itself, that SDP (36) attains its maximum
(an unconditional existence claim for an optimal S⋆); this formalization states only the
conditional consequences of such an S⋆ existing, not that one does — proving or asserting
solvability is out of this mission's scope, so the Lean statement is strictly weaker than Theorem
25's own conclusion on this point, disclosed rather than silently dropped. All risk-style suprema
are EReal-valued and
Integrable-guarded, matching the series' convention. No milestone theorem is included: the
paper's own proof sketch derives (33)'s and by extension (36)'s SDP "via Theorem 16", but Theorem
16 (indefinite quadratic loss and p=2, eq. 23) was itself judged too heavy to state faithfully
in 02-gelbrich's time budget and is not redefined here either — see STATUS.md. Theorem 24 (the
Wasserstein shrinkage estimator, this chapter's originally recommended goal) is out of scope: its
closed-form eigenvalue transformation (eq. 34a/34b) requires transcribing nested square roots from
a rendered PDF page that this session's time budget did not allow verifying to the standard the
brief demands (pitfall 1); the brief's own documented fallback to Theorem 25 was taken instead.
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
Nguyen, V. A., Shafieezadeh-Abadeh, S., Yue, M.-C., Kuhn, D., & Wiesemann, W. (2021).
Optimistic distributionally robust optimization for nonparametric likelihood approximation.
Advances in Neural Information Processing Systems, 32.
Shafieezadeh-Abadeh, S., Nguyen, V. A., Kuhn, D., & Mohajerin Esfahani, P. (2018). Wasserstein
distributionally robust Kalman filtering. Advances in Neural Information Processing Systems,
31.
Wasserstein Distributionally Robust Optimization II: The Gelbrich Ambiguity Set and Elliptical TractabilityTextbook
Motivation
Distributionally robust optimization (DRO) hedges a decision against every distribution within
some ambiguity set around an estimated (nominal) distribution, rather than trusting the
estimate exactly. When the ambiguity set is a ball of radius ε around the empirical
distribution P^N in the type-p Wasserstein metric, the resulting worst-case risk problem
inherits attractive statistical guarantees (Mohajerin Esfahani & Kuhn 2018) but is, in general, an
optimization problem over an infinite-dimensional space of measures. Kuhn, Mohajerin Esfahani,
Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter surveys when this problem becomes
computationally tractable. One route — the subject of this mission — discards everything about
the nominal distribution except its mean vector and covariance matrix and replaces the Wasserstein
ball with a set built only from these two moments, the Gelbrich hull. The construction is due
to Gelbrich (1990), who first bounded the Wasserstein distance between two distributions using
only their means and covariances.
Setting
Fix Ξ⊆Rm, a nominal distribution P^N∈P(Ξ), a radius
ε>0 and an exponent p≥1. The type-p Wasserstein distance between two
probability measures Q,Q′ on Rm is
Wp(Q,Q′)=(π∈Π(Q,Q′)inf∫∥ξ−ξ′∥pdπ(ξ,ξ′))1/p,
the infimum over couplings π (probability measures on Rm×Rm with
marginals Q and Q′) of the p-th root of the expected p-th power of Euclidean distance. The
Wasserstein ambiguity set is Bε,p(P^N)={Q∈P(Ξ):Wp(Q,P^N)≤ε}, and the worst-case risk of a loss function ℓ is
Rε,p(P^N,ℓ)=supQ∈Bε,p(P^N)EQ[ℓ(ξ)].
Suppose P^N has mean vector μ^ and covariance matrix Σ^∈S+m (the
positive semidefinite m×m matrices). The mean-covariance uncertainty set is
where Σ1/2 is the positive-semidefinite square root. The Gelbrich hull is
Gε(μ^,Σ^)={Q∈P(Ξ):(EQ[ξ],CovQ[ξ])∈Uε(μ^,Σ^)}: the distributions on Ξ whose own mean and covariance lie
in Uε(μ^,Σ^). An elliptical distributionEg(μ,Σ) has density
f(ξ)=C⋅det(Σ)−1g((ξ−μ)⊤Σ−1(ξ−μ)) for a density
generator g and normalizing constant C; two elliptical distributions "have the same density
generator" when their g coincide (e.g. both Gaussian, both Student-tν for the same ν).
Formalization targets
Goal (Theorem 13, Gelbrich hull). For every p≥2,
Bε,p(P^N)⊆Gε(μ^,Σ^).
This is an outer approximation: every distribution within ε of P^N in
Wasserstein distance has a mean and covariance inside Uε(μ^,Σ^), so
optimizing over the Gelbrich hull instead of the Wasserstein ball can only enlarge the feasible
set, never shrink it below the truth.
Supporting results. Theorem 4 (Gelbrich bound) gives the moment-only lower bound on W2 that
Theorem 13 is built from, with equality for elliptical distributions sharing a generator.
Proposition 1 sharpens the goal's containment to an equality on the mean-covariance projection
itself, under the same two conditions (Ξ=Rm, P^N elliptical). Corollary 1
propagates the goal's set containment to the risk level: Rε,p(P^N,ℓ)≤Rε(μ^,Σ^,ℓ) for every ℓ, where Rε(μ^,Σ^,ℓ)=supQ∈Gε(μ^,Σ^)EQ[ℓ(ξ)] is the Gelbrich risk.
Significance
Theorem 13 is the hinge between an intractable infinite-dimensional worst-case-risk problem and a
tractable one: the paper goes on (Theorem 16, outside this mission's scope) to show that for
quadratic loss functions and elliptical nominal distributions the Gelbrich risk itself equals the
optimal value of a semidefinite program with two linear matrix inequality constraints — and that,
under those same conditions, the Wasserstein worst-case risk, the Gelbrich risk and the SDP value
all coincide. Corollary 1 is what makes the Gelbrich risk usable as a conservative surrogate even
outside that special case: it upper-bounds the true worst-case risk for any loss function and
anyp≥2, at the cost of discarding all but first- and second-order information about the
nominal distribution. Formalizing the goal and Corollary 1 gives the exact scope in which this
moment-relaxation is licensed — the p≥2 restriction and the outer-approximation direction are
both easy to get backwards, and this mission's Lean encoding fixes both irreversibly.
Difficulty
The obvious first argument is to prove containment pointwise: fix Q∈Bε,p(P^N) and show its mean and covariance land in Uε(μ^,Σ^). That reduces
Theorem 13 to Proposition 1's containment half, which in turn reduces to the Gelbrich bound
(Theorem 4) applied to the pair (Q,P^N) — the inequality direction of Theorem 4 suffices
for containment; only the sharper equality direction (needed for Proposition 1's own equality
clause) requires the elliptical hypothesis. The non-obvious step is Theorem 4 itself: bounding
W2(Q,Q′) below by a closed-form expression in the two distributions' first two moments only,
for arbitraryQ,Q′ with those moments, requires an argument that survives every coupling
π — the paper's proof goes through a lower bound on the coupling's cross-covariance term via
the eigenvalues of Σ1/2Σ′Σ1/2, not a direct manipulation of W2's
definition.
Formalization scope
Rm is EuclideanSpace ℝ (Fin m); a "distribution" is a MeasureTheory.Measure on it
constrained by Q Set.univ = 1 (probability) and Q Ξᶜ = 0 (support in Ξ). The Wasserstein
distance is ENNReal-valued (Definition 1's infimum over couplings, matching 01-duality's
convention); the worst-case and Gelbrich risks are EReal-valued suprema restricted to loss
functions integrable under the candidate distribution, avoiding Mathlib's junk value for a
non-integrable Bochner integral. Σ1/2 is the positive-semidefinite matrix square root,
picked by choice from its defining existential and applied in this mission only to matrices
hypothesized (or, per Section 2.3's standing assumption, given) positive semidefinite. Elliptical
distributions (IsElliptical) are represented by the paper's own density formula (a measure
equal to volume.withDensity of C·det(Σ)⁻¹·g((ξ-μ)ᵀΣ⁻¹(ξ-μ)) for some C>0), together with
the mean/covariance facts every theorem in this chunk reads off directly; an earlier draft kept
only the latter, under which "same density generator" held vacuously for any moment-matched
pair — corrected after moderation flagged it (see STATUS.md).
Because 01-duality (Wasserstein distance, ambiguity set, worst-case risk) is not yet a published
mission, this chunk redefines those objects locally in its own namespace rather than importing an
unpublished draft, per the series' definition-reuse policy; a future upload can retire the
duplication once 01-duality is live. A formalization that dropped Theorem 4's "same density
generator" condition from its equality clause, or that stated the goal's containment for all p≥1 rather than p≥2, would be trivializing or simply false — both are explicit hypotheses in
the Lean statements. Matrix.PosSemidef and its Loewner order carry the S+m constraints; no
elliptical-distribution or Gelbrich-hull infrastructure exists elsewhere on the platform, so this
mission's definitions are original contributions reusable by any later extension (Theorem 16/17,
Lemma 1/2's SDP representations) of this series.
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
Gelbrich, M. (1990). On a formula for the L2 Wasserstein metric between measures on Euclidean
and Hilbert spaces. Mathematische Nachrichten, 147(1), 185–203.
Mohajerin Esfahani, P., & Kuhn, D. (2018). Data-driven distributionally robust optimization
using the Wasserstein metric: performance guarantees and tractable reformulations.
Mathematical Programming, 171(1), 115–166.
Foundations of Machine Learning XIII: The Johnson-Lindenstrauss LemmaTextbook
Motivation
High-dimensional data is often computationally expensive to work with and hard to visualize.
The Johnson-Lindenstrauss lemma answers a striking question in this setting: can any finite
set of points, no matter how high-dimensional the ambient space, be squeezed into a space of
dimension depending only on the number of points (logarithmically) and the desired accuracy,
while barely disturbing the distances between them? The answer is yes, and — remarkably — a
single, data-independent random construction (a random Gaussian matrix) achieves it with
positive probability for any point set. This mission formalizes the lemma and the two
probabilistic results its proof is built from.
Setting
For a set V of m points in RN, a map f:RN→Rk is a
(1±ϵ)-distance-preserving embedding of V if
(1−ϵ)∥u−v∥2≤∥f(u)−f(v)∥2≤(1+ϵ)∥u−v∥2 for every u,v∈V. The
book's proof constructs f=A/k from a random matrix A∈Rk×N with
i.i.d. standard normal (N(0,1)) entries, and argues by the probabilistic method: for a
fixed pair of points, Lemma 15.3 shows f preserves their squared distance up to
(1±ϵ) with probability at least 1−2e−(ϵ2−ϵ3)k/4, because the
ratio ∥f(x)∥2/∥x∥2 (for x the difference of the two points) is exactly a χk2
random variable, whose two-sided concentration around its mean k is Lemma 15.2. A union bound
over the O(m2) pairs in V then shows the probability that every pair is simultaneously
preserved is still strictly positive — so a map with the desired property must exist, even
though no single fixed matrix is exhibited.
Formalization targets
Lemma 15.2 (Chi-squared concentration, milestone). If Q∼χk2, then for
0<ϵ<1/2, P[(1−ϵ)k≤Q≤(1+ϵ)k]≥1−2e−(ϵ2−ϵ3)k/4.
Lemma 15.3 (Gaussian random projection distortion, milestone). For x∈RN,
k<N, and A∈Rk×N with i.i.d. N(0,1) entries,
P[(1−ϵ)∥x∥2≤k1Ax2≤(1+ϵ)∥x∥2]≥1−2e−(ϵ2−ϵ3)k/4.
Lemma 15.4 — the mission's goal (Johnson-Lindenstrauss). For 0<ϵ<1/2, integer
m>4, and k=20log(m)/ϵ2, any set V of m points in RN admits a map
f:RN→Rk with (1−ϵ)∥u−v∥2≤∥f(u)−f(v)∥2≤(1+ϵ)∥u−v∥2 for all u,v∈V.
Significance
This is one of the cleanest instances in the book of the probabilistic method: existence is
proved without exhibiting the object, by showing a random construction succeeds with positive
probability. The target dimension k=O(logm/ϵ2) is independent of the ambient
dimension N — the embedding works no matter how large the original feature space is, which
is exactly why the lemma has inspired random-projection methods throughout dimensionality
reduction, streaming algorithms, and compressed sensing. Prior art on the Prove2Me platform is
not faithful here: HighDimProb.Isoperimetry.johnson_lindenstrauss (Vershynin series) proves a
Johnson-Lindenstrauss-type bound, but via a uniformly-random m-dimensional subspace and its
orthogonal projection, rescaled by n/m — a genuinely different construction from this
book's explicit i.i.d.-Gaussian-matrix map f=A/k, and with different (existentially
quantified, unspecified) constants rather than this book's explicit k=20log(m)/ϵ2.
The two are classically known to give essentially the same qualitative guarantee, but showing
them equivalent would require an independent equivalence proof neither platform item nor this
mission undertakes; per the chunk's own brief, the Vershynin theorem is cited here only as
related work, not reused as a kind: reference item.
Not formalized here: Theorem 15.1 (the PCA solution), the chapter's other headline result.
BRIEF.md explicitly flags PCA and JL as the chapter's two independent capstones, not a
proof chain, and recommends dropping PCA if the mission focuses purely on JL. Theorem 15.1's
proof is an Eckart-Young-type Frobenius-norm optimization argument over the set of rank-k
orthogonal projection matrices — sharing no definitions, hypotheses, or proof technique with
the probabilistic-method argument this mission's three items are built from. Formalizing it
would mean standing up a second, unrelated piece of mathematics (constrained matrix
optimization, singular value decomposition) from scratch for a single additional item; per the
captain brief's guidance to leave out, rather than approximate, material disproportionate to
the time budget, it is omitted. §15.2 (kernel PCA) and §15.3 (Isomap, LLE, Laplacian
eigenmaps) are likewise out of scope, per BRIEF.md's own page-range restriction — applications-
heavy manifold-learning material with no numbered result feeding Lemma 15.4's proof.
Difficulty
Lemma 15.2's proof is a genuine Chernoff-bound argument: apply Markov's inequality to
exp(λQ), substitute the chi-squared distribution's own moment-generating function
(1−2λ)−k/2, and optimize the resulting bound over λ∈(0,1/2) by calculus
(the book's own choice λ=ϵ/(2(1+ϵ)) is exactly the minimizer) — not a
one-line union of tail bounds, and the same argument must be repeated (with a sign flip) for
the lower tail before combining via a union bound. Lemma 15.3's proof needs the non-obvious
observation that Tj=xj/∥x∥ (for x=Ax) are themselves i.i.d. standard
normal — a consequence of A's i.i.d. Gaussian entries and E[xj2]=∥x∥2,
not immediate from the definitions alone — before the sum of their squares can be recognized as
exactly a χk2 variable and Lemma 15.2 applied. Lemma 15.4's own proof, while
conceptually simple (a single union bound), needs the specific numerical accounting
2m2e−(ϵ2−ϵ3)k/4=2m5ϵ−3<2m−1/2 at the chosen
k=20log(m)/ϵ2 and ϵ≤1/2 to conclude the success probability is strictly
positive — a formalization that merely asserted "the union bound gives a positive probability"
without this exact accounting would not establish the book's specific, tight constant
k=20log(m)/ϵ2.
Formalization scope
SqNorm is the coordinate-wise squared Euclidean norm (∑ᵢ vᵢ²), used in place of Mathlib's
EuclideanSpace/PiLp norm typeclass machinery to keep the statements close to the book's own
concrete ℝ^N/ℝ^k-coordinate notation. IsChiSquaredMGF states the moment-generating-function
characterization of a chi-squared distribution that the proof of Lemma 15.2 itself cites
(Eq. C.25), rather than restating the book's own Definition C.7, which sits in an out-of-chapter
appendix not read for this mission; this is checked (in SELF_REVIEW.md) to be a faithful,
uniquely-determining substitute, since a real random variable's law is determined by its MGF
wherever it is finite near 0. IsIIDStandardGaussianMatrix states "i.i.d. standard normal
entries" via Mathlib's gaussianReal 0 1 (marginal law) together with iIndepFun (joint
independence). The goal theorem's target dimension k is taken as ⌈20 log(m)/ε²⌉ (Nat.ceil)
rather than the book's real-valued 20 log(m)/ε², since a map's codomain dimension must be a
natural number; this rounding only strengthens (never weakens) the existential conclusion, since
the union-bound success probability is monotonically increasing in k. No numerical constant in
any of the three items is otherwise altered from the book's own displayed form. A trivializing
formalization this mission avoids: stating Lemma 15.4 with an unspecified k = O(log m/ε²)
(an asymptotic, not an explicit constant) — per BRIEF.md's own naming of this as one of the
series' "explicit-constant" results, k's exact formula 20 log(m)/ε² (up to the ceiling
needed for well-typedness) is stated directly.
Selected references
M. Mohri, A. Rostamizadeh, A. Talwalkar, Foundations of Machine Learning, 2nd ed., MIT
Press, 2018, Chapter 15, §15.4.
W. B. Johnson, J. Lindenstrauss, "Extensions of Lipschitz mappings into a Hilbert space,"
Contemporary Mathematics 26, 1984, 189-206.
S. Vempala, The Random Projection Method, DIMACS Series in Discrete Mathematics and
Theoretical Computer Science, 2004.
Support Vector Machines VII: Consistency of Support Vector Machines for RegressionTextbook
Motivation
Chapter 9 asks whether the support vector machine — a regularized empirical risk minimizer
fD,λ over an RKHS H — is a statistically consistent estimator for regression: does
RL,P(fD,λn)→RL,P∗ as the sample size n→∞, for a suitable
regularization schedule λn→0? The chapter's main theorem (Theorem 9.1) answers yes,
under an explicit polynomial rate condition on λn. Its proof reduces the question to
bounding how far the empirical regularized solution can be from the population regularized
solution, and that reduction bottoms out in a single concentration-of-measure fact: how tightly
does an empirical mean of i.i.d. Hilbert-space-valued random variables concentrate around its
true mean, given only a bound on one q-th moment (no exponential-moment assumption at all)? That
fact is Lemma 9.2, "the following lemma to bound the probability of ∣RL,P(fD,λ)−RL,P(fP,λ)∣≤ε for ∣D∣→∞" — the technical core the whole
chapter's consistency argument rests on, and this mission's goal.
Setting
Fix a measurable space Z, a distribution P on Z, a separable Hilbert space H, and a
measurable g:Z→H. Its q-th moment norm, for q∈(1,∞), is ∥g∥q:=(EP∥g∥Hq)1/q — the direct Hilbert-space analogue of an ordinary Lq norm. The
proof machinery behind concentration results of this kind is symmetrization: replacing a
centered i.i.d. sum n1∑i(ξi−EPξi) by a Rademacher-randomized sum
n1∑iεiξi, where a Rademacher sequenceε1,…,εn
is a family of independent ±1-valued random variables, each taking each sign with probability
1/2. Once randomized, the sum's Lp-norms (for different p) become comparable to each other
via Kahane's inequality, with a universal constant depending only on the two exponents
involved — never on the sample size or the ambient Banach space.
Formalization targets
Goal: Lemma 9.2 (concentration of Hilbert-space-valued sample means)
for a universal constant cq>0 depending only on q, every ε>0 and every n≥1.
This is a genuine generalization of Chebyshev's inequality to Hilbert-space-valued means, sharp
enough (via the explicit rate n−q∗) to drive Theorem 9.1's own polynomial regularization
condition λnp∗n→∞.
Milestones (attack order)
Theorem A.8.1 (Symmetrization) — EPΨ(∥n1∑i(ξi−EPξi)∥)≤EPEνΨ(2∥n1∑iεiξi∥) for convex
non-decreasing Ψ, i.i.d. P-integrable ξi valued in a separable Banach space, and a
Rademacher sequence εi. Directly cited in Lemma 9.2's proof ("Using the
symmetrization argument given in Theorem A.8.1...").
Theorem A.8.3 (Kahane's inequality) — for a Rademacher sequence, every two Lp(ν) and
Lq(ν) norms of ∥∑iεixi∥ are comparable via a universal constant
Kp,q, independent of n and the Banach space E. Directly cited in Lemma 9.2's proof
("If q∈(1,2], we obtain with Kahane's inequality, see Theorem A.8.3, that...").
Theorem 9.1 itself (BRIEF.md's recommended goal — the full SVM-regression consistency theorem)
was not attempted this session; see STATUS.md for the reason and the fallback taken instead.
Significance
Lemma 9.2 is stated and proved once, in the Appendix's general Rademacher-sequence toolkit and
this chapter, and then used directly to obtain Theorem 9.1's consistency guarantee: substituting
g:= the pointwise SVM "difference process" into Lemma 9.2 converts a purely probabilistic
concentration fact into a statement about how close the empirical SVM solution's risk is to the
population solution's risk, for every sample size. Because the bound depends on nothing but a
single moment ∥g∥q — no boundedness, no sub-Gaussian tail — it is what lets Theorem 9.1 avoid
assuming the loss or the label distribution has any exponential tail control, which is essential
for regression (where Y⊂R need not be bounded, unlike the classification setting
of this series' earlier chapters). Symmetrization and Kahane's inequality are themselves standard,
reusable tools of empirical process theory (used throughout Chapter 7's entropy-number program,
excluded from this series, and Chapter 6's classification oracle inequality).
Difficulty
The published proof of Lemma 9.2 is a short but dense computation: Markov's inequality reduces the
tail bound to bounding EPn∥h∥Hq for the centered mean h; Theorem A.8.1
symmetrizes; for q∈(1,2], Theorem A.8.3 (Kahane) converts the q-th moment of the
Rademacher sum to its second moment, which an explicit orthogonality computation (the book's Eq.
(9.4), Eνn∥∑iεixi∥2=∑i∥xi∥2 for any fixed
x1,…,xn, an immediate consequence of the Rademacher signs' independence and the Hilbert
space's parallelogram identity) reduces to a sum of individual second moments; the case q>2
argues analogously with a different exponent split. None of this computation is captured by this
mission's two milestones alone — they supply the two cited theorems, not the connecting algebra
— so a complete proof of the goal from the milestones as stated still requires reconstructing this
argument, exactly as the captain brief's milestones are meant to be (the book's own attack path,
not a fully mechanized proof outline).
Formalization scope
Z and Θ (the Rademacher sequence's own probability space) are arbitrary measurable
spaces; H is [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [MeasurableSpace H] [BorelSpace H] [SeparableSpace H] (a separable real Hilbert space with its Borel
σ-algebra), matching "H be a separable Hilbert space" without narrowing to a concrete
space (e.g. ℓ2) the book itself does not assume. IsRademacherSequence states independence
via Mathlib's iIndepFun and the ±1-probability-1/2 condition directly, since no ready-made
"Rademacher distribution" object exists in this Mathlib revision (checked by search). q∗:=min{1/2,1−1/q} is substituted algebraically rather than introducing a separate conjugate
exponent q′, since 1/q+1/q′=1 pins q′ down uniquely — not a change of content. In Theorem
A.8.3, "for all Banach spaces E" quantifies over E : Type (the Type 0 universe) rather than
every universe Type*, a disclosed minor restriction with no effect on this mission's own use of
the theorem (with E instantiated to a Type* Hilbert space H that is, in every actual
application, itself at the Type level).
A trivializing formalization here would drop the "independent" half of IsRademacherSequence
(leaving only the marginal ±1-probability-1/2 condition, true even for perfectly correlated
signs) or drop the "i.i.d." qualifier on ξ1,…,ξn in Theorem A.8.1 (both symmetrization
and Kahane's inequality are false, or at least unproven by the book's own argument, without
independence) — both are ruled out here by stating iIndepFun explicitly rather than only the
marginal distribution conditions.
IsRademacherSequence is reusable beyond this mission: any future formalization of Chapter 7's
entropy-number/Rademacher-complexity program, or of Chapter 6's oracle inequality's own use of
Rademacher averages, would restate it locally (per Hard Rule 9) from the same book definition.
Contributions completing the three sorrys are welcome; Theorem 9.1 itself remains a natural,
substantially larger follow-up mission built on top of this one's two milestones together with
the RKHS/regularized-risk-minimizer apparatus already available in this series' 04-representer
mission (restated locally, per Hard Rule 9).
Selected references
I. Steinwart & A. Christmann, Support Vector Machines, Springer, Information Science and
Statistics, 2008. https://doi.org/10.1007/978-0-387-77242-4 (Chapter 9, §§9.1-9.2, pp. 333-337,
and Appendix §A.8, pp. 535-537).
J.-P. Kahane, Some Random Series of Functions, 2nd ed., Cambridge University Press, 1985
(Kahane's inequality, Theorem A.8.3's original source).
A. W. van der Vaart & J. A. Wellner, Weak Convergence and Empirical Processes, Springer, 1996
(Lemma 2.3.1, the source of Theorem A.8.1's proof technique).
High-Dimensional Probability X: Exact Sparse RecoveryTextbook
Motivation
Compressed sensing asks a question that looks impossible at first: can a signal x∈Rn
be reconstructed exactly from far fewer than n linear measurements y=Ax∈Rm, m≪n? Classical linear algebra says no — an underdetermined system has infinitely many solutions.
But if x is known in advance to be sparse (most of its coordinates are zero), the extra
structure makes recovery possible: solving the convex program that minimizes the ℓ1 norm of
a candidate solution, subject to matching the measurements, recovers x exactly, for a
measurement matrix A with a suitable geometric property. This idea, developed by Candès, Romberg,
Tao and Donoho in the mid-2000s, underlies modern MRI acceleration, single-pixel cameras, and
sparse signal processing generally.
The chapter isolates the exact geometric property a measurement matrix needs — the restricted
isometry property (RIP) — and proves, purely by linear algebra with no probability involved,
that RIP alone is sufficient for exact recovery by ℓ1 minimization. (A companion result,
outside this mission, shows random sub-gaussian matrices satisfy RIP with high probability once
m is large enough, which is what makes the deterministic guarantee here practically useful; this
mission formalizes the deterministic half.)
Setting
For a vector v indexed by a finite set, write ∥v∥0 for its number of non-zero coordinates
(so v is s-sparse if ∥v∥0≤s), ∥v∥1:=∑i∣vi∣ for its ℓ1 norm, and
∥v∥2:=∑ivi2 for its Euclidean norm.
An m×n matrix A satisfies the restricted isometry property (RIP) with parameters
α,β,s if
α∥v∥2≤∥Av∥2≤β∥v∥2for every s-sparse v∈Rn,
i.e. A acts as an approximate isometry on every s-sparse vector — equivalently (the book's own
Exercise 10.5.9), the singular values of every m×s column-submatrix of A lie in
[α,β].
Given a matrix A and measurements y=Ax for an unknown sparse x, the exact-recovery
program is
∃x^=xwheneverx^ solves the exact-recovery program for y=Ax,
precisely: suppose A satisfies RIP with parameters α,β,(1+λ)s where
λ>(β/α)2; then for every s-sparse x, every x^ that is feasible
(Ax^=Ax) and ℓ1-optimal among feasible vectors satisfies x^=x. No constant here
is hard-coded beyond the book's own explicit threshold λ>(β/α)2 — the weakest
stable form of the claim.
Significance
RIP isolates exactly the geometric mechanism that makes ℓ1-minimization work for sparse
recovery: once a matrix is known to satisfy it, exact recovery is a deterministic, provable
consequence with no appeal to randomness, no failure probability, and no measurement-count formula
to verify beyond the RIP parameters themselves. This clean separation — a purely geometric
sufficient condition (RIP), proved separately (in the book's Theorem 10.5.11, outside this
mission) to hold with high probability for random sub-gaussian matrices — is the template
compressed sensing theory follows throughout: geometric/deterministic guarantee first, probabilistic
verification that random constructions meet it second. The theorem is one of the two standard
routes (with the direct probabilistic argument of Theorem 10.5.1) to the chapter's central claim
that m=O(slogn) measurements suffice to recover any s-sparse signal in Rn —
exponentially fewer than the n measurements a naive linear-algebraic argument would need.
The result itself, and the RIP framework, are classical and well-established (Candès-Tao 2005).
This mission formalizes the deterministic linear-algebra core of the argument — the statement
infrastructure (RIP, sparsity, the exact-recovery program stated as an explicit optimization
problem) and the goal theorem — for a solver to close with a proof.
Difficulty
The natural first idea for showing x^=x is to try to bound the recovery error h:=x^−x
directly using ∥Ah∥2 (which vanishes, since both x and x^ are feasible) together with
RIP applied to h itself — but h need not be sparse at all: it is the difference of two
sparse-ish vectors and can have full support. The actual argument decomposes h's support into
blocks by descending magnitude (the support I0 of x, then the λs largest remaining
coordinates I1, then the next λs, and so on), applies RIP only to the leading block
I0,1=I0∪I1 (which genuinely has bounded sparsity ≤(1+λ)s), and separately
bounds the contribution of every later block using the fact that x^ is ℓ1-optimal (so
∥hI0c∥1≤∥hI0∥1, the "cone constraint"): each later block's ℓ2 norm is
controlled by the ℓ1 mass of the previous block divided by its size. This is a genuinely
multi-step argument combining a purely geometric fact (RIP on one bounded-sparsity block) with a
purely combinatorial one (the magnitude-sorted decomposition), and the "obvious" idea of applying
RIP to h as a whole does not typecheck, since RIP says nothing about vectors with more than
(1+λ)s non-zero entries.
Formalization scope
Vectors are plain functions ι → ℝ on a finite index type, not EuclideanSpace ℝ ι: the latter's
fixed ℓ2 norm instance cannot also host the ℓ1 norm the program's objective needs, so
both norms (L2Norm, L1Norm) are defined directly by their defining sums on the same underlying
type. Sparsity (Sparsity) takes a real-valued threshold s : ℝ, matching that the RIP parameter
(1+λ)s used by the goal theorem is a real number even at integer base sparsity. A solution
x^ "of the program" is formalized as an explicit argmin membership — feasibility
(A.mulVec xhat = A.mulVec x) conjoined with optimality over the exact feasible set
(∀ x', A.mulVec x' = A.mulVec x → l1Norm xhat ≤ l1Norm x') — never "there exists an estimator
such that", the trivialization risk this chapter's own triage brief flags explicitly (shared with
Chapter 3's Max-Cut): an existential reading would prove a different, strictly weaker statement.
The conclusion is stated for every such x^, not one witness, matching that RIP forces
uniqueness.
This mission covers Theorem 10.5.10 only, as the sole item; the probabilistic goal Theorem 10.5.1
(exact recovery for random sub-gaussian measurement matrices, which needs Theorem 10.5.10 together
with a separate probabilistic argument, Theorem 10.5.11, that random matrices satisfy RIP), and the
Lasso guarantee (Theorem 10.6.1), are both left out for lack of session time: each would need a
fresh probabilistic apparatus (independent isotropic sub-gaussian random rows, a failure-probability
bound) built from scratch in this chapter's own sub-namespace, with no reusable published
definition from an earlier chunk. L2Norm, L1Norm, Sparsity and RIP are reusable by any
later chapter or mission needing sparse vectors or the restricted isometry property; solvers'
contributions are welcome on completing the proof of Theorem 10.5.10 itself (the magnitude-sorted
support decomposition sketched under Difficulty above), and, beyond this mission's current scope,
on Theorem 10.5.11 and Theorem 10.5.1.
R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data
Science, Cambridge University Press, 2018, Chapter 10. https://doi.org/10.1017/9781108231596
High-Dimensional Statistics IV: Dudley's Entropy Integral BoundTextbook
Motivation
Many of the central questions of high-dimensional statistics reduce to bounding the expected
supremum of a stochastic process: the maximum correlation of noise with a family of candidate
signals, the operator norm of a random matrix, the uniform deviation of an empirical process from
its mean. Whenever the index set of the process is infinite or exponentially large, a naive union
bound over "all" indices is either vacuous or requires re-deriving a tail bound from scratch for
every new problem. Chaining is the general-purpose technique that removes this need: it bounds
the expected supremum of a process purely in terms of the geometry of its index set, measured by
how many balls of a given radius are needed to cover it. The classical form of this bound is due to
Dudley (1967), building on ideas that trace to Kolmogorov; the exposition here follows Wainwright,
High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019),
Chapter 5.
Setting
Fix an index set T and a collection of zero-mean random variables {Xθ,θ∈T}.
Say this collection is a sub-Gaussian process with respect to a (pseudo)metric ρX on T
(Definition 5.16) if
E[eλ(Xθ−Xθ′)]≤eλ2ρX(θ,θ′)2/2for all θ,θ′∈T,λ∈R.
This single condition covers, as special cases, the canonical Gaussian process
Xθ=⟨θ,w⟩ for w a standard Gaussian vector (with ρX the
Euclidean metric) and the Rademacher process built from i.i.d. Rademacher signs.
A δ-cover of T with respect to a metric ρ is a finite set
{θ1,…,θN}⊂T such that every θ∈T lies within ρ-distance
δ of some θi; the δ-covering numberN(δ;T,ρ) is the size of the
smallest such cover (Definition 5.1). The quantity logN(δ;T,ρ) is the metric
entropy of T at scale δ. Writing D:=supθ,θ′∈TρX(θ,θ′)
for the diameter of T, the δ-truncated Dudley entropy integral is
J(δ;D):=∫δDlogN(u;T)du.
Formalization targets
Goal — Theorem 5.22 (Dudley's entropy integral bound)
E[θ,θ′∈Tsup(Xθ−Xθ′)]≤2E[γ,γ′∈TρX(γ,γ′)≤δsup(Xγ−Xγ′)]+32J(δ/4;D),for any δ∈[0,D].
The bound holds for every zero-mean sub-Gaussian process, with no further structure on T beyond
its metric entropy — this is what makes it a general-purpose tool rather than a bound tailored to
one model.
The same conclusion with 32J(δ/4;D) replaced by the cruder single-scale term
4D2logN(δ;T), under the extra technical hypothesis N(δ;T)≥10. This is
the one-step precursor whose refinement — iterating the discretization over a geometric sequence
of scales instead of applying it once — is exactly what chaining improves.
Milestone — Theorem 5.25 (the Gaussian comparison principle)
A general comparison principle for pairs of centered Gaussian random vectors whose pairwise
covariances are ordered coordinatewise and tested against a function with matching sign
conditions on its mixed second partial derivatives: E[F(X)]≤E[F(Y)]. This is
the source, by specializing F and the covariance-ordering sets, of both Slepian's inequality and
the Sudakov–Fernique comparison, the two workhorse tools of Gaussian process theory used elsewhere
in the chapter to obtain sharper, Gaussian-specific bounds than the sub-Gaussian chaining bound
above.
Significance
Dudley's bound is the single most-used tool for controlling suprema of stochastic processes in
high-dimensional statistics and empirical process theory: Gaussian complexity bounds for convex
bodies, operator-norm bounds for random matrices, and uniform laws of large numbers for function
classes are all obtained by computing a covering-number bound for the relevant index set and
substituting it into Theorem 5.22 (see, for instance, Examples 5.18–5.21 later in the same
chapter, and Chapters 13–14 of the book). Its significance is exactly its generality: it converts
a purely geometric quantity — how "big" a set is under a metric — into a probabilistic bound,
uniformly over every sub-Gaussian process on that set.
Formalizing it. The mathematical proof (interpolation-free, based on chaining and repeated
union bounds) is well understood and not itself in question; what this mission produces is a
faithful Lean statement of the theorem, its immediate one-step precursor, and the general Gaussian
comparison principle that underlies the chapter's complementary (Gaussian-specific) results, each
against Mathlib's own measure-theoretic and Gaussian-process infrastructure. All three theorems are
currently stated as open goals (:= by sorry); no claim is made here that they are already
formalized elsewhere on the platform (a fresh prior-art search for "Dudley," "chaining," "Slepian,"
"Sudakov," and "Gaussian comparison" returned no faithful matches).
Difficulty
The naive approach — apply Proposition 5.17's one-step discretization once, at whatever scale
δ seems best — cannot see improvement past the cruder D2logN(δ;T) scaling
of the metric entropy at a single resolution. The chaining argument that proves Theorem 5.22 instead
telescopes the supremum across a geometric ladder of covers at scales D2−1,D2−2,…,
paying for each scale's approximation with a union bound over its own (much smaller, for a small
δ) covering number, and only then summing the resulting terms into an integral. The
difficulty is not any single step of this argument — each step is an elementary sub-Gaussian tail
bound — but bookkeeping the composition correctly: the recursive "best approximation at level m
of the best approximation at level m+1" chain (Eq. (5.47)) must be built explicitly, and the
telescoping sum of L union bounds, each over a set that itself depends on the level m, is what
converts into an integral only in the L→∞ limit as the covers refine to T itself.
Formalization scope
The index set T is formalized as a nonempty Fintype, rather than the book's general totally
bounded metric space: this keeps every covering number, diameter, and supremum in this mission a
genuine maximum over a finite, nonempty family (realized via ⨆/sInf over finite index types),
rather than requiring the full apparatus of totally bounded infinite metric spaces to state the
covering-number definition (Definition 5.1) faithfully without risking a vacuous or ill-defined
infimum. This is a genuine narrowing of the book's stated generality, disclosed here rather than
left implicit — the underlying mathematics of the proof does not depend on finiteness, but a
faithful formalization of a general totally bounded space's covering number was judged out of
scope for this mission's budget.
The constant 32 in the goal theorem is kept exactly as stated; the book's own remark that "there
is no particular significance to the constant 32, which could be improved with a more careful
analysis" is not license to substitute a sharper constant, since doing so would no longer match
what this particular proof establishes. Expectations are Bochner integrals against an explicit
probability measure Prob, with integrability required as an explicit hypothesis in the
sub-Gaussian process definition (SubGaussianProcess) rather than left implicit, since Mathlib's
Bochner integral silently returns 0 for a non-integrable function — a trivializing formalization
this mission's definitions and hypotheses rule out.
Theorem 5.25's "centered Gaussian random vector" is formalized using Mathlib's own
ProbabilityTheory.HasGaussianLaw predicate (a genuine multivariate Gaussian law, not merely
Gaussian marginals) together with an explicit coordinatewise mean-zero hypothesis, and its mixed
second partial derivative condition is formalized via iteratedFDeriv ℝ 2 F applied to the
relevant pair of standard basis vectors, keeping the sign pattern over the disjoint index sets A
and B exact rather than collapsing it to a global convexity assumption on F.
Out of scope for this mission: Sudakov's minoration (the complementary lower bound on the
expected supremum of a genuinely Gaussian process, Theorem 5.30, misidentified as "Theorem 5.36" in
this mission's planning brief — the correct Sudakov minoration statement is Theorem 5.30, p. 148;
Theorem 5.36 is instead a tail-bound generalization of Dudley's bound to ψq-Orlicz processes)
and the Slepian/Sudakov–Fernique corollaries of Theorem 5.25 (Corollary 5.26, Theorem 5.27) — both
natural follow-on work for a later contribution, once the Gaussian comparison principle formalized
here is in place.
Selected references
M. J. Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University
Press, 2019. DOI: 10.1017/9781108627771. Chapter 5.
R. M. Dudley, "The sizes of compact subsets of Hilbert space and continuity of Gaussian
processes," Journal of Functional Analysis, 1(3):290–330, 1967.
M. Ledoux and M. Talagrand, Probability in Banach Spaces: Isoperimetry and Processes,
Springer, 1991.
High-Dimensional Probability VII: Slepian's Inequality for Gaussian ProcessesTextbook
Motivation
A Gaussian process is a family (Xt)t∈T of jointly Gaussian real random variables
indexed by an arbitrary set T — not necessarily time. The canonical example is Xt=⟨g,t⟩ for t ranging over a subset T⊆Rn and g a standard
Gaussian vector in Rn; this single family already encodes questions as varied as the
operator norm of a random matrix, the size of a random projection, and the metric complexity of a
convex body. In every one of these applications the object of interest reduces to the same
quantity: Esupt∈TXt, the expected supremum of the process.
Bounding Esupt∈TXt directly is hard — computing it exactly is possible only in special
cases, such as the reflection principle for Brownian motion. Slepian's inequality (David
Slepian, 1962) sidesteps this by comparison: if a second Gaussian process (Yt)t∈T has
matching variances and at-least-as-large pairwise increments as (Xt)t∈T, then Y's
supremum stochastically dominates X's. This turns a hard direct estimate into a search for a
simpler comparison process — the technique that Sudakov and Fernique later sharpened by dropping
the equal-variance hypothesis (Theorem 7.2.11), and that Sudakov used to derive a purely
geometric lower bound on Esupt∈TXt from the covering numbers of (T,d) (Theorem 7.4.1,
Sudakov's minoration inequality). Together these results are the entry point to the theory of
Gaussian width and generic chaining that occupies the rest of the book (Chapters 7–9, 11), and
they underlie sharp bounds on random matrices (Section 7.3), random projections (Chapter 9), and
high-dimensional geometry more broadly (Adler and Taylor, Random Fields and Geometry, Springer,
2007; Talagrand, Upper and Lower Bounds for Stochastic Processes, Springer, 2014).
Setting
Fix a probability space (Ω,F,P). A random process indexed by a set T is a
family (Xt)t∈T of real random variables on Ω. It is a Gaussian process if
every finite linear combination ∑t∈T0atXt (T0⊆T finite, at∈R) is a (possibly degenerate) normal random variable — equivalently, every finite
marginal (Xt)t∈T0 is a multivariate Gaussian vector. A process is mean zero if
EXt=0 for every t.
For a mean zero process, the incrementsd(t,s):=∥Xt−Xs∥L2=(E(Xt−Xs)2)1/2 always define a (pseudo)metric on T — the canonical metric — turning the
otherwise unstructured index set into a metric space. For a metric space (T,d) and $\varepsilon
0,the∗∗coveringnumber∗∗N(T,d,\varepsilon)isthesmallestcardinalityofafinitesubsetN\subseteq TsuchthateverypointofTiswithin\varepsilonofsomepointofN(an\varepsilon−net);N(T,d,\varepsilon) := \infty$ if no finite net exists.
Because T need not be countable, supt∈TXt(ω) need not be a measurable function
of ω. Following the book's own convention, every quantity built from this supremum —
Esupt∈TXt and P{supt∈TXt≥τ} — is instead defined through the process's
finite-dimensional marginals: as the supremum, over finite nonempty T0⊆T, of
Emaxt∈T0Xt (respectively P{maxt∈T0Xt≥τ}). This sidesteps the
measurability question entirely, at the cost of the quantity possibly being +∞.
Formalization targets
Slepian's inequality (Theorem 7.2.1, goal)
Let (Xt)t∈T and (Yt)t∈T be mean zero Gaussian processes with EXt2=EYt2
and E(Xt−Xs)2≤E(Yt−Ys)2 for all t,s∈T. Then for every τ∈R,
Under only the increment hypothesis E(Xt−Xs)2≤E(Yt−Ys)2 (no equal-variance
hypothesis),
Et∈TsupXt≤Et∈TsupYt.
This is the weaker-hypothesis, strictly more applicable form: it is what Sudakov's minoration
inequality and the sharp Gaussian random matrix bound of Section 7.3 both invoke.
Let (Xt)t∈T be a mean zero Gaussian process with canonical metric d. For every
ε≥0 at which N(T,d,ε)=:N is finite,
Et∈TsupXt≥cεlogN
for an absolute constant c>0. This is the weakest, most stable form of the bound: it names no
numerical value for c, so it survives any later sharpening of the constant.
Slepian's inequality, finite-dimensional case (Theorem 7.2.9, milestone)
The vector-indexed special case of Theorem 7.2.1 (T finite), proved first by Gaussian
interpolation and then extended to the general index set.
Significance
The results themselves. Slepian's inequality is the founding comparison theorem for Gaussian
processes; Sudakov-Fernique's inequality is its practically indispensable generalization, used
routinely to bound suprema of Gaussian processes without needing to track variances explicitly.
Sudakov's minoration inequality is the first bridge from the probability of a Gaussian process to
the metric geometry of its index set, complementing Dudley's upper bound (Chapter 8) and
together giving matching bounds — up to a logarithmic factor, and exactly in many cases of
interest — on Esupt∈TXt purely from the covering numbers of (T,d). Downstream, this
machinery gives the sharp bound E∥A∥≤m+n on Gaussian random
matrices (Section 7.3), underlies the Gaussian width used throughout convex geometry and
compressed sensing (Chapters 9, 11), and bounds the covering numbers of polytopes and other
convex sets (Corollary 7.4.4).
Formalizing it. All three inequalities are proved by the book (Gaussian interpolation and
integration by parts for Slepian/Sudakov-Fernique; a direct application of Sudakov-Fernique to a
well-chosen comparison process for Sudakov's minoration), so this mission's work is formalizing
the statements faithfully and precisely — including the finite-marginal convention needed to
make Esupt∈TXt and P{supt∈TXt≥τ} meaningful for an uncountable index
set without begging the underlying measurability question. The Gaussian interpolation technique
itself (Lemmas 7.2.3, 7.2.5, 7.2.7) is not part of this mission's formalization scope; it is the
proof method for the milestones and belongs to solvers closing them.
Difficulty
The obvious first idea — bound EsuptXt by controlling each Xt separately, e.g. via a
union bound over a net — throws away exactly the structure Slepian-type comparisons exploit: the
joint Gaussianity across t, not marginal tail behavior at each fixed t. A union bound needs
a net and a modulus of continuity to begin with; Slepian's and Sudakov-Fernique's inequalities
need neither — they compare two processes directly through their covariance structure, which is
what makes the technique (Gaussian interpolation: continuously deform the covariance of one
process into the other's, and track how a smooth, nearly-indicator functional behaves along the
path) work with no assumption on T beyond the two hypotheses stated. The genuine difficulty is
the smooth-interpolation argument itself — showing that Ef(Z(u)) is monotone in u for the
right choice of test function f — which is exactly the part left as a milestone for solvers to
formalize, not sketched here per the mission format's own rule against proof ideas.
Formalization scope
Esupt∈TXt (ProcessESup) is valued in EReal, not ℝ: the finite-marginal supremum a
real-valued definition would silently default to the junk value 0 when the set of finite-marginal
expectations is unbounded above — exactly the case the book itself records as Esupt∈TXt=∞ (Exercise 7.4.2, a non-relatively-compact index set). P\{\sup_{t\in T}X_t\ge\tau\}
(ProcessTailProb) stays real-valued, since it is always bounded in [0,1] and so carries no
such risk. Both are defined through finite nonempty subsets of T, per the book's own footnote
to Section 7.2; no separability, continuity, or countability assumption is placed on T itself.
Gaussianity is Mathlib's ProbabilityTheory.IsGaussianProcess — every finite restriction of the
process has a Gaussian law — which is definitionally the book's Definition 7.1.10 ("every finite
linear combination is Gaussian"); mean-zero is stated as an explicit hypothesis alongside it.
Integrability of every quantity appearing under an expectation is not stated as a separate
hypothesis: Fernique's theorem (already in Mathlib for general Gaussian measures) guarantees a
Gaussian process has finite moments of every order, exactly as the book takes for granted.
Sudakov's minoration inequality (Theorem 7.4.1) is formalized for the case the book's own proof
actually covers — N(T,d,ε) finite, taken as a hypothesis = (N : ℕ) rather than as a
case split inside the conclusion — since the book itself defers the infinite-covering-number case
to a separate, unproved exercise (7.4.2). This keeps T fully general (still possibly
uncountable) at every fixed ε where the net is finite, which rules out a trivializing
reading of the theorem: nothing here forces T itself to be finite or countable, only the
covering number at the scale ε in play, which is the book's own hypothesis.
Definitions reusable beyond this mission: ProcessESup, ProcessTailProb, CanonicalMetric,
and CoveringNumber are exactly the substrate Chapters 8 ("Dudley's Integral Inequality"), 9
("The Matrix Deviation Inequality"), and 11 ("Dvoretzky-Milman's Theorem") need for Gaussian
width and generic chaining; per this series' plan those missions restate them locally (drafts
cannot import another draft's definitions), using this chunk's forms as the faithful reference.
Contributions closing the Gaussian-interpolation machinery (Lemmas 7.2.3–7.2.8) as a reusable
definitions layer, beyond what any one milestone needs, are welcome.
D. Slepian, "The one-sided barrier problem for Gaussian noise", Bell System Technical
Journal 41 (1962), 463–501.
V. N. Sudakov, "Gaussian random processes and measures of solid angles in Hilbert space",
Soviet Mathematics Doklady 12 (1971), 412–415.
X. Fernique, "Regularité des trajectoires des fonctions aléatoires gaussiennes", in École
d'Été de Probabilités de Saint-Flour IV-1974, Springer Lecture Notes in Mathematics 480
(1975), 1–96.
M. Talagrand, Upper and Lower Bounds for Stochastic Processes: Modern Methods and Classical
Problems, Springer, 2014.
Introduction to Online Convex Optimization XI: Boosting via Online Convex OptimizationTextbook
Motivation
A "rule of thumb" classifier — a single pixel's brightness distinguishing handwritten "0" from
"1" — is trivial to produce and barely better than a coin flip. A rule that gets every example
right is, in general, far harder. Boosting asks whether many weak, easy-to-produce rules can be
combined into one strong, hard-to-produce rule, and Chapter 11 answers it via a black-box
reduction: any online convex optimization algorithm with sublinear regret, paired with access to
a weak learner, yields a boosting algorithm — the same OCO-to-learning-theory template Chapter IX
used for generalization, now applied to training-set fitting.
Setting
A concept class H is γ-weakly-learnable (Definition 11.1) if some algorithm, given
enough labeled samples, returns a hypothesis with error at most 21−γ with high
probability — better than random guessing by a fixed margin γ, far short of the
arbitrarily-small error strong (PAC) learning demands. Section 11.2.1 fixes a simplified setting:
binary zero-one loss, a realizable concept class (some h⋆∈H has zero error), and a
weak-learning oracle W(p,δ′) returning, on distribution p over a fixed sample S of
size m, a hypothesis with Pr[errorp(W(p,δ′))≥21−γ]≤δ′.
Algorithm 34 runs an OCO algorithm AOCO over the m-dimensional simplex
Δm (distributions over the sample): at each round it calls the weak learner on the
current distribution pt, builds the {0,1}-valued cost vector rt recording which
examples ht got right, updates pt+1←AOCO(f1,…,ft) for the
linear cost ft(p)=rt⊤p, and finally outputs the majority vote
hˉ(x)=sign(∑t=1Tht(x)).
Formalization targets
Theorem 11.2 — the mission's sole target (goal)
For T chosen so T1RegretT(AOCO)≤2γ, Algorithm 34
returns hˉ with Pr[errorS(hˉ)=0]≥1−δ: with high probability,
hˉ classifies the entire training sample S perfectly.
Significance
This is one of the cleanest reduction theorems in the book: it needs no property of the weak
learner beyond its γ-margin guarantee, and no property of the OCO algorithm beyond a
regret bound — any of Chapters III–X's algorithms (multiplicative weights, OGD, RFTL, ONS...)
plugs in directly, and §11.2.3 specializes the reduction with multiplicative weights to recover a
close relative of AdaBoost, one of machine learning's most influential algorithms. The proof
technique — a contradiction argument on the existence of a "hard" residual distribution p⋆
uniform over the misclassified examples — is itself instructive and structurally different from
Chapter IX's martingale/concentration argument, despite both chapters being "OCO implies a
learning-theoretic guarantee" reductions. No prior art was found on the platform for boosting or
AdaBoost (planning search: q=boosting, q=AdaBoost — 0 hits); this mission drafts the theorem
fresh.
Difficulty
The proof's key step packages the algorithm's regret guarantee (a worst-case statement, true
for every cost sequence including an adversarially-constructed one) into a proof by
contradiction: assuming some nonempty set of misclassified examples Sϕ survives, the
uniform distribution p⋆ over Sϕ is shown to make every ht perform at best exactly
at the 21 threshold on average (since hˉ's sign disagrees with the true label on
every point of Sϕ, at most half of the T rounds' hypotheses can have agreed there),
while the weak-learner guarantee (via a union bound over all T rounds) forces the actual
played distributions pt to see ≥21+γ average performance — and the algorithm's
low regret against p⋆ specifically then closes the gap into an outright contradiction
(21+γ≤21+2γ, impossible for γ>0). This chain — union
bound over rounds, regret bound against one specific (adversarially-identified) comparator, and
an averaging argument over the residual set — is more intricate than its short proof suggests.
Formalization scope
EmpiricalErrorWeighted/EmpiricalError give the (weighted and uniform) training-error
quantities exactly as the book states them, with real-valued (±1) labels and predictions — the
convention this chapter's sign-based majority vote needs, distinct from Chapter IX's
Bool-valued zero-one loss (a deliberate, chunk-local choice, not a conflict, since the two
chapters use different label conventions for different reasons — see MODERATION_NOTES.md).
IsBoostingRun formalizes Algorithm 34's five lines, with the weak learner's round-t call
modeled as a random hypothesis h_t : Ω → X → ℝ (since a weak-learning call is itself
probabilistic) rather than a deterministic function, matching the book's own probabilistic
per-call guarantee. The goal theorem states the weak-learner guarantee (hweak), the OCO
regret guarantee (hA), and the choice of T (hTreg) as explicit hypotheses, per BRIEF.md's
own instruction that these are the theorem's real content, not incidental setup. h̄ is typed as
an arbitrary X → ℝ, never coerced into H — the book's own explicit remark that the boosted
hypothesis need not belong to the original weak-hypothesis class.
This chunk has no milestones: Chapter 11 is short and largely monolithic around Theorem 11.2,
with Section 11.2.1 ("Simplification of the setting") and 11.2.2 ("Algorithm and analysis")
building directly to it with no other numbered lemma on the relevant pages (PDF 207–211).
Definition 11.1 (weak learnability) is drafted as a definition, not manufactured into a
milestone, per CAPTAIN_BRIEF.md's own rule that definitions are never milestones and
BRIEF.md's explicit allowance for a mission with fewer than 3. §11.2.3's AdaBoost
specialization (a corollary discussion, not a separately numbered theorem on these pages) is not
formalized.
Selected references
E. Hazan, Introduction to Online Convex Optimization, 2nd ed., arXiv:1909.05207v3, Chapter 11.
R.E. Schapire, "The strength of weak learnability," Machine Learning 5(2), 1990, 197-227.
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
(AdaBoost).
Introduction to Online Convex Optimization II: Convergence Rates for Well-Conditioned Convex OptimizationTextbook
Motivation
Convex optimization — minimizing a convex function over a convex set — is the offline
problem that online convex optimization (OCO) generalizes: an OCO algorithm run against a
single, fixed cost function repeated every round is exactly an algorithm for this classical
problem. Its convergence theory, developed over decades and surveyed comprehensively in
Nesterov [Introductory Lectures on Convex Optimization, 2004] and Boyd and Vandenberghe
[Convex Optimization, 2004], supplies the analytical toolkit — potential functions,
strong convexity, smoothness — that every regret bound in the rest of this book reuses. This
chapter is the book's own self-contained account of that toolkit: it proves nothing about
regret or adversaries, but the algorithms and inequalities it establishes for gradient
descent recur, essentially unchanged, in the online setting three chapters later.
The chapter's own capstone, a linear convergence rate under a joint strong-convexity and
smoothness assumption, traces to Nesterov's classical analysis of gradient descent under a
condition-number bound; the Polyak step size predates it, going back to Polyak's 1969
subgradient method for problems with a known optimal value.
Setting
Fix a real, complete inner product space E (a Hilbert space) and a convex, closed set
K⊆E, the decision set. A function f:E→R is α-strongly
convex (with gradient map g:E→E) if for every x,y∈E,
f(y)≥f(x)+⟨g(x),y−x⟩+2α∥y−x∥2,
and β-smooth if for every x,y∈E,
f(y)≤f(x)+⟨g(x),y−x⟩+2β∥y−x∥2.
Strong convexity lower-bounds f by a quadratic of curvature at least α at every
point; smoothness upper-bounds it by a quadratic of curvature at most β. When f is
twice differentiable these say αI⪯∇2f(x)⪯βI for every
x. A function that is both is called γ-well-conditioned, where
γ:=α/β≤1 is its condition number.
Write x⋆ for a minimizer of f (over E, or over K in the constrained case), and
for any point x define three measures of distance to optimality: the value gap
hx:=f(x)−f(x⋆), the Euclidean distance dx:=∥x−x⋆∥, and the
gradient norm ∥∇x∥:=∥g(x)∥. Gradient descent starts at x0 and iterates
xt+1=xt−ηtg(xt) for a step-size schedule ηt; in the constrained case
each step is followed by a projection xt+1=ΠK(yt+1) back onto K.
Formalization targets
Goal: Theorem 2.6 (linear convergence for well-conditioned functions)
ht+1≤h1⋅e−γt/4for every t≥0,
for constrained gradient descent (Algorithm 4) on a γ-well-conditioned f over K,
with the constant step size ηt=1/β. This is the chapter's strongest rate: for
the best-conditioned class of functions it considers, the optimality gap shrinks by a
constant factor every round, rather than polynomially in t.
Milestone: Theorem 2.2 (KKT optimality condition)
⟨∇f(x⋆),y−x⋆⟩≥0for every y∈K,
when x⋆ minimizes f over a convex K. The multi-dimensional first-order
optimality condition for constrained minimization, generalizing ∇f(x⋆)=0 in
the unconstrained case (K=E).
Milestone: Theorem 2.3 (GD with the Polyak step size)
for unconstrained gradient descent with step size ηt=ht/∥∇t∥2, where
xˉ achieves the smallest value among x0,…,xT. A single algorithm, needing no
prior knowledge of α, β, or G beyond the (assumed available) optimal value
f(x⋆), automatically attains whichever of the four rates applies to f.
The chapter's basic toolkit: four inequalities letting a proof substitute one measure of
progress (value gap, distance, gradient norm) for another as needed.
Significance
Theorem 2.6 is the model result behind every subsequent linear-rate claim in convex
optimization: it isolates the exact mechanism (strong convexity plus smoothness, combined
multiplicatively through the condition number) that turns a 1/T or 1/T rate into
an e−Ω(t) one. Theorem 2.3 demonstrates the opposite phenomenon — a single
step-size rule that adapts to whatever structure f happens to have, without needing to
know which structure that is — a design principle the book's later chapters (adaptive
regret, adaptive gradient methods) return to repeatedly. Lemma 2.4 is used directly inside
the book's own proof of Theorem 2.6 and is stated separately because later chapters cite
its four bounds individually.
None of these four statements has a machine-checked proof on the platform prior to this
mission (see Formalization scope). Formalizing them establishes strong convexity and
smoothness, in the book's own quadratic-bound form, as reusable definitions, together with
the constrained- and unconstrained-gradient-descent update rules that Chapter III's online
algorithm specializes.
Difficulty
The linear rate of Theorem 2.6 does not follow from Lemma 2.4 alone: chaining the smoothness
upper bound and the strong-convexity lower bound gives only a bound relating ht+1 to
dt2, not to ht itself, and a naive one-step decrease argument stalls at a rate of
1−γ per round rather than 1−γ/4 — the factor of four comes from combining
the projection's contraction property (the constrained analogue of Theorem 2.3's telescoping
argument) with the smoothness bound simultaneously, not from either alone. The Polyak step
size of Theorem 2.3 is remarkable, and its analysis correspondingly delicate, because the
step size ηt=ht/∥∇t∥2 depends on the unknown optimal value f(x⋆)
through ht; the proof must derive all four regimes (general convex, smooth, strongly
convex, well-conditioned) of BT from the same one-line per-round inequality, rather than
running four separate arguments.
Formalization scope
E is formalized as an arbitrary real, complete inner product space, not fixed to
Rd, matching this book's chapter-wide convention (Chapter III's mission of this
series does the same). Strong convexity and smoothness are formalized in the book's own
quadratic-bound form with an explicit gradient map g as a separate parameter (not tied to
f by automatic differentiation), rather than via the second-derivative characterization; a
theorem needing g to be the actual gradient of f adds that as a separate hypothesis. This
avoids a trivializing formalization under which the predicate could be satisfied by an
unrelated g: every theorem here that uses StronglyConvexOn/SmoothOn also assumes g is
a global gradient map for f. Theorem 2.3's realized-gradient bound ∥∇t∥≤G is
formalized only over the run's own iterates x0,…,xT (not as a global Lipschitz bound
on f), matching the book's own statement ("assuming ∥∇t∥≤G"): a global
gradient bound would be jointly unsatisfiable with global strong convexity on any
infinite-dimensional or unbounded E, since a strongly convex function's gradient grows
without bound away from its minimizer. Sequences are 0-indexed, so a book statement at round
t+1 (1-indexed) is stated here at index t; each theorem's docstring records the exact
shift. The projection in Algorithm 4 reuses OnlineConvexOpt.FirstOrder.IsMetricProjection,
already published for this series' Chapter III, rather than redeclaring it.
Theorem 2.10 (the chapter's further, book-stated-without-proof rate) is out of scope: the
book explicitly defers its proof to outside references, so it cannot be a faithful milestone
under this platform's provenance requirement. Section 2.4's reductions of non-smooth or
non-strongly-convex problems to this chapter's setting (via randomized smoothing) are left
for a future extension, since they introduce a new construction not needed by the goal or its
milestones.
High-Dimensional Probability II: Concentration Inequalities for Sums of Independent Random VariablesTextbook
Motivation
The central limit theorem tells us that a normalized sum of independent random variables
converges in distribution to a Gaussian. For applications — bounding the failure
probability of a randomized algorithm, controlling the error of a Monte Carlo estimator,
proving a generalization bound in learning theory — a limiting distribution is not enough:
what is needed is a single, explicit, non-asymptotic inequality that holds for every fixed
sample size N, not merely as N→∞. Hoeffding's inequality (Wassily Hoeffding,
1963) and Bernstein's inequality (Sergei Bernstein, 1920s–1940s, in the form used here due
to Vadim Bennett and later authors) are the two archetypal answers: both give an explicit
Gaussian-type tail bound for a weighted sum of independent random variables, valid for
every N, with all constants made explicit. They are the workhorses behind concentration
of measure, high-dimensional statistics, and the non-asymptotic analysis of randomized
algorithms; a textbook trying to reach the Johnson–Lindenstrauss lemma, random matrix
norms, or the restricted isometry property has to pass through this chapter first, because
every one of those results is itself an application of a weighted-sum concentration
inequality to a specific choice of random variables.
The central limit theorem's own error term is the obstruction that direct concentration
inequalities are built to avoid: the Berry–Esseen theorem (Andrew C. Berry, 1941; Carl-Gustav
Esseen, 1942) bounds the normal approximation's error at order 1/N, which is too
slow to recover a genuinely exponential tail bound for finite N. Hoeffding's and Bernstein's
inequalities are proved instead by a direct argument — bounding the moment generating
function of the sum and optimizing a Markov/Chernoff exponential tilt — that never invokes
the central limit theorem or its error term at all.
The sub-gaussian and sub-exponential norms
Fix a probability space (Ω,F,P). For a real random variable X on
(Ω,F,P), define its sub-gaussian norm
∥X∥ψ2:=inf{t>0:Eexp(X2/t2) is finite and ≤2}
and its sub-exponential norm
∥X∥ψ1:=inf{t>0:Eexp(∣X∣/t) is finite and ≤2}.
In both definitions, the requirement that the exponential moment be finite (i.e. that the
moment-generating integrand be integrable), and not merely satisfy "≤2" as a bare
inequality, is essential: without it a moment that is genuinely infinite for a given t
would vacuously count as "≤2" under the Bochner integral's convention that a
non-integrable function integrates to 0, and every random variable — however heavy-tailed
— would trivially have norm 0. X is called sub-gaussian (respectively sub-exponential)
when this infimum is over a nonempty set, i.e. when some finite t makes the moment finite
and at most 2. These are genuine norms (up to
the identification of almost-surely-equal random variables) on the vector space of random
variables for which they are finite, and they are the natural non-asymptotic yardsticks for
tail heaviness: ∥X∥ψ2<∞ characterizes a Gaussian-type tail
P{∣X∣≥t}≤2exp(−ct2/∥X∥ψ22), while ∥X∥ψ1<∞
characterizes an exponential-type tail P{∣X∣≥t}≤2exp(−ct/∥X∥ψ1). Every
bounded random variable — in particular every Bernoulli or Rademacher (symmetric Bernoulli)
random variable — is sub-gaussian, and the square of a sub-gaussian random variable is
sub-exponential; a genuinely sub-exponential (not sub-gaussian) example is the squared
coordinate gi2 of a standard Gaussian vector, or the exponential distribution itself.
Formalization targets
Goal — Theorem 2.8.2 (Bernstein's inequality, weighted sum). Let X1,…,XN be
independent, mean-zero, sub-exponential random variables on (Ω,F,P), and
let a=(a1,…,aN)∈RN. Then, for every t≥0,
where K=maxi∥Xi∥ψ1 and c>0 is an absolute constant that does not depend
on N, the Xi, a, or t.
The goal is deliberately the weighted and sub-exponential form, the weakest of the
chapter's results that is still stable under the improvements a solver might find: it
neither fixes ai≡1 (the unweighted Theorem 2.8.1, a special case) nor restricts to
the lighter sub-gaussian tail (Theorem 2.6.3, which follows from a strictly stronger
hypothesis). Both weaker theorems, plus Hoeffding's and Chernoff's inequalities, are
included as milestones because Bernstein's own proof is built directly from them.
Significance
The result itself. Bernstein's inequality is the two-tail-regime concentration bound: a
sub-gaussian tail exp(−ct2/(K∥a∥2)2) near the mean, transitioning to a heavier
sub-exponential tail exp(−ct/(K∥a∥∞)) far from it, exactly the behavior one should
expect from a mixture of light-tailed terms with one heavy-tailed outlier. It underlies the
concentration of quadratic forms (Chapter 6's Hanson–Wright inequality controls
∑εiεj-type terms, which are themselves products of sub-gaussians
and hence sub-exponential by Lemma 2.7.7), and it is the standard tool for bounding
empirical-process suprema whose summands are not bounded but merely light-tailed.
Formalizing it. No formalization of Bernstein's inequality — in either the weighted or
unweighted, or sub-gaussian or sub-exponential form — exists yet on Prove2Me (GET /theorems?q=Bernstein and q=sub-exponential return no relevant hits, checked
2026-09-17). What this mission produces is not just the statement but the machinery
underneath it: a working Orlicz-norm treatment of ψ1 and ψ2 that a later mission
(the Hanson–Wright inequality, or any future chapter that needs sub-exponential
concentration) can build on directly.
Difficulty
The obvious first idea — squaring both sides and applying Chebyshev, as one does to prove
the weak law of large numbers — gives only a polynomial tail bound decaying like 1/N,
far too weak to be useful (this is exactly the point made by the chapter's opening
discussion of the coin-tossing example, comparing the linear decay from Chebyshev against
the target exponential decay). The central limit theorem promises the right shape of tail
asymptotically but, per Berry–Esseen, with an error of order 1/N that swamps any
exponential gain for large deviations — the CLT approximation is simply not valid in the
tail regime the inequality needs. The actual argument instead controls the moment
generating function of the full sum directly and optimizes an exponential (Chernoff) tilt;
this is why the sub-gaussian and sub-exponential norms — MGF-control objects, not moment or
tail objects per se — are the right technical vehicle, even though Proposition 2.5.2 and
2.7.1 show all these characterizations are equivalent up to constants. The min of two terms
in Bernstein's exponent is not an artifact of a loose proof: it reflects a genuinely
two-regime tail (Gaussian near the mean, exponential in the far tail), and collapsing it to
a single term in either direction would either be false (dropping the exponential term) or
needlessly weak (dropping the Gaussian term, which is what a naive union bound over the
worst single term would give).
Formalization scope
Random variables are ℝ-valued functions on an explicit probability space (Ω, mΩ, P)
(Ω : Type, MeasurableSpace Ω, P : Measure Ω, [IsProbabilityMeasure P]), matching the
book's setup throughout. Independence is Mathlib's ProbabilityTheory.iIndepFun, and
tail probabilities are stated with P.real, Mathlib's ℝ-valued measure evaluation, which
corresponds directly to the book's P{⋅}.
Both Orlicz norms are defined locally, as genuine infima matching Definitions 2.5.6 and
2.7.5 verbatim (subgaussianNorm, subexponentialNorm, each
sInf {t > 0 : Integrable (fun ω => E[...]) P ∧ E[...] ≤ 2}), rather than reused from
Mathlib's HasSubgaussianMGF (Mathlib.Probability.Moments.SubGaussian). The Integrable
conjunct is not optional dressing: Mathlib's Bochner integral of a non-integrable function is
0 by convention, so a bare E[...] ≤ 2 (without asserting integrability) would be satisfied
by everyt for which the moment is actually infinite, collapsing the sub-gaussian norm of
a standard Gaussian (and, symmetrically, the sub-exponential norm of any heavy-tailed
variable) to 0 — a trivializing formalization the mission was moderated to rule out. The
same Integrable conjunct appears in every moment hypothesis (general_hoeffding,
bernstein_unweighted, bernstein_weighted): ∃ s > 0, Integrable (...) P ∧ ∫ ... ≤ 2, so
that the hypothesis is not satisfied vacuously by non-integrable exponential moments either.
HasSubgaussianMGF bounds the moment generating function directly with a variance-proxy
parameter σ2 (E exp(tX) ≤ exp(c t²/2)), which is a different object definitionally
from the Orlicz ψ2 norm — equivalent up to a constant factor by the book's own
Proposition 2.5.2, but not interchangeable without restating that equivalence — and
Mathlib has no sub-exponential analogue at all. Since the goal theorem and two of its
milestones need the sub-exponential norm, one consistent convention (the book's own Orlicz
norms) is used for both ψ1 and ψ2 throughout the mission, rather than mixing
Mathlib's MGF-based sub-gaussian convention with a locally defined sub-exponential one.
Every occurrence of the book's "c is an absolute constant" is formalized as a genuine
existential quantifier fixed before the random variables, the vector a, and t are
introduced: ∃ c : ℝ, 0 < c ∧ ∀ ..., P.real {...} ≤ 2 * Real.exp (-(c * ...)). No numeral is
substituted for c anywhere; a solver's proof may use any positive constant it can establish,
exactly mirroring the book's own non-constructive existence claims. The trivializing
formalization this rules out is fixing c to a specific small numeral (which would be a
strictly stronger, easier, and unfaithful claim) or, in the other direction, weakening the
statement by allowing c to depend on N, the Xi, a, or t (which would make the
theorem vacuous, since any such bound trivially holds for a small enough c depending on the
instance).
Chernoff's inequality (Theorem 2.3.1) needs no Orlicz norm — Bernoulli parameters pi are
given directly via P.real {X i = 1} = p i ∧ P.real {X i = 0} = 1 - p i, and the conclusion
uses Real.rpow (^ on ℝ → ℝ → ℝ) for the real exponent t in (eμ/t)t. Hoeffding's
inequality for symmetric Bernoulli variables (Theorem 2.2.2) is likewise self-contained,
needing only the two-point probability hypothesis defining the Rademacher distribution.
Selected references
W. Hoeffding, Probability Inequalities for Sums of Bounded Random Variables, Journal of
the American Statistical Association 58(301), 1963. https://doi.org/10.2307/2282952
S. Bernstein, The Theory of Probabilities, Gastehizdat Publishing House, Moscow, 1946
(Russian; the inequality is due to Bernstein's earlier 1920s–1930s work, this textbook
states the modern sub-exponential form following later expositions).
A. C. Berry, The Accuracy of the Gaussian Approximation to the Sum of Independent
Variates, Transactions of the American Mathematical Society 49(1), 1941.
https://doi.org/10.2307/1990053
C.-G. Esseen, On the Liapunoff Limit of Error in the Theory of Probability, Arkiv för
Matematik, Astronomi och Fysik A28, 1942.
R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data
Science, Cambridge University Press, 2018, Chapter 2. https://doi.org/10.1017/9781108231596
High-Dimensional Probability I: Approximate Carathéodory's TheoremTextbook
Motivation
Many arguments in high-dimensional geometry, statistics and computer science need to
approximate a point of a convex set by an average of a handful of extreme points, rather than
represent it exactly. The classical Carathéodory theorem (1907) answers the exact question:
every point of the convex hull of a set T⊆Rn is a convex combination of at
most n+1 points of T. That bound is tight and grows with the dimension n, which makes it
useless whenever n is large — exactly the regime of interest in high-dimensional probability.
A convex combination of finitely many points z1,…,zm∈Rn is a sum
∑i=1mλizi with λi≥0 and ∑iλi=1. The convex
hullconv(T) of a set T⊆Rn is the set of all convex
combinations of all finite collections of points of T. The diameter of T is
diam(T)=sup{∥s−t∥2:s,t∈T}, the Euclidean norm throughout.
The classical Carathéodory theorem states that every x∈conv(T) is a convex
combination of at most n+1 points of T — with n+1 generally unavoidable, attained by a
simplex. The question this mission answers is different: given that we are willing to
approximatex rather than represent it exactly, and willing to use only combinations with
equal coefficients 1/k (an average of k points, with repetition allowed), how large must
k be as a function of the desired accuracy?
The quantifiers are exactly this order: for every bounded T, every point of its convex
hull, and every target k, such an averaging set exists. This is the weakest stable
statement carrying the theorem's content — the number of points k does not depend on the
dimension n, and the coefficients are forced to be uniform — and it is the form the corollary
below invokes directly.
Milestone — Corollary 0.0.4, Covering polytopes by balls
This is a direct application of the goal to computational geometry's covering problem: how many
balls of radius ε are needed to cover a polytope, and where should they be centered.
Significance
The result itself. The approximate Carathéodory theorem is the prototype of a dimension-free
approximation result: whenever a set is bounded, a fixed number of points (depending only on the
target accuracy, not the ambient dimension) suffices to approximate any point of its convex hull.
This is what makes possible dimension-independent covering-number bounds such as Corollary 0.0.4,
which in turn are the starting point for the book's later treatment of entropy, packing and
generic chaining (Chapters 4, 7–8). The technique generalizes far beyond Rn: it
underlies covering-number bounds for operators between Banach spaces (Carl's original
application) and is a recurring device in learning theory for bounding the size of an
ε-net of a hypothesis class.
Formalizing it. Both results are elementary and already fully proved in the literature; no
open mathematical content remains. What this mission contributes is a machine-checked,
faithful Lean statement of Maurey's construction and its corollary, phrased over Mathlib's
existing convex-hull and metric-diameter machinery, so that later missions in this series
(concentration inequalities, Johnson–Lindenstrauss, chaining) can build on a verified base case
of "probability constructs a deterministic covering," and so that the empirical method itself
becomes a reusable, linked component on the platform. The proof of the goal (via the probabilistic
argument sketched by the book: interpret a convex combination as a probability distribution,
average k i.i.d. samples, and bound the variance) is left open for solvers.
Difficulty
The identity that makes the proof work — averaging k independent copies of a random vector
concentrates around its mean at rate 1/k in mean-square — is a two-line computation once
the convex combination is reinterpreted probabilistically. The step that is easy to miss is this
reinterpretation itself: nothing in the statement mentions probability, so the "obvious" attack
of manipulating the convex-combination weights directly, or trying to construct x1,…,xk
by some explicit combinatorial recipe, does not see a path to a bound independent of n. The
probabilistic argument produces the points non-constructively, via an averaging/existence
argument (the expected squared distance is small, so some realization achieves it) rather than
an explicit formula — a solver has to introduce a probability space and a random vector that
does not appear anywhere in the formal statement to be proved.
Formalization scope
Both results are stated over EuclideanSpace ℝ (Fin n) for an explicit dimension n : ℕ, so
‖·‖ is the Euclidean norm and Mathlib's Metric.diam is used directly for
diam(T)=sup{∥s−t∥2}. The convex hull is Mathlib's convexHull ℝ T; by
Mathlib's convexHull_eq, this already coincides with the book's own definition of a convex
combination of finitely many points of T, so no bespoke convex-combination definition is
introduced — this mission needs no supporting definitions of its own. In the corollary, "a
polytope P with N vertices" is formalized, following the book's own proof, as
P=conv(T) for a finite vertex set T with #T=N, rather than via a
separate Polytope structure (which Mathlib does not provide and the book's argument does not
need). The covering bound N⌈1/ε2⌉ is an exponent, not a product with
N — matching the book's own proof, which counts the Nk ordered k-tuples of vertices with
repetition, k:=⌈1/ε2⌉; the typeset "N⌈1/ε2⌉" in
the corollary statement is the same juxtaposition-as-exponent notation the proof uses for
"Nk" one line earlier.
A trivializing formalization is ruled out explicitly: the goal must hold for every integer
k>0 and everyx∈conv(T), not merely some convenient choice — e.g.
k=1 together with x∈T trivially satisfies the inequality but proves nothing about the
theorem's actual content, that a fixed, dimension-independentk works uniformly over all
points of the hull. The formal statement quantifies T, then x, then k, and only then
asserts existence of the x1,…,xk, exactly in that order.
Classical Carathéodory (Theorem 0.0.1, stated for context in the source but not used by
either formalized result's proof) is not drafted here: Mathlib already proves the corresponding
statement via affine independence
(Caratheodory.eq_pos_convex_span_of_mem_convexHull, Analysis/Convex/Caratheodory.lean),
from which the book's "n+1 points" bound follows via
AffineIndependent.card_le_finrank_succ. It is not added as a kind: reference milestone
because no corresponding theorem is yet published on the Prove2Me platform to point at (checked
2026-09-17: GET /theorems?q=Caratheodory returns only unrelated tropical-convexity results),
and re-drafting existing Mathlib content as a new platform theorem would duplicate rather than
reuse it.
Selected references
R. Vershynin, High-Dimensional Probability: An Introduction with Applications in Data
Science, Cambridge University Press, 2018, DOI 10.1017/9781108231596,
Appetizer (pp. 1–5).
G. Pisier, "Remarques sur un résultat non publié de B. Maurey," Séminaire d'Analyse
Fonctionnelle (Maurey–Schwartz), 1980–1981, exposé no. 5.
numdam.org/item/SAF_1980-1981____A5_0
B. Carl, "Inequalities of Bernstein-Jackson-type and the degree of compactness of operators in
Banach spaces," Annales de l'Institut Fourier, 35(3), 1985, 79–118.
numdam.org/item/AIF_1985__35_3_79_0
Foundations of Reinforcement Learning II: Contextual Bandits and Inverse Gap WeightingTextbook
Motivation
Decision-making problems rarely present the same fixed choice twice. A doctor prescribing a
treatment sees each patient's medical history and symptoms before deciding; a website choosing
which article to show sees the visitor's profile first. The multi-armed bandit model —
where the learner repeatedly picks from a fixed set of arms with no side information — cannot
express this: it is blind to the covariates that any real decision-maker actually observes.
The contextual bandit model closes this gap by letting the learner see a context before
acting, and asks for a decision rule that generalizes across contexts rather than memorizing a
policy per context. Foster and Rakhlin's Foundations of Reinforcement Learning and Interactive
Decision Making (arXiv:2312.16730v1, Section 3, pp. 38–53) develops this model and its
algorithms as the bridge between supervised learning and sequential decision making, en route to
general reinforcement learning. Contextual bandits with a learned reward-function class underlie
production systems for content recommendation, online advertising, and adaptive clinical trial
design (Li et al., A Contextual-Bandit Approach to Personalized News Article Recommendation,
2010, https://arxiv.org/abs/1003.0146; Agarwal et al., Making Contextual Decisions with Low
Technical Debt, 2016, https://arxiv.org/abs/1606.03966).
The algorithmic history in this chapter runs through two distinct principles. The optimism
principle (LinUCB, Section 3.2) generalizes the UCB algorithm to contexts under a linear reward
model, but the chapter's own Example 3.1 (Section 3.3) shows optimism fails outside such
structured classes, incurring regret linear in the size of the context space or the class.
Foster and Rakhlin then present two "black-box" alternatives that use any function class F
through an abstract regression subroutine: the naive ε-Greedy method (Section 3.4),
and the Inverse Gap Weighting (IGW) strategy underlying the SquareCB algorithm (Bietti,
Agarwal & Langford, A Contextual Bandit Bake-off, 2018, https://arxiv.org/abs/1802.04064;
Foster & Rakhlin, Beyond UCB: Optimal and Efficient Contextual Bandits with Regression Oracles,
2020, https://arxiv.org/abs/2002.04926). SquareCB attains a regret rate that both generalizes
across contexts (no dependence on the size of the context space) and matches the optimal
T rate — improving on ε-Greedy's T2/3 rate — while remaining agnostic to
the internal structure of F.
Setting
Over T rounds, a decision-maker faces the contextual bandit protocol: at each round t,
it observes a context xt∈X, selects a decision πt from a finite action set
Π={1,…,A}, and observes a reward rt∈R. Rewards are generated
independently as rt∼M⋆(⋅∣xt,πt) for a fixed, unknown conditional
model M⋆; write f⋆(x,π):=E[r∣x,π] for the mean reward function
and π⋆(x):=argmaxπf⋆(x,π) for the optimal, context-dependent policy. The
context sequence x1,…,xT is arbitrary — fixed in advance or adversarially chosen — while
rewards remain stochastic. Performance is measured by regret against π⋆:
where pt is the learner's (possibly randomized) action distribution at round t.
To generalize across contexts, the learner is given a class F⊆{f:X×Π→R} with f⋆∈F, and aims for regret scaling with the statistical complexity
log∣F∣ rather than with ∣X∣. Both algorithms in this mission access F only through an
online regression oracle (Definition 3, p. 47): given the history
(x1,π1,r1),…,(xt−1,πt−1,rt−1), it returns an estimate
f^t:X×Π→R satisfying, with probability at least 1−δ,
∑t=1TEπt∼pt[(f^t(xt,πt)−f⋆(xt,πt))2]≤EstSq(F,T,δ) — for instance, exponential weights on a finite class F achieves
EstSq(F,T,δ)=log(∣F∣/δ). SquareCB (p. 50–51) then samples its action from
the Inverse Gap Weighting distribution (Definition 4, p. 50): given a vector of estimated
values f^∈RA with greedy action πˉ=argmaxπf^(π), and an
exploration parameter γ≥0, p=IGWγ(f^) is p(π)=1/(λ+2γ(f^(πˉ)−f^(π))) for the unique λ∈[1,A] making p a probability
distribution.
This holds for anyf^,f⋆∈RA and any γ>0, with no reference to
F or to how f^ was produced — it is the purely algebraic core the goal theorem invokes at
every round.
Goal — Proposition 10 (SquareCB regret bound)
Reg≤2ATEstSq(F,T,δ)
with probability at least 1−δ, for SquareCB run with γ=TA/EstSq(F,T,δ), for any context sequence x1,…,xT. This is the
weakest stable target level in the chapter's oracle-based development: it is stated for an
arbitrary class F and oracle, so it survives any future improvement to the oracle's own
EstSq bound, unlike a version hard-coded to a specific class or oracle.
Significance
Proposition 10 shows that Inverse Gap Weighting converts any estimation-error guarantee into a
regret guarantee with the same statistical rate, with no algorithm-side dependence on the
structure of F or the size of X: the same SquareCB template, driven by a plug-in regression
oracle, is minimax optimal whenever the oracle itself is. When F is finite, this yields
Reg≲ATlog(∣F∣/δ), matching the optimal rate for stochastic
multi-armed bandits (Section 2) while generalizing across contexts — a guarantee that optimism
(Proposition 7) provably cannot deliver outside linear classes (Example 3.1), and that the
simpler ε-Greedy baseline (Proposition 8) only delivers at a slower T2/3 rate.
Foster and Rakhlin describe Proposition 9 itself as being "at the core of the development for the
rest of the course": the same IGW mechanism reappears, generalized, in the book's treatment of
general decision-making and the Decision-Estimation Coefficient.
Both propositions are proved results, not open questions; this mission's contribution is a
machine-checked formalization of their exact statements and hypotheses — the precise
OracleGuarantee hypothesis Proposition 10 requires, the exact constant (2, not a bare
≲) its proof yields at the stated optimal γ, and the universally-quantified form
of the IGW inequality (Proposition 9) that makes it reusable independently of any particular
oracle or class.
Difficulty
The obvious first idea for exploiting an estimator f^t is a UCB-style optimism approach:
build a confidence set around f^t and act greedily on its upper envelope, as in LinUCB
(Proposition 7). Example 3.1 shows this fails in general: a class F can force the confidence
set to remain wide on a fresh action at every new context, driving regret linear in
min{∣F∣,∣X∣} — the confidence width in the regret bound does not shrink merely because the
oracle's cumulative estimation error is small, since that error is not localized to the
specific action the confidence-set approach tries next. Uniform exploration
(ε-Greedy) sidesteps this but wastes exploration budget on actions already known to
be far from optimal, which is what caps its rate at T2/3 (Proposition 8). Inverse Gap
Weighting instead ties the sampling probability itself to the estimated gap from the greedy
action, so cheap-to-rule-out actions are down-weighted continuously rather than either fully
explored (ε-Greedy) or trusted outright (optimism); the technical content of Proposition 9 is
showing this specific reciprocal-gap form gives a bound with no hidden dependence on F or X,
for every pair (f^,f⋆) simultaneously — a guarantee optimism cannot match because
its confidence sets are class-dependent by construction.
Formalization scope
Contexts form an arbitrary type X; actions are Fin A for A : ℕ. A finite probability
distribution over Fin A is represented directly as p : Fin A → ℝ with ∀ π, 0 ≤ p π and
∑ π, p π = 1, and Eπ∼p[g] as the finite sum ∑ π, p π * g π, rather than
via Mathlib's PMF (which is ℝ≥0∞-valued) — an equivalent and lighter-weight representation of
a distribution on a finite type. The normalizing constant λ of Definition 4 and the
optimal actions π⋆, πˉ are each specified by their defining property (existence
of λ∈[1,A] realizing the IGW formula; ∀π,f(π)≤f(argmax)) rather
than constructed explicitly via an intermediate-value or Finset.argmax argument, avoiding
committing to one choice function for a value the book itself leaves implicit. The class F
enters neither proposition's statement directly: it appears in the source only through the
abstract bound EstSq(F,T,δ), which is carried as an explicit real-valued
parameter and hypothesis (OracleGuarantee) rather than as a literal subset of a function space,
since no property of F beyond producing this bound is ever used. The probability-(1−δ)
qualifier attached to the online regression oracle's guarantee is likewise the explicit
hypothesis OracleGuarantee ... EstSq on a fixed realized run, rather than a statement
quantified over an underlying probability space of histories — every subsequent step in both
propositions' proofs is deterministic given that this event holds, so this does not weaken either
conclusion. A trivializing formalization would fix A=1 (a single ever-optimal action, making
both Reg and the IGW inequality vacuous) or take EstSq as an unconstrained free variable with
no positivity hypothesis (making γ in Proposition 10 undefined); this mission's statements
require 0 < EstSq and leave A, T, X, F-via-EstSq fully general.
This mission omits Proposition 7 (LinUCB): its proof rests on an entirely disjoint apparatus
(finite linear parameter sets, least-squares confidence sets, the elliptic potential lemma) that
neither Proposition 9 nor 10 requires, and Example 3.1 (the failure of optimism) is a worked
example rather than a numbered, formalizable claim. It also omits Proposition 8
(ε-Greedy): the source leaves the optimal ε unspecified ("choosing
ε appropriately"), and deriving its own optimal value and matching constant
independently — rather than reusing the book's own explicit constant, as Rule 7 of this
formalization effort requires — was judged too likely to introduce an unfaithful, invented
constant within this mission's time budget; both are natural extensions for a follow-up mission
or contribution. Reusable infrastructure: the Fin A-indexed finite-distribution convention and
the OracleGuarantee/optimal-action-by-property pattern extend directly to any later chapter
built on the same online-regression-oracle abstraction.
Selected references
Foster, D. J. and Rakhlin, A. Foundations of Reinforcement Learning and Interactive Decision
Making. 2023. https://arxiv.org/abs/2312.16730
Foster, D. J. and Rakhlin, A. Beyond UCB: Optimal and Efficient Contextual Bandits with
Regression Oracles. ICML 2020. https://arxiv.org/abs/2002.04926
Bietti, A., Agarwal, A., and Langford, J. A Contextual Bandit Bake-off. JMLR 2021 (arXiv
2018). https://arxiv.org/abs/1802.04064
Li, L., Chu, W., Langford, J., and Schapire, R. E. A Contextual-Bandit Approach to
Personalized News Article Recommendation. WWW 2010. https://arxiv.org/abs/1003.0146
Foundations of Reinforcement Learning I: Multi-Armed Bandits and the UCB AlgorithmTextbook
Motivation
The multi-armed bandit is the simplest model of sequential decision-making under
partial feedback: a learner repeatedly picks one of finitely many options and
observes a reward only for the option chosen, never for the alternatives. It
formalizes problems ranging from clinical trial design (which treatment to offer a
patient) to online advertising (which ad to show) and A/B testing more generally.
The framework dates to Robbins' 1952 paper on sequential design, and the algorithm
this mission's goal theorem concerns — the Upper Confidence Bound (UCB) algorithm of
Lai and Robbins [1985] and Auer, Cesa-Bianchi and Fischer [2002] — is the canonical
answer to how to explore efficiently: instead of exploring uniformly at random, act
optimistically with respect to the current uncertainty about each option's value.
This mission draws its formalization from Chapter 2 of Foster and Rakhlin's 2023
lecture notes, Foundations of Reinforcement Learning and Interactive Decision
Making, which develops the bandit problem as the first rung of a ladder of
increasingly general interactive decision-making settings (contextual bandits,
structured bandits, reinforcement learning) that the book's later chapters build.
Setting
Fix a finite decision (action) space Π={1,…,A}. In the multi-armed
bandit protocol, for each round t=1,…,T the learner selects a decision
πt∈Π, possibly at random according to a distribution pt depending on
the history Ht−1=((π1,r1),…,(πt−1,rt−1)) observed so far, and
then observes a reward rt∈R drawn independently from a fixed
conditional distribution M⋆(⋅∣πt) (the stochastic rewards
assumption). Writing f⋆(π):=E[r∣π] for the mean reward
function and π⋆:=argmaxπf⋆(π) for an optimal decision, the
learner's performance is measured by the regret
Reg:=t=1∑Tf⋆(π⋆)−t=1∑TEπt∼pt[f⋆(πt)].
Because the learner observes a reward only for the action played (bandit feedback),
a purely greedy strategy that always plays the current empirical maximizer can commit
to a suboptimal action forever, incurring linear regret; some form of deliberate
exploration is necessary. The chapter's central construction is the confidence
interval: a pair of functions ft,fˉt:Π→R
such that, with probability at least 1−δ, f⋆(π)∈[ft(π),fˉt(π)] for every round t and decision π
simultaneously. The UCB algorithm plays the optimistic action
πt=argmaxπfˉt(π) at every round, using the confidence interval
built from Hoeffding's inequality around the empirical mean f^t(π).
Formalization targets
Goal — Proposition 5 (UCB regret)
Reg≲ATlog(AT/δ)
holding with probability at least 1−δ, for the UCB algorithm using the
confidence radius 2log(2T2A/δ)/nt(π) of Eq. (2.19). This is the
weakest stable statement the chapter proves: it is optimal up to the log factor, and
strengthening it (e.g. to the sharper instance-dependent bound of Remark 10) is
explicitly left to later work by the book itself.
Milestones
Proposition 4 (ε-Greedy regret):Reg≲A1/3T2/3log1/3(AT/δ) — the book's preceding, weaker result, establishing that naive forced exploration already gives sublinear regret, and motivating why an adaptive strategy (UCB) does better.
Lemma 7 (Optimism): the per-round regret of the optimistic action is bounded by the confidence width at that action.
Lemma 8 (Confidence width potential lemma):∑t=1T(1/nt(πt)∧1)≲AT, a pigeonhole bound on how often any one action's confidence interval can still be wide.
Significance
UCB is the prototype of the "optimism in the face of uncertainty" principle that
recurs, in increasingly abstract form, throughout the rest of the book: the same
two-step argument (Lemma 7 + Lemma 8) reappears for linear bandits, structured
bandits via the Decision-Estimation Coefficient, and UCB-VI for tabular
reinforcement learning. Formalizing Chapter 2 in full therefore front-loads the
proof pattern every later chapter in this series specializes. The result itself is
also of standalone interest: the AT minimax rate is the benchmark every
subsequent bandit algorithm in the literature is compared against, and the
A1/3T2/3-vs-AT contrast between ε-Greedy and UCB is the standard
illustration, in any course on the subject, of why adaptive exploration matters.
No formalization of this exact statement — realizability with respect to a
function class f⋆∈F=RΠ and a generic confidence
interval, rather than a per-arm sub-Gaussian empirical mean — currently exists on
the platform (see Formalization scope below); the mission both proves this specific
regret bound and seeds the generic optimism/potential lemma pair (Lemma 7, Lemma 8)
that the book's later, more structured settings specialize.
Difficulty
The natural first attempt — bound the regret of the empirical-mean-greedy algorithm
directly — fails outright: on a two-armed instance where one arm is deterministic
and the other only slightly better in expectation, the greedy algorithm can commit
to the worse arm forever with constant probability, giving linear, not sublinear,
regret (§2.1). The obvious fix, ε-Greedy, forces exploration uniformly across all
actions regardless of how much is already known about each, so the exploration cost
scales with εT even for actions whose value is already well
determined — this is exactly what caps ε-Greedy at the T2/3 rate. UCB's
optimism principle resolves this by exploring an action only in proportion to how
uncertain it still is; the technical core, isolated in Lemma 7 and Lemma 8, is
disentangling "the algorithm made a mistake" from "the algorithm is still
uncertain," which are conflated in the naive per-round regret decomposition used for
ε-Greedy.
Formalization scope
Both the goal and the milestones fix a finite decision space Fin A, a mean reward
function fStar : Fin A → ℝ with fStar π ∈ [0,1], and an optimal decision
piStar. Regret is defined generically (Eq. (2.3)) via per-round decision weights
p : ℕ → Fin A → ℝ, so it applies uniformly to a randomized algorithm (ε-Greedy) and
a deterministic one (UCB, via the point mass at the played action). The book's "with
probability at least 1−δ" qualifier on both Proposition 4 and Proposition 5 is
formalized as the deterministic consequence of the underlying concentration event
(Eq. (2.9) and Eq. (2.18) respectively) holding — exactly the move the book's own
proofs make ("Let us condition on the event in (2.18) ... "). The concentration
events themselves rest on Hoeffding's inequality for adaptive stopping times
(Lemma 33) and Bernstein's inequality (Lemma 5), both stated in the book's technical
appendix outside this chapter, and are not drafted here; a solver may either take
them as a hypothesis (as this mission's statements do) or import/prove them
separately. A trivializing formalization is ruled out explicitly: taking δ outside
(0,1), or dropping the fStar π ∈ [0,1] hypothesis, would make the stated
constants vacuous or false, so both are retained as explicit hypotheses in every
theorem. In every ≲ statement (Prop. 4, Lemma 8, Prop. 5) the witnessed constant
C is quantified before the instance parameters (A, T, δ, and the realized
sequences): ∃ C, 0 < C ∧ ∀ A T δ ..., Reg ≤ C * (rate), not the other order. This
is deliberate, not stylistic: quantifying C after the instance lets it depend on
A, T, δ, making the bound satisfiable by an arbitrarily large C chosen per
instance and hence content-free, which is not what the book's ≲ means (a single
constant working uniformly over all instances). Proposition 5's UCB decision rule
is stated in the book's own two clauses, not collapsed into a single "maximize the
upper confidence bound" rule: the confidence radius of Eq. (2.19) is +∞ at
nt(π)=0 (an action never yet sampled), so the book's UCB always plays an
unsampled action before ever comparing indices, and only compares finite upper
confidence bounds once every action has been sampled at least once; the confidence
event of Eq. (2.18) is correspondingly assumed only at sampled actions, since the
book's own bound is vacuous otherwise. An earlier draft instead capped the radius
at 1 when nt(π)=0, which is a true statement about a different algorithm (a
sampled action can have index above the capped unsampled index), and was corrected
to the book's own rule after moderation. Reuse from the platform's existing bandit library (BanditAlgorithm,
Lattimore & Szepesvári) is deliberately avoided: that library's UCB
(bandit_ucb_regret_bound, bandit_ucb_minimax_regret_bound) is stated for
per-arm 1-sub-Gaussian rewards with δ=1/n2 fixed by the horizon, whereas
this chapter's UCB is stated for a free failure probability δ and a generic
confidence-interval abstraction (the multi-armed case being F=RΠ of the book's general realizability framework) — the two are
related but not the same statement. Contributions extending the mission with the
generic confidence-interval form of Lemma 7/8 applied to other chapters in this
series (contextual and structured bandits) are welcome.
Selected references
T. Lai and H. Robbins, Asymptotically Efficient Adaptive Allocation Rules, Advances in Applied Mathematics, 1985.
P. Auer, N. Cesa-Bianchi, and P. Fischer, Finite-time Analysis of the Multiarmed Bandit Problem, Machine Learning, 2002.
D. Foster and A. Rakhlin, Foundations of Reinforcement Learning and Interactive Decision Making, arXiv:2312.16730, 2023. https://arxiv.org/abs/2312.16730
T. Lattimore and C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020.