Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Introductory physics is normally taught as a sequence of unrelated chapters — kinematics, dynamics, energy, optics, gravitation — each with its own rules. A recurring proposal in physics education is to teach instead from a single organising statement: among all conceivable histories of a system, the one realised in nature is the one that makes a certain integral, the action, stationary. Edwin Taylor's editorial A Call to Action (American Journal of Physics, 2003) argued for building the first-year curriculum on it; Lachlan McGinness and Craig Savage reported classroom results for such a course at the Australian National University (Action physics, American Journal of Physics, 2016); Massimiliano Malgieri tested a sum-over-paths treatment in an Italian secondary school (2017).
The source monograph for this mission, Julliana Rodrigues Martins, A Ação Estacionária como Eixo Unificador do Ensino de Física no Ensino Médio (Trabalho de Conclusão de Curso, Universidade Federal do Ceará, 2025), develops this programme for secondary education. Its Chapters 2 and 3 are quantitative: they follow the historical line from antiquity to the nineteenth century and carry out every calculation in full. This mission formalises that quantitative core, and nothing of the pedagogical Chapter 4.
The historical line the monograph reconstructs, and which the milestone list follows:
Fix real endpoints and an integrand , a real-valued function of three real arguments. A path is a function , and its action over is
Neighbouring paths are produced by an admissible variation: a twice continuously differentiable with , giving the family . The path is stationary when
Writing and for the partial derivatives of in its first and second slots, the Euler–Lagrange expression along is
In mechanics one takes , and , so that stationarity of is Hamilton's principle and is the Lagrange equation of motion.
For , twice continuously differentiable in all three arguments and twice continuously differentiable, if is stationary for then
This is equation (3.9) of the monograph, and — through the substitution , , — equation (3.17). It is stated as the weakest stable form: stationarity, not minimality, and an arbitrary admissible integrand rather than a particular Lagrangian.
The supporting statements are the analytic ingredients of that derivation (the fundamental lemma, the first variation formula, the first integral for a cyclic coordinate), its two mechanical applications worked out in the monograph (harmonic oscillator, plane pendulum), its geometric application (shortest path), and the historical minimisation problems of Chapter 2 (Heron, Galileo, Fermat, Maupertuis).
The Euler–Lagrange equation is the bridge the whole unification argument rests on: once it is available, Newton's second law, the pendulum equation, Snell's law, geodesics and conservation laws all become consequences of one statement about an integral, which is exactly the claim the monograph makes to justify teaching physics this way. The Chapter 2 statements are the historically prior special cases, each obtained by a one-variable minimisation rather than by the general machinery, and together they exhibit how far elementary optimisation alone reaches before the calculus of variations is needed.
What this mission adds beyond the source is a machine-checked version of an argument that, in every textbook presentation including this one, is carried out at the level of rigour of formal manipulation: the interchange of differentiation and integration is performed without justification, the passage from a vanishing integral to a vanishing integrand is asserted, and the regularity needed for to exist is left implicit. All of it is true under the stated hypotheses; none of it is proved in the source. Mathlib has the analytic infrastructure (interval integrals, differentiation under the integral sign, smooth bump functions) but, at the environment pinned for this mission, no Euler–Lagrange equation and no calculus-of-variations layer built on it. The definitions published here — action, admissible variation, stationary path, Euler–Lagrange expression — are reusable by any later variational mission.
The obvious argument is three lines: differentiate under the integral sign, integrate by parts, and conclude that the integrand vanishes because is arbitrary. Each line is where the work is.
Differentiating under the integral sign needs a dominating bound valid uniformly for near ; it is available here because the data are and the interval is compact, but it has to be produced. The integration by parts needs to be differentiable, which is where the second derivative of and the second derivatives of are consumed — a path is not enough for this formulation. The final step needs test functions: a bump supported in a small interval around a point where the continuous coefficient is nonzero, which is why the fundamental lemma is a separate milestone rather than a step.
A standing trap in the Lean formulation is that deriv returns at points where a function is not differentiable, so a statement about can be accidentally true for the wrong reason unless the regularity hypotheses are genuinely strong enough. Every statement here carries the hypotheses that make each derivative a real derivative.
The development is one-dimensional and real: paths are , the integrand is a curried with argument order matching the source's , and all integrals are interval integrals over . Partial derivatives are one-dimensional derivatives in the frozen remaining arguments; smoothness of is stated for its uncurried form on . Regularity is throughout — for the integrand, for the path, and for the variations — matching the monograph's requirement that have continuous first and second derivatives.
Stationarity is a hypothesis quantified over all admissible variations, so the goal cannot be satisfied by exhibiting one convenient ; and the conclusion is an equation at every point of the closed interval, not almost everywhere, so it cannot be weakened to a null-set statement. The mechanical milestones are stated as equivalences between the Euler–Lagrange equation for the explicit Lagrangian and the classical equation of motion, which rules out a one-directional reading that would be vacuous for a path that never satisfies either.
Physical constants (, , , , the speeds ) are free real parameters, with positivity or non-vanishing assumed only where the source's conclusion requires it — the pendulum equivalence divides by , so and appear, while the oscillator equivalence needs no such assumption. Angles never appear as primitive objects in the optics milestones: the sines of the incidence and refraction angles are written as the ratios that the figures define them by, so no convention about angle ranges is smuggled in.
Contributions welcome: proofs of any milestone, and reusable infrastructure for differentiation under the interval integral sign and for bump functions with prescribed support, both of which are of use well beyond this mission.
Hubble's law — officially the Hubble–Lemaître law — is the observation that galaxies recede from us at a speed proportional to their distance, . It is the first observational basis for the expansion of the universe and one of the standard pieces of evidence cited for the Big Bang model. Georges Lemaître derived the proportionality from relativistic cosmology in 1927; Edwin Hubble published the observational relation in 1929, building on Vesto Slipher's redshifts and Henrietta Swan Leavitt's Cepheid distance scale. Alexander Friedmann had already shown in 1922 that the Einstein field equations admit expanding solutions, with an expansion rate governed by what is now called the scale factor.
Behind the astronomy sits a piece of elementary mathematics that is rarely written out in full: in a spatially homogeneous expansion, the linear velocity–distance relation is forced, it holds with the same constant for every observer, and the Hubble "constant" is in fact a function of time whose evolution is fixed by a single dimensionless parameter. This mission formalizes that kinematic core: the statements are about the scale factor and its derivatives, and involve no Einstein equations.
A scale factor is a function of cosmic time . A comoving point is labelled by a fixed coordinate (with the Euclidean norm), and its proper position at time is
The proper distance between the comoving points and is
The Hubble parameter and the dimensionless deceleration parameter are
denotes the present-day value of ; the name "Hubble constant" refers to the fact that is constant in space at a fixed time, not in time.
The goal theorem is the idealized Hubble law, stated in the source as a theorem of Euclidean geometry: any two points moving away from the origin, each along a straight line and with speed proportional to its distance from the origin, move away from each other with a speed proportional to their distance apart. Formally, for , a time and curves with
the separation satisfies
The relative velocity is parallel to the separation vector and its magnitude is times the separation, with the same for every pair — so no comoving observer occupies a distinguished centre of the expansion.
The milestones supply the cosmological content that surrounds this geometric fact:
The result itself is elementary but load-bearing: it is what licenses reading a linear redshift–distance diagram as evidence for uniform expansion rather than for a privileged position in space, and items 4–6 are the statements through which cosmological observations (the sign of , the approach of to in CDM) are turned into claims about the past and future behaviour of and .
Formalizing it produces a small, reusable Lean layer for expansion kinematics: the scale factor, the Hubble and deceleration parameters, proper position and proper distance, with the differentiation lemmas that connect them. The platform already carries Friedmann-equation missions that fix the dynamics of ; this mission is the kinematic complement, and its Hubble parameter is the same function that those developments use. Nothing here is an open research problem: every statement is a known textbook fact, and the work is the formalization.
The mathematical content is a few lines of calculus, so the difficulty is entirely in the encoding. Three places are easy to get wrong. First, proper distance is defined through a norm, so the identity needs positivity of , and differentiating it needs positivity on a neighbourhood, not just at the point. Second, is defined by a quotient with in the denominator: in Lean division by zero returns zero, so a statement about that forgets silently changes meaning. Third, milestone 5 propagates a hypothesis stated on down to the endpoint , where the Big Bang condition lives; the continuity argument at the endpoint is the only step with any technical content.
Time is and space is EuclideanSpace ℝ (Fin 3); derivatives are Mathlib's
deriv / HasDerivAt, so "velocity" is always a derivative at a point rather than a
difference quotient. Smoothness is assumed exactly where it is used: differentiability at a
single time for the first-order statements, ContDiff ℝ 2 for the statements involving
. Positivity of the scale factor is stated explicitly wherever it is needed, as is
in the statements mentioning .
Degenerate readings are excluded: the goal's hypotheses are satisfiable (any pair of comoving points in an expanding universe satisfies them, as milestone 2 shows), and the milestones are non-vacuous for concrete scale factors such as and . The goal theorem's second clause is a norm identity that is true for every ; it carries the "speed proportional to distance" half of the source's statement, while the first clause carries the "moving away from each other along the separation" half.
The definition layer is a single self-contained file (scale factor derived quantities, proper position, proper distance); it is reusable by any mission about expansion kinematics. Contributions of the milestone proofs, and of variants such as the redshift relation derived from null geodesics rather than assumed, are welcome.
Perturbative quantum field theory computes correlation functions of a field by expanding around a Gaussian (free) theory. Every term of that expansion is a Feynman diagram, and the rule that turns a diagram into a number is Wick's theorem: the expectation of a product of Gaussian field modes is the sum, over all ways of pairing the modes up, of the product of the two-point functions of the pairs. The same identity is known in probability and statistics as the Isserlis theorem (L. Isserlis, 1918) and is the standard tool for computing moments of Gaussian vectors; in random-matrix theory the counting of pairings it produces is the origin of the Catalan-number asymptotics of Wigner's semicircle law.
The uploaded source is the Wikipedia article Feynman diagram, which states Wick's theorem for the free scalar field and then, in the section Higher Gaussian moments — completing Wick's theorem, verifies the one-variable case by direct Gaussian integration. This mission formalizes that content: the combinatorics of pairings, the one-dimensional Gaussian moment formulas, and the multivariate identity itself.
Fix and work on with coordinates . Let be a centered Gaussian measure on : a Gaussian probability measure all of whose coordinate means vanish, for every . Its covariance (in the physics reading, the propagator) is
A pairing of the labels is a partition of these labels into unordered pairs; equivalently, a permutation of the labels with and for all (a fixed-point-free involution). The set of pairings is written . For a weight indexed by labels, the Wick sum is
the inner product ranging over the pairs of , each counted once through its smaller element.
In the article's field-theory notation the labels are momenta , the coordinates are the field modes , and the two-point function carries the momentum-conserving delta function, . This mission works with the finite-dimensional Gaussian vector rather than the field, so the delta functions are absorbed into the covariance matrix .
For a centered Gaussian measure on and any labels ,
No hypothesis is imposed on the covariance: it may be singular and the labels may repeat, which is exactly the situation the article's "completing Wick's theorem" section addresses.
Targets 1–3 are the article's displayed Gaussian integrals, target 4 is its pairing count, targets 5–6 are the two explicit consequences it records for the field correlators.
Wick's theorem is the computational content of every Feynman-diagram expansion: once it is available, a perturbative term is a finite sum over diagrams, and the symmetry factors of diagrams are bookkeeping on the pairing set . On the probabilistic side it gives all moments of a Gaussian vector in closed form, which is the entry point to Gaussian chaos expansions, Wiener–Itô integrals, and moment methods for random matrices.
Mathlib (revision 0df444a) has real Gaussian measures gaussianReal, the general class
IsGaussian of Gaussian measures on a topological vector space, the Gaussian integral
, and the double factorial Nat.doubleFactorial, but no
higher-moment formula for Gaussian measures and no Isserlis/Wick statement. The mission therefore
produces new library-level content, not a re-derivation of existing formal results; the result
itself has been classical since 1918 (Isserlis) and 1950 (Wick).
The obvious route — expand the characteristic function and differentiate times at — requires differentiating under an integral sign times and identifying the resulting combinatorial sum with a sum over pairings; both steps are where the formal work lies. Integrability is not automatic from the statement and has to be established (Gaussian measures have moments of all orders, but the product must be shown integrable before any manipulation). The naive attempt to reduce to the independent case by diagonalizing meets a second difficulty: the change of variables must be tracked through the pairing sum, and may be singular, so no invertible whitening transform exists in general. The one-variable case (milestone 3) is not a special case to be waved through either: it is the statement the article singles out, because a naive "each mode pairs with a distinct partner" argument fails when all labels coincide.
The ambient space is EuclideanSpace ℝ (Fin d); measures are Mathlib Measures and Gaussianity
is the Mathlib class IsGaussian, which is defined by every continuous linear functional pushing
forward to a real Gaussian law. Centering is stated as an explicit hypothesis on the coordinate
means, so the measure is not assumed standard and the covariance is unconstrained (in particular
degenerate covariances, and repeated labels , are included). Integrals are Bochner
integrals, which return for non-integrable functions; the statements are nonetheless
non-vacuous because Gaussian measures integrate all polynomials.
Pairings are formalized as fixed-point-free involutions of Fin (2 * n) and the pair product
ranges over , so each pair contributes once. The case is included:
the empty product is , the unique pairing of the empty label set is the identity, and both
sides of the goal equal . The double factorial is Mathlib's Nat.doubleFactorial, evaluated at
2 * n - 1 in truncated natural subtraction, so the value is .
Contributions welcome: the Gaussian moment lemmas (milestones 1–3) as standalone Mathlib-style results, the pairing count (milestone 4) as pure combinatorics independent of the analysis, and any reduction of the goal to the independent-coordinate case.
Linear systems are the inner loop of scientific computing: discretized differential equations, least-squares fitting, network flow balances and equilibrium models all end in . Direct elimination solves the system exactly in operations, but for the large sparse systems produced by discretization the cost and the round-off growth make iterative methods preferable: start from an arbitrary vector and apply a cheap update until the residual is small. The question such a method raises is when the iteration converges, and to that the chapter gives a clean sufficient answer: diagonal dominance.
This mission is the third in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (UFMS, 2000). It covers the iterative part of Chapter 5, Solução de Sistemas Lineares.
Let be a real matrix and . Assume for all .
The Jacobi method computes every coordinate of the new iterate from the old one:
The Gauss-Seidel method updates the coordinates in order and uses the values already updated in the same sweep:
Both are instances of an affine iteration associated with an equivalent rewriting .
The matrix is diagonally dominant when each diagonal entry dominates its row:
The goal theorem is Proposição 5.10.1: if is diagonally dominant and x^\\star solves Ax^\\star = b, then the Gauss-Seidel iterates converge to x^\\star from any starting vector.
The milestones are the general facts the source uses to get there: that the limit of a convergent affine iteration is a fixed point of it and hence a solution of the system (Proposição 5.5.1), that a contraction condition with forces convergence to the solution (Proposição 5.5.3), and that the Jacobi sweep has exactly the solutions of as its fixed points (Proposição 5.5.2).
Diagonal dominance is the hypothesis a practitioner can check by inspection, and it is satisfied by the matrices that come from standard finite-difference stencils, from strictly diagonally dominant collocation systems and from many equilibrium models. The theorem says that for those systems Gauss-Seidel needs no spectral analysis and no preconditioner to be safe: convergence holds from any starting vector. The supporting milestones isolate the two halves of the argument — a fixed-point identification and a contraction estimate — in a form reusable for other splittings (Jacobi, SOR, block variants).
Mathlib has Banach's fixed point theorem and the theory of matrix norms, but not the Gauss-Seidel sweep, the notion of diagonal dominance as used here, or the convergence statement, which is what this mission adds.
Gauss-Seidel is not a plain affine map applied coordinatewise: within one sweep the coordinates are updated sequentially, so the new value of coordinate depends on the new values of coordinates . Formalizing the sweep therefore requires a recursion over the coordinate index before the recursion over the iteration counter, and the contraction estimate has to be propagated along that inner recursion. The classical proof compares \\max_i |x_i^{(k+1)} - x_i^\\star| with \\max_i |x_i^{(k)} - x_i^\\star| and needs, for each , a bound that already uses the improved bounds for ; getting that induction right is the substance of the mission.
Vectors are functions from a finite index type with elements to , and convergence is convergence in that finite product space (equivalently, coordinatewise). The Gauss-Seidel sweep is defined through an auxiliary partial sweep: after inner steps the first coordinates carry their new values and the remaining ones their old values, and the full sweep is the partial sweep after steps. The Jacobi sweep is defined directly. Diagonal dominance is the strict inequality above, with the sum taken over the row with the diagonal index removed; for every statement is vacuous, and the goal theorem is then trivially true because the space has a single point. Division by the diagonal entry is total division, so the definitions make sense even when ; diagonal dominance rules that out, because the right-hand side of the dominance inequality is nonnegative. The goal theorem assumes a solution x^\\star is given rather than asserting its existence, and it asserts convergence for every starting vector, generalizing the source's choice . The contraction milestone states the consistency of the norms as the hypothesis in the supremum norm rather than fixing a particular matrix norm.
Most equations that arise in applications cannot be solved in closed form: the age of the Moon from a radioactive-decay balance, the deflection of a clamped beam, the equilibrium of a catenary, all reduce to solving for a function with no algebraic inverse. A first course in numerical methods therefore opens with root finding: constructive procedures that produce a sequence of approximations together with a theorem saying that the sequence converges to a root and how fast.
This mission is the first in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (Departamento de Computação e Estatística, UFMS, 2000). It covers Chapter 3, Zeros de Funções, whose capstone is the local convergence of Newton's method.
Let and let be a zero of , i.e. . The chapter studies three constructions.
Bisection. Starting from an interval with , put and keep the half of on whose endpoints still changes sign. The width of the bracketing interval is halved at every step.
Linear iteration (MIL). Rewrite as a fixed-point equation and iterate from an arbitrary .
Newton's method. Take the particular iteration function
obtained by truncating the Taylor expansion of at after the linear term.
A sequence has order of convergence when tends to a finite constant, where ; is linear and quadratic convergence.
The goal theorem is the local convergence of Newton's method at a simple zero. If is twice differentiable on an open interval containing , its second derivative is continuous there, and never vanishes on , then there is such that
where is the Newton sequence started at . This is the formal content of the chapter's statement that Newton's method converges provided the initial guess is chosen close enough to the root.
The milestones are the supporting results of the chapter: the error bound and convergence of bisection, the convergence of the linear iterative method under a derivative bound , the a posteriori estimate , and the quadratic order of Newton's method at a simple zero.
Bisection, fixed-point iteration and Newton's method are the three root finders every numerical-analysis course starts with, and the three convergence theorems above are what justifies using them. The a posteriori estimate is what turns the iteration into an algorithm with a stopping criterion: it bounds the distance to the root by a quantity the program can measure. The quadratic order statement explains the observed doubling of correct digits per step at a simple zero and its loss at a multiple zero.
On the formalization side, Mathlib already has a fixed-point theorem for contractions on complete spaces and the mean value theorem, but not the statements in the form used in numerical analysis: bisection with its explicit bracket, the a posteriori bound, or Newton's local convergence and quadratic rate stated for the concrete iteration sequence. This mission asks for those.
The delicate point in all three theorems is that the iterates must be known to stay in the region where the hypotheses hold; the informal proofs assume this silently. For the linear iterative method the mission therefore states the invariance hypothesis explicitly ( maps the closed interval into itself). For Newton's method, no such hypothesis is given: the existence of a neighbourhood of that the iteration preserves is part of what must be proved, and it comes from the continuity of together with . The quadratic-order milestone also has to handle the degenerate possibility , which would put a zero in the denominator; it is excluded by hypothesis.
Everything is over the real numbers. The iterations are given as explicit recursive sequences: the bisection construction returns the bracketing pair and its midpoint, and there are separate sequences for the fixed-point and Newton iterations. Newton's method takes the derivative as a separate function argument , tied to by a hypothesis of the form " has derivative at every of the interval"; this avoids relying on any junk value of a derivative operator where fails to be differentiable. Division is total, so a step at a point where vanishes would leave the iterate unchanged; the hypotheses exclude this inside the interval.
Two deliberate deviations from the source are worth flagging for the auditor. First, Proposição 3.5.1 assumes only for , but its proof divides by ; the formal statement assumes on the whole interval, so is a simple zero. Second, the convergence statement for the linear iterative method adds the hypothesis that maps the closed interval into itself, without which the iterates may leave the region where the derivative bound is assumed.
A table of values is all one has of many functions: measurements, tabulated physical constants, the output of an expensive simulation. Interpolation reconstructs a function between tabulated points by passing a polynomial through them, and it underlies much of the rest of numerical analysis — quadrature rules, finite-difference formulas and predictor-corrector schemes for differential equations are all obtained by integrating or differentiating an interpolating polynomial. What makes the reconstruction trustworthy is a formula for the error committed away from the nodes.
This mission is the fifth in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (UFMS, 2000). It covers Chapter 7, Interpolação.
Let be distinct nodes and the tabulated values of a function . The Lagrange form of the interpolating polynomial is
so that for every , and is the unique polynomial of degree at most with this property.
The interpolation error at a point that is not a node is the difference .
The goal theorem is Proposição 7.3.1: if is times differentiable on and all nodes lie in , then for every different from all nodes there exists with
The milestones are the other results of the chapter needed to make sense of it: the existence and uniqueness of the interpolating polynomial of degree at most through points with distinct abscissas (Proposição 7.2.1), the fact that the Lagrange formula does interpolate the data, and the practical error bound of Proposição 7.3.2, when .
The error formula is the reason interpolation is a numerical method and not just a curve-drawing device: it shows that the error is governed by two independent factors, the smoothness of through and the geometry of the nodes through the product . Everything downstream follows from it — the and error terms of the trapezoidal and Simpson rules in the next mission are obtained by integrating exactly this expression, and the choice of Chebyshev nodes is the attempt to make the product factor small.
The standard proof introduces the auxiliary function with chosen so that , and then applies Rolle's theorem times to conclude that vanishes somewhere. Formalizing the repeated application of Rolle's theorem, keeping track of the distinct zeros and the nested intervals they generate, is the substance of the work; it is an induction that has to be organized carefully rather than a computation.
The nodes are given as a strictly increasing family of reals lying in the open interval , and the interpolating polynomial is the explicit Lagrange sum rather than an abstract polynomial: at a node it is defined by the same formula, whose factors then include contributions unless the nodes are distinct, which is why the distinctness hypothesis appears in the interpolation milestone. Smoothness is expressed as continuous differentiability of order on the open interval , and the derivative appearing in the error term is the iterated derivative computed within that set; since the set is open this agrees with the ordinary -st derivative. The evaluation point is assumed to lie in and to differ from every node; the point is asserted to exist in , with no claim of uniqueness or of any relation to beyond membership in the interval. The uniqueness milestone is stated with Mathlib's polynomial type and the degree bound , which includes the zero polynomial.
Reinforcement learning formalizes a scenario supervised learning cannot: an agent that actively interacts with an environment, choosing actions that change both the state it observes next and the reward it receives, rather than passively receiving an i.i.d. labeled sample. Every practical treatment of this scenario — from classical dynamic programming to modern deep reinforcement learning — is built on the Markov decision process (MDP), a model in which the effect of an action depends only on the current state, not on the full history that led to it. Two questions define the theory this mission covers: given a fixed way of acting (a policy), what value does it obtain, and how is that value actually computed rather than merely characterized as the solution of a fixed-point equation? Mohri, Rostamizadeh and Talwalkar's chapter 17 answers both for the stationary, infinite-horizon discounted case, and this mission targets its two central results: that a fixed policy's value is not just characterized but uniquely determined by a linear system with an explicit closed-form solution (Theorem 17.10), and that the optimal value function — obtained instead by choosing the best action at every state — can be computed by an iterative algorithm guaranteed to converge regardless of where it starts (Theorem 17.11).
A (finite) Markov decision process consists of a finite set of states , a finite set of actions , a transition kernel giving the distribution over the next state after taking action at state , and an expected reward for that transition. A (stationary) policy assigns each state a distribution over actions — possibly, but not necessarily, a point mass on a single action. Fixing turns the MDP into an ordinary Markov chain on : at each step the agent is at some state , draws , receives (expected) reward , and moves to a state drawn from . For a discount factor , the value of at is the expected discounted sum of future rewards starting from ,
and the state-action value function is the analogous quantity for taking at and then following . Marginalizing the raw kernel and reward over the mixed action gives the induced transition matrix and induced reward vector — the objects that turn 's value into a genuinely linear-algebraic quantity. A policy is optimal if for every policy and every state ; write for its value function.
Theorem 17.10 (goal). For a finite MDP and a fixed policy , the matrix (with the policy-induced transition matrix) is invertible, and 's value function is the unique solution of the Bellman equations, given in closed form by
Proposition 17.9 (milestone). The value function itself satisfies the linear system that Theorem 17.10 solves:
Theorem 17.7 (milestone). A policy is optimal if and only if it places probability only on -maximizing actions: for every with , .
Theorem 17.11 (milestone). The Bellman optimality operator , , is a -contraction for ; consequently, for any starting vector , the value-iteration sequence converges to a fixed point of .
Theorem 17.10 is what makes policy evaluation on a finite MDP an exact, finite computation rather than an infinite limit: instead of summing an infinite discounted series or solving an implicit fixed-point equation numerically, a single matrix inversion gives the policy's value at every state simultaneously. It is also the base case every planning algorithm in the chapter builds on: policy iteration alternates optimizing a policy with exactly this evaluation step. Theorem 17.11 gives the complementary guarantee for the harder problem of finding the optimal value function directly, without fixing a policy first: value iteration converges from any starting point, with a convergence rate ( iterations for -accuracy) that follows from the same contraction argument. Together, the two results are the mathematical content behind why dynamic-programming planning for finite MDPs is tractable at all — the discount factor , not any structural assumption on rewards or transitions, is what buys both the uniqueness in Theorem 17.10 and the convergence in Theorem 17.11. Formalizing them requires reproducing this linear-algebraic and metric content precisely, not just asserting the conclusions: an invertibility claim asserted without the operator-norm argument, or a convergence claim without the contraction property, would state something true by fiat rather than the book's actual result. No faithful prior art exists on the platform for this exact model (see Formalization scope).
The obvious shortcut for Theorem 17.10 is to assert is invertible without proof — true, but not what the book does, and not informative about why it holds. The genuine content is that , being row-stochastic (every row of sums to exactly , since and are both proper distributions), has operator norm exactly, so strictly; this rules out as an eigenvalue of , which is exactly what invertibility of requires. The same fact, applied differently, drives Theorem 17.11: showing is -Lipschitz requires bounding by comparing the maximizing action for against the same action's value under (not 's own maximizer), since the two suprema need not be attained at the same action — a step easy to state incorrectly as a direct comparison of two maxima. Both theorems fail if is allowed: the discounted setting's central asset, a strict contraction, disappears exactly at that boundary.
States and actions are modeled as finite types (Fintype S, Fintype A); the raw kernel and
reward P : S → A → S → ℝ, Er : S → A → ℝ are unconstrained functions, with IsTransitionKernel
asserting the required distribution property explicitly rather than assuming it silently. A
policy is π : S → A → ℝ with IsPolicy π asserting π s is a distribution over A for every
s — deliberately not π : S → A or a PMF-valued function, since Theorem 17.7's own
quantifier ("for any pair (s,a) with π(s)(a) > 0") requires treating π(s) as a genuine
mixture. PolicyValue is defined as the actual infinite discounted expectation (via an explicit
state-occupation-distribution recursion), not as the Bellman fixed point — so that Proposition
17.9 (the value function satisfies the linear system) and Theorem 17.10 (that system has a
unique, invertible-matrix solution) are both non-vacuous claims about the same object, rather
than one being definitionally true of the other. The trivializing formalization this rules out
is asserting IsUnit (1 - γ • P) as a bare hypothesis, or defining V_π as (1-γP)⁻¹R and
calling the resulting identity a theorem; both would erase the mission's actual content.
Two platform modules model related MDPs (BertsekasSSPModel, a stochastic-shortest-path model
with a termination-probability deficit rather than exact row-stochasticity, and
FoundationsRL.RLBasics, a finite-horizon episodic model indexed by layer) — neither
specializes exactly to this chapter's stationary, always-continuing, infinite-horizon discounted
convention, so every definition here is drafted fresh rather than imported. This chunk covers
§17.2–17.4.2 (the MDP model, policy value, Bellman's equations, value and policy iteration);
§17.4.3 (the linear-programming formulation) and §17.5 (stochastic-approximation learning
algorithms — TD(0), Q-learning, SARSA) are out of scope, since they require a
stochastic-approximation convergence substrate this mission does not build.
Maximum entropy (Maxent) models are a widely used family of density-estimation algorithms: given a sample and a set of features, they select the distribution that matches the empirical feature averages while being otherwise as "agnostic" (close to a prior, usually uniform) as possible — a principle that, notably, never requires specifying a parametric family of distributions to search over. This mission formalizes the theorem that explains why this works in practice: Maxent's primal optimization (over distributions, subject to feature-matching constraints) is exactly dual to an unconstrained maximum-likelihood problem over a specific, rich parametric family — the Gibbs distributions — even though the Maxent principle never mentions that family at all.
For a sample drawn i.i.d. from over a finite set , and a feature map with , the Maxent principle seeks (the simplex of distributions over ) minimizing the relative entropy to a prior , subject to (problem 12.7). Introducing the indicator function ( on , elsewhere) turns this into the unconstrained primal objective (Eq. 12.8), with the feature-constraint set. A Gibbs distribution with parameter is , the partition function (Eq. 12.9); its associated dual objective is (Eq. 12.10) — note is exactly the empirical log-loss , so maximizing is minimizing an L1-regularized log-loss over the Gibbs family.
Theorem 12.2 — the mission's goal (Maxent duality). . Furthermore, letting and : for any and any with , .
Theorem 12.3 (Maxent L1-regularization generalization bound, milestone). Fix . Let solve the L1-regularized dual (12.12) with . Then, with probability at least ,
Theorem 12.2 is one of the most striking dualities in the book: the Maxent principle, phrased
purely in terms of closeness to a prior distribution, turns out to always produce a solution in
the Gibbs family — not because that family was ever specified, but because relative entropy is
the specific measure of closeness whose Fenchel conjugate is the log-partition function. This
explains a whole zoo of models (log-linear models, exponential families, Gaussian and bimodal
Gibbs distributions from quadratic features) as instances of a single duality theorem, and gives
a computationally friendlier route to the (constrained, infinite-if--is-large) primal problem
via the (unconstrained, -dimensional) dual. The theorem's proof is a genuine application of
conditional (Fenchel) strong duality, not an unconditional fact — this is, per the chapter's own
brief, the sharpest trivialization risk in the entire mission series, since "strong duality
always holds for convex problems" is false in general, and a formalization skipping the book's
own qualification condition (, placing in the interior of the constraint set)
would prove a different, potentially-false statement. No prior art on the platform is faithful:
GET /theorems?q=maximum+entropy returns no hits, and Mathlib's generic Fenchel-conjugate
machinery (Analysis/Convex/Conjugate) does not package the book's own specific qualification
conditions as a single reusable theorem matching Theorem B.39 — reusing it inside a proof
(not the audited statement) remains available to whoever proves this theorem later.
Not formalized here: Theorem 12.4 (a Bregman-divergence generalization of Theorem 12.2) and
Theorem 12.5 (its L2-regularized concrete special case). BRIEF.md itself flags Theorem 12.4
as possibly too heavy and offers Theorem 12.5 as an easier alternative; this mission omits both,
since even Theorem 12.5 requires a second, structurally parallel dual-objective-and-minimizer
formalization (for L2 rather than L1 regularization) — disproportionate to this mission's budget
once Theorem 12.2's own qualification-condition bookkeeping (the heaviest single item in this
mission series) is accounted for. §12.1 (density estimation without features: ML/MAP), §12.7
(coordinate descent), and §12.8-12.9 (Bregman-divergence extensions, L2-regularization in
general) are likewise out of scope, per BRIEF.md's own page-range restriction.
Theorem 12.2's proof is the book's own explicit application of the Fenchel duality theorem
(Theorem B.39, Appendix B) to the specific triple , ,
— every qualification condition (A a bounded linear map, u_0\in A(\mathrm{dom}f)\cap\mathrm{cont}(g), needing \lambda>0 to place u_0 in int(C)) must be
checked for this triple, not assumed generically; the conjugate computations themselves
(f^*(q)=\log\sum_xp_0(x)e^{q(x)}$ via Lemma B.37, g^(w)=E_{\hat D}[w\cdot\Phi]+\lambda|w|_1 via the dual-norm identity) are specific algebraic derivations, not immediate from abstract duality alone. The second clause's proof needs a further, non-obvious algebraic identity (G(w)-D(p^|p_0)+D(p^|p_w)expanding, via Hölder's inequality applied to the primal feasibility ofp^, to something \le0) that is not a restatement of the first clause but a separate argument built on top of it. Theorem 12.3's proof structurally mirrors chunk 04's SRM bound (bounding L_D(\hat w)-L_S(\hat w)via Hölder's inequality and the Rademacher-complexity feature-concentration bound of Eq. 12.5, then using\hat w`'s optimality twice), but is applied
to the log-loss of a Gibbs distribution rather than a generic bounded loss.
MaxEntPrimalObjective uses EReal (the extended reals) so that the book's own +\infty
values (from I_K, \tilde D) are represented exactly, matching the chapter's own explicit use
of an extended-real-valued indicator function rather than a soft penalty — a trivializing
formalization this mission avoids is silently replacing +\infty with a large real sentinel,
which would misstate a convex-analysis object whose entire role in the proof is its infinite
value outside the feasible/simplex set. hlam : 0 < lam is a genuine load-bearing hypothesis in
the goal theorem, matching the book's own use of \lambda>0 to invoke Theorem B.39's
qualification condition — not a free convexity assumption; this is the mission's central
faithfulness guard against the chapter's own named trivialization risk. EmpiricalRademacherComplexity/
RademacherComplexity are restated locally, byte-identical to chunks 05-svm/07-boosting's
own copies (a draft item cannot import another chunk's draft module). p^* in the goal theorem
and \hat w in Theorem 12.3 are both quantified via explicit hypotheses (IsLeast, a
minimizer inequality) rather than assumed to exist unconditionally, matching the book's own "let
p^*=..."/"let \hat w be a solution of..." phrasing without asserting existence or uniqueness
beyond what the book itself asserts. No numerical constant in either theorem is altered from
the book's own displayed form.
In the Standard Model the scalar sector consists of a single complex doublet. The general Two-Higgs-Doublet Model (THDM) replaces it by two complex doublets of the same weak hypercharge . This is the minimal extension of the scalar sector that is still renormalisable and gauge invariant, and it is forced on any supersymmetric completion: the Minimal Supersymmetric Standard Model has exactly two Higgs doublets. Before any phenomenology can be done with such a model, two questions have to be answered for the given parameter point: is the scalar potential stable, i.e. bounded from below, and does its global minimum break down to the electromagnetic ?
The general THDM potential has real parameters, and answering these questions directly in field space — eight real scalar degrees of freedom, of which three are gauge — is unwieldy. Maniatis, von Manteuffel, Nachtmann and Nagel (2006) proposed a reformulation in terms of gauge-invariant bilinears, in which the gauge orbits of the Higgs fields are parametrised by a Minkowski-type four-vector confined to the closed forward light cone, and the potential becomes a quadratic polynomial on that cone. In these variables the stability question reduces to a one-variable problem: the sign of an explicit rational function on a finite set of at most ten real numbers. This mission formalizes that analysis: the gauge-orbit parametrisation (their Theorem 4), the classification of the stationary points of the potential (their Theorem 2), and the stability criterion itself (their Theorem 1).
Write the two doublets as rows of a complex matrix,
and form the hermitian matrix of gauge-invariant scalar products , i.e. . Decomposing in the Pauli basis gives four real functions
Positive semi-definiteness of is equivalent to and : the four-vector lies on or inside the forward light cone. A gauge transformation acts as with , and leaves invariant.
The most general gauge-invariant renormalisable potential is
with real parameters , and a real symmetric matrix . For one sets , so that , and
Stationary points of on the ball are governed by the functions
where is a Lagrange multiplier for the constraint . The finite set collects: every regular with ; the point when ; and every eigenvalue of at which stays finite and . It has at most ten elements, and is exactly the set of stationary values of .
For the stationary points of the full potential one uses four-vector notation , , and the metric , so that on the domain , , with .
For the potential is stable for , marginal for and unstable for . For ,
and if on with equality somewhere, the sign of — replaced by when is an eigenvalue of — decides between stability in the weak sense and instability.
Theorem 4 (gauge orbits); the four stability cases (a), (b.2), (b.3), (b.4) of Section 4 including the criterion for the marginal case; equation (4.39) identifying the stationary values of with ; equations (4.42)–(4.44) giving at those stationary points; and Theorem 2, the classification of the stationary points of .
The criterion is a decision procedure: given the parameters of a THDM, stability is settled by evaluating one rational function at the roots of another, without any search in field space. The authors use it to re-derive the known stability conditions for the MSSM potential and to settle the stability and symmetry-breaking properties of the THDM potential of Gunion et al., for which , and come out as the strong-stability conditions. Theorem 4 is what makes the whole approach legitimate: it says that nothing is lost in passing from fields to the invariants , because the fibres of that map are exactly the gauge orbits.
The results are established in the published literature; what this mission adds is machine-checked proofs. The statements are not present in Mathlib in any form, and the note added in version 3 of the paper — a condition for the marginal case that was missing in the original version — is a concrete reminder that the case analysis here is easy to get subtly wrong.
The obvious route to stability is to minimise directly; it fails because the domain is a cone with a boundary, and the minimisation over the boundary introduces a Lagrange multiplier whose admissible values are the roots of , including the degenerate "exceptional" solutions where is singular. Those exceptional solutions are not a technicality: they are where the eigenvalue clauses of , the correction in (4.43), and the junk-value behaviour of matrix inverses all live. The marginal case ( and vanishing simultaneously somewhere) is not decided by the signs alone and needs the quantitative bound .
Vectors in are plain functions Fin 3 → ℝ with an explicitly defined dot product; is a Matrix (Fin 3) (Fin 3) ℝ and its symmetry is carried as a hypothesis. Four-vectors are indexed by Unit ⊕ Fin 3 so that and are block matrices, with the first component being . Higgs configurations are complex matrices and ; a gauge transformation is with .
Stability is formalized as the honest statement that is bounded from below on the physical domain , — not as any of the sign conditions that the theorem derives — so none of the implications is true by definition. Matrix inversion in Lean returns the zero matrix at a singular argument; every occurrence of is therefore guarded by a regularity hypothesis, and the values of at an eigenvalue of are defined as limits, with the existence of those limits part of the membership condition for . The projection is characterised by its defining property (it lies in the eigenspace and is orthogonal to it) rather than by a choice of eigenbasis.
A complete development needs linear algebra over (resolvents, symmetric matrices, eigenspaces), and the spectral decomposition of positive semi-definite complex matrices for Theorem 4, and elementary real analysis (compactness of the ball, limits of rational functions) for Section 4. The gauge-orbit statement and the light-cone parametrisation are reusable for any multi-doublet scalar sector; contributions of the -doublet generalisation (Appendix B, Theorem 5) are welcome as follow-ups.
Every guarantee in the preceding chapters assumes a fixed distribution and i.i.d. sampling. On-line learning drops both assumptions: an algorithm processes one example at a time, in an adversarial (worst-case) sequence, and is judged by regret against the best fixed comparator in hindsight rather than by generalization error. This chapter develops the theory for this setting — mistake bounds and regret bounds for prediction with expert advice, a margin-based mistake bound for the Perceptron — and then closes a conceptual gap: since on-line algorithms need no distributional assumption, can their guarantees be converted into ordinary distributional (batch) generalization guarantees when the data does happen to be i.i.d.? The on-line-to-batch conversion theorem answers yes, using nothing but an Azuma's-inequality martingale argument on the sequence of hypotheses the algorithm actually produces.
At round t, an on-line algorithm receives x_t, predicts ŷ_t, receives the true label
y_t, and incurs loss L(ŷ_t,y_t); its regret R_T (Eq. 8.1) compares its cumulative loss to
the best fixed action's in hindsight. §8.2 develops this for prediction with expert advice: the
Halving algorithm (realizable case), Weighted Majority and its randomized version RWM
(zero-one loss, Theorem 8.4's L_T ≤ log(N)/(1-β) + (2-β)L_T^min, proved by the chapter's
recurring potential-function technique applied to W_t = ∑_i w_{t,i}), and the Exponential
Weighted Average algorithm (convex losses). §8.3.1 analyzes the Perceptron, a linear
classification algorithm whose margin-based mistake bound (Theorem 8.8, separable case; the
non-separable Theorem 8.11, restated here, in terms of an arbitrary comparator v's hinge
losses) depends only on the normalized margin, not the ambient dimension. §8.4 shows that
averaging the hypotheses h_1,…,h_T an on-line algorithm produces while processing an i.i.d.
sample S yields a hypothesis with controlled true risk: Lemma 8.14 bounds the average of
the per-round risks R(h_t) by the average on-line loss via a martingale argument on
V_t = R(h_t) - L(h_t(x_t),y_t), and Theorem 8.15 upgrades this, via the loss's convexity, to
a bound on the risk of the averaged hypothesis (1/T)∑h_t.
Theorem 8.4 (milestone). Fix β∈[1/2,1). For any T≥1: L_T ≤ log(N)/(1-β) + (2-β)L_T^min; for β=max{1/2,1-√(log(N)/T)}: L_T ≤ L_T^min + 2√(T log N).
Theorem 8.11 (milestone). M ≤ inf_{ρ>0,‖v‖₂≤1}[(r/ρ+√(r²/ρ²+4‖l_ρ‖₁))/2]², where
l_ρ=(l_t)_{t∈I}, l_t=max{0,1-y_t(v·x_t)/ρ}.
Lemma 8.14 (milestone). For any δ>0, with probability at least 1-δ:
(1/T)∑_tR(h_t) ≤ (1/T)∑_tL(h_t(x_t),y_t) + M√(2log(1/δ)/T).
Theorem 8.15 — the mission's goal (first inequality). Under Lemma 8.14's hypotheses, with
L additionally convex in its first argument: for any δ>0, with probability at least
1-δ: R((1/T)∑_th_t) ≤ (1/T)∑_tL(h_t(x_t),y_t) + M√(2log(1/δ)/T).
Theorem 8.15 is the chapter's conceptual capstone: it is the only bridge in the whole book
between the adversarial on-line-learning framework and the distributional PAC/statistical
framework every other chapter develops, and its proof needs nothing beyond Lemma 8.14 plus
convexity — no new machinery, just the right observation about the loss's structure. Theorem
8.4 is the chapter's cleanest instance of its recurring potential-function proof technique
(reused, with variations, for Theorems 8.3, 8.6 and 8.7), and — checked against the platform's
existing OnlineConvexOpt.Introduction.randomized_weighted_majority_mistake_bound (Hazan
series) — a genuinely different result from what is already on the platform: that lemma
bounds a mistake count with a (1+ε) multiplier, this bounds the RWM algorithm's own
weighted-mixture loss with a 1/(1-β) term and a distinct optimal-β substitution,
confirming BRIEF.md's assessment that the two are close but not interchangeable. Theorem
8.11 is the non-realizable generalization of the separable-case Perceptron bound (Theorem 8.8)
that motivates soft-margin algorithms generally, expressed via an arbitrary comparator's hinge
loss rather than assuming perfect separability. No prior art exists for the chapter's other
content: GET /theorems?q=online%20to%20batch returns zero hits, and GET /theorems?q=perceptron returns only an unrelated neural-network topology result.
Theorem 8.4's proof (mirrored by Theorem 8.3's WM analogue) derives matching upper and lower
bounds on the potential W_t, combines them via a logarithm, and substitutes a specific
optimal β found by differentiating the resulting bound — a genuine two-step optimization
argument, not a direct algebraic identity. Theorem 8.11's proof solves a quadratic inequality
in √M after summing the hinge-loss-defining inequalities over the update set I and
invoking the Cauchy-Schwarz step already used in Theorem 8.8's proof; keeping the inf over
both ρ and v in the statement (not fixing them, per BRIEF.md's pitfall note) is what
makes this a genuine bound rather than a bound for one arbitrary choice. Lemma 8.14's proof is
an application of Azuma's inequality (the book's own Theorem D.7) to the martingale difference
sequence V_t = R(h_t) - L(h_t(x_t),y_t), which requires h_t to be measurable with respect
to the history strictly before round t — the on-line algorithm's hypothesis at round t
must not depend on the pair drawn at that same round, per BRIEF.md's pitfall note. Theorem
8.15's step beyond Lemma 8.14 is the passage from the average of T individual risks to the
risk of the averaged hypothesis, licensed by Jensen's inequality under the loss's convexity in
its first argument — dropping convexity breaks exactly this step, not merely weakening a
constant.
GeneralizationError restates chunk 11-regression's Eq. (11.1) convention locally (Y := ℝ,
consistent with that chunk's own harmless simplification), needed here since Theorem 8.15
requires averaging hypotheses into a single real-valued function. OnlineHypothesis A S t is
formalized so that its type signature itself enforces history-adaptedness: the on-line
algorithm A : (n:ℕ) → (Fin n → X × ℝ) → (X → ℝ) is a function of the prefix of the sample
seen so far, and OnlineHypothesis A S t applies it only to S's first t pairs — this is
what licenses Azuma's inequality's martingale-difference argument (the conditional-mean-zero
property of V_t), per BRIEF.md's pitfall note. Revision (2026-09-19), correcting an
earlier claim in this section: history-adaptedness does not by itself guard against
GeneralizationError's Bochner integral silently junking to 0 for a non-measurable
hypothesis (a distinct property — whether h_t, as a function of x, is Measurable — from
whether h_t depends on round t's own draw). Moderation found this a live gap in both Lemma
8.14 and Theorem 8.15's drafted statements; both now carry an explicit hAmeas/hLmeas
hypothesis in addition to the history-adapted type signature.
RWM's w_{t,i}, W_t, p_{t,i}, L_t, L_T, L_{T,i}, L_T^min are modeled as their own
recursively-defined algorithm state (mirroring, but never substituting into, chunk
07-boosting's AdaBoost pattern), matching this chapter's own loss-based (not mistake-count)
quantities, per BRIEF.md's pitfall note distinguishing them from AdaBoost's and RWM-mistake
variants. The Perceptron's w_t, update-index set I, and M = |I| are modeled the same way,
using Eq. (8.23)'s equivalent sign-agreement update rule (the book's own reformulation of
Figure 8.6's sgn-based rule). Theorem 8.11's inf_{ρ>0,‖v‖₂≤1} is a genuine nested restricted
infimum (⨅ ρ ∈ Set.Ioi 0, ⨅ v ∈ Metric.closedBall 0 1, …), not a bound instantiated at fixed
ρ, v, per BRIEF.md's explicit pitfall note. No numerical constant is altered from the
book in any of the four theorems.
Not formalized: Theorems 8.1-8.3 (Halving and WM mistake bounds — the chapter's warm-up
results, superseded in content by the more general RWM/EWA theorems that follow), Theorem 8.5
(a matching lower bound, a distinct impossibility result rather than an algorithm's guarantee),
Theorems 8.6-8.7 (Exponential Weighted Average regret bounds — a third algorithm with its own
potential-function proof, out of scope per BRIEF.md's restriction to §8.2's Halving/WM/RWM),
Theorems 8.8-8.10 (the Perceptron's separable-case bound and its leave-one-out-based expected
generalization bounds, both superseded in generality by Theorem 8.11 for this mission's
purposes), Theorem 8.12 (Perceptron's L²-norm hinge-loss bound, the book's own note that it is
implied by, and looser than, Theorem 8.11's L¹-norm bound), the dual/kernel Perceptron (an
equivalent reformulation, not new generalization content), and Theorem 8.15's second displayed
inequality (a regret-form corollary depending on the regret decomposition of the surrounding
discussion, not drafted per BRIEF.md's own recommendation to commit to the first inequality
as the goal). §8.3.2 (Winnow) and §8.5 (the game-theoretic connection) are out of scope per
BRIEF.md's chapter restriction.
Weak learning — a base classifier only slightly better than random guessing — is easy to come by; strong learning, in the PAC sense of Chapter 2, is not. Boosting is the technique that turns the first into the second: combine many weak classifiers, each trained on a reweighted version of the sample that emphasizes previously misclassified points, into a single strong ensemble. AdaBoost, the algorithm this chapter studies, does this with a specific, closed-form weighting rule, and comes with two distinct theoretical guarantees: its training error decreases exponentially fast in the number of rounds (Theorem 7.2), and — more surprisingly — its test error can keep improving even after the training error has already reached zero, an empirical phenomenon that Chapter 3's VC-dimension bound cannot explain at all (it predicts overfitting for large numbers of rounds) but that a margin-based analysis, structurally identical to Chapter 5's SVM theory, does (Theorem 7.7). This mission formalizes both routes.
AdaBoost (Figure 7.1) takes a labeled sample with and a base classifier set , and runs for rounds. It maintains a distribution over the sample indices, starting uniform (); at round it selects a base classifier with small -weighted error , sets and , and reweights: . After rounds it returns ; its normalized version is . Since makes , is a genuine convex combination of base classifiers, i.e. a member of the convex hull (Eq. 7.12). The chapter reuses Chapter 5's confidence-margin apparatus (empirical margin loss , Rademacher complexity /) to analyze 's generalization.
Theorem 7.2 (AdaBoost empirical error bound, milestone). The empirical (zero-one) error of satisfies , and, if for all , : training error decays exponentially in whenever every round beats random guessing by a fixed margin (the "edge" ).
Lemma 7.4 (milestone). : the convex hull of a hypothesis set, though generally much larger, has exactly the same empirical Rademacher complexity as the set itself.
Corollary 7.5 (Ensemble Rademacher margin bound, milestone). For a set of real-valued functions and , with probability at least , every satisfies (and the empirical-complexity analogue with an extra additive term) — this is Theorem 5.8's margin bound applied to , then rewritten via Lemma 7.4 so its complexity term is 's own, not the (much larger) convex hull's.
Theorem 7.7 — the mission's goal. Assume for every (so ). Then for any ,
Theorem 7.7's bound is what makes margin theory a genuine explanation of AdaBoost's empirical
behavior: combined with Corollary 7.5 (applied to ), it shows that if
AdaBoost's edge stays bounded away from zero, the empirical margin loss at a fixed
decreases exponentially in while the generalization bound's complexity term does not depend
on at all — so continuing to boost past zero training error can still shrink the true risk,
by growing the margin on the training points that are already correctly classified. This
resolves the puzzle that opens §7.3.1: AdaBoost's test error is empirically observed to keep
decreasing well after its training error hits zero, which the chapter's own earlier
VC-dimension bound on (Eq. 7.9, growing as ) predicts should
eventually overfit, not improve. No prior art on the Prove2Me platform is faithful:
GET /theorems?q=boosting and q=AdaBoost return no hits; this chunk's Rademacher-complexity
apparatus is restated locally (a draft item cannot import chunk 05-svm's or 03-rademacher-vc's
own draft copies) rather than reused, matching the precedent those chunks' own STATUS.md
records recommend for every later chunk needing the same machinery.
Not formalized here: Theorem 7.6 (the VC-dimension-based ensemble margin bound, a direct
corollary of Corollary 7.5 via chunk 03's VC-dimension apparatus) — restating 03's own
machinery a second time for a single further corollary is disproportionate within this
mission's budget, and the chapter's actual capstone targets the sharper, dimension-free
Rademacher-complexity route (Theorem 7.7) instead. Also out of scope: §7.2.2's coordinate-
descent equivalence, §7.2.3's practical (decision-stump) use, and §7.3.4-7.3.5's margin-
maximization LP and game-theoretic interpretation — discussion sections with no numbered result
feeding the goal's proof.
Theorem 7.2's proof needs the telescoping identity (Eq. 7.2), obtained by repeatedly unfolding the recursive weight update — a genuine induction on , not a one-line algebraic manipulation — before the elementary inequality turns the empirical error into a telescoping product of the 's, each of which is then re-expressed in closed form via a case split on . Theorem 7.7's proof reuses the same identity but with an added margin-shift term inside the exponential, requiring the same telescoping machinery plus a separate accounting of against the product of factors coming from each 's own closed form — a proof that shares its main structural step with Theorem 7.2 but is not a trivial corollary of it. Corollary 7.5's proof is Lemma 7.4 (itself a careful supremum-exchange argument using the dual-norm characterization of , not a routine calculation) composed with Theorem 5.8, applied to the specific set rather than a generic hypothesis class — a formalization that stated the corollary only for a "sufficiently nice" abstract class, without deriving it from Lemma 7.4's convex-hull identity, would be proving a different, weaker-provenance statement.
WeightedError, AdaBoostAlpha, AdaBoostNormalizer, AdaBoostDist, AdaBoostEpsilon,
AdaBoostEnsemble, AdaBoostNormalizedEnsemble, EmpiricalError and ConvHull are new,
capturing AdaBoost as an actual algorithm (a genuine recursion on the round index, closed under
Definitions.Def_FoundationsML_Boosting_AdaBoostDist's own recursive equation) rather than an
unspecified "boosting procedure" — the trivialization trap BRIEF.md names for this chapter.
AdaBoostDist takes the sequence of base classifiers actually selected at each round,
h : ℕ → X → ℝ, as external data rather than deriving it via an argmin over H; this is
checked in SELF_REVIEW.md to drop no content either milestone or the goal theorem's statement
actually needs, since neither invokes h_t's optimality, only the weighted error ε_t it
produces under AdaBoost's own distribution D_t. PhiRho, EmpiricalMarginLoss,
MarginGeneralizationError, EmpiricalRademacherComplexity and RademacherComplexity are
restated locally, byte-identical to chunk 05-svm's own copies of Definitions 5.5, 5.6, 2.1
(specialized), 3.1, 3.2 (a draft item cannot import another chunk's draft module); this
duplication collapses once 05-svm and 03-rademacher-vc are uploaded and listed in
missions/README.md's "Published definitions" table. No numerical constant in any of the four
theorems is altered from the book's own displayed form. A trivializing formalization this
mission avoids: stating Theorem 7.2/7.7 for an arbitrary sequence of error rates
satisfying , disconnected from any actual
algorithm — AdaBoostEpsilon instead ties every ε_t to the weighted error AdaBoost's own
recursively defined D_t assigns to its own selected h_t, so the bound is provably about
this algorithm's error trajectory, not an arbitrary one.
Quantum field theory begins, mathematically, with a question that has a completely precise answer: what is the state space of a single relativistic particle? Non-relativistic quantum mechanics answers and moves on. Relativity does not allow that answer, because the state space must carry an action of the symmetry group of Minkowski spacetime — the Poincaré group — and the choice of Hilbert space is dictated by which such action one wants. The construction that results is the foundation on which Fock space, creation and annihilation operators, free fields and eventually interacting theories are built, and it is where the objects that reappear everywhere in the subject are introduced: the mass shell, the Lorentz-invariant measure on it, and the double cover that is responsible for spin.
This mission formalizes that construction as it is presented in S. Chatterjee's Lectures on Quantum Field Theory (Stanford, 2018–19), Lectures 9–11 and Lecture 25: the one-particle space of a massive scalar boson, the one-particle space of an electron, and the statement that both carry inner products invariant under the Poincaré action.
Minkowski spacetime is with the bilinear form
A Lorentz transformation is a linear map with ; the restricted Lorentz group consists of those with and . The Poincaré group is with the group law .
For a mass , the four-momentum of a particle satisfies and , so it lies on the mass shell
a three-dimensional manifold parametrised by the spatial momentum through with . On there is, up to a multiplicative constant, exactly one measure invariant under ; with the normalisation used in the lectures it is the measure determined by
The state space of a massive scalar boson is , acted on by .
For an electron the wave function takes values in and the group acts through the double cover. To each four-vector one attaches the Hermitian matrix
and for the transformation of is defined by ; the map is a surjective two-to-one homomorphism onto . Writing , each is reached from by a unique positive-definite , the pure boost, and the electron inner product is the -weighted one,
with the group acting by .
For , , and :
for in the weighted space of -valued functions. The goal fixes no constants beyond the normalisation of , and it is the statement that the spaces defined in the mission really are the one-particle spaces of the theory: a Hilbert space together with a Poincaré action by isometries.
The milestone list follows the lectures: the parametrisation of ; invariance of under ; the integration formula for (eq. (10.1)); invariance of ; uniqueness of the invariant measure up to a constant; the composition law and unitarity of the scalar representation; and bijectivity of onto Hermitian matrices; as a multiplicative map into ; surjectivity of with fibres ; existence and uniqueness of the pure boost ; Lemma 25.1; and the identification of the weighted electron space with the plain -valued space via .
The objects here are used unchanged for the rest of a QFT course: the bosonic and fermionic Fock spaces are built on these one-particle spaces, and the free scalar and Dirac fields are operator-valued distributions written as integrals against on . Formalizing them fixes, once and for all, the conventions later work must match — the normalisation of , the sign convention of the metric, which of the two elements of acts, and the weight in the electron inner product.
What this mission adds beyond the lectures is a machine-checked development of material usually treated as routine but rarely written out: the uniqueness of the invariant measure, the covering map and its fibres, and the existence-uniqueness of the pure boost are all stated in the source either without proof or as exercises. Mathlib has the general theory of spaces, push-forward measures, Hermitian and positive-definite matrices, and , but it has no mass shell, no invariant measure on it, and no covering map onto the restricted Lorentz group; all of that is constructed here and is reusable by any later mission on free fields or Fock spaces.
The obvious route to the invariant measure — "restrict Lebesgue measure to the submanifold " — does not work: the induced Riemannian volume of the hyperboloid in the Euclidean metric is not Lorentz invariant. The lectures instead take a scaling limit of Lebesgue measure on the invariant annuli ; the formalization takes the resulting formula (10.1) as the definition and must then prove invariance, which amounts to a change-of-variables computation whose Jacobian is exactly -dependent. Uniqueness is harder: it is a statement about invariant measures on a homogeneous space of a non-compact group, with no finiteness available.
On the spinor side, the central difficulty is that the weight is unbounded on , so the electron space is not the naive -valued — the two spaces consist of different functions, and are related only through the measurable field of isomorphisms . A formalization that silently uses the unweighted space would prove a different, and false, unitarity statement.
Four-vectors are functions , with the metric signature ; Lorentz transformations are real matrices, and membership in is the predicate (, , form preserved). is a Borel measure on all of carried by , defined as the push-forward of ; the boson space is the library space of that measure. The pure boost is given by the closed formula — the positive-definite square root of — rather than by a choice function, and a milestone certifies that it is the unique positive-definite element of carrying to . The electron space is the set of -valued measurable functions of finite weighted norm, with the weighted pairing given explicitly; the milestone identifying it with the plain space via the inverse boost is what supplies its Hilbert-space structure.
The unitarity statements are formalized as equalities of integrals over pairs of wave functions rather than as statements about abstract operators, so that no trivializing reading is available: in particular the electron clause is stated for the weighted pairing, which is not the standard inner product, and the hypotheses (, , in the respective spaces) are satisfiable, so no clause holds vacuously. Total-function conventions of the library (inverse of a singular matrix is ; integral of a non-integrable function is ) are visible in the statements and are recorded in each item's read-back.
Contributions of any of the milestones are welcome; the measure-theoretic milestones (invariance and uniqueness) and the covering milestones are independent of each other and can be attacked in parallel.
A device's mean residual life at age — its conditional expected remaining lifetime given that it has survived to — is one of the oldest and most interpretable summaries in reliability and survival analysis: it is what an insurer, a maintenance planner, or a hospital outcomes researcher actually wants to know about a unit still in service. Comparing two mean residual life functions pointwise gives the mean residual life order , a natural "the survivor of is worn less, on average, than the survivor of " comparison that is weaker than the usual stochastic order but not directly comparable to it (the book states plainly that neither implies the other in general). This mission formalizes the order's definition and its precise relationship to the stronger hazard rate order : under an extra monotone-ratio condition the two orders coincide, and one direction of that coincidence always holds. A third milestone gives one of the chapter's closure properties, showing that "decreasing mean residual life" (DMRL) — an aging notion used throughout reliability theory to describe units that wear out, rather than improve, with age — is preserved under adding independent noise.
Fix a probability space and a real-valued random variable with survival function and finite mean. The mean residual life function of at is
For a second random variable on with mrl function , is smaller than in the mean residual life order, , if for every . The hazard rate order, restated in this mission's own namespace (Chapter 1's version cannot be imported — see Formalization scope), is the general, absolute-continuity-free comparison for all , where is 's survival function. A random variable is DMRL (decreasing mean residual life) if its mrl function is decreasing in .
Combined with the companion milestone below, this is a genuine conditional equivalence: under the monotone-ratio hypothesis, and coincide, and in particular under that condition. Without the hypothesis, the book states explicitly (the paragraph immediately preceding Theorem 2.A.1) that neither nor implies the other.
Each milestone is stated exactly as the book states it: no constant is hard-coded, no or asymptotic approximation is involved, and the goal's monotone-ratio hypothesis is the genuine ratio , not two separately-monotone functions (a different, unrelated condition the book itself does not state).
The mean residual life order sits at a specific point in the book's own hierarchy of orders: strictly implied by the hazard rate order (Theorem 2.A.1), and — the goal theorem — reversible into the hazard rate order under one extra monotonicity hypothesis on the ratio of the two mrl functions. This "sandwich" structure is exactly the kind of comparison-of-orders result that makes Chapter 1's usual and hazard rate orders (already formalized in Chunk 01 of this series, restated locally here since drafts cannot import each other) into a genuinely connected theory rather than a list of unrelated definitions. The DMRL closure property (Theorem 2.A.11) is separately significant: DMRL is one of the book's standard "aging" notions, used in reliability engineering to model components that wear out over time, and its preservation under adding independent noise is a basic tool for building compound reliability models (e.g. a component with an added, uncorrelated failure mode) from simpler DMRL parts.
No prior art exists on the platform for either order: GET /theorems?q=mean+residual+life
returns zero hits, and GET /theorems?q=hazard+rate returns exactly one hit
(DQJSQ.theorem2_ifr), an unrelated queueing-theory IFR (increasing failure rate) lemma about
patience densities in a fluid queueing model, not this order — it names a different object under
a coincidentally similar keyword and is not reused. This mission is a foundational island for the
mean residual life order.
The mrl function is a genuinely two-case object: a real conditional expectation on , and a hard outside that region. The goal theorem's proof (not formalized here; only the statement is a milestone) differentiates and , uses the identity relating the mrl function to the hazard rate, and compares the two resulting hazard-rate expressions using the ratio's monotonicity — a genuinely analytic argument, not a routine unfolding of definitions. The chief formalization difficulty is keeping the shape of (a pointwise comparison of a derived function) visibly distinct from the function-class shape of used in Chapter 1, since the book explicitly warns that conflating the two orders is a live error (neither implies the other in general) — see Formalization scope below for how each shape is kept separate.
All three random variables in this mission's milestones are real-valued measurable functions on
a MeasureTheory.Measure space, matching this series' Chapter 1 convention (Chunk 01). The mrl
function mrl μ X t is defined as if 0 < P{X>t} then (∫ ω in {X>t}, (X ω - t) ∂μ) / P{X>t} else 0, formalizing the case split on directly via positivity of the survival probability
(its defining equivalent under the survival function's monotonicity) rather than through the
derived quantity itself. MrlOrder μ ν X Y is ∀ t : ℝ, mrl μ X t ≤ mrl ν Y t — a direct
pointwise comparison of two functions, deliberately kept a different shape from Chapter 1's
UsualOrder (a ∀ φ ∈ 𝒞, E[φ∘X] ≤ E[φ∘Y] function-class quantifier), since the book's own
warning that and neither implies the other is a warning against treating
them as interchangeable comparison shapes.
The hazard rate order is restated locally in this chapter's own namespace
(StochasticOrders.MeanResidualLife.HazardRateOrder) rather than imported from Chunk 01's
StochasticOrders.Usual.HazardRateOrder, because each chapter's mission is drafted and reviewed
as an independent Prove2Me proposal and one draft cannot import another draft's unpublished Lean;
its definition is identical in shape to Chunk 01's own restatement of the general,
absolute-continuity-free survival-function form of (not the density-ratio form, which
requires absolute continuity the book does not assume at this level of generality).
Every milestone that consumes mrl carries explicit Integrable hypotheses on the random
variables involved (Integrable X μ, and Integrable Y ν or Integrable Z μ as applicable),
formalizing the book's own standing "finite mean" hypothesis from §2.A.1's definition of the mrl
function: without it, the Bochner integral inside mrl would return its junk value 0 for a
non-integrable variable on some tail set, letting a hypothesis like MrlOrder μ ν X Y hold of a
function that is not actually the book's mean residual life function. DMRL μ X is
Antitone (mrl μ X), the book's own " is decreasing in " in the weak, non-strict
monotone sense used throughout the book for "increasing"/"decreasing".
A trivializing formalization this mission rules out: stating the goal theorem with the ratio
hypothesis as two separate monotonicity conditions on and individually (rather than
genuine monotonicity of the ratio on the region where ) would be a different,
strictly stronger and easier-to-satisfy hypothesis than the book's own — the milestone here states
MonotoneOn (fun t => mrl μ X t / mrl ν Y t) {t | 0 < mrl ν Y t}, the genuine ratio restricted to
where the denominator does not vanish, matching Theorem 2.A.2's own " increases in
" verbatim.
StochasticOrders.Usual), for the usual and hazard rate orders this
chapter's own restated definitions parallel.Every method in Chapters 2-4 of this series solves a projection or proximal subproblem at every step — a Euclidean projection, or a Bregman-divergence prox-mapping — which can itself be as hard as the original problem when is a complicated feasible set (a spectrahedron, a flow polytope, a matroid base polytope). The conditional gradient method (Frank & Wolfe, 1956) sidesteps this entirely: instead of a projection, each step calls a linear optimization (LO) oracle — minimize a linear function over — which is frequently far cheaper (over a spectrahedron, this reduces to a single eigenvector computation; over many combinatorial polytopes, to a greedy algorithm). This is the origin of the modern "projection-free" family of optimization methods widely used at the scale where projections are the bottleneck.
Fix a nonempty compact convex set in a real normed space and a convex with -Lipschitz gradient (Eq. (7.1.4)): . The classic conditional gradient (CndG) method, Algorithm 7.1, sets , , and for : calls the LO oracle , then sets for a stepsize , either the fixed schedule (Eq. (7.1.9)) or exact line search (Eq. (7.1.10)).
Section 7.1.1.2 extends this to bilinear saddle-point problems, where itself is the (generally nonsmooth) function (Eq. (7.1.5)) for a compact convex and linear operator . Since is nonsmooth, the method is applied instead to a family of smooth approximations built from a strongly convex on (Eq. (7.1.21)-(7.1.23)), with the smoothing parameter allowed to vary across iterations rather than being fixed in advance.
Every constant here is exactly the book's; the goal theorem's bound is left in terms of the actual step distances , not a diameter-based simplification (see Difficulty).
This mission formalizes the founding convergence result of the entire projection-free family (Frank-Wolfe methods), which has become central to large-scale machine learning precisely because its per-iteration cost can be orders of magnitude below that of a projection-based method on structured feasible sets. Theorem 7.1's specific form — a rate depending on the realized step distances rather than a fixed diameter — is also the more informative, tighter statement (the book's own remarks show it recovers the classical diameter-based complexity as a corollary, but also explains why the rate can be much better in practice when the iterates settle near an extreme point).
No result matching conditional gradient / Frank-Wolfe methods exists on the platform as of
2026-09-18 (q=Frank-Wolfe and q=conditional gradient both return zero hits — see Prior art
in MODERATION_NOTES.md).
The chief formalization difficulty is representing "with the stepsize policy in (7.1.9) or
(7.1.10)" faithfully without either restricting to one policy (weaker than the book's stated
theorem) or introducing an awkward disjunction of two separate algorithm definitions. The book's
own proof resolves this by a single observation used for both policies at once: for the point the fixed schedule would have
produced — trivially by equality under (7.1.9), or because is chosen to minimize over
the entire line segment under (7.1.10), of which is one point. This mission's
hyk_le hypothesis states exactly this shared consequence, which is genuinely what the proof
uses and genuinely covers both policies, rather than picking one arbitrarily.
A second difficulty is not collapsing into a diameter bound inside the milestone itself — the book's own remarks perform that substitution as a separate, weaker corollary (Eq. (7.1.19)) after stating Theorem 7.1 in its sharper form; folding the substitution into the goal statement itself would silently prove a different, weaker theorem.
conditional_gradient_rate and saddle_point_cndg_rate state the LO oracle's exactness
(x k ∈ Argmin_{z∈X}⟨fGrad(y(k-1)),z⟩) as a pointwise hypothesis rather than deriving it from
IsCompact X via an existence lemma — matching the pointwise-hypothesis convention this series
uses throughout for argmin-defined algorithmic steps (chunk 03-deterministic's mirror-descent
updates, chunk 04-stochastic's stochastic mirror-descent update). X compact convex is still
included as a hypothesis, matching the book's own standing assumption on the problem class, even
though it is not itself needed to derive the stated conclusion from the other hypotheses.
smoothed_objective_monotone and saddle_point_cndg_rate realize / via sSup of the
image of under the pointwise saddle-point objective, matching the book's own max_{y∈Y}{...}
definition (Eq. (7.1.5), (7.1.23)) directly rather than introducing a separate Def_ file for a
"bilinear saddle-point objective" structure — no other item in this mission reuses that
definition verbatim, so per this series' convention (no shared substrate bundled into a structure
unless reused), it is inlined at each use.
A trivializing formalization this mission rules out: stating the LO oracle via an
-approximate minimizer ((fGrad (y(k-1))) (x k) ≤ (fGrad (y(k-1))) z + ε for some
ε) rather than an exact one — this is explicitly a different, weaker algorithm the book does not
analyze in Theorem 7.1/7.2 (the book studies approximate LO oracles separately, later in the
chapter, not selected here).
Left out of scope, for time: Theorem 7.7 (the matching lower complexity bound for LO-oracle
methods, Eq. (7.1.60)) — formalizing it faithfully requires first modeling the abstract class of
"LCP methods" (any algorithm restricted to LO-oracle calls) as a universally-quantified object,
a substantially different and more involved formalization task than the two upper-bound
convergence theorems selected here; named per Hard Rule 7 rather than approximated. The
d(x)=\sum x_i\log x_i entropy-smoothing remark and the primal/primal-dual averaging CndG
variants (§7.1.2, not covered by this mission's page range) are likewise not attempted.
A multistage stochastic program's exact deterministic equivalent grows exponentially with the number of periods, even when each period's random data takes only a handful of values (Chapter 9's concern was the growth in the number of realizations; Chapter 10 adds growth in the number of periods). One remedy, generalizing Chapter 8's single-period Jensen bound, is to replace the exact per-period random data by a coarser, aggregated version — conditional expectations over a partition of the history space at each stage — and solve the resulting smaller deterministic equivalent instead. This is only useful if the aggregated problem's optimal value is provably a bound (here, a lower bound) on the exact problem's, and Birge & Louveaux's Chapter 10, §10.1, Theorem 1 is exactly the statement that makes this legitimate, together with a genuinely necessary extra condition the book states explicitly two paragraphs before the theorem: "if not [i.e. if the extra condition fails], then the conditional expectation form ... may not actually achieve a bound." This mission formalizes that theorem.
The book's exact multistage stochastic linear program (Eq. 1.1, p. 418) is
min c¹x¹ + E_Ω[c²x² + ⋯ + cᴴxᴴ]
s.t. W¹x¹ = h¹, Tᵗ⁻¹xᵗ⁻¹ + Wᵗxᵗ = hᵗ (t=2,…,H, a.s.), xᵗ ≥ 0 a.s., xᵗ nonanticipative (Σᵗ-measurable),
over the exact event space Ω = Ω₁ × ⋯ × Ω_H. Given a consistent nested partition of each
Ωᵗ = Ω₁ × ⋯ × Ωₜ into finitely many blocks Sᵗ₁, …, Sᵗ_νₜ, and aggregated data (h̄ᵗᵢ, T̄ᵗᵢ) = E^{Sᵗᵢ}[(hᵗ,Tᵗ)] (the conditional expectation of the true random data over block i), the
aggregated problem (Eq. 1.2, p. 419) replaces the exact recursion by a finite tree of blocks, one
decision per block, linked to its parent block's decision. Both (1.1) and (1.2) are, structurally,
the same kind of object — a finite-tree deterministic-equivalent recourse LP — differing only in
which tree and which node data they use; this mission formalizes that shared shape once
(Tree, Instance, Feasible, obj) and instantiates it twice.
Formalized as: a shared Tree H structure (a finite node type, per-node stage, anc, and a
root), the same representation Chunk 06's Multistage.Tree uses for the exact scenario tree of
its own (different) chapter, restated here rather than imported (a draft cannot import another
chunk's draft). An Instance H n m T bundles a tree's node-varying LP data
(c, W, Tmat, h, p); Feasible/obj give its feasible set and objective. The exact
problem (1.1) is Instance H n m TFine for a fine/exact tree TFine; the aggregated problem
(1.2) is Instance H n m TCoarse for a coarser tree TCoarse, connected to TFine by an
aggregation map agg : TFine.Node → TCoarse.Node.
agg respects the tree structure (root, stage, ancestor);
W, c agree between the fine and coarse instances (up to agg);
coarse.h, coarse.Tmat are the p-weighted conditional expectations of fine.h, fine.Tmat over
each aggregation fiber;
∀ coarse nodes i,i' at the same stage sharing a "current-period outcome",
coarse.h i = coarse.h i' ∧ coarse.Tmat i = coarse.Tmat i'
⟹ zCoarse ≤ zFine
This is the mission's only formalization target: BRIEF.md records that no separately numbered
lemma precedes Theorem 1's proof in this section to serve as an independent milestone (the proof
is a direct LP-duality argument against the theorem's own hypotheses), and that Chapter 8's
Theorem 1 — the two-period case this theorem generalizes — is a cross-chapter dependency
belonging to Chunk 08's own mission, not a milestone here. milestones.yaml is accordingly empty;
see STATUS.md for the explicit accounting of what else in this chapter was considered and left
out (Theorem 3, the aggregation error bound of §10.2, an unrelated and substantially heavier
result).
Theorem 1 is what licenses every aggregation-based approximation scheme the rest of the book's
multistage material builds on: it says precisely when replacing a multistage recourse problem's
random data by within-period conditional expectations preserves a valid lower bound, and precisely
identifies the condition (aggregated nodes sharing a current-period outcome must carry identical
aggregated data) whose failure breaks the bound — a condition the book states is not decorative
("if not, then the conditional expectation form ... may not actually achieve a bound," p. 418).
Formalizing it gives Prove2Me a first structural result connecting Chapter 8's single-period Jensen
bound (Chunk 08) to genuinely multistage approximation, using the same finite-scenario-tree
deterministic-equivalent representation Chunk 06 uses for the exact nested Benders decomposition
— the two missions' shared representation choice (documented in both STATUS.md files) means a
future mission relating them formally (e.g. instantiating Chunk 06's exact tree as this mission's
TFine) has a compatible object to work with, even though neither imports the other's draft.
The theorem's proof (p. 419-420) is a direct LP weak-duality argument: given an optimal dual
solution to the aggregated problem, the book constructs a dual-feasible solution to the exact
problem attaining the same value, using precisely the "common outcome ⟹ equal aggregated data"
hypothesis to make the constructed dual solution well-defined across the exact tree's finer
structure. This is a real argument, not a citation, but it is left as sorry: formalizing the
proof would need the multistage LP duality machinery (the "multistage version of Theorem 3.13" the
book's own proof invokes, itself left as Exercise 1) that no chunk of this series has built. The
value of this mission is the faithful statement of the bound and its exact hypotheses.
(ωt−1,ωt) ∈ Stj if and only if there exist some (ω̂t−1,ωt) ∈ Stj" —
S^t_j appears on both sides of the "if and only if," where the sentence's own subject ("S^t_i
and S^t_j that have a common outcome") requires the left side to range over S^t_i. Confirmed
against a direct render of PDF page 436 (uv run --with pymupdf python), not assumed from OCR:
the PDF's own typesetting has this repetition, not an artefact of text extraction. This
formalization reads the corrected clause as "S^t_i and S^t_j project onto the same set of
period-t outcomes" and states it via an explicit label type Θ and curOutcome : TCoarse.Node → Θ, since the aggregated tree alone does not carry a literal per-period outcome
space to project onto (see Setting above — Tree records only history-node structure, not the
underlying product space Ω = Ω₁ × ⋯ × Ω_H).W, c shared exactly, not aggregated, matching the book's explicit assumption that the
recourse matrix and per-stage cost are deterministic and identical across (1.1) and (1.2)
("Wt known and not random," "ct = ct," p. 418) — formalized as direct equality hypotheses
(hW_agree, hc_agree) rather than folding W/c into the conditional-expectation machinery
that h/Tmat go through.zFine/zCoarse are hypothesis-characterized, not sInf-defined, avoiding the real
infimum's junk value 0 on an unbounded-below or empty feasible set
(reference/FAITHFULNESS_TRAPS.md trap 5) — neither tree-LP's feasible set is shown bounded or
nonempty by the hypotheses alone.p·h/p·Tmat, not h/Tmat
alone, matching the book's own E^{Sti}[·] = (h̄ti,T̄ti) read as "the fiber-sum of p·(h,T)
equals p_i·(h̄ti,T̄ti)" — the standard definition of a conditional expectation against counting
measure on a finite partition. Instance's own hp_pos (every node's probability is strictly
positive) rules out the degenerate case a bare unweighted equation would need to guard
separately (a coarse node of probability 0, which cannot occur, is what the read-back of this
theorem flags as the one case where the weighted equation would not pin down h_coarse/
Tmat_coarse themselves — moot here since hp_pos excludes it).coarse.h/coarse.Tmat
be arbitrary constants unrelated to fine.h/fine.Tmat (dropping the conditional-expectation
defining equations) would still typecheck a "lower bound" conclusion but assert nothing about
aggregation — exactly the risk BRIEF.md flags: "a formalization that treats (h̄ti,T̄ti) as
arbitrary constants rather than as conditional expectations over a partition of the scenario
space at time t loses the theorem's actual content." Both hCoarse_h/hCoarse_T (the
defining equations) and hCommonOutcome (the theorem's own extra hypothesis) are load-bearing
and present.Two-stage stochastic programs with recourse — choose a first-stage decision now, observe a random outcome , then choose a second-stage recourse decision to repair whatever left infeasible or suboptimal — are the workhorse model of the field, used for capacity planning, inventory and financial portfolio problems since the 1950s (Dantzig 1955; Beale 1955). When ranges over a finite set of scenarios, the recourse function that averages the second-stage cost over scenarios is piecewise linear and convex in , so the overall problem is itself a large linear program — but one whose constraint matrix has a scenario for every column block and can be far too large to hand to a general-purpose LP solver directly. Van Slyke and Wets' L-shaped method (1969), the subject of this mission, is the algorithm that made two-stage recourse problems with finite scenario sets practically solvable: it is Benders decomposition specialized to this block structure, alternating between a small master program over (and a scalar approximating the recourse cost) and, at each candidate , a batch of second-stage linear programs that either certify 's second-stage feasibility or supply a linear underestimate — a cut — of around . Birge & Louveaux's Introduction to Stochastic Programming (2nd ed., Springer 2011), Chapter 5 §5.1, gives the algorithm and proves its two central guarantees: a shortcut feasibility test for a special case (Theorem 1) and the algorithm's finite convergence in general (Theorem 2), which is this mission's goal.
A two-stage recourse instance consists of a first-stage feasible region for , and, for each of finite scenarios (occurring with probability ), second-stage data defining the recourse subproblem
where the recourse matrix is fixed — the same across every scenario, the case this chapter treats. is the set of for which every scenario's subproblem is feasible, and the two-stage problem is
A basis of the recourse subproblem is an injective choice of of 's columns (where is 's row count); each basis determines a simplex multiplier , and when attains the true optimum of , LP duality gives — the mechanism that turns a batch of second-stage LP solves into linear cuts on .
The L-shaped algorithm proceeds in three steps, repeated until neither applies:
Formalized as: starting from the empty cut set, there is a finite-length run of the algorithm's Step-1/2/3 transition relation, of length bounded by the total number of distinct feasibility- and optimality-cut witnesses available, ending at a state admitting no further step — at which point either the master program has become infeasible (certifying ) or its optimum is second-stage feasible, passes every fresh Step-3 test, and is optimal for the two-stage problem.
A shortcut avoiding separate feasibility LPs at Step 2: under these structural assumptions on , checking feasibility at the single componentwise-worst right-hand side certifies feasibility at every scenario simultaneously.
Van Slyke and Wets' method (and Benders decomposition more generally, of which it is the recourse-problem specialization) underlies essentially every large-scale two-stage stochastic program solved in practice, and its finite-convergence guarantee — not merely that an optimum exists, but that this specific cutting-plane procedure reaches it in finitely many outer iterations — is what makes the method a decision procedure rather than a heuristic. The proof's content is an explicit finiteness argument (the number of distinct simplex bases of the recourse subproblem and the feasibility-test LP is finite, so the algorithm cannot generate infinitely many distinct cuts before either exhausting the feasible region or converging), not a general compactness or fixed-point argument; formalizing it means formalizing the cutting-plane mechanism itself as a transition system and proving termination combinatorially, over the finite type of available bases, rather than proving only that some optimal exists.
The natural shortcut — state only "an optimal exists, or " — is not Theorem 2's actual content and is not what this mission targets: that weaker claim would already follow from being a nonempty polyhedron (or empty), with no reference to the algorithm at all, and would not require the finiteness-of-bases argument the book's proof turns on. The genuine difficulty is representing Steps 1-3 faithfully as a relation on accumulating cut sets, and pinning the termination bound to the actual combinatorial object the book cites (the finite set of bases of the two LPs the algorithm solves at each iteration) rather than to a numeral or an abstract compactness bound. A second, quieter difficulty is Step 1's own optimum: once optimality cuts exist, the master program optimizes jointly, but before the first one it optimizes alone; conflating the two (e.g. always requiring to be part of the optimum) does not match Step 1 as the book states it.
First-stage and second-stage vectors are Fin n1 → ℝ / Fin n2 → ℝ; the finite scenario set is
Fin K with probability vector p. A basis is {b : Fin m2 → Fin n2 // Function.Injective b} (m2 = the recourse matrix's row count), matching "an injective choice of columns of
"; its finiteness is definitional, from Fin m2 → Fin n2 being finite. Simplex multipliers use
Matrix.inv, whose junk value 0 on a singular matrix is never reachable in a proof because
multipliers are only ever used through an IsOptimalAt/IsFeasBasisOptimalAt hypothesis that
pins the basis to one genuinely attaining the LP's true optimum. The recourse value
is EReal-valued (reusing this series' Instance/QVal convention from Chunk 03), so an
optimality-cut witness's claimed value is compared to it by an explicit EReal cast, never by
EReal arithmetic. The algorithm's state is a pair of finite sets of witnesses recorded so far
(Finset (Fin K × FeasBasis n2 m2) × Finset (Fin K → Basis n2 m2)); Step is an inductive
relation with one constructor per Step-2 and Step-3 branch, each requiring its witness not already
recorded, and the goal states a bounded-length Step-path from the empty state to a state
admitting no further Step. This mission does not restate Chapter 3's polyhedrality fact
about as a separate lemma: the finiteness fact it is invoked for is already exposed directly
and structurally by the finite Fintype bound on the number of bases, so no additional axiom
stands in for it (see MODERATION_NOTES.md). Lemmas 3-9 and Theorem 10 of §5.2 (Regularized
Decomposition, a different algorithm) are out of scope. The trivializing formalization this
mission rules out is exactly the one named under Difficulty above: a bare existence-of-optimal-or-
infeasible- statement with no reference to Steps 1-3 or to a finite bound on the number of
iterations — such a statement would be true of any nonempty polyhedron and would not be Theorem 2.
Von Neumann introduced amenable groups in 1929 to explain the Hausdorff–Banach–Tarski paradox, and showed that the class of amenable groups contains all finite and all abelian groups and is closed under four processes: (I) subgroups, (II) quotients, (III) extensions and (IV) directed unions. Day named the smallest class with these properties , the elementary amenable groups. For fifty years these were the only amenable groups anyone could exhibit, and von Neumann's question whether every non-amenable group contains a free subgroup on two generators — whether equals the class of groups without such a subgroup — was open. (It was answered in the negative by Ol'shanskii in 1980, the year of this paper, by different methods.)
Ching Chou's Elementary amenable groups (Illinois J. Math. 24 (1980) 396–407, doi:10.1215/ijm/1256047608) gives the structure theory of that everything later relies on. Its central result is that the class can be built from finite and abelian groups by extensions and directed unions alone — subgroups and quotients add nothing (Proposition 2.2). From that description three things follow: periodic elementary amenable groups are locally finite, so the periodic non-locally-finite groups of Golod and Novikov–Adjan show (Theorem 2.3); a finitely generated simple elementary amenable group is finite (Corollary 2.4); and Wolf's conjecture holds in : a finitely generated elementary amenable group is almost nilpotent or has exponential growth (Theorem 3.2, extending Milnor and Wolf's theorem for solvable groups). A final section introduces a packing property (P) of groups and proves it for every elementary amenable group (Proposition 4.2) and every residually elementary amenable group (Corollary 4.7).
On this platform the definition of is already published
(the bundle Chou_ElementaryAmenable, from the mission
Cannon–Floyd–Parry: Thompson's group F and the simplicity of its commutator subgroup),
together with the theorem that Thompson's group is not elementary amenable
(Theorem 4.10) and, from Brin and Squier, that has no free subgroup on two
generators (CannonFloydParry.no_free_subgroup_of_rank_two). This mission formalizes
Chou's paper on top of that definition.
The class and its constructible core. Chou.ElementaryAmenable G is an inductive
predicate on groups: finite groups and abelian groups are in the class, and the class is closed
under isomorphism, subgroups, quotients, extensions and directed unions of subgroups; each rule
is a constructor of the published bundle Chou_ElementaryAmenable, where it is stated precisely. Chou builds the hierarchy
by transfinite recursion, applying only extensions and directed unions to the finite and
abelian groups, and proves that is closed under subgroups and
quotients, hence equals . The union is realised here without
ordinals, as the inductive predicate Chou.Constructible, whose constructors are of_finite,
of_commGroup, of_mulEquiv, extension and directedUnion; Chou's transfinite induction
over becomes structural induction over a derivation, with the same case analysis.
Periodic and locally finite groups. A group is periodic if every element has finite order
(Mathlib's IsMulTorsion) and locally finite if every finitely generated subgroup is finite
(Chou.IsLocallyFinite). Day's class is Chou.NoFreeSubgroupOfRankTwo: no homomorphism
from the free group on two generators into is injective.
Growth. For a finite generating set of , Chou.wordBall S n is the set of products
of at most factors, each in or with inverse in . has exponential growth if for
some finite generating set the ball of radius has at least elements for some
and all ; it is exponentially bounded if for some finite generating set and every
the balls are eventually smaller than . Chou works with for products of exactly
elements of a finite generating set ; for symmetric and containing the identity the
two agree, and Wolf's observation that the growth type is independent of the generating set is
one of the milestones. "Almost nilpotent" is Mathlib's Group.IsVirtuallyNilpotent: a
nilpotent subgroup of finite index. A free subsemigroup on two generators means two elements
such that distinct positive words in are distinct in
(Chou.HasFreeSubsemigroupOfRankTwo).
Packings. A pair of subsets is a packing of if is a
bijection (Chou.IsPacking), and has property (P) if every finite
subset lies in a finite for which some is a packing (Chou.HasPackingProperty).
is residually elementary amenable if every survives in some elementary amenable
quotient (Chou.ResiduallyElementaryAmenable).
The goal is Chou's description of the class, Proposition 2.2 (b) (p. 397): “ is the smallest
class of groups which contains all finite groups and all abelian groups and is closed under
processes (III) and (IV).” It is stated as the equivalence ElementaryAmenable G ↔ Constructible G.
The milestones follow the paper's order.
Section 2. Proposition 2.1 in two halves — the constructible groups are closed under subgroups and under quotients — which is the whole proof of the goal. Theorem 2.3: periodic elementary amenable groups are locally finite; and its consequence that is nonempty. Corollary 2.4: finitely generated simple elementary amenable groups are finite.
Section 3. Lemma 3.1 (an extension of almost nilpotent by almost nilpotent is almost nilpotent or of exponential growth), Theorem 3.2 and Rosenblatt's sharpening Theorem 3.2′, together with the facts Chou uses on the way: a finite-by-nilpotent group is almost nilpotent; a free subsemigroup forces exponential growth; Wolf's independence of the generating set; and Milnor's existence of the growth rate, in the form "exponentially bounded means not of exponential growth".
Section 4. Property (P) for finite groups, for , for finitely generated abelian groups; Lemma 4.1 (directed unions and extensions preserve (P)); Proposition 4.2 (every elementary amenable group has (P)); Lemma 4.6 (a) and Corollary 4.7 (residually elementary amenable groups have (P)); and the free groups.
Chou's Section 3 rests on results the paper cites rather than proves, none of which is in Mathlib. They are stated here as milestones in their own right, so that the dependence is visible and each is a well-defined target: the Milnor–Wolf theorem (a finitely generated solvable group that is exponentially bounded is almost nilpotent); M. Hall's theorem that a finitely generated group has finitely many subgroups of each finite index; that finitely generated nilpotent groups are finitely presented and that a group with a finitely presented subgroup of finite index is finitely presented; Milnor's Lemmas 1–2 in the form Chou states on p. 400 (in a finitely generated exponentially bounded group, a normal subgroup with finitely presented quotient is finitely generated); and Rosenblatt's variant of Lemma 3.1. Section 4 needs one more: free groups are residually finite. Lemma 3.1 and Theorems 3.2, 3.2′ can be closed only once these are; every other milestone is provable from Mathlib and the published library.
Two remarks on Theorem 2.3. Chou's witness for is a periodic group that is not locally finite (Golod; Novikov–Adjan), whose existence is not formalized. The platform already holds a different witness: Thompson's group is not elementary amenable (Cannon–Floyd–Parry, Theorem 4.10) and has no free subgroup on two generators (Brin–Squier); both are published and proved, and the milestone is proved from them. The inclusion itself is von Neumann's theorem that amenable groups contain no free subgroup of rank two, which passes through the definition of amenability and is not part of this mission.
The ordinal-indexed hierarchy and the remark that it stabilises at some (Proposition 2.2 (a)) are replaced by the inductive predicate. Chou's two examples of finitely generated groups in that are not almost solvable (p. 402), the Golod–Shafarevich discussion, and Lemma 4.6 (b) (ordinal-indexed normal series) are omitted. Propositions 4.3–4.5 on almost convergent sets, and Milnor's remark that exponentially bounded groups are amenable, need invariant means on ; amenability itself is the subject of Garrido I.
Given independent random variables , when does converge? Not absolutely — that question is settled by and is usually too strong. The interesting question is when the partial sums converge for almost every outcome, and here independence buys something that holds for no general sequence: convergence is not a delicate matter of cancellation but is decided, once and for all, by three numerical series.
Chapter 2 of Rick Durrett's Probability: Theory and Examples (Version 5, 2019) reaches this in section 2.5. Kolmogorov's three-series theorem fixes a truncation level , replaces each by , and asserts that converges almost surely if and only if
Three deterministic conditions on the distributions decide an almost-sure question about paths, and the answer does not depend on which is chosen. Through Kronecker's lemma this is also the route to the strong law of large numbers, which is how the chapter uses it.
Let be independent real random variables on a probability space, with partial sums . Say that converges almost surely when for almost every the sequence has a real limit; following Durrett, " converges" means exists, not that it converges absolutely.
Three tools from the same section support the theorem. Kolmogorov's maximal inequality strengthens Chebyshev from to the maximum of the whole path,
for independent, centred, square-integrable summands. From it comes the convergence criterion: if and then converges almost surely. Kronecker's lemma is the deterministic bridge to averages: if and converges then . And the Hewitt–Savage 0-1 law says that for an i.i.d. sequence every permutable event — one unchanged by rearranging finitely many coordinates — has probability or .
Both directions are asserted, as Durrett states the theorem. The truncation level is arbitrary and fixed in the statement; that the three conditions hold for one exactly when they hold for every is a consequence, not an assumption.
Kolmogorov's maximal inequality (2.5.5); the convergence criterion under summable variances (2.5.6); Kronecker's lemma (2.5.9); and the Hewitt–Savage 0-1 law (2.5.4).
The result itself. The three-series theorem is the complete answer to a question that has no complete answer without independence, and the shape of the answer is the interesting part: a pathwise, almost-sure property is equivalent to three conditions each computable from the marginal distributions alone. Each of the three does a separate job — the first says and its truncation differ only finitely often, so Borel–Cantelli lets them be exchanged; the second controls the drift of the truncated sums; the third controls their fluctuation. The theorem is also the standard route to the strong law: applying it to and then Kronecker's lemma gives , which is why section 2.5 sits where it does.
Formalizing it. Mathlib has the strong law of large numbers (strong_law_ae), both
Borel–Cantelli lemmas, and Kolmogorov's 0-1 law for the tail σ-field. It has none of the
following: Kolmogorov's maximal inequality, the almost-sure convergence criterion for random
series with summable variances, Kronecker's lemma, the Hewitt–Savage 0-1 law, or the three-series
theorem. The mission therefore contributes the whole of section 2.5, and the pieces are reusable
well beyond it — the maximal inequality and Kronecker's lemma in particular are standard tools with
no probabilistic content in the second case at all.
The maximal inequality is the step where the argument stops being routine. Chebyshev bounds and no more; controlling the maximum over the whole path needs the first passage decomposition and the observation that is measurable with respect to the first variables while is independent of them, so the cross terms vanish. That is a stopping-time argument in disguise, and it is what makes the whole section work.
The sufficiency half of the goal is then assembly: the third series and the convergence criterion give convergent, the second adds the means back, and the first plus Borel–Cantelli replaces by . Necessity is the harder direction, and Durrett does not prove it in Chapter 2 at all — he defers it to Example 3.4.12, where it follows from the Lindeberg–Feller central limit theorem. A solver attacking the goal should expect the reverse implication to need machinery from outside this section.
The Hewitt–Savage law has a difficulty of its own kind: the natural statement is about a σ-field of events on a sequence space, and the proof approximates a permutable event by cylinder events and then applies the permutation that swaps the first coordinates with the next .
Random variables are measurable real-valued functions on a probability space and independence is
Mathlib's iIndepFun. Variance is Mathlib's variance, and square-integrability is stated as
membership in where the maximal inequality and the convergence criterion need it. The
three-series theorem itself assumes no integrability: the truncated variables are bounded, so
their means and variances exist automatically, which is exactly why the truncation is there.
" converges" is formalized as convergence of the sequence of partial sums to a real
limit, not as Summable, which in Mathlib means unconditional and hence absolute convergence for
real series. This distinction is not pedantic here: condition (ii) of the theorem is convergence of
in Durrett's sense and would be a strictly stronger condition if read as
summability. Conditions (i) and (iii) are series of non-negative terms, where the two notions
agree, and are stated as Summable.
Almost-sure convergence of is "for almost every there exists a real with " — the limit is not asserted to be measurable in , and does not need to be for the statement to say what it should.
For the Hewitt–Savage law the sequence space is the countable product carrying
the infinite product of copies of one law, which is Mathlib's Measure.infinitePi, and a
permutable event is a measurable set invariant under every finitely supported permutation of the
coordinates. That is Durrett's exchangeable σ-field stated directly rather than constructed as a
σ-field object.
Contributions welcome beyond the listed items: the converse direction via Lindeberg–Feller (Example 3.4.12); the derivation of the strong law from the three-series theorem and Kronecker's lemma; the Marcinkiewicz–Zygmund law (2.5.12); and the rates of convergence of section 2.5.1.
Many hard combinatorial optimization problems — finding the maximum cut of a graph, deciding the ground state of an Ising spin system, bounding the correlation of a physical system — can be written as maximizing a bilinear form over sign vectors . Exhaustive search over sign patterns is intractable, so practitioners relax the problem: replace each sign by a unit vector in a higher-dimensional space and optimize the resulting inner products instead. This relaxation, a semidefinite program, is convex and solvable in polynomial time. The question is how much is lost in the relaxation — whether its optimal value can be far from the true, combinatorial optimum.
Grothendieck's inequality, proved by Alexander Grothendieck in 1953 in the context of Banach space theory (Résumé de la théorie métrique des produits tensoriels topologiques, Bol. Soc. Mat. São Paulo 8 (1953), 1–79), answers this for a broad class of such relaxations: replacing signs by unit vectors in an arbitrary Hilbert space changes the optimal value by at most an absolute, dimension-free constant factor. The inequality has since become a standard tool across combinatorial optimization, Banach space geometry, and (via the Goemans-Williamson algorithm for maximum cut, Section 3.6 of the source) approximation algorithms; see U. Haagerup, The Grothendieck inequality for bilinear forms on -algebras, Adv. Math. 56 (1985) for the tightest known constant, and Alon–Naor, Approximating the cut-norm via Grothendieck's inequality, SIAM J. Comput. 35 (2006), for the algorithmic connection this mission's Theorem 3.5.6 sets up.
Fix positive integers . Consider a real matrix . Say is normalized if for every choice of numbers ,
This says , viewed as a bilinear form on , has sup-norm at most . Now let be any real Hilbert space — a real vector space equipped with an inner product complete in the induced norm — and consider vectors and , each of unit norm . Replacing the scalar product by the inner product in the same bilinear form gives , a real number depending on the choice of and of the unit vectors. The question is how large this can be, uniformly over every such choice.
for every real Hilbert space and unit vectors , where is a constant depending on neither , its dimensions, nor . This mission's goal formalizes the book's own first-pass bound (Section 3.5), proved by a Gaussian truncation argument; it does not fix a numeral for , only that some absolute constant works, matching the shape of the true statement rather than a specific numeral that a sharper argument (the book's own Section 3.7 gives ) would immediately obsolete. See Formalization scope below for why this is the goal, not the sharper bound.
The result itself. Grothendieck's inequality is the single fact that makes semidefinite relaxation a provably good algorithmic strategy rather than a heuristic: whatever the true, hard-to-compute combinatorial optimum of a -valued bilinear optimization is, the tractable Hilbert-space relaxation cannot overshoot it by more than the constant . Milestone Theorem 3.5.6 makes this concrete for positive-semidefinite matrices, showing the semidefinite relaxation SDP of the integer program INT satisfies INT SDP INT — the guarantee underlying the Goemans-Williamson 0.878-approximation algorithm for maximum cut (Theorem 3.6.5 of the source, out of scope for this mission; see Formalization scope).
Formalizing it. The inequality and its two chapter milestones are proved but not previously
formalized on this platform (checked by concept search for "Grothendieck", "semidefinite",
"positive-semidefinite", and "max-cut" — no hits beyond the unrelated Grothendieck-Teichmüller
group). What remains after this mission is the sharper argument of Section 3.7
(the "kernel trick"), a separate, heavier development building on positive-definite kernels,
and full proofs of every milestone below (currently open sorry goals).
The statement of Grothendieck's inequality contains no randomness, yet every known elementary proof is probabilistic; this is itself a striking feature of the result. The obvious approach — bound directly by exploiting the normalization hypothesis on — fails because the normalization hypothesis only controls against sign vectors, and there is no way to project an arbitrary unit vector in a Hilbert space onto without losing information. The book's proof instead represents each unit vector via a scalar Gaussian random variable for a single Gaussian vector , recovering the inner products in expectation (Exercise 3.3.5); but these Gaussian variables are unbounded, so the normalization hypothesis (which bounds against bounded inputs) cannot be applied to them directly. The core technical step is a truncation argument: splitting each Gaussian variable into a bounded part and a small--norm unbounded remainder, applying the hypothesis to the bounded parts, and bounding the remainder terms by treating them as elements of the Hilbert space and invoking the very inequality being proved (Theorem 3.5.1 itself, applied with ) as a self-referential bootstrap — this is why the proof fixes as the smallest valid constant before starting, rather than building it up from scratch.
The goal and both milestones work with the real matrix and real inner product space directly;
H is required to be a complete real inner product space (NormedAddCommGroup,
InnerProductSpace ℝ, CompleteSpace), matching the book's "any Hilbert space." No
dimension bound on is imposed — the inequality's content is exactly that does not grow
with .
This mission does not formalize the sharper bound of Section 3.7, nor Theorem 3.6.5 (the 0.878-approximation guarantee for maximum cut via randomized rounding): the latter's statement quantifies over "the result of a randomized rounding of the solution of the semidefinite program," which would drag a specific algorithm into the audited statement rather than keeping it a self-contained mathematical claim (the statement/proof-separation trap this series' triage rubric flags). Grothendieck's identity (Lemma 3.6.6), the key fact behind that rounding step, is included on its own as a milestone, stated with an explicit, named random sign variable rather than an opaque "rounding procedure."
A trivializing formalization would state the goal with allowed to depend on , , ,
or — every such bound is easy (e.g. ) and carries none of the
theorem's content; the Lean statement rules this out by quantifying before every other
object. and (Theorem 3.5.6) are defined from scratch in this
chunk's namespace, using Matrix.PosSemidef from Mathlib for the positive-semidefiniteness
hypothesis (which bundles the real-symmetric condition); Mathlib has no ready-made SDP-value
construction to reuse. The sub-gaussian (Orlicz ) norm used by Theorem 3.1.1 is reused,
unchanged, from the 01-concentration mission in this series (HighDimProb.Concentration.SubgaussianNorm)
rather than redefined.
Any dataset of points can be described exactly by embedding it in for large enough — but a large is expensive: nearest-neighbor search, clustering, and streaming algorithms all scale with the ambient dimension, not with . The question that opens this mission is whether the dimension can be cut down while leaving the data's geometry — the pairwise distances between points — essentially untouched.
Johnson and Lindenstrauss answered this in 1984, while studying extensions of Lipschitz maps into Hilbert space (W. Johnson, J. Lindenstrauss, Extensions of Lipschitz mappings into a Hilbert space, Contemp. Math. 26 (1984), 189–206): points in any Euclidean space, of any dimension , can be mapped by a single linear map into a space of dimension only , distorting every pairwise distance by at most a factor of . The map does not depend on the data beyond its cardinality — a single random object works simultaneously for the whole point set with high probability. This is now one of the standard tools of randomized dimension reduction, cited across nearest-neighbor search, streaming linear algebra, compressed sensing, and machine learning pipelines that need to shrink feature dimension before a downstream algorithm runs.
Fix a probability space . A random orthogonal projection of rank in is a map , continuous and linear for each , such that almost surely is idempotent (), self-adjoint, and has range of dimension — i.e. is the orthogonal projection onto some -dimensional subspace . It is uniformly distributed in the Grassmannian (written ) when its law is rotation invariant: for every orthogonal transformation of , the conjugated map has the same law as . Conjugating a projection by is exactly the projection onto the image of its range under , so this says the law of the random subspace is invariant under the full orthogonal group — the operational definition Vershynin himself uses for a "uniformly distributed" random subspace, since no coordinate-free formula for such a subspace's law is given directly.
A companion notion drives the proof: a random vector is uniform on the Euclidean sphere of radius , , when it lies on that sphere almost surely and its law is likewise rotation invariant. And a real random variable is sub-gaussian with sub-gaussian () norm , the standard non-asymptotic measure of how light-tailed 's distribution is (a bounded or Gaussian random variable has finite norm; the tail probability then decays at least as fast as ).
for every finite , every , and every random orthogonal projection of rank uniformly distributed in . The universal quantifier over pairs sits inside the single probability event — this is the union-bound content that makes the statement a genuine simultaneous guarantee for the whole point set, not a restatement of the single-vector lemma below for one fixed pair. Both constants are the book's own unnamed absolute constants, never depending on , , , or ; this is the weakest stable form of the claim (no numeral is hard-coded for or ), matching the book's own statement exactly.
The lemma gives a universal, data-oblivious dimension-reduction guarantee: the target dimension depends only on the number of points and the desired distortion, never on the ambient dimension or on the geometry of the specific point set. This is what makes it usable as a black-box preprocessing step ahead of an algorithm whose cost scales with — the projection is drawn once, without looking at the data, and works with high probability for every pairwise distance simultaneously. The bound is also known to be essentially optimal in : Alon (Problems and results in extremal combinatorics, Discrete Math. 273 (2003)) showed a lower bound of on the target dimension, so the dependence cannot be removed.
The theorem itself has been proved for decades and admits several proof strategies (this book's route through Lipschitz concentration on the sphere; the original volume/measure-concentration argument; later "sparse" or structured variants of the projection for faster computation). This mission formalizes the classical dense-Gaussian-projection proof route as Vershynin presents it, building the sphere-concentration engine (Theorem 5.1.4) and the single-vector projection lemma (Lemma 5.3.2) that the union-bound argument for the goal rests on. No machine-checked formal proof of this chain is known to exist on the platform prior to this mission (see Formalization scope below); what is contributed is the statement infrastructure — the goal and its two direct supporting lemmas, stated with explicit, unpinned absolute constants — for solvers to close.
The natural first idea — bound the distortion of a single fixed vector under a random projection, then take a union bound over the pairwise differences — is exactly the strategy Lemma 5.3.2 and the goal use, but it does not by itself explain why the single-vector concentration bound (Lemma 5.3.2(b)) holds with the stated sub-gaussian-type tail. That bound is not elementary: it reduces to a uniform concentration statement for an arbitrary Lipschitz function of a uniformly random point on a high-dimensional sphere (Theorem 5.1.4), since , viewed as a function of a rotated copy of , is a -Lipschitz function on the sphere. Proving that every Lipschitz function concentrates — not just linear ones, for which sub-gaussianity was already established in Chapter 3 — needs a genuinely different tool: comparing the sub-level sets of an arbitrary Lipschitz function to spherical caps via an isoperimetric inequality on the sphere. This geometric input is what makes the concentration phenomenon behind Johnson-Lindenstrauss a dimension-free fact rather than a special property of coordinate projections.
is a Finset of points in EuclideanSpace ℝ (Fin n), matching "a set of points"; is
read off as X.card. The random subspace is represented throughout by the
orthogonal projection onto it (IsUniformProjection), following the book's own statements,
which are phrased in terms of rather than ; the scaled map of the goal is
written Real.sqrt (n/m) • P ω applied to x - y, using linearity of to realize
. Both "uniform on the sphere" and "uniform in the Grassmannian" are defined
operationally by rotation invariance of the underlying law, since Mathlib has no ready-made
normalized surface measure on a general-radius Euclidean sphere or Haar-measure construction on
the Grassmannian/orthogonal group to build a canonical uniform object from; rotation invariance
uniquely determines the corresponding measure among those supported on the relevant set, so the
operational and constructive definitions coincide extensionally. Every "absolute constant" in the
book ( in Theorem 5.3.1's sample-complexity hypothesis, in every failure-probability bound,
and the sub-gaussian constant of Theorem 5.1.4) is existentially quantified ahead of the
dimension, sample size, and every other object, and pinned to no numeral — a formalization that
hard-coded a specific numeral for any of these would be invalidated by the next sharper constant
in the literature and would not match what the book actually proves.
A trivializing formalization is one that states the conclusion for a single fixed pair rather than universally over all pairs inside one event; that would collapse the union-bound content that makes this a dimension-reduction statement for a whole point set (with points), rather than a restatement of the single-vector Lemma 5.3.2(b). This mission's goal statement is built to rule that out explicitly (see Formalization targets above).
Reusable infrastructure: subgaussianNorm (the Orlicz norm, restated per Vershynin
Definition 2.5.6) and the rotation-invariance idiom for "uniformly distributed" random geometric
objects are of independent interest to any later chapter needing sub-gaussian random vectors or
random subspaces/projections (e.g. Chapters 4, 6, 7, 9, 11 of this same book series). Solvers'
contributions are welcome on: the isoperimetric inequality on the sphere and its use to prove
Theorem 5.1.4 (the mission's hardest open leaf); the coordinate-projection computation underlying
Lemma 5.3.2(a); and the concentration-plus-union-bound argument closing the goal from the three
supporting lemmas.
A recurring question in economics and operations research is: when a decision problem depends on a parameter, does the optimal decision move monotonically as the parameter changes? A firm's optimal input mix as a price rises, a consumer's optimal consumption bundle as income grows, a Cournot firm's optimal output as a rival's output changes — in each case one wants "more of the parameter implies (weakly) more of the optimum" without assuming convexity, differentiability, or a unique optimizer. The classical tool for such comparative statics questions is the implicit function theorem, which needs smoothness and a nondegenerate Hessian and breaks down the moment the optimum is not unique or the objective is not differentiable. Topkis [1978] showed that a purely order-theoretic condition — supermodularity of the objective jointly in the decision variable and the parameter — is sufficient on its own, with no smoothness, uniqueness, or convexity assumed at all, and Milgrom and Roberts [1990a, 1994] later showed this lattice-theoretic approach subsumes and strengthens the classical monotone-comparative-statics results in economics. This mission formalizes the two central results this book calls "Topkis's theorem" (Theorem 2.8.1 and Theorem 2.8.2), together with the structural fact about maximizers of a supermodular function (Theorem 2.7.1) that both rest on, and the strengthening to strictly ordered optimal selections (Theorem 2.8.4).
Let be a lattice: a partially ordered set in which every pair
has a join and a meet . A real-valued function
is supermodular on if
for all ; this is
the same relativized notion (SupermodularOn) used, with , throughout chunk I of
this series.
Now let also be a partially ordered set (the parameter set), and let be a real-valued function of the pair . has increasing differences in if, for every in , the map is monotone (order-preserving) in ; equivalently, the marginal gain from raising is itself increasing in . Replacing "monotone" with "strictly monotone" gives strictly increasing differences. To compare the resulting sets of optimizers rather than single points, this mission reuses the induced set ordering from chunk I: for , holds when and for all , .
Let and be lattices, let be a sublattice of the product lattice , and let be the section of at . If is supermodular on (jointly in the pair ), then
is increasing in , with respect to , on .
With increasing in (with respect to ), supermodular in for each fixed , and having increasing differences in on , the same conclusion — increasing in — holds. Theorem 2.8.2's joint-supermodularity hypothesis on a sublattice of automatically forces both of Theorem 2.8.1's hypotheses, so 2.8.1 is the logically weaker, more elementary statement from which 2.8.2's proof proceeds.
Under the hypotheses of Theorem 2.8.1 but with strictly increasing differences, every individual optimal solution at a larger parameter value dominates every individual optimal solution at a smaller one: , , and together force — a genuinely stronger conclusion than alone gives.
A supporting result is formalized as a milestone because both goals' proofs use it directly: Theorem 2.7.1, that is a sublattice of whenever is supermodular on — the structural fact that makes it meaningful to compare optimal-solution sets with in the first place.
The result itself. Theorem 2.8.2 is the book's own headline theorem, cited throughout the rest of the monograph: it underlies the assortative-matching existence theorem (Chapter 3), monotone optimal policies in Markov decision processes (Chapter 3), and equilibrium comparative statics in supermodular games (Chapter 4) — each a later mission in this series. Its distinguishing feature relative to the implicit function theorem is that it needs no differentiability, no uniqueness of the optimizer, and no interiority: it applies equally to discrete decision problems (integer programming, combinatorial selection) and continuous ones.
Formalizing it. Nothing in Mathlib currently states a parametric monotone-comparative-
statics result of this shape: the closest neighboring material (order-preserving maps,
MonotoneOn, lattice structures) supplies only the vocabulary, not the theorem. This
mission is the first formalization of Topkis's theorem on this platform and introduces
the increasing-differences vocabulary (IncreasingDifferencesOn,
StrictlyIncreasingDifferencesOn) that later missions in this series (matching, MDPs,
supermodular games) reuse directly.
The natural first idea — differentiate in , set the gradient to zero, and use the implicit function theorem on the resulting first-order condition — fails immediately because nothing here is assumed differentiable, and need not be a single point. The correct argument instead compares two arbitrary elements , directly through the supermodularity inequality applied to the pair against (a chain of inequalities Topkis calls "Lemma 2.8.1"), using increasing differences only to move the parameter from to inside that chain — at no point is a derivative, a selection function, or an interior point used. A second subtlety is that "increasing" in the conclusion is with respect to the induced set order , not a claim that some selection is monotone: proving the stronger, pointwise-ordered conclusion (Theorem 2.8.4) genuinely needs the strict form of increasing differences, not merely increasing differences plus an extra hypothesis.
and are kept as abstract Lattice/PartialOrder types throughout, matching the
book's own generality — Theorem 2.8.1's and 2.8.2's /
corollary via second partial derivatives (discussed in the book's prose immediately after
Theorem 2.8.2, p. 77) is not itself a numbered theorem and is not formalized here.
Supermodularity, increasing differences, and strictly increasing differences are each
formalized as a single relativized definition (SupermodularOn f S,
IncreasingDifferencesOn f S, StrictlyIncreasingDifferencesOn f S) so the same
declaration expresses both "supermodular on the whole lattice " (used by Theorem 2.7.1
and Theorem 2.8.1's per- hypothesis) and "jointly supermodular on a sublattice of
" (Theorem 2.8.2) — a formalization that instead only ever supermodularized
for fixed would collapse Theorem 2.8.2's genuinely joint hypothesis into
a restatement of Theorem 2.8.1, which is exactly the trivialization this mission's chunk
brief warns against. is written out as the set
of that dominate every other element of under , and every
conclusion is stated only for pairs at which both argmax sets are assumed
nonempty — matching the book's own restriction to , since holds
vacuously whenever either side is empty. This mission depends on chunk I's
InducedSetOrder; it introduces no reusable infrastructure beyond its own three
definitions, which later missions in the series (matching, MDPs, supermodular games) are
expected to import directly rather than redefine.
This mission formalizes §4 of Cannon, Floyd and Parry's Introductory notes on Richard Thompson's groups, together with the definition of Thompson's group from their §1. The goal is their Theorem 4.5: the commutator subgroup is simple.
In the 1960s Richard Thompson defined three groups, now written , and , whose properties have kept them in use ever since as a source of examples at the edge of what groups can do. is the smallest of the three and the least understood. It is finitely presented (§3 of the source) and torsion-free, it has no free subgroup of rank two, and whether it is amenable — whether it carries a finitely additive left-invariant probability measure defined on all its subsets — is open. Cannon, Floyd and Parry record (§4, p. 227) that Geoghegan raised the question and conjectured in 1979 both that contains no non-Abelian free subgroup and that is not amenable.
That question is what makes worth pinning down precisely. Write for the class of
amenable discrete groups, for the elementary amenable ones, and for the groups with
no free subgroup of rank two. That was noted by
Day and follows from
von Neumann; whether it is strict is the von
Neumann–Day problem. It is: Olshanskii proved in a 1984 ICM address and
Gromov gave an independent proof — but by
examples that are not finitely presented. Brin and Squier proved in 1985 that , and
is not elementary amenable (Theorem 4.10 of the source, CannonFloydParry.not_elementaryAmenable_F). So
is a finitely presented group in if it is amenable and in
if it is not — a question with no other finitely presented candidate.
Call a real number dyadic if it has the form with and .
Thompson's group , as §1 of the source defines it, is the set of piecewise linear homeomorphisms of the closed unit interval onto itself that are differentiable except at finitely many dyadic rationals, and whose derivatives, where they exist, are powers of . Since those derivatives are positive, every element preserves orientation, so the elements of are increasing. Composition of two such maps is again one, and so is the inverse of one, so is a group.
The formalization calls such a map piecewise linear over the dyadics, and defines as the subgroup generated by those maps — so that closure under composition and inverses is a theorem rather than part of the construction, as the source has it. What the model fixes rather than derives is under Formalization scope below.
Two particular elements generate it. Write
An element of is trivial near if it fixes every point of some interval , and trivial near if it fixes every point of some . The support of is the set of points of that moves. The commutator convention throughout is , and denotes the commutator subgroup.
This is the capstone of §4: it says the commutator subgroup has no normal subgroup other than itself and the trivial one. It is the goal because the rest of the section feeds it — both halves of Theorem 4.1, Theorem 4.3, and both supporting lemmas below are consumed by its proof.
So has no interesting proper quotients at all. With the first part of Theorem 4.1 this forces every nontrivial normal subgroup of to contain .
That the piecewise-linear maps are already closed under composition and inverses, so that consists of exactly those maps; a transitivity lemma on dyadic partitions of ; the fact that the subgroup of elements supported in a dyadic interval of dyadic length is isomorphic to itself; triviality of the center; that contains no non-Abelian free group; and that admits a total order invariant under multiplication on both sides.
What the results give. Theorem 4.1 identifies concretely — a subgroup defined by a global algebraic condition turns out to be cut out by local behavior at the two endpoints — and computes the abelianization, making the pair of endpoint slopes a complete invariant of modulo commutators. Theorem 4.3 and the simplicity of together determine the whole normal subgroup lattice: every normal subgroup of is trivial or contains . That lattice is the input to the elementary-amenability argument.
What formalizing adds. All of these are proved in the source; none is in Mathlib, which has no piecewise-linear homeomorphism API and no Thompson group. Four of the milestones are proved as part of this proposal: that the piecewise-linear maps form a subgroup, that elements of permute the dyadic rationals, that embeds in the group Brin and Squier work with, and the absence of a free subgroup of rank two, which follows from the already-formalized Brin–Squier theorem via that embedding. The rest are open. The piecewise-linear machinery built along the way — local affineness, dyadic-breakpoint bookkeeping, extension by the identity — is reusable for , for , and for the wider family of piecewise-linear homeomorphism groups.
The obvious approach to the goal is to argue that a normal subgroup of containing a nontrivial element must be everything, by conjugating that element around. It fails on its own: an element of is pinned down only by being trivial near the two endpoints, and one still has to manufacture — inside , not merely inside — an element carrying a prescribed pair of neighborhoods into those. That construction is what the dyadic-partition transitivity lemma supplies, and it is where the combinatorics of dyadic subdivision enters.
The second difficulty was that the source proves §4 using the tree-diagram normal form of §2.
That section is now formalized in its own mission, Cannon–Floyd–Parry §2: tree diagrams and the
normal form (mission ffd1e4ea-9f9a-4cb6-8419-78e70f2545e8), all of whose milestones are proved.
Corollary 2.6 — milestone 5 here, the same theorem object — is closed from there, and Theorem
2.5 (represents_word_exponents) and the normal form (existsUnique_normalForm) are available to
a solver attacking Theorem 4.3, so the source's argument can now be followed. A solution file
imports only definitions, so whatever it uses from §2 must be reproved inline; the §2 solutions
are public and written to be reused that way. The piecewise-linear route — dyadic-partition
transitivity, Lemma 4.4 and Theorem 4.1 — remains an alternative, and is what Theorem 4.5's own
argument uses.
The unit interval is as a subtype, and an element of is an order isomorphism of it, so orientation preservation is built into the representation rather than derived — faithful to the source's set, but assuming one sentence CFP prove. Piecewise linearity is stated as: there is a finite set of dyadic reals such that the map is affine, with slope a power of two, on every closed interval whose interior misses . Intercepts are not required to be dyadic — that is derived by induction along the breakpoints, not part of the definition.
The definition is not vacuous: and of Example 1.1 are constructed explicitly, and that is not the trivial group is one of the milestones below — so no statement here is satisfied by the trivial group. In particular the goal, which asserts simplicity and therefore nontriviality, is not trivially false.
A companion definition places the same data on the real line, each element extended by the identity outside ; that line realisation is what the bridge statement connects to Brin and Squier's group.
Before any geometry of surfaces can be done, one has to say what a surface is, in a way that supports calculus: a subset of that is locally the smooth, non-degenerate image of an open piece of the plane. Every statement in the later theory — the first and second fundamental forms, the Gauss map, curvature, geodesics — is written in local coordinates, and is therefore meaningful only once one knows that the answer does not depend on the coordinates chosen. That independence is the content of the change-of-parameters theorem, which is what makes "differentiable function on a surface" and "geometric quantity of a surface" well-defined notions.
The reference for this mission is Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition (Dover, 2016), §2-2 "Regular Surfaces; Inverse Images of Regular Values" (pp. 54–71) and §2-3 "Change of Parameters; Differentiable Functions on Surfaces" (pp. 72–85): Definition 1 (p. 54), Propositions 1–4 of §2-2 (pp. 59, 61, 63, 65) and Proposition 1 of §2-3 (p. 74).
This is the fourth mission of a series formalizing do Carmo's book, sharing the namespace
DoCarmoDG with the others.
A subset is a regular surface when every has an open neighbourhood such that is the image of a map , defined on an open set , satisfying the three conditions of do Carmo's Definition 1:
Such an is a parametrization, or system of local coordinates, and is a coordinate neighbourhood.
Given a differentiable on an open set , a value is a regular value of when is surjective — equivalently, nonzero — at every with (do Carmo Definition 2, §2-2).
If and are two parametrizations of a regular surface with , then
is a diffeomorphism: is differentiable, bijective, and is differentiable.
The graph of a differentiable function of two variables is a regular surface (Proposition 1); the inverse image of a regular value is a regular surface (Proposition 2); a regular surface is locally the graph of a differentiable function of one of the three coordinate pairs (Proposition 3); and an injective map satisfying conditions 1 and 3 whose image lies in a regular surface automatically has a continuous inverse (Proposition 4).
Proposition 2 is the practical criterion: it is what shows in one line that spheres, ellipsoids, tori and the level sets of generic polynomials are regular surfaces, and it is applied throughout the book. Proposition 3 is the structural statement that a regular surface is locally a graph, which is the form in which most local computations are carried out; Proposition 4 removes the awkward homeomorphism clause from the verification of examples. The change-of-parameters theorem is what allows every subsequent definition — differentiable function on a surface, tangent plane, first fundamental form, curvature — to be given in coordinates and then shown to be independent of them, and it is also the reason a regular surface carries a smooth structure at all.
Mathlib has smooth manifolds, the implicit and inverse function theorems, and ContDiffOn, but it
does not contain do Carmo's concrete definition of a regular surface as a subset of
or these four propositions about it. Establishing them is what allows the rest of this series to
work with patches while knowing that the objects so defined are coordinate-independent.
Everything here rests on the inverse function theorem, but each proposition needs it in a slightly different form. Proposition 2 requires completing to a local diffeomorphism and reading off the level set — with the complication that which partial derivative is nonzero varies from point to point, so the coordinate that is solved for is not fixed in advance. Proposition 3 needs the same case distinction on which Jacobian minor of is nonzero, and this is exactly why the conclusion is a disjunction over the three coordinate pairs. Proposition 4 is where the homeomorphism condition is shown to be redundant, and the argument goes through the local factorization .
The change-of-parameters theorem is not a direct application of the inverse function theorem to : the map is defined only on a subset of the plane and is, a priori, merely continuous. One first extends to a local diffeomorphism of a neighbourhood in and then composes; the continuity of (condition 2 of Definition 1) is what makes the domain of open, and it cannot be dispensed with.
A surface is a set S : Set (EuclideanSpace ℝ (Fin 3)), and a parametrization is a map
x : ℝ × ℝ → EuclideanSpace ℝ (Fin 3) together with an open U : Set (ℝ × ℝ). Smoothness is
ContDiffOn ℝ (⊤ : ℕ∞), matching do Carmo's "differentiable" for ; regularity is
injectivity of the Fréchet derivative at each point of U, which is do Carmo's condition 3; and
the homeomorphism condition is stated as injectivity on U together with the existence of a
continuous left inverse on the image, which is the content of "the inverse is continuous". The
neighbourhood clause of Definition 1 is x '' U = V ∩ S for an open V containing the point.
Graphs are formalized as three separate sets, one for each of , and
, so that Proposition 3 can state its disjunction faithfully; in that statement the
neighbourhood is an open set W of and the claim is W ∩ S = W ∩ graph.
The goal states the diffeomorphism property of explicitly — two maps, mutually inverse on the
relevant domains, both ContDiffOn, together with the openness of those domains — rather than
through a bundled structure, so that no library convention is assumed. There is no trivializing
reading: the domains are those forced by the two parametrizations, and in the degenerate case
where the images do not overlap the statement reduces to a true but empty claim about the empty
set, while the substance is in the overlapping case.
The local theory of curves describes what happens near one point; the global theory asks what a curve must satisfy because it closes up. Two classical statements make the difference visible. The isoperimetric inequality says that among all simple closed plane curves of a given length, the circle encloses the largest area — a question already settled in intent by the Greeks, but given a satisfactory proof only in the nineteenth century, and the short proof reproduced by do Carmo is E. Schmidt's from 1939. The four-vertex theorem says that the curvature of a simple closed convex curve has at least four critical points, so no convex oval has the curvature profile of a curve that just rises and falls once.
The reference for this mission is Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition (Dover, 2016), §1-7, "Global Properties of Plane Curves" (pp. 31–46): the area formula, equation (1) on p. 33; the isoperimetric inequality, Theorem 1 on p. 34; the theorem of turning tangents on p. 37; the lemma, equation (5) on p. 38; and the four-vertex theorem, Theorem 2 on p. 37.
This is the third mission of a series formalizing do Carmo's book, and shares the namespace
DoCarmoDG with the earlier ones.
A closed plane curve of length is a regular map whose derivatives of all orders agree at the two endpoints; equivalently, and as used here, a smooth -periodic map . It is parametrized by arc length when for all , in which case is its length. It is simple when it has no self-intersection: for distinct .
Write for rotation by , . For a curve parametrized by arc length the signed curvature is
which is do Carmo's convention of §1-5, Remark 1: the normal is chosen so that has the orientation of the natural basis, and then . A vertex is a parameter with . The curve is convex when, for every parameter , the whole trace lies in one of the two closed half-planes bounded by the tangent line at .
An angle function for is a smooth with ; the rotation index is . The area bounded by a positively oriented simple closed curve is given by do Carmo's equation (1),
The three equivalent forms of the area formula (1); the existence of a smooth angle function; the identity ; the theorem of turning tangents (the rotation index of a simple closed curve is ); the isoperimetric inequality with equality exactly for circles; and do Carmo's lemma (5), , which drives the proof of the goal.
The isoperimetric inequality is the ancestor of a large family of geometric inequalities, and its sharp case characterizes the circle — the first instance of the pattern "extremal configuration is the round one" that recurs throughout geometry. The four-vertex theorem is a genuinely global statement with no local counterpart: locally, the curvature of a convex arc may be strictly monotone, and it is only the requirement that the curve close up convexly that forces four critical points. Its converse, for strictly positive curvature, was proved by H. Gluck in 1971; do Carmo notes that the theorem also holds for simple closed curves that are not convex, by a harder argument.
Mathlib contains integration, the winding number of a loop in the complex plane and the Jordan curve theorem, but it does not contain the signed curvature of a plane curve, the theorem of turning tangents in this form, the isoperimetric inequality for curves with its equality case, or the four-vertex theorem. What this mission adds is that vocabulary and machine-checked proofs of the four classical statements.
Each target fails for a different reason under the naive approach.
For the area formula, the identification of with the area of the interior is exactly the Jordan-curve input that do Carmo declares he is assuming; the formalization avoids that dependency by defining the bounded area through the integral, so a solver has to prove only the integration-by-parts identities among the three forms of (1).
For the theorem of turning tangents, the difficulty is that a smooth lift of the tangent indicatrix must be produced and then shown to increase by exactly over one period — a degree-theoretic statement about a loop in the circle, where simplicity of the curve is what excludes the values .
For the isoperimetric inequality, Schmidt's proof compares the curve with a circle tangent to two parallel supporting lines and uses the arithmetic–geometric mean inequality; the equality discussion, which is where the characterization of the circle lives, is the delicate part.
For the four-vertex theorem, the obvious argument — "curvature on a compact interval attains a maximum and a minimum, so there are two vertices" — gives only two, and the whole content is the step from two to four. The lemma (5) supplies the contradiction: if changed sign only at the maximum and the minimum, a suitable line through those two points would make the integrand of (5) of one sign and not identically zero.
Curves are smooth maps ℝ → EuclideanSpace ℝ (Fin 2), closedness being -periodicity with
, which is do Carmo's condition that the curve and all its derivatives agree at the
endpoints. Unit speed is imposed globally, so the parameter is arc length and is the length.
Simplicity is injectivity on the half-open period . Convexity is stated per parameter: for
each the trace lies in one closed half-plane of the tangent line at , the choice of side
being allowed to depend on , as in the book's phrasing.
The area is defined by do Carmo's integral (1) rather than as the measure of the interior of the curve, so no Jordan curve theorem is presupposed; consequently the isoperimetric statement is formulated with the absolute value , which makes it independent of the curve's orientation and equal to the enclosed area for a positively oriented simple curve. The equality case asserts that the trace lies on a circle of positive radius.
"At least four vertices" is formalized as the existence of four pairwise distinct parameters in at which vanishes, which rules out the degenerate reading in which one vertex is counted several times.
Until 1827 the curvature of a surface in space was understood as a statement about how the surface sits inside : it was computed from the way the unit normal turns, that is, from the second fundamental form. Gauss's Disquisitiones generales circa superficies curvas showed that one particular combination of those extrinsic quantities — the product of the principal curvatures — can be recomputed from measurements made entirely inside the surface, using only lengths of curves drawn on it. This is the Theorema Egregium, and it is the reason the subject splits into extrinsic and intrinsic geometry; the latter is what becomes Riemannian geometry.
The reference for this mission is Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition (Dover, 2016), §4-3, "The Gauss Theorem and the Equations of Compatibility" (pp. 235–240). The theorem is stated on page 237 and derived from the Gauss formula, equation (5) of that section; the Mainardi–Codazzi equations (6) and (6a) on page 238 complete the list of compatibility equations.
This is the second mission of a series formalizing do Carmo's book; it shares the namespace
DoCarmoDG with the first, on the local theory of curves.
A regular parametrized patch is a map , defined and smooth on an open set with coordinates , whose partial derivatives satisfy at every point of ; the last condition says that is injective, so spans a -dimensional tangent plane at each point and
is a unit normal field along the patch.
The first fundamental form is the restriction of the ambient inner product to the tangent plane; in the parametrization it is recorded by the three functions
and . The second fundamental form is recorded by
and the Gaussian curvature is
The three second derivatives decompose in the basis ; the tangential coefficients are the Christoffel symbols of the patch, and the normal coefficients are , , , which is do Carmo's system (1) of §4-3:
Two patches over the same parameter domain are isometric when their first fundamental forms coincide, , , at every point: lengths of curves, angles and areas computed in the parameter domain then agree, and a local isometry between the two surfaces is obtained by matching parameters.
The Gaussian curvature of a regular patch is determined by its first fundamental form alone, although its definition uses the second fundamental form, i.e. the position of the surface in space.
The existence and uniqueness of the Christoffel symbols; the linear system (2) expressing them through and their first derivatives; the Gauss formula (5),
the Mainardi–Codazzi equations (6) and (6a); the closed formula for in an orthogonal parametrization (Exercise 1, p. 240); the invariance of under a change of parameters; and, as a corollary, that no neighbourhood of a point of the unit sphere is isometric to a piece of a plane (Exercise 4, p. 240).
The theorem is what makes intrinsic geometry possible: a quantity defined through the embedding turns out to be computable from the metric, so it survives every isometric deformation. Concrete consequences include the impossibility of a distortion-free map of the sphere — the reason every cartographic projection distorts lengths — and the equality of the Gaussian curvatures of the catenoid and the helicoid at corresponding points, which do Carmo notes immediately after the theorem. In the structure of the book, the Gauss formula is also the identity that makes the global Gauss–Bonnet theorem of §4-5 a statement about intrinsic data.
Mathlib has inner product spaces, iterated derivatives and the smooth manifold library, but it does not contain the first and second fundamental forms of a parametrized surface, the Christoffel symbols of a patch, the Gaussian curvature in this sense, or the compatibility equations. This mission produces that vocabulary together with machine-checked proofs of the classical identities. The mathematics is Gauss's, from 1827; what is open is the formalization.
The proof is a computation, but not a short one: one differentiates the system (1), uses , re-expands every second derivative through (1) again, and equates coefficients in the basis . Formally, the cost sits in three places: justifying the interchange of the mixed partial derivatives; establishing that the coefficient functions obtained pointwise from linear algebra are differentiable in the parameters; and carrying out the coefficient comparison in a basis that is not orthonormal, where one must use that rather than take inner products with an orthonormal frame.
The naive route to the Theorema Egregium — "solve the system (2) for the , then quote the Gauss formula" — is the right one, but the first step must actually be carried out: the system (2) determines the symbols only because each of its three blocks has determinant , and that is where the regularity hypothesis is used.
A patch is a curried map x : ℝ → ℝ → EuclideanSpace ℝ (Fin 3), so that the partial derivatives
and are ordinary one-variable derivatives, and the domain is an open set
U : Set (ℝ × ℝ); smoothness is ContDiffOn ℝ (⊤ : ℕ∞) of the uncurried map on U, matching
do Carmo's use of "differentiable" for . Regularity is stated as
on U, with the vector product defined componentwise. All quantities
(, , , , , , , ) are total functions of the parameters, taking junk
values off U; every statement restricts to points of U.
Christoffel symbols are not defined by a formula: a statement that mentions them quantifies over
functions assumed to satisfy do Carmo's decomposition (1) on U, and a separate
milestone asserts that such functions exist and are unique on U. The symmetry
is built into the notation, as in the book.
Isometry is formalized as equality of , , over a common parameter domain rather than as a map between surfaces; together with the milestone on invariance under change of parameters, this recovers do Carmo's statement that is invariant under local isometries. The formalization deliberately keeps the surface concrete (a patch, not an abstract manifold), which is what makes the compatibility equations expressible as identities between explicit derivatives.
This mission's definition file builds on the vector-product definition introduced in mission I of this series (Fundamental Theorem of the Local Theory of Curves), so mission I must be submitted first: its definitions have to be published before the definition file of this mission can compile.
There is no vacuous reading: the hypotheses are satisfiable — every regular patch, for instance a graph or a surface of revolution, satisfies them — and the conclusion compares two curvature functions pointwise.