Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Chapter I's usual stochastic order compares two real-valued random variables by "how large" they tend to be. Chapter VI lifts the same idea to random vectors: is smaller than in the usual multivariate stochastic order if is less likely than to land in any upper set of — any region defined by "at least this large in every coordinate." This mission formalizes that order and its two founding characterizations: a coupling theorem (the direct -dimensional generalization of Chapter I's own coupling theorem) and a common-source representation, plus two closure properties that make the order usable in practice.
Let be a random vector taking values in on a probability space , and let be a random vector taking values in on a (possibly different) probability space . is smaller than in the usual multivariate stochastic order, written , if
where an upper set is one closed upward under the coordinatewise partial order on ( iff for every ). Equivalently, iff for every increasing (increasing with respect to that same coordinatewise order) for which the two expectations exist — the form this mission drafts as the definition, exactly parallel to the univariate order's own equivalent form.
This is the direct -dimensional generalization of Chunk 01's Theorem 1.A.1: a joint law on the random vectors' shared space realizing as an almost-sure coordinatewise inequality between copies. The book does not give this direction's proof here (an explicit construction appears later, in a special case irrelevant to a statements-only mission), and the claim is exactly as citable either way.
The usual multivariate stochastic order is the natural tool for comparing random vectors — costs, resource-usage profiles, portfolio returns — that must be ranked simultaneously across several coordinates rather than reduced to a single scalar summary first. It underlies simulation comparisons (via the coupling and common-source characterizations, both constructive), reliability comparisons of multi-component systems (whose component lifetimes are naturally vector-valued), and comparative-statics arguments in queueing and inventory models with several state variables. The closure properties are what make the order compositional: conjunction closure says a vector-by-vector comparison of independent inputs survives any coordinatewise-increasing post-processing, and marginalization closure says a joint comparison restricts consistently to any sub-collection of coordinates — together they are the two properties an analyst reaches for first when reducing a multivariate comparison to a more tractable one.
No platform prior art exists: GET /theorems?q=stochastic+order and q=coupling return zero
genuine hits (checked at this book's triage time, re-confirmed this session). This mission
restates the usual multivariate stochastic order and its two founding theorems as a
self-contained foundation, in the same spirit as Chunk 01's univariate mission but independently
drafted, since drafts cannot import each other's Lean.
The chief formalization risk this chapter's own brief flags is conflating "increasing" for
with some order other than the coordinatewise one (a total
order via a fixed embedding, or a lexicographic order): the book's order on is
always the componentwise partial order, and Mathlib gives Fin n → ℝ exactly that order by
default (its Pi/product order), so Monotone φ for φ : (Fin n → ℝ) → ℝ already means what the
book means with no extra predicate to get wrong — but it would be easy to instead encode
ℝ^n-valued objects some other way (e.g. a fixed linear functional into ℝ) that silently swaps
in a different, weaker order. The second risk is Theorem 6.B.16(b)'s literal codomain: the book
states (scalar), so the closure conclusion is a genuinely
univariate stochastic-order statement about applied to vector inputs, not a
vector-to-vector closure (that is part (a), not drafted here) — stating it as a multivariate
conclusion by mistake would silently strengthen a theorem the book does not claim.
Random vectors are drafted as functions into Fin n → ℝ from arbitrary measurable spaces, which
inherit Mathlib's default coordinatewise (Pi) order — the same order the book uses throughout
this chapter, requiring no separate order predicate. MultivariateOrder μ ν X Y quantifies over
φ : (Fin n → ℝ) → ℝ with Monotone φ in that order and Integrable (φ ∘ X) μ/Integrable (φ ∘ Y) ν stated inside the ∀, exactly matching "for which the expectations exist." Equality in
law is ProbabilityTheory.IdentDistrib. Theorem 6.B.2's random variable is drafted as
-valued specifically (not an arbitrary-type common source), matching the book's own
"for all " quantification exactly.
Theorem 6.B.16(b) is drafted for a common dimension across all rather than the
book's per- dimension : the concatenated input then lives in Fin m → Fin n → ℝ (nested
Pi types, carrying the coordinatewise order on exactly as needed), avoiding a
dependent-sum concatenation of vectors of genuinely different lengths that a mission of this size
does not justify. This is the "closed under convolutions" special case the book itself names as a
corollary of the general statement, not a different claim — but it is a genuine restriction of
scope, recorded here rather than silently applied, and the general varying-dimension statement is
left for a future pass (see STATUS.md). The theorem's conclusion is stated as the univariate
order's own defining inequality on ℝ (∀ x, μ {ω | x < ψ(X_∙ ω)} ≤ ν {ω | x < ψ(Y_∙ ω)}),
restated locally rather than importing Chunk 01's UsualOrder, since drafts cannot import
another mission's definitions. Theorem 6.B.16(c)'s sub-index set of size
is encoded as an injective reindexing r : Fin k → Fin n, with drafted as X, Y
precomposed coordinatewise with r, matching the book's own subvector notation (6.A.1) exactly.
A trivializing formalization this mission rules out: drafting MultivariateOrder with an
order on Fin n → ℝ other than the coordinatewise one (for instance, a fixed linear functional
collapsing the vector to a scalar and reusing the univariate order), which would silently state a
different, generally weaker order under the same name; and drafting Theorem 6.B.16(b)'s conclusion
with a vector-valued (rather than the book's literal scalar-valued) , which would silently
strengthen a theorem the book states only for real-valued . This mission draws on no
platform prior art (searches for "stochastic order" and "coupling" as of 2026-09-18 return zero
genuine matches). Reusable beyond this mission: the MultivariateOrder definition pattern and its
coupling/common-source characterization parallel Chunk 01's univariate pair closely enough that a
future chapter needing a multivariate order's own coupling theorem (Chapter VII's multivariate
convex order is the direct next instance in this series) could restate the same shape with minimal
adaptation.
StochasticOrders.Usual), for the univariate usual stochastic order and
its coupling/common-source characterizations this chapter directly generalizes.Every statistical guarantee for a learning algorithm ultimately rests on a concentration inequality: a bound on how far an empirical average can stray from its expectation. For real-valued averages, Bernstein's inequality (1924, refined through the 20th century) is the classical tool — sharper than Hoeffding's inequality whenever the summands' variance is small compared to their range. Modern learning theory, however, frequently needs to control averages of objects that are not real numbers but elements of a Hilbert space: feature vectors , gradients of a loss, or the values a kernel machine's empirical risk functional takes. Steinwart & Christmann, Support Vector Machines (Springer 2008, Information Science and Statistics), Chapter 6, develop exactly the vector-valued extension needed for the book's own SVM consistency proofs: Theorem 6.14, Bernstein's inequality for independent random variables taking values in a separable Hilbert space, and its corollaries.
Fix a probability space and a separable real Hilbert space . Random variables are independent if the family is mutually independent (not merely pairwise), and has essential supremum bound , , if for -almost every . Writing for , the quantities of interest are the mean (a Bochner integral) and the variance bound , an upper bound on .
The classical scalar case (Theorem 6.12, itself a refinement of Hoeffding's inequality, Theorem 6.10) bounds for real-valued, mean-zero, range- and variance-bounded . The tool behind both the scalar and the vector-valued case is a general exponential-moment inequality (Theorem 6.13) valid for independent, integrable random variables taking values in any separable Banach space :
for independent, mean-zero with and . This is the weakest stable form of the claim: it is stated for a general separable Hilbert space (not a fixed finite dimension), with the tail written as a sum of three explicit terms rather than folded into an unspecified constant, so it survives specialization to any concrete without modification.
Theorem 6.13 (above) is the direct tool Theorem 6.14's own proof invokes ("we will prove the assertion by applying Theorem 6.13"); Theorem 6.12 is the scalar analogue Theorem 6.14 generalizes, included to make the generalization's exact form (three terms, not two) checkable against its source; Corollary 6.15, Hoeffding's inequality in Hilbert spaces, is the immediate mean-free-of-a-variance-bound consequence of Theorem 6.14 obtained by centering, reused directly in the book's own oracle-inequality proof (§6.4).
Theorem 6.14 is the concentration inequality behind the book's later empirical-process arguments for SVMs: whenever an SVM's analysis needs to bound the deviation of an empirical average of Hilbert-space-valued quantities (feature-map evaluations, loss gradients) from its mean, this is the tool invoked, via Corollary 6.15 in the book's own oracle-inequality derivation. Its distinct contribution over simply applying the scalar Theorem 6.12 coordinate-by-coordinate (which is not available without a fixed, finite orthonormal basis, and even then would produce dimension- dependent bounds) is that the bound here is entirely dimension-free: it depends on only through the variance bound and the range bound , not through .
The scalar Bernstein inequality is classical (Bernstein 1924, refined by Bennett 1962 and others
to the sharper multiplicative form used here); its Banach- and Hilbert-space generalizations
(via the martingale-difference / Yurinskii-type argument Theorem 6.13's proof uses) are standard
in the empirical-process-theory literature by the time of this book (see, e.g., Pinelis 1994 for
closely related Banach-space martingale inequalities). No machine-checked Lean proof of the
Hilbert-space form is known to exist on the platform at the time of writing (the platform's own
HighDimProb.Concentration.bernstein_unweighted, from the Vershynin series, is a different,
sub-exponential-norm scalar statement — see Formalization scope); this mission asks for the
book's own bounded-summand, explicit-constant Hilbert-space form.
The natural first attempt generalizes the scalar proof's Markov-inequality argument directly: bound using independence. This breaks immediately because is not linear, so does not factor over the way does in the scalar case — there is no vector-valued analogue of the moment generating function that tensorizes under independence directly. Theorem 6.13's proof resolves this with a martingale-difference decomposition (writing the deviation as a telescoping sum of conditional-expectation differences across the filtration generated by ) rather than a direct product-of-moment-generating-functions argument, at the cost of needing separable (for the conditional expectations and the resulting sums to be well-defined and measurable). Deriving Theorem 6.14 from Theorem 6.13 then requires controlling the two extra terms Theorem 6.13 introduces (the mean-norm term and the per-summand correction) using only the Hilbert-space-specific facts for (from independence and mean-zero) and the scalar bound on — which is exactly where the tail's extra term originates, and is not obtainable by naively reusing the scalar Theorem 6.12's two-term optimization over unchanged.
(and, for Theorem 6.13, ) is an arbitrary separable real (Hilbert, resp. Banach) space —
not fixed to a Euclidean space of any dimension — matching the book's own generality, which is
essential since the theorem's dimension-independence is part of its content. is formalized as the almost-sure bound ∀ᵐ ω ∂P, ‖ξ i ω‖ ≤ B, matching the book's
convention rather than requiring the bound to hold for literally every .
Independence is the mutual independence of the whole family (Mathlib's iIndepFun), matching
Theorem 6.13's proof, which uses independence of from for every
simultaneously, not merely pairwise independence.
A trivializing formalization would state the conclusion in terms of the scalar random variable rather than the vector-valued average's norm — this would collapse the theorem to an easier scalar statement about a nonnegative random variable and lose the whole point of the vector-valued generalization; it is ruled out here by writing the norm of the sum (not a sum of norms) inside the probability. Likewise, dropping the middle term of the tail bound (present here, absent from the scalar Theorem 6.12) would silently understate the genuine dimension-independent cost of vector-valued concentration; all three terms are kept.
Theorem 6.13's general Banach-space statement, and the scalar Theorem 6.12, are reusable beyond
this mission (Theorem 6.13 is the tool any future Banach-space-valued concentration mission in
this series would reach for first). The platform's existing HighDimProb.Concentration. bernstein_unweighted/hoeffding_rademacher (Vershynin series) are not reused as kind: reference items here: they use a sub-Gaussian/sub-exponential-Orlicz-norm parameterization and a
universal (unspecified) constant, a genuinely different hypothesis structure from this chapter's
explicit -bounded, exact-constant form — reusing them would misrepresent this chapter's
own, sharper statement. Completing the four sorrys (Theorems 6.12-6.14, Corollary 6.15) is
welcome; the martingale-difference argument behind Theorem 6.13 is the natural starting point,
since the other three all reduce to it directly.
Support vector machines (SVMs) are trained by solving a regularized empirical risk minimization problem over a reproducing kernel Hilbert space (RKHS) — a space that is typically infinite-dimensional. On its face, this looks computationally hopeless: how can a computer search an infinite-dimensional space for a minimizer? The representer theorem is the result that makes SVM training tractable at all: it shows that no matter how large the RKHS is, the minimizer of the SVM objective for a sample of size always lies in the -dimensional subspace spanned by the kernel evaluated at the sample points. This turns an infinite- dimensional optimization problem into a finite-dimensional one before a single line of an optimization algorithm is written, and it is the reason every practical SVM solver (from the original sequential minimal optimization algorithm onward) searches only over coefficients rather than over an abstract function space.
The theorem in this mission — Theorem 5.5 of Steinwart and Christmann, Support Vector Machines (Springer, 2008) — is stated for general convex losses and general kernels, subsuming the classification-SVM and regression-SVM special cases that appear throughout the machine learning literature. Its lineage traces to Kimeldorf and Wahba's 1971 representer theorem for spline-smoothing problems; the book's own version (attributed to a 1971 result, generalized here to arbitrary convex losses and RKHSs) is the general form used throughout the rest of the book.
Fix a nonempty set (the input space) and a loss function : a measurable map where is the cost of predicting label by value when the input is . is convex if is convex for every fixed .
A reproducing kernel Hilbert space (RKHS) over is a real Hilbert space of real-valued functions on that carries a kernel with two properties: for every , and the reproducing property holds for every and . Intuitively, lets you evaluate any at a point by taking an inner product with the fixed function — this is what makes a space of genuine, pointwise-evaluable functions rather than an abstract Hilbert space.
Given a finite sample , the empirical -risk of is . For a regularization parameter , the SVM training problem asks for a minimizer of the regularized empirical risk
over all of . A minimizer of this objective is called an empirical SVM solution .
The theorem asserts both halves at once: the regularized empirical risk has a unique minimizer over the (possibly infinite-dimensional) , and that unique minimizer is representable as a finite linear combination of the kernel functions at the sample points. Neither the coefficients nor the finite-dimensional subspace they live in are fixed in advance by the statement; only their existence is asserted, so a stronger claim (e.g. uniqueness or an explicit formula for the ) would be a different, harder theorem not proved here.
The book develops the representer theorem's existence-and-uniqueness clause by first proving it for the corresponding population problem — minimizing over a distribution rather than a finite sample — and then adapting the same two arguments to the empirical case:
The representer theorem is the single fact that turns kernel-based learning from a theoretical curiosity into a practical algorithm family: every popular SVM solver (SMO, coordinate descent, interior-point methods for the dual) is, at bottom, a method for finding the coefficients the theorem guarantees exist, not for searching directly. The representation also underlies the "kernel trick": since the objective and the solution both depend on only through inner products , an SVM can be trained and evaluated without ever computing with elements of explicitly, using only the Gram matrix of kernel values.
Formalizing this theorem means formalizing the existence-and-uniqueness argument (Lemma 5.1's strict-convexity computation for the midpoint of two hypothetical minimizers, together with the weak-compactness argument used for existence) and the orthogonal-projection argument for the representation clause (projecting any candidate minimizer onto the finite-dimensional span of the kernel functions at the sample points strictly improves — or leaves unchanged — both the norm term and the risk term, so an optimal solution can always be chosen inside that span). No part of this argument has a machine-checked Lean proof in Mathlib or elsewhere at the time of writing; only the underlying general-purpose tools (Hilbert-space projections, convexity of norms) are already in Mathlib.
The natural first idea for the representation clause is to try to exhibit the coefficients directly, e.g. by writing down the dual optimization problem and reading off its KKT multipliers. This is exactly backwards: the book's proof (and any faithful one) derives the representation before knowing anything about a dual problem, purely from the orthogonal decomposition of into the span of the sample's kernel functions and its orthogonal complement. The key insight — one that a solver who reaches for duality first will miss — is that projecting any onto leaves the empirical risk exactly unchanged (since only sees 's values at the sample points, and the reproducing property shows those values are unaffected by throwing away the component) while weakly decreasing the norm term, so the infimum over all of is already attained inside the finite-dimensional .
For the existence-and-uniqueness clause, the difficulty is genuinely functional-analytic rather than algorithmic: existence needs a compactness argument in a space with no compact balls (Theorem 5.2 gets around this via lower semicontinuity and boundedness of the sublevel set, not via any finite-dimensional trick), and uniqueness needs the parallelogram-law strict convexity of the Hilbert norm, not merely convexity of the loss.
is represented as an arbitrary real Hilbert space together with an injective linear
evaluation map into (so that is genuinely realized as a space of functions,
not an abstract Hilbert space with no relation to ), and a kernel satisfying the
reproducing property with respect to that evaluation map (IsRKHSOfKernel). This is an
equivalent, operative rendering of " is the RKHS of the kernel " (Definition 4.18 together
with Lemma 4.19 of the book), chosen because it is exactly the form the chapter's own proofs use;
it is restated inside this chunk's own InfiniteSample sub-namespace rather than imported from
the Kernels chapter's mission, since drafts in this series cannot import one another.
The population risk is formalized as a lower Lebesgue integral into
(ENNReal), which is always well-defined for a nonnegative integrand with no integrability
hypothesis — matching the book's own remark that "the integral always exists, although it is not
necessarily finite." The empirical risk , by contrast, is a manifestly finite average
over the sample points and is formalized as an ordinary real number. The sample size is
required positive (), matching the book's implicit convention that the empirical measure
presupposes a nonempty sample.
A trivializing formalization of the representer theorem would state only the representation
clause while assuming the existence of "the"
solution as a hypothesis; this begs the question, since the book's own proof
establishes existence and uniqueness as part of the theorem, not as a standing assumption. This
mission's goal keeps both clauses bundled into one ∃! statement for exactly this reason.
The infrastructure needed — a general convex loss, a Nemitski-loss integrability condition, and the RKHS/reproducing-kernel bundle — is restated locally here and is reusable, with the same caveat about not being importable across this series' independently drafted chapters, by any later mission (e.g. this book's own Chapters 6, 8 and 9) that needs the same objects. Contributed proofs are welcome for either the existence/uniqueness argument (Lemma 5.1/Theorem 5.2's techniques) or the orthogonal-projection representation argument; the two are largely independent and could be solved separately.
Many of the orders in Shaked and Shanthikumar's Stochastic Orders (Springer, 2007) are built by fixing a class of test functions and declaring whenever for every in that class: all increasing functions give the usual stochastic order, all convex functions give the convex order. This mission formalizes the order obtained from the single function , — the Laplace transform order — together with its principal alternative characterization and three of its closure properties. Unlike almost every other order in the book, this one has essentially no dependence on material from earlier chapters, which is why it is a natural standalone mission.
Let be a real-valued random variable on a probability space , and let be a real-valued random variable on a (possibly different) probability space . is smaller than in the Laplace transform order, written , if
The order is meant for nonnegative random variables: the book's own standing convention for the whole of §5.A is that every random variable mentioned is nonnegative, since otherwise need not even be finite. Every theorem below carries that hypothesis explicitly rather than folding it into the order's own definition, so the definition itself is stated exactly as broadly as the book's raw equation (5.A.1) is — a comparison of two expectations, for two random variables that need not share a probability space, since is a comparison of distributions.
A second definition supports one of the milestones: a function is completely monotone if all its derivatives exist and for every and every . Every , , is completely monotone, which is what connects the raw definition of to its function-class characterization below.
where and are the survival functions of and . This is the book's principal restatement of the order, obtained from the identity : instead of comparing the raw Laplace transforms of and themselves, it compares the Laplace transforms of their survival functions, weighted the same way. It is the natural goal for a standalone chapter mission: the chapter's own defining equation plus one elementary identity is exactly the book's own proof, and it is the form of the order that the chapter's closure properties are stated against.
The Laplace transform order is the natural comparison for nonnegative quantities that arise as sums or mixtures of exponential-type random variables — waiting times, workloads, service completion times — precisely because it is preserved under convolution (Theorem 5.A.7(d)) and under the broad class of transformations with a completely monotone derivative (Theorem 5.A.7(a)), which includes every concave power , . It sits strictly between the convex-type orders and weaker moment comparisons: Eq. (5.A.5) shows it implies ordered means, but (unlike ) it does not require equal means, and (unlike ) it is not implied by a pointwise comparison of integrated tails alone — it is its own, genuinely different order, useful whenever a modeler's comparison naturally arises through Laplace-transform (equivalently, moment-generating-function-at- negative-argument) calculations rather than through a coupling or a tail-probability argument. Theorem 5.A.3's function-class form is the bridge that lets the order be verified either way: by a single-parameter family of exponential test functions, or by the full class of completely monotone functions of which they are the extreme rays.
The chapter's own first warning applies directly: the order's every characterization requires
, and dropping that hypothesis anywhere — as opposed to carrying it explicitly on each
theorem, per this mission's convention — would silently change which statements are even
well-posed, since can diverge for unbounded below. The quantifier "" in both the raw definition and Theorem 5.A.1 ranges over the whole positive half-line, not a
bounded or discretized set of test points; narrowing it would produce a strictly weaker order. In
CompletelyMonotone, the phrase "all its derivatives exist" is a genuine hypothesis, not a
formality: stating only the sign condition on iteratedDeriv n φ x without also requiring φ to
be C^∞ would let the definition be satisfied vacuously wherever a derivative fails to exist (a
classic junk-value trap), which is why the mission's definition bundles smoothness explicitly.
Theorem 5.A.7(a)'s " positive" is a hypothesis on 's values at the nonnegative reals that
and actually take, not on all of , and must not be silently strengthened to "
everywhere positive" or weakened to " nonnegative" (which would let vanish and break the
order's need for to be well-behaved).
LaplaceOrder μ ν X Y takes on and on a separate , matching the series' convention (e.g.
StochasticOrders.Usual.UsualOrder) that the order compares distributions, not jointly defined
variables. Nonnegativity of and is an explicit hypothesis ∀ ω, 0 ≤ X ω / ∀ ω, 0 ≤ Y ω
on every theorem, never built into LaplaceOrder itself. CompletelyMonotone φ is ContDiff ℝ ⊤ φ ∧ ∀ n x, 0 < x → 0 ≤ (-1)^n * iteratedDeriv n φ x — the smoothness conjunct guards the
junk-value trap described above. The survival function in the goal theorem
is formalized inline as (μ {ω | x < X ω}).toReal, valid since μ is a probability measure (so
the underlying ENNReal value is finite and the conversion to ℝ loses no information); the
integral is Bochner integration over Set.Ici (0 : ℝ). "Provided the expectations
exist" becomes explicit Integrable hypotheses per statement (on , themselves for Eq.
5.A.5; on , for each in Theorem 5.A.3), rather than a
blanket integrability assumption that would understate which expectations the book actually needs.
Independence in the convolution corollary is ProbabilityTheory.iIndepFun, one family per side, as
in Chunk 01's own convolution corollary. A trivializing formalization is ruled out: is
not restated as a comparison of one moment or of the raw random variables' means, and the
"universal function class" of Theorem 5.A.3 is exactly the completely monotone functions the book
names, not a fixed finite subfamily or a narrowed subclass (e.g. only the exponentials themselves,
which would make Theorem 5.A.3 a restatement of the definition rather than its own theorem).
This mission draws on no platform prior art: repeated searches for "Laplace transform" and
"completely monotone" during this session return only unrelated analytic-number-theory
formalizations (a Langlands–Tunnell Laplace–Mellin transform identity) and no hits at all,
respectively — confirming BRIEF.md's expectation that this subarea is untouched on the platform.
It is one of nine missions in a series covering the whole book; per the series' own convention,
its definitions are not imported by any other chapter's mission, and it does not import any other
chapter's definitions in turn (the chapter itself has essentially no cross-chapter dependence, the
reason it was flagged as the series' most self-contained chunk).
Support vector machines were, for two decades, the workhorse of applied classification, and the reason offered for their success was always geometric: SVMs maximize the margin between the two classes. Chapter 3's VC-dimension bound cannot explain why this should help — for linear hypotheses in its bound depends on and is uninformative whenever the feature dimension is large relative to the sample size, exactly the regime (kernel-induced or high-dimensional features) where SVMs are most often used. Chapter 5 answers the question this leaves open: a generalization bound for a real-valued hypothesis, stated in terms of its margin on the training sample, that does not depend on the ambient dimension at all. This is also the template every later chapter's margin bound specializes (multi-class classification, ranking, and, indirectly, boosting all reuse the same Rademacher-complexity-of-a-Lipschitz-loss argument developed here).
A hypothesis here is a real-valued function , not (as in Chapters 2-3) a function into : for a labeled point with , the sign of gives the prediction and is read as the classifier's confidence. The confidence margin of at is ; it is positive exactly when classifies correctly. For , the -margin loss (Definition 5.5) is
equal to when (misclassified), when (classified with confidence at
least ), and interpolating linearly in between; it is -Lipschitz. The
empirical margin loss on a sample with labels
(Definition 5.6) is — the
fraction of training points misclassified or classified with confidence below , a
strictly stronger requirement than plain misclassification. The (population) generalization
error is . Rademacher complexity, and
(Definitions 3.1-3.2, restated here since chunk 03-rademacher-vc's own copies are
still drafts), measure how well a real-valued hypothesis class correlates with random sign
noise on a sample, and are the vehicle through which the margin bound's complexity term is
expressed.
Lemma 5.7 (Talagrand's lemma, milestone). For -Lipschitz and any hypothesis set of real-valued functions,
Theorem 5.10 (Rademacher complexity of bounded-norm linear hypotheses, milestone). For and ,
Corollary 5.11 (margin bound for linear hypotheses, milestone). For the same and , fixing , with probability at least ,
Theorem 5.8 — the mission's goal. For any set of real-valued functions and , with probability at least , both
hold simultaneously for all .
Theorem 5.8 is genuinely dimension-free: unlike Chapter 3's VC-dimension bound (5.36 in the
book, restated from Corollary 3.19), it holds regardless of the ambient feature dimension ,
depending instead only on the hypothesis class's Rademacher complexity and the chosen margin
. Specialized to bounded-norm linear hypotheses (Corollary 5.11), this gives the
theoretical justification most often cited for SVMs and every other margin-maximization
algorithm: whenever the training data admits a large geometric margin, the empirical margin
loss at that margin is small (often zero, in the separable case) and the bound is tight
regardless of . Every later chapter's own margin bound (multi-class in Chapter 9, ranking in
Chapter 10) is a direct structural descendant of Theorem 5.8's proof technique. No prior art on
the Prove2Me platform is faithful: GET /theorems?q=support+vector+machine and q=margin+bound
return no hits on this book's model (the two q=margin+bound hits found, both from the Aether
Catalog, state a different comparison — a VC-type bound is eventually worse than a fixed
Rademacher-type bound as a function of dimension — not Theorem 5.8 itself); q=Talagrand and
q=contraction+principle return several hits (Ledoux/Talagrand convex-distance concentration,
Rudin's Banach-space contraction-mapping theorem, a generic Rademacher-sign contraction lemma
for quadratic sums) but every one states either a different mathematical object (metric-space
fixed points, Talagrand's concentration inequality on product spaces) or a different idiom
(squared vs. linear coordinate sums) from Lemma 5.7's function-composition contraction — none
reused. All nine items are drafted fresh.
Not formalized here: Theorem 5.4 (the SVM sparsity/leave-one-out bound). It is listed as a
candidate milestone in BRIEF.md, but its statement and proof depend on the primal/dual SVM
optimization problem itself (the Lagrangian, KKT conditions, and the resulting definition of a
"support vector" as a training point with nonzero dual coefficient) — a materially different,
non-margin-based proof technique (leave-one-out stability of the trained hypothesis, via Lemma
5.3) that shares no definitions with the margin-bound family this mission's goal and other
milestones are built on. Formalizing it faithfully would require standing up the SVM primal/dual
formalism (Lagrangian, complementary slackness, the "support vector" predicate itself) from
scratch, which is disproportionate to a single additional milestone within this mission's
budget; per the captain brief's guidance to leave out, rather than approximate, a statement that
cannot be made faithful in the time available, it is omitted.
The proof of Theorem 5.8 needs the empirical margin loss's zero-one-loss upper bound () applied before invoking Theorem 3.3's Rademacher generalization bound on the composed class , — reversing this order (bounding by a Rademacher complexity computed on the zero-one loss directly) does not work, because the zero-one loss is not Lipschitz. Talagrand's lemma is exactly what lets the -Lipschitz surrogate be pulled outside the Rademacher complexity, at the cost of a factor and no worse; its own proof is an induction removing one Rademacher variable at a time, using a two-point supremum argument (fixing , choosing near-optimal ) that does not simplify to anything less than genuine care with suprema of non-smooth objects — a formalization attempting to replace this with a naive linearity-of-expectation argument would be proving a false or vacuous statement, since does not commute with linear combinations. Theorem 5.10's bound needs the Cauchy-Schwarz and Jensen inequalities used in the particular order the book uses them (Cauchy-Schwarz on the empirical sup, then Jensen on the expectation of a norm, then the independence of the s) — the bound does not follow from either inequality alone.
EmpiricalRademacherComplexity/RademacherComplexity are restated locally in SVM,
byte-identical to chunk 03-rademacher-vc's own copies (a draft item cannot import another
chunk's draft module); this duplication collapses once 03-rademacher-vc is uploaded and listed
in missions/README.md's "Published definitions" table. MarginGeneralizationError is a new,
real-valued-hypothesis specialization of Definition 2.1 (R(h) = P[y h(x) ≤ 0]), distinct from
every earlier chunk's {-1,+1}-valued GeneralizationError, since no earlier chunk's own copy
matches this chapter's real-valued convention. PhiRho/EmpiricalMarginLoss are new. The goal
theorem (margin_bound_binary_classification) states H's own Rademacher complexity computed
on the marginal X-distribution (D.map Prod.fst), matching the book's final displayed form —
the proof's intermediate step (the lifted class having the
same Rademacher complexity as itself, since ) is not separately drafted, only
the theorem's statement. Theorem 5.10/Corollary 5.11 generalize the book's ambient
to an arbitrary real inner-product space X ([NormedAddCommGroup X] [InnerProductSpace ℝ X]), a harmless generalization since the book's proof (Cauchy-Schwarz,
Jensen, orthogonality of Rademacher signs) uses only the inner-product structure, never finite
dimension; [BorelSpace X] is added to Corollary 5.11's statement to make the measurable
structure under which MarginGeneralizationError is well-posed explicit, since every
x ↦ ⟨w, x⟩ is automatically Borel-measurable — not a substantive restriction, the book never
discusses measurability of linear functionals. No numerical constant in any of the four
theorems is altered from the book's own displayed form. A trivializing formalization this
mission avoids: stating Theorem 5.8 only for a Finset/finite H (which would make it a
disguised instance of Chapter 2's finite-hypothesis bound rather than the chapter's genuinely
new, complexity-based argument) — H : Set (X → ℝ) is left fully general, exactly as the book
states it.
Quantum field theory begins, mathematically, with a question that has a completely precise answer: what is the state space of a single relativistic particle? Non-relativistic quantum mechanics answers and moves on. Relativity does not allow that answer, because the state space must carry an action of the symmetry group of Minkowski spacetime — the Poincaré group — and the choice of Hilbert space is dictated by which such action one wants. The construction that results is the foundation on which Fock space, creation and annihilation operators, free fields and eventually interacting theories are built, and it is where the objects that reappear everywhere in the subject are introduced: the mass shell, the Lorentz-invariant measure on it, and the double cover that is responsible for spin.
This mission formalizes that construction as it is presented in S. Chatterjee's Lectures on Quantum Field Theory (Stanford, 2018–19), Lectures 9–11 and Lecture 25: the one-particle space of a massive scalar boson, the one-particle space of an electron, and the statement that both carry inner products invariant under the Poincaré action.
Minkowski spacetime is with the bilinear form
A Lorentz transformation is a linear map with ; the restricted Lorentz group consists of those with and . The Poincaré group is with the group law .
For a mass , the four-momentum of a particle satisfies and , so it lies on the mass shell
a three-dimensional manifold parametrised by the spatial momentum through with . On there is, up to a multiplicative constant, exactly one measure invariant under ; with the normalisation used in the lectures it is the measure determined by
The state space of a massive scalar boson is , acted on by .
For an electron the wave function takes values in and the group acts through the double cover. To each four-vector one attaches the Hermitian matrix
and for the transformation of is defined by ; the map is a surjective two-to-one homomorphism onto . Writing , each is reached from by a unique positive-definite , the pure boost, and the electron inner product is the -weighted one,
with the group acting by .
For , , and :
for in the weighted space of -valued functions. The goal fixes no constants beyond the normalisation of , and it is the statement that the spaces defined in the mission really are the one-particle spaces of the theory: a Hilbert space together with a Poincaré action by isometries.
The milestone list follows the lectures: the parametrisation of ; invariance of under ; the integration formula for (eq. (10.1)); invariance of ; uniqueness of the invariant measure up to a constant; the composition law and unitarity of the scalar representation; and bijectivity of onto Hermitian matrices; as a multiplicative map into ; surjectivity of with fibres ; existence and uniqueness of the pure boost ; Lemma 25.1; and the identification of the weighted electron space with the plain -valued space via .
The objects here are used unchanged for the rest of a QFT course: the bosonic and fermionic Fock spaces are built on these one-particle spaces, and the free scalar and Dirac fields are operator-valued distributions written as integrals against on . Formalizing them fixes, once and for all, the conventions later work must match — the normalisation of , the sign convention of the metric, which of the two elements of acts, and the weight in the electron inner product.
What this mission adds beyond the lectures is a machine-checked development of material usually treated as routine but rarely written out: the uniqueness of the invariant measure, the covering map and its fibres, and the existence-uniqueness of the pure boost are all stated in the source either without proof or as exercises. Mathlib has the general theory of spaces, push-forward measures, Hermitian and positive-definite matrices, and , but it has no mass shell, no invariant measure on it, and no covering map onto the restricted Lorentz group; all of that is constructed here and is reusable by any later mission on free fields or Fock spaces.
The obvious route to the invariant measure — "restrict Lebesgue measure to the submanifold " — does not work: the induced Riemannian volume of the hyperboloid in the Euclidean metric is not Lorentz invariant. The lectures instead take a scaling limit of Lebesgue measure on the invariant annuli ; the formalization takes the resulting formula (10.1) as the definition and must then prove invariance, which amounts to a change-of-variables computation whose Jacobian is exactly -dependent. Uniqueness is harder: it is a statement about invariant measures on a homogeneous space of a non-compact group, with no finiteness available.
On the spinor side, the central difficulty is that the weight is unbounded on , so the electron space is not the naive -valued — the two spaces consist of different functions, and are related only through the measurable field of isomorphisms . A formalization that silently uses the unweighted space would prove a different, and false, unitarity statement.
Four-vectors are functions , with the metric signature ; Lorentz transformations are real matrices, and membership in is the predicate (, , form preserved). is a Borel measure on all of carried by , defined as the push-forward of ; the boson space is the library space of that measure. The pure boost is given by the closed formula — the positive-definite square root of — rather than by a choice function, and a milestone certifies that it is the unique positive-definite element of carrying to . The electron space is the set of -valued measurable functions of finite weighted norm, with the weighted pairing given explicitly; the milestone identifying it with the plain space via the inverse boost is what supplies its Hilbert-space structure.
The unitarity statements are formalized as equalities of integrals over pairs of wave functions rather than as statements about abstract operators, so that no trivializing reading is available: in particular the electron clause is stated for the weighted pairing, which is not the standard inner product, and the hypotheses (, , in the respective spaces) are satisfiable, so no clause holds vacuously. Total-function conventions of the library (inverse of a singular matrix is ; integral of a non-integrable function is ) are visible in the statements and are recorded in each item's read-back.
Contributions of any of the milestones are welcome; the measure-theoretic milestones (invariance and uniqueness) and the covering milestones are independent of each other and can be attacked in parallel.
Many statistical estimators are defined by minimizing an empirical average over a class of candidate models — empirical risk minimization, maximum likelihood, and binary classification all fit this template. Analyzing such an estimator's excess risk reduces, in each case, to controlling how far the empirical average of a whole class of functions can deviate from its population expectation, not just a single fixed function — a much stronger requirement than the ordinary law of large numbers, which only controls one function at a time. This mission formalizes the central non-asymptotic tool for this problem, the Rademacher complexity-based uniform law, following Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 4.
Let be a class of real-valued functions with a common domain, indexed as , and let be i.i.d. samples from a distribution . The empirical process deviation (Eq. (4.7)) is
Given an independent Rademacher sequence (each equiprobably), the symmetrized process (Eq. (4.19)) and the Rademacher complexity (Eq. (4.13)) of are
A class is -uniformly bounded if for every .
For any -uniformly bounded class , any , and any ,
with -probability at least .
For any convex non-decreasing , , where is the recentered class. This generalizes the specific symmetrization step used in Theorem 4.10's own proof (the case ) to an entire family of moment comparisons.
For a -uniformly bounded, i.i.d.-sampled class , with -probability at least , obtained via the bounded-differences method. Combined with Proposition 4.11's bound on by , this is exactly Theorem 4.10's proof.
Theorem 4.10 is the general-purpose engine behind the classical Glivenko–Cantelli theorem (recovered by taking to be the class of half-line indicator functions, Example 4.6) and behind uniform convergence guarantees for empirical risk minimization more broadly (Section 4.1.2): whenever a task can be reduced to bounding the Rademacher complexity of a specific function class — a purely combinatorial/geometric quantity independent of any particular statistical model — Theorem 4.10 converts that bound directly into a high-probability uniform convergence guarantee. Proposition 4.11 is separately significant as the general symmetrization principle from which Theorem 4.10's specific bound, and many similar bounds throughout empirical process theory, are instances.
Formalizing it. No faithful prior art exists on the platform: a fresh search for "uniform
law," "symmetrization," "Rademacher complexity," "Glivenko-Cantelli," and "empirical process"
found only unrelated hits and the existing RademacherSymmetrization.*/RademacherMassart.*
items, which are specific to finite function classes (Finset (X → ℝ)) — a strictly narrower
setting than Theorem 4.10's fully general (possibly infinite) function classes, and not reused
here. All three theorems are drafted as open goals (:= by sorry).
The naive approach to bounding — apply a scalar concentration bound to each individually and union-bound over — fails outright when is infinite (there is no union bound to take). The two-step resolution captured by this mission's milestones avoids this entirely: first, itself, viewed as a single function of the samples, is shown to concentrate sharply around its own mean via the bounded-differences method (no union bound over needed — the argument treats as one Lipschitz function of the samples). Second, the mean itself, a single deterministic number, is bounded via symmetrization: introducing an independent "ghost sample" with the same law as converts the un-symmetric quantity into the manifestly symmetric , and it is only after this symmetrization that the supremum over becomes tractable via the geometry of (its Rademacher complexity) rather than requiring finite.
The function class is realized as the range of an index family
rather than a Set (D → ℝ), matching the standard representation of a (possibly infinite)
function class by an index type; ι carries no finiteness assumption, matching the book's own
full generality (in contrast to the platform's existing RademacherSymmetrization/
RademacherMassart items, which are finite-class-specific). The population expectation
is realized via an explicit population variable sharing the samples'
common law, rather than a separately axiomatized abstract distribution object. The Rademacher
sequence and the samples are packaged into one jointly independent family Z : ℕ → Ω → D × ℝ
with an explicit hypothesis that the two coordinates are themselves independent at each index —
capturing " independent of , both i.i.d." exactly, without a bespoke
joint-independence predicate.
Theorem 4.10's own qualitative corollary ("consequently,
whenever ") is not included in the goal's conclusion: it concerns an infinite
sequence of samples and asymptotic convergence via the Borel–Cantelli lemma, a substantially
different formal object (requiring Filter.Tendsto over ℕ→∞ and ∀ᵐ almost-sure convergence)
from the single- non-asymptotic tail bound (4.14) this mission's goal states, and is left as
natural follow-on work, alongside a direct formalization of the classical Glivenko–Cantelli
theorem (Theorem 4.4) as a corollary.
Lemma 4.14 (the polynomial-discrimination route to bounding Rademacher complexity for VC-type classes) is out of scope for this mission: its displayed inequality is extracted with heavily garbled math layout from the source PDF (a known, disclosed limitation of this book's text extraction at that specific page), and confirming it character-for-character against the rendered page image was judged out of budget for this chunk relative to Proposition 4.11 and Eq. (4.16), both of which are directly load-bearing in Theorem 4.10's own proof and extracted cleanly.
Chapter I's usual stochastic order compares "how large" two random variables tend to be. A different, equally common question in operations research is "how spread out" a random variable is: two portfolios with the same expected loss can differ sharply in how much that loss varies, and a risk-averse decision maker or a convex cost function cares about exactly that difference. Shaked and Shanthikumar's Stochastic Orders (Springer, 2007) formalizes this comparison as the convex order, the book's mean-preserving-spread order (known outside OR and probability circles as the Rothschild–Stiglitz order from economics). This mission formalizes the order and its central structural result: Strassen's martingale-coupling characterization.
Let be a real-valued random variable on a probability space , and let be a real-valued random variable on a (possibly different) probability space . is smaller than in the convex order, written , if
Convex functions take their relatively largest values on the "extreme" regions outside some interval, so says is more likely than to take extreme values: is "more variable" than . Unlike the usual stochastic order, forces the two means to agree (, taking , both convex) — the convex order compares spread holding location fixed, exactly the mean-preserving-spread reading. Two equivalent forms make it tractable: comparing tail integrals of the survival/distribution functions (Theorem 3.A.1), and comparing mean absolute deviations from every point (Theorem 3.A.2).
Furthermore, can be chosen so that the conditional law stochastically increases with (in ). This is the convex-order analogue of Chapter I's Theorem 1.A.1: instead of one variable dominating the other pathwise, 's copy is a fair (martingale) randomization of 's copy whose spread only grows in the conditioning value. The book itself calls the constructive direction "not easy to prove"; this mission states the theorem faithfully, including the "Furthermore" strengthening, without attempting a proof.
The convex order is the standard way operations research and actuarial science formalize "more variable, same average": comparing the riskiness of two portfolios with matched expected return, the effect of aggregation or diversification on total claim size, or the value of information in a stochastic program (where a random variable degenerates to its mean exactly when the decision maker learns everything, the two extremes of a convex-order chain). Strassen's characterization is what turns "compare against every convex function" — an intractable universal quantifier — into a single explicit construction: exhibit one martingale coupling and the comparison is settled for every convex function at once, by Jensen's inequality. This is the technique behind bounding the effect of information or risk aggregation without checking convexity function by function, and the "Furthermore" monotonicity clause is what makes the coupling itself informative about how the spread grows with the conditioning variable, not merely that some fair coupling exists.
Formalizing this theorem fixes, for the whole book series, the exact shape every later coupling theorem for a variability-type order (the increasing convex/concave orders of Chapter IV via a submartingale, the multivariate convex order of Chapter VII) is expected to restate. No proof is attempted; the book's own remark that the constructive direction is "not easy" marks it as a genuine target for a future proof-bearing pass, not a formality.
The definitional trap mirrors Chapter I's: "for every convex " must be a genuine
universal quantifier over Mathlib's own convexity predicate, with the existence of both
expectations stated as an explicit integrability hypothesis inside the quantifier, not assumed
globally or dropped. The coupling theorem doubles the difficulty of Theorem 1.A.1's: the
conditional-expectation condition a.s. is with respect to the
-algebra generated by , not an informal "expected value given ", and must
use the martingale API's own convention (Mathlib's condExp) precisely. The "Furthermore" clause
compounds this: it is a claim about the regular conditional distribution of given
for every point , not merely the conditional expectation, and dropping it silently
(as a "remark" rather than part of the theorem) would understate what Theorem 3.A.4 actually
claims — the chapter brief flags this explicitly as a trap, and it is kept as a conjunct of the
same existential witness here.
Random variables are again measurable functions into from arbitrary measurable
spaces, ConvexOrder μ ν X Y taking on and on a separate ,
matching Chapter I's convention and this series' own pattern. Convexity is Mathlib's ConvexOn ℝ Set.univ φ; "equality in law" is again ProbabilityTheory.IdentDistrib. The martingale condition
uses Mathlib's conditional-expectation notation ρ[Ŷ | m] =ᵐ[ρ] X̂ with m the -algebra
MeasurableSpace.comap X̂ inferInstance generated by X̂ — the martingale API's own convention,
not a hand-rolled gloss. The "Furthermore" clause uses Mathlib's ProbabilityTheory.condDistrib,
the regular conditional distribution kernel of Ŷ given X̂ (available since ℝ is a standard
Borel space), and states "increasing in x in ≤st" via the kernel's survival function being
monotone in x at every threshold — restating, locally to this chapter's namespace, the same
tail-probability shape Chapter I's UsualOrder uses (drafts cannot import another mission's
definitions, per this series' convention). A trivializing formalization is ruled out explicitly:
the martingale and monotonicity conjuncts are both kept as genuine content of the existential
witness in the goal theorem, not weakened to a bare coupling or dropped as an optional remark.
This mission draws on no platform prior art (searches for "convex order", "Strassen",
"martingale", "Jensen" returned only unrelated geometry/algorithm/physics results as of
2026-09-18); Mathlib's Probability/Martingale/* supplies the conditional-expectation and kernel
machinery the coupling condition and its "Furthermore" clause are built from, but no platform
theorem states the convex order or its coupling characterization itself. Reusable beyond this
mission: the condExp/condDistrib-based martingale-coupling pattern is the shape Chapter IV's
analogous submartingale coupling (Theorem 4.A.5) and Chapter VII's multivariate convex order
(Theorem 7.A.1) are each expected to restate independently.
A device's mean residual life at age — its conditional expected remaining lifetime given that it has survived to — is one of the oldest and most interpretable summaries in reliability and survival analysis: it is what an insurer, a maintenance planner, or a hospital outcomes researcher actually wants to know about a unit still in service. Comparing two mean residual life functions pointwise gives the mean residual life order , a natural "the survivor of is worn less, on average, than the survivor of " comparison that is weaker than the usual stochastic order but not directly comparable to it (the book states plainly that neither implies the other in general). This mission formalizes the order's definition and its precise relationship to the stronger hazard rate order : under an extra monotone-ratio condition the two orders coincide, and one direction of that coincidence always holds. A third milestone gives one of the chapter's closure properties, showing that "decreasing mean residual life" (DMRL) — an aging notion used throughout reliability theory to describe units that wear out, rather than improve, with age — is preserved under adding independent noise.
Fix a probability space and a real-valued random variable with survival function and finite mean. The mean residual life function of at is
For a second random variable on with mrl function , is smaller than in the mean residual life order, , if for every . The hazard rate order, restated in this mission's own namespace (Chapter 1's version cannot be imported — see Formalization scope), is the general, absolute-continuity-free comparison for all , where is 's survival function. A random variable is DMRL (decreasing mean residual life) if its mrl function is decreasing in .
Combined with the companion milestone below, this is a genuine conditional equivalence: under the monotone-ratio hypothesis, and coincide, and in particular under that condition. Without the hypothesis, the book states explicitly (the paragraph immediately preceding Theorem 2.A.1) that neither nor implies the other.
Each milestone is stated exactly as the book states it: no constant is hard-coded, no or asymptotic approximation is involved, and the goal's monotone-ratio hypothesis is the genuine ratio , not two separately-monotone functions (a different, unrelated condition the book itself does not state).
The mean residual life order sits at a specific point in the book's own hierarchy of orders: strictly implied by the hazard rate order (Theorem 2.A.1), and — the goal theorem — reversible into the hazard rate order under one extra monotonicity hypothesis on the ratio of the two mrl functions. This "sandwich" structure is exactly the kind of comparison-of-orders result that makes Chapter 1's usual and hazard rate orders (already formalized in Chunk 01 of this series, restated locally here since drafts cannot import each other) into a genuinely connected theory rather than a list of unrelated definitions. The DMRL closure property (Theorem 2.A.11) is separately significant: DMRL is one of the book's standard "aging" notions, used in reliability engineering to model components that wear out over time, and its preservation under adding independent noise is a basic tool for building compound reliability models (e.g. a component with an added, uncorrelated failure mode) from simpler DMRL parts.
No prior art exists on the platform for either order: GET /theorems?q=mean+residual+life
returns zero hits, and GET /theorems?q=hazard+rate returns exactly one hit
(DQJSQ.theorem2_ifr), an unrelated queueing-theory IFR (increasing failure rate) lemma about
patience densities in a fluid queueing model, not this order — it names a different object under
a coincidentally similar keyword and is not reused. This mission is a foundational island for the
mean residual life order.
The mrl function is a genuinely two-case object: a real conditional expectation on , and a hard outside that region. The goal theorem's proof (not formalized here; only the statement is a milestone) differentiates and , uses the identity relating the mrl function to the hazard rate, and compares the two resulting hazard-rate expressions using the ratio's monotonicity — a genuinely analytic argument, not a routine unfolding of definitions. The chief formalization difficulty is keeping the shape of (a pointwise comparison of a derived function) visibly distinct from the function-class shape of used in Chapter 1, since the book explicitly warns that conflating the two orders is a live error (neither implies the other in general) — see Formalization scope below for how each shape is kept separate.
All three random variables in this mission's milestones are real-valued measurable functions on
a MeasureTheory.Measure space, matching this series' Chapter 1 convention (Chunk 01). The mrl
function mrl μ X t is defined as if 0 < P{X>t} then (∫ ω in {X>t}, (X ω - t) ∂μ) / P{X>t} else 0, formalizing the case split on directly via positivity of the survival probability
(its defining equivalent under the survival function's monotonicity) rather than through the
derived quantity itself. MrlOrder μ ν X Y is ∀ t : ℝ, mrl μ X t ≤ mrl ν Y t — a direct
pointwise comparison of two functions, deliberately kept a different shape from Chapter 1's
UsualOrder (a ∀ φ ∈ 𝒞, E[φ∘X] ≤ E[φ∘Y] function-class quantifier), since the book's own
warning that and neither implies the other is a warning against treating
them as interchangeable comparison shapes.
The hazard rate order is restated locally in this chapter's own namespace
(StochasticOrders.MeanResidualLife.HazardRateOrder) rather than imported from Chunk 01's
StochasticOrders.Usual.HazardRateOrder, because each chapter's mission is drafted and reviewed
as an independent Prove2Me proposal and one draft cannot import another draft's unpublished Lean;
its definition is identical in shape to Chunk 01's own restatement of the general,
absolute-continuity-free survival-function form of (not the density-ratio form, which
requires absolute continuity the book does not assume at this level of generality).
Every milestone that consumes mrl carries explicit Integrable hypotheses on the random
variables involved (Integrable X μ, and Integrable Y ν or Integrable Z μ as applicable),
formalizing the book's own standing "finite mean" hypothesis from §2.A.1's definition of the mrl
function: without it, the Bochner integral inside mrl would return its junk value 0 for a
non-integrable variable on some tail set, letting a hypothesis like MrlOrder μ ν X Y hold of a
function that is not actually the book's mean residual life function. DMRL μ X is
Antitone (mrl μ X), the book's own " is decreasing in " in the weak, non-strict
monotone sense used throughout the book for "increasing"/"decreasing".
A trivializing formalization this mission rules out: stating the goal theorem with the ratio
hypothesis as two separate monotonicity conditions on and individually (rather than
genuine monotonicity of the ratio on the region where ) would be a different,
strictly stronger and easier-to-satisfy hypothesis than the book's own — the milestone here states
MonotoneOn (fun t => mrl μ X t / mrl ν Y t) {t | 0 < mrl ν Y t}, the genuine ratio restricted to
where the denominator does not vanish, matching Theorem 2.A.2's own " increases in
" verbatim.
StochasticOrders.Usual), for the usual and hazard rate orders this
chapter's own restated definitions parallel.Chapter 2's finite-hypothesis-set learning bound is uninformative the moment is infinite — diverges — yet most hypothesis sets used in practice (linear separators, neural networks, decision trees) are infinite. Chapter 3 answers the question the previous chapter's own worked example (axis-aligned rectangles, Example 2.4) leaves open: is efficient learning from a finite sample still possible for an infinite hypothesis set, and can this be shown in general rather than case by case? The chapter's answer runs through two complementary notions of complexity — Rademacher complexity, a data-dependent measure of how well a function family correlates with random noise, and the VC-dimension, a purely combinatorial measure of the number of distinct labelings a hypothesis set can realize on a finite point set — connected by Massart's lemma and Sauer's lemma, and culminating in a generalization bound that replaces with the VC-dimension .
For a family of functions and a sample , the empirical Rademacher complexity (Definition 3.1) measures how well fits random sign noise on ; the Rademacher complexity (Definition 3.2) averages this over samples. Theorem 3.3 converts a Rademacher-complexity bound directly into a generalization bound via McDiarmid's inequality. For binary hypothesis sets , the growth function (Definition 3.6) counts the maximum number of distinct dichotomies realizes on points, and the VC-dimension (Definition 3.10) is the largest for which (i.e. shatters some set of points). Massart's lemma (Theorem 3.7) is the purely combinatorial tool bounding the expected maximum of a sum of signed vector components by , and Sauer's lemma (Theorem 3.17) bounds the growth function itself, by induction on , whenever the VC-dimension is finite.
Theorem 3.3 (Rademacher generalization bound, milestone). For and any , with probability at least over an i.i.d. sample of size , for all : .
Theorem 3.7 (Massart's lemma, milestone). For a finite with : .
Theorem 3.17 (Sauer's lemma, milestone). For with , for all : .
Corollary 3.19 — the mission's goal. For with and any , with probability at least , for all :
Corollary 3.19 is the chapter's answer to the question chapter 2 leaves open: it is Theorem
2.13's direct infinite-hypothesis-set generalization, replacing (undefined for
infinite ) with the VC-dimension (finite even for many infinite hypothesis sets, such
as halfspaces in , which have VC-dimension ). It is also the template every
later margin bound in the book specializes (Chapters 5, 9, 10's SVM, multi-class and ranking
margin bounds all replace this bound's uniform /VC-dimension term with a
scale-sensitive complexity measure derived from the same Rademacher-complexity machinery), and
Sauer's lemma is independently one of the most cited results in learning theory and extremal
combinatorics. No prior art on the Prove2Me platform is faithful to any of this chapter's
content: RademacherSymmetrization.radS_chernoff (Aether Catalog) proves a different,
Massart-optimized Chernoff bound for the empirical Rademacher complexity of a finite class —
a different object (empirical vs. population) with a different bound form from Theorem 3.3/3.5
— and sauerShelah_full proves only the trivial identity sauerShelahBound k k = 2^k, not
Sauer's lemma itself. A further hit, sauer_shelah (Aether Catalog, Algebra/SauerShelah.lean),
does state the Sauer-Shelah bound itself (F.card ≤ ∑_{i≤d} C(n,i) for a family F of subsets
of Fin n shattering no set larger than d) — checked and not reused: it is a different idiom
from Theorem 3.17 as this chunk needs it, a fixed finite ambient domain Fin n with F a
Finset of its subsets directly, rather than the book's own growth function Π_H(m) (a
supremum over point-tuples drawn from an arbitrary, possibly infinite X, Definition 3.6) that
this chunk's other items and the goal (Corollary 3.19) are built on; reusing it would require
either abandoning GrowthFunction/HasVCDim (needed faithfully by the goal itself) or a
nontrivial reduction lemma this mission's budget does not include, so sauer_lemma is drafted
fresh against this chunk's own GrowthFunction/HasVCDim. All ten items are drafted fresh.
Sauer's lemma's proof is a genuine two-parameter induction (on ) with a real combinatorial
construction: restricting to a sample of size , then splitting the restricted
family into (its restriction to the first points) and (the concepts whose
membership in changes with the addition of the -th point), with and
— a genuinely combinatorial argument, not a
statement that unfolds by simp; a weaker restatement using only the trivial bound
would be true but is explicitly not what Theorem 3.17 states (BRIEF.md's
named trivializing formalization for this chapter). Massart's lemma needs the expectation of a
supremum over a finite set of -many sign patterns kept as an honest average, not silently
replaced by a looser union bound. Corollary 3.19's own term inside the logarithm needs
the side condition carried through explicitly — Corollary 3.18's own domain restricts
to , and the bound is false, not merely unproved, without it (at , can be
smaller than , making the logarithm negative).
GeneralizationError/EmpiricalError are restated locally in this chunk's RademacherVC
namespace (byte-identical in content to chunk 02-pac's own copies), since a draft item cannot
import another chunk's draft module; this duplication is expected and will collapse once
02-pac is moderated, uploaded and listed as reusable in missions/README.md's "Published
definitions" table. EmpiricalRademacherComplexity/Massart's lemma model the Rademacher signs
σ as ranging over the finite type Fin m → Bool rather than a measure-theoretic i.i.d.
process, so the "expectation over σ" in both is the exact finite uniform average over its
2^m outcomes — faithful and simpler than a MeasureTheory construction, since σ's
distribution really is uniform on a finite set of outcomes for every finite m. GrowthFunction
takes a tuple of m points (Fin m → X) rather than a size-m subset of X, a harmless
generalization (repeated points never increase the dichotomy count) documented in the item's own
docstring. HasVCDim is a Prop parametrized by the candidate dimension rather than a total
ℕ/ℕ∞-valued function, so it does not cover the book's VCdim(H)=+\infty case (Examples
3.15-3.16); every theorem using it takes HasVCDim H d as an explicit hypothesis, matching the
book's own "let H... with VCdim(H)=d." Theorem 3.3 adds an explicit measurability
hypothesis on G (hGm) beyond the book's own displayed statement, needed to keep the Bochner
integral ∫ z, g z ∂D from silently evaluating to 0 for a non-measurable g — this is the
book's own standing assumption (footnote 3, p. 30) made an explicit hypothesis rather than an
implicit one. No numerical constant in any of the four theorems is altered from the book's own;
Corollary 3.19's side condition d ≤ m is kept explicit, per BRIEF.md's pitfall note.
Not formalized: Lemma 3.4 and Theorem 3.5 (the binary-classification specialization of Theorem
3.3 via the zero-one-loss identity ), Corollary 3.8 and
Corollary 3.9 (the intermediate Rademacher-to-growth-function and growth-function
generalization bounds), and Corollary 3.18 (the VC-dimension bound on the growth function,
for ) — five intermediate results in the proof chain
Theorem 3.3 → Theorem 3.5 → Corollary 3.8/3.9 → Sauer's lemma → Corollary 3.18 → Corollary 3.19
that are not independently drafted as milestones, per the budget guidance to keep a chunk to a
goal plus its most load-bearing 3-8 milestones rather than every numbered result on the page;
the three drafted milestones (Theorem 3.3, Massart's lemma, Sauer's lemma) are the chain's three
genuinely distinct proof techniques (McDiarmid's inequality, a probabilistic-maximum bound, and
a combinatorial induction), and the goal theorem's own statement is Corollary 3.19 exactly as
displayed, not a restatement of any intermediate corollary. Radon's theorem (Theorem 3.13,
background for the hyperplane VC-dimension example) and the worked VC-dimension examples
(intervals, hyperplanes, rectangles, convex polygons, sine functions) are illustrations, not
general results, and are not formalized — drafting only the example computations (e.g.
VCdim(hyperplanes) = d+1) instead of the general finite-H machinery is exactly the
trivializing formalization this mission avoids.
How many labeled examples does a learning algorithm need to see before its output generalizes well to unseen data? Chapter 2 of Foundations of Machine Learning answers this question for the simplest nontrivial setting — a finite hypothesis set — and in doing so introduces the book's central object, the Probably Approximately Correct (PAC) learning framework: a distribution-free, high-probability guarantee relating a learner's sample size to the accuracy and confidence of its output. Every later chapter's generalization bound (VC-based, Rademacher-based, margin-based) is a variant of the same "probability of a bad event is small" argument this chapter proves in its most elementary form, so getting the chapter's core definitions and its two bracketing theorems (consistent and inconsistent finite-) right is the foundation the rest of the book's guarantees build on.
A learner sees a sample drawn i.i.d. from a fixed but unknown distribution on an instance space , labeled by an unknown target concept drawn from a concept class ; a hypothesis from a fixed hypothesis set is judged by its generalization error (Definition 2.1) against its empirical error (Definition 2.2) on the observed sample. A concept class is PAC-learnable (Definition 2.3) if some algorithm, given a polynomially-bounded number of samples, returns a hypothesis whose generalization error is at most with probability at least , for every accuracy and confidence and every distribution — the "distribution-free" and "for all target concepts" character of the definition is what makes it a genuine worst-case learning guarantee rather than an average-case one tailored to a particular data-generating process.
Theorem 2.5 (consistent case, milestone). If is finite and algorithm always returns a hypothesis consistent with the target concept on the training sample (), then whenever .
Corollary 2.11 (single-hypothesis Hoeffding bound, milestone). For a fixed hypothesis and any , with probability at least , .
Theorem 2.13 (inconsistent case, goal). For a finite hypothesis set and any , with probability at least , simultaneously for every ,
Theorem 2.13 is the chapter's capstone because it removes Theorem 2.5's consistency
requirement — the typical case in practice, where no hypothesis in perfectly fits the
training data — while paying only an additive price inside the square root, via a
union bound over applied to Corollary 2.11's per-hypothesis concentration bound. It is also
the template every later generalization bound in the book refines: Chapter 3 replaces
with the growth function / VC-dimension to handle infinite hypothesis sets, and Chapter 3's
Rademacher-complexity bound is the direct machine-independent generalization of the same
argument. No prior art on the Prove2Me platform is faithful to this chapter's PAC-learning
content (GET /theorems?q=PAC-learnable returns no hits), so all six items are drafted fresh.
Theorem 2.13's own proof is a short combination of two ideas already present in the chapter (Corollary 2.11's Hoeffding bound plus a union bound over hypotheses), but each ingredient carries its own faithfulness burden. Corollary 2.11 needs the sample and the target hypothesis kept in the right relationship — fixed, random — for the bound to be Hoeffding's inequality and not a vacuous statement about a random hypothesis. Theorem 2.13 needs the quantifier placed inside the probability event (a single sample must work for every at once), not outside it (which would only assert each 's bound holds with high probability for a sample chosen depending on ) — the difference between a uniform convergence bound and separate, weaker statements. Definition 2.3's "polynomial function " is a genuine formalization judgment call, addressed below.
GeneralizationError/EmpiricalError are typed generally over (matching Definition
2.1/2.2's own general statement, ""), since Theorem 2.5 itself is stated for general
, not just ; Corollary 2.11 and Theorem 2.13 specialize to
, matching their own explicit "" (Corollary 2.11) and the
surrounding inconsistent-case section's restriction to binary classification. The i.i.d. sample
is modeled as the identity random variable on the product-measure space
in both Corollary 2.11 and
Theorem 2.13, matching the book's own notation exactly. IsPACLearnable
(Definition 2.3) makes "polynomial function" precise as a function bounded above by
for some constants , , uniform in its (nonnegative)
arguments — the standard reading of "polynomial in its arguments" in the absence of a
ready-made multivariate polynomial-growth predicate in Mathlib; dropping this constraint
entirely (stating only "there is some threshold function") would silently weaken Definition
2.3 to a strictly easier notion of learnability, since virtually any finite or well-behaved
concept class admits some (possibly super-polynomial) sample-complexity threshold — this is
exactly the distinction Example 2.7 (the universal concept class) uses to demonstrate a class
that is not PAC-learnable despite admitting a consistent hypothesis set. No numerical
constant in Theorem 2.5, Corollary 2.11 or Theorem 2.13 is altered from the book's own; no
upper bound on is added anywhere the book itself leaves it unrestricted (the theorems
remain true, if vacuous, for ). Not formalized: the "efficiently PAC-learnable"
running-time clause of Definition 2.3 (a second, independent polynomial-time condition on
not needed by either milestone or the goal); Corollary 2.10 (the raw two-sided Hoeffding
statement Corollary 2.11 is immediately derived from by solving for , making it
redundant with Corollary 2.11 as a formalization target); the axis-aligned-rectangles worked
example (Example 2.4–2.9), which illustrates the framework rather than proving a new general
result, and the trivializing formalization this chapter invites — reusing Mathlib's rectangle
machinery to encode only the specific two-dimensional geometric argument rather than the
general finite- theorems — is exactly what this mission avoids by drafting Theorems 2.5 and
2.13 in their general, hypothesis-set-agnostic form.
Composite convex programs — objectives split into a smooth piece and a nonsmooth piece — are ubiquitous in data analysis: LASSO-type inverse problems, regularized empirical-risk minimization, and total-variation-type image reconstruction all minimize over a convex set, where is smooth (a data-fidelity term, often expensive to differentiate — a large matrix-vector product, a PDE solve, a black-box simulation), is nonsmooth but structurally cheap (an -type penalty, a simple subgradient), and enforces a "relatively simple" constraint absorbed into the proximal step. Classical accelerated proximal-gradient methods (Nesterov; Beck–Teboulle) solve such problems by computing and a subgradient once per iteration, giving an optimal bound on evaluations of both. But in every example above, the two oracle calls have wildly different costs, and paying for as often as for is wasteful. Ghadimi, Lan and Zhang (SIAM J. Optim., 2014, arXiv:1406.5613, "Generalized Uniformly Optimal Methods for Nonlinear Programming") posed the resulting question: given separate first-order access to and , can the number of -evaluations be reduced without inflating the (already-optimal) number of -evaluations? The gradient sliding (GS) algorithm formalized here, from Lan's textbook treatment (Chapter 8, building on Lan's own 2016 Mathematical Programming paper "Gradient sliding for composite optimization"), answers this in the affirmative: it "slides" past -evaluations on most iterations while still achieving the optimal subgradient count for .
Fix a real inner-product space and a closed convex set . The composite problem is
where is a "relatively simple" convex function (its own proximal step is assumed cheap), is convex with -Lipschitz gradient,
and is convex and -Lipschitz-like in the sense that for every subgradient ,
Let be a Bregman-type prox-function built from a 1-strongly-convex distance-generating function (Sect. 3.2), so .
The gradient sliding (GS) algorithm (Algorithm 8.1) keeps an outer iterate , model point , and running average (). Each outer step delegates to the prox-sliding (PS) procedure: given the affine model , prox-center , parameter , and sliding length , PS runs inner iterations
where (8.1.14), without ever recomputing during these steps — the single affine model is reused throughout. This is the mechanism by which GS "slides" past most -evaluations. PS returns , and the outer loop updates .
where and satisfy the recursion (8.1.20). This is the per-inner-iteration guarantee on how close comes to solving 's own minimization.
Assuming the PS schedule (8.1.20) and GS schedule conditions (8.1.25), (8.1.33) (the case where may be unbounded),
a general bound in terms of the abstract schedule, obtained by telescoping Proposition 8.1's guarantee (via Proposition 8.2's per-outer-step recursion, cited but not restated here) across outer iterations.
With the concrete schedule , (8.1.39), and, for a fixed horizon and free parameter ,
This is the explicit-constant complexity bound: it is the weakest statement stable under changing , obtained purely algebraically from Theorem 8.1(a)'s general bound once the schedule is plugged in.
Corollary 8.1(a), together with the schedule of , shows the total number of outer
iterations — and hence -evaluations — needed for an -solution is , matching the optimal rate for smooth-only minimization (no penalty for the
nonsmooth term's presence), while the total number of inner iterations — and hence
-evaluations — remains , the rate that is already known to be unimprovable
for nonsmooth convex minimization. GS is thus the first method (per the section's own account) to
decouple the two oracle costs at their respective optimal rates, rather than paying the worse of
the two for both. This underlies later chapters' extensions (accelerated gradient sliding,
decentralized optimization over networks) and is directly applicable whenever a composite
objective's two components have asymmetric evaluation cost, as in the LASSO-type and
regularized-loss examples above. Formalizing it contributes a machine-checked account of the
telescoping/recursion argument across two nested loops (outer GS, inner PS) — a pattern distinct
from the single-loop accelerated-gradient arguments already in this series (Chapters 3, 7) and not
otherwise present in the corpus (q=gradient sliding, q=prox sliding, q=composite optimization
all return zero hits as of 2026-09-18).
The obvious first idea — treat the PS procedure's inexact inner solve as adding an error term to a standard accelerated-gradient argument and bound that error by the number of inner steps — fails because a naive termination criterion (the function-value optimality gap of the PS subproblem) does not yield the accelerated rate; the book's own analysis (the paragraph preceding Proposition 8.1) states this explicitly. The working criterion instead combines the optimality gap and the distance to the optimal solution, weighted by the -sequence — this is exactly the left-hand side of (8.1.21), not a simpler quantity, and it is this specific combination that telescopes cleanly across both the inner PS loop and, subsequently, the outer GS loop.
E is NormedAddCommGroup E, InnerProductSpace ℝ E; X : Set E. The Bregman divergence V,
model function g/lh, and constraint function chi are hypothesis-carrying objects (functions
with the defining (in)equalities as hypotheses), matching this series' convention rather than
fixing them to the Euclidean/entropic special case. ps_procedure_bound (Proposition 8.1) takes
the three-point inequality that the argmin in (8.1.17) yields (a standard consequence of Lemma 3.5,
cited but not re-derived) as an explicit hypothesis on the sequence u, rather than proving
well-posedness of the argmin itself. gs_convergence_bound (Theorem 8.1(a)) similarly takes
Proposition 8.2's per-outer-step recursion (8.1.26) as a hypothesis — its own proof composes
Proposition 8.1 with model-function inequalities (8.1.27)-(8.1.31) that are outside this mission's
selected scope — and formalizes only part (a) (unbounded X), not part (b) (compact X, reverse
monotonicity), since only (a) is on the goal's dependency path. explicit_gs_rate (Corollary
8.1(a)) uses the closed forms and that the specific
schedule (8.1.39)-(8.1.40) produces (8.1.44, 8.1.46 — cited, not restated), rather than the general
recursion, and takes Theorem 8.1(a)'s bound, specialized to this schedule, as a hypothesis: its own
content is the purely algebraic simplification (8.1.45)-(8.1.48) into the closed-form bound
(8.1.41), not a re-derivation of the general theorem. The source PDF's own printed (8.1.40) is a text-extraction artifact (no such -indexed quantity appears anywhere in this
section); the proof's own algebra (, using
, ) is consistent only with , which is what is
formalized. A trivializing formalization would fix or , collapsing the
composite problem to plain smooth minimization and making the entire PS-procedure apparatus
vacuous; this is ruled out by keeping and as free convex functions throughout with
hMLip an active, non-degenerate hypothesis. Proposition 8.2 (the recursion gs_convergence_bound
cites) and Theorem 8.1(b) (the compact-X case) are natural extensions a further contribution
could add.
Most machine learning training objectives — deep network losses, matrix factorization, regularized empirical risk with a nonconvex loss — are not convex, yet the great majority of convergence theory available before Ghadimi and Lan's 2013 work applied only to convex problems or gave no non-asymptotic rate at all. Ghadimi and Lan (2013) established the first non-asymptotic complexity bounds for stochastic first-order methods on smooth nonconvex problems, using the norm of a gradient mapping (rather than function-value suboptimality, which is meaningless without convexity) as the convergence measure, together with a randomized stopping rule that removes the need to know in advance which iterate will be best. This mission formalizes the constrained, composite generalization of that theory — Lan's own extension (2020) to problems with a nonsmooth term and a general Bregman geometry rather than the Euclidean norm — culminating in the stochastic complexity bound for the randomized stochastic mirror descent (RSMD) algorithm.
Fix a nonempty closed convex , a continuously differentiable (possibly nonconvex) with -Lipschitz gradient, and a simple convex (possibly nonsmooth) (e.g. or ); write , (assumed finite). For a distance-generating function with modulus 1 and its prox-function , the generalized projection at with gradient-like input and stepsize is
which reduces to itself when and : is a generalized projected gradient (or gradient mapping) of at , and its norm going to zero is the right notion of "approximately stationary" for the composite, possibly-nonconvex problem .
The randomized stochastic mirror descent (RSMD) algorithm, given only a stochastic first-order oracle returning with and (Assumption 13), forms a mini-batch average of oracle calls at each step , updates via the generalized projection with , and stops at a randomly chosen index (drawn from a prescribed pmf , independently of the optimization process) rather than a deterministic final iterate.
for (strict for at least one ) and chosen as in (6.2.30), the expectation over both and the oracle randomness .
Every result states its constants exactly as the book derives them; no milestone or the goal hides a rate behind an unspecified .
The goal theorem gives the complexity of the RSMD algorithm in terms of a squared generalized gradient-mapping norm — the correct convergence criterion for constrained, composite, possibly nonconvex stochastic optimization, since function-value suboptimality is not controllable without convexity and unconstrained gradient norms are meaningless once or is nonsmooth. Choosing and appropriately (a corollary this mission does not formalize) turns this bound into the celebrated total-oracle-call complexity for finding an -stationary point in expectation — the standard benchmark every later stochastic nonconvex method (variance-reduced SGD, SPIDER, and their composite/constrained variants) is compared against.
No result in this mission has a machine-checked proof on Prove2Me under this exact hypothesis set.
The two closest platform results, both from lean-optrates (Shi), are genuinely different
objects: ShiOptRates.gd_exact_rate is plain, unconstrained, deterministic gradient descent
(, no set , no composite , no generalized projection), and
ShiOptRates.Stochastic.sgd_rate is plain SGD under the same unconstrained, non-composite
setup — its filtration/conditional-expectation formalization pattern (a Filtration ℕ, μ[·|ℱ k] for the unbiasedness and variance-bound hypotheses) is the same one this mission's goal
theorem uses, confirming it as the platform's established idiom for this class of result, but the
mathematical content (plain gradient step vs. generalized-projection/mirror-descent step, no
or ) is different. Neither is reused; both are noted as the platform's nearest existing work.
The generalized projection replaces the Euclidean projection with an arbitrary Bregman-based prox-mapping and absorbs the nonsmooth term directly into the subproblem — a formalization that quietly assumes or would collapse every milestone here into the special case and prove nothing about the constrained composite problem the chapter is actually about. The harder difficulty is in the goal theorem's own randomness: the book's proof does not use an unconditional (marginal) form of Assumption 13, because from step 2 onward is itself a random variable (a function of the history ), so the cross-term the proof needs to vanish requires a conditional statement — "" is the book's own phrasing. A formalization using only marginal moment bounds would either be unprovable as stated or, worse, would misstate the theorem by using hypotheses too weak for the claimed conclusion.
generalized_projection_gradient_bound, generalized_projection_characterization,
nonconvex_md_bound and nonconvex_md_rate are stated over a real inner product space (Chapter
6's own generality — unlike Chapter 3, §6.2.3 explicitly restricts to "the norm associated with
the inner product"), with every argmin-defined point (, and the iterate sequence )
represented by its pointwise minimality property rather than an argmin term, consistent with
this series' convention. The goal theorem, rsmd_complexity_bound, additionally introduces a
probability space (Ω,P) and a Mathlib Filtration ℕ 𝒢, with x k/G k required
𝒢(k-1)-strongly-measurable and Assumption 13 stated via MeasureTheory.condExp (𝒢 (k-1))
(conditional mean 0, conditional second moment ≤ σ²/m_k) — the conditional form the book's own
proof actually needs, not a weaker marginal substitute. The σ²/m_k bound is (6.2.40)'s
conclusion for the m_k-sample batch average, taken as a hypothesis on the already-averaged G k
directly rather than re-derived from m_k raw i.i.d. calls (that derivation is not itself a
numbered result of the book). 's independence from the process is stated via
ProbabilityTheory.IndepFun; every integrability side condition the conclusion's Bochner
integral needs to be non-vacuous is stated explicitly, guarding against the well-known trap of an
uninhabited/non-integrable hypothesis silently defaulting condExp/the integral to 0 and making
the theorem trivially true.
A trivializing formalization this mission rules out: taking and
throughout would make every generalized projection collapse to the ordinary gradient, reducing
this entire mission to a restatement of plain (stochastic) gradient descent — exactly the
ShiOptRates results already on the platform — rather than the constrained composite theory the
chapter develops; , and are kept as genuine free parameters in every milestone and the
goal.
Left out of scope, for time: Theorem 6.6(b) (the convex-case corollary on , requiring the nondecreasing/nonincreasing stepsize side-conditions of (6.2.33)/(6.2.35)); the raw-sample derivation of (6.2.40); Lemma 6.3 (the stationarity consequence of a small gradient mapping, using and the normal cone ); the 2-RSMD algorithm and its large-deviation improvement; and the gradient-free (RSMDF) variant.
Gradient descent's convergence rate for a general smooth convex problem is in the function-value gap; Nemirovski and Yudin (1983) proved that no first-order method can do better than is achievable, and Nesterov (1983, 1988, 2004) constructed the first method attaining it — the accelerated (or "fast") gradient method. For thirty years this was the standard route to -rate solvers in convex optimization, and the technique underlies essentially every modern accelerated first-order method used at scale in machine learning (accelerated SGD, momentum methods, Nesterov-style extensions of Adam). The two building blocks this mission formalizes on the way there — subgradient descent (Polyak, 1960s) and mirror descent (Nemirovski & Yudin, 1983) — are themselves the default tools whenever the objective is nonsmooth or the constraint set's natural geometry is not Euclidean (e.g. the probability simplex, where mirror descent with the entropic distance-generating function beats projected subgradient descent by a factor).
Fix a nonempty closed convex set (in Lean: a normed real vector space , X : Set E) and a
convex ; write and for an arbitrary
minimizer. The projected-subgradient update is for a subgradient and stepsize
. Its generalization, mirror descent, replaces the Euclidean proximal term with a
Bregman divergence built from a
1-strongly-convex distance-generating function with respect to a general norm
(dual norm ): ,
where is now a continuous linear functional (a subgradient in the dual space, since the
norm need not come from an inner product). Choosing recovers and the plain subgradient update as a special case.
The accelerated gradient method additionally assumes has -Lipschitz gradient () and is -generalized-strongly-convex w.r.t. ( for ), and tracks three coupled sequences from :
With , and :
Every constant here is exactly the book's; no milestone hides an behind an unspecified absolute constant.
The chain culminates in an explicit, non-asymptotic certificate for accelerated gradient descent — the theoretically optimal rate for smooth convex minimization by a first-order method (matching the Nemirovski–Yudin lower bound, not re-derived here). Formalizing it forces every implicit convention in a standard optimization-course derivation to become explicit: which of the three sequences a given quantity refers to, exactly which inequality (3.3.7)-(3.3.9) each specific stepsize schedule needs to satisfy, and the precise index range over which the chapter's own stated hypotheses actually get used in its own proof (see Difficulty below).
None of these six results (or their strongly-convex counterpart, Theorem 3.7, left for future
work — see Formalization scope) has a machine-checked proof on Prove2Me. The one theorem with
the same name as this mission's subject, BanditAlgorithm.mirror_descent_regret_bound
(Lattimore & Szepesvári, Theorem 28.4), is a different object: an online, adversarial regret
bound against a changing sequence of loss vectors , not an offline function-value gap for a
single fixed ; not reused. Likewise OnlineConvexOpt.FirstOrder.online_gradient_descent_regret
(Hazan) and OnlineConvexOpt.ConvexBasics.constrained_gd_well_conditioned_convergence are,
respectively, an online-regret bound and a plain-gradient-descent (non-accelerated) linear-rate
result — checked and confirmed not reusable per the mission brief.
The three-point inequalities (Lemmas 3.1/3.4) are routine consequences of a strongly-convex minimizer's optimality condition. The real difficulty is bookkeeping across three coupled sequences in the accelerated method: a formalization using only and (dropping , the point at which the gradient is actually evaluated) is not Lan's algorithm and proves either a false or a different bound — is what lets the method use a gradient computed at a point between and , which is exactly the extrapolation step that makes acceleration work.
A second, subtler difficulty is that Theorem 3.6's own stated hypothesis — "(3.3.15) for any " — is not quite what its proof uses. Telescoping Proposition 3.1's per-step bound via (3.3.15) requires the previous step's constants ; at these would be , values the recursion (3.3.4)-(3.3.6) never defines (it only ever uses for ). The book's own proof, read closely, invokes (3.3.15) only for , with handled directly by Proposition 3.1's conclusion connecting to the given base data . Formalizing the literal hypothesis range would either be unstatable (no exist) or vacuous (adding unused ghost parameters); this mission states the range the proof actually needs.
Chapter 3's own §3.1/§3.2 split (Euclidean vs. general norm) is preserved rather than collapsed:
subgradient_iterate_three_point/subgradient_descent_bound are stated over a real inner
product space with the vector subgradient and the Euclidean norm, exactly matching
§3.1; mirror_iterate_three_point/mirror_descent_bound and the two accelerated-method
milestones are stated over a general real normed space [NormedAddCommGroup E] [NormedSpace ℝ E], with subgradients as continuous linear functionals E →L[ℝ] ℝ (whose Mathlib operator norm
is already the dual norm , needing no separate definition) and the Bregman
divergence left as a free two-point function — but, following a
2026-09-19 revision, no longer a totally free function. V is now required to satisfy the two
facts (3.2.2)/(3.2.3)/(3.2.6) actually establish and every downstream proof (Lemma 3.4, Theorem
3.5, Proposition 3.1, Theorem 3.6) uses: nonnegativity ( for ) and the
three-point/cosine identity ,
the latter made explicit via an added parameter dV : E → E → (E →L[ℝ] ℝ) read as "the gradient
of at ." Without these two hypotheses the five items that use an abstract V
(mirror_iterate_three_point, mirror_descent_bound, accelerated_one_step_recursion,
accelerated_gradient_recursion_bound, accelerated_gradient_rate) are false as stated — a
constant V satisfies the bare pointwise-minimality hypotheses while violating the conclusion, as
two worked counterexamples confirmed. This mission does not derive V/dV from an explicit
distance-generating function (the heavier, fully book-literal route (3.2.1)-(3.2.2) would);
it takes the two facts the proofs actually consume as hypotheses directly, which is lighter and
sufficient. Satisfiability is witnessed by the Euclidean case already in §3.1:
, , , exactly how
subgradient_iterate_three_point/subgradient_descent_bound already handle the Euclidean
special case. A trivializing formalization this mission rules out: specializing to the
Euclidean squared distance in mirror_iterate_three_point/mirror_descent_bound would make
those two milestones restatements of the §3.1 Euclidean results rather than genuine
generalizations, exactly the pitfall the chapter brief flags.
Every argmin-defined iterate ( in each of the three update rules) is represented by
its defining pointwise-minimality property rather than by an IsMinOn/argmin term, so no
existence or uniqueness lemma for the underlying minimization problem is needed anywhere in this
mission — matching how the book's own proofs use these updates (via their first-order optimality
condition, never via an explicit formula for the minimizer).
Left out of scope, for time: Theorem 3.7 (the strongly-convex, linear-rate
companion to Theorem 3.6, sharing Proposition 3.1 as its own base lemma) and Corollary 3.5 (the
composite-objective extension ). Both are natural continuations reusing this
mission's accelerated_one_step_recursion; a later mission or an amendment to this one could add
them as additional milestones/goals without touching what is here.
Von Neumann's minimax theorem (Chapter VIII) settles two-player zero-sum games with scalar payoffs. In 1956, Blackwell asked the natural generalization: what can a player guarantee in a repeated game with vector-valued payoffs, where "winning" means driving the average payoff into a target set rather than above a target value? For decades the resulting theory — approachability — and the regret-minimization theory this book develops were believed to be different, with approachability seen as the stronger notion. Chapter 13 closes that gap: approachability and online convex optimization are shown to be algorithmically equivalent, each reducible to the other with no loss of efficiency, and along the way this equivalence yields a constructive, rate-quantified proof of Blackwell's own theorem.
A generalized vector game (Definition 13.2) is given by bounded convex closed decision sets and a vector payoff . A set is approachable (Definition 13.3) if some non-anticipating algorithm, playing in against any sequence , drives the average payoff's distance to to zero. Blackwell's theorem (13.4) characterizes exactly which are approachable via a purely geometric condition: every column-player strategy admits a row-player best response landing the payoff in .
Section 13.2 constructs an explicit approachability algorithm from any OCO algorithm: given a best-response oracle realizing Blackwell's condition, Algorithm 37 runs the OCO algorithm on the proxy losses (the support function letting distance-to- be written, via Lemma 13.5's minimax duality, as a convex optimization problem over the unit ball), queries the oracle at the OCO algorithm's play , and averages the resulting rewards.
This chapter's headline claim — approachability and OCO are equivalent — is proved in two
directions in the book (§13.2 and §13.3); this mission drafts the direction the book itself
foregrounds as "the more interesting implication" and constructively proves: any sublinear-regret
OCO algorithm converts directly into an explicit approachability algorithm with an explicit
convergence rate, giving a self-contained, algorithmic proof of a 1956 game-theory theorem using
1990s–2000s online-learning machinery. Historically, this equivalence resolved a standing
misconception (approachability believed strictly stronger) and reframes Blackwell's theorem as a
special case of regret minimization rather than a separate theory requiring its own toolkit. No
prior art was found on the platform for Blackwell approachability (planning search:
q=Blackwell — the one hit, PRNGCompression.prng_no_free_lunch's cousin, an unrelated
Rao-Blackwellization result, is not a substitute); this mission drafts both items fresh.
Theorem 13.4's statement is a clean geometric implication, but the book is explicit that its
proof is entirely carried by Theorem 13.7 plus an unstated "explicit conclusion" left as an
exercise (the passage from a finite-horizon rate bound to the asymptotic Dist → 0 claim, using
any of the book's own sublinear-regret OCO algorithms as a witness). Theorem 13.7's own proof
combines three nontrivial facts: Lemma 13.5's minimax-duality rewriting of as a linear optimization over the unit ball (itself proved via Sion's minimax theorem, not
excerpted here), the best-response oracle's defining inequality (13.2) applied pointwise at each
round's , and the OCO algorithm's own regret guarantee applied to the specific proxy-loss
sequence built from the realized game trajectory — a genuine composition of three separate
pieces of machinery from earlier in the book (Chapters III–VIII), not a routine substitution.
IsApproachable is declared as its own definition (per BRIEF.md's explicit instruction, since
Theorem 13.4 depends on it), with the non-anticipation clause made explicit (matching the
series' IsOnlineAlgorithm convention from Chunk 03) even though the book's own Definition 13.3
states it only informally ("x_t ← A(y_1,\dots,y_{t-1})"). SupportFunction is h_S exactly as
displayed, as a real supremum (a genuine maximum given the chapter's standing "closed, bounded"
hypothesis on S). throughout is Euclidean distance, rendered as Mathlib's
Metric.infDist — confirmed the chapter uses no other distance notion (checked §13.1-13.3
directly, per the pitfall BRIEF.md flags). Theorem 13.7 transcribes Algorithm 37's
construction faithfully, including its one-round offset (using the
previous round's realized reward to build the current round's proxy loss, while the
conclusion averages the current round's rewards) — exactly as the book's own pseudocode has it,
not smoothed over.
Scope decision on Theorem 13.4's biconditional. The book states Theorem 13.4 as an ↔ but
proves, and explicitly flags as proved, only the sufficiency direction (←): "The necessity of
this condition is left as an exercise... Our reductions henceforth give an explicit proof of
Blackwell's theorem [meaning: of the sufficiency direction]." Per CAPTAIN_BRIEF.md rule 6 and
BRIEF.md's explicit instruction, this mission drafts only that direction, named as such in the
goal item's own docstring; see STATUS.md.
Not formalized (out of scope for this mission, given the remaining budget and the explicit
"exercise" status of several results on these pages): the necessity direction of Theorem 13.4;
Lemma 13.5 (minimax duality for Dist, itself relying on Sion's theorem, not separately
formalized here); Lemma 13.6 (the equivalent best-response-oracle condition); §13.3's entire
approachability-to-OCO direction (Theorem 13.9, Lemma 13.8, the cone/polar-cone machinery of
§13.3.1) and §13.3.3 (existence of a best-response oracle for the constructed set); the "explicit
conclusion" of Blackwell's theorem from Theorem 13.7, left as an exercise by the book itself.
Chapter XI boosted a weak learner into a strong one for a single offline fit to a fixed sample. Chapter 12 asks the analogous question online: when the pool of experts is too large to run Hedge over directly (the contextual-learning setting, where "experts" are policies mapping contexts to actions and their number is exponential), can black-box access to a cheap approximate — "weak" — online learner be boosted into an algorithm with vanishing regret against the whole hypothesis class, without ever touching it directly? Chapter 12 answers yes, by cascading weak learners through a Frank–Wolfe-style online construction whose running time is independent of the hypothesis class's size.
A -weak OCO learner (WOCL, Definition 12.1) for hypothesis class guarantees, against any linear loss sequence with bounded range, — competitive with only a -fraction of the best fixed hypothesis's performance, plus a sublinear additive term. Because a -multiple guarantee is not shift-invariant, this is stated (Eq. 12.2) after normalizing losses so at the decision set's center of mass.
The weak learner's predictions must be scaled by to be useful, which pushes them outside the decision set — so Algorithm 36 needs a way to evaluate a proxy loss at points outside and project back without paying much. Section 12.3's extension operator (a smoothed, distance-penalized version of ) solves this: Lemma 12.3 shows it agrees with on up to , and that projecting onto costs at most another .
Algorithm 36 cascades copies of a -WOCL: starting from , each stage takes a -weighted step toward the -th weak learner's scaled prediction, and each weak learner is fed the gradient of the extended loss at the previous stage's iterate as its own linear loss — a genuinely projection-free, Frank–Wolfe-style construction (as in Chapter VII), applied here to a cascade of learners rather than a single gradient-descent sequence.
for ; for .
For -smooth and -Lipschitz, .
With , , Algorithm 36's predictions satisfy
Theorem 12.4's comparator is the convex hull of , not the best single hypothesis — strictly
stronger, and (as the book notes) still a meaningful guarantee even at (a weak learner
that already matches 's best hypothesis), since the boosting algorithm's payoff is purely the
upgrade from to . Combined with §12.1.1's binary-classification instantiation and the
-vs--style efficiency argument, this is the
chapter's answer to whether contextual-learning-scale expert classes (exponential in context
count) can be handled with per-round cost independent of — a genuinely new computational
regime relative to Hedge's -dependence. No prior art was found on the platform for
online boosting or the extension operator (planning search: q=online+boosting,
q=extension+operator — 0 hits); this mission drafts all three results fresh, building
internally on a Frank–Wolfe-style construction restated locally (Chunk 07 is not yet published).
Lemma 12.3's proof combines the smoothing operator's own approximation guarantee (part 1, "since for , this follows immediately from Lemma 2.8") with a Cauchy–Schwarz argument balancing the gradient-norm bound against the penalty coefficient exactly at (part 2) — a delicate one-parameter tuning, not a generic estimate. Lemma 12.5's proof (not fully excerpted here, continuing past PDF p. 223 with an inductive argument on across the cascade stages) is structurally the Chapter VII Theorem 7.1/Lemma 7.4 argument applied once per stage, compounding the -WOCL guarantee's slack across all stages simultaneously — a genuinely two-dimensional induction (over both rounds and stages ) that the offline or single-stage online analyses do not need. Theorem 12.4's own proof (PDF p. 224 onward, not fully excerpted) combines both lemmas with the specific parameter substitutions , , and to reach the stated closed-form bound.
Extension/SmoothedFunction redeclare Chapter II's smoothing operator (matching
BanditConvex.SmoothedFunction, Chunk 06, in content — neither is yet published) rather than
importing it, per Addendum 2 rule 5. IsGammaWOCL is drafted at the shifted-form Eq. (12.2) the
rest of the chapter actually works with (not Definition 12.1's own unshifted form with the
center-of-mass term ), matching the book's own explicit simplification. IsOnlineBoostingRun
mechanizes Algorithm 36's full five-line cascade (stage-by-stage iterate, weak-learner scaling,
final projection, and the per-stage linear-loss construction from the extended loss's gradient) —
the fullest mechanization in this mission's items, since Theorem 12.4's own hypotheses (hWOCL,
one γ-WOCL guarantee per stage) need the run's internal structure to connect xplay to the weak
learners' regret guarantees at all. Lemma 12.5 is drafted at a more abstract level (x^N,
x^\star, Regret_T(W) as direct inputs, matching how the book's own proof of that lemma
proceeds before Theorem 12.4's own parameter substitution), consistent with the "no more
mechanization than the statement needs" principle used throughout this series (e.g. Chunk 10's
Lemma 7.4-style scoping). CH(H) is Mathlib's own convexHull ℝ H, applied to H viewed as a
subset of the function space — a faithful match to the book's {∑_{h∈H}p_hh \mid p\in\Delta_H}
that also correctly handles infinite H, which the book's own sum notation does not
literally cover.
Not formalized: §12.1's motivating discussion and its binary-classification/personalized-article
examples (illustrative, not numbered theorems); the running-time-independent-of-|H| claim
(prose, not part of Theorem 12.4's own mathematical content, per BRIEF.md); Remarks 1-2
following Theorem 12.4 (commentary, no further claim).
Every algorithm in Chapters I–V observes the full cost function after playing . Many applications only reveal the scalar cost incurred — routing a network and observing total latency, or placing an ad and observing the click-through revenue, without ever seeing the cost of a path or bid not taken. This is the bandit feedback model, and Chapter 6 asks whether sublinear regret survives it. The chapter's answer is a general two-part reduction — turn a first-order full-information algorithm into a bandit algorithm by feeding it an unbiased gradient estimator built from a single scalar observation — instantiated concretely on online gradient descent to produce the first historical bandit convex optimization algorithm, the FKM algorithm (Flaxman–Kalai–McMahan).
Let be the decision set, containing the unit ball centered at , with diameter at most . At each round the player picks , an adversary has fixed a cost function (Lipschitz constant , bounded by in absolute value on ), and the player observes only the scalar — never itself or its gradient. Regret is , exactly as in the full-information setting, but now the algorithm's plays are themselves random (they depend on the sampled gradient estimates), so the guarantee is on expected regret.
The chapter's construction has two independent parts. Part 1 (Lemma 6.5) is a black-box reduction: given any first order full-information algorithm (Definition 6.4 — one that depends on each cost function only through its gradient at the played point) with a full-information regret bound , feeding an unbiased estimator of in place of the true gradient preserves the regret bound in expectation, up to evaluated at the estimators instead of the true gradients. Part 2 (Lemma 6.7) supplies such an estimator using only one scalar observation per round: sample uniformly from the unit sphere, play for a small radius , and is (for linear ) an unbiased estimator of — more precisely, an unbiased estimator of the gradient of 's -smoothed version , by a Stokes'-theorem identity relating a ball integral to a sphere integral.
for any fixed , any first order algorithm with full-information bound , and any sequence of estimators with .
The FKM algorithm (Algorithm 23: play , form , update on the shrunk set ) with , guarantees
Theorem 6.9's rate is strictly worse than the rate of full-information online gradient descent (Chapter III) — this gap, not a shared rate, is the chapter's real content: bandit feedback provably costs regret, and the FKM algorithm is the historically first algorithm to pin down how much, via the clean two-part reduction that later chapters' improved bandit algorithms (§6.5's self-concordant-barrier method, not formalized here) all refine. Lemma 6.5 is independently reusable: it is a template, quantified over an arbitrary first-order algorithm and an arbitrary unbiased-estimator family, not tied to the sphere-sampling construction that instantiates it for Theorem 6.9. No prior art was found on the platform for bandit convex optimization, gradient-free methods, or Frank–Wolfe-style estimators; this mission's three items formalize the standard textbook account fresh.
Lemma 6.5's proof is a martingale-style argument: it introduces auxiliary deterministic functions (where ) whose gradient at is exactly , applies 's full-information bound to the 's (a genuinely random cost sequence, since is random), and then takes expectations, using unbiasedness () to show and for the fixed comparator . This requires a genuine filtration and conditional expectation, not merely an unconditional expectation, since and are themselves random and adapted to different points in the history. Lemma 6.7's proof invokes Stokes' theorem to relate to , then uses the volume ratio — a calculus fact about Euclidean balls and spheres, not itself re-derived in this mission's Lean (the identity is drafted as the statement Lemma 6.7 asserts, to be proved from Mathlib's own ball/sphere volume and divergence-theorem lemmas).
IsFirstOrderOnlineAlgorithm formalizes only the substitution property of Definition 6.4 (the
book's second bullet); the first bullet, a closure condition on the admissible family of loss
functions, is a precondition on 's domain rather than a checkable mathematical property and is
not formalized — see MODERATION_NOTES.md. SmoothedFunction (Eq. (6.4)) and
IsUniformOnUnitSphere are declared once and shared by both milestones and the goal, rather than
re-derived inline. Lemma 6.5's history is modeled by an explicit filtration 𝓕 (with x t
adapted to 𝓕 t and g t to 𝓕 (t+1)), since Lean's conditional expectation needs a concrete
σ-algebra to condition on; the book's informal "history " is exactly this
filtration once the (deterministic) 's are set aside as carrying no randomness. Kδ, the
shrunk decision set Algorithm 23 actually projects onto, is kept a separate object from K
throughout (a pitfall the chapter brief flags explicitly), and in Theorem 6.9 is
rendered as an infimum, checked non-vacuous since is nonempty and the objective is bounded
below on by the chapter's own assumption.
Not formalized: §6.5's self-concordant-barrier bandit linear optimization algorithm (starred, out of the recommended goal's scope) and Corollary 6.8's ellipsoidal-sampling generalization (a routine corollary of Lemma 6.7 the book itself derives, not independently central).
Online convex optimization (OCO) asks a learner to repeatedly pick a point in a convex set , pay a cost that an adversary reveals only after the choice is made, and be judged against the best fixed point in hindsight. Chapter III of this series formalized the simplest general-purpose answer, online gradient descent (OGD): take a gradient step, project back onto . OGD's analysis, however, is tied to the Euclidean geometry of the projection step — it treats every coordinate of alike, and its regret bound degrades badly when 's natural geometry is not Euclidean (the probability simplex under the norm is the standard example, where a Euclidean-projection algorithm's regret scales with in the dimension , while an algorithm that exploits the simplex's own geometry attains regret scaling only with ).
Regularized Follow the Leader (RFTL) is the meta-algorithm this chapter introduces to fix this: rather than fixing a specific geometry, RFTL is parameterized by an arbitrary regularization function , and its regret bound depends on only through two scalar quantities the mission makes explicit — the range of over , and a -dependent "local norm" of the gradients. Choosing to match 's geometry (entropy regularization on the simplex, for instance) recovers the sharp bounds that plain OGD cannot. RFTL and its close relative Online Mirror Descent (OMD), also introduced here, are the ancestors of essentially every regularization-based online learning algorithm in use today, including the multiplicative-weights/Hedge algorithm of Chapter I as a special case (entropy regularization on the simplex) and the exponentiated-gradient algorithm this book's own Chapter VIII reuses (Corollary 5.7, a further specialization of Theorem 5.2 this mission's Theorem 5.2 underlies). The naive "Follow the Leader" strategy this chapter opens by refuting — always play the empirically best point so far — is a natural first idea and provably fails: the book gives an explicit two-point cost sequence on which it incurs regret linear in the horizon. Regularization is the fix, and quantifying exactly how much it costs and buys is this chapter's content.
Fix a convex, nonempty decision set in a real inner product space and a sequence of convex cost functions . As in Chapter III, regret after rounds is
A regularization function is a strongly convex, smooth, twice differentiable function with a positive-definite Hessian on the interior of . Its Bregman divergence measures the gap between and its own first-order Taylor approximation:
By the mean value theorem, for some point on the segment , where is the norm induced by the Hessian ; its dual norm, denoted , is the local norm at . Writing for the local norm between consecutive iterates , the -diameter of is .
The RFTL algorithm (Algorithm 13), with step size , plays , then at every round updates
The agile Online Mirror Descent algorithm (Algorithm 14, agile version) instead maintains a dual point with , updates it by , and projects via the Bregman divergence, (with defined the same way from ). RFTL and the lazy variant of OMD coincide for linear costs (Lemma 5.5, not formalized here — it is not used by either target); the agile variant's analysis is genuinely different and is the mission's second target.
This is the mission's goal: RFTL, run with any admissible regularizer, attains a regret bound governed only by the cumulative squared local norm of the gradients and 's range over . The bound is proved via two milestones: Lemma 5.3 (regret controlled by the total "prediction drift" plus ), which in turn rests on Lemma 5.4 (a "follow-the-leader beats be-the-leader" comparison inequality, proved by induction on the horizon).
A structurally similar bound for the agile variant, included as its own goal-level item since — as the book states explicitly — its proof technique is unrelated to RFTL's, not a corollary of it.
Both targets are the book's own tightest, non-asymptotic statements: neither is weakened to an form, and the book's own further (unnumbered) corollary specializing Theorem 5.2 to a uniform local-norm bound is left out, matching this series' convention of formalizing only the numbered results.
The results themselves. Theorem 5.2 is the general regret theorem behind every regularization scheme in online learning: instantiating recovers the projected-gradient bound of Chapter III (Euclidean ), the multiplicative-weights bound of Chapter I (entropy on the simplex), and — through the exponentiated-gradient specialization (Corollary 5.7, not itself a target here) — the row-player regret bound this book's own Chapter VIII cites as "Eq. (8.1)" in its reduction of zero-sum games to regret minimization. Theorem 5.6 gives the same guarantee for an algorithm (agile OMD) that, unlike RFTL, maintains a feasible point at every round, which the book notes is preferable in the adaptive-regret setting of Chapter X.
Formalizing it. Both theorems have complete, elementary proofs in the source (no gaps, no "with high probability", no hidden regularity conditions); the mission's work is converting the analytic argument — the Bregman-divergence identity, the generalized Cauchy-Schwarz inequality bounding the drift term by the local norm, and the two induction arguments underlying Lemma 5.4 — into machine-checked statements. No formalization of RFTL, OMD, or the local-norm machinery exists on the platform (checked below); the closest Formalpedia entries state a related but distinctly narrower result.
The central obstacle is that the regularizer is a hypothesis, not a fixed function: the theorem must hold for every admissible simultaneously, so nothing about beyond its stated properties (strong convexity, smoothness, twice differentiability) may be used. A newcomer's first instinct — bound the local norm by a fixed multiple of the Euclidean dual norm — fails in general and is exactly the bound RFTL is designed to avoid needing; the whole point of the local-norm formulation is that it can be tight for regularizers (like entropy) whose Hessian is very far from a multiple of the identity. A second obstacle is Lemma 5.4's induction, which compares (a minimizer over terms) against using the minimality of at exactly the right instantiation — an argument that looks almost circular until the induction hypothesis is applied at , not at the theorem's free variable.
ranges over an arbitrary real, complete inner product space (a real Hilbert space),
matching Chapters III and IV, not a fixed . The RFTL and agile-OMD update
rules are represented relationally (IsArgMinOn), since Mathlib has no canonical argmin
operator for a general convex set — mirroring IsMetricProjection's precedent from Chapter
III. The Hessian at the mean-value-theorem's intermediate point is represented via the
second Fréchet derivative of 's gradient map (HasFDerivAt), since Mathlib has no
dedicated Hessian type; the local dual norm is then any value satisfying the resulting
existential characterization (IsLocalDualNormSq), stated once and shared by both targets.
A boundedness hypothesis on over is added to Lemma 5.3's statement to keep the
-diameter from collapsing to Mathlib's junk value for an unbounded supremum — a
condition every regularizer the book actually uses (strongly convex and smooth over a
bounded ) already satisfies, so it narrows nothing.
Trivializing formalization ruled out. A regret bound stated for an "algorithm" defined
loosely enough to include the after-the-fact optimal choice would be vacuous; IsRFTLRun
and IsOMDAgileRun instead pin down the exact history-dependent update rule of Algorithms
13 and 14 (the current gradient sequence, the current regularizer, and nothing else) as a
hypothesis, so a proof must genuinely use the specific update. Theorem 5.2 and Theorem 5.6
are kept as two separate items rather than one theorem parameterized by an algorithm choice,
since — per the chapter's own remark that their analyses are unrelated — a merged statement
would either need to branch internally on the algorithm or silently identify two genuinely
different update rules.
Reuse and prior art. OnlineConvexOpt.FirstOrder.RegretT (Chapter III, published) is
imported and reused verbatim, keeping the regret functional identical across the whole
book. Definitions specific to Chapter IV (OnlineConvexOpt.SecondOrder, not yet published)
are not imported per this series' convention that a draft cannot import another draft;
quadForm is redeclared locally instead. On the platform, BanditAlgorithm.ftrl_regret_bound,
BanditAlgorithm.mirror_descent_regret_bound, and BanditAlgorithm.ftrl_simplex_exp_weights_regret
(the Bandit Algorithms series, Chapter XII) state regret bounds for FTRL and Mirror Descent
in the linear-cost, bandit-idiom setting (a fixed linear loss at
each round, regret compared via a Bregman-divergence potential at fixed points). Hazan's
Theorem 5.2 and 5.6 are for general convex and use the book's own local-norm
object, which has no counterpart in those statements; they are read in full and are not
faithful substitutes (different hypothesis class), so this mission drafts its own,
independent items rather than reusing them.
Online convex optimization measures a decision maker against the best fixed decision in hindsight, and the standard guarantee — achieved, for instance, by online gradient descent — is regret growing like over rounds. This rate is unimprovable for general convex losses: an adversary can always force regret against any algorithm. But many losses that arise in practice are not merely convex — they carry extra curvature that a first-order method cannot exploit. The paradigm case is online portfolio selection: a trader repeatedly rebalances wealth across assets, observes the market's return vector, and is scored by the logarithm of her wealth growth. Thomas Cover's 1991 universal portfolio theory showed that a decision maker with vanishing average regret against this log-wealth objective grows her wealth, asymptotically, at the same rate as the best fixed (constantly rebalanced) portfolio in hindsight — without any statistical assumption on how the market behaves, in sharp contrast to the Geometric Brownian Motion model of mainstream finance (Cover, Universal Portfolios, Mathematical Finance 1991). Cover's own algorithm, and the class of losses his analysis needs, turned out to generalize far beyond portfolio selection: the same curvature condition governs online square-loss regression (Azoury–Warmuth 2001) and other exp-concave learning problems. This chapter isolates that condition — exp-concavity — and shows it buys a logarithmic-in- regret bound via a second-order algorithm, online Newton step, introduced by Hazan, Agarwal and Kale (Logarithmic Regret Algorithms for Online Convex Optimization, Machine Learning 2007), building on the polynomial-time randomization of Cover's algorithm due to Kalai and Vempala (Efficient Algorithms for Universal Portfolios, Journal of Machine Learning Research 2003) and on the multiplicative-weights algorithm EWOO, which Hazan, Kalai, Kale and Agarwal extended to general exp-concave losses (2006).
Fix a real inner-product space (in the goal theorem, ) and a convex, bounded decision set . As in Chapters I and III, an online convex optimization protocol runs for rounds: at round the player picks , an adversary reveals a convex cost , the player incurs , and regret is
exactly Eq. (1.2) of Chapter I (OnlineConvexOpt.FirstOrder.RegretT, reused unchanged here).
The costs are assumed -gradient-bounded ( on ) and has
diameter ( for ), the same standing hypotheses as
Chapters II–III.
A convex is -exp-concave over (Definition 4.1) if is concave on . This is strictly weaker than -strong convexity (Chapter III), yet Lemma 4.2 shows it is exactly a directional strong-convexity condition: a twice-differentiable is -exp-concave at iff its Hessian dominates — strong curvature only along the gradient direction, not in every direction, which is what lets loss functions like (rank-one Hessian, far from strongly convex) qualify. Lemma 4.3 turns this into the quadratic lower bound the whole chapter runs on: for and ,
Two algorithms are formalized. The Exponentially Weighted Online Optimizer (Algorithm 11,
EWOO) plays the -weighted centroid of , with ; it needs no Lipschitz or diameter
bound but is only quasi-polynomial-time in general. Online Newton step (Algorithm 12, ONS)
instead maintains a running second-moment matrix
() and moves by , projecting
back onto in the norm induced by rather than the Euclidean norm. The
formalization represents not as a matrix but as an operator , with
rendered as Mathlib's rank-one operator
InnerProductSpace.rankOne ℝ ∇_t ∇_t, as ContinuousLinearMap.inverse, and the
generalized projection as minimizing over
(quadForm/IsGeneralizedProjection in Def_..._OnlineNewtonStep).
This is the chapter's capstone: logarithmic regret in , at the price of a factor of the ambient dimension — a genuine trade-off against the dimension-free of Chapter III, stated as such rather than hidden inside an .
Also logarithmic and, unlike Theorem 4.5, independent of and — the price is EWOO's running time, not its regret, so this is not a weaker version of the same target but an incomparable algorithm formalized for contrast.
Exp-concavity is the precise dividing line between -regret losses and losses that admit regret via a tractable algorithm — narrower than convexity, broader than strong convexity, and satisfied by the log-loss of universal portfolio selection, the square loss of online regression, and (Chapter IX onward) losses arising from PAC learning reductions. The dimension dependence in Theorem 4.5 is not an artifact of a loose proof: it is inherent to the second-moment-matrix approach and is the reason later work (self-concordant barriers, sketching) is needed to remove it in special cases. Both regret bounds have long been proved on paper; formalizing them contributes machine-checked statements of the exp-concavity characterization, the quadratic lower bound it yields, and both algorithms' regret guarantees — none of which currently exist on the platform in any form (a search for "exp-concave", "online Newton step", "second-order online" and "universal portfolio" returned no hits).
The natural first idea for bounding is to bound each round's progress the way online gradient descent's analysis does: a generalized-Pythagorean argument (Lemma 4.6) reduces the regret to — this much follows the OGD template with the Euclidean norm replaced by the -norm. The obstruction is bounding itself: term-by-term it need not be summable, since does not shrink with on its own. The book's proof instead recognizes as a discrete log-determinant increment and telescopes it against , using a matrix generalization of the scalar inequality . This determinant argument (the book's Lemma 4.7) is not itself formalized as a milestone here — see Formalization scope — so a solver of Theorem 4.5 must reconstruct or restate it.
, , and are the chapter's standing hypotheses, stated explicitly on every
theorem rather than left as ambient unused variables, exactly as in Chapters II–III;
and are pinned to the theorem's own formulas via explicit hypotheses
(hγ, hε) rather than left as free existentials — Rule 7 of the captain brief. The running
matrix is formalized as a continuous linear operator on , not as a
Matrix (Fin n) (Fin n) ℝ: the rank-one update uses InnerProductSpace.rankOne, and
uses ContinuousLinearMap.inverse, which is total (it returns the zero map when is not
invertible, a convention that never bites here since every is positive definite by
construction — and each update only adds a positive semidefinite
rank-one term, so .inverse always agrees with the genuine inverse). IsOnlineNewtonStep and
IsGeneralizedProjection are dimension-free, stated for a general real inner-product space;
only the goal theorem and Theorem 4.4 fix , since only their bounds mention
the dimension explicitly. RegretT is imported unchanged from
OnlineConvexOpt.FirstOrder.Protocol (kind: reference), keeping the regret notation identical
across the whole book series. A trivializing formalization is ruled out by requiring
, , and nonempty throughout: dropping any of these would let
, , or the bound itself degenerate (e.g. would make the
projection's norm ill-behaved), producing a statement that is vacuously true rather than the
book's actual claim. Lemma 4.7 (the log-determinant inequality) and the exercises are not
formalized: the former is a general fact about positive definite operators disconnected from
the OCO-specific definitions this mission introduces, and the latter are pedagogical, not
numbered results the chapter's own proofs depend on. Reusable beyond this mission: the
exp-concavity definitions (IsExpConcaveOn, IsExpConcaveAt) for any later chapter's
exp-concave losses (the series plan flags Chapters V and X), and the generalized-projection
machinery for any future second-order OCO algorithm.
Online decision-making problems — multi-armed bandits, contextual bandits, structured bandits, and episodic reinforcement learning — look superficially different but share a common shape: a learner repeatedly acts, observes feedback, and is scored by regret against the best action in hindsight. Foster, Kakade, Qian and Rakhlin's Foundations of Reinforcement Learning and Interactive Decision Making (Foster & Rakhlin, arXiv:2312.16730v1) develops a unifying account of this shape and asks a sharper question than "does this specific algorithm work?": for a given class of possible environments, what is the best regret any algorithm can achieve? The Decision-Estimation Coefficient (DEC), introduced by Foster, Kakade, Qian and Rakhlin (2021, "The Statistical Complexity of Interactive Decision Making") and refined by Foster, Golowich, Qian, Rakhlin and Sekhari (2023), was proposed as the answer: a single real-valued complexity measure of a model class that simultaneously (i) drives a generic optimal-up-to-constants algorithm (Estimation-to-Decisions, E2D), and (ii) lower-bounds the regret of every algorithm. Item (ii) is what turns the DEC from "a complexity measure that happens to work for the algorithms we know" into a genuine characterization of statistical difficulty, in the same sense that minimax rates characterize the difficulty of estimation problems in classical statistics. This mission formalizes that lower bound.
Chapter 6 of the book (pp. 93–128) introduces Decision Making with Structured Observations (DMSO), a protocol general enough to subsume the contextual-bandit, structured-bandit and episodic tabular-RL protocols of earlier chapters. Over rounds, the learner selects a decision from a decision space ; nature draws a reward-observation pair from a fixed, unknown model , where a model maps each decision to a distribution over a reward space and an observation space . The learner has access to a model class containing (realizability). For , write for the mean reward function and for the optimal decision; regret is , exactly as in the bandit chapters, now for the general model class.
Because observations, not just mean rewards, now carry information, the DEC needs a way to measure distance between the full conditional distributions and , not just between scalars and . The chapter uses the squared Hellinger distance , one of a family of Csiszár -divergences that also includes total variation () and Kullback-Leibler () divergence. For a reference model and scale , the general Decision-Estimation Coefficient is the min-max game value
and . This mission's Lean development (FoundationsRL.GeneralDM)
formalizes discrete versions of , , for a finite outcome type, the DMSO
regret, and this DEC.
The goal is Proposition 28 (DEC Lower Bound), p. 105:
Here is the constrained DEC (§6.5.1), a variant of the offset DEC above that hard-constrains the information gain rather than subtracting it — a technical refinement needed to make the lower-bound direction go through — and the "localization condition" is a genuine hypothesis of the proposition, not a footnote. Unlike almost every other target in this series of missions, the statement quantifies over every algorithm rather than naming one: it is a genuine impossibility result. Two supporting divergence facts are included as milestones because the DEC's information-theoretic argument rests on them: Lemma 19 () and Lemma 20 (a bounded-likelihood-ratio refinement bounding in terms of ). The chapter's own matching upper bound, Proposition 26 (the E2D regret bound for the general DMSO protocol, the direct analogue of Chapter 4's Proposition 13), is included as a milestone to give the reader the matching pair the chapter presents together. Finally, Corollary 1 restates the lower bound in terms of the localized offset DEC (combining Proposition 28 with Proposition 27), included as a milestone showing the lower bound's reach beyond the constrained DEC alone.
Proposition 28 is what makes the DEC a genuine characterization of the statistical complexity of interactive decision making, rather than merely a sufficient condition for a particular algorithm family to succeed. Combined with the (uncited, technically deeper) matching upper bound for the constrained DEC — Proposition 29, stated but not proved in the book — it shows that for any finite model class, the constrained DEC is necessary and sufficient for low regret up to a factor in the localization radius: no complexity measure that is substantially different from the DEC can characterize the same problems. This is the general decision-making analogue of how minimax rates pin down statistical estimation, now for interactive protocols with adaptive feedback.
Formalizing the lower bound is new work: no result of this shape exists on the Prove2Me platform
(searches for "decision-estimation", "general divergence", "constrained DEC" and "Hellinger" — the
last of which surfaces two related-but-distinct affinity/Le Cam bounds from a different mission on
bandit lower bounds — return no faithful prior art; see MODERATION_NOTES.md). The formal
statement is the boxed proposition; the book gives a self-contained but simplified proof (two
named simplifying assumptions, §6.5.3) and cites Foster, Golowich, Qian, Rakhlin & Sekhari (2023)
for the unrestricted argument. This mission's Lean items are draft statements (:= by sorry), not
proofs; formalizing the proof itself — a two-point adaptive testing argument using the chain rule
for KL divergence and a change-of-measure step — is the open contribution this mission proposes.
The obvious first attempt is to try to prove the lower bound by exhibiting one fixed pair of hard models , as in classical two-point minimax lower bounds (Le Cam's method, Fano's inequality). This fails here because the decision-making protocol is interactive and adaptive: the algorithm's queries depend on what it has observed, so a model pair chosen obliviously (before seeing the algorithm) cannot in general be made indistinguishable to every algorithm — an adaptive algorithm can be constructed that distinguishes any two fixed models quickly by querying where they differ. The book's proof instead selects the "hard" alternative model as a function of the algorithm's own strategy (via the constrained DEC's arg max, Eq. (6.36)), so that the pair is hard specifically for the algorithm under consideration, then uses the chain rule for KL divergence plus the change-of-measure identity between the algorithm's induced distributions under and to conclude that the algorithm's realized decisions must look similar under both models — hence it cannot get low regret on both simultaneously. Every step of this argument depends on the exact game structure of the constrained DEC, not just its numerical value; a formalization that leaves as an unconstrained real parameter (rather than the actual - game with its information-gain constraint) would make the lower bound's conclusion vacuous, since the hypothesis would no longer track any actual property of .
The decision space and the outcome (reward, observation) alphabet are both taken as
finite types (Fintype); a model is a conditional probability
vector, and a reward-extraction map recovers the mean reward
. hellingerSq, totalVariationDiscrete,
klDivDiscrete specialize the book's general dominating-measure divergence formula (Eq. (6.5)) to
the counting measure on this finite type; klDivDiscrete returns an ENNReal so its
case (when is not absolutely continuous w.r.t. ) is represented honestly. The DEC, the
constrained DEC and the localized subclass are literal sInf-of-sSup/sSup-of-sSup
transcriptions of the book's min-max games — the same convention this series uses for the
Chapter-4 DEC — not opaque free real numbers, which rules out the trivializing formalization named
above.
Three deviations from this series' usual convention of pinning every constant to the value the
book's own proof derives are deliberate and disclosed. First, the numerical constant in
is explicitly called "not important" by the authors themselves
(footnote a, p. 105); it is existentially quantified (∃ c > 0) rather than pinned to a numeral.
Second — added at moderation, round 2, 2026-09-19, after the constant was found to be pinned
incorrectly — the lower bound's own multiplicative constant is also existentially quantified
(∃ c' > 0) rather than pinned to 1/20. The book's printed proof (§6.5.3, pp. 107–110) derives
1/20 (p. 110, not p. 109 as an earlier draft of this mission stated) only under two named
simplifying assumptions the theorem's hypotheses do not carry (p. 107, "Simplifications": a
class-wide bounded-curvature hypothesis, Eq. (6.34); and a bound on the unaugmented
rather than the officially-defined,
augmented this mission's decC implements). Since
augmenting either supremum's domain can only raise its value, the printed proof's bound on the
narrower, unaugmented quantity does not license a pinned 1/20 against the fully general decC
this theorem states; the book itself attributes the proof of the general statement to an external
reference (Foster, Golowich, Qian, Rakhlin & Sekhari 2023) not in this document. The existential
c' matches the book's own unpinned for Proposition 28 as printed on pp. 105–106.
Third, "any algorithm" and are formalized, as throughout
this series, without a full stochastic-process/history model: regret is a deterministic quantity
evaluated at a fixed realized decision-distribution sequence , rather than an expectation over an adaptive, history-dependent algorithm's own
randomness. Formalizing the fully adaptive, measure-theoretic version of "any algorithm" — with an
explicit filtration and expectation over the induced process law — is future work a solver
could add; the current statement is faithful to the book's deterministic-per-realization content
but not to its full generality over randomized, history-dependent strategies. The DMSO protocol
(Def_FoundationsRL_GeneralDM_Protocol) and the DEC (Def_FoundationsRL_GeneralDM_DEC) are
restated locally rather than imported from Chapter 4's mission (FoundationsRL.Structured), since
draft items cannot import another chunk's drafts; contributions extending either mission to reuse
the other's substrate once both are published are welcome.
A multistage stochastic program's exact deterministic equivalent grows exponentially with the number of periods, even when each period's random data takes only a handful of values (Chapter 9's concern was the growth in the number of realizations; Chapter 10 adds growth in the number of periods). One remedy, generalizing Chapter 8's single-period Jensen bound, is to replace the exact per-period random data by a coarser, aggregated version — conditional expectations over a partition of the history space at each stage — and solve the resulting smaller deterministic equivalent instead. This is only useful if the aggregated problem's optimal value is provably a bound (here, a lower bound) on the exact problem's, and Birge & Louveaux's Chapter 10, §10.1, Theorem 1 is exactly the statement that makes this legitimate, together with a genuinely necessary extra condition the book states explicitly two paragraphs before the theorem: "if not [i.e. if the extra condition fails], then the conditional expectation form ... may not actually achieve a bound." This mission formalizes that theorem.
The book's exact multistage stochastic linear program (Eq. 1.1, p. 418) is
min c¹x¹ + E_Ω[c²x² + ⋯ + cᴴxᴴ]
s.t. W¹x¹ = h¹, Tᵗ⁻¹xᵗ⁻¹ + Wᵗxᵗ = hᵗ (t=2,…,H, a.s.), xᵗ ≥ 0 a.s., xᵗ nonanticipative (Σᵗ-measurable),
over the exact event space Ω = Ω₁ × ⋯ × Ω_H. Given a consistent nested partition of each
Ωᵗ = Ω₁ × ⋯ × Ωₜ into finitely many blocks Sᵗ₁, …, Sᵗ_νₜ, and aggregated data (h̄ᵗᵢ, T̄ᵗᵢ) = E^{Sᵗᵢ}[(hᵗ,Tᵗ)] (the conditional expectation of the true random data over block i), the
aggregated problem (Eq. 1.2, p. 419) replaces the exact recursion by a finite tree of blocks, one
decision per block, linked to its parent block's decision. Both (1.1) and (1.2) are, structurally,
the same kind of object — a finite-tree deterministic-equivalent recourse LP — differing only in
which tree and which node data they use; this mission formalizes that shared shape once
(Tree, Instance, Feasible, obj) and instantiates it twice.
Formalized as: a shared Tree H structure (a finite node type, per-node stage, anc, and a
root), the same representation Chunk 06's Multistage.Tree uses for the exact scenario tree of
its own (different) chapter, restated here rather than imported (a draft cannot import another
chunk's draft). An Instance H n m T bundles a tree's node-varying LP data
(c, W, Tmat, h, p); Feasible/obj give its feasible set and objective. The exact
problem (1.1) is Instance H n m TFine for a fine/exact tree TFine; the aggregated problem
(1.2) is Instance H n m TCoarse for a coarser tree TCoarse, connected to TFine by an
aggregation map agg : TFine.Node → TCoarse.Node.
agg respects the tree structure (root, stage, ancestor);
W, c agree between the fine and coarse instances (up to agg);
coarse.h, coarse.Tmat are the p-weighted conditional expectations of fine.h, fine.Tmat over
each aggregation fiber;
∀ coarse nodes i,i' at the same stage sharing a "current-period outcome",
coarse.h i = coarse.h i' ∧ coarse.Tmat i = coarse.Tmat i'
⟹ zCoarse ≤ zFine
This is the mission's only formalization target: BRIEF.md records that no separately numbered
lemma precedes Theorem 1's proof in this section to serve as an independent milestone (the proof
is a direct LP-duality argument against the theorem's own hypotheses), and that Chapter 8's
Theorem 1 — the two-period case this theorem generalizes — is a cross-chapter dependency
belonging to Chunk 08's own mission, not a milestone here. milestones.yaml is accordingly empty;
see STATUS.md for the explicit accounting of what else in this chapter was considered and left
out (Theorem 3, the aggregation error bound of §10.2, an unrelated and substantially heavier
result).
Theorem 1 is what licenses every aggregation-based approximation scheme the rest of the book's
multistage material builds on: it says precisely when replacing a multistage recourse problem's
random data by within-period conditional expectations preserves a valid lower bound, and precisely
identifies the condition (aggregated nodes sharing a current-period outcome must carry identical
aggregated data) whose failure breaks the bound — a condition the book states is not decorative
("if not, then the conditional expectation form ... may not actually achieve a bound," p. 418).
Formalizing it gives Prove2Me a first structural result connecting Chapter 8's single-period Jensen
bound (Chunk 08) to genuinely multistage approximation, using the same finite-scenario-tree
deterministic-equivalent representation Chunk 06 uses for the exact nested Benders decomposition
— the two missions' shared representation choice (documented in both STATUS.md files) means a
future mission relating them formally (e.g. instantiating Chunk 06's exact tree as this mission's
TFine) has a compatible object to work with, even though neither imports the other's draft.
The theorem's proof (p. 419-420) is a direct LP weak-duality argument: given an optimal dual
solution to the aggregated problem, the book constructs a dual-feasible solution to the exact
problem attaining the same value, using precisely the "common outcome ⟹ equal aggregated data"
hypothesis to make the constructed dual solution well-defined across the exact tree's finer
structure. This is a real argument, not a citation, but it is left as sorry: formalizing the
proof would need the multistage LP duality machinery (the "multistage version of Theorem 3.13" the
book's own proof invokes, itself left as Exercise 1) that no chunk of this series has built. The
value of this mission is the faithful statement of the bound and its exact hypotheses.
(ωt−1,ωt) ∈ Stj if and only if there exist some (ω̂t−1,ωt) ∈ Stj" —
S^t_j appears on both sides of the "if and only if," where the sentence's own subject ("S^t_i
and S^t_j that have a common outcome") requires the left side to range over S^t_i. Confirmed
against a direct render of PDF page 436 (uv run --with pymupdf python), not assumed from OCR:
the PDF's own typesetting has this repetition, not an artefact of text extraction. This
formalization reads the corrected clause as "S^t_i and S^t_j project onto the same set of
period-t outcomes" and states it via an explicit label type Θ and curOutcome : TCoarse.Node → Θ, since the aggregated tree alone does not carry a literal per-period outcome
space to project onto (see Setting above — Tree records only history-node structure, not the
underlying product space Ω = Ω₁ × ⋯ × Ω_H).W, c shared exactly, not aggregated, matching the book's explicit assumption that the
recourse matrix and per-stage cost are deterministic and identical across (1.1) and (1.2)
("Wt known and not random," "ct = ct," p. 418) — formalized as direct equality hypotheses
(hW_agree, hc_agree) rather than folding W/c into the conditional-expectation machinery
that h/Tmat go through.zFine/zCoarse are hypothesis-characterized, not sInf-defined, avoiding the real
infimum's junk value 0 on an unbounded-below or empty feasible set
(reference/FAITHFULNESS_TRAPS.md trap 5) — neither tree-LP's feasible set is shown bounded or
nonempty by the hypotheses alone.p·h/p·Tmat, not h/Tmat
alone, matching the book's own E^{Sti}[·] = (h̄ti,T̄ti) read as "the fiber-sum of p·(h,T)
equals p_i·(h̄ti,T̄ti)" — the standard definition of a conditional expectation against counting
measure on a finite partition. Instance's own hp_pos (every node's probability is strictly
positive) rules out the degenerate case a bare unweighted equation would need to guard
separately (a coarse node of probability 0, which cannot occur, is what the read-back of this
theorem flags as the one case where the weighted equation would not pin down h_coarse/
Tmat_coarse themselves — moot here since hp_pos excludes it).coarse.h/coarse.Tmat
be arbitrary constants unrelated to fine.h/fine.Tmat (dropping the conditional-expectation
defining equations) would still typecheck a "lower bound" conclusion but assert nothing about
aggregation — exactly the risk BRIEF.md flags: "a formalization that treats (h̄ti,T̄ti) as
arbitrary constants rather than as conditional expectations over a partition of the scenario
space at time t loses the theorem's actual content." Both hCoarse_h/hCoarse_T (the
defining equations) and hCommonOutcome (the theorem's own extra hypothesis) are load-bearing
and present.Two-stage stochastic programs with recourse — choose a first-stage decision now, observe a random outcome , then choose a second-stage recourse decision to repair whatever left infeasible or suboptimal — are the workhorse model of the field, used for capacity planning, inventory and financial portfolio problems since the 1950s (Dantzig 1955; Beale 1955). When ranges over a finite set of scenarios, the recourse function that averages the second-stage cost over scenarios is piecewise linear and convex in , so the overall problem is itself a large linear program — but one whose constraint matrix has a scenario for every column block and can be far too large to hand to a general-purpose LP solver directly. Van Slyke and Wets' L-shaped method (1969), the subject of this mission, is the algorithm that made two-stage recourse problems with finite scenario sets practically solvable: it is Benders decomposition specialized to this block structure, alternating between a small master program over (and a scalar approximating the recourse cost) and, at each candidate , a batch of second-stage linear programs that either certify 's second-stage feasibility or supply a linear underestimate — a cut — of around . Birge & Louveaux's Introduction to Stochastic Programming (2nd ed., Springer 2011), Chapter 5 §5.1, gives the algorithm and proves its two central guarantees: a shortcut feasibility test for a special case (Theorem 1) and the algorithm's finite convergence in general (Theorem 2), which is this mission's goal.
A two-stage recourse instance consists of a first-stage feasible region for , and, for each of finite scenarios (occurring with probability ), second-stage data defining the recourse subproblem
where the recourse matrix is fixed — the same across every scenario, the case this chapter treats. is the set of for which every scenario's subproblem is feasible, and the two-stage problem is
A basis of the recourse subproblem is an injective choice of of 's columns (where is 's row count); each basis determines a simplex multiplier , and when attains the true optimum of , LP duality gives — the mechanism that turns a batch of second-stage LP solves into linear cuts on .
The L-shaped algorithm proceeds in three steps, repeated until neither applies:
Formalized as: starting from the empty cut set, there is a finite-length run of the algorithm's Step-1/2/3 transition relation, of length bounded by the total number of distinct feasibility- and optimality-cut witnesses available, ending at a state admitting no further step — at which point either the master program has become infeasible (certifying ) or its optimum is second-stage feasible, passes every fresh Step-3 test, and is optimal for the two-stage problem.
A shortcut avoiding separate feasibility LPs at Step 2: under these structural assumptions on , checking feasibility at the single componentwise-worst right-hand side certifies feasibility at every scenario simultaneously.
Van Slyke and Wets' method (and Benders decomposition more generally, of which it is the recourse-problem specialization) underlies essentially every large-scale two-stage stochastic program solved in practice, and its finite-convergence guarantee — not merely that an optimum exists, but that this specific cutting-plane procedure reaches it in finitely many outer iterations — is what makes the method a decision procedure rather than a heuristic. The proof's content is an explicit finiteness argument (the number of distinct simplex bases of the recourse subproblem and the feasibility-test LP is finite, so the algorithm cannot generate infinitely many distinct cuts before either exhausting the feasible region or converging), not a general compactness or fixed-point argument; formalizing it means formalizing the cutting-plane mechanism itself as a transition system and proving termination combinatorially, over the finite type of available bases, rather than proving only that some optimal exists.
The natural shortcut — state only "an optimal exists, or " — is not Theorem 2's actual content and is not what this mission targets: that weaker claim would already follow from being a nonempty polyhedron (or empty), with no reference to the algorithm at all, and would not require the finiteness-of-bases argument the book's proof turns on. The genuine difficulty is representing Steps 1-3 faithfully as a relation on accumulating cut sets, and pinning the termination bound to the actual combinatorial object the book cites (the finite set of bases of the two LPs the algorithm solves at each iteration) rather than to a numeral or an abstract compactness bound. A second, quieter difficulty is Step 1's own optimum: once optimality cuts exist, the master program optimizes jointly, but before the first one it optimizes alone; conflating the two (e.g. always requiring to be part of the optimum) does not match Step 1 as the book states it.
First-stage and second-stage vectors are Fin n1 → ℝ / Fin n2 → ℝ; the finite scenario set is
Fin K with probability vector p. A basis is {b : Fin m2 → Fin n2 // Function.Injective b} (m2 = the recourse matrix's row count), matching "an injective choice of columns of
"; its finiteness is definitional, from Fin m2 → Fin n2 being finite. Simplex multipliers use
Matrix.inv, whose junk value 0 on a singular matrix is never reachable in a proof because
multipliers are only ever used through an IsOptimalAt/IsFeasBasisOptimalAt hypothesis that
pins the basis to one genuinely attaining the LP's true optimum. The recourse value
is EReal-valued (reusing this series' Instance/QVal convention from Chunk 03), so an
optimality-cut witness's claimed value is compared to it by an explicit EReal cast, never by
EReal arithmetic. The algorithm's state is a pair of finite sets of witnesses recorded so far
(Finset (Fin K × FeasBasis n2 m2) × Finset (Fin K → Basis n2 m2)); Step is an inductive
relation with one constructor per Step-2 and Step-3 branch, each requiring its witness not already
recorded, and the goal states a bounded-length Step-path from the empty state to a state
admitting no further Step. This mission does not restate Chapter 3's polyhedrality fact
about as a separate lemma: the finiteness fact it is invoked for is already exposed directly
and structurally by the finite Fintype bound on the number of bases, so no additional axiom
stands in for it (see MODERATION_NOTES.md). Lemmas 3-9 and Theorem 10 of §5.2 (Regularized
Decomposition, a different algorithm) are out of scope. The trivializing formalization this
mission rules out is exactly the one named under Difficulty above: a bare existence-of-optimal-or-
infeasible- statement with no reference to Steps 1-3 or to a finite bound on the number of
iterations — such a statement would be true of any nonempty polyhedron and would not be Theorem 2.
Every regret guarantee through Chapter IX compares the algorithm to the single best fixed decision in hindsight. That comparison is meaningless when the environment itself changes: a commuter's best route differs on weekdays versus weekends, an investor's best portfolio differs in a bull versus a bear market. A standard sublinear-regret algorithm, competing against one static comparator, will converge to some average compromise between regimes — exactly the wrong behavior when the regimes are genuinely different. Chapter 10 develops adaptive regret, a strictly stronger performance metric that demands low regret on every contiguous sub-interval of time simultaneously, and an efficient algorithm (Simple-FLH) that attains it for any base OCO algorithm at only a logarithmic additive cost.
For a comparator sequence with path length , the dynamic regret measures performance against a moving target (§10.1). The chapter's central object, adaptive regret (Definition 10.2), instead takes the supremum of ordinary regret over every contiguous sub-interval :
An algorithm is strongly adaptive if its adaptive regret matches its ordinary regret up to logarithmic factors in (§10.2.1).
The chapter builds toward this via the Fixed-Share algorithm (§10.3, Algorithm 30) — a variant of Hedge for the discrete expert-tracking problem, adding a uniform exploration term to each round's multiplicative update so that no expert's weight can vanish entirely — and then lifts it (§10.4) to the continuous OCO setting via Simple-FLH (Algorithm 32): run one fresh copy of a base OCO algorithm per starting time , and apply Fixed-Share to this set of "experts."
Online gradient descent with constant step size satisfies, for every comparator sequence ,
Given -exp-concave losses, Fixed-Share with guarantees, for every interval and every expert ,
Simple-FLH guarantees
Theorem 10.6 answers §10.2.1's own question — are there algorithms simultaneously optimal in
ordinary regret and adaptive regret? — affirmatively and constructively: Simple-FLH pays only an
additive over whatever regret its base algorithm already achieves, for
any -exp-concave-loss algorithm (in particular, taking to be the Online Newton
Step algorithm of Chapter IV gives an adaptive-regret algorithm with no asymptotic cost at all).
This is the chapter's capstone reduction, structurally similar to Chapter IX's OCO-to-PAC
reduction: a generic wrapper around any algorithm in a broad class, converting one guarantee into
a strictly stronger one. No prior art was found on the platform for adaptive regret, dynamic
regret, or Fixed-Share (planning search: q=adaptive+regret, q=dynamic+regret,
q=tracking+regret — no hits); this mission drafts all three results fresh.
Theorem 10.1's proof adapts Theorem 3.1's telescoping-sum argument to a moving comparator, picking up an extra term that Cauchy–Schwarz and the diameter bound convert into the path length — a genuinely different quantity from regret, not a trivial corollary. Theorem 10.3's proof (Lemma 10.4, an exp-concavity-driven potential argument structurally parallel to Hedge's own analysis in Chapter I) tracks how the fixed-share exploration term prevents any expert's weight from decaying below a usable floor, so that even an expert active only over a short sub-interval still has enough accumulated weight at time for the argument to close — the sup-over-all-intervals form of the guarantee is exactly what this floor buys. Theorem 10.6's own proof is comparatively short (a direct application of Theorem 10.3 to Simple-FLH's experts, instantiated at the expert matching the interval's own start point), but depends on both of the preceding results' analyses for its correctness.
AdaptiveRegretT is stated as a genuine supremum over a finite index set (subintervals of
[0,T-1]), so it is a maximum, never a real-suprema-of-an-unbounded-set junk value — the chapter
brief's own flagged pitfall (do not state it as a sum or average). ExpConcave is redeclared
locally (Chapter IV's own exp-concavity is not yet a published series definition; see
MODERATION_NOTES.md). IsFixedShareRun gives expert decisions xi as external data (matching
the book's own treatment, where "an expert i suggests decision x^i_t" is not itself part of
Fixed-Share's specification) — Theorem 10.3 is drafted at this level of generality, applying to
Fixed-Share on any experts, matching how the book itself proves it once and reuses it for
Simple-FLH. The goal (Theorem 10.6) connects Simple-FLH's experts to the base algorithm A via
the one property the book's own proof actually uses — each expert's interval-regret bound
inherited from A — rather than mechanizing Algorithm 32's exact re-indexing formula for
starting a fresh copy of A at each round, which never enters the numerical bound; see
MODERATION_NOTES.md. Three of this chapter's headline results (Theorems 10.1, 10.3, 10.6) are
stated in the book with a bare O(·); per CAPTAIN_BRIEF.md rule 7 and BRIEF.md's explicit
guidance, this mission uses the explicit constant each proof actually derives instead (Theorem
10.1's own η-parametrized inequality before the unstated optimal choice of η; Theorems 10.3
and 10.6's own final displayed bounds before they are folded into O(·) notation).
Not formalized: Definition 10.2's own generalization to -shifting comparators (a remark, not a
numbered theorem), §10.2.1's tightness/lower-bound claims (left as exercises in the book, no
proof given), Lemma 10.4 (an intermediate step whose content is folded directly into Theorem
10.3's own explicit bound), and §10.5's starred FLH2 (Theorem 10.7, poly-logarithmic running
time) — an advanced, optional stretch goal per BRIEF.md, not attempted given the chapter's
non-starred primary goal (Theorem 10.6) was reachable within budget.
Von Neumann introduced amenable groups in 1929 to explain the Hausdorff–Banach–Tarski paradox, and showed that the class of amenable groups contains all finite and all abelian groups and is closed under four processes: (I) subgroups, (II) quotients, (III) extensions and (IV) directed unions. Day named the smallest class with these properties , the elementary amenable groups. For fifty years these were the only amenable groups anyone could exhibit, and von Neumann's question whether every non-amenable group contains a free subgroup on two generators — whether equals the class of groups without such a subgroup — was open. (It was answered in the negative by Ol'shanskii in 1980, the year of this paper, by different methods.)
Ching Chou's Elementary amenable groups (Illinois J. Math. 24 (1980) 396–407, doi:10.1215/ijm/1256047608) gives the structure theory of that everything later relies on. Its central result is that the class can be built from finite and abelian groups by extensions and directed unions alone — subgroups and quotients add nothing (Proposition 2.2). From that description three things follow: periodic elementary amenable groups are locally finite, so the periodic non-locally-finite groups of Golod and Novikov–Adjan show (Theorem 2.3); a finitely generated simple elementary amenable group is finite (Corollary 2.4); and Wolf's conjecture holds in : a finitely generated elementary amenable group is almost nilpotent or has exponential growth (Theorem 3.2, extending Milnor and Wolf's theorem for solvable groups). A final section introduces a packing property (P) of groups and proves it for every elementary amenable group (Proposition 4.2) and every residually elementary amenable group (Corollary 4.7).
On this platform the definition of is already published
(the bundle Chou_ElementaryAmenable, from the mission
Cannon–Floyd–Parry: Thompson's group F and the simplicity of its commutator subgroup),
together with the theorem that Thompson's group is not elementary amenable
(Theorem 4.10) and, from Brin and Squier, that has no free subgroup on two
generators (CannonFloydParry.no_free_subgroup_of_rank_two). This mission formalizes
Chou's paper on top of that definition.
The class and its constructible core. Chou.ElementaryAmenable G is an inductive
predicate on groups: finite groups and abelian groups are in the class, and the class is closed
under isomorphism, subgroups, quotients, extensions and directed unions of subgroups; each rule
is a constructor of the published bundle Chou_ElementaryAmenable, where it is stated precisely. Chou builds the hierarchy
by transfinite recursion, applying only extensions and directed unions to the finite and
abelian groups, and proves that is closed under subgroups and
quotients, hence equals . The union is realised here without
ordinals, as the inductive predicate Chou.Constructible, whose constructors are of_finite,
of_commGroup, of_mulEquiv, extension and directedUnion; Chou's transfinite induction
over becomes structural induction over a derivation, with the same case analysis.
Periodic and locally finite groups. A group is periodic if every element has finite order
(Mathlib's IsMulTorsion) and locally finite if every finitely generated subgroup is finite
(Chou.IsLocallyFinite). Day's class is Chou.NoFreeSubgroupOfRankTwo: no homomorphism
from the free group on two generators into is injective.
Growth. For a finite generating set of , Chou.wordBall S n is the set of products
of at most factors, each in or with inverse in . has exponential growth if for
some finite generating set the ball of radius has at least elements for some
and all ; it is exponentially bounded if for some finite generating set and every
the balls are eventually smaller than . Chou works with for products of exactly
elements of a finite generating set ; for symmetric and containing the identity the
two agree, and Wolf's observation that the growth type is independent of the generating set is
one of the milestones. "Almost nilpotent" is Mathlib's Group.IsVirtuallyNilpotent: a
nilpotent subgroup of finite index. A free subsemigroup on two generators means two elements
such that distinct positive words in are distinct in
(Chou.HasFreeSubsemigroupOfRankTwo).
Packings. A pair of subsets is a packing of if is a
bijection (Chou.IsPacking), and has property (P) if every finite
subset lies in a finite for which some is a packing (Chou.HasPackingProperty).
is residually elementary amenable if every survives in some elementary amenable
quotient (Chou.ResiduallyElementaryAmenable).
The goal is Chou's description of the class, Proposition 2.2 (b) (p. 397): “ is the smallest
class of groups which contains all finite groups and all abelian groups and is closed under
processes (III) and (IV).” It is stated as the equivalence ElementaryAmenable G ↔ Constructible G.
The milestones follow the paper's order.
Section 2. Proposition 2.1 in two halves — the constructible groups are closed under subgroups and under quotients — which is the whole proof of the goal. Theorem 2.3: periodic elementary amenable groups are locally finite; and its consequence that is nonempty. Corollary 2.4: finitely generated simple elementary amenable groups are finite.
Section 3. Lemma 3.1 (an extension of almost nilpotent by almost nilpotent is almost nilpotent or of exponential growth), Theorem 3.2 and Rosenblatt's sharpening Theorem 3.2′, together with the facts Chou uses on the way: a finite-by-nilpotent group is almost nilpotent; a free subsemigroup forces exponential growth; Wolf's independence of the generating set; and Milnor's existence of the growth rate, in the form "exponentially bounded means not of exponential growth".
Section 4. Property (P) for finite groups, for , for finitely generated abelian groups; Lemma 4.1 (directed unions and extensions preserve (P)); Proposition 4.2 (every elementary amenable group has (P)); Lemma 4.6 (a) and Corollary 4.7 (residually elementary amenable groups have (P)); and the free groups.
Chou's Section 3 rests on results the paper cites rather than proves, none of which is in Mathlib. They are stated here as milestones in their own right, so that the dependence is visible and each is a well-defined target: the Milnor–Wolf theorem (a finitely generated solvable group that is exponentially bounded is almost nilpotent); M. Hall's theorem that a finitely generated group has finitely many subgroups of each finite index; that finitely generated nilpotent groups are finitely presented and that a group with a finitely presented subgroup of finite index is finitely presented; Milnor's Lemmas 1–2 in the form Chou states on p. 400 (in a finitely generated exponentially bounded group, a normal subgroup with finitely presented quotient is finitely generated); and Rosenblatt's variant of Lemma 3.1. Section 4 needs one more: free groups are residually finite. Lemma 3.1 and Theorems 3.2, 3.2′ can be closed only once these are; every other milestone is provable from Mathlib and the published library.
Two remarks on Theorem 2.3. Chou's witness for is a periodic group that is not locally finite (Golod; Novikov–Adjan), whose existence is not formalized. The platform already holds a different witness: Thompson's group is not elementary amenable (Cannon–Floyd–Parry, Theorem 4.10) and has no free subgroup on two generators (Brin–Squier); both are published and proved, and the milestone is proved from them. The inclusion itself is von Neumann's theorem that amenable groups contain no free subgroup of rank two, which passes through the definition of amenability and is not part of this mission.
The ordinal-indexed hierarchy and the remark that it stabilises at some (Proposition 2.2 (a)) are replaced by the inductive predicate. Chou's two examples of finitely generated groups in that are not almost solvable (p. 402), the Golod–Shafarevich discussion, and Lemma 4.6 (b) (ordinal-indexed normal series) are omitted. Propositions 4.3–4.5 on almost convergent sets, and Milnor's remark that exponentially bounded groups are amenable, need invariant means on ; amenability itself is the subject of Garrido I.
Given independent random variables , when does converge? Not absolutely — that question is settled by and is usually too strong. The interesting question is when the partial sums converge for almost every outcome, and here independence buys something that holds for no general sequence: convergence is not a delicate matter of cancellation but is decided, once and for all, by three numerical series.
Chapter 2 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) reaches this in section 2.5. Kolmogorov's three-series theorem fixes a truncation level , replaces each by , and asserts that converges almost surely if and only if
Three deterministic conditions on the distributions decide an almost-sure question about paths, and the answer does not depend on which is chosen. Through Kronecker's lemma this is also the route to the strong law of large numbers, which is how the chapter uses it.
Let be independent real random variables on a probability space, with partial sums . Say that converges almost surely when for almost every the sequence has a real limit; following Durrett, " converges" means exists, not that it converges absolutely.
Three tools from the same section support the theorem. Kolmogorov's maximal inequality strengthens Chebyshev from to the maximum of the whole path,
for independent, centred, square-integrable summands. From it comes the convergence criterion: if and then converges almost surely. Kronecker's lemma is the deterministic bridge to averages: if and converges then . And the Hewitt–Savage 0-1 law says that for an i.i.d. sequence every permutable event — one unchanged by rearranging finitely many coordinates — has probability or .
Both directions are asserted, as Durrett states the theorem. The truncation level is arbitrary and fixed in the statement; that the three conditions hold for one exactly when they hold for every is a consequence, not an assumption.
Kolmogorov's maximal inequality (2.5.5); the convergence criterion under summable variances (2.5.6); Kronecker's lemma (2.5.9); and the Hewitt–Savage 0-1 law (2.5.4).
The result itself. The three-series theorem is the complete answer to a question that has no complete answer without independence, and the shape of the answer is the interesting part: a pathwise, almost-sure property is equivalent to three conditions each computable from the marginal distributions alone. Each of the three does a separate job — the first says and its truncation differ only finitely often, so Borel–Cantelli lets them be exchanged; the second controls the drift of the truncated sums; the third controls their fluctuation. The theorem is also the standard route to the strong law: applying it to and then Kronecker's lemma gives , which is why section 2.5 sits where it does.
Formalizing it. Mathlib has the strong law of large numbers (strong_law_ae), both
Borel–Cantelli lemmas, and Kolmogorov's 0-1 law for the tail σ-field. It has none of the
following: Kolmogorov's maximal inequality, the almost-sure convergence criterion for random
series with summable variances, Kronecker's lemma, the Hewitt–Savage 0-1 law, or the three-series
theorem. The mission therefore contributes the whole of section 2.5, and the pieces are reusable
well beyond it — the maximal inequality and Kronecker's lemma in particular are standard tools with
no probabilistic content in the second case at all.
The maximal inequality is the step where the argument stops being routine. Chebyshev bounds and no more; controlling the maximum over the whole path needs the first passage decomposition and the observation that is measurable with respect to the first variables while is independent of them, so the cross terms vanish. That is a stopping-time argument in disguise, and it is what makes the whole section work.
The sufficiency half of the goal is then assembly: the third series and the convergence criterion give convergent, the second adds the means back, and the first plus Borel–Cantelli replaces by . Necessity is the harder direction, and Durrett does not prove it in Chapter 2 at all — he defers it to Example 3.4.12, where it follows from the Lindeberg–Feller central limit theorem. A solver attacking the goal should expect the reverse implication to need machinery from outside this section.
The Hewitt–Savage law has a difficulty of its own kind: the natural statement is about a σ-field of events on a sequence space, and the proof approximates a permutable event by cylinder events and then applies the permutation that swaps the first coordinates with the next .
Random variables are measurable real-valued functions on a probability space and independence is
Mathlib's iIndepFun. Variance is Mathlib's variance, and square-integrability is stated as
membership in where the maximal inequality and the convergence criterion need it. The
three-series theorem itself assumes no integrability: the truncated variables are bounded, so
their means and variances exist automatically, which is exactly why the truncation is there.
" converges" is formalized as convergence of the sequence of partial sums to a real
limit, not as Summable, which in Mathlib means unconditional and hence absolute convergence for
real series. This distinction is not pedantic here: condition (ii) of the theorem is convergence of
in Durrett's sense and would be a strictly stronger condition if read as
summability. Conditions (i) and (iii) are series of non-negative terms, where the two notions
agree, and are stated as Summable.
Almost-sure convergence of is "for almost every there exists a real with " — the limit is not asserted to be measurable in , and does not need to be for the statement to say what it should.
For the Hewitt–Savage law the sequence space is the countable product carrying
the infinite product of copies of one law, which is Mathlib's Measure.infinitePi, and a
permutable event is a measurable set invariant under every finitely supported permutation of the
coordinates. That is Durrett's exchangeable σ-field stated directly rather than constructed as a
σ-field object.
Contributions welcome beyond the listed items: the converse direction via Lindeberg–Feller (Example 3.4.12); the derivation of the strong law from the three-series theorem and Kronecker's lemma; the Marcinkiewicz–Zygmund law (2.5.12); and the rates of convergence of section 2.5.1.