Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Paging is the problem of managing a two-level memory: a cache holds of the pages a program uses, every request must find its page in the cache, and a request to a page outside the cache (a page fault) forces the algorithm to bring the page in and evict another. An on-line algorithm chooses what to evict without seeing future requests. Sleator and Tarjan (CACM 1985) measured on-line paging algorithms against the optimal off-line algorithm, which knows the whole request sequence, and showed that no deterministic on-line algorithm can be within a factor smaller than of it.
Randomization changes that picture. Fiat, Karp, Luby, McGeoch, Sleator and Young (J. Algorithms 1991; arXiv:cs/0205038) gave a randomized algorithm, the marking algorithm, whose expected number of faults is within of the optimum, where . This mission formalizes the other half of their paper's picture: no randomized paging algorithm can do better than . The bound says that the logarithmic behaviour is not an artefact of one algorithm but a property of the problem.
Timeline:
Let be a set of vertices with the uniform metric: any two distinct vertices are at distance . A configuration of servers is a map ; server sits at , and a vertex is covered when some server sits on it. A request sequence is a finite list of vertices. A deterministic on-line algorithm assigns to every prefix of requests the configuration after serving it, in such a way that the vertex just requested is covered; its cost on is the total distance travelled by its servers, which on the uniform metric is the number of server moves. Paging with cache slots and pages is exactly this -server problem on uniform vertices.
The optimal off-line cost is the least cost of any schedule of configurations that starts at and covers each request of in turn.
A randomized on-line algorithm is a probability space of coin outcomes together with a deterministic on-line algorithm for each outcome . Its expected cost is the average of the cost of on over . The request sequence is fixed in advance and does not depend on the coins (an oblivious adversary). Following the paper, is -competitive from the initial configuration if there is a constant such that
For the lower-bound argument, the probability vector after a prefix has equal to the probability, over , that vertex is not covered by after serving . A set of marked vertices and the number of unmarked vertices are bookkeeping of the adversary, updated as the marking algorithm would update them.
For , every randomized on-line algorithm with servers on uniform vertices, every initial configuration and every real ,
The case : no randomized algorithm for the uniform -server problem on vertices is -competitive with .
With the probability vector, the marked set, and :
The result. Together with the marking algorithm's upper bound, the corollary pins the randomized competitive ratio of paging to , an exponential improvement over the deterministic ratio that no randomized algorithm can push below . For the marking algorithm itself is -competitive, so Theorem 4 makes it optimal there. The bound is the benchmark every later randomized paging algorithm is measured against, including the -competitive algorithm of McGeoch and Sleator, and it is the uniform-metric base case of the randomized -server conjecture.
Formalizing it. The theorem is proved and classical; no machine-checked proof is known to exist. The platform already has the deterministic bound (KServer.uniform_not_competitive_below_k, ratio ) and a formal Yao averaging principle for randomized -server algorithms (KServer.randomized_yao_averaging), but no randomized paging lower bound. This mission produces the first formal lower bound, stated against the published randomized -server model, and a formal version of the paper's adversary argument. Either route — the paper's adaptive construction of a nemesis sequence from the probability vector, or Raghavan's distributional argument through Yao's principle — is welcome.
The adversary may not look at the coins, yet it must build one fixed sequence against which the expected cost is high in every phase. Requesting an uncovered vertex is not available, since which vertex is uncovered depends on the coins; requesting the vertex with the largest uncovered probability gives only per request and loses the harmonic sum. Lifting the per-phase bound to the asymptotic statement also requires handling the additive constant , the initial configuration of the off-line algorithm, and, for Corollary 5, the reduction from vertices to of them for an algorithm that may still place servers on the others.
The Lean development reuses the published definitions KServer_model (configurations Fin k → M, deterministic on-line algorithms as functions of the request prefix, offlineCost) and KServer_randomized (RandomizedAlgorithm: a probability measure on coin outcomes, a deterministic algorithm per outcome, measurable costs; expCost as a lower Lebesgue integral in ; IsCompetitiveFrom C₀ c: every drawn algorithm starts at and there is one constant , fixed before the sequence, with expCost σ ≤ ENNReal.ofReal (c * offlineCost C₀ σ + a)). The clamp at in ENNReal.ofReal only weakens the property the goal refutes. The vertex set is an abstract type with an equivalence Fin n ≃ M and the uniform metric as a hypothesis, never the line metric of Fin n. is Mathlib's harmonic k cast to . The goal quantifies over every algorithm and every initial configuration, with no laziness or distinct-positions assumption, and over every real , including .
A formalization in which competitiveness is vacuous (a model with no algorithms, or a cost that is always infinite), in which the adversary may choose the sequence after seeing the coins, or which fixes or the additive constant, would be a different statement and is ruled out by the published definitions used here.
The probability vector is the one new definition, uncoveredProb A σ i. Milestones about it assume the uncovered events measurable, the standing convention that is a probability; the model itself only guarantees measurable costs. The milestone assumes the servers occupy distinct vertices, as in the paper; in general . The arithmetic milestones are stated for an arbitrary probability vector on a finite set. Reusable pieces: the probability vector and the cost lemma apply to any randomized -server algorithm on a uniform metric, and a restriction lemma (from vertices to ) would serve other paging lower bounds.
Paging is the problem of managing a two-level memory: a fast cache holding pages and a slow memory holding the rest. When a requested page is not in the cache (a page fault), it must be brought in and, if the cache is full, some page must be evicted. An on-line paging algorithm decides which page to evict without knowing future requests. Sleator and Tarjan (CACM 1985) compared on-line algorithms with the optimal off-line algorithm on every request sequence and showed that the best deterministic algorithms (LRU, FIFO) lose a factor of exactly , and that no deterministic on-line algorithm does better.
Randomization changes this picture. Fiat, Karp, Luby, McGeoch, Sleator and Young (J. Algorithms 1991; arXiv:cs/0205038) showed that the randomized marking algorithm is -competitive, where , and that no randomized algorithm is better than -competitive. For the marking algorithm does not reach , already for and . For two servers the same paper gives a different algorithm, EATR ("end after twice requested"), and proves it -competitive. Since , EATR is strongly competitive for : no randomized algorithm has a smaller competitive factor. This mission formalizes that result.
Timeline:
The uniform -server problem has a finite set of vertices, any two distinct vertices at distance , and two servers. A request sequence is a list of vertices; each request must be covered by a server when it is served, and the cost is the number of server moves. This is paging with a cache of two pages: vertices are pages and the covered vertices are the cache.
A deterministic algorithm has a cost ; a randomized algorithm has an expected cost , averaged over its random choices. is -competitive if there is a constant such that for every request sequence and every deterministic algorithm (on-line or off-line),
Algorithm EATR. The servers start on the vertices and . The algorithm divides into phases; the first phase starts at the first request to a vertex other than and . Let be the set of vertices occupied by the servers at the end of the previous phase ( before the first phase). During a phase, a vertex is clean if it is not in and has not been requested during this phase; a vertex is stale if it is neither clean nor the most recently requested vertex . EATR keeps one server on and the other uniformly at random on the stale set. When a stale vertex is requested, the servers are placed on and and the phase ends; the next phase starts at the next request to a vertex not covered by a server. Requests between phases, and repeated requests to , move nothing.
For a phase, denotes the number of clean vertices requested in it. For a deterministic algorithm , and denote the numbers of 's servers that do not coincide with any of EATR's servers at the beginning and at the end of the phase. An algorithm is lazy if it moves no server on a request to a covered vertex and exactly one server on a request to an uncovered one.
With the optimal off-line cost of serving from the servers' starting position , there is a constant such that for all
The constant is left free; the factor is the paper's and is optimal.
The result. Theorem 3 settles the randomized competitive ratio of paging with two cache slots: combined with the paper's lower bound (Corollary 5, the subject of a companion mission), the optimal factor for is exactly , against for every deterministic algorithm. The general case was settled later by McGeoch and Sleator's -competitive partitioning algorithm, which is considerably more complicated.
Formalizing it. The result has been proved since 1991; no machine-checked proof of it is on the platform (a search for EATR, randomized paging and two-server results on 2026-09-26 found only deterministic -server theorems). The mission produces a formal model of a randomized on-line algorithm as a probability distribution over states evolving with the request sequence, a formal treatment of the phase decomposition and of the telescoping amortization that relates expected on-line cost to the optimal off-line cost, and a first strongly competitive randomized paging result on the platform, alongside the deterministic -server results already there.
The per-phase computations are short. The main difficulty is the global accounting. The adversary's cost in a phase is bounded only in amortized form, , where and compare the adversary's servers with EATR's at the phase boundaries; the bound becomes a statement about only after the and terms telescope across phases. This needs care with the requests that lie outside every phase (before the first phase, between phases, and in an unfinished last phase), during which the adversary may move. A further difficulty is that the off-line optimum ranges over arbitrary schedules, which may move several servers on one request, while the phase bound is proved for lazy on-line algorithms: the reduction from one to the other must be made explicit. Finally, the uniform law of the stale server is an invariant of a Markov chain on states that must be tracked through the whole phase.
The vertices are an abstract metric space with an enumeration , , and the hypothesis that distinct points are at distance ; the metric of is not used. The starting vertices are . is KServer.offlineCost of the published KServer model: the infimum of total movement over all schedules serving from . Comparing with this infimum covers every deterministic starting from EATR's position; a starting elsewhere differs by at most , which the constant absorbs. The constant is quantified before .
EATR is a PMF over states: a deterministic record (the set , whether a phase is in progress, the last requested vertex, the vertices requested in the phase) and the random position of the second server. Its expected cost is the expected number of server moves, summed over the requests. The paper fixes only that the second server is uniform on the stale set; when a clean request enlarges the stale set, the formalization moves one server by a fixed coupling that keeps the law uniform, and this choice is stated in the definition. A formalization that defines EATR's expected cost by the closed formula of the proof, or that restricts to complete phases, would make the goal a different statement; neither is done here. The pre-phase prefix and an unfinished last phase belong to and are covered by the constant.
Needed infrastructure: finite probability distributions (Mathlib's PMF), the published KServer model and its laziness theorem, and bookkeeping lemmas on the deterministic phase record. The phase record and the amortization argument are reusable for the marking algorithm of the companion mission. Proofs of any milestone, and alternative decompositions of the goal, are welcome.
A risk measure assigns to a random financial position a capital requirement : the amount of cash that must be added to to make it acceptable. The axiomatic theory of convex risk measures (Föllmer–Schied 2002; Frittelli–Rosazza Gianin 2002) treats this number as computed with no information beyond the model. In practice a regulator or a risk manager revises the requirement as information arrives, so the requirement becomes a random variable measurable with respect to the information available at the time of measurement. Detlefsen and Scandolo (SFB 649 Discussion Paper 2005-006; published in Finance and Stochastics 9(4), 2005, doi:10.1007/s00780-005-0159-6) develop this conditional theory: axioms, a robust representation, and a treatment of dynamic risk measurement.
The entropic risk measure is the standard example of a convex risk measure that is not coherent. It is the capital requirement of an agent with exponential utility , and its penalty function in the robust representation is the relative entropy (Föllmer–Schied, Stochastic Finance, Example 4.60, as cited by the paper). Section 5 of the paper carries this example to the conditional setting and shows that its penalty is a conditional relative entropy. The same identity appears in dynamic entropic risk measures, exponential-utility indifference pricing and recursive utility, where one-period conditional entropic measures are composed over time.
Fix a probability space and a sub--algebra , the information available at the time of measurement. is the space of essentially bounded random variables and its -measurable part. All equalities and inequalities between random variables hold -almost surely.
A conditional convex risk measure is a map that is translation invariant ( for ), monotone (), conditionally convex ( for , ), and satisfies .
The relevant probability models are
The essential supremum of a family of -valued random variables is the a.s. smallest random variable that dominates every member a.s.; the essential infimum is defined symmetrically. The minimal penalty of is
For a risk aversion , the conditional entropic risk measure is
the capital requirement for the acceptance set . For with density , the conditional relative entropy is
For every :
The first identity is representability with the minimal penalty as the penalty; the second identifies that penalty.
The result gives the conditional entropic risk measure an explicit dual description: the capital requirement is a worst case over conditional models, each penalized by its conditional relative entropy. This duality is what makes entropic risk measures computable in dynamic settings. Recursive compositions of over a filtration are time consistent, and their penalties add up by the chain rule for conditional relative entropy. Lemma 5.5 is also the conditional form of the Donsker–Varadhan (Gibbs) variational principle, which is used on its own in large deviations and in PAC-Bayesian bounds.
On status: the results are proved in the paper, and the unconditional versions are textbook material. Mathlib has unconditional Kullback–Leibler divergence, tilted measures, conditional Jensen's inequality and a -valued conditional expectation. As far as the platform search could establish, neither the conditional relative entropy nor the conditional Donsker–Varadhan formula nor any conditional risk measure has been formalized. This mission produces the first machine-checked conditional version, with allowed to be infinite.
In the unconditional case both sides of Lemma 5.5 are numbers, and the supremum is a supremum over reals. Conditionally, both sides are random variables. The supremum over the uncountable family indexed by must be taken in the essential sense, and a pointwise supremum is neither measurable nor meaningful. The conditional relative entropy can be on a set of positive probability. The integrand need not be integrable, so the usual conditional expectation of is not available for it, and the "" direction must reach an unbounded target through bounded test variables while controlling at the same time. The ess.sup in the goal ranges over measures, not random variables, and each is a conditional expectation under a different measure. These are identified with -a.s. objects through the condition on .
IsProbabilityMeasure P), and is m : MeasurableSpace Ω with hm : m ≤ mΩ. Payoffs are real functions with MemLp X ⊤ P. membership is StronglyMeasurable[m] plus MemLp ⊤. Every (in)equality between random variables is -a.e.P[·|m] and Q[·|m]. Bounded variables are integrable under every , so no junk value arises.Q.rnDeriv P. and are generalized conditional expectations, , built from Mathlib's -valued condLExp and valued in EReal. The negative parts are integrable, so never arises. In EReal, a real number minus is , which is how a model with infinite entropy drops out of the supremum.IsEssSup, IsEssInf) on a candidate -a.e. measurable EReal-valued function. The candidate must dominate every member a.s. and lie a.s. below every a.s. upper bound.P[φ * log φ | m] (which returns when is not integrable) or through a pointwise supremum would make the goal false or vacuous, and so would stating it for an abstract convex risk measure in place of . The formalization uses the extended-valued , the essential supremum, and the explicit .CondConvexRisk.Entropic and does not assume the general representation theorem (Theorem 3.2). The generalized conditional expectation and the conditional Donsker–Varadhan formula are reusable beyond risk measures. Contributions are welcome on the ess.sup API (existence, upward-directed families), on conditional monotone convergence for condExp, and on the conditional Jensen step for .Gradient descent needs a step size, and the classical choices each ask for something the user may not have. A constant step needs the Lipschitz constant of the gradient, which is rarely known and often pessimistic. Backtracking needs repeated function evaluations. The exact line search needs a one-dimensional minimization at every iteration. Fatkhullin and Polyak (arXiv:2004.09875v2, SIAM J. Control Optim. 2021, doi:10.1137/20M1329858) proposed a step size for the static linear-quadratic regulator (their rule (4.8), §4.3, p. 11). In §6.1 they point out that the same rule applies to any smooth unconstrained problem . The rule divides the squared gradient norm by the Hessian quadratic form along the gradient. It needs one Hessian–vector product per iteration and neither nor the strong convexity constant . In the paper's LQR experiment (§5, Figure 8, p. 13) the algorithm built on this step converges much faster than gradient descent with a constant step tuned at the first iterations.
The paper proves the method converges linearly for strongly convex functions (Theorem 6.1, p. 13). The proof takes one page (Appendix D.4, p. 19). This mission formalizes that theorem. It is the third mission of a series on this paper; the other two concern the LQR gradient method and gradient flow, and this one uses none of their control-theoretic objects.
Let be twice differentiable, with gradient and Hessian . Three constants describe it.
Let be the global minimizer of . The Hessian step size at a point is
the minimizer of the second-order Taylor model of along . The method (6.1) runs
from a starting point . The damped method with factor runs . For a quadratic the method (6.1) is steepest descent with exact line search.
Under the hypotheses above:
The constants are the paper's, stated exactly.
Theorem 6.1 gives a rate for a step size computed from local second-order information alone. Part 1 says that near the minimizer the method converges at least as fast as gradient descent with step , with no step-size parameter to tune. Part 2 gives convergence from every starting point, at the price of knowing a lower bound on for the damping. The same step appears in the paper's LQR method (rule (4.8)) and in gradient projection methods (p. 13, citing [37]), so the one-step inequalities are reusable beyond this theorem.
The result is proved in the paper. As of this writing none of it has a machine-checked proof. The formal work is the full development: the cubic Taylor bound from a Lipschitz second derivative on , the two one-step inequalities, and the inductions that give the rates.
The obvious argument for gradient descent uses the quadratic upper bound and a step no larger than . The Hessian step can be as large as , far outside that range, so the quadratic bound in the Euclidean norm gives no decrease. Two different replacements are needed. For the undamped method, the cubic Taylor error must be controlled along the whole trajectory, and condition (6.2) is imposed only on : the proof must show the gradient stays small enough at every later iterate. For the damped method, the upper bound must be measured in the local Hessian norm (D.1), which trades the step's size for the condition number .
On the Lean side, Mathlib has Taylor's theorem in one variable. The cubic bound for a function on with a Lipschitz Fréchet second derivative must be assembled from it or from the integral form along a segment. Mathlib has no ready-made link between strong convexity and a lower bound on the Hessian either.
The space is EuclideanSpace ℝ (Fin n). The gradient is Mathlib's gradient f. The Hessian quadratic form is fderiv ℝ (fderiv ℝ f) x v v. Twice differentiability is differentiability of f and of fderiv ℝ f everywhere. The Lipschitz constant of the Hessian is in the operator norm of the bilinear map, not the Frobenius norm. Strong convexity is StrongConvexOn Set.univ μ f with 0 < μ; Mathlib's modulus is . and are real constants in the Lipschitz inequalities. The minimizer is a hypothesis ( for all ), not constructed.
Deviations from the page, all recorded in the items' Formalization Notes:
At a stationary point the step is ; Lean evaluates it to , so the method stays at the minimizer, and both rates remain true.
The iterates are those of the defined recursions (6.1) and its damped version. A statement about an arbitrary sequence satisfying a descent inequality would be a different, weaker theorem and does not discharge the goal. Condition (6.2) is imposed on only; a version assuming it at every iterate is also not the goal.
Contributions welcome: the multivariate cubic Taylor bound (reusable wherever a Lipschitz Hessian appears, e.g. in cubic regularization of Newton's method); the Hessian bounds from strong convexity and a Lipschitz gradient; and the inequality .
A buyer and a seller negotiate over a single indivisible good. Each knows how much the good is worth to them, but not how much it is worth to the other side. Whether the two will trade, and at what price, then depends on how each party shades its offer to exploit the other's uncertainty. Chatterjee and Samuelson (Bargaining under Incomplete Information, Operations Research 31(5), 1983) modelled this situation as a one-shot game in which both parties submit sealed offers simultaneously, and characterised its Bayesian equilibria.
The model became the standard reference point for bilateral trade with two-sided private information. Myerson and Satterthwaite (J. Econ. Theory 29, 1983) showed that no mechanism can guarantee efficient trade in this setting, and that the equilibrium of the Chatterjee–Samuelson game with and uniform values attains the second-best efficiency bound. Later work on the -double auction (Satterthwaite and Williams, J. Econ. Theory 48, 1989; Leininger, Linhart and Radner, J. Econ. Theory 48, 1989) studies the continuum of equilibria of exactly this game. The object of the present mission, a pair of linked differential equations, is the tool these papers use to construct and classify equilibria.
A seller has reservation price and a buyer has reservation price . Each knows their own value. The buyer's belief about is a probability measure with distribution function ; the seller's belief about is with distribution function . The subscript names the player who holds the belief, not the variable. Each belief is regular: , , and is strictly increasing and differentiable on the value interval, with density (respectively ).
Under the Bargaining Rule, the seller asks and the buyer offers simultaneously. If the good is sold at for a fixed ; otherwise nothing happens. Profits are for the seller and for the buyer on trade, and zero otherwise.
An offer strategy is a function (for the seller) or (for the buyer) from values to offers. Against , a buyer with value offering earns in expectation
and symmetrically . The pair is an equilibrium if maximises over all real offers for every buyer value , and maximises for every seller value .
A strategy is of class if its offers are bounded, it is nondecreasing, it is strictly increasing except where it sits at its lowest offer or its highest offer , and it is differentiable wherever its offer lies strictly between and . A class equilibrium is an equilibrium in which both strategies are of class .
In a class equilibrium, wherever the seller's strategy is strictly increasing around and the buyer value offers ,
and wherever the buyer's strategy is strictly increasing around and the seller value asks ,
The paper writes in (3a) and in (3b).
The milestones assume (respectively ), which the paper's formula for the offer density needs. The goal does not assume it.
Theorem 2 reduces the search for equilibria to the analysis of a pair of ordinary differential equations. Every explicit equilibrium in the paper and in the later -double-auction literature is found as a solution of (3a)–(3b) with suitable boundary conditions: the linear equilibrium for uniform beliefs (the paper's Example 1), the one-parameter families of Satterthwaite–Williams, and the non-linear equilibria of Leininger–Linhart–Radner. The equations also expose how the split parameter distributes bargaining power: at equation (3b) forces the seller to ask their own value, and at equation (3a) forces the buyer to bid theirs.
The result is proved in the paper. To the best of a search of the platform, no formalization of it or of the bargaining model exists. This mission produces a machine-checked version of the necessary conditions. Its definitions of beliefs, expected profits, equilibrium and class are also the basis for companion missions on the uniform linear equilibrium and its trade probability.
The paper's proof is four lines: differentiate the expected profit, set the derivative to zero, substitute. Three steps of that argument do not survive a careful reading.
First, the paper differentiates under an offer density that exists only if is strictly increasing and has a positive derivative. Class allows to be flat at its bounds, to jump between them, and to have zero derivative. The formal goal assumes none of this. It must handle the case , where the offer distribution has an infinite density at and the first-order condition becomes a one-sided argument.
Second, identifying with requires that no seller value outside a neighbourhood of makes the same offer. That is a global statement about , and it is where monotonicity on the whole interval and the "flat only at the bounds" clause of class enter.
Third, the first-order condition needs the equilibrium offer to be an interior maximiser of a function of that is differentiable there. The profit is an integral over the belief, and its differentiability at must be derived from the differentiability of at the single point and of . Neither nor is assumed continuous elsewhere.
Values, offers and are real numbers. Beliefs are probability measures on , with distribution function Mathlib's ProbabilityTheory.cdf. Expected profits are Bochner integrals over the opponent's value, not over an offer density. The two agree whenever the density exists, and the integral form needs none. Integrability is not assumed: for a class strategy and a regular belief supported on the value interval, the integrand is bounded and almost everywhere measurable. Ties () trade. Deviations range over all real offers. Strategies are arbitrary functions whose values outside the value interval play no role.
The derivative is deriv S y. The paper's inverses and are not introduced as functions. The matching value is a universally quantified variable with , so no junk value of an inverse can make an equation true or false. The equations are asserted only at values interior to an open subinterval on which is strictly increasing. A formalization that assumed the first-order condition, or restricted to strategies with everywhere, would be a different and weaker theorem.
A complete development needs: differentiation of parametric integrals of indicator type (the derivative of ), the change of variables from values to offers under a strictly increasing strategy, and Fermat's rule (IsLocalMax.hasDerivAt_eq_zero). The first two are reusable for auctions and other Bayesian games with monotone strategies. Proofs of the milestones, alternative proofs of the goal, and general lemmas about monotone strategies are welcome.
The gradient projection method minimizes a continuously differentiable function over a closed convex set by alternating a gradient step with a projection back onto the set. It was proposed by Goldstein (1964) and by Levitin and Polyak (1966), and it is the basic step of many algorithms for bound constrained and linearly constrained optimization, including large-scale quadratic programming codes.
The classical convergence results either need a Lipschitz constant for the gradient to choose the step (Goldstein; Levitin–Polyak), or assume a bounded sequence of iterates and conclude only that limit points are stationary (Bertsekas, 1976, for the Armijo rule on a box; Dunn, 1981). Calamai and Moré (1987) introduced a general step-size rule that contains the Armijo procedure, and proved a convergence statement that needs no boundedness of the iterates: the projected gradients tend to zero. This statement is what later results on finite identification of the active constraints use as their hypothesis, so it is the natural entry point to the paper.
Let be a finite-dimensional real inner product space with norm , let be nonempty, closed and convex, and let be continuously differentiable on , with gradient taken with respect to the inner product. The problem is
A run of the gradient projection method is a pair of sequences , with , and , where . For fixed constants and , the steps satisfy the sufficient decrease condition
and the condition that the step is not too small: either , or for some at which sufficient decrease fails,
In Lean these objects are proj, projGrad and IsGradientProjectionRun in the namespace CalamaiMore.Convergence, together with the shared definitions tangentCone and IsStationaryPoint in CalamaiMore.Shared.
If, in addition, the steps are bounded, for some constant (3.2), is bounded below on , and is uniformly continuous on , then
No boundedness of is assumed, and no specific step rule beyond (2.1)–(2.3).
By Lemma 3.1, vanishes exactly at stationary points, so Theorem 3.2 says that the method approaches stationarity in a quantitative sense even when the iterates are unbounded. With Lemma 3.3 it gives that every limit point is stationary. For polyhedral it is the hypothesis of the paper's Theorem 4.1: any sequence with converging to a nondegenerate point identifies the active constraints in finitely many iterations, which is the basis of active-set methods that switch between gradient projection steps and subspace minimization.
The results are proved in the paper. To our knowledge they have no machine-checked proof. This mission produces a formal account of the gradient projection method with a general step rule, a reusable projected gradient and tangent cone on a general finite-dimensional inner product space, and the standard projection estimates of §2, which are also the starting point of the paper's other two main results.
The obvious argument fails at two places. First, the continuity of cannot be used: the map is not continuous, and can be bounded away from zero in every neighborhood of a stationary point, because the tangent cone changes discontinuously at the boundary of . So with stationary does not by itself force , and here the iterates need not converge at all. Second, the steps may tend to zero along a subsequence; the step rule gives information only through a trial step , at a point other than , and comparing the two projected steps is where the argument must work.
The space is a type E with [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]; is Mathlib's gradient f. "Continuously differentiable on " is ∀ x ∈ Ω, DifferentiableAt ℝ f x together with ContinuousOn (gradient f) Ω. Bounded below is BddBelow (f '' Ω), uniform continuity is UniformContinuousOn (gradient f) Ω. Sequences are ℕ → E indexed from ; a subsequence is an infinite K : Set ℕ with limits along atTop ⊓ 𝓟 K; a limit point is a MapClusterPt. The projection and the projected gradient are total functions through a nearest-point map that returns when no nearest point exists; every theorem assumes nonempty, closed and convex, and evaluates only at points of , where the nearest point exists and is unique. The step rule is a predicate on the pair of sequences, so the theorems cover every rule satisfying (2.1)–(2.3); the auxiliary condition , which the paper uses only to show that an admissible step exists, is not imposed.
The run predicate is satisfiable: for a constant , the constant sequence with is a run, so the goal is not vacuous. A formalization that states the goal for an arbitrary map in place of the projection, drops the bound , or replaces by proves a different theorem and is not accepted.
Contributions welcome: the projection estimates (reusable for any projection-based method), existence and uniqueness of the projected gradient, the characterization of stationarity, and the two limit theorems.
Integer programs are routinely solved by first solving their linear programming (LP) relaxation and then searching for an integer optimum near the fractional one. How near an integer optimum must be is the subject of proximity theorems. They bound the search region of branch-and-bound and of dynamic programming, and they turn a fractional optimum into a starting point for exact algorithms.
The classical bound is due to Cook, Gerards, Schrijver and Tardos (Math. Programming 34, 1986): for an integer program in inequality form that is feasible and bounded, every optimal LP solution has an optimal integer solution with , where is the largest absolute value of a subdeterminant of . For programs in standard form with rows this gives, via the Hadamard bound, , which grows with the number of variables .
Eisenbrand and Weismantel (ACM Trans. Algorithms 16(1), Article 5, 2019; conference version SODA 2018) removed the dependence on altogether, using the Steinitz lemma on rearranging vectors so that all partial sums stay short. Their bound depends only on and on the largest absolute value of an entry of , and it is the basis of their faster algorithms for integer programs with few constraints.
Fix natural numbers (rows) and (variables). The data are a matrix , a right-hand side , an objective and upper bounds . A natural number bounds the entries: for all . The integer program (10) is
and its LP relaxation is the same problem over . Its feasible region is a polytope, lpPolytope A b u. An optimal vertex solution is an optimal solution of the LP relaxation (IsLPOptimal) that is an extreme point of . An optimal integer solution is IsIPOptimal. Both are maxima.
Distances are measured in the -norm .
A vector is a cycle of (Eq. (14)) if and, for every , and : an integer kernel vector that is sign-compatible with and dominated by it (IsCycle).
The Steinitz lemma (Theorem 1.1) concerns vectors in an -dimensional normed space with and . It asserts a permutation with for all , and the paper uses Sevast'anov's constant .
If (10) has an integer feasible point and is an optimal vertex solution of its LP relaxation, then there is an optimal solution of (10) with
The constant is the paper's. The goal holds for all , , , and ; only and enter the bound.
The bound is independent of the number of variables. Combined with the paper's dynamic program, it gives the paper's running-time results for integer programs with upper bounds: an optimal LP vertex is computed, and the integer optimum is searched for within an -ball of radius around it. Eq. (21) bounds the absolute integrality gap by the same quantity, scaled by . The Steinitz lemma with constant is a general tool in discrepancy theory and in scheduling algorithms.
All of these results have published proofs. No machine-checked proof of Theorem 3.3 or of the Steinitz lemma is known to this mission, and Mathlib has no Steinitz lemma. The mission asks for complete Lean proofs of the milestones and of the goal. A proof of the Steinitz lemma with constant for arbitrary norms is reusable well beyond integer programming.
Lemmas 3.1 and 3.2 and the counting step are elementary. The substance lies in two places. The first is the Steinitz lemma with the linear constant for an arbitrary norm: the bound must hold uniformly in the number of vectors, and the constant must be exactly , because the goal's constant counts integer points of -norm at most . The second is the passage from a vertex to at most fractional coordinates. The paper argues this in one sentence (" has at most positive entries"), which is not literally true for (10) with upper bounds: coordinates at their upper bound are positive. The correct fact concerns coordinates strictly between and , and it has to be derived from the extreme-point property of .
IPProximity.Eisenbrand. The data are integral: A : Matrix (Fin m) (Fin n) ℤ, b : Fin m → ℤ, c : Fin n → ℤ, u : Fin n → ℕ (entries allowed), Δ : ℕ. They are cast to ℝ once, inside the LP definitions. and are allowed.Set.extremePoints ℝ (lpPolytope A b u). It is not defined through bases or by counting fractional coordinates.∑ i, |(z i : ℝ) - x i|. Mathlib's norm on Fin n → ℝ is the sup norm, and it is used only where the paper has (the of Eq. (21)).Contributions welcome: proofs of any milestone, in particular the Steinitz lemma, and a proof of the goal from the milestones.
The maximum flow problem asks how much of a commodity can be sent from a source to a sink through a network whose arcs have capacities. It underlies bipartite matching, transportation, scheduling and many reductions in combinatorial optimization. The classical method for it, the labeling method of Ford and Fulkerson (Flows in Networks, 1962), repeatedly finds an augmenting path and pushes flow along it. With integer capacities it terminates, but the number of augmentations can be as large as the maximum flow value itself, and Edmonds and Karp exhibit a four-node network on which this happens (p. 250). With irrational capacities the method need not terminate at all.
Edmonds and Karp, Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems, J. ACM 19(2):248–264, 1972 (doi:10.1145/321694.321699), showed that two simple rules for choosing the augmenting path repair this. The first, augmenting along a path with fewest arcs, is the subject of mission 1 of this series. This mission covers the second (§1.3): augment along a path that gives the largest possible augmentation. For integer capacities the number of augmentations then grows only logarithmically in the maximum flow value.
A network has a finite set of nodes, a source and a sink , and a set of arcs, ordered pairs with , at most one from each node to another. One arc is the return arc ; the other arcs form the set , and each has a capacity . A flow is a nonnegative function on the arcs of with on and flow conservation at every node, and included. Its value is , the flow returned along the return arc; a maximum flow has the largest value among all flows, and denotes that value.
The residual network has an arc whenever and , or and . An augmenting path is a directed path of distinct nodes in . Each of its arcs has a residual amount , equal to , , or according to which of , lie in , and the path's augmentation is . Augmenting increases by and changes the flow on the arcs of the path accordingly, with the paper's own rule when both and are arcs. The labeling method produces flows by augmenting along a path relative to as long as one exists.
The rule studied here chooses, at every step, an augmenting path whose is at least that of every other augmenting path relative to the current flow. The bound involves an integer such that every partition of the nodes into and has at most arcs of with one end on each side.
For a network with integer capacities, as above, and a run of the labeling method with maximum augmentations started from an integer-valued flow,
and if no augmenting path relative to exists, then is a maximum flow.
The milestone list follows the paper's argument:
Theorem 2 was among the first bounds showing that a maximum flow algorithm can be made polynomial in the size of the numbers rather than in their values: since and is at most times the average capacity, the bound is in terms of the number of nodes and the average capacity (p. 254). The largest-augmentation rule, often called the fattest-path or maximum-capacity augmenting path rule, is a standard textbook variant, and its geometric-decrease argument is the model for later capacity-scaling methods, including the scaling algorithm for the Hitchcock problem in §2 of the same paper (mission 3 of this series).
The theorem has been proved since 1972 and appears in standard texts. As far as a platform search shows (2026-09-26), no machine-checked proof of it exists on Prove2Me. The platform does contain LinearOptimization.max_flow_min_cut and LinearOptimization.max_flow_ford_fulkerson_integer_termination, which state max-flow min-cut and termination of the generic method in a different network model (parallel arcs, extended nonnegative capacities, no return arc); they give no count of augmentations and are related work only. This mission would contribute a formal proof of the counting bound together with the general labeling-method facts (milestones 1–3), which mission 1 needs as well.
The obvious argument, that each augmentation raises the value by at least 1, gives only the bound , and on the four-node example of p. 250 that bound is attained by an arbitrary choice of paths. The logarithmic bound needs a lower bound on the size of the largest augmentation in terms of the remaining gap . The largest augmentation is defined by comparison with all augmenting paths relative to the current flow, while the gap is a global quantity of the network, and neither integrality nor the maximum-augmentation rule alone controls it. Milestone 2's converse, that a non-maximum flow always admits an augmenting path, is itself the max-flow min-cut theorem in this model, and the formal proof has to establish it for the paper's return-arc model rather than import it from a different one.
V with decidable equality. A : Finset (V × V) contains no loops and not . Capacities are real, c : V → V → ℝ, positive on A. Integrality is the hypothesis IntegralCaps N, and for the initial flow IsIntegralOn N (f 0) (integer values on the arcs of , the return arc included).V → V → ℝ constrained only on the arcs of . A maximum flow is the predicate IsMaxFlow, comparing with every flow, not a supremum. The goal takes a maximum flow g as a hypothesis and sets ; every network has one.IsMaxAugRun N K f P. Its initial flow is arbitrary except for integrality, and each later flow is the augmentation of the previous one along a path of maximum among all augmenting paths.CrossArcsBounded N M counts the arcs of , return arc included, with one end on each side of every – partition. This is the literal reading of p. 253.(K : ℝ) ≤ 1 + Real.logb ((M : ℝ) / ((M : ℝ) - 1)) (g N.t N.s) with a natural number. When , Real.logb gives and the bound reads . The contraction factor is 1 - (M : ℝ)⁻¹.Von Neumann's minimax theorem says that in a zero-sum game with real payoffs, Player I can guarantee an expected gain of at least the value and Player II can hold it to at most . In a long series of plays, the law of large numbers turns this into a statement about the average payoff: I can make it exceed , II can keep it below , with probability approaching one.
Blackwell's 1956 paper asks the same question when the payoff of each play is a vector in rather than a number. A single player then cannot optimize "the" payoff, and the natural question becomes geometric: can a player force the running average of the payoff vectors to converge to a prescribed set , whatever the opponent does? The resulting notion, approachability, became a basic tool in repeated games with incomplete information (Aumann–Maschler), in the theory of calibration and regret minimization (Foster–Vohra; Hart–Mas-Colell), and in online learning, where no-regret algorithms and Blackwell approachability are known to be equivalent (Abernethy–Bartlett–Hazan 2011).
Timeline.
Fix integers and , and a closed, bounded, convex set . The game is an matrix whose entries are probability distributions concentrated on . Write for the mean of , for the simplex of mixed actions of Player I, and for that of Player II.
A strategy of I is a sequence of measurable maps from the -tuples of past outcomes to ; is a point of . Strategies of II take values in . A play of is a sequence of random vectors such that, given , the players draw and independently from and , and is drawn from . The average payoff is , and is its distance from .
A set is approachable with if for every there is such that for every strategy of II,
It is excludable with if there is such that for every there is such that for every strategy of I,
is approachable (excludable) if some strategy approaches (excludes) it. Finally, for and ,
is the set of expected payoffs I can guarantee to stay in by playing , and the set II can confine them to by playing .
For a closed convex set ,
and if then is excludable with the stationary strategy . In particular every closed convex set is either approachable or excludable. Both sentences are part of the goal.
The result. THEOREM 3 is the vector analogue of the minimax theorem. For a closed convex target it reduces an infinite-horizon stochastic question, about every strategy of the opponent over all histories, to a finite family of one-shot conditions on the mean matrix , and it shows that the game is determined for convex targets: one of the two players always wins. Its sufficient condition, THEOREM 1, is the origin of the "Blackwell strategy", which steers the average toward the target by playing, at each step, a mixed action that pushes the expected next payoff across the supporting hyperplane. Regret-matching, calibration algorithms and the reductions between online linear optimization and approachability are instances of this construction.
Formalizing it. The result is proved in the paper; to the best of available knowledge no machine-checked proof of it exists. This mission produces one: the stochastic model of a repeated game with vector payoffs, the probabilistic estimates (THEOREM 2 and the LEMMA) with the uniform rate the paper claims, and the minimax reduction for convex sets. A related platform mission, Introduction to Online Convex Optimization XIII, states a deterministic, sufficiency-only textbook variant for bounded sets; the present mission covers the stochastic model, unbounded convex targets, and the excludability half.
The obvious argument shows that the expected squared distance decreases like . That is not approachability: the definition asks for the probability that the average is ever again -far after time , uniformly over the opponent's strategies. Controlling the whole tail of the path, with a threshold that does not depend on the opponent, is the step that fails for a naive expectation bound and is why the paper needs a maximal inequality for sums with negative conditional drift. On the geometric side, the "only if" direction is not automatic: it requires that approachability and excludability be incompatible, which in turn requires that a play of every pair of strategies exists.
Points live in EuclideanSpace ℝ (Fin N); pure actions are Fin r and Fin s; mixed actions are elements of stdSimplex. The game is a structure carrying (closed, bounded, convex) and the distributions (probability measures with ). A play is described by the conditional law of the next outcome given the past, and approachability and excludability quantify over every probability space in Type carrying such a play. Distances are extended (Metric.infEDist), equal to to the empty set.
Conventions and disclosed additions:
is not assumed bounded or nonempty. With the real-valued distance, the empty set would be approachable with every strategy and THEOREM 3 would be false; the extended distance rules this out. Stating only the sufficiency direction, fixing the approaching strategy in the hypotheses, or assuming a play exists would each trivialize the goal, and none is done.
A complete development needs: conditional laws of the next outcome from a strategy pair (Ionescu–Tulcea, Kernel.traj in Mathlib), a nonnegative-supermartingale maximal inequality, the metric projection onto closed convex sets, and the minimax theorem (Mathlib's Sion theorem). The maximal inequality of THEOREM 2 and the LEMMA are reusable beyond this mission. Contributions to any milestone, and to a construction of plays, are welcome.
The Steiner problem in graphs asks for the cheapest way to connect a prescribed set of nodes of a network, where intermediate nodes may be used freely. It is the network version of the classical Euclidean Steiner tree problem surveyed by Gilbert and Pollak (SIAM J. Appl. Math. 16, 1968), and it arises wherever a few sites must be joined through an existing network at minimum total cost: communication and pipeline layout, VLSI routing, and phylogenetics. With two terminals it is the shortest-path problem; with all nodes as terminals it is the minimum spanning tree problem; in between it is NP-hard.
Dreyfus and Wagner (Networks 1(3):195–207, 1971) gave the first exact algorithm whose running time is exponential only in the number of terminals and polynomial in the number of nodes. The paper states it, as Algorithm A, together with its proof of correctness and an exact count of its elementary operations.
Timeline. 1968: Gilbert and Pollak survey Steiner minimal trees. 1971: Dreyfus and Wagner, a dynamic program over subsets of terminals running in time proportional to . 1987: Erickson, Monma and Veinott give the same subset recursion for general network flow problems. 2007: Björklund, Husfeldt, Kaski and Koivisto (STOC 2007) improve the exponential dependence on for small integer weights. The Dreyfus–Wagner recursion remains the standard exact method and the basis of the fixed-parameter tractability of the problem in .
A graph has a finite set of nodes and a set of undirected arcs, each arc having a positive length ; is connected. For a set of arcs, . A set connects a node set if all members of are joined by paths composed only of arcs in .
Given , a Steiner path (or Steiner tree) connecting is a set that connects with minimum. Its length is the Steiner length . For nodes , is the length of a shortest path from to ; .
Algorithm A fixes a linear order of (so that each nonempty set has a first element ), picks , sets , and fills a table for nonempty and :
and returns
A minimum over an empty set is . In the Lean development these objects are steinerLength, pathDist, tableA and algorithmA in the namespace DreyfusWagner.Steiner.
For every finite connected graph with positive arc lengths, every linear order on its nodes, every with and every ,
This is the caption of Algorithm A ("Computes the length of the Steiner tree connecting ", p. 203). The statement is an equality, not a bound.
In the order the proof uses them:
Two companion items accompany the goal: the numerical illustration of §3 (seven nodes, , Algorithm A returns ), and the exact count of elementary statements of §5, .
The result turns the Steiner problem with few terminals into a polynomial computation in the size of the network: for fixed the running time is including all-pairs shortest paths. It is the reference exact algorithm against which heuristics and approximation algorithms for Steiner trees are evaluated, a standard example of dynamic programming over subsets, and the origin of the fixed-parameter tractability of the Steiner tree problem parameterized by the number of terminals. The subset recurrence reappears in group Steiner, prize-collecting and directed Steiner variants.
The paper's proof is complete and the result is classical; it has not, to our knowledge, been machine-checked. This mission produces a checked account of the exactness of the recursion: the structural facts about minimum connecting arc sets (acyclicity, optimality of branches, the three-way decomposition) and the passage from these to the algorithm's table. These facts about weighted graphs, minimum connecting arc sets and shortest paths are reusable well beyond this paper.
The upper bound is routine: each term of each minimum is the length of some connecting arc set, so no term can beat the optimum. The content is the reverse inequality, which needs the Optimal Decomposition Theorem: one must show that some optimal tree actually splits at a single node into a shortest path to and two optimal subtrees whose terminal sets partition into two nonempty parts. The naive choice fails when is a leaf, and the choice of the first branching node fails when the path from meets another terminal first; the paper handles these as separate cases. A second difficulty is the passage from arc sets to trees: minimum connecting sets are forests only because lengths are positive, and "the arcs of involved in connecting" a set of terminals must be identified with a subtree. Finally the table recursion must be matched with the recurrence, including the restriction that enumerates each splitting once.
Nodes are a finite type V with a LinearOrder (the paper's "(ordered) set"; the goal holds for every order). The graph is a SimpleGraph V with decidable adjacency, arcs are unordered pairs Sym2 V, and lengths are ℓ : Sym2 V → ℝ. Every theorem assumes the paper's standing hypotheses of p. 195: all arcs of have positive length (∀ e ∈ G.edgeSet, 0 < ℓ e) and is connected. The paper allows several arcs between the same two nodes; the simple-graph model keeps one, which does not change any Steiner length since an optimal set uses only the shortest of parallel arcs. Connecting means reachability in the graph formed by the arcs of . Steiner lengths, and all minima of the algorithm take values in WithTop ℝ, where ⊤ is , ⊤ + x = ⊤ and an empty minimum is ⊤; no real-valued infimum with a junk value is used. is a minimum over paths of .
The goal assumes , the paper's own hypothesis (Appendix A, p. 205). For Algorithm A as printed returns because line (18) admits no set ; the two-node case is covered by milestone 2. The algorithm is defined from , addition and minima only: a formalization in which tableA or algorithmA refers to Steiner lengths, or in which the goal only asserts , would be trivial and is ruled out. The loop order of lines (4)–(14) is replaced by recursion on , which the paper states is immaterial (p. 203).
Useful infrastructure: sums of lengths along walks and paths, reachability in edge-subgraphs, acyclicity of minimum connecting sets, and splitting a tree at a node. Contributions of these as reusable lemmas are welcome, as are proofs of individual milestones in any order. Tree reconstruction (§2, p. 200) and the empirical running times (p. 205) are out of scope.
Infinite-horizon sequential decision problems (deterministic optimal control, Markov decision processes, minimax control) share one computational question: does the dynamic programming (DP) algorithm, which starts from a terminal cost and repeatedly applies the Bellman operator, converge to the optimal cost? For discounted problems with bounded costs the answer is yes, by the contraction mapping theorem (Blackwell 1965; Denardo 1967). Without discounting and boundedness the answer depends on the sign structure of the problem. Strauch's negative programming model (Strauch 1966) and Blackwell's positive programming model behave differently, and in the former the DP algorithm can fail to converge to the optimal cost even for simple deterministic problems.
Bertsekas (1977) recast these models in one abstract framework: a monotone mapping that encodes the one-stage problem, with no probabilistic or additive structure assumed. Two sign conditions organise the theory: uniform increase (Assumption I, containing Strauch's model) and uniform decrease (Assumption D, containing the deterministic version of Blackwell's positive model, e.g. deterministic problems with nonpositive stage costs). This mission formalizes the uniform-decrease half of Section 5: under D, the finite-horizon problems are solved by the DP algorithm, is the limit of the finite-horizon values, Bellman's equation holds, and the DP algorithm converges to . The same framework became the basis of Bertsekas–Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978) and of Bertsekas's Abstract Dynamic Programming (2013, 3rd ed. 2022).
States, controls, policies. (nonempty) and are sets. Each has a nonempty constraint set . is the set of selectors with for all , and a policy is a sequence of selectors. The policy is stationary if for all .
Functions and the mapping . is the set of functions , ordered pointwise, and is the constant function . A mapping is given, and it is monotone: implies for every and . It defines
is the -fold composition, with the identity, and applies first.
Costs. A terminal function with is given. The cost of a policy, the optimal cost, the -stage optimal cost and the limit of the DP algorithm are
all pointwise. denotes the cost of the stationary policy .
Assumptions. D: for all , . Under D every sequence above is nonincreasing, so the limits exist in . D.1: for every sequence with , . D.2: there is such that for all and .
If D holds, and either D.1 holds or for every , then
The goal is the paper's answer, in the uniform-decrease case, to the question it poses in the introduction: when is ?
The result. Proposition 9 justifies value iteration from for every problem that fits Assumption D, including deterministic and stochastic control with nonpositive costs (reward maximization with nonnegative rewards) and minimax problems satisfying D.1. Propositions 6 and 8 characterise as the largest solution of Bellman's equation below and give a verification test for stationary policies. The hypotheses are sharp in the sense the paper documents: its Counterexamples 2 and 3 show when D.1 is dropped together with D.2 or with the finiteness condition . Under the mirror assumption I, can fail, so the asymmetry between the two sign conditions is part of the content.
Formalizing it. All results are proved in the 1977 paper and reappear in later monographs. No machine-checked version of this abstract framework is known. The platform's existing dynamic programming items are finite-state, real-valued and contraction-based, so this mission would add the first formal treatment of extended-real-valued, non-contractive dynamic programming, and a model definition that other results of the same theory can reuse.
The obvious argument for Proposition 9, " and ", hides two separate interchanges of limits and infima. Lemma 1 interchanges with , which works only because every sequence is monotone in the right direction under D. Proposition 3 is where the work is: the -stage infimum over policies must be matched by the iterated infimum , which requires building near-optimal selectors stage by stage and passing a limit through times, using D.1, or controlling accumulated errors through D.2. The latter breaks down when values reach , which is why that branch needs . All arithmetic is in , where expressions such as are not defined, and , , may equal even though does not.
The model is a Lean structure MonotoneDP.Decrease.Model S C with fields U, U_nonempty, H, mono, Jbar, Jbar_ne_bot and S_nonempty; is S → EReal. Policies are ℕ → Selector, where a selector is a function with values in the constraint sets. is an infimum over U x only, and , are infima over admissible policies. and are limUnder atTop; every theorem assumes D, under which both sequences are nonincreasing and converge, so these are the paper's limits. In D.1 both limits are limUnder. D.2 carries its scalar as a parameter, and "D.2 holds" is ∃ α, AssumptionD2 α. Only real scalars are ever subtracted from extended reals.
is defined for every , and Propositions 3 and 9 quantify over as the paper does. In Proposition 3 the condition belongs to the D.2 branch only. No hypothesis beyond the page is added. Nonempty constraint sets and are the paper's standing assumptions, stated in the model, not in the theorems. Without nonempty constraint sets there would be no policies, and would be , and several statements would hold trivially; the model rules this out.
Useful contributions: general lemmas about monotone sequences in EReal (interchanging ⨅ and limits), the monotonicity facts (25) and under D, and reusable constructions of near-optimal selectors. Corollary 6.1 (the finite-state D.2 variant) is not included.
Many problems in convex optimization, variational inequalities and signal processing reduce to finding a zero of a sum of three monotone operators, one of which is single-valued and smooth. Davis and Yin (Set-Valued Var. Anal. 25, 2017) introduced a splitting scheme that evaluates each of the three operators separately: the two set-valued ones through their resolvents, the single-valued one through a forward step. With a fixed stepsize, their Algorithm 1 converges weakly but can be slow: the paper's Section 3.4 constructs examples where the squared distance of the iterates to the solution decays no faster than for every .
When one of the operators is strongly monotone (for example the subdifferential of a strongly convex function), first-order splitting methods can be accelerated by letting the stepsize shrink like ; the paper relates its stepsizes to those of Chambolle and Pock's accelerated primal–dual method (J. Math. Imaging Vis. 40, 2011, Algorithm 2) and of Boţ, Csetnek, Heinrich and Hendrich (Math. Program. 150, 2015, Algorithm 5). Section 3.3 of Davis–Yin carries this device over to three-operator splitting and obtains an rate for the squared distance. This mission formalizes that result.
Let be a real Hilbert space. A set-valued operator is monotone if for all , , and maximal monotone if its graph is not properly contained in the graph of another monotone operator. It is -strongly monotone if for all such pairs. A single-valued is -cocoercive if , and -Lipschitz if .
The problem is to find , that is, , where , are maximal monotone and is monotone and single-valued. For the resolvent is the map with .
Algorithm 3 fixes stepsizes and an initial point , sets , , and iterates for
The stepsize changes in the middle of an iteration. Two stepsize rules are considered, each defined recursively from :
Let be -strongly monotone with .
The goal asserts the shape of the rate only; the constant is not fixed.
The theorem shows that strong monotonicity of or can be converted into a quadratically decaying distance bound without knowledge of the solution, with stepsizes that are computable from the strong monotonicity and cocoercivity (or Lipschitz) constants alone. Since the rate is established for , it applies directly to splitting schemes for strongly convex composite problems with smooth, where is the proximal point of .
The result is proved in the paper; no machine-checked version is known. The formalization adds a precise statement of the admissible parameter ranges, a check of the index conventions of a scheme whose stepsize changes mid-iteration, and a correction of the one-step inequalities at the first iteration (see Formalization scope). The stepsize limits are statements about explicit real recursions and are of independent use for other accelerated schemes.
The one-step inequalities (3.9) and (3.10) are long but elementary chains of inner-product identities and Young's inequality; the work lies in bookkeeping two stepsizes per iteration. The rate itself does not follow from the one-step inequality alone: telescoping gives a bound of the form , and one must then show decays exactly like . The rules (3.6) and (3.7) are nonlinear recursions without closed form, so their asymptotics require a Stolz–Cesàro type argument, which is not available in Mathlib under that name. Choosing a stepsize sequence of the form instead is a different algorithm and not covered by the theorem.
InnerProductSpace ℝ H, CompleteSpace H), not a Euclidean space.JA JB : ℝ → H → H required to satisfy the resolvent inclusion for every ; for maximal monotone operators such maps exist and are unique, so nothing is lost.Contributions are welcome at every level: proofs of the real-sequence milestones (a general Stolz–Cesàro lemma would be reusable well beyond this mission), of the two one-step inequalities, and of the telescoping argument that assembles the goal.
Conic quadratic problems (also called second-order cone programs) arise directly in applications such as contact problems with Coulomb friction, and a wide range of nonlinear convex problems can be rewritten in this form (Lobo, Vandenberghe, Boyd and Lebret 1998). Interior-point methods solve them in polynomial time, but around 2000 the available software for conic quadratic problems handled far fewer variables than linear programming software. Ben-Tal and Nemirovski (2001) therefore asked whether a conic quadratic problem can be replaced by a linear program of comparable size. Their construction replaces each second-order cone by a polyhedral cone that is exact up to a factor . The feasible set of the resulting linear program, projected back to the original variables, lies between the feasible set of the original problem and that of its -relaxation.
This sandwich is only useful if the relaxed problem is close to the original one, and in general it is not: the paper notes that (CQP) can be infeasible while every relaxation with is feasible. Proposition 4.1 of the paper, the target of this mission, gives a sufficient condition under which the two feasible sets are -close.
For let be the Euclidean norm. A conic quadratic problem in the variable is
where is a matrix and (the inequality is componentwise), and for each the matrix is , , and . For the -relaxation is
denotes the feasible set of a problem ; in Lean these are feas P and feasRelaxed P ε, subsets of Fin n → ℝ, for a problem datum P : CQP n k₀ m.
Two conditions on (CQP) are used.
IsStrictlyFeasible P x̄ r).IsSemibounded P R).Put .
If (CQP) has conic constraints and is strictly feasible and semibounded, then for every with ,
The left-hand side is the image of under , not a Minkowski sum.
The milestones follow the paper's proof in order.
The result. Proposition 4.1 turns the qualitative sandwich "exact ⊆ polyhedral ⊆ relaxed" into a quantitative statement. When a problem is strictly feasible with margin and its conic right-hand sides are bounded by on the feasible set, the relaxed feasible set, shrunk towards by , lies inside the exact one. The error of the relaxation is thus controlled by , which is linear in . Together with the paper's main theorem, that a polyhedral -approximation of the Lorentz cone with variables and inequalities exists, this measures how well a linear program of moderate size approximates the conic problem. The paper uses it this way for the examples in its introduction.
The formalization. The proposition is proved in the paper; no machine-checked version is known. This mission produces a Lean formalization of conic quadratic problems and their relaxations with the Euclidean norm, together with the strict feasibility and semiboundedness conditions and the proof. The Lorentz-cone approximation results of the same paper are the subject of the companion missions I and II of this series.
The right inclusion is immediate. The left inclusion does not follow from convexity alone. A relaxed-feasible point may violate every conic constraint of (CQP), and nothing about bounds how far it is from . The needed information comes from semiboundedness, which constrains only feasible points of (CQP). That hypothesis therefore cannot be applied to itself, and the shrink factor must be obtained without any bound on given in advance. The obvious attempt, bounding the violation at by , fails for exactly this reason.
Fin n → ℝ; the conic constraints are indexed by Fin m (0-based) with a dependent family of matrices (ℓ : Fin m) → Matrix (Fin (k ℓ)) (Fin n) ℝ, so the row sizes may differ. The norm is written out as eucNorm y = √(∑ i, y i ^ 2); Mathlib's norm on Fin k → ℝ is the sup norm and is not used.IsStrictlyFeasible states.eucNorm, or a transfer to EuclideanSpace ℝ (Fin k)) and linearity of Matrix.mulVec and dotProduct. A convexity lemma for feas P would be reusable beyond this mission, and contributions of it are welcome.A linear program is solved with known data, but in planning problems the data are often only known in distribution when the main decision is taken: demands, yields and requirements are revealed later, and a corrective action is taken after they are. E. M. L. Beale's 1955 paper On Minimizing a Convex Function Subject to Linear Inequalities formulates this situation in its §5, "Linear Programming with Random Coefficients", as what is now called a two-stage stochastic linear program with recourse. Beale's motivating example is the transportation problem of Hitchcock (1941) with random requirements at the destinations, where every unit of shortage or excess incurs a loss. The same model was put forward in the same year by Dantzig, Linear Programming under Uncertainty (Management Science, 1955), as the paper's note added in proof acknowledges.
Timeline:
Constants , and an matrix are given. The data , an matrix, and are random variables on a probability space : their distribution is known when the first-stage decision , , is chosen, and their values are known when the second-stage decision , , is chosen. The cost is
For a right-hand side the second-stage value is
and for fixed data the cost of a first-stage decision is . The expected cost is
The problem is to choose minimising . In Lean the value is secondStageValue D f b, the cost is cost c f D A β x, and the expected cost is expectedCost P c f D A β x, all in the namespace BealeConvexMin.RandomLP.
Assume that for every the second-stage minimum is attained for almost every outcome and that is integrable. Then
that is, is convex on the non-negative orthant. The statement fixes no distribution class: it is claimed for any known distribution of .
The result. Theorem 2 is the basic structural fact of two-stage stochastic linear programming: the first-stage problem is a convex program in , whatever the distribution of the data. It is what makes local optimality global for the first-stage problem, what justifies cutting-plane and decomposition methods that approximate from below by supporting hyperplanes, and what makes sample-average approximations convex programs. Theorem 3, joint convexity in the data, gives through Jensen's inequality the comparison between the stochastic problem and its mean-value problem that Beale draws on p. 182. The discrete reformulation (5.5)–(5.6) is the deterministic-equivalent linear program used for finitely many scenarios.
Formalizing it. The theorems are proved in the paper, and their content is classical. The mission produces machine-checked statements of the model with its implicit hypotheses made explicit (attainment of the second stage, integrability of the cost), and proofs of the three results in Lean. The platform already has related statements in other models (finite scenario sets with extended-real recourse, and a complete-recourse, finite-second-moment version); none has Beale's hypotheses, and none states convexity of for an arbitrary distribution.
The mathematics is short; the difficulty is in the encoding. The second-stage value is a minimum that may fail to exist: the second stage may be infeasible for some and some outcomes, or unbounded below. A real-valued infimum then takes an arbitrary default value, and convexity would become a statement about that default. Similarly, the mean value only exists when the cost is integrable. A faithful statement has to carry attainment and integrability exactly where the paper tacitly assumes them, on the domain the paper uses, and no stronger condition (such as complete recourse or moment bounds) that the paper does not make. In the discrete reformulation, the minimum over the whole family has to be matched with the probability-weighted sum of per-scenario minima.
Fin n → ℝ, matrices Matrix (Fin m) (Fin n) ℝ, inner products dotProduct, and is the componentwise order. The random data are functions A : Ω → Matrix (Fin m) (Fin n) ℝ and β : Ω → Fin m → ℝ on a measurable space with a probability measure P; no measurability of the data is assumed beyond integrability of the cost.Many computations in scientific computing, statistics and machine learning need the trace of a matrix that is never formed explicitly: may be for a large sparse , an inverse , or a product of operators, and the only access to it is the ability to compute products for chosen vectors . Examples are log-determinant estimation in Gaussian process regression, counting triangles in graphs through , computing charge densities in electronic structure calculations, and generalized cross-validation in regularized regression. For such matrices the diagonal entries are not available, and computing them one at a time costs matrix–vector products.
Randomized trace estimators replace this by a small number of products: draw random vectors from a fixed distribution with and average the quadratic forms. Hutchinson (1989) introduced the estimator with Rademacher vectors and computed its variance; Silver and Röder (1997) used Gaussian vectors. Before Avron and Toledo (2011), the analyses of these estimators were variance computations, which do not say how many samples guarantee a given relative accuracy with a given probability. Avron and Toledo gave the first such sample bounds for several estimators, stated in terms of an guarantee; this mission formalizes their bound for the Gaussian estimator. Later work (Roosta-Khorasani and Ascher 2015; Cortinovis and Kressner 2022) sharpened these bounds and extended them to indefinite matrices.
Let be symmetric positive semi-definite, and write . Fix a number of samples . Let be random vectors whose entries are independent standard normal random variables. The Gaussian trace estimator (Definition 3.1) is
Each term has expectation , so is unbiased. A randomized trace estimator is an -approximator of (Definition 4.1) if
that is, if its relative error is at most except on an event of probability at most .
The analysis uses the eigenvalues of , listed with multiplicity, and the polynomial , where ranges over subsets of ; it satisfies .
For every symmetric positive semi-definite , every , every and every natural number with
the estimator is an -approximator of . The sample count depends on neither nor .
The theorem gives a number of matrix–vector products, , that suffices for a relative-error guarantee on the trace of any positive semi-definite matrix, independent of its dimension and spectrum. It is the reference row of the paper's Table I, against which the Hutchinson, normalized Rayleigh-quotient and unit-vector estimators are compared, and it is the form in which trace estimation enters the analysis of randomized algorithms for log-determinants, spectral densities and matrix functions.
The result is proved in the paper; to our knowledge it has not been formalized in any proof assistant. The mission produces a machine-checked version with the constant and the range of made explicit, and with the misprints of the printed argument resolved (see Formalization scope). It also produces reusable pieces: the moment generating function of a Gaussian quadratic form, and the bound on elementary symmetric sums by powers of the power sum. Sharper constants, the removal of the restriction , or a direct formalization of the lower tail through a tail bound are welcome as further theorems.
Unbiasedness and the variance formula do not give the result: Chebyshev's inequality with yields , with a polynomial rather than logarithmic dependence on . A logarithmic bound needs exponential moments of , and the exponential moment of is finite only for below ; the argument has to choose inside that range uniformly in the spectrum, using only . The second obstacle is distributional: is not a sum of independent terms in the coordinates of , and reducing it to a weighted sum of independent variables requires the rotation invariance of the standard Gaussian vector. The paper proves only the upper tail with an explicit constant and states that the lower tail follows "using the same technique"; that step has to be supplied.
Matrices are Matrix (Fin n) (Fin n) ℝ; "symmetric positive semi-definite" is A.PosSemidef, "symmetric" is A.IsHermitian, and eigenvalues are Matrix.IsHermitian.eigenvalues. The sample space is Fin M → Fin n → ℝ with the product measure of copies of gaussianReal 0 1, so the law of the samples is constructed, not assumed; . Probabilities are Measure.real; the moment generating function is Mathlib's mgf; the variance is Mathlib's variance, and Lemma 5.1 asserts square integrability so that neither the integral nor the variance takes its default value. The sample count is a natural number ; and are real.
Corrections of the printed text, each recorded in the item's Formalization Note:
A formalization that makes the goal trivial is ruled out: the estimator's law is the explicit product Gaussian measure rather than a hypothesis, ranges over all natural numbers above the threshold, and the approximator predicate is evaluated on the genuine event .
A complete development needs rotation invariance of the standard Gaussian on (Mathlib's stdGaussian_map), the moment generating function of a squared standard normal, independence of products of Gaussian vectors, and a Chernoff bound from the moment generating function. The Gaussian quadratic-form results (milestones 1 and 2) are reusable for the other Gaussian estimators of the paper, such as the rank estimator of Lemma 5.3. Proofs of any milestone, alternative proofs of the lower tail, and helper lemmas on moment generating functions are welcome.
Retailers of fashion and seasonal goods sell at a premium price early in the season and mark down later. When customers anticipate the markdown, some of them wait, and the seller's pricing problem becomes a game between the seller and a population of forward-looking (strategic) customers. Aviv and Pazgal (MSOM 10(3), 2008) study this game in a model with limited inventory, stochastic arrivals and valuations that decline over the season, under two classes of seller policies: contingent pricing, where the discount depends on the inventory left, and announced fixed-discount pricing, where the seller commits to both prices upfront. Their numerical study (§7.3) compares the two classes and finds that precommitment can raise expected revenue by up to about 8%.
That comparison needs, for every announced price path, the customers' equilibrium response. Theorem 2 of the paper (p. 348) supplies it: a threshold purchasing policy, pinned down by a scalar fixed-point equation for the probability that a waiting customer is served. This mission formalizes Theorem 2. A companion mission of the same series formalizes Theorem 1, the contingent-pricing counterpart.
A seller has units to sell over a season , split at a fixed time with . Customers arrive by a Poisson process with rate . Customer has a base valuation drawn from a continuous distribution (tail ), and at time values the product at , where the decline factor is common to all customers.
Under an announced price path the seller commits to a premium price on and a discount price from on; does not depend on the remaining inventory. Customers know the initial inventory but not the current one.
A customer arriving at buys immediately if and only if (i) the current surplus is nonnegative and (ii) it is at least the expected surplus of waiting,
where is the probability that a unit will be allocated to the customer at time . Units left at are rationed at random among the customers who request one.
For a threshold function on the paper defines three segment rates: , the expected number of customers who buy at ; , those who could buy at but wait and want to buy at ; and , those whose valuation was below and who want to buy at . Each is times an integral over of at scaled prices (p. 345). With the Poisson probabilities, the allocation probability of units is
For let
and suppose solves
Then, when all other customers use (so that a waiting customer is served with the probability on the right of (8)), every customer arriving at buys immediately if and only if : the symmetric threshold profile is a Nash equilibrium.
Theorem 2 reduces the customers' equilibrium under an announced path to a single scalar . Everything downstream in §5 and §7 rests on it: the seller's expected revenue (p. 348) is written in terms of , the seller's optimal announced path maximizes it, and the comparison between announced and contingent pricing uses the resulting value . The theorem also explains the qualitative prediction of the model: the threshold exceeds exactly when the announced discount is deep relative to the decline of valuations, and it rises with the perceived availability .
The result is proved in the paper; to the best of our search it has no machine-checked proof. A formal development contributes the model objects (segment rates for threshold policies, the allocation probability for random rationing among Poisson requesters) in a form reusable by the rest of the series and by other strategic-customer pricing models, and a checked proof of the equilibrium property. The existence of a solution to (8) is not proved in the paper and is a natural further target.
The best-response part of the argument is elementary once the availability is known. The substance of the statement lies in the availability itself: the probability that a waiting customer is served is not a free parameter but the one generated, through (8), by the other customers' use of the same threshold. A formalization must connect the segment rates, the Poisson counts and random rationing into one expression and keep the fixed-point coupling between and intact; dropping it turns the theorem into a one-line inequality about an arbitrary . The division by also degenerates when and , and has to be excluded explicitly.
The Lean development lives in namespace SeasonalPricing.Announced. Conventions:
μ : Measure ℝ with IsProbabilityMeasure μ, = ProbabilityTheory.cdf μ, and continuity of (the paper's "continuous distribution") is a hypothesis of the goal. No support condition on is imposed; the statement quantifies over every real base valuation .tsum) as printed, not its closed form.availability is the right-hand side of (8), with built from by (7).Readings of the paper's informal words:
A formalization in which is an arbitrary number in , not tied to (8), is ruled out: it is the best-response lemma alone, not Theorem 2. Contributions welcome: proofs of the two milestones and the goal; lemmas such as and summability of its series; the closed form of printed on p. 346; and an existence result for (8).
In high-dimensional regression the number of candidate predictors can far exceed the number of observations . A regression function can then be estimated only if it is well approximated by a combination of a few elements of a large dictionary. The Lasso is the most widely used estimator in this regime. The question this mission formalizes is how well the Lasso predicts when the truth is not assumed to be sparse, or even to lie in the span of the dictionary.
A sparsity oracle inequality answers it. It bounds the prediction error of the estimator by the error of the best sparse approximation of the truth, which only an oracle knowing the truth could compute, plus a remainder proportional to the sparsity of that approximation times . Bickel, Ritov and Tsybakov (arXiv:0801.1095, Ann. Statist. 37(4), 2009) proved such an inequality for the Lasso under their restricted eigenvalue (RE) condition. Earlier oracle inequalities for Lasso-type estimators in fixed design (Bunea, Tsybakov and Wegkamp, 2006–2007) required the Gram matrix to be positive definite or to satisfy a mutual-coherence condition. The RE condition is weaker and allows , and it is now the standard hypothesis in this literature.
A dictionary is evaluated at fixed points . This gives the design matrix and, for an unknown regression function , the vector . The observations are
Nothing is assumed about . For the empirical norm is , and for we write . The column norms are assumed nonzero, with and . The support of is and its sparsity is .
The Lasso is any minimiser of
and .
Assumption RE holds with constant if, for every with and every with ,
The paper's is the largest such constant.
Fix , , , , and let RE hold with constant . With probability at least , every Lasso solution satisfies, simultaneously for all with ,
The theorem says that, up to the factor and a remainder of order , the Lasso predicts as well as the best -sparse linear combination of the dictionary. This is the case even when is not sparse and not in the span of the dictionary. The remainder is the parametric rate for parameters, inflated by and by the ill-posedness factor . Together with Theorem 5.1 of the same paper (mission II of this series), it shows that the Lasso and the Dantzig selector are within the same distance of the sparse oracle. The oracle inequality is used in aggregation, in model selection, and as a black box in later sparse-estimation papers.
The result is proved in the paper. It has not been formalized: at the time of writing, no Lasso oracle inequality and no probabilistic Lasso bound exist on Prove2Me or in Mathlib. What this mission contributes is a machine-checked proof of the paper's Theorem 6.1 with an explicit constant . The paper leaves unspecified, and its proof fixes the value used here. The mission also formalizes the Gaussian-tail step (B.4) and the deterministic basic inequality (B.1), both of which are shared with the paper's other Lasso results.
There is no sparse truth, so the usual argument does not apply. That argument places the error in the RE cone and reads off a rate. Here the competitor is arbitrary, and the approximation error can dominate the penalty terms, in which case the error is not in the cone. The RE assumption can be used only where the error does lie in a cone, and the cone constant available there depends on and on the column-norm ratio , because the penalty is weighted while RE is stated for unweighted vectors. What RE then yields is an inequality quadratic in with a cross term, not the form directly, and the constant is determined by how that cross term is absorbed. On the probabilistic side, the whole argument must run on one event of probability at least . That event may depend neither on nor on the choice of minimiser. The Lasso need not have a unique solution.
Matrix (Fin n) (Fin M) ℝ) and the target only through , which is arbitrary. The noise is a family W : Fin n → Ω → ℝ of measurable, independent random variables, each with law gaussianReal 0 σ², and .In high-dimensional linear regression one observes with a design matrix whose number of columns may far exceed the sample size . The two standard estimators of a sparse , the Lasso (Tibshirani, 1996) and the Dantzig selector (Candès and Tao, 2007), both come with error bounds of order for an -sparse , but only under a condition on : since has a non-trivial kernel when , some form of restricted invertibility is unavoidable.
Bickel, Ritov and Tsybakov (arXiv:0801.1095, Ann. Statist. 2009) introduced the restricted eigenvalue (RE) condition, which asks for invertibility of only on a cone of approximately sparse vectors. It is weaker than the conditions used before it and has since become the default assumption in the sparse-estimation literature. Section 4 of the paper relates RE to the earlier conditions:
This mission formalizes those implications.
Fix integers and and a matrix with columns . The Gram matrix is . For and , is the vector equal to on and off ; , are the and Euclidean norms; is the number of non-zero coordinates of ; is the complement of .
The cone condition for and is
Assumption RE holds with constant if for every with and every satisfying (4.1). For , let be a set of indices outside carrying the largest , and ; Assumption RE replaces by .
The restricted eigenvalues are and , the minimum and maximum of over with . The restricted correlations are the maximum of over disjoint index sets with and non-zero . Two constants are attached to them:
is the orthogonal projector in onto the span of the columns , .
For integers , , and , if Assumption 2 holds, then , RE and RE hold with constant , and for every with and every satisfying (4.1)
Assumption 2 involves no correlations, only extreme eigenvalues of small principal submatrices of .
For and , Assumption 1 implies the same conclusions with and constant .
For and , each of
(Assumptions 3, 4, 5) implies RE, with the constants , and respectively.
The milestones are the steps of the proof in Appendix A — the projection inequality (A.1), the block bound (A.2), the shelling bound (A.3), the Candès–Tao correlation bound used for part (i) — followed by part (i) and the three coherence-type implications.
RE with and is the hypothesis of the paper's prediction and bounds for the Lasso and the Dantzig selector (Theorems 5.1, 6.1, 7.1, 7.2), and RE is the hypothesis of its bounds. Assumptions 1–5 are stated through quantities that are standard in compressed sensing and random matrix theory, so known bounds for , and of random designs transfer, through this mission's theorems, to every result stated under RE. Lemma 4.1 also shows that RE is weaker than the Candès–Tao condition used for the Dantzig selector.
The results are proved in the paper; parts of Lemma 4.1's proof (the correlation bound for part (i)) are cited from Candès and Tao without proof. None of these results is formalized: the platform has pairwise-incoherence and restricted-nullspace statements from Wainwright's textbook (a different conclusion and normalization) and restricted isometry definitions, but neither restricted eigenvalues , restricted correlations , nor the RE condition in this form.
The naive attempt to bound from below splits and applies an eigenvalue bound to each part. This fails: can have up to non-zero coordinates, and no condition on - or -sparse submatrices controls directly. The cone condition bounds only the norm of , while eigenvalue conditions speak about norms of sparse vectors; bridging the two with the right constant , and keeping track of how the leading block interacts with the rest through the projector , is where the work lies. For part (i), the interaction between disjoint sparse blocks has to be controlled by rather than by .
Matrix (Fin n) (Fin M) ℝ; vectors are Fin M → ℝ and Fin n → ℝ; . The projector is Mathlib's orthogonal projection on EuclideanSpace ℝ (Fin n) onto the span of the columns indexed by .RE X s c0 κ asserts the RE inequality with constant for all admissible and . The paper's is the largest such (the minimum is attained), so "RE holds with " is exactly " is a witness". This avoids a real infimum over an empty set when .sInf/sSup over nonempty bounded sets (a basis vector for ; two disjoint singletons for , since ), so they equal the paper's attained min/max. , , are natural numbers; is written .Generalized pattern search (GPS) is a class of derivative-free methods for minimizing a function that can only be evaluated, not differentiated. Such objectives arise in engineering design, where one evaluation is an expensive simulation that may fail and return no value at all. The helicopter rotor design problem of Booker et al. is one example: no value was returned for roughly 66% of the trial points (Booker et al., 1999). A method for such problems has to tolerate objectives that are discontinuous or take the value .
Earlier convergence theory for GPS assumed continuous differentiability of the objective on a neighbourhood of the level set. Torczon established it for unconstrained problems (SIAM J. Optim. 7, 1997), and Lewis and Torczon extended it to bound constraints (1999) and to finitely many linear constraints (SIAM J. Optim. 10, 2000). Audet and Dennis (SIAM J. Optim. 13, 2003) replaced these analyses with a single argument. Its conclusions are local and are graded by the smoothness of the objective at the limit point only, through Clarke's generalized directional derivative. That paper is the source of this mission. Its analysis is the basis of the later mesh adaptive direct search (MADS) theory (Audet, Dennis, SIAM J. Optim. 17, 2006).
The problem is
with and in . The algorithm works with the barrier function , equal to on and to elsewhere.
The algorithm uses a finite set of directions , the columns of the product of a nonsingular and an integer matrix . The directions form a positive spanning set: their nonnegative combinations give all of . At iteration , with iterate and mesh size parameter , the mesh is . A poll set is drawn from a positive spanning subset . Each iteration ends in one of two ways:
Here is rational and are integers. The assumptions are A1 , A2 is rational, and A3 all iterates lie in a compact set. A refining subsequence is an infinite set of mesh local optimizers along which (Definition 3.5). For Lipschitz near , Clarke's derivative is
Assume A1–A3. Let be the limit of a refining subsequence, and let be a direction polled at a feasible point for infinitely many in the subsequence. If is Lipschitz near , then
Theorem 3.7 gives a first-order conclusion at a limit point from a local hypothesis at that point alone. It does not require smoothness elsewhere, finiteness of elsewhere, or continuity. It turns the heuristic "the method stopped improving on ever finer meshes" into a statement about generalized derivatives. The unconstrained stationarity result (Theorem 3.9) and the linearly constrained KKT result (Theorem 3.14) follow from it, and they recover the Torczon and Lewis–Torczon theorems under weaker smoothness assumptions. The chain Lemma 3.2 → Lemma 3.3 → Proposition 3.4 → Theorem 3.6 shows that the goal's hypothesis is always met. Every run satisfying A1 and A3 has a refining subsequence, which rests on the rationality of and on the integer structure of .
All results in this mission are proved in the source paper. None of them has, to the best of our knowledge, a machine-checked proof. The mission contributes a formal model of the GPS algorithm class as a class of runs, a formal Clarke directional derivative, and checked proofs of the mesh-refinement chain and the main theorem.
Given a refining subsequence, the goal is a comparison of limsups: the poll inequalities give nonnegative difference quotients at the points , which converge to . The difficulty lies in two places. First, the objective is extended-valued, and the barrier hides at infeasible poll points, where the poll inequality says nothing. The hypothesis on has to supply feasibility, and the Lipschitz hypothesis has to supply finiteness near . Second, the existence of refining subsequences is not a compactness argument alone. Coarsening is allowed, so need not decrease, and with an irrational or a direction set that is not an integer lattice image (for instance in ) the meshes can be dense and can be positive. The lattice argument behind Proposition 3.4 is where the integrality hypotheses are used.
Points of are Fin n → ℝ, takes values in WithTop ℝ, and the bounds are EReal-valued, so gives . The barrier is defined by cases, never by extended addition. Directions are the columns of G * Zbar indexed by Fin p, and is a Finset (Fin p). A GPS run is a structure of sequences and a per-iteration predicate "mesh local optimizer", subject to exactly the two update rules above, , rational and the exponent bounds. The SEARCH step, the choice of and the exponents are left free, since the paper allows any strategy. A subsequence is a strictly increasing map . The Clarke derivative of a real function is an EReal-valued limit superior along , . " Lipschitz near " means that agrees near with a real function Lipschitz there, and the conclusions are stated for every such function. Strict differentiability is the directional notion of Section 3.4 of the paper.
The goal is not trivialized by an empty run class: Theorem 3.6, on the same class, asserts that refining subsequences exist. The mesh-local-optimizer branch requires the complete poll inequality over . The Clarke limit superior cannot take a default value. The direction must be polled at feasible points infinitely often, which is the paper's " was evaluated".
Contributions welcome: proofs of any milestone, and reusable lemmas on positive spanning sets, lattice points in compact sets, and the Clarke derivative (for instance, that it equals under strict differentiability).
Maximizing a submodular set function without constraints contains Max Cut, Max Directed Cut, maximum facility location and several graph and hypergraph cut problems as special cases, and it appears in operations research wherever a value exhibits diminishing returns but is not monotone (profit that combines coverage with a cost, for example). These problems are NP-hard, so the question is which fraction of the optimum an efficient algorithm can guarantee when the function is accessible only through a value oracle that returns for a queried set .
Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011) gave the first constant-factor approximation algorithms for maximizing a general nonnegative submodular function. The simplest of them returns a uniformly random set and achieves of the optimum; this mission is about the next one, a nonadaptive algorithm: it decides all of its oracle queries before seeing any answer, then computes a set from the answers. Such an algorithm can be run in one round of parallel queries. The paper shows that this restricted access already beats and reaches .
Timeline. For Max Directed Cut, a random cut achieves . Feige, Mirrokni and Vondrák (FOCS 2007; journal version 2011) proved for a random set and nonadaptively for general nonnegative submodular functions, and by adaptive local search, and that requires exponentially many queries. Buchbinder, Feldman, Naor and Schwartz (FOCS 2012, SIAM J. Comput. 2015) later reached the optimal with a randomized double-greedy algorithm.
Let be a finite ground set with elements. A function is submodular (Definition 1.1) if
Throughout, is nonnegative, the paper's standing assumption, and .
For , denotes the random subset of containing each element independently with probability ; is a uniformly random subset. For a set , is the analogous random subset of . The averaged marginal value of an element (Definition 2.4) is
Algorithm NA (p. 1139):
Given the estimates, the expected value NA returns is .
For every nonnegative submodular and every estimate with for all ,
The printed theorem says "at least "; the term is what the proof establishes (p. 1140, last display).
Milestones 3–7 are the displayed steps of the proof of Theorem 2.6, stated for arbitrary sets where the page's argument does not use the optimality of .
The theorem shows that nonadaptive access, a fixed batch of polynomially many value queries followed by a computation, suffices for a -approximation of unconstrained nonnegative submodular maximization, strictly better than the of any algorithm that must return one of its queried sets (the paper shows is optimal in that class, §4.2). The quantity generalizes the in-degree/out-degree test for Max Directed Cut to arbitrary submodular functions, and Lemmas 2.2 and 2.3 are general sampling inequalities for submodular functions that the paper reuses for its adaptive smooth local search.
Formalizing it produces machine-checked versions of Lemmas 2.2 and 2.3 as statements about exact finite averages, a reusable expectation operator on product-distributed random subsets, and a checked version of the argument with its explicit error term. The result is proved in the paper; to our knowledge none of it has been formalized in a proof assistant.
The two regimes the proof separates, " is already good" and "one of , is large", must be tied to the value of a uniformly random set, whereas the elements of and are chosen from estimated averages, not from the optimal set . The natural attempt, comparing with element by element, fails because is not monotone: adding elements of to can decrease the value. The accuracy of the estimates must also be propagated through a sum over up to elements, which is where the error term comes from. The sampling lemmas require handling expectations over pairs of independent random subsets of possibly overlapping sets.
Fintype X with DecidableEq, assumed Nonempty, so and the divisions by and are genuine; sets are Finset X; is real valued with nonnegativity as an explicit hypothesis. Lemmas 2.2 and 2.3 are stated for real with no sign condition, as printed.Finset.univ.sup' _ f, the true maximum over all subsets.Welcome contributions: proofs of Lemmas 2.2 and 2.3 (reusable for mission IV of this series), the identity , and general lemmas about the operator (splitting a uniform random set along a partition).
The continuous-review policy is the standard replenishment rule of inventory theory: whenever the inventory position (stock on hand plus on order minus backorders) drops to the reorder point , order a fixed order quantity . It is used in practice and taught in every operations management course, usually after the deterministic economic order quantity (EOQ) model, which is the same system with a constant demand stream.
Practitioners and textbooks rely on a robustness property of the EOQ: its cost is very insensitive to the choice of order quantity. If the order quantity is off by a factor , the cost rises only by the factor ; ordering 50% too much costs about 8% extra. The insensitivity of the stochastic system to its control parameters had been observed numerically (Wagner, O'Hagan and Lundh 1965; Naddor 1975; Archibald and Silver 1978), but, as Zheng notes, no analytical result on it was known.
Timeline:
Demands arrive at rate ; orders arrive after a fixed leadtime ; all stockouts are backordered. Each order costs ; holding costs accrue at rate per unit in stock and penalty costs at rate per unit backordered. The leadtime demand has distribution with finite mean .
The inventory cost rate at inventory position is
assumed to attain its minimum at a unique point . The long-run average cost of the policy is
For fixed let be a reorder point minimizing , and let
is the cost of the order quantity when the reorder point is always chosen optimally for it. An optimal order quantity minimizes over , and .
The EOQ model is the same system with the constant leadtime demand . Its cost rate is , and , , are the objects above at , with optimum and .
The goal holds for every demand distribution satisfying the standing assumptions and every optimal . Both regimes, and , are included.
In the order the proof uses them:
In the EOQ model the relative cost of a scaled order quantity is exactly (Eq. (25) of the paper). Theorem 4 shows that the stochastic system is at least as forgiving. The bound holds for every leadtime-demand distribution with a unique newsvendor minimizer, and it does not depend on the parameters , , , or . Because the reorder point is re-optimized for each quantity, the bound applies to the practical question of how much a misestimated lot size costs when the safety stock is set correctly.
Together with the other results of the paper (the bound for the EOQ heuristic and the bounds between and , which are separate missions of this series), it gives a closed-form account of why the EOQ is a good heuristic for stochastic systems.
The result has a complete published proof. It has not been machine-checked. The work that remains is a formal proof for general distributions: the paper differentiates and twice, and a formal proof has to replace those derivatives with arguments that need no density.
is defined through an inner minimization over the reorder point, so its shape in is controlled by the implicitly defined function rather than by directly. The obvious approach would bound with the reorder point fixed at . That approach is the wrong comparison: it bounds a larger quantity, and the resulting bound depends on the distribution.
The paper's proof uses three properties of : that it is convex, that its slope never exceeds the EOQ slope , and that it dominates . The paper obtains these from the derivatives and under a smooth demand distribution. Without a density, is only an argmin and need not be differentiable, so none of these three properties can be read off a derivative formula; the asymptotic slope in particular depends on the finite mean and on the behaviour of at .
The mission is set in Lean 4 with Mathlib. All objects are real valued.
QRModel bundles , a probability measure on with integrable identity, , almost surely, and the unique-minimizer hypothesis on . is implicit in the paper and made explicit here. No density is assumed; deterministic and discrete demands are allowed, and the paper's own numerical study uses Poisson demand.IsOptQty Q, meaning and for all . Its existence is asserted in the Eq. (8) milestone, so the goal is not vacuous. "" is a real with real division . In Lemma 9 the integral is oriented, as on the page.A complete development needs the following:
These facts about newsvendor cost functions are reusable in the other missions of this series. Contributions of any of them as separate lemmas are welcome.
The continuous-review policy is the standard control rule for a single stocked item with random demand: whenever the inventory position falls to the reorder point , an order of fixed size is placed. It is implemented in a large share of commercial inventory systems. Choosing the two parameters jointly has traditionally required numerical search (Hadley and Whitin, 1963; Federgruen and Zheng, 1992). In practice the order quantity is therefore often taken from the deterministic economic order quantity (EOQ) formula with backorders, and the reorder point is then set for the random demand.
Zheng (1992) turned this practice into a question with an exact answer: how does the optimal order quantity of the stochastic model compare with the EOQ quantity computed from the same cost data and the same mean demand? Its Theorem 2 answers it with a two-sided bound. This mission formalizes that theorem. Companion missions of the same series formalize the paper's cost bounds (Theorem 3), the flatness of the cost curve (Theorem 4) and the bound on the cost of using the EOQ quantity (Theorem 5).
Demand arrives at rate and replenishment orders arrive after a fixed leadtime . Shortages are backordered. Holding costs accrue at rate per unit held, backorder penalties at rate per unit short, and every order costs . The leadtime demand is a nonnegative random variable with law and mean . The expected inventory cost rate at inventory position is the newsvendor cost
assumed, as in the paper, to attain its minimum at a unique point . The long-run average cost of the policy is
For each , let be an optimal reorder point, i.e. a minimizer of . The analysis runs through the curves
and through the cost of order quantity with the reorder point set optimally. The optimal order quantity is the minimizer of over .
The EOQ model is the case of a constant leadtime demand . Its cost rate is , and the same construction gives , , and the optimal quantity
For , let , , be the positive solutions of
Each has exactly one positive solution, and
Moreover, with and the demand law fixed, is nondecreasing on and converges to a finite constant as .
The milestones are the paper's own numbered results that feed Theorem 2, listed in the order the argument uses them:
The result. Theorem 2 says that the EOQ formula always underestimates the optimal order quantity when leadtime demand is random. The underestimate is bounded by , a quantity that stays bounded however large the ordering cost is. So the relative error of the EOQ quantity vanishes as grows. The first inequality, , is also an ingredient of the paper's Theorem 3 (cost bounds) and Theorem 5 (the EOQ quantity raises costs by at most ). The explicit bounds , , bracket and give a search interval for it.
Formalizing it. The theorem has been proved on paper since 1992. No machine-checked version of it, or of the continuous-review cost of Eq. (1), exists on this platform. The inventory items already here treat the discrete cost with integer order quantities, a normally distributed demand, or the EOQ without backorders. This mission provides a machine-checked version of the paper's optimality conditions for a general demand distribution. The paper's argument differentiates twice, i.e. it tacitly assumes a density. The formal statements do not, so a formal proof must redo those steps with one-sided (convexity) arguments. The printed argument for the limit in part (b) shows only that a derivative tends to zero. A complete proof of convergence is part of the work.
The obvious route to compares the two cost curves and directly. It fails because pointwise, and a pointwise inequality between two convex functions says nothing about the order of their minimizers. The stochastic curve is defined only implicitly, as evaluated at a minimizer of a parametric integral, so its growth relative to the linear has to be established before any comparison of order quantities. For part (b), a vanishing derivative does not imply convergence ( also has a vanishing derivative), so the printed proof of the limit does not go through as written.
Without a density, need not be differentiable. Every derivative in the paper's proofs (of , and ) must be replaced by monotonicity or chord arguments.
The Lean development uses the namespace ZhengQR.OrderQty. Its conventions:
Infrastructure needed includes the following. Much of it is reusable for any single-item inventory model:
Contributions welcome: proofs of the milestones in any order, general lemmas on the newsvendor cost, and a complete convergence argument for part (b).
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.