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.
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 derivation of Kepler's three laws from Newton's inverse-square law of gravitation is the calculation with which mathematical physics begins. Kepler published the laws in 1609 and 1619 as empirical regularities distilled from Tycho Brahe's naked-eye astrometry: planets travel on ellipses with the Sun at a focus, the Sun–planet segment sweeps equal areas in equal times, and the square of the orbital period scales as the cube of the orbit's size. That an attractive force falling off as forces exactly these three regularities was established by Newton in the Principia (1687); as David Tong remarks in the source notes, the third law was within reach of several of Newton's contemporaries, but the derivation of the first — that the orbit is a conic section with the centre of attraction at a focus — was Newton's alone.
This mission formalizes that derivation as it is presented in §4 (Central Forces) of David Tong's Dynamics and Relativity, the Cambridge Part IA Mathematical Tripos lecture notes (Lent 2013). It is the first mission in a series covering those notes, and it targets the chapter's capstone, Kepler's first law.
A point particle of mass moves in Euclidean -space along a trajectory , assumed twice continuously differentiable and never passing through the origin, where the field below is singular. Write and .
The particle moves in a central force field when it obeys Tong's equation of motion (4.1),
where gives the radial component of the force at distance ; for a force derived from a central potential one has . The Kepler problem (Tong §4.3.1) is the inverse-square special case, potential (4.12)
with for gravitational attraction by a mass fixed at the origin. (The same equations govern the Coulomb problem, with , which is repulsive when ; this mission fixes .)
Two conserved quantities organize the problem. The angular momentum is the vector
and we write for the angular momentum per unit mass, which in the plane polar coordinates of Tong (4.5) is . The total energy of the Kepler problem is
Tong's solution (4.14) of the orbit equation states that the trajectory lies on a conic section with a focus at the origin. Coordinate-free, this says that there is a fixed eccentricity vector , pointing towards the point of closest approach, with
which is Tong's with the eccentricity and measured from the direction of , and the semi-latus rectum.
Finally, a set is an ellipse with a focus at the origin when there are a nonzero normal vector , a second focus with , and a real number with , such that is exactly the set of points of the plane satisfying the two-foci (string) property
The inequality forces and rules out the degenerate loci; gives a circle.
The goal theorem is Kepler's first law, K1 of Tong §4.3.2: each planet moves in an ellipse, with the Sun at one focus. Formally, for a trajectory of the attractive inverse-square problem with nonvanishing angular momentum and negative total energy,
The hypothesis excludes purely radial free-fall, whose trajectory is a segment rather than an ellipse, and is the bounded regime, which by Tong (4.16) is exactly .
The milestones follow the source in order: conservation of angular momentum and the resulting planarity of the motion (§4, p. 48); Kepler's second law (K2), which holds for any central force; conservation of energy; the conic orbit (4.14); the identification of a conic of eccentricity as an ellipse with a focus at the origin (4.15); the energy–eccentricity relation (4.16); and Kepler's third law (K3, p. 62),
The result. K1 is the statement that fixes the inverse-square law among all central force laws: K2 holds for every central force, and dimensional analysis alone gives the shape of K3, but closed orbits that are exact ellipses with the attracting centre at a focus are special to the force (and to the harmonic force, with the centre at the centre of the ellipse). Everything quantitative in classical celestial mechanics — orbit determination, the mass–period relation used to weigh binary stars, and the perturbative treatment of precession that eventually exposed the anomaly in Mercury's orbit — is built on the Kepler solution.
Formalizing it. The mathematics has been settled for three centuries; what this mission produces is a machine-checked treatment of the Newtonian derivation, starting from the differential equation rather than from a prescribed orbit. Mathlib has no central-force or two-body library, so the definitions here — central force motion, angular momentum, conserved energy, swept area, and the two-foci characterization of an ellipse — are new and reusable across the rest of the series and by any later mission in classical mechanics. The existing platform mission Celestial Mechanics I: Binary Star Systems runs the complementary direction, verifying that a prescribed conic orbit satisfies the equations of motion and reducing the two-body problem to a one-body problem; the present mission asks for the converse, which is the harder half and the one Newton is credited with.
The derivation in the source changes the independent variable from time to the polar angle , substitutes , and solves the resulting linear oscillator equation (4.11). Each of those steps needs infrastructure that does not exist in Mathlib. There is no polar-angle function attached to a curve in the plane: one has to produce a continuously differentiable angle lifting the trajectory, show never vanishes so that is a legitimate change of variable, and then transport a second-order ODE through that reparametrization. Solving (4.11) then requires a uniqueness theorem for the inhomogeneous harmonic oscillator, and reading the conic back into Cartesian form requires the algebra of (4.15).
Kepler's third law carries an extra burden beyond the formula: the statement quantifies over the least period of the motion, so a solution must establish that a negative-energy orbit is periodic at all, and must identify and as the periapsis and apoapsis distances .
Trajectories are maps ℝ → EuclideanSpace ℝ (Fin 3), with ContDiff ℝ 2 smoothness and the standing hypothesis for all built into the definition of central force motion, together with . Time is all of : the trajectories considered are globally defined, so collision orbits are excluded by hypothesis rather than by a maximal-interval argument. Derivatives are Mathlib's deriv, so velocity and acceleration are the first and second derivatives of the trajectory.
Three conventions are worth flagging. First, the force is given by its radial profile rather than by a potential, avoiding any appeal to the junk value of a derivative at ; the Kepler case is the instance . Second, the swept area of K2 is the integral , which is the standard area element of the source written invariantly; the content of K2 is that this integrand is constant in time, so that the area depends on alone. Third, K1 asserts that the trajectory is contained in an ellipse; it does not assert that the particle traverses the whole ellipse, which is a separate (true) statement about periodic orbits.
The degenerate readings are ruled out explicitly. The eccentricity vector formulation of the conic is an equation holding at every time, not an existence claim at one time; the ellipse predicate carries , so a point or a segment does not qualify; and the hypothesis in K1 and in the conic milestone is necessary, since a radial trajectory satisfies every other hypothesis but lies on no ellipse.
Contributions of independent interest are welcome: a plane polar coordinate API for curves, uniqueness for the forced harmonic oscillator, and the classification of the loci into ellipse, parabola and hyperbola according to , , (this mission needs only the first case) would all be reusable well beyond this series.
Diffusion models in a bounded region need a rule for what happens when a path reaches the boundary. Two standard mechanisms are absorption, where the boundary kills the generator contribution, and oblique reflection, where a prescribed vector field pushes the process back into the region. Ethier and Kurtz treat these mechanisms as neighboring variants of the same uniformly elliptic model in Chapter 8, Section 1 of Markov Processes: Characterization and Convergence. The distinction is structural: the interior differential operator is shared, but its admissible generator graph changes with the boundary condition. This mission formalizes Theorems 1.4 and 1.5, retaining oblique reflection as the capstone and absorbed diffusion as the required related result.
Let be bounded, open, and connected, with . Its boundary is locally represented in orthogonal coordinates as the graph of a scalar function. The formal predicate C²,μ boundary regularity requires one positive chart radius valid at every boundary point, a connected local boundary patch, and a graphing function whose second partial derivatives satisfy the source's componentwise Hölder oscillation condition. The exponent obeys .
The diffusion coefficients are a symmetric positive-semidefinite matrix field and a drift field . Their entries satisfy the same local componentwise Hölder convention. Uniform ellipticity means that one satisfies
for every and every unit vector . For smooth , the interior operator is
Functions live on the compact closure as bounded continuous functions. Their ambient extensions are differentiated only at interior points. The second coordinate of each graph is itself continuous on the closure, so it records the boundary trace of rather than assigning an arbitrary value after differentiation.
Theorem 1.5 adds a reflection field whose components have C¹,μ boundary regularity. An outward unit normal is oriented by a local defining function that is negative precisely inside . Uniform obliqueness is the global lower bound
for one positive . The reflected graph requires a continuous derivative trace that agrees with in the interior and satisfies
The target asserts that the uniform closure of this graph is single-valued and is exactly the full generator of a positive strongly continuous contraction semigroup preserving the constant function one. The generator condition is a biconditional derivative limit, so it identifies the complete domain rather than only a convenient operator restriction.
Theorem 1.4 keeps the same smooth-region and ellipticity assumptions but uses the absorbed graph. Its continuous operator trace satisfies on the boundary. It has the same full generation conclusion: graph single-valuedness, a positive strongly continuous contraction semigroup, preservation of one, and exact identification of the generator. The absorbed zero trace is not imported into the reflected theorem, and the oblique derivative condition is not imposed on the absorbed graph.
These results connect a local elliptic expression and a geometric boundary condition to a global Markov evolution on continuous functions over the closed region. The conclusions contain more than existence of a semigroup: they determine the whole infinitesimal generator, ensure positivity and contraction, and retain the conservative convention used by Ethier and Kurtz. The paired statements make the effect of the boundary mechanism explicit while holding the interior model fixed.
The formal contribution is a machine-checkable statement layer, not a proof of the source theorems. It records the componentwise Hölder convention, uniform boundary charts, ellipticity, normal orientation, continuous derivative trace, the two distinct generator graphs, and every semigroup clause. These definitions can support later work on reflected processes, elliptic boundary problems, and martingale formulations without rebuilding the geometric conventions.
The main difficulty is simultaneous control of interior regularity, boundary geometry, and the closed generator domain. Pointwise obliqueness is insufficient: the source requires a uniform positive lower bound over the whole compact boundary. Likewise, merely writing for an arbitrary ambient extension would not supply a well-defined boundary derivative. The graph therefore carries a continuous derivative trace agreeing with the interior derivative. Replacing the biconditional generator equality by a one-way inclusion, or silently imposing the absorbed zero trace on the reflected graph, would weaken or change the source result.
The state space is EuclideanSpace ℝ (Fin (n + 1)) with 2 ≤ n + 1. Connectedness supplies nonemptiness. Matrix positive semidefiniteness supplies symmetry and nonnegative quadratic forms; a separate hypothesis gives strict uniform ellipticity. Local oscillation bounds apply within connected components of small intersections and do not compare different components.
The absorbed and reflected graphs use bounded continuous functions on closure Ω. The arbitrary zero extension outside the closure is never differentiated at a boundary point. The reflected boundary equation uses a continuous field of linear derivative maps, while the absorbed equation uses the continuous second graph coordinate. No vacuous region, pointwise-only ellipticity or obliqueness, weakened generator inclusion, proof-only theorem dependency, or synthetic theorem combining the two boundary mechanisms is admitted.
In 1985 R. S. Ward conjectured that "many (and perhaps all?) of the ordinary and partial differential equations that are regarded as being integrable or solvable may be obtained from the self-dual gauge field equations (or its generalizations) by reduction". The self-dual Yang–Mills (SDYM) equations are therefore often called the master integrable system: choosing a gauge algebra and a symmetry group to reduce by produces, on the one hand, the classical soliton equations and the Painlevé transcendents, and on the other — once infinite-dimensional gauge algebras are allowed — a family of third-order equations whose solutions have movable natural barriers and are therefore not of Painlevé type.
This mission formalizes the endpoint of one such reduction chain, as surveyed by Ablowitz, Chakravarty and Halburd, Integrable systems and reductions of the self-dual Yang–Mills equations, J. Math. Phys. 44 (2003) 3147–3173, Section V. Reducing SDYM to functions of a single variable gives the Nahm equations; taking the gauge algebra to be the divergence-free vector fields on turns them into a matrix flow which, after diagonalizing the symmetric part, becomes the generalized Darboux–Halphen system. Its trace is governed by the Chazy equation, written down by Chazy in 1909, and — this is the paper's historical observation — the Chazy equation is equivalent to the differential system Ramanujan derived in 1916 for the Eisenstein series , , . Chazy and Ramanujan worked on the same equation at nearly the same time and apparently did not know it.
Throughout, and are complex variables and all functions are complex-valued; a "solution on " means the stated derivative identities hold at every point of a set .
The classical Chazy equation is the third-order equation
The classical Darboux–Halphen system is the first-order system for
together with its two cyclic images. It arose in Darboux's study of triply orthogonal surfaces and was solved by Halphen. Its generalized form adds a term to each right-hand side, where and cyclically.
Ramanujan's system is
satisfied by , , , where .
Finally, the matrix flow obtained from the Nahm equations with the gauge algebra is
and the generalized Chazy equation with parameter is
If satisfy Ramanujan's system on a region of the punctured -plane, then
satisfies the classical Chazy equation on the preimage region. In particular is a solution of the Chazy equation, and knowing the general solution of Chazy gives the general solution of Ramanujan's system.
The milestone list covers the reduction chain in both directions: the matrix flow and its reduction to the Darboux–Halphen system (eqs. (51)–(54)), the first integrals (55), the passage from Darboux–Halphen to Chazy and back through the roots of a cubic, the symmetry (73) of the Chazy equation, Rankin's fourth-order equation for the discriminant cusp form, the change of variable between the two forms of Ramanujan's system, and the generalized Chazy equation (81).
The Chazy equation is the bridge between integrable systems and the theory of modular forms. Its particular solution makes the quasi-modularity of the second Eisenstein series an ODE statement; via it turns into Rankin's homogeneous fourth-order equation for the discriminant cusp form , whose Fourier coefficients are the Ramanujan -function. The action on solutions is exactly the weight-2 quasi-modular transformation law. In the other direction, the general solution of Chazy is a ratio of hypergeometric functions with a movable natural barrier, which is why these reductions are used as the standard counterexample to the identification of integrability with the Painlevé property.
None of this material is currently in Mathlib: there is no Chazy equation, no Darboux–Halphen system, no Ramanujan differential system, and no Eisenstein-series ODE. The mission builds that layer from scratch. Each statement is a closed-form differential identity, so the development is self-contained: it needs no analytic continuation theory, no modular-forms library, and no existence theory for ODEs. What a solver must supply is careful derivative bookkeeping and polynomial algebra.
Status honesty: every statement in this mission is a classical, published result — Darboux, Halphen, Chazy (1909–1911), Ramanujan (1916), Rankin (1956), and Ablowitz–Chakravarty–Halburd (1990s–2003). Nothing here is open mathematics. What is open is the machine-checked proof; to the captain's knowledge no formalization of these identities exists.
The obvious approach — "differentiate three times and call ring" — fails for two reasons. First, the statements are about functions, not about polynomials: each differentiation step requires producing the derivative of a product, a quotient, or a composition from the hypotheses, and only then is the resulting algebraic identity a ring problem. Second, two of the targets go against the flow of the hypotheses. Recovering the Darboux–Halphen system from a Chazy solution means recovering from the derivatives of the three elementary symmetric functions of the : this is a linear system whose matrix is a Vandermonde matrix in , invertible precisely because the roots are assumed distinct — which is why the distinctness hypothesis is not decoration. Similarly, the matrix milestone needs the conjugation-equivariance of , which holds for the transpose only because the conjugating matrix is complex orthogonal.
Everything is over , matching the paper. Solutions are represented pointwise on an arbitrary set rather than on all of , because the solutions of interest have movable singularities and natural barriers; no openness, holomorphy or connectivity is assumed unless a statement needs it.
Higher derivatives are carried as explicit extra function arguments joined by HasDerivAt hypotheses rather than through iterated deriv. This avoids junk values entirely: a statement never asserts anything about the value of a derivative that does not exist. The same convention is used for the matrix flow, where the derivative is imposed entrywise, so that no norm or normed-space structure on the space of matrices needs to be chosen.
Divisions are arranged so that no denominator can vanish under the stated hypotheses: Ramanujan's system is written in the form , with no division by ; the generalized Chazy equation carries the hypothesis ; and the first-integral and discriminant statements carry explicit nonvanishing hypotheses.
There is no trivializing formalization available here. Every statement is an implication between two systems of differential equations whose hypotheses are satisfied by the classical explicit solutions (, , for the Ramanujan system; Halphen's solutions for Darboux–Halphen), so none of them is vacuous, and none is an identity that holds for arbitrary functions.
A complete development needs only Mathlib's derivative calculus (HasDerivAt and its product, quotient and composition rules), Complex.exp, and Matrix.adjugate with the basic adjugate identities. Contributions of reusable pieces are welcome: in particular a clean statement of the derivative of the elementary symmetric functions of a triple of functions, and the Vandermonde inversion step, would both be of use beyond this mission.
Sums of independent random variables are well understood: Bernstein's inequality and its relatives give sharp, non-asymptotic tail bounds for whenever the are independent and light-tailed. Many quantities that arise in high-dimensional statistics and random matrix theory, however, are not linear but quadratic in an independent sample — the squared norm of a random vector after a linear transformation, a quadratic-form test statistic, the diagonal of a sample covariance matrix, or the number of edges cut by a random partition in a random graph. A quadratic form is a sum with dependent terms: and share the factor , so classical sum-of-independent-variables tools do not apply directly.
The Hanson-Wright inequality, first obtained by Hanson and Wright (1971) for sub-gaussian variables and later sharpened and popularized in this form by Rudelson and Vershynin (2013, "Hanson-Wright inequality and sub-gaussian concentration," Electronic Communications in Probability), closes this gap: it gives a concentration inequality for around its mean with the same two-regime (sub-gaussian near the center, sub-exponential in the tail) shape as Bernstein's inequality for linear sums. It is now a standard tool wherever quadratic statistics of independent data are analyzed: covariance estimation, compressed sensing, randomized numerical linear algebra, and the analysis of random matrices more broadly draw on it routinely.
Fix a probability space and let be a random vector whose coordinates are independent, mean zero, and sub-gaussian: each has a finite sub-gaussian (Orlicz ) norm , the smallest with . Write .
Let be an real matrix, with no constraint on its diagonal, and form the quadratic form
Two matrix norms measure the size of : the Frobenius norm (the Euclidean norm of 's entries) and the operator (spectral) norm (the largest singular value of ). Always , so the two norms can differ by a factor as large as — the gap between them is exactly what produces the inequality's two regimes below.
where is an absolute constant, not depending on , , , or . Stating the constant only as "some absolute " (rather than pinning it to a numeral) is deliberate: the book's own proof does not track a sharp value, and a goal that only asserts the shape of the bound survives any later improvement to .
The result itself. Hanson-Wright turns a two-dimensional (in ) dependency structure into a one-dimensional concentration statement controlled by two scalar quantities, and . This is what makes it usable: a practitioner bounding a quadratic statistic need only compute these two norms, not analyze the joint dependency structure of directly. It specializes to Bernstein's inequality (Chapter 2 of this book) when is diagonal, and it underlies non-asymptotic guarantees for covariance estimation, the Johnson-Lindenstrauss lemma via a different route, and the concentration of Lipschitz functions of sub-gaussian vectors.
Formalizing it. The published proof of Hanson-Wright is not a single argument but a chain of four steps: a decoupling reduction (Section 6.1), a direct computation for Gaussian chaos (Lemma 6.2.2), a comparison lemma extending the Gaussian bound to general sub-gaussian vectors via a replacement trick (Lemma 6.2.3), and a final assembly that separates the diagonal part (handled by Bernstein's inequality) from the off-diagonal part (handled by decoupling and comparison). This mission formalizes the goal theorem's statement and the first, most reusable link in that chain — the decoupling machinery of Section 6.1, which reduces the analysis of the dependent chaos to the independent-once-conditioned bilinear form — together with the chapter's separate contraction principle (Section 6.7), a general comparison tool for Rademacher-weighted sums used repeatedly in the book's later chaining chapters. The Gaussian MGF computation and the replacement-trick comparison lemma (Lemmas 6.2.2–6.2.3) are left as future milestones on top of this mission: they require Gaussian rotation invariance and the singular value decomposition of , substantially more machinery than the milestones included here.
The obvious first idea — treat as if it were a sum of independent terms and apply Bernstein's inequality termwise — fails immediately: the terms for fixed are not independent across , since they all share the factor . Decoupling (Theorem 6.1.1) is the non-obvious fix: it replaces the off-diagonal chaos by a bilinear form in an independent copy , which genuinely does become a sum of independent terms once one of the two vectors is conditioned on. The price is a universal constant factor of and the restriction to diagonal-free matrices, which is exactly why the full Hanson-Wright proof must separate the diagonal contribution to (handled directly by Bernstein's inequality, Chapter 2) before decoupling can be applied to what remains.
Random variables and vectors are real-valued on an explicit probability space . The sub-gaussian norm is HighDimProb.Concentration.subgaussianNorm, the
Orlicz--norm definition already published for this series (01-concentration), reused
here as a reference item rather than redefined. is written as a
finite supremum over the coordinate index, ⨆ i, subgaussianNorm P (X i); because the index
type is always a Fintype (Fin n), this supremum is well-defined and, at the degenerate index
, reduces to a true (if content-free) instance of the inequality rather than a vacuous or
false one. The Frobenius and operator norms of are this mission's own frobeniusNorm and
opNorm, stated directly from their defining formulas rather than through Mathlib's scoped
matrix-norm typeclass instances, which are deliberately not global defaults (to avoid a diamond
between the two norms) and so are unsuitable for a statement that needs both simultaneously.
Every place the goal or a milestone integrates a quantity, that quantity is required
Integrable, guarding against Mathlib's convention of returning 0 for the Bochner integral of
a non-integrable function — without these hypotheses, a mean-zero or expectation hypothesis
could hold vacuously, or a conclusion could hold trivially, for reasons having nothing to do
with the book's mathematics.
The formalization deliberately does not restrict 's diagonal in the goal theorem: doing so would collapse Hanson-Wright to a restatement of Bernstein's inequality for the special case of a diagonal matrix, discarding the chapter's actual content, which is handling the off-diagonal, genuinely quadratic dependence between coordinates. The diagonal-free restriction does appear, correctly, in the Decoupling theorem (6.1.1), whose proof needs it.
Reusable beyond this mission: frobeniusNorm and opNorm are needed by any future chapter
using matrix norms (Chapter 4's random matrix norms, Chapter 9's matrix deviation inequality);
the decoupling theorem and convex decoupling lemma are the standard entry point for any later
formalization of chaos concentration; the contraction principle is reused throughout the book's
chaining chapters (7 and 8). Welcome contributions include the Gaussian MGF and comparison
lemmas (6.2.2–6.2.3) needed to complete a full proof of the goal theorem, and the two-sided
version of Bernstein's inequality needed for the diagonal part of that proof.
A recurring question in high-dimensional statistics is how tightly a scalar quantity built from many random inputs concentrates around its mean, even as the number of inputs grows without bound. Two classical answers organize the whole toolkit: martingale methods, which control a sum of dependent increments one conditional step at a time, and Gaussian-specific isoperimetry, which shows that essentially any regular (Lipschitz) function of a high-dimensional Gaussian vector concentrates as tightly as a single Gaussian coordinate, regardless of dimension. This mission formalizes one representative theorem from each line: the general martingale Bernstein bound (Wainwright, High-Dimensional Statistics, 2019, Theorem 2.19) and the Gaussian concentration of Lipschitz functions (Theorem 2.26), following Chapter 2 of the same book.
A random variable with mean is sub-Gaussian with parameter (Definition 2.2) if for all ; it is sub-exponential with parameters (Definition 2.7, a strictly milder condition) if the same bound holds only for , with the convention so that recovers the sub-Gaussian case exactly.
A sequence , adapted to a filtration , is a martingale difference sequence if each is -measurable and . Such sequences arise throughout statistics via the Doob martingale construction: given a function of independent variables , setting telescopes to , converting a deviation question about into a martingale concentration question.
A function is -Lipschitz with respect to the Euclidean norm if for all (Eq. (2.38)).
Let be i.i.d. standard Gaussian and be -Lipschitz with respect to the Euclidean norm. Then is sub-Gaussian with parameter at most , and hence
The bound is dimension-free: it depends on only through 's Lipschitz constant, not the ambient dimension itself.
For any differentiable and convex , for independent — the interpolation identity Theorem 2.26's proof is built on.
Given a martingale difference sequence with a per-index sub-exponential conditional moment-generating-function bound for , the sum is itself sub-exponential with parameters , and satisfies the two-regime concentration inequality of Eq. (2.28): sub-Gaussian for small deviations, sub-exponential for large ones. This is the chapter's central general-purpose martingale concentration tool.
Theorem 2.19 is the source of two of the most-cited concentration inequalities in the field —
the Azuma–Hoeffding inequality (Corollary 2.20) and the bounded-differences/McDiarmid
inequality (Corollary 2.21), both already faithfully covered elsewhere on the platform
(azuma_hoeffding_two_sided, bounded_diff_martingale_two_sided) and included here as
kind: reference milestones rather than redrafted. Theorem 2.26's Gaussian Lipschitz
concentration is separately significant: it is the tool behind dimension-free operator-norm
bounds for random matrices, concentration of the empirical spectral distribution, and much of
the machinery of Chapters 5 and 6 of the same book.
Formalizing it. No faithful prior art exists on the platform for either the martingale
Bernstein bound or Lipschitz-Gaussian concentration itself (a fresh search for "martingale
Bernstein," "sub-exponential martingale," "Gaussian interpolation," and "Lipschitz
concentration" returned no hits; the existing Vershynin-book item
HighDimProb.Isoperimetry.lipschitz_concentration_sphere concentrates a Lipschitz function on
the sphere, a different underlying space and a different proof from Theorem 2.26's Gaussian
vector). Both goal-adjacent theorems and the Gaussian interpolation lemma are drafted here as
open goals (:= by sorry); the two Azuma–Hoeffding/bounded-differences corollaries are reused
from the platform's existing, already-proved formalizations.
The naive approach to Theorem 2.26 — try to bound directly via a Lipschitz-type argument in — has no obvious route to a dimension-free bound, since a union bound over coordinates (or over an -net of the domain) picks up a factor that grows with . The resolution, Lemma 2.27's interpolation identity, instead exploits a special structural fact about the Gaussian distribution — its rotation invariance — to replace the nonlinear quantity with the linear, and hence exactly computable, Gaussian quantity , at the mild cost of a non-optimal constant. Theorem 2.19's difficulty is bookkeeping rather than a conceptual obstruction: the recursive conditioning step (Eq. (2.29)) must be iterated exactly times while keeping track of the interplay between the two parameters per difference, and Proposition 2.9's two-regime tail bound (small-deviation sub-Gaussian behavior, large-deviation sub-exponential behavior) must be carried through unchanged into the final statement — dropping either regime understates what the theorem proves.
Expectations are Bochner integrals against an explicit probability measure, with integrability
required as an explicit hypothesis in IsSubGaussian and IsSubExponential (Mathlib's Bochner
integral silently returns for a non-integrable function, which this mission's definitions
rule out as a trivializing formalization). The sub-exponential condition's domain restriction
|λ| < 1/α is realized as the disjunction α = 0 ∨ |λ| < 1/α, since Lean's real division
convention 1/0 = 0 is exactly backwards from the book's own stated 1/0 = +\infty convention
for the degenerate sub-Gaussian case.
" independent" (Lemma 2.27, Theorem 2.26) is formalized via Mathlib's
HasGaussianLaw predicate together with explicit coordinatewise mean-zero and
identity-covariance hypotheses, which together pin down the standard multivariate normal law,
plus IndepFun. The inner product is realized as
fderiv ℝ f (X ω) (Y ω), the Fréchet derivative applied to — equal to
by the Riesz representation of the gradient on a
Hilbert space, avoiding the need to separately construct a gradient vector field.
Theorem 2.19's printed parameter pair for part (a), "," is formalized
as : Definition 2.7 parametrizes the sub-exponential MGF bound
by (with appearing in the exponent), so a literal transcription of the printed
pair's first entry would silently square the effective parameter and make part (a), read
literally, inconsistent with part (b)'s own tail-bound formula (which the book derives from
part (a) via the general sub-exponential tail bound, Proposition 2.9). The corrected pairing is
the one the book's own proof actually establishes; see MODERATION_NOTES.md for the full
derivation.
Out of scope for this mission: Proposition 2.5 (plain Hoeffding for a sum of independent sub-Gaussians), used in the book only as background for Theorem 2.26's proof and not redrafted, since the goal theorem's own statement does not depend on it once Lemma 2.27 is in hand.
Every algorithm in the first three chapters of Foster and Rakhlin's Foundations of Reinforcement Learning and Interactive Decision Making — ε-Greedy and UCB for the multi-armed bandit, Inverse Gap Weighting and SquareCB for contextual bandits — is a special case of the same two-step recipe: estimate a model of the world with an online regression oracle, then convert the estimate into a decision that trades exploration against exploitation. Chapter 4 asks whether this recipe can be made generic: given any structured decision-making problem, specified only by a function class and a decision space , is there a single quantity that governs the best achievable regret, the way governs the multi-armed bandit and governs the linear bandit? The chapter's answer is the Decision-Estimation Coefficient (DEC), introduced by Foster, Kakade, Qian, and Rakhlin [40] as a complexity measure that both upper- and lower-bounds achievable regret for a general decision-making protocol, unifying results that were previously proved from scratch, case by case, for each structured setting. This mission formalizes the chapter's central upper bound (Proposition 13) together with the machinery that makes it computable in two concrete cases — the multi-armed bandit (Proposition 14) and the linear bandit (Propositions 16–17).
Fix a finite decision space and a class of candidate mean-reward functions, with a ground-truth (realizability). Over rounds, at each round the learner observes an estimate produced by an online regression oracle, plays a decision distribution (possibly depending on and the history), and the regret is
where . The oracle's cumulative estimation error is assumed bounded: with probability at least (Definition 7). Writing , the DEC game value at a reference model and scale is the min-max quantity
and the DEC of itself is . The Estimation-to-Decisions (E2D) algorithm plays, at each round, a certifying (i.e. attaining or beating) the value of this min-max game at .
with probability at least , for any exploration parameter . This is the weakest stable statement the chapter proves about E2D: it holds for an arbitrary function class and an arbitrary regression oracle, with no structural assumption on beyond realizability, and the chapter's later sections instantiate it rather than strengthen it.
The Decision-Estimation Coefficient is, in the book's own words, "the main result" of this line of work: Foster, Kakade, Qian, and Rakhlin [40] show it is not merely an upper bound but (in a suitable localized form, developed further in Chapter 6) a tight characterization of the minimax regret for structured bandits and, more generally, for the interactive decision-making protocol the rest of the book studies. Proposition 13 is the mechanism that makes this useful in practice: it reduces regret analysis for a new structured problem to a single, purely convex-analytic computation of , in place of a bespoke exploration argument. Propositions 14–17 are the demonstration that this reduction is not vacuous — they recompute, via the DEC alone, the two rates (multi-armed and linear bandit) that earlier chapters of the book derived by direct, setting-specific arguments, and the match is exact. Formalizing this chapter therefore captures the book's unifying abstraction itself, not just one more instance of it. No formalization of the Decision-Estimation Coefficient, in any form, currently exists on the platform (see Formalization scope).
The obvious formalization mistake is to state Proposition 13's conclusion with left as an unconstrained free real-number parameter satisfying only the inequality the theorem asserts — a formalization under which the "theorem" would be a triviality about an arbitrary real number, since nothing about the actual min-max game would ever be checked. The chapter's content is precisely the opposite: that this specific minimax quantity can be computed (Proposition 14) or bounded via a concrete strategy (Proposition 17), and — as Chapter 6 shows for a lower bound outside this chunk's scope — that no smaller quantity would do. A second difficulty is proof-theoretic rather than notational: the book's own proof of Proposition 13 bounds regret by an unconstrained supremum over all reference functions , and only identifies this with the official, -restricted of Eq. (4.16) via Proposition 24 — a fact stated on p. 80, outside this chapter's numbered range, whose own proof the book defers to an exercise. A formalization that quietly imports Proposition 24 to close this gap would rest the goal theorem on an unverified fact; this mission instead states the hypothesis the book's own text uses to motivate restricting to in the first place (online estimation algorithms produce ), so the goal is faithful to what is actually established within the chapter's own pages.
Every item fixes a finite decision space (Fin A, Fin n, or a generic Fintype S)
and states the DEC as the literal sInf-of-sSup transcription of the min-max game
(Eqs. (4.15)–(4.16)), never as an opaque bound — this is the trivializing
formalization the chunk's own reading of the chapter rules out (see Difficulty).
piStar : (S → ℝ) → S is a hypothesized global maximizer selector throughout,
constrained to be a genuine argmax only on the function class in scope (F or
Set.univ), matching how the book treats as a fixed but arbitrary
tie-breaking choice. The goal theorem (Proposition 13) adds the explicit hypothesis
hfhat : ∀ t, fhat t ∈ convexHull ℝ F, replacing an appeal to the out-of-range
Proposition 24 (see Difficulty); this is the one place this mission's statement is not
a line-by-line transcription of the book's own displayed proof steps, and it is
recorded here and in MODERATION_NOTES.md. Proposition 14's and Proposition 17's
are replaced by the explicit constants the book's own proofs establish
( exactly, and respectively — the latter obtained
by summing the three terms the proof of Proposition 17 isolates). Proposition 14's
Lean statement splits the book's single equality into an upper bound on the literal decGf, a lower bound restricted
to full-support distributions, and IGW's own exact game value, because the book's
min over the whole simplex is not provable as a literal Lean equality: a
distribution with a zero-weight arm makes the inner supremum genuinely unbounded, and
Lean's total Real.sSup returns a junk value smaller than there
(caught in moderation, MODERATION_NOTES.md); the three-conjunct statement recovers
exactly the book's real content without asserting that false literal equality. Lemma 9
is restated
inside FoundationsRL.Structured rather than imported from the Chapter 2 mission,
since draft items across chunks cannot import one another; its source citation still
points to its original location (p. 32). Proposition 16 is not drafted: the
platform's existing BanditAlgorithm.kiefer_wolfowitz_equivalence (Lattimore &
Szepesvári, Theorem 21.1) states the identical existence claim — compact set with
full-dimensional span, a design with G-value at most — as one clause of a larger
equivalence, and is reused as a reference item rather than redrafted. Proposition 22
(primal/dual DEC equivalence, §4.4) is deliberately excluded: the book states it "under
mild regularity conditions" it does not pin down in the statement itself, which is
exactly the kind of unquantified hypothesis this series' faithfulness standard
excludes from a goal or milestone. Contributions extending this mission with Chapter
6's lower bound (matching from below, establishing tightness)
or with a formalization of Proposition 24 itself (removing this mission's hfhat
hypothesis) are welcome.
The magic-square programme already on this platform works at fixed small orders: MacMahon's enumeration of the squares, both the magic count and the semi-magic count ; the classification of the normal squares; and the counts of the panmagic and symmetric order-three classes. Each of those is a statement about a single order. This mission changes the axis: it asks what the counting function does when the order itself is allowed to vary.
Timeline.
That split is the point of the mission, so it is worth naming before anything is proved. A quasi-polynomial of degree and period agrees with a degree- polynomial on each residue class modulo , the polynomials differing between classes; a polynomial is the case . For the magic squares the values do depend on modulo a period — at order three vanishes unless — and the same is true of every other class. For it never happens.
An semi-magic square of line sum is an array of nonnegative integers in which every row and every column sums to . Entries may repeat, and no condition is placed on the diagonals. Write for the number of such arrays.
In Lean the array is a Square n ℕ, that is, a Matrix (Fin n) (Fin n) ℕ; the condition is IsSemiMagic M t, which asks every rowSum and every colSum to equal t; and the counting function is semiMagicCount n t, the cardinality of the finset of all arrays over Fin (t + 1) satisfying IsSemiMagic. Restricting the entries to Fin (t + 1) loses nothing, since an entry of a square of line sum is at most .
Dividing by turns such an array into a doubly stochastic matrix, a nonnegative real matrix whose every row and column sums to . So is equally the number of lattice points in the -fold dilation of the Birkhoff polytope . Two geometric facts about are what the mission is about. Its dimension is : the entries satisfy line equations, exactly one of which is dependent. Its vertices are the permutation matrices, by the Birkhoff–von Neumann theorem, hence integral. The mission states that both facts are visible in the arithmetic of .
This is Theorem 1 of [BCCG 2003], stated there for . It is the shape of the truth, not a closed form, so no later improvement of the explicit formulas can invalidate it. The three parts are not independent: the degree is the dimension of , and the two identities are the reciprocity law for lattice-point counting, applied to .
The goal is far from the easy cases, and the mission is laid out so that each rung is an independently provable statement.
MagicSquares.semi_magic_count_two () and MagicSquares.semi_magic_count_three (MacMahon's ). Included as references, not as targets.Its leading coefficient is and its normalised volume is .
The result itself. The theorem makes the semi-magic squares countable in closed form at every order, and it is why the semi-magic count can be tabulated as a polynomial while the magic, symmetric and pandiagonal counts cannot: a polynomial is determined by finitely many values, a quasi-polynomial is not without knowing its period. The reciprocity identities are the same statement seen from the interior of , which is why they are what pins an explicit polynomial down once its degree is known. The order-four polynomial above was verified against direct enumeration on seventeen values of ; that verification is evidence, not proof, and is recorded because the general statement is what has to be proved.
Formalizing it. The theorem has been known since 1973 and has had an elementary proof since 1980; what does not exist anywhere is a machine-checked proof. Mathlib contains no Ehrhart theory, no quasi-polynomial machinery and no rational-generating-function toolbox — the string "Ehrhart" does not occur in it — so a formalization must construct its own lattice-point-counting argument for this family of polytopes, or find an elementary route that avoids polytopes altogether. Either outcome is reusable: the same absence blocks the quasi-polynomial counts , and of BCCG's Theorem 2, which the earlier missions approach only at order three.
The first idea anyone has is to interpolate: compute for enough values of and fit a polynomial. That works, and it is how the order-four rung was produced, but it cannot prove the general statement: the degree is what is being asserted, so the number of values needed is not known in advance, and with itself a variable no finite computation settles it. Interpolation is legitimate as a target at order four; it must not be mistaken for a route to the goal.
The second idea is to import the geometry as a black box: a rational polytope dilated by has a counting function that is a quasi-polynomial of degree equal to its dimension, with period dividing the least common multiple of the vertex denominators. That is Ehrhart's theorem, and it is the textbook route. It is not available here, and reconstructing it in general is a larger project than this mission; the statements the mission asks for are the ones that survive without it.
The part of the goal with no counting interpretation at all is the second line. is defined on ; the assertion that a polynomial agreeing with it there vanishes at and satisfies is a statement about the interior of the polytope, and it cannot be read off from the combinatorial definition. A solver who proves only the polynomiality and the degree has not finished the goal.
The formalization commits to the following conventions.
semiMagicCount n t, the Finset.card of the arrays over Square n (Fin (t+1)) satisfying IsSemiMagic. Entries are natural numbers, not integers or reals.ℚ and is quantified existentially. Negative arguments are handled by casting the integer into ℚ and evaluating there; Polynomial.eval₂ is unusable for the reciprocity, since it would need a ring homomorphism , which does not exist.p.natDegree = (n - 1) ^ 2, with natural-number subtraction, which makes the case harmless rather than degenerate.1 ≤ n is carried explicitly although the statement is meaningful at ; it matches the source.∀ t by a finite range of values, or replacing semiMagicCount by a smooth surrogate, would make the statement easy and empty. The universal quantifier over and the exact value of natDegree are what give the goal its content.Reusable beyond this mission: any development of lattice-point counting in the Birkhoff polytope, of dilations of rational polytopes, or of quasi-polynomials. The vocabulary of the programme (MagicSquares, MagicSquaresPandiagonal, MagicSquaresMostPerfect, MagicSquaresTransforms, MagicSquaresNormal3) is shared with the earlier missions and is included as reference items rather than redefined.
The real Clifford algebra is the smallest Euclidean Clifford algebra whose full structure carries a nontrivial multiplicity-eight representation-theoretic decomposition, and it has become a recurring object in programs that build internal gauge and family structure from Clifford generators rather than imposing it by hand. Within such programs, the single most basic representation-theoretic question one can ask about the algebra is: how does a distinguished subalgebra, acting by the adjoint action, decompose the odd part of the algebra as a representation?
This mission answers that question exactly, for the specific triple of bivectors built on the index set . The computation was carried out structurally (by splitting active indices from spectator indices) in the LeanProofs research program in 2026 and recorded with exact multiplicities; no machine-checked proof exists yet. The purpose here is to close that gap: the result is finite-dimensional linear algebra, completely within reach of a Lean 4 + Mathlib development, and every constant in it is explicit.
Fix with its standard inner product and the associated quadratic form , and let be the real Clifford algebra generated by symbols with
The algebra is -graded in the usual sense: it is the direct sum of its grade- subspaces, spanned by products of distinct generators, of dimension . The odd sector is the linear span of the odd grades,
On it, register three bivectors and their halved adjoint actions:
where . The triple satisfies the relations and cyclic permutations, so the generate a copy of with cyclically. The associated quadratic Casimir is the endomorphism
Because each is even, every preserves the odd sector, and so does .
the two eigenspaces spanning the whole odd sector. Equivalently, as a representation of the generated ,
eight copies of the spin-1 module and eight copies of the trivial module. The goal deliberately asserts only the eigenspace dimensions and their spanning property — the decomposition shape — not any particular basis or pairing.
the three weight spaces spanning the sector. This refines the goal: each copy contributes weights and each copy contributes weight .
The result itself. The spectrum pins down exactly how an acting from inside the algebra sees the odd sector: not irreducibly, but as a clean multiplicity split between spin-1 and spin-0. In the LeanProofs program this decomposition is load-bearing for everything downstream that distinguishes "active" indices from "spectator" indices — the multiplicity is the number of spectator degrees of freedom, and its appearance in the spectrum is what makes the split structural rather than coincidental. The weight decomposition further identifies the Cartan grading and is the natural first test case for any technology that must eventually handle larger Clifford algebras or other subalgebras.
Formalizing it. The computation is proved (structurally, by hand, in the research record) but not machine-checked. Everything needed lives in Mathlib: CliffordAlgebra, its grading CliffordAlgebra.evenOdd, Submodule, LinearMap, Module.finrank. What the mission produces is a fully verified finite spectral computation inside Clifford algebra — a reusable certificate that the platform's Clifford and grading infrastructure supports exact representation-theoretic bookkeeping, not just algebraic identities.
The obstruction is bookkeeping, not ideas. The natural attack — split indices into active and spectator , decompose as a tensor product of graded pieces, and read off the multiplicity from the spectator sector — requires transferring the action across such a tensor decomposition, which Mathlib does not provide ready-made for Clifford algebras. A purely computational route (fix the 64-element blade basis, build the matrices of the explicitly, compute kernels) is straightforwardly correct but laborious; making it readable is the real work. The statement is stated through arbitrary endomorphisms bound pointwise to the halved adjoint actions precisely so that solvers may choose either route.
The mission commits to: the quadratic form Q60 as QuadraticMap.weightedSumSquares ℝ (fun _ : Fin 6 => 1); generators e6 i = CliffordAlgebra.ι Q60 (Pi.single i 1); the odd sector as the Mathlib-native CliffordAlgebra.evenOdd Q60 1; and the registered triple as products of two generators. All theorems quantify over endomorphism witnesses bound pointwise to , so no particular matrix realization is privileged. Spectra are stated as eigenspace decompositions with exact Module.finrank multiplicities — never as pointwise eigenvalue claims, which would be false for mixed vectors. No trivializing formalization exists: the multiplicities are hard constants, and the dimension gate (32) rules out statements about degenerate sector choices. The definition file is reusable for any future mission on ; the su(2) relations and dimension gate are self-contained milestones. Contributions of either a structural (active/spectator split) or computational (explicit blade basis) proof are equally welcome.
Mathlib.LinearAlgebra.CliffordAlgebra.Grading (the evenOdd grading used as the odd sector).A robust counterpart draws a hard line. Inside the uncertainty set the constraint must hold; outside it, nothing is promised — and in a real problem the perturbation does sometimes land outside. Chapter 3 answered this for linear problems with the globalized robust counterpart: keep the constraint exactly on the normal range , and let it degrade at a controlled rate outside, proportionally to the distance from . That mission published Proposition 3.2.1, which says the GRC of an uncertain linear inequality is equivalent to two ordinary robust counterparts.
Chapter 11 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization (Princeton, 2009) does the same for conic constraints, and the move is not routine. The left hand side of a conic constraint is a vector, not a scalar, so "the constraint is violated by at most " has no direct meaning. What replaces it is the observation that a scalar inequality is the inclusion , and that the violation is the distance from the left hand side to . In that form the notion lifts verbatim, and the whole chapter follows.
Definition 11.1.2. Consider an uncertain convex constraint
with nonempty, closed and convex. Let the perturbation space split as , each factor carrying a normal range , a closed convex cone and a norm , and let be a norm on . A candidate is robust feasible with global sensitivities if
where and .
The object that makes the analysis work is the recessive cone of (Definition 11.3.1): for any ,
which does not depend on and is a nonempty closed convex cone.
A candidate is feasible for the GRC (11.1.6) if and only if it satisfies the system
Line (a) is the ordinary robust counterpart over the normal range. Each line (b) is a bounded semi-infinite constraint — the perturbation ranges over the unit ball of a cone, not over an unbounded set — measuring the distance to the recessive cone rather than to itself.
The goal is the chapter's structural result and it does exactly what Proposition 3.2.1 did one level down: it converts a single semi-infinite constraint over an unbounded perturbation set into a robust counterpart over the bounded normal range plus finitely many constraints over unit balls. That matters because every tractability result of Chapters 6 to 9 is about bounded uncertainty sets; without the decomposition none of them applies to a GRC.
The two halves of the decomposition are genuinely different objects. Line (a) is familiar. Lines (b) are not: they measure the distance from a linear image of a ball to the recessive cone, and that is the function
of §11.4, which is almost a norm on linear maps — nonnegative, positively homogeneous, subadditive, but neither symmetric nor strictly positive. Proposition 11.4.1 says this function is self-dual in the precise sense that of a map with respect to a setup equals of the adjoint map with respect to the dual setup: dual norms, dual cones, source and destination exchanged. That single identity is what lets every bound on be computed on whichever side of the duality is tractable, and it is the engine of §11.4's tractability results.
The recessive cone results are the vocabulary. The one that earns its place is : the conic sets of this book are all of that form, so it says the recessive cone of every constraint in sight is computed by deleting the constant term.
The goal is an equivalence and the two directions are asymmetric.
Forward — GRC implies the system — is where the recessive cone is discovered rather than used. Fix and in the unit ball of , and run out along the cone. The GRC bounds the distance to by , so there are with ; the rescaled points stay bounded, and a limit point of them lies in by the limit characterization of the recessive cone. This is a genuine compactness argument, and it is why the recessive cone — not — is what appears in lines (b).
Backward is a decomposition-and-assemble: split each with , realizing the distance, get a point of from line (a) and a recession direction from each line (b), and add them — using that .
Proposition 11.4.1 is a chain of polarity identities: the polar of is for compact convex containing the origin, the polar of a norm ball of radius is the dual-norm ball of radius , and bipolarity. Each step is standard and the composition is not.
Built on the module published by the third mission of this series, which carries the linear-case globalized robust counterpart and the dual cone. New here: norms as functions with their defining properties, dual norms, the two distances, the recessive cone, the conic GRC, and the function .
Conventions committed to:
IsNormOn bundles definiteness, absolute homogeneity and the triangle inequality, and
nonnegativity follows from them.Erlang's formula, the subject of mission I of this series, sizes a single telephone link. Real networks are not single links: a call occupies a circuit on every link of its route simultaneously, and it is lost unless every one of those links has a free circuit. That is the loss network, the model of Chapter 3 of Frank Kelly and Elena Yudovina's Stochastic Networks (Cambridge University Press, 2014), and it describes not only circuit-switched telephony but any system in which a request must acquire several resources at once or be refused: wavelength assignment in optical networks, radio channel allocation under interference constraints, slot booking, and admission control generally. The term used in those application areas is circuit-switched: before a request is accepted it is checked that enough resource is available for each stage of it.
The exact equilibrium distribution of a loss network is known and has product form. It is also useless for computation — its normalizing constant is a sum over the feasible states, and for a general resource matrix computing it is NP-hard. What practitioners use instead is the Erlang fixed point: pretend the links block independently, so that the traffic offered to link is the traffic on the routes through it thinned by the blocking probability of every other link on each route, and then apply Erlang's formula link by link. The result is a system of coupled copies of Erlang's formula. The chapter's aim, in its own words, is to give insight into why that approximation works as well as it does; the first step is to show that it is well posed at all.
The links are , link carrying circuits. A route belongs to a set of routes, and the link-route incidence matrix records how much of each link a route needs: a call on route requires circuits from link and is lost if any link has fewer than free. (The classical case is a – matrix and exactly when ; from section 3.3 the book allows any non-negative integers.)
Calls requesting route arrive as a Poisson process of rate , independently across routes, and hold their circuits for an exponentially distributed time of unit mean. Writing for the number of calls in progress on route , the process is Markov on
and is called a loss network with fixed routing.
Write for Erlang's formula, , published in mission I of this series. The Erlang fixed point equations are
The factor removes link 's own thinning from the product, so in the – case the argument is , the reduced load offered to link .
The goal fixes no formula for and no rate of convergence: it asserts only that the approximation the field has used since the 1960s names a single, well-defined object. Existence alone is a short argument from Brouwer's theorem, since (3.7) defines a continuous self-map of the compact convex cube ; uniqueness is the substance.
The exact theory that the fixed point approximates: Lemma 3.4 on truncating a reversible process; the uncapacitated network as an instance of the open migration product form of mission II; equation (3.3), the exact equilibrium distribution on ; and the acceptance probability . Then the optimization side: that and the utilization are strictly increasing in , which is what makes the revised dual objective strictly convex; and Theorem 3.10, that a minimizer of the Dual problem (3.5) over the positive orthant satisfies the conditions on , equation (3.6).
The result itself. Without Theorem 3.20 the phrase "the Erlang fixed point" is not well formed, and neither is any engineering procedure that computes one — repeated substitution converges to a solution, and damped iteration is guaranteed to converge to one, but "the blocking probabilities predicted by the reduced-load approximation" names a unique vector only because of this theorem. The proof is also the interesting part: the fixed point equations are re-read as the stationary conditions of a strictly convex minimization, the revised dual (3.8), which is the Dual problem (3.5) of the maximum-probability analysis with its linear term replaced by . That connection is what later lets the book prove the approximation asymptotically exact in a limiting regime: Corollary 3.22 says the Erlang fixed point converges to the vector coming from the maximum-probability problem.
Formalizing it. Nothing here is open. What the mission produces is the loss network model in
Lean — state space, truncated rates, normalizing constant, incidence matrix — and a machine-checked
statement of the object the reduced-load approximation computes. It is also where this series'
earlier missions pay off: the uncapacitated network is literally the open migration process of
mission II with , , , and the exact distribution
(3.3) is its truncation by Lemma 3.4 to the feasible set, using the DetailedBalance layer of
mission I. Mathlib has no loss network theory and no Erlang formula beyond what mission I
published.
Existence of a fixed point is easy and is not where the difficulty lies. Uniqueness resists every direct attack: the map defined by (3.7) is not a contraction in any obvious metric, its monotonicity structure is not the kind that forces a unique fixed point, and iterating it undamped can cycle. The book's route is indirect — exhibit a strictly convex function whose stationary conditions are exactly (3.7) — and finding that function is the whole content. Its strict convexity comes from a monotonicity fact about Erlang's formula, that the utilization is strictly increasing in , which is itself a milestone here.
A second, formal difficulty: the equations involve , so a solution with would be meaningless. It is worth checking before starting that no such solution exists for , rather than assuming it.
Routes and links are indexed by finite types, the incidence matrix has natural-number entries (the general case of section 3.3, not only –), capacities are natural numbers, and arrival rates are positive reals. The feasible set is a subset of the state space, and a truncated process is the rate matrix restricted to that subset — which is exactly the book's truncation, since a transition leaving the set simply has no target.
Conventions: holding times have unit mean throughout, matching the book, so the departure rate from route is and no separate service-rate parameter appears. Normalizing constants are introduced through summability hypotheses that assert convergence and the value together, rather than as possibly-infinite quantities; is the reciprocal of the sum in the book's notation. Capacities are assumed at least in the goal: a link with no circuits blocks everything, identically, and the factor would then be undefined rather than merely large.
The goal cannot be satisfied trivially: it is a uniqueness statement, so a vacuous or degenerate reading would have to produce no solution, and existence is half of what is asserted.
Contributions welcome beyond the listed items: the Brouwer argument for existence of a solution to the – equations (3.1) of section 3.2; the utilization function and the revised dual (3.8); the central limit theorem 3.14 and Corollary 3.17; Lemma 3.21 and Corollary 3.22 on the limiting regime; and the diverse-routing models of section 3.7.
Consider a decision maker who must choose, at each of rounds, between two actions on the advice of "experts," none of which is known in advance to be reliable. This is the prediction-from-expert-advice problem, introduced by Littlestone and Warmuth [Littlestone & Warmuth, The Weighted Majority Algorithm, FOCS 1989/Inf. Comput. 1994] and generalized to real-valued losses by Freund and Schapire's Hedge algorithm [Freund & Schapire, A decision-theoretic generalization of on-line learning and an application to boosting, JCSS 1997]. It is one of the two founding problems of online learning (the other being universal portfolio selection, also introduced in this book's first chapter) and the historical origin of the multiplicative-weights update method, later recognized as a single algorithmic idea underlying results across game theory, optimization, and computational complexity [Arora, Hazan & Kale, The Multiplicative Weights Update Method: a Meta-Algorithm and Applications, Theory of Computing 2012]. This mission formalizes the chapter's three central guarantees: a matching deterministic lower bound, the Weighted Majority mistake bound, and Hedge's loss bound — the earliest instance, in the book's own development, of the "online convex optimization" phenomenon that its later chapters generalize to arbitrary convex losses.
At each round , a decision maker chooses one of two actions, or . After the choice, the true outcome for that round is revealed, and any action that disagrees with it is charged a mistake. experts also each commit to a prediction every round, and the decision maker may consult their record.
The Weighted Majority (WM) algorithm maintains a weight for each expert , initialized to . It predicts whichever action currently carries at least half the total weight, and after seeing the outcome, multiplies the weight of every expert who erred by for a fixed parameter , leaving correct experts' weights unchanged. denotes the algorithm's own mistake count through round , and expert 's.
The Randomized Weighted Majority (RWM) algorithm uses the same weights, but instead of following the majority it samples an expert with probability proportional to its weight, , and follows that expert's prediction; is its expected mistake count.
Hedge generalizes further, from binary mistakes to arbitrary non-negative real-valued losses suffered by expert at round . It samples expert with probability from weights updated multiplicatively in the loss, . Writing losses and the mixed strategy as vectors, the algorithm's expected loss at round is .
where . This is the chapter's most general result and the one the book reuses later on; it leaves free (no asymptotic tuning), so it survives whatever later chapters do with .
Theorem 1.1 shows the mistake-bound question has no trivial answer: even against only two
maximally simple experts, any deterministic strategy is beaten by a factor of by an
adversary who knows its code. Lemmas 1.3 and 1.4 show this factor is essentially removable —
first by relaxing "guarantee" to "guarantee in expectation" (RWM halves the deterministic
penalty from to ), then Theorem 1.5 removes the
binary-mistake restriction altogether, replacing it with an explicit second-moment correction
term that vanishes as losses shrink. Together they trace
the chapter's own narrative arc from "no algorithm beats " to "an explicit, parameter-free
family of algorithms gets within of the best expert for any ."
All four results are proved by the book via the same device — a potential function
— one of the first instances of the potential-function method that
recurs throughout the rest of the book (e.g. Online Gradient Descent's regret proof) and
throughout online learning generally. None of these four statements, in this exact form, has a
formalized proof on Prove2Me or (to the extent searchable) elsewhere: the platform's closest
existing result, BanditAlgorithm.ftrl_simplex_exp_weights_regret (see Formalization scope
below), proves an asymptotically similar bound by an entirely different route and under a
different loss model.
The natural first attempt at any of these bounds is to track (or , or ) directly and induct on ; this fails because the quantity itself has no useful recursive structure — knowing the algorithm's mistake count through round says nothing about round 's outcome, which the adversary chooses to inflict maximum damage. The proofs instead introduce an auxiliary potential that is not the quantity being bounded, track it in two directions — an upper bound in terms of the algorithm's own performance (using , or, for Hedge, for ) and a lower bound via the single best expert's weight, — and only convert back to the mistake/loss bound at the very end via one logarithm. Getting the direction of every inequality right (each of the four proofs chains four or five inequalities, each valid only in the stated parameter range) is the entire difficulty; there is no shortcut that avoids introducing .
Each algorithm is represented as a Prop-valued run predicate parametrizing over the weight
sequence, the input (expert predictions/losses and true outcomes), and the algorithm's own
output (predictions or mixed strategy), rather than as an executable program: IsHedgeRun
fixes W 0 i = 1, the update W (t+1) i = W t i * exp(-ε * ℓ t i), and
x t i = W t i / ∑ j, W t j; IsWeightedMajorityRun additionally fixes the majority-vote
prediction rule explicitly (per the triage rubric, the algorithm is part of the audited
statement here, not a black box the proof is free to instantiate). Randomization in RWM and
Hedge is captured exactly as the book itself does — as a deterministic expectation, i.e. the
inner product of the probability vector with the {0,1}-mistake or loss vector — rather than as
a measure-theoretic random variable; the book's own Section 1.3.3 makes this identification
explicit ("denote in vector notation the expected loss of the algorithm by
"), so no probability space is introduced. Theorem
1.1's "deterministic algorithm" is a causal map from an outcome history to a prediction
(prediction at round depends only on outcomes before ), instantiated at the book's own
two-expert construction (one expert always predicts , the other always ) rather than a
fully general -expert adversary argument — a strictly weaker instance of the general claim,
but the exact one the book's proof establishes, so no scope is lost relative to what is proved.
is kept as an explicit free parameter throughout, per the book's own presentation
(no substitution of the corollary's optimized
into the milestone statements).
A trivializing formalization to rule out: fixing (a single expert) would make Lemmas 1.3–1.5 hold vacuously with regardless of the potential-function argument; every formal statement here quantifies over an unconstrained with , not a hard-coded small case.
The mission needs no Mathlib infrastructure beyond finite sums, Real.log, and Real.exp; the
book's own OCO protocol and regret definition (§1.1) are not needed, since this chapter's
proofs work directly with mistake/loss counts (per the chunk brief). BanditAlgorithm.ftrl_simplex_exp_weights_regret (Bandit Algorithms XII, Prop. 28.7, arXiv:2003.05963 §28) proves
for exponential weights on the simplex against -valued losses,
via an FTRL/mirror-descent instantiation — the same asymptotic phenomenon as Theorem 1.5, but a
different proof technique, a different (bounded, not merely non-negative) loss assumption, and
stated for simplex-comparator regret rather than the per-expert loss comparator here; it is
listed as a reference/comparison point, not reused.
Two-stage stochastic linear programming with recourse models a decision made before uncertainty resolves (the first-stage variables ) followed by a corrective decision made after (the second-stage, or recourse, variables ). Solving such a program means minimizing , where is the expected cost of the best recourse action given -- an object defined only implicitly, as the value of an embedded linear program that must be solved (or bounded) for every realization of the uncertain data. Before any algorithm for this problem can be justified -- the L-shaped method, stochastic decomposition, scenario decomposition, all developed in later chapters of Birge & Louveaux, Introduction to Stochastic Programming (Springer, 2011) -- one needs to know that is well-behaved enough to optimize over at all: that the feasible region is closed and convex, that itself is a finite, Lipschitz, convex function on it, that an optimal solution is actually attained rather than only approached in the limit, and finally what an optimality condition for the resulting nonsmooth convex program even looks like. This mission formalizes exactly that foundational layer, Chapter 3, Section 3.1 of the book.
Fix natural numbers and a finite scenario count . A two-stage recourse instance consists of first-stage data , , , a fixed recourse matrix , and, for each scenario , a cost vector , a right-hand side , a technology matrix , and a probability with (Eq. (1.1)). The first-stage feasible region is .
For a fixed and scenario , the second-stage value is
(Eq. (1.6)), taken as an extended real: if no feasible exists, if the inner program is unbounded below. The expected recourse value is (Eq. (1.3)), combined so that -- the book's own convention (p. 109): infeasibility in one scenario is treated as fatal even if another scenario is unboundedly favorable. The second-stage feasibility set is , and the deterministic-equivalent objective is (Eq. (1.2)). For with finite, the subdifferential is the set of satisfying for every (p. 115).
A simple-recourse instance is the special case : the recourse cost splits as , and decomposes componentwise via the closed form of Eq. (1.9)-(1.10) using the (left- and right-limit) distribution functions of each .
given that (1.2) has a finite optimal value. This is the KKT-style necessary and sufficient optimality condition for the two-stage recourse LP, and the weakest of the mission's targets in the sense that everything else supports it: convexity and finiteness of (Theorem 6) are what make the left-to-right implication meaningful, closedness/convexity of (Theorem 5) makes the feasible region well-posed, and attainment (Theorem 8) is what makes " is optimal" a statement about a point that exists rather than an infimum that may not be reached.
Theorem 9 is the hinge on which the rest of the book's algorithmic chapters turn. The L-shaped method (Chapter 5) is a cutting-plane scheme whose cuts are literally elements of ; stochastic decomposition and sampling-based methods use the same subdifferential structure with estimated cuts; the differentiable specialization (Eq. (1.14), ) underlies nonlinear-programming approaches to the smooth case. None of this is meaningful without first knowing is convex, finite where it needs to be, and that a minimizer exists to characterize. Formalizing this mission's four milestones from the actual definition of as an embedded linear program's value -- rather than assuming these properties -- is exactly the content the book itself proves (or, for Theorem 6, explicitly cites to Wets [1972] and Kall [1976] rather than proving); this mission asks for genuine Lean proofs of Theorems 5, 8, 9 and Corollary 10 from the LP structure of , and records Theorem 6 as a stated (not re-derived) input, matching the book's own presentation.
The obvious shortcut is to treat as an opaque convex function and apply a textbook convex-KKT
theorem off the shelf. This fails to capture what Theorem 9 actually is: a statement about the
specific function , built from finitely many parametric linear programs, each of which can be infeasible
() or unbounded () depending on . Convexity of
must come from convexity of the value function of a parametric LP in its right-hand side
(the book's Theorem 2 argument: a convex combination of optimal solutions at two right-hand
sides is feasible, hence suboptimal, at the combined right-hand side) -- not from an assumed
hypothesis. Handling correctly is a second, easy-to-miss source of error: the book
fixes an explicit, non-default convention ( dominates ) for combining
per-scenario values, the opposite of the convention Mathlib's own extended-real arithmetic uses,
so any formalization that reaches for EReal's built-in addition to aggregate silently
states a different theorem. Theorem 8's attainment condition is a genuine existence result, not
an automatic consequence of convexity: continuity alone does not give attainment on an unbounded
feasible region, and the book's own counterexample (Eq. (1.11), a negative-exponential tail with
infimum attained by no finite ) shows the boundedness/recession hypotheses are load-bearing.
The scenario set is modeled as Fin K, a finite discrete random variable, matching Section
3.1b's development; under this model " has finite second moments" (the standing hypothesis
of Theorems 4-11 in the general, possibly-continuous case) holds automatically and so does not
appear as a separate hypothesis anywhere in this mission. Q(x,\xi_k) is defined as an EReal
via sInf of the second-stage LP's feasible objective values -- sInf of the empty set is
⊤, and of a set unbounded below is ⊥ -- and is genuinely derived from that inner
minimization rather than assumed convex; this rules out the chapter's trivializing
formalization, which the paper-level triage explicitly warns against: taking Q(x) as an
opaque convex-function hypothesis instead of deriving its properties from the inner LP's
structure. Aggregating the per-scenario values into uses a bespoke bookAdd operation
implementing the book's stated convention , since Mathlib's EReal
addition is defined with the opposite convention (). is
the ordinary subgradient-inequality set for this extended-real-valued function.
Theorem 8's condition (b) is stated with the book's own quantifier structure: the threshold
and the recession value depend on the point and direction exactly as
written, with no strengthening. Theorem 6(a)'s Lipschitz bound is stated, not derived -- the book
itself cites it to Wets [1972] and Kall [1976] without proof -- so a faithful Lean proof of that
milestone is expected to remain out of scope for this mission. Corollary 10 similarly takes the
closed form of from Eq. (1.10) as a hypothesis on an abstract , matching how
the book itself uses (1.10) as an already-established fact rather than re-deriving it from the
second-stage LP in the corollary's own proof. Theorem 11's subdifferential-decomposition result
() is deliberately left out of
this mission's scope: it is not needed by Theorem 9's own proof, and its normal-cone term would
require relatively-complete-recourse machinery this mission does not otherwise need. No prior-art
match was found on the platform: VectorSpaceOpt.fenchel_duality and the Luenberger-derived
VectorSpaceOpt.generalized_kuhn_tucker / kkt_complementary_slackness family use a
differentiable (Gateaux-derivative) or conjugate-function KKT model over general normed spaces,
not this chapter's finite-dimensional, possibly-nondifferentiable subgradient formulation over
the specific polyhedral set , so none is a faithful match and all items here are original
drafts.
Let be an odd squarefree positive integer and let be a set of units modulo with . Then : every residue class, unit or not, is a sum of three elements of .
This is Corollary 1.5 of Xuancheng Shao, A density version of the Vinogradov three primes theorem, Duke Math. J. 163 (2014) 489-512, arXiv:1206.6139v2. It is the local input to Shao's density version of the three primes theorem, and it is a clean finite statement in its own right.
At the set has five elements, so exactly, and is not a sum of three of its elements. The hypothesis therefore fails by nothing at all and the conclusion already fails. If is weakened to , the statement is false.
The corollary cannot be proved by induction on sets. Passing from to a prime factor splits into fibers of different densities, and a set is the wrong object to carry through that split. The induction has to run on functions , and the corollary is the case of a weighted statement, Proposition 1.4. That is the one step from which the rest follows.
The weighted statement then splits at the primes 3 and 5. For coprime to 30 the induction runs on the prime factors, using Cauchy-Davenport-Chowla for three sets modulo a prime, and it produces the stronger bilinear conclusion . The modulus 15 is handled separately by a linear program over the eight units. Two averaging inequalities, one symmetric and one asymmetric, are what turn a density above into a single good triple in both halves.
The nine milestones follow Shao's own numbering: the two averaging inequalities of Section 2 (Lemmas 2.1 and 2.2), the finite check at (Lemma 2.3), the three-set Cauchy-Davenport-Chowla bound, the divisor reduction that lets the proof assume , the induction away from 3 and 5 (Proposition 3.1), the modulus-15 case (Proposition 3.2), the weighted local result (Proposition 1.4), and the counting bridge that the units modulo number .
Every item is stated in Mathlib primitives alone, so the mission needs no definition items: IsUnit, Nat.totient, Odd, Squarefree, Finset, and Antitone. The set of units modulo is written Finset.univ.filter (fun x => IsUnit x) at each use rather than through a defined abbreviation, so a reader auditing a statement has to trust only Mathlib. That is also why open scoped Classical appears in the preamble.
The density hypothesis is written 5 * Nat.totient m < 8 * A.card, which is cleared of division so the whole statement stays in with no rounding.
Almost every competitive online algorithm built by the primal-dual method rests on the same two facts about a pair of linear programs. The first is weak duality: any feasible solution of the dual is a lower bound on any feasible solution of the primal. The second is complementary slackness: if a feasible primal-dual pair satisfies a local, per-coordinate tightness condition, the pair is optimal — and if it satisfies that condition only up to factors and , the primal is within of optimal.
The second fact in its approximate form is the engine of the whole method. An online algorithm cannot compute an optimum; what it can do is maintain a primal solution and a dual solution side by side so that each new request preserves an approximate tightness invariant. The approximate complementary slackness theorem then converts that local invariant into a global competitive ratio, with no reference to the optimum at all. Chapter 2 of Buchbinder's thesis states it as the background result on which the rest of the work is built.
Fix finite index types (primal variables) and (primal constraints), a matrix , a cost vector and a right-hand side . The covering primal and packing dual are
Note the index convention: carries the primal-variable index first, so the primal constraint indexed by sums over and the dual constraint indexed by sums over .
Given , the pair satisfies approximate complementary slackness when
For a primal-feasible , a dual-feasible , and satisfying the two conditions above,
Taking recovers exact complementary slackness and hence optimality of both members of the pair. The goal is stated with the source's hypotheses, including the two-sided bounds, rather than the weakest hypotheses that make the inequality go through; a separate item records the minimal-hypothesis strengthening.
with no nonnegativity assumption on , or beyond feasibility itself.
Strong duality is not proved in this mission. The platform already carries LinearOptimization.lp_strong_duality, proved in this exact environment, for linear programs in Bertsimas–Tsitsiklis general form over Fin-indexed data. This mission's contribution is an adapter: from a primal optimum of , produce a dual optimum of of equal value, for Fin-indexed instances. Reference items point at the imported theorem, its dual construction, and the dual-of-dual identity.
The biconditional — a dual optimum exists if and only if a primal optimum does — is deliberately left open. Weak duality does not derive the existence of a primal optimum from the existence of a dual one; the reverse implication needs strong duality applied to the dual program together with the dual-of-dual identity, and that reduction is not yet compiled. It is offered as a parallel target rather than claimed as established.
This mission is the foundation of the series. Every later mission — set cover, ski rental, and the online covering and packing problems that follow — states its approximation or competitiveness result as an instance of approximate complementary slackness. Formalizing it once, over arbitrary finite index types, is what makes the later missions short.
It also fills a real gap. Mathlib currently has no linear-programming duality: four separate attempts were closed unmerged. Approximate complementary slackness appears not to be formalized in any public library, so the goal theorem is, as far as we can determine, first of its kind.
The goal is a summation argument, not a deep theorem: the work is in handling the per-coordinate case split on versus and in interchanging a double sum. Three mechanical milestones isolate exactly those steps. The strong-duality adapter is the hard item, because it must reconcile two different presentations of the same program — index types, matrix orientation, and bundling all differ between our definitions and the imported theorem's.
Definitions cover §2.1 of the source. Four distinct notions of "the program has a finite optimum" are separated on purpose — attained optimum, nonempty feasible set, bounded objective, and the conjunction — because the source's informal word "bounded" conflates them. The definitions are stated over arbitrary finite index types; the strong-duality items are stated only for Fin, because that is the only index type for which the imported dependency path exists.
Mirror symmetry began as an empirical observation in string theory: certain pairs of Calabi–Yau threefolds, with no evident geometric relation, give rise to the same physical theory, and invariants that are hard to compute on (counts of holomorphic curves) turn into easy computations on (variations of complex structure). The paper Mirror symmetry is T-duality by A. Strominger, S.-T. Yau and E. Zaslow, Nucl. Phys. B 479 (1996) 243–259, proposed the first structural explanation: should carry a fibration by special Lagrangian 3-tori, the mirror should be obtained by replacing each fibre with its dual torus, and the mirror map should be fibrewise T-duality. This proposal is now called the SYZ conjecture, and it organises most later geometric work on mirror symmetry.
The string-theoretic argument of Sections 1–2 of the paper is heuristic and is not formalizable as stated. Section 3 is different: it is a self-contained piece of differential geometry about the moduli space of a special Lagrangian submanifold together with a flat connection on it. This mission formalizes Section 3.
A short timeline of the mathematics the section rests on:
Fix . The ambient Calabi–Yau manifold is modelled by , carrying
Here is the standard Hermitian product of , conjugate-linear in its first argument.
The brane is an -torus. It is presented by its universal cover: a map that is periodic up to translation,
for a fixed family of periods . Such an is exactly a map of the torus into the complex torus , and integration over is integration over the unit cube .
Write for the partial derivatives of . The map is Lagrangian at if for all , i.e. ; it is special Lagrangian if in addition , i.e. . This is the supersymmetry condition of the paper (Section 2, conditions (ii) and (iii)). The induced metric is , the volume density is , and the second fundamental form of a Lagrangian immersion is the totally symmetric tensor
Given a family of such maps, its deformation -form is
the -form obtained by contracting the velocity into the Kähler form. For an -parameter family , , one gets such forms , , one per moduli direction.
The moduli data of Section 3 is a smooth -parameter family of special Lagrangian tori, all with the same periods, subject to two normalizations taken from the paper: each is harmonic for the induced metric (closed and co-closed), and the cohomology class of each is constant along the family. The (McLean) metric on the moduli parameters is
The full moduli space of the paper also records the flat connection; its moduli form a torus of the same dimension, with coordinates . On , modelled by with coordinates , the paper puts the block-diagonal metric and the constant almost complex structure , , with fundamental -form .
The goal theorem is the conclusion of Section 3: for every such family, the fundamental -form of the moduli space is closed,
and since is constant in these coordinates it is integrable, so is Kähler.
The milestones are the numbered intermediate results of the paper, in the paper's own order:
$$\textbf{ closed:}\quad \partial_c \int_L \theta^{a_1}\wedge\cdots\wedge\theta^{a_n} = 0 .
\textbf{Hessian} \Rightarrow \textbf{Kähler:}\quad \partial_a g_{bc} = \partial_b g_{ac} ;\Longrightarrow; d,\omega_{\mathcal M} = 0 .$$
Together, Propositions 1 and 2 are the statement that the tangent space to the moduli space consists of harmonic -forms — McLean's theorem in the form the paper uses it. Eq. (3.4) is the technical heart, and the last milestone is the step from it to the goal.
The result. Section 3 supplies the only rigorous mathematics in the paper. It says that the object the physics predicts to be a Calabi–Yau manifold — the moduli space of a supersymmetric brane — does carry the first piece of that structure, a Kähler metric, and that it carries a natural -form which, for toroidal branes, is a holomorphic -form and hence a candidate for the Calabi–Yau form of the mirror. Eq. (3.4) says the McLean metric is locally the Hessian of a potential; this affine-Hessian structure of the SYZ base is the starting point of the later large-complex-structure-limit programme.
Formalizing it. The Section 3 results have rigorous published proofs (McLean for the tangent space, Hitchin for the Hessian property), but no machine-checked proof exists for any of them, and Mathlib currently has no special Lagrangian geometry, no Hodge theory, and no differential forms on manifolds. The mission therefore also produces reusable infrastructure: a workable coordinate model of calibrated submanifold geometry, the variation formulas for the induced metric and for the pullbacks of and , and the Hessian-metric criterion for a Kähler structure, which is independent of the rest and reusable wherever affine-Kähler geometry appears.
The obvious approach to the goal — "the metric is Hessian, so take the potential and write down the Kähler form" — is not available: the potential is not part of the data, and producing it requires the symmetry first. That symmetry is the hard step, and it is hard for a specific reason: differentiating in the direction produces four terms — from , from , from the inverse metric , and from the volume density — and only their sum is symmetric in . Two of them are killed by an integration by parts that needs both harmonicity of and compactness of (this is where the torus, and not a coordinate patch, is essential); one is killed because a special Lagrangian submanifold is minimal, so the mean curvature term in vanishes; what survives is , which is symmetric because is a symmetric -tensor. Every one of those four cancellations has to be carried out.
Proposition 2 carries a separate difficulty: it is an identity between the variation of a determinant and a divergence, and it is false without the hypothesis that is special Lagrangian at the point in question — for a merely Lagrangian there is a further term proportional to the Lagrangian angle.
The formalization commits to the following, all of which are visible in the definition item and none of which are silent:
fderiv returns at a point of non-differentiability, so a statement about derivatives of a non-smooth map is a statement about zeros; every item therefore carries an explicit smoothness hypothesis, and the moduli-level items carry it inside the family structure.A complete development needs, beyond the definition item: the chain and product rules for fderiv on , symmetry of second derivatives, differentiation under the integral sign on a compact box, integration by parts for periodic functions on , and the derivative of and of matrix inversion. The last two, and the Hessian-implies-Kähler milestone, are reusable outside this mission. Contributions that replace the flat ambient by a general Kähler ambient chart, or that lift the model to Mathlib manifolds once differential forms exist there, are welcome and would supersede parts of this development.
Waldspurger's non-standard fundamental lemma is an identity between stable orbital integrals on the Lie algebras of two reductive groups that are not isomorphic, and not even isogenous as algebraic groups, but whose root data become identified after tensoring with . The basic example is the pair , whose root systems and are exchanged by Langlands duality; the identity is what allows the twisted fundamental lemma to be deduced from the ordinary one. Waldspurger formulated the conjecture in L'endoscopie tordue n'est pas si tordue (2008); it is Theorem 1.12.7 of Bao Chau Ngo, Le lemme fondamental pour les algebres de Lie, Publ. Math. IHES 111 (2010), 1-169 (DOI), proved there in equal characteristic by the same Hitchin-fibration argument that gives the ordinary fundamental lemma.
Before any of that geometry can start, the two sides have to be compared: one needs a single Cartan subalgebra, a single Weyl group and a single space of characteristic polynomials serving both groups at once. Producing that comparison is a self-contained piece of linear algebra over the root data, carried out in Ngo's §1.12, and it is what this mission asks for.
Let and be split reductive groups over a field, pinned, with maximal tori and . Each is determined by its root datum , where is the set of roots, the set of coroots and the set of simple roots singled out by the pinning.
An isogeny of root data between and (Ngo, Definition 1.12.1) is a pair of isomorphisms of -vector spaces
which are transposes of one another, such that carries the set of lines () bijectively onto the set of lines (), matching lines of simple roots with lines of simple roots, and such that has the same property for the lines spanned by coroots. Two semisimple groups with the same adjoint group are isogenous in this sense; so are a group and its Langlands dual, the interesting cases being , and , where a short root is sent to and a long root to with . Groups obtained by twisting a pair of isogenous pinned groups by a common torsor are called paired.
A prime is good with respect to when it divides neither of the indices
the two lattices being compared inside the single -vector space identified by .
i.e. conjugation by carries the Weyl group acting on onto the Weyl group acting on . Ngo's reason is that the reflection attached to a root depends only on the line through that root, so the bijection of root lines transports reflections to reflections. This equivariance is what makes the induced isomorphism descend to an isomorphism of the spaces of characteristic polynomials, which is Lemme 1.12.6 and which is what allows two points and with to be compared at all.
Two steps lead there: the reflection computation that makes a matched pair of root lines give a matched pair of reflections, and the integral statement behind Ngo's good-characteristic hypothesis — that when the two indices above are invertible in the base ring, the two lattices become identified after base change.
Theorem 1.12.7, the non-standard fundamental lemma, asserts that for two paired groups over with residue characteristic exceeding twice the Coxeter numbers, and for points and corresponding under , the stable orbital integrals of the characteristic functions of and agree. Waldspurger showed that this identity, together with the ordinary fundamental lemma, implies the twisted fundamental lemma. None of the objects in that statement — reductive group schemes over a discrete valuation ring, orbital integrals, Haar measures on the centralizer tori — exists in Mathlib today. The comparison of §1.12 does not need any of them: it is a statement about lattices, root systems and Weyl groups, and it is a strict prerequisite, since without the isomorphism the two sides of Theorem 1.12.7 cannot even be matched up.
Beyond this paper, the notion of an isogeny of root data and the good-characteristic base change of a pair of lattices are reusable: they are the standard bookkeeping behind Langlands duality for split groups, and neither is currently available.
The reflection step looks like a one-line computation and is one — but only once the two proportionality constants are known to agree. If and , the conjugate of is exactly when , and that is forced by transposition together with . The genuine difficulty in the goal is different: the definition only says that and permute lines, so one has to show that the bijection induced on root lines and the bijection induced on coroot lines are the same bijection. A solver who assumes this without proof has assumed the substance of 1.12.4.
The lattice milestone has its own trap: the quotient must be shown to have vanishing after base change, not merely to vanish, or the inclusion becomes only surjective.
Root data are modelled by Mathlib's RootPairing ι ℚ M N, with the character space,
the cocharacter space, and rational coefficients throughout, so that "tensoring with
" is built into the ambient objects rather than performed explicitly. A choice of
simple roots is recorded as a subset of the index type rather than as a RootPairing.Base;
nothing in the statements depends on that subset beyond its role in the definition of an
isogeny. The Weyl group is the subgroup of linear automorphisms of the cocharacter space
generated by the coreflections, which is the form in which it acts on the Cartan.
The goal is stated as a two-sided intertwining property rather than as an equality of subgroups: every element of is intertwined by with some element of and conversely. This avoids introducing a conjugation homomorphism, and it is the form in which the statement is used. Both root pairings in the goal are required to be finite, reduced root systems, matching Ngo's hypothesis that and are reductive groups.
The good-characteristic condition is formalized exactly as Ngo writes it, by the invertibility in the base ring of the two indices, each expressed as the cardinality of an explicit quotient group; the conclusion is the bijectivity of the map induced on the tensor product by the inclusion of the intersection. If a quotient were infinite its cardinality is reported as , and invertibility of then forces the base ring to be trivial, so no false statement hides in that corner.
No statement here is vacuous: any pair consisting of a root system and itself, with and the identity, satisfies every hypothesis, and the pair gives the intended non-trivial instances.
A stochastic partial differential equation is driven by noise that lives on an infinite-dimensional function space, and the first object one has to control is the law of that noise: a Gaussian measure on a separable Banach space. Martin Hairer's lecture notes An Introduction to Stochastic PDEs (arXiv:0907.4178) devote their first technical chapter (Section 4) to exactly this, because every later construction — stochastic convolutions, invariant measures for semilinear equations, the ergodic theory of the stochastic Navier–Stokes equations — is phrased against it.
The single structural fact that chapter produces is the Cameron–Martin theorem (Theorem 4.44, p. 31). It answers the question: in which directions may one translate an infinite-dimensional Gaussian measure without destroying its null sets? In finite dimensions the answer is "all of them", because Lebesgue measure is translation invariant. In infinite dimensions the admissible directions form a proper, and typically much smaller, Hilbert subspace — the Cameron–Martin space — and the translated measure is either equivalent to or mutually singular with it, with nothing in between. This dichotomy is the reason Girsanov-type changes of measure, Schilder-type large deviation rate functions, support theorems and Malliavin calculus all take the form they do.
Throughout, is a separable Banach space, its topological dual, and a Borel probability measure on .
is Gaussian (Definition 4.4, p. 19) if for every continuous linear functional the push-forward is a Gaussian measure on in the sense of Definition 4.1, i.e. has characteristic function ; the degenerate case , a Dirac mass, is included. It is centred if all these one-dimensional laws have mean zero, which is expressed here as .
For a centred Gaussian the covariance form (4.2, p. 20) is
It is well defined because is -integrable, and it is a bounded bilinear form (Corollary 4.14, p. 22).
The Cameron–Martin space (Definition 4.26, p. 27) is classically built as the completion of
under . This mission uses the equivalent intrinsic description of Exercise 4.38 (p. 29), which avoids the completion:
The supremum is taken in ; since is admissible whenever is, it equals over the same set. For write , .
For a centred Gaussian measure on a separable Banach space and ,
Both implications are asserted: translation along a Cameron–Martin direction produces an absolutely continuous measure, and translation along any other direction does not (in fact it produces a mutually singular measure).
The milestone list follows the route of Section 4.2:
The Cameron–Martin theorem is what makes the Cameron–Martin space a canonical object rather than a formal construction: is simultaneously the set of admissible shifts, the intersection of all full-measure linear subspaces (Proposition 4.45), and the space whose unit ball governs Gaussian isoperimetry (Theorem 4.53, Borell–Sudakov–Cirel'son). Downstream in the notes it is used to identify invariant measures of linear SPDEs and to compare them; outside the notes it is the starting point of Malliavin calculus and of large deviation theory for Gaussian measures.
Status, precisely. The Mathlib library pinned by this mission already contains a substantial part of Section 4: the predicate IsGaussian (Definition 4.4), uniqueness of measures with equal characteristic functionals on a separable Banach space (Propositions 4.8 and 4.11), invariance of under rotations (Proposition 4.12), Fernique's theorem (Theorem 4.13), and the covariance form of (4.2) together with its boundedness (Corollary 4.14) as a continuous bilinear form on the dual. Those results are therefore not milestones here; they are the assumed foundation. What is absent, and what this mission asks for, is everything from the Cameron–Martin space onwards: its definition, its elementary properties, and Theorem 4.44 itself. No machine-checked proof of the infinite-dimensional Cameron–Martin theorem is known to the captain in any Lean library.
The naive route — write down the two densities and take their ratio — is unavailable: there is no translation-invariant reference measure on an infinite-dimensional Banach space, so "the density of " does not exist and the Radon–Nikodym derivative of with respect to must be produced directly, as the exponential of a random variable.
That random variable is the obstruction. For the functional is continuous and the computation is a characteristic-function identity. But is in general strictly smaller than : a general has an associated that exists only as an -limit of continuous functionals, defined -almost everywhere and linear only on a measurable subspace of full measure (Propositions 4.34 and 4.39). Establishing that these limits are Gaussian with the expected variance (Proposition 4.40) is the technical bridge, and it is why milestone 3 is stated as a statement about -limits rather than about elements of .
The converse half has a different shape. One must produce, for , a single one-dimensional projection that separates from arbitrarily well; unboundedness of over the covariance unit ball supplies with and as large as desired, and the quantitative Gaussian total-variation bound of milestone 5 converts this into total variation distance , i.e. mutual singularity.
The development is in Lean 4 with Mathlib, in the namespace HairerSPDE, shared by the whole series drawn from these notes. The conventions it commits to:
NormedAddCommGroup, NormedSpace ℝ, its Borel σ-algebra, CompleteSpace and SecondCountableTopology — the last two encode "separable Banach space".IsGaussian, which is Definition 4.4 verbatim; centredness is the extra hypothesis , needed because IsGaussian permits a non-zero mean.covarianceBilinDual, which equals (4.2) for centred measures with finite second moment and is set to zero otherwise; Fernique's theorem rules the degenerate branch out for Gaussian measures.fun x ↦ x + h, absolute continuity is Mathlib's ≪, and "measurable linear subspace" is a Submodule ℝ B whose carrier is a measurable set.The goal is an equivalence, so neither half can be discharged vacuously: the direction is non-trivial already for in finite dimensions, and the converse has content precisely when . Note that always, and that for a Dirac mass the covariance form vanishes and ; both degenerate cases are inside the statement rather than excluded by hypothesis.
Contributions welcome beyond the milestones: the reproducing kernel space and the isomorphism of Proposition 4.34, measurable linear extensions (Proposition 4.39), the dilation singularity of Proposition 4.43, and in the infinite-dimensional case (second half of Proposition 4.45). All of these are reusable outside this mission.
For a complex parameter , iterate the quadratic map
starting at the critical point . The Mandelbrot set is the set of parameters for which this orbit stays bounded:
Equivalently -- and this is the first milestone of the mission -- if and only if for every , which exhibits as a compact subset of the plane.
is the parameter-space picture of the simplest non-trivial family in complex dynamics, and it acts as a dictionary: the shape of near a parameter encodes the dynamics of on its Julia set, so structural questions about are questions about the whole quadratic family at once. Douady and Hubbard proved in 1982 that is connected, by exhibiting a conformal isomorphism
between the complement of and the exterior of the closed unit disk.
MLC conjecture. is locally connected: every point of has a neighbourhood basis, in the subspace topology, consisting of connected sets.
By Caratheodory's theorem, MLC is equivalent to the statement that extends continuously to the unit circle. That extension would deliver a complete combinatorial description of -- the pinched disk model of Douady and Thurston -- in which every boundary point is labelled by the external rays landing on it. Two headline consequences follow: the density of hyperbolicity in the quadratic family (Fatou's conjecture: every quadratic polynomial can be perturbed to one with an attracting cycle), and zero area for .
MLC has been open since the early 1980s and is regarded as the central problem of one-dimensional complex dynamics.
The goal theorem is MLC itself, in the form "the Mandelbrot set, as a topological subspace of , is a locally connected space".
The milestones are of three kinds, and are ordered accordingly:
All statements are phrased against a single shared definition file, so a solver can move between milestones without re-fixing conventions.
Chapter 11 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) replaces the Riemann integral of Chapter 6 with the Lebesgue integral, and the reward is a theory of integration whose limit theorems have no superfluous hypotheses and whose space of square-integrable functions is complete. The chapter runs from set functions and outer measures, through the Carathéodory construction of Lebesgue measure, measurable functions and the integral, to the convergence theorems (monotone convergence, Fatou, dominated convergence) and finally to the space and the Riesz–Fischer theorem (Theorem 11.42):
That completeness is what makes a Hilbert space, and it is the reason the Fourier series of Chapter 8 converge in the mean to the functions they represent.
This mission is the eleventh and last in a series formalizing Rudin Chapters 1–11. It uses the Riemann–Stieltjes integral of Mission VI (for Theorem 11.33, comparing the two integrals) and the trigonometric Fourier series of Mission VIII (for the reading of Parseval's theorem).
A set function on a ring of sets is countably additive if it takes the value on a countable disjoint union. Rudin constructs an outer measure from such a by covering with elementary sets and taking an infimum, calls a set measurable when it is approximable by elementary sets in the metric , and proves that the measurable sets form a -algebra on which is countably additive (Theorem 11.10). A real function is measurable when is measurable for every , and the integral is defined first for simple functions, then for nonnegative measurable functions as a supremum, and then for general by .
The space consists of the measurable with , normed by ; a sequence converges in the mean to if .
Mathlib's measure theory is used wherever it is mathematically the same object:
MeasureTheory.OuterMeasure and its Carathéodory -algebra, MeasurableSet,
Measurable, the lower Lebesgue integral ∫⁻ for nonnegative extended-real functions, the
Bochner integral ∫ and Integrable for the general case. What is set up freshly is Rudin's
of functions — Rudin.MemL2, Rudin.L2Norm, Rudin.CauchyL2,
Rudin.TendstoL2 — rather than Mathlib's quotient space Lp, because the Riesz–Fischer theorem
as Rudin states it produces an honest limit function, and the ε-N phrasing of Cauchyness and
of mean convergence is part of the statement.
If is a Cauchy sequence in , then there exists with : the space is complete.
Rudin's proof extracts a subsequence with , sums the telescoping series, uses the monotone convergence theorem and the Schwarz inequality to show that the sum converges almost everywhere, and identifies the pointwise limit as the mean limit of the whole sequence. Every ingredient is a milestone of this mission.
The Lebesgue theory is the point at which analysis acquires limit theorems that do not require uniform convergence. Monotone convergence, Fatou's lemma and dominated convergence are the three statements that make the integral usable in probability, in Fourier analysis and in the theory of partial differential equations, and the Riesz–Fischer theorem is what makes a Hilbert space and therefore the natural home of Fourier expansions: Parseval's identity (11.45) is the assertion that the Fourier coefficient map is an isometry onto .
Theorem 11.33 is the bridge back to the earlier chapters — every Riemann-integrable function is Lebesgue-integrable with the same integral, and a bounded function on is Riemann-integrable exactly when it is continuous almost everywhere — so the two halves of the book agree wherever both apply.
Mathlib has an extensive measure theory and proves many of these results in considerable generality. This mission's contribution is to state them in Rudin's formulation, for Rudin's of functions and with his explicit ε-N definitions, so that the chapter is available as a coherent, self-contained unit that matches the textbook line by line and links back to the Riemann–Stieltjes integral of Mission VI.
Individually, most milestones will reduce to Mathlib results after the correct dictionary is in
place, and the interesting work is exactly in that translation: Rudin's measurability
({x : f(x) > a} measurable) versus Mathlib's Measurable, Rudin's integral of a nonnegative
function versus ∫⁻ with values in ℝ≥0∞, Rudin's of genuine functions versus
Lp as a quotient by almost-everywhere equality. The last of these is what makes the goal
theorem nontrivial to derive: Mathlib's completeness of Lp gives a limit class, and one must
choose a measurable representative and verify Rudin's mean convergence with the concrete norm
Rudin.L2Norm, which is Real.sqrt (∫ f²) and not an ENNReal quantity.
Theorem 11.33 (Riemann implies Lebesgue) and Theorem 11.38 (density of continuous functions)
are the two other places where real work is required: the first has to connect the Chapter 6
definition of the Riemann integral with intervalIntegral, and the second is an approximation
argument.
Conventions fixed by this mission:
MeasureTheory.Measure, MeasurableSet,
Measurable, Integrable, ∫⁻ x, f x ∂μ for nonnegative ℝ≥0∞-valued integrands and
∫ x, f x ∂μ for the general real case. Rudin's Carathéodory construction is
MeasureTheory.OuterMeasure.caratheodory.ℝ≥0∞-valued
functions, matching Rudin's use of extended real values there.Rudin.MemL2 μ f is "f is measurable and f² is integrable"; Rudin.L2Norm μ f is
Real.sqrt (∫ x, (f x)^2 ∂μ); Rudin.CauchyL2 and Rudin.TendstoL2 are Rudin's ε-N Cauchy
condition and mean convergence. No quotient is taken, so the goal theorem produces a function.Rudin.RiemannIntegrable and Rudin.RiemannIntegral from
Mission VI, so the two integrals are literally compared.Contributions of the convergence theorems (11.28, 11.31, 11.32) and of the Schwarz inequality (11.35) are especially useful, since the goal theorem consumes them directly.
Chapter 8 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) puts the general theory of the preceding chapters to work on concrete functions. Power series are differentiated term by term; the exponential function is defined by its series and the trigonometric functions and the number are extracted from it; the fundamental theorem of algebra is proved; Fourier series are introduced through general orthonormal systems; and the Gamma function is characterized by log-convexity.
The chapter's capstone is Parseval's theorem (Theorem 8.16): for Riemann-integrable -periodic functions, the Fourier series converges in the mean square sense and the inner product is computed by the (absolutely convergent) sum of products of Fourier coefficients. It is the statement that the trigonometric system is not merely orthonormal but complete, and it is the finite-dimensional Pythagorean theorem carried to infinite dimensions.
This mission is the eighth in a series formalizing Rudin Chapters 1–11; it uses the convergence tests of Mission III and the uniform-convergence and approximation theorems of Mission VII, and it is the analytic counterpart of the abstract theory of Mission XI.
A power series is ; by Chapter 3 it converges on an interval . A sequence of complex functions on is an orthonormal system if for and ; the Fourier coefficients of relative to it are , and the Fourier series is . For the trigonometric system on one writes
A trigonometric polynomial is a finite sum . The Gamma function is for .
For Riemann-integrable -periodic and with Fourier coefficients and :
Parseval's theorem is the completeness statement for the trigonometric system: Bessel's inequality (8.12) holds for every orthonormal system, and equality for all is exactly what distinguishes a complete system. The proof shows how the pieces of the book fit together: it uses the approximation theorem 8.15 (itself a corollary of Stone–Weierstrass from Chapter 7), the minimizing property 8.11, and the Schwarz inequality of Chapter 1. Chapter 11 generalizes the conclusion to arbitrary complete orthonormal systems in , where the Riemann-integrable hypothesis can be dropped.
The other milestones are where the elementary functions acquire their properties: the -periodicity of the complex exponential, the definition of as twice the first positive zero of the cosine, and the log-convexity characterization of the Gamma function are all established here rather than assumed.
Mathlib has the exponential and trigonometric functions, , the fundamental theorem of algebra, the Gamma function with the Bohr–Mollerup theorem, and a Fourier theory on the additive circle. The work in this mission is to state Rudin's versions — -periodic functions on , generic orthonormal systems on an interval, Riemann-integrable rather than square-integrable hypotheses — and connect them to that library.
Parseval's theorem is where an approximation argument in the uniform norm has to be converted into one in the mean square norm. The chain is: approximate in by a continuous periodic (a nontrivial step for a merely Riemann-integrable , and the place where the hypothesis is really used), approximate uniformly by a trigonometric polynomial , and then use the minimizing property of the partial sums to conclude is small. The first step has no analogue in the uniform theory and is the main obstacle; the third depends on being an orthogonal projection, which is Theorem 8.11.
Conventions fixed by this mission:
∫ x in a..b, f x, not the real-valued Riemann–Stieltjes integral built in Mission VI; for
the Riemann-integrable integrands of this chapter the two agree. Integrability hypotheses are
stated as IntervalIntegrable.Rudin.fourierCoeff, Rudin.fourierPartialSum, Rudin.L2Norm,
Rudin.IsTrigPolynomial, Rudin.HasPeriodTwoPi, and, for general systems,
Rudin.IsOrthonormalSystem and Rudin.genFourierCoeff, all following Rudin's normalizations
(in particular the in and in ).Rudin.SeriesConvergesTo from Mission III, so that conditional
convergence is expressible; the two-sided sums of Parseval are
stated as limits of the symmetric partial sums , as in Rudin.Chapter 10 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) builds the calculus of differential forms in and proves the theorem that unifies the integral theorems of vector analysis. The fundamental theorem of calculus, the Green, divergence and classical Stokes theorems all say the same thing — that integrating a derivative over a region is the same as integrating the original object over the boundary of that region — and Stokes' theorem (Theorem 10.33),
is that statement, once "region" is made precise as a chain of parametrized surfaces and "derivative" as the exterior derivative.
This mission is the tenth in a series formalizing Rudin Chapters 1–11; it uses the inverse function theorem and the several-variable calculus of Mission IX.
For an open , a -surface in is a -mapping from a parameter domain — a -cell or the standard simplex — into ; surfaces are maps, not point sets. A -form in is a formal sum
with continuous coefficients, whose meaning is the rule assigning to each -surface the number
The exterior derivative of is the -form with coefficients ; the pullback along a differentiable substitutes into the coefficients and the differentials. A -chain is a formal integer combination of -surfaces with parameter domain , its integral is the corresponding combination of integrals, and its boundary is obtained from the alternating sum of the faces of .
If is a -chain of class in an open and is a -form of class in , then
For this is the fundamental theorem of calculus, for Green's theorem, for the divergence theorem, and for , the theorem of Stokes.
Stokes' theorem is the organizing theorem of multivariable analysis; its formal content is that and are adjoint, which is also the starting point of de Rham cohomology. Poincaré's lemma is its local converse: on a convex set the only obstruction to a closed form being exact disappears, so the failure of exactness measures the shape of the domain. The change of variables theorem (10.9) is what makes integrals independent of the parametrization and is used in the proof of Stokes itself, and partitions of unity (10.8) are the standard device for passing from local to global statements.
Mathlib has a general change-of-variables theorem for the Lebesgue integral, smooth partitions of unity, and the theory of alternating forms and de Rham differentials on manifolds; it does not have Rudin's concrete apparatus of parametrized surfaces, affine chains, and their boundaries, nor a version of Stokes' theorem for such chains. This mission builds that apparatus and states the chapter's theorems for it; the definitions are reusable for any development that wants a hands-on, coordinate-based treatment of forms.
This is the most demanding mission of the series, for two reasons. First, the objects have to be set up before anything can be said: forms as coefficient families, their integrals as Jacobian integrals, chains, and the boundary operator with its signs. Second, Stokes' theorem is proved by reducing to a single oriented simplex, transporting along the parametrization by Theorem 10.25, and then computing the integral over by an iterated integral in which all but two terms of the boundary cancel; the cancellation is entirely a matter of getting the signs of the face maps right, and it is where a formalization will spend its time.
A further subtlety: with forms presented by coefficients indexed by all index tuples, the identity is false coefficient-wise and true as an identity of forms. Since Rudin defines a form to be its integration functional, statements of the shape "this form vanishes" are formalized as "its integral over every surface vanishes", and that is how 10.20, 10.22(c) and 10.39 are stated here.
Conventions fixed by this mission:
Fin n → ℝ. A -form is Rudin.KForm k n, a coefficient
function indexed by all tuples Fin k → Fin n, following Rudin's equation (34).Rudin.integralOverCell and Rudin.integralOverSimplex are Rudin's equation (35) for the two
admissible parameter domains, with Rudin.jacobian the determinant of the matrix of partial
derivatives. The integral over the parameter domain is the Lebesgue integral for the volume
measure, which agrees with Rudin's Riemann integral for continuous integrands.Rudin.extDeriv and Rudin.pullback are the exterior derivative and the pullback;
Rudin.Chain, Rudin.Chain.integral and Rudin.Chain.boundary are chains with integer
multiplicities, their integrals, and the boundary built from the faces of the standard simplex
with Rudin's signs .ContDiff ℝ 1 and ContDiff ℝ 2 for Rudin's and .Contributions of the supporting differential-form identities (10.20, 10.22, 10.25) are especially welcome, since they are exactly the lemmas the goal theorem consumes.
Chapter 5 of Walter Rudin's Principles of Mathematical Analysis (3rd edition, McGraw-Hill, 1976) is the differential calculus of one real variable, developed from the definition of the derivative as a limit of difference quotients. Its organizing result is the mean value theorem and the family of consequences that follow from it: monotonicity criteria, L'Hospital's rule, and — the chapter's capstone — Taylor's theorem (Theorem 5.15), which approximates a function by a polynomial of degree and expresses the error exactly as a single -th derivative evaluated at an unspecified intermediate point.
Taylor's theorem is what makes differentiability quantitatively useful. It is the tool that turns local smoothness into explicit error bounds, and the estimates of Chapter 8 for the exponential, trigonometric and Gamma functions all rest on it.
This mission is the fifth in a series formalizing Rudin Chapters 1–11; it uses the continuity and compactness results of Mission IV.
Let be real-valued on . For the derivative is
whenever the limit exists. Higher derivatives are defined by iteration; exists on a set only if exists in a neighbourhood of each of its points. has a local maximum at if for all near .
Given a positive integer and a point , the Taylor polynomial of at of degree is
Let be continuous on , let exist for , and let be points of . Then there is a point strictly between and such that
For this is exactly the mean value theorem.
The mean value theorem converts a hypothesis about derivatives into a statement about increments, and everything in the chapter is an application of that conversion. Monotonicity criteria (5.11) are the basis of every "the function is increasing, hence injective" argument, including the change of variable in Chapter 6. Darboux's theorem (5.12) shows that derivatives, though not necessarily continuous, cannot have simple discontinuities — a fact that is easy to state and impossible to guess from the definition. Theorem 5.19 is the form of the mean value theorem that survives for vector-valued functions: the equality is lost (there need be no single point where the vector increment is proportional to the derivative), and only the inequality remains; the same phenomenon dictates the statements of Chapter 9.
Mathlib contains the mean value theorem, L'Hospital's rule, and a Taylor theorem with various remainder forms. The value of this mission is a statement of Taylor's theorem in Rudin's exact formulation — arbitrary distinct endpoints in , hypotheses only on and , an intermediate point strictly between them — and the derivation of the chapter's other results in a form the later missions can quote.
Taylor's theorem is proved by choosing the constant so that and applying Rolle's theorem times to ; the bookkeeping is in tracking that for and that each application produces a new intermediate point strictly inside the previous interval. In a proof assistant the iteration is the awkward part: the induction is on with the interval shrinking, and the statement must be general enough in and (either order) for the inductive step to apply. The hypothesis that exists only on the open interval, while is merely continuous on the closed one, must be preserved — strengthening it to on would make the statement weaker than Rudin's.
Conventions fixed by this mission:
deriv and iteratedDeriv, which are total functions returning
0 where the function is not differentiable; every statement therefore carries explicit
differentiability hypotheses exactly where Rudin states them.Set.Icc a b and Set.Ioo a b, and "for some between and
" is stated as an explicit disjunction, since the goal does not assume
.EuclideanSpace ℝ (Fin k), and the conclusion
is the inequality, not an equality — the equality version is false, as Rudin notes.A reservoir computer learns a dynamical input/output relation with a recurrent network whose internal weights are fixed once and never trained; only a linear readout on the state is fitted. The method works in practice — it is a standard tool for learning chaotic dynamics — but its justification requires an approximation theorem: the family of reservoirs used must be rich enough to reach any reasonable target system.
The target class is fixed by fading memory, the continuity notion Boyd and Chua introduced in 1985 for the approximation of nonlinear operators: a filter has fading memory when inputs that agree on the recent past produce nearby present outputs, however much they differ long ago. The question is then which reservoir families are dense in that class.
Non-homogeneous state-affine systems are the family that answers it. They are affine in the state, with coefficients depending polynomially on the input, and the density result proved for them is what every later universality theorem for reservoir computing rests on — including the one for echo state networks, whose proof approximates a target filter by a state-affine system first and only then by a network.
Timeline.
Time is indexed by the nonpositive integers, so an input has an infinite past and a present. Inputs are real-valued and bounded by one: the set of sequences with .
A non-homogeneous state-affine system is the reservoir
where is a polynomial with matrix coefficients, a polynomial with -vector coefficients, and the linear readout. Writing , the system is affine in the state and polynomial in the input.
Two constants govern it: and . When the state map contracts, the system has the echo state property — exactly one bounded state sequence per input — and the states obey . The induced map from input history to present output is the SAS functional .
Any fading memory filter on uniformly bounded scalar inputs is approximated, uniformly over all such inputs, by a state-affine system read out linearly.
The result itself. It is the density theorem of reservoir computing. Without it, nothing guarantees that a reservoir family can represent the system one is trying to learn, and the practice of fitting only a linear readout has no theoretical backing. It is also the input to the universality theorem for echo state networks: that proof replaces the target filter by a state-affine system before replacing it by a network, so the present result is a prerequisite rather than a parallel statement.
Formalizing it. The supporting target is a specialization of a result already published on this platform: a state-affine system is a contracting reservoir map, so its echo state property follows from the abstract contraction theorem rather than from a new argument. What this mission adds beyond that is the density statement itself, which is of a different nature — an approximation theorem in a function space, not a fixed point argument.
The obvious approach to the goal is to exhibit an approximating system directly, and it fails: the target is an arbitrary fading memory filter, given by no formula, so no construction can be read off it. The proof is not constructive in that sense. It proceeds instead by showing that the family of SAS functionals is a polynomial algebra which separates points and contains the constants, and by applying a Stone-Weierstrass argument on a space of input sequences made compact by the weighted topology.
Two points resist. The compactness is not that of the supremum norm — the space of uniformly bounded sequences is not compact for it — but of the weighted norm, and it is that topology in which the approximation is obtained. And the algebra property is delicate: the product of two SAS functionals must again be one, which is what forces the non-homogeneous form. The corresponding statement fails for linear reservoirs, whose products leave the family.
Time is indexed by , index denoting the instant steps into the past and the present; the system equation reads . This is a relabelling of the source's indexing, not a weakening.
Inputs are scalar, as in the source's Section 3, where the restriction is made explicit and the multidimensional extension deferred to a remark. Polynomials are given by their coefficient families, and evaluated as ; the bounds and are stated as explicit operator and norm bounds valid on rather than through a maximum, so that any valid bound may be supplied.
The fading memory property of the target is the one already published on this platform, stated for a functional rather than a filter: the two are in linear bijection, so nothing is lost and causality and time-invariance need not be formalized separately.
One trivialization is ruled out. The goal quantifies over state sequences satisfying the system equation, and the supporting target is what guarantees such a sequence exists and is unique under the stated bounds; without it, the approximation claim could be read as vacuous.
A complete development needs the Stone-Weierstrass theorem, available in Mathlib, together with compactness of the weighted sequence space, which is not and has to be built. Contributions are welcome on both targets.
An obstacle representation turns a graph into a visibility system: vertices are points in the plane, and nonedges are blocked by polygonal obstacles. The obstacle number asks for the minimum number of obstacles needed. OPG-37357 records two different questions for planar graphs. The first asks whether one obstacle can ever be insufficient. The second asks whether some universal constant bounds the ordinary obstacle number of every planar graph.
The status of the two parts is different. Berman, Chappell, Faudree, Gimbel, Hartman, and Williams proved in 2017 that explicit planar graphs, including the icosahedron and their graphs and , have ordinary obstacle number two. Thus the first question has a published positive answer. The universal-constant question remains the research target here. A separate invariant called planar or plane obstacle number requires a crossing-free visibility drawing; results for that invariant must not be substituted for the ordinary obstacle number used by this mission.
A finite simple graph has a -obstacle drawing when its vertices are placed injectively as points in and there are pairwise disjoint closed connected polygonal obstacles such that
Graph vertices lie outside every obstacle. The ordinary obstacle number is the least such . The drawing itself may contain crossings between visible graph edges; planarity is a property of the abstract input graph, not an extra constraint on the obstacle drawing.
The Lean model represents a polygonal obstacle as a connected finite union of closed filled triangles. This gives a compact polygonal region with exact real-coordinate segment incidence. Straight-line planarity of the abstract graph is represented separately.
The source records both
and
The first assertion is known in the literature and appears as a published-result milestone. The second is open and is therefore the mission's main theorem. Together they preserve the two-part source without presenting the whole record as unresolved.
A milestone formalizes the stronger published statement
This captures ordinary obstacle number exactly two without hard-coding one graph before its adjacency data and lower-bound certificate are formalized.
The open milestone asks for a single natural number , chosen before the graph, that works for every finite planar graph. The number of obstacle corners is not bounded by this theorem; only the number of connected polygonal obstacles is.
The published first part establishes that planarity alone does not force a one-obstacle representation. The second part asks whether planar graphs nevertheless have uniformly bounded visibility complexity. A positive answer would produce a common finite obstacle budget independent of graph order; a negative answer would require a family of planar graphs with unbounded ordinary obstacle number.
Formalization is especially useful because several nearby notions differ by one word but have different known bounds: ordinary versus plane obstacle number, arbitrary polygonal versus convex obstacles, and fixed-placement versus freely chosen drawings. The mission's definitions make those choices explicit and provide reusable segment-obstacle semantics for later geometric graph formalizations.
A finite combinatorial graph does not come with a canonical visibility drawing. Even when one starts with an arbitrary connected blocking set, replacing it by one bounded simple polygon requires compactness, component, incidence, and polygonal-neighborhood arguments. Conversely, lower bounds must quantify over every possible placement and obstacle, not merely refute a selected coordinate drawing.
Counting results for unrestricted graphs do not automatically preserve planarity. Bounds for planar obstacle number impose a crossing-free drawing and therefore answer a different question. The known two-obstacle examples close only the existential first part and give no universal .
All graph vertex types are finite. Obstacles are closed connected polygonal regions represented by finite triangle unions; they are pairwise disjoint and avoid graph vertices. Visibility uses the full closed segment, so tangency or boundary contact blocks a nonedge. The planarity witness is independent of the obstacle drawing. Empty and one-vertex graphs remain in the universal quantifier and should be handled without division or nonemptiness assumptions.
The repository's fixed-placement polygonization argument and finite arrangement code are candidate_only. They may motivate supporting lemmas, but they neither prove the unrestricted obstacle-drawing completeness theorem nor settle the universal bound. Contributions are welcome on exact geometry primitives, the published two-obstacle construction and lower bound, conversions between connected blockers and polygonal obstacles, and the universal root. A proof for the plane invariant, convex invariant, one fixed drawing, or a finite order cutoff must be labeled at that narrower scope.
An edge partition into cliques compresses the adjacency structure of a graph into complete pieces without allowing any edge to be counted twice. Erdős Problem 81 asks for the asymptotically sharp upper bound on the number of pieces needed when the graph is chordal. Chordal graphs have strong elimination structure, but that structure does not make the partition parameter additive under arbitrary edge deletion, and obtaining a linear error term remains substantially stronger than identifying the leading quadratic coefficient.
Erdős, Ordman, and Zalcstein studied clique partitions of chordal graphs in 1993. Their examples already exhibit the scale, while their general upper estimate had a larger quadratic coefficient. Later dense-packing results of Haxell–Rödl and Yuster compare fractional and integer triangle packings with an gap. The project candidate combines that interface with chordal elimination arguments to formulate a uniform milestone. It does not supply the remainder asked for by the root.
A finite simple graph is chordal when it has no induced cycle of length greater than three. The Lean definition uses the equivalent perfect-elimination form: vertices admit an injective ranking such that the later neighbors of every vertex form a clique.
An edge partition into cliques is a finite family of complete vertex sets such that every edge of belongs to exactly one member of . Members may share vertices but may not share edges. Write for the minimum possible number of pieces.
The asymptotic notation
means that there are constants and , chosen independently of and , such that every chordal -vertex graph with has a clique partition with at most pieces.
The root theorem is
The quantifier order is essential: and are universal and cannot depend on the graph.
The supporting target records the weaker uniform statement
This is the precise form. It is not equivalent to the root: choosing is invalid because the cutoff may depend on the fixed value of .
The root would determine the clique-partition extremum for chordal graphs up to a linear remainder, matching the scale of the complete-split examples that motivate the coefficient . It would refine a leading-order asymptotic theorem into a uniform estimate strong enough to distinguish second-order behavior.
Formalization creates a clean interface among perfect elimination orderings, exact edge partitions, fractional edge-and-triangle decompositions, and integer triangle packings. It also forces the proof to distinguish a partition from a cover and original graph order from the order of any auxiliary hypergraph. These definitions can support other decomposition problems on chordal and split graphs.
Perfect elimination does not by itself give the sharp partition count. Greedily taking maximal cliques may overlap in edges or accumulate too many singleton pieces. Similarly, a fractional edge-and-triangle partition can achieve the right leading coefficient while integer rounding loses pieces; the root requires that loss to be only .
The dense-packing theorem has quantifiers of the form “for every fixed there exists .” It therefore yields a uniform subquadratic error but no linear error. Any proof of the root must add a chordal-specific rounding or extremal reduction rather than treating the general packing theorem as if its could vary with .
Graphs are finite and simple. Chordality is encoded by existence of a perfect-elimination ranking, including disconnected and edgeless graphs. A clique piece is a finite vertex set that spans a complete subgraph. Exactness means every actual edge occurs in exactly one piece; no nonedge can occur inside a piece. Bounds are compared in so the displayed asymptotic expressions retain their conventional form, while the number of parts remains a natural number.
The candidate derivation of the leading coefficient imports finite linear-programming duality and the Haxell–Rödl/Yuster fixed-triangle packing approximation. It is candidate_only, not an admitted result or kernel proof. Contributions may formalize the perfect-elimination lemmas, the fractional compression, the uniform packing interface, complete-split lower examples, or the root linear rounding theorem. A result for edge-and-triangle pieces only, a fractional partition, or one fixed order must not be presented as the unrestricted integer clique-partition theorem.