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?
A serial supply chain is the simplest multiechelon system: a retailer orders from a warehouse, which orders from a plant, which orders from an outside supplier with unlimited stock. Only the retailer sees customer demand, only the retailer pays a stockout penalty, and every stage pays to hold inventory. Choosing how much each stage should hold looks like a joint optimization over all stages at once, because an upstream stockout delays every downstream replenishment. Clark and Scarf (1960) showed that it is not: measured in echelon terms, the optimal policy is a base-stock policy at every stage, and the optimal levels can be found one stage at a time from the customer upward, each step a single-variable convex minimization. Chapter 6 of Snyder and Shen's Fundamentals of Supply Chain Theory (2019) presents the infinite-horizon form of that result as its Theorem 6.3, the bounds of Shang and Song (2003) that make the levels cheap to approximate, and the contrasting guaranteed-service model of Graves and Willems (2000), in which stages quote delivery times rather than fill rates and the optimal safety stocks are all-or-nothing. This mission formalizes the chapter's numbered results, with Theorem 6.3 as its goal.
Stages are numbered from the customer upward. Stage has a local holding
cost per unit per period; its echelon holding cost is with
, so that (localHolding, echelonHolding). Stage
's echelon consists of stages , and its echelon on-hand inventory
(echelonOnHand) is all on-hand and in-transit stock in that echelon. Stage 1 pays a
stockout cost per unit per period. Orders placed by stage arrive after a lead time
if stage can ship them; denotes the lead-time demand at stage .
An echelon base-stock policy gives each stage a level and orders to keep its echelon
inventory position at . The chapter derives, from conservation of flow, a recursion that
evaluates the expected cost of any echelon base-stock vector (csBar, csHat, csG):
and the expected cost of the system under is . The term is the
implicit penalty function: it charges stage for the downstream consequences of
running short. A vector is sequentially optimal (CSSequential) when each minimizes
, which depends only on .
The Shang-Song bounds compare with the cost of the -stage truncated system when all its
local holding costs are set to one value, for the lower bound and for
the upper (ssLower, ssUpper). With equal holding costs all stock is held at stage 1, so each
bound is a single-stage newsvendor cost for the demand over the
cumulative lead time (tildeLaw) with stockout cost , plus the holding cost of the
stock in transit to stages , whose mean is
(pipelineMean).
In the guaranteed-service model each stage has a processing time , quotes a
committed service time to its customer, and receives an inbound time
from its supplier (gsInbound), being external. Demand is bounded, so the stage can meet
every order within by holding safety stock with ,
and the holding cost is (gsCost) over the
feasible times (GSFeasible).
For echelon holding costs , stockout cost and lead-time demands of finite mean, if is sequentially optimal then for every echelon base-stock vector ,
and is the optimal cost. This is clark_scarf_sequential.
Proposition 6.1, ; the stage-1 identities (6.29) and (6.30), that is a newsvendor cost with penalty and its minimizer solves ; convexity of every under sequential optimality; existence of a sequentially optimal vector when and ; Theorem 6.4, , and where minimizes and minimizes (the book's pairing, p. 200); and Theorem 6.5, that in the guaranteed-service serial system with every optimal is or .
Theorem 6.2, the optimality of echelon base-stock policies among all policies, is stated in the book without a model of the policy space and is not a target here; Theorem 6.3 is the optimization it licenses.
Theorem 6.3 is what Zipkin calls the fundamental equations of supply chain theory. It reduces a joint optimization over coupled levels to one-dimensional convex problems, and every exact method and most heuristics for serial and assembly systems, Rosling's reduction of assembly systems to serial ones included, run through it. Theorem 6.4 turns the recursion into closed-form bounds and the Shang-Song heuristic, which the book reports as accurate to within a fraction of a percent. Theorem 6.5 explains the shape of optimal safety stock placement under guaranteed service and why its dynamic program only needs to examine endpoints.
None of these results has a machine-checked proof. The book proves none of them in full: Theorem 6.3 is asserted after an informal derivation, Theorem 6.4 is cited, and Proposition 6.1 and Theorem 6.5 are left as exercises. Formalizing the recursion's convexity and the exchange argument behind Theorem 6.3 produces a reusable treatment of the implicit penalty function; the concavity-on-a-polytope argument for Theorem 6.5 is reusable for the tree systems of Sect. 6.3.5.
The obvious attack on Theorem 6.3, differentiating the system cost in each , fails immediately: the cost depends on through inside nested expectations and is not convex in jointly. The argument that works is an induction along the recursion, comparing with pointwise. Its key step is that, for the convex minimized at , the value is the least value of on , so that any other truncation point can only cost more. That step needs convexity of , which needs convex, which needs to be a minimizer; for an arbitrary the functions are not convex, and the induction must carry both vectors at once.
Integrability is a second, silent obstacle. Each is an expectation of translates of ; the recursion preserves Lipschitz continuity with a constant growing with the costs, and finite means are exactly what make every integral in the recursion a genuine expectation rather than Lean's default value zero.
Theorem 6.4 requires relating the recursion, in which demands enter one stage at a time, to a single newsvendor cost in the sum , which is a convolution; the inequalities come from the structure of (6.31) in the two extreme holding-cost profiles and are not obvious from the recursion's formulas. Theorem 6.5 is a statement about every minimizer, not the existence of an extreme one, so the proof must show the cost is strictly concave along every feasible direction that changes a net lead time and then classify the vertices of the feasible region.
Stages are indexed by natural numbers ; the cost functions take total functions on and never read values outside that range. The recursion is defined for every vector , so the theorem compares values of one family of functions rather than a separately defined system cost; the identification of with the steady-state expected cost of the physical system is the book's derivation and is not restated. Expectations are Lebesgue integrals under the lead-time demand laws, assumed to be probability measures on with finite means. Sequential optimality is a hypothesis of the goal; a separate target shows it is satisfiable when and , so the goal is not vacuous.
The bounding functions of Theorem 6.4 keep the holding cost of pipeline stock that the truncated cost (6.31) charges. The book omits that constant when it writes their minimizers, which it does not affect, but part (a) compares values, and without the constant the upper bound fails already in the book's own Example 6.1. For part (b) the minimizers of the bounding functions are asserted to exist and to bracket ; when the fractiles of are unique these are the book's quantile values. Theorem 6.5 is stated over real service times; because the feasible region's vertices are integral when the data are, every integer-optimal vector is optimal over the reals, so the real statement contains the book's integer program (6.38) to (6.42). Proposition 6.1 is stated with built into the echelon sum.
The definition module is shared by all nine items. The dynamic program (6.43) to (6.44) for guaranteed-service serial systems and the tree-system algorithm of Sect. 6.3.6 are natural extensions on the same definitions.
The derivation of Kepler's three laws from Newton's inverse-square law of gravitation is the calculation with which mathematical physics begins. Kepler published the laws in 1609 and 1619 as empirical regularities distilled from Tycho Brahe's naked-eye astrometry: planets travel on ellipses with the Sun at a focus, the Sun–planet segment sweeps equal areas in equal times, and the square of the orbital period scales as the cube of the orbit's size. That an attractive force falling off as forces exactly these three regularities was established by Newton in the Principia (1687); as David Tong remarks in the source notes, the third law was within reach of several of Newton's contemporaries, but the derivation of the first — that the orbit is a conic section with the centre of attraction at a focus — was Newton's alone.
This mission formalizes that derivation as it is presented in §4 (Central Forces) of David Tong's Dynamics and Relativity, the Cambridge Part IA Mathematical Tripos lecture notes (Lent 2013). It is the first mission in a series covering those notes, and it targets the chapter's capstone, Kepler's first law.
A point particle of mass moves in Euclidean -space along a trajectory , assumed twice continuously differentiable and never passing through the origin, where the field below is singular. Write and .
The particle moves in a central force field when it obeys Tong's equation of motion (4.1),
where gives the radial component of the force at distance ; for a force derived from a central potential one has . The Kepler problem (Tong §4.3.1) is the inverse-square special case, potential (4.12)
with for gravitational attraction by a mass fixed at the origin. (The same equations govern the Coulomb problem, with , which is repulsive when ; this mission fixes .)
Two conserved quantities organize the problem. The angular momentum is the vector
and we write for the angular momentum per unit mass, which in the plane polar coordinates of Tong (4.5) is . The total energy of the Kepler problem is
Tong's solution (4.14) of the orbit equation states that the trajectory lies on a conic section with a focus at the origin. Coordinate-free, this says that there is a fixed eccentricity vector , pointing towards the point of closest approach, with
which is Tong's with the eccentricity and measured from the direction of , and the semi-latus rectum.
Finally, a set is an ellipse with a focus at the origin when there are a nonzero normal vector , a second focus with , and a real number with , such that is exactly the set of points of the plane satisfying the two-foci (string) property
The inequality forces and rules out the degenerate loci; gives a circle.
The goal theorem is Kepler's first law, K1 of Tong §4.3.2: each planet moves in an ellipse, with the Sun at one focus. Formally, for a trajectory of the attractive inverse-square problem with nonvanishing angular momentum and negative total energy,
The hypothesis excludes purely radial free-fall, whose trajectory is a segment rather than an ellipse, and is the bounded regime, which by Tong (4.16) is exactly .
The milestones follow the source in order: conservation of angular momentum and the resulting planarity of the motion (§4, p. 48); Kepler's second law (K2), which holds for any central force; conservation of energy; the conic orbit (4.14); the identification of a conic of eccentricity as an ellipse with a focus at the origin (4.15); the energy–eccentricity relation (4.16); and Kepler's third law (K3, p. 62),
The result. K1 is the statement that fixes the inverse-square law among all central force laws: K2 holds for every central force, and dimensional analysis alone gives the shape of K3, but closed orbits that are exact ellipses with the attracting centre at a focus are special to the force (and to the harmonic force, with the centre at the centre of the ellipse). Everything quantitative in classical celestial mechanics — orbit determination, the mass–period relation used to weigh binary stars, and the perturbative treatment of precession that eventually exposed the anomaly in Mercury's orbit — is built on the Kepler solution.
Formalizing it. The mathematics has been settled for three centuries; what this mission produces is a machine-checked treatment of the Newtonian derivation, starting from the differential equation rather than from a prescribed orbit. Mathlib has no central-force or two-body library, so the definitions here — central force motion, angular momentum, conserved energy, swept area, and the two-foci characterization of an ellipse — are new and reusable across the rest of the series and by any later mission in classical mechanics. The existing platform mission Celestial Mechanics I: Binary Star Systems runs the complementary direction, verifying that a prescribed conic orbit satisfies the equations of motion and reducing the two-body problem to a one-body problem; the present mission asks for the converse, which is the harder half and the one Newton is credited with.
The derivation in the source changes the independent variable from time to the polar angle , substitutes , and solves the resulting linear oscillator equation (4.11). Each of those steps needs infrastructure that does not exist in Mathlib. There is no polar-angle function attached to a curve in the plane: one has to produce a continuously differentiable angle lifting the trajectory, show never vanishes so that is a legitimate change of variable, and then transport a second-order ODE through that reparametrization. Solving (4.11) then requires a uniqueness theorem for the inhomogeneous harmonic oscillator, and reading the conic back into Cartesian form requires the algebra of (4.15).
Kepler's third law carries an extra burden beyond the formula: the statement quantifies over the least period of the motion, so a solution must establish that a negative-energy orbit is periodic at all, and must identify and as the periapsis and apoapsis distances .
Trajectories are maps ℝ → EuclideanSpace ℝ (Fin 3), with ContDiff ℝ 2 smoothness and the standing hypothesis for all built into the definition of central force motion, together with . Time is all of : the trajectories considered are globally defined, so collision orbits are excluded by hypothesis rather than by a maximal-interval argument. Derivatives are Mathlib's deriv, so velocity and acceleration are the first and second derivatives of the trajectory.
Three conventions are worth flagging. First, the force is given by its radial profile rather than by a potential, avoiding any appeal to the junk value of a derivative at ; the Kepler case is the instance . Second, the swept area of K2 is the integral , which is the standard area element of the source written invariantly; the content of K2 is that this integrand is constant in time, so that the area depends on alone. Third, K1 asserts that the trajectory is contained in an ellipse; it does not assert that the particle traverses the whole ellipse, which is a separate (true) statement about periodic orbits.
The degenerate readings are ruled out explicitly. The eccentricity vector formulation of the conic is an equation holding at every time, not an existence claim at one time; the ellipse predicate carries , so a point or a segment does not qualify; and the hypothesis in K1 and in the conic milestone is necessary, since a radial trajectory satisfies every other hypothesis but lies on no ellipse.
Contributions of independent interest are welcome: a plane polar coordinate API for curves, uniqueness for the forced harmonic oscillator, and the classification of the loci into ellipse, parabola and hyperbola according to , , (this mission needs only the first case) would all be reusable well beyond this series.
Every wireless network control algorithm — routing, scheduling, power control, admission control — is ultimately judged against one question: which traffic loads can it keep stable? Answering that question requires a precise, algorithm-independent notion of queueing stability under random arrivals and a randomly time-varying, possibly non-ergodic-looking channel. Tassiulas & Ephremides (1992) and Neely, Modiano & Rohrs (2005) developed the framework used throughout Georgiadis, Neely & Tassiulas's survey Resource Allocation and Cross-Layer Control in Wireless Networks (Foundations and Trends in Networking, 2006): "strong stability" of a queue backlog process, defined purely through the time-averaged expected backlog, with no assumption that the arrival or service process is stationary, Markov, or even has a well-defined long-run average. The present mission formalizes the chapter's foundational single-queue results — the two structural facts every later network-wide capacity and control result in the book is built from.
A queue is described by three processes on slots : an arrival process (new bits admitted at the end of slot ), a service process (the transmission rate offered during slot ), and the backlog , evolving by the queueing law
The queue is strongly stable if its expected backlog has a bounded time average, . An arrival process is admissible with rate if (i) its time-average expected rate is , (ii) its second moment conditioned on the history is uniformly bounded, and (iii) for every there is an averaging window over which the conditional average rate exceeds by at most , uniformly in the starting time — a robust substitute for "the rate is exactly " that holds for i.i.d., Markov-modulated, and burstiness-constrained arrivals alike. A service process is admissible with rate analogously, with a deterministic pointwise upper bound in place of the second-moment condition. Both notions are formalized here on a filtered probability space , with the history of slots exactly as the book's own .
This is the chapter's central single-queue result: it converts the purely structural notion of strong stability into the one comparison — arrival rate versus service rate — that every later capacity-region and control-algorithm argument in the book reduces to.
This is the elementary real-analysis fact — no admissibility, no probability beyond an already-given expectation sequence — that underlies the necessity half of Lemma 3.6's proof.
Strong stability and the admissibility framework are the load-bearing definitions of the entire book: every later chapter's algorithm-performance theorem (Chapter 4's backpressure throughput optimality, Chapter 5's utility-optimal Lyapunov drift bound, Chapter 6's energy-constrained control) is a theorem about when its induced queues are strongly stable, and every one of those proofs cites Lemma 3.6 (or its network generalization, Theorem 3.8's capacity region) as the final step converting a drift bound into a stability conclusion. Formalizing it fixes, once for the whole series, the precise real-analysis and conditional-expectation content of "arrival rate below service rate implies stability" that a Prove2Me solver would otherwise have to reconstruct from scratch for each downstream chapter.
Formalizing it. No result in this mission has a machine-checked proof anywhere; nothing adjacent exists on the platform (searched for strong stability, admissible arrival process, Lyapunov drift, network capacity region — the one hit, a Foster–Lyapunov hitting-time bound for a finite-state MDP, is a scalar drift-to-a-target-state object, not a queue-backlog vector with no absorbing state, and is not reused). This mission is the first formalization of either result.
The obvious first idea for the sufficiency half (b) is to try to bound directly by unrolling the queueing recursion and taking expectations termwise. This fails immediately: expectation does not commute with , so in general — the whole reason admissibility's second-moment and -slot averaging clauses exist is to control exactly this gap between the pathwise recursion and its expectation, via a genuine (non-elementary) drift argument. The necessity half (a) has the opposite trap: it is tempting to prove from a single-slot expectation inequality, but a queue can be strongly stable while oscillates on any finite window, so the argument has to go through the time-averaged (Lemma 3.3) quantity, not a slot-by-slot one.
Admissibility's conditional-expectation clauses are stated with Mathlib's Filtration ℕ and
condExp (P[f | 𝓕 t]), following this platform's established idiom for martingale-difference
hypotheses. Every conditional or plain expectation in a defining clause carries an explicit
Integrable guard, because Mathlib's Bochner integral and condExp both silently default to 0
on a non-integrable function — without the guard, a process with an undefined or infinite second
moment would satisfy admissibility vacuously, which is not the book's assumption (the book assumes
these moments are finite; it never derives it). Lemma 3.3 is formalized directly on the real
sequences representing , , —
exactly the content the book's own statement and proof use, with no further probabilistic
structure, since the lemma's hypotheses and conclusion never mention anything but these
expectations. Out of scope for this mission: the network-wide capacity region (Definition 3.7,
Theorem 3.8, Corollaries 3.9-3.10) and the graph-family construction /
of §3.2-3.3. Faithfully formalizing " is stably supportable by the network" requires
embedding admissible-process realizations into a full multi-queue routing model, which is
substantially heavier than either result formalized here and was left out entirely — per this
series' faithfulness-over-coverage rule — rather than approximated by, e.g., dropping the
second-moment or -slot clauses of admissibility, which would silently change what "admissible"
means. A trivializing formalization to rule out: defining AdmissibleArrival/AdmissibleService
without the Integrable guards above would make Lemma 3.6 provable by choosing a non-integrable
process, which is not the book's theorem.
Diffusion models in a bounded region need a rule for what happens when a path reaches the boundary. Two standard mechanisms are absorption, where the boundary kills the generator contribution, and oblique reflection, where a prescribed vector field pushes the process back into the region. Ethier and Kurtz treat these mechanisms as neighboring variants of the same uniformly elliptic model in Chapter 8, Section 1 of Markov Processes: Characterization and Convergence. The distinction is structural: the interior differential operator is shared, but its admissible generator graph changes with the boundary condition. This mission formalizes Theorems 1.4 and 1.5, retaining oblique reflection as the capstone and absorbed diffusion as the required related result.
Let be bounded, open, and connected, with . Its boundary is locally represented in orthogonal coordinates as the graph of a scalar function. The formal predicate C²,μ boundary regularity requires one positive chart radius valid at every boundary point, a connected local boundary patch, and a graphing function whose second partial derivatives satisfy the source's componentwise Hölder oscillation condition. The exponent obeys .
The diffusion coefficients are a symmetric positive-semidefinite matrix field and a drift field . Their entries satisfy the same local componentwise Hölder convention. Uniform ellipticity means that one satisfies
for every and every unit vector . For smooth , the interior operator is
Functions live on the compact closure as bounded continuous functions. Their ambient extensions are differentiated only at interior points. The second coordinate of each graph is itself continuous on the closure, so it records the boundary trace of rather than assigning an arbitrary value after differentiation.
Theorem 1.5 adds a reflection field whose components have C¹,μ boundary regularity. An outward unit normal is oriented by a local defining function that is negative precisely inside . Uniform obliqueness is the global lower bound
for one positive . The reflected graph requires a continuous derivative trace that agrees with in the interior and satisfies
The target asserts that the uniform closure of this graph is single-valued and is exactly the full generator of a positive strongly continuous contraction semigroup preserving the constant function one. The generator condition is a biconditional derivative limit, so it identifies the complete domain rather than only a convenient operator restriction.
Theorem 1.4 keeps the same smooth-region and ellipticity assumptions but uses the absorbed graph. Its continuous operator trace satisfies on the boundary. It has the same full generation conclusion: graph single-valuedness, a positive strongly continuous contraction semigroup, preservation of one, and exact identification of the generator. The absorbed zero trace is not imported into the reflected theorem, and the oblique derivative condition is not imposed on the absorbed graph.
These results connect a local elliptic expression and a geometric boundary condition to a global Markov evolution on continuous functions over the closed region. The conclusions contain more than existence of a semigroup: they determine the whole infinitesimal generator, ensure positivity and contraction, and retain the conservative convention used by Ethier and Kurtz. The paired statements make the effect of the boundary mechanism explicit while holding the interior model fixed.
The formal contribution is a machine-checkable statement layer, not a proof of the source theorems. It records the componentwise Hölder convention, uniform boundary charts, ellipticity, normal orientation, continuous derivative trace, the two distinct generator graphs, and every semigroup clause. These definitions can support later work on reflected processes, elliptic boundary problems, and martingale formulations without rebuilding the geometric conventions.
The main difficulty is simultaneous control of interior regularity, boundary geometry, and the closed generator domain. Pointwise obliqueness is insufficient: the source requires a uniform positive lower bound over the whole compact boundary. Likewise, merely writing for an arbitrary ambient extension would not supply a well-defined boundary derivative. The graph therefore carries a continuous derivative trace agreeing with the interior derivative. Replacing the biconditional generator equality by a one-way inclusion, or silently imposing the absorbed zero trace on the reflected graph, would weaken or change the source result.
The state space is EuclideanSpace ℝ (Fin (n + 1)) with 2 ≤ n + 1. Connectedness supplies nonemptiness. Matrix positive semidefiniteness supplies symmetry and nonnegative quadratic forms; a separate hypothesis gives strict uniform ellipticity. Local oscillation bounds apply within connected components of small intersections and do not compare different components.
The absorbed and reflected graphs use bounded continuous functions on closure Ω. The arbitrary zero extension outside the closure is never differentiated at a boundary point. The reflected boundary equation uses a continuous field of linear derivative maps, while the absorbed equation uses the continuous second graph coordinate. No vacuous region, pointwise-only ellipticity or obliqueness, weakened generator inclusion, proof-only theorem dependency, or synthetic theorem combining the two boundary mechanisms is admitted.
In 1985 R. S. Ward conjectured that "many (and perhaps all?) of the ordinary and partial differential equations that are regarded as being integrable or solvable may be obtained from the self-dual gauge field equations (or its generalizations) by reduction". The self-dual Yang–Mills (SDYM) equations are therefore often called the master integrable system: choosing a gauge algebra and a symmetry group to reduce by produces, on the one hand, the classical soliton equations and the Painlevé transcendents, and on the other — once infinite-dimensional gauge algebras are allowed — a family of third-order equations whose solutions have movable natural barriers and are therefore not of Painlevé type.
This mission formalizes the endpoint of one such reduction chain, as surveyed by Ablowitz, Chakravarty and Halburd, Integrable systems and reductions of the self-dual Yang–Mills equations, J. Math. Phys. 44 (2003) 3147–3173, Section V. Reducing SDYM to functions of a single variable gives the Nahm equations; taking the gauge algebra to be the divergence-free vector fields on turns them into a matrix flow which, after diagonalizing the symmetric part, becomes the generalized Darboux–Halphen system. Its trace is governed by the Chazy equation, written down by Chazy in 1909, and — this is the paper's historical observation — the Chazy equation is equivalent to the differential system Ramanujan derived in 1916 for the Eisenstein series , , . Chazy and Ramanujan worked on the same equation at nearly the same time and apparently did not know it.
Throughout, and are complex variables and all functions are complex-valued; a "solution on " means the stated derivative identities hold at every point of a set .
The classical Chazy equation is the third-order equation
The classical Darboux–Halphen system is the first-order system for
together with its two cyclic images. It arose in Darboux's study of triply orthogonal surfaces and was solved by Halphen. Its generalized form adds a term to each right-hand side, where and cyclically.
Ramanujan's system is
satisfied by , , , where .
Finally, the matrix flow obtained from the Nahm equations with the gauge algebra is
and the generalized Chazy equation with parameter is
If satisfy Ramanujan's system on a region of the punctured -plane, then
satisfies the classical Chazy equation on the preimage region. In particular is a solution of the Chazy equation, and knowing the general solution of Chazy gives the general solution of Ramanujan's system.
The milestone list covers the reduction chain in both directions: the matrix flow and its reduction to the Darboux–Halphen system (eqs. (51)–(54)), the first integrals (55), the passage from Darboux–Halphen to Chazy and back through the roots of a cubic, the symmetry (73) of the Chazy equation, Rankin's fourth-order equation for the discriminant cusp form, the change of variable between the two forms of Ramanujan's system, and the generalized Chazy equation (81).
The Chazy equation is the bridge between integrable systems and the theory of modular forms. Its particular solution makes the quasi-modularity of the second Eisenstein series an ODE statement; via it turns into Rankin's homogeneous fourth-order equation for the discriminant cusp form , whose Fourier coefficients are the Ramanujan -function. The action on solutions is exactly the weight-2 quasi-modular transformation law. In the other direction, the general solution of Chazy is a ratio of hypergeometric functions with a movable natural barrier, which is why these reductions are used as the standard counterexample to the identification of integrability with the Painlevé property.
None of this material is currently in Mathlib: there is no Chazy equation, no Darboux–Halphen system, no Ramanujan differential system, and no Eisenstein-series ODE. The mission builds that layer from scratch. Each statement is a closed-form differential identity, so the development is self-contained: it needs no analytic continuation theory, no modular-forms library, and no existence theory for ODEs. What a solver must supply is careful derivative bookkeeping and polynomial algebra.
Status honesty: every statement in this mission is a classical, published result — Darboux, Halphen, Chazy (1909–1911), Ramanujan (1916), Rankin (1956), and Ablowitz–Chakravarty–Halburd (1990s–2003). Nothing here is open mathematics. What is open is the machine-checked proof; to the captain's knowledge no formalization of these identities exists.
The obvious approach — "differentiate three times and call ring" — fails for two reasons. First, the statements are about functions, not about polynomials: each differentiation step requires producing the derivative of a product, a quotient, or a composition from the hypotheses, and only then is the resulting algebraic identity a ring problem. Second, two of the targets go against the flow of the hypotheses. Recovering the Darboux–Halphen system from a Chazy solution means recovering from the derivatives of the three elementary symmetric functions of the : this is a linear system whose matrix is a Vandermonde matrix in , invertible precisely because the roots are assumed distinct — which is why the distinctness hypothesis is not decoration. Similarly, the matrix milestone needs the conjugation-equivariance of , which holds for the transpose only because the conjugating matrix is complex orthogonal.
Everything is over , matching the paper. Solutions are represented pointwise on an arbitrary set rather than on all of , because the solutions of interest have movable singularities and natural barriers; no openness, holomorphy or connectivity is assumed unless a statement needs it.
Higher derivatives are carried as explicit extra function arguments joined by HasDerivAt hypotheses rather than through iterated deriv. This avoids junk values entirely: a statement never asserts anything about the value of a derivative that does not exist. The same convention is used for the matrix flow, where the derivative is imposed entrywise, so that no norm or normed-space structure on the space of matrices needs to be chosen.
Divisions are arranged so that no denominator can vanish under the stated hypotheses: Ramanujan's system is written in the form , with no division by ; the generalized Chazy equation carries the hypothesis ; and the first-integral and discriminant statements carry explicit nonvanishing hypotheses.
There is no trivializing formalization available here. Every statement is an implication between two systems of differential equations whose hypotheses are satisfied by the classical explicit solutions (, , for the Ramanujan system; Halphen's solutions for Darboux–Halphen), so none of them is vacuous, and none is an identity that holds for arbitrary functions.
A complete development needs only Mathlib's derivative calculus (HasDerivAt and its product, quotient and composition rules), Complex.exp, and Matrix.adjugate with the basic adjugate identities. Contributions of reusable pieces are welcome: in particular a clean statement of the derivative of the elementary symmetric functions of a triple of functions, and the Vandermonde inversion step, would both be of use beyond this mission.
Regularization — adding a penalty on model complexity to an empirical risk minimization objective — is one of the oldest and most reliably effective tools in statistical learning: ridge regression, LASSO, and margin-based support vector machines all fit this template. For decades the regularization weight and penalty function were chosen heuristically or by cross-validation, with only asymptotic or worst-case generalization bounds explaining why they help. Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter on Wasserstein distributionally robust optimization (DRO) gives regularization a different, non-asymptotic justification: a decision rule that is robust to adversarial perturbations of its training data, measured in Wasserstein distance, is exactly a regularized empirical risk minimizer — no approximation, no asymptotics. This mission formalizes the general form of that equivalence, Theorem 10 (p. 14), which underlies every regularization-by-robustification result the chapter derives for classification and regression alike.
Fix a normed space , a convex loss function , a radius , and training samples (). The empirical distribution is . The worst-case risk of at radius (eq. (6), p. 6) is
where is the type- Wasserstein ball of radius around (Definition 1, p. 3) — the set of probability measures on within Wasserstein distance of the empirical distribution, under a norm on and its transportation exponent . The Lipschitz modulus (possibly ) measures how fast can grow.
Goal (Theorem 10, convex loss and ). If is convex and , then the worst-case risk of over the type-1 Wasserstein ball around the empirical distribution coincides with the Lipschitz-regularized empirical loss:
where is the ordinary empirical risk. The left side is the worst-case expected loss under adversarial perturbations of the training data of bounded aggregate Wasserstein cost; the right side is the ordinary empirical risk plus a regularization term proportional to the perturbation radius and the loss's own Lipschitz modulus — no approximation, an exact equality for every convex .
This is the single result underlying every specific regularization-by-robustification corollary
the chapter derives — the -regularized SVM and its / variants,
regularized logistic regression, and the regression analogue with a Lipschitz loss (Proposition 3)
— because each of those is obtained by substituting a specific convex, Lipschitz loss (hinge,
logloss, a linear-model margin loss) for the general here and reading off
in closed form. Theorem 10 is exact (, Ξ = R^m) precisely because a
type-1 transportation cost is dual to the Lipschitz modulus (a consequence of the Kantorovich-
Rubinstein duality this book's earlier duality theorems establish), whereas the corresponding
statement for (Theorem 11 elsewhere in the chapter) needs a strictly stronger hypothesis
on . Formalizing Theorem 10 fixes, machine-checkably, the exact scope of the equivalence —
which losses qualify (convex, no boundedness or smoothness needed), which transportation exponent
is required (, not any ), and that the equality is exact, not an upper or lower bound —
the single fact every classification- and regression-specific robustification corollary in the
chapter cites without re-deriving.
The natural first attempt treats the worst-case risk as an instance of the general finite convex
reduction (Theorem 8, which needs or a related concave/convex-conjugate structure and
applies for a general norm exponent with ) and specializes it to . This is
not the paper's own route for Theorem 10: at the dual exponent , and the general
finite-convex-program reduction (11) degenerates in a way that is more naturally derived directly
from the type-1 Wasserstein distance's own dual (Kantorovich-Rubinstein) representation — a
Lipschitz test function pairs exactly with a type-1 transportation cost, which is why the answer is
Lipschitz-regularization and not some other penalty. The Lean statement records only the final
equality (the proof itself, via Theorem 8 or the direct Kantorovich-Rubinstein route, is left as
sorry, as required for a draft item), but the choice of which milestones would support that proof
is exactly this: the type-1/Lipschitz-modulus duality is a structurally different argument from the
finite-convex-program machinery Theorem 8 needs for other , which is why this chapter's earlier
draft mistakenly tried to reach a specialization of Theorem 10 (Proposition 2, restated for a
labeled, ambiguity set) through a finite-atom shortcut that does not actually
capture the general type-1 ball Theorem 10's own proof needs — see Formalization scope.
is EuclideanSpace ℝ (Fin m) (fixed to Set.univ, matching the theorem's own "Ξ = R^m"
hypothesis) with an arbitrary fixed norm as a type-class parameter, not specialized to Euclidean.
The worst-case risk, Wasserstein distance, ambiguity set, nominal risk, empirical distribution and
Lipschitz modulus are all redefined locally in this chapter's own namespace, verbatim restatements
of 01-duality's own drafts of the same objects (identical EReal/ENNReal/Integrable
conventions), because 01-duality is not yet a published mission
(CAPTAIN_ADDENDUM_WAVE2.md rule 5); a later upload can retire the duplication once it is live.
hN : 0 < N excludes the empty-sample case the paper's own "N training samples" presupposes;
hℓ : Integrable ℓ (empiricalDistribution ξhat) guards the empirical risk's Bochner integral
(automatically satisfied under any real-valued ℓ since the empirical distribution is a finite
convex combination of Dirac masses, but stated explicitly rather than assumed silently). No
constant is pinned to a numeral. This mission originally targeted Proposition 2 (regularization
by robustification for classification, p. 25), a specialization of Theorem 10 to a labeled,
κ=∞ input-output ambiguity set — but that draft's κ=∞ ambiguity set restricted admissible
perturbations to a finite family of exactly N atoms, each sample's entire mass moving as one
indivisible unit, which is a strict, non-faithful subset of the true κ=∞ Wasserstein ball
(splitting a sample's mass across several destinations is a legitimate, and for a convex loss
strictly more powerful, perturbation by Jensen's inequality). This made the goal theorem false for
at least one of the three loss functions (Table 1) the mission itself certified as covered
(logloss), not merely narrower than the paper's claim — moderation caught this and required either
a faithful general-ambiguity-set reformulation or retargeting the goal. This mission takes the
latter: Theorem 10 itself, already correctly and generally stated using the unrestricted
Wasserstein ball throughout, is now the goal, with no further milestone (no other numbered result
in this chunk's scope is needed for Theorem 10's own statement beyond the shared definitions
above). A future mission in this series can revisit Proposition 2/3 with a properly general
labeled ambiguity set once that construction (label-pinned marginal plus an aggregate coupling
condition on the input coordinate, rather than a finite atom family) is built.
A decision maker who solves a distributionally robust optimization (DRO) problem over a Wasserstein ball chooses a radius by hand, and it is natural to ask what guarantee that choice actually buys: how large must be, as a function of the sample size and a desired confidence level, before the resulting worst-case risk is provably not an underestimate of the true (unknown-distribution) risk? Kuhn, Mohajerin Esfahani, Nguyen & Shafieezadeh-Abadeh's 2019 INFORMS TutORials chapter answers this for the mean-covariance relaxation of Wasserstein DRO introduced via the Gelbrich hull (Section 2.3): Theorem 21 gives a concentration inequality for how fast the sample mean and covariance approach the true mean and covariance, and Theorem 22 turns that concentration bound into a finite-sample statistical guarantee for the Gelbrich risk itself. This mission formalizes both.
Fix . Let be the unknown true distribution on with mean vector and covariance matrix , and suppose is light-tailed: there exist and with . Let be independent, identically distributed samples from ; write for their joint law (the -fold product measure) and for the resulting sample mean and sample covariance, i.e. the mean and covariance of the empirical distribution . Recall from the Gelbrich construction the mean-covariance uncertainty set , and the Gelbrich risk of a loss function over the Gelbrich hull .
Milestone (Theorem 21, concentration inequalities II). There is , depending on only through (not on any finer feature of ), such that for every ,
Goal (Theorem 22(a), finite sample guarantees II). Under the same hypotheses, for every and ,
With probability at least over the draw of the training sample, the Gelbrich risk
computed from that sample upper-bounds the true risk of every admissible loss function
simultaneously — not just of one fixed chosen in advance. (The paper's part (b), the
analogous guarantee $P^N\{R(P,\ell^\star) \le R_\varepsilon(\hat\mu,\hat\Sigma,\ell^\star)\} \ge 1-\eta$ for the specific optimizer of the Gelbrich risk minimization problem, is not
formalized in this mission — see Formalization scope.)
Theorem 22 is what makes the Gelbrich-risk relaxation of Wasserstein DRO more than a computational convenience: it certifies that solving the tractable Gelbrich risk minimization problem gives a decision whose true out-of-sample risk is, with high probability, no worse than the value the solver reports — a genuine confidence guarantee, not merely an approximation of the Wasserstein worst-case risk. Theorem 21's rate, , is also of independent interest: it is dimension-free (no curse of dimensionality), in contrast to the paper's earlier general-distribution concentration result (Theorem 18, out of scope for this mission) whose rate degrades with . Formalizing Theorem 21 fixes, machine-checkably, the exact functional form of and the precise sense in which is "distribution-free" given — a subtlety easy to state informally but easy to get wrong formally (see Difficulty).
The central formalization difficulty is not proving the theorems (both are left as sorry in this
draft) but stating the existential constant correctly. The paper says "depends on only
through " — informally, a promise that is uniform across every
distribution sharing those five parameters, not merely that some exists for each
separately (a vacuously true, much weaker statement obtained by naively quantifying after ).
The correct encoding places before the universal quantifier over : for fixed
, one must work for every with that mean, covariance, and tail
bound. Getting this quantifier order backwards silently converts a genuine finite-sample guarantee
into a triviality (FAITHFULNESS_TRAPS.md trap 8).
Distributions live on EuclideanSpace ℝ (Fin m); , the law of iid samples, is the
-fold product measure MeasureTheory.Measure.pi (fun _ => P) on Fin N → EuclideanSpace ℝ (Fin m) — an event about the random sample sequence is a set of such tuples, and "" is that product measure's mass on the event set. All risk and uncertainty-set
definitions (meanVector, covarianceMatrix, meanCovarianceUncertaintySet, gelbrichHull,
gelbrichRisk, nominalRisk, empiricalDistribution) are redefined locally in this chapter's own
namespace, matching 02-gelbrich's conventions exactly, since neither 01-duality nor
02-gelbrich is yet a published mission (CAPTAIN_ADDENDUM_WAVE2.md rule 5); a later upload can
retire the duplication once those missions are live. The existential constant c is placed before
the universal quantifier over P in both theorems, exactly capturing "depends on P only through
µ,Σ,α,A,m" — see Difficulty. Only Theorem 22's part (a) (the uniform bound over a loss class
L) is formalized; part (b) — the bound for the specific optimizer ℓ* of the Gelbrich risk
minimization problem (19) — is left out, because it requires first formalizing "ℓ* is an
optimizer of problem (19)" as an object (an infimum-attaining selection over a data-dependent
optimization problem), which is additional infrastructure this mission's time budget did not
cover; formalizing it as an unconditional bound over an arbitrary data-dependent ℓ* (dropping the
optimality hypothesis) would be unfaithful — the guarantee genuinely depends on ℓ* being an
optimizer, not an arbitrary measurable function of the sample. The goal theorem also carries
hΞ, stating Ξ contains the support of P (the paper's own standing assumption, p. 6, for
every later use of Ξ), and hLInt, an Integrable ℓ P guard for every ℓ ∈ L, matching
Assumption 1 (p. 9); both were added after moderation found the goal's original statement,
without them, admitted a counter-instance (Ξ = ∅ collapses the Gelbrich hull to empty and the
risk supremum to ⊥, making the guarantee provably false rather than merely undisclosed). Theorem 18 (the general, dimension-
dependent concentration inequality with its piecewise ε_N(η) formula) and Theorems 19/20/23 (its
downstream guarantees and the asymptotic-consistency results) are out of scope for this mission,
which targets the Gelbrich-risk branch (Theorems 21/22) specifically.
Every generalization bound in Chapters 2-11 depends only on the complexity of a fixed hypothesis set — Rademacher complexity, VC-dimension, growth function — and holds regardless of which algorithm within actually returns the hypothesis. This is both a strength (broad applicability) and a limitation: it throws away everything specific to how an algorithm searches , and can be uninformative when itself is large or unbounded (e.g. a regularized objective that implicitly restricts the search without shrinking as a set). Chapter 14 introduces a fundamentally different route to a generalization bound — a property of the algorithm rather than the hypothesis class — first used by Devroye, Rogers and Wagner for -nearest-neighbor rules and given its modern general form by Bousquet and Elisseeff (2002), whose treatment this chapter follows and (for non-differentiable convex losses) extends.
A labeled example is ; for a loss function (where may differ from , e.g. but for a real-valued hypothesis), the loss of a hypothesis at is . Given a learning algorithm that maps a sample of size to a hypothesis , the empirical error and generalization error are and . Uniform -stability (Definition 14.1) says: for any two samples , differing by a single point, the algorithm's returned hypotheses satisfy for every — replacing one training point can change the algorithm's loss on any point by at most . For the regularized algorithms studied in §14.3, a kernel-based regularization algorithm minimizes over the RKHS of a positive-definite kernel , and a loss is -admissible (Definition 14.3) if for all hypotheses — a Lipschitz-like smoothness condition satisfied by the standard regression and classification losses.
Proposition 14.4 (milestone). For a PDS kernel with and a convex, -admissible loss , the kernel-based regularization algorithm is -stable with
Corollary 14.5 (milestone). For SVR (the -insensitive loss , bounded by ), with probability at least :
Theorem 14.2 — the mission's goal. For a loss bounded by and a -stable algorithm , with probability at least over a sample of size :
Theorem 14.2 is the book's demonstration that algorithm-dependent analysis is not merely a
special-case curiosity: it is broad enough to cover an entire family (every kernel-based
regularization algorithm — KRR, SVR, SVMs, and beyond) uniformly, via a single stability
coefficient computation (Proposition 14.4) that is then specialized per algorithm just by
plugging in that loss's admissibility constant . Corollary 14.5's SVR bound is the
concrete payoff: a fully explicit, dimension-free generalization guarantee for a widely used
regression algorithm, with every constant (, , ) traceable to the algorithm's own
hyperparameters, no VC-dimension or Rademacher-complexity computation required. Unlike Chapters
3-11, whose bounds are oblivious to how is searched, algorithmic stability is the first
tool in the book that can, in principle, certify generalization for a hypothesis class too large
or poorly understood for a complexity-based bound to be informative, provided the algorithm
itself is stable. No prior art on the Prove2Me platform is faithful: GET /theorems?q=algorithmic+stability, q=uniform+stability return no hits; q=McDiarmid returns
only bounded_diff_martingale_two_sided (Boucheron-Lugosi-Massart's own two-sided
bounded-differences martingale inequality), which is McDiarmid's inequality's own proof engine
(the background result Theorem 14.2's proof applies), not any result of this chapter — a
different mathematical object entirely, not reused. All eleven items are drafted fresh.
Not formalized here: Corollary 14.6 (KRR bound), Lemma 14.7 (boundedness of kernel-regularization hypotheses) and Corollary 14.8 (SVM bound). Corollary 14.6 is structurally identical to Corollary 14.5 (a different loss function's admissibility constant plugged into the same Proposition 14.4 + Theorem 14.2 chain) and adds no new formalization content beyond Corollary 14.5, already drafted; Lemma 14.7 and Corollary 14.8 are omitted together, since 14.8's own statement needs 14.7's bound on to compute its explicit (unlike Corollary 14.5, which is given as a hypothesis) — a genuine additional formalization layer (the reproducing-kernel norm bound ) disproportionate to a single further corollary within this mission's budget.
The chapter's central technical step is recognizing that -stability plus the loss bound together give exactly the bounded-difference property McDiarmid's inequality needs, applied to as a function of the sample: replacing one point of changes by at most (stability applied to the population loss, an expectation over ) and changes by at most (stability on the shared points, plus the full loss bound on the one point that actually changed) — two different, asymmetric arguments that must be combined correctly to get , not merely "stability implies boundedness" asserted directly. Proposition 14.4's own proof (not formalized here beyond its statement) needs a generalized Bregman divergence to handle a possibly non-differentiable convex loss — an extension of Bousquet-Elisseeff's original argument the book credits to itself as novel — via the reproducing-kernel property and Cauchy-Schwarz to convert a divergence bound into a bound on , then back into a pointwise loss bound.
IsRKHSOf/IsMinimizer are restated locally in Stability, byte-identical to chunk
06-kernels's own copies (a draft item cannot import another chunk's draft module); H is an
abstract real inner-product space with an evaluation map ev : H → X → ℝ standing for "elements
of H are functions on X", the same device chunk 06's own RKHS formalization uses, since
Mathlib's abstract Hilbert spaces are not themselves spaces of functions. UniformlyStable fixes
the sample size m as part of the algorithm's type (A : (Fin m → X × Y) → (X → Y')), matching
the book's own standing convention of a fixed sample size m throughout the chapter.
Proposition 14.4 is stated pairwise — for any two samples differing by one point and any
minimizers of their respective regularized objectives, the pointwise loss bound holds — rather
than fixing a global choice-function algorithm A, since the book's own proof picks an arbitrary
minimizer of each objective without asserting uniqueness; Corollary 14.5 does fix a choice
function A (one minimizer per sample), since Theorem 14.2's own statement needs a single
algorithm evaluated across the whole product-measure sample space. No numerical constant in any
of the three theorems is altered from the book's own displayed form. A trivializing
formalization this mission avoids: stating Theorem 14.2 only for the strict per-hypothesis loss
bound (∀ h ∈ H, ∀ z, L_z(h) ≤ M) rather than the book's own weaker, algorithm-specific
condition (hbound, ∀ S, ∀ z, L_z(A S) ≤ M) — the weaker hypothesis is kept, exactly matching
the book's explicit statement that "a weaker condition suffices."
Estimating a covariance matrix from samples is a canonical high-dimensional problem: the natural estimator, the sample covariance , is consistent in operator norm only when , which fails outright in the regime common to modern applications. When is additionally known to be sparse — few nonzero entries per row — a simple fix restores consistency even when : threshold every entry of below a data-dependent level to zero. This mission formalizes the matrix concentration machinery behind that fix and the resulting guarantee, following Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 6.
For a random matrix , the matrix variance is , and the Loewner order on symmetric matrices means is positive semidefinite. A zero-mean symmetric random matrix satisfies Bernstein's condition (Definition 6.10) with parameter if for — the matrix analogue of the scalar Bernstein condition of Chapter 2. The operator (spectral) norm is 's largest singular value.
Given a threshold , the hard-thresholding operator is , extended entrywise to matrices (Eq. (6.52)). A covariance matrix 's sparsity pattern is captured by its adjacency matrix (p. 181); always, with equality only when has no zero entries, and whenever has at most nonzero entries per row.
Let be i.i.d. zero-mean random vectors with covariance , each coordinate sub-Gaussian with parameter at most . If , then for any , the thresholded sample covariance with satisfies
The error scales with the graph sparsity , not with directly — the whole point of thresholding when the ambient dimension is much larger than the sample size.
For independent, zero-mean, symmetric random matrices satisfying Bernstein's condition with parameter ,
This is the general matrix concentration tool the whole chapter builds toward; Theorem 6.23 is one of its corollaries.
For any with , — a purely deterministic fact, with no probability involved, that reduces Theorem 6.23's proof to a single probabilistic input: controlling .
Theorem 6.17 is the workhorse of the whole chapter: besides Theorem 6.23, it also underlies Corollary 6.20's operator-norm bound for the unstructured sample covariance matrix (used in turn for the two example ensembles in Section 6.4.5), by taking . Theorem 6.23 itself is the standard justification for thresholding-based covariance estimators used throughout high-dimensional statistics whenever the sparsity pattern of , though unknown, is believed to be structured.
Formalizing it. No faithful prior art exists on the platform for the matrix Bernstein bound
or covariance thresholding (a fresh search for "matrix Bernstein," "Bernstein condition
matrix," "thresholding covariance," and "sparse covariance" returned no hits). The existing
RademacherWigner.* items formalize spectral-edge and empirical-spectral-distribution bounds
for the Wigner ensemble specifically (a symmetric matrix with i.i.d. entries) — a narrower,
different random-matrix model from the general Bernstein-condition matrices this chapter treats,
and not reused here. All three theorems are drafted as open goals (:= by sorry).
The naive approach to a matrix tail bound — apply the scalar Chernoff/Bernstein technique directly to the operator norm — fails because the operator norm is not a linear functional of , so the scalar moment generating function bound does not translate directly. The resolution (Lemma 6.13, not itself part of this mission) instead bounds the trace of the matrix exponential of the sum, which is linear-algebraically tractable via the Golden–Thompson-type inequality and the union bound over the (at most ) nonzero eigenvalue directions of the aggregate variance — this is exactly why the bound's prefactor is , not the ambient dimension : a low-rank aggregate variance (e.g. from a highly structured collection of matrices) yields a much tighter bound than a naive union bound over all eigen-directions would. Theorem 6.23's own difficulty is entirely in the reduction to Theorem 6.17 plus Eq. (6.54): checking that satisfies the Bernstein condition with the stated parameters, and that concentrates at the stated rate via a union bound over the matrix entries.
"Symmetric" is realized via Mathlib's Matrix.IsSymm; the Loewner order via
(B-A).PosSemidef. The matrix moment generating function itself (ΨQ(λ):=E[e^{λQ}]) is not
formalized, since none of this mission's three theorem statements need it directly — Bernstein's
condition (Definition 6.10) is stated purely in terms of polynomial moments ,
avoiding the substantial extra machinery (Mathlib's NormedSpace.exp for matrices) that a
faithful matrix-exponential definition would require, at no cost to faithfulness for the three
statements actually drafted.
Independence of / is realized via Mathlib's iIndepFun; this required adding
a local MeasurableSpace (Matrix (Fin d) (Fin d) ℝ) instance in the workspace, since Matrix is
a def, not an abbrev, over the underlying Pi type, so Lean's instance search does not
automatically find the Pi-type MeasurableSpace instance for it. "Identically distributed" is
realized via Mathlib's IdentDistrib against a fixed reference index. "Each component
sub-Gaussian" is restated locally as an explicit MGF bound at the reference index, per this
book's cross-chapter rule against importing another chapter's draft definitions.
If a statement admits a trivializing formalization: the rank(...) prefactor of Theorem 6.17
is kept exactly, not replaced by the ambient dimension (which would be a strictly weaker,
non-trivializing but unfaithful simplification, since the bound's whole point is that
rank(...) ≤ d can be much smaller). ‖·‖_max and opNorm at d=0 return Mathlib's junk
value 0 (harmless: no matrix entries or singular values exist at that degenerate size either).
Out of scope for this mission: Theorem 6.15 (the sub-Gaussian-tail matrix concentration result
that precedes Theorem 6.17 in the same section) and Corollary 6.20 (the unstructured
covariance-estimation corollary) — both natural follow-on work, cut for this chunk's time
budget; see STATUS.md.
Maximum entropy (Maxent) models are a widely used family of density-estimation algorithms: given a sample and a set of features, they select the distribution that matches the empirical feature averages while being otherwise as "agnostic" (close to a prior, usually uniform) as possible — a principle that, notably, never requires specifying a parametric family of distributions to search over. This mission formalizes the theorem that explains why this works in practice: Maxent's primal optimization (over distributions, subject to feature-matching constraints) is exactly dual to an unconstrained maximum-likelihood problem over a specific, rich parametric family — the Gibbs distributions — even though the Maxent principle never mentions that family at all.
For a sample drawn i.i.d. from over a finite set , and a feature map with , the Maxent principle seeks (the simplex of distributions over ) minimizing the relative entropy to a prior , subject to (problem 12.7). Introducing the indicator function ( on , elsewhere) turns this into the unconstrained primal objective (Eq. 12.8), with the feature-constraint set. A Gibbs distribution with parameter is , the partition function (Eq. 12.9); its associated dual objective is (Eq. 12.10) — note is exactly the empirical log-loss , so maximizing is minimizing an L1-regularized log-loss over the Gibbs family.
Theorem 12.2 — the mission's goal (Maxent duality). . Furthermore, letting and : for any and any with , .
Theorem 12.3 (Maxent L1-regularization generalization bound, milestone). Fix . Let solve the L1-regularized dual (12.12) with . Then, with probability at least ,
Theorem 12.2 is one of the most striking dualities in the book: the Maxent principle, phrased
purely in terms of closeness to a prior distribution, turns out to always produce a solution in
the Gibbs family — not because that family was ever specified, but because relative entropy is
the specific measure of closeness whose Fenchel conjugate is the log-partition function. This
explains a whole zoo of models (log-linear models, exponential families, Gaussian and bimodal
Gibbs distributions from quadratic features) as instances of a single duality theorem, and gives
a computationally friendlier route to the (constrained, infinite-if--is-large) primal problem
via the (unconstrained, -dimensional) dual. The theorem's proof is a genuine application of
conditional (Fenchel) strong duality, not an unconditional fact — this is, per the chapter's own
brief, the sharpest trivialization risk in the entire mission series, since "strong duality
always holds for convex problems" is false in general, and a formalization skipping the book's
own qualification condition (, placing in the interior of the constraint set)
would prove a different, potentially-false statement. No prior art on the platform is faithful:
GET /theorems?q=maximum+entropy returns no hits, and Mathlib's generic Fenchel-conjugate
machinery (Analysis/Convex/Conjugate) does not package the book's own specific qualification
conditions as a single reusable theorem matching Theorem B.39 — reusing it inside a proof
(not the audited statement) remains available to whoever proves this theorem later.
Not formalized here: Theorem 12.4 (a Bregman-divergence generalization of Theorem 12.2) and
Theorem 12.5 (its L2-regularized concrete special case). BRIEF.md itself flags Theorem 12.4
as possibly too heavy and offers Theorem 12.5 as an easier alternative; this mission omits both,
since even Theorem 12.5 requires a second, structurally parallel dual-objective-and-minimizer
formalization (for L2 rather than L1 regularization) — disproportionate to this mission's budget
once Theorem 12.2's own qualification-condition bookkeeping (the heaviest single item in this
mission series) is accounted for. §12.1 (density estimation without features: ML/MAP), §12.7
(coordinate descent), and §12.8-12.9 (Bregman-divergence extensions, L2-regularization in
general) are likewise out of scope, per BRIEF.md's own page-range restriction.
Theorem 12.2's proof is the book's own explicit application of the Fenchel duality theorem
(Theorem B.39, Appendix B) to the specific triple , ,
— every qualification condition (A a bounded linear map, u_0\in A(\mathrm{dom}f)\cap\mathrm{cont}(g), needing \lambda>0 to place u_0 in int(C)) must be
checked for this triple, not assumed generically; the conjugate computations themselves
(f^*(q)=\log\sum_xp_0(x)e^{q(x)}$ via Lemma B.37, g^(w)=E_{\hat D}[w\cdot\Phi]+\lambda|w|_1 via the dual-norm identity) are specific algebraic derivations, not immediate from abstract duality alone. The second clause's proof needs a further, non-obvious algebraic identity (G(w)-D(p^|p_0)+D(p^|p_w)expanding, via Hölder's inequality applied to the primal feasibility ofp^, to something \le0) that is not a restatement of the first clause but a separate argument built on top of it. Theorem 12.3's proof structurally mirrors chunk 04's SRM bound (bounding L_D(\hat w)-L_S(\hat w)via Hölder's inequality and the Rademacher-complexity feature-concentration bound of Eq. 12.5, then using\hat w`'s optimality twice), but is applied
to the log-loss of a Gibbs distribution rather than a generic bounded loss.
MaxEntPrimalObjective uses EReal (the extended reals) so that the book's own +\infty
values (from I_K, \tilde D) are represented exactly, matching the chapter's own explicit use
of an extended-real-valued indicator function rather than a soft penalty — a trivializing
formalization this mission avoids is silently replacing +\infty with a large real sentinel,
which would misstate a convex-analysis object whose entire role in the proof is its infinite
value outside the feasible/simplex set. hlam : 0 < lam is a genuine load-bearing hypothesis in
the goal theorem, matching the book's own use of \lambda>0 to invoke Theorem B.39's
qualification condition — not a free convexity assumption; this is the mission's central
faithfulness guard against the chapter's own named trivialization risk. EmpiricalRademacherComplexity/
RademacherComplexity are restated locally, byte-identical to chunks 05-svm/07-boosting's
own copies (a draft item cannot import another chunk's draft module). p^* in the goal theorem
and \hat w in Theorem 12.3 are both quantified via explicit hypotheses (IsLeast, a
minimizer inequality) rather than assumed to exist unconditionally, matching the book's own "let
p^*=..."/"let \hat w be a solution of..." phrasing without asserting existence or uniqueness
beyond what the book itself asserts. No numerical constant in either theorem is altered from
the book's own displayed form.
Every generalization bound in chapters 2-5 is for binary classification. Most real-world
classification problems have more than two classes, and the number of classes can itself be
in the hundreds or thousands (topic classification, speech recognition). Chapter 9 extends the
margin-based generalization theory of chapter 5 (SVMs) to this multi-class, mono-label setting,
using the same Rademacher-complexity machinery as chunk 03-rademacher-vc, but with a new
combinatorial ingredient — bounding the Rademacher complexity of a family built by taking a
pointwise maximum over several hypothesis sets — needed because a multi-class prediction is
itself an argmax over per-class scores.
A multi-class hypothesis is a scoring function with
(mono-label case); the predicted label is , and the margin
(p. 215) is negative exactly when misclassifies
. The empirical margin loss (Eq. 9.5) uses the same margin-loss
function (Definition 5.5) as chunk 05-svm, restated locally here. (p. 217) projects a multi-class hypothesis set onto ordinary
real-valued functions on — the object the chapter's Rademacher-complexity bound actually
controls, since has no norm of its own without such a
projection. Lemma 9.1 is a purely combinatorial tool: the empirical Rademacher complexity of a
family built by taking the pointwise max over hypothesis sets is bounded by the sum of
their individual empirical Rademacher complexities — used to control the argmax structure of a
multi-class prediction. Theorem 9.2 combines this with chunk 03's Rademacher-complexity
generalization machinery (Theorem 3.3) to give the chapter's margin bound. Proposition 9.3 and
Corollary 9.4 specialize this to kernel-based hypotheses, where each class has its own weight
vector in a reproducing kernel Hilbert space and the weight vectors are jointly constrained
by an -type group norm .
Lemma 9.1 (milestone). For hypothesis sets in , , and : .
Theorem 9.2 — the mission's goal. For , , fix . For any , with probability at least , for all :
Proposition 9.3 (milestone). For a PDS kernel with feature map and : .
Corollary 9.4 (milestone). Under Proposition 9.3's hypotheses, fix . For any , with probability at least , for all : .
Theorem 9.2 is the multi-class generalization of chunk 05-svm's Theorem 5.8, and its proof is
the chapter's genuine new technique rather than a restatement: it needs a -way application of
Lemma 9.1 (once for the argmax structure of the margin, once summing over the possible
labels), which is exactly where the factor comes from. Corollary 9.4 is the direct
theoretical basis for the multi-class SVM algorithm the chapter derives next (§9.3.1): the
displayed dual optimization problem literally minimizes the right-hand side of the corollary's
bound. No prior art exists on the platform: GET /theorems?q=multi-class%20classification
returns zero hits, and chunk 03's Rademacher-complexity machinery (needed by the proof route)
is a draft, not reusable, per the "drafts cannot import drafts" rule.
Lemma 9.1's proof is a genuine two-function argument (max as ,
Talagrand's lemma applied to ) generalized to functions by induction, not a
one-line consequence of chunk 03's single-hypothesis-set bound. Theorem 9.2's own proof
(PDF pp. 234-236) is the chapter's most involved: it introduces an auxiliary margin function
with a free parameter later fixed to , splits the resulting
Rademacher complexity into a "diagonal" term (bounded via a further one-hot decomposition
across the classes, giving the first factor of ) and a "off-diagonal" term bounded via
Lemma 9.1 (giving the second factor, folded into the same constant). A formalization that
stated Theorem 9.2 for itself rather than , or that treated as an unrelated
free constant rather than the actual number of classes, would misstate the theorem — precisely
the pitfall BRIEF.md names for this chapter. Proposition 9.3's proof is a clean
Cauchy-Schwarz/Jensen argument in the RKHS but needs the -group-norm hypothesis class
stated with its exact footnote definition (PDF p. 236), not a simplified
special case.
GeneralizationError, EmpiricalRademacherComplexity and RademacherComplexity are restated
locally in this chunk's MultiClass namespace (the last two identical in content to chunk
03-rademacher-vc's own copies); MarginLossFunction restates chunk 05-svm's Definition 5.5
(the same function, needed here for this chapter's own EmpiricalMarginLoss); IsPDS
restates chunk 06-kernels's PDS-kernel definition. All are duplicated rather than imported
since a draft item cannot import another chunk's draft module, and none of 03, 05, 06 is
listed as reusable in missions/README.md's "Published definitions" table at the time of this
session. GeneralizationError is formalized via the book's own established equivalence "
misclassifies iff " (the form Theorem 9.2's own proof displays and
works with), rather than via an explicit argmax classifier construction — checked as
faithful, not a weakening, since it is exactly the quantity the chapter's proof bounds.
MarginFunction's ⨆_{y'≠y} is a real supremum rather than a Finset.sup', avoiding a
nonempty-finset side proof at definition time; every consuming theorem supplies 2 ≤ k
(Y = Fin k) to guard it against trap 5. MaxFamily's index type is Fintype+Nonempty
rather than a Finset-cardinality parameter l, a harmless generalization matching "l ≥ 1
hypothesis sets" via Nonempty. IsPDS's feature map Φ and its defining property
K(x,y) = ⟪Φ(x),Φ(y)⟫ are supplied as hypotheses to the two kernel theorems rather than as a
separate "feature mapping associated to a kernel" definition — the book itself treats this as
a given correspondence, not a construction. No numerical constant is altered: 4k/ρ and
log(1/δ) in Theorem 9.2, r²Λ²/m in Proposition 9.3, and 4k and r²Λ²/ρ²/m in Corollary
9.4 are exactly as displayed.
Not formalized: §9.1's discussion of the multi-label case (Eq. 9.2/9.3, the Hamming-distance risk) and Eq. 9.4 (empirical Hamming error) — background for a case this chapter's own generalization-bound section (§9.2) does not cover (the mono-label case only); the multi-class SVM primal/dual optimization problems (§9.3.1, an algorithm derived from Corollary 9.4, not a generalization-theoretic theorem); AdaBoost.MH (§9.3.2, a boosting algorithm, analyzed via a convex-surrogate argument rather than the Rademacher-complexity route this mission formalizes); and the uniform-over- extension mentioned at the end of the Theorem 9.2 proof (an unnumbered remark referencing Theorem 5.9's technique from a different chapter, not restated here). Drafting only the algorithmic consequences (the multi-class SVM's optimization problem) in place of the generalization bounds themselves would be this chapter's trivializing formalization.
Every guarantee in the preceding chapters assumes a fixed distribution and i.i.d. sampling. On-line learning drops both assumptions: an algorithm processes one example at a time, in an adversarial (worst-case) sequence, and is judged by regret against the best fixed comparator in hindsight rather than by generalization error. This chapter develops the theory for this setting — mistake bounds and regret bounds for prediction with expert advice, a margin-based mistake bound for the Perceptron — and then closes a conceptual gap: since on-line algorithms need no distributional assumption, can their guarantees be converted into ordinary distributional (batch) generalization guarantees when the data does happen to be i.i.d.? The on-line-to-batch conversion theorem answers yes, using nothing but an Azuma's-inequality martingale argument on the sequence of hypotheses the algorithm actually produces.
At round t, an on-line algorithm receives x_t, predicts ŷ_t, receives the true label
y_t, and incurs loss L(ŷ_t,y_t); its regret R_T (Eq. 8.1) compares its cumulative loss to
the best fixed action's in hindsight. §8.2 develops this for prediction with expert advice: the
Halving algorithm (realizable case), Weighted Majority and its randomized version RWM
(zero-one loss, Theorem 8.4's L_T ≤ log(N)/(1-β) + (2-β)L_T^min, proved by the chapter's
recurring potential-function technique applied to W_t = ∑_i w_{t,i}), and the Exponential
Weighted Average algorithm (convex losses). §8.3.1 analyzes the Perceptron, a linear
classification algorithm whose margin-based mistake bound (Theorem 8.8, separable case; the
non-separable Theorem 8.11, restated here, in terms of an arbitrary comparator v's hinge
losses) depends only on the normalized margin, not the ambient dimension. §8.4 shows that
averaging the hypotheses h_1,…,h_T an on-line algorithm produces while processing an i.i.d.
sample S yields a hypothesis with controlled true risk: Lemma 8.14 bounds the average of
the per-round risks R(h_t) by the average on-line loss via a martingale argument on
V_t = R(h_t) - L(h_t(x_t),y_t), and Theorem 8.15 upgrades this, via the loss's convexity, to
a bound on the risk of the averaged hypothesis (1/T)∑h_t.
Theorem 8.4 (milestone). Fix β∈[1/2,1). For any T≥1: L_T ≤ log(N)/(1-β) + (2-β)L_T^min; for β=max{1/2,1-√(log(N)/T)}: L_T ≤ L_T^min + 2√(T log N).
Theorem 8.11 (milestone). M ≤ inf_{ρ>0,‖v‖₂≤1}[(r/ρ+√(r²/ρ²+4‖l_ρ‖₁))/2]², where
l_ρ=(l_t)_{t∈I}, l_t=max{0,1-y_t(v·x_t)/ρ}.
Lemma 8.14 (milestone). For any δ>0, with probability at least 1-δ:
(1/T)∑_tR(h_t) ≤ (1/T)∑_tL(h_t(x_t),y_t) + M√(2log(1/δ)/T).
Theorem 8.15 — the mission's goal (first inequality). Under Lemma 8.14's hypotheses, with
L additionally convex in its first argument: for any δ>0, with probability at least
1-δ: R((1/T)∑_th_t) ≤ (1/T)∑_tL(h_t(x_t),y_t) + M√(2log(1/δ)/T).
Theorem 8.15 is the chapter's conceptual capstone: it is the only bridge in the whole book
between the adversarial on-line-learning framework and the distributional PAC/statistical
framework every other chapter develops, and its proof needs nothing beyond Lemma 8.14 plus
convexity — no new machinery, just the right observation about the loss's structure. Theorem
8.4 is the chapter's cleanest instance of its recurring potential-function proof technique
(reused, with variations, for Theorems 8.3, 8.6 and 8.7), and — checked against the platform's
existing OnlineConvexOpt.Introduction.randomized_weighted_majority_mistake_bound (Hazan
series) — a genuinely different result from what is already on the platform: that lemma
bounds a mistake count with a (1+ε) multiplier, this bounds the RWM algorithm's own
weighted-mixture loss with a 1/(1-β) term and a distinct optimal-β substitution,
confirming BRIEF.md's assessment that the two are close but not interchangeable. Theorem
8.11 is the non-realizable generalization of the separable-case Perceptron bound (Theorem 8.8)
that motivates soft-margin algorithms generally, expressed via an arbitrary comparator's hinge
loss rather than assuming perfect separability. No prior art exists for the chapter's other
content: GET /theorems?q=online%20to%20batch returns zero hits, and GET /theorems?q=perceptron returns only an unrelated neural-network topology result.
Theorem 8.4's proof (mirrored by Theorem 8.3's WM analogue) derives matching upper and lower
bounds on the potential W_t, combines them via a logarithm, and substitutes a specific
optimal β found by differentiating the resulting bound — a genuine two-step optimization
argument, not a direct algebraic identity. Theorem 8.11's proof solves a quadratic inequality
in √M after summing the hinge-loss-defining inequalities over the update set I and
invoking the Cauchy-Schwarz step already used in Theorem 8.8's proof; keeping the inf over
both ρ and v in the statement (not fixing them, per BRIEF.md's pitfall note) is what
makes this a genuine bound rather than a bound for one arbitrary choice. Lemma 8.14's proof is
an application of Azuma's inequality (the book's own Theorem D.7) to the martingale difference
sequence V_t = R(h_t) - L(h_t(x_t),y_t), which requires h_t to be measurable with respect
to the history strictly before round t — the on-line algorithm's hypothesis at round t
must not depend on the pair drawn at that same round, per BRIEF.md's pitfall note. Theorem
8.15's step beyond Lemma 8.14 is the passage from the average of T individual risks to the
risk of the averaged hypothesis, licensed by Jensen's inequality under the loss's convexity in
its first argument — dropping convexity breaks exactly this step, not merely weakening a
constant.
GeneralizationError restates chunk 11-regression's Eq. (11.1) convention locally (Y := ℝ,
consistent with that chunk's own harmless simplification), needed here since Theorem 8.15
requires averaging hypotheses into a single real-valued function. OnlineHypothesis A S t is
formalized so that its type signature itself enforces history-adaptedness: the on-line
algorithm A : (n:ℕ) → (Fin n → X × ℝ) → (X → ℝ) is a function of the prefix of the sample
seen so far, and OnlineHypothesis A S t applies it only to S's first t pairs — this is
what licenses Azuma's inequality's martingale-difference argument (the conditional-mean-zero
property of V_t), per BRIEF.md's pitfall note. Revision (2026-09-19), correcting an
earlier claim in this section: history-adaptedness does not by itself guard against
GeneralizationError's Bochner integral silently junking to 0 for a non-measurable
hypothesis (a distinct property — whether h_t, as a function of x, is Measurable — from
whether h_t depends on round t's own draw). Moderation found this a live gap in both Lemma
8.14 and Theorem 8.15's drafted statements; both now carry an explicit hAmeas/hLmeas
hypothesis in addition to the history-adapted type signature.
RWM's w_{t,i}, W_t, p_{t,i}, L_t, L_T, L_{T,i}, L_T^min are modeled as their own
recursively-defined algorithm state (mirroring, but never substituting into, chunk
07-boosting's AdaBoost pattern), matching this chapter's own loss-based (not mistake-count)
quantities, per BRIEF.md's pitfall note distinguishing them from AdaBoost's and RWM-mistake
variants. The Perceptron's w_t, update-index set I, and M = |I| are modeled the same way,
using Eq. (8.23)'s equivalent sign-agreement update rule (the book's own reformulation of
Figure 8.6's sgn-based rule). Theorem 8.11's inf_{ρ>0,‖v‖₂≤1} is a genuine nested restricted
infimum (⨅ ρ ∈ Set.Ioi 0, ⨅ v ∈ Metric.closedBall 0 1, …), not a bound instantiated at fixed
ρ, v, per BRIEF.md's explicit pitfall note. No numerical constant is altered from the
book in any of the four theorems.
Not formalized: Theorems 8.1-8.3 (Halving and WM mistake bounds — the chapter's warm-up
results, superseded in content by the more general RWM/EWA theorems that follow), Theorem 8.5
(a matching lower bound, a distinct impossibility result rather than an algorithm's guarantee),
Theorems 8.6-8.7 (Exponential Weighted Average regret bounds — a third algorithm with its own
potential-function proof, out of scope per BRIEF.md's restriction to §8.2's Halving/WM/RWM),
Theorems 8.8-8.10 (the Perceptron's separable-case bound and its leave-one-out-based expected
generalization bounds, both superseded in generality by Theorem 8.11 for this mission's
purposes), Theorem 8.12 (Perceptron's L²-norm hinge-loss bound, the book's own note that it is
implied by, and looser than, Theorem 8.11's L¹-norm bound), the dual/kernel Perceptron (an
equivalent reformulation, not new generalization content), and Theorem 8.15's second displayed
inequality (a regret-form corollary depending on the regret decomposition of the surrounding
discussion, not drafted per BRIEF.md's own recommendation to commit to the first inequality
as the goal). §8.3.2 (Winnow) and §8.5 (the game-theoretic connection) are out of scope per
BRIEF.md's chapter restriction.
A support vector machine for classification is trained by minimizing a regularized hinge-loss
objective — never the classification loss itself, which is non-convex and computationally
intractable to minimize. Every earlier mission in this series supplies one piece of the argument
that this substitution is nonetheless justified: 01-loss-functions shows the excess hinge risk
controls the excess classification risk (Zhang's inequality); 05-concentration supplies a
Hilbert-space concentration inequality; and Chapter 6 of the book (not itself a mission in this
series, but cited here) combines concentration with a stability argument to bound how far the
empirical SVM solution's regularized hinge risk can be from its population minimum. Steinwart &
Christmann, Support Vector Machines (Springer 2008, Information Science and Statistics), Chapter
8, assembles exactly these three pieces into Theorem 8.1: an explicit, finite-sample,
non-asymptotic bound on how close an SVM classifier's classification risk gets to the Bayes
risk — the payoff result the whole apparatus of Chapters 2, 5 and 6 was built to deliver.
Fix a measurable space and . A loss , a distribution on , the -risk , and the Bayes risk are exactly as in
01-loss-functions, restated locally here. The hinge loss is and the classification loss is .
Let be a reproducing kernel Hilbert space (RKHS) of a kernel over , i.e. a Hilbert space of functions in which point evaluation is represented by an inner product against a feature map with . Write for the kernel's sup-bound. For a sample , the empirical risk is , and the SVM decision function is the minimizer over of — the regularized empirical risk minimizer a practical SVM solver computes. The restricted Bayes risk on is , and the approximation error function is : the price, in excess risk, of restricting attention to at regularization strength .
with -probability at least , for the hinge loss, a separable RKHS with , and such that is dense in . The bound is finite-sample (valid for every fixed , not just asymptotically) and fully explicit: no unspecified constants beyond itself, which is a genuine, computable-in-principle quantity depending on , and , not a placeholder. Making the right-hand side small — e.g. letting slowly as — is exactly what proves an SVM classifier consistent for the classification risk, even though it never optimizes that risk directly.
Three milestones, each the specific instance of an earlier chapter's result that this proof invokes (attack order):
01-loss-functions mission's zhang_inequality, second assertion, restated locally.Chaining these three (with milestone 2 used to rewrite milestone 1's as , then milestone 3 applied to ) is exactly the book's four-line proof of Theorem 8.1.
Theorem 8.1 is this series' capstone: every other chapter's result (loss calibration, RKHS theory, representer theorem, Hilbert-space concentration, the general SVM oracle inequality) is a prerequisite this theorem consumes, and nothing later in the book depends on formalizing it further to be meaningful in its own right — it is already a complete, citable, explicit consistency-and-rate statement for SVM classification. It is also the first result in this series whose statement combines three distinct chapters' machinery into a single inequality, making the "restate the specific instance, not the general machinery" discipline (Hard Rule 9) most visibly load-bearing here: none of Theorem 6.24, Theorem 5.31 or Theorem 2.31 in their full generality is needed, only the narrow slice each contributes to this one proof.
No machine-checked formalization of an SVM classification oracle inequality of this kind is known to exist in a public Lean/Mathlib development (see prior-art search below): statistical learning theory results of this shape (finite-sample high-probability bounds combining regularization, approximation error and concentration) are largely unformalized outside isolated concentration inequalities.
The difficulty here is compositional rather than computational: each of the three milestones is,
in its own chapter, a short consequence of substantial earlier machinery (Theorem 6.24 rests on a
stability argument plus Hilbert-space Hoeffding; Theorem 5.31 rests on continuity of the risk
functional on ; Theorem 2.31 rests on a pointwise case analysis), but none of that earlier
machinery is re-derived here — only the specific numerical instance each milestone hands to
Theorem 8.1's proof. Getting the three instances to compose correctly (in particular, making sure
milestone 1's restrictedBayesRisk and milestone 2's equality target the identical quantity, so
the substitution the book's proof performs is literally available) is the main formalization
risk, not any single proof step.
The probabilistic statement itself is genuinely over the product measure on samples of size , not an expectation or almost-sure claim, and the bounded-kernel hypothesis is load-bearing (it is what fixes the "" and "" constants exactly, not just up to a normalization).
is an arbitrary measurable space; is a general real Hilbert space (NormedAddCommGroup H,
InnerProductSpace ℝ H, CompleteSpace H), not specialized to a concrete function space, matching
the book's own generality. IsRKHSOfKernel, risk/bayesRisk, classLoss/hingeLoss and
empiricalRisk are restated locally in this mission's own Classification sub-namespace — per
Hard Rule 9, a draft mission cannot import another draft's definitions, so these duplicate (with
identical mathematical content) definitions already drafted in 01-loss-functions and
04-representer. IsSVMSolution encodes " minimizes the regularized empirical
risk over " directly as a hypothesis rather than re-deriving existence and uniqueness
(04-representer's territory). DenseInL1 renders " dense in " as an
-approximation property in the seminorm rather than via the Lp subtype, to
keep the statement self-contained without importing Chapter 5's own Lp-space apparatus.
is ∀ x, k x x ≤ 1 (since , Eq. (4.15)).
"With -probability at least " is stated as a lower bound on
(Measure.pi (fun _ : Fin n => P)).real {D | ...}, the -fold product measure of the event.
Theorem 8.2 (Classification with benign kernels), the polynomially-decaying-entropy-number
specialization of Theorem 8.1 stated immediately after it in the book, is deliberately out of
scope for this mission: it requires entropy-number and covering-number machinery (dyadic entropy
numbers , Lemma 6.21's covering-number bound) that none of this
mission's three milestones need, and formalizing it faithfully would roughly double the
mission's scope for a result that is a refinement, not a prerequisite, of Theorem 8.1. A
trivializing formalization of the goal would state the conclusion for an unconstrained
fSVM : (Fin n → X × ℝ) → H with no connection to L, D or λ (making the bound a tautology
about whatever function is supplied, independent of what an SVM actually computes); this is ruled
out here by requiring hfSVM : ∀ D, IsSVMSolution H toFun hingeLoss lam n D (fSVM D), which pins
fSVM D to be an actual minimizer of the regularized empirical hinge risk for that specific
sample D.
01-loss-functions mission (Theorem 2.31, full statement and proof) and
04-representer mission (Chapter 5's RKHS and SVM-solution machinery, in full generality).Weak learning — a base classifier only slightly better than random guessing — is easy to come by; strong learning, in the PAC sense of Chapter 2, is not. Boosting is the technique that turns the first into the second: combine many weak classifiers, each trained on a reweighted version of the sample that emphasizes previously misclassified points, into a single strong ensemble. AdaBoost, the algorithm this chapter studies, does this with a specific, closed-form weighting rule, and comes with two distinct theoretical guarantees: its training error decreases exponentially fast in the number of rounds (Theorem 7.2), and — more surprisingly — its test error can keep improving even after the training error has already reached zero, an empirical phenomenon that Chapter 3's VC-dimension bound cannot explain at all (it predicts overfitting for large numbers of rounds) but that a margin-based analysis, structurally identical to Chapter 5's SVM theory, does (Theorem 7.7). This mission formalizes both routes.
AdaBoost (Figure 7.1) takes a labeled sample with and a base classifier set , and runs for rounds. It maintains a distribution over the sample indices, starting uniform (); at round it selects a base classifier with small -weighted error , sets and , and reweights: . After rounds it returns ; its normalized version is . Since makes , is a genuine convex combination of base classifiers, i.e. a member of the convex hull (Eq. 7.12). The chapter reuses Chapter 5's confidence-margin apparatus (empirical margin loss , Rademacher complexity /) to analyze 's generalization.
Theorem 7.2 (AdaBoost empirical error bound, milestone). The empirical (zero-one) error of satisfies , and, if for all , : training error decays exponentially in whenever every round beats random guessing by a fixed margin (the "edge" ).
Lemma 7.4 (milestone). : the convex hull of a hypothesis set, though generally much larger, has exactly the same empirical Rademacher complexity as the set itself.
Corollary 7.5 (Ensemble Rademacher margin bound, milestone). For a set of real-valued functions and , with probability at least , every satisfies (and the empirical-complexity analogue with an extra additive term) — this is Theorem 5.8's margin bound applied to , then rewritten via Lemma 7.4 so its complexity term is 's own, not the (much larger) convex hull's.
Theorem 7.7 — the mission's goal. Assume for every (so ). Then for any ,
Theorem 7.7's bound is what makes margin theory a genuine explanation of AdaBoost's empirical
behavior: combined with Corollary 7.5 (applied to ), it shows that if
AdaBoost's edge stays bounded away from zero, the empirical margin loss at a fixed
decreases exponentially in while the generalization bound's complexity term does not depend
on at all — so continuing to boost past zero training error can still shrink the true risk,
by growing the margin on the training points that are already correctly classified. This
resolves the puzzle that opens §7.3.1: AdaBoost's test error is empirically observed to keep
decreasing well after its training error hits zero, which the chapter's own earlier
VC-dimension bound on (Eq. 7.9, growing as ) predicts should
eventually overfit, not improve. No prior art on the Prove2Me platform is faithful:
GET /theorems?q=boosting and q=AdaBoost return no hits; this chunk's Rademacher-complexity
apparatus is restated locally (a draft item cannot import chunk 05-svm's or 03-rademacher-vc's
own draft copies) rather than reused, matching the precedent those chunks' own STATUS.md
records recommend for every later chunk needing the same machinery.
Not formalized here: Theorem 7.6 (the VC-dimension-based ensemble margin bound, a direct
corollary of Corollary 7.5 via chunk 03's VC-dimension apparatus) — restating 03's own
machinery a second time for a single further corollary is disproportionate within this
mission's budget, and the chapter's actual capstone targets the sharper, dimension-free
Rademacher-complexity route (Theorem 7.7) instead. Also out of scope: §7.2.2's coordinate-
descent equivalence, §7.2.3's practical (decision-stump) use, and §7.3.4-7.3.5's margin-
maximization LP and game-theoretic interpretation — discussion sections with no numbered result
feeding the goal's proof.
Theorem 7.2's proof needs the telescoping identity (Eq. 7.2), obtained by repeatedly unfolding the recursive weight update — a genuine induction on , not a one-line algebraic manipulation — before the elementary inequality turns the empirical error into a telescoping product of the 's, each of which is then re-expressed in closed form via a case split on . Theorem 7.7's proof reuses the same identity but with an added margin-shift term inside the exponential, requiring the same telescoping machinery plus a separate accounting of against the product of factors coming from each 's own closed form — a proof that shares its main structural step with Theorem 7.2 but is not a trivial corollary of it. Corollary 7.5's proof is Lemma 7.4 (itself a careful supremum-exchange argument using the dual-norm characterization of , not a routine calculation) composed with Theorem 5.8, applied to the specific set rather than a generic hypothesis class — a formalization that stated the corollary only for a "sufficiently nice" abstract class, without deriving it from Lemma 7.4's convex-hull identity, would be proving a different, weaker-provenance statement.
WeightedError, AdaBoostAlpha, AdaBoostNormalizer, AdaBoostDist, AdaBoostEpsilon,
AdaBoostEnsemble, AdaBoostNormalizedEnsemble, EmpiricalError and ConvHull are new,
capturing AdaBoost as an actual algorithm (a genuine recursion on the round index, closed under
Definitions.Def_FoundationsML_Boosting_AdaBoostDist's own recursive equation) rather than an
unspecified "boosting procedure" — the trivialization trap BRIEF.md names for this chapter.
AdaBoostDist takes the sequence of base classifiers actually selected at each round,
h : ℕ → X → ℝ, as external data rather than deriving it via an argmin over H; this is
checked in SELF_REVIEW.md to drop no content either milestone or the goal theorem's statement
actually needs, since neither invokes h_t's optimality, only the weighted error ε_t it
produces under AdaBoost's own distribution D_t. PhiRho, EmpiricalMarginLoss,
MarginGeneralizationError, EmpiricalRademacherComplexity and RademacherComplexity are
restated locally, byte-identical to chunk 05-svm's own copies of Definitions 5.5, 5.6, 2.1
(specialized), 3.1, 3.2 (a draft item cannot import another chunk's draft module); this
duplication collapses once 05-svm and 03-rademacher-vc are uploaded and listed in
missions/README.md's "Published definitions" table. No numerical constant in any of the four
theorems is altered from the book's own displayed form. A trivializing formalization this
mission avoids: stating Theorem 7.2/7.7 for an arbitrary sequence of error rates
satisfying , disconnected from any actual
algorithm — AdaBoostEpsilon instead ties every ε_t to the weighted error AdaBoost's own
recursively defined D_t assigns to its own selected h_t, so the bound is provably about
this algorithm's error trajectory, not an arbitrary one.
Modern regression problems routinely have far more candidate predictors than observations: genomics with tens of thousands of genes and a few hundred patients, signal recovery from far fewer measurements than the signal's ambient dimension, image reconstruction from an undersampled set of linear projections. In every such setting the classical least-squares estimator is either undetermined or hopelessly noisy, and the ordinary theory of linear regression, built for , has nothing to say.
The Lasso — -penalized least squares, introduced by Tibshirani (1996) — is the workhorse response: penalize the least-squares objective by the -norm of the coefficient vector, which both drives many coordinates exactly to zero and remains a convex, tractable program. What is far from obvious a priori is that this convex relaxation is not just computationally convenient but statistically correct: under a condition on the design matrix, its estimation error is controlled at a rate matching what one could hope for even knowing the true support in advance. Wainwright's High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 7, gives the deterministic backbone of this guarantee — the part of the argument that holds for any noise vector and any design matrix satisfying a single geometric condition, before any probability is introduced.
Consider the linear model , where is a known design matrix, is an unknown coefficient vector, and is a noise vector, observed together with the response . Write and . The Lagrangian Lasso is the convex program
with regularization parameter chosen by the user.
Say is supported on if for every , and write for its sparsity. For a subset and a constant , the cone
collects the directions in which an estimation error concentrated near the true support can plausibly point. The matrix satisfies the restricted eigenvalue (RE) condition over with parameters if
Ordinarily, when , the quadratic cost's Hessian is rank-deficient and has a large flat subspace, so no uniform positive-curvature bound like this can hold over all of ; the RE condition asks for curvature only along the cone that the Lasso's own optimality actually forces its error into.
The companion notion — the restricted nullspace property, — is the noiseless analogue: it is exactly the condition under which the -relaxed basis pursuit program s.t. exactly recovers every -sparse from (Theorem 7.8). A small pairwise incoherence is one simply-checked sufficient condition for it (Proposition 7.9).
Under (A1) supported on , , and (A2) satisfies the RE condition over with parameters : for any solving the Lagrangian Lasso with ,
The bound is the deterministic core underneath every high-dimensional consistency guarantee for the Lasso: once a statistician checks that a particular random design (Gaussian, sub-Gaussian, or otherwise) satisfies the RE condition with high probability, and bounds using concentration of the noise, this one inequality converts directly into a rate — Wainwright's own Examples 7.14–7.15 do exactly this for the classical Gaussian linear model and for compressed sensing. It also isolates why the Lasso is competitive with an oracle that already knows the support: the rate (up to log factors, once is instantiated) is the same order one would get regressing only on the true coordinates.
The theorem is already proved in the source; this mission's contribution is a machine-checked formal statement (and, eventually, proof) of the bound together with its two supporting structural results, in a form that composes with the rest of this book's formalized chapters and with any future formalization of the concentration arguments (Chapters 2–6) that supply 's numerical value in specific models.
The proof is short but every step leans on getting the cone membership exactly right. The first hurdle is showing the error lands in at all — this needs the Lagrangian basic inequality (from 's optimality against ), not the simpler constrained-Lasso argument used for parts (b)/(c), and the constant (not ) comes precisely from the factor of in the bound combined with Hölder's inequality on the noise term. A tempting shortcut is to assume the uniform curvature bound (7.24), for all — but in the regime this uniform bound is never satisfiable, since has a -dimensional null space; the entire point of the restricted eigenvalue condition is to demand curvature only on the cone the optimality argument already produces.
, , , are unconstrained vectors/matrices over
Fin n/Fin d-indexed reals; is a Finset (Fin d). The RE condition's constant
is required positive, since the book divides by it throughout the discussion
of Theorem 7.13 even though Definition 7.12 itself states the condition schematically;
is fixed to the book's own value, not a free parameter of the goal. The
- and pairwise-incoherence suprema are real iSups over finite index
types, which default to Mathlib's junk value at dimension — a degenerate
corner with no vector to measure, not a trivializing case of the theorem's actual
content. A trivializing formalization would drop the final-sentence -bound as
"a trivial Cauchy–Schwarz corollary" or silently substitute the stronger, later-defined
restricted isometry property for the restricted eigenvalue condition; this mission
does neither. Parts (b) (constrained Lasso) and (c) (relaxed basis pursuit) of
Theorem 7.13, and the primal–dual-witness support-recovery result (Theorem 7.21), are
out of this mission's scope; a full-strength companion mission covering them,
including the RIP-based Proposition 7.11 and the random-design certification
Theorem 7.16, is natural future work.
Random matrices with independent rows are the workhorse of high-dimensional statistics and compressed sensing: sample covariance matrices, sub-sampled measurement operators, and randomized sketches are all of this form. A basic question about such a matrix is how close stays to its typical size — not just for one fixed , but simultaneously for every in some set of interest (a sphere, a cone, the difference set of a data cloud). A bound that holds only pointwise in is of limited use, since most applications need to reason about the worst case over an entire geometric set at once.
This chapter proves such a uniform bound — the matrix deviation inequality — for matrices with independent, isotropic, sub-gaussian rows, controlling the deviation by a single geometric parameter of , its Gaussian complexity. The result is a direct descendant of the chaining machinery of Chapter 8 (via Talagrand's comparison inequality, Chapter 8.6) and, in this book's own account, subsumes several results proved earlier by other methods — two-sided bounds on random matrices, the Johnson-Lindenstrauss lemma for infinite sets — while also yielding two new consequences central to high-dimensional convex geometry: the bound and the Escape theorem, both controlling how a random subspace intersects a fixed geometric set.
Fix a probability space . A random vector in is isotropic if its covariance matrix is the identity, — equivalently (the book's own Lemma 3.2.3), for every . The sub-gaussian norm of a random vector is , the supremum over the unit sphere of the scalar sub-gaussian (Orlicz ) norm of its one-dimensional marginals; is sub-gaussian when this is finite.
Fix a standard Gaussian random vector in (a vector whose coordinates in any orthonormal basis are independent standard normal). For a subset , the Gaussian width and Gaussian complexity of are
two closely related measures of the geometric size of — "cousins" that agree up to a factor of whenever contains the origin, and agree exactly when is origin-symmetric.
for every matrix whose rows are independent, isotropic, sub-gaussian random vectors with , and every (whenever is finite). is the book's own unnamed absolute constant, hard-coded to no numeral — the weakest stable form of the claim.
for the same class of matrices and any bounded , where is the (random) kernel of , a subspace of codimension at most . A direct one-paragraph consequence of the goal theorem (apply it to , then restrict to , where vanishes).
The matrix deviation inequality converts a purely algebraic quantity — how close stays to — into a single geometric parameter of the index set , letting it subsume, via specializations of , results that were previously proved by separate ad hoc arguments: two-sided singular value bounds on random matrices ( a sphere), Johnson-Lindenstrauss-type embeddings for possibly infinite point sets ( a difference set), and covariance estimation. The bound is one of the two classical consequences the book develops fresh from the inequality (the other, the Escape theorem, is outside this mission's scope): it answers, quantitatively, how large a random affine section of a fixed convex body typically is, a question at the heart of the local theory of Banach spaces and of compressed sensing's recovery guarantees (Chapter 10 builds directly on this chapter's machinery). Both results have long-standing, well-understood classical proofs; this mission formalizes their statements, not open research.
The natural first idea — bound pointwise for a fixed using concentration of the norm of a sub-gaussian random vector, then take a union bound over — only works when is finite, and gives a bound that scales with rather than with the actual geometric size of . The book's actual route treats , indexed by , as a genuine random process and shows it has sub-gaussian increments () — itself a nontrivial fact proved in stages (first for a single unit vector via concentration of the norm, Theorem 3.1.1; then for a pair of unit vectors via a squared-process argument; only then in full generality) — and then invokes Talagrand's comparison inequality (a consequence of the chaining machinery of Chapter 8) to pass from sub-gaussian increments directly to a bound in terms of Gaussian complexity, without ever performing a union bound over itself.
A is represented by its rows, A : Fin m → Ω → EuclideanSpace ℝ (Fin n), with ‖Ax‖₂ recovered
as Real.sqrt (∑ i, ⟨Aᵢ,x⟩²) rather than constructing A as a Matrix/LinearMap — this
matches the book's own row-by-row hypotheses exactly and is what both theorems' own proofs use
directly. IsIsotropic is formalized via the book's basis-free Lemma 3.2.3 characterization
(E⟨X,x⟩² = ‖x‖² for every x) rather than the matrix equation Σ(X)=Iₙ, avoiding a fixed-basis
covariance-matrix construction the rest of this chunk's definitions do not otherwise need.
SubgaussianVectorNorm reuses the published scalar subgaussianNorm. GaussianWidth and
GaussianComplexity realize the standard Gaussian vector g ∼ N(0,Iₙ) as the identity map on
Mathlib's own standard Gaussian measure on a finite-dimensional inner product space
(ProbabilityTheory.stdGaussian), and both, together with the goal's own left-hand side, use a
locally-defined finite-marginal expected-supremum convention (ExpSup, EReal-valued) matching
the book's own footnote-3 convention (Section 7.2), reused throughout the series. Both theorems'
right-hand sides presuppose their respective geometric parameter ( or ) is a
finite real number; since both are EReal-valued in general, each theorem takes an explicit real
witness together with a proof that it equals the true value — the same finiteness-disclosure
pattern 07-chaining's Dudley inequality uses for its own right-hand integral, needed here for
exactly the same reason (the book's own display does not spell out why the quantity is finite,
true whenever is bounded, as in every application). (and, in the milestone, the same
again — the two are not asserted equal, matching that the book states them as two separate
"absolute constants") is existentially quantified before every type, instance and hypothesis it is
uniform over. The bound milestone (m_star_bound) additionally carries the hypothesis
: its conclusion divides by , and without this hypothesis Lean's real-division
convention () makes the right-hand side at regardless of — false
whenever has positive diameter, not merely a weaker or vacuous claim. The book's own proof
("Dividing by yields …", p. 241) already implicitly assumes , matching every
other use of in the chapter as a positive count of measurement rows.
A trivializing formalization would fix to be a finite set, collapsing the goal to the
elementary union-bound case the book explicitly contrasts its own more general statement against
(Section 9.1's opening paragraph: "we may choose an arbitrary subset "); this
mission's goal quantifies over an arbitrary Set (EuclideanSpace ℝ (Fin n)) to rule that out.
This mission covers Theorem 9.1.1 and Theorem 9.4.2 only; Theorem 9.4.7 (the Escape theorem) and
Theorem 9.2.4 (covariance estimation for lower-dimensional distributions), both named as candidate
milestones, are left out for lack of session time given the substantial shared infrastructure this
chapter needed from scratch. ExpSup, IsIsotropic, SubgaussianVectorNorm, GaussianWidth and
GaussianComplexity are reusable by any later chapter needing an isotropic or sub-gaussian random
vector, or a Gaussian-width-type quantity (Chapters 4, 10, 11 of this same book series all use one
or more of these notions). Solvers' contributions are welcome on: Theorem 9.1.3 (the sub-gaussian
increments of the deviation process, the technical heart of the goal's proof), Talagrand's
comparison inequality itself (outside this mission, in 07-chaining's companion chapter), and the
one-paragraph reduction from the goal to the bound.
Chapter I's usual stochastic order compares two real-valued random variables by "how large" they tend to be. Chapter VI lifts the same idea to random vectors: is smaller than in the usual multivariate stochastic order if is less likely than to land in any upper set of — any region defined by "at least this large in every coordinate." This mission formalizes that order and its two founding characterizations: a coupling theorem (the direct -dimensional generalization of Chapter I's own coupling theorem) and a common-source representation, plus two closure properties that make the order usable in practice.
Let be a random vector taking values in on a probability space , and let be a random vector taking values in on a (possibly different) probability space . is smaller than in the usual multivariate stochastic order, written , if
where an upper set is one closed upward under the coordinatewise partial order on ( iff for every ). Equivalently, iff for every increasing (increasing with respect to that same coordinatewise order) for which the two expectations exist — the form this mission drafts as the definition, exactly parallel to the univariate order's own equivalent form.
This is the direct -dimensional generalization of Chunk 01's Theorem 1.A.1: a joint law on the random vectors' shared space realizing as an almost-sure coordinatewise inequality between copies. The book does not give this direction's proof here (an explicit construction appears later, in a special case irrelevant to a statements-only mission), and the claim is exactly as citable either way.
The usual multivariate stochastic order is the natural tool for comparing random vectors — costs, resource-usage profiles, portfolio returns — that must be ranked simultaneously across several coordinates rather than reduced to a single scalar summary first. It underlies simulation comparisons (via the coupling and common-source characterizations, both constructive), reliability comparisons of multi-component systems (whose component lifetimes are naturally vector-valued), and comparative-statics arguments in queueing and inventory models with several state variables. The closure properties are what make the order compositional: conjunction closure says a vector-by-vector comparison of independent inputs survives any coordinatewise-increasing post-processing, and marginalization closure says a joint comparison restricts consistently to any sub-collection of coordinates — together they are the two properties an analyst reaches for first when reducing a multivariate comparison to a more tractable one.
No platform prior art exists: GET /theorems?q=stochastic+order and q=coupling return zero
genuine hits (checked at this book's triage time, re-confirmed this session). This mission
restates the usual multivariate stochastic order and its two founding theorems as a
self-contained foundation, in the same spirit as Chunk 01's univariate mission but independently
drafted, since drafts cannot import each other's Lean.
The chief formalization risk this chapter's own brief flags is conflating "increasing" for
with some order other than the coordinatewise one (a total
order via a fixed embedding, or a lexicographic order): the book's order on is
always the componentwise partial order, and Mathlib gives Fin n → ℝ exactly that order by
default (its Pi/product order), so Monotone φ for φ : (Fin n → ℝ) → ℝ already means what the
book means with no extra predicate to get wrong — but it would be easy to instead encode
ℝ^n-valued objects some other way (e.g. a fixed linear functional into ℝ) that silently swaps
in a different, weaker order. The second risk is Theorem 6.B.16(b)'s literal codomain: the book
states (scalar), so the closure conclusion is a genuinely
univariate stochastic-order statement about applied to vector inputs, not a
vector-to-vector closure (that is part (a), not drafted here) — stating it as a multivariate
conclusion by mistake would silently strengthen a theorem the book does not claim.
Random vectors are drafted as functions into Fin n → ℝ from arbitrary measurable spaces, which
inherit Mathlib's default coordinatewise (Pi) order — the same order the book uses throughout
this chapter, requiring no separate order predicate. MultivariateOrder μ ν X Y quantifies over
φ : (Fin n → ℝ) → ℝ with Monotone φ in that order and Integrable (φ ∘ X) μ/Integrable (φ ∘ Y) ν stated inside the ∀, exactly matching "for which the expectations exist." Equality in
law is ProbabilityTheory.IdentDistrib. Theorem 6.B.2's random variable is drafted as
-valued specifically (not an arbitrary-type common source), matching the book's own
"for all " quantification exactly.
Theorem 6.B.16(b) is drafted for a common dimension across all rather than the
book's per- dimension : the concatenated input then lives in Fin m → Fin n → ℝ (nested
Pi types, carrying the coordinatewise order on exactly as needed), avoiding a
dependent-sum concatenation of vectors of genuinely different lengths that a mission of this size
does not justify. This is the "closed under convolutions" special case the book itself names as a
corollary of the general statement, not a different claim — but it is a genuine restriction of
scope, recorded here rather than silently applied, and the general varying-dimension statement is
left for a future pass (see STATUS.md). The theorem's conclusion is stated as the univariate
order's own defining inequality on ℝ (∀ x, μ {ω | x < ψ(X_∙ ω)} ≤ ν {ω | x < ψ(Y_∙ ω)}),
restated locally rather than importing Chunk 01's UsualOrder, since drafts cannot import
another mission's definitions. Theorem 6.B.16(c)'s sub-index set of size
is encoded as an injective reindexing r : Fin k → Fin n, with drafted as X, Y
precomposed coordinatewise with r, matching the book's own subvector notation (6.A.1) exactly.
A trivializing formalization this mission rules out: drafting MultivariateOrder with an
order on Fin n → ℝ other than the coordinatewise one (for instance, a fixed linear functional
collapsing the vector to a scalar and reusing the univariate order), which would silently state a
different, generally weaker order under the same name; and drafting Theorem 6.B.16(b)'s conclusion
with a vector-valued (rather than the book's literal scalar-valued) , which would silently
strengthen a theorem the book states only for real-valued . This mission draws on no
platform prior art (searches for "stochastic order" and "coupling" as of 2026-09-18 return zero
genuine matches). Reusable beyond this mission: the MultivariateOrder definition pattern and its
coupling/common-source characterization parallel Chunk 01's univariate pair closely enough that a
future chapter needing a multivariate order's own coupling theorem (Chapter VII's multivariate
convex order is the direct next instance in this series) could restate the same shape with minimal
adaptation.
StochasticOrders.Usual), for the univariate usual stochastic order and
its coupling/common-source characterizations this chapter directly generalizes.Many questions in high-dimensional probability reduce to bounding the expected supremum of a random process — the maximum, over an entire indexed family of random variables, of how large any one of them can get. When is finite this is routine (a union bound over terms suffices), but the interesting cases have infinite, even uncountable: a supremum over a continuum of test functions, a norm expressed as a supremum over a sphere, or an empirical process indexed by a whole class of functions. A naive union bound is unusable here, since is infinite.
R. M. Dudley's 1967 entropy bound (R. M. Dudley, The sizes of compact subsets of Hilbert space and continuity of Gaussian processes, Journal of Functional Analysis 1 (1967), 290–330) resolved this for Gaussian processes, controlling the expected supremum purely in terms of the metric entropy of — how many balls of radius are needed to cover , at every scale . The technique behind the proof, chaining, builds a sequence of increasingly fine finite approximations to and telescopes the resulting bounds; it is one of the central tools of the field, reused throughout empirical process theory, statistical learning theory (via Vapnik-Chervonenkis theory), and non-asymptotic random matrix theory. This mission formalizes the chapter's generalization of Dudley's bound beyond Gaussian processes, to any process with sub-gaussian increments, together with the purely combinatorial Sauer-Shelah lemma that the chapter's applications to statistical learning theory build on.
Fix a probability space . A random process is a family of real random variables on indexed by an arbitrary set , with no independence or measurability-of-the-supremum assumed between different 's. Since need not be measurable in for a general index set , its expectation is understood — following the book's own convention, set once in Chapter 7 and reused throughout — through the process's finite-dimensional marginals:
Now fix a metric on , making a metric space. The covering number , for , is the smallest cardinality of a finite -net of : a finite set such that every point of lies within distance of some point of (or if no finite -net exists). The quantity is the metric entropy of at scale : it measures how large looks when resolved only down to scale .
A process has sub-gaussian increments with parameter if
where is the sub-gaussian (Orlicz) norm of Chapter 2: the smallest with . This says the increments of the process are controlled by the metric the way a Gaussian process's increments are controlled by its own canonical metric — but without assuming is Gaussian.
A class of Boolean functions on a set shatters a subset if every function arises as the restriction to of some . The VC (Vapnik-Chervonenkis) dimension is the largest cardinality of a subset of shattered by (or if arbitrarily large finite subsets, or an infinite one, are shattered) — a purely combinatorial measure of how rich the class is.
for every mean-zero random process on a metric space with sub-gaussian increments parameter , whenever the integral is finite. is the book's own unnamed absolute constant, never depending on , , or the process. This is the weakest stable form of the claim: no numeral is hard-coded for , and the statement asks only for the shape of the bound, matching what the book actually proves.
for every class of Boolean functions on a finite -point set . This is a purely combinatorial fact, with no probability involved, but it is the bridge (via the covering-number bound Theorem 8.3.18, outside this mission's scope) between the chapter's Dudley-inequality engine and its statistical-learning applications — a bound on how large a finite class of Boolean functions can be, in terms of a single combinatorial complexity parameter.
Dudley's inequality is, in the book's own words, "the main result" of the chaining chapter: it converts a purely geometric quantity — the metric entropy of an index set, computable in many cases from covering-number estimates already available for balls, ellipsoids, and other convex bodies — into a probabilistic control on the size of a random process indexed by that set. This is what lets later chapters (uniform laws of large numbers over function classes, the matrix deviation inequality, the Dvoretzky-Milman theorem on almost-spherical sections of convex bodies) bound suprema over infinite, even uncountable, index sets without ever performing a union bound. The bound is also known to be tight only up to a logarithmic factor in general — Sudakov's minoration inequality (Chapter 7) gives a matching lower bound for Gaussian processes, and the book's own Exercise 8.1.12 exhibits a set where the two bounds genuinely diverge — so the constant here cannot in general be sharpened away.
The Sauer-Shelah lemma is one of the two founding results of VC theory (together with the Glivenko-Cantelli-type uniform convergence it feeds into), independently discovered by Vapnik and Chervonenkis, Sauer, and Shelah in the early 1970s; it underlies the sample-complexity bounds of statistical learning theory (a hypothesis class with finite VC dimension is PAC-learnable) and, through Theorem 8.3.18, gives one of the two standard routes (the other being direct combinatorial counting) to bounding covering numbers of infinite function classes.
Both results are decades old and have long-established, standard proofs; no open mathematical
question is being formalized. What this mission contributes is the machine-checked statement
infrastructure — the goal and the Sauer-Shelah milestone, together with the definitions
(CoveringNumber, ProcessESup, Shatters, VcDim) a faithful Lean rendering of either result
needs — for a solver to close with a proof. No formalization of Dudley's inequality or the
Sauer-Shelah lemma is known to exist on the platform prior to this mission.
The natural first idea for bounding is a single-scale -net argument: replace by a finite -net, bound the maximum over the (finite) net by a union bound using the sub-gaussian tail, and separately bound the error of replacing by the net using the Lipschitz-in-probability control the sub-gaussian-increments hypothesis gives. This works, but it only ever sees at one fixed resolution , and optimizing over afterward gives a bound with an extra -type loss that does not match Dudley's inequality. The actual difficulty is genuinely multi-scale: chaining builds a whole sequence of nets at dyadic scales simultaneously, connects each point of to its nearest net point at every scale to form a "chain" of successive approximations back to a single fixed basepoint, and telescopes the resulting sum of increments — turning itself into a sum of differences between successive links of the chain, each individually well controlled by the sub-gaussian hypothesis at its own scale. Passing from the resulting discrete sum over dyadic scales (Theorem 8.1.4) to the continuous integral of the goal is a further, separate technical step.
For the Sauer-Shelah lemma, the natural first idea — bound directly by counting — has no obvious purchase on an arbitrary class of Boolean functions. The actual argument goes through Pajor's lemma, which reduces bounding to counting the shattered subsets of instead of the functions in themselves; only then does the cardinality bound on shattered sets become directly usable, via a binomial-sum estimate.
CoveringNumber T ε is ℕ∞-valued (ℕ∞ = WithTop ℕ), defined as the infimum, over the subtype
of finite -nets of the whole type T (an instance of MetricSpace T), of their
cardinality; the infimum of the empty family in this complete lattice is ⊤, reproducing " if no finite net exists" with no case split. ProcessESup is EReal-valued, defined as
the supremum over finite nonempty of the Bochner integral of the finite max —
EReal, not ℝ, because a real-valued supremum would silently return the junk value if the
family of marginal expectations were unbounded above. Shatters and VcDim are direct
transcriptions of Definition 8.3.1, with VcDim valued in ℕ∞ via a supremum of Set.encard
over the (always-nonempty, since is trivially shattered) subtype of shattered
subsets. The goal's mean-zero hypothesis is stated as Integrable (X t) P ∧ ∫ X t = 0 rather than
the bare equation, since a non-integrable variable's Bochner integral is 0 in Mathlib by
convention regardless of its true mean — a bare-equation hypothesis would let a non-mean-zero,
non-integrable process satisfy the theorem vacuously. Two further hypotheses make explicit what
the book's own displayed statement treats as understood without spelling out: that
is finite for every (total boundedness of ), and that the
resulting integrand is integrable on — both hold whenever is totally bounded,
since the integrand vanishes once , so neither hypothesis excludes
any case the book's own proof does not also need. [Nonempty T] excludes the degenerate empty
index set. The absolute constant is existentially quantified ahead of every type, instance,
and hypothesis it is uniform over, and pinned to no numeral, matching " is an absolute
constant" — a formalization hard-coding a specific numeral for would be invalidated by the
next sharper constant in the literature and would not match what the book proves.
A trivializing formalization of the Sauer-Shelah lemma would fix at a hard-coded
small value, or drop the second (exponential) inequality in favor of the weaker first one; this
mission's statement keeps both inequalities, with genuinely computed from VcDim, and handles
the boundary (where the exponential bound's base involves a division by zero under Lean's
x/0=0 convention) explicitly rather than excluding it, since x^0=1 still recovers the book's
correct bound there.
This mission covers Theorem 8.1.3 and Theorem 8.3.16 only; Theorem 8.3.18 (covering numbers via VC
dimension) and Theorem 8.2.3 (the uniform law of large numbers, the chapter's direct application
of Dudley's inequality) are left out, not approximated, for lack of the additional empirical-
process measurability machinery — the class of Lipschitz functions of Eq. (8.22), measurability of
the resulting empirical process — that a faithful statement of either would need beyond what this
mission's items already provide. CoveringNumber and ProcessESup are reusable by any later
chapter needing a metric space's covering numbers or a general random process's expected
supremum (this book's own Chapters 7, 9, and 11 all use one or both); Shatters and VcDim are
reusable by any later development of VC theory or statistical learning theory. Solvers'
contributions are welcome on: the chaining argument itself (the mission's hardest open leaf, via
the discrete dyadic form of Theorem 8.1.4), Pajor's lemma underlying Sauer-Shelah, and the
binomial-sum estimate closing its second inequality.
Chapter I's usual stochastic order compares "how large" two random variables tend to be; Chapter III's convex order compares "how spread out" they are, holding the mean fixed. Chapter IV's increasing convex and increasing concave orders combine the two: says is both smaller and less variable than in a single comparison, without forcing equal means. These are the orders a decision-maker with risk-averse (concave-utility) or risk-loving (convex-cost) preferences actually uses to rank random outcomes, since expected utility is exactly an expectation of an increasing concave or convex function. This mission formalizes both orders and their coupling characterization: the submartingale/supermartingale analogue, one chapter over, of Chapter III's Strassen martingale coupling for the plain convex order.
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 increasing convex order, written , if
and smaller than in the increasing concave order, , if the same holds for every increasing concave . Taking (increasing and both convex and concave) gives under either order — unlike the convex order, no equality of means is forced. Two equivalent tail-integral characterizations (Theorem 4.A.2) make the orders tractable: iff for every , and iff for every , where and are the survival and distribution functions.
Furthermore, can be chosen so that stochastically increases with (in ). This is the increasing-convex analogue of Chapter III's Theorem 3.A.4: instead of a martingale, need only be a submartingale — the copy of is, conditionally on the copy of , at least a fair randomization of it. The book states its proof is "similar to the proof of Theorem 3.A.4" and calls the constructive direction "not easy to prove"; this mission states the theorem faithfully, including the "Furthermore" strengthening, without attempting a proof.
The same theorem's other bracketed case: iff there exist on a common space with , , and a supermartingale, a.s. — note the swapped roles of and in the conditioning relative to the increasing-convex case, not merely a flipped inequality. Drafted as a separate Lean theorem from the goal (see Formalization scope), since the two conditioning structures are genuinely different predicates, not sign-flipped rewrites of one another.
The increasing convex and concave orders are the natural language of expected-utility comparisons: a risk-averse agent with concave utility prefers to exactly when implies for every increasing concave — the order is defined precisely so that "every risk-averse agent with increasing utility agrees" collapses to one comparison. In operations research this underlies stochastic dominance of the second kind in portfolio and inventory models, and the increasing-convex order similarly formalizes "second-order stochastic dominance for costs" used to compare random cost/loss distributions under risk-loving or regret-averse preferences. The submartingale-coupling characterization is what turns the intractable "for every increasing convex " quantifier into a single explicit construction, exactly as Strassen's theorem does for the plain convex order — and, being the direct chapter-IV successor to Chapter III's coupling theorem in this series, it fixes the second data point for what a "coupling-characterization" mission in this book's series looks like when the order being characterized is not symmetric between the two variables' roles.
No platform prior art exists: GET /theorems?q=increasing+convex, q=increasing+concave, and
q=submartingale return zero genuinely matching hits (the one submartingale hit, a bandit
subgaussian maximal inequality, uses Doob's inequality for a concentration bound, not this
order). This mission restates the increasing convex/concave orders and their coupling
characterization as a foundational, self-contained pair of definitions, parallel in structure to
Chunk 03's convex-order mission but independently drafted (drafts cannot import each other's Lean).
The chief formalization risk is the one this chapter's own brief flags explicitly: the book states
Theorem 4.A.5 as a single statement with bracketed alternatives (" [] iff
… is a submartingale [ is a supermartingale] …"), and the
two cases are not symmetric rewrites of each other — the conditioning variable in
E[Ŷ|X̂]≥X̂ swaps to E[X̂|Ŷ]≤Ŷ in the concave case, not just a flipped inequality on the same
conditioning. A Lean statement that tried to unify both cases with a single Or or a naive
sign-flip would either conflate two different predicates or silently state the wrong condition for
one of the two cases. The duality theorem (4.A.1) compounds this risk in the other direction: its
content is exactly that and are related (by negating the variables), so a
formalization that makes this equivalence provable by unfolding definitions (rather than as a
genuine ↔ between two independently-stated predicates) would trivialize the one theorem whose
entire content is that relationship.
Random variables are measurable functions into from arbitrary measurable spaces,
matching this series' convention; IcxOrder μ ν X Y and IcvOrder μ ν X Y are drafted as two
separate definitions (not one order parametrized by an Or of function classes), each
quantifying over Monotone φ ∧ ConvexOn ℝ Set.univ φ (resp. ConcaveOn) with the two
expectations' existence stated as explicit Integrable hypotheses inside the ∀, exactly as
Chunk 03's ConvexOrder. Equality in law is ProbabilityTheory.IdentDistrib. The goal's
submartingale condition uses Mathlib's conditional-expectation notation X̂ ≤ᵐ[ρ] ρ[Ŷ | m] with
m the σ-algebra generated by X̂; its companion's supermartingale condition uses ρ[X̂ | m'] ≤ᵐ[ρ] Ŷ with m' generated by Ŷ instead — the conditioning variable is genuinely swapped between the
two theorems, matching the book's own bracket ordering {X̂,Ŷ} vs. {Ŷ,X̂}. The "Furthermore"
clause in both is kept (not dropped), via Mathlib's ProbabilityTheory.condDistrib, restated as
the relevant conditional-distribution kernel's survival function being monotone at every
threshold — the same shape Chapter I's UsualOrder and Chunk 03's goal theorem use, necessarily
restated locally since drafts cannot import another mission's definitions.
Theorem 4.A.1 (duality) and Theorem 4.A.8(d) (convolution closure) are each drafted as a single
Lean theorem with two independent conjuncts (an ∧ of two ↔s, or of two implications), one per
bracketed case, since the book states both cases as the two halves of one theorem sharing every
hypothesis — this is not the same shape as the goal/companion split, where the two cases have
genuinely different internal structure (the swapped conditioning) rather than a shared statement
instantiated at two function classes. A trivializing formalization this mission rules out:
stating Theorem 4.A.1's duality by relabeling IcvOrder as IcxOrder applied to negated
arguments (making the equivalence a rfl or single simp unfolding) rather than keeping the two
orders as independently-defined predicates whose relationship is the theorem's actual content.
This mission draws on no platform prior art (searches for "increasing convex", "increasing
concave", and "submartingale" as of 2026-09-18 return zero genuine matches — the sole
submartingale hit is an unrelated bandit concentration inequality via Doob's inequality). Reusable
beyond this mission: the IcxOrder/IcvOrder definition pattern and the
submartingale/supermartingale coupling shape parallel Chunk 03's ConvexOrder
martingale-coupling pattern closely enough that a future chapter needing "coupling
characterization of a location-and-spread order" (none of the remaining chapters currently in
this series' first wave) could restate the same shape with minimal adaptation.
StochasticOrders.Convex), for the plain convex order and Strassen's
martingale coupling this chapter's submartingale/supermartingale coupling directly generalizes.The support vector machine and every other kernel method (Gaussian processes, kernel ridge regression, kernel PCA) is specified by choosing a kernel: a function measuring similarity between two inputs, used in place of an inner product on the raw data. This lets a linear algorithm implicitly work in a very high- or infinite-dimensional feature space without ever computing a feature vector explicitly (the "kernel trick"). The definition of a kernel most directly tied to this trick — for some feature map into a Hilbert space — is exactly the definition that makes verifying a candidate similarity function is a valid kernel hard: it asks for an explicit Hilbert space and map that in practice nobody wants to construct by hand.
Schoenberg's theorem (1938, for a special class of functions on the sphere) and the general theory developed by Aronszajn and others through the mid-20th century established the alternative used ever since: a function is a kernel exactly when it is symmetric and positive definite, a checkable condition on finite point sets alone. Steinwart & Christmann, Support Vector Machines (Springer 2008, Information Science and Statistics), Theorem 4.16 gives the modern, self-contained real-Hilbert-space proof of this equivalence, and it is the theorem every later construction in the book's kernel chapter (sums, products, limits, and the specific kernel families used in practice) rests on.
Fix a non-empty set (the input space; no further structure is assumed). A function is a kernel on if there exist a real Hilbert space and a feature map such that
Neither nor are determined by : for , admits both the identity map on and as feature maps.
Separately, is symmetric if for all , and positive definite if, for every , every , and every ,
equivalently: the Gram matrix is positive semidefinite for every finite point set. This condition mentions only , , and finite sums — no Hilbert space at all.
The forward direction is elementary (a two-line computation from the feature-map definition, recorded in the book just before the theorem statement). The goal is the full equivalence, including the converse: a symmetric, positive definite function, given with no reference to any ambient Hilbert space at all, is nonetheless a kernel.
Neither is a hypothesis Theorem 4.16's own proof consumes; both are included as further chapter results built on the same two definitions, chosen because they are the tools the book uses immediately afterward to construct concrete kernels (polynomial kernels, kernels given by convergent power series) without exhibiting a feature map for each one by hand, and because Corollary 4.17's one-line proof ("every is symmetric and satisfies (4.5); therefore so is the pointwise limit ") only makes sense once Theorem 4.16 is available as the bridge back to "is a kernel".
Theorem 4.16 is the single result that turns "is a kernel" from an existential, non-constructive question (does some Hilbert space and feature map exist?) into a universal, checkable one (does a finite-dimensional matrix inequality hold for every finite point set?). Every kernel actually used in the book from this point on — polynomial kernels, the Gaussian RBF kernel, kernels built from Taylor or Fourier series — is verified to be a kernel via this characterization, not by exhibiting a feature map directly (an infinite-dimensional one, in most of these cases). Lemma 4.5 and Corollary 4.17 are the two closure properties that make positive-definiteness verification compositional: a new kernel is usually built as a sum, nonnegative multiple, product, or limit of kernels already known to be positive definite, rather than checked from scratch.
The result itself is classical (Schoenberg 1938 for the special case relevant to distance-based kernels on spheres; the general Hilbert-space statement is standard by the mid-20th century, see Aronszajn 1950's RKHS paper and Berg–Christensen–Ressel's monograph). No machine-checked Lean proof of this specific real-Hilbert-space equivalence is known to exist on the platform at the time of writing (see prior-art search below); this mission asks for its formalization exactly as the book states and proves it, via the explicit pre-Hilbert-space-of-finite-combinations construction rather than any other known proof of the same fact (e.g. via Riesz representation).
The forward direction (kernel symmetric and positive definite) is immediate once a feature map is given. The converse is not: starting from only the two finite, algebraic conditions, the proof must manufacture a Hilbert space and a feature map out of nothing but and . The book's construction — the space of finite linear combinations , with inner product — requires checking, in order, that this inner product is well-defined independently of how and are represented as such combinations (using the reproducing-type identity ), that it is positive definite as an actual inner product (not just on the Gram-matrix diagonal, i.e. as a function, which uses a Cauchy–Schwarz argument on itself before is known to be an inner product space), and only then completing to an honest Hilbert space. Each of these three steps individually looks routine, but the middle one is circular-looking on a first reading (using an inner-product inequality to prove the pairing is an inner product) and is the step every attempted shortcut skips.
is an arbitrary non-empty type (Nonempty X), matching Definition 4.1's own standing
hypothesis; no additional topological or measurable structure is imposed, since none is used by
either the definitions or Theorem 4.16's proof. IsKernel existentially quantifies over a
Type Hilbert space (NormedAddCommGroup, real InnerProductSpace, CompleteSpace) and a
feature map, matching Definition 4.1 specialized to the real field ; the
complex case of Definition 4.1 is out of scope, since Theorem 4.16 itself is stated only for
real-valued . PositiveDefinite and Symmetric (Definition 4.15) quantify over an arbitrary
finite family via Fin n → X / Fin n → ℝ for n : ℕ, exactly the book's "for all ,
, ".
A trivializing formalization would fix a specific small Hilbert space (e.g. for a
fixed ) in IsKernel's existential rather than an arbitrary one, which would make the
"if" direction of Theorem 4.16 false in general (a positive definite kernel's minimal feature
space can be infinite-dimensional) or silently restrict the theorem's scope; this is ruled out
here by existentially quantifying over an unconstrained Hilbert space type.
IsKernel, Symmetric, and PositiveDefinite are reusable well beyond this mission: every
later kernel construction in the book (polynomial kernels, Lemma 4.6's product kernels, the
reproducing kernel Hilbert space of Section 4.2) is stated in terms of them. Completing the two
milestone proofs and the goal's own sorry (the construction above) is
welcome; a from-scratch formalization of Lemma 4.6 (products of kernels, needing the completed
tensor product of two Hilbert spaces) or of the chapter's other named kernel families would be
natural, faithful extensions of this mission but are out of scope for it.
Support vector machines were, for two decades, the workhorse of applied classification, and the reason offered for their success was always geometric: SVMs maximize the margin between the two classes. Chapter 3's VC-dimension bound cannot explain why this should help — for linear hypotheses in its bound depends on and is uninformative whenever the feature dimension is large relative to the sample size, exactly the regime (kernel-induced or high-dimensional features) where SVMs are most often used. Chapter 5 answers the question this leaves open: a generalization bound for a real-valued hypothesis, stated in terms of its margin on the training sample, that does not depend on the ambient dimension at all. This is also the template every later chapter's margin bound specializes (multi-class classification, ranking, and, indirectly, boosting all reuse the same Rademacher-complexity-of-a-Lipschitz-loss argument developed here).
A hypothesis here is a real-valued function , not (as in Chapters 2-3) a function into : for a labeled point with , the sign of gives the prediction and is read as the classifier's confidence. The confidence margin of at is ; it is positive exactly when classifies correctly. For , the -margin loss (Definition 5.5) is
equal to when (misclassified), when (classified with confidence at
least ), and interpolating linearly in between; it is -Lipschitz. The
empirical margin loss on a sample with labels
(Definition 5.6) is — the
fraction of training points misclassified or classified with confidence below , a
strictly stronger requirement than plain misclassification. The (population) generalization
error is . Rademacher complexity, and
(Definitions 3.1-3.2, restated here since chunk 03-rademacher-vc's own copies are
still drafts), measure how well a real-valued hypothesis class correlates with random sign
noise on a sample, and are the vehicle through which the margin bound's complexity term is
expressed.
Lemma 5.7 (Talagrand's lemma, milestone). For -Lipschitz and any hypothesis set of real-valued functions,
Theorem 5.10 (Rademacher complexity of bounded-norm linear hypotheses, milestone). For and ,
Corollary 5.11 (margin bound for linear hypotheses, milestone). For the same and , fixing , with probability at least ,
Theorem 5.8 — the mission's goal. For any set of real-valued functions and , with probability at least , both
hold simultaneously for all .
Theorem 5.8 is genuinely dimension-free: unlike Chapter 3's VC-dimension bound (5.36 in the
book, restated from Corollary 3.19), it holds regardless of the ambient feature dimension ,
depending instead only on the hypothesis class's Rademacher complexity and the chosen margin
. Specialized to bounded-norm linear hypotheses (Corollary 5.11), this gives the
theoretical justification most often cited for SVMs and every other margin-maximization
algorithm: whenever the training data admits a large geometric margin, the empirical margin
loss at that margin is small (often zero, in the separable case) and the bound is tight
regardless of . Every later chapter's own margin bound (multi-class in Chapter 9, ranking in
Chapter 10) is a direct structural descendant of Theorem 5.8's proof technique. No prior art on
the Prove2Me platform is faithful: GET /theorems?q=support+vector+machine and q=margin+bound
return no hits on this book's model (the two q=margin+bound hits found, both from the Aether
Catalog, state a different comparison — a VC-type bound is eventually worse than a fixed
Rademacher-type bound as a function of dimension — not Theorem 5.8 itself); q=Talagrand and
q=contraction+principle return several hits (Ledoux/Talagrand convex-distance concentration,
Rudin's Banach-space contraction-mapping theorem, a generic Rademacher-sign contraction lemma
for quadratic sums) but every one states either a different mathematical object (metric-space
fixed points, Talagrand's concentration inequality on product spaces) or a different idiom
(squared vs. linear coordinate sums) from Lemma 5.7's function-composition contraction — none
reused. All nine items are drafted fresh.
Not formalized here: Theorem 5.4 (the SVM sparsity/leave-one-out bound). It is listed as a
candidate milestone in BRIEF.md, but its statement and proof depend on the primal/dual SVM
optimization problem itself (the Lagrangian, KKT conditions, and the resulting definition of a
"support vector" as a training point with nonzero dual coefficient) — a materially different,
non-margin-based proof technique (leave-one-out stability of the trained hypothesis, via Lemma
5.3) that shares no definitions with the margin-bound family this mission's goal and other
milestones are built on. Formalizing it faithfully would require standing up the SVM primal/dual
formalism (Lagrangian, complementary slackness, the "support vector" predicate itself) from
scratch, which is disproportionate to a single additional milestone within this mission's
budget; per the captain brief's guidance to leave out, rather than approximate, a statement that
cannot be made faithful in the time available, it is omitted.
The proof of Theorem 5.8 needs the empirical margin loss's zero-one-loss upper bound () applied before invoking Theorem 3.3's Rademacher generalization bound on the composed class , — reversing this order (bounding by a Rademacher complexity computed on the zero-one loss directly) does not work, because the zero-one loss is not Lipschitz. Talagrand's lemma is exactly what lets the -Lipschitz surrogate be pulled outside the Rademacher complexity, at the cost of a factor and no worse; its own proof is an induction removing one Rademacher variable at a time, using a two-point supremum argument (fixing , choosing near-optimal ) that does not simplify to anything less than genuine care with suprema of non-smooth objects — a formalization attempting to replace this with a naive linearity-of-expectation argument would be proving a false or vacuous statement, since does not commute with linear combinations. Theorem 5.10's bound needs the Cauchy-Schwarz and Jensen inequalities used in the particular order the book uses them (Cauchy-Schwarz on the empirical sup, then Jensen on the expectation of a norm, then the independence of the s) — the bound does not follow from either inequality alone.
EmpiricalRademacherComplexity/RademacherComplexity are restated locally in SVM,
byte-identical to chunk 03-rademacher-vc's own copies (a draft item cannot import another
chunk's draft module); this duplication collapses once 03-rademacher-vc is uploaded and listed
in missions/README.md's "Published definitions" table. MarginGeneralizationError is a new,
real-valued-hypothesis specialization of Definition 2.1 (R(h) = P[y h(x) ≤ 0]), distinct from
every earlier chunk's {-1,+1}-valued GeneralizationError, since no earlier chunk's own copy
matches this chapter's real-valued convention. PhiRho/EmpiricalMarginLoss are new. The goal
theorem (margin_bound_binary_classification) states H's own Rademacher complexity computed
on the marginal X-distribution (D.map Prod.fst), matching the book's final displayed form —
the proof's intermediate step (the lifted class having the
same Rademacher complexity as itself, since ) is not separately drafted, only
the theorem's statement. Theorem 5.10/Corollary 5.11 generalize the book's ambient
to an arbitrary real inner-product space X ([NormedAddCommGroup X] [InnerProductSpace ℝ X]), a harmless generalization since the book's proof (Cauchy-Schwarz,
Jensen, orthogonality of Rademacher signs) uses only the inner-product structure, never finite
dimension; [BorelSpace X] is added to Corollary 5.11's statement to make the measurable
structure under which MarginGeneralizationError is well-posed explicit, since every
x ↦ ⟨w, x⟩ is automatically Borel-measurable — not a substantive restriction, the book never
discusses measurability of linear functionals. No numerical constant in any of the four
theorems is altered from the book's own displayed form. A trivializing formalization this
mission avoids: stating Theorem 5.8 only for a Finset/finite H (which would make it a
disguised instance of Chapter 2's finite-hypothesis bound rather than the chapter's genuinely
new, complexity-based argument) — H : Set (X → ℝ) is left fully general, exactly as the book
states it.
Chapter 2 of Steinwart & Christmann, Support Vector Machines, showed the hinge loss controls the classification loss (Zhang's inequality, Theorem 2.31). That result was special to one target/surrogate pair. Chapter 3 asks the question in general: given any target loss (the loss whose risk we actually care about) and any surrogate loss (the loss a learning algorithm actually minimizes, chosen for tractability — convexity, differentiability), when does controlling the excess -risk control the excess -risk? The book's answer factors the question through a purely pointwise object, the calibration function, that depends only on the two losses and a single label distribution — not on the learning problem's ambient space or the unknown data-generating distribution at all.
Fix a measurable space and a closed label set . For a loss , a distribution on , and , the inner -risk is and the minimal inner risk is (Definition 3.3). Eq. (3.5) rewrites the ordinary -risk of against a full distribution on as : the outer risk is an average of inner risks over the -marginal, one inner risk per conditional distribution . The set of -approximate minimizers is (Definition 3.5).
The calibration function of a pair (Definition 3.13) is the largest such that every -approximate surrogate minimizer is already an -approximate target minimizer: when , and otherwise. is -calibrated with respect to a set of label distributions if for every , , — one working uniformly over the whole class , not just a single fixed distribution.
when is bounded. This is the mission's capstone: a purely pointwise, -independent condition (calibration) is shown equivalent to a whole-class-of-distributions statistical guarantee, not merely necessary for it.
Theorem 3.22 (BRIEF.md's originally recommended goal — the fully quantitative uniform
calibration inequality, using a Fenchel-Legendre biconjugate) was not attempted; see
STATUS.md for the reason and the fallback taken instead.
Corollary 3.19 is the chapter's answer to "is calibration actually useful, or just necessary?" Theorem 3.17 alone only rules out non-calibrated surrogates; Corollary 3.19 shows that for the two most important bounded target losses in the book — the classification loss and the density-level- detection loss — calibration is exactly the right test, with no gap between necessity and sufficiency. Concretely: the book's Example 3.16 computes that both the least-squares and hinge losses are calibrated surrogates for the classification loss for every , and this corollary is what turns that pointwise computation into the qualitative consistency guarantee "minimizing empirical hinge risk is a statistically sound way to approach the empirical classification risk," ahead of the sharper quantitative form Zhang's inequality already supplies for that one pair (Theorem 2.31) and Theorem 3.22 supplies in general.
The apparatus itself — inner risks, approximate-minimizer sets, the calibration function — is the
chapter's real content, and getting the finite/infinite distinction right throughout is the
chapter's central technical difficulty: Lemma 3.11's whole point is that " for a.e. " is a genuine dichotomy, not a standing assumption, and the calibration
function's own definition branches on exactly this finiteness. A real-valued, junk-at-infinity
convention for risks (as used in the 01-loss-functions mission, where losses were always
bounded) would silently collapse this dichotomy and trivialize Lemma 3.11 and much of Theorem
3.17's content. The definitions in this mission are built in ENNReal (Lean's )
throughout specifically to avoid this trap.
is an arbitrary measurable space; label distributions range over Measure ℝ with no
IsProbabilityMeasure requirement in InnerRisks/CalibrationFunction/Lemma 3.14 — re-reading
Lemma 3.14's proof directly (p. 59) found no step that uses having total mass , so this
hypothesis is dropped as a disclosed generalization there, matching the convention this series
already used for Lemma 2.23's convexity hypothesis. Wherever a genuine distribution on
is required (Lemma 3.4, Lemma 3.11, Theorem 3.17, Corollary 3.19), is represented
as a pair — an -marginal and a measurable family of conditional distributions — with ∀ x, IsProbabilityMeasure (κ x) added explicitly at each such use site, since the (PX, κ)
representation does not force this by its types alone. X being a complete measurable space
(required by all four theorem-kind items but Lemma 3.14) is rendered as the disclosed sufficient
condition " a probability measure for which -null sets have every subset
measurable" rather than the book's exact universal-completion equality — see
Def_..._IsCompleteMeasurableSpace's own note. ranges over ENNReal throughout, so
""/"" need no narrowing, unlike this series' real-valued
conventions elsewhere.
A trivializing formalization here would let IsCalibrated/the calibration function be an
unconstrained hypothesis disconnected from innerRisk/approxMinimizers, or let κ/PX range
freely with no link to outerRisk/bayesRisk as actually defined — both are ruled out since
every item's statement is built compositionally from the same innerRisk/minInnerRisk/
approxMinimizers/outerRisk/bayesRisk definitions, traced back to Definitions 3.3, 3.5, 2.2
and 2.3 exactly as the book states them.
Loss, innerRisk/minInnerRisk/approxMinimizers, outerRisk/bayesRisk/IsOfType, and
calibrationFunction/IsCalibrated are reusable beyond this mission: this series' 06- classification chunk restates this chapter's apparatus locally (per Hard Rule 9, drafts cannot
import each other) when it reuses Chapter 3's calibration ideas for its own oracle inequality.
Contributions completing the five sorrys are welcome; Theorem 3.22 itself (the fully
quantitative version this mission's BRIEF.md recommended as the primary goal) remains a natural
follow-up mission built on top of this one's definitions.
Many statistical estimators are defined by minimizing an empirical average over a class of candidate models — empirical risk minimization, maximum likelihood, and binary classification all fit this template. Analyzing such an estimator's excess risk reduces, in each case, to controlling how far the empirical average of a whole class of functions can deviate from its population expectation, not just a single fixed function — a much stronger requirement than the ordinary law of large numbers, which only controls one function at a time. This mission formalizes the central non-asymptotic tool for this problem, the Rademacher complexity-based uniform law, following Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 4.
Let be a class of real-valued functions with a common domain, indexed as , and let be i.i.d. samples from a distribution . The empirical process deviation (Eq. (4.7)) is
Given an independent Rademacher sequence (each equiprobably), the symmetrized process (Eq. (4.19)) and the Rademacher complexity (Eq. (4.13)) of are
A class is -uniformly bounded if for every .
For any -uniformly bounded class , any , and any ,
with -probability at least .
For any convex non-decreasing , , where is the recentered class. This generalizes the specific symmetrization step used in Theorem 4.10's own proof (the case ) to an entire family of moment comparisons.
For a -uniformly bounded, i.i.d.-sampled class , with -probability at least , obtained via the bounded-differences method. Combined with Proposition 4.11's bound on by , this is exactly Theorem 4.10's proof.
Theorem 4.10 is the general-purpose engine behind the classical Glivenko–Cantelli theorem (recovered by taking to be the class of half-line indicator functions, Example 4.6) and behind uniform convergence guarantees for empirical risk minimization more broadly (Section 4.1.2): whenever a task can be reduced to bounding the Rademacher complexity of a specific function class — a purely combinatorial/geometric quantity independent of any particular statistical model — Theorem 4.10 converts that bound directly into a high-probability uniform convergence guarantee. Proposition 4.11 is separately significant as the general symmetrization principle from which Theorem 4.10's specific bound, and many similar bounds throughout empirical process theory, are instances.
Formalizing it. No faithful prior art exists on the platform: a fresh search for "uniform
law," "symmetrization," "Rademacher complexity," "Glivenko-Cantelli," and "empirical process"
found only unrelated hits and the existing RademacherSymmetrization.*/RademacherMassart.*
items, which are specific to finite function classes (Finset (X → ℝ)) — a strictly narrower
setting than Theorem 4.10's fully general (possibly infinite) function classes, and not reused
here. All three theorems are drafted as open goals (:= by sorry).
The naive approach to bounding — apply a scalar concentration bound to each individually and union-bound over — fails outright when is infinite (there is no union bound to take). The two-step resolution captured by this mission's milestones avoids this entirely: first, itself, viewed as a single function of the samples, is shown to concentrate sharply around its own mean via the bounded-differences method (no union bound over needed — the argument treats as one Lipschitz function of the samples). Second, the mean itself, a single deterministic number, is bounded via symmetrization: introducing an independent "ghost sample" with the same law as converts the un-symmetric quantity into the manifestly symmetric , and it is only after this symmetrization that the supremum over becomes tractable via the geometry of (its Rademacher complexity) rather than requiring finite.
The function class is realized as the range of an index family
rather than a Set (D → ℝ), matching the standard representation of a (possibly infinite)
function class by an index type; ι carries no finiteness assumption, matching the book's own
full generality (in contrast to the platform's existing RademacherSymmetrization/
RademacherMassart items, which are finite-class-specific). The population expectation
is realized via an explicit population variable sharing the samples'
common law, rather than a separately axiomatized abstract distribution object. The Rademacher
sequence and the samples are packaged into one jointly independent family Z : ℕ → Ω → D × ℝ
with an explicit hypothesis that the two coordinates are themselves independent at each index —
capturing " independent of , both i.i.d." exactly, without a bespoke
joint-independence predicate.
Theorem 4.10's own qualitative corollary ("consequently,
whenever ") is not included in the goal's conclusion: it concerns an infinite
sequence of samples and asymptotic convergence via the Borel–Cantelli lemma, a substantially
different formal object (requiring Filter.Tendsto over ℕ→∞ and ∀ᵐ almost-sure convergence)
from the single- non-asymptotic tail bound (4.14) this mission's goal states, and is left as
natural follow-on work, alongside a direct formalization of the classical Glivenko–Cantelli
theorem (Theorem 4.4) as a corollary.
Lemma 4.14 (the polynomial-discrimination route to bounding Rademacher complexity for VC-type classes) is out of scope for this mission: its displayed inequality is extracted with heavily garbled math layout from the source PDF (a known, disclosed limitation of this book's text extraction at that specific page), and confirming it character-for-character against the rendered page image was judged out of budget for this chunk relative to Proposition 4.11 and Eq. (4.16), both of which are directly load-bearing in Theorem 4.10's own proof and extracted cleanly.
Sums of independent random variables are well understood: Bernstein's inequality and its relatives give sharp, non-asymptotic tail bounds for whenever the are independent and light-tailed. Many quantities that arise in high-dimensional statistics and random matrix theory, however, are not linear but quadratic in an independent sample — the squared norm of a random vector after a linear transformation, a quadratic-form test statistic, the diagonal of a sample covariance matrix, or the number of edges cut by a random partition in a random graph. A quadratic form is a sum with dependent terms: and share the factor , so classical sum-of-independent-variables tools do not apply directly.
The Hanson-Wright inequality, first obtained by Hanson and Wright (1971) for sub-gaussian variables and later sharpened and popularized in this form by Rudelson and Vershynin (2013, "Hanson-Wright inequality and sub-gaussian concentration," Electronic Communications in Probability), closes this gap: it gives a concentration inequality for around its mean with the same two-regime (sub-gaussian near the center, sub-exponential in the tail) shape as Bernstein's inequality for linear sums. It is now a standard tool wherever quadratic statistics of independent data are analyzed: covariance estimation, compressed sensing, randomized numerical linear algebra, and the analysis of random matrices more broadly draw on it routinely.
Fix a probability space and let be a random vector whose coordinates are independent, mean zero, and sub-gaussian: each has a finite sub-gaussian (Orlicz ) norm , the smallest with . Write .
Let be an real matrix, with no constraint on its diagonal, and form the quadratic form
Two matrix norms measure the size of : the Frobenius norm (the Euclidean norm of 's entries) and the operator (spectral) norm (the largest singular value of ). Always , so the two norms can differ by a factor as large as — the gap between them is exactly what produces the inequality's two regimes below.
where is an absolute constant, not depending on , , , or . Stating the constant only as "some absolute " (rather than pinning it to a numeral) is deliberate: the book's own proof does not track a sharp value, and a goal that only asserts the shape of the bound survives any later improvement to .
The result itself. Hanson-Wright turns a two-dimensional (in ) dependency structure into a one-dimensional concentration statement controlled by two scalar quantities, and . This is what makes it usable: a practitioner bounding a quadratic statistic need only compute these two norms, not analyze the joint dependency structure of directly. It specializes to Bernstein's inequality (Chapter 2 of this book) when is diagonal, and it underlies non-asymptotic guarantees for covariance estimation, the Johnson-Lindenstrauss lemma via a different route, and the concentration of Lipschitz functions of sub-gaussian vectors.
Formalizing it. The published proof of Hanson-Wright is not a single argument but a chain of four steps: a decoupling reduction (Section 6.1), a direct computation for Gaussian chaos (Lemma 6.2.2), a comparison lemma extending the Gaussian bound to general sub-gaussian vectors via a replacement trick (Lemma 6.2.3), and a final assembly that separates the diagonal part (handled by Bernstein's inequality) from the off-diagonal part (handled by decoupling and comparison). This mission formalizes the goal theorem's statement and the first, most reusable link in that chain — the decoupling machinery of Section 6.1, which reduces the analysis of the dependent chaos to the independent-once-conditioned bilinear form — together with the chapter's separate contraction principle (Section 6.7), a general comparison tool for Rademacher-weighted sums used repeatedly in the book's later chaining chapters. The Gaussian MGF computation and the replacement-trick comparison lemma (Lemmas 6.2.2–6.2.3) are left as future milestones on top of this mission: they require Gaussian rotation invariance and the singular value decomposition of , substantially more machinery than the milestones included here.
The obvious first idea — treat as if it were a sum of independent terms and apply Bernstein's inequality termwise — fails immediately: the terms for fixed are not independent across , since they all share the factor . Decoupling (Theorem 6.1.1) is the non-obvious fix: it replaces the off-diagonal chaos by a bilinear form in an independent copy , which genuinely does become a sum of independent terms once one of the two vectors is conditioned on. The price is a universal constant factor of and the restriction to diagonal-free matrices, which is exactly why the full Hanson-Wright proof must separate the diagonal contribution to (handled directly by Bernstein's inequality, Chapter 2) before decoupling can be applied to what remains.
Random variables and vectors are real-valued on an explicit probability space . The sub-gaussian norm is HighDimProb.Concentration.subgaussianNorm, the
Orlicz--norm definition already published for this series (01-concentration), reused
here as a reference item rather than redefined. is written as a
finite supremum over the coordinate index, ⨆ i, subgaussianNorm P (X i); because the index
type is always a Fintype (Fin n), this supremum is well-defined and, at the degenerate index
, reduces to a true (if content-free) instance of the inequality rather than a vacuous or
false one. The Frobenius and operator norms of are this mission's own frobeniusNorm and
opNorm, stated directly from their defining formulas rather than through Mathlib's scoped
matrix-norm typeclass instances, which are deliberately not global defaults (to avoid a diamond
between the two norms) and so are unsuitable for a statement that needs both simultaneously.
Every place the goal or a milestone integrates a quantity, that quantity is required
Integrable, guarding against Mathlib's convention of returning 0 for the Bochner integral of
a non-integrable function — without these hypotheses, a mean-zero or expectation hypothesis
could hold vacuously, or a conclusion could hold trivially, for reasons having nothing to do
with the book's mathematics.
The formalization deliberately does not restrict 's diagonal in the goal theorem: doing so would collapse Hanson-Wright to a restatement of Bernstein's inequality for the special case of a diagonal matrix, discarding the chapter's actual content, which is handling the off-diagonal, genuinely quadratic dependence between coordinates. The diagonal-free restriction does appear, correctly, in the Decoupling theorem (6.1.1), whose proof needs it.
Reusable beyond this mission: frobeniusNorm and opNorm are needed by any future chapter
using matrix norms (Chapter 4's random matrix norms, Chapter 9's matrix deviation inequality);
the decoupling theorem and convex decoupling lemma are the standard entry point for any later
formalization of chaos concentration; the contraction principle is reused throughout the book's
chaining chapters (7 and 8). Welcome contributions include the Gaussian MGF and comparison
lemmas (6.2.2–6.2.3) needed to complete a full proof of the goal theorem, and the two-sided
version of Bernstein's inequality needed for the diagonal part of that proof.
Chapters 2 and 3 bound the estimation error of a hypothesis chosen from a fixed hypothesis set , but the choice of itself is left open: a richer lowers the approximation error (how close comes to the Bayes classifier) at the price of a looser generalization bound, and a poorer does the reverse. Chapter 4 is the book's answer to this trade-off. It first shows that Empirical Risk Minimization (ERM) alone cannot resolve it — ERM ignores the complexity of entirely — and then develops Structural Risk Minimization (SRM): decompose a rich hypothesis set into a nested countable union of increasingly complex pieces, and let the learning algorithm balance empirical fit against a complexity penalty for each automatically. The chapter closes by showing how the same balance can be achieved computationally through convex surrogate losses, whose minimization is tractable where minimizing the zero-one loss directly is not.
For a hypothesis chosen from , the excess error decomposes into an estimation
term and an approximation term (Eq. 4.1).
Proposition 4.1 bounds ERM's estimation error by twice the uniform deviation
. For a nested family and ,
denotes the least index with ; SRM selects by minimizing
jointly over and , where
is 's Rademacher complexity (Definitions 3.1/3.2, restated locally in this
chunk's ModelSelection namespace). Theorem 4.2 is the resulting learning guarantee. Section
4.4 develops a competing model-selection procedure, cross-validation, and Theorem 4.4 directly
compares its guarantee to SRM's on a held-out split of the sample. Section 4.7 turns to
real-valued scoring functions with sign convention
and a convex non-decreasing surrogate of the zero-one loss; the Bayes scoring function
(Eq. 4.9) and the -loss (Eq. 4.10) let Theorem 4.7
bound the true excess error by a power of the surrogate's own excess loss.
Proposition 4.1 (ERM bound, milestone). For any sample , .
Theorem 4.2 — the mission's goal. For a nested countable union and minimizing over the whole union, for any , with probability at least :
Theorem 4.4 (Cross-validation versus SRM, milestone). Splitting a sample of size into (size , training) and (size , validation), for any , with probability at least :
Theorem 4.7 (Convex-surrogate excess-error bound, milestone). For convex and non-decreasing with satisfying for all : .
Theorem 4.2 is the chapter's headline result and the theoretical justification for
regularization-based learning: it shows that a single algorithm, without knowing in advance
which contains a good hypothesis, achieves a guarantee that is — up to the
penalty — as favorable as if an oracle had revealed the best-in-class
index in advance (Eq. 4.6). It is also the chapter's genuine new content beyond chunk
03-rademacher-vc's single-hypothesis-set bound: the countable union bound (a 1/k²-weighted
union over converging to , hence the appearing in place of )
is not a restatement of Theorem 3.3 but a distinct argument, and the goal's inf over the
whole nested family is what makes SRM a model-selection method rather than a bound for one
fixed . Theorem 4.4 is the chapter's only head-to-head comparison between two competing
model-selection procedures, on two genuinely different samples. Theorem 4.7 is the bridge
between the learning-theoretic guarantees of chapters 2-4 and the actually-implemented convex
optimization problems of chapters 5 (SVM), 6 (kernels) and beyond, all of which minimize a
convex surrogate rather than the zero-one loss directly. No prior art exists on the platform:
GET /theorems?q=structural%20risk%20minimization and GET /theorems?q=model%20selection both
return zero hits.
Theorem 4.2's proof genuinely uses the union bound over a countably infinite family indexed
by with weight converging to (Eq. 4.5) — this is the chapter's
distinct new technique, not an application of chunk 03's finite/VC-dimension machinery to a
single ; a formalization that stated the bound only for one fixed , or dropped the
inf over the whole union in favor of a single best-in-class , would be Theorem 4.2's
named trivializing formalization (BRIEF.md's pitfall note) rather than the theorem itself.
Theorem 4.4 requires keeping two distinct samples (, , of different, precisely
related sizes) and two distinct hypotheses (, ) apart throughout;
conflating them collapses the comparison to a tautology. Theorem 4.7's difficulty is in its
setup, not its statement: the Bayes scoring function, the -loss, and the pointwise
-minimizer (which the book allows to take the extended values at
the degenerate points ) all need care to state without silently altering
the theorem's content.
GeneralizationError, EmpiricalError, EmpiricalRademacherComplexity and
RademacherComplexity are restated locally in this chunk's ModelSelection namespace
(identical in content to chunk 03-rademacher-vc's own copies), since a draft item cannot
import another chunk's draft module. LeastIndex H h (k(h)) is Nat.sInf {k | 1 ≤ k ∧ h ∈ H k}; every theorem using it carries the standing hypothesis that h lies in the relevant union,
guarding against trap 5 (Nat.sInf of an empty set). Theorem 4.2's hSRM and Proposition 4.1's
hERM are hypothesis-supplied functions satisfying the book's optimality property, not
constructed via choice over an unconstrained H; H.Nonempty (Proposition 4.1) and
(⋃ k ≥ 1, Hk k).Nonempty (Theorem 4.2) guard the outer sInf/inf terms against trap 5.
Theorem 4.7's is formalized as a real-valued function satisfying the pointwise
minimization property for all ; the book's own extended-real convention
( exactly where ) is outside this formalization —
disclosed here and in MODERATION_NOTES.md — since no real number satisfies the minimizing
property at those degenerate points, the theorem as stated applies precisely to the case a
real-valued can be supplied, which is the book's own generic case. No numerical
constant is altered from the book in any of the four theorems: 2 and log(3/δ) in Theorem
4.2, 2 (twice) and log(4/δ) in Theorem 4.4, and 2c and the exponent 1/s in Theorem 4.7
are exactly as displayed.
Not formalized: the discussion of computing via binary search (a computational, not a statistical, result); -fold and leave-one-out cross-validation (Section 4.5, a practical variant of Theorem 4.4's two-sample cross-validation without its own numbered generalization bound); regularization-based algorithms (Section 4.6, the uncountable-union extension of SRM, which the book itself only sketches without a numbered theorem); Lemma 4.5 and Proposition 4.6 (intermediate results establishing that induces the same classifier as , needed for Theorem 4.7's proof but not part of its statement); and the worked examples for the hinge, exponential and logistic losses (instantiations of Theorem 4.7's , not separate theorems). Drafting only these worked instantiations in place of Theorem 4.7's general statement would be a trivializing formalization for this chapter.