Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A gas of interacting particles is described exactly by coordinates, and by no useful equation. Kinetic theory replaces that description by a single scalar field, the one-particle distribution function , whose evolution is governed by the Boltzmann equation. The price is the collision operator: the true Boltzmann collision integral is quadratic and five-dimensional, and almost every statement about it is hard. The BGK operator (Bhatnagar, Gross and Krook, 1954) replaces it by simple relaxation of towards the local Maxwellian at a fixed rate . It is the standard first model for rarefied gas dynamics, the basis of lattice-Boltzmann numerics, and the model in which the structural features of kinetic theory — conserved moments, an -theorem, hydrodynamic closure — can be exhibited in closed form.
This mission formalizes the BGK material as it is posed in Question 1 of the Oxford MMathPhys Kinetic Theory examination paper of Hilary Term 2019: the conservation of the hydrodynamic moments by the collision operator, the sign of the entropy production together with the characterisation of equality, the slab-geometry reduction to a closed two-field system, and the vanishing of the resulting stress and heat-flux corrections at equilibrium.
Velocities and positions range over . A distribution function is a map on velocity space (at a fixed position and time), assumed everywhere positive, integrable, and with finite second velocity moment. Particles have unit mass and the Boltzmann constant is set to . Its moments are
the mass density, the bulk velocity and the temperature. The Maxwellian with parameters is
and the local Maxwellian of is : the Maxwellian carrying the same three moments as . The BGK collision operator with relaxation time is
and the Boltzmann equation with this operator is
In the slab geometry of parts (c)-(d) of the source, , , with , and is independent of and ; the reduced fields are and .
This is part (b) of the source question, including the answer to "under what conditions does equality hold". It is stated for every admissible and every ; it fixes no rate and no constant, so it is not invalidated by sharper quantitative versions.
The three conservation identities say that the BGK operator, however crude as a model of binary collisions, respects the exact conservation laws of the gas: they are what makes the moment hierarchy of the BGK equation reduce to the Euler equations at leading order. The entropy inequality is the model's -theorem: it forces the entropy to be non-decreasing under collisions and singles out the Maxwellians as the only collisional equilibria, which is the statement that fixes the direction of time in the model. The slab reduction of part (c) is the standard device by which a three-dimensional kinetic problem is reduced to a pair of one-dimensional kinetic equations, used throughout computational rarefied gas dynamics; part (d) identifies exactly which moments of the reduced fields carry the non-equilibrium stress and heat flux.
Formalizing this material requires building the moment calculus of Gaussians on against Lebesgue measure — normalisation, first and central second moments, and the partial integration over two of the three velocity components — none of which exists in Mathlib in a form adapted to kinetic theory. The mathematics is classical and the proofs are known; the work is in the analysis bookkeeping: integrability of moments, dominated convergence, and the a.e. equality case of a strict pointwise inequality.
The obvious computation for the -theorem — expand and integrate term by term — does not by itself give a sign: has no sign, and neither does . The argument needs the conservation identities as an input, because they are what allows , which is a quadratic polynomial in , to be subtracted for free. Only then is the integrand pointwise of one sign. Formally, the obstacle is that none of the pieces of the integrand is separately integrable in general: the statements are formulated with the integrability of the entropy-production integrand as an explicit hypothesis, and any splitting of it must be justified.
The equality case adds a second difficulty. Vanishing of the integral of a non-negative integrable function gives vanishing only almost everywhere, so the conclusion is an a.e. identity , and the strictness of for must be used pointwise.
Velocity space is EuclideanSpace ℝ (Fin 3) with its Lebesgue (volume) measure, and
integrals are Bochner integrals; vector-valued moments are integrals of
EuclideanSpace-valued functions. Distribution functions are total functions
with no measurability packaged into the type, so every statement
carries its own integrability hypotheses; admissibility (positivity everywhere, integrability,
finite second moment) is bundled in a predicate. The Maxwellian prefactor is written with a
real power , so is required wherever it appears. The relaxation
time satisfies .
Two traps are worth naming. First, in Lean the integral of a non-integrable function is by convention, so an entropy inequality stated without an integrability hypothesis would be satisfiable for trivial reasons; the goal therefore assumes the entropy-production integrand is integrable, and states the equality case as an iff, which is not satisfiable by a degenerate reading. Second, the local Maxwellian is defined from the moments of itself, not from externally supplied parameters, so none of the conservation statements can be discharged by choosing convenient parameters.
The slab-geometry part of the mission is developed in its own definition file, with the
perpendicular velocity in EuclideanSpace ℝ (Fin 2) and the reduced fields as functions
. The Gaussian moment lemmas produced here are reusable for any
Maxwellian-based kinetic model; contributions that add Mathlib-level lemmas on Gaussian moments
in , rather than ad-hoc computations, are especially welcome.
The rise and fall of the ocean surface under the gravitational pull of the moon and the sun is the oldest quantitative problem in physical oceanography, and it is still a working one: satellite altimetry can only see ocean circulation after the tidal signal has been removed, and the removal is done with a numerical solution of Laplace's tidal equations (LTE) constrained by tide-gauge and altimeter data (Le Provost et al., J. Geophys. Res. 99 (1994) 24777). The same equations carry the global tidal energy budget: an estimate of where the roughly 3.5 TW of tidal energy is dissipated — shallow-sea bottom drag versus conversion into internal tides over deep-ocean topography — is obtained by integrating the energy identity of these equations against observed elevation data (Egbert and Ray, Nature 405 (2000) 775).
The material formalized here is M. Hendershott, Lecture 3: Solutions to Laplace's Tidal Equations (Woods Hole Oceanographic Institution, Geophysical Fluid Dynamics Program lecture notes, pp. 34–44), notes taken by V. Birman and E. Williams Frajka. The lecture states the separable normal-mode solutions of the stratified problem, the solid Earth tide and the Love number decomposition, models of dissipation, coastal boundary conditions, and finally the energy equation of the tides, both ignoring and including the yielding of the solid Earth.
Write and for the two components of the depth-independent horizontal velocity, for the free-surface elevation, for the solid Earth tide (the elastic displacement of the crust under the tidal load), and for the observed, geocentric tide. The ocean has resting depth , constant density , gravity , and constant Coriolis parameter . The astronomical forcing enters through the tide generating potential and the dissipation through a force per unit area .
Laplace's tidal equations are the two momentum equations
together with the continuity equation, which in the presence of the solid Earth tide reads
For a stratified ocean the same system arises mode by mode after separation of variables, with replaced by the equivalent depth of the -th mode and the vertical structure solving , where is the buoyancy frequency.
with
This is a pointwise identity, valid at every for every solution of the equations above, with variable depth and no assumption on the form of the dissipation.
The milestone list covers the corresponding identity with the solid Earth tide ignored (eqs. (29)–(30)), the two normal-mode facts of §2 — the vertical structure equation with the equivalent depth (eq. (4)) and the nonrotating barotropic plane wave with its dispersion relation (§2.1) — and the two averaging statements of §6: that the period mean of the time derivative of a periodic energy density vanishes (eq. (31)) and the resulting period-averaged balance (eq. (32)).
The energy identity is what converts elevation observations into a dissipation estimate: averaged over a tidal period and integrated over a basin with no flux through its boundary, the flux divergence drops out and the work done by the tide generating potential equals the dissipation, so is computable from alone. Every term in that chain — which terms are exact, which vanish only on average, which require the Love numbers to be real — is a hypothesis that a formal statement has to carry explicitly, and the lecture is explicit that the identity holds "provided that the Love numbers are real", i.e. provided the solid Earth tide is dissipation-free.
Formalizing this material produces a reusable model of a rotating shallow-water system with forcing, dissipation and an elastic bottom boundary, together with the calculus lemmas needed to differentiate products of fields of several variables. Nothing here is an open problem: the results are classical, and the contribution is a machine-checked derivation from a precisely stated model, including the bookkeeping that textbook derivations compress.
The obstacle is not depth of argument but faithfulness of the model. The derivation multiplies the two momentum equations by and , the continuity equation by , and adds; every step needs a product rule for a field of three variables, and the Coriolis terms must cancel exactly rather than approximately. Two places in the source require care before they can be formalized: equation (29) prints the surface term with coefficient , and the printed in §6.1 has signs that do not follow from the printed ; the identities are true with and respectively. The potential energy (37) also differs from by a term independent of time, which is invisible in and therefore harmless. A naive formalization that copies the printed formulas without checking these will state something false.
Fields are real-valued functions of , and ; partial derivatives are Lean's
one-dimensional deriv applied slot-wise, and differentiability is imposed as an explicit
hypothesis in each variable separately, rather than through Fréchet derivatives. Depth is a
function that does not depend on time, and positivity of and is assumed
where the momentum equations are divided by . The equations themselves are packaged
as a structure with three fields, one per equation, so that a solution is an explicit witness
rather than an assumption schema; this rules out a vacuous reading, since constant fields with
zero forcing satisfy the structure. The barotropic plane wave of §2.1 is stated with
complex-valued and and the physical normalization , , and is
an equivalence: the wave solves the system exactly when . The
vertical mode statement uses the rigid-lid conditions ; the lecture's
free-surface condition at is satisfied by the sine modes only
in the limit of small equivalent depth, and is not claimed. Period averaging is formalized as
of an interval integral at a fixed horizontal position, with periodicity and
continuity of the relevant time derivative as hypotheses.
Contributions extending this mission are welcome in three directions: the derivation of the equations from the linearized Euler equations of Lecture 2, the solid Earth tide of §3 with the Love number decomposition (17)–(20), and the basin-integrated form of the energy budget (33), which needs a divergence theorem for the flux term.
Graphene is a single sheet of carbon atoms arranged on a honeycomb lattice. Its electrons are described, to a first approximation that is quantitatively good near the Fermi level, by a nearest-neighbour tight-binding model: a hopping amplitude between adjacent carbon sites and nothing else. What makes the model worth studying is that this two-parameter lattice problem produces a band structure with two bands that touch at isolated points of the Brillouin zone and disperse linearly around them, so that low-energy electrons obey a two-dimensional massless Dirac equation rather than a Schrödinger equation with an effective mass. That observation organises the standard review literature on graphene (Castro Neto, Guinea, Peres, Novoselov, Geim, The electronic properties of graphene, Rev. Mod. Phys. 81 (2009) 109), and goes back to Wallace's 1947 band theory of graphite.
This mission formalises a self-contained set of lecture notes that carries the computation out in full: F. Utermohlen, Tight-Binding Model for Graphene (2018). It is the two-dimensional, two-sublattice counterpart of the tight-binding chain: the chain gives a single band with no band touching, while the honeycomb lattice, whose unit cell contains two inequivalent sites, produces a Bloch matrix and the conical band touchings targeted here.
Fix a carbon–carbon distance and a hopping amplitude . The honeycomb lattice is two interpenetrating triangular lattices, the and sublattices, with lattice unit vectors , and nearest-neighbour vectors
each joining an site to one of its three neighbours. The corners of the first Brillouin zone — the Dirac points — are
Fourier transforming the second-quantised hopping Hamiltonian gives with and the Bloch Hamiltonian
where is called the structure factor. The mission takes this matrix as its starting point: the second-quantised derivation (Eqs. 2–8 of the notes) is not formalised, and together with is defined by the displayed formulas. The band energies are the eigenvalues of , and is the quantity the statements are written in terms of. The Fermi velocity is (units with ).
with , and . The three clauses say, in order, that really are the eigenvalues of the Bloch Hamiltonian, that the two bands touch at the Brillouin-zone corner , and that they disperse linearly and isotropically around it. The goal deliberately asserts the shape of the low-energy dispersion — a first-order expansion, with no quantitative remainder — so it is not invalidated by sharper error estimates.
The milestone list follows the notes equation by equation: the closed form of (Eq. 11), the characteristic polynomial of (Eq. 9), the two explicit forms of the dispersion (Eqs. 12 and 13–14), the Pauli-matrix form of (Eq. 18), the vanishing of at and , the first-order expansions at both Dirac points (Eqs. 22–23 and 30), the spectrum of the linearised Hamiltonians (Eq. 32), and the gap opened by a mass term (Eqs. 33–34).
The three clauses of the goal are what turn a lattice hopping problem into the massless-Dirac-fermion picture used throughout graphene physics: they are the precise sense in which "graphene has Dirac cones at and with Fermi velocity ". Downstream, the same objects carry the valley structure — the two expansions are complex conjugates of one another — and the mass milestone shows how a sublattice-asymmetric on-site potential (boron nitride rather than graphene) opens a gap , the standard model of a gapped Dirac material.
The mathematics is classical and the physics literature regards it as settled; what this mission adds is a machine-checked development in which the honeycomb geometry, the Bloch matrix, its spectrum and the Dirac-point expansions are reusable definitions and lemmas rather than a computation redone by hand. No part of the development is claimed to be new mathematics.
The obstacles are in the analysis, not the algebra. The first two clauses of the goal are a trigonometric identity and a determinant. The third is a genuine differentiability statement, and the naive route — expand , cancel the zeroth-order terms, read off the linear term — has to be carried out uniformly in the direction of ; moreover the quantity being expanded is , a modulus, which is not differentiable at a zero of . The linear behaviour of survives only because the modulus of a function with a nonzero complex-linear differential at a zero is asymptotically the modulus of that differential, and the elementary estimate is what lets the error be transported through the modulus. Note also that itself is not differentiable at — the cone has a vertex there — so no Taylor theorem applies to directly.
Wave vectors and lattice vectors are pairs of reals, . Because that product type carries the sup norm, the Euclidean length is introduced as a separate definition and is the one used in every statement; the little-o statements are taken with respect to the neighbourhood filter of the origin, for which the two norms agree up to constants. is a finite sum over a three-element index set, is a concrete complex matrix, and "eigenvalues" are always expressed through the characteristic polynomial rather than through an eigenvector predicate. Lattice constant and hopping amplitude are real parameters; the standing hypotheses of the goal are exactly and , and several milestones need less. Units are , so .
Two things the formalization deliberately does not do: it does not derive the Bloch Hamiltonian from the second-quantised hopping Hamiltonian (Eqs. 2–8), which would require a Fock-space development, and it does not claim that and are the only zeros of . No statement is vacuous: every hypothesis is satisfiable (take ), and the goal's third clause is a nontrivial asymptotic rather than an identity.
Contributions welcome beyond the milestone list: the second-quantised derivation, the identification of the full zero set of modulo the reciprocal lattice, eigenvector-level (pseudospin) statements, the density of states, and the extension to next-nearest-neighbour hopping.
Which workers end up at which firms, and does higher quality always land at the more productive employer? This is the question of assortative matching: whether an efficient assignment pairs the best workers with the best firms, the second-best with the second-best, and so on down the line. The question has a long history in labor economics. Becker [1973] showed, for the simplest case of two-sided homogeneous firms and a single worker characteristic, that profit maximization under complementarity forces exactly this kind of sorting. Kremer [1993] extended the analysis to firms with many workers of a single type, under a specific Cobb–Douglas production function. What was missing was a general theory: one that covers firms hiring several types of workers simultaneously, firms that differ in efficiency, and labor markets of any degree of tightness, while still deriving sorting from a single primitive economic condition rather than from functional-form assumptions.
Topkis's Chapter 3, §3.2 supplies exactly that theory, as an application of the book's central tool — supermodularity — to the assignment problem. The condition that drives every result in this mission is a single complementarity hypothesis on the firms' profit functions: no concavity, no differentiability, no specific functional form. That a purely order-theoretic hypothesis pins down the qualitative shape of an optimal assignment is the mission's central content, and the platform currently has no lattice-theoretic treatment of matching at all — its one matching result formalizes Gale–Shapley two-sided stable matching by preference, an entirely different mechanism (see Formalization scope below).
Fix worker types, indexed , each with a lattice of available worker qualities, and firms, indexed . A matching assigns to each firm a vector of qualities — one worker of each type hired by that firm (a firm that hires no worker of some type, or several, is accommodated by adjoining an artificial "no worker" element to , or by splitting a type into several, as Topkis notes on p. 97; the model itself needs neither device). If firm hires the quality vector , it earns profit ; the dependence on reflects differences among firms such as technology or management efficiency. A matching is optimal if it maximizes the total profit over every matching.
A matching is increasing if — a single chain, firm by firm, under the pointwise order on — and ordered if every two of its firm-assignments are comparable (a weaker, only pairwise, condition). The labor market is loose if each firm's hiring problem can be solved by unconstrained maximization over the whole quality space , without regard to the other firms' decisions, and tight if the supply of each worker type is exactly , so a feasible matching must assign every available worker to exactly one firm.
The hypothesis common to every result is that is supermodular in the joint variable on : for every and , . By Theorem 2.6.1 of Chapter 2, this is equivalent to having increasing differences both between any two worker types' qualities (complementarity among the worker types) and between each worker type's quality and the firm index (complementarity between quality and firm efficiency).
Existence of an increasing optimal matching, with no loose-market hypothesis — the general case, and the harder of this mission's results to formalize, since its proof is a non-constructive lexicographic-minimization argument rather than a direct reduction to per-firm optimization.
The result gives a clean, hypothesis-light account of assortative matching: sorting by quality is a structural consequence of complementarity in the profit function, not an artifact of a particular production technology. It generalizes Becker's and Kremer's special cases to arbitrarily many worker types, heterogeneous firms, and any degree of labor-market tightness, identifying supermodularity in as the single condition doing all the work. Formalizing it contributes a genuinely new object to the platform: a firm-quality matching model driven by lattice-theoretic complementarity rather than by preference orderings, together with the four distinct comparative-statics conclusions (loose-market optimality, general existence, orderedness, increasingness) that the strength of the supermodularity hypothesis buys. No prior formalized proof of any of these four theorems exists on the platform or, to the author's knowledge, in any other proof assistant library.
The obvious approach — prove the goal (Theorem 3.2.3) by reducing to the loose case, firm by firm, as in Theorem 3.2.1 — does not work, because the loose-market argument crucially uses that each firm's decision does not constrain any other's; without that, a locally optimal per-firm choice need not combine into a globally optimal matching. Topkis's actual proof is non-constructive: among all optimal matchings, pick one that lexicographically minimizes the "latest" failure of the increasing property (a well-ordering argument over the finite but unbounded set of optimal matchings, not an inequality chase), then show that if it still fails to be increasing, exchanging the two offending firms' assignments via strictly increases total profit — contradicting optimality by supermodularity. Formalizing this requires setting up the lexicographic minimization (over pairs ordered by then ) as a well-founded induction, not merely restating the inequality (3.2.3) at the end of the proof.
Worker-type quality spaces are modeled as finite, nonempty lattices (Lattice,
Fintype, Nonempty); firms are indexed by Fin m. A matching is Fin m → ∀ i, X i with no
constraint beyond membership — the general matching problem (3.2.1) imposes no injectivity or
supply constraint on its own, a modeling choice Topkis's own text supports (p. 96: the
"" representation of a matching "may not distinguish between
all distinct assignments of workers to firms if the qualities of different workers of any given
type are not all distinct, but that ambiguity is inconsequential"). Tightness is instead
formalized as an explicit feasibility predicate (a bijection between firms and the available
workers of each type) supplied as a hypothesis exactly where a tight-market theorem needs it,
never folded into the general optimality predicate.
A trivializing formalization to avoid: collapsing Theorem 3.2.4's "ordered" conclusion and
Theorem 3.2.5's "increasing" conclusion into the same statement, or conflating their two
distinct supermodularity hypotheses (joint-non-strict-plus-per-firm-strict versus jointly
strict) — the mission's four milestones are kept as four genuinely different claims with their
own hypotheses, not variations proved once and restated. AGT.stable_matching_exists
(Gale–Shapley) is not reused here, despite the shared word "matching": it produces a
two-sided, preference-based stable matching with no notion of aggregate profit, a mechanism
unrelated to this mission's profit-maximizing, supermodularity-driven assignment.
Reused from earlier missions in this series: the induced set ordering InducedSetOrder
(mission I) and joint supermodularity SupermodularOn (mission II), both published platform
definitions. Contributions most welcome on the goal theorem's lexicographic-minimization
argument, the mission's hardest step.
Two-stage stochastic programs with recourse are already hard to optimize when the recourse problem is a linear program: Chapters 4–6 of this series show how the L-shaped method exploits the recourse function's convexity and polyhedrality to converge finitely by cutting planes. Adding integrality restrictions destroys both properties. Birge and Louveaux open Chapter 7 by naming the consequence directly: "properties of stochastic integer programs are scarce," duality is lost, and the recourse value for even a single first-stage point may itself require solving an integer program from scratch, with no warm start available across scenarios (Birge & Louveaux, Introduction to Stochastic Programming, 2nd ed., Springer 2011, p. 290).
Section 7.2 isolates the one structural feature that still buys finite convergence: first-stage variables restricted to . Laporte and Louveaux's Integer L-shaped method (1993) exploits this by combining a branch-and-bound search over the finitely many binary first-stage points with a new family of optimality cuts, valid wherever a finite lower bound on the recourse value is available. This mission formalizes that method's specification and its finite-convergence guarantee, together with the two propositions its proof rests on.
A stochastic integer program (SIP) extends a two-stage stochastic linear program with fixed
recourse (Chapter 3's Recourse.Instance: first-stage data , fixed recourse matrix ,
and scenarios of with probabilities ) by two further restrictions:
where restricts the first stage and restricts the recourse variable — typically requiring
integrality of . Section 7.2's standing hypothesis narrows further: every coordinate of
is binary. Write for the resulting recourse value (a possibly-infinite expectation, by
the same convention as the continuous case) and for the value of the continuous
relaxation, obtained by dropping the restriction and keeping only — exactly the
recourse value Chapter 3's Recourse.Instance already computes.
The method needs one further hypothesis, Assumption 2: a finite lower bound with , not required to be tight. For a subset of the first-stage index set, write , and let be the binary point with for , otherwise — measures how far a binary point is from matching exactly, reaching its maximum only at .
Any L-shaped optimality cut valid for the continuous relaxation's value remains valid for the true, integrality-restricted recourse value, since pointwise.
is a valid lower bound on for every binary first-stage-feasible , given a binary feasible point with true recourse value and a lower bound satisfying Assumption 2.
Under Assumption 2, the Integer L-shaped method — the branch-and-bound search over binary first-stage points, tightened at each iteration by a fresh cut of the Proposition 3 form — finitely converges to an optimal solution of an SIP with relatively complete recourse and binary first-stage variables, when one exists. "Finitely" is quantified explicitly: a bound of on the number of iterations, the number of distinct binary first-stage points.
Proposition 4 is the chapter's payoff: it turns "solve an SIP with binary first-stage variables" from an open-ended search into a procedure with a certified stopping point, at the cost of one additional hypothesis (a computable lower bound ) that is often easy to obtain by relaxing the second-stage integrality restriction, as the book's Example 1 illustrates directly. Propositions 1 and 3 are the two soundness facts the method's cuts rest on: Proposition 1 lets an implementation reuse the continuous L-shaped method's own optimality cuts as valid (if weaker) constraints, and Proposition 3 supplies the chapter's genuinely new cut, tailored to the binary structure and strong enough by itself to guarantee termination.
Formalizing this mission fixes, machine-checkably, the exact hypotheses under which the method is correct — in particular, that "binary" is load-bearing (the finiteness bound is literally ) and that "relatively complete recourse" cannot be dropped, since it is what keeps the recourse value from becoming at a feasible point. No result here has, to the mission's knowledge, been formalized elsewhere; the propositions and the method's specification are drafted fresh.
The recourse function is neither convex nor polyhedral once is integer-restricted, so the argument cannot follow the continuous L-shaped method's proof line for line — that proof leans on 's convexity to certify a cut from finitely many bases. Proposition 3's cut instead argues purely combinatorially: for every binary , with equality forcing , so the cut's right-hand side collapses to the true value exactly there and falls to at most everywhere else — a fact about the finitely many binary points of , not about 's analytic structure. The natural first idea, adapting a continuous L-shaped cut by simply restricting its domain to binary , fails: nothing forces such a cut to be tight at the current iterate, so it need not exclude a revisited point, and finite convergence (the content Proposition 4 actually asserts, not just "an optimum exists") would be lost.
The mission represents first-stage points as Fin n1 → ℝ with a Binary predicate
(∀ i, x i = 0 ∨ x i = 1) rather than a Fin n1 → Bool type, so that the master problem's
feasible region and its binary-restricted subset share one ambient space, matching how the book
moves between and its binary points. The second-stage restriction is left an arbitrary
Set (Fin n2 → ℝ); taking it to be all of recovers exactly Chapter 3's continuous
recourse value, without a second definition. Flagged (moderator review, 2026-09-19):
Proposition 1's own is the book's -based continuous/LP-relaxation of
(Eq. (1.3)-(1.4)), which can retain bounds imposes beyond integrality — the book's own
worked example on the same page gives binary , so , not
alone. This mission's prop1_cuts_valid_for_sip uses the dropped- relaxation
(only ) rather than , which coincides with the book's only when
is itself an unbounded integrality restriction; the theorem is a narrower result than the
book's Proposition 1 whenever carries additional structure, though it remains true as
stated because the dropped- value is unconditionally the book's -based
, which is itself — see the item's own Formalization Note for the full
argument. The existential lower bound of Assumption 2 is kept a bare existentially-quantified real, never
sharpened to a formula, matching the book's own "no requirement is made that the bound should
be tight."
The Integer L-shaped method's branch-and-bound bookkeeping (Steps 0, 1, 3, 4: pendant-node list management, bound-based fathoming, and branching on a violated integrality restriction) is abstracted into a direct optimization over the binary first-stage feasible set at each iteration, since Proposition 3's cut is proved valid there without appeal to any specific branching order — the same level of abstraction the Chapter 5 mission uses for the continuous L-shaped method's own master-problem bookkeeping. What is retained explicitly is the part the finiteness bound actually depends on: Step 5's recourse-value computation and Step 6's binary choice between fathoming and adding a fresh cut, modeled as a state machine whose state is the finite set of binary points already excluded by a cut. A formalization that dropped this state machine — asserting only "if Assumption 2 and relatively complete recourse hold, an optimal solution exists" — would trivialize the proposition's actual content, the finite bound on the number of steps; this mission keeps that bound as an explicit, checkable part of the goal statement.
Definitions reused from earlier missions in this series: StochasticProg.Recourse.Instance
(Chapter 3) for the underlying two-stage recourse data and its continuous-relaxation value.
Contributions welcome on strengthening Proposition 4's proof to also derive Proposition 3 as a
lemma, and on formalizing the improved cuts of Propositions 5–7 (out of scope here, left for a
possible follow-up mission).
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.
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.
A network of resistors solves an optimization problem. Nobody tells the electrons what to do; each one moves under a purely local rule, and the current distribution that emerges minimizes energy dissipation over all distributions satisfying Kirchhoff's node law. Add a wire and the network can only become easier to traverse. This is the encouraging case, and Chapter 4 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) opens with it.
Road traffic is the discouraging case. Drivers also follow a local rule — take the fastest route — and the pattern that emerges is again characterized by an optimization problem, but not the one anyone wants solved. Braess's paradox is the sharp form of the discrepancy: in a small road network carrying six cars per unit time, every route takes 83 time units at equilibrium; open an extra road, and at the new equilibrium every route takes 92. Building road capacity made everyone slower. The difference from the electrical case is that a driver's choice imposes a delay on everyone else sharing the road and the driver does not pay for it, and correcting that — pricing the externality — is how a decentralized rule can be made to produce good global behaviour. That idea recurs in Chapters 7 and 8 of the book as the basis of Internet congestion control.
The network is a set of directed links. A route is a subset of links, and is the set of routes under consideration — not necessarily all physically possible ones. The link-route incidence matrix has when and otherwise. Writing for the flow on route , the flow on link is
Each link has a delay function , continuous and increasing in the flow on that link, and the delay along a route is the sum of the delays of its links, . Drivers care only about getting from origin to destination: is the set of source–destination pairs, each route serves exactly one of them, written , and the flow requirement between pair is .
A routing pattern is stable when no driver has an incentive to switch. Definition 4.2 makes this precise: a Wardrop equilibrium is a feasible vector of route flows such that
Every route actually carrying traffic is a shortest route, in delay, for the traffic it carries.
The goal asserts existence only, for an arbitrary network, arbitrary route set and arbitrary continuous increasing delay functions. It fixes no uniqueness claim, because the equilibrium flows need not be unique even though the link loads are, and no efficiency claim, because Braess's paradox is precisely the statement that the equilibrium is not efficient.
Kirchhoff's node law as the equations satisfied by the expected reward in the random-walk game of section 4.1; the two Braess networks of Figures 4.4a and 4.4b, with their equilibrium delays and ; convexity of for increasing ; the optimization characterization that makes the goal reachable — a minimizer of over the feasible flows is a Wardrop equilibrium; and the exact externality decomposition of the queueing network of section 4.3.1.
The result itself. Theorem 4.3 is what makes the Wardrop equilibrium a usable object: a traffic model that could fail to have an equilibrium would be describing nothing. Its proof does more than establish existence — it identifies the equilibrium as the solution of a specific convex program, minimizing . That function is not the total delay , and the gap between the two is exactly Braess's paradox: selfish routing optimizes the wrong objective. Once the two objectives are written side by side, the fix is readable off them, and it is the fix used in practice — a toll on link equal to , the marginal delay a driver imposes on everyone else, makes the selfish objective coincide with the social one. Section 4.3 then carries the same accounting into queueing and loss networks, where the derivative of the mean cost splits into a term for the delay a customer suffers and a term for the knock-on cost it inflicts.
Formalizing it. Nothing here is open; Wardrop stated the principle in 1952 and Beckmann, McGuire and Winsten gave the optimization formulation in 1956. What the mission produces is a machine-checked model of selfish routing — incidence matrix, link flows, delay functions, the equilibrium condition — and a formal record of Braess's paradox as a concrete pair of networks rather than a story. Mathlib has no traffic or congestion-game theory.
Existence is not a fixed-point argument in the obvious variable: the best-response map of the routing game is not continuous, since a small change in flows can flip which route is shortest and move all the traffic. The book's route is to replace the equilibrium condition by the stationarity conditions of a convex program on a compact feasible set, where existence is routine and the content is the translation. The translation is where the care is needed, and it is stated here as a separate milestone: the first-order conditions say the Lagrange multiplier equals the route delay on routes carrying traffic and is a lower bound on the others, which is Definition 4.2 restated.
The subtlety worth naming in advance is that "increasing" is doing real work in two different places. It makes convex, which is what makes the program tractable; and it is what makes each interpretable as a price. Neither convexity of itself nor strict monotonicity is needed, and assuming them would be assuming more than the book does.
Links, routes and source–destination pairs are indexed by finite types. The incidence matrix is real-valued with entries constrained to be or , matching the book's definition in this chapter (unlike Chapter 3, which allows general non-negative integers). The map from routes to source–destination pairs is given as a function rather than as the matrix , which is exactly the book's statement that each column of sums to .
Delay functions are total functions , continuous and monotone. This excludes the vertical asymptote that Figure 4.5 permits — a link with a finite capacity at which delay blows up — and that restriction is recorded here rather than left implicit. The equilibrium condition is stated as the inequality " for every serving the same pair", which is Definition 4.2 with the minimum written out; the two are equivalent because itself serves , and the inequality form avoids having to produce a minimum over a possibly empty set.
The goal is not vacuous: the feasibility hypotheses (, and each source–destination pair served by at least one route) are exactly what makes the feasible set non-empty, and without them the existence claim would be false rather than trivial.
Contributions welcome beyond the listed items: uniqueness of the equilibrium link loads ; the marginal-cost toll that aligns the selfish and social optima; Rayleigh monotonicity (Exercise 4.3, that effective resistance does not decrease when a resistance is increased); the price of anarchy for affine delays; and Theorem 4.6 on the derivatives of the loss-network rate of return with respect to offered traffic and capacity.
A queueing network is a collection of service stations through which customers — jobs, packets, telephone calls, patients — move one at a time. The state of such a network is a vector of occupancy counts, one per station, and the number of states grows exponentially in the number of stations, so solving the equilibrium equations directly is hopeless for any network worth modelling. The product form is what rescues the subject: for a large and identifiable class of networks the equilibrium distribution factorizes into one term per station, as if the stations were independent, and a network of stations costs one-dimensional calculations instead of one exponentially large one.
Chapter 2 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014) establishes this for migration processes, the Markov model in which individuals move between colonies one at a time at a rate that factorizes as : a part depending only on the two colonies and a part depending only on the occupancy of the source. The class covers single-server and -server queues, infinite-server queues, and networks of them, open or closed.
There are colonies, and a state is a vector of non-negative integers, being the number of individuals in colony . Three operators move one individual:
An open migration process is the Markov process on with transition rates
where : nothing leaves an empty colony. Immigration into colony is Poisson of rate . Taking and and restricting to states of a fixed total gives a closed migration process. Setting models an -server queue at colony ; models individuals moving independently.
The traffic equations define from the rates. In the open case they are
and in the closed case with and . Finally set
If then
is an equilibrium distribution: it satisfies the equilibrium equations for the open migration rates, and it sums to one over . Both halves are asserted, because the first alone is satisfied by every positive multiple of and the second is what makes the convergence hypothesis do work.
The closed-network product form of Theorem 2.4; the two families of partial balance equations (2.3) and (2.4) that the proof reduces to; Theorem 2.9, that the time reversal of a stationary open migration process is again an open migration process with rates , and ; the single M/M/1 queue that the chapter starts from; the cycle identity (2.6) behind Little's law; and the traffic equations of Kendall's family-size process, an open migration process with infinitely many colonies.
The result itself. Theorem 2.8 says that at a fixed time the occupancies of an open migration network are independent, each distributed as if its colony were fed by a Poisson stream of rate — even though the actual arrival stream into a colony is in general not Poisson, and the occupancies are emphatically not independent as processes. That gap between the one-time-marginal and the process is the reason the theorem is useful and the reason it is easy to misapply. Everything downstream in the book rests on it: the loss networks of Chapter 3 are the truncation of a product-form process to a capacity set, and the flow-level models of Chapter 8 ask when a product form survives a bandwidth-sharing policy. Theorem 2.9 supplies the reversibility argument from which Burke's theorem and the Poisson character of the exit streams follow.
Formalizing it. The mathematics is classical — Jackson (1957), Whittle (1968), Kelly (1979) —
and none of it is open. What the mission produces is a machine-checked model of a queueing
network: the migration operators, the rate matrix, the traffic equations and the product form, in
a form later missions in this series import rather than restate. Mathlib has no queueing theory
and no theory of continuous-time Markov chains on a countable state space, so this is the first
such development. It builds on the DetailedBalance / FullBalance layer published in mission I.
An open migration process is not reversible — the detailed balance equations fail, as Figure 2.5 of the book shows with an arrival stream of geometrically sized bursts — so the method of Chapter 1 does not apply and the equilibrium equations must be met head on. The content of the proof is that they split: a separate balance holds for each colony (rate of individuals leaving colony equals rate arriving into it) and one more across the boundary with the outside world, and each of those is equivalent to a traffic equation. Finding that split is the step, and it is why the partial balance equations are milestones in their own right.
The formal obstacle is different and worth naming. The equilibrium equation at a state sums over the states that can jump into , and the naive transcription silently assumes is a state, which fails when . Over such a term must be dropped, and a formalization that keeps it — with read as truncated subtraction — states something false.
The state space is Fin J → ℕ, a function from a finite index type of colonies to occupancy
counts, with J finite; no irreducibility is assumed, since none of the statements below need it.
Rates are real-valued and the whole rate matrix is a single function of two states, assembled as a
sum of indicator terms over the possible transitions, so the equilibrium equations can be stated
as the FullBalance predicate of mission I, with unconditional sums over the countable state
space. This is what avoids the trap above: a sum over actual states never includes a
would-be-negative one, and any spurious coincidence of operators at a boundary carries a
factor and contributes nothing.
Conventions the development commits to: , so a transfer is always between distinct
colonies; and for ; ; and is asserted
via HasSum, which states convergence and the value at once, rather than as an extended real that
might be infinite. Occupancy vectors use truncated natural subtraction, so the partial balance and
reversed-rate statements carry an explicit where the book's state space carries it
implicitly; the goal itself does not need such a guard.
A trivializing formalization is ruled out by the second conjunct of the goal: the equilibrium equations alone are a homogeneous linear condition satisfied by , whereas the requirement that sum to forces the constants to be exactly the ones stated.
Contributions welcome beyond the listed items: Burke's theorem (2.1) and the Poisson character of the exit streams, Corollary 2.10, the closed-form of the telephone banking example (Exercise 2.6), the Chinese restaurant process of Exercise 2.13, and Bartlett's theorem (2.17) on linear migration processes over a general space.
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.