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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
Sequential planning problems — inventory replenishment, hydro-thermal power scheduling, asset-liability management — routinely span more than two decision epochs, with information about the future revealed gradually as each period unfolds. A two-stage recourse model (decide now, observe once, recourse once) is too coarse for these: it either collapses the whole horizon into a single "wait and see" observation or forces an ad-hoc rolling-horizon heuristic with no optimality guarantee. The multistage stochastic program is the natural model that keeps the full sequence of decisions and observations, and Benders (L-shaped) decomposition is the workhorse algorithm the field has used to solve it since Van Slyke and Wets [1969] introduced it for the two-stage case. Ho and Manne [1974] and Glassey [1973] first proposed nested decomposition for deterministic multistage models; Louveaux [1980] extended it to multistage quadratic stochastic programs, and Birge [1985] gave the linear multistage generalization this mission formalizes, later implemented at scale by Pereira and Pinto [1985] and Gassmann [1990] and still the basis of production stochastic-programming solvers today.
A multistage stochastic linear program unfolds over stages . At each stage, uncertainty resolves into one of finitely many realizations, so the whole process of realizations forms a scenario tree: a single scenario at (the root), branching into finitely many scenarios at , each of those again branching at , and so on. Write for a scenario (a tree node) and for its ancestor, the scenario at stage that descends from; is the set of scenario 's descendants at the next stage. Each scenario at stage carries its own decision vector , bounded above (, coordinatewise), subject to the linear constraint
where the recourse matrix depends only on the stage (fixed recourse) while the transition matrix and right-hand side may vary scenario by scenario. Stacking every scenario's constraint over the whole tree gives the deterministic equivalent linear program, minimizing the probability-weighted total cost over this feasible region — problem (3.4.1) in the source.
The nested L-shaped method solves (3.4.1) by decomposition rather than forming this (typically enormous) single LP directly. Each scenario owns a small subproblem, , that looks exactly like a two-stage L-shaped subproblem: it has 's own constraint and bound, plus a running set of feasibility cuts and optimality cuts accumulated so far, plus, if has descendants, an approximation variable standing in for the (unknown, convex, piecewise-linear) future cost of everything downstream of . Solving either finds it infeasible — in which case a feasibility cut is derived from the infeasibility certificate and sent up to 's parent — or finds an optimal dual solution, whose aggregate over all of 's children (weighted by conditional probability) becomes a candidate optimality cut for . The method sweeps forward and backward across the tree, feasibility and optimality cuts accumulating at every internal node, until no node's subproblem produces a fresh cut.
This is the chapter's only numbered result and the weakest faithful statement of "the method works": it makes no claim about the number of iterations beyond finiteness, and none about which sequencing protocol (forward-forward-back, or any other) is used to choose which subproblem to solve next.
Finite convergence is what separates an algorithm from a heuristic: without it, nothing rules out an infinite sequence of ever-finer cuts that never certifies optimality or infeasibility. Birge's 1985 result is the reason nested Benders decomposition can be used as an exact method rather than an approximation, and every later refinement (bunching, sifting, multicuts, parallel implementations, all mentioned in the source text) modifies how cuts are generated or which subproblem is solved next without touching this finiteness guarantee — they are all still instances of the same cut-generation mechanism this mission formalizes. The two-stage case (Chapter 5, Theorem 2) is the special case of this theorem; the mission's tree-indexed state and transition relation are written to specialize to the two-stage development directly when the tree has one branching level, though the two developments are not connected by an import (see Formalization scope). No machine-checked proof of either the two-stage or multistage case appears to exist prior to this series; formalizing it here produces the first Lean statement of the mechanism nested Benders decomposition rests on.
The obvious first idea — prove finiteness by bounding the total number of cuts a node can ever receive, the way a flat scenario set bounds the two-stage method's cut count by its number of LP bases — fails because a node's own subproblem is not a fixed-size LP: every cut recorded at node becomes a new row of 's own constraint set, so the "number of possible bases" at keeps changing as the algorithm runs, and the bound at depends recursively on how many cuts 's own children could ever produce. The book's actual argument (p. 290) is a genuine induction on the stage index, from the last stage backward: assume the bound holds for every node at stage , then combinatorially bound the finite number of extended bases at stage that this permits, then take the finite union over every possible extension size. This mission's Lean development commits to a scope that keeps a node's basis a fixed-size object (see below) rather than re-deriving that combinatorial bound.
Every stage shares one decision dimension and one constraint dimension (Fin n,
Fin m); the book allows these to vary by stage but nothing in Theorem 1's statement
needs that generality. Scenario probabilities p are the unconditional probability of
reaching a node, required strictly positive and summing to within each stage
(Instance.hp_pos, Instance.hp_sum); the aggregation formulas use only the ratio
for a child of , which reads the same whether p is unconditional or
conditional, so this is a normalization choice, not a substantive restriction. The upper
bound ub is ℝ-valued rather than extended-real-valued, which is Theorem 1's own
hypothesis ("finite upper bounds"), not an added convention.
The one deliberate scope-narrowing choice, flagged here and in MODERATION_NOTES.md, and
strengthened in this revision after moderator review (2026-09-19,
CHANGES_REQUESTED.md #2): a node 's dual witness (Basis, FeasBasis) is read off
's original constraint (1.2) alone — the fixed-size recourse matrix
— never off the extended constraint set (1.2)-(1.4). The gap this
leaves is broader than "accumulated cuts are ignored": 's own continuation variable
— present in (1.1)'s objective, and fixed to from Step 0 onward, not
merely absent until cuts accumulate — has no representation at all in Basis,
multiplier, basisValue, or the optimality-cut coefficients optCutCoeffs computes
for a parent of . Consequently, whenever a child used in an optimality cut is
itself an interior node ( has children of its own, i.e. ,
which happens for every tree), the mechanized cut coefficients are not the
book's of Eq. (1.1) and are not the printed algorithm's
mechanism at that node — they are the dual of 's plain sub-LP alone, omitting 's
own contribution to the recourse value entirely, not only the portion contributed by
's accumulated cuts. This gap is inert exactly when every child aggregated in a cut is
a last-stage node (, where the mechanism coincides with the already-published
two-stage sibling 05-two-stage-methods) and active for every deeper cut, which is most
of what a general Tree H actually exercises. Concretely: as mechanized, the
optimality-cut half of Step (Bases.optCutCoeffs, Step.opt) is faithful to the
printed nested L-shaped method's cut-generation step only when every child it
aggregates over is a last-stage node; for an interior child it computes a value that
omits that child's own term rather than the book's recursive one. The
feasibility-cut half (Bases.feasCutCoeffs, Step.feas) has no such gap — feasibility
does not involve at any stage — and the tree/instance layer (Tree, Instance)
and the goal theorem's own outer shape are unaffected: thm1_finite_convergence's
statement (existence of a finite, Step-reachable state that is infeasible-certified
or globally optimal) is not weakened, but the reader should treat the mechanized Step
relation itself, for H ≥ 3, as a documented variant of Steps 1-2 rather than a literal
transcription of them at every node — see STATUS.md's Revision section for the
moderator exchange this responds to. Reworking cut generation to consume each child's own
current witness directly, so that an interior child's continuation
value is no longer dropped, is left to a future revision; it is a materially larger
change (the child's local optimum is then piecewise-linear rather than linear in its own
parent's decision, so the duality argument needs a genuinely different — not merely
extended — basis notion) than this session's time budget allows. This keeps every basis
type a fixed-size Fin m → Fin n object, exactly as in the two-stage method, and keeps
the algorithm's finite-step bound an explicit, provable cardinality
(|Node × FeasBasis| + |Node → Basis|) rather than the book's own implicit,
recursively-defined one. The trivializing formalization this scope choice must not fall
into — declaring victory by proving the plain two-stage case is what convergence
"reduces to" without ever quantifying over the tree — is avoided because every definition
and the goal statement itself are stated for a general Tree H with unrestricted
branching, not merely ; what is disclosed above is a gap in how faithfully Step
models the book's own cut-generation mechanism at depth, not a restriction of the
statement to .
Reusable beyond this mission: Def_StochasticProg_Multistage_Tree (the finite scenario
tree) is a natural building block for 07-integer-programs (an integer restriction of
the same two-stage subproblem) and 10-multistage-approximations (multistage Jensen
bounds, which need the same tree). Contributions welcome: a faithful account of the
extended-basis induction sketched above, and a formalization of Chapter 6, Theorem 3
(finite termination of the quadratic nested decomposition of Section 6.2), which this
mission omits for time (see STATUS.md).
A micron-sized bead suspended in water and held by an optical tweezer is one of the standard measuring instruments of soft-matter physics: the bead's fluctuating position reports on the viscosity of the medium, on the stiffness of the trap, and on the forces exerted by whatever is attached to the bead. The quantity that experiments record is the mean-squared displacement (MSD) of the bead. Interpreting such data rests on a single classical calculation, due to Paul Langevin (1908): write Newton's second law for the bead including the drag of the fluid, the trap force and the fluctuating force of the molecular environment, multiply the equation by the position, and average over realizations. What comes out is a closed, deterministic, second-order ordinary differential equation for — no stochastic calculus required. This mission formalizes exactly that derivation, and the solution of the resulting equation, for a particle in a harmonic trap.
A particle of mass moves in Cartesian dimensions. Its position at time is the vector with components , ; its velocity components are and its acceleration components . The particle feels three forces: a hydrodynamic drag with drag coefficient ; a harmonic trap force with spring constant ; and a random force exerted by the surrounding medium, which is held at temperature . Newton's second law then reads
A single solution of this equation, for one realization of the random force, is called a path. An ensemble is a probability space of such paths, and the ensemble average of a quantity is . Two physical inputs single out a thermal environment: the random force is uncorrelated with the instantaneous position, , and the velocity obeys equipartition, with Boltzmann's constant. The mean-squared displacement is .
This is the weakest stable form of the result: it fixes no initial condition, no sign convention on the roots, and no regime (inertial or overdamped), and every later statement about the MSD of a trapped Brownian particle is a consequence of it.
For each realization, with ,
which is Newton's equation contracted with and rewritten using and .
With the two distinct roots of ,
solves the goal equation with , and in the inertialess (overdamped) case the solution reduces to , which grows as at short times and saturates at the equipartition plateau .
The MSD equation is what converts a measured displacement trace into physical numbers: its plateau calibrates trap stiffness, its short-time slope gives the diffusion coefficient , and the crossover between the two identifies the relaxation time . The derivation is also the historical template for treating noisy dynamics without a theory of stochastic integrals: Langevin's move of averaging the equation multiplied by is what makes the noise term drop out.
Formalizing it produces a machine-checked statement of the classical calculation together with the assumptions it actually needs, each of which is carried explicitly as a hypothesis rather than left implicit in the prose: interchange of ensemble averaging with time differentiation, integrability of the averaged quantities, decorrelation of the random force from the position, and equipartition. The pathwise identity and the solution-verification statements are elementary calculus; the substance of the mission is that the physical derivation is faithful once those hypotheses are written down.
The obvious route — solve the stochastic equation for and then square and average — requires a theory of stochastic integration against the random force, whose statistics the problem never specifies beyond the two averaged facts above. Langevin's derivation avoids this entirely, but the step "average the equation" hides two real assumptions: that commutes with (so that is the second derivative of ), and that vanishes at every time. Neither follows from the equation of motion; both must be hypotheses, and stating them precisely without weakening the theorem into vacuity is the formalization problem.
Paths are represented in components: position, velocity, acceleration and force are families , and the model predicate records that is the derivative of , that is the derivative of , and that Newton's law holds at every time, so no differentiability is smuggled in. Euclidean contractions are the single helper , so that , , and are all instances of one definition. Ensembles are an arbitrary probability space with the integral as average, and paths are indexed by the sample point; the averaging assumptions appear as hypotheses relating and its derivatives to integrals of the pathwise quantities. Dimension is arbitrary, the source's being a special case.
No hypothesis of the goal is vacuous: a deterministic ensemble (one path, a Dirac measure) with and a particle at rest satisfies all of them when , and nondegenerate instances exist for every choice of parameters, so the statement is not satisfied only in an empty context. All statements target real-valued time and real coefficients; no positivity of , , is assumed except where a milestone needs it for an asymptotic claim.
A black body is an idealized object that absorbs all radiation falling on it and, when held at a fixed absolute temperature , re-emits radiation whose spectrum depends on alone — not on the material, shape, or history of the body. Measuring that spectrum, and explaining it, was the central problem of late nineteenth-century thermal physics: the classical prediction of Rayleigh and Jeans grows without bound at short wavelengths, which is not what cavity radiation does.
Max Planck's 1900 formula fits the measured spectrum at every temperature and every wavelength, and it does so by quantizing the energy exchanged between matter and the radiation field. Two features of that formula are used constantly outside physics proper — in astronomy, remote sensing, radiometry, and illumination engineering. The first is the shape of the curve. The second is where its maximum sits: the peak wavelength is inversely proportional to the temperature, which is Wien's displacement law, discovered by Wilhelm Wien several years before Planck's formula and recovered from it as a corollary. This is why a heated piece of metal runs red, then orange, then white; why the Sun's per-wavelength emission peaks near ; and why infrared cameras aimed at mammals at are built for about .
This mission formalizes Planck's law as a definition and derives Wien's displacement law from it, in both the wavelength and the frequency parameterization, including the transcendental maximization equation and the numerical value of its root.
Fix three positive real parameters: the Planck constant , the speed of light , and the Boltzmann constant . They are left as variables rather than numerical constants, so that every statement is a theorem about the functional form, valid in any unit system.
For an absolute temperature , Planck's law is given in two parameterizations. Per unit frequency , the spectral radiance is
and per unit wavelength it is
These are different functions, not the same function in different letters: radiance is defined per increment of the independent variable, so passing between them carries the Jacobian factor . Consequently the two curves peak at different physical locations, and the mission keeps both.
The third object is the dimensionless shape function
with for the wavelength form and for the frequency form.
The goal is Wien's displacement law in the wavelength parameterization. Writing for the positive solution of the maximization equation , the goal asserts the existence of a constant
such that for every temperature the function on has a strict global maximum, attained at
and nowhere else. With SI values of , , this is .
The milestones build to this: the Jacobian relation between the two parameterizations; the strong (temperature-independent shape) form of the law; existence and uniqueness of the root of the maximization equation; the strict maximum of at that root; the frequency-parameterized displacement law, with and ; and a rigorous numerical enclosure of .
The result itself. Wien's displacement law is the quantitative content of "hotter means bluer". It converts an observed color into a temperature, which is how stellar surface temperatures, incandescent filament temperatures, and remote-sensed surface temperatures are read off in practice. Its strong form — that the spectrum has one fixed shape, rescaled by — is what licenses tabulating the Planck spectrum once and reusing it at all temperatures, including the percentile table of the radiation distribution.
Formalizing it. Both results are classical and completely settled mathematically; the work here is machine-checked derivation, not discovery. Mathlib has the exponential function, derivatives, and the tools for strict-monotonicity and interval arguments, but carries no formalization of the Planck spectrum. This mission contributes a definition bundle for the Planck spectral radiance that later work (Stefan–Boltzmann, the Rayleigh–Jeans and Wien-approximation limits, the percentile table) can import directly, plus reusable analytic lemmas about and about the equation that are independent of the physics.
The obvious argument — differentiate, set the derivative to zero, solve — fails at the last step: has no closed-form solution in elementary functions, and the informal source resolves it with the Lambert function. A formal proof therefore cannot produce the maximizer explicitly; it must establish existence and uniqueness of the critical point and separately prove the critical point is a strict global maximum, which needs the behavior of at both ends of rather than a local second-derivative test. The numerical milestone adds a different difficulty: certified bounds on a transcendental root require explicit rigorous estimates on at a specific rational point, not floating-point evaluation.
A second trap is the parameterization. Substituting into does not give , and the two peaks genuinely differ (for , against ). The Jacobian milestone is stated precisely so that this cannot be blurred.
Everything is over the real numbers. , , , , , are real variables carrying explicit positivity hypotheses wherever the statement needs them; no numerical values of the physical constants are hard-coded, and the physical dimensions are not modeled. The spectral radiance is defined by a total function, so it returns a junk value outside the intended domain (in particular where the denominator vanishes, at ); every theorem restricts to the physical range by hypothesis, so no claim rests on junk values.
The peak statements are formulated as strict inequalities against all other admissible arguments — for the goal, every with — rather than as a local maximum or a vanishing-derivative condition. This rules out the trivializing formalizations: a first-order condition alone would not exclude a minimum or an inflection, and a local statement would not exclude a second, higher peak elsewhere.
The maximization constants are pinned down, not merely asserted to exist: the goal requires the constant to equal for a positive satisfying , and a separate milestone gives the enclosure . Uniqueness of that root is itself a milestone, so the pair determines completely.
A complete development needs Mathlib's Real.exp API, differentiability and the mean
value theorem or a strict-monotonicity argument, and interval arithmetic or explicit
Taylor bounds for the numerical enclosure. The lemmas about the shape function and about
are stated for a general exponent and are reusable beyond this
mission. Contributions of the Stefan–Boltzmann integral, the Rayleigh–Jeans and Wien
approximation limits, and the logarithmic ("per proportional bandwidth")
parameterization would be natural follow-ups but are out of scope here.
Roughly half of the stars in our galaxy belong to binary star systems: pairs of stars close enough to each other that their mutual gravitational attraction dominates every other influence, and far enough from every other star that the rest of the galaxy can be ignored. Such a pair is the cleanest physical realization of the Newtonian two-body problem, and it is the reason the two-body problem is not merely a textbook exercise: the masses of stars other than the Sun are known almost entirely because binaries can be observed, and the observation is converted into a mass by exactly the chain of reasoning formalized in this mission.
This mission formalizes Section 4.16, "Binary star systems", of Richard Fitzpatrick's
Celestial Mechanics lecture notes (University of Texas at Austin), Eqs. (4.108)–(4.119). It is
the first mission of a planned series on the same source; the whole series shares the Lean
namespace CelestialMechanics.
Two point masses move in under Newtonian gravity, with position vectors and defined for all times . Write for the relative separation and for the distance between the stars. The gravitational force the first star exerts on the second is Eq. (4.108),
and Newton's second law for each star reads
A pair of twice continuously differentiable, never-colliding trajectories satisfying these two equations is what this mission calls a Newtonian gravitational two-body system.
Three derived objects organize the material. The center of mass is . The relative Kepler problem with gravitational parameter , , is the equation
for a nowhere-vanishing curve . A Keplerian conic orbit with major radius , eccentricity and angular momentum per unit reduced mass is a planar curve given in polar coordinates by
which are Eqs. (4.112)–(4.114); the elements are tied together by Eq. (4.115), .
The goal theorem is an existence-and-description statement: for every , every pair of masses and every choice of orbital elements , , there exist trajectories , polar functions and a time such that
The milestones are the individual steps of Section 4.16, ordered as in the source: the reduction of the two-body system to the one-body problem (4.110)–(4.111); the uniform motion of the center of mass, which makes the center-of-mass frame inertial; the positions of the two stars in that frame (4.118)–(4.119); the verification that the conic (4.112)–(4.115) solves (4.110); the period of revolution (4.116)–(4.117); and the inversion of these relations that yields the two stellar masses from observation.
The result itself. The theorem is the complete qualitative and quantitative picture of a binary orbit: each star traverses an ellipse about the common center of mass, the two stars are diametrically opposite one another at every instant, the distances from the center of mass are in the fixed ratio , and the period depends only on the major radius and the total mass. The last two facts are what astronomers use: the measured pair gives the mass sum , the observed ratio of the two apparent orbits gives , and sum plus ratio give the individual masses. The same reduction also supplies the finite-mass correction to one-body solar-system orbit theory, in which is replaced by .
Formalizing it. The mathematics has been settled since Newton, so the contribution here is a
machine-checked development rather than a new result. Mathlib currently has extensive analysis
infrastructure — iterated derivatives, ContDiff, Euclidean spaces — but no development of the
Kepler problem: neither the conic solution of the inverse-square equation of motion nor Kepler's
laws. The reusable output of this mission is therefore a small, self-contained Kepler library:
the two-body reduction, the conic solution, and the period law, stated for curves in
in a form that later missions in the series (perturbations, orbital elements,
the restricted three-body problem) can import unchanged.
Two milestones carry essentially all of the analytic work.
The first is showing that the conic really solves (4.110). The obvious route — differentiate twice and simplify — runs into the fact that is given as a function of and is given only implicitly, through the angular-momentum law . Even the regularity in the conclusion has to be earned: the hypotheses supply only differentiability of , and twice-continuous differentiability of the curve must be bootstrapped from the two polar equations. Getting the Cartesian second derivative into the form requires the relation at exactly the right place, and this is where a sign or a factor typically goes wrong.
The second is the goal theorem, which is an existence statement and therefore needs the angular equation to be solved globally in time, on all of and not merely on a small interval. The right-hand side is smooth and, for , bounded above and below by positive constants, so the solution exists for all time and advances by in a fixed time ; but "exists for all time" is a real obligation in Lean, and a naive appeal to a local existence theorem does not discharge it.
Space is EuclideanSpace ℝ (Fin 3), so the norm is the Euclidean one and the three Cartesian
components are indexed ; the orbital plane is fixed to be the - plane, exactly as
in Eq. (4.112). Trajectories are total functions : all statements are
global in time, and no restriction to an interval or to positive times is made. Derivatives are
iteratedDeriv, and smoothness is ContDiff ℝ 2. Masses and are positive reals wherever the
physics needs it, and this is stated explicitly rather than left implicit. Eccentricity is
restricted to throughout, so only bound (elliptical and circular) orbits are in
scope; the parabolic and hyperbolic cases of Sections 4.13–4.15 are left to later missions.
Two trivializing formalizations are ruled out by construction. The definitions never allow the separation to vanish, so no statement is satisfied by a collision; and in the goal theorem the angular momentum and the period are not existentially quantified but pinned to their Keplerian values in terms of , so the orbit cannot be rescaled to make the conditions easy to meet.
Contributions of independent interest are welcome: conservation of angular momentum and of energy for (4.110), the equal-areas law, the eccentricity (Laplace–Runge–Lenz) vector, and the Kepler equation relating mean and eccentric anomaly all sit naturally on top of this development.
A "rule of thumb" classifier — a single pixel's brightness distinguishing handwritten "0" from "1" — is trivial to produce and barely better than a coin flip. A rule that gets every example right is, in general, far harder. Boosting asks whether many weak, easy-to-produce rules can be combined into one strong, hard-to-produce rule, and Chapter 11 answers it via a black-box reduction: any online convex optimization algorithm with sublinear regret, paired with access to a weak learner, yields a boosting algorithm — the same OCO-to-learning-theory template Chapter IX used for generalization, now applied to training-set fitting.
A concept class is -weakly-learnable (Definition 11.1) if some algorithm, given enough labeled samples, returns a hypothesis with error at most with high probability — better than random guessing by a fixed margin , far short of the arbitrarily-small error strong (PAC) learning demands. Section 11.2.1 fixes a simplified setting: binary zero-one loss, a realizable concept class (some has zero error), and a weak-learning oracle returning, on distribution over a fixed sample of size , a hypothesis with .
Algorithm 34 runs an OCO algorithm over the -dimensional simplex (distributions over the sample): at each round it calls the weak learner on the current distribution , builds the -valued cost vector recording which examples got right, updates for the linear cost , and finally outputs the majority vote .
For chosen so , Algorithm 34 returns with : with high probability, classifies the entire training sample perfectly.
This is one of the cleanest reduction theorems in the book: it needs no property of the weak
learner beyond its -margin guarantee, and no property of the OCO algorithm beyond a
regret bound — any of Chapters III–X's algorithms (multiplicative weights, OGD, RFTL, ONS...)
plugs in directly, and §11.2.3 specializes the reduction with multiplicative weights to recover a
close relative of AdaBoost, one of machine learning's most influential algorithms. The proof
technique — a contradiction argument on the existence of a "hard" residual distribution
uniform over the misclassified examples — is itself instructive and structurally different from
Chapter IX's martingale/concentration argument, despite both chapters being "OCO implies a
learning-theoretic guarantee" reductions. No prior art was found on the platform for boosting or
AdaBoost (planning search: q=boosting, q=AdaBoost — 0 hits); this mission drafts the theorem
fresh.
The proof's key step packages the algorithm's regret guarantee (a worst-case statement, true for every cost sequence including an adversarially-constructed one) into a proof by contradiction: assuming some nonempty set of misclassified examples survives, the uniform distribution over is shown to make every perform at best exactly at the threshold on average (since 's sign disagrees with the true label on every point of , at most half of the rounds' hypotheses can have agreed there), while the weak-learner guarantee (via a union bound over all rounds) forces the actual played distributions to see average performance — and the algorithm's low regret against specifically then closes the gap into an outright contradiction (, impossible for ). This chain — union bound over rounds, regret bound against one specific (adversarially-identified) comparator, and an averaging argument over the residual set — is more intricate than its short proof suggests.
EmpiricalErrorWeighted/EmpiricalError give the (weighted and uniform) training-error
quantities exactly as the book states them, with real-valued (±1) labels and predictions — the
convention this chapter's sign-based majority vote needs, distinct from Chapter IX's
Bool-valued zero-one loss (a deliberate, chunk-local choice, not a conflict, since the two
chapters use different label conventions for different reasons — see MODERATION_NOTES.md).
IsBoostingRun formalizes Algorithm 34's five lines, with the weak learner's round-t call
modeled as a random hypothesis h_t : Ω → X → ℝ (since a weak-learning call is itself
probabilistic) rather than a deterministic function, matching the book's own probabilistic
per-call guarantee. The goal theorem states the weak-learner guarantee (hweak), the OCO
regret guarantee (hA), and the choice of T (hTreg) as explicit hypotheses, per BRIEF.md's
own instruction that these are the theorem's real content, not incidental setup. h̄ is typed as
an arbitrary X → ℝ, never coerced into H — the book's own explicit remark that the boosted
hypothesis need not belong to the original weak-hypothesis class.
This chunk has no milestones: Chapter 11 is short and largely monolithic around Theorem 11.2,
with Section 11.2.1 ("Simplification of the setting") and 11.2.2 ("Algorithm and analysis")
building directly to it with no other numbered lemma on the relevant pages (PDF 207–211).
Definition 11.1 (weak learnability) is drafted as a definition, not manufactured into a
milestone, per CAPTAIN_BRIEF.md's own rule that definitions are never milestones and
BRIEF.md's explicit allowance for a mission with fewer than 3. §11.2.3's AdaBoost
specialization (a corollary discussion, not a separately numbered theorem on these pages) is not
formalized.
Rings of arithmetic power series — power series with integer coefficients that converge on a disc of radius close to — sit between algebra and analysis: an element has both archimedean zeros, in the complex disc, and non-archimedean ones, at -adic points. Harbater (Convergent arithmetic power series, Amer. J. Math. 106 (1984), 801–846, DOI 10.2307/2374325) showed that a well-chosen ring of such series is a principal ideal domain and identified its prime ideals; the same ring is the arithmetic model of the closed disc of radius in the adic space .
The result was put to work in Clausen–Scholze's Lectures on Analytic Geometry (Lecture VII), where supplies a two-term presentation of the real numbers as a condensed abelian group: for there is an exact sequence , whose existence rests on the principality of the kernel of evaluation at . The quantitative refinement of that sequence (Propositions 7.2 and 7.3 of the notes) is what produces the -norms in the analytic ring structure on .
Fix a real number with . An integral Laurent series is a family of integers whose support is bounded below, written ; these form the ring under coefficientwise addition and the Cauchy product.
Define
Concretely, lies in when the associated Laurent expansion converges on some punctured disc with strictly larger than — an overconvergence condition. For a real or complex number, denotes the evaluation, whenever the family is summable.
Two features distinguish this ring from the classical Tate algebra. The coefficients are integers, not elements of a complete field, so reduction modulo a prime is available and produces . And the condition is an overconvergence condition: the radius is required to be strictly larger than , which is what makes the ring behave like the ring of functions on a closed disc rather than an open one.
The ring is a subring of the domain , so integrality is automatic and the content of the goal is that every ideal is generated by one element.
Theorem 7.1 of the source also classifies the nonzero primes: kernels of evaluation at a complex with (up to conjugation); the ideals for prime; and kernels of evaluation at a topologically nilpotent unit of a finite extension of (up to Galois conjugacy). The milestones below formalize the parts of the classification that the principality proof actually consumes — surjectivity of the three evaluation maps, and principality of the archimedean kernels — and leave the full classification statement for a later mission in this series.
The result itself. Principality gives, for each point of the closed disc, a single equation cutting it out; that is exactly what the presentation needs. Downstream, that presentation is the input to the computation of measures on in the analytic-ring formalism, and the reason -spaces with appear there at all. Without it, one has no finite free resolution of by rings of arithmetic functions, and the structure results of Lectures VI–VII of the source lose their computational base.
Formalizing it. The mathematics is classical and fully proved; nothing here is open. What is missing is a machine-checked version. Mathlib has Hahn series, Laurent series, complex analysis on discs, and the -adic numbers, but nothing about arithmetic overconvergent series: not the ring itself, not the greedy expansions that make real evaluation surjective, not the invertibility criterion. Each milestone below is a self-contained piece of that missing theory, reusable outside this mission.
The obvious approach — Weierstrass preparation, as for the Tate algebra over a complete field — does not apply: the coefficient ring is not a field, and no single valuation controls it. An element of must be divided simultaneously by archimedean generators (complex zeros in the disc) and -adic ones, with the quotient required to stay integral and still overconvergent. Two steps carry the weight and fail for naive reasons:
Finiteness — that a nonzero element lies in only finitely many of the listed maximal ideals — mixes the identity theorem for holomorphic functions with a -adic Weierstrass argument, which is why the reduction and -adic surjectivity milestones are prerequisites rather than side remarks.
The ambient ring is Mathlib's LaurentSeries ℤ (Hahn series over indexed by ), and is given as a set of such series, cut out by the decay condition as for some . Evaluations are unordered sums over ; where a statement asserts a value of an evaluation, summability is asserted alongside it, so the junk value of a divergent sum cannot be exploited.
Because the carrier is a set, the goal theorem is stated for an arbitrary subring of whose underlying set is . That form would be vacuous if no such subring existed, which is precisely why the first milestone asserts its existence; the two together carry the intended content, and the mission is not considered advanced by the goal alone.
Milestone 6 formalizes only the case of part (3) of the source theorem (topologically nilpotent units of proper finite extensions of are out of scope, since Mathlib lacks the ambient theory of such extensions). Milestone 3 drops the "with multiplicity one" clause of the source and asserts only that the zero set in the punctured closed disc is .
A complete development will need: closure of the decay condition under the Cauchy product; summability of evaluations on the closed disc; the identity theorem for the induced holomorphic functions; greedy -adic expansions of real numbers with bounded integer digits; and -adic expansions in the lattice generated by a topologically nilpotent unit. Contributions of any of these, as standalone lemmas, are welcome.
Reflection positivity turns a factorized weight across a reflection plane into a positive-semidefinite kernel of observables. The first mission in this series certified that finite split-weight mechanism and its two-observable chessboard inequality. A physical finite-volume Gibbs model needs one more layer before it can consume those results: its unnormalized weight must have a strictly positive partition function, normalization must preserve the split representation, and the hypotheses used for probability normalization must not be confused with those used for reflection positivity.
This mission isolates that finite algebraic layer. It does not present the results as new mathematics; its purpose is to make the interfaces and their failure modes explicit enough for later clock and XY consumers.
Let be a finite half-configuration space and let a full configuration be . A split weight is
where is finite, , and . Its partition function and normalized weight are
For observables , define the reflected kernel
Positive semidefiniteness means symmetry together with nonnegativity of every real quadratic form.
The mission keeps two logically independent requirements visible. Nonnegative split coefficients give reflection positivity through a weighted Gram factorization. Pointwise nonnegativity , together with one strictly positive value, gives and probability normalization. Neither requirement is silently substituted for the other.
The positive targets prove:
Two controls freeze the boundary. The symmetric two-point matrix with diagonal and off-diagonal is pointwise positive and normalizes to a probability weight, but its raw and normalized delta-observable kernels are not PSD. Conversely, zero split data have nonnegative coefficients and PSD raw kernels, but and their formally normalized weight is not a probability weight.
The result is a reusable adapter between an unnormalized finite Gibbs factorization and the previously certified reflection-positive kernel API. It prevents a later model proof from treating pointwise positivity as if it were a Gram representation, or treating reflection positivity as if it guaranteed a nonzero normalizer. The next physical consumer can therefore focus on proving an explicit nonnegative factorization of its cross-plane Boltzmann weight.
All types and sums used for normalization and kernels are finite, and all weights, coefficients, features, observables, and matrices are real. The mission proves no clock- or XY-specific Gibbs factorization, no spectral or Gaussian-domination theorem, no thermodynamic limit, and no Kosterlitz--Thouless conclusion. Those require separate missions. Physical and are not conclusions here.
Finite Reflection Positivity Methods I: Split Weights and Infrared Modes, mission db962332-7a71-4d34-a01c-e85cdee243ce.ReflectionPositivityInfraredBound.lean, repository snapshot
dbf503b2909cc17787d40a21eb75a0c9354cc6ef:
https://github.com/MonumentalSystems/LeanProofs/blob/dbf503b2909cc17787d40a21eb75a0c9354cc6ef/LeanProofs/StatMech/ReflectionPositivityInfraredBound.leanA Markov process is reversible when, in equilibrium, transitions from to occur at the same average rate as transitions from to . Algebraically this is the detailed balance condition , and it is the single most useful structural property a network process can have: it replaces a global linear system by one equation per pair of states, and it hands you the equilibrium measure as a product of rate ratios rather than as the solution of anything.
The catch is that detailed balance mentions , which is exactly what one is trying to find. Chapter 2 of Richard Serfozo's Introduction to Stochastic Networks (Springer, 1999) removes the circularity. Kolmogorov's criterion characterizes reversibility by a condition on the rates alone: around every closed path, the product of the forward rates equals the product of the backward rates. And the proof is constructive — once the criterion holds, the invariant measure is
along any path from a fixed origin to , the criterion being precisely what makes the answer independent of the path chosen.
is a non-negative rate function on a state space , with the two-way communication property that and are positive together — a process failing this is visibly not reversible, since some transition would be possible but its reverse would not. A path is a sequence with throughout, and is assumed irreducible: every state is reachable from every other along a path. Write for the rate ratio.
is reversible when some positive satisfies the detailed balance equations. Such a is automatically an invariant measure, the total balance equations being the sum of the detailed ones.
Three statements are equivalent:
And when they hold, fixing any origin there is a positive with satisfying detailed balance and given at every state by the product of ratios along any path from .
The canonical form (2.2), that is reversible with respect to exactly when for a symmetric non-negative ; Example 2.1, the birth–death process with ; Theorem 2.2, that a process whose communication graph is a tree is reversible; and Theorem 2.5, the time-reversal criterion, which identifies a stationary distribution from a candidate reversed rate function without mentioning reversibility at all.
The results themselves. Kolmogorov's criterion is the working test. It is how one checks that a birth–death process, a random walk on a tree, a reversible Jackson network or a Whittle network with reversible routing is reversible, and it is a finite check on cycles rather than a search for an unknown measure. The ratio form (iii) is what gets used in practice: it says the product of ratios along a path is a well-defined function of the endpoints, which is exactly what licenses defining by that product.
Theorem 2.2 is the structural special case with no computation at all — a tree has no cycles, so the criterion is vacuous and reversibility is automatic. Theorem 2.5 points in a different direction: it identifies a stationary distribution from a guess at the time-reversed rates, and it is the tool Serfozo uses later to prove the Whittle equilibrium theorem a second way and to establish that departure processes from networks are Poisson.
Formalizing them. Mathlib has no reversibility theory for Markov processes: no detailed balance,
no Kolmogorov criterion, no time reversal of a rate function. It has SimpleGraph.IsTree, which the
tree item uses, and nothing else that bears on this chapter. The whole apparatus is contributed
here.
The goal is a genuine equivalence with a constructive core, and the three implications are of quite different character.
(i) (ii) is the easy one: multiply the detailed balance equations around the closed path and cancel the 's, which is legitimate because the values are positive. Note the criterion is asserted for arbitrary closed sequences, not only for paths; the two-way property is what makes both sides vanish together when some rate is zero.
(ii) (iii) is a cycle-splicing argument: two paths with the same endpoints concatenate, one reversed, into a closed path, and the criterion says its forward and backward products agree, which is the equality of ratio products.
(ii) (i) is where the construction lives. Fix an origin ; irreducibility gives a path to every state; define by the ratio product; (iii) makes it well defined; and then detailed balance at an edge follows by extending a path by that edge. Serfozo's Remark 2.9 gives the same construction as a recursion over the sets of states reachable in steps, which may be the easier route to organize.
The birth–death item is a telescoping recursion, , and the observation that the two families of detailed balance equations — for and for — are the same family. Theorem 2.2 is a cut argument: removing an edge of a tree splits the state space into two pieces joined by that edge alone, so the flow balance across the cut is the detailed balance equation for that edge. Theorem 2.5 is two lines of rearrangement once the sums are known to converge.
The state space is an arbitrary type and is an arbitrary non-negative real rate function; nothing here needs a process, a measure space or even countability, because reversibility as Serfozo defines it "applies to any nonnegative rates or probabilities as an algebraic property, not necessarily associated with a stochastic process". The same statements therefore cover discrete-time chains with read as transition probabilities, which is what the book points out.
Paths are functions with positive consecutive rates. A path of length zero is a single state and its ratio product is the empty product , which is consistent with .
Kolmogorov's criterion is stated for arbitrary closed sequences, exactly as the book states it, not only for closed paths. Under two-way communication the two readings agree — if one rate in the sequence vanishes then so does its reverse and both products are zero — but the book's form is the one that is directly checkable.
The canonical measure is not defined by a choice function. Instead the conclusion asserts the existence of a positive with satisfying detailed balance and agreeing with the ratio product along every path from the origin. That is the content of (2.9) without needing to pick a path for each state.
Theorem 2.2 is stated for a finite state space. Serfozo assumes the process is ergodic, and the cut-flow argument then sums the balance equations over one side of the cut; on an infinite state space that summation needs an integrability condition that the book leaves implicit in "ergodic". Finiteness makes the rearrangement unconditional and the statement clearly true; the general case is listed under contributions.
Theorem 2.5 is stated as the conclusion that satisfies the balance equations, with explicit summability hypotheses for the three families of sums involved. That is the stationary distribution additionally requires it to be normalized and the process to be ergodic, neither of which is part of the algebraic content.
Contributions welcome beyond the listed items: Theorem 2.4, the characterization of reversibility by invariance of the finite-dimensional distributions under time reversal; Remark 2.9's recursive construction of the canonical measure; Theorem 2.22 on reversible network processes with batch movements; Theorem 2.31 and the partition-reversible processes of Sections 2.8 and 2.9; and the reversibility criteria for Jackson and Whittle networks in Examples 2.24 and 2.25.
The central limit theorem says that converges to a normal random variable. Donsker's theorem says something much stronger: the whole rescaled path of the random walk converges to the whole path of a Brownian motion, as a random element of .
The payoff is a machine. Once in , every functional of the path that is continuous — or merely continuous at almost every Brownian path — transfers automatically. The maximum of the walk converges to the maximum of Brownian motion; the fraction of time the walk spends above a level converges to the corresponding occupation time; the last zero before time converges to the last Brownian zero before time , which is how the arcsine law escapes the simple random walk it was proved for. This is the invariance principle of Erdős and Kac: the asymptotic behaviour of a functional of should not depend on the step distribution, as long as the central limit theorem applies.
Chapter 8 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) proves this by embedding rather than by the usual tightness argument. Skorokhod's representation theorem puts a mean-zero, finite-variance random variable inside a Brownian motion as the value at a stopping time; iterating puts the whole walk inside one Brownian motion at a sequence of stopping times whose gaps are i.i.d.; and the law of large numbers then forces the embedded walk to be uniformly close to the Brownian path.
Let be i.i.d. with mean and variance , and . Define to be at integer and linear in between, and set
a random element of , the continuous functions on the unit interval with the uniform norm and its Borel -algebra.
On the Brownian side, let be a Brownian motion, and write for its restriction to , again a random element of .
that is, the laws of on converge weakly to the law of Brownian motion. This is a statement about measures on a function space, not about finite-dimensional marginals: it is exactly the extra content over the central limit theorem.
Theorem 8.1.1, Skorokhod's representation theorem: a mean-zero, square-integrable law is the law of for a stopping time with ; Theorem 8.1.2, the embedding of the whole walk, giving stopping times with distributed as the walk and with i.i.d. gaps; Theorem 8.1.5, the continuous mapping theorem for almost surely continuous functionals; and its two workhorse instances, Example 8.1.6 on maxima and Example 8.1.8 on occupation times of half-lines.
The results themselves. Donsker's theorem is the reason the arcsine law, the distribution of the maximum, and the occupation-time law are universal rather than artefacts of the simple random walk for which they were first computed. It is also the prototype for every later functional limit theorem — for martingales in Durrett's section 8.2, for stationary sequences in 8.3, for the empirical process converging to a Brownian bridge in 8.4.
Skorokhod's embedding deserves separate billing. It says any centred law with finite variance sits inside Brownian motion, which is what makes the path-space comparison possible at all, and it is the tool behind the law of the iterated logarithm in Durrett's section 8.5. The construction is a two-point mixture: write the law as a mixture of two-point laws with mean zero, use the exit time of for each, and the exit-time identity integrates to .
Formalizing them. Mathlib has the i.i.d. central limit theorem, convergence in distribution for
random elements of an arbitrary topological space (TendstoInDistribution, with the continuous
mapping theorem and Slutsky), Brownian motion as a process with its invariances, and the machinery
of stopping times for filtered spaces. It has no functional limit theorem of any kind, no Wiener
measure on , no Skorokhod embedding, and no continuous-time optional stopping. Nothing in
the library relates a random walk to a Brownian path.
The goal is the hardest item in this series, and the embedding route is the reason the mission is stated the way it is. Durrett's proof: with and stopping times realizing as , Lemma 8.1.9 says that if in probability for each , then in probability. The hypothesis is the weak law applied to the i.i.d. gaps of Theorem 8.1.2 after Brownian scaling; the conclusion plus the converging-together lemma gives the theorem. The work is uniform control of the Brownian path over shrinking time windows — the modulus of continuity — together with the bookkeeping of the polygonal interpolation.
Skorokhod's theorem needs the two exit-time facts for Brownian motion, Durrett's Theorems 7.5.3 and 7.5.5: takes the values and with probabilities and , and . Both come from optional stopping applied to and , and continuous-time optional stopping is itself not in the library. The mixture identity,
is elementary but needs Fubini and the two expressions for .
Theorem 8.1.5 is the Mann–Wald theorem in the form that allows a discontinuous : Mathlib's
TendstoInDistribution.continuous_comp handles genuinely continuous maps, and the extension to maps
continuous almost everywhere with respect to the limit law is the milestone. Given it, the two
examples are short — the maximum is continuous outright, and the occupation-time functional is
continuous at every path spending no time at the level , which Fubini shows is almost every
Brownian path.
is C(Set.Icc (0:ℝ) 1, ℝ), whose compact-open topology is the uniform one because the
domain is compact, with the Borel -algebra — Mathlib has no measurable-space instance on a
space of continuous maps, so the mission supplies it, and a BorelSpace instance with it.
The polygonal interpolation is written as a finite sum,
which agrees with at integer and is linear in between, and is manifestly continuous,
so walkPath is a genuine element of with no side condition. Both properties were proved
in Lean before publishing rather than assumed. Indexing is from zero, so .
The Brownian limit is brownianPath B, the restriction of the path to . Restriction is a
total function: it returns the zero path for a discontinuous argument. That junk branch is never
reached, because every statement assumes every path of is continuous, not merely almost
every one — one may always modify a Brownian motion on a null set to achieve this, and Durrett's
canonical construction on has it by definition. Without it there would be no
-valued random variable to speak of.
Weak convergence is Mathlib's TendstoInDistribution, the same predicate mission II used for the
Lindeberg–Feller theorem, instantiated at rather than at .
Skorokhod's theorem and the embedding of the walk are stated as existence of a probability space
carrying the Brownian motion, a filtration and the stopping times. This is how Durrett states them
— the construction needs an independent pair alongside the Brownian motion, and he notes
himself that is a stopping time only for the enlarged filtration. The filtration is
therefore an explicit family that is increasing, sits inside the ambient -field, and
contains — the pastSigma of mission V, which this mission imports as a
reference. The stopping-time property is {T ≤ t} ∈ F_t, stated directly rather than through a
bundled filtration structure.
Theorem 8.1.2's conclusion "" is read as equality of the laws of the whole processes: the push-forward of equals the law of the partial-sum process of an i.i.d. sequence with step law , taken on the infinite product measure. The gaps are required to be independent and identically distributed, as the book says.
The counting in Example 8.1.8 is a sum of indicators rather than a filtered cardinality, to keep a decidability side condition out of the statement, and the limit is the Lebesgue measure of as a real number. Example 8.1.6 takes the maximum over , which includes , and the limit is the supremum of over , attained because the path is continuous on a compact interval.
Existence of a Brownian motion is a hypothesis, not a claim, exactly as in mission V, except in Theorems 8.1.1 and 8.1.2 where the existence of a suitable space is the content of the statement and a Brownian motion must be produced; that is Durrett's Theorem 7.1.1, which the library does not yet have, so those two items subsume it.
Contributions welcome beyond the listed items: Lemma 8.1.9 on its own; Theorem 8.1.3, the CLT derived from the embedding; Example 8.1.7, the last zero before time and the arcsine law; continuous-time optional stopping and the exit identities 7.5.3 and 7.5.5 that Skorokhod's theorem rests on; the extension to ; and the martingale, stationary-sequence and empirical-process versions of sections 8.2 to 8.4.
Convex optimization — minimizing a convex function over a convex set — is the offline problem that online convex optimization (OCO) generalizes: an OCO algorithm run against a single, fixed cost function repeated every round is exactly an algorithm for this classical problem. Its convergence theory, developed over decades and surveyed comprehensively in Nesterov [Introductory Lectures on Convex Optimization, 2004] and Boyd and Vandenberghe [Convex Optimization, 2004], supplies the analytical toolkit — potential functions, strong convexity, smoothness — that every regret bound in the rest of this book reuses. This chapter is the book's own self-contained account of that toolkit: it proves nothing about regret or adversaries, but the algorithms and inequalities it establishes for gradient descent recur, essentially unchanged, in the online setting three chapters later.
The chapter's own capstone, a linear convergence rate under a joint strong-convexity and smoothness assumption, traces to Nesterov's classical analysis of gradient descent under a condition-number bound; the Polyak step size predates it, going back to Polyak's 1969 subgradient method for problems with a known optimal value.
Fix a real, complete inner product space (a Hilbert space) and a convex, closed set , the decision set. A function is -strongly convex (with gradient map ) if for every ,
and -smooth if for every ,
Strong convexity lower-bounds by a quadratic of curvature at least at every point; smoothness upper-bounds it by a quadratic of curvature at most . When is twice differentiable these say for every . A function that is both is called -well-conditioned, where is its condition number.
Write for a minimizer of (over , or over in the constrained case), and for any point define three measures of distance to optimality: the value gap , the Euclidean distance , and the gradient norm . Gradient descent starts at and iterates for a step-size schedule ; in the constrained case each step is followed by a projection back onto .
for constrained gradient descent (Algorithm 4) on a -well-conditioned over , with the constant step size . This is the chapter's strongest rate: for the best-conditioned class of functions it considers, the optimality gap shrinks by a constant factor every round, rather than polynomially in .
when minimizes over a convex . The multi-dimensional first-order optimality condition for constrained minimization, generalizing in the unconstrained case ().
for unconstrained gradient descent with step size , where achieves the smallest value among . A single algorithm, needing no prior knowledge of , , or beyond the (assumed available) optimal value , automatically attains whichever of the four rates applies to .
For -strongly-convex and -smooth , at every point :
The chapter's basic toolkit: four inequalities letting a proof substitute one measure of progress (value gap, distance, gradient norm) for another as needed.
Theorem 2.6 is the model result behind every subsequent linear-rate claim in convex optimization: it isolates the exact mechanism (strong convexity plus smoothness, combined multiplicatively through the condition number) that turns a or rate into an one. Theorem 2.3 demonstrates the opposite phenomenon — a single step-size rule that adapts to whatever structure happens to have, without needing to know which structure that is — a design principle the book's later chapters (adaptive regret, adaptive gradient methods) return to repeatedly. Lemma 2.4 is used directly inside the book's own proof of Theorem 2.6 and is stated separately because later chapters cite its four bounds individually.
None of these four statements has a machine-checked proof on the platform prior to this mission (see Formalization scope). Formalizing them establishes strong convexity and smoothness, in the book's own quadratic-bound form, as reusable definitions, together with the constrained- and unconstrained-gradient-descent update rules that Chapter III's online algorithm specializes.
The linear rate of Theorem 2.6 does not follow from Lemma 2.4 alone: chaining the smoothness upper bound and the strong-convexity lower bound gives only a bound relating to , not to itself, and a naive one-step decrease argument stalls at a rate of per round rather than — the factor of four comes from combining the projection's contraction property (the constrained analogue of Theorem 2.3's telescoping argument) with the smoothness bound simultaneously, not from either alone. The Polyak step size of Theorem 2.3 is remarkable, and its analysis correspondingly delicate, because the step size depends on the unknown optimal value through ; the proof must derive all four regimes (general convex, smooth, strongly convex, well-conditioned) of from the same one-line per-round inequality, rather than running four separate arguments.
is formalized as an arbitrary real, complete inner product space, not fixed to
, matching this book's chapter-wide convention (Chapter III's mission of this
series does the same). Strong convexity and smoothness are formalized in the book's own
quadratic-bound form with an explicit gradient map as a separate parameter (not tied to
by automatic differentiation), rather than via the second-derivative characterization; a
theorem needing to be the actual gradient of adds that as a separate hypothesis. This
avoids a trivializing formalization under which the predicate could be satisfied by an
unrelated : every theorem here that uses StronglyConvexOn/SmoothOn also assumes g is
a global gradient map for f. Theorem 2.3's realized-gradient bound is
formalized only over the run's own iterates (not as a global Lipschitz bound
on ), matching the book's own statement ("assuming "): a global
gradient bound would be jointly unsatisfiable with global strong convexity on any
infinite-dimensional or unbounded , since a strongly convex function's gradient grows
without bound away from its minimizer. Sequences are 0-indexed, so a book statement at round
(1-indexed) is stated here at index ; each theorem's docstring records the exact
shift. The projection in Algorithm 4 reuses OnlineConvexOpt.FirstOrder.IsMetricProjection,
already published for this series' Chapter III, rather than redeclaring it.
Theorem 2.10 (the chapter's further, book-stated-without-proof rate) is out of scope: the book explicitly defers its proof to outside references, so it cannot be a faithful milestone under this platform's provenance requirement. Section 2.4's reductions of non-smooth or non-strongly-convex problems to this chapter's setting (via randomized smoothing) are left for a future extension, since they introduce a new construction not needed by the goal or its milestones.
A Brownian path is continuous, and that is essentially all it is. It has no derivative anywhere, it crosses zero infinitely often in every interval , and it becomes positive and negative immediately after time zero. None of this is visible from the finite-dimensional distributions; it is a statement about the germ of the path at a point, and the tool that unlocks it is a zero-one law.
Chapter 7 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) develops that tool. The natural filtration is enlarged to , which allows "an infinitesimal peek at the future" — a quantity like is -measurable but not -measurable. Blumenthal's 0-1 law (Theorem 7.2.3) says that at this enlargement buys nothing probabilistically: the germ -field is trivial.
Everything local follows. If the path had any chance of staying non-positive on some interval , that would be a germ event of probability at least by symmetry, so it has probability one — and the path enters immediately. Continuity then forces it to return to zero immediately as well. Combined with the time inversion , which turns the germ at into the tail at , the same law gives and the recurrence of one-dimensional Brownian motion.
Let be a probability space and a Brownian motion: its finite-dimensional laws are centred Gaussian with covariance , and almost every path is continuous. In particular almost surely, so this is Durrett's .
Three -fields organize the chapter:
The first is the past, the second the germ at time zero, the third the tail at infinity.
A path is Lipschitz at the point with constant when for all within some positive distance of . A path differentiable at is Lipschitz at , so failing this at every point and for every constant is a strong form of nowhere differentiability.
In words: the germ -field is trivial. Nothing about the path in an arbitrarily short initial interval is genuinely random.
Theorem 7.1.5, that Brownian paths are Hölder continuous of every exponent on every bounded interval; Theorem 7.1.6, that with probability one they are not Lipschitz at any point, hence nowhere differentiable — the Paley–Wiener–Zygmund theorem in the proof of Dvoretsky, Erdős and Kakutani; Theorem 7.2.4, that the path enters immediately; Theorem 7.2.5, that its zero set accumulates at ; and Theorem 7.2.8, that and .
The results themselves. Blumenthal's law is the gateway to every local path property of Brownian motion, and Durrett uses it immediately for exactly that. Theorems 7.2.4 and 7.2.5 together say the path oscillates across zero infinitely often in every initial interval — the reason the zero set is an uncountable closed set of Lebesgue measure zero, and the reason the "first return to zero" is not a useful notion at time . Theorem 7.2.8 is the same law pushed to by time inversion, and it is what makes one-dimensional Brownian motion recurrent (Theorem 7.2.9).
The Hölder pair is the sharp description of path regularity. Exponent always works, never does, and the borderline is subtle: for each fixed , but Davis (1983) showed . Nowhere differentiability is the historical headline — Paley, Wiener and Zygmund (1933) — and the proof given here is a short covering argument rather than a series construction.
Formalizing them. Mathlib has the object but almost none of the theory. It defines
IsPreBrownianReal and IsBrownianReal, proves that a centred Gaussian process with covariance
is pre-Brownian, and supplies the invariances — negation, scaling
, the shift , and the time inversion
— together with the weak Markov property IsPreBrownianReal.indepFun_shift. It
does not have the germ or tail -fields, Blumenthal's law, the strong Markov property,
any path-regularity result, or the Kolmogorov–Chentsov continuity theorem: Probability/Process/Kolmogorov.lean
defines IsKolmogorovProcess, the hypothesis, and stops there. So this mission supplies the
-fields and then everything Durrett proves with them.
The goal reduces to Durrett's Theorem 7.2.2, that
for bounded path-measurable ; at , is trivial because
almost surely, so
almost surely, and an indicator almost surely equal to a constant forces that constant to be
or . Theorem 7.2.2 itself is a monotone class argument on top of the Markov property, and the
Markov property in this setting is Mathlib's indepFun_shift plus the observation that the
conditional expectation of a product over lands in
. Assembling that is the work.
Theorem 7.2.4 is then three lines — by symmetry of the Gaussian, let , apply the goal — provided the event has been shown to lie in the germ field, which is where continuity of paths enters. Theorem 7.2.5 follows from 7.2.4 applied to and together with the intermediate value theorem.
Theorem 7.1.5 needs the Kolmogorov–Chentsov continuity theorem, which has to be built: from
one gets Hölder- control for
, and gives every . The dyadic chaining and Borel–Cantelli
step is the substance, and it is worth building as a general theorem about
IsKolmogorovProcess rather than only for Brownian motion.
Theorem 7.1.6 is self-contained and short: fix , let be the event that some has whenever , and bound ; since increases, every .
Theorem 7.2.8 needs the tail 0-1 law, Theorem 7.2.7, which is the goal transported through the time
inversion — Mathlib's IsPreBrownianReal.inv — because the tail field of is the
germ field of . With that,
by scaling, so the probability is one, and is arbitrary.
The process is Mathlib's IsBrownianReal, indexed by ℝ≥0, on an abstract probability space —
not the canonical path space that Durrett uses. This is why the shift operators
and the family do not appear: there is one measure, the process starts
at almost surely, and each statement is about that process. Theorem 7.2.7 as Durrett states it
quantifies over all starting points and has no direct analogue here; the tail 0-1 law for the
process started at does, and is listed under contributions as the route to Theorem 7.2.8.
The three -fields are built as suprema and infima in the lattice of -algebras on
: pastSigma B t is the supremum of the pullbacks of the Borel field along for
, and germSigma B, tailSigma B are the corresponding infima. The goal carries the
hypothesis that each is measurable, not merely almost-everywhere measurable, which is what
IsPreBrownianReal gives and what puts these -fields below the ambient one; the canonical
construction satisfies it, and without it "" for a germ event would be an outer
measure.
Hölder continuity is stated locally — for almost every path, every admits a constant — since global Hölder continuity on is false. The order of quantifiers puts the null set first, so a single path works for every at once.
The hitting statements avoid an infimum over a possibly empty set. " almost surely" is
written as: almost surely, for every there is with ; and
" almost surely" as the same with . These are equivalent to Durrett's statements and
say what the infimum is there to say. Similarly Theorem 7.2.8 is written with ∃ᶠ … in atTop rather
than as an extended-real , which is what "" means and avoids a coercion.
LipschitzAtPoint f s C is "there is a scale on which ". Its
negation for every and every is Theorem 7.1.6, and it has content in both directions: the
identity path is Lipschitz at every point with , while is not Lipschitz at
with — both checked in Lean before publishing.
Existence is not part of this mission. Mathlib proves nothing of the form "a Brownian motion exists", and nothing here needs it: every item takes a Brownian motion as a hypothesis. That the hypothesis is satisfiable is a theorem — Durrett's 7.1.1, via Kolmogorov extension and the continuity theorem — and it is listed under contributions, where it belongs, since building it is a project of its own.
Contributions welcome beyond the listed items: Kolmogorov–Chentsov as a general statement about
IsKolmogorovProcess; Theorem 7.1.1, the existence of Brownian motion; Theorem 7.2.2 in full, for
every ; the tail 0-1 law and Theorem 7.2.9, recurrence; the strong Markov property and the
reflection principle of section 7.3; and Exercise 7.1.5, that no path is Hölder of any exponent
.
A Markov chain forgets. Run it long enough and the distribution of its position stops depending on where it started — that is the intuition behind shuffling a deck, behind Markov chain Monte Carlo, behind PageRank, and behind the stationary analyses of every queueing model. Chapter 5 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) makes it a theorem, and identifies exactly what can go wrong.
Two things can. The chain may fail to reach parts of the state space, and the answer is irreducibility. Or it may reach them only on a lattice of times — a chain alternating between two halves of its state space never forgets whether the clock is even or odd — and the answer is aperiodicity. Theorem 5.6.6 says that is the complete list: an irreducible, aperiodic chain with a stationary distribution has , for every pair of states, whatever the starting point.
Let be a countable state space and a transition probability: non-negative, with each row summing to one. The -step transition probabilities are the matrix powers, and .
Hitting is described by the first-passage probabilities , given by and — the chain moves once and then reaches for the first time, having avoided it meanwhile. Summing them gives
A state is recurrent when , the chain is irreducible when for all , and a state is aperiodic when the greatest common divisor of is . A stationary distribution is a probability vector with .
The goal asserts pointwise convergence of the transition probabilities, not convergence in total variation and not a rate; those are strengthenings, and stating the weakest useful form is what keeps the theorem stable.
Theorem 5.3.1, that a state is recurrent exactly when diverges — the bridge between the hitting picture and the matrix picture; Theorem 5.3.2, that recurrence is contagious; Theorem 5.5.10, that every state in the support of a stationary distribution is recurrent; and Theorem 5.5.11, that for an irreducible chain with a stationary distribution .
The result itself. Theorem 5.6.6 is what licenses reading a stationary distribution as a long-run frequency. Without it, is merely a fixed point of a linear map; with it, is the limiting probability of being at , from any start. Theorem 5.5.11 then gives the quantity a second, purely local meaning — is the reciprocal of the mean return time to — which is the identity behind every renewal-reward computation in applied probability and behind the "expected time between visits" estimates that Monte Carlo methods rely on. The two necessary hypotheses are sharp: a periodic chain has oscillating rather than converging, and Durrett's Theorem 5.7.2 gives the corrected statement in that case.
Formalizing it. Mathlib has no countable-state Markov chain theory. It has ProbabilityTheory.Kernel
and an Irreducible notion for kernels, but nothing about recurrence, transience, first-passage
decompositions, stationary measures or the convergence theorem, and nothing that specializes to a
transition matrix on a countable set. The mission therefore contributes the whole apparatus of
sections 5.3, 5.5 and 5.6 — the -step and first-passage probabilities, , the mean
return time, recurrence, irreducibility, aperiodicity and stationarity — together with the results
that make it usable.
The usual proof of the goal is a coupling argument, and it is short but not obvious: run two independent copies of the chain, one from and one from , on the product space with transition probability ; aperiodicity plus irreducibility make the product chain irreducible, is stationary for it, so it is recurrent and the two copies meet almost surely; after they meet they can be exchanged. Each step of that is a separate obligation, and the one that consumes aperiodicity is the irreducibility of the product chain — for a periodic chain it fails, which is exactly why the theorem does.
The number-theoretic ingredient is worth flagging: irreducibility of the product needs that , being closed under addition with , contains every sufficiently large integer. That is the numerical semigroup fact, and it is where aperiodicity is actually used.
The state space is any countable type with decidable equality, and the transition probability is a
plain function constrained by IsTransition: non-negative entries,
summable rows, rows summing to one. Sums over the state space are unconditional sums, so no
finiteness is assumed anywhere.
The chain's law is not constructed. Every quantity here — , , , — is defined by an explicit recursion on the transition matrix, not as an expectation against a measure on path space. This is a deliberate choice: building the path measure is a substantial project of its own, and none of the statements in these sections need it. The recursions are the standard ones and they are the definitions the book's own computations use. The cost is that probabilistic statements about paths, such as Theorem 5.6.1 on the almost-sure limit of the visit counts , cannot be phrased in this language and are not part of the mission.
Conventions: is the identity matrix; vanishes at ; and are unconditional sums over , so an infinite mean return time appears as a non-summable series rather than as an extended real. Theorem 5.5.11 is therefore stated as summability together with , which asserts finiteness of the mean return time rather than silently relying on a division convention.
Aperiodicity is "the only natural number dividing every element of is ", which is written without needing a gcd of a set; it is false when is empty, which is correct, since the period of such a state is undefined.
The goal is not vacuous: the hypotheses are satisfiable by any strictly positive transition matrix on a finite set.
Contributions welcome beyond the listed items: Theorem 5.3.3 on finite closed sets; the decomposition theorem 5.3.5; existence of a stationary measure from a recurrent state (5.5.7) and its uniqueness (5.5.9); the equivalence of positive recurrence and the existence of a stationary distribution (5.5.12); Theorem 5.7.2 for the periodic case; and the path-level results of section 5.6, which need the chain's law on path space.
Chapter 7 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) studies a network with a fixed set of users, and shows that a decentralized rate control converges to a fair allocation. Chapter 8 asks the question one time scale up. Files finish and their flows leave; new files arrive and new flows appear. The number of flows on each route is therefore itself a random process, and the rate allocation — assumed to settle instantly, since rate control runs much faster than files arrive and depart — depends on it.
The question is whether this system is stable: does the number of flows in progress stay bounded, or does it grow without limit? The answer is the best one could hope for. A weighted -fair allocation, the family that contains proportional fairness, TCP fairness, max-min fairness and throughput maximization as special cases, is stable exactly when the offered load at each resource is below that resource's capacity. No more is required — no condition coupling different resources, no dependence on , no dependence on the topology beyond the loads themselves.
A network has resources and routes with incidence matrix . Let be the number of flows active on route and the rate given to each of them, so route consumes at each resource it uses. Flows arrive on route as a Poisson process of rate and carry files that are exponentially distributed with parameter , so
and is the load on route .
Given weights and , the weighted -fair allocation is the solution of
with in place of the objective when . Written in the aggregate rates this becomes
The family interpolates between the fairness notions of Chapter 7: with maximizes throughput, is weighted proportional fairness, with is TCP fairness, and with approaches max-min fairness.
Suppose the load respects every capacity, for all . Then there is an , depending only on the loads and capacities, such that for every flow count and the -fair aggregate rates ,
The left-hand side is the drift of the Lyapunov function , by the identity (8.3); the right-hand side is the book's displayed bound. The single is uniform in , which is what a Foster–Lyapunov argument needs, and it is the whole deterministic content of Theorem 8.2's sufficiency half.
The derivative of the objective, in the same form for every including (Exercise 8.3); strict concavity of the objective; the characterization of the optimum by with primal and dual feasibility and complementary slackness (Exercise 8.4); the tangent-plane inequality (8.5) that concavity gives at the optimum; the drift identity (8.3); and that recovers weighted proportional fairness, connecting this chapter to Proposition 7.4 of mission VII.
The result itself. Theorem 8.2 says the stability region of an -fair network is the largest it could possibly be — the same region a single isolated resource would have — and that it does not shrink as varies. That is a strong statement about a large design space, and it is not automatic: section 8.4 of the book exhibits rate allocation schemes for which it fails, so the natural condition (8.2) is a property of -fairness and not of rate allocation in general. Since the family covers the fairness notions actually implemented in transport protocols, the theorem is what licenses treating "is the load below capacity?" as the only capacity-planning question at flow level.
Formalizing it. Nothing here is open; the theorem is due to Bonald and Massoulié (2001), with
the fluid-limit machinery from Gromoll and Williams and from Massoulié. What the mission produces
is a machine-checked -fair allocation — objective, derivative, concavity, KKT conditions —
and the exact drift inequality, on top of the congestion-control layer published in mission VII of
this series, whose networkFeasible and linkFlow it reuses. Mathlib has no network utility
maximization and no fairness criteria.
The proof is short but the step that makes it work is easy to miss. The drift is , and there is no reason for this to be negative term by term — some routes are over-served and some under-served. What makes the sum negative is that is itself a feasible point of the same optimization problem (8.4) that solves, and is concave, so the tangent plane at lies above :
Since , taking gives the drift immediately. Strict negativity comes from taking instead, which is still feasible because (8.2) is a strict inequality, and then dividing through by . The whole argument is one application of concavity at a cleverly chosen point, and the choice of that point is the content.
The scaling that makes it uniform in is the other thing to notice: depends only on how much slack (8.2) leaves, not on , because enters only through the common factor that appears on both sides.
Resources and routes are indexed by finite types, the incidence matrix is real-valued with entries
or , and the feasible set is mission VII's networkFeasible, so Chapters 7 and 8 agree on
what a feasible flow vector is. The objective is stated in the aggregate variables of
problem (8.4) rather than the per-flow rates of (8.1): they are equivalent, but (8.4) is the form
the drift argument uses and the form in which the feasible set does not depend on .
The objective is defined with an explicit case split at , exactly as the book defines it, and the derivative milestone asserts that the resulting derivative has the same form in both cases — which is the point of Exercise 8.3. Powers are real exponents, so positivity of the flow counts, weights, loads and rates is hypothesised wherever a power appears.
What is formalized and what is quoted. Theorem 8.2 is a statement about positive recurrence of a Markov process, proved by a Foster–Lyapunov criterion whose remaining hypotheses the book leaves to Exercises 8.6 and D.2. There is no theory of continuous-time Markov chains on a countable state space in Mathlib to state positive recurrence against, so this mission formalizes the deterministic drift inequality that carries the argument and quotes the probabilistic wrapper. The inequality is exactly the one the book displays, including the , and the necessity half — that the process is unstable when (8.2) fails — is a coupling argument and is quoted too.
The goal is not vacuous: the hypotheses are satisfiable, and for a single resource of capacity the -fair optimum is , for which the inequality holds with and strictly positive slack.
Contributions welcome beyond the listed items: the single-resource equilibrium distribution of Exercise 8.1 and the geometric law of the total number of flows; the bounded-drift estimate of Exercise 8.6; the necessity half of Theorem 8.2; the limiting cases and ; and the instability examples of section 8.4.
When a file is transferred over the Internet, no part of the network decides how fast it should go. The machines inside the network forward packets; when a resource is heavily loaded it drops or marks one; the destination reports that to the source; and the source slows down, then gradually speeds up again until the next signal. This end-to-end cycle of increase and decrease is TCP, and it is the mechanism by which the Internet discovers available capacity and divides it among competing flows.
Chapter 7 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) asks what such a scheme converges to. The answer is the chapter's organizing idea: the decentralized dynamics solve a global optimization problem that no participant can see. Each source knows only its own rate and the congestion signals it receives; no machine anywhere holds the link-route incidence matrix; and yet the flow rates converge to the unique maximizer of a concave network utility, and that maximizer is the proportionally fair allocation. This is the same phenomenon as the electrical network of Chapter 4, now with the local rule chosen so that the global objective is the one we want.
A network has resources and routes, with link-route incidence matrix : when route uses resource . Route carries a time-varying flow rate , and the load on resource is .
Each resource generates congestion signals at rate
where is non-negative, continuous, increasing and not identically zero — one may read as the probability that a packet is dropped or marked at resource under load . The primal algorithm is the response of the sources:
with : a steady increase proportional to the weight , and a decrease proportional to the stream of congestion signals received. Both sums are local — over the resources on route , and over the routes through resource — so nothing in the network needs to know .
The network problem of section 7.1 is to maximize over with , and a feasible is weighted proportionally fair when every feasible satisfies .
is a Lyapunov function for (7.5): the unique maximizer of over the positive orthant is an equilibrium point, and every trajectory of the primal algorithm converges to it.
The goal asserts both halves of the book's last sentence: that maximizes , and that the trajectory converges to it. It fixes no rate of convergence and no basin restriction beyond starting in the interior, which is what "global" means here.
Proposition 7.4, that solving and being weighted proportionally fair are the same condition; strict concavity of on the positive orthant; the partial derivative that identifies the maximizer; the equivalence between a stationary point of and an equilibrium of (7.5); and the Lyapunov identity (7.7),
The result itself. Theorem 7.6 is the statement that a decentralized rule solves a centralized problem. Its practical content is that the choice of and determines what is optimized, so a protocol designer who wants a particular notion of fairness can get it by choosing the local rule accordingly — the -fair family of Chapter 8 is exactly this dial. Its theoretical content is the identification of the limit: because 's first term is , the limit is the weighted proportionally fair allocation, which by Proposition 7.4 is the solution of the network problem and, by Remark 7.5, also the Nash bargaining solution and a market-clearing equilibrium. Three quite different notions of "the right allocation" coincide, and a simple end-to-end feedback rule finds it.
Formalizing it. Nothing here is open; the model and the theorem are from Kelly, Maulloo and Tan (1998). What the mission produces is a machine-checked congestion-control model — the network problem, proportional fairness, the primal dynamics and the Lyapunov function — and a statement of the convergence result in a form later work can cite. Mathlib has no network utility maximization and no congestion control.
The Lyapunov identity is a chain-rule computation and is not the hard part, and neither is . The gap the book flags explicitly is between " increases along trajectories" and "": a strictly increasing Lyapunov function does not by itself force convergence, because the derivative could decay fast enough for the system to stall short of the maximum. The book closes it with a compactness argument — the trajectory is trapped in , which is compact, and on the complement of an -ball around within that set the derivative (7.7) is continuous and therefore bounded away from zero, so only finite time can be spent there. Reproducing that argument is the substance of the goal, and it needs the compactness of the sublevel set, which comes from strict concavity and the growth of .
A second difficulty is one of representation rather than mathematics. The primal algorithm is an ODE, and a formal statement must say what a trajectory is. Here a trajectory is given as a differentiable function satisfying (7.5) pointwise, with positivity assumed rather than derived; deriving positivity from the dynamics is a separate (true, and welcome) result.
Resources and routes are indexed by finite types and the incidence matrix is real-valued with
entries constrained to or , matching the book and the convention of mission IV of this
series, whose linkFlow is reused here. Flow vectors live in the positive orthant, stated as
∀ r, 0 < x r: the utility contains , which has no meaning at , and the book's
own maximum is interior to the positive orthant.
The network problem's objective is maximized over the intersection of the feasible set with the positive orthant rather than over , since is not a real number; the fairness condition, by contrast, is quantified over all feasible including boundary points, exactly as the book states it, and the inequality is meaningful there.
A trajectory is a function of real time satisfying the derivative condition at each , and staying in the positive orthant is a hypothesis. The equilibrium is given by its stationarity condition rather than by an existence claim, so the goal is about the trajectory rather than about solving the fixed-point equation; that the stationary point is the maximizer is the first conjunct of the conclusion, so nothing is assumed about it that is not also proved.
The goal cannot be satisfied vacuously: the hypotheses are jointly satisfiable — for instance one resource, one route, , , — and the conclusion is a genuine limit.
Contributions welcome beyond the listed items: that the positive orthant is invariant under (7.5); uniqueness and existence of the max-min fair allocation; Theorem 7.2 on problem decomposition into user and network problems; Theorem 7.8, the corresponding global stability result for the TCP-like system of section 7.4; and the dual algorithm of section 7.6.
When many stations share one broadcast channel, something has to decide who transmits. A token passed around the stations works when there are few of them and none is silent for long, but it scales badly and breaks if the token is lost. The alternative is to let stations transmit whenever they like and use randomness to recover from the resulting collisions. That is the design of ALOHA, built in the 1970s to connect terminals across the Hawaiian islands, and of Ethernet, and of essentially every contention-based access protocol since.
Chapter 5 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) asks what such protocols can achieve, and the answers are largely negative. ALOHA with a fixed retransmission probability jams: with probability one there is a finite random time after which every slot contains a collision and no packet ever succeeds again, for every positive arrival rate. Ethernet's binary exponential backoff does better, but only just: it has a positive critical arrival rate, above which only finitely many packets are ever transmitted, and it is still not positive recurrent at rates where it does transmit infinitely many. The chapter's general statement is the one this mission targets: any backoff slower than exponential jams at every positive arrival rate.
Time is slotted, and a transmission attempt occupies exactly one slot. New packets arrive in a Poisson stream of rate , so the number arriving in a slot is Poisson with mean . A slot in which exactly one station transmits carries its packet successfully; a slot in which two or more transmit is a collision and carries nothing.
In an acknowledgement-based scheme a station learns nothing about the channel except whether its own transmissions succeeded. A packet arriving in slot attempts transmission in slots with , the sequence chosen independently for each packet, and
is the retransmission function. For ALOHA, for every ; for Ethernet's binary exponential backoff, .
Now imagine the channel externally jammed from time , so that every retransmission actually occurs. The attempts in slot are then Poisson with mean , and the probability that fewer than two attempts are made in slot is
The expected number of such slots is , which is decreasing in , and the critical rate is
Theorem 5.11 of the book says deserves its name: below it infinitely many packets are transmitted with probability one, above it only finitely many.
Since for every positive , the critical rate is , and by Theorem 5.11 the expected number of successful transmissions is finite at every positive arrival rate. The goal fixes no constant and no rate: it says only that the dividing line between "jams always" and "has a positive capacity" sits at logarithmic growth of , which is exponential growth of the backoff.
The ALOHA drift calculation of section 5.1 and its consequence that the drift is positive once the backlog is large enough; the summability that combines with Borel–Cantelli to give Proposition 5.3; the monotonicity of in ; the opposite extreme, that a scheme with — one that gives up on a packet after finitely many attempts — has ; that ALOHA's own retransmission function satisfies condition (5.7); and the bound of Remark 5.14, that a positive recurrent acknowledgement-based scheme needs and hence , which is strictly below Ethernet's .
The result itself. Condition (5.7) is the chapter's structural statement about random access, and it is a sharp one. Any retransmission rule under which a packet keeps trying at a rate that does not decay fast enough — a fixed probability, a polynomially growing backoff, anything short of exponential — has critical rate zero: the channel jams at every positive load. Exponential backoff is not a tuning choice, it is the minimum that makes the protocol work at all, and the formula for a backoff by factor (Exercise 5.7) then says how much capacity each choice of buys. The gap recorded in Remark 5.14 is the other half of the picture: even above the threshold, "infinitely many packets get through" is much weaker than "the backlog is stable", and between and Ethernet does the first and provably not the second.
Formalizing it. None of this is open; the analysis is due to Kelly and MacPhee (1987) and Aldous (1987). What the mission contributes is a machine-checked account of the analytic core: the definitions of , and , the two extremes of the classification, and the ALOHA calculations. Mathlib has no protocol analysis and nothing about random access channels.
The obstacle is a modelling one and it is worth stating plainly rather than discovering halfway through. The chapter's headline results — Proposition 5.3 that ALOHA jams almost surely, Theorem 5.11 that is the critical rate, Theorem 5.15 that geometric Ethernet is transient — are statements about sample paths of a Markov chain built on a Poisson arrival stream, and their proofs are coupling arguments comparing a system started empty with one started with a backlog. Nothing in Mathlib supports that construction, and building it is a research-scale project rather than a chapter. This mission therefore formalizes the analytic half and quotes the probabilistic half, which is the same division the book itself makes when it computes for a scheme: Theorem 5.11 is proved once, and every subsequent statement about a protocol is a convergence question about .
Within that analytic half the difficulty is real but ordinary. The summand is a product of a factor growing with and one decaying exponentially in it, so the growth hypothesis has to be turned into a summable bound without assuming any regularity of beyond non-negativity — in particular need not be eventually monotone in any useful quantitative sense, only divergent faster than .
The retransmission function is any non-negative real sequence; the normalization is not imposed, since none of the statements need it and imposing it would exclude the comparison schemes. and the partial sums are real-valued, and "" is stated as summability of the sequence rather than as a bound on an extended-real sum, so convergence is asserted rather than assumed. The goal is stated for each fixed separately, which is what makes ; it is not stated as a claim about the infimum, because the infimum of the set adds nothing once the set is known to be all of .
The growth hypothesis is the book's condition (5.7) verbatim: . Note that at and the quotient involves and is not meaningful; divergence to infinity is an eventual statement, so this costs nothing, but it is why the hypothesis is a limit rather than a pointwise bound.
The mission is not vacuous in either direction: the ALOHA milestone exhibits a retransmission function satisfying the hypothesis, and the milestone exhibits one that fails it as strongly as possible, with for every .
Contributions welcome beyond the listed items: Ethernet's and the resulting ; the generalization of Exercise 5.7; the scheme with ; the continuous-time halving of Kelly and MacPhee; and, for anyone willing to build the probabilistic layer, Proposition 5.3 and Theorem 5.11 themselves.
In the early twentieth century Agner Krarup Erlang worked for the Copenhagen Telephone Company and faced a sizing question that every shared-resource operator still faces: how many parallel circuits must a telephone link carry so that an arriving call is almost never turned away? The answer he published — the Erlang loss formula — is still the standard dimensioning tool for circuit-switched links, call centres, hospital beds, rental fleets, and any system in which a customer who finds every server occupied leaves rather than waits.
The formula is the first capstone of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014), where it closes Chapter 1 and supplies the building block for the loss networks of Chapter 3. It is also the cleanest possible demonstration of the book's method: write down the transition rates of a Markov process, guess that the process is reversible, solve the detailed balance equations, and read the answer off the normalizing constant. This mission formalizes that chapter: the reversibility apparatus, the birth-and-death chain of the loss link, and Erlang's formula itself.
A link carries parallel circuits. Calls arrive as a Poisson process of rate and each call, while it lasts, occupies one circuit for an exponentially distributed holding time of parameter ; holding times are independent of one another and of the arrival times. A call that arrives to find all circuits busy is lost — it does not queue.
Let be the number of busy circuits. Then is a Markov process with transition rates
and otherwise. A collection of numbers is in detailed balance with rates when
and satisfies the equilibrium (full balance) equations when
Detailed balance is the statement that, in equilibrium, transitions from to occur as frequently as transitions from to . Writing for the traffic intensity, Erlang's formula is
The goal fixes no numerical constant: it says that whatever probability vector solves the detailed balance equations of the loss link assigns exactly to the blocking state. The hypothesis is detailed balance rather than full balance, which is what the book's derivation actually uses and is the stronger assumption to discharge.
together with the reversibility results that justify the method: detailed balance implies full balance, the reversed process of Proposition 1.1 has rates and retains as an equilibrium distribution, and holds exactly when and are in detailed balance.
The result itself. is the blocking probability of the link, so it converts a traffic measurement and a target grade of service into a circuit count. It is insensitive: the same formula holds for any holding-time distribution with mean , which is why it survives as an engineering tool far outside the exponential model that produces it here. Chapter 3 of the book builds loss networks on top of it, and the Erlang fixed point that approximates a whole network is a system of coupled copies of this one formula. The derivative identity is the ingredient that makes tractable in optimization: it shows is increasing in , and the recursion it encodes is how the formula is evaluated numerically without overflow.
Formalizing it. Nothing here is open mathematics; the value of the mission is a
machine-checked statement of the loss model and a reusable reversibility layer. Mathlib has no
theory of detailed balance or of reversible Markov processes over a countable state space, so
this mission contributes the first: the predicates DetailedBalance and FullBalance, the
reversed rate matrix, and the three structural facts relating them. Those are shared by every
later mission in this series — the migration processes of Chapter 2 and the loss networks of
Chapter 3 are all proved reversible or quasi-reversible by exactly these means.
The obvious route to is to solve the equilibrium equations directly, and for a
birth-and-death chain that is a three-term recursion whose general solution needs two boundary
conditions. Detailed balance replaces it with a two-term recursion and one boundary condition,
and the whole content of the reversibility section is that the substitution is legitimate.
The remaining work is bookkeeping that Lean makes less forgiving than the page does: the
detailed balance equations must be indexed so that the and boundaries are not
silently assumed away, the normalizing sum must be shown positive before it can be inverted,
and the induction that produces has to carry the Fin (C+1) index through
Nat.factorial. For the derivative identity, the naive differentiation of a quotient gives
in the numerator, and recognizing it as
times the denominator is the step that produces the stated form.
The state space is Fin (C + 1), so the link with circuits has states and finiteness
is built in; is a plain function Fin (C + 1) → ℝ constrained by hypotheses rather than a
PMF, so that the normalization appears explicitly wherever it is used.
FullBalance is written with unconditional sums (tsum) over an arbitrary state space, so the
same predicate serves the countable chains of later chapters; over a Fintype it is the finite
sum. Rates are real-valued and q j j = 0 by construction, matching the book's convention that
a Markov process must change state when it jumps.
The rates carry as hypotheses. This rules out the degenerate reading in which
makes every downward rate vanish: with the detailed balance equations force
for , so the only normalized solution is the point mass at , and
while Lean evaluates for ; the goal would be false.
Erlang's formula is stated for the last state Fin.last C, not for an unconstrained index, so
it cannot be satisfied by a degenerate reindexing.
Contributions welcome beyond the listed items: the insensitivity of to the holding time distribution, the recursion , the finite-source variant and the PASTA statement that an arriving call in that model sees , and the parking-space identity of Exercise 1.9.
The central limit theorem tells us that a normalized sum of independent random variables converges in distribution to a Gaussian. For applications — bounding the failure probability of a randomized algorithm, controlling the error of a Monte Carlo estimator, proving a generalization bound in learning theory — a limiting distribution is not enough: what is needed is a single, explicit, non-asymptotic inequality that holds for every fixed sample size , not merely as . Hoeffding's inequality (Wassily Hoeffding, 1963) and Bernstein's inequality (Sergei Bernstein, 1920s–1940s, in the form used here due to Vadim Bennett and later authors) are the two archetypal answers: both give an explicit Gaussian-type tail bound for a weighted sum of independent random variables, valid for every , with all constants made explicit. They are the workhorses behind concentration of measure, high-dimensional statistics, and the non-asymptotic analysis of randomized algorithms; a textbook trying to reach the Johnson–Lindenstrauss lemma, random matrix norms, or the restricted isometry property has to pass through this chapter first, because every one of those results is itself an application of a weighted-sum concentration inequality to a specific choice of random variables.
The central limit theorem's own error term is the obstruction that direct concentration inequalities are built to avoid: the Berry–Esseen theorem (Andrew C. Berry, 1941; Carl-Gustav Esseen, 1942) bounds the normal approximation's error at order , which is too slow to recover a genuinely exponential tail bound for finite . Hoeffding's and Bernstein's inequalities are proved instead by a direct argument — bounding the moment generating function of the sum and optimizing a Markov/Chernoff exponential tilt — that never invokes the central limit theorem or its error term at all.
Fix a probability space . For a real random variable on , define its sub-gaussian norm
and its sub-exponential norm
In both definitions, the requirement that the exponential moment be finite (i.e. that the moment-generating integrand be integrable), and not merely satisfy "" as a bare inequality, is essential: without it a moment that is genuinely infinite for a given would vacuously count as "" under the Bochner integral's convention that a non-integrable function integrates to , and every random variable — however heavy-tailed — would trivially have norm . is called sub-gaussian (respectively sub-exponential) when this infimum is over a nonempty set, i.e. when some finite makes the moment finite and at most . These are genuine norms (up to the identification of almost-surely-equal random variables) on the vector space of random variables for which they are finite, and they are the natural non-asymptotic yardsticks for tail heaviness: characterizes a Gaussian-type tail , while characterizes an exponential-type tail . Every bounded random variable — in particular every Bernoulli or Rademacher (symmetric Bernoulli) random variable — is sub-gaussian, and the square of a sub-gaussian random variable is sub-exponential; a genuinely sub-exponential (not sub-gaussian) example is the squared coordinate of a standard Gaussian vector, or the exponential distribution itself.
Goal — Theorem 2.8.2 (Bernstein's inequality, weighted sum). Let be independent, mean-zero, sub-exponential random variables on , and let . Then, for every ,
where and is an absolute constant that does not depend on , the , , or .
The goal is deliberately the weighted and sub-exponential form, the weakest of the chapter's results that is still stable under the improvements a solver might find: it neither fixes (the unweighted Theorem 2.8.1, a special case) nor restricts to the lighter sub-gaussian tail (Theorem 2.6.3, which follows from a strictly stronger hypothesis). Both weaker theorems, plus Hoeffding's and Chernoff's inequalities, are included as milestones because Bernstein's own proof is built directly from them.
The result itself. Bernstein's inequality is the two-tail-regime concentration bound: a sub-gaussian tail near the mean, transitioning to a heavier sub-exponential tail far from it, exactly the behavior one should expect from a mixture of light-tailed terms with one heavy-tailed outlier. It underlies the concentration of quadratic forms (Chapter 6's Hanson–Wright inequality controls -type terms, which are themselves products of sub-gaussians and hence sub-exponential by Lemma 2.7.7), and it is the standard tool for bounding empirical-process suprema whose summands are not bounded but merely light-tailed.
Formalizing it. No formalization of Bernstein's inequality — in either the weighted or
unweighted, or sub-gaussian or sub-exponential form — exists yet on Prove2Me (GET /theorems?q=Bernstein and q=sub-exponential return no relevant hits, checked
2026-09-17). What this mission produces is not just the statement but the machinery
underneath it: a working Orlicz-norm treatment of and that a later mission
(the Hanson–Wright inequality, or any future chapter that needs sub-exponential
concentration) can build on directly.
The obvious first idea — squaring both sides and applying Chebyshev, as one does to prove the weak law of large numbers — gives only a polynomial tail bound decaying like , far too weak to be useful (this is exactly the point made by the chapter's opening discussion of the coin-tossing example, comparing the linear decay from Chebyshev against the target exponential decay). The central limit theorem promises the right shape of tail asymptotically but, per Berry–Esseen, with an error of order that swamps any exponential gain for large deviations — the CLT approximation is simply not valid in the tail regime the inequality needs. The actual argument instead controls the moment generating function of the full sum directly and optimizes an exponential (Chernoff) tilt; this is why the sub-gaussian and sub-exponential norms — MGF-control objects, not moment or tail objects per se — are the right technical vehicle, even though Proposition 2.5.2 and 2.7.1 show all these characterizations are equivalent up to constants. The min of two terms in Bernstein's exponent is not an artifact of a loose proof: it reflects a genuinely two-regime tail (Gaussian near the mean, exponential in the far tail), and collapsing it to a single term in either direction would either be false (dropping the exponential term) or needlessly weak (dropping the Gaussian term, which is what a naive union bound over the worst single term would give).
Random variables are ℝ-valued functions on an explicit probability space (Ω, mΩ, P)
(Ω : Type, MeasurableSpace Ω, P : Measure Ω, [IsProbabilityMeasure P]), matching the
book's setup throughout. Independence is Mathlib's ProbabilityTheory.iIndepFun, and
tail probabilities are stated with P.real, Mathlib's ℝ-valued measure evaluation, which
corresponds directly to the book's .
Both Orlicz norms are defined locally, as genuine infima matching Definitions 2.5.6 and
2.7.5 verbatim (subgaussianNorm, subexponentialNorm, each
sInf {t > 0 : Integrable (fun ω => E[...]) P ∧ E[...] ≤ 2}), rather than reused from
Mathlib's HasSubgaussianMGF (Mathlib.Probability.Moments.SubGaussian). The Integrable
conjunct is not optional dressing: Mathlib's Bochner integral of a non-integrable function is
0 by convention, so a bare E[...] ≤ 2 (without asserting integrability) would be satisfied
by every t for which the moment is actually infinite, collapsing the sub-gaussian norm of
a standard Gaussian (and, symmetrically, the sub-exponential norm of any heavy-tailed
variable) to 0 — a trivializing formalization the mission was moderated to rule out. The
same Integrable conjunct appears in every moment hypothesis (general_hoeffding,
bernstein_unweighted, bernstein_weighted): ∃ s > 0, Integrable (...) P ∧ ∫ ... ≤ 2, so
that the hypothesis is not satisfied vacuously by non-integrable exponential moments either.
HasSubgaussianMGF bounds the moment generating function directly with a variance-proxy
parameter (E exp(tX) ≤ exp(c t²/2)), which is a different object definitionally
from the Orlicz norm — equivalent up to a constant factor by the book's own
Proposition 2.5.2, but not interchangeable without restating that equivalence — and
Mathlib has no sub-exponential analogue at all. Since the goal theorem and two of its
milestones need the sub-exponential norm, one consistent convention (the book's own Orlicz
norms) is used for both and throughout the mission, rather than mixing
Mathlib's MGF-based sub-gaussian convention with a locally defined sub-exponential one.
Every occurrence of the book's " is an absolute constant" is formalized as a genuine
existential quantifier fixed before the random variables, the vector a, and t are
introduced: ∃ c : ℝ, 0 < c ∧ ∀ ..., P.real {...} ≤ 2 * Real.exp (-(c * ...)). No numeral is
substituted for c anywhere; a solver's proof may use any positive constant it can establish,
exactly mirroring the book's own non-constructive existence claims. The trivializing
formalization this rules out is fixing c to a specific small numeral (which would be a
strictly stronger, easier, and unfaithful claim) or, in the other direction, weakening the
statement by allowing c to depend on N, the , a, or t (which would make the
theorem vacuous, since any such bound trivially holds for a small enough depending on the
instance).
Chernoff's inequality (Theorem 2.3.1) needs no Orlicz norm — Bernoulli parameters are
given directly via P.real {X i = 1} = p i ∧ P.real {X i = 0} = 1 - p i, and the conclusion
uses Real.rpow (^ on ℝ → ℝ → ℝ) for the real exponent in . Hoeffding's
inequality for symmetric Bernoulli variables (Theorem 2.2.2) is likewise self-contained,
needing only the two-point probability hypothesis defining the Rademacher distribution.
Many arguments in high-dimensional geometry, statistics and computer science need to approximate a point of a convex set by an average of a handful of extreme points, rather than represent it exactly. The classical Carathéodory theorem (1907) answers the exact question: every point of the convex hull of a set is a convex combination of at most points of . That bound is tight and grows with the dimension , which makes it useless whenever is large — exactly the regime of interest in high-dimensional probability.
B. Maurey's empirical method — an unpublished 1980–81 result reported by G. Pisier, "Remarques sur un résultat non publié de B. Maurey," Séminaire d'Analyse Fonctionnelle 1980–1981 — and later applied by B. Carl to bound covering numbers of operators between Banach spaces (Inequalities of Bernstein-Jackson-type and the degree of compactness of operators in Banach spaces, Ann. Inst. Fourier 35(3), 1985, 79–118), replaces the exact question with an approximate one and removes the dimension dependence entirely: to approximate to accuracy , the number of points needed depends only on , never on . Vershynin's High-Dimensional Probability opens with this result as its "Appetizer," using it to illustrate the book's central theme — that randomness is a tool for constructing deterministic combinatorial objects — before any probabilistic machinery has been introduced.
A convex combination of finitely many points is a sum with and . The convex hull of a set is the set of all convex combinations of all finite collections of points of . The diameter of is , the Euclidean norm throughout.
The classical Carathéodory theorem states that every is a convex combination of at most points of — with generally unavoidable, attained by a simplex. The question this mission answers is different: given that we are willing to approximate rather than represent it exactly, and willing to use only combinations with equal coefficients (an average of points, with repetition allowed), how large must be as a function of the desired accuracy?
The quantifiers are exactly this order: for every bounded , every point of its convex hull, and every target , such an averaging set exists. This is the weakest stable statement carrying the theorem's content — the number of points does not depend on the dimension , and the coefficients are forced to be uniform — and it is the form the corollary below invokes directly.
This is a direct application of the goal to computational geometry's covering problem: how many balls of radius are needed to cover a polytope, and where should they be centered.
The result itself. The approximate Carathéodory theorem is the prototype of a dimension-free approximation result: whenever a set is bounded, a fixed number of points (depending only on the target accuracy, not the ambient dimension) suffices to approximate any point of its convex hull. This is what makes possible dimension-independent covering-number bounds such as Corollary 0.0.4, which in turn are the starting point for the book's later treatment of entropy, packing and generic chaining (Chapters 4, 7–8). The technique generalizes far beyond : it underlies covering-number bounds for operators between Banach spaces (Carl's original application) and is a recurring device in learning theory for bounding the size of an -net of a hypothesis class.
Formalizing it. Both results are elementary and already fully proved in the literature; no open mathematical content remains. What this mission contributes is a machine-checked, faithful Lean statement of Maurey's construction and its corollary, phrased over Mathlib's existing convex-hull and metric-diameter machinery, so that later missions in this series (concentration inequalities, Johnson–Lindenstrauss, chaining) can build on a verified base case of "probability constructs a deterministic covering," and so that the empirical method itself becomes a reusable, linked component on the platform. The proof of the goal (via the probabilistic argument sketched by the book: interpret a convex combination as a probability distribution, average i.i.d. samples, and bound the variance) is left open for solvers.
The identity that makes the proof work — averaging independent copies of a random vector concentrates around its mean at rate in mean-square — is a two-line computation once the convex combination is reinterpreted probabilistically. The step that is easy to miss is this reinterpretation itself: nothing in the statement mentions probability, so the "obvious" attack of manipulating the convex-combination weights directly, or trying to construct by some explicit combinatorial recipe, does not see a path to a bound independent of . The probabilistic argument produces the points non-constructively, via an averaging/existence argument (the expected squared distance is small, so some realization achieves it) rather than an explicit formula — a solver has to introduce a probability space and a random vector that does not appear anywhere in the formal statement to be proved.
Both results are stated over EuclideanSpace ℝ (Fin n) for an explicit dimension n : ℕ, so
‖·‖ is the Euclidean norm and Mathlib's Metric.diam is used directly for
. The convex hull is Mathlib's convexHull ℝ T; by
Mathlib's convexHull_eq, this already coincides with the book's own definition of a convex
combination of finitely many points of , so no bespoke convex-combination definition is
introduced — this mission needs no supporting definitions of its own. In the corollary, "a
polytope with vertices" is formalized, following the book's own proof, as
for a finite vertex set with , rather than via a
separate Polytope structure (which Mathlib does not provide and the book's argument does not
need). The covering bound is an exponent, not a product with
— matching the book's own proof, which counts the ordered -tuples of vertices with
repetition, ; the typeset "" in
the corollary statement is the same juxtaposition-as-exponent notation the proof uses for
"" one line earlier.
A trivializing formalization is ruled out explicitly: the goal must hold for every integer and every , not merely some convenient choice — e.g. together with trivially satisfies the inequality but proves nothing about the theorem's actual content, that a fixed, dimension-independent works uniformly over all points of the hull. The formal statement quantifies , then , then , and only then asserts existence of the , exactly in that order.
Classical Carathéodory (Theorem 0.0.1, stated for context in the source but not used by
either formalized result's proof) is not drafted here: Mathlib already proves the corresponding
statement via affine independence
(Caratheodory.eq_pos_convex_span_of_mem_convexHull, Analysis/Convex/Caratheodory.lean),
from which the book's " points" bound follows via
AffineIndependent.card_le_finrank_succ. It is not added as a kind: reference milestone
because no corresponding theorem is yet published on the Prove2Me platform to point at (checked
2026-09-17: GET /theorems?q=Caratheodory returns only unrelated tropical-convexity results),
and re-drafting existing Mathlib content as a new platform theorem would duplicate rather than
reuse it.
Many results in economics and operations research reduce to a single question: does a
system of interacting, mutually reinforcing choices settle at an equilibrium? A firm
choosing input levels that are complements, a Cournot duopoly whose best responses move
together, a matching market where agents' preferences reinforce assortative pairings —
each is a fixed-point problem, but classical fixed-point theory (Brouwer, Kakutani) asks
for convexity and continuity that these problems rarely have. Tarski's fixed point
theorem [1955] showed that order, not topology, suffices: every increasing (monotone)
self-map of a nonempty complete lattice has a fixed point, and the fixed points themselves
form a nonempty complete lattice, with no continuity or convexity assumed at all. Zhou
[1994] extended this from single-valued functions to set-valued correspondences,
which is what is needed once "best response" becomes "the (possibly non-unique) set of
optimizers." This mission formalizes Zhou's theorem (Topkis's Theorem 2.5.1) together
with its parametric extension (Theorem 2.5.2), the two capstones of the lattice-theoretic
toolkit that the rest of Topkis's monograph — and, within this series, its mission on
supermodular games (Supermodularity and Complementarity V) — builds on directly.
A lattice is a partially ordered set in which every pair of elements has a join (least upper bound) and a meet (greatest lower bound). is a complete lattice if every subset (not just every pair) has a supremum and an infimum in ; a nonempty complete lattice always has a greatest element and a least element .
To compare sets of points — not just points — Topkis defines the induced set ordering : for , holds when every and satisfy and . Restricted to singletons, says exactly , so is the natural extension of from points to sets, and it is the order with respect to which set-valued maps (correspondences) are called increasing: implies .
A subset is a sublattice if it is closed under the binary join and meet of . is subcomplete if, more strongly, the supremum and infimum in of every nonempty subset of exist and lie in — so a subcomplete sublattice is itself a complete lattice under the order it inherits. A point is a fixed point of a correspondence if .
Let be a nonempty complete lattice and an increasing correspondence with subcomplete for every . Then:
and the set of fixed points of , under its inherited order, is itself a nonempty complete lattice.
Let be a partially ordered set and a jointly increasing, subcomplete-valued correspondence on . Then for each the greatest and least fixed points , of exist and are increasing functions of ; under the further hypothesis that whenever , both become strictly increasing in . This is the theorem that gives comparative statics their bite: it says an equilibrium moves monotonically — even strictly — as a parameter of the underlying system changes.
Two supporting results are formalized as milestones because Theorem 2.5.1's own proof invokes them directly: Lemma 2.4.2 (supremum and infimum are monotone under , whenever they exist) and Theorem 2.4.2 (an intersection of increasing correspondences, if it stays nonempty, is itself increasing).
The result itself. Tarski–Zhou is the order-theoretic alternative to Brouwer–Kakutani: where the latter needs a convex, compact strategy space and a continuous map, Tarski–Zhou needs only a lattice order and monotonicity, and it delivers something Brouwer–Kakutani does not — a greatest and a least fixed point, with an explicit order-theoretic formula for each, and the guarantee that the whole fixed-point set is a complete lattice in its own right. This is exactly the machinery behind existence proofs for supermodular games (Topkis's own Theorem 4.2.1, where the fixed points of the best-response correspondence are the pure-strategy Nash equilibria) and behind monotone comparative statics more broadly (Milgrom–Roberts [1994], of which Theorem 2.5.2 is a strict generalization to correspondences).
Formalizing it. Mathlib already has Tarski's theorem for single-valued monotone
functions (OrderHom.lfp/gfp, fixedPoints.completeLattice, Knaster–Tarski). Nothing
in Mathlib currently proves it for set-valued correspondences: this mission is a genuine
strengthening of existing formalized mathematics, not a restatement of it, and it
introduces the induced set ordering and subcompleteness — reused throughout the rest of
this book's mission series — for the first time.
The natural first idea — "apply Knaster–Tarski to some selection function built from " — fails because there is no canonical way to select a single point from each that remains monotone without already knowing the theorem: an arbitrary selection from an increasing correspondence need not itself be increasing (this is exactly the subtlety Topkis's Theorem 2.4.3 addresses only for correspondences with a greatest/least element). The real argument instead builds the candidate fixed point directly as a supremum over an auxiliary set and establishes it is a fixed point using the monotonicity lemma (Lemma 2.4.2) at each step — no selection is ever made. A second subtlety is that the fixed-point set is not, in general, a sublattice of : Topkis's Example 2.5.1 exhibits an increasing self-map of whose four fixed points are not closed under /. Part (b)'s claim that the fixed points form their own complete lattice must therefore be proved without ever assuming, or implying, that ambient joins and meets of fixed points are again fixed points.
is formalized as an abstract CompleteLattice, not ℝⁿ — the theorem is genuinely
about order, and specializing to would hide exactly the generality Zhou's result
adds over finite-dimensional fixed-point theorems. The induced set ordering
InducedSetOrder and the predicate Subcomplete are defined once in this mission and
reused by every later mission in the series that reasons about correspondences ordered
by . A formalization that replaced the correspondence by a single-valued
function would trivialize the mission into a restatement of Mathlib's existing
Knaster–Tarski theorem; the set-valued, subcomplete-ranged correspondence is not an
optional generality but the entire content being added. Part (b) of Theorem 2.5.1 is
formalized as a completeness statement about the induced order on the fixed-point set
itself — not as a claim that the fixed-point set is closed under 's ambient join and
meet, which Example 2.5.1 refutes. "Partially ordered set" throughout is Lean's
PartialOrder, matching the book's own usage in Chapter 2.
Decision-making problems rarely present the same fixed choice twice. A doctor prescribing a treatment sees each patient's medical history and symptoms before deciding; a website choosing which article to show sees the visitor's profile first. The multi-armed bandit model — where the learner repeatedly picks from a fixed set of arms with no side information — cannot express this: it is blind to the covariates that any real decision-maker actually observes. The contextual bandit model closes this gap by letting the learner see a context before acting, and asks for a decision rule that generalizes across contexts rather than memorizing a policy per context. Foster and Rakhlin's Foundations of Reinforcement Learning and Interactive Decision Making (arXiv:2312.16730v1, Section 3, pp. 38–53) develops this model and its algorithms as the bridge between supervised learning and sequential decision making, en route to general reinforcement learning. Contextual bandits with a learned reward-function class underlie production systems for content recommendation, online advertising, and adaptive clinical trial design (Li et al., A Contextual-Bandit Approach to Personalized News Article Recommendation, 2010, https://arxiv.org/abs/1003.0146; Agarwal et al., Making Contextual Decisions with Low Technical Debt, 2016, https://arxiv.org/abs/1606.03966).
The algorithmic history in this chapter runs through two distinct principles. The optimism principle (LinUCB, Section 3.2) generalizes the UCB algorithm to contexts under a linear reward model, but the chapter's own Example 3.1 (Section 3.3) shows optimism fails outside such structured classes, incurring regret linear in the size of the context space or the class. Foster and Rakhlin then present two "black-box" alternatives that use any function class through an abstract regression subroutine: the naive -Greedy method (Section 3.4), and the Inverse Gap Weighting (IGW) strategy underlying the SquareCB algorithm (Bietti, Agarwal & Langford, A Contextual Bandit Bake-off, 2018, https://arxiv.org/abs/1802.04064; Foster & Rakhlin, Beyond UCB: Optimal and Efficient Contextual Bandits with Regression Oracles, 2020, https://arxiv.org/abs/2002.04926). SquareCB attains a regret rate that both generalizes across contexts (no dependence on the size of the context space) and matches the optimal rate — improving on -Greedy's rate — while remaining agnostic to the internal structure of .
Over rounds, a decision-maker faces the contextual bandit protocol: at each round , it observes a context , selects a decision from a finite action set , and observes a reward . Rewards are generated independently as for a fixed, unknown conditional model ; write for the mean reward function and for the optimal, context-dependent policy. The context sequence is arbitrary — fixed in advance or adversarially chosen — while rewards remain stochastic. Performance is measured by regret against :
where is the learner's (possibly randomized) action distribution at round .
To generalize across contexts, the learner is given a class with , and aims for regret scaling with the statistical complexity rather than with . Both algorithms in this mission access only through an online regression oracle (Definition 3, p. 47): given the history , it returns an estimate satisfying, with probability at least , — for instance, exponential weights on a finite class achieves . SquareCB (p. 50–51) then samples its action from the Inverse Gap Weighting distribution (Definition 4, p. 50): given a vector of estimated values with greedy action , and an exploration parameter , is for the unique making a probability distribution.
This holds for any and any , with no reference to or to how was produced — it is the purely algebraic core the goal theorem invokes at every round.
with probability at least , for SquareCB run with , for any context sequence . This is the weakest stable target level in the chapter's oracle-based development: it is stated for an arbitrary class and oracle, so it survives any future improvement to the oracle's own bound, unlike a version hard-coded to a specific class or oracle.
Proposition 10 shows that Inverse Gap Weighting converts any estimation-error guarantee into a regret guarantee with the same statistical rate, with no algorithm-side dependence on the structure of or the size of : the same SquareCB template, driven by a plug-in regression oracle, is minimax optimal whenever the oracle itself is. When is finite, this yields , matching the optimal rate for stochastic multi-armed bandits (Section 2) while generalizing across contexts — a guarantee that optimism (Proposition 7) provably cannot deliver outside linear classes (Example 3.1), and that the simpler -Greedy baseline (Proposition 8) only delivers at a slower rate. Foster and Rakhlin describe Proposition 9 itself as being "at the core of the development for the rest of the course": the same IGW mechanism reappears, generalized, in the book's treatment of general decision-making and the Decision-Estimation Coefficient.
Both propositions are proved results, not open questions; this mission's contribution is a
machine-checked formalization of their exact statements and hypotheses — the precise
OracleGuarantee hypothesis Proposition 10 requires, the exact constant (, not a bare
) its proof yields at the stated optimal , and the universally-quantified form
of the IGW inequality (Proposition 9) that makes it reusable independently of any particular
oracle or class.
The obvious first idea for exploiting an estimator is a UCB-style optimism approach: build a confidence set around and act greedily on its upper envelope, as in LinUCB (Proposition 7). Example 3.1 shows this fails in general: a class can force the confidence set to remain wide on a fresh action at every new context, driving regret linear in — the confidence width in the regret bound does not shrink merely because the oracle's cumulative estimation error is small, since that error is not localized to the specific action the confidence-set approach tries next. Uniform exploration (-Greedy) sidesteps this but wastes exploration budget on actions already known to be far from optimal, which is what caps its rate at (Proposition 8). Inverse Gap Weighting instead ties the sampling probability itself to the estimated gap from the greedy action, so cheap-to-rule-out actions are down-weighted continuously rather than either fully explored (ε-Greedy) or trusted outright (optimism); the technical content of Proposition 9 is showing this specific reciprocal-gap form gives a bound with no hidden dependence on or , for every pair simultaneously — a guarantee optimism cannot match because its confidence sets are class-dependent by construction.
Contexts form an arbitrary type X; actions are Fin A for A : ℕ. A finite probability
distribution over Fin A is represented directly as p : Fin A → ℝ with ∀ π, 0 ≤ p π and
∑ π, p π = 1, and as the finite sum ∑ π, p π * g π, rather than
via Mathlib's PMF (which is ℝ≥0∞-valued) — an equivalent and lighter-weight representation of
a distribution on a finite type. The normalizing constant of Definition 4 and the
optimal actions , are each specified by their defining property (existence
of realizing the IGW formula; ) rather
than constructed explicitly via an intermediate-value or Finset.argmax argument, avoiding
committing to one choice function for a value the book itself leaves implicit. The class
enters neither proposition's statement directly: it appears in the source only through the
abstract bound , which is carried as an explicit real-valued
parameter and hypothesis (OracleGuarantee) rather than as a literal subset of a function space,
since no property of beyond producing this bound is ever used. The probability-
qualifier attached to the online regression oracle's guarantee is likewise the explicit
hypothesis OracleGuarantee ... EstSq on a fixed realized run, rather than a statement
quantified over an underlying probability space of histories — every subsequent step in both
propositions' proofs is deterministic given that this event holds, so this does not weaken either
conclusion. A trivializing formalization would fix (a single ever-optimal action, making
both Reg and the IGW inequality vacuous) or take EstSq as an unconstrained free variable with
no positivity hypothesis (making in Proposition 10 undefined); this mission's statements
require 0 < EstSq and leave , , , -via-EstSq fully general.
This mission omits Proposition 7 (LinUCB): its proof rests on an entirely disjoint apparatus
(finite linear parameter sets, least-squares confidence sets, the elliptic potential lemma) that
neither Proposition 9 nor 10 requires, and Example 3.1 (the failure of optimism) is a worked
example rather than a numbered, formalizable claim. It also omits Proposition 8
(-Greedy): the source leaves the optimal unspecified ("choosing
appropriately"), and deriving its own optimal value and matching constant
independently — rather than reusing the book's own explicit constant, as Rule 7 of this
formalization effort requires — was judged too likely to introduce an unfaithful, invented
constant within this mission's time budget; both are natural extensions for a follow-up mission
or contribution. Reusable infrastructure: the Fin A-indexed finite-distribution convention and
the OracleGuarantee/optimal-action-by-property pattern extend directly to any later chapter
built on the same online-regression-oracle abstraction.
The multi-armed bandit is the simplest model of sequential decision-making under partial feedback: a learner repeatedly picks one of finitely many options and observes a reward only for the option chosen, never for the alternatives. It formalizes problems ranging from clinical trial design (which treatment to offer a patient) to online advertising (which ad to show) and A/B testing more generally. The framework dates to Robbins' 1952 paper on sequential design, and the algorithm this mission's goal theorem concerns — the Upper Confidence Bound (UCB) algorithm of Lai and Robbins [1985] and Auer, Cesa-Bianchi and Fischer [2002] — is the canonical answer to how to explore efficiently: instead of exploring uniformly at random, act optimistically with respect to the current uncertainty about each option's value. This mission draws its formalization from Chapter 2 of Foster and Rakhlin's 2023 lecture notes, Foundations of Reinforcement Learning and Interactive Decision Making, which develops the bandit problem as the first rung of a ladder of increasingly general interactive decision-making settings (contextual bandits, structured bandits, reinforcement learning) that the book's later chapters build.
Fix a finite decision (action) space . In the multi-armed bandit protocol, for each round the learner selects a decision , possibly at random according to a distribution depending on the history observed so far, and then observes a reward drawn independently from a fixed conditional distribution (the stochastic rewards assumption). Writing for the mean reward function and for an optimal decision, the learner's performance is measured by the regret
Because the learner observes a reward only for the action played (bandit feedback), a purely greedy strategy that always plays the current empirical maximizer can commit to a suboptimal action forever, incurring linear regret; some form of deliberate exploration is necessary. The chapter's central construction is the confidence interval: a pair of functions such that, with probability at least , for every round and decision simultaneously. The UCB algorithm plays the optimistic action at every round, using the confidence interval built from Hoeffding's inequality around the empirical mean .
holding with probability at least , for the UCB algorithm using the confidence radius of Eq. (2.19). This is the weakest stable statement the chapter proves: it is optimal up to the log factor, and strengthening it (e.g. to the sharper instance-dependent bound of Remark 10) is explicitly left to later work by the book itself.
UCB is the prototype of the "optimism in the face of uncertainty" principle that recurs, in increasingly abstract form, throughout the rest of the book: the same two-step argument (Lemma 7 + Lemma 8) reappears for linear bandits, structured bandits via the Decision-Estimation Coefficient, and UCB-VI for tabular reinforcement learning. Formalizing Chapter 2 in full therefore front-loads the proof pattern every later chapter in this series specializes. The result itself is also of standalone interest: the minimax rate is the benchmark every subsequent bandit algorithm in the literature is compared against, and the -vs- contrast between ε-Greedy and UCB is the standard illustration, in any course on the subject, of why adaptive exploration matters.
No formalization of this exact statement — realizability with respect to a function class and a generic confidence interval, rather than a per-arm sub-Gaussian empirical mean — currently exists on the platform (see Formalization scope below); the mission both proves this specific regret bound and seeds the generic optimism/potential lemma pair (Lemma 7, Lemma 8) that the book's later, more structured settings specialize.
The natural first attempt — bound the regret of the empirical-mean-greedy algorithm directly — fails outright: on a two-armed instance where one arm is deterministic and the other only slightly better in expectation, the greedy algorithm can commit to the worse arm forever with constant probability, giving linear, not sublinear, regret (§2.1). The obvious fix, ε-Greedy, forces exploration uniformly across all actions regardless of how much is already known about each, so the exploration cost scales with even for actions whose value is already well determined — this is exactly what caps ε-Greedy at the rate. UCB's optimism principle resolves this by exploring an action only in proportion to how uncertain it still is; the technical core, isolated in Lemma 7 and Lemma 8, is disentangling "the algorithm made a mistake" from "the algorithm is still uncertain," which are conflated in the naive per-round regret decomposition used for ε-Greedy.
Both the goal and the milestones fix a finite decision space Fin A, a mean reward
function fStar : Fin A → ℝ with fStar π ∈ [0,1], and an optimal decision
piStar. Regret is defined generically (Eq. (2.3)) via per-round decision weights
p : ℕ → Fin A → ℝ, so it applies uniformly to a randomized algorithm (ε-Greedy) and
a deterministic one (UCB, via the point mass at the played action). The book's "with
probability at least " qualifier on both Proposition 4 and Proposition 5 is
formalized as the deterministic consequence of the underlying concentration event
(Eq. (2.9) and Eq. (2.18) respectively) holding — exactly the move the book's own
proofs make ("Let us condition on the event in (2.18) ... "). The concentration
events themselves rest on Hoeffding's inequality for adaptive stopping times
(Lemma 33) and Bernstein's inequality (Lemma 5), both stated in the book's technical
appendix outside this chapter, and are not drafted here; a solver may either take
them as a hypothesis (as this mission's statements do) or import/prove them
separately. A trivializing formalization is ruled out explicitly: taking δ outside
, or dropping the fStar π ∈ [0,1] hypothesis, would make the stated
constants vacuous or false, so both are retained as explicit hypotheses in every
theorem. In every ≲ statement (Prop. 4, Lemma 8, Prop. 5) the witnessed constant
C is quantified before the instance parameters (A, T, δ, and the realized
sequences): ∃ C, 0 < C ∧ ∀ A T δ ..., Reg ≤ C * (rate), not the other order. This
is deliberate, not stylistic: quantifying C after the instance lets it depend on
A, T, δ, making the bound satisfiable by an arbitrarily large C chosen per
instance and hence content-free, which is not what the book's ≲ means (a single
constant working uniformly over all instances). Proposition 5's UCB decision rule
is stated in the book's own two clauses, not collapsed into a single "maximize the
upper confidence bound" rule: the confidence radius of Eq. (2.19) is at
(an action never yet sampled), so the book's UCB always plays an
unsampled action before ever comparing indices, and only compares finite upper
confidence bounds once every action has been sampled at least once; the confidence
event of Eq. (2.18) is correspondingly assumed only at sampled actions, since the
book's own bound is vacuous otherwise. An earlier draft instead capped the radius
at when , which is a true statement about a different algorithm (a
sampled action can have index above the capped unsampled index), and was corrected
to the book's own rule after moderation. Reuse from the platform's existing bandit library (BanditAlgorithm,
Lattimore & Szepesvári) is deliberately avoided: that library's UCB
(bandit_ucb_regret_bound, bandit_ucb_minimax_regret_bound) is stated for
per-arm 1-sub-Gaussian rewards with fixed by the horizon, whereas
this chapter's UCB is stated for a free failure probability and a generic
confidence-interval abstraction (the multi-armed case being of the book's general realizability framework) — the two are
related but not the same statement. Contributions extending the mission with the
generic confidence-interval form of Lemma 7/8 applied to other chapters in this
series (contextual and structured bandits) are welcome.
Two-stage stochastic programs with recourse require evaluating , the expected value of a recourse function, at every candidate first-stage decision . When is high-dimensional or continuously distributed, this expectation is a multivariate integral of a piecewise-linear, generally nondifferentiable integrand, and classical quadrature rules — built for smooth integrands in low dimension — do not apply (Birge & Louveaux, §8.1). What does apply is convexity: is convex whenever the recourse problem is a linear program in , and convexity alone is enough to sandwich between two computable discrete approximations. This chapter develops that sandwich, and it is the standard device used throughout the stochastic-programming literature to bound and iteratively refine the recourse function: the lower bound goes back to Jensen [1906]; the upper bound is due to Edmundson [1956] and Madansky [1959], with the mean-consistent LP refinement due to Madansky [1960] and Gassmann & Ziemba [1986]. Refinements of both bounds appear in Huang, Ziemba & Ben-Tal [1977], Kall & Stoyan [1982] and Frauendorfer [1988].
Fix a probability space and an integrand , where is the (convex, closed) support of a random vector and is a real vector space (in the recourse application, and is the first-stage feasible region). Write .
A partition of into measurable blocks determines, for each block, its probability and its conditional mean . Equivalently — and this is the convention this mission's Lean development uses — the blocks may be taken directly on the sample space as the pulled-back sets , with and the Bochner integral average of over the block; the two descriptions coincide.
This is the sharpest statement the chapter proves for the lower bound: it holds for every finite measurable partition, with no assumption beyond convexity of and integrability.
For compact, let be the extreme points of , carrying the Borel field of all its subsets. If, for every , is a probability measure on with barycenter (i.e. ) and is measurable for every , then
Together the two targets give the chapter's headline sandwich: for convex , the finite-partition Jensen value and the Edmundson-Madansky value bracket the true expectation, and refining the partition (resp. the disintegration) tightens both sides toward it.
The Jensen bound is the workhorse of discrete-distribution approximation in stochastic
programming: it is what makes a valid, refinable
lower-approximation of the true recourse function, and it underlies the partition-refinement
schemes (§8.2, following Birge & Wets [1986] and Frauendorfer & Kall [1988]) used inside the
-shaped method and separable-programming solvers described later in the chapter (§8.3). The
Edmundson-Madansky bound is its indispensable upper counterpart: without it there is no
certificate of how far a lower approximation can be from the truth, and the mean-consistent LP
refinement (eq. 2.9, not part of this mission) reduces to a moment-problem computation over
. Both bounds are, to date, unformalized: the platform holds no theorem matching either a
finite-partition conditional-Jensen inequality or an extreme-point disintegration bound (searched
GET /theorems?q=... for "Jensen", "conditional expectation", "Edmundson Madansky", "partition
convex" — no relevant hits), so this mission is a first formalization of both, not a
reformulation of existing platform content. Mathlib supplies the raw convexity substrate this
mission is built from — finite Jensen (Analysis/Convex/Jensen.lean) and, critically, the
set-average integral Jensen inequality (ConvexOn.map_set_average_le in
Analysis/Convex/Integral.lean), exactly the per-block step the book's proof of Theorem 1
performs — but no existing lemma assembles these into the partitioned, conditional-mean statement
the book actually states.
The obvious shortcut is to prove "convex functions lie above their tangent line" and stop — this captures no partition structure at all and is not the theorem the book states (the theorem is about , a sum over blocks, not a single linearization). The real content is bookkeeping across the partition: writing as (an exact identity, no convexity needed), then applying ordinary Jensen inside each block to replace by from below — the inequality only enters at the second step, once per block. Proving this in Lean means correctly discharging, for every block, the side conditions Mathlib's integral-Jensen lemma needs (closedness of , continuity of on , integrability on the block) and then summing the per-block inequalities against weights that themselves depend on the partition — an easy step to get wrong by, e.g., letting be an arbitrary point of rather than exactly its conditional mean, which understates what Jensen actually forces. Theorem 2 additionally requires setting up the disintegration correctly: is a probability measure defined as an integral of the kernel-like family against , and both the barycenter condition on and the measurability of are load-bearing — dropping either makes ill-defined or the bound's proof inapplicable.
for a complete real normed vector space (NormedAddCommGroup E,
NormedSpace ℝ E, CompleteSpace E); no finite-dimensionality is assumed since neither theorem's
proof needs it. The parameter ranges over an arbitrary type with ,
and is left as a bare function α → E → ℝ, matching the book's level of abstraction (the
recourse LP's own data is never used in either proof).
The partition is formalized directly on the sample space (a Partition structure:
pairwise-disjoint measurable blocks covering , each of positive measure) rather than on
, per the equivalence noted under Setting; is defined as the Bochner-integral
average , so it is forced to be the conditional mean and cannot be
weakened to an arbitrary sample point of the block — the change the chunk brief flags as the main
faithfulness trap for this chapter.
Two explicit hypotheses are added beyond the book's own statement of Theorem 1, both needed by
Mathlib's integral-Jensen lemma rather than narrowings of the mathematical content:
ContinuousOn (g x) Ξ (finite-dimensional convex functions are automatically continuous on the
interior of their domain, which is what the book implicitly relies on; stated explicitly since
is not assumed finite-dimensional) and integrability of and of
(needed for and each to be well-defined). For Theorem 2, the
disintegrating family is E → Measure Ext for an abstract type Ext (standing for
) with the discrete MeasurableSpace (every subset measurable, matching the
book's "Borel field ... the collection of all subsets"), mapped into by an embedding toE
whose range is exactly (convexHull ℝ Ξ).extremePoints ℝ; the measure (named μExt in
the Lean code, since λ is a reserved keyword) is a hypothesis satisfying its defining equation
(2.6) rather than constructed, since constructing a measure from a set function is a separate,
book-external piece of measure theory the chapter's own proof does not perform either — it simply
asserts is the probability measure with that value on every set.
A trivializing formalization is ruled out explicitly: a version that lets range over an arbitrary point of , or that proves only the ordinary (unconditional) Jensen inequality without ever introducing the partition, states something strictly weaker than the book and is not what is formalized here.
Both draft theorems end in := by sorry; a full Lean proof of Theorem 1 combines Mathlib's
ConvexOn.map_set_average_le applied per block with the exact decomposition of into
over the partition's disjoint, covering blocks. Reusable beyond this mission:
the Partition structure and its weight/condMean accessors generalize to any chapter needing
a finite measurable partition with conditional means (this book's later approximation schemes,
§8.2-8.5 and Chapter 10, all build on the same device). Contributions solving either theorem, or
formalizing the partition-refinement monotonicity (eq. 2.3, not part of this mission's milestone list since it is not itself a
numbered theorem) as a follow-up, are welcome.
Thompson's group is the group of piecewise-linear order-preserving homeomorphisms of with finitely many breakpoints, all at dyadic rationals, and all slopes powers of . Two earlier missions formalize its definition and its first structural facts (§1 and §4: the commutator subgroup is simple, is not elementary amenable) and its tree-diagram normal form (§2). What neither says is how looks as an abstract group: by generators and relations.
That is §3 of Cannon, Floyd and Parry's Introductory notes on Richard Thompson's groups (L'Enseignement Math. 42 (1996), doi:10.5169/seals-87877), which gives two presentations of and proves that both present the group of homeomorphisms:
The finite presentation is the form in which enters most of the literature — the word problem, the growth and amenability questions, the homological results of Brown and Geoghegan all start from it — and the infinite presentation is the one that makes the normal form of §2 visible as an algebraic fact.
Throughout, , the source's convention, and groups are written multiplicatively with composition of maps as the product: .
The functions. and are the two specific homeomorphisms of from the §1
mission (mapA, mapB: halves , is a translation on ,
and doubles ; is the identity on and acts like , scaled,
on ). For , and ; these are the
functions X n of the §2 bundle. Corollary 2.6 of the source, proved in the §2 mission, says
and generate .
The formal symbols. and are presented groups: the free group on the listed
symbols modulo the normal closure of the listed relators. In Lean they are Mathlib's
PresentedGroup applied to explicit relator sets: relsF1, a two-element set of words in
the free group on the two-element type FormalAB, and relsF2, the set of words
for in the free group on . The symbols
are distinct objects from the functions; the whole content of the section is that the map
"symbol function" is an isomorphism.
Auxiliary objects. In the source sets and
for (Y), the intended images of the . In a list of nonnegative
exponents determines the positive word
(wordF2), the formal counterpart of the §2 bundle's word; the normal-form conditions of
Corollary-Definition 2.7 are the §2 predicate IsNormalFormData, reused verbatim.
The goal is the finite presentation, Theorem 3.4 for :
On the way, in the order the source proves them:
A one-line consequence closes the list: is finitely presented, in Mathlib's sense
Group.IsFinitelyPresented.
The result. A presentation is what makes an object of combinatorial group theory. The two relators are what one checks a homomorphism against, the infinite presentation is what the normal form is a normal form for, and "finitely presented" is the hypothesis under which is a test case for conjectures about finitely presented groups. Every later algebraic statement about — the word problem is solvable, the abelianization is , the automorphism group, the presentations of and — is stated relative to one of these two presentations.
Formalizing it. Both theorems are proved in the source and their proofs are short, so what this mission produces is the machine-checked bridge between the two existing developments: the analytic definition of and its tree-diagram normal form on one side, an abstract presented group on the other. The isomorphism is where §2's uniqueness theorem is used rather than merely proved: injectivity of is exactly the statement that distinct normal forms give distinct functions. Nothing here is machine-checked anywhere else; the platform has no presentation of .
Theorem 3.1 is a computation in and offers no surprises once lines (3.2) and (3.3) of the source are set up as their own statements: the induction that establishes from the two relators is the only place care is needed, and the source spells it out.
The central difficulty is the paragraph on p. 226 proving that is injective. The
source argues in prose that "every nontrivial element of can be expressed as a
positive element times a negative element", and then "put in normal form" by deleting an
from both parts and re-indexing when is absent. Formally this is a rewriting
argument inside the abstract group , with no geometry to lean on: one needs the three
derived relations , ,
(for ), an induction that sorts an arbitrary word into
positive-times-negative form, and a second induction that reduces such a form until the
normal-form conditions hold. The obvious shortcut — "every element of is the image of
some function, and functions have normal forms" — is circular, because it presupposes the
injectivity being proved. The milestone exists_isNormalFormData_F2 isolates this step.
word/wordFrom and the predicate
IsNormalFormData are the published definitions of the §1 and §2 missions
(CannonFloydParry, CannonFloydParry_Trees, CannonFloydParry_TreeDiagrams), imported
unchanged. Elements of are order isomorphisms of the subtype ,
and is the subgroup they generate; membership of , , in is a proved
theorem, not a definition.CannonFloydParry_Presentations adds only the formal side: the symbol type
FormalAB, the relator sets relsF1, relsF2, the presented groups F1, F2, the
symbol maps symF2 (into ) and symF (into the interval maps), the elements Y, and
the words wordF2. Relators are written out as ; no commutator notation
is used in published statements.MulEquiv sending the named generators to the
named images. Nothing is asserted about uniqueness of the isomorphism (it is unique, since
the generators generate).closure_mapA_mapB_eq_F), the §2 normal-form
theorems (exists_isNormalFormData, word_ne_one_of_isNormalFormData), and the §4
mission's mem_commutator_iff if a solver prefers to verify the relators of in
through supports rather than by direct computation. Solutions may import them.Group.IsFinitelyPresented instance built from
the isomorphism (the last milestone), and, further off, the presentations of and
from §5–§6, which extend by one and two generators.Thompson's group is a finitely presented group of piecewise-linear homeomorphisms of the unit interval that has served since the 1960s as a standard supply of counterexamples in combinatorial group theory: its commutator subgroup is simple, every proper quotient of it is abelian, it contains no free subgroup of rank two, it is not elementary amenable, and whether it is amenable is a question Cannon, Floyd and Parry report as having been raised by Geoghegan in 1979 and still open when they wrote (CFP96, §4 and p. 227).
Almost nothing about is computed directly from that analytic definition. What makes the group tractable is a combinatorial calculus: each element is encoded by a pair of finite binary trees, and multiplication becomes a cancellation between trees. Cannon, Floyd and Parry credit the device to Brown and devote §2 of their notes to it; everything later in those notes that requires a computation — the two presentations of §3, the normal subgroup lattice of §4, the treatment of Thompson's group in §5 — runs through it.
This mission formalizes that calculus and the normal form it yields.
A real number is dyadic when it has the form with an integer and a nonnegative integer. Thompson's group consists of the increasing homeomorphisms of that are piecewise linear with finitely many breakpoints, all breakpoints dyadic and every slope an integer power of , under composition. Two of its elements are
and from them come and for , so that .
A standard dyadic interval is one of the form with and nonnegative integers and . A partition of is a standard dyadic partition when every is a standard dyadic interval.
An ordered rooted binary tree is a finite tree in which each vertex has either no children or an ordered left child and right child. Its childless vertices are its leaves, which carry a canonical left-to-right order; its right side is the path from the root always taking the right child; a caret is a vertex with its two children. Assigning to the root and splitting each interval at its midpoint between the two children gives every vertex a standard dyadic interval, and the leaves then cut out a standard dyadic partition — the sense in which such a tree is a -tree. The exponents of a -tree are one nonnegative integer per leaf, in order: the th is the length of the longest arc of left edges beginning at the th leaf that does not reach the right side.
A tree diagram is an ordered pair of -trees with equally many leaves. An element of has that diagram when is affine on each interval cut out by the leaves of and carries those intervals, in order, onto the intervals cut out by the leaves of . Adjoining a caret to and to at the same leaf gives another diagram for the same ; a diagram admitting no such reduction — no position where both trees carry a caret — is reduced.
Every in is
for exactly one choice of nonnegative integers , , subject to two conditions: exactly one of and is nonzero, and if and for some then or .
It fixes no bound on and no normalization beyond those two conditions, so no later refinement of how the exponents are presented can invalidate it.
The milestone list follows §2 in order: the correspondence between standard dyadic partitions and -trees, the bijection between and the reduced tree diagrams, the word read off the exponents of , a criterion for a diagram to be reduced, generation by and , and closure under multiplication of the positive elements — those of the form with every exponent nonnegative.
A normal form is a decision procedure: two words in the generators name the same element exactly when their normal forms agree, so the word problem for is solved by computing them. The generation statement is what licenses treating as a two-generator group, and it is the input to both presentations in §3. The positive elements and their closure under multiplication are used, with the normal form, throughout §5 on Thompson's group .
The §2 results this mission targets — Lemma 2.2, the correspondence between and the reduced tree diagrams, Theorem 2.5, Corollary 2.6, Corollary-Definition 2.7 and Lemma 2.8 — are proved mathematics: Cannon, Floyd and Parry are expounding material that goes back to Thompson's unpublished notes. None of them has a machine-checked proof on this platform, and the library contains no tree-diagram machinery to build on, so the definitions published here fix the interface for anyone later formalizing Thompson's groups and , which occupy the same notes and are built from the same trees.
There is also a concrete dependency. The companion mission on §4 of the same paper has eleven of its fifteen milestones machine-checked, and all four that remain wait on this section: Cannon, Floyd and Parry prove their Theorem 4.1 through Corollary 2.6 and their Theorem 4.3 through the normal form. Corollary 2.6 appears in this milestone list as the same theorem object that is open there, so closing it here closes it there.
The obvious way to attach a diagram to an element is to use the partition given by its breakpoints. That fails twice over: the breakpoints of need not be the division points of any -tree, and even when they are, their images under need not be either, since the definition of constrains the breakpoints and slopes of and says nothing about where the image partition sits. Both failures must be repaired by refining the partition before any tree appears, which is why that refinement is a milestone rather than a preliminary.
Uniqueness of the reduced diagram is a difficulty of a different kind: two reduced diagrams for the same element admit no a priori map between their trees, so they cannot be compared directly.
A third is not visible in the source. For trees with leaves the exponent lists always end in , so the outermost factors of the word above vanish; but the normal form demands that exactly one of , be nonzero. The two indexings differ, and a re-indexing step sits between the theorem producing the word and the corollary stating the normal form. The paper prints them one under the other. That step is a milestone of its own, flagged as absent from the source, so a solver working from the paper alone is not ambushed by it.
Ordered rooted binary trees are an inductive type — a leaf, or a pair of subtrees — rather than graphs with a root and valence conditions. Those conditions say exactly that every non-leaf vertex has two distinguished children, so both descriptions pick out the same objects, but the inductive type is a reformulation of the paper's definition and the definition bundle says so. The infinite tree of all standard dyadic intervals is likewise never built: the subdivision of comes from a recursion halving at each node, which turns the paper's observation that the leaves of a -tree are the intervals of a standard dyadic partition from something given into something proved.
is imported rather than redefined, from the published definition bundle of the companion mission, where it is the subgroup generated by the piecewise-linear maps described above; membership in that subgroup is identified with the piecewise-linear description by a theorem already machine-checked there. Exponent data is carried by finite lists, and the uniqueness in the goal is uniqueness of that list data.
The goal is vacuous in neither direction: its hypothesis is met by and themselves, and a separate milestone asserts that every choice of exponent data meeting the two conditions names an element other than the identity.
The tree combinatorics — leaf counts, right sides, the subdivision map, the exponents, carets — is published here as a separate definition node that mentions nowhere and needs nothing but Mathlib, so it is reusable as it stands; the diagram vocabulary is built on it. Any milestone is open to contribution, as are routes other than the paper's.
Within that paper tree diagrams are credited to Brown and the word-length algorithm to Fordham, cited there as [Bro1] and [Fo].
Almost every classical transcendence theorem is a statement about the interaction between the additive structure of and the exponential function. Hermite proved in 1873 that is transcendental, Lindemann in 1882 that is transcendental for every nonzero algebraic — hence that is transcendental and the circle cannot be squared — and Weierstrass in 1885 extended this to the linear independence of over for distinct algebraic . Gelfond and Schneider settled Hilbert's seventh problem in 1934, and Baker's 1966 theorem on linear forms in logarithms made the subject effective.
Schanuel's conjecture, formulated by Stephen Schanuel in the 1960s and first published by Lang (Introduction to Transcendental Numbers, Addison–Wesley, 1966, Chapter III), is a single statement that contains all of these as special cases, together with a large number of statements that remain open — for instance that and are algebraically independent, or that is irrational. No case of it is known beyond those already covered by the Lindemann–Weierstrass theorem or by Baker's theorem.
Timeline, with the hypotheses each result actually assumes:
Write for the complex exponential function. A tuple of complex numbers is linearly independent over when the only rationals with are ; here is viewed as a vector space over .
For a subset , let denote the subfield of generated by over . The transcendence degree is the cardinality of a transcendence basis of over : the largest number of elements of that are algebraically independent over . A number is transcendental over when no nonzero polynomial with rational coefficients vanishes at , and numbers are algebraically independent over when no nonzero polynomial in variables with rational coefficients vanishes at .
The goal fixes no numerical constant and no special shape for the : it asserts only the inequality, for every and every -linearly independent tuple. The case is vacuous and the conclusion is a bound on a cardinal, so nothing is hidden in a degenerate convention.
The milestone list consists of the landmark unconditional theorems that Schanuel's conjecture generalizes, the known function-field analogue, and one conditional corollary that records what the conjecture buys:
Schanuel's conjecture decides, in one stroke, a long list of questions that are individually open: the algebraic independence of and , the irrationality of and of , the transcendence of and , the four exponentials conjecture, and — combined with work of Macintyre and Wilkie — the decidability of the first-order theory of the real exponential field. Its restriction to algebraic is exactly the Lindemann–Weierstrass theorem, and its restriction to whose exponentials are algebraic is exactly Baker's theorem, so the conjecture is a common generalization of the two main unconditional pillars of the subject.
On the formalization side, the state of the art in Lean's mathematical library is modest relative to this history: the analytic core of the Lindemann–Weierstrass argument is present, but the Hermite–Lindemann theorem, the Lindemann–Weierstrass theorem, the transcendence of , the Gelfond–Schneider theorem, the six exponentials theorem and Baker's theorem are not available as usable statements in the pinned environment. Each milestone here is therefore a genuine formalization project with a known mathematical proof, and none of them is a restatement of an existing library result. The goal theorem itself is open mathematically; the realistic contributions to it are reductions — implications between the goal and other statements — and closing the milestones that the conjecture generalizes.
The obvious approach to any single case — build an auxiliary function with many zeros, bound its derivatives, and derive a contradiction from an integrality argument — is the method behind every result on the milestone list, and it is exactly what fails for the conjecture in general. Those proofs need the exponentials, or the arguments, to be algebraic somewhere, so that heights and denominators can be controlled; for a general -linearly independent tuple there is no arithmetic input at all, and no known construction produces the required auxiliary function. Ax's theorem shows that the differential-algebraic shadow of the statement is true, but its proof uses the derivation on the function field and has no arithmetic counterpart. A solver should not expect the conjecture itself to fall to a variation of the classical method.
All statements are over , with the complex exponential. Tuples are indexed by Fin n, ℚ-linear independence is Mathlib's LinearIndependent ℚ, transcendence degree is Mathlib's Algebra.trdeg, the generated field is IntermediateField.adjoin, and the inequality is between cardinals, so the goal reads (n : Cardinal) ≤ Algebra.trdeg ℚ (adjoin ℚ (Set.range z ∪ Set.range (Complex.exp ∘ z))). Algebraicity is IsAlgebraic ℚ, transcendence is Transcendental ℚ, and algebraic independence is AlgebraicIndependent ℚ.
There is no trivializing formalization here: the hypothesis LinearIndependent ℚ z is satisfiable for every , so the goal is not vacuous, and the conclusion is an inequality of cardinals rather than a statement about a definition introduced for this mission.
The Ax milestone is stated for formal power series in one variable over : the exponential relation is expressed as the differential equation with PowerSeries.derivative, and the conclusion bounds Algebra.trdeg ℂ of the ℂ-subalgebra generated by the and the . The conditional corollary takes the full statement of Schanuel's conjecture as an explicit hypothesis, so it is provable unconditionally as stated.
Infrastructure that a complete development needs, and that is reusable well beyond this mission: Siegel's lemma and height machinery for algebraic numbers, the standard auxiliary-function construction with derivative bounds, and interface lemmas relating Algebra.trdeg, AlgebraicIndependent and Transcendental. Reductions between the milestones — for example deriving Hermite–Lindemann from Lindemann–Weierstrass, or the six exponentials theorem from a general Baker-type statement — are welcome as sketches.