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.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
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?
Most equations that arise in applications cannot be solved in closed form: the age of the Moon from a radioactive-decay balance, the deflection of a clamped beam, the equilibrium of a catenary, all reduce to solving for a function with no algebraic inverse. A first course in numerical methods therefore opens with root finding: constructive procedures that produce a sequence of approximations together with a theorem saying that the sequence converges to a root and how fast.
This mission is the first in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (Departamento de Computação e Estatística, UFMS, 2000). It covers Chapter 3, Zeros de Funções, whose capstone is the local convergence of Newton's method.
Let and let be a zero of , i.e. . The chapter studies three constructions.
Bisection. Starting from an interval with , put and keep the half of on whose endpoints still changes sign. The width of the bracketing interval is halved at every step.
Linear iteration (MIL). Rewrite as a fixed-point equation and iterate from an arbitrary .
Newton's method. Take the particular iteration function
obtained by truncating the Taylor expansion of at after the linear term.
A sequence has order of convergence when tends to a finite constant, where ; is linear and quadratic convergence.
The goal theorem is the local convergence of Newton's method at a simple zero. If is twice differentiable on an open interval containing , its second derivative is continuous there, and never vanishes on , then there is such that
where is the Newton sequence started at . This is the formal content of the chapter's statement that Newton's method converges provided the initial guess is chosen close enough to the root.
The milestones are the supporting results of the chapter: the error bound and convergence of bisection, the convergence of the linear iterative method under a derivative bound , the a posteriori estimate , and the quadratic order of Newton's method at a simple zero.
Bisection, fixed-point iteration and Newton's method are the three root finders every numerical-analysis course starts with, and the three convergence theorems above are what justifies using them. The a posteriori estimate is what turns the iteration into an algorithm with a stopping criterion: it bounds the distance to the root by a quantity the program can measure. The quadratic order statement explains the observed doubling of correct digits per step at a simple zero and its loss at a multiple zero.
On the formalization side, Mathlib already has a fixed-point theorem for contractions on complete spaces and the mean value theorem, but not the statements in the form used in numerical analysis: bisection with its explicit bracket, the a posteriori bound, or Newton's local convergence and quadratic rate stated for the concrete iteration sequence. This mission asks for those.
The delicate point in all three theorems is that the iterates must be known to stay in the region where the hypotheses hold; the informal proofs assume this silently. For the linear iterative method the mission therefore states the invariance hypothesis explicitly ( maps the closed interval into itself). For Newton's method, no such hypothesis is given: the existence of a neighbourhood of that the iteration preserves is part of what must be proved, and it comes from the continuity of together with . The quadratic-order milestone also has to handle the degenerate possibility , which would put a zero in the denominator; it is excluded by hypothesis.
Everything is over the real numbers. The iterations are given as explicit recursive sequences: the bisection construction returns the bracketing pair and its midpoint, and there are separate sequences for the fixed-point and Newton iterations. Newton's method takes the derivative as a separate function argument , tied to by a hypothesis of the form " has derivative at every of the interval"; this avoids relying on any junk value of a derivative operator where fails to be differentiable. Division is total, so a step at a point where vanishes would leave the iterate unchanged; the hypotheses exclude this inside the interval.
Two deliberate deviations from the source are worth flagging for the auditor. First, Proposição 3.5.1 assumes only for , but its proof divides by ; the formal statement assumes on the whole interval, so is a simple zero. Second, the convergence statement for the linear iterative method adds the hypothesis that maps the closed interval into itself, without which the iterates may leave the region where the derivative bound is assumed.
A table of values is all one has of many functions: measurements, tabulated physical constants, the output of an expensive simulation. Interpolation reconstructs a function between tabulated points by passing a polynomial through them, and it underlies much of the rest of numerical analysis — quadrature rules, finite-difference formulas and predictor-corrector schemes for differential equations are all obtained by integrating or differentiating an interpolating polynomial. What makes the reconstruction trustworthy is a formula for the error committed away from the nodes.
This mission is the fifth in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (UFMS, 2000). It covers Chapter 7, Interpolação.
Let be distinct nodes and the tabulated values of a function . The Lagrange form of the interpolating polynomial is
so that for every , and is the unique polynomial of degree at most with this property.
The interpolation error at a point that is not a node is the difference .
The goal theorem is Proposição 7.3.1: if is times differentiable on and all nodes lie in , then for every different from all nodes there exists with
The milestones are the other results of the chapter needed to make sense of it: the existence and uniqueness of the interpolating polynomial of degree at most through points with distinct abscissas (Proposição 7.2.1), the fact that the Lagrange formula does interpolate the data, and the practical error bound of Proposição 7.3.2, when .
The error formula is the reason interpolation is a numerical method and not just a curve-drawing device: it shows that the error is governed by two independent factors, the smoothness of through and the geometry of the nodes through the product . Everything downstream follows from it — the and error terms of the trapezoidal and Simpson rules in the next mission are obtained by integrating exactly this expression, and the choice of Chebyshev nodes is the attempt to make the product factor small.
The standard proof introduces the auxiliary function with chosen so that , and then applies Rolle's theorem times to conclude that vanishes somewhere. Formalizing the repeated application of Rolle's theorem, keeping track of the distinct zeros and the nested intervals they generate, is the substance of the work; it is an induction that has to be organized carefully rather than a computation.
The nodes are given as a strictly increasing family of reals lying in the open interval , and the interpolating polynomial is the explicit Lagrange sum rather than an abstract polynomial: at a node it is defined by the same formula, whose factors then include contributions unless the nodes are distinct, which is why the distinctness hypothesis appears in the interpolation milestone. Smoothness is expressed as continuous differentiability of order on the open interval , and the derivative appearing in the error term is the iterated derivative computed within that set; since the set is open this agrees with the ordinary -st derivative. The evaluation point is assumed to lie in and to differ from every node; the point is asserted to exist in , with no claim of uniqueness or of any relation to beyond membership in the interval. The uniqueness milestone is stated with Mathlib's polynomial type and the degree bound , which includes the zero polynomial.
Reinforcement learning formalizes a scenario supervised learning cannot: an agent that actively interacts with an environment, choosing actions that change both the state it observes next and the reward it receives, rather than passively receiving an i.i.d. labeled sample. Every practical treatment of this scenario — from classical dynamic programming to modern deep reinforcement learning — is built on the Markov decision process (MDP), a model in which the effect of an action depends only on the current state, not on the full history that led to it. Two questions define the theory this mission covers: given a fixed way of acting (a policy), what value does it obtain, and how is that value actually computed rather than merely characterized as the solution of a fixed-point equation? Mohri, Rostamizadeh and Talwalkar's chapter 17 answers both for the stationary, infinite-horizon discounted case, and this mission targets its two central results: that a fixed policy's value is not just characterized but uniquely determined by a linear system with an explicit closed-form solution (Theorem 17.10), and that the optimal value function — obtained instead by choosing the best action at every state — can be computed by an iterative algorithm guaranteed to converge regardless of where it starts (Theorem 17.11).
A (finite) Markov decision process consists of a finite set of states , a finite set of actions , a transition kernel giving the distribution over the next state after taking action at state , and an expected reward for that transition. A (stationary) policy assigns each state a distribution over actions — possibly, but not necessarily, a point mass on a single action. Fixing turns the MDP into an ordinary Markov chain on : at each step the agent is at some state , draws , receives (expected) reward , and moves to a state drawn from . For a discount factor , the value of at is the expected discounted sum of future rewards starting from ,
and the state-action value function is the analogous quantity for taking at and then following . Marginalizing the raw kernel and reward over the mixed action gives the induced transition matrix and induced reward vector — the objects that turn 's value into a genuinely linear-algebraic quantity. A policy is optimal if for every policy and every state ; write for its value function.
Theorem 17.10 (goal). For a finite MDP and a fixed policy , the matrix (with the policy-induced transition matrix) is invertible, and 's value function is the unique solution of the Bellman equations, given in closed form by
Proposition 17.9 (milestone). The value function itself satisfies the linear system that Theorem 17.10 solves:
Theorem 17.7 (milestone). A policy is optimal if and only if it places probability only on -maximizing actions: for every with , .
Theorem 17.11 (milestone). The Bellman optimality operator , , is a -contraction for ; consequently, for any starting vector , the value-iteration sequence converges to a fixed point of .
Theorem 17.10 is what makes policy evaluation on a finite MDP an exact, finite computation rather than an infinite limit: instead of summing an infinite discounted series or solving an implicit fixed-point equation numerically, a single matrix inversion gives the policy's value at every state simultaneously. It is also the base case every planning algorithm in the chapter builds on: policy iteration alternates optimizing a policy with exactly this evaluation step. Theorem 17.11 gives the complementary guarantee for the harder problem of finding the optimal value function directly, without fixing a policy first: value iteration converges from any starting point, with a convergence rate ( iterations for -accuracy) that follows from the same contraction argument. Together, the two results are the mathematical content behind why dynamic-programming planning for finite MDPs is tractable at all — the discount factor , not any structural assumption on rewards or transitions, is what buys both the uniqueness in Theorem 17.10 and the convergence in Theorem 17.11. Formalizing them requires reproducing this linear-algebraic and metric content precisely, not just asserting the conclusions: an invertibility claim asserted without the operator-norm argument, or a convergence claim without the contraction property, would state something true by fiat rather than the book's actual result. No faithful prior art exists on the platform for this exact model (see Formalization scope).
The obvious shortcut for Theorem 17.10 is to assert is invertible without proof — true, but not what the book does, and not informative about why it holds. The genuine content is that , being row-stochastic (every row of sums to exactly , since and are both proper distributions), has operator norm exactly, so strictly; this rules out as an eigenvalue of , which is exactly what invertibility of requires. The same fact, applied differently, drives Theorem 17.11: showing is -Lipschitz requires bounding by comparing the maximizing action for against the same action's value under (not 's own maximizer), since the two suprema need not be attained at the same action — a step easy to state incorrectly as a direct comparison of two maxima. Both theorems fail if is allowed: the discounted setting's central asset, a strict contraction, disappears exactly at that boundary.
States and actions are modeled as finite types (Fintype S, Fintype A); the raw kernel and
reward P : S → A → S → ℝ, Er : S → A → ℝ are unconstrained functions, with IsTransitionKernel
asserting the required distribution property explicitly rather than assuming it silently. A
policy is π : S → A → ℝ with IsPolicy π asserting π s is a distribution over A for every
s — deliberately not π : S → A or a PMF-valued function, since Theorem 17.7's own
quantifier ("for any pair (s,a) with π(s)(a) > 0") requires treating π(s) as a genuine
mixture. PolicyValue is defined as the actual infinite discounted expectation (via an explicit
state-occupation-distribution recursion), not as the Bellman fixed point — so that Proposition
17.9 (the value function satisfies the linear system) and Theorem 17.10 (that system has a
unique, invertible-matrix solution) are both non-vacuous claims about the same object, rather
than one being definitionally true of the other. The trivializing formalization this rules out
is asserting IsUnit (1 - γ • P) as a bare hypothesis, or defining V_π as (1-γP)⁻¹R and
calling the resulting identity a theorem; both would erase the mission's actual content.
Two platform modules model related MDPs (BertsekasSSPModel, a stochastic-shortest-path model
with a termination-probability deficit rather than exact row-stochasticity, and
FoundationsRL.RLBasics, a finite-horizon episodic model indexed by layer) — neither
specializes exactly to this chapter's stationary, always-continuing, infinite-horizon discounted
convention, so every definition here is drafted fresh rather than imported. This chunk covers
§17.2–17.4.2 (the MDP model, policy value, Bellman's equations, value and policy iteration);
§17.4.3 (the linear-programming formulation) and §17.5 (stochastic-approximation learning
algorithms — TD(0), Q-learning, SARSA) are out of scope, since they require a
stochastic-approximation convergence substrate this mission does not build.
Ranking is the learning problem behind search engines, recommendation systems and fraud-alert
triage: what matters is not a single classification decision but the relative order the system
assigns to a set of items, because a user or analyst can only act on the very top of a ranked
list. Chapter 10 develops margin-based generalization theory for the score-based ranking
setting, transplanting chunk 05-svm's single-sample Rademacher-complexity machinery to a
genuinely two-sample structure: a ranking example is a pair of points, one drawn from each of
two positions, and the chapter's bound must therefore control two marginal complexities rather
than one. It also introduces RankBoost, the ranking analogue of AdaBoost, with a boosting-style
empirical-error guarantee proved by the same normalization-factor telescoping argument as
chunk 07's AdaBoost bound, adapted to RankBoost's own pairwise per-round quantities.
A ranking example is a pair (x,x') drawn from a distribution D over X×X, labeled by a
preference function f; restricted to {-1,+1} labels (the simplification §10.2 adopts), a
scoring function h:X→ℝ misranks (x,x') when f(x,x')(h(x')-h(x)) ≤ 0 (Eq. 10.1/10.2). The
empirical margin loss R̂_{S,ρ}(h) (Eq. 10.3) uses the same Φ_ρ (Definition 5.5) as chunk
05-svm, restated locally here. Writing S1, S2 for the two coordinate projections of a
pair sample S, and D1, D2 for the corresponding marginals of D, R_m^{D1}(H) and
R_m^{D2}(H) are the Rademacher complexities of H under each marginal (p. 241). Theorem
10.1 bounds R(h) in terms of these two Rademacher-complexity terms, both in their population
form (R_m^{D1}, R_m^{D2}) and their empirical form (R̂_{S1}, R̂_{S2}), via chunk 03's
Theorem 3.3 applied through an auxiliary hypothesis family H̃ = {((x,x'),y) ↦ y[h(x')-h(x)]}.
Corollary 10.2 specializes this to kernel-based linear scoring hypotheses; §10.4 introduces
RankBoost (Figure 10.1), whose per-round weighted pairwise-outcome fractions ε_t^+, ε_t^-
(Eq. 10.11) play the role AdaBoost's single ε_t plays in chunk 07, and Theorem 10.3 bounds
RankBoost's empirical error in terms of them. Corollary 10.4 combines Theorem 10.1 with Lemma
7.4 (the convex hull of H has the same empirical Rademacher complexity as H, restated as a
standing fact of the boosting series) to give RankBoost's own margin-based guarantee.
Theorem 10.1 — the mission's goal. For H a set of real-valued functions, ρ>0, δ>0,
with probability at least 1-δ, for all h∈H:
Corollary 10.2 (milestone). For a PDS kernel K with r an upper bound on K(x,x),
feature map Φ, and H = {x↦w·Φ(x) : ‖w‖≤Λ}, fixed ρ>0: R(h) ≤ R̂_{S,ρ}(h) + 4√(r²Λ²/ρ²/m) + √(log(1/δ)/(2m)).
Theorem 10.3 (milestone). RankBoost's empirical error verifies R̂_S(f) ≤ exp(-2∑_t((ε_t^+-ε_t^-)/2)²), and ≤ exp(-2γ²T) if the edge is uniformly at least γ>0.
Corollary 10.4 (milestone). Theorem 10.1's first bound, applied to h∈conv(H).
Theorem 10.1's proof is the chapter's genuine new technique, not a restatement of chunk 05's
Theorem 5.8: the two-sample decomposition (splitting the supremum over H̃ into a term on x'
alone and a term on x alone, each bounded by the Rademacher complexity under its own
marginal) is what the 2/ρ · (R_m^{D1}+R_m^{D2}) structure expresses, and collapsing it to a
single-sample bound would either be false or silently assume D1=D2 (which only holds for a
symmetric D, an assumption the theorem does not make). Corollary 10.2 is the direct
theoretical basis for the ranking SVM algorithm §10.3 derives. Theorem 10.3 mirrors chunk
07-boosting's Theorem 7.2 almost line for line in its proof technique (the same telescoping
product of normalization factors Z_t), but with genuinely different per-round quantities
(ε_t^+, ε_t^- rather than a single ε_t) that must not be conflated with AdaBoost's own, per
BRIEF.md's pitfall note. Corollary 10.4 is what makes RankBoost's output (a linear, not
convex, combination — normalized by ‖α‖_1) provably generalize independently of the number of
boosting rounds T, the ranking analogue of chunk 07's Corollary 7.5. No prior art exists on
the platform: GET /theorems?q=ranking%20loss returns zero hits.
Theorem 10.1's proof needs the two-sample structure carried through explicitly: H̃'s
Rademacher complexity splits, via the sub-additivity of sup and the fact that y_iσ_i and
σ_i have the same distribution, into a term on S2 alone and a term on S1 alone — treating
a ranking sample as an ordinary single sample (chunk 03's single-hypothesis-set machinery
applied naively) would drop this structure entirely and is exactly the pitfall BRIEF.md
names. Theorem 10.3's proof requires Z_t = ε_t^0 + 2√(ε_t^+ε_t^-) be bounded via the identity
4ε_t^+ε_t^- = (1-ε_t^0)^2 - (ε_t^+-ε_t^-)^2 and the inequality 1-x ≤ e^{-x} — the same
telescoping-normalizer technique as AdaBoost's Theorem 7.2, but RankBoost's own D_t,
ε_t^+, ε_t^- genuinely differ (they are defined via pairwise outcomes y_i(h(x'_i)-h(x_i)) ∈ {-1,0,+1}, not a single-point disagreement h(x_i)≠y_i) and must be modeled as their own
recursively-defined algorithm state, not obtained by substitution into chunk 07's AdaBoost
Lean.
MarginLossFunction restates chunk 05-svm's Definition 5.5; EmpiricalRademacherComplexity/
RademacherComplexity restate chunk 03-rademacher-vc's Definitions 3.1/3.2; IsPDS restates
chunk 06-kernels's PDS-kernel definition; ConvHull restates chunk 07-boosting's convex-hull
definition — all duplicated rather than imported since a draft item cannot import another
chunk's draft module, and none is listed as reusable in missions/README.md's "Published
definitions" table at the time of this session. D1, D2 are computed directly as
Measure.map Prod.fst D/Measure.map Prod.snd D rather than posited via a separate marginal
hypothesis, so the theorem statement itself pins down that they are genuinely the marginals of
the sampling distribution D, not independent parameters. Corollary 10.2's r is an explicit
upper bound on K(x,x) (hrK : ∀ x, K x x ≤ r) rather than a literal sSup, per BRIEF.md's
pitfall note about the possibly-infinite supremum — the theorem's conclusion is monotonic in
r, so this is not a weakening. RankBoost's D_t, ε_t^+, ε_t^-, α_t, Z_t and returned
function f are modeled as their own recursively-defined algorithm state (mirroring chunk
07's AdaBoostDist/AdaBoostEpsilon/AdaBoostEnsemble pattern exactly, but built from
RankBoost's own pairwise-outcome quantities, never by substituting into the AdaBoost Lean, per
BRIEF.md's pitfall note) — RankBoostEpsilonPlus/RankBoostEpsilonMinus are already tied to
RankBoost's own D_t and selected base ranker, so Theorem 10.3 needs no separate hypothesis
connecting them (the same trivialization guard chunk 07's own Theorem 7.2 documents). No
numerical constant is altered from the book in any of the four theorems.
Not formalized: §10.3's ranking-SVM primal/dual optimization problems (an algorithm derived
from Corollary 10.2, not a generalization-theoretic result); §10.4.2 (RankBoost as coordinate
descent, an algorithmic-equivalence argument, not a generalization bound); §10.5 (bipartite
ranking, its own distinct problem formulation with a different generalization error, Eq. 10.20,
explicitly out of scope per BRIEF.md); §10.6-10.7 (preference-based ranking, other criteria),
out of scope per BRIEF.md. The uniform-over-ρ extension mentioned after both Theorem 10.1's
and Corollary 10.2's proofs (referencing Theorem 5.9's technique from a different chapter) is
not drafted, matching chunk 09-multiclass's identical scope decision for the analogous remark.
In the Standard Model the scalar sector consists of a single complex doublet. The general Two-Higgs-Doublet Model (THDM) replaces it by two complex doublets of the same weak hypercharge . This is the minimal extension of the scalar sector that is still renormalisable and gauge invariant, and it is forced on any supersymmetric completion: the Minimal Supersymmetric Standard Model has exactly two Higgs doublets. Before any phenomenology can be done with such a model, two questions have to be answered for the given parameter point: is the scalar potential stable, i.e. bounded from below, and does its global minimum break down to the electromagnetic ?
The general THDM potential has real parameters, and answering these questions directly in field space — eight real scalar degrees of freedom, of which three are gauge — is unwieldy. Maniatis, von Manteuffel, Nachtmann and Nagel (2006) proposed a reformulation in terms of gauge-invariant bilinears, in which the gauge orbits of the Higgs fields are parametrised by a Minkowski-type four-vector confined to the closed forward light cone, and the potential becomes a quadratic polynomial on that cone. In these variables the stability question reduces to a one-variable problem: the sign of an explicit rational function on a finite set of at most ten real numbers. This mission formalizes that analysis: the gauge-orbit parametrisation (their Theorem 4), the classification of the stationary points of the potential (their Theorem 2), and the stability criterion itself (their Theorem 1).
Write the two doublets as rows of a complex matrix,
and form the hermitian matrix of gauge-invariant scalar products , i.e. . Decomposing in the Pauli basis gives four real functions
Positive semi-definiteness of is equivalent to and : the four-vector lies on or inside the forward light cone. A gauge transformation acts as with , and leaves invariant.
The most general gauge-invariant renormalisable potential is
with real parameters , and a real symmetric matrix . For one sets , so that , and
Stationary points of on the ball are governed by the functions
where is a Lagrange multiplier for the constraint . The finite set collects: every regular with ; the point when ; and every eigenvalue of at which stays finite and . It has at most ten elements, and is exactly the set of stationary values of .
For the stationary points of the full potential one uses four-vector notation , , and the metric , so that on the domain , , with .
For the potential is stable for , marginal for and unstable for . For ,
and if on with equality somewhere, the sign of — replaced by when is an eigenvalue of — decides between stability in the weak sense and instability.
Theorem 4 (gauge orbits); the four stability cases (a), (b.2), (b.3), (b.4) of Section 4 including the criterion for the marginal case; equation (4.39) identifying the stationary values of with ; equations (4.42)–(4.44) giving at those stationary points; and Theorem 2, the classification of the stationary points of .
The criterion is a decision procedure: given the parameters of a THDM, stability is settled by evaluating one rational function at the roots of another, without any search in field space. The authors use it to re-derive the known stability conditions for the MSSM potential and to settle the stability and symmetry-breaking properties of the THDM potential of Gunion et al., for which , and come out as the strong-stability conditions. Theorem 4 is what makes the whole approach legitimate: it says that nothing is lost in passing from fields to the invariants , because the fibres of that map are exactly the gauge orbits.
The results are established in the published literature; what this mission adds is machine-checked proofs. The statements are not present in Mathlib in any form, and the note added in version 3 of the paper — a condition for the marginal case that was missing in the original version — is a concrete reminder that the case analysis here is easy to get subtly wrong.
The obvious route to stability is to minimise directly; it fails because the domain is a cone with a boundary, and the minimisation over the boundary introduces a Lagrange multiplier whose admissible values are the roots of , including the degenerate "exceptional" solutions where is singular. Those exceptional solutions are not a technicality: they are where the eigenvalue clauses of , the correction in (4.43), and the junk-value behaviour of matrix inverses all live. The marginal case ( and vanishing simultaneously somewhere) is not decided by the signs alone and needs the quantitative bound .
Vectors in are plain functions Fin 3 → ℝ with an explicitly defined dot product; is a Matrix (Fin 3) (Fin 3) ℝ and its symmetry is carried as a hypothesis. Four-vectors are indexed by Unit ⊕ Fin 3 so that and are block matrices, with the first component being . Higgs configurations are complex matrices and ; a gauge transformation is with .
Stability is formalized as the honest statement that is bounded from below on the physical domain , — not as any of the sign conditions that the theorem derives — so none of the implications is true by definition. Matrix inversion in Lean returns the zero matrix at a singular argument; every occurrence of is therefore guarded by a regularity hypothesis, and the values of at an eigenvalue of are defined as limits, with the existence of those limits part of the membership condition for . The projection is characterised by its defining property (it lies in the eigenspace and is orthogonal to it) rather than by a choice of eigenbasis.
A complete development needs linear algebra over (resolvents, symmetric matrices, eigenspaces), and the spectral decomposition of positive semi-definite complex matrices for Theorem 4, and elementary real analysis (compactness of the ball, limits of rational functions) for Section 4. The gauge-orbit statement and the light-cone parametrisation are reusable for any multi-doublet scalar sector; contributions of the -doublet generalisation (Appendix B, Theorem 5) are welcome as follow-ups.
Every convergence-rate result in the preceding chapters is an upper bound: some specific estimator (the Lasso, PCA, kernel ridge regression) achieves a given error rate. A natural and much harder question is the complementary one: is that rate actually the best any procedure could achieve, no matter its computational cost? Answering this requires a theory of lower bounds that holds simultaneously for every conceivable estimator — a fundamentally different kind of argument from constructing and analyzing one particular algorithm. Wainwright's High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 15, develops this theory, unifying classical techniques (Le Cam, Assouad, Fano) under one reduction: converting continuous estimation into discrete hypothesis testing.
Let be a sample space and a class of probability distributions on . A functional assigns each distribution a parameter of interest. An estimator is a measurable map . Fix a semi-metric — symmetric, triangle-inequality-satisfying, , but possibly for — and an increasing . The minimax risk is
the smallest worst-case expected loss achievable by any measurable estimator (Eq. (15.2)).
Given a 2δ-separated set
(every pair satisfies ) with representative distributions
, Wainwright constructs a testing problem: sample
uniformly from , then ; write for the resulting joint law of
. A test function attempts to recover from ; its
error probability is .
For any increasing and any 2δ-separated set with its induced joint testing measure
,
This mission formalizes Proposition 15.1 alone (see Formalization scope below for why, and what a follow-up mission would add to reach Fano's method proper, Proposition 15.12).
Proposition 15.1 is the single reduction every subsequent technique in the chapter specializes: Le Cam's two-point method (Lemma 15.9, , bounding the testing error via total variation distance), Fano's method (Proposition 15.12, bounding it via mutual information and Fano's inequality), and Assouad's method (a different, hypercube-based packing). Formalizing it in full generality — general , general semi-metric, general -ary packing set — gives a single reusable lemma that a future mission proving any of these specific bounds can build on directly, rather than re-deriving the reduction each time.
The theorem is already proved in the source; this mission's contribution is a machine-checked formal statement (and, eventually, proof) of the reduction, in a form composing with any future formalization of the chapter's testing-error bounds (total variation, Fano, or otherwise).
The proof combines two ingredients that must each be kept in their sharpest form: Markov's inequality applied to (which only needs increasing, not convex or any specific shape — a premature specialization to would silently prove a weaker, less reusable statement), and the reduction of any estimator to a test via nearest- packing-point assignment (Eq. (15.4)), which uses the triangle inequality on in a specific direction (bounding from below via and ) to show that a small estimation error forces the induced test to be correct. Getting the direction and strictness of every inequality right — non-strict separation, but strict distance in the "test is correct" event — is where a naive restatement goes wrong.
, are arbitrary measurable spaces; the distribution class is
realized as an indexed family measure : Idx → Measure 𝒳 rather than a bare set of measures,
composing directly with θ : Idx → Ω. The semi-metric is a bare function with explicit
nonnegativity/reflexivity/symmetry/triangle-inequality hypotheses, matching the book's own
footnote definition, rather than Mathlib's PseudoMetricSpace typeclass (kept self-contained,
no extra instance machinery). The minimax risk is valued in ENNReal via the lower Lebesgue
integral ∫⁻, not the Bochner integral, specifically to avoid the non-integrable-loss junk
value 0 that a Bochner-integral formalization would silently introduce — a trivializing
formalization would use ∫ (Bochner) here, letting a non-integrable loss vanish and making the
inequality easier to satisfy than the book's actual claim; this mission does not do that. The
joint testing measure is characterized by its slice-measure equations directly on the
product space , avoiding Mathlib's general conditional/disintegration
machinery while remaining exactly equivalent to " uniform, ".
Disclosed major scope decision. BRIEF.md recommended Proposition 15.12 (the Fano bound
itself, Φ(δ)(1 - (I(Z;J)+\log 2)/\log M)) as this mission's goal. That statement requires, in
addition to everything above, a formalized notion of mutual information between a
finite-valued and a general (possibly continuous) random variable, and its use of a Fano-type
inequality (Eq. (15.31), itself deferred by the book to "Section 15.4" and not fully quoted in
the brief). Building a faithful mutual-information formalization general enough for this
setting (finite , arbitrary measurable ) — matching Mathlib's or this repo's existing,
narrower information-theoretic developments (SourceCoding.*, built for a different,
channel-coding purpose per BRIEF.md's own prior-art note) or building one from scratch — is
substantially more than this session's remaining budget after building and self-reviewing
08-pca and 07-sparse-linear. This mission instead formalizes Proposition 15.1, the
foundational reduction Proposition 15.12 itself specializes (via a particular bound on
), so that a follow-up mission can add the mutual-information/Fano
step on top of HighDimStat.Minimax.estimation_to_testing without redoing this reduction.
This mission's name, fixed from missions/README.md, still names "Fano's Method" as the
series slot this chunk occupies; its actual content is the reduction step every method in that
family (including Fano's) shares — recorded explicitly here and in STATUS.md, not left
implicit.
Regression is usually taught with a fixed parametric model: linear regression fits a -dimensional coefficient vector, and the estimation error is controlled by . Many regression problems in practice have no such finite-dimensional description — the regressor is only known to be, say, convex, monotone, or smooth, and the estimator is a least-squares fit over the (infinite-dimensional) set of functions with that shape. This is nonparametric regression, and the basic question is the same as in the parametric case: how close is the fitted function to the truth, as a function of the sample size ? Answering it requires replacing "dimension" with a genuinely functional notion of complexity, since an infinite- dimensional function class can still be small enough to estimate well (a Sobolev ball) or too large to estimate at all. The theory in this mission, due to van de Geer and developed in Chapter 13 of Wainwright (High-Dimensional Statistics: A Non-Asymptotic Viewpoint, Cambridge University Press, 2019), gives a single non-asymptotic template — the localized Gaussian complexity — that answers this question for an arbitrary star-shaped function class, and recovers the familiar parametric and Sobolev/RKHS rates as special cases.
Fix design points in an arbitrary covariate space (fixed, not random — this is the fixed-design setting) and observe
where is the unknown regression function, is a known noise level, and are i.i.d. standard Gaussian. Given a class of candidate functions, the nonparametric least-squares estimate is any minimizer
Error is measured in the empirical (design-dependent) seminorm . A class of functions is star-shaped if and together imply — every convex class containing the origin has this property, and it is the minimal structural assumption under which the theory below applies. For a star-shaped class and radius , the local Gaussian complexity
measures how much a mean-zero Gaussian process can be made to look like a member of restricted to the ball of radius . A critical radius is any positive solution of ; by Lemma 13.6, is non-increasing on star-shaped, so this inequality always has a smallest positive solution.
Lemma 13.6. For any star-shaped , is non-increasing on , and consequently has a smallest positive solution for every .
Theorem 13.5 (special case, ).
Theorem 13.13 (goal — general oracle inequality, not assumed in ). With solving the critical inequality for , there are universal constants such that for all ,
with probability at least . The goal is deliberately the statement with unresolved universal constants and an infimum over , rather than any single instantiated bound, so the target survives sharper constant tracking.
Theorem 13.13 is the "master" result behind essentially every concrete rate in the chapter: orthogonal series regression, convex/monotone regression, and (via the KRR specialization of Section 13.4) kernel ridge regression rates for Sobolev and Gaussian-kernel classes are all obtained by bounding for a particular and reading off . Its value is that it isolates exactly the one place where the geometry of enters — the local Gaussian complexity — while the probabilistic argument (a peeling/chaining argument controlling a localized empirical process) is generic. Formalizing it produces, for the first time on the platform, the statement-level infrastructure (star-shaped classes, local Gaussian complexity, critical radius) that any future mission on a concrete nonparametric-regression rate — kernel ridge regression, convex regression, isotonic regression — can specialize, without re-deriving the oracle inequality from scratch. The proof itself (concentration of Gaussian complexity via Borell-TIS/Gaussian comparison plus a peeling argument over dyadic scales) is not attempted here; only the statement is formalized, as a draft goal for future proof contributions.
The naive route to Theorem 13.13 is to bound pointwise via the basic inequality and then bound the right side by for — but is itself random (it depends on the estimate), so this is circular: the bound on the right depends on the very quantity being bounded. The chapter's actual argument resolves this with a peeling device: partition the event space by which dyadic annulus falls into, and apply a uniform (non-circular) bound on each annulus separately via Gaussian concentration, summing a geometric series of tail probabilities. This is the step every first attempt misses, and it is why the local Gaussian complexity — rather than the simpler global complexity of Chapter 4/5 — is the right object: localizing to radius is what makes the per-annulus bound tight enough for the final sum to converge.
Design points are an arbitrary type X (no topology or metric structure is needed for the
statements themselves); the least-squares estimate is represented as a Prop
(IsLeastSquaresEstimate) picking out any function achieving the empirical minimum, matching
the book's "any minimizer" phrasing rather than assuming uniqueness. The local Gaussian
complexity is defined as an expectation over an explicit i.i.d.-standard-Gaussian noise vector
on an abstract probability space, with the inner supremum taken over the subtype of the
radius-restricted slice of the class — this is well-defined (not the junk value 0 of an
unbounded Set ℝ supremum) whenever the slice is nonempty, which holds automatically for any
nonempty star-shaped class (taking exhibits in the class). Since neither X nor
H carries a topology, separability or countability constraint, SatisfiesCriticalInequality
adds an explicit Integrable hypothesis on that same supremum (added in revision), guarding
against Mathlib's Bochner integral silently returning the junk value 0 for a non-measurable
integrand — a value that would otherwise trivially satisfy the critical inequality for every
positive δ, regardless of the function class's actual local complexity. The trivializing
formalization to rule out here is stating Theorem 13.13's universal constants after the
quantification over the function class and sample size, which would let
secretly depend on the instance and make the "universal" claim vacuous; this mission places
the constant quantifiers first, before the class, design and noise data they must not depend
on. A complete downstream development would add: the concentration-of-Gaussian-complexity step
(Borell–TIS or a comparable tail bound), the peeling argument, and the metric-entropy /
Dudley-integral machinery of Section 13.2.1 for bounding explicitly on concrete classes
(Sobolev balls, RKHS balls) — none of which is attempted here.
Every convex optimization algorithm in machine learning — from projected gradient descent to support vector machines to the mirror-descent methods of later chapters of this book — is justified by a small set of optimality certificates: a checkable condition on a candidate solution that guarantees it actually solves the problem, without searching the whole feasible set. The most widely used such certificate is the Karush–Kuhn–Tucker (KKT) system: a set of gradient and complementary-slackness equations that a solution of a convex program with differentiable data must satisfy, and that (under a mild constraint qualification) is also sufficient. It is the tool a practitioner reaches for to check optimality of a numerical solver's output, and the tool a theorist reaches for to derive an algorithm (dual ascent, augmented Lagrangian, interior point methods) in the first place. Every convex machine learning model introduced in Chapter 1 of this book — regularized least squares, support vector machines, logistic regression with constraints — is an instance of the general convex program these milestones analyze.
The result traces back to Kuhn and Tucker's 1951 paper Nonlinear Programming, with Karush's 1939 unpublished thesis establishing the same conditions independently and earlier; Slater's 1950 unpublished note is the source of the constraint qualification that bears his name and that makes the necessity direction possible. Lan's Chapter 2 gives a compact, modern, purely finite-dimensional derivation of the whole chain — separation, duality, saddle points, KKT — from first principles, self-contained in about twenty pages, aimed squarely at the convex programs that appear in machine learning.
Fix and work in with its standard inner product . A convex program (2.3.16) is
where is a nonempty closed convex set, are convex, and are affine. A point is feasible if it satisfies every and ; is optimal if it is feasible and for every feasible .
The normal cone of at is — the set of directions that make an obtuse angle with every direction into from ; it is when , recovering unconstrained first-order optimality. The Lagrangian is for multipliers , ; the Lagrange dual value is , and the Lagrange dual problem is . Weak duality, , holds unconditionally by construction. Slater's condition asks for with , ; the restricted Slater condition weakens the interior requirement to the relative interior while keeping strict inequality for every (here: every) nonlinear constraint.
Each of these five is stated the way the book states it — no constant is hard-coded, no O(·) is involved, and every hypothesis (closedness, convexity, Slater/restricted-Slater) is exactly the one the corresponding proof uses.
The KKT system is the interface between convex optimization theory and every algorithm that
exploits it: primal-dual methods track approximate KKT residuals as a stopping criterion, and the
derivation of the Lagrange dual (used throughout the book's later treatment of composite and
constrained problems) rests on strong duality, milestone strong_duality here. The saddle-point
characterization (saddle_point_sufficient/saddle_point_necessary) is the standard route to
designing an algorithm: a method that provably drives a pair to a saddle point
of is provably convergent to an optimal , without ever needing to verify optimality
directly against the primal problem.
None of the six substantive results here has a machine-checked proof on Prove2Me. The platform
holds a genuinely weaker unconstrained-in- condition (OnlineConvexOpt.ConvexBasics. kkt_optimality, Hazan's Theorem 2.2: for ,
with no inequality/equality constraints or multipliers at all) and a structurally different,
strictly more general cone-based Lagrange-duality development (VectorSpaceOpt.lagrange_duality
and VectorSpaceOpt.lagrangian_saddle_sufficient_pointed, from Luenberger, which bundle all
constraints into a single map into a convex cone in a general normed space, rather than Lan's
explicit inequality / equality split). Formalizing this mission
produces the finite-dimensional convex-program version of KKT in exactly the shape it is used and
taught: separate multiplier vectors for inequality and equality constraints, an explicit normal
cone rather than a cone-map abstraction, and both directions of the necessity/sufficiency split.
The separation theorem (Theorem 2.1) itself is routine once the projection onto a closed convex set is available. The real difficulty is entirely in the direction of the Convex Theorem on Alternative that Proposition 2.9 states: the naive idea — "insolvability of (I) should give a separating hyperplane between and directly" — fails, because these are sets in and separating them there does not produce a sign-definite multiplier vector. Lan's proof instead lifts to and separates the epigraph-like set from the open orthant-like set ; only in this lifted space does the separating normal's sign constraint (forced by 's unboundedness in the positive directions) translate into . Getting the sign of the -th coordinate strictly positive — needed to normalize and divide — is itself a small separate argument using the Slater subsystem's solution. The KKT necessity direction (the goal) then chains three of these already-nontrivial results (separation → CTA → strong duality → saddle necessity) before translating the saddle-point condition on into the gradient/normal-cone form via differentiability of at .
All milestones are stated over EuclideanSpace ℝ (Fin n) with Convex/ConvexOn from Mathlib.
Affine equality constraints are represented by explicit witnesses with , so that is
available without a separate affine-differentiability lemma. The normal cone is Lan's
own primal-space object (normalCone); the restricted Slater condition uses Mathlib's
intrinsicInterior ℝ X for , distinct from the plain interior X used by
the un-restricted Slater condition of Theorems 2.6/2.7(b). Primal optimal values and Lagrange dual
values are stated via IsGLB/pointwise-inequality forms rather than raw sInf, so that no
hypothesis is silently made true by an empty or unbounded set defaulting sInf to a junk value —
in every milestone here the relevant set is guaranteed nonempty by the Slater-point hypothesis
already present.
A trivializing formalization this mission rules out: stating kkt_necessary/kkt_sufficient
with (no set constraint) and empty (no functional constraints) would
collapse the normal-cone condition to and make the whole KKT apparatus vacuous
of any duality content; the milestones here keep , and as genuine free parameters (the
theorems are stated for arbitrary m, p : ℕ, including but not restricted to the degenerate case)
so that the constrained content of Lan's theorem is what gets proved.
Reusable beyond this mission: normalCone and lagrangian are generic enough that any later
chapter of this book needing Lagrangian duality or normal-cone stationarity (none of the current
first-wave chapters 03/06 needs them directly) could import them once published rather than
redeclaring. Contributions most welcome on the two hardest milestones,
cta_solvable_of_insolvable and kkt_necessary, since they carry the mission's real difficulty;
separation_point_closed can likely be discharged quickly via Mathlib's
geometric_hahn_banach_point_closed.
Many statistical problems — nonparametric regression, density estimation, dimension reduction, testing — are naturally posed as optimization over a space of functions rather than a finite-dimensional parameter vector. Hilbert spaces provide the right generality: they carry an inner product and a norm, so notions of projection, orthogonality and least-squares fitting all make sense, exactly as in ordinary Euclidean space, even though the "vectors" are now functions. Reproducing kernel Hilbert spaces (RKHSs) are the particular class of function-valued Hilbert spaces that make this program computationally tractable: they are generated by a single bivariate kernel function, and every RKHS computation reduces to evaluating that kernel, never to manipulating an infinite-dimensional object directly (the "kernel trick"). Wainwright's High-Dimensional Statistics (2019), Chapter 12, develops the foundational correspondence between kernels and Hilbert spaces that makes this possible, and this mission formalizes its two central theorems.
A Hilbert space is a complete inner product space (Definitions 12.1–12.2); this mission
uses Mathlib's own NormedAddCommGroup/InnerProductSpace ℝ/CompleteSpace typeclasses for
this notion throughout. A linear functional is bounded if
for some and all ; the Riesz representation theorem
(Theorem 12.5) says every such functional is for a unique .
A bivariate function is a positive semidefinite (PSD) kernel (Definition 12.6) if it is symmetric and every finite Gram matrix is positive semidefinite — the natural generalization of a PSD matrix to a (possibly infinite) index set , with no topological structure on required. A reproducing kernel Hilbert space (RKHS) for a kernel is a Hilbert space of functions on such that, for every , the function belongs to and
— the reproducing property. Equivalently (Definition 12.12), is an RKHS exactly when every evaluation functional is bounded on .
Given any PSD kernel function on any set , there is a Hilbert space (embedded into functions on ) in which satisfies the reproducing property (12.3) — and this Hilbert space is unique: any two Hilbert spaces with this property for the same are linearly isometric via an isometry intertwining their embeddings into functions on .
Theorem 12.11 is the theorem that makes the entire RKHS apparatus well-posed: every time a statistician writes down a kernel — linear, polynomial, Gaussian — Theorem 12.11 guarantees that a canonical Hilbert space of functions exists in which that kernel reproduces, so that optimizing over "the RKHS associated with " is a well-defined problem, not merely a suggestive shorthand. Theorem 12.13's converse shows the correspondence is exact — the class of kernel-generated Hilbert spaces is exactly the class of function spaces with bounded evaluation, the class relevant to any statistical application that samples a function at finitely many points. Together, these two results are the foundation the book's own later chapters build directly on: Chapter 13's nonparametric least-squares oracle inequality, and Chapter 14's kernel density estimation, both work by optimizing over an RKHS and are only well-posed because of this correspondence. Mercer's theorem, in turn, is what connects the RKHS viewpoint back to the earlier feature-map viewpoint of Chapter 12.2.2 (Eq. 12.2): the eigenfunctions give an explicit feature map into realizing , and its expansion is what later underlies the book's discussion of kernel PCA and of RKHS balls as ellipsoids in -coordinates.
The formalization difficulty is concentrated in getting the type of the existence-and-
uniqueness claim right, not in any single hypothesis. A Hilbert space is not naturally a
subtype of a fixed ambient space in Lean, so "the Hilbert space " of Theorem 12.11 is
formalized as an abstract type together with its own NormedAddCommGroup/InnerProductSpace ℝ/CompleteSpace instances, connected to "a space of functions on " via an injective
linear embedding into — and uniqueness must then be stated as an isometric
equivalence between any two witnessing Hilbert spaces that respects this embedding, the
faithful rendering of the book's own proof, which literally shows two candidate Hilbert spaces
are equal as sets of functions. A second subtlety is keeping Theorem 12.11's hypotheses
(a bare PSD kernel, no topology on ) cleanly separated from Mercer's theorem's additional
compactness, continuity and measure-theoretic apparatus — the two theorems are frequently
conflated informally, but the book is explicit that Theorem 12.11 needs none of Mercer's
structure.
is an unconstrained Type* for Theorem 12.5, 12.11 and 12.13 — no topology, matching the
book's own generality. Mercer's theorem (Theorem 12.20) additionally requires [MetricSpace X] [CompactSpace X] [MeasurableSpace X] [BorelSpace X] and a finite measure P, matching its
own compactness/continuity/measure-theoretic hypotheses exactly, never applied outside that
scope. The integral operator of Eq. (12.11a) is presented as an abstract linear map on
Lp ℝ 2 P tied to the defining integral formula via an explicit hypothesis, rather than
constructed as a def, since constructing it as a genuine well-defined operator (needing
integrability and a.e.-measurability arguments) is proof content, not definitional content,
and this mission's definitions file is sorry-free by convention. Mercer's orthonormal-basis
index type is existentially quantified over a countable ι (∃ (ι : Type) (_ : Countable ι), ...) rather than fixed to ℕ, since L²(X;P) can be finite-dimensional for finite X
(Example 12.18/12.21), where no infinite orthonormal basis exists; the uniform-convergence
conjunct is correspondingly quantified over every bijection e : ℕ ≃ ι (vacuous when ι is
finite, a genuine order-independent claim when ι is countably infinite). A trivializing formalization
of this chapter would state only existence in Theorem 12.11 and drop uniqueness (explicitly
warned against by this chapter's own brief), or state Mercer's convergence merely pointwise
or in rather than absolutely and uniformly; this mission avoids both. Out of scope: the
constructive proof detail of Theorem 12.11 (the explicit span-and-complete construction is proof
content, not part of the statement), the chapter's worked kernel examples (linear, polynomial,
Gaussian kernels, Examples 12.7–12.9), and the further consequences of Mercer's theorem
(Corollary 12.26 on RKHS-ball ellipsoids, the feature-map connection of Eq. 12.14) — all natural
follow-on work for a future mission on kernel-based nonparametric regression (Chapter 13,
mission 13-nonparametric-ls), which restates whatever RKHS objects it needs locally rather
than importing this mission's draft, per this book's series-wide convention.
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.
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.
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.
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.
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 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.
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.
A network of resistors solves an optimization problem. Nobody tells the electrons what to do; each one moves under a purely local rule, and the current distribution that emerges minimizes energy dissipation over all distributions satisfying Kirchhoff's node law. Add a wire and the network can only become easier to traverse. This is the encouraging case, and Chapter 4 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) opens with it.
Road traffic is the discouraging case. Drivers also follow a local rule — take the fastest route — and the pattern that emerges is again characterized by an optimization problem, but not the one anyone wants solved. Braess's paradox is the sharp form of the discrepancy: in a small road network carrying six cars per unit time, every route takes 83 time units at equilibrium; open an extra road, and at the new equilibrium every route takes 92. Building road capacity made everyone slower. The difference from the electrical case is that a driver's choice imposes a delay on everyone else sharing the road and the driver does not pay for it, and correcting that — pricing the externality — is how a decentralized rule can be made to produce good global behaviour. That idea recurs in Chapters 7 and 8 of the book as the basis of Internet congestion control.
The network is a set of directed links. A route is a subset of links, and is the set of routes under consideration — not necessarily all physically possible ones. The link-route incidence matrix has when and otherwise. Writing for the flow on route , the flow on link is
Each link has a delay function , continuous and increasing in the flow on that link, and the delay along a route is the sum of the delays of its links, . Drivers care only about getting from origin to destination: is the set of source–destination pairs, each route serves exactly one of them, written , and the flow requirement between pair is .
A routing pattern is stable when no driver has an incentive to switch. Definition 4.2 makes this precise: a Wardrop equilibrium is a feasible vector of route flows such that
Every route actually carrying traffic is a shortest route, in delay, for the traffic it carries.
The goal asserts existence only, for an arbitrary network, arbitrary route set and arbitrary continuous increasing delay functions. It fixes no uniqueness claim, because the equilibrium flows need not be unique even though the link loads are, and no efficiency claim, because Braess's paradox is precisely the statement that the equilibrium is not efficient.
Kirchhoff's node law as the equations satisfied by the expected reward in the random-walk game of section 4.1; the two Braess networks of Figures 4.4a and 4.4b, with their equilibrium delays and ; convexity of for increasing ; the optimization characterization that makes the goal reachable — a minimizer of over the feasible flows is a Wardrop equilibrium; and the exact externality decomposition of the queueing network of section 4.3.1.
The result itself. Theorem 4.3 is what makes the Wardrop equilibrium a usable object: a traffic model that could fail to have an equilibrium would be describing nothing. Its proof does more than establish existence — it identifies the equilibrium as the solution of a specific convex program, minimizing . That function is not the total delay , and the gap between the two is exactly Braess's paradox: selfish routing optimizes the wrong objective. Once the two objectives are written side by side, the fix is readable off them, and it is the fix used in practice — a toll on link equal to , the marginal delay a driver imposes on everyone else, makes the selfish objective coincide with the social one. Section 4.3 then carries the same accounting into queueing and loss networks, where the derivative of the mean cost splits into a term for the delay a customer suffers and a term for the knock-on cost it inflicts.
Formalizing it. Nothing here is open; Wardrop stated the principle in 1952 and Beckmann, McGuire and Winsten gave the optimization formulation in 1956. What the mission produces is a machine-checked model of selfish routing — incidence matrix, link flows, delay functions, the equilibrium condition — and a formal record of Braess's paradox as a concrete pair of networks rather than a story. Mathlib has no traffic or congestion-game theory.
Existence is not a fixed-point argument in the obvious variable: the best-response map of the routing game is not continuous, since a small change in flows can flip which route is shortest and move all the traffic. The book's route is to replace the equilibrium condition by the stationarity conditions of a convex program on a compact feasible set, where existence is routine and the content is the translation. The translation is where the care is needed, and it is stated here as a separate milestone: the first-order conditions say the Lagrange multiplier equals the route delay on routes carrying traffic and is a lower bound on the others, which is Definition 4.2 restated.
The subtlety worth naming in advance is that "increasing" is doing real work in two different places. It makes convex, which is what makes the program tractable; and it is what makes each interpretable as a price. Neither convexity of itself nor strict monotonicity is needed, and assuming them would be assuming more than the book does.
Links, routes and source–destination pairs are indexed by finite types. The incidence matrix is real-valued with entries constrained to be or , matching the book's definition in this chapter (unlike Chapter 3, which allows general non-negative integers). The map from routes to source–destination pairs is given as a function rather than as the matrix , which is exactly the book's statement that each column of sums to .
Delay functions are total functions , continuous and monotone. This excludes the vertical asymptote that Figure 4.5 permits — a link with a finite capacity at which delay blows up — and that restriction is recorded here rather than left implicit. The equilibrium condition is stated as the inequality " for every serving the same pair", which is Definition 4.2 with the minimum written out; the two are equivalent because itself serves , and the inequality form avoids having to produce a minimum over a possibly empty set.
The goal is not vacuous: the feasibility hypotheses (, and each source–destination pair served by at least one route) are exactly what makes the feasible set non-empty, and without them the existence claim would be false rather than trivial.
Contributions welcome beyond the listed items: uniqueness of the equilibrium link loads ; the marginal-cost toll that aligns the selfish and social optima; Rayleigh monotonicity (Exercise 4.3, that effective resistance does not decrease when a resistance is increased); the price of anarchy for affine delays; and Theorem 4.6 on the derivatives of the loss-network rate of return with respect to offered traffic and capacity.
A queueing network is a collection of service stations through which customers — jobs, packets, telephone calls, patients — move one at a time. The state of such a network is a vector of occupancy counts, one per station, and the number of states grows exponentially in the number of stations, so solving the equilibrium equations directly is hopeless for any network worth modelling. The product form is what rescues the subject: for a large and identifiable class of networks the equilibrium distribution factorizes into one term per station, as if the stations were independent, and a network of stations costs one-dimensional calculations instead of one exponentially large one.
Chapter 2 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) establishes this for migration processes, the Markov model in which individuals move between colonies one at a time at a rate that factorizes as : a part depending only on the two colonies and a part depending only on the occupancy of the source. The class covers single-server and -server queues, infinite-server queues, and networks of them, open or closed.
There are colonies, and a state is a vector of non-negative integers, being the number of individuals in colony . Three operators move one individual:
An open migration process is the Markov process on with transition rates
where : nothing leaves an empty colony. Immigration into colony is Poisson of rate . Taking and and restricting to states of a fixed total gives a closed migration process. Setting models an -server queue at colony ; models individuals moving independently.
The traffic equations define from the rates. In the open case they are
and in the closed case with and . Finally set
If then
is an equilibrium distribution: it satisfies the equilibrium equations for the open migration rates, and it sums to one over . Both halves are asserted, because the first alone is satisfied by every positive multiple of and the second is what makes the convergence hypothesis do work.
The closed-network product form of Theorem 2.4; the two families of partial balance equations (2.3) and (2.4) that the proof reduces to; Theorem 2.9, that the time reversal of a stationary open migration process is again an open migration process with rates , and ; the single M/M/1 queue that the chapter starts from; the cycle identity (2.6) behind Little's law; and the traffic equations of Kendall's family-size process, an open migration process with infinitely many colonies.
The result itself. Theorem 2.8 says that at a fixed time the occupancies of an open migration network are independent, each distributed as if its colony were fed by a Poisson stream of rate — even though the actual arrival stream into a colony is in general not Poisson, and the occupancies are emphatically not independent as processes. That gap between the one-time-marginal and the process is the reason the theorem is useful and the reason it is easy to misapply. Everything downstream in the book rests on it: the loss networks of Chapter 3 are the truncation of a product-form process to a capacity set, and the flow-level models of Chapter 8 ask when a product form survives a bandwidth-sharing policy. Theorem 2.9 supplies the reversibility argument from which Burke's theorem and the Poisson character of the exit streams follow.
Formalizing it. The mathematics is classical — Jackson (1957), Whittle (1968), Kelly (1979) —
and none of it is open. What the mission produces is a machine-checked model of a queueing
network: the migration operators, the rate matrix, the traffic equations and the product form, in
a form later missions in this series import rather than restate. Mathlib has no queueing theory
and no theory of continuous-time Markov chains on a countable state space, so this is the first
such development. It builds on the DetailedBalance / FullBalance layer published in mission I.
An open migration process is not reversible — the detailed balance equations fail, as Figure 2.5 of the book shows with an arrival stream of geometrically sized bursts — so the method of Chapter 1 does not apply and the equilibrium equations must be met head on. The content of the proof is that they split: a separate balance holds for each colony (rate of individuals leaving colony equals rate arriving into it) and one more across the boundary with the outside world, and each of those is equivalent to a traffic equation. Finding that split is the step, and it is why the partial balance equations are milestones in their own right.
The formal obstacle is different and worth naming. The equilibrium equation at a state sums over the states that can jump into , and the naive transcription silently assumes is a state, which fails when . Over such a term must be dropped, and a formalization that keeps it — with read as truncated subtraction — states something false.
The state space is Fin J → ℕ, a function from a finite index type of colonies to occupancy
counts, with J finite; no irreducibility is assumed, since none of the statements below need it.
Rates are real-valued and the whole rate matrix is a single function of two states, assembled as a
sum of indicator terms over the possible transitions, so the equilibrium equations can be stated
as the FullBalance predicate of mission I, with unconditional sums over the countable state
space. This is what avoids the trap above: a sum over actual states never includes a
would-be-negative one, and any spurious coincidence of operators at a boundary carries a
factor and contributes nothing.
Conventions the development commits to: , so a transfer is always between distinct
colonies; and for ; ; and is asserted
via HasSum, which states convergence and the value at once, rather than as an extended real that
might be infinite. Occupancy vectors use truncated natural subtraction, so the partial balance and
reversed-rate statements carry an explicit where the book's state space carries it
implicitly; the goal itself does not need such a guard.
A trivializing formalization is ruled out by the second conjunct of the goal: the equilibrium equations alone are a homogeneous linear condition satisfied by , whereas the requirement that sum to forces the constants to be exactly the ones stated.
Contributions welcome beyond the listed items: Burke's theorem (2.1) and the Poisson character of the exit streams, Corollary 2.10, the closed-form of the telephone banking example (Exercise 2.6), the Chinese restaurant process of Exercise 2.13, and Bartlett's theorem (2.17) on linear migration processes over a general space.
Many hard combinatorial optimization problems — finding the maximum cut of a graph, deciding the ground state of an Ising spin system, bounding the correlation of a physical system — can be written as maximizing a bilinear form over sign vectors . Exhaustive search over sign patterns is intractable, so practitioners relax the problem: replace each sign by a unit vector in a higher-dimensional space and optimize the resulting inner products instead. This relaxation, a semidefinite program, is convex and solvable in polynomial time. The question is how much is lost in the relaxation — whether its optimal value can be far from the true, combinatorial optimum.
Grothendieck's inequality, proved by Alexander Grothendieck in 1953 in the context of Banach space theory (Résumé de la théorie métrique des produits tensoriels topologiques, Bol. Soc. Mat. São Paulo 8 (1953), 1–79), answers this for a broad class of such relaxations: replacing signs by unit vectors in an arbitrary Hilbert space changes the optimal value by at most an absolute, dimension-free constant factor. The inequality has since become a standard tool across combinatorial optimization, Banach space geometry, and (via the Goemans-Williamson algorithm for maximum cut, Section 3.6 of the source) approximation algorithms; see U. Haagerup, The Grothendieck inequality for bilinear forms on -algebras, Adv. Math. 56 (1985) for the tightest known constant, and Alon–Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35 (2006), for the algorithmic connection this mission's Theorem 3.5.6 sets up.
Fix positive integers . Consider a real matrix . Say is normalized if for every choice of numbers ,
This says , viewed as a bilinear form on , has sup-norm at most . Now let be any real Hilbert space — a real vector space equipped with an inner product complete in the induced norm — and consider vectors and , each of unit norm . Replacing the scalar product by the inner product in the same bilinear form gives , a real number depending on the choice of and of the unit vectors. The question is how large this can be, uniformly over every such choice.
for every real Hilbert space and unit vectors , where is a constant depending on neither , its dimensions, nor . This mission's goal formalizes the book's own first-pass bound (Section 3.5), proved by a Gaussian truncation argument; it does not fix a numeral for , only that some absolute constant works, matching the shape of the true statement rather than a specific numeral that a sharper argument (the book's own Section 3.7 gives ) would immediately obsolete. See Formalization scope below for why this is the goal, not the sharper bound.
The result itself. Grothendieck's inequality is the single fact that makes semidefinite relaxation a provably good algorithmic strategy rather than a heuristic: whatever the true, hard-to-compute combinatorial optimum of a -valued bilinear optimization is, the tractable Hilbert-space relaxation cannot overshoot it by more than the constant . Milestone Theorem 3.5.6 makes this concrete for positive-semidefinite matrices, showing the semidefinite relaxation SDP of the integer program INT satisfies INT SDP INT — the guarantee underlying the Goemans-Williamson 0.878-approximation algorithm for maximum cut (Theorem 3.6.5 of the source, out of scope for this mission; see Formalization scope).
Formalizing it. The inequality and its two chapter milestones are proved but not previously
formalized on this platform (checked by concept search for "Grothendieck", "semidefinite",
"positive-semidefinite", and "max-cut" — no hits beyond the unrelated Grothendieck-Teichmüller
group). What remains after this mission is the sharper argument of Section 3.7
(the "kernel trick"), a separate, heavier development building on positive-definite kernels,
and full proofs of every milestone below (currently open sorry goals).
The statement of Grothendieck's inequality contains no randomness, yet every known elementary proof is probabilistic; this is itself a striking feature of the result. The obvious approach — bound directly by exploiting the normalization hypothesis on — fails because the normalization hypothesis only controls against sign vectors, and there is no way to project an arbitrary unit vector in a Hilbert space onto without losing information. The book's proof instead represents each unit vector via a scalar Gaussian random variable for a single Gaussian vector , recovering the inner products in expectation (Exercise 3.3.5); but these Gaussian variables are unbounded, so the normalization hypothesis (which bounds against bounded inputs) cannot be applied to them directly. The core technical step is a truncation argument: splitting each Gaussian variable into a bounded part and a small--norm unbounded remainder, applying the hypothesis to the bounded parts, and bounding the remainder terms by treating them as elements of the Hilbert space and invoking the very inequality being proved (Theorem 3.5.1 itself, applied with ) as a self-referential bootstrap — this is why the proof fixes as the smallest valid constant before starting, rather than building it up from scratch.
The goal and both milestones work with the real matrix and real inner product space directly;
H is required to be a complete real inner product space (NormedAddCommGroup,
InnerProductSpace ℝ, CompleteSpace), matching the book's "any Hilbert space." No
dimension bound on is imposed — the inequality's content is exactly that does not grow
with .
This mission does not formalize the sharper bound of Section 3.7, nor Theorem 3.6.5 (the 0.878-approximation guarantee for maximum cut via randomized rounding): the latter's statement quantifies over "the result of a randomized rounding of the solution of the semidefinite program," which would drag a specific algorithm into the audited statement rather than keeping it a self-contained mathematical claim (the statement/proof-separation trap this series' triage rubric flags). Grothendieck's identity (Lemma 3.6.6), the key fact behind that rounding step, is included on its own as a milestone, stated with an explicit, named random sign variable rather than an opaque "rounding procedure."
A trivializing formalization would state the goal with allowed to depend on , , ,
or — every such bound is easy (e.g. ) and carries none of the
theorem's content; the Lean statement rules this out by quantifying before every other
object. and (Theorem 3.5.6) are defined from scratch in this
chunk's namespace, using Matrix.PosSemidef from Mathlib for the positive-semidefiniteness
hypothesis (which bundles the real-symmetric condition); Mathlib has no ready-made SDP-value
construction to reuse. The sub-gaussian (Orlicz ) norm used by Theorem 3.1.1 is reused,
unchanged, from the 01-concentration mission in this series (HighDimProb.Concentration.SubgaussianNorm)
rather than redefined.