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?
Many problems in optimization and equilibrium modelling reduce to a system of equations whose map is Lipschitz but not differentiable: reformulations of nonlinear complementarity problems through the componentwise minimum or the Fischer–Burmeister function, Karush–Kuhn–Tucker systems of constrained programs, and gradients of augmented Lagrangians all have kinks. Newton's method, , is the standard fast local solver for smooth systems, but it needs a derivative at every iterate.
Qi and Sun (Math. Programming 58, 1993) replaced the Jacobian by an arbitrary element of Clarke's generalized Jacobian and showed that the resulting method converges locally superlinearly under a regularity condition they called semismoothness, extending Mifflin's notion for functionals (Mifflin, SIAM J. Control Optim. 15, 1977) to vector-valued maps. This theorem is the foundation of the family of semismooth Newton methods used in complementarity, variational inequalities and PDE-constrained optimization.
Timeline. Robinson (1988) and Pang (Math. OR 15, 1990) studied Newton methods built on B-derivatives, with convergence proved under a strong Fréchet derivative at the solution; Kummer (1988) gave an abstract framework for Newton methods for nonsmooth equations; Qi and Sun (1993) proved local superlinear convergence for the generalized-Jacobian iteration under semismoothness and nonsingularity of , with order under -order semismoothness.
Let be locally Lipschitz. By Rademacher's theorem is differentiable on a set of full measure; write for the Jacobian at . The generalized Jacobian is
the convex hull of all limits of Jacobians along sequences of differentiability points converging to . The one-sided directional derivative is .
is semismooth at if it is Lipschitz near and, for every , the limit of over , , exists. For , is -order semismooth at if in addition for , .
For , the nonsmooth Newton method is
where any element of may be chosen at each step. A run is a pair of sequences , with and for all . A root () is regular when every is nonsingular.
Let be locally Lipschitz, , semismooth at , and every nonsingular. Then there is such that every with is nonsingular, a Newton step from such a stays within of , and every run with satisfies
The goal asserts only the shape of the convergence (superlinear) and fixes no constants.
If moreover is -order semismooth at , , there are and with
for every run started within of .
The milestones follow the paper's route: Proposition 2.1 (the limit in the definition of semismoothness is the directional derivative), Lemma 2.2 (Lipschitz continuity of and its realisation by an element of ), Theorem 2.3 (semismoothness is equivalent to and to the corresponding condition at differentiability points), the Remark's expansion (2.17), Proposition 3.1 (uniform invertibility near a regular point), the order- sentence of Theorem 3.2, and Corollary 2.5 (strong Fréchet differentiability implies semismoothness).
The theorem gives a locally superlinearly convergent method for Lipschitz equations with no smoothness beyond semismoothness at the root. Convex, smooth and subsmooth functions are semismooth, as are sums and scalar products of semismooth functions (the paper, citing Mifflin), and later work showed that the complementarity and KKT reformulations on which semismooth Newton solvers are built are semismooth as well; the order- variant gives local quadratic convergence for strongly semismooth maps. Mission II of this series treats the paper's global convergence theorem on a ball, and Mission III the semismoothness of augmented Lagrangian gradients, which supplies the application.
The results are proved in the paper. No machine-checked version of the generalized Jacobian, of semismoothness or of the nonsmooth Newton method is known to exist in Mathlib or on this platform; the platform's formalized Newton results concern one-dimensional functions (MetodosNumericos.newton_local_convergence) and smooth convex minimization. A complete development would provide the first formal library for Clarke's generalized Jacobian and semismooth maps.
The classical Newton proof compares with its linearization and uses continuity of the Jacobian at . Here neither is available: need not be differentiable at or at any iterate, the element is chosen arbitrarily from a set, and need not be close to any fixed linear map. The comparison has to go through the directional derivative , which is only positively homogeneous, not linear. The analytic content therefore sits in Section 2: showing that semismoothness, defined through a limit over a set-valued map, controls uniformly in the direction, and that is small. Both rest on Clarke's mean-value inclusion and on compactness and upper semicontinuity of , none of which is in Mathlib. The superlinear rate also requires a uniform bound on in a whole neighbourhood, not just at .
Everything lives in the namespace NonsmoothNewton.Local. Section 2 results are stated for maps between finite-dimensional real normed spaces (the paper's is the Euclidean instance); Section 3 results use EuclideanSpace ℝ (Fin n). Conventions fixed by the Lean statements:
fderiv; the generalized Jacobian is the convex hull (no closure) of limits of fderiv along sequences of differentiability points.lineDeriv; its value is a limUnder, used only where existence is a hypothesis or a consequence.IsUnit in the ring of continuous linear endomorphisms; is a two-sided inverse of operator norm at most .IsLittleO along atTop; the printed Theorem 3.2 states only well-definedness and convergence. "Order " is pinned as with and uniform over runs. Every in (2.8), (2.9) and (2.17) is its – form with a non-strict inequality , and every is an explicit constant and radius.HasStrictFDerivAt, which corrects the misprint for in the paper's display (2.16).A trivializing formalization is ruled out: the update is not written with a junk inverse (which would make a singular step "well defined"), the generalized Jacobian is the paper's nonempty set rather than one that could be empty, and the theorem quantifies over every run rather than asserting that some run converges.
A complete development needs Clarke's mean-value inclusion (2.2), compactness and upper semicontinuity of for locally Lipschitz maps (via Rademacher's theorem, available in Mathlib), and perturbation bounds for inverses of linear maps. The generalized-Jacobian and semismoothness layer is reusable beyond this mission, in particular for Missions II and III of this series. Contributions of proofs of any milestone, and of general lemmas about , are welcome.
Connecting a set of terminals by a network of direct links of least total length is one of the oldest problems of combinatorial optimization. R. C. Prim's 1957 paper in the Bell System Technical Journal (DOI) was motivated by the rate structure for Bell System leased-line services, in which the charge for connecting a set of terminals depends on the length of a shortest network connecting them. The paper states two local construction principles, P1 and P2, and shows that any sequence of their applications produces a shortest network, first for points in the plane and then for arbitrary connected labelled graphs with arbitrary real edge lengths. The paper's §V specialization of the principles, growing a single fragment, is what is now called Prim's algorithm, and its §IV statement is the form of the minimum spanning tree theorem used throughout network design, clustering and approximation algorithms.
Timeline. O. Borůvka (1926) solved the problem for an electrical network in Moravia; V. Jarník (1930) gave the single-fragment procedure; J. B. Kruskal (1956, Proc. AMS 7, 48–50) proved that adding globally shortest links avoiding cycles yields a shortest spanning tree; Prim (1957) gave the more permissive principles P1 and P2, which contain both the Jarník procedure and Kruskal's rule as special orders of application; E. W. Dijkstra (1959) rediscovered the single-fragment procedure.
Let be a finite set of terminals and a simple graph on , the labelled graph whose edges are the possible links. Each edge carries a real length ; lengths may be negative, zero, or tie. For a finite set of links, denotes the graph on whose edges are the links of .
Only edges of are possible links; in Prim's distance table a missing edge has length .
For every finite connected graph and every ,
This is the sentence "P1 and P2 will provide a SSS for any connected labelled graph with any set of real edge lengths." It fixes nothing about the order of applications, the component chosen, or the tie-breaking.
The goal is the correctness theorem of a whole family of greedy minimum spanning tree procedures at once: Jarník–Prim (one growing fragment), Kruskal (globally shortest link first) and Borůvka-style interleavings all produce sequences of P1/P2 applications. Because lengths are arbitrary reals, it also covers maximum spanning trees by a sign change (p. 1397) and graphs that are not complete.
The result is classical and fully proved in the literature. What this mission adds is a machine-checked statement in exactly Prim's generality. Mathlib has spanning trees of connected graphs (SimpleGraph.Connected.exists_isTree_le) and the edge count of trees, but no minimum spanning tree theory. Existing Prove2Me items on minimum spanning trees are either restricted to complete graphs with distance matrices or state a cut property in existence form at a single vertex; none states Prim's principles or his necessary conditions.
The obvious argument, "each link P1 or P2 adds belongs to the shortest network", uses a unique shortest network, and that fails with ties: when two links tie, a P1/P2 link need not lie in a given SSS. Prim's own treatment of ties (§III) is an informal perturbation argument; the formal statement must hold for every tie-breaking choice made during a construction, not only for a generic perturbed instance. Negative lengths remove the easy reading "shortest connected spanning subgraph": the minimum must range over trees only. The statements also involve the component structure of as it changes during a construction, and tree paths in an arbitrary, not necessarily complete, graph.
Namespace ShortestConnection.Principles, Mathlib SimpleGraph. Conventions:
Fintype with decidable equality; is a SimpleGraph V (at most one link per pair, no loops, which is Prim's setting). Lengths are w : Sym2 V → ℝ; only values on edges of matter.Finset (Sym2 V); linkGraph F is SimpleGraph.fromEdgeSet F. A spanning subtree requires ↑F ⊆ G.edgeSet and (linkGraph F).IsTree.linkGraph F; the P2 condition is a single inequality against every -edge leaving it, which is equivalent to "nearest neighbor and shortest link" in Prim's sense.List (Sym2 V) checked entrywise against l.take i; complete means length Fintype.card V - 1 (natural subtraction, used only for nonempty ).sInf of the lengths of spanning subtrees; continuity is in the product topology.Implicit hypotheses made explicit: connected (hence ) wherever an SSS or a complete construction is involved; at least two terminals for Necessary Condition 1; nonempty and for Necessary Condition 2; pairwise distinct edge lengths only in milestone 4, as in the paper's temporary assumption.
The goal's existence clause rules out a vacuous formalization in which no complete construction exists; the step predicates are defined from lengths and components only, never through shortest spanning subtrees, and they are not restricted to one growing fragment or to the globally shortest link.
Needed infrastructure: tree exchange (adding an edge to a spanning tree creates one cycle; removing any other cycle edge yields a spanning tree), component counts under edge addition, and minima of finitely many continuous functions. The exchange and counting lemmas are reusable for any matroid-greedy or spanning-tree mission. Contributions of intermediate lemmas, and proofs of the milestones in any order, are welcome.
Quasi-Newton methods minimize a smooth function on by moving along , where is the gradient and is an approximation of the inverse Hessian built from observed gradient differences. The BFGS update is the most widely used way of building , but it stores a dense matrix, which is prohibitive for large .
Nocedal's 1980 paper (Math. Comp. 35, 773–782) proposed keeping only the last correction pairs and rebuilding the matrix from a simple initial matrix at every step. The resulting method, called SQN in the paper, is now known as L-BFGS, and it is the default large-scale unconstrained optimizer in many numerical libraries and in machine learning. The paper's main theoretical claim is that this truncation does not destroy the finite termination of BFGS on quadratics.
Timeline:
Let be a symmetric positive definite matrix and , and let , a strictly convex quadratic with gradient and unique minimizer .
Exact line search. Along a direction from , the step minimizes .
BFGS update. For a pair with and , the BFGS update of is
Special BFGS matrices. Fix symmetric positive definite and a number of stored corrections. Given pairs , the special matrix is updated by the pairs , oldest first (the paper's (4)–(5)). Only the most recent pairs enter, and the matrix is rebuilt from .
SQN. Starting from , with :
with the exact step and the special matrix built from the last pairs.
PCG with fixed preconditioner . , , with .
For every , every symmetric positive definite and , every , and every ,
where are the SQN iterates. The statement fixes no constant beyond the dimension bound .
The result shows that storing only correction pairs costs nothing on quadratics: for any , SQN terminates in at most steps, like full BFGS and conjugate gradients. It explains why L-BFGS with small is competitive, and it is the model case for later analyses of limited-memory methods (their linear convergence on uniformly convex functions, and their relation to Krylov methods). Property (b) is the reason one expects efficiency to grow with : the matrix satisfies the secant equation on the most recent directions.
The claims are classical and generally accepted, but the paper argues them in a few lines ("it is straightforward to show"), deferring the PCG facts (15)–(16) to a reference. No machine-checked proof of the termination of BFGS, L-BFGS or preconditioned conjugate gradients is known to this mission. A formalization would provide a verified model of L-BFGS on quadratics and a reusable development of conjugate-direction methods with a preconditioner.
The obvious route, "SQN is BFGS and BFGS terminates", fails: SQN discards old corrections, so the classical BFGS argument (hereditary secant conditions on all past directions) does not apply once more than steps have been taken. The paper asserts the identity of SQN with preconditioned conjugate gradients in one sentence ("using a similar argument as for the SCG"), and the PCG relations it relies on are quoted from a technical report. The other difficulty is bookkeeping: the window of stored pairs shifts, the matrix is a nested product, and the runs must remain meaningful after the minimizer is reached.
Vectors are Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, is dotProduct, and is Matrix.vecMulVec. Symmetric positive definiteness is Matrix.PosDef. Indices are 0-based, as in the paper. The exact line search is the closed-form step . The iterations have no stopping rule: once the gradient vanishes the direction and step are zero and the iterate stays at the minimizer (Lean's ). Past that point the zero pair stored by SQN leaves the BFGS step unchanged. The hypotheses are exactly the paper's: , , and exact line searches. need not be diagonal.
Two misprints are corrected and flagged in the items: the denominator of in (13) is (as in (12) and p. 778), and the second relation of (16) is stated for (as used on p. 778), since it fails for .
Ruled out: SQN is defined through its own matrices (4)–(5), rebuilt from and the last pairs. It is not defined through the PCG recurrence, not by one BFGS update of the previous matrix, and not with a stop rule that returns . The standing assumption is not a hypothesis of any statement about a run (it fails after termination and would make the goal vacuous). With SQN is steepest descent and the goal is false, so is required.
Needed infrastructure: algebra of rank-one updates and of Matrix.PosDef under congruence, conjugate-direction lemmas for quadratics, and the fact that mutually -orthogonal vectors in include a zero vector. The PCG results (milestones 5–7) are reusable beyond this mission. Proofs of any milestone, or of the goal directly, are welcome.
Newton's method is the standard second-order algorithm for unconstrained minimization, but without safeguards it has no global guarantee: far from a minimizer the Newton step can increase the objective, and at a point where the Hessian is indefinite the step can head for a saddle point or a maximum. The usual repairs (line search, trust regions, Levenberg–Marquardt damping) come with convergence proofs, but for nonconvex objectives those proofs typically give no rate at all, or only the rate of the gradient method.
Nesterov and Polyak (Math. Program. 108 (2006) 177–205) proposed to regularize the second-order Taylor model of the objective with a cubic term and to take as the next iterate a global minimizer of the regularized model. They showed that the resulting method has a global worst-case rate of convergence to points satisfying the second-order necessary conditions, for every objective with a Lipschitz continuous Hessian and without any convexity. That rate, for the gradient norm, is better than the of the gradient method. It became the reference point for the complexity theory of nonconvex second-order optimization: adaptive variants (Cartis, Gould and Toint, Math. Program. 127 (2011) 245–295) and lower bounds showing that iterations are optimal among second-order methods (Carmon, Duchi, Hinder and Sidford, Math. Program. 184 (2020) 71–120) are stated against it.
This mission formalizes the general convergence result of that paper, Theorem 1 of Section 3, together with the properties of the cubic step from Section 2 on which it rests.
Let be a closed convex set with nonempty interior, and let be twice differentiable on with gradient and Hessian . A starting point is fixed, and is assumed to contain the level set in its interior. Assumption 1: the Hessian is Lipschitz continuous on in the spectral norm, for all , with .
For a parameter the cubic model of at is
The cubic-regularized Newton step is any global minimizer of over ; it exists because the model is continuous and coercive. Write and .
The cubic regularization of Newton method (3.3) fixes , starts at and, for , chooses such that , then sets . The choice always passes the test.
Write for the smallest eigenvalue of a symmetric matrix . The measure of local optimality is
It is nonnegative and vanishes exactly when and .
If for all , then every run of method (3.3) satisfies, for every ,
The constant and the exponent are the paper's; the statement holds for every admissible choice of the parameters and of the global minimizers .
Inequality (3.4) is a global, dimension-free complexity bound for reaching approximate second-order stationarity. It controls both the gradient norm, , and the most negative curvature, , along the best iterate, from a single scalar potential . The second claim of Theorem 1 gives the asymptotic counterpart: every limit point satisfies the second-order necessary conditions. Section 4 of the paper derives its faster rates for star-convex and gradient-dominated functions from the same Section 2 lemmas.
The result is proved on paper and widely cited; to our knowledge no machine-checked proof of it or of the Section 2 lemmas exists. A formalization adds a checked statement of the method with its exact constants, and reusable facts about global minimizers of cubic models (Proposition 1 in particular) that the companion missions on star-convex, gradient-dominated and locally quadratic convergence also rely on.
Most steps are short inequalities, but two are not. Proposition 1 is a statement about a global minimizer of a nonconvex function: the first- and second-order conditions of a local minimizer give only , which is weaker. The natural first attempt, "take the second-order optimality condition of the model at ", therefore fails. The paper proves it in Section 5.1 through a one-dimensional dual characterization of the minimizer.
The second is Lemma 2's second claim, used for (2.12): showing that stays in requires a boundary argument along the segment from to , since the Taylor bounds are only available inside . The remaining work is calculus in : the integral form of Taylor's theorem for the gradient under a Lipschitz Hessian, and eigenvalue perturbation for the second entry of .
The space is EuclideanSpace ℝ (Fin n) for arbitrary n : ℕ. The gradient and Hessian are maps g and H with HasGradientAt f (g x) x and HasFDerivAt g (H x) x at every x ∈ F. At boundary points of this asks for two-sided derivatives, a mild strengthening of "twice differentiable on ". The Lipschitz condition uses the operator norm, which is the spectral norm. is represented by the predicate IsCubicStep (global minimizer of cubicModel), and every lemma is stated for every such minimizer. The run predicate IsCubicNewtonRun is 0-based. It writes as plus the model value at , which is the minimum because attains it. is lamMin, the Rayleigh-quotient infimum over the unit sphere, which equals the smallest eigenvalue for the (symmetric) Hessian. The lower bound is required on only. The minimum over is written as the existence of an index attaining the bound.
A stationary point of the cubic model is not an admissible step, and the run must keep the test and the acceptance test. Replacing the step by any point with makes the goal false, and dropping the square root in makes Lemma 5 false. The statements rule out all three. Lemma 5 carries the hypothesis , which its printed proof uses and which holds at every iterate.
A complete development needs the Taylor bounds (2.2)–(2.3) for vector-valued derivatives on convex sets, and first- and second-order optimality for the cubic model. It also needs a proof of Proposition 1 (Section 5.1 or any other correct argument) and eigenvalue perturbation via Rayleigh quotients. The cubic-model lemmas and Proposition 1 are reusable across the whole series. Proofs of any milestone, alternative proofs of Proposition 1, and general Mathlib-level lemmas about Rayleigh quotients are welcome.
A maximal independent set (MIS) of a graph is a set of vertices, no two adjacent, to which no further vertex can be added. Sequentially an MIS is found greedily in linear time, but the greedy scan is inherently serial. Whether an MIS can be found fast in parallel was a central question of parallel complexity in the early 1980s: an MIS algorithm is a subroutine for maximal matching, vertex colouring with colours, and many other symmetry-breaking tasks.
Luby's algorithm is the standard textbook example of a randomized parallel algorithm and remains the basis of distributed MIS algorithms in the LOCAL model. Its analysis rests on one statement, Theorem 1 of the paper, which this mission formalizes.
All algorithms in the paper run the same loop on a finite simple undirected input graph with vertices. The current graph is , initially . For the neighbourhood is . One execution of the loop body selects a set independent in , adds it to the output, and replaces by the subgraph induced on . The loop stops when is empty.
For write for its neighbours and for its degree. The two Monte Carlo select steps are:
Let be the number of edges of before the -th execution of the loop body. The number of edges eliminated by that execution is : exactly the edges of with at least one endpoint in . For the paper uses the weight .
For the current graph and ,
The constants are those printed in the paper. No connectivity, degree or size condition on is assumed.
Theorem 1 says that each round removes, in expectation, a constant fraction of the remaining edges. From it the paper derives that the expected number of rounds of either algorithm is , and hence that MIS has a Monte Carlo algorithm running in expected time on a CRCW P-RAM and on an EREW P-RAM with processors. Algorithm B and the proof of part (2) are also the basis of the paper's deterministic algorithm: the analysis of Lemma B uses only pairwise independence of the coins. The companion mission (A Simple Parallel Algorithm for the Maximal Independent Set Problem II) formalizes that derandomization and reuses the statements of milestones 2, 5 and 6.
The results are proved in the paper and reproduced in textbooks (e.g. Motwani and Raghavan, Randomized Algorithms), but not formalized: no statement of Theorem 1, Lemma A or Lemma B was found on the platform. A formal proof would make the per-round analysis of a standard parallel randomized algorithm reusable. That includes the degree-weighted counting of milestone 6 and the Bonferroni-type bound of the Technical Lemma, both of which recur in later analyses of distributed symmetry breaking.
The obvious argument tries to show that a fixed vertex enters with good probability. That fails, because a high-degree vertex rarely wins against all its neighbours. The analysis instead bounds the probability that a vertex is removed, i.e. lands in . This event is a union over neighbours of dependent events, so the first Bonferroni inequality alone does not give a lower bound: the pairwise-intersection terms must be controlled. The union bound can also be very lossy when is large, which is why the conclusion involves a minimum with a constant.
A second obstacle is the passage from vertices to edges: vertices of small can have high degree while contributing little probability. The per-vertex bounds therefore have to be summed with degree weights and redistributed over edges. For Algorithm A there is an additional complication: priorities from can collide, so the argument about a uniformly random order holds only on the event that is injective. That event appears as the factor .
SimpleGraph V on a finite type with decidable adjacency, and . The degree is SimpleGraph.degree, is neighborFinset, and is edgeFinset.card.Theorem 1 is false for arbitrary distributions of priorities or coins. A formalization that takes "Pr" as an unconstrained parameter, conditions on the event of interest, or replaces by does not state the paper's theorem.
A complete development needs finite product probability spaces, inclusion–exclusion (Bonferroni) inequalities for finite unions, the symmetry of uniform priorities conditioned on injectivity, and degree-sum identities (SimpleGraph.sum_degrees_eq_twice_card_edges). The Technical Lemma and milestones 5 and 6 are reusable beyond this mission. Proofs of any milestone, and alternative proofs of Lemmas A and B, are welcome.
The Critical-Path Method (CPM) was introduced by J. E. Kelley, Jr. (Remington Rand) and M. R. Walker (du Pont) in Critical-Path Planning and Scheduling (Proc. Eastern Joint Computer Conference, 1959, pp. 160–173, doi:10.1145/1460299.1460318). Together with PERT, developed at the same time for the Polaris programme, it became the standard way to plan and schedule large projects in construction, maintenance and engineering, and it is taught in every introductory operations research course.
The paper reduces project scheduling to arithmetic on a directed acyclic graph: the earliest and latest times of the project's events are computed by two recursions, and the jobs whose timing has no slack, the critical jobs, are singled out by an equation. Its central structural claim is that critical jobs, when they exist, form a path from the start of the project to its end. The paper states this without proof ("a detailed development being reserved for a separate paper", p. 161). This mission formalizes that claim and the facts about the two recursions on which it rests.
A project network has events labelled with : event is the origin and event the terminus. A job is an arrow from an event to an event , written job ; the jobs form a finite set of ordered pairs of events. Two standing assumptions of the paper (pp. 161–162) are part of the model:
Each job has a real duration . The earliest event times are given by display (1) of the paper,
and, for a project completion time , the latest event times by display (2),
The maximum time available for job is . The job is critical if this equals its duration, , and a floater if it exceeds it. A critical path is a contiguous path of critical jobs from origin to terminus: events with every a critical job of .
In the Lean development these are ProjectNetwork n (with field P), earliest N y, latest N y λ, maxTimeAvailable, IsCritical, IsFloater and IsCriticalPath, in the namespace CriticalPath.Events.
For every project network, durations and completion time ,
This is the paper's "A project will contain critical jobs only when . If a project does contain critical jobs, then it also contains at least one contiguous path of critical jobs through the project diagram from origin to terminus." Only the "only when" direction is asserted, as on the page.
The result. The theorem is what makes the method's name meaningful: it says that the jobs without slack are not scattered but line up along an origin–terminus path, and that such jobs exist only when the project is scheduled at its earliest possible completion time. Project managers use this to decide which jobs to watch, which to expedite, and which may slip; the delay statement (milestone 4) is the quantitative form of that advice. The characterisations of (1) and (2) as least and greatest feasible schedules are the bridge between CPM and linear programming: they identify and with extreme solutions of the system of difference constraints , which the paper's own §3 uses to build the project cost curve.
Formalizing it. The results are classical and folklore, but the paper proves none of them, and textbook treatments usually define the critical path as a longest path, which makes the goal a tautology. This mission states the claims with the paper's own definitions: criticality by the float equation, event times by the recursions. To the best of current knowledge no machine-checked version of these statements for activity-on-arrow networks exists; the platform has a related activity-on-node development (Brucker and Knust, Complex Scheduling) in which the critical path is defined as a longest path.
The recursions (1) and (2) are local: each event looks only at its immediate predecessors or successors. The goal is global: from one critical job it asserts a statement about the whole completion time and a whole origin–terminus path. The float equation mixes a quantity computed forward from the origin with one computed backward from the terminus, and neither recursion alone says anything about the other. The naive reading "a critical job lies on a longest path" is not available as a definition: it is, in substance, what has to be established from the recursions. The formal overhead is the well-founded recursion on the labels, in both directions, and the bookkeeping of lists of events forming a path.
Events are Fin (n + 1), origin 0, terminus Fin.last n, with 1 ≤ n. Jobs are a Finset of ordered pairs, so there is at most one job per ordered pair. The standing assumptions (labels increase along jobs; origin precedes and terminus follows every event, via Relation.ReflTransGen) are fields of the structure ProjectNetwork and are never dropped. Durations and times are real numbers; durations are a function Fin (n+1) → Fin (n+1) → ℝ read only on jobs of P, with no sign condition, as in the paper's deterministic case.
The event times are defined by the recursions (1) and (2) themselves, by well-founded recursion on the label with Finset.sup'/Finset.inf' over the predecessor/successor set; these sets are nonempty by the standing assumptions, so no fallback value exists. The latest times are defined for every real ; the paper's assumption is a hypothesis of every theorem that uses them.
Disclosed readings: "earliest time occurance" (milestone 1) and "latest time … relative to a fixed project completion time" (milestone 2) are read as least and greatest vectors satisfying the job constraints (the paper's constraint (8), p. 165); milestone 3 is the fact implicit in the dichotomy "critical or floater"; "comparable delay" (milestone 4) is read as an exact delay of in for .
A trivializing formalization is ruled out: defining a critical job or path through longest paths, or taking and as arbitrary functions satisfying (1) and (2), would make the goal a restatement of its definitions; here criticality is the float equation and the times are computed by the recursions. Dropping the reachability assumptions would make (2) ill-defined at events without successors.
Contributions welcome: proofs of the milestones, general lemmas on longest paths in finite labelled DAGs and on difference constraints , which are reusable for the companion mission on the project cost curve.
Many operational systems move between a finite number of states at random times: a machine alternates between working and repair, a queue between occupancy levels, an inventory between stock positions. When the time spent in a state is not exponential and not a fixed period, neither discrete-time Markov decision processes nor continuous-time Markov chains describe the system faithfully. William S. Jewell's 1963 paper Markov-Renewal Programming. I extends Howard's Markov decision processes to Markov-renewal processes (also called semi-Markov processes), in which the time between transitions is a random variable whose law depends on the current state, the next state, and the decision taken. The resulting model, now called a semi-Markov decision process, is standard in maintenance, queueing control and reliability.
Timeline:
A Markov-renewal program has a finite set of states (the paper's ) and a finite, nonempty set of alternatives (the paper's ), each available in every state. For each alternative and states it specifies:
The Laplace–Stieltjes transform is the expected discount over one interval. The average one-step return is , and for a vector of returns the test quantity is
A stationary policy is a map ; a nonstationary policy is a sequence of such maps, being used at the -th transition. The -step return of a policy, with boundary rewards , is the test quantity of applied to the -step return of the shifted policy; the optimal -step return of equation (6) replaces by a maximum over . The value-determination equations (15) of a stationary policy are .
The algorithm of Fig. 1 alternates two steps: solve (15) for the current policy, then in every state pick an alternative maximizing the test quantity, keeping the old alternative if it still attains the maximum. It stops when two successive policies are identical.
For every : (15) has a unique solution for every stationary policy, and every run of Fig. 1 reaches with , where
for every state and all boundary rewards, every limit existing. This is the paper's "the algorithm of Fig. 1 produces an optimal, stationary policy that is as good as any optimal, nonstationary policy".
The result says that the infinite-step discounted Markov-renewal program is solved exactly, in finitely many cycles, by a finite-dimensional algorithm, and that the answer is a stationary policy. As the paper notes, this matters operationally because a nonstationary policy is hard to follow. The sojourn distributions enter only through the numbers , so the same algorithm serves any sojourn-time law. For fixed the model is a discounted Markov decision process whose discount factor depends on the transition, which contains Howard's and Blackwell's constant-discount problem as the case of intervals of fixed length (p. 943).
The results are classical and proved in the literature. The paper itself refers the proofs to Howard and Blackwell. Machine-checked versions exist on this platform for finite stochastic shortest path and constant-discount problems (Bertsekas, Dynamic Programming and Optimal Control, Prop. 7.2.2 and 7.3.1, mission Dynamic Programming and Optimal Control VII). No formal treatment of Markov-renewal programs, of transition-dependent discounting, or of the retention rule of Fig. 1 is known to exist. The mission produces a verified policy-iteration theorem for semi-Markov decision processes, with an explicit termination bound and the comparison against nonstationary policies.
The discount over one transition, , varies with , and , so the problem is not a constant- contraction of textbook form; the relevant bound is that every row of sums to less than one, which rests on . Entries in alone, the paper's stated justification of Claim (a), do not make invertible: the matrix with every entry has entries in , yet minus it is singular.
Finite termination is not automatic either. If the improvement step may switch between tied maximizers, the iterates can cycle forever between two policies with equal returns; the retention rule of Fig. 1 excludes this, and Claim (b) must deliver a strict increase in some state, with no decrease anywhere, to rule out revisiting a policy. Comparing with nonstationary policies requires controlling returns of arbitrary policy sequences, whose limits must be shown to exist, not assumed.
Reusable infrastructure: bounds for substochastic matrices with row sums below one (invertibility, Neumann series, nonnegative inverse), convergence of iterated Bellman operators with transition-dependent discount, and the policy-iteration termination argument with a tie-breaking rule. Proofs of any milestone and alternative arguments are welcome.
The conjugate gradient method (cg-method) of Hestenes and Stiefel is the standard iterative solver for linear systems with a symmetric positive definite matrix . It is used for the large sparse systems of finite-element and finite-difference discretizations, as the inner solver of Newton-type and interior-point methods in optimization, and as the prototype of the Krylov subspace methods. Its original 1952 paper (Hestenes and Stiefel, J. Res. NBS 49(6), 1952) already presented it as two things at once: a direct method that reaches the exact solution in at most steps, and a method of successive approximations whose intermediate estimates are useful in their own right.
The second view needs a guarantee that the intermediate estimates actually approach the solution. The method is built to decrease the -weighted error , and the residual need not decrease (Section 18 of the paper, p. 432, notes that it can increase at every step). Theorem 6:3 of the paper supplies the guarantee in the plain Euclidean length: the distance from the estimate to the solution decreases strictly at every step, by an exactly computable amount. This mission formalizes that theorem together with the relations from Sections 5 and 6 of the paper on which its proof rests.
Timeline:
Let be a real matrix that is symmetric and positive definite, let , and let be the solution of . Write and . From an arbitrary starting point , the cg-method (5:1) computes estimates , residuals and direction vectors by
The error vector of is . The error function (4:5) is , which is nonnegative and vanishes only at . The Rayleigh quotient (4:12) of a vector is . The Lean development names these cgIter A k x₀ i (with fields .x, .r, .p), cgAlpha for , errorFun A h x and rayleigh A z.
For every step that the method performs, that is, every with ,
The paper writes the step from to ; the Lean statement shifts the index by one. The goal holds for every dimension , every symmetric positive definite , every and every .
The theorem is what makes an early stop of the cg-method safe in the norm a user usually cares about. Every intermediate estimate is closer to the solution, in Euclidean distance, than the previous one, and the identity (6:5) states by how much. It also separates the cg-method from methods that minimize the residual: the -norm error, the Euclidean error and the residual behave differently, and only the first two are monotone along cg.
The results are proved in the 1952 paper. They have not been formalized: the Prove2Me library has no statement of the conjugate gradient recursion (5:1), and Mathlib has none either. What this mission adds is a machine-checked version of the paper's Section 6 argument for the recursion exactly as printed, including the case analysis at termination that the paper leaves implicit, and a reusable Lean definition of the cg iteration with its basic identities.
The obvious argument does not reach the conclusion. The method decreases at every step, but a decrease in this -weighted norm does not imply a decrease in the Euclidean norm: for a single step along an arbitrary direction, even the best step for can lengthen the Euclidean error. So the theorem cannot be proved one step at a time from the local minimization property. It depends on how the current direction relates to all the later directions of the same run, and those relations in turn rest on the mutual orthogonality of the residuals and the conjugacy of the directions, which are established by an induction over the whole run.
A second difficulty is bookkeeping at the end of the run. The recursion divides by and by , which vanish after termination. Every milestone has to hold, or be guarded, past that point, and the goal needs the hypothesis exactly because the strict inequality fails once .
Vectors are Fin n → ℝ, the scalar product is dotProduct (⬝ᵥ), is Matrix.mulVec (*ᵥ), and the standing assumption is A.PosDef, which in Mathlib includes symmetry. The solution is a variable with the hypothesis A *ᵥ h = k. Indices are 0-based. The cg recursion is the definition cgIter, which computes (5:1b)–(5:1f) literally and in order; it has no stopping rule, and Lean's convention makes it stay at with once . Lengths appear squared, as . The milestones are stated for every index without a termination guard, because both sides of each identity vanish after termination; only the goal carries .
Two formalizations would trivialize the goal and are ruled out. The goal does not assume termination () or any bound on : it quantifies over every cg run and every step that takes place. And it is about the Euclidean length , not the error function (that is Theorem 6:1, a different and weaker statement) and not the residual.
A complete development needs Theorem 5:1 (orthogonality of residuals, conjugacy of directions) for the literal recursion, the identities (5:2) and (5:3c), and the positivity of for . These are reusable for any further work on the cg-method, including the sister mission on finite termination. Proofs of any milestone, and alternative proofs of Theorem 6:3 through the Krylov-subspace characterization, are welcome.
Solving a linear system with a large symmetric positive definite matrix is a basic task of scientific computing: it arises from discretized elliptic equations, least-squares problems and the Newton steps of optimization methods. In 1952 Magnus Hestenes and Eduard Stiefel published the conjugate gradient method (cg-method) (J. Res. Natl. Bur. Stand. 49 (1952) 409–436). The method uses only through matrix–vector products and stores a few vectors. The paper's abstract states its central property in one sentence: "The solution is given in steps."
The paper obtains this property from a more general scheme, the method of conjugate directions (cd-method), which also contains Gaussian elimination as a special case. Its argument has two parts. Every cd-method with nonzero directions reaches the solution within steps (Theorem 4:2). The cg-method is a cd-method (Theorem 5:2), which follows from the orthogonality and conjugacy relations of Theorem 5:1. This mission formalizes that chain.
Vectors are real -tuples, with scalar product and squared length . The matrix is real, , symmetric and positive definite, which is the paper's standing assumption (p. 410). The solution satisfies . The residual of an estimate is . Two vectors are conjugate when .
The cg-method (eq. (3:1), p. 411) starts from an arbitrary estimate and sets . Given , , , it computes
In Lean the iterates are cgIter A k x₀ i, a structure with fields x, r, p. The step length is cgA.
The cd-method (Section 4, p. 412) chooses an arbitrary first direction and then sets with and . Each new direction may be any vector conjugate to . Because the directions are free, a cd-run is a property of sequences: IsCDRun A k x r p.
For every , every symmetric positive definite , every and with , and every initial estimate ,
where is the -th cg iterate. This is the statement of the abstract and of Section 3 (p. 410): "one will reach an estimate () at which . This estimate is the desired solution ."
IsCDRun.Finite termination is the property that distinguishes the conjugate gradient method from stationary iterations such as Jacobi or Gauss–Seidel. It explains why the method can be used as a direct solver in exact arithmetic. It is the starting point for the later theory of Krylov subspace methods. The relations of Theorem 5:1 are the checks the paper recommends for monitoring a computation (eq. (3:3)). They are also the input to the paper's further results on the monotone decrease of the error (Section 6) and on the connection with orthogonal polynomials (Sections 14–18).
The result has been proved since 1952 and appears in every numerical linear algebra textbook. As far as a search of the Prove2Me catalog shows (September 2026), it has no machine-checked proof there. The only conjugate gradient material on the platform is a Hilbert-space convergence result for a different recurrence. This mission adds a faithful formal version of the original recursion (3:1) and of the cd-method. It also adds the complete termination argument, organized as in the paper. The definitions and the Theorem 5:1 relations are reusable by any later formalization of Krylov methods, including the second mission of this series on the decrease of the error .
The obvious argument says that the residuals are mutually orthogonal, so at most of them are nonzero. That argument is only as good as the orthogonality, and Theorem 5:1 must be established by a simultaneous induction over four families of relations. The recursion defines by an update, not as , so even needs a proof. Orthogonality of to the earlier residuals needs the conjugacy of the earlier directions, and conjugacy of needs the orthogonality of the earlier residuals. Neither family can be proved first.
A second obstacle is the passage from orthogonality to termination. A cd-run with a zero direction stalls, so Theorem 4:2 needs the directions to be nonzero. The cg directions become zero exactly when the solution is reached, so applying Theorem 4:2 to cg needs a case split at the first vanishing residual.
Vectors are Fin n → ℝ, the scalar product is dotProduct (⬝ᵥ), and is Matrix.mulVec (*ᵥ). The hypothesis on is Mathlib's Matrix.PosDef, which includes symmetry. The solution enters only through the hypothesis A *ᵥ h = k. Indices are 0-based, as in the paper.
The cg iteration is total and has no stopping test. Once , Lean's convention gives and . From then on the iteration stays at , with zero residuals and directions. For this reason the relations of Theorem 5:1 are stated for all indices without guards: after termination they hold trivially.
Two formulations would make the goal trivial, and neither is used. One is a stopping test or step that refers to or to . The other replaces (3:1b), (3:1d) or (3:1e) by the equivalent formulas (3:2a), (3:2b) or , which would move Theorem 5:5 and part of Theorem 5:2 into the definition. The iteration is (3:1) literally.
The cd-method's implicit hypothesis, that the directions are nonzero, is an explicit binder of Theorem 4:2. Without it the statement fails (take ). The hypothesis is satisfiable: the cg run with nonzero residuals is one example.
A complete development needs the standard facts that mutually conjugate nonzero vectors are linearly independent and that independent vectors span . It also needs the induction behind Theorem 5:1. Contributions welcome beyond the milestones include the converse half of Theorem 5:2, the relation (5:2) expressing through , and Theorem 4:5 (the cd-method computes ).
In online convex optimization a player repeatedly chooses a point from a convex set , after which an adversary reveals a convex cost function and the player pays . The player's regret after rounds is its total cost minus the cost of the best fixed point in hindsight. The model covers online portfolio selection, online regression and prediction with expert advice, and it underlies the analysis of stochastic and adaptive optimization methods (Zinkevich 2003; Cesa-Bianchi and Lugosi 2006).
For general convex costs the best achievable regret is of order . Hazan, Agarwal and Kale (Mach Learn 69, 2007) showed that a curvature condition, -exp-concavity, brings the regret down to order , and gave several algorithms that achieve it. This mission concerns the simplest of them, Exponentially Weighted Online Optimization (EWOO), which needs nothing beyond exp-concavity: no bound on gradients and no bound on the diameter of .
Timeline.
Fix and a set that is nonempty, closed, bounded and convex, with positive Lebesgue volume . Fix . The cost functions are , each continuous on and -exp-concave on : the function is concave on (LogRegretOCO.EWOO.IsExpConcave).
EWOO keeps the weights
and on round plays the -weighted mean of ,
(LogRegretOCO.EWOO.ewooPoint). In particular is the centroid of , and each depends only on . The regret against a comparator is .
For every and every ,
This is the paper's printed constant. The paper's proof yields the slightly sharper ; the printed form is the goal.
The proof in §3.4 (p. 187) passes through five displays, each a milestone:
The result. Theorem 7 shows that exp-concavity alone suffices for logarithmic regret, with a constant that does not depend on the size of or on the gradients of the costs. Specialised to the log-loss on the simplex, where , it recovers the regret of Cover's universal portfolio. The bound is the benchmark against which the computationally cheaper second-order methods of the same paper (Online Newton Step, Follow the Approximate Leader) are compared: those need a gradient bound and diameter and pay a factor .
Formalizing it. The theorem is proved in the paper, and a textbook version with a different constant, , appears in Hazan's Introduction to Online Convex Optimization (Theorem 4.4). No machine-checked proof of either is known. The work here is to formalize the paper's proof: Jensen's inequality for a weighted Lebesgue average in , the change of volume under homothety, and the elementary inequality . A companion draft of the textbook version exists on the platform as a private item (OnlineConvexOpt.SecondOrder.ewoo_regret) with another constant; it is not reused.
The pieces are classical, but they have to be assembled in measure-theoretic form. The point is a Bochner integral of a vector-valued function over , and its membership in and the Jensen inequality both require the normalised weight to be a genuine probability measure on , with every integrand integrable. The obvious one-dimensional intuition — "the weighted mean of a convex set lies in the set" — hides the requirement that be closed and have positive volume.
The second obstacle is that Eq. (18) compares the algorithm with an average of the product over all of , while the regret compares it with a single point. The natural attempt, bounding the average below by the value at the comparator, fails: the average can be far smaller than the maximum, and a lower bound that loses more than a factor polynomial in destroys the logarithmic rate. Controlling this loss in dimensions, with a constant independent of the shape and size of , is the heart of the argument.
Points live in EuclideanSpace ℝ (Fin n) with its Lebesgue (Haar) measure volume. Rounds are numbered from : the weights sum over Finset.Ico 1 t, the regret over Finset.Icc 1 T. Cost functions are defined on all of ; only their values on enter. The algorithm is the total function ewooPoint P α f t, and the goal is stated for equal to it — not for an arbitrary sequence satisfying a Jensen-type inequality.
Conventions and corrections relative to the printed text:
⨅ or sInf over , which in Lean would return a junk value off its intended domain and trivialize the statement.volume P ≠ 0 is added: the algorithm divides by , which the paper leaves implicit. Without it Lean's convention would set .Infrastructure that a complete development needs, and that is reusable beyond this mission: Jensen's inequality for concave functions under a probability measure with a continuous density on a compact convex set (Mathlib has ConcaveOn.le_map_integral and Convex.integral_mem); the scaling identity for Haar measure (MeasureTheory.Measure.addHaar_smul); and the elementary bound . Proofs of any milestone, and a general weighted-Jensen lemma usable across the milestones, are welcome.
Online convex optimization models repeated decision making against an adversary: in each round a player chooses a point of a convex set, and only then learns the convex cost of that round. It covers online portfolio selection, online regression and routing, and it is the standard lens for analysing learning algorithms that must commit before seeing data. The figure of merit is regret, the player's total cost minus the cost of the best fixed decision in hindsight. For general convex costs regret over rounds is optimal; for costs with curvature it can be logarithmic.
Hazan, Agarwal and Kale (Mach Learn 69 (2007) 169–192) gave several algorithms with regret for -exp-concave costs, the class that contains the log-loss of portfolio selection. This mission formalizes one of them, Follow the Approximate Leader (FTAL). It connects to the oldest online algorithm, Follow the Leader (FTL), which plays the minimiser of all past costs: FTAL is FTL run on quadratic lower models of the costs, and the paper's analysis shows that FTL itself has logarithmic regret on a class of curved costs.
Timeline. Zinkevich (2003) proved regret for online gradient descent on convex costs. Cover (1991) gave a universal portfolio with logarithmic regret for the log-loss, at a running time exponential in the dimension. Kalai and Vempala (2005) analysed perturbed Follow the Leader through the "be the leader" argument. Hazan, Agarwal and Kale (2007) gave efficient algorithms (Online Newton Step, FTAL, EWOO) with regret for exp-concave costs.
The decision set is nonempty, convex, closed and bounded, and bounds its diameter: for . In rounds the player picks and then pays , where is a cost function differentiable at the points of with gradient norm on . The cost is -exp-concave () if is concave on . The regret over rounds against a comparator is .
Follow the Leader plays (any point of in round 1). Follow the Approximate Leader (version 1 of the paper's Fig. 3) with parameter plays FTL on the approximate costs
In the Lean development these are IsFTLRun P f x and IsFTALRun P β f x, predicates on a whole trajectory .
With , every FTAL run on -exp-concave costs satisfies, for every and ,
This is the paper's statement with its constant, stated for the algorithm as defined, and for every adversarial sequence of costs.
Theorem 6 shows that a simple rule, re-solving a convex quadratic program over all past linearized costs, achieves regret on exp-concave costs, matching the Online Newton Step up to constants. Theorem 5 is of independent interest: it shows that unmodified Follow the Leader, which has linear regret on linear costs, has logarithmic regret whenever each cost is a strongly curved function of one linear form. Portfolio selection is such a case. The appendix lemmas (log-determinant potential, elliptical potential) are standard tools reused throughout the bandit and online-learning literature.
On formalization: the results are proved on paper; none is formalized. The Lean development provides a reusable encoding of Follow the Leader as a trajectory predicate, the "be the leader" reduction, the surrogate reduction for regret, and the matrix potential inequalities, which the Online Newton Step analysis also needs. The paper's printed statements of Theorem 5 and Lemma 10 contain errors (see below); this mission states corrected versions that suffice for the goal.
The obvious attempt, bounding each term by how far the leader moves, requires knowing how far the minimiser of a constrained problem moves when one cost is added. For unconstrained strongly convex quadratics this is an explicit Newton step, but here the minimiser lies in a general convex set and each cost contributes curvature in only one direction, so the accumulated curvature can be singular for many rounds and no per-round strong convexity is available. Turning the per-round movement into a sum that grows only like , with the paper's explicit constant, is the core of the work; the printed Theorem 5 bound is negative for small , so the constants must be tracked exactly rather than asymptotically.
Points are in EuclideanSpace ℝ (Fin n) so that is the Euclidean norm; cost functions are functions on all of , differentiable at the points of , with Mathlib's gradient. Rounds are -based; and are unused. is any upper bound on pairwise distances in . Exp-concavity is ConcaveOn ℝ P (fun x => Real.exp (-α * f t x)). Algorithms are predicates on the trajectory, required at every round, so every tie-breaking rule is covered and adaptive adversaries are included.
Regret is always stated against every comparator . A formalization with a real-valued ⨅/sInf over , or one that bounds the regret of an arbitrary sequence of points rather than of an FTAL run with the paper's , would be trivial or false, and is excluded: the goal carries IsFTALRun with .
Corrections and conventions relative to the printed paper:
deriv with explicit differentiability at the points , .Needed infrastructure: first-order optimality for convex minimisation over a convex set, a mean-value theorem along segments, determinants and eigenvalues of symmetric positive definite matrices (Mathlib has most of this), and the matrix inequality . Contributions welcome: proofs of any milestone, and a proof of the goal from the milestones.
Online convex optimization models repeated decision making against an unknown, possibly adversarial environment: in each round a player picks a point of a convex set , and only then learns a convex cost function and pays . Performance is measured by regret, the excess of the total cost over that of the best fixed point in hindsight. Zinkevich (ICML 2003) showed that online gradient descent has regret for arbitrary convex costs with bounded gradients, and this rate cannot be improved in general.
Many costs met in practice have more curvature than bare convexity. The log-loss of universal portfolio management (Cover, Math. Finance 1991) is not strongly convex, but it is exp-concave. Hazan, Agarwal and Kale (Mach Learn 69, 2007) gave the first efficient algorithms with regret logarithmic in for exp-concave costs. This mission formalizes the second of their algorithms, the Online Newton Step (ONS), and its regret bound (Theorem 2 of the paper). ONS is the basis of later second-order online methods and appears as a standard algorithm in textbooks on online learning.
Timeline:
The decision set is nonempty, closed, bounded and convex, and bounds its diameter: for all , with the Euclidean norm. The costs are real functions, differentiable at every point of , with gradient bound on . A cost is -exp-concave () if is concave on .
For a matrix , the generalized projection is a point of minimising over .
The Online Newton Step fixes
writes and , plays an arbitrary , and then
The regret after rounds against a comparator is ; the paper's regret is its maximum over .
In Lean the objects are LogRegretOCO.ONS.onsBeta, onsEps, onsMatrix, IsGenProj and IsONSRun, with the regularised Gram matrix regGram and the quadratic form quadForm.
For every run of ONS, every horizon with , and every ,
The added condition is what makes the printed constant correct (see Formalization scope).
Theorem 2 shows that exp-concavity alone, without strong convexity, suffices for regret logarithmic in , at a per-round cost of one rank-one matrix update and one generalized projection. Its consequences include logarithmic regret for universal portfolio selection with a polynomial-time algorithm, and, by online-to-batch conversion, fast rates for stochastic exp-concave optimization. Lemma 11 (the elliptical potential bound) is used well beyond this paper, in linear bandits and online regression.
The result has been proved on paper since 2007. The remaining work is its machine-checked proof: the potential argument, the log-determinant inequality and the generalized-projection inequality for positive semidefinite matrices. As far as is known, none of these results is formalized in Mathlib. Prove2Me holds a related elliptical potential lemma for linear bandits (BanditAlgorithm.elliptical_potential_lemma, with and a , a different statement) and the Euclidean case of Lemma 8 (UnderstandingML.projection_lemma). The textbook version of ONS (OnlineConvexOpt.SecondOrder.online_newton_step_regret, with and bound ) is an open private draft with different parameters.
The obvious route to logarithmic regret, the gradient-descent argument of Theorem 1 with step sizes , needs a uniform lower bound on the Hessians. Exp-concave costs such as the log-loss have no such bound: their curvature vanishes in directions orthogonal to the gradients seen so far. The analysis therefore has to track curvature only along the observed gradient directions. This requires a matrix-valued potential and a projection in the norm of rather than the Euclidean norm. The Euclidean projection inequality does not transfer to this norm, which changes from round to round. Bounding the potential requires determinant inequalities for positive definite matrices. The analytic facts are elementary, but their Lean statements involve the interaction of EuclideanSpace, Matrix.mulVec, Matrix.inv and Matrix.det.
Points live in EuclideanSpace ℝ (Fin n), so all norms are Euclidean; matrices are Matrix (Fin n) (Fin n) ℝ acting on coordinate vectors. Rounds are 1-based: sums run over Finset.Icc 1 T and the index is unused. Cost functions are ambient functions , differentiable at the points of , with given by Mathlib's gradient. The paper's standing assumptions of convexity and twice differentiability are not needed and are omitted. enters only as an upper bound on distances in . The generalized projection is a predicate that every minimiser satisfies, and ONS is the predicate IsONSRun on the whole trajectory, so the goal covers every tie-break and every adaptive adversary.
Corrections and added hypotheses:
Regret is stated against every comparator , never as a real infimum ⨅ over , which is junk-valued in Lean on unbounded or empty sets. The goal is a statement about runs of the paper's algorithm with the paper's , and . A bound for an arbitrary sequence satisfying the p. 178 display would be a milestone, not Theorem 2. The hypotheses are jointly satisfiable: the closed unit ball with , , , is a model.
A complete development needs: first-order conditions for concave functions on convex sets at boundary points; the optimality condition for minimising a convex quadratic over a convex set; spectral facts about symmetric positive definite matrices (square roots, eigenvalues, and ); and the telescoping of log-determinants. Lemmas 8, 11 and 12 are reusable beyond this mission, in the sibling missions of this series (Follow the Approximate Leader) and in linear-bandit analyses. Proofs of any milestone are welcome, as are alternative proofs of Lemma 12 through concavity of .
Many combinatorial optimization problems ask for a subset of a finite ground set that maximizes a set function with diminishing returns: Max Cut and Max Directed Cut in graphs, facility location, maximum entropy sampling, and welfare problems in combinatorial auctions all fit this pattern. The common abstraction is the maximization of a submodular function, the discrete analogue of a concave function. Unlike the monotone case, where the objective only grows as elements are added, the non-monotone problem has no constraint at all and is still NP-hard, since Max Cut is a special case.
For Max Cut and Max Directed Cut, the simplest algorithm there is, putting every vertex on a side by an independent fair coin, already cuts half, respectively a quarter, of the optimum in expectation. Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011; extended abstract at FOCS 2007) showed that this is not a feature of cut functions: the same random choice achieves the same factors for every nonnegative submodular function, and for every symmetric one. This mission formalizes that result, Theorem 2.1 of the paper, together with the two sampling lemmas on which it rests. The paper's other results (a nonadaptive 1/3-approximation, deterministic and smoothed local search, and query lower bounds) are the subjects of companion missions in the same series.
Let be a finite set with elements. A set function assigns a real number to every subset . It is submodular if
equivalently if the marginal value of an element does not increase as the set grows. It is symmetric if for every ; the cut function of an undirected graph is the standard example. The optimum is
For , denotes the random subset of containing each element independently with probability ; similarly is the random subset of a fixed . The Random Set Algorithm (RS) returns , a uniformly random subset of , without querying . Its expected value is the average of over all subsets,
where is the multilinear extension of , the expectation of on a random set that includes element independently with probability .
For every nonnegative submodular ,
and if is in addition symmetric,
Both parts form the goal, stated as one theorem. The constants and are exact, not asymptotic, and they are tight: the directed cut of a single arc attains , and the cut of a single edge attains .
The milestones need no sign on the function; nonnegativity enters only in the goal.
The result. Theorem 2.1 gives an algorithm that makes no query at all and is still a constant-factor approximation for unconstrained non-monotone submodular maximization. It sets the baseline that every later algorithm for the problem is measured against: the paper's own nonadaptive -algorithm and its local search algorithms with factors and , followed by later work culminating in the tight -approximation of Buchbinder, Feldman, Naor and Schwartz (FOCS 2012). The paper also shows that is optimal among nonadaptive algorithms required to return one of the queried sets, and that is optimal for symmetric functions among all algorithms using polynomially many value queries, so both factors of Theorem 2.1 have a precise place in the complexity landscape. Lemma 2.3, the probabilistic inequality behind it, is reused in the analyses of the nonadaptive algorithm and of smooth local search.
Formalizing it. The result is proved, with a short proof. What this mission adds is a machine-checked version of the random-set guarantee and of the two sampling lemmas, stated for arbitrary finite ground sets and, for the lemmas, for real-valued submodular functions without a sign. To our knowledge none of these statements has a machine-checked proof; Mathlib has no theory of submodular set functions or of their multilinear extension.
The goal itself is a two-line consequence of the third milestone. The work sits in the lemmas and in one change of viewpoint.
Lemma 2.2 is not a pointwise statement: the random set can be any subset of , and can be smaller on it than both and . The inequality holds only in expectation, and only because submodularity controls the marginal value of each element uniformly across the sets it can be added to. Lemma 2.3 needs a conditioning argument over two independent samples; the sets and may overlap, and on the union contains an element with probability , so it is not the product distribution with probability on and on . Finally, the third milestone requires identifying the uniform random subset with the union of independent half-samples of and of its complement, as a statement about finite sums.
The obvious attempt at the goal, comparing with for an optimal set by set, fails: is not monotone, so a random set that contains most of may still have small value, and a random set can pick up elements that hurt.
The ground set is a Lean type X with [Fintype X] [DecidableEq X]; subsets are Finset X and set functions are f : Finset X → ℝ. Submodularity is the lattice inequality of Definition 1.1, not the decreasing-marginals property. Nonnegativity, the paper's standing assumption , is the hypothesis ∀ S, 0 ≤ f S; it appears only in the goal. Symmetry is ∀ S, f Sᶜ = f S for all subsets, not only for an optimal one. is Finset.univ.sup' Finset.univ_nonempty f, a maximum over the always nonempty family of all subsets, so it is attained. The ground set may be empty; the goal holds there too and no nonemptiness is assumed.
Expectations are written as exact finite sums, not as integrals. is the multilinear extension F f (fun _ => 1/2). is , and is the double sum over independent samples , with the product of the two weights. The ranges and , implied in the paper by the word "probability", are explicit hypotheses; Lemma 2.2 is false without them.
Trivializing formalizations are excluded: the weights are exactly those of the uniform distribution on all subsets, is the true maximum rather than the value at one fixed set, and is required to be both nonnegative and submodular.
Reusable infrastructure produced by a complete development: the multilinear extension of a set function and its expression as an expectation, product-weight identities for independent sampling of subsets (including the decomposition of along a set and its complement), and Lemmas 2.2 and 2.3, which the companion missions on the nonadaptive algorithm and on smooth local search also need. Proofs of any milestone are welcome independently.
Stochastic programs are solved in practice on a finite set of scenarios: a discrete probability distribution that approximates the true distribution of the uncertain data. The size of the resulting deterministic problem grows with , and for multistage models it grows very fast, so is often reduced before solving. The question is which scenarios to delete and how to reweight the remaining ones so that the optimal value and solutions of the stochastic program change as little as possible.
Dupačová, Gröwe-Kuska and Römisch (Math. Program. Ser. A 95 (2003) 493–511) answered this with probability metrics. Stability results for stochastic programs bound the change of the optimal value by a Fortet–Mourier type distance, which is in turn bounded by a Kantorovich functional (an optimal transport cost). Scenario reduction then becomes: find a measure supported on a subset of the scenarios with small. Section 3 of the paper solves the weight part of this problem in closed form. That result, together with the heuristics built on it (backward reduction and forward selection), became the standard scenario-reduction method, implemented for example in the GAMS tool SCENRED.
Let be a set and a cost function with if and only if , and (conditions (C1)–(C2), p. 498). The original distribution has scenarios with weights and . Write .
A set of scenarios is deleted. The reduced measure is with reduced weights , . A transport plan from to is a nonnegative matrix with row sums and column sums . The Kantorovich functional (10) is the value of this transportation problem,
and is the best distance achievable once is fixed. The optimal deletion problem (13) asks for for a given .
In the Lean development these objects are IsReducedWeight, IsTransportPlan, transportCost, transportValue (), optWeightsValue () and optimalDeletionValue (the value of (13)), all in the namespace ScenarioReduction.Redistribution.
For every ,
and the minimum is attained at the optimal redistribution rule , where and , for every such choice of .
Theorem 2 reduces the continuous part of scenario reduction to a formula: once the set of kept scenarios is chosen, the best reweighting is to move the mass of every deleted scenario to a nearest kept scenario, and the resulting distance is an explicit sum. This leaves only the combinatorial choice of , which Theorem 4 brackets by two greedy procedures; these are the backward-reduction and forward-selection algorithms of the paper and of later work by Heitsch and Römisch. Theorem 3 covers the case in which the reduced weights are fixed by the modeller, for instance to keep a uniform distribution uniform.
The results are proved in the paper by elementary linear-programming arguments. As far as is known, none of them has a machine-checked proof. Formalizing them produces a verified finite transportation-problem layer with a general (not necessarily metric) cost and a deleted index set, and verified correctness certificates for the two standard scenario-reduction heuristics.
The upper bound of Theorem 2 is a direct construction. The content lies in the lower bound, which must hold for every reweighting simultaneously; this needs the dual side of the transportation problem, and the full primal–dual representation (Milestone 1) requires strong duality for a transportation problem with only the kept columns, which Mathlib does not provide in this form. A naive argument that bounds each plan row by row gives the lower bound directly for plans, but relating it to as an infimum also requires that plans exist and that the infimum is attained. In Theorem 4, the recursions (16) and (17) are greedy and do not in general produce optimal sets; the lower bound works only because its inner minimum ranges over all , not over the kept scenarios.
Scenarios are indexed by Fin N (0-based), scenarios are a function ω : Fin N → Ω into an arbitrary type Ω, the cost is c : Ω → Ω → ℝ, and weights, plans and dual variables are real-valued functions on Fin N and Fin N × Fin N. Only the entries at kept indices enter any constraint, cost or objective. No measure theory is used: the index-level transportation problem is the paper's own representation of for discrete measures (p. 495). Every theorem carries the standing assumptions of Section 3: , (C1), (C2), and . Measurability of and conditions (C3) and (C4) concern and play no role for finitely supported measures; they are dropped, so the statements are more general than the page. The hypothesis , implicit in Theorem 2, is stated explicitly; in Theorem 4, plays this role.
and are real infima (sInf) of transport costs and are only asserted about where the underlying sets are nonempty and bounded below; "min" is stated as attainment (IsLeast), not as an equality of infima. is defined as the transportation problem and is not defined by the closed form ; under that definition Theorem 2 would be trivial, and it is ruled out here. Likewise the reduced-weight constraint does not force .
Needed infrastructure: finite transportation problems with nonnegativity and marginal constraints, existence of optimal plans (compactness of the feasible polytope), and LP duality for transportation problems. The transportation-problem layer is reusable beyond this mission. Contributions welcome: proofs of the milestones, a general strong-duality result for finite transportation problems, and the examples of p. 502 (single scenario deletion, keeping one scenario).
Minimizing the sum of weighted completion times of jobs on identical parallel machines is one of the basic objectives of machine scheduling: it measures the average time a job spends in the system, weighted by its importance. When the jobs are subject to precedence constraints (a job may start only after certain other jobs have finished), the problem is strongly NP-hard already in very restricted cases, and the question becomes how close to optimal a polynomial-time algorithm can guarantee to be.
Chekuri, Motwani, Natarajan and Stein, Approximation Techniques for Average Completion Time Scheduling (SIAM J. Comput. 31(1), 2001, doi:10.1137/S0097539797327180), develop a general way to turn a good schedule for a single machine into a good schedule for machines. For arbitrary precedence constraints their conversion (Delay List, §4.1–4.3) loses a factor over a -approximate one-machine schedule, which is when the one-machine schedule is optimal. In §4.4 they show that for in-tree precedence without release dates, the plain list-scheduling rule of Graham, fed with an optimal one-machine schedule, already achieves ratio . In-trees are the precedence structures of assembly processes: every job feeds into at most one later job.
Timeline of the relevant results:
There are jobs and identical machines. Job has a processing time and a weight ; every job is available at time (there are no release dates).
The precedence constraints form an in-tree (more generally, an in-forest): every job has at most one immediate successor , and following successors never returns to the start. Write if is reached from by following successors one or more times.
A feasible schedule on machines gives each job a start time and a machine; a job runs without interruption for time units; two jobs on the same machine do not overlap; and implies that starts no earlier than completes. The completion time is and the value of the schedule is .
The critical-path length (Definition 4.1 with no release dates) is if has no predecessors and otherwise.
A list is an ordering of the jobs that obeys the precedence constraints. It defines the one-machine schedule that runs the jobs in list order without idle time; its completion times are , the total processing time of the jobs up to and including in the list. An optimal one-machine schedule is a list minimizing .
List scheduling (Graham's rule, footnote 3 of the paper) on machines with list : whenever a machine is free, start on it the first job of the list that is ready, i.e. whose predecessors have all completed.
Let be an optimal one-machine schedule and the list schedule on machines with list . Then for every feasible -machine schedule ,
Lemma 4.16 (any precedence-respecting list , with its idle-free one-machine schedule ): for every job ,
Lemma 4.10: , i.e. for an optimal list and every feasible .
Lemma 4.11: , i.e. for every feasible on any number of machines, and the value is attained by a feasible schedule on machines.
The result. Theorem 4.17 gives a simple, fast algorithm with a guaranteed factor for a strongly NP-hard problem, halving the factor that the general Delay List conversion gives for the same class. The per-job bound of Lemma 4.16 is stronger than the aggregate statement: every single job completes within its critical-path length plus a share of its one-machine completion time, so the same bound applies to other objectives built from completion times.
Formalizing it. The paper's proof is complete and short, but it argues about events at a time (jobs that finish exactly at , jobs that become ready at , machines freed at ) and runs an induction over jobs ordered by start time with an invariant about idle time. A machine-checked version fixes what "list scheduling" means precisely, pins down the counting argument that uses the in-tree structure, and yields reusable definitions of nonpreemptive parallel-machine schedules, critical paths and list schedules. To the knowledge of this mission, none of these results has a machine-checked proof.
List scheduling may start a job that is late in the list before an earlier one, because the earlier job is not yet ready; so the one-machine order is not preserved and the obvious comparison with fails. Idle machines are the other obstacle: a machine can stay idle while a job waits for its predecessors, and a per-job bound of the form holds only if such idle time can be accounted for by 's own chain of predecessors. For general precedence constraints, and for out-trees (every job has at most one immediate predecessor), the paper's accounting breaks down, and the paper states the per-job bound only for in-trees; the in-tree structure is essential to the argument. Events with several jobs finishing at the same instant, and ties in start times, have to be handled without loss.
Fin n, machines Fin m, times real numbers. Processing times and weights are strictly positive. There are no release dates: start times are nonnegative. The paper admits only in lower-bound instances elsewhere; the bounds here assume .succ : Fin n → Option (Fin n) with no cycles; this covers in-forests, the reading of "in-trees" in Theorem 4.17. The precedence relation is its transitive closure.Welcome contributions: proofs of the two existence items (Graham's list schedule by event-driven construction; an optimal order over the finite set of linear extensions), of Lemmas 4.10 and 4.11, and of Lemma 4.16. The schedule and list-scheduling definitions are reusable for other parallel-machine results with precedence constraints.
A supplier and a retailer who trade a seasonal product must decide who carries the inventory risk: the stock left unsold, or the demand left unserved, when the season ends. With a push contract the retailer orders everything before the season and bears the risk; with a pull contract he orders during the season from the supplier's stock at a single wholesale price, and the supplier bears it. Cachon (Management Science 50(2), 2004) studies the two and the contract between them, the advance-purchase discount, in which units ordered before the season are cheaper than units ordered during it.
In the base model of that paper, shipping a unit during the season costs the same as shipping it before. In practice orders placed during the season are often smaller and more urgent, and shipping and handling them costs more. §5.1 of the paper adds such a cost and asks whether pull contracts remain attractive. Theorem 8 answers that they are then never Pareto efficient: some advance-purchase discount is better for both firms.
Demand for the season has law on , distribution function and density . As in §3 of the paper, , is strictly increasing on , on , and the generalized failure rate is strictly increasing (IGFR). The expected sales from available units are
The retail price is , the unit production cost , the salvage value , with .
A contract is a pair of wholesale prices . Before production the retailer submits a prebook order of units at . The supplier then produces . During the season, after running out of prebooked stock, the retailer places at-once orders at , filled from the supplier's remaining stock. Pull is ; an advance-purchase discount is . In §5.1 the supplier pays an extra shipping and handling cost per at-once unit. The profits are
A supplier best response to maximizes over . An outcome of is a pair with a best response to and maximizing when every alternative prebook is followed by a best response to it.
Fix and , and suppose the retailer does not prebook under the pull contract : is his unique best reply, followed by the supplier's best response . Then there is with
such that has an outcome, and every outcome of it satisfies
Without shipping costs, advance-purchase discounts with coordinate the supply chain (Theorem 7 of the paper, the subject of mission 2 of this series), and a pull contract can lie in the Pareto set among push and pull contracts (Theorem 6, mission 1). Theorem 8 shows that the second fact does not survive an at-once shipping cost of any size: pulling inventory during the season incurs a cost the integrated chain would avoid, and a small discount for early commitment shifts part of the stock to the prebook, where it is cheaper to ship. The Pareto set then no longer consists of a single contract type. The result supports the paper's conclusion that each of its three extensions makes push relatively more attractive than pull.
The theorem is proved in the paper, not formalized anywhere. A formal proof requires making precise two points the paper passes over: what "the retailer does not prebook" means when the retailer could switch to a large prebook once a discount is offered, and why no positive density at is needed. Formalized, the statement also gives a checked account of the prebook game under a two-price contract, reusable for the other extensions of §5.
The paper's argument differentiates the supplier's profit along the retailer's optimal prebook and takes the limit as . That limit involves , which the model does not provide: is differentiable only on , and for gamma demand with shape above the density vanishes at , so the paper's limit is . A proof of the goal must therefore not rest on the limit display alone.
The second obstacle is the retailer's global choice. The calculus concerns prebooks below the supplier's production . Once , the retailer might instead prefer a prebook at least , turning the chain into push mode, and the outcome would then not be the one the derivative describes. Ruling this out for close to requires the strict form of the premise and a uniform comparison of the two regimes; it is not a local argument at .
Demand is a probability measure μ on ℝ with F := ProbabilityTheory.cdf μ, and the standing assumptions of §3 form the predicate DemandModel μ f; differentiability of F is required on only, so the exponential law is admitted. Quantities range over . Best responses and outcomes are defined as maximizers, not by the closed forms of milestones 1 and 2. All profit formulas are those of §4.5 for , and every statement assumes it. The shipping cost enters only the supplier's at-once net revenue . The prebook function in milestones 5 and 6 is a function pinned on by Eq. (22), which determines it uniquely.
Readings of the paper's words:
A version of the goal that assumed , assumed , compared only one favourably chosen outcome of the discounted contract, or stated either firm's gain with , would be weaker than Theorem 8 and is not the target.
A complete development needs the concavity and first-order conditions for , the inverse-function derivative for , and the regime comparison between prebooks below and above . The first two are reusable across all newsvendor-type models; contributions proving the milestones in any order are welcome.
A supplier who must produce before a selling season, and a retailer who sells into uncertain demand, have to decide who holds the inventory that may go unsold. Cachon (Management Science 50(2), 2004) studies this allocation of inventory risk using nothing but wholesale prices. With a push contract the retailer orders everything before production and bears all the risk; with a pull contract the retailer orders only during the season and the supplier bears it; an advance-purchase discount sits between the two, offering a lower price for early orders. The paper's introduction contrasts Trek, which holds bicycle inventory and ships to retailers on demand, with O'Neill, which offers retailers a prebook discount for ordering before the season.
The classical view is that wholesale-price contracts cannot coordinate a supply chain: a single wholesale price above marginal cost makes the retailer order too little (the double-marginalization effect). Coordination was known to need richer terms, such as buyback contracts (Pasternack 1985) or revenue sharing (Cachon and Lariviere 2005). This mission formalizes the paper's Theorem 7, which shows that two wholesale prices, one for early and one for in-season orders, suffice both to coordinate the chain and to divide its profit arbitrarily. A companion mission of the same series formalizes Theorem 6, the Pareto set of push and pull contracts alone.
Demand is a random variable with distribution function and density . The paper assumes , strictly increasing, and an increasing generalized failure rate (IGFR): has . Production costs per unit, the retail price is , and leftover units are salvaged for , with . Expected sales with units available are
and the integrated supply chain's expected profit is . It is maximized at with ; write . The efficiency of a contract is , where is the quantity produced.
A contract is a pair of wholesale prices with . The retailer first prebooks units at each. The supplier, seeing , produces . During the season the retailer sells the prebook and, once it runs out, places at-once orders at per unit from the supplier's remaining stock, provided . The supplier's and retailer's expected profits are
with the at-once terms absent when . An outcome of a contract is a pair where maximizes the supplier's profit given , and maximizes the retailer's profit given that he anticipates the supplier's response. The contract classes are push (), pull () and advance-purchase discount (). A contract is Pareto if no outcome of any contract in these classes makes one firm strictly better off and neither firm worse off than one of its own outcomes (p. 224).
For every with , the contract has an outcome and is Pareto; every outcome of every Pareto contract satisfies
and for every some contract with has an outcome with payoffs
A further draft theorem states the step of the proof in which the retailer's outcome profit along falls strictly from to as rises from to .
The theorem identifies a coordinating family inside the simplest contract language there is. Setting the at-once price equal to the retail price gives the supplier exactly the chain's marginal incentive for capacity, so she produces ; the prebook price then acts as a pure transfer. Every division of is reached, so for any bargaining process the Pareto set is fully efficient. This contrasts with Theorem 6 of the same paper, where push and pull contracts alone leave the Pareto set inefficient, and with the buyback and revenue-sharing coordination results (formalized on the platform as Theorems 14.4–14.6 of Snyder and Shen's Fundamentals of Supply Chain Theory), which need contract terms beyond wholesale prices.
The result is proved in the paper and has not been machine-checked. The mission produces a formal prebook game (best responses, outcomes and Pareto dominance as optimization statements) and Theorem 7 with all three claims, including the claim about every Pareto contract, which the paper argues in one sentence.
The closed forms are fractile equations, and the obvious argument substitutes them. That argument is incomplete in three places. First, the retailer's anticipated profit is piecewise: below the supplier's own quantity he gets at-once service, above it the chain runs in push mode, and the proof must show the retailer never prefers the push branch when . Second, "every Pareto contract is efficient" is a statement about all contracts, including push and pull, and needs both firms' payoffs to be nonnegative at every outcome of every admissible contract, which depends on the prebook always being available and on . Third, the division claim is surjectivity of the retailer's equilibrium payoff over , which needs the solution of to vary continuously with , including at both ends ( at , at ).
Demand is a probability measure on with = ProbabilityTheory.cdf μ. The standing assumptions are a structure: , strictly increasing on , on , and on . Differentiability is required only on , so the exponential distribution, which the paper names as IGFR, is admitted. Theorem 7 does not use IGFR; it is kept so that the series shares one model. Quantities range over . is a parameter with the hypothesis ; its existence is part of milestone 1.
Readings of informal words: "includes all" means every contract with has an outcome and each of its outcomes is undominated; "the Pareto set coordinates" is stated for every Pareto contract, not only the family; "any division is achievable" is surjectivity onto ; "increasing" in Eq. (2) and "decreases" in the proof are strict; "arg max" in Eqs. (3) and (22) is the unique maximizer; "the optimal production is " is an if-and-only-if characterization of the supplier's best responses. At-once orders are submitted exactly when (p. 226, "with push , so at-once orders are never submitted"). Additions to the paper's contract classes: every class requires (p. 228 sets aside as Pareto inferior); pull includes (the paper's remark in the proof) and advance-purchase discounts include (as Theorem 7 names them). Pareto dominance is between payoff pairs of outcomes.
Outcomes are defined as maximizers, not by the closed forms (21)–(22). Defining the outcome of as would turn the goal into algebra, and is ruled out.
Needed infrastructure: continuity and inverse of a strictly increasing distribution function, concavity of , and first-order conditions on half-lines. The definitions of the prebook game are reusable for Theorem 8 of the same paper. Proofs of the milestones and of the goal are welcome.
A supplier and a retailer trade a product with a single selling season and uncertain demand. Someone has to decide, before demand is known, how many units exist, and someone has to be left holding the units that do not sell. With a push contract the retailer orders (prebooks) before the season and bears all of this risk; with a pull contract the supplier produces to stock and the retailer only orders during the season, so the supplier bears it. Both are single wholesale price contracts, the simplest and most common contracts in practice. Cachon (Management Science 50(2), 2004) asks which of these contracts two negotiating firms could plausibly agree on, independently of how they bargain, and answers it by computing the Pareto set of push and pull contracts together.
Push alone is the "selling to the newsvendor" problem studied by Lariviere and Porteus (MSOM 2001), whose unimodality result this mission uses. The novelty of §4 of Cachon's paper is to put push and pull contracts in one contract space and to show that the Pareto set then contains contracts of both kinds.
Demand has distribution function and density . The paper's standing assumptions (§3, p. 225) are: , strictly increasing, and the generalized failure rate strictly increasing (IGFR); the normal, exponential, gamma and Weibull laws qualify. Units cost to produce, sell at the retail price , and are salvaged at .
Expected sales with units available are , and the integrated chain earns . It is maximized at the newsvendor quantity , , with ; the efficiency of a contract is .
A contract is described by the quantity it induces.
Write and (the hazard rate). The retailer's preferred pull contract is and the supplier's preferred push contract is .
A contract Pareto dominates if no firm is worse off and one firm is strictly better off; the Pareto set consists of the contracts no other contract dominates.
A pull contract is only played as pull if the retailer does not prefer to prebook anyway. In the prebook game (§4.5) the retailer prebooks and the supplier then chooses her production to maximize . A pull contract survives the push challenge if the retailer's profit is strictly highest at .
There is a quantity , , the unique positive quantity at which each firm is indifferent between the pull and the push contract, such that
and every pull contract with survives the push challenge.
The theorem says that when both allocations of inventory risk are on the table, neither firm's preferred contract ( for the supplier, for the retailer) is Pareto, and the least efficient Pareto contract, , is more efficient than the least efficient contract of either push-only or pull-only negotiation. In the Pareto set the supplier prefers every pull contract to every push contract and the retailer the reverse, so each firm earns more by bearing the risk itself.
The results are proved in the paper, with the calculus informal, the unimodality of cited, and half of Theorem 6's proof called "analogous". The mission produces a machine-checked version under exactly stated hypotheses; the IGFR concavity and single-crossing facts (Lemma 1, Theorem 2, Lemma 4) are reusable for other contract analyses. No part of this paper is formalized elsewhere; a related platform statement, Snyder–Shen Theorem 14.3 (SupplyChainTheory.wholesale_supplier_unimodal), is the Lariviere–Porteus lemma under stronger assumptions (nonnegative salvage value, finite mean, a continuous positive density, and only a weakly increasing failure rate).
The comparisons are between functions of different shapes: the supplier's push profit is a margin times a quantity, the retailer's pull profit a margin times expected sales. Signing derivatives needs the monotonicity of (Lemma 1), and that fails to be routine at , where need not be differentiable. The set equality compares four profit curves at once, and survival of the push challenge is a statement about a different game, the supplier's best reply to every prebook.
Demand is a probability measure on with = ProbabilityTheory.cdf μ. The predicate DemandModel μ f records , strictly increasing on , on , and for . Differentiability is not required at : the exponential law has a kink there, and it is the paper's own IGFR example. Prices satisfy ; no sign is imposed on . Quantities range over . The paper's is a parameter characterized by , and the first milestone proves it exists and is unique.
Profits are defined in the paper's primitive (quantity, price) forms composed with the inducing prices; the closed forms are milestones, not definitions.
Readings of informal words, each named in the item concerned:
The statement does not follow trivially from a degenerate encoding. The demand assumptions are satisfiable, since the exponential law meets them. , , and are shown to exist inside the statements that use them, and the Pareto set is taken over both modes and every admissible quantity, not only over the claimed interval.
Welcome contributions: basic facts about , and under the demand assumptions, reusable across the series' other two missions.
In the predict-then-optimize framework, a machine-learning model predicts the cost vector of a linear optimization problem , and a decision is made by solving that problem with the prediction. Elmachtoub and Grigas (Smart "Predict, then Optimize", Management Science 2022) proposed judging predictions by the SPO loss, the excess cost of the decision induced by when the true cost is . El Balghiti, Elmachtoub, Grigas and Tewari (arXiv:1905.11488v3) develop generalization bounds for learning with the SPO loss.
The SPO loss is discontinuous in : its value jumps where the optimization problem has several optimal solutions. The paper's sharper bounds (its Theorems 4 and 5) therefore replace the SPO loss by a margin SPO loss that is Lipschitz, and they hold whenever the feasible region satisfies a geometric condition called the strength property. This mission formalizes the paper's first class of feasible regions for which that condition holds: strongly convex sets, such as Euclidean balls and balls with .
Let be a finite-dimensional real vector space with a norm (the paper's with a generic norm). A cost vector is a linear functional on ; its value at is written , and its dual norm is . The closed ball of radius around is .
The feasible region is nonempty, compact and convex. An optimization oracle is any map with and for all ; no tie-breaking rule is fixed.
If is compact, not a singleton, and -strongly convex for some , then for every oracle ,
The strength parameter equals the strong convexity constant.
Theorem 7 is what makes the paper's margin-based bounds usable for a concrete family of feasible regions. It says two things: the strength property holds with , so the Lipschitz constants in the margin analysis are explicit; and , so the margin of a prediction, and with it the empirical margin SPO loss, is as easy to compute as a dual norm. Combined with bounds on the multivariate Rademacher complexity, this gives generalization bounds for strongly convex regions whose dependence on the dimension improves on the paper's Natarajan-dimension bound. In dimension one it recovers the classical margin bounds for binary classification (Example 7, p. 24).
The results are proved in the paper; Proposition 1 is due to Vial (1983). None of them has a machine-checked proof known to this mission, and Mathlib has no notion of a strongly convex set (its StrongConvexOn concerns functions). The mission produces a formal definition of strongly convex sets for a general norm, the normal-cone characterization, and the connection to the predict-then-optimize strength property. It is one of four missions on this paper; the margin-based generalization bound itself is the subject of mission II, and polyhedral regions of mission IV.
Definition 5 speaks about balls around convex combinations, while Proposition 1 is a pointwise inequality with the exact constant . Evaluating the ball inclusion at any single convex combination loses that constant, since the admissible radius and the displacement of the centre both shrink with the mixing weight. Relating a ball to a linear functional also requires the maximum of over a ball to be attained and equal to , a fact about dual norms whose attainment depends on finite dimensionality.
For , comparing with gives only the inequality ; equality needs every nonzero cost vector to have a unique minimizer over . The oracle minimizes, whereas the normal cone is written for maximizers, so the signs in (5) and (8) do not match directly and are a common source of error.
StrongDual ℝ E), so is c w and the operator norm is the dual norm; balls are Metric.closedBall.S.Nontrivial. Proposition 1 and the ball identity carry no compactness hypothesis, as in the paper.Metric.infDist to the degenerate set; the parameter conditions and are hypotheses of the theorems, not parts of the predicates.The k-median problem asks where to open facilities so that the total distance from a set of clients to their nearest open facility is as small as possible. It is a basic model of facility location in operations research (placing depots, warehouses or servers) and of clustering with representative centres, and it is NP-hard, so the question of interest is how close a polynomial-time method can come to the optimum.
Local search is among the most widely used heuristics for it: start from any facilities and repeatedly exchange one open facility for a closed one while the cost decreases. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) gave the first constant-factor guarantee for this heuristic on metric instances: every local optimum of the single-swap local search costs at most five times any solution with facilities. This mission formalizes that result.
Timeline of the relevant bounds:
A metric instance consists of a finite set of clients, a finite set of facilities and a distance on that is nonnegative, symmetric and satisfies the triangle inequality. Write for the cost of serving client by facility .
For a nonempty set of open facilities every client is served by its nearest open facility, and the cost of is
The k-median problem asks for a set of at most facilities of minimum cost.
A swap closes a facility and opens a facility , giving . The neighbourhood of is
and is locally optimum if for every . The local search starts from an arbitrary set of facilities and applies improving swaps until none exists; swaps preserve the number of facilities, so it stops at a locally optimum set of exactly facilities. The locality gap is the supremum, over instances, of the ratio between the cost of a worst local optimum and the optimal cost.
The analysis uses the following notation. For a solution , let assign each client to a nearest facility of , let be the service cost of client , and let be the set of clients served by . For two solutions and put . A facility captures if ; is bad if it captures some and good otherwise.
For every metric instance, every , every locally optimum set of exactly facilities and every nonempty set of at most facilities,
The comparison solution is arbitrary, not an optimum; the statement is the locality gap bound in the form the proof gives.
Theorem 3.2 shows that the simplest exchange heuristic for k-median is a constant-factor approximation on every metric instance, and the paper states that the analysis is tight: its example of §3.5, given for swaps of two facilities, is said to generalize to swaps of facilities, where the bound is 5 for . Combined with the standard device of accepting only swaps that improve the cost by a factor , it yields a polynomial-time -approximation (p. 548). The same capture-and-reassignment argument is reused for multi-swap k-median, for uncapacitated and capacitated facility location in the same paper, and in later work on k-means and on local search for clustering; its milestones (the capture graph and the mapping ) are the reusable part.
The result has been proved since 2001 and is textbook material (Williamson and Shmoys, The Design of Approximation Algorithms, 2011, Chapter 9). No machine-checked proof of it is known; Mathlib has no k-median problem and no locality-gap result for any clustering objective. The work remaining is to formalize the known proof.
The obvious argument adds up the inequalities over a pairing of with , rerouting the clients of the closed facility to the nearest remaining facility. This fails when a single facility of serves most clients of several facilities of : closing it leaves those clients with no nearby open facility, and no bound in terms of follows. The analysis must choose which swaps to consider so that such facilities are never closed, and must reroute the displaced clients of the facilities it does close to a facility other than the closed one while paying only a constant multiple of their own service costs. Both choices must work for arbitrary ties in the nearest-facility assignments and when and share facilities.
Namespace LocalSearchFL.KMedian. Clients and facilities are types Cl, Fa with Fintype and DecidableEq; the distance is a real-valued function on Cl ⊕ Fa with fields for nonnegativity, symmetry and the triangle inequality, and is not assumed. Solutions are Finset Fa. The cost is defined only for nonempty sets, from a nonemptiness proof, so no value is assigned to the empty solution; the goal takes nonempty with S.card = k, which is the paper's . Local optimality quantifies over every swap with and , exactly the neighbourhood of Theorem 3.2, and not only over the swaps with that the proof uses. The inequality is stated multiplied out, , so it is meaningful when .
The milestones quantify over nearest-facility assignments , with arbitrary ties. Capture is stated in integers as . The bijection of is a permutation of all clients fixing every client outside ; in inequality (2) it is a single permutation preserving every . Milestones 1–3 are purely combinatorial and are stated for arbitrary assignments, which contains the paper's case.
A formalization in which local optimality ranges over the swaps , , only, or in which or optimal is assumed, or in which the cost of the empty set is , is a different statement and is ruled out.
A complete development needs the finite-sum and Finset.inf' API of Mathlib, permutations (Equiv.Perm) and finite counting. The capture machinery and the mapping are reusable for the multi-swap and facility location missions of this series. Proofs of individual milestones are welcome independently of the goal.
The bilinear program
with and polyhedra, is one of the recurring nonconvex problems of mathematical programming. It arises from constrained bimatrix games (Mangasarian 1964), dynamic Markovian assignment, multicommodity network flow and certain dynamic production problems (Konno 1971, 1976). Its classical structural fact is that, because the constraints on and on are separate and the objective is linear in each block, an optimal solution can be found at an extreme point of (Falk 1973, doi:10.1007/BF01580119). Vertex-enumeration, extreme-point ranking and cutting-plane methods for the problem rest on that fact.
Al-Khayyal and Falk (Math. Oper. Res. 8(2), 1983) consider the jointly constrained version, in which the feasible region is an arbitrary set of pairs , so that constraints may couple and . They observe that the extreme-point property is then lost, and replace it with a weaker structural fact that survives: a minimum is attained on the boundary of the feasible region. This mission formalizes that result, Theorem 1 of the paper, together with the two examples on p. 274 that delimit it.
Write points of as , and let be a nonempty compact set. No convexity of is assumed. Let be continuous on .
The function is biconcave over (Lean: BiconcaveOn S φ) when both partial functions are concave wherever they live inside : for every fixed , the map is concave on every convex set with ; and for every fixed , the map is concave on every convex set with . Equivalently, is concave along every segment of that is parallel to the -block or to the -block. A bilinear objective with and concave is biconcave; joint concavity of is not required.
The boundary is the topological frontier of in : the closure of minus its interior. A solution of is a point with for all (Lean: IsMinOn φ S z). The Euclidean distance on the product (Lean: eucDist) is .
If () is nonempty and compact, and is continuous on and biconcave over , then
The conclusion is existence of a boundary minimizer. It does not assert that every minimizer lies on (a constant is a counterexample to that).
Theorem 1 is the structural statement that separates jointly constrained bilinear and biconcave programs from their separably constrained special case. It says where a global search may restrict attention, namely to , and example 3 shows that this cannot be sharpened to extreme points once the constraints couple the blocks. Example 4 records that such problems have proper local minima, so a local method alone does not solve them; this motivates the branch-and-bound algorithm of the same paper, which is the subject of the companion mission.
The result is proved in the paper; this mission produces its machine-checked statement and proof. Mathlib contains the Bauer-type principle for jointly concave functions on compact convex sets, but no statement of this kind for biconcave functions on nonconvex sets, and no formalization of Theorem 1 is known. The two examples are small but exact computations, and they certify that the definitions admit the intended instances.
The first idea is to apply the concave-minimization principle: a concave function on a compact convex set attains its minimum at an extreme point. It does not apply. need not be convex, so it has no useful extreme-point structure, and is concave only along segments parallel to one block, so it is not concave along the segment from an interior point to a boundary point in a general direction. Example 3 shows that the conclusion "extreme point" is actually false here.
What remains is local geometry around an interior minimizer: one must find points of around it at which biconcavity can be applied in both blocks, and control their membership in without convexity. The feasibility of the mixed points and , which the paper uses without comment, is where the choice of the Euclidean distance matters, and it is recorded as a separate milestone.
EuclideanSpace ℝ (Fin p) × EuclideanSpace ℝ (Fin q). The boundary is Mathlib's frontier in this product; it does not depend on the norm. Only milestone 1 refers to a distance, and it uses eucDist, the Euclidean distance written out, because Mathlib's default metric on a product is the maximum of the block distances.IsCompact S, S.Nonempty, ContinuousOn φ S (continuity only on ), and BiconcaveOn S φ. One hypothesis is added: . For the space is a point, whose only nonempty subset has empty frontier, so the conclusion fails; the paper works in positive dimension throughout.IsLocalMinOn relative to the box, and non-globality of records the paper's word "proper".IsCompact.exists_mem_frontier_infDist_compl_eq_dist, stated for the ambient metric), the fact that a closed ball about an interior point whose radius is the distance to the frontier lies in the set, and concavity on segments. A lemma that works for an arbitrary norm on the product would be reusable. Contributions of alternative proofs are welcome.Mission Free Energy Principle I published the core variational step of the free energy principle (FEP): whatever recognition density a system carries, the posterior-form variational free energy never undercuts the data's surprisal, the bound is exact at the Bayesian posterior, and equality characterizes the posterior. That mission's shared finite substrate — normalized finite laws, finite kernels, entropy/cross-entropy/KL, and the finite generative model — now exists as platform definitions in the namespace FreeEnergyPrinciple.
The Free Energy Principle II mission formalizes the four structures the FEP literature builds on top of that core, all already machine-checked in the source repository fep_lean / fep_formal (Active Inference Institute):
Timeline of the mathematical content this mission formalizes:
fep_formal (Active Inference Institute): a machine-checked Lean 4 catalogue of 155 FEP topics compiled with zero proof holes against a pinned Mathlib. This mission transcribes the proved modules behind expected free energy, native Markov blankets, the scalar Gaussian filter/VFE, and Bayesian model reduction onto the platform.Two carriers, both fully machine-checked in the source repository:
Definitions.Def_fep_finite_laws, Def_fep_finite_information, and Def_fep_generative_model — no substrate is re-published. Zero-mass atoms are handled by the same totalized conventions as FEP-I: entropy uses Real.negMulLog (so exactly), KL is the nonnegative klFun integrand, and division premises are explicit.gaussianReal/gaussianPDF at a fixed strictly positive variance; the scalar OU prediction and the closed filter update give the posterior mean/variance the recognition family varies over. The native KL between two family members is exactly — proved against Mathlib's log-likelihood-ratio definition.The four definition items of this mission package exactly these carriers:
Def_fep2_expected_free_energy — the predicted state-outcome joint, preference risk, likelihood ambiguity, epistemic value, pragmatic cost, expected free energy (epistemic sign fixed by definition), the full-support contract, and the marginal/product/conditional-entropy/mutual-information lemmas the decomposition needs. Imports FEP-I.Def_fep2_gaussian_vfe — fixed-variance Gaussian family with its exact KL, scalar OU parameters, the exact scalar Gaussian filter (prediction, observation kernel, gain, closed posterior, evidence law), evidence surprisal, and the posterior-form Gaussian variational free energy. Self-contained.Def_fep2_bayesian_model_reduction — posterior odds, Bayes factor, and the model-odds update , with totalized division boundaries kept explicit. Imports FEP-I.Def_fep2_native_blanket — the static blanket factorization, the Dirac-mass embedding of finite laws into native measures, blanket/internal/external coordinates, the conditional-pair kernel, and the marginal/composition identifications the independence proof needs. Imports FEP-I.For every finite generative model, every policy , and every model with full support:
The epistemic-value sign is fixed by definition ( pragmatic cost epistemic value); the decomposition follows from two entropy identities: epistemic value is predicted outcome entropy minus ambiguity, and risk is cross-entropy minus the same entropy (Gibbs' inequality under full reference support). Nonnegativity of follows as a corollary — but the decomposition, not the bound, is the target.
For the exact scalar Gaussian filter, the posterior-form variational free energy at recognition mean is
the exact fixed-variance Gaussian KL (the recognition-to-posterior gap) plus the density-relative evidence surprisal. Equality with the surprisal holds exactly at the posterior mean — the Gaussian analogue of FEP-I's exactness theorem.
Bayes' rule in odds form: at positive evidence,
with the reference prior mass and reference likelihood as exact division premises. The multiplicative Bayes-factor structure (topic fep-120: factorized evidence ratios multiply; sequential model-odds updates agree with one update by product evidence) is available from the same definition layer as a further target.
The embedded static blanket factorization satisfies Mathlib's native CondIndepFun predicate: internal coordinates are conditionally independent of external coordinates given the blanket coordinate. The result is obtained by identifying the authored finite conditional kernels with Mathlib conditional distributions (the embedding preserves marginals and joints exactly on discrete carriers) — not by a finite mutual-information argument.
These four results are the load-bearing extensions of FEP-I's bound: expected free energy converts the variational principle into a theory of action selection; Markov blankets make "internal states" and "external states" well-defined relative to a blanket, which is what lets the FEP talk about self-organizing systems at all; the Gaussian filter is the tractable regime in which the variational machinery becomes the Kalman update; and Bayesian model reduction is the learning/comparison step that updates structure, not just parameters.
Formalizing them. All four families are proved with zero proof holes in the source repository, against a pinned Mathlib; the definition layer here is faithful (same carriers, same totalized conventions, same support contracts made explicit) and every item below compiles locally against the platform environment. The mission's value is reusable community infrastructure: the definition items publish the EFE layer, the Gaussian filter, the odds layer, and the native-blanket embedding in the shared namespace FreeEnergyPrinciple, so later missions (policy trees, collective inference, predictive coding) can import them instead of re-deriving. Status honesty: all eight items below are formalized and machine-checked locally against the platform environment; each is an open problem on the platform only in the sense that no proof has yet been submitted to it.
Committed conventions of this mission's Lean development:
Free Energy Principle I finite substrate (namespace FreeEnergyPrinciple, definitions Def_fep_finite_laws, Def_fep_finite_information, Def_fep_generative_model); this mission adds definition items Def_fep2_expected_free_energy, Def_fep2_gaussian_vfe, Def_fep2_bayesian_model_reduction, and Def_fep2_native_blanket, all in the same namespace.gaussianReal/gaussianPDF, no finite substrate, no manifold geometry, no singular (zero-variance) branch.nextStaticModel construction.How much fluid does a pipe carry for a given pressure drop? For slow, viscous flow the answer is Poiseuille's law, . It is the standard first quantitative model of blood flow in vessels and appears in Lecture 15 ("The Mathematics of Water") of the Drexel biophysics course PHYS 461/561 (Fall 2011), where it is derived from the Navier–Stokes equation and then used to estimate flow speeds in capillaries. The fourth-power dependence on the diameter is what makes small changes in vessel radius matter so much physiologically.
A Newtonian fluid of viscosity flows steadily through a straight cylindrical pipe of diameter and length under a pressure drop . By cylindrical symmetry the velocity is axial, , where is the distance to the axis. The force balance on a thin cylindrical shell (slide 14), integrated along the pipe (slide 15), gives the radial equation
with boundary conditions: finite at the axis, and no slip, , at the wall. The flow rate is and the average velocity is .
Milestones, in order:
Goal (Poiseuille's law): for every pipe flow as above,
The result is classical and completely known; the value of the mission is a clean, machine-checked version of the full chain from the radial ODE and its boundary conditions to the flow-rate formula, rather than just the final integral. The ODE-uniqueness step (milestones 1–2), which uses boundedness at the axis to exclude the logarithmic solution, is the part lecture notes usually wave through.
Milestones 3 and 4 are calculus exercises. The real work is milestones 1–2: turning "integrate twice" into a rigorous statement on an open interval (a function with zero derivative on an interval is constant), and then showing that boundedness near forces (because ) and that continuity plus no-slip at the wall fixes .
All quantities are real. The ODE is imposed pointwise on the open interval with explicit differentiability; "" is encoded as boundedness of on , and the wall condition as plus continuity from inside. are assumed positive in every theorem; is an arbitrary real. The pressure field itself is not modelled: the statements start from the integrated radial equation of slide 15. Two typos on the slides are corrected: slide 15 writes the homogeneous term as (correct: ), and slide 16 prints (correct, as used on slide 17: ). All definitions are in the single definition file MathematicsOfWater_PipeFlow; all declarations use the namespace MathematicsOfWater.
Chapter 26 bounded the rate of uniform convergence by the Rademacher complexity; Chapter 27 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), introduces a second, metric measure of the size of a set of vectors, its covering numbers , the smallest number of Euclidean balls of radius needed to cover , and connects the two through Dudley's chaining. Covering numbers behave well under scaling and under coordinatewise Lipschitz maps (Lemmas 27.2–27.3), they are easily bounded for sets lying in a low-dimensional subspace (Example 27.1), and the chaining lemma turns a bound on at all scales into a bound on (Lemma 27.4), with the clean corollary when (Lemma 27.5). The chapter's example recovers for sets in a -dimensional subspace, the technique that the book says would sharpen the fundamental theorem's sample complexity from to .
For with the Euclidean metric, is an -cover of if every is within distance of some , and is the cardinality of the smallest -cover (Definition 27.1). The Rademacher complexity is Mission XX's. Chaining is run at the scales , , where is a radius of a ball containing , the book's being the smallest such radius.
For a nonempty , , contained in the ball of radius about some , and every integer ,
Example 27.1 (the grid -cover of a set of norm at most in a -dimensional subspace, of size ); Lemma 27.2 (scaling and translation); Lemma 27.3 (the contraction principle); Lemma 27.5 (the corollary of chaining). Further item: Example 27.2 ( for sets in a -dimensional subspace).
Chaining is the standard way to get sharp uniform convergence rates: a single-scale union bound (Massart's lemma at one resolution) loses a logarithmic factor, and summing Massart bounds over a geometric sequence of scales, applied to the increments between successive nearest cover points, recovers it. Lemma 27.4 is the discrete Dudley integral, and Lemma 27.5 is the form in which it is used: any polynomial-in- covering number gives -type bounds without the extra logarithm. On the platform these items complete the complexity toolbox begun in Mission XX and provide covering numbers as a reusable notion; the contraction and scaling lemmas mirror their Rademacher counterparts.
Lemmas 27.2 and 27.3 are immediate: the image of an -cover under the affine map is an -cover, and under a coordinatewise -Lipschitz map a -cover, since ; formally they are manipulations of the infimum in . Example 27.1 needs an orthonormal basis of the subspace (Gram–Schmidt, or Mathlib's orthonormal bases of finite-dimensional inner product subspaces of with the Euclidean structure) and the rounding of coordinates to a grid. Lemma 27.4 is the real work: after centering, take minimal -covers , the near-maximizer of (which depends on ), its nearest points , the telescoping , the bound , and Massart's lemma (Mission XX) on the sets of increments, of cardinality at most ; a formal proof must handle the supremum not being attained (approximate maximizers) and the dependence of all choices on inside the finite average. Lemma 27.5 lets using and . Example 27.2 combines Example 27.1 at the scales with Lemma 27.5, with the book's constant . The book's derivation uses the count without , so a proof needs the volumetric covering bound for and a direct count for .
Vectors are Fin m → ℝ with an explicit Euclidean norm, because Mathlib's norm on that type is the sup norm; covers are arbitrary finsets of and is an infimum in , so no junk value arises when no finite cover exists, and the chaining statements read through ENat.toNat for the bounded sets they concern, where it is finite. Subspaces are Mathlib Submodules with finrank = d. Two statements are given with the constants their proofs support, and the item texts say so. Example 27.1's grid has points per coordinate, so the cover has size , not , which is less than for and cannot bound a covering number of a nonempty set; Example 27.2 correspondingly has in place of . Lemma 27.4 is stated for any enclosing radius about any center, since the proof only uses that is a -cover of ; the book's minimal radius is the special case, and this is the form Example 27.2 needs (with and ). Lemma 27.5 keeps the book's .
Not stated: nothing else is in the chapter beyond the bibliographic remarks.
The book is discriminative almost throughout: it learns predictors, not distributions, following Vapnik's advice not to solve a more general problem as an intermediate step. Chapter 24 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), presents the generative alternative: assume a parametric form for the data distribution and estimate its parameters. The maximum likelihood principle is introduced on Bernoulli and Gaussian samples, shown to be empirical risk minimization for the log-loss, and analyzed through the decomposition of the true log-loss risk into a relative entropy plus an entropy (24.5), which explains both its consistency under a correct model and its overfitting on small samples. Naive Bayes and linear discriminant analysis show how generative assumptions reduce the number of parameters and make the Bayes classifier linear (24.8). The chapter's main theorem concerns the Expectation-Maximization algorithm of Dempster, Laird and Rubin for latent-variable models such as Gaussian mixtures: EM never decreases the log-likelihood (Theorem 24.3), because it is an alternate maximization of a lower bound that touches the likelihood at the posterior (Lemma 24.2). The chapter ends with Bayesian reasoning and the rule of succession.
A Bernoulli sample has log-likelihood and estimator (24.1); a Gaussian sample has . The log-loss is (24.4); on a finite domain, and . A latent-variable model is a parametric joint , , with ; , over the set of row-stochastic matrices, and EM alternates the E-step (24.10) with the M-step (24.11).
For a positive parametric joint , a sample , and any run of EM (each M-step returning some maximizer of ), the log-likelihood never decreases:
Equation (24.2) (Hoeffding for the Bernoulli estimator); the Gaussian maximum likelihood estimates of §24.1.1; Equation (24.5) (the risk decomposition ); Equation (24.8) (the LDA log-likelihood ratio is affine); Lemma 24.2 (EM as alternate maximization of , with and equality at the posterior). Further items: Gibbs' inequality, the Bernoulli maximum likelihood estimator (24.1)/(24.3), Exercise 1 (the biased variance estimate), Equation (24.6), the overfitting example of §24.1.3, Exercise 3 / (24.14), the weighted-centroid M-step (24.13), and the rule of succession of §24.5.
Theorem 24.3 is the guarantee that makes EM a sensible algorithm: it does not find the maximum likelihood estimate, but it climbs monotonically, and Lemma 24.2 identifies why, the E-step chooses the tightest lower bound at the current parameter and the M-step maximizes it. This variational view underlies a large part of modern latent-variable inference. Equation (24.5) is the information-theoretic content of maximum likelihood: the true risk is the entropy of the data plus the relative entropy to the model, so the best parameter is a projection of the data distribution onto the model class, and Gibbs' inequality is what makes that projection meaningful. The Bernoulli and Gaussian computations are the standard first examples, and Equation (24.8) is the reason linear classifiers appear in generative modeling. On the platform, the mission adds the relative entropy on finite domains, the EM objects, and Gaussian-integral identities that later probabilistic work can reuse.
The Bernoulli and Gaussian maximum likelihood facts are calculus, but as global maximization statements they need the concavity of and an explicit completion of squares rather than the book's stationary-point argument; the Gaussian case reduces to minimizing . Equation (24.5) is a finite-sum identity; Gibbs' inequality is Jensen for with the equality case, or the elementary . Lemma 24.2 is Jensen's inequality applied row by row to , with care at entries , where the convention is exactly Lean's junk value; Theorem 24.3 chains the lemma's three parts as the book does. The Gaussian expectation identities (Exercise 1 and (24.6)) require the moments of gaussianReal and Fubini over the product law. Hoeffding's inequality (24.2) is Mission II's Theorem for Bernoulli variables; the overfitting example is the inequality on . The rule of succession is a Beta-function identity provable by integration by parts.
Parametric families are functions from a parameter type to real-valued probabilities or densities, following the book's convention (p. 344) that denotes either; no measure-theoretic densities are needed except in the two Gaussian-integral items, which use gaussianReal and the i.i.d. law of Mission I, and in the two Bernoulli probability items, which use the Bernoulli law of Mission XIV. Lean's log 0 = 0 is handled explicitly: the EM items assume a positive joint, since with junk logarithms Theorem 24.3 is false (the M-step could pick a parameter with a zero component and inflated ), while the entropy terms use the convention that the book intends; the Bernoulli maximum likelihood statement ranges over ; the log-loss decomposition and Gibbs' inequality take the second distribution positive. The M-step is a predicate ("some maximizer"), so Assumption 24.1 is not modeled, and an EM run is any sequence of such steps. The Gaussian maximum likelihood statement requires a nonconstant sample, without which the likelihood is unbounded; the overfitting example is stated for , the range on which the book's inequality holds. Equation (24.8) is stated as a matrix identity for any symmetric in place of ; the soft k-means M-step is stated as the weighted-centroid minimization it amounts to.
Not stated: Naive Bayes (24.7), which is a rewriting of Bayes' rule; the mixture density itself and the E-step formula (24.12); the Bayesian derivations (24.16) and maximum a posteriori estimation; Exercise 2.