Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Set cover is the problem of covering a finite ground set with as few members of a given family of subsets as possible. It models facility location, crew scheduling, test-suite minimization and many other selection problems in operations research, and it is one of the canonical NP-hard problems. The greedy algorithm, which repeatedly picks the subset covering the most uncovered points, finds a cover at most about times larger than the optimum on an instance with points (Johnson 1974; Lovász 1975; Chvátal 1979). Whether any efficient algorithm does substantially better was open for two decades.
Timeline of the lower bounds:
This mission formalizes Feige's theorem, the result that fixed as the threshold.
An instance consists of points and a list of subsets . A cover is a set of indices whose subsets together contain every point. The instance is coverable if every point lies in some . It is written as a string: in unary, then each subset as its characteristic vector.
A deterministic polynomial-time algorithm approximates set cover within if, for some threshold and every coverable instance with points, the value it outputs satisfies , where is the size of a smallest cover.
is the class of languages that a deterministic one-tape Turing machine decides within steps, for some constant . Machines, and are those of the published definition CookPvsNP_defs.
The proof passes through three objects, each defined in the mission:
The statement fixes no constant beyond . The parameters , and of the reduction are choices made inside the proof. The goal carries three cited results as hypotheses: Theorem 2.1.1 (MAX 3SAT-B gap), the consequence of Raz's parallel repetition theorem for the clause–variable game, and the Naor–Schulman–Srinivasan construction of partition systems.
The result. Combined with the greedy algorithm, Theorem 4.4 shows that is the approximation threshold of set cover under a mild complexity assumption. Set cover reduces approximation-preservingly to many covering problems, so the threshold transfers to them. Examples are dominating set, several facility-location and group Steiner problems, and hitting-set formulations used in scheduling and testing. The -prover system with two acceptance predicates and the partition-system gadget became standard tools for later hardness-of-approximation proofs.
Formalizing it. The theorem is proved and has been strengthened (Dinur–Steurer 2014), but no machine-checked proof of any inapproximability of set cover is known. This mission contributes:
Thm211, RazRepetition, NaorPartitionSystems) and a hypothesis of the goal.
RazRepetition is only the consequence of Raz's theorem that the paper uses (p. 642): a error bound for the repeated clause–variable game on 3CNF-5 formulas far from satisfiable.NaorPartitionSystems relaxes "time linear in " to polynomial time and renders " polynomial in " as . Both relaxations weaken the hypothesis.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 .
The linear-quadratic regulator (LQR) is the basic problem of optimal control: steer a linear system so as to minimize an integrated quadratic cost. When the full state is measured and the gain may be chosen freely, the optimal feedback is given by the algebraic Riccati equation (Kalman, 1960). In many applications only an output is measured, and the controller is restricted to a static feedback . For this output-feedback problem no Riccati-type characterization exists; the design problem is a non-convex optimization over the gain matrix .
Direct optimization of the gain by gradient descent, known in the control literature since Levine and Athans (1970) and revived in reinforcement learning as policy gradient (Fazel, Ge, Kakade and Mesbahi, 2018, arXiv:1801.05039), is therefore of interest both to control engineers and to the learning community. Fatkhullin and Polyak (arXiv:2004.09875, SIAM J. Control Optim. 2021) give a self-contained analysis of the continuous-time problem: the cost is coercive on the set of stabilizing gains, smooth on sublevel sets, and, for state feedback, satisfies a gradient-domination (Łežanski–Polyak–Łojasiewicz) inequality. From these they derive convergence guarantees for the gradient method.
Fix real matrices , , and weights , , and an initial-state covariance . A gain is a matrix , and the closed-loop matrix is . A square matrix is Hurwitz if all its complex eigenvalues have negative real part. The set of stabilizing gains is
For let be the unique solution of the Lyapunov equation
and define the cost , the expected integrated quadratic cost of the closed loop from a random initial state with covariance . With the solution of , the gradient of in the Frobenius inner product is
A known stabilizing gain is given, and is its sublevel set. The standing assumptions are , and . State feedback (SLQR) is the case .
The gradient method with step sizes is
A number is a smoothness constant if for all .
For , an optimal gain , and any smoothness constant :
and there are , with .
In attack order:
The theorem shows that a plain first-order method, started from any stabilizing gain, never destabilizes the closed loop and decreases the cost monotonically, for output feedback as well as state feedback. For state feedback it converges globally and linearly to the optimal gain. The cost is non-convex, and its domain is open, possibly non-convex and unbounded, so this does not follow from convex optimization theory. It is the continuous-time counterpart of the policy-gradient guarantees of Fazel et al. for discrete-time LQR, and it underlies model-free and data-driven variants of gain tuning.
The result is proved in the paper, but it has not been formalized. The formalization adds three things. It makes the invariance argument (the iterates stay in ) explicit, and the paper describes that argument as the non-trivial part. It corrects the statements where the printed text is wrong (see below). It also produces a reusable library of Lyapunov-equation facts. Mathlib has no Lyapunov equation, no LQR cost and no Hurwitz stability theory, and the platform has no continuous-time LQR material. The nearest platform items treat discrete-time Riccati iteration (BertsekasDP.riccati_convergence_stability) and Polyak–Łojasiewicz rates on a whole normed space (ShiOptRates.pl_rate). Neither applies to a function defined only on a non-convex open subset.
The standard descent-lemma argument assumes is defined and -smooth on the whole space. Here is defined only on , and it is not smooth on all of : it blows up at the boundary. A gradient step from a point of could in principle jump out of , where the Lyapunov equation has no meaningful solution. The smoothness bound is available only inside , so the argument must show that the whole segment from to stays in before the descent inequality can be used on it. That requires coercivity, compactness of and an exit-time argument. For the linear rate, gradient domination has to be established on with constants controlled by , and passing from function values to distances to needs that minimizer's structure. Gradient domination fails for output feedback (the paper's Example 3.4 has two disconnected components with different minima), so the linear rate is stated only for .
Matrices are Matrix (Fin p) (Fin q) ℝ. Hurwitz means every element of the complex spectrum has negative real part. , are "the unique solution of the Lyapunov equation, if there is none or several"; this junk value is never used, because every statement evaluates and only at gains proved or assumed to lie in . The iterates' membership in is a conclusion of the goal, never a hypothesis; assuming it would delete the theorem's content. is defined by the formula (3.3), and Lemma 3.11 is the theorem that it is the gradient. is , is the spectral (operator) norm, and are the minimum and maximum eigenvalue of a symmetric matrix. State feedback is the instance , . In (4.6) the Frobenius norm replaces the paper's spectral norm, which is equivalent because is existential. The minimum over requires .
Deviations from the printed text, each recorded in the item's Formalization Note:
Not stated: Theorem 4.3 and Algorithm 4.1, Lemma 3.6, Lemmas 3.12–3.14, Corollary 3.16 and the explicit constant (3.8). Welcome contributions include a Lyapunov-equation library (existence, uniqueness, integral representation, positivity), continuity of the spectrum, and the exit-time argument, which is reusable for any descent method on a sublevel set of an open domain.
Variational inequalities and complementarity problems are the standard formulation of equilibrium in operations research and mathematical economics: traffic equilibria, spatial price equilibria, Nash equilibria of convex games, and the optimality conditions of constrained optimization all take this form. Many applications have two features that the classical theory does not cover. The feasible set of a player or a flow can depend on the current state (a quasi-variational inequality, as in generalized Nash games with shared constraints), and the response map can be set-valued (a subdifferential, or a best-response correspondence). D. Chan and J. S. Pang (Math. Oper. Res. 7 (1982) 211–222) introduced the generalized quasi-variational inequality covering both, proved existence theorems for it, and derived existence for a new generalized implicit complementarity problem.
Timeline of the results this mission builds on:
Throughout, carries the Euclidean inner product and norm . A point-to-set mapping assigns to each a set . Given point-to-set mappings and , the problem asks for vectors with
A cone is a convex set containing and closed under nonnegative scaling. The dual cone of a set is . For a point-to-point map , a cone-valued map and a point-to-set map , the problem asks for with
A mapping is upper semicontinuous on a set at if for each open there is a neighbourhood of with for ; lower semicontinuous if for each open meeting , meets for all near in ; continuous if both. A set is contractible if some point and a continuous satisfy , . is the closed ball of radius about the origin, its boundary sphere. For point-to-set maps and , the coercivity function is
with . The map is strongly copositive with respect to at if and for some and , for all and . For and , .
Let be a closed cone with nonempty interior, continuous, , and a mapping with nonempty contractible compact values, upper semicontinuous on . If some satisfies for all , and is strongly copositive with respect to at , then for every
Theorem 4.2 gives existence for complementarity problems whose cone is translated by a state-dependent map and whose response map is set-valued. It contains existence for the implicit complementarity problem of Capuzzo-Dolcetta, Mosco and Pang () with strongly monotone data (Corollary 4.2 of the paper), and Saigal's generalized complementarity problem (). Theorems 3.2 and 4.1 are general-purpose existence tools for quasi-variational inequalities with set-valued maps; Theorem 3.2 reduces to the Fang–Peterson theorem when is constant, and Corollary 3.1 to the Hartman–Stampacchia theorem when in addition is single-valued.
All results of the paper are proved; none is open. To our knowledge none of them has been formalized: no proof assistant library contains quasi-variational inequalities with set-valued maps, and Mathlib has neither Kakutani's nor the Eilenberg–Montgomery fixed point theorem (nor Brouwer's). A formal proof of the goal therefore also produces a reusable library of set-valued existence theory.
The whole chain rests on Theorem 3.1, whose proof applies the Eilenberg–Montgomery fixed point theorem for upper semicontinuous maps with acyclic (here contractible) compact values; this in turn needs either singular homology or an approximation argument, neither of which is available in Mathlib. Replacing "contractible" by "convex" to use Kakutani's theorem would prove a strictly weaker theorem: the paper states contractible values deliberately. The second difficulty is that the fixed point only solves the problem on the truncation ; turning it into a solution over all of needs the boundary argument of Theorem 3.2, and for Theorem 4.2 the continuity of , which is where the solidity of is used. The obvious approach of applying Theorem 3.2 directly with fails because must be compact.
The space is EuclideanSpace ℝ (Fin n), so all norms and balls are Euclidean (not the sup norm of Fin n → ℝ). Point-to-set mappings are functions into Set; semicontinuity "on " is Mathlib's UpperHemicontinuousOn/LowerHemicontinuousOn with neighbourhoods relative to , and "on " is UpperHemicontinuous. Cones are PointedCone ℝ _ (convex, containing , as footnote 1 of the paper says). Balls are centred at the origin.
Conventions that the Lean statements make explicit:
A trivializing formalization is ruled out: the GQVI solution tests over all of , not over , and the GICP solution keeps both the dual-cone condition and the complementarity equation. Dropping any of these would turn the goal into a restatement of Theorem 3.1.
A complete development needs: an Eilenberg–Montgomery (or at least Kakutani plus an acyclicity argument) fixed point theorem for set-valued maps, Berge's maximum theorem, and basic facts on hemicontinuity of intersections and translates of set-valued maps. The fixed point theorems, the maximum theorem and the hemicontinuity lemmas are reusable far beyond this mission. Contributions of any of these as separate theorems 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.
Many problems in signal processing, statistics and machine learning minimise a sum of three convex terms: a smooth data-fit term and two nonsmooth regularisers or constraints, each of which is easy to handle on its own (through its proximal map) but not in combination. Examples are constrained sparse regression, matrix completion with a nuclear-norm penalty and box constraints, and support-vector machines with a norm penalty. Davis and Yin (Set-Valued Var. Anal. 25 (2017)) introduced a three-operator splitting scheme that evaluates each proximal map and the gradient of the smooth term once per iteration and reduces to Douglas–Rachford splitting (Lions and Mercier 1979) and forward–backward splitting as special cases. Section 3 of that paper gives the objective-error rates of the scheme on convex problems. This mission formalizes those rates for general convex problems.
Let be a real Hilbert space. The problem is
where are closed, proper, convex functions (lower semicontinuous, never , finite somewhere, with convex epigraph) and is convex and differentiable with -Lipschitz gradient , .
For the proximal map is the unique minimiser of . Algorithm 2 of the paper picks and and iterates, with relaxation ,
Equivalently for the three-operator map
If is a fixed point of , then minimises (3.1). The weighted ergodic iterate is
and is defined the same way from .
Let be a fixed point of , , and suppose is -Lipschitz continuous on the closed ball . Then there is a constant , independent of , with
The goal asserts the order and leaves the constant free, so it is not invalidated by a sharper constant.
The result. Theorem 3.1 gives the last iterate an objective error of . Theorem 3.2 shows that averaging with linearly increasing weights improves this to , the rate of the standard uniform ergodic average, while putting more weight on recent iterates. The paper notes that this matters when the iterates are sparse vectors or low-rank matrices and the average should stay close to them. The rates hold under a local Lipschitz condition on one of the two nonsmooth terms only, so may be the indicator function of a constraint set. They therefore cover the constrained applications of Section 4 of the paper.
Formalizing it. The results are proved in the paper. No machine-checked version of this scheme or its rates exists on the platform or, as far as is known, in Mathlib. A formalization produces a checked proof in an arbitrary real Hilbert space with extended-valued . It also produces infrastructure that Mathlib lacks: proximal maps characterised by minimisation, the prox-subgradient inclusion, Fejér monotonicity of an averaged-operator iteration, and a weighted Jensen inequality for extended-valued convex functions. All of these can be reused by other splitting and proximal-gradient missions. The formalization also checks the constants: the last display of the published proof of Theorem 3.2 drops a factor in front of the Lipschitz term, and the printed ball in both theorems is centred at where the proof needs .
The obvious argument sums the one-step inequality (3.2). That controls the objective at the two different points and , and only appears, never . Moving from one point to the other needs the Lipschitz hypothesis on , and so it needs every iterate, and every weighted average, to stay in the ball on which that hypothesis holds. For the weighted average there is a further obstacle: the cross term does not telescope under the weights . Controlling it requires the summability of the gradient differences (2.7), which is inherited from the averagedness analysis of Section 2 and not from convexity alone. Uniform averaging with the same argument does not give the weighted statement, and the weights must not be replaced.
InnerProductSpace ℝ H, CompleteSpace H), not .EReal. They are proper (never , somewhere ), lower semicontinuous, and have a convex epigraph in . is convex and differentiable, and Mathlib's gradient h is -Lipschitz.Welcome contributions: the prox–subgradient inclusion for EReal-valued convex functions, averagedness and Fejér monotonicity of (the companion mission on Section 2 treats the general operator case), a weighted Jensen inequality in EReal, and proofs of the milestones in the listed order.
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.Many objective functions in optimization are pointwise maxima: the worst case of a loss over an uncertainty set, the value of a minimax problem as a function of the outer variable, a penalty for a system of constraints, or the largest eigenvalue of a symmetric matrix. Such a function
is typically not differentiable even when every piece is smooth, because the maximizing jumps. Descent methods, optimality conditions and sensitivity analysis for these problems all need a substitute for the gradient of and a formula for its directional derivatives.
Danskin's theorem (Danskin 1966) answers this when exists and is continuous in and is compact: has one-sided directional derivatives , where is the set of maximizers. Convex analysis gives the analogue when each is convex (Rockafellar 1970). In Generalized gradients and applications (Clarke 1975) Frank Clarke introduced the generalized gradient of a locally Lipschitz function and proved, as his first application, a single theorem, Theorem (2.1), that contains both cases. The generalized gradient became the standard object of nonsmooth analysis (Clarke 1983), and Theorem (2.1) is the prototype of every "subdifferential of a max function" rule used in minimax optimization.
Work in with the Euclidean norm and inner product . A function is locally Lipschitz if for every bounded set there is with for . By Rademacher's theorem such is differentiable almost everywhere.
and the one-sided directional derivative is when the limit exists.
For the max function, is a nonempty sequentially compact topological space and . Write , , for the objects above applied to at . Let and . The hypotheses of Theorem (2.1) are:
Under (a)–(d):
The result. Theorem (2.1) computes the directional derivatives and the generalized gradient of a max function from those of its active pieces. It yields Danskin's theorem when is continuous, and the convex max rule when each is convex, and it applies to nonsmooth, nonconvex families satisfying (c), a property later called regularity (Clarke 1983, §2.3). In the same paper it is applied to the distance function to compute (Proposition (2.4), Corollary (2.5)), which then drives the characterization of flow-invariant sets in §4. Proposition (1.4) and Corollary (1.10), which the theorem rests on, are the duality between and used throughout nonsmooth optimization: Clarke stationarity, bundle methods and subgradient methods for weakly convex functions all state their results against them.
Formalizing it. The results are classical and proved; none of them, to the platform's knowledge, has a machine-checked proof. Mathlib has Rademacher's theorem, gradients and convex hulls, but no Clarke generalized gradient. This mission builds the first layer of nonsmooth analysis: the definitions of , , and upper semicontinuity of multifunctions, the support-function duality, and the max rule.
The obvious approach reads off a single active piece. It fails because the active set changes as , may be infinite, and need not converge; can be differentiable at points where no individual piece is known to be. Hypothesis (c) cannot be dropped: for a single point and on , has while , so conclusion (3) fails. Limits of maximizers exist only through the sequential compactness of together with (a), and limits of gradients only through the joint closed-graph condition (d) in ; continuity in for each fixed is not enough. Proposition (1.4), on which everything rests, is itself a measure-theoretic statement: it relates the upper limit of difference quotients over all nearby base points to gradients that exist only almost everywhere.
EuclideanSpace ℝ (Fin n), is inner ℝ ζ v, is Mathlib's gradient, and " exists" is DifferentiableAt ℝ f x.LipschitzOnBounded. Hypothesis (b) is ∀ B bounded, ∃ K, ∀ u, LipschitzOnWith K (g · u) B: the constant is uniform in .gradient is where is not differentiable.Filter.limsup in along ; this is a junk value for non-Lipschitz , so every statement using assumes the Lipschitz hypothesis. The one-sided derivative is a Tendsto along .IsGreatest, which asserts attainment. The max function is ⨆ u, g x u; is nonempty ([Nonempty U]) and SeqCompactSpace, and (a) is Mathlib's UpperSemicontinuous on . The paper uses implicitly; with conclusion (4) would be false.UpperHemicontinuous.sSup without attainment would make the statements trivial or false; these are ruled out as above.Contributions welcome: proofs of the milestones, in particular Proposition (1.4) and Corollary (1.10), which are reusable for every later nonsmooth-analysis mission; lemmas that is nonempty and compact; the equivalence of LipschitzOnBounded with Mathlib's LocallyLipschitz.
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 .A sorting network is a sorting procedure whose sequence of comparisons is fixed in advance, independently of the data. Its depth, the number of rounds of simultaneous comparisons on disjoint pairs, is the parallel running time. Sorting networks are used in parallel and hardware sorting, in switching networks, and in cryptography, where a data-independent (oblivious) sequence of operations is required. How small the depth can be as a function of the number of inputs is a basic question of parallel computation.
Timeline:
There are registers holding elements of a linearly ordered set. An elementary step (a comparator) with compares the contents of and and exchanges them if the content of is larger. Afterwards holds the minimum and the maximum of the two, and every other register is unchanged. A parallel step is a set of comparators in which no register occurs twice, so it has at most comparators. A comparator network is a finite sequence of parallel steps, fixed before the input is seen. Its depth is the number of parallel steps and its size the total number of comparators. sorts if for every input the output satisfies .
The construction runs on the tree of finite - sequences, whose levels are ordered lexicographically. A chain on level assigns to every node of that level a set of registers, with the sets pairwise disjoint and of a common size . A ⟨k, ε⟩ expander on ⟨A, B⟩, for disjoint register sets and , is a bipartite graph between and of maximum degree in which every nonempty has more than neighbours, and symmetrically for . The Lean development uses the names ComparatorNetwork, compareExchange, IsChain, chainN, IsExpander, IsLowerSection for these objects.
The constant is absolute and is not fixed. Any explicit value would be invalidated by the next improvement, and the paper gives none.
The result. The AKS theorem settles the asymptotic depth of sorting networks at and their size at . It gives an -time sorting algorithm with processors that performs only data-independent comparisons. It is the standard reference point for oblivious sorting in parallel algorithms, circuit complexity (sorting is in via comparators) and oblivious RAM constructions. Lemma 4, the ε-halver property of expander comparisons, is the component that later constructions (Paterson) reuse.
Formalizing it. The theorem has been proved since 1983. No Lean proof of the AKS theorem is known. Mathlib has no expander graphs in the ⟨k, ε⟩ sense and no sorting networks. The mission asks for a formal proof of the headline theorem by any route (the AKS construction or Paterson's variant), and for formal proofs of the paper's verified lemmas as reusable components. The expander lemma needs either an explicit family (Margulis; Gabber–Galil) or a probabilistic existence argument, both substantial on their own.
Every elementary argument stalls at depth : recursive merging needs merge rounds, and merging two sorted lists by a comparator network needs depth . A depth of therefore cannot come from exact merging. It must come from constant-depth approximate operations (ε-halvers, which require bounded-degree expanders) combined with a mechanism that corrects the errors they leave. In the paper this mechanism is a movement of registers up and down a binary tree, controlled by a family of constants chosen in a fixed order ("", p. 2). The accounting that shows the misplaced elements decay geometrically is the hard part. Several intermediate lemmas of the paper are false as printed, so the paper's text is not a checklist to transcribe.
Conventions committed to in Lean:
Fin n, and contents lie in an arbitrary linearly ordered type. A network is a List of layers, each a List (Fin n × Fin n) of comparators with distinct endpoints, and no register occurs twice in a layer. A comparator puts the minimum into , and both directions and are allowed. Sorts means the output is monotone for every linearly ordered type and every input, not only for permutations.Real.logb 2 n, and the goal is stated for . The constant is quantified before .Fin (2^i), with numeric order equal to lexicographic order. A chain is a Fin (2^i) → Finset R.Trivializing formalizations are ruled out. The goal is not "for every there is a network of depth " with the constant chosen after , which is true for trivial reasons. Layers without the disjointness condition would let a single layer contain a whole insertion sort. A bound on the number of comparisons alone, with unbounded depth, is a different and much older result; the goal states both the depth and the size bound.
The mission states the AKS theorem and the paper's lemmas that are correct as stated. It does not formalize the AKS algorithm itself (, , the operations CH1–CH4, IMP) or its intermediate Lemmas 5–11 and 13–15. Those depend on unspecified constants constrained only by "sufficiently small" chains, and Lemmas 5, 10 and 12(b) are false as printed. A solver may of course define the algorithm, with pinned constants, as part of a proof.
Contributions welcome: a library of comparator networks (composition, the 0-1 principle, depth of Batcher's networks), existence of bounded-degree bipartite expanders, the ε-halver lemma, and any complete proof of the goal. The network and expander definitions are independent of this paper and reusable.
A retailer or manufacturer that stocks several grades of the same item (memory chips of different speeds, steel of different strengths, seats in fare classes) can often meet demand for a lower grade with a higher one when the lower grade runs out. This downward substitution changes the stocking decision: each product now protects the demand of every class below it, so the optimal stock of one product depends on the stock of all the others, and the single-product newsvendor answer no longer applies product by product.
Bassok, Anupindi and Akella (Operations Research 47(4), 1999) set up a single-period model with products and full downward substitution and showed that the optimal ordering policy still has a simple structure: there is a base-stock vector ; products below it are ordered up to it, and a product already at or above its base-stock level is not ordered at all. Earlier work on multiproduct ordering, Veinott (1965) and Ignall and Veinott (1969), gave monotonicity conditions through a substitute matrix condition on the Hessian of the cost, which is hard to verify for a general -product substitution structure; the paper works instead with concavity, submodularity and explicit first partial derivatives. Two-product substitution models had been analysed by McGillivray and Silver (1978) and Parlar and Goyal (1984).
There are products and demand classes, both numbered . Class can be served by product whenever , at a unit substitution cost when . Each class has unit revenue and unit backorder cost ; each product has unit purchase cost and effective unit salvage value (salvage value minus holding cost, possibly negative). Put if , if , and . The standing assumptions are: (1) for ; (2) for ; (3) for .
The sequence of events: the starting inventory is observed; stock is raised to at unit costs ; the demand vector is realized; stock is allocated to classes; leftovers are salvaged. For fixed and the allocation is the linear program
subject to , , and , where is the amount of product given to class , the shortage of class and the leftover of product . The expected profit is
and the ordering problem is ; a maximizer is an optimal level .
Allocation Algorithm (A) serves the classes in the order , class first from product and then from the leftovers of products . The subproblem shortage is the unmet demand of class when (A) runs on the classes with the products only; means for all . The paper's first partial derivatives of are sums of salvage values, substitution costs and the , weighted by probabilities of such shortage events.
With a maximizer of over , every optimal level for every starting inventory satisfies
Theorems 1 and 2 give the optimal ordering policy of the substitution model its base-stock form: a vector , computed once, determines the decision for every starting inventory in the region and fixes the order of every overstocked product elsewhere. The paper builds its bounds on , its iterative algorithm for two products and its computational study of the value of substitution (§3) on this structure. Proposition 1 turns the second-stage linear program into a closed-form greedy allocation, which is what makes the derivative formula (4) explicit.
The results are proved in the paper, but none of them has been machine-checked. Several steps of the paper are informal: Proposition 1 is proved by reference to Monge sequences of transportation problems, the proof of Theorem 2 treats only the adjacent pair , and the paper uses independence of demand classes, densities and a unique optimal level without stating them. A formal development makes these hypotheses explicit and checks each step. The model, the greedy allocation and the shortage calculus are reusable for other multi-product newsvendor and assortment models.
The obvious argument for Theorem 2 is the one-dimensional one: if then at , so product should not be raised. It fails because depends on the other coordinates: at some products are raised above and others kept at , and concavity plus submodularity alone do not control the sign. For a general concave submodular function the conclusion is false; a three-variable quadratic in which raising one coordinate lowers the optimal level of a second one, which in turn raises the marginal value of the first, is a counterexample. The proof has to use the specific structure of the substitution model, through the pairwise comparison of the partial derivatives in Eq. (4). The derivative formula itself requires a careful account of how an extra unit of product propagates through the greedy allocation of every later class.
Products and classes are indexed by Fin N (the paper's index is Lean index ); stocks, demands and prices are real. The allocation LP is encoded with the upward arcs , , forbidden (fixed to ), as in the paper's proof of Proposition 1; is the supremum of the LP objective. The demand law is a product . Submodularity is the lattice inequality , which is equivalent to the paper's nonpositive cross partials (Definition 2) for twice differentiable functions. Derivatives are stated with HasDerivAt, and the derivative inequalities of Lemmas 2 and 5 in the stronger monotone form, so that no statement is made true by a junk value of deriv. The "…" in Eq. (4) and in the lemmas are expanded as finite sums with the general term inferred from the printed first and last terms.
Hypotheses the paper uses without stating, made explicit here:
The goal quantifies over every maximizer of and every optimal ; it is not an existence statement, and is not chosen by the prover. Without the full-support hypothesis the universal statement fails already for one product (a flat-topped profit). Lemmas 4 and 6 of the paper are not included: under the definitions used here both are false as printed (small two- and three-product computations with exponential demands show it), and Theorem 3 comes after the goal and fails as printed for .
A proof needs integrals of piecewise-linear functions of the demand vector, differentiation under the integral sign, and facts about product measures. Contributions of any of the milestones, and of general lemmas on the greedy allocation (monotonicity of in and ), are welcome.
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).
Retailers that sell the same product can raise their joint profit by pooling: stock left over at one location is shipped to meet unmet demand at another, and stock can be held in shared warehouses until demand is known (Eppen 1979; Eppen and Schrage 1981). When the retailers are independent firms, pooling creates two questions at once. After demand is realized, the extra profit from shipping must be split in a way no group of retailers would reject. Before demand is realized, each retailer chooses its own stock, and that choice depends on how the split will be made. A split that is fair ex post may lead to stocking decisions that are poor for the system as a whole.
Anupindi, Bassok and Zemel (MSOM 2001) model the ex-post split as a cooperative game, the ex-ante stocking as a non-cooperative game, and ask whether a single allocation rule can serve both. Their framework is a standard reference for "coopetition" models in supply chains, where firms compete on stocking decisions and cooperate on redistribution.
There are retailers and warehouses . Retailer has unit cost , revenue and salvage value ; warehouse has purchasing cost and salvage value . Shipping from location to retailer costs per unit, and a fraction of the customers at accept service from .
Before demand, retailer chooses a position : local stock and claims on warehouse stock, so warehouse holds . A profile is . Demand is random with law . After demand, retailer has local sales , residual inventory and residual demand .
The snapshot allocation game SAG gives each coalition the value : the optimal value of the linear program (6), which ships units from to at profit per unit, subject to , and . Its core is the set of allocations with for every and (7).
An allocation rule AR- assigns surplus ; retailer earns
and expects . A Nash equilibrium (10) is a profile at which no retailer gains by changing its own position. The first-best profile maximizes the expected centralized profit , where .
The fractional rule AR-f (11) pays with fixed shares , . The dual allocation (8) is for optimal dual prices of (6) for . The modified rule AR-c is with .
For a first-best profile and a measurable choice of dual prices at ,
with integrable side payments.
The goal answers the paper's central question positively: there is an allocation mechanism under which the centrally optimal stock levels are an equilibrium of the decentralized stocking game, while every ex-post split of the pooling surplus is stable against all coalitions. Theorem 4.1 is the ex-post half: shadow prices of the shipping LP give a stable split for every realization, independently of who owns which units. The paper also shows (Proposition 5.1, not included here) that the dual allocation alone does not induce first-best stocking, which is why the side payments of Theorem 5.1 are needed.
The results are proved in the paper; Theorem 4.1 is proved there only by reference to the LP-game literature (Owen 1975; Samet and Zemel 1984). None of them has a machine-checked proof. The mission would produce the first formal treatment on Prove2Me of a linear-production (LP) game and its core, and of a model combining a cooperative second stage with a non-cooperative first stage.
Theorem 4.1 is an instance of Owen's theorem on LP games, but the instance is not a standard linear production game: coalition LPs have variables only on arcs inside the coalition, warehouse capacity is limited to the coalition's own claims, and the acceptance constraint divides by , which may be zero, so the general theorem cannot be quoted as it stands. The paper leaves the dual of (6) unwritten, and Mathlib has no ready-made LP duality in this form.
The stochastic layer is the other obstacle. Expected payoffs are integrals, and the side payment is built from a choice of dual prices for each demand realization. Its integrability requires measurability of that choice and of the LP value as a function of demand; neither is given by the paper, which treats the side payments as "constants".
Retailers are Fin N, warehouses Fin W, locations Fin N ⊕ Fin W; quantities, prices and demands are real numbers; demand is a probability measure on Fin N → ℝ; expectations are Bochner integrals. is the real supremum of (6a) over the feasible set, and profiles are required to be nonnegative, which makes the feasible set nonempty and bounded. Arcs with carry no shipment. The core is the platform definition Supermodularity.Cooperative.Core. The dual of (6) is written out explicitly (the paper does not state it). The paper's continuous-CDF assumption is not used and is dropped.
Pinned readings:
Not acceptable: a core without the efficiency equation (7b); a feasible set that lets sell to customers who balk; an arbitrary side payment instead of the constructed one; or a Nash equilibrium evaluated through non-integrable payoffs, whose Bochner integral is and makes every profile an equilibrium.
Useful infrastructure: finite-dimensional LP duality in inequality form, measurable selection of LP optimal solutions, and continuity of LP values in the right-hand side. All of it can be reused in other LP-game and two-stage stochastic programming missions.
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.