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 decision-maker has projects, each a Markov reward process, and at every decision time may advance exactly one of them; the others stay frozen. Which project to advance so as to maximize the expected total discounted reward? Posed as a dynamic program the problem has a state space that is the product of the state spaces, and the size of that product defeats every general method. The index theorem of Gittins and Jones (1974) says the dynamic program is solved exactly by an index policy: there is a real number , computable for each bandit process from its own data and its own current state , such that always advancing a process of greatest index is optimal. Chapter 2 of Gittins, Glazebrook and Weber, Multi-armed Bandit Allocation Indices (2nd ed., doi:10.1002/9780470980033), introduces the index, proves the theorem three times, and works out the properties of the index that the rest of the book, from jobs and superprocesses to restless bandits, is built on: which stopping time attains it, how it is computed, how it moves with the discount factor, and when it collapses to the myopic rule.
The index theorem itself is already on the platform, proved, as BanditAlgorithm.gittins_index_theorem in the Bandit Algorithms series (Lattimore and Szepesvári, Theorem 35.9). This mission cites it and formalizes what Chapter 2 establishes around it.
A bandit process (§2.3–2.4) is a Markov reward process on a countable state space : transition probabilities , a bounded reward received each time the continuation control is applied in state , and a discount factor ; the freeze control leaves the state unchanged and yields nothing. The law of the process started at is and is its state at process time . A stopping time is a past-measurable rule for switching from continuation to freezing, taking values in . For such , is the expected discounted reward and the expected discounted time; their ratio (2.7) is the equivalent constant reward rate of that portion of . The Gittins index is
and, equivalently, the fair charge (2.5): the greatest rent per period for which continuing for one or more periods, paying each period, can be done without expected loss. A simple family of alternative bandit processes (SFABP) is such processes with a common discount factor, one of which is continued at each decision time; an index policy continues a process of greatest index. In the Lean development the single-arm model is the platform's (GittinsIndex): the chain law is built by the Ionescu–Tulcea construction, stopping times are adapted -valued maps on trajectories, and gittinsIndex P r a x is (2.6).
The supremum in (2.6) is attained. For the initial state , the attaining stopping rule may be taken to be "stop at the first time at which the state lies in " for any set with
and every such rule has .
Theorem 2.1 as a reference to the proved platform theorem; Eq. (2.5), the fair-charge characterization of the index; the restart-in-state formulation of §2.6.4 as the convergence of the Katehakis–Veinott value iteration; Theorem 2.3, monotonicity in the discount factor; Lemma 2.4, the interchange of two bandit portions; Propositions 2.5–2.8, the monotone-index cases in which the index is the immediate reward, or is attained only after the first step, or only at .
Lemma 2.2 is the working form of the index: it turns the supremum over all stopping times into a specific rule, the first time the index falls below its starting value, and it is what the interchange proof of §2.7, the modified-forwards-induction policies of §2.6.6, the monotone-index propositions of §2.11 and the treatment of jobs in Chapter 3 all use. The fair-charge form (2.5) is the prevailing-charge proof of the theorem (Weber 1992) and the interpretation that carries over to superprocesses and restless bandits. The restart formulation is how indices are computed in practice (Katehakis and Veinott 1987), and Theorem 2.3 is the first of the comparative statics used throughout Chapters 7 and 8. Lemma 2.4 is the elementary inequality behind the original proof of Gittins and Jones.
Of these, only the index theorem has a machine-checked proof today. Formalizing the rest gives the platform the index as a usable object: a characterization of the optimal stopping rule, a convergent algorithm for it, and the monotonicity facts, all stated against the existing model so that every later mission of this series and every future use of the L&S model can build on them.
The obvious first move for Lemma 2.2, "take the stopping time that achieves the supremum", is what has to be proved: the supremum is over an uncountable family, and attainment comes from the optimal stopping problem with charge , whose value function satisfies , together with the fact that its optimal stopping set is characterized by the strict and non-strict inequalities and . That last step is the content: it identifies the local decision "stop or continue" with a comparison of indices, which is why any set between the two level sets works. On the platform's model this requires the dynamic-programming theory of discounted optimal stopping on a countable space (Theorem 2.10 of the book), the identification of fairChargeProfit with that value function, and the strong Markov property of markovChainMeasure at a trajectory stopping time. Theorem 2.3 needs randomized stopping times (a geometric kill) and the fact that they do not enlarge the supremum. The restart iteration is monotone and bounded but its operator is not a contraction in the restart value, so its limit has to be identified with the restart problem's value directly; that value is , not , because restarting forever is free.
The state space is a countable type with measurable singletons, so every subset is measurable; rewards are bounded; . The chain law, stopping times, the discounted stopped sums and the index are the platform's, unchanged. Expectations are Bochner integrals; with bounded rewards they are finite and no total-function default value enters. IsPositiveStoppingTime fixes everywhere, so and the ratio (2.7) is a genuine quotient. The stopping rule of Lemma 2.2 is the hitting time from time of a set, with when the set is never hit. The fair-charge profit is a real supremum over the nonempty bounded family of positive stopping times, and (2.5) is stated with the outer supremum over , a nonempty set bounded above. The restart iteration is stated as a limit, with the value : for a nonnegative index this is the book's , and the maximum is forced by a one-state example with negative reward. The propositions' hypotheses are almost-sure events under , written as events of measure one.
Two trivializing readings are excluded: the index is never taken over all -valued maps but over adapted stopping times, and the stopping set of the goal is not restricted to the two extreme level sets. Contributions welcome: the optimal-stopping dynamic program on markovChainMeasure (value iteration, the strong Markov property at a stopping time), the equivalence of randomized and non-randomized stopping times for the supremum, and the monotone convergence of the restart iteration.
An airline sells one flight, a hotel one night, a car-rental firm one day of one car: a fixed capacity, perishable at a deadline, sold to customers who arrive over time and are willing to pay different amounts. Chapter 2 of Talluri and van Ryzin's The Theory and Practice of Revenue Management (2004) is the theory of that single resource. Its three models answer the same question with increasing generality: Littlewood's two-class rule, the -class static model and its dynamic-arrival version give the seller a protection level per class, a booking limit or a bid price, all three equivalent; the discrete-choice model, in which customers buy down when a cheaper fare is open, replaces classes by offer sets and shows that only the efficient sets, ordered by their purchase probability, are ever offered, with a higher set the more capacity or the less time remains. This mission formalizes that last result, Theorem 2.3, together with the structural results of the two earlier models that it generalizes.
Static model. Classes with prices arrive in
stages, lowest class first, with demands distributed on . With units left at
stage the seller observes and accepts units; the value function
is the Bellman equation (2.3), ,
(staticValue), and is the marginal value of capacity. The
protection level (protLevel), the booking limit
(bookLimit) and the bid price
(bidPrice) define the three controls of Theorem 2.1.
Dynamic model. Over periods at most one request arrives per period, of class with
probability ; the value function (2.17) is
(dynValue), with time-dependent protection levels (2.19), booking limits (2.20) and bid
prices (2.18).
Choice model. When the set of classes is open an arriving customer buys class
with probability ; is the purchase probability and
the expected revenue (purchaseProb, expRevenue). The value
function (2.26) is
(choiceValue). A set is inefficient (Definition 2.1, IsInefficient) if a
randomization over the subsets has and
, and efficient otherwise.
In every period with capacity left, some efficient set maximizes (2.26); and, the efficient
sets being ordered by , the largest optimal set is nondecreasing in the remaining capacity
and nondecreasing in the period : choice_optimal_policy. Monotonicity is stated as
"every efficient optimal set at is matched by one at , , with at
least as large a purchase probability", and likewise in .
Littlewood's rule (2.1), and the acceptance criterion; Proposition 2.1, the marginal values of the static model are decreasing in and increasing in the stages remaining; Theorem 2.1, nested protection levels, nested booking limits and bid-price tables each attain the Bellman maximum at every stage; Proposition 2.2 and Theorem 2.2, the same two results for the dynamic model, with marginal values now decreasing in time; Proposition 2-2.A.4 of the appendix, the marginal values of the choice model are decreasing in and in ; Proposition 2.3, an inefficient set is never optimal; and the ordering of efficient sets, implies when is efficient.
The continuous-demand optimality conditions (2.9) of Sect. 2.2.2.3, stated without proof, the computational and heuristic methods of Sects. 2.2.3-2.2.4, the overbooking models of Sect. 2.7 and the nested-policy characterization of Sect. 2.6.2.5 are not targets.
Theorem 2.3 is the structural result behind choice-based revenue management: it reduces the offer sets to the efficient frontier of , orders that frontier, and shows the optimal policy walks up it as capacity grows or the deadline nears. It was the analytical core of Talluri and van Ryzin's (2004) choice-model paper and is the reason the efficient sets, not the fare classes, are the unit of control when customers substitute between fares. The static and dynamic results, from Littlewood (1972) and Brumelle and McGill (1993) to Lee and Hersh (1993), are the foundation of every airline seat inventory control system; the equivalence of protection levels, booking limits and bid prices is what lets the same optimal policy be implemented on any of the three kinds of reservation system. None of these results has a machine-checked proof.
The two marginal-value propositions are inductions in which the inductive step is the discrete
concavity of a max-plus convolution, Lemma 2-2.A.1 of the appendix: is concave when is, which in Lean requires reasoning about the
argmax on and the truncated subtraction. The static model's expectation is a
tsum against a pmf, so every step also needs summability of a bounded family. The
protection-level theorems then need the down-set structure of
under monotonicity of , and the three controls have to be shown to coincide unit by
unit. For the choice model, Proposition 2.3 is a one-line convexity argument once
is known, and the monotonicity in Theorem 2.3 is a monotone comparative-statics
argument on the objective , which is easy in but must be combined
with Proposition 2-2.A.4 in both and ; the existence of an efficient maximizer uses
Proposition 2.3 and the finiteness of the subsets.
Capacities, stages and periods are natural numbers, the value functions recurse on the stage or
on the number of periods to go, and the book's ranges (, , ) are
hypotheses of the theorems. Demand in the static model is a pmf on rather than a
random variable, so the expectation in (2.3) is a tsum; the dynamic model's expectation over
is written out, including the no-arrival term, which vanishes under nonnegative prices.
The choice model is defined by its compact form (2.26), and the maximization includes the empty
offer set. Optimality of a control means attaining the inner maximum of the Bellman equation at
every state, which is what the book's proofs establish. The bid-price control is formalized with
the bid price of the -th unit allocated; the book prints ,
which is one unit off from (2.5). The appendix's Proposition 2-2.A.4 prints its time
monotonicity in the reverse direction; the formal statement is the direction consistent with
Proposition 2.2 and Theorem 2.3. The ordering of efficient sets is stated with non-strict
inequalities, since Definition 2.1 admits ties in revenue.
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.
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 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.
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.
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.
Binary classification asks for a rule that predicts a label from an observation . The natural loss for this task, the classification loss , is a step function: minimizing its empirical average over a class of functions is generally NP-hard, because the objective is non-convex and discontinuous in . Every practical classification algorithm — logistic regression, boosting, and the support vector machine this book is about — sidesteps this by minimizing a convex surrogate loss instead, such as the hinge loss , and hoping that a small surrogate risk implies a small classification risk.
Zhang (2004) and Bartlett, Jordan & McAuliffe (2006) put this hope on a rigorous footing: for a wide class of convex surrogates, controlling the excess surrogate risk controls the excess classification risk, with an explicit quantitative relationship. Steinwart & Christmann, Support Vector Machines (Springer 2008, Information Science and Statistics), Chapter 2, develop the special case of the hinge loss in closed form as Theorem 2.31 ("Zhang's inequality"), the sharpest and most self-contained instance of this calibration phenomenon: an exact equality for bounded functions, not merely an inequality.
Fix a measurable space and a closed label set ; throughout this mission . A loss function is a measurable map , read as the cost of predicting by when is observed. Given a distribution on , the -risk of a measurable is the average cost , and the Bayes risk is the smallest risk any measurable function can achieve.
The classification loss is — it charges exactly when the sign of the prediction disagrees with the label — where is the sign function with the book's convention . The hinge loss is , a convex, piecewise-linear upper bound on up to a factor of . Writing for the conditional probability of the positive label given , the Bayes classification function is : it predicts the majority label at .
A loss can be clipped at if truncating every prediction to never increases the loss: for the clipped value of . Both and can be clipped at .
The first target is an exact identity for bounded predictors: the excess hinge risk equals a weighted distance to the Bayes classifier. The second, weaker but unrestricted, statement is what makes the hinge loss a valid classification surrogate for arbitrary real-valued scores: no matter how large grows, the excess classification risk it incurs is bounded by its excess hinge risk. Because the second statement is the one actually used downstream (Chapter 6's oracle inequality composes it with a bound on the excess hinge risk to bound the excess classification risk), it is the weakest stable form of the calibration claim and the natural target to keep in mind when judging whether a variant formalization is still faithful.
Zhang's inequality is the single fact that licenses every consistency and rate-of-convergence result for SVM classification in the rest of the book (flagged explicitly on p. 38: "we will show in Section 3.4 that the other margin-based losses ... are also reasonable surrogates," and reused directly, e.g., in Chapter 6's oracle inequality via its restatement as Theorem 6.24 in Chapter 6 of this series). Its role is entirely mechanical but load-bearing: every SVM consistency proof reduces to bounding an excess surrogate risk, and Theorem 2.31 is what converts that bound back into a statement about the classification error anyone actually cares about.
The result itself has been known since Zhang (2004) and Bartlett–Jordan–McAuliffe (2006) in more general form (arbitrary convex margin losses, with an explicit "-transform" relating excess risks); Theorem 2.31 is the closed-form hinge-loss instance, with the equality (not just an inequality) available because the hinge loss's clipped value is exactly linear in . No machine-checked proof of either the general or the hinge-specific statement is known to exist in a public Lean/Mathlib development at the time of writing (see prior-art search below); this mission asks for a formalization of the hinge-specific case exactly as the book states it.
The natural first attempt is to expand both risk differences directly as integrals over and compare integrands. This works for the equality (bounded ), because the hinge loss is piecewise linear in and the calculation collapses to the algebraic identity once is spelled out by cases on the sign of . It fails for the inequality on unbounded : neither risk difference has a closed algebraic form once is allowed to leave , and the excess classification risk itself is genuinely discontinuous in . The book's proof resolves this by clipping first (Lemma 2.23: clipping a convex loss at a minimizer's interval only decreases its risk) and observing the excess classification risk is invariant under clipping — this reduces the general case to the bounded case, at the cost of needing Lemma 2.23 as a genuine prerequisite rather than a routine remark. The remaining pointwise step (Lemma 2.30) is a case-by-case real-variable inequality with no probabilistic content of its own, but gets the boundary case (equivalently , where the book's sign convention is load-bearing) wrong if that convention is not tracked precisely.
is an arbitrary measurable space; is fixed to throughout. A
loss is represented as a plain function Loss X := X → ℝ → ℝ → ℝ; nonnegativity and the
restriction of the middle argument to are supplied as explicit hypotheses at each use
site rather than built into the type, since only some lemmas of the chapter need them (Lemma 2.23
needs neither). risk/bayesRisk are ordinary real-valued Bochner integrals/infima, not
extended-real-valued as in the book; consequently every assertion that could otherwise degrade to
a vacuous 0 - 0 from a non-integrable loss carries an explicit Integrable hypothesis on the
relevant loss composed with — automatic in the book's own setting (bounded losses on a
probability space) but not implied by the Lean types alone. is
represented by its defining disintegration identity,
for every measurable , rather
than via a general regular-conditional-probability construction — a specific, checkable
representation of "the conditional probability of given " rather than a synonym for it.
A trivializing formalization would let or be an unconstrained hypothesis unconnected to and (making the goal a tautology about whatever function is supplied); this is ruled out here by deriving from by the book's own formula and constraining by the disintegration identity above, not taking either as a free unconstrained parameter.
Lemma 2.23, Lemma 2.30, L_class/L_hinge, risk/bayesRisk and CanBeClipped/clip are
reusable beyond this mission: Lemma 2.23 and the risk/Bayes-risk vocabulary recur throughout the
book (clippability is used again in Section 7.4 and, per this series' README, this chapter's
Theorem 2.31 itself is restated inside Chapter 6's oracle inequality). Contributions completing
the two milestone proofs and the goal's sorry are welcome; a from-scratch alternative proof
avoiding Lemma 2.23 (e.g. by a direct case analysis on outside ) would also be a
valid solution to the goal, since the milestones are the book's own attack path, not a required
lemma structure.
How many labeled examples does a learning algorithm need to see before its output generalizes well to unseen data? Chapter 2 of Foundations of Machine Learning answers this question for the simplest nontrivial setting — a finite hypothesis set — and in doing so introduces the book's central object, the Probably Approximately Correct (PAC) learning framework: a distribution-free, high-probability guarantee relating a learner's sample size to the accuracy and confidence of its output. Every later chapter's generalization bound (VC-based, Rademacher-based, margin-based) is a variant of the same "probability of a bad event is small" argument this chapter proves in its most elementary form, so getting the chapter's core definitions and its two bracketing theorems (consistent and inconsistent finite-) right is the foundation the rest of the book's guarantees build on.
A learner sees a sample drawn i.i.d. from a fixed but unknown distribution on an instance space , labeled by an unknown target concept drawn from a concept class ; a hypothesis from a fixed hypothesis set is judged by its generalization error (Definition 2.1) against its empirical error (Definition 2.2) on the observed sample. A concept class is PAC-learnable (Definition 2.3) if some algorithm, given a polynomially-bounded number of samples, returns a hypothesis whose generalization error is at most with probability at least , for every accuracy and confidence and every distribution — the "distribution-free" and "for all target concepts" character of the definition is what makes it a genuine worst-case learning guarantee rather than an average-case one tailored to a particular data-generating process.
Theorem 2.5 (consistent case, milestone). If is finite and algorithm always returns a hypothesis consistent with the target concept on the training sample (), then whenever .
Corollary 2.11 (single-hypothesis Hoeffding bound, milestone). For a fixed hypothesis and any , with probability at least , .
Theorem 2.13 (inconsistent case, goal). For a finite hypothesis set and any , with probability at least , simultaneously for every ,
Theorem 2.13 is the chapter's capstone because it removes Theorem 2.5's consistency
requirement — the typical case in practice, where no hypothesis in perfectly fits the
training data — while paying only an additive price inside the square root, via a
union bound over applied to Corollary 2.11's per-hypothesis concentration bound. It is also
the template every later generalization bound in the book refines: Chapter 3 replaces
with the growth function / VC-dimension to handle infinite hypothesis sets, and Chapter 3's
Rademacher-complexity bound is the direct machine-independent generalization of the same
argument. No prior art on the Prove2Me platform is faithful to this chapter's PAC-learning
content (GET /theorems?q=PAC-learnable returns no hits), so all six items are drafted fresh.
Theorem 2.13's own proof is a short combination of two ideas already present in the chapter (Corollary 2.11's Hoeffding bound plus a union bound over hypotheses), but each ingredient carries its own faithfulness burden. Corollary 2.11 needs the sample and the target hypothesis kept in the right relationship — fixed, random — for the bound to be Hoeffding's inequality and not a vacuous statement about a random hypothesis. Theorem 2.13 needs the quantifier placed inside the probability event (a single sample must work for every at once), not outside it (which would only assert each 's bound holds with high probability for a sample chosen depending on ) — the difference between a uniform convergence bound and separate, weaker statements. Definition 2.3's "polynomial function " is a genuine formalization judgment call, addressed below.
GeneralizationError/EmpiricalError are typed generally over (matching Definition
2.1/2.2's own general statement, ""), since Theorem 2.5 itself is stated for general
, not just ; Corollary 2.11 and Theorem 2.13 specialize to
, matching their own explicit "" (Corollary 2.11) and the
surrounding inconsistent-case section's restriction to binary classification. The i.i.d. sample
is modeled as the identity random variable on the product-measure space
in both Corollary 2.11 and
Theorem 2.13, matching the book's own notation exactly. IsPACLearnable
(Definition 2.3) makes "polynomial function" precise as a function bounded above by
for some constants , , uniform in its (nonnegative)
arguments — the standard reading of "polynomial in its arguments" in the absence of a
ready-made multivariate polynomial-growth predicate in Mathlib; dropping this constraint
entirely (stating only "there is some threshold function") would silently weaken Definition
2.3 to a strictly easier notion of learnability, since virtually any finite or well-behaved
concept class admits some (possibly super-polynomial) sample-complexity threshold — this is
exactly the distinction Example 2.7 (the universal concept class) uses to demonstrate a class
that is not PAC-learnable despite admitting a consistent hypothesis set. No numerical
constant in Theorem 2.5, Corollary 2.11 or Theorem 2.13 is altered from the book's own; no
upper bound on is added anywhere the book itself leaves it unrestricted (the theorems
remain true, if vacuous, for ). Not formalized: the "efficiently PAC-learnable"
running-time clause of Definition 2.3 (a second, independent polynomial-time condition on
not needed by either milestone or the goal); Corollary 2.10 (the raw two-sided Hoeffding
statement Corollary 2.11 is immediately derived from by solving for , making it
redundant with Corollary 2.11 as a formalization target); the axis-aligned-rectangles worked
example (Example 2.4–2.9), which illustrates the framework rather than proving a new general
result, and the trivializing formalization this chapter invites — reusing Mathlib's rectangle
machinery to encode only the specific two-dimensional geometric argument rather than the
general finite- theorems — is exactly what this mission avoids by drafting Theorems 2.5 and
2.13 in their general, hypothesis-set-agnostic form.
Most machine learning training objectives — deep network losses, matrix factorization, regularized empirical risk with a nonconvex loss — are not convex, yet the great majority of convergence theory available before Ghadimi and Lan's 2013 work applied only to convex problems or gave no non-asymptotic rate at all. Ghadimi and Lan (2013) established the first non-asymptotic complexity bounds for stochastic first-order methods on smooth nonconvex problems, using the norm of a gradient mapping (rather than function-value suboptimality, which is meaningless without convexity) as the convergence measure, together with a randomized stopping rule that removes the need to know in advance which iterate will be best. This mission formalizes the constrained, composite generalization of that theory — Lan's own extension (2020) to problems with a nonsmooth term and a general Bregman geometry rather than the Euclidean norm — culminating in the stochastic complexity bound for the randomized stochastic mirror descent (RSMD) algorithm.
Fix a nonempty closed convex , a continuously differentiable (possibly nonconvex) with -Lipschitz gradient, and a simple convex (possibly nonsmooth) (e.g. or ); write , (assumed finite). For a distance-generating function with modulus 1 and its prox-function , the generalized projection at with gradient-like input and stepsize is
which reduces to itself when and : is a generalized projected gradient (or gradient mapping) of at , and its norm going to zero is the right notion of "approximately stationary" for the composite, possibly-nonconvex problem .
The randomized stochastic mirror descent (RSMD) algorithm, given only a stochastic first-order oracle returning with and (Assumption 13), forms a mini-batch average of oracle calls at each step , updates via the generalized projection with , and stops at a randomly chosen index (drawn from a prescribed pmf , independently of the optimization process) rather than a deterministic final iterate.
for (strict for at least one ) and chosen as in (6.2.30), the expectation over both and the oracle randomness .
Every result states its constants exactly as the book derives them; no milestone or the goal hides a rate behind an unspecified .
The goal theorem gives the complexity of the RSMD algorithm in terms of a squared generalized gradient-mapping norm — the correct convergence criterion for constrained, composite, possibly nonconvex stochastic optimization, since function-value suboptimality is not controllable without convexity and unconstrained gradient norms are meaningless once or is nonsmooth. Choosing and appropriately (a corollary this mission does not formalize) turns this bound into the celebrated total-oracle-call complexity for finding an -stationary point in expectation — the standard benchmark every later stochastic nonconvex method (variance-reduced SGD, SPIDER, and their composite/constrained variants) is compared against.
No result in this mission has a machine-checked proof on Prove2Me under this exact hypothesis set.
The two closest platform results, both from lean-optrates (Shi), are genuinely different
objects: ShiOptRates.gd_exact_rate is plain, unconstrained, deterministic gradient descent
(, no set , no composite , no generalized projection), and
ShiOptRates.Stochastic.sgd_rate is plain SGD under the same unconstrained, non-composite
setup — its filtration/conditional-expectation formalization pattern (a Filtration ℕ, μ[·|ℱ k] for the unbiasedness and variance-bound hypotheses) is the same one this mission's goal
theorem uses, confirming it as the platform's established idiom for this class of result, but the
mathematical content (plain gradient step vs. generalized-projection/mirror-descent step, no
or ) is different. Neither is reused; both are noted as the platform's nearest existing work.
The generalized projection replaces the Euclidean projection with an arbitrary Bregman-based prox-mapping and absorbs the nonsmooth term directly into the subproblem — a formalization that quietly assumes or would collapse every milestone here into the special case and prove nothing about the constrained composite problem the chapter is actually about. The harder difficulty is in the goal theorem's own randomness: the book's proof does not use an unconditional (marginal) form of Assumption 13, because from step 2 onward is itself a random variable (a function of the history ), so the cross-term the proof needs to vanish requires a conditional statement — "" is the book's own phrasing. A formalization using only marginal moment bounds would either be unprovable as stated or, worse, would misstate the theorem by using hypotheses too weak for the claimed conclusion.
generalized_projection_gradient_bound, generalized_projection_characterization,
nonconvex_md_bound and nonconvex_md_rate are stated over a real inner product space (Chapter
6's own generality — unlike Chapter 3, §6.2.3 explicitly restricts to "the norm associated with
the inner product"), with every argmin-defined point (, and the iterate sequence )
represented by its pointwise minimality property rather than an argmin term, consistent with
this series' convention. The goal theorem, rsmd_complexity_bound, additionally introduces a
probability space (Ω,P) and a Mathlib Filtration ℕ 𝒢, with x k/G k required
𝒢(k-1)-strongly-measurable and Assumption 13 stated via MeasureTheory.condExp (𝒢 (k-1))
(conditional mean 0, conditional second moment ≤ σ²/m_k) — the conditional form the book's own
proof actually needs, not a weaker marginal substitute. The σ²/m_k bound is (6.2.40)'s
conclusion for the m_k-sample batch average, taken as a hypothesis on the already-averaged G k
directly rather than re-derived from m_k raw i.i.d. calls (that derivation is not itself a
numbered result of the book). 's independence from the process is stated via
ProbabilityTheory.IndepFun; every integrability side condition the conclusion's Bochner
integral needs to be non-vacuous is stated explicitly, guarding against the well-known trap of an
uninhabited/non-integrable hypothesis silently defaulting condExp/the integral to 0 and making
the theorem trivially true.
A trivializing formalization this mission rules out: taking and
throughout would make every generalized projection collapse to the ordinary gradient, reducing
this entire mission to a restatement of plain (stochastic) gradient descent — exactly the
ShiOptRates results already on the platform — rather than the constrained composite theory the
chapter develops; , and are kept as genuine free parameters in every milestone and the
goal.
Left out of scope, for time: Theorem 6.6(b) (the convex-case corollary on , requiring the nondecreasing/nonincreasing stepsize side-conditions of (6.2.33)/(6.2.35)); the raw-sample derivation of (6.2.40); Lemma 6.3 (the stationarity consequence of a small gradient mapping, using and the normal cone ); the 2-RSMD algorithm and its large-deviation improvement; and the gradient-free (RSMDF) variant.