Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The Standard Model of particle physics assigns to each elementary fermion a vector in a representation of the compact Lie group . The pattern of hypercharges this forces on quarks and leptons looks arbitrary. Three grand unified theories from the mid 1970s explain the pattern by enlarging the symmetry group: Georgi and Glashow's theory, Georgi's theory, and the Pati-Salam model based on .
Baez and Huerta, The Algebra of Grand Unified Theories (2011), isolates the part of this story that is pure algebra: homomorphisms out of , their kernels and images, and the way the three unified groups sit inside one another. This mission formalizes that group theoretic core. It deliberately leaves out the representation theoretic half of the paper (the exterior algebra , the binary codes, the Dirac spinor representations), which is a natural follow-up mission.
Write for the group of complex numbers of modulus one, and for the complex matrices with and . The Standard Model gauge group is the product
Fix the splitting and write matrices in in the corresponding block form. The Georgi-Glashow homomorphism is
where means the scalar times the matrix . Fixing instead the splitting (colour plus lepton number), the Pati-Salam homomorphism is
Finally, forgetting the complex structure of gives a real inner product space , and every complex-linear map becomes a real-linear one. Writing each complex coordinate as a pair of real coordinates turns a complex matrix into a real matrix , built from the blocks . Under , the splitting becomes .
Concretely: a real matrix is simultaneously (i) the realification of some and (ii) block diagonal with blocks in and , if and only if for some . The image of is a copy of , which is why this is the statement of Theorem 8; the quotient itself never has to be formed.
The milestones establish, in order: that is a homomorphism into ; that its kernel is exactly , a group of order six; that its image is the subgroup of preserving the splitting; the same programme for the Pati-Salam homomorphism , whose kernel turns out to have order three; that realification is an injective homomorphism carrying into ; and the diagram chase by which Theorem 9 (p. 69) upgrades Theorem 8 from to .
The kernel computation is what makes the theory testable at the level of algebra: because is nontrivial, no representation coming from can distinguish the six elements of that kernel, so the Standard Model representation must be trivial on them — a nontrivial relation between hypercharge, isospin and colour that the observed fermions do satisfy. The intersection theorem says the Standard Model group is not merely contained in both unified theories: inside it is precisely their intersection, so the two routes to unification determine it exactly.
Formalizing this produces reusable Lean infrastructure for classical matrix groups: block decompositions of , the subgroup , and the realification homomorphism with its determinant and orthogonality properties, none of which is currently available off the shelf. The mathematics is classical and fully proved in the source; what is open here is only the formalization.
The obvious first move — " is visibly a homomorphism, so quotient by its kernel and apply the first isomorphism theorem" — settles the milestones but not the goal. The goal compares two subgroups of that are defined by different structures: one by preserving a complex structure and a volume form, the other by preserving a splitting of the real space. Showing the intersection is no larger than the image of requires knowing that a real matrix commuting with the complex structure and respecting the real splitting must respect the complex splitting, and that the determinant conditions then match up exactly; the surjectivity half needs a sixth root of the determinant of the block to exist inside .
Theorem 9 is a second, independent difficulty: and its double cover of are not available in the current Lean library, so the milestone states the diagram chase of the published proof with the covering data as hypotheses rather than constructing .
The Lean development commits to the following conventions.
fromBlocks. Likewise is indexed by .No statement is vacuous: every milestone is universally quantified over the whole group, the goal is an equivalence between two nonempty subsets of (both contain the identity), and the hypotheses of the Theorem 9 milestone are satisfied by the real data of the source.
Contributions welcome beyond the milestones: constructing and its covering map so Theorem 9 can be stated unconditionally, and the representation theoretic half of the paper (Theorems 1-7), which needs and the Dirac spinor representations.
Chapter 9 asks whether the support vector machine — a regularized empirical risk minimizer over an RKHS — is a statistically consistent estimator for regression: does as the sample size , for a suitable regularization schedule ? The chapter's main theorem (Theorem 9.1) answers yes, under an explicit polynomial rate condition on . Its proof reduces the question to bounding how far the empirical regularized solution can be from the population regularized solution, and that reduction bottoms out in a single concentration-of-measure fact: how tightly does an empirical mean of i.i.d. Hilbert-space-valued random variables concentrate around its true mean, given only a bound on one -th moment (no exponential-moment assumption at all)? That fact is Lemma 9.2, "the following lemma to bound the probability of for " — the technical core the whole chapter's consistency argument rests on, and this mission's goal.
Fix a measurable space , a distribution on , a separable Hilbert space , and a measurable . Its -th moment norm, for , is — the direct Hilbert-space analogue of an ordinary norm. The proof machinery behind concentration results of this kind is symmetrization: replacing a centered i.i.d. sum by a Rademacher-randomized sum , where a Rademacher sequence is a family of independent -valued random variables, each taking each sign with probability . Once randomized, the sum's -norms (for different ) become comparable to each other via Kahane's inequality, with a universal constant depending only on the two exponents involved — never on the sample size or the ambient Banach space.
for a universal constant depending only on , every and every . This is a genuine generalization of Chebyshev's inequality to Hilbert-space-valued means, sharp enough (via the explicit rate ) to drive Theorem 9.1's own polynomial regularization condition .
Theorem 9.1 itself (BRIEF.md's recommended goal — the full SVM-regression consistency theorem)
was not attempted this session; see STATUS.md for the reason and the fallback taken instead.
Lemma 9.2 is stated and proved once, in the Appendix's general Rademacher-sequence toolkit and this chapter, and then used directly to obtain Theorem 9.1's consistency guarantee: substituting the pointwise SVM "difference process" into Lemma 9.2 converts a purely probabilistic concentration fact into a statement about how close the empirical SVM solution's risk is to the population solution's risk, for every sample size. Because the bound depends on nothing but a single moment — no boundedness, no sub-Gaussian tail — it is what lets Theorem 9.1 avoid assuming the loss or the label distribution has any exponential tail control, which is essential for regression (where need not be bounded, unlike the classification setting of this series' earlier chapters). Symmetrization and Kahane's inequality are themselves standard, reusable tools of empirical process theory (used throughout Chapter 7's entropy-number program, excluded from this series, and Chapter 6's classification oracle inequality).
The published proof of Lemma 9.2 is a short but dense computation: Markov's inequality reduces the tail bound to bounding for the centered mean ; Theorem A.8.1 symmetrizes; for , Theorem A.8.3 (Kahane) converts the -th moment of the Rademacher sum to its second moment, which an explicit orthogonality computation (the book's Eq. (9.4), for any fixed , an immediate consequence of the Rademacher signs' independence and the Hilbert space's parallelogram identity) reduces to a sum of individual second moments; the case argues analogously with a different exponent split. None of this computation is captured by this mission's two milestones alone — they supply the two cited theorems, not the connecting algebra — so a complete proof of the goal from the milestones as stated still requires reconstructing this argument, exactly as the captain brief's milestones are meant to be (the book's own attack path, not a fully mechanized proof outline).
and (the Rademacher sequence's own probability space) are arbitrary measurable
spaces; is [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [MeasurableSpace H] [BorelSpace H] [SeparableSpace H] (a separable real Hilbert space with its Borel
-algebra), matching " be a separable Hilbert space" without narrowing to a concrete
space (e.g. ) the book itself does not assume. IsRademacherSequence states independence
via Mathlib's iIndepFun and the -probability- condition directly, since no ready-made
"Rademacher distribution" object exists in this Mathlib revision (checked by search). is substituted algebraically rather than introducing a separate conjugate
exponent , since pins down uniquely — not a change of content. In Theorem
A.8.3, "for all Banach spaces " quantifies over E : Type (the Type 0 universe) rather than
every universe Type*, a disclosed minor restriction with no effect on this mission's own use of
the theorem (with instantiated to a Type* Hilbert space that is, in every actual
application, itself at the Type level).
A trivializing formalization here would drop the "independent" half of IsRademacherSequence
(leaving only the marginal -probability- condition, true even for perfectly correlated
signs) or drop the "i.i.d." qualifier on in Theorem A.8.1 (both symmetrization
and Kahane's inequality are false, or at least unproven by the book's own argument, without
independence) — both are ruled out here by stating iIndepFun explicitly rather than only the
marginal distribution conditions.
IsRademacherSequence is reusable beyond this mission: any future formalization of Chapter 7's
entropy-number/Rademacher-complexity program, or of Chapter 6's oracle inequality's own use of
Rademacher averages, would restate it locally (per Hard Rule 9) from the same book definition.
Contributions completing the three sorrys are welcome; Theorem 9.1 itself remains a natural,
substantially larger follow-up mission built on top of this one's two milestones together with
the RKHS/regularized-risk-minimizer apparatus already available in this series' 04-representer
mission (restated locally, per Hard Rule 9).
Chapters III and IV formalize what it means for one random variable to be "more spread out" or "larger and more spread out" than another. Chapter VIII asks a different kind of question: if the number of terms in a sum of i.i.d. random variables is itself random, and one count is larger than another in one of these orders, does the resulting random sum inherit the comparison? This mission formalizes the chapter's own answer — Theorem 8.A.13 — a clean, self-contained closure result that needs only the icx/icv/cx orders from Chunks 03/04 (restated locally) and one nonnegative-integer-valued index, without the heavier parametric-family apparatus (SICX, SICV, SIL, and the stochastic-convexity-of-a-family notions) that occupies most of the rest of the chapter.
This chapter restates the univariate increasing convex, increasing concave and convex orders (Chunks 04 and 03's own subjects) locally, since drafts cannot import another mission's definitions: for random variables , [] if for every increasing convex [concave] for which the expectations exist, and if the same holds for every convex (dropping "increasing"). Theorem 8.A.13 applies these same three orders to nonnegative-integer-valued random variables — a special case of the real-valued order (after the coercion ), not a separate discrete order, per this chapter's own pitfall 1.
Let be i.i.d. nonnegative random variables, independent of the two nonnegative discrete random variables and . Then
Comparing the number of terms propagates to a comparison of the resulting random sums. This is
"an application of these notions in establishing a stochastic inequality," in the book's own
words right before the theorem — the formal content behind Example 8.A.2's claim that a
homogeneous Poisson process is SIL, via the semigroup property of Example 8.A.7 (neither a
numbered theorem, so neither is drafted as a milestone here — cited as background only, per
CAPTAIN_BRIEF.md rule 5).
The book's proof defines for an increasing convex [concave] and observes (via the unnumbered Example 8.A.4) that is itself increasing and convex [concave] in ; the icx/icv order on then transfers directly to vs. , giving part (a). Part (b) follows from part (a) together with the equal-means fact under (Theorem 4.A.35, a Chapter 4 result not restated in this mission).
Random sums are the natural model for aggregate risk, total service time, or total demand when the number of contributing terms is itself uncertain — the number of claims in an insurance period, the number of customers served, the number of jobs in a batch. Theorem 8.A.13 is the tool that lets an analyst reduce a comparison of two such aggregates to a comparison of the (often much simpler) counting processes that generate them, without having to reason about the joint distribution of the sums directly. It is also the concrete instance, stripped of the rest of the chapter's parametric-family machinery, of a pattern that recurs throughout the book: an order on an index set (here, the count vs. ) transferring through a monotone/convex construction (here, summation) to an order on the resulting random variables — the same shape Chunk 06's Theorem 6.B.16(b) and Chunk 07's Theorem 7.A.9 each illustrate in their own settings.
No platform prior art exists: GET /theorems?q=random+sum, q=compound+distribution,
q=Poisson+process, and q=renewal return nothing usable (the last returns only
MarkovMixing/CLT-adjacent hits, not classical renewal or compound-sum results, confirmed at
triage time and re-checked this session). This mission restates the icx/icv/cx orders and their
random-sum closure as a self-contained result, independently drafted since drafts cannot import
Chunks 03/04's Lean.
The chief formalization risk is treating as a separate "discrete" order rather than
the same real-valued order applied to -valued random variables after coercion — this
chapter's own pitfall 1. A second risk is drafting as a fixed-length sum with
substituted in afterward, rather than a genuine random (randomly-stopped) sum where is
itself random and independent of the sequence — this chapter's own pitfall 2; the
independence hypothesis has to be carried explicitly, not left as an unstated convention. A third
risk, common to every bracketed theorem in this series, is conflating the icx and icv cases of
part (a) into a single Or-joined statement rather than two clearly distinguished conjuncts —
this chapter's own pitfall 3.
A different kind of risk, specific to this chapter, is scope creep into the parametric-family
apparatus (SI, SCX, SICX, SIL, and the "family indexed by " definitions) that
occupies most of Chapter 8: as BRIEF.md's own Setup note observes, that apparatus is heavier
than the rest of the book (a family, a parameter set, and several bracketed cases per
definition), and a trivializing risk specific to it — flagged in this chapter's pitfall 4 — is a
family predicate that is vacuously true for a degenerate parametrization (e.g. a
singleton). This mission avoids that risk entirely by choosing the one clean, self-contained
closure theorem in the chapter that needs none of it.
The icx/icv/cx orders are restated locally (IcxOrder, IcvOrder, ConvexOrder, univariate,
real-valued), exactly matching Chunks 04 and 03's own shapes, since drafts cannot import another
mission's definitions. are nonnegative-integer-valued; the orders are
applied to them via the coercion fun ω => (M ω : ℝ) (resp. N), matching pitfall 1 exactly —
no separate discrete-order predicate is introduced. The i.i.d. sequence is drafted as
Y : ℕ → Ω → ℝ (indexing Y 0, Y 1, … for the book's Y_1, Y_2, …, a one-step reindexing noted
explicitly rather than left implicit), with iIndepFun Y μ for mutual independence and
IdentDistrib (Y j) (Y k) μ μ for every j, k for identical distribution, plus 0 ≤ᵐ[μ] Y k for
nonnegativity. The random sum itself is ∑ k ∈ Finset.range (M ω), Y k ω — a genuine
randomly-stopped sum, per pitfall 2 — and independence of from jointly is
IndepFun (fun ω => (M ω, N ω)) (fun ω k => Y k ω) μ, treating the whole sequence as one
ℕ → ℝ-valued random element, stated as an explicit hypothesis rather than an implicit
convention. The theorem's three conjuncts (icx, icv, cx) mirror the book's own single Theorem
8.A.13, whose part (a) bundles the icx/icv brackets and whose part (b) states the cx case
separately, per pitfall 3.
A trivializing formalization this mission rules out: substituting M into a fixed-length
Finset.range n sum after the fact (erasing the random-stopping structure that makes this a
random-sum theorem at all) rather than genuinely summing over Finset.range (M ω), and treating
M ≤icx N as anything other than the same real-valued order Chunks 03/04 define, applied after
coercion. This mission draws on no platform prior art (searches for "random sum", "compound
distribution", "Poisson process" and "renewal" as of 2026-09-18 return nothing usable). Unlike
every other chapter in this series so far, this mission has no milestone theorems: every
other numbered result near the goal in this chapter needs the parametric-family apparatus this
mission deliberately avoids, and the un-numbered facts the goal's own proof cites (Example
8.A.4's potential-function monotonicity, Example 8.A.7's semigroup property) cannot be milestones
per CAPTAIN_BRIEF.md rule 5 — see STATUS.md for the full accounting.
StochasticOrders.Convex) and Chunk 04 (StochasticOrders.MonotoneConvex),
for the univariate convex and increasing convex/concave orders this chapter restates locally.Compressed sensing asks a question that looks impossible at first: can a signal be reconstructed exactly from far fewer than linear measurements , ? Classical linear algebra says no — an underdetermined system has infinitely many solutions. But if is known in advance to be sparse (most of its coordinates are zero), the extra structure makes recovery possible: solving the convex program that minimizes the norm of a candidate solution, subject to matching the measurements, recovers exactly, for a measurement matrix with a suitable geometric property. This idea, developed by Candès, Romberg, Tao and Donoho in the mid-2000s, underlies modern MRI acceleration, single-pixel cameras, and sparse signal processing generally.
The chapter isolates the exact geometric property a measurement matrix needs — the restricted isometry property (RIP) — and proves, purely by linear algebra with no probability involved, that RIP alone is sufficient for exact recovery by minimization. (A companion result, outside this mission, shows random sub-gaussian matrices satisfy RIP with high probability once is large enough, which is what makes the deterministic guarantee here practically useful; this mission formalizes the deterministic half.)
For a vector indexed by a finite set, write for its number of non-zero coordinates (so is -sparse if ), for its norm, and for its Euclidean norm.
An matrix satisfies the restricted isometry property (RIP) with parameters if
i.e. acts as an approximate isometry on every -sparse vector — equivalently (the book's own Exercise 10.5.9), the singular values of every column-submatrix of lie in .
Given a matrix and measurements for an unknown sparse , the exact-recovery program is
precisely: suppose satisfies RIP with parameters where ; then for every -sparse , every that is feasible () and -optimal among feasible vectors satisfies . No constant here is hard-coded beyond the book's own explicit threshold — the weakest stable form of the claim.
RIP isolates exactly the geometric mechanism that makes -minimization work for sparse recovery: once a matrix is known to satisfy it, exact recovery is a deterministic, provable consequence with no appeal to randomness, no failure probability, and no measurement-count formula to verify beyond the RIP parameters themselves. This clean separation — a purely geometric sufficient condition (RIP), proved separately (in the book's Theorem 10.5.11, outside this mission) to hold with high probability for random sub-gaussian matrices — is the template compressed sensing theory follows throughout: geometric/deterministic guarantee first, probabilistic verification that random constructions meet it second. The theorem is one of the two standard routes (with the direct probabilistic argument of Theorem 10.5.1) to the chapter's central claim that measurements suffice to recover any -sparse signal in — exponentially fewer than the measurements a naive linear-algebraic argument would need.
The result itself, and the RIP framework, are classical and well-established (Candès-Tao 2005). This mission formalizes the deterministic linear-algebra core of the argument — the statement infrastructure (RIP, sparsity, the exact-recovery program stated as an explicit optimization problem) and the goal theorem — for a solver to close with a proof.
The natural first idea for showing is to try to bound the recovery error directly using (which vanishes, since both and are feasible) together with RIP applied to itself — but need not be sparse at all: it is the difference of two sparse-ish vectors and can have full support. The actual argument decomposes 's support into blocks by descending magnitude (the support of , then the largest remaining coordinates , then the next , and so on), applies RIP only to the leading block (which genuinely has bounded sparsity ), and separately bounds the contribution of every later block using the fact that is -optimal (so , the "cone constraint"): each later block's norm is controlled by the mass of the previous block divided by its size. This is a genuinely multi-step argument combining a purely geometric fact (RIP on one bounded-sparsity block) with a purely combinatorial one (the magnitude-sorted decomposition), and the "obvious" idea of applying RIP to as a whole does not typecheck, since RIP says nothing about vectors with more than non-zero entries.
Vectors are plain functions ι → ℝ on a finite index type, not EuclideanSpace ℝ ι: the latter's
fixed norm instance cannot also host the norm the program's objective needs, so
both norms (L2Norm, L1Norm) are defined directly by their defining sums on the same underlying
type. Sparsity (Sparsity) takes a real-valued threshold s : ℝ, matching that the RIP parameter
used by the goal theorem is a real number even at integer base sparsity. A solution
"of the program" is formalized as an explicit argmin membership — feasibility
(A.mulVec xhat = A.mulVec x) conjoined with optimality over the exact feasible set
(∀ x', A.mulVec x' = A.mulVec x → l1Norm xhat ≤ l1Norm x') — never "there exists an estimator
such that", the trivialization risk this chapter's own triage brief flags explicitly (shared with
Chapter 3's Max-Cut): an existential reading would prove a different, strictly weaker statement.
The conclusion is stated for every such , not one witness, matching that RIP forces
uniqueness.
This mission covers Theorem 10.5.10 only, as the sole item; the probabilistic goal Theorem 10.5.1
(exact recovery for random sub-gaussian measurement matrices, which needs Theorem 10.5.10 together
with a separate probabilistic argument, Theorem 10.5.11, that random matrices satisfy RIP), and the
Lasso guarantee (Theorem 10.6.1), are both left out for lack of session time: each would need a
fresh probabilistic apparatus (independent isotropic sub-gaussian random rows, a failure-probability
bound) built from scratch in this chapter's own sub-namespace, with no reusable published
definition from an earlier chunk. L2Norm, L1Norm, Sparsity and RIP are reusable by any
later chapter or mission needing sparse vectors or the restricted isometry property; solvers'
contributions are welcome on completing the proof of Theorem 10.5.10 itself (the magnitude-sorted
support decomposition sketched under Difficulty above), and, beyond this mission's current scope,
on Theorem 10.5.11 and Theorem 10.5.1.
A cooperative game with side payments models a set of economic agents who can form coalitions and split the proceeds. The central question is stability: is there a way to split the total payoff among all the players so that no subset of them would do better by breaking away and acting on its own? The set of such stable splits is the core, introduced by Gillies [1959] and studied extensively since (Shapley [1971], Shapley [1953]). Sharkey [1982c] surveys the core's role in the economics of natural monopoly, where "no coalition wants to secede" is exactly the condition that a cost-sharing scheme is defensible against any subgroup of customers.
The core of an arbitrary cooperative game can be empty — there may be no split that satisfies every coalition simultaneously — and even when nonempty it can be hard to exhibit a point in it, since it is cut out by linear inequalities. Shapley [1971] identified a large and economically natural class, the convex games (characteristic functions that are supermodular in the coalition), for which the core is always nonempty, and for which an explicit family of core points — one per ordering of the players — can be written down directly. This mission formalizes Shapley's theorem and its later sharpening: this book's central result of Chapter 5, together with a genuine converse (Moulin [1990], sharpening an observation of Sharkey [1982a]) and comparative-statics theorem (Topkis [1987]) showing how these core points move as the underlying economics changes.
Fix a finite set of players . A characteristic function assigns a real number to every coalition , with ; is the net return a coalition could earn on its own. The pair is a cooperative game, and throughout this chapter is assumed superadditive: for disjoint . A payoff vector is feasible if , and acceptable if for every coalition . The core is the set of payoff vectors that are both:
is a convex game if is supermodular on the Boolean lattice of coalitions: for all . ("Convex" is the game-theory literature's name for this supermodularity property; it has no relation to convexity of sets or of real functions, a collision the book itself flags.) Equivalently, by Theorem 2.6.1/2.6.4, a game is convex exactly when the marginal value of any player to any coalition not containing increases as grows — the more players already committed to a project, the more valuable one more player is to it.
Given a permutation of , let . The greedy algorithm builds the payoff vector by paying each player its marginal contribution when added in the order : . The Shapley value pays player the average of over all permutations , equivalently .
A core is large if every acceptable payoff vector is dominated, coordinatewise, by one in the core; a subgame restricts to subsets of ; a core is totally large if the core of every subgame is large.
The weakest stable statement here is already the union of these three claims: nonemptiness of the core (b) is a formal consequence of (a) for any single permutation, and (c) is a genuinely separate fact about the average of the 's, not implied by (a) and (b) alone.
Theorem 5.2.1 is the reason convex games are the tractable case of cooperative game theory: it turns an existence question about linear inequalities into an explicit construction (any ordering of the players gives a point in the core), and it identifies the Shapley value — an axiomatically motivated but a priori only feasible payoff rule — as one that always respects every coalition's participation constraint on this class. Theorem 5.2.6 shows this is not an accident of the sufficient condition: total largeness of the core is a genuine characterization of convexity, so "does every subgame's core dominate every acceptable vector" is an equivalent, purely core-theoretic way to test convexity. Theorem 5.2.7 gives the comparative statics that make convex games useful in applied models (Chapter 5's later sections build monopoly, surplus sharing, and procurement games on exactly this apparatus): as a game's characteristic function improves in a complementary way with some parameter (a price, a technology level, a capacity), every player's greedy payoff and Shapley value improve monotonically, with no separate argument needed for each application.
Formalizing this mission produces, for the first time on the platform, machine-checked statements of the core, convex games, the greedy algorithm and the Shapley value — definitions that later missions in this series's own polyhedral-structure sections, and any future cooperative-game-theory mission, can reuse rather than re-derive. All three results already have a complete proof in the literature; this mission's remaining work is formalizing that known argument, not any open mathematics.
The routine first idea — check acceptability for the greedy vector one subset at a time using only the definition of supermodularity — does not directly work: Theorem 5.2.1(a)'s proof needs to compare a subset against the initial coalitions built by the particular permutation , splitting by the first and last time one of its elements appears in 's order and applying supermodularity along the resulting chain, not a single inequality. Theorem 5.2.6's converse direction is the harder half: showing a totally large core forces supermodularity requires constructing an auxiliary characteristic function from an arbitrary acceptable vector and showing is itself supermodular (via Theorem 2.6.4 and Theorem 2.7.6, results from the earlier monotone-comparative-statics chapter this mission depends on) before the argument closes.
Players are modeled as Fin n and a characteristic function as f : Finset (Fin n) → ℝ; a
payoff vector is y : Fin n → ℝ, and the core's feasibility and acceptability conditions are
stated with respect to Finset.univ (the whole player set) or a coalition U : Finset (Fin n)
for a subgame, never approximated by a finite sample of coalitions or by feasibility alone — the
acceptability condition genuinely quantifies over every subset. The Shapley value's coefficient
is the exact rational weight S.card.factorial * (n - S.card - 1).factorial / n.factorial cast
to ℝ, not a placeholder constant. The greedy algorithm's InitialCoalition σ j uses Lean's
0-indexed Equiv.Perm (Fin n) throughout, with the book's 1-indexed absorbed into
the definition rather than into the index j, so the definition and the goal read the same j
consistently. Theorem 5.2.7(c), which needs Theorem 5.2.4's convex-combination-of-extreme-points
machinery beyond this section, is out of scope for this mission.
A trivializing formalization would state acceptability only on singleton coalitions, or would
let n = 0/an empty player set stand in for the general case; neither is used here — every
Core/IsLargeCore statement quantifies over arbitrary subsets, and none of the theorems
restrict n.
This mission reuses Supermodularity.Monotonicity.SupermodularOn and
Supermodularity.Monotonicity.IncreasingDifferencesOn from this series's chunk II
(02-monotonicity) rather than restating supermodularity or increasing differences for
coalitions from scratch. InitialCoalition, Core, GreedyPayoff, IsConvexGame,
IsLargeCore, IsTotallyLargeCore and ShapleyValue are new to this mission and reusable by
any later mission on cooperative games, polymatroids, or the polyhedral structure of the core
(Section 5.2.3 of this chapter). Contributions completing the sorrys — Theorem 5.2.1(a)'s
chain-splitting argument, Theorem 5.2.6's auxiliary-function construction, and Theorem
5.2.7(a,b)'s direct comparison — are all welcome.
Many of the central questions of high-dimensional statistics reduce to bounding the expected supremum of a stochastic process: the maximum correlation of noise with a family of candidate signals, the operator norm of a random matrix, the uniform deviation of an empirical process from its mean. Whenever the index set of the process is infinite or exponentially large, a naive union bound over "all" indices is either vacuous or requires re-deriving a tail bound from scratch for every new problem. Chaining is the general-purpose technique that removes this need: it bounds the expected supremum of a process purely in terms of the geometry of its index set, measured by how many balls of a given radius are needed to cover it. The classical form of this bound is due to Dudley (1967), building on ideas that trace to Kolmogorov; the exposition here follows Wainwright, High-Dimensional Statistics: A Non-Asymptotic Viewpoint (Cambridge University Press, 2019), Chapter 5.
Fix an index set and a collection of zero-mean random variables . Say this collection is a sub-Gaussian process with respect to a (pseudo)metric on (Definition 5.16) if
This single condition covers, as special cases, the canonical Gaussian process for a standard Gaussian vector (with the Euclidean metric) and the Rademacher process built from i.i.d. Rademacher signs.
A -cover of with respect to a metric is a finite set such that every lies within -distance of some ; the -covering number is the size of the smallest such cover (Definition 5.1). The quantity is the metric entropy of at scale . Writing for the diameter of , the -truncated Dudley entropy integral is
The bound holds for every zero-mean sub-Gaussian process, with no further structure on beyond its metric entropy — this is what makes it a general-purpose tool rather than a bound tailored to one model.
The same conclusion with replaced by the cruder single-scale term , under the extra technical hypothesis . This is the one-step precursor whose refinement — iterating the discretization over a geometric sequence of scales instead of applying it once — is exactly what chaining improves.
A general comparison principle for pairs of centered Gaussian random vectors whose pairwise covariances are ordered coordinatewise and tested against a function with matching sign conditions on its mixed second partial derivatives: . This is the source, by specializing and the covariance-ordering sets, of both Slepian's inequality and the Sudakov–Fernique comparison, the two workhorse tools of Gaussian process theory used elsewhere in the chapter to obtain sharper, Gaussian-specific bounds than the sub-Gaussian chaining bound above.
Dudley's bound is the single most-used tool for controlling suprema of stochastic processes in high-dimensional statistics and empirical process theory: Gaussian complexity bounds for convex bodies, operator-norm bounds for random matrices, and uniform laws of large numbers for function classes are all obtained by computing a covering-number bound for the relevant index set and substituting it into Theorem 5.22 (see, for instance, Examples 5.18–5.21 later in the same chapter, and Chapters 13–14 of the book). Its significance is exactly its generality: it converts a purely geometric quantity — how "big" a set is under a metric — into a probabilistic bound, uniformly over every sub-Gaussian process on that set.
Formalizing it. The mathematical proof (interpolation-free, based on chaining and repeated
union bounds) is well understood and not itself in question; what this mission produces is a
faithful Lean statement of the theorem, its immediate one-step precursor, and the general Gaussian
comparison principle that underlies the chapter's complementary (Gaussian-specific) results, each
against Mathlib's own measure-theoretic and Gaussian-process infrastructure. All three theorems are
currently stated as open goals (:= by sorry); no claim is made here that they are already
formalized elsewhere on the platform (a fresh prior-art search for "Dudley," "chaining," "Slepian,"
"Sudakov," and "Gaussian comparison" returned no faithful matches).
The naive approach — apply Proposition 5.17's one-step discretization once, at whatever scale seems best — cannot see improvement past the cruder scaling of the metric entropy at a single resolution. The chaining argument that proves Theorem 5.22 instead telescopes the supremum across a geometric ladder of covers at scales , paying for each scale's approximation with a union bound over its own (much smaller, for a small ) covering number, and only then summing the resulting terms into an integral. The difficulty is not any single step of this argument — each step is an elementary sub-Gaussian tail bound — but bookkeeping the composition correctly: the recursive "best approximation at level of the best approximation at level " chain (Eq. (5.47)) must be built explicitly, and the telescoping sum of union bounds, each over a set that itself depends on the level , is what converts into an integral only in the limit as the covers refine to itself.
The index set is formalized as a nonempty Fintype, rather than the book's general totally
bounded metric space: this keeps every covering number, diameter, and supremum in this mission a
genuine maximum over a finite, nonempty family (realized via ⨆/sInf over finite index types),
rather than requiring the full apparatus of totally bounded infinite metric spaces to state the
covering-number definition (Definition 5.1) faithfully without risking a vacuous or ill-defined
infimum. This is a genuine narrowing of the book's stated generality, disclosed here rather than
left implicit — the underlying mathematics of the proof does not depend on finiteness, but a
faithful formalization of a general totally bounded space's covering number was judged out of
scope for this mission's budget.
The constant in the goal theorem is kept exactly as stated; the book's own remark that "there
is no particular significance to the constant 32, which could be improved with a more careful
analysis" is not license to substitute a sharper constant, since doing so would no longer match
what this particular proof establishes. Expectations are Bochner integrals against an explicit
probability measure Prob, with integrability required as an explicit hypothesis in the
sub-Gaussian process definition (SubGaussianProcess) rather than left implicit, since Mathlib's
Bochner integral silently returns for a non-integrable function — a trivializing formalization
this mission's definitions and hypotheses rule out.
Theorem 5.25's "centered Gaussian random vector" is formalized using Mathlib's own
ProbabilityTheory.HasGaussianLaw predicate (a genuine multivariate Gaussian law, not merely
Gaussian marginals) together with an explicit coordinatewise mean-zero hypothesis, and its mixed
second partial derivative condition is formalized via iteratedFDeriv ℝ 2 F applied to the
relevant pair of standard basis vectors, keeping the sign pattern over the disjoint index sets
and exact rather than collapsing it to a global convexity assumption on .
Out of scope for this mission: Sudakov's minoration (the complementary lower bound on the expected supremum of a genuinely Gaussian process, Theorem 5.30, misidentified as "Theorem 5.36" in this mission's planning brief — the correct Sudakov minoration statement is Theorem 5.30, p. 148; Theorem 5.36 is instead a tail-bound generalization of Dudley's bound to -Orlicz processes) and the Slepian/Sudakov–Fernique corollaries of Theorem 5.25 (Corollary 5.26, Theorem 5.27) — both natural follow-on work for a later contribution, once the Gaussian comparison principle formalized here is in place.
A Gaussian process is a family of jointly Gaussian real random variables indexed by an arbitrary set — not necessarily time. The canonical example is for ranging over a subset and a standard Gaussian vector in ; this single family already encodes questions as varied as the operator norm of a random matrix, the size of a random projection, and the metric complexity of a convex body. In every one of these applications the object of interest reduces to the same quantity: , the expected supremum of the process.
Bounding directly is hard — computing it exactly is possible only in special cases, such as the reflection principle for Brownian motion. Slepian's inequality (David Slepian, 1962) sidesteps this by comparison: if a second Gaussian process has matching variances and at-least-as-large pairwise increments as , then 's supremum stochastically dominates 's. This turns a hard direct estimate into a search for a simpler comparison process — the technique that Sudakov and Fernique later sharpened by dropping the equal-variance hypothesis (Theorem 7.2.11), and that Sudakov used to derive a purely geometric lower bound on from the covering numbers of (Theorem 7.4.1, Sudakov's minoration inequality). Together these results are the entry point to the theory of Gaussian width and generic chaining that occupies the rest of the book (Chapters 7–9, 11), and they underlie sharp bounds on random matrices (Section 7.3), random projections (Chapter 9), and high-dimensional geometry more broadly (Adler and Taylor, Random Fields and Geometry, Springer, 2007; Talagrand, Upper and Lower Bounds for Stochastic Processes, Springer, 2014).
Fix a probability space . A random process indexed by a set is a family of real random variables on . It is a Gaussian process if every finite linear combination ( finite, ) is a (possibly degenerate) normal random variable — equivalently, every finite marginal is a multivariate Gaussian vector. A process is mean zero if for every .
For a mean zero process, the increments always define a (pseudo)metric on — the canonical metric — turning the otherwise unstructured index set into a metric space. For a metric space and $\varepsilon
0N(T,d,\varepsilon)N\subseteq TT\varepsilonN\varepsilonN(T,d,\varepsilon) := \infty$ if no finite net exists.
Because need not be countable, need not be a measurable function of . Following the book's own convention, every quantity built from this supremum — and — is instead defined through the process's finite-dimensional marginals: as the supremum, over finite nonempty , of (respectively ). This sidesteps the measurability question entirely, at the cost of the quantity possibly being .
Let and be mean zero Gaussian processes with and for all . Then for every ,
and consequently .
Under only the increment hypothesis (no equal-variance hypothesis),
This is the weaker-hypothesis, strictly more applicable form: it is what Sudakov's minoration inequality and the sharp Gaussian random matrix bound of Section 7.3 both invoke.
Let be a mean zero Gaussian process with canonical metric . For every at which is finite,
for an absolute constant . This is the weakest, most stable form of the bound: it names no numerical value for , so it survives any later sharpening of the constant.
The vector-indexed special case of Theorem 7.2.1 ( finite), proved first by Gaussian interpolation and then extended to the general index set.
The results themselves. Slepian's inequality is the founding comparison theorem for Gaussian processes; Sudakov-Fernique's inequality is its practically indispensable generalization, used routinely to bound suprema of Gaussian processes without needing to track variances explicitly. Sudakov's minoration inequality is the first bridge from the probability of a Gaussian process to the metric geometry of its index set, complementing Dudley's upper bound (Chapter 8) and together giving matching bounds — up to a logarithmic factor, and exactly in many cases of interest — on purely from the covering numbers of . Downstream, this machinery gives the sharp bound on Gaussian random matrices (Section 7.3), underlies the Gaussian width used throughout convex geometry and compressed sensing (Chapters 9, 11), and bounds the covering numbers of polytopes and other convex sets (Corollary 7.4.4).
Formalizing it. All three inequalities are proved by the book (Gaussian interpolation and integration by parts for Slepian/Sudakov-Fernique; a direct application of Sudakov-Fernique to a well-chosen comparison process for Sudakov's minoration), so this mission's work is formalizing the statements faithfully and precisely — including the finite-marginal convention needed to make and meaningful for an uncountable index set without begging the underlying measurability question. The Gaussian interpolation technique itself (Lemmas 7.2.3, 7.2.5, 7.2.7) is not part of this mission's formalization scope; it is the proof method for the milestones and belongs to solvers closing them.
The obvious first idea — bound by controlling each separately, e.g. via a union bound over a net — throws away exactly the structure Slepian-type comparisons exploit: the joint Gaussianity across , not marginal tail behavior at each fixed . A union bound needs a net and a modulus of continuity to begin with; Slepian's and Sudakov-Fernique's inequalities need neither — they compare two processes directly through their covariance structure, which is what makes the technique (Gaussian interpolation: continuously deform the covariance of one process into the other's, and track how a smooth, nearly-indicator functional behaves along the path) work with no assumption on beyond the two hypotheses stated. The genuine difficulty is the smooth-interpolation argument itself — showing that is monotone in for the right choice of test function — which is exactly the part left as a milestone for solvers to formalize, not sketched here per the mission format's own rule against proof ideas.
(ProcessESup) is valued in EReal, not ℝ: the finite-marginal supremum a
real-valued definition would silently default to the junk value when the set of finite-marginal
expectations is unbounded above — exactly the case the book itself records as (Exercise 7.4.2, a non-relatively-compact index set). P\{\sup_{t\in T}X_t\ge\tau\}
(ProcessTailProb) stays real-valued, since it is always bounded in and so carries no
such risk. Both are defined through finite nonempty subsets of , per the book's own footnote
to Section 7.2; no separability, continuity, or countability assumption is placed on itself.
Gaussianity is Mathlib's ProbabilityTheory.IsGaussianProcess — every finite restriction of the
process has a Gaussian law — which is definitionally the book's Definition 7.1.10 ("every finite
linear combination is Gaussian"); mean-zero is stated as an explicit hypothesis alongside it.
Integrability of every quantity appearing under an expectation is not stated as a separate
hypothesis: Fernique's theorem (already in Mathlib for general Gaussian measures) guarantees a
Gaussian process has finite moments of every order, exactly as the book takes for granted.
Sudakov's minoration inequality (Theorem 7.4.1) is formalized for the case the book's own proof
actually covers — finite, taken as a hypothesis = (N : ℕ) rather than as a
case split inside the conclusion — since the book itself defers the infinite-covering-number case
to a separate, unproved exercise (7.4.2). This keeps fully general (still possibly
uncountable) at every fixed where the net is finite, which rules out a trivializing
reading of the theorem: nothing here forces itself to be finite or countable, only the
covering number at the scale in play, which is the book's own hypothesis.
Definitions reusable beyond this mission: ProcessESup, ProcessTailProb, CanonicalMetric,
and CoveringNumber are exactly the substrate Chapters 8 ("Dudley's Integral Inequality"), 9
("The Matrix Deviation Inequality"), and 11 ("Dvoretzky-Milman's Theorem") need for Gaussian
width and generic chaining; per this series' plan those missions restate them locally (drafts
cannot import another draft's definitions), using this chunk's forms as the faithful reference.
Contributions closing the Gaussian-interpolation machinery (Lemmas 7.2.3–7.2.8) as a reusable
definitions layer, beyond what any one milestone needs, are welcome.
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.
Most stochastic programs cannot be solved exactly: the expectation defining the objective is an
integral over a continuous or high-dimensional random parameter, and evaluating it exactly is as
hard as the optimization itself. The standard remedy is Monte Carlo: draw a sample of size ν
from the random parameter, replace the true expectation by the sample average, and solve the
resulting finite-dimensional "sample average approximation" (SAA) instead. This only helps if the
SAA's optimal value and optimal solution actually converge to the true problem's as ν → ∞, and
if that convergence is fast enough to be useful with a sample size one can actually draw and solve.
Birge & Louveaux's Chapter 9, §9.5, states the two central asymptotic results that justify this
approach for a general (not necessarily linear, not necessarily two-stage) stochastic program:
a central limit theorem describing the SAA optimal value's fluctuations around the truth
(Theorem 6, after Shapiro [1991]), and an exponential-rate large-deviation bound on how quickly
both the SAA value and the SAA solution concentrate near their true counterparts as the sample
grows (Theorem 7, after Dai, Chen & Birge [2000]). This mission formalizes both statements.
Fix a feasible set X ⊆ ℝⁿ of first-stage decisions and an outcome space Ξ carrying a
σ-algebra. The book considers the general stochastic program
z* = inf_{x ∈ X} ∫_Ξ g(x,ξ) P(dξ), (5.1)
with g : ℝⁿ × Ξ → ℝ an abstract integrand — no longer specialized to the two-stage recourse cost
Q(x,ξ) of Chapters 3–7, matching the book's own level of generality at this point in §9.5 — and
ξ a random element of (Ξ, 𝓑, P). Given an i.i.d. sample ξ₁, ξ₂, … from P, the sample average
approximation of size ν is
zν = inf_{x ∈ X} (1/ν) Σᵢ₌₁^ν g(x,ξᵢ) . (5.2)
Both z* and zν are attained (an optimal solution x* of (5.1); a random optimal solution
xν(ω) of (5.2) at each sample outcome ω). The two chapter results describe, in different
regimes, how (zν, xν) relates to (z*, x*) as ν → ∞.
Formalized in this mission: X sits in EuclideanSpace ℝ (Fin n); the sample is a sequence
ξ : ℕ → Ω → Ξ on an ambient probability space (Ω, P), independent and identically distributed
(Mathlib's iIndepFun/IdentDistrib); z*, x*, zν, xν are given as hypotheses that pin them
down as the optimal value and an optimal point of (5.1)/(5.2) (a lower bound over X plus
attainment at the named point), rather than computed via sInf/sSup of an image set — Real's
extended-real infimum returns the junk value 0 on an unbounded-below or empty set, which would
silently misstate the theorems if X, g are only assumed as loosely as the book states them.
∀ ε>0, ∃ α>0, ∃ β>0,
(∀ ν>0, P[|zν − z*| ≥ ε] ≤ α·e^{−βν})
∧ (x* the unique optimal solution of (5.1) → ∀ ν≥1, P[‖xν − x*‖ ≥ ε] ≤ α·e^{−βν})
under the moment hypothesis: there exist a>0, θ₀>0, η : Ξ → ℝ with |g(x,ξ)| ≤ a·η(ξ) for
all x ∈ X, and E[e^{θ·η(ξ)}] < ∞ for every θ ∈ [0,θ₀]. This is the mission's goal because it
is a clean, self-contained existential-constants statement — no algorithm to define, unlike most of
the chapter's other convergence results — and because, like Chunk 03's Theorem 6(a), the book's own
proof cites an external paper (Dai, Chen & Birge [2000], Theorems 3.1–3.2) and gives no in-text
derivation: the statement itself, not a derivation from a preceding numbered result of this book,
is the mission's content.
X compact, g(x,·) measurable ∀x∈X, g Lipschitz in x with an L²(μ) envelope a,
x0 the unique minimizer of x ↦ E g(x) over X
⟹ √ν·[zν − E g(x0)] converges in distribution to N(0, Var g(x0))
Included as a milestone (not used in Theorem 7's proof, which the book does not give — see above)
because it is the chapter's other general SAA convergence result, standing on the same setup
(5.1)–(5.2), and because Mathlib's MeasureTheory.Function.ConvergenceInDistribution (the
TendstoInDistribution predicate) plus Probability.Distributions.Gaussian.Real (gaussianReal)
and Mathlib's own i.i.d. central limit theorem
(ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub) supply exactly the vocabulary
needed to state — not prove — a faithful weak-convergence-to-Gaussian conclusion. Chunk 09's
BRIEF.md flagged this as a milestone to attempt "only if your workspace has enough of a
weak-convergence/CLT toolkit in Mathlib to state it faithfully"; the toolkit is present (verified
directly, not assumed from substrate.md, which predates this rev's addition of
ConvergenceInDistribution.lean), so it is included.
Every practical Monte Carlo solution method for stochastic programming — every discretization,
every scenario-reduction heuristic, every "solve on a sample and hope" approach used throughout
the rest of the book and the wider literature — rests on exactly these two results: that the SAA
converges at all (Theorem 6's CLT gives the asymptotic distribution of the error) and that it
converges fast enough to bound the error at a finite, computable sample size (Theorem 7's
exponential rate). Formalizing them gives Prove2Me a first foothold in convergence-rate theory for
stochastic optimization under sampling, a genre distinct from the concentration-of-measure results
already reachable via Mathlib's sub-Gaussian machinery (Probability/Moments/SubGaussian.lean):
sub-Gaussian concentration bounds a fixed-size sample's deviation from its own mean, not the
rate-in-ν convergence of a nested sequence of optimization problems' values and solutions to a
limiting problem's — the object Theorem 7 is actually about.
Theorem 6 needs a functional/uniform argument over the whole feasible set X (not the plain i.i.d.
CLT at the single point x0) to control the interaction between sampling noise and the
optimization over x; the book states it without proof, citing Shapiro [1991]. Theorem 7's
constants α, β are produced by a large-deviation argument specific to the exponential-moment
condition, again cited rather than derived in the book. Both are left as sorry; the value of this
mission is the faithful statement, matching the difficulty pattern already established for
Chunk 03's Theorem 6(a) (a result the book itself only cites).
α, β are
∃-bound exactly as the book leaves them (trap 8 of reference/FAITHFULNESS_TRAPS.md: the
existentials sit outside every quantifier they must be uniform over — in particular outside the
∀ ν). No closed form for α, β in terms of a, θ0, ε is invented.P[E[zν − z*)] ≥ ε] ≤ αe^{−βν} — an unmatched parenthesis and a stray E[·] around a quantity
that is already deterministic. milestones.yaml/MODERATION_NOTES.md quote the typo verbatim;
the Lean and natural_language_statement use the unambiguous P[|zν − z*| ≥ ε] the surrounding
prose (and every other occurrence of this quantity in the section) plainly intends.g is left fully abstract, not specialized to the two-stage recourse cost Q(x,ξ) of
Chunks 03–07, matching §9.5's own generality and keeping this mission independent of every other
chunk's namespace (no cross-chunk import, per missions/README.md's "Prior art" column for this
chunk: "none expected").z*, x*, zν, xν are hypothesis-characterized, not sInf/sSup-defined, to avoid the
real extended-value junk-value trap (trap 5) discussed under Setting above.zν, xν is an added hypothesis (hzSAA_meas/hxSAA_meas/hzSAA_meas in
Theorem 6), not derivable from the other hypotheses since g is abstract; the book is silent on
this technical point, standard for an applied convergence theorem, but Lean's P {ω | …} needs
it for the displayed probability to be the actual measure of the event rather than an outer-measure
value on a possibly non-measurable set.TendstoInDistribution,
with the limiting Gaussian supplied as an explicit random variable Y on a separate probability
space with HasLaw Y (gaussianReal 0 σ²) P' — the same pattern Mathlib's own CLT
(tendstoInDistribution_inv_sqrt_mul_sum_sub) uses for its own conclusion.paper.md's book-wide list item 5). A
formalization that quantifies α, β universally, or with an invented closed form, would assert
something the book's proof (cited, not given) does not establish; a formalization of Theorem 7
that used a computable sInf-defined zν on a set that is not shown bounded below would let the
conclusion hold vacuously via the junk value 0, independent of the genuine large-deviation
content — both are excluded by the choices above.STATUS.md for why it is out of scope).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.