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?
Block coordinate descent (BCD), also called the nonlinear Gauss–Seidel method or alternating minimization, minimizes a function of several blocks of variables by exactly minimizing over one block at a time while the others are held fixed. It is used wherever the subproblem in a single block is cheap even though the joint problem is not: alternating least squares, EM-type updates, matrix and tensor factorization, Lasso-type regression with separable penalties, and decomposition methods for large structured programs.
Classical convergence theory for BCD asks for differentiability and strict convexity or uniqueness of block minimizers (Bertsekas and Tsitsiklis, 1989; Grippo and Sciandrone, 2000). Many applications have a nondifferentiable, extended-valued objective: a smooth or merely continuous coupling term plus separate penalties or constraint indicators on each block. Tseng (2001) gave convergence results for this setting. Its §5, formalized here, shows that the separable structure lets one drop continuity of on a level set and replace strict convexity by quasiconvexity and hemivariance in each block.
Timeline. Auslender (1976) proved convergence of cyclic BCD for strongly convex continuous on a product of closed convex sets with convex . Bertsekas and Tsitsiklis (1989, Prop. 3.9 in §3.3.5) treated continuously differentiable convex with block-wise unique minimizers. Grippo and Sciandrone (2000, Prop. 5.1) extended this to continuously differentiable, blockwise strictly pseudoconvex with each the indicator of a closed convex set. Tseng (2001, Prop. 5.1 and Thm. 5.1) covers lower semicontinuous, extended-valued under Assumptions B1–B3 and C1 or C2 below.
Fix and block dimensions . A point is with . The objective has form (1):
with and each taking values in . The effective domain of is .
A function is quasiconvex if for all and , and hemivariate if it is not constant on any nondegenerate line segment contained in .
The BCD method starts at . At iteration it chooses a block and sets and for . Under the essentially cyclic rule there is a constant such that every block is chosen at least once in any consecutive iterations.
A point is a coordinatewise minimum point of if for every block and every .
The assumptions of §5 are:
Under B1–B3, C1 or C2, and boundedness of for some ,
Without the level-set bound, for every essentially cyclic BCD sequence that is defined,
The milestone list follows the paper's proof: attainment of the block minimization on a bounded level set (p. 478); monotonicity of and membership of cluster points in (p. 485); claim (11), that consecutive iterates share limits along subsequences; its iterate (20) over a window of steps; inequality (21) at cluster points; Proposition 5.1 itself; and the remark (p. 483) that a quasiconvex hemivariate function has at most one minimum point.
The result. Theorem 5.1 guarantees that exact block minimization, applied in any order that visits every block within a bounded window, cannot accumulate at points where a single-block move still decreases . It applies to objectives that are neither differentiable nor continuous on their domain and that need not be convex, which covers problems with constraint indicators on each block and couplings with finite values on the boundary of their domain (Assumption C2). Convexity in each block alone is not enough for results of this kind: the paper notes (pp. 483–484) that Theorem 4.1(b) becomes false under that weaker hypothesis, because Powell's three-variable example is convex in each variable.
The formalization. The result is proved in the paper; no machine-checked proof of it, or of a BCD convergence theorem of this kind, has been published. A formal proof would supply a reusable account of extended-valued lower semicontinuous functions on product spaces, of subsequence arguments for descent methods, and of quasiconvexity and hemivariance, none of which is packaged for this purpose in Mathlib.
The obvious argument fixes a cluster point and a block and passes to the limit in the block-optimality of the iterates. That needs the iterates in which block was last updated to converge to the same , and nothing forces consecutive iterates to be close: BCD can oscillate between distinct limit points of different subsequences. Claim (11) supplies this, and it is where quasiconvexity and hemivariance are spent. The second obstacle is passing to the limit in , which is only continuous on its domain and only lower semicontinuous globally; Assumption C1 or C2 is what keeps the comparison points inside .
(k : Fin N) → EuclideanSpace ℝ (Fin (n k))), with 0-based blocks: paper block is Lean index . The product carries the sup norm of the blocks; boundedness, convergence, cluster points and semicontinuity are the same as for the Euclidean norm.EReal). Standing hypotheses: and every never take the value , so is never and is exactly when one summand is. The objective is always the sum , defined once, never a free function with an equation hypothesis.A statement that assumes claim (11), (20) or (21), or that the values converge, would trivialize the goal; the goal and Proposition 5.1 assume none of these.
A complete development needs: compactness of closed bounded sets in the product space and minimization of lower semicontinuous EReal functions on compact sets; subsequence extraction for cluster points; and the segment argument behind (11). Contributions of general lemmas on quasiconvex and hemivariate functions, and on lower semicontinuity of finite sums of EReal functions that avoid , are reusable beyond this mission and welcome.
AdaBoost (Freund and Schapire, 1996) combines many weak classifiers, such as small decision trees, into a single strong classifier by repeatedly reweighting the training data. In the late 1990s it was among the most accurate off-the-shelf classifiers, but why it worked was unclear. Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) gave a statistical explanation: AdaBoost fits an additive model by stagewise minimization of the exponential criterion , and the population minimizer of that criterion is half the log-odds of the class probability. Boosting is therefore a form of additive logistic regression. This reading underlies gradient boosting, LogitBoost, and the later theory of classification-calibrated surrogate losses.
The exponential criterion was introduced by Schapire and Singer (1998) as an upper bound on misclassification error, and Breiman (1997) used it in his analysis of AdaBoost. Lemma 1 of the 2000 paper is the statement that identifies its population minimizer.
A feature ranges over a measurable space and a label takes the values and . The pair has a joint law , a probability measure on , with marginal on . Disintegrating gives the conditional class probabilities and .
For a function the exponential criterion (11) is the joint expectation
a number in . Its conditional version at is . Given a current estimate , the weighted conditional expectation with weight is
and . The half log-odds is
Assume for -almost every . Then is measurable, and for every measurable ,
and, for -almost every , (13) and (14) hold:
Lemma 1 is what makes the rest of the paper a statement about logistic regression. Because the minimizer of is the half log-odds, an additive model built by minimizing estimates , and the transform (13) converts it into a class probability. Result 2 shows that one population step of Real AdaBoost from any starting point already reaches , so the many iterations used in practice come from the crude approximation of conditional expectations by trees, not from the criterion. Corollary 3 gives the first-order condition used to interpret the AdaBoost weights. The other missions of this series (Discrete AdaBoost, LogitBoost, Gentle AdaBoost, multiclass LogitBoost) all rest on these population facts.
All of these results are proved in the paper; none is open. What this mission adds is a machine-checked version in the population setting, with conditional probabilities obtained from an honest disintegration of the joint law instead of being postulated. No formalization of the exponential criterion's population minimizer is known to exist on the platform or in Mathlib. The pointwise calculus is elementary; the work is in the measure-theoretic layer.
The paper's proof minimizes the conditional criterion pointwise and sets the derivative to zero. Turning this into a statement about requires three things the one-line proof does not mention. First, the joint expectation must be rewritten as an iterated integral, which needs the disintegration of and measurability of everything integrated. Second, the pointwise minimizer must itself be a measurable function of , which the calculus says nothing about. Third, the comparison is against every measurable competitor, including those with , so integrability cannot be assumed. Corollary 3 has a further difficulty: it assumes nothing about the class probabilities, so a proof must show that optimality of forces them strictly between and almost everywhere, a fact the paper's one-line proof does not address.
Labels live on Bool, with sgn true = 1 and sgn false = -1. The joint law is ν : Measure (X × Bool) with [IsProbabilityMeasure ν] on an arbitrary measurable space X. is (ν.condKernel x {b}).toReal, read off Mathlib's conditional kernel. It is determined only -almost everywhere, so (13), (14), Corollary 3 and the identity of Result 2 are almost-everywhere statements; the conditional formula and its derivative hold at every . is a lower Lebesgue integral in . Competitors range over all measurable functions . Derivatives are stated with HasDerivAt.
The hypothesis almost everywhere is added to Lemma 1 and Result 2. Without it the ratio in (12) is or undefined, Real.log 0 = 0 would give a junk value, and no minimizer of exists. Corollary 1 assumes both labels occur in the region, which is the sample counterpart.
Several formalizations would make the targets trivial, and none is used here. Defining through its conditional formula would make milestone 1 a definition and the goal pointwise, so is the joint expectation under . A Bochner integral would return for a non-integrable and make every such a minimizer, so takes values in . A bare deriv is at points of non-differentiability. Writing the logistic transform as in place of would lose the factor that (15) records.
A complete development needs the disintegration of a measure on , iterated lower integrals, measurability of the conditional kernel, and elementary calculus of . Lemmas about conditional expectations against condKernel on a finite label set, and the measurability of , are reusable in the other missions of this series. Contributions of either kind are welcome.
Boosting combines many weak classifiers into a strong one. Friedman, Hastie and Tibshirani (Ann. Statist. 28 (2000) 337–407) explained the two-class AdaBoost algorithms statistically: in the population, boosting fits an additive logistic regression model by stagewise optimization of a criterion on the log-odds scale. Section 5 of that paper carries the explanation to classes. It answers two questions a practitioner faces when boosting a multiclass problem:
The paper's answer to the second question is LogitBoost for classes (Algorithm 6). Result 6 asserts that it takes quasi-Newton steps on the multinomial log-likelihood. Algorithm 6 underlies later multiclass gradient boosting, where the per-class Newton step with a diagonal Hessian and the factor reappears (Friedman, Ann. Statist. 29 (2001)).
Fix classes, labelled , and a measurable space of features. A probability measure on is the joint law of the feature and the class . The classes are mutually exclusive.
Definition 1 (p. 354) introduces the symmetric multiple logistic transformation
and states that it is equivalent to
For this is the two-class .
AdaBoost.MH (Algorithm 5) treats each class against the rest. Its population criterion is .
LogitBoost ( classes) (Algorithm 6, population version) keeps a fit and the probabilities given by (40). For each class it forms the working response and weight
It takes the weighted conditional mean , and updates
The multilogit parametrization with base class writes , so that . The multinomial log-likelihood of one observation is
Result 6 states that the LogitBoost algorithm ( classes, population version) uses quasi-Newton steps for fitting an additive symmetric logistic model by maximum likelihood. The goal states, for every and every current fit , the three facts the Derivation makes precise:
each minimizing the class--against-the-rest exponential criterion.
The result places J-class LogitBoost inside likelihood theory. Its population step is a Newton-type step for multinomial maximum likelihood. Two approximations separate it from the full Newton step: the Hessian is replaced by its diagonal, and the base class is averaged out. Result 5 shows that AdaBoost.MH, in contrast, solves decoupled one-against-the-rest problems whose implied probabilities need not sum to one. That contrast is the paper's argument for the coupled procedure.
All statements here are proved in the paper by direct calculation. They have not been formalized before. The mission produces machine-checked versions of the population claims and of the algebra behind them. That algebra comprises the softmax/centred-logit equivalence, the multinomial score and Hessian in base-class coordinates, and the base-class averaging identity. These pieces are reusable for any multinomial logistic or softmax model.
There is no deep step. The work lies in keeping two parametrizations apart: the base-class multilogit coordinates , with free entries, and the symmetric centred coordinates , with entries summing to zero. The derivatives are taken in . The algorithm and (40) live in . The step is converted back by symmetrization. Mixing the two makes the averaging identity false or vacuous.
A second point is that the update is not the Newton step . The page states this explicitly: for full Newton stepping the symmetrization would be redundant. The tempting shortcut of proving that Algorithm 6 equals the full Newton step therefore does not prove Result 6.
Fin J, with where needed.Fin J.ν.condKernel x.Trivializing encodings are ruled out:
HasDerivAt along coordinate lines, and the Hessian is the derivative of an explicitly given partial derivative, never a deriv equation that would be a junk at non-differentiable points.All objects are defined in one definitions file in the namespace AddLogReg.Multiclass. Proofs of any of the milestones are welcome. Lemmas on the softmax map, such as positivity, the derivative of log-sum-exp in base coordinates and shift invariance, are reusable beyond this mission.
Block coordinate descent (BCD), also called the nonlinear Gauss–Seidel method or alternating minimization, minimizes a function of several blocks of variables by minimizing over one block at a time with the others held fixed. It is used wherever the full problem is hard but each block subproblem is easy: proximal point methods, the Arimoto–Blahut algorithm for channel capacity, alternating projections, matrix factorization, and sparse regression with separable penalties. The basic question is what the limit points of the method are. Without assumptions they need not even be stationary: Powell (1973) gave a smooth three-variable function on which cyclic coordinate descent cycles among nonstationary points.
P. Tseng's 2001 paper (JOTA 109, 475–494) gave conditions under which the cluster points are stationary for nondifferentiable objectives of the form , with smooth on its domain and each an arbitrary extended-real function of one block. The paper is a standard reference for BCD on composite problems.
Timeline. Auslender (1976) treated the convex nondifferentiable case; Grippo and Sciandrone (Oper. Res. Lett. 26, 2000) the continuously differentiable case with closed convex block constraints, under pseudoconvexity assumptions; Zadeh (1970) the unconstrained differentiable case; Powell (1973) the counterexamples. Tseng (2001) unifies these in Theorem 4.1, which this mission targets, and adds a quasiconvex–hemivariate result (§5, the sibling mission).
Let and . A point is with coordinate blocks , and is the vector whose th block is and whose other blocks are zero. The objective has effective domain and, at , lower directional derivative
The BCD method starts at ; iteration chooses a block and sets
Under the essentially cyclic rule there is such that every block is chosen at least once in any consecutive iterations; the cyclic rule chooses block at iterations . The level set is .
A point is stationary if for all , and a coordinatewise minimum point if for all and all . The function is regular at if for every with for all . It is pseudoconvex in if whenever , is supported on blocks and , and ; it has at most one minimum in if every block- section has at most one minimum point.
Assume is compact and is continuous on . Then the BCD iterates are defined, and essentially cyclic runs are bounded. Moreover:
In (c), a cluster point at which is regular is moreover stationary.
The proof's steps, in attack order: the descent and attainment step; the limit relations (6)–(8) for the window limits of a convergent subsequence; claim (9) for (a), (b); the window collapse for (c); the §3 remark that a regular coordinatewise minimum is stationary; and parts (a), (b), (c) separately. Lemma 3.1 (regularity of under the smoothness assumptions A1 or A2 on ) is a companion target.
Theorem 4.1 is the convergence result that the paper's applications rest on: the proximal minimization algorithm, the Arimoto–Blahut algorithm and an algorithm of Han are all instances of BCD on functions of the form , and Lemma 3.1 supplies the regularity that turns coordinatewise minima into stationary points. Part (b) is sharp: Powell's example shows it fails if pseudoconvexity is weakened to convexity in each block.
None of these results has a machine-checked proof on the platform. A formalization would provide a reusable framework for block methods on extended-real objectives: one-sided directional derivatives in , block pseudoconvexity, and the subsequence-of-windows argument that recurs in the analysis of Gauss–Seidel and alternating methods.
The obvious argument says that a cluster point is the limit of iterates that each minimize in one block, so it minimizes in every block. This fails: the iterate that minimizes in block is not the iterate converging to but one of neighbours in a window, and these neighbours may converge to different points . Each is minimal only in its own block . Combining these windowed facts into a statement about one point is the content of the theorem. Under (a), (b) this uses regularity and pseudoconvexity in pairs, propagated along the window by induction (claim (9)). Under (c) it uses uniqueness of block minima to show that the window collapses. Powell's example shows that some such hypothesis is necessary. A second difficulty is extended-real bookkeeping: takes the value , directional derivatives may be , and limits must be taken in .
The Lean development lives in namespace TsengBCD.Stationary. The conventions are:
EReal. The standing hypothesis is that never takes the value , together with .dirDeriv is the EReal liminf over .Fin N indices and each block is EuclideanSpace ℝ (Fin (n k)). The product carries the sup norm, which does not affect any statement.s r is the block of iteration . The cyclic rule is s r = r mod N, and is .Continuity on . The hypothesis " is continuous on " is formalized as continuity of , as a map into , at every point of . The weaker reading, continuity of the restriction , makes the printed theorem false. Take , , and
with . Then is a compact ellipse together with the isolated point , and the restriction of to is continuous. The cyclic iterates have both coordinates positive and never meet the lines or . They converge to , yet . Part (c), which for has no uniqueness hypothesis, would assert that is a coordinatewise minimum. The limit step (7) of the proof needs continuity at points approached from outside . This repair excludes the paper's later application to the Arimoto–Blahut algorithm (Example 6.2), which is not part of this mission.
Trivializations ruled out. The goal does not assume the window limits, the relations (6)–(9) or the block pattern ; these appear only in milestones. The existence of runs is part of the goal, so the cluster-point claims are not vacuous.
Infrastructure needed. A complete development needs:
EReal liminf calculus (liminf of sums; nonnegativity of difference quotients);The EReal directional-derivative lemmas and the window extraction are reusable for the sibling mission (Theorem 5.1) and for other block methods. Proofs of any milestone are welcome, as are counterexamples showing that a hypothesis cannot be dropped.
Interior-point methods for linear programming are usually analysed under two assumptions: a strictly feasible starting point is known, and the problem has an optimal solution. In practice neither is known in advance. The homogeneous self-dual embedding of Ye, Todd and Mizuno (Math. Oper. Res. 19(1), 1994) removes both assumptions. It embeds a standard-form linear program and its dual into one artificial program that always has an obvious interior starting point. A solution of the artificial program either yields optimal solutions of the original pair or certifies that one of them is infeasible. The embedding underlies the infeasibility detection of several interior-point LP and conic solvers.
The paper's main result is an iteration bound. Section 4, "Analysis of the output", asks a different, practical question: what can be read off the iterates if the algorithm is stopped early, at an approximate solution? Theorem 8 answers it. This mission formalizes Theorem 8 and the results its proof uses.
Let , , . The primal and dual programs are
with dual slack . An optimal solution pair is an optimal of (LP) together with an optimal of (LD).
Write for the all-ones vector and set , , . The homogeneous self-dual program (HLP), in the paper's normalization , , has variables with , , :
is its feasible set and the subset with . A self-complementary solution is an optimal solution of (HLP). A strictly self-complementary one also has and . For a point of (HLP) put , and for let
The predictor–corrector algorithm with starts at . At even (predictor step) it solves the Newton system (11)–(12) with target and moves along the direction by the largest step that stays in (13). At odd (corrector step) it solves the system with target and takes a full step.
For every predictor–corrector sequence :
for all .
In the order the proof uses them:
Theorem 8 is a stopping criterion. Either stays bounded away from zero, which happens exactly when (LP) has an optimal solution, or and go to zero at the same rate while stays bounded away from zero. An implementation can therefore watch and and decide the status of (LP) from an approximate iterate, without the exact rounding procedure needed for the bound. The bounds hold for real data, with no integrality and no bit length.
Theorem 8 has a published proof on one page, building on the self-duality facts of §2 and the Mizuno–Todd–Ye step analysis. None of it is machine-checked. A complete development would give a verified account of the homogeneous self-dual embedding, including:
These are the ingredients of every analysis of the embedding. Homogeneous self-dual programs appear on Prove2Me in other conventions (Vanderbei's (22.4) and (22.21), Matoušek's (SD)), but their statements concern different programs: no artificial variable , no normalizing row. They do not formalize any statement here.
The two branches of Theorem 8 rest on facts of different depth.
The obvious first idea is to treat Theorem 8 as a consequence of Theorem 6. It fails: Theorem 8 is about every iterate of an infinite run and uses no iteration count. The constant depends on the instance and is not explicit.
A : Matrix (Fin m) (Fin n) ℝ, b : Fin m → ℝ, c : Fin n → ℝ, with no rank assumption and no integrality. (LP)/(LD) feasibility and optimality are built on the published general-form LP definition LinearOptimization_DualLP. "(LP) has a solution (feasible and bounded)" in Theorem 3 is read as "(LP) has an optimal solution".y x τ θ s κ. The slacks are pinned to the constraint expressions. (HLP) is defined for general ; the instance (7) is obtained by substitution. Optimality means minimizing the objective over , not "", so Theorem 2 (iv) is not built into the definition.IsPCSequence: , and each step is for some solution of (11)–(12). The relation is needed because is not unique when is rank-deficient.Needed infrastructure: LP duality and Goldman–Tucker strict complementarity for real standard-form programs, and the skew-symmetric orthogonality lemma. These are reusable well beyond this mission. Proofs of any milestone, and alternative arguments (e.g. via the central-path limit) for the existence of , are welcome.
Many linear programs that arise in combinatorial optimization have a few "complicating" constraints on top of a set over which linear optimization is easy: multicommodity flow, where is a product of single-commodity flow polytopes; scheduling and the Held–Karp bound, where is a polytope of assignments or trees. Plotkin, Shmoys and Tardos showed that for such problems an approximate solution can be found with a number of calls to the linear optimizer over that depends on the required accuracy and on a structural quantity, the width, but only logarithmically on the number of constraints. Their packing and covering algorithms (§§2–3 of the paper) assume nonnegative data. Section 4 removes that assumption and treats an arbitrary system of linear inequalities over a convex set. This framework, later known as the multiplicative-weights method for linear programs, is among the standard tools of approximation algorithms (Arora, Hazan and Kale's 2012 survey gives the modern account).
Timeline. Shahrokhi and Matula (1990) gave an exponential-potential algorithm for the maximum concurrent flow problem. Plotkin, Shmoys and Tardos (FOCS 1991; Cornell ORIE Technical Report 999, 1992; Mathematics of Operations Research 1995) generalized it to fractional packing, covering and the general problem of this mission. Grigoriadis and Khachiyan (1994–1996) obtained related bounds for block-angular and convex resource-sharing problems. Garg and Könemann (1998) and Arora, Hazan and Kale (2012) gave width-free or simplified variants.
An instance of the GENERAL problem consists of an arbitrary real matrix with rows , an arbitrary vector , a convex set , and a positive vector that sets the scale of the allowed error. The question is whether some satisfies . Such a point is an exact solution; a point with is an -approximate solution.
For write
the least with ; it may be negative. The width is . Access to is through subroutine (10): given in , return minimizing over . For a dual vector let . The relaxed optimality conditions for a point with and a dual vector are
The dual solution corresponding to with parameter is , and its potential is . Procedure IMPROVE-GENERAL (Figure 4) starts from with , fixes and a step size , and, while and fails, replaces by , where is the oracle's answer for the current dual solution. The driver calls IMPROVE-GENERAL repeatedly, stopping with an -approximate solution or with a report that none exists.
For every , every start and every exact minimizing oracle, the driver stops; an output point is an -approximate solution; an infeasibility report is correct ( with ); and the number of oracle calls is at most
The result gives an -relaxed decision procedure for any system of linear inequalities over a convex set with a linear-optimization oracle, with no sign conditions on the data. Its oracle-call count is independent of and logarithmic in , which is what makes it useful when is large and has a fast combinatorial optimizer. The simultaneous packing-and-covering problem is the special case where every row is either nonnegative or nonpositive; the paper's width-reduction techniques (§5) and applications (§6) build on this procedure and on its packing and covering counterparts.
The paper's statements use and ; this mission states the explicit constants that the paper's own proofs give. The result is proved in the literature; no machine-checked proof of it is known on Prove2Me or in Mathlib. It also records a gap in Figure 4 (below) and states the theorem for the smallest correction that makes the paper's proof go through. Formalizing the analysis yields reusable potential-function arguments (second-order bounds on , geometric decrease of a potential between two levels) of the kind used throughout multiplicative-weights analyses.
The correctness half is short; the complexity half carries the weight. Lemma 4.3 needs a second-order bound on the exponential that is valid only when the step changes each exponent by at most , so the step size must be tied to and . Theorem 4.4 then has to control the potential between a ceiling and a floor while moves, and Theorem 4.5 has to sum the per-call bounds over a sequence of calls whose halves each time, so that the last call dominates.
The first reading of Figure 4 fails here: Figure 4 fixes and from , but the loop runs for every . For the hypothesis of Lemma 4.3 fails, and the decrease bound from its proof becomes negative for . At , the hypothesis of Lemma 4.2 requires , which the printed does not meet, so and the infeasibility certificate are not guaranteed. With the printed parameters, the iteration bound is not established by the paper's argument.
Fin m with ([NeZero m]), coordinates by Fin n; is a real matrix and , real vectors with ; is a convex set. No sign hypothesis is put on , or .Fin m, second-order bounds on Real.exp and monotonicity of Real.log, convex combinations, induction over fuelled recursions. The potential-decrease lemmas are reusable for the packing and covering missions of the same paper. Proofs of any milestone are welcome independently.A retailer deciding how many variants of a product to carry (colours, sizes, flavours) faces a trade-off. A broader assortment captures customers whose favourite variant would otherwise be missing, but it splits demand into more, smaller streams, each of which needs its own safety stock. van Ryzin and Mahajan (Management Science 45(11), 1999) combine a multinomial logit model of customer choice with a newsvendor model of inventory and show that the optimal assortment always consists of the most popular variants for some (their Theorem 1). That reduces "how much variety" to a single index, and the paper's Theorem 2 then answers which economic parameters push that index up or down: the selling price, the strength of the customers' outside option, and the store's traffic volume. These comparative statics are the paper's main managerial predictions (high-margin categories and high-traffic "super stores" carry more variety; categories with a weak outside option carry less), and they are what later work on assortment planning cites the model for.
There are variants . Variant has a preference and the option of buying nothing has preference . The variants are numbered so that , and denotes the set of the most popular variants (, ).
When the store offers an assortment , each customer buys variant with the multinomial logit share
Each variant sells at price and costs per unit, with . Let be the standard normal distribution function and define the critical fractile ; it moves with .
Two models of aggregate demand are compared. In the independent population model, customers arrive on average, demand for variant is normal with mean and standard deviation , where and , and each variant is stocked at its newsvendor optimum. The resulting optimal expected profit is
In the trend-following population model all customers make the same choice, so variant sells units with probability and nothing otherwise, and the optimal expected profit is
Inside the proofs, and denote the shares on and on .
For all :
The goal is a single Lean theorem whose conjuncts are (a), (b) and (c), each for every admissible value of the parameters held fixed. In the trend-following half of (b) it carries the extra hypothesis ; see Formalization scope.
together with the strict version. 3. Equation (14): if and only if , with the strict version. 4. and the left side of (13) are increasing in on . 5. As , , so . 6. As , the numerator of the right side of (13) converges to a positive constant. 7. The left side of (13) is increasing (and unbounded) in .
The result. Theorem 2 gives three qualitative predictions with opposite signs, all from one model: higher margins favour broader assortments, a vanishing outside option favours narrower ones (customers then buy something regardless, so extra variants mainly cannibalise each other and add safety stock), and in the independent model higher volume favours broader assortments through risk pooling, a scale economy that the trend-following model does not have because its profit is proportional to . Combined with Theorem 1 these statements locate the optimal number of variants, not only its direction of change.
Formalizing it. The theorem is proved in the paper, but the published argument is a sketch: the positivity of the limiting numerator in (b) is asserted ("one can easily show"), and the trend-following half of (b) is dispatched in one sentence that does not cover every case (see below). A machine-checked development fixes exactly which hypotheses each part needs. No part of this paper has been formalized before, and Mathlib has no normal quantile function; the development of and of the monotonicity of in is reusable for any newsvendor analysis.
The comparisons are between finite sums of real powers of shares whose denominators all move with the parameter. Three steps are not routine. For (a), the left side of (13) is a product of and , and is not monotone in (it decreases while , i.e. while ); so monotonicity of the product depends on the shape of the normal distribution, and part (a) also needs this left side to grow without bound, which the paper does not state. For (b), the positivity of the limiting numerator is where the ordering and enter; it fails for unordered preferences. For the trend-following half of (b), the positive parts make the comparison piecewise, and the strict inequality can fail outright.
All objects live in RetailVariety.Statics. Variants are Fin n, 0-based (the paper's variant is ⟨j-1, _⟩), and is A n i, the indices with value below , so . The preferences are v : Fin n → ℝ with 0 < v j and Antitone v; is a separate real v0, not a variant. The shares are share v v0 S j. is ProbabilityTheory.cdf (gaussianReal 0 1), and is criticalFractile p c, the infimum of ; it is a function of , never a free parameter. Powers are real powers (Real.rpow); shares of offered variants are positive, so the convention does not enter. is max x 0. Price, cost, volume, , and are explicit arguments of profitI and profitT.
"Sufficiently high/low" is encoded as an eventual statement: ∀ᶠ p in atTop, ∀ᶠ v0 in 𝓝[>] 0 (a right limit, since ), ∀ᶠ lam in atTop. Fixed parameters stay in the paper's ranges: , , throughout, and in (a), in (b) and (c).
One deviation from the printed statement. In the trend-following model, part (b) as printed is false: with , , and , every share is below , so for every . The goal therefore assumes for that conjunct only (the most popular variant earns a positive margin on when ); the condition is also necessary for the strict inequality.
Formalizations that would trivialize the mission are ruled out: an existential ("for some ") in place of the eventual quantifiers; non-strict inequalities in the goal; a critical fractile independent of ; dropping the trend-following half of (a); and equal preferences or a fixed number of variants.
Needed infrastructure: the normal quantile and its basic properties, monotonicity facts about the normal distribution function and density, limits of the shares as , and elementary inequalities for with . Proofs of any milestone, and of the quantile facts as standalone lemmas, are welcome.
Prediction with expert advice asks a learner to predict a binary label on each of a sequence of trials, after seeing the predictions of a pool of candidate functions, and to make few more mistakes than the best member of the pool. Littlestone and Warmuth's The Weighted Majority Algorithm (Inform. and Comput. 108, 1994) gave the deterministic algorithm WM and its randomized variant WMR, and proved worst-case bounds that hold for every sequence of trials, with no probabilistic assumption on the data. Their §8 asks how good such bounds can possibly be when the data contain anomalies: disagreements with a candidate function, counted relative to the best-fitting member of the pool. Such disagreements can arise from noise in the instances or labels, or from instances that do not determine the label.
For the randomized algorithm WMR the expected number of mistakes grows, by Corollary 6.1 of the paper, at rate per anomaly, which tends to as . Theorem 8.2 shows that no randomized learner, however it is built, can do better than rate : an adversary who fixes the sequence in advance can force half the noise-free optimum plus one expected mistake per anomaly. Together with the deterministic counterpart, Theorem 8.1 (rate ), it locates the cost of label noise in online learning exactly. Mistake-bound lower bounds of this kind are a standard reference point for the analysis of online classification and of the expert-advice algorithms descended from WM (Cesa-Bianchi and Lugosi, Prediction, Learning, and Games, 2006).
Timeline: Littlestone (1988) characterized the optimal noise-free mistake bound by complete mistake trees (the Littlestone dimension); Littlestone and Warmuth (FOCS 1989; journal version 1994) introduced WM and WMR and proved Theorems 8.1 and 8.2.
Let be an arbitrary domain and a pool of functions , finite or infinite. A trial is a pair with and ; a sequence of trials is a finite list , in which an instance may repeat with different labels. The number of anomalies of with respect to is , and is the collection of sequences for which some has at most anomalies.
A deterministic algorithm maps the past trials and the current instance to a predicted label; counts its wrong predictions, and
A randomized algorithm uses random choices independent of the sequence. On a fixed sequence its behaviour at trial is summarized by , the probability that it predicts given the preceding instances and labels and the current instance; its expected number of mistakes is , and
the infimum ranging over all maps from (past trials, current instance) to .
For every pool with and every integer ,
Both sides live in ; when the statement says .
"For any pool of functions there exists a complete -mistake tree" ([Lit88]). On the platform this is the proved Lemma 21.7 of Shalev-Shwartz and Ben-David, , together with Lemma 21.6, for every ; a tree shattered by is a complete mistake tree.
The theorem shows that the expected-mistake bound of WMR is optimal in its dependence on the number of anomalies: its coefficient of approaches , and no randomized learner achieves a smaller one on every pool with two or more functions. It also quantifies the advantage of randomization: the deterministic rate is (Theorem 8.1), the randomized rate is , and the noise-free term halves. The lower bound is obliviously adversarial, since the sequence is chosen before any coin is tossed, so it applies equally to the stronger model in which the adversary adapts to the learner's predictions.
The result has been proved since 1994. To our knowledge it has no machine-checked proof; the platform holds the Littlestone-dimension characterization of the noise-free optimum (Shalev-Shwartz and Ben-David, Chapter 21) but no statement about anomalies or randomized lower bounds. This mission formalizes the definitions of anomalies, and , and the theorem.
An adversary against a randomized learner cannot react to its predictions: the whole sequence, instances and labels, must be fixed in advance, so the adaptive adversary that proves the deterministic bound is not directly available. The lower bound must instead come from the learner's prediction probabilities, which depend only on the sequence prefix; the content of the theorem is that this information is enough to construct, for every learner, one fixed sequence that stays inside while forcing the stated expected count. Taking the infimum over learners inside an extended-real supremum over sequences of every length adds bookkeeping when is infinite.
Sequences are Fin T → X × Bool for every T : ℕ. Deterministic algorithms, the mistake count, shattered trees and the Littlestone dimension are reused from the published definition UnderstandingML_Online (OnlineAlg, mistakes, ShattersTree, ldim, soa); randomized algorithms are its OnlineAlgR X := List (X × Bool) → X → ℝ restricted by IsRandAlg to values in , and the expected mistake count is its cumLoss. is a natural number. takes values in ℕ∞ and in ℝ≥0∞; the paper's "minimum" is read as an infimum. is F.Nontrivial, which admits infinite pools.
The reduction of randomized algorithms to probability maps is the main modelling choice: on a fixed sequence the expected number of mistakes of any algorithm whose randomization is independent of the sequence equals , and every map with values in is realized by such an algorithm, so the two infima coincide. Dropping the constraint , or quantifying only over deterministic algorithms, gives a different quantity and is ruled out.
Needed: the definitions above, and the existence of a complete -mistake tree, available through the proved platform theorems on ldim and soa. Lemmas relating mistakes along a path of a shattered tree to ldim, and a reusable statement that an oblivious adversary can force expected loss per trial, would serve other lower bounds in the Littlestone–Warmuth series and in online learning generally. Contributions of such lemmas are welcome.
Many security-relevant inputs are noisy and do not repeat exactly: fingerprint minutiae, iris codes, lists of personal preferences, the set of features extracted from a document. A cryptographic key derived from such an input must be reproducible from a later, slightly different reading, without storing the input itself. Dodis, Ostrovsky, Reyzin and Smith (SIAM J. Comput. 38(1), 2008; arXiv:cs/0602007) introduced secure sketches for this purpose: public helper data that lets the holder of a nearby reading recover the original exactly, while revealing as little as possible about it.
When the input is a set of features, the natural distance is the size of the symmetric difference. Juels and Sudan proposed the fuzzy vault for this setting (Des. Codes Cryptogr. 38, 2006). Section 6.2 of Dodis et al. gives a simpler, deterministic variant, the improved Juels–Sudan sketch (Construction 5), whose storage and entropy loss are both for -element subsets of an -element universe, independent of . The paper's Theorem 6.1 is the analysis of that construction. This mission formalizes it.
Laws and average min-entropy. A random variable is identified with its law. For a pair ,
which equals , the average min-entropy of §2.4: the negative logarithm of the best probability of guessing after seeing .
Secure sketches. Let be a set with an integer-valued distance . A pair of procedures is an average-case -secure sketch (Definitions 3 and 4) if
The difference is the entropy loss.
The metric. For a finite universe with , is the set of -element subsets of with .
Construction 5. Identify with a finite field of elements and let .
The Lean development names these charPoly, sketchCoeffs, sketch, pHigh, Step3Cond and recover, and the metric SDifS with distance sdifDist, in the namespace FuzzyExtractors.ImprovedJS.
For every finite field with elements, all and every real ,
The goal is uniform in : the entropy loss does not depend on the input distribution.
The paper's argument on p. 21 splits into four steps, each a milestone:
A fifth, off the goal's path, records Step 2's remark that the sketch consists of the first elementary symmetric polynomials of , up to sign.
The security half is the entropy bound: since takes at most values, (the paper cites its Lemma 3.1, which is posed in the first mission of this series and is not restated here).
The result. Theorem 6.1 gives a secure sketch for set difference whose sketch length and entropy loss are , which the paper shows is essentially optimal when (§6.2, via Lemma C.1 and a constant-weight code bound). It improves the original fuzzy vault, whose entropy loss the paper analyses in Appendix D and finds good only when the stored data is very large. Through the paper's generic composition with randomness extractors (Lemma 4.1), it yields fuzzy extractors for set-valued inputs in large universes, the regime of biometric feature sets.
Formalizing it. The theorem is proved in the paper; no machine-checked version exists on Prove2Me or, to our knowledge, elsewhere. A formal proof combines three pieces of reusable infrastructure: a probabilistic layer (average min-entropy of laws on arbitrary types, and the chain-rule-type bound for a function with few values), the combinatorics of symmetric differences of equal-size sets, and the algebra of Reed–Solomon unique decoding (a low-degree polynomial is determined by its values on enough points). Each of these is useful beyond this mission.
No step is deep; the difficulty is in the bookkeeping. The correctness argument relies on exact degree accounting: must agree with in every coefficient of degree at least , so that the remainder has degree at most , and the uniqueness count ("two candidates agree on at least points") requires the threshold to be at least ; the paper's sentence says "more than", which does not support the argument as written. The roots of must be shown to form exactly the set , with no multiplicities lost. The security half needs the average min-entropy of a joint law with a deterministic, -valued component bounded uniformly over all auxiliary variables, including those with infinite or uncountable range, where sums are infinite sums of extended nonnegative reals.
Conventions committed to in Lean:
PMFs; the procedures are kernels M → PMF S, here deterministic (PMF.pure). Average min-entropy is the joint form above, logarithms base 2, and the auxiliary ranges over an arbitrary ι : Type (a superset of the paper's ), never restricted to finite types.[Field 𝔽] [Fintype 𝔽], with = Fintype.card 𝔽; the paper's " is a prime power" is then automatic.degree < s - t, so when .A formalization that checks only correctness, drops or trivializes the entropy clause, or lets see itself, would not be Theorem 6.1. The goal states both clauses through the definition of an average-case secure sketch, with given only and the sketch.
Contributions welcome: proofs of the milestones, a general lemma bounding average min-entropy loss by the logarithm of the number of sketch values (the paper's Lemma 2.2(b) and Lemma 3.1), and Reed–Solomon uniqueness lemmas stated for reuse.
Monotone comparative statics asks when the optimal choice of an agent moves in a predictable direction as a parameter of the problem changes: does a firm hire more of every input when the output price rises, does a monopolist raise its price when its marginal cost rises? Topkis (1978) gave a cardinal answer: if the objective is supermodular in the choice and has increasing differences in , the set of maximizers is nondecreasing in . Milgrom and Shannon (1994) replaced these conditions by ordinal ones, quasisupermodularity and the single crossing property, and showed in their Monotonicity Theorem that the ordinal conditions are both necessary and sufficient for the argmax to be monotone in the parameter and the constraint set.
Supermodularity is therefore never necessary for monotone comparative statics. Theorem 10 of Milgrom and Shannon identifies a setting where it is: when the objective must keep the ordinal properties after adding an arbitrary linear price term (or subtracting an arbitrary nonnegative cost ), the only objectives that qualify are the supermodular ones. This is the situation of a price-taking firm whose revenue or cost is linear in its activity levels, and the result explains why supermodularity is the natural assumption in such models even though the ordinal theory does not require it.
Let be a lattice: a partially ordered set in which every two elements have a least upper bound (join) and a greatest lower bound (meet). On the order is componentwise, so and are the componentwise maximum and minimum; on a product the order is the product order. For , .
A function is supermodular if for all . It is quasisupermodular if, for all , (i) implies , and (ii) implies .
Let be a partially ordered set and . The function has increasing differences in if for the difference is nondecreasing in . It has the single crossing property in if for all and , implies , and implies . The function is quasisupermodular in if is quasisupermodular for every , and nondecreasing in if is nondecreasing for every .
In the Lean development the domain is Fin n → ℝ, is curried as f : (Fin n → ℝ) → ℝ → ℝ, is p ⬝ᵥ x, and supermodularity and increasing differences are the published Supermodularity.Monotonicity.SupermodularOn and IncreasingDifferencesOn with the domain Set.univ.
Let . Then
and, if is nondecreasing in ,
Here " is supermodular" means supermodular on the lattice , jointly in .
The result. The Monotonicity Theorem shows that the ordinal conditions are exactly what monotone comparative statics needs for a single objective. Theorem 10 shows that the cardinal conditions are exactly what is needed for a family of objectives closed under linear prices. It separates two questions that are often conflated: whether a particular optimization problem has monotone solutions (ordinal), and whether a model's monotonicity conclusion is robust to the prices or costs the modeller adds to it (cardinal). The second sentence specializes to the economically common case of nonnegative input costs, where the restriction to is offset by the monotonicity of .
Formalizing it. The result is proved in the paper, with the converse direction given in detail only for the step "supermodular in " and the remaining cases left as "similar arguments". The mission produces machine-checked proofs of both equivalences, including the cases the paper does not write out: the recovery of increasing differences from the single crossing property under all price perturbations, and the recovery under the sign restriction . No part of Milgrom and Shannon's paper was found formalized on the platform when this mission was drafted; Topkis's supermodularity theory is partly available on the platform as the Supermodularity.* series.
The forward direction is a chain of short implications. The content is in the converse: from purely ordinal information about many functions one must recover a cardinal inequality. The single crossing property and quasisupermodularity only compare values of one function at two points, so a single perturbation can never yield an inequality between sums of four values; the argument must choose, for each violating configuration, a price vector that makes two of the four values tie, and the choice must be compatible with the sign constraint in the second statement. That compatibility is where the hypothesis that is nondecreasing in enters, and without it the second equivalence fails. A second subtlety is the decomposition of joint supermodularity on into supermodularity in and increasing differences in , which the paper uses without statement; the platform does not yet have it.
Fin n → ℝ with Mathlib's pointwise order and lattice operations; is arbitrary. The product carries Mathlib's product order.QuasiSupermodularOn and SingleCrossing are shared with the two sibling missions on Milgrom and Shannon's Theorems 4 and 8 and will be merged with them. A lemma decomposing supermodularity on a product lattice into supermodularity in each factor and increasing differences would be reusable well beyond this mission; contributions of such general lattice lemmas are welcome.Interior-point methods solve linear programs in polynomially many iterations, but the classical analyses assume something about the instance before the algorithm starts: a known strictly feasible primal–dual pair, a nonempty interior, or a big- bound on the feasible region of order , where is the bit length of the data. In practice none of this is known in advance, and an infeasible or unbounded instance should be reported rather than assumed away.
Ye, Todd and Mizuno (1994) removed these assumptions. They embed a standard-form linear program and its dual into a single homogeneous and self-dual artificial program (HLP), which always has a known interior starting point, and apply the Mizuno–Todd–Ye predictor–corrector method to it. The resulting algorithm needs no regularity assumption, no big- parameter, and an iteration bound, the best known for interior-point methods. Self-dual embeddings of this kind are now the standard initialization in interior-point solvers for linear and conic programs.
Timeline. Karmarkar (1984) gave the first polynomial interior-point method on a homogeneous canonical form. Mizuno, Todd and Ye (1990) introduced the predictor–corrector method with iterations under a known interior start. Kojima, Mizuno and Yoshise (1993) built a self-dual big- artificial problem. Ye, Todd and Mizuno (1994) combined homogeneity and self-duality without big , obtaining the result formalized here.
Given , , , the primal problem is (LP) and its dual is (LD) , with dual slacks .
Fix , , and put , , . The homogeneous self-dual program (HLP) in the variables is
Its feasible set is , and is the subset with . A strictly self-complementary solution is an optimal solution with and . The paper then fixes , , so the objective is and .
With , the neighborhood of the central path is (Euclidean norm). The predictor–corrector algorithm starts at . At even steps it solves a Newton system with centering parameter and moves by the largest step keeping the iterate in . At odd steps it takes a full Newton step with . A termination projection then solves a least-squares problem on the columns where and produces a candidate exact solution.
For integer data with bit length and , there is an absolute constant and a finite predictor–corrector run that reaches, within
iterations, an iterate whose termination output either has with optimal for (LP) and optimal for (LD), or has with and (LD) infeasible, or and (LP) infeasible.
The same bound, with the conclusion that the termination output, rescaled to the normalization , is a strictly self-complementary solution of (HLP).
Proposition 1 (self-duality of skew-symmetric programs), Theorem 2 (ii), (iv), (v), Theorem 5 (ii), the two Mizuno–Todd–Ye estimates in the proof of Theorem 6, the predictor-step and corrector-step claims, the termination claim, the integrality and size of the (HLP) data, and Theorem 3 (i), (ii).
The result. Corollary 7 gives a single polynomial algorithm that decides the status of an arbitrary linear program. It returns optimal primal and dual solutions when they exist and an infeasibility certificate otherwise. It needs no Phase I, no big- constant and no interior assumption, and its iteration count matches the best bound known under those assumptions. Theorem 3 is the bridge: an exact strictly self-complementary solution of (HLP) determines the status of (LP) and (LD).
Formalizing it. The paper's result is proved; no machine-checked proof of it is known. The mission produces a formal account of the self-dual embedding, the central-path neighborhood analysis for (HLP), an exact finite-termination step from an approximate iterate, and the reading of a bit-length complexity bound with explicit quantifier order. The neighborhood estimates and the bit-length machinery are reusable for other interior-point and complexity results.
The per-step estimates are short calculations once the orthogonality is available. The step that resists is termination. Geometric decrease of the gap reaches in iterations, but turning such an iterate into an exact strictly self-complementary solution requires a quantitative separation: on , once the gap is below , the comparison must identify the optimal partition and the least-squares projection must land in the positive orthant. That separation bound rests on determinant estimates for integer matrices (Hadamard-type bounds in terms of ) and on the strict complementarity of (HLP), neither of which comes from the iteration analysis itself. A second subtlety is that the algorithm is not a function: without a rank assumption the Newton system leaves undetermined.
LinearOptimization_DualLP). The self-dual objects of the Vanderbei and Matoušek series are different embeddings and are not reused.A complete development needs: skew-symmetric LP duality and strict complementarity (Goldman–Tucker) for (HLP), the Mizuno–Todd–Ye neighborhood calculus, and Hadamard-type bounds on integer determinants. Contributions to any milestone, or to these supporting libraries, are welcome.
Inventory pooling lets several locations serve their combined demand from one stock of goods. Classical newsvendor analysis predicts lower optimal cost when pooling reduces demand variation, but the reduction can vanish when demands are perfectly correlated. Xuanming Su asks whether that conclusion survives when managers make noisy stocking decisions rather than always choose the optimum. In the published 2008 article, Bounded Rationality in Newsvendor Models, the decision noise follows a continuous logit model, in which better quantities are chosen more often. Proposition 7 gives conditions under which pooling strictly lowers expected cost, including a case where classical pooling has no cost gain. Su, 2008
The question matters for multilocation inventory systems because an order quantity is a decision as well as a response to demand. Pooling changes both the distribution of demand faced by the system and the number of independently chosen orders. A comparison based only on optimal costs leaves the second change out. This mission isolates the paper's mathematical claim about the combined effect of demand and decision variation. Su, 2008, §9
There are locations. Demand at location is normally distributed with mean and standard deviation . The total demand has normal law with mean and standard deviation . An order of against a realized demand incurs holding cost for unsold units and backlog cost for unmet demand. Its expected cost is . The decentralized system incurs one such cost at each location; the pooled system orders once for total demand. The published InventoryControl_newsboy definition supplies this Gaussian expected cost, with the same orientation of holding and backlog penalties as Su's equations (29) and (31). Su, 2008, p. 584
For an expected profit function on a decision set , the logit choice density is proportional to on , where is a common bounded-rationality parameter. Larger spreads choices more widely; smaller positive concentrates them near high-profit choices. For normal demand, the decision domain is all of . With and , expected profit differs from minus expected cost by a constant independent of the order. The same logit law is therefore obtained from utility . The random behavioral order is denoted at location and for the pool. Su, 2008, pp. 571–572, 584
The goal is Proposition 7. Under positive holding and backlog costs, one common positive , at least two locations, positive individual standard deviations, and
the claim is
The first standard-deviation inequality is automatic for the sum of jointly normal demands. The second excludes a total demand whose standard deviation is smaller than an individual location's. The result still includes perfect positive correlation, where the first inequality is an equality. Su, 2008, Proposition 7, p. 585
Five milestones record the source's route to that comparison: invariance of the choice distribution under an order-preserving affine change of quantity (Lemma 1), invariance under an additive shift in utility (Lemma 2), standardization of the Gaussian newsvendor objective (equation (63)), the optimum of the canonical standard-normal newsvendor and the nonpositivity of its profit, and the comparison of its expected values at different positive scales. The milestone text preserves the wording of the printed article; the precise Lean conditions and corrections are stated with the items. Su, 2008, pp. 572, 587–588
The strict inequality separates two mechanisms of pooling. Demand aggregation can reduce variability, while a single pooled order also avoids accumulating the costs of several noisy decisions. Proposition 7 shows that the latter mechanism can make the cost reduction strict even when perfect correlation removes the usual variance benefit. It provides a condition that can be checked from individual and total standard deviations, rather than requiring an explicit covariance matrix in the final comparison. Su, 2008, pp. 584–585
The result is proved in the paper; the remaining task is a machine-checked formalization of its definitions and argument. The Gaussian expected-cost object is already published on Prove2Me, while the continuous logit law and this behavioral pooling theorem are new to this mission. The invariance statements and canonical profit comparison are reusable wherever a continuous logit rule acts on a transformed one-dimensional objective.
The usual pooling comparison evaluates cost at an optimal order. Here each system draws its order from a different continuous probability law, and the cost to compare is averaged over those choices. Comparing with alone does not compare the logit distributions; in particular, it gives equality under perfect positive correlation while the target is strict. A formal development must also show that the normalizing integrals and the resulting cost expectations are genuine finite integrals for every set of parameters covered by the theorem.
The Lean model uses Mathlib's real Gaussian law with variance and the published InventoryControl_newsboy.newsboyCost for equations (29) and (31). It records the choice density, CDF, expectation, canonical profit, and behavioral expected cost as separate definitions. The behavioral density uses on ; the utility shift from profit is covered by Lemma 2. The theorem specifies normal marginals and a normal total with mean and standard deviation . Every jointly normal demand vector in the paper yields these laws, and the final comparison uses no further feature of its joint distribution.
The conditions , , and are standing readings needed for the continuous choice law on the unbounded domain. Proposition 7 additionally states and : for one location the alleged strict comparison becomes equality, while zero variance makes the paper's continuous density on a point support undefined. Lemma 1 requires positive affine scale because a negative scale reverses CDF order, and its two invariance lemmas require a finite positive normalizer. Equation (66) is read with , as dictated by the surrounding formulas; the printed display drops the word “min.” These corrections and the cost-based choice convention are recorded item by item in the moderation notes.
No optimizer is supplied as a free variable, and no zero normalizer is allowed to turn a logit expectation into a trivial zero. Useful solver contributions include proofs that the cost-based logit normalizer and expected cost are integrable, Gaussian change-of-variables lemmas, and the strict scale comparison. These analytic facts can serve other continuous-choice models.
The queue has identical servers, a general arrival process, and independent service times with a common distribution . In the Halfin–Whitt regime the number of servers and the offered load grow together, so that the fraction of delayed customers stays strictly between and . This is the standard asymptotic model of large call centers and service systems (Halfin and Whitt, Operations Research 29, 1981, doi:10.1287/opre.29.3.567). For exponential service times the diffusion limit has been known since 1981; for general service distributions the queue length is no longer Markov, and its limit requires a different device.
Reed (Annals of Applied Probability 19, 2009, arXiv:0912.2837) supplied that device. The number in system satisfies a nonlinear convolution equation, (2.8) on p. 9 of the paper, in which the only nonlinearity is the term . Section 3 of the paper isolates that equation as a deterministic regulator map: a map that takes an input path to the unique solution of the equation. Its fluid limit (Theorem 4.1) and diffusion limit (Theorem 5.1) are both obtained by applying this map, through the continuous mapping theorem, to the limits of simpler free processes. The regulator map plays here the role that the one-sided reflection map plays in conventional heavy-traffic theory.
Timeline:
A path is a function . It is càdlàg if it is right continuous everywhere and has a finite left limit at every . is the set of càdlàg paths. For the supremum metric on is .
Let be a cumulative distribution function on , that is, for a probability measure , and let . Write . For an input , the regulator equation (3.1) asks for a path with
The integral runs over the closed interval , so an atom of at counts. The regulator map sends to the solution . The paper applies it with , the service-time distribution: for the fluid-scaled queue and for the diffusion-scaled one.
The proof works with the operator and the successive approximations , of (A.3).
carries the Kolmogorov σ-algebra, the one generated by the evaluations , . In the Lean development the objects are IsCadlag, supNorm, Dpath, SolvesRegulator, psi and picard.
Assume . Then there is a map with the following properties:
The constant is not fixed. The proof gives , but the goal asserts only its existence.
Proposition 3.1 is the deterministic core of the paper. Uniqueness makes the queue length a well-defined function of its free process. Lipschitz continuity in the topology of uniform convergence on compacts carries convergence of the inputs over to convergence of the outputs. Measurability is needed because the inputs are random: it makes the output a random element of , so that the continuous mapping theorem applies. Without the proposition neither Theorem 4.1 nor Theorem 5.1 can be stated in the form the paper gives. Example 1 and Corollary 5.1 are the two explicit solutions the paper extracts from it: a periodic, discontinuous sawtooth, and a constant.
The proposition is proved in the paper's Appendix (pp. 32–36). As far as the platform's records show, none of it has been formalized. The mission produces a machine-checked version with every convention fixed. It also corrects the statement: as printed, the proposition fails when is the unit mass at , because the equation then reads . With and this has no solution. The goal therefore carries the hypothesis . That hypothesis holds for every service distribution of mean on , which is the only case the paper uses. It also covers the mixed cases that fall between the two cases of the printed proof, such as an atom at together with mass elsewhere.
Theorems 4.1 and 5.1 themselves, which are weak convergence in with the Skorohod topology, are not part of this mission.
The equation is a Volterra equation with a nonlinear but -Lipschitz integrand. The first idea is to treat it as a contraction in . That fails: the kernel has total mass , so on the operator is only nonexpansive, not contractive. The contraction has to be recovered locally, from windows of length on which puts mass less than . This works only if such windows exist, and they do not exist when is a point mass at .
Atoms are the second difficulty. With atoms, is càdlàg but not continuous, and the closed-interval convention matters at every step. The third is measurability. The map is not continuous in for the Skorohod topology when has atoms, so the paper splits into its continuous and discrete parts.
ℝ → ℝ, and only its values on are constrained or read. Every equation is asserted for , and every uniqueness claim is equality on (Set.EqOn … (Set.Ici 0)). is the structure Dpath of càdlàg paths.Set.Icc 0 t, so it includes an atom at , and mass on never enters.Infrastructure. A complete development needs the following, all reusable beyond this mission:
The related platform objects are of other shapes:
ChenWhitt93.Reflection.Basic (IsCadlagOn, vector-valued paths on ) and EthierKurtz_HasCadlagPaths (processes indexed by ) define càdlàg paths in other settings.BellmanDP.Inventory.renewal_equation_exists_unique is a linear renewal equation with a density kernel of mass below .Contributions are welcome on any milestone, in any order. The windowed estimates (milestones 2–4) and the measurability step (milestone 5) are independent of each other.
Primal–dual interior-point methods solve a linear program by following, approximately, the central path of strictly feasible primal–dual pairs. Two families dominate the theory. Path-following methods keep the iterates in a neighbourhood of the path and measure progress by the duality gap. Potential-reduction methods measure progress by a merit function, the primal–dual potential of Todd and Ye (Todd–Ye 1990), and choose the step to decrease it.
The potential carries a parameter . The classical analyses (Ye 1991, Freund, Anstreicher–Bosch, Kojima–Mizuno–Yoshise) give iterations with . Practical codes, however, performed better with much larger (McShane–Monma–Shanno, Lustig–Marsten–Shanno). Mizuno, Todd and Ye (Cornell ORIE Technical Report No. 944, 1990, rev. 1991; journal version Math. Oper. Res. 18(4), 1993, doi:10.1287/moor.18.4.964) supply a worst-case justification for a large parameter. With and the step chosen to minimise the potential inside the wide neighbourhood , the method needs iterations. That matches the adaptive-step path-following method in the same neighbourhood (their Theorem 2).
Timeline:
Fix , , , , . The primal problem is subject to , . The dual is subject to , . The strictly feasible set is the set of pairs with , , and for some . The duality measure is .
For put and . For , the wide neighbourhood is
i.e. for all , where and is the all-ones vector.
The potential is
with the natural logarithm. At and for , a search direction solves
and the iterates move along , . The scaled vectors are and , , and .
Algorithm 3. Start from with and . While , compute at , choose with and for every with , and move to .
Let with and
For every and every run of Algorithm 3,
The paper states " iterations". The explicit count is the one its own proof yields, and it is stated so that the goal is not an existential over a constant.
The result shows that a potential-reduction method with of order keeps a polynomial worst-case bound. The earlier analyses cited by the report used of order . It thereby gives a worst-case justification for the large parameters that worked in practice. It also connects the two families: the direction is the path-following direction, and only the step rule changes. Corollary 3 of the paper adds that iterations with a small second-order term decrease the potential far more.
The result is proved in the report. As far as the platform's index shows, no part of it has been machine-checked. The platform already holds the potential function (Bertsimas–Tsitsiklis §9.3) and a proved bookkeeping theorem converting a constant per-iteration decrease into an iteration count (Bertsimas–Tsitsiklis Theorem 9.4). This mission adds the analysis of a concrete algorithm: the admissibility of the step in , the potential decrease (16), and the complexity bound.
The step is defined by minimisation, not by an explicit formula, so its decrease must be bounded by comparison with a step whose effect can be computed. That reference step must be shown to stay in the neighbourhood. This requires controlling the second-order term of the Newton direction in the one-sided norm , together with the centrality of the current iterate. A fixed decrease of order arises only because is of order . Below that scale, the duality-gap term of the potential no longer dominates the loss in centrality from a long step.
A second obstacle is specific to formal work. Algorithm 3's rule ranges over every real whose point lies in the neighbourhood, and a minimiser need not exist. The goal must hold for every run, including the degenerate ones.
Vectors are Fin n → ℝ, with index mapped to Fin n; is Mathlib's sup norm. The general standard-form LP pair is a separate definition, and the neighbourhood and algorithm build on its strict feasibility predicate. is the published definition LinearOptimization.interiorPointPotential with . It equals (1) at every strictly positive pair, and it is evaluated only at points of . All logarithms are natural, and are real powers with real . A run is a pair of sequences satisfying the start conditions and, whenever the current gap exceeds , the step relation of Algorithm 3. Iterates after termination are unconstrained.
Conventions and repairs:
A formalization in which no run can exist for any instance, or in which or the iteration count absorbs an instance-dependent constant, would trivialize the goal. The step relation above is satisfiable for whenever the potential attains its minimum along the line, and the count is the explicit expression above.
Needed infrastructure: the algebra of system (2), namely , the identity , and . Also needed are the bounds and on when , and the arithmetic–geometric mean inequality for . These facts are shared with the sibling missions on the predictor–corrector and wide-neighbourhood algorithms of the same paper, and lemmas proved here are welcome there. The proved Bertsimas–Tsitsiklis theorem LinearOptimization.interior_point_potential_reduction is included as a reference item for the final counting step. Its hypotheses quantify over all iterations and need explicit dual iterates, so it does not apply verbatim.
Many linear programs that arise in combinatorial optimization ask only whether a convex set contains a point satisfying a family of nonnegative linear constraints. In the fractional covering problem the constraints have the form with : the fractional relaxation of set cover, the Held–Karp lower bound for the travelling salesman problem, and the cutting-stock relaxation all have this shape. General-purpose LP methods solve such problems exactly but slowly. Plotkin, Shmoys and Tardos showed that when a fast subroutine can optimize a linear function over the convex set, a Lagrangean-relaxation scheme with an exponential potential finds an approximate solution with a number of subroutine calls that depends on a width parameter and on the accuracy, not on the dimension of the set (Plotkin, Shmoys, Tardos, Cornell ORIE TR 999, 1992; journal version Math. Oper. Res. 20(2), 1995).
The covering half of that paper (§3) is the object of this mission. It is the template for later covering and mixed packing–covering solvers, including those of Garg and Könemann (SIAM J. Comput. 2007) and Young (FOCS 2001).
Fix integers , . Let be a real matrix with nonnegative entries and rows , write , let with , and let be a nonempty convex set contained in the nonnegative orthant.
The Lean names match: rowVal, lam, WidthBound, IsMaxOracle, C1, C2, dualY, potential, improveCover, initCover, coverAlgorithm, in the namespace FracPackCover.Covering.
For every instance as above, every width bound , every exact maximization oracle and every , the covering algorithm stops after at most
calls to subroutine (7), and either returns with , or reports that no has , correctly. This is the paper's with the constants of its proof.
In the order the proof uses them:
Theorem 3.7 says that approximate fractional covering is no harder, in subroutine calls, than about linear optimizations over , plus lower-order terms in . In §6 of the paper this yields fast approximation algorithms for covering-type relaxations such as the Held–Karp bound and the bin-packing and cutting-stock relaxations, where is a product of simple sets and the subroutine is a minimum-spanning-tree or knapsack computation. The result also certifies infeasibility: when the algorithm reports that no exact solution exists, the dual vector at hand proves it.
The result has been proved since 1991 and has been reproved in several later frameworks. As far as is known, it has not been machine-checked. A formal development contributes the explicit constants and a precise statement of the driver, which the paper gives only in prose. It also provides a reusable Lean account of exponential-potential methods with an optimization oracle.
The obvious argument tracks the potential and stops when it is small. This does not work directly, because is tied to , and the guarantee depends on staying close to throughout. Lemma 3.4 controls that, and it is a statement about the reachable states of a while loop, not about an arbitrary point. Two further points are delicate. Unlike packing, condition is not scaled by , so and give -optimality only when is near ; the first phase must first raise from by repeated doubling. And the cost of -scaling is bounded only because each phase starts from a -optimal point, which requires carrying Lemma 3.1 across phase boundaries. The bookkeeping that turns per-call bounds into a single explicit , over a fuel-bounded run, is substantial.
Rows are Fin m with [NeZero m], coordinates Fin n; is a Matrix (Fin m) (Fin n) ℝ; is a Set (Fin n → ℝ), convex, nonempty and in the nonnegative orthant. is a Finset.inf' over the rows. Conventions committed to:
some (result, oracle calls) when they stop within the fuel. Each while-test that reaches the check costs one oracle call; the loop body reuses that answer. The goal asserts that the run with fuel stops; it does not assume termination.initCover, firstPhase and scalingPhases with .A trivializing formalization is ruled out: the goal requires the run to return an outcome within the stated number of oracle calls, for every exact oracle and every width bound, and each outcome must be correct.
A complete development needs elementary real analysis (the second-order bound for ), geometric-decay counting arguments, and induction over fuel-bounded loops. The potential-decrease and termination lemmas are reusable for the packing and general missions of the same paper. Proofs of any milestone, and alternative arguments with better constants, are welcome.
Lagrangian duality turns a constrained minimization problem into the maximization of a dual function over multipliers. For convex programs the duality is clean: under mild conditions the dual optimal value equals the primal one, and an optimal multiplier vector exists. Computationally, however, the ordinary Lagrangian has a well-known defect. Knowing an optimal does not tell where the primal optimum is, because the minimizers of over typically include points that are not optimal and not even feasible. A linear program is the extreme case: is then often constant.
The penalty Lagrangian (also called the augmented Lagrangian) of Hestenes, Powell and Rockafellar repairs this defect. R. T. Rockafellar's 1973 paper Math. Programming 5, 354–373 develops its duality theory for convex programs in an arbitrary real vector space. This mission formalizes the "exactness" part of that theory, §3 of the paper: for , minimizing the penalty Lagrangian at an optimal multiplier gives exactly the optimal solutions of the original problem. The paper puts it as "a strong property whose well-known absence for has been a serious impediment to computational approaches based on duality" (p. 362). Together with the smoothness of the dual function (Theorem 3.2, another mission of this series), this property is what justifies the method of multipliers as an algorithm for constrained optimization.
Timeline. Hestenes (1969) and Powell (1969) proposed the multiplier method for equality constraints. Rockafellar (1973, this paper) gave the inequality-constrained penalty Lagrangian below and its convex duality theory. Bertsekas's monograph Constrained Optimization and Lagrange Multiplier Methods (1982) systematized the theory.
Let be a real vector space, a nonempty convex set, and convex functions. The problem is
A point is feasible if it lies in and satisfies the constraints. The optimal value "inf in (P)" is the infimum of over the feasible points, an element of . An optimal solution is a feasible with for every feasible .
For (no sign restriction), and , the penalty Lagrangian is
The ordinary Lagrangian is for , and otherwise. The dual objectives are and . Problem maximizes over .
In Lean these are Lr, L0, gr, g0, primalValue, dualValue, IsNormal, IsDualOptimal, IsKTVector, IsSaddle, IsOptimal and KuhnTuckerConditions, in the namespace PenaltyLag.Exact.
Assume (P) is normal, is a dual optimal solution, and . Then for every
The result. Theorem 3.5 turns a constrained problem into an unconstrained one with no loss of exactness. Once an optimal multiplier is known, every minimizer of over solves (P), and conversely. Section 4 of the paper builds the computational scheme on this: maximize the smooth concave function over , then minimize over . For the ordinary Lagrangian the corresponding statement is false (p. 363), so the theorem marks precisely what the quadratic penalty term adds. Corollary 3.4 records the other half of the picture: in Kuhn–Tucker vectors and saddle points, behaves exactly like .
Formalizing it. All results are proved in the paper, partly by citation of Rockafellar's Convex Analysis (§§28–30, 36). On the Prove2Me platform, saddle-point characterizations exist only for the ordinary Lagrangian on (for instance ConvexOptimization.lagrangian_saddle_iff_strong_duality, and Beck's Theorem 2.7 as FirstOrderOpt.ConvexTheory.saddle_point_sufficient / saddle_point_necessary). This mission adds the penalty Lagrangian, convex sets in an arbitrary real vector space, extended-real dual values, and the exactness theorem itself. None of these statements is known to us to be machine-checked elsewhere.
The "if" direction is the substantive one. A minimizer of is not known to be feasible; feasibility must come from maximality of in the dual. The natural argument for breaks at exactly this point: is affine on the orthant, and minimality in gives no information about . For the link is the differentiability of the dual function with (Theorem 3.2), which is posed in another mission of this series and is not available as a platform result. Every statement involves extended-real dual values on a vector space with no topology, so must be handled at each step.
AddCommGroup E, Module ℝ E), as in the paper; no norm or topology is used.Set E. Each statement assumes the paper's standing hypothesis (p. 358): convex and nonempty, convex on .E → ℝ, and only their values on enter. Constraint indices are Fin m (0-based), with a separate argument.EuclideanSpace ℝ (Fin m).EReal-valued. An infeasible (P) has value , and off .Lr at is not .The solver needs the representation , weak duality, the envelope formula and differentiability of (Theorem 3.2), and a convex-duality fact for normal programs. Those parts are reusable beyond this mission, and proofs of the paper's Theorem 3.2 in this setting are welcome as auxiliary results.
A pseudorandom number generator replaces repeated random sampling with a deterministic update of a small state. Its useful lifetime depends on the length and structure of the resulting orbit. In Marsaglia and Zaman’s 1991 paper, the subtract-with-borrow generators use only digit subtraction and a one-bit borrow while attaining cycles that can be almost as long as the whole set of digit tuples. The mathematical question is exact: which fraction encodes an output sequence, when does an arbitrary seed enter a cycle, and how long is that cycle?
This mission concerns the paper’s first subtract-with-borrow rule, called Method 1 in §4.5. The paper also studies a second rule that reverses the order of the two subtracted digits. Its modulus and period analysis differ. The distinction matters because the same state format supports both rules while their arithmetic claims are different.
Choose an integer base and lags . A state is a row of digits and one borrow bit, , where each is in and . The leftmost digit is the oldest. One update discards it, shifts the remaining digits left, and appends a new digit. Put . If , the appended digit is and the new borrow is zero. If , the appended digit is and the new borrow is one. Write this deterministic map as .
The digits emitted after the seed obey modulo , with updated at each step. The associated modulus is . For , write for the th digit after the point in the base- expansion of , with . The digit stream is read in reverse order when it is matched to an expansion: the latest generated digit in a finite block is the first fractional digit. A state is strictly periodic when it is already on a cycle under ; otherwise it may pass through a transient before reaching one.
Two states have period one: and . These are the trivial seeds. They are exceptions to the order-of-base period formula. A third useful object is the multiplicative order , the least positive for which . Since , the base is coprime to this modulus.
For prime and any nontrivial seed , the goal identifies the minimal state period after the transient:
The assertion includes both that is on a cycle and that its period is exactly the order. It makes no primitive-root assumption. If is a primitive root modulo , the right side specializes to , the full period discussed in §3 of the paper.
The milestones state that the fractional digits of have least period when and are coprime to ; that a primitive root yields digit period ; that the two trivial seeds are precisely the fixed points; and that every seed reaches a cycle after at most updates. They also formalize the reverse-digit relation for every finite generated block and the paper’s Method 1 inequalities that classify nontrivial seeds already on a cycle. These targets use the paper’s own claims in §§4.1, 4.3, and 4.5 rather than an arbitrary decomposition of the goal.
The result converts the orbit-length problem of a digit-and-borrow machine into a multiplicative-order calculation in a finite residue ring. A prime modulus and a primitive base produce a nontrivial cycle of length ; a nonprimitive base still has the exact order-of-base period. The seed classification separates states already on that cycle from states with an initial transient. These statements are what allow a proposed numerical parameter set to be assessed mathematically before the generator is used.
Marsaglia and Zaman proved these results in the cited paper. This mission asks for machine-checked Lean proofs of the statements, starting from an explicit finite-state update. The reusable output includes exact base- digit arithmetic, links between digit periods and multiplicative order, and methods for reasoning about the eventual cycles of finite-state digit generators. The present proposal consists of compiled statements and definitions; the theorem bodies are open proof targets.
Finiteness alone shows that every state eventually repeats, but it gives neither the bound of steps nor the exact cycle length. Likewise, observing that a generated digit block matches a prefix of some fraction does not by itself identify one period for the whole state orbit. The proof must keep track of the borrow bit and the direction in which the digit block is read. It must also show that a nontrivial seed does not collapse to one of the two fixed states. The source’s integer tableaux explain the arithmetic link, but turning their finite strings into a statement uniform over every seed and every block length is the main formalization challenge.
Lean represents digits by Fin b, the borrow by Fin 2, and the row by a function on Fin r. Lean index zero is , so the digit used in the update, , has index . The update branches on an ordinary integer comparison before any natural-number subtraction can truncate a negative value. The modulus is a natural number, and with makes an exact subtraction. The th fractional digit is computed by an exact quotient and remainder; only has the mathematical meaning used in the theorems. The generated stream is one-based, and the first digit beyond the seed is .
The paper’s “after a few iterations” is pinned to its stated upper bound “at most .” Its “period” is the minimal positive state period of , not a mere period divisor or the period of an arbitrarily selected digit window. “Appropriately chosen” parameters mean a prime for the goal and exclusion of the two named fixed seeds. The reverse-digit milestone permits the numerator to depend on the finite endpoint, as the tableau argument does. No seed is excluded from the at-most- milestone.
The discussion on pp. 473–474 prints the Method 1 seed inequalities in the opposite direction from the Method 1 listing on p. 472. The Lean seed-classification milestone uses the p. 472 directions, which agree with the step map on p. 466 and with direct finite checks. The §5 claim that every five-tuple except the patterns appears once in the special full cycle is left for a later extension. The other subtraction order, its modulus , and the paper’s large parameter certificates are outside this mission.
An encoding that merely asserts the existence of some period, allows an impossible seed hypothesis, or replaces the update by a different subtraction order would make the goal vacuous or change the result. The intended development needs Mathlib’s ZMod, multiplicative order, finite iterations, periodic points, and natural-number quotient and remainder. Contributions proving the numbered milestones, strengthening their arithmetic interfaces, or closing the goal are in scope.
Many algorithms for graphs and finite metric spaces begin by placing the points in a geometric space and then working with the geometry. Euclidean space is the most convenient target: distances there are controlled by inner products, so the question "where should the points go?" becomes a question about matrices. Linial, London and Rabinovich (Combinatorica 15 (1995)) made this viewpoint systematic and drew algorithmic consequences from it, among them the approximate multicommodity max-flow/min-cut theorem treated in a companion mission.
A finite metric space rarely embeds in Euclidean space without changing some distances. The natural measure of the damage is the distortion, and the least distortion of a space is a basic invariant in metric geometry and in the analysis of approximation algorithms. Section 3.1 of the paper (pp. 221–225) shows that is the value of a semidefinite program, so that it can be approximated in polynomial time, and Corollary 3.5 turns the dual of that program into a complete list of certificates that bound from below.
Timeline. The isometric case () is classical: Schoenberg (1935) and Young–Householder (1938) characterised the finite metric spaces that embed isometrically in Euclidean space by positive semidefiniteness of an associated matrix; the paper cites this as its Remark 3.7. Bourgain (1985) proved that every -point metric space embeds in Euclidean space with distortion . Linial, London and Rabinovich (1995) gave the semidefinite characterisation of for every (Corollary 3.5) and showed that the bound is tight for constant-degree expanders.
Let be a finite set of points and a semi-metric: , , is symmetric and satisfies the triangle inequality. Distinct points may be at distance zero, as the paper allows. Write .
For , the space embeds in a Euclidean space with distortion at most if there are and with
where is the Euclidean norm (Definition 2.1, p. 218). The Lean predicate is EmbedsEuclidean d c.
is the cone of real symmetric positive semidefinite matrices indexed by . For a matrix , the condition says that every row of sums to zero. The trace pairing of two matrices is .
For a finite semi-metric space and , embeds in a Euclidean space with distortion at most if and only if for every with
The sums run over ordered pairs. The statement is exact: distortion at most is attained, not approached.
The result. Corollary 3.5 makes the least Euclidean distortion a dual object: every positive semidefinite with zero row sums is a certificate that , and the corollary says that the best such certificate is exact. Lower bounds on distortion in later work, for expanders, hypercubes and other families, are proved by exhibiting such a , often a graph Laplacian. The same duality is the basis of the semidefinite relaxations used for sparsest cut and related problems.
Formalizing it. The result is proved in the literature, but nothing of it is machine-checked. A formal development produces three reusable pieces: the Gram-matrix description of Euclidean point configurations up to distortion, self-duality of the positive semidefinite cone under the trace pairing (not in Mathlib), and a theorem of alternatives for a specific semidefinite feasibility problem, where no constraint qualification can be assumed for free.
The direction from an embedding to the inequalities is short. The difficulty is the converse. "By convex programming duality" is not automatic for semidefinite systems: theorems of alternatives for cone programs can fail when the image of the cone under the relevant linear map is not closed, so the step that turns "no feasible " into an explicit certificate needs an argument specific to this system. A second subtlety is that the left side asks for an embedding with distortion exactly at most ; a separation argument that only produces embeddings with distortion for every does not prove the statement.
X (Fintype, DecidableEq); is not otherwise used. The semi-metric is a function d : X → X → ℝ with the axioms bundled in IsPseudometric.EuclideanSpace ℝ (Fin m) with m existentially quantified. Distortion is the contractive form of Definition 2.1 with both inequalities; with only one of them the zero map or a large scaling would make every space embed, so that reading is ruled out.Matrix.PosSemidef (symmetric by definition); is Q.mulVec (fun _ => 1) = 0. Both hypotheses on are needed: without zero row sums the all-ones matrix, and without semidefiniteness , would violate the inequality for every space with two points at positive distance.Proofs of any milestone, alternative proofs of the goal, and reusable lemmas on the positive semidefinite cone are welcome.
A retailer who restocks a product every period must choose an order-up-to level without knowing the demand distribution, and in most retail settings it observes only sales, the minimum of demand and stock. Demand above the stock is lost and never recorded. This is censored demand: the data needed to estimate the distribution are truncated exactly at the decision. Classical inventory theory assumes the distribution is known, and then the optimal policy in the stationary case is to order up to the newsvendor quantity in every period.
Huh and Rusmevichientong (Math. Oper. Res. 34(1), 2009) give a nonparametric policy that learns from censored sales alone, the Adaptive Inventory Management (AIM) algorithm, and prove that its average expected cost approaches the newsvendor cost at rate . The perishable case reduces to online convex optimization in the sense of Zinkevich (2003) and Flaxman, Kalai and McMahan (2005). The non-perishable case is new: leftover stock constrains the next decision, and the paper controls this constraint through a single-server queue.
Demands are independent and identically distributed with an unknown law of finite mean; denotes a generic demand and its distribution function. A holding cost is paid per unit left over and a penalty per unit of lost demand. The newsvendor cost of a level is
and the newsvendor quantity is .
In period the manager holds units (), raises the stock to , and observes . Excess inventory is either perishable () or non-perishable ().
Assumption 1 gives the manager a bound , and in the non-perishable case a bound with . AIM keeps a target and an implemented level : , and for
with the projection , steps for a scale , and the censored gradient estimate if and if . The manager can compute from the observed sales.
For the waiting times , describe a GI/D/1 queue with inter-arrival times and service time . Its busy periods are the stretches between successive returns to . The auxiliary queue , has shrinking service times.
For every , in the perishable case
and in the non-perishable case, if and , there is a constant , independent of , with
The non-perishable bullet asserts only the existence of , because the paper's explicit formula (9) depends on Proposition 4 (i), which is false as printed.
Theorem 2 shows that a manager who never observes lost sales can still reach the cost of a manager who knows the distribution, at a dimension-free rate, under only a sixth-moment condition in the non-perishable case. The example of §2.5 of the paper shows that the rate cannot be improved in general for AIM. Theorem 6, the coupling of the excess inventory with a queue, is the step that handles decisions constrained by past decisions, and the same paper reuses it when is unknown (§3.2).
The results are proved in the paper, and none of them is formalized as far as is known. This mission formalizes them and also corrects them: Proposition 4 (i) fails for deterministic demand, its explicit constant has to be replaced, and Eq. (2) labels a right derivative as a left one. Lemma 3 for decreasing steps and Lemma 12 are standard tools that are not in Mathlib.
The perishable case is a stochastic subgradient method, but its estimates are conditionally unbiased only given the current iterate, and is merely convex, not differentiable, so the textbook smooth argument does not apply directly. In the non-perishable case the implemented levels are not the gradient iterates, and is not small along a path: carried-over stock can keep above the target for many periods. A bound on for each does not follow from a bound on one period. The queue dominates the whole excess process, but it is non-stationary. Its sum has to be compared with the stationary queue , whose busy period covering a fixed time is length-biased, so second moments of busy periods enter.
All declarations are in the namespace AIMInventory.Known. The demand law and the i.i.d. path measure are the published CappedBaseStock.DemandLaw and demandPathLaw, whose law has finite and strictly positive mean. and are the published backorderCost and newsvendorLevel of LostSalesOrderUpTo.Asymptotic.Backorder. The optimality of is the already posed LostSalesOrderUpTo.Asymptotic.newsvendor_optimal and is included as a reference.
Conventions:
d (t - 1)), and all paper indices are kept.ℕ∞-valued. Every expectation that can be infinite is a lower Lebesgue integral in . The expectations in Theorem 2 have bounded integrands.The mission does not accept a formalization that sums over arbitrary sequences with instead of the AIM run, uses an uncensored gradient, or lets a non-integrable expectation default to .
Contributions toward a stochastic subgradient method with anytime steps, moment bounds for i.i.d. sums, and busy periods of Lindley's recursion are reusable beyond this mission.
A retailer who stocks a perishable or storable product each period must choose an order-up-to level without knowing the demand distribution. Worse, demand is censored: when the shelf empties, the retailer observes sales, not demand. Huh and Rusmevichientong (Math. Oper. Res. 34(1), 2009) proposed the Adaptive Inventory Management (AIM) algorithm, a projected stochastic subgradient method that uses only the censored observation "was there stock left at the end of the period?". They proved that its average expected cost converges to the cost of the optimal newsvendor level at rate , with no parametric assumption on demand.
In the non-perishable case, where leftover stock carries over, the main convergence theorem (Theorem 2, p. 7) requires the step-size scale to satisfy , where is a known lower bound on mean demand. Section 3.2 of the paper removes this requirement. Its Theorem 8 bounds the excess cost of AIM for every step scale , at the price of a hitting time and a busy period in the bound. This mission formalizes Theorem 8 and the steps of its proof.
Demands are independent, nonnegative, identically distributed, with finite positive mean and otherwise unknown law. The holding cost is per unit left over and the penalty is per unit of unmet demand. The newsvendor cost of stocking up to is
and the newsvendor quantity is . The manager knows an upper bound .
AIM, non-perishable case. Fix and a starting target . Put , . In period the step is , the observed slope is if and otherwise, and
The target follows the gradient step. The implemented level can exceed it because stock that has already been bought cannot be returned. The excess-cost term is
Auxiliary processes. Let . For a real :
For , the proof uses and .
For every and every with ,
The statement makes no moment assumption on demand. It is stated with the paper's explicit constants, and both expectations on the right may be infinite.
The result. The cost of AIM relative to the newsvendor benchmark splits as . Stochastic subgradient descent controls for every , so Theorem 8 is the remaining step in showing that AIM converges at rate without any knowledge of a lower bound on mean demand. The first term of the bound is whenever is finite, and Lemma 9 gives that under a finite fourth moment. The second term is whenever is finite, and the paper's Proposition 4 gives that under a finite sixth moment. The result therefore removes the one piece of prior information about demand, other than , that the non-perishable analysis needed.
Formalizing it. The paper's proof is complete and short, but it moves between expectations of random indices, pathwise couplings and renewal arguments, and the statements of Theorem 8 and Lemma 9 contain the slips recorded below. None of these results has a machine-checked proof. The mission produces a checked AIM recursion, a pathwise domination of excess inventory by a queue, and hitting-time and busy-period bounds for random walks with nonnegative i.i.d. decrements.
The argument behind Theorem 2 dominates by a queue whose inflow is below the mean demand. For large the inflow exceeds in early periods, so the queue is unstable at first and its busy periods are not controlled by a stationary queue. A direct bound on through busy periods of fails, because may never empty when . The proof therefore separates a random initial stretch, which ends at the first time after that empties, from the remainder. The two parts are bounded by different processes. The random index sits inside the sums, so the expectations have to be handled with that dependence.
CappedBaseStock_Model (DemandLaw, the i.i.d. path measure demandPathLaw). Its law has finite and strictly positive mean. The cost and are the published backorderCost and newsvendorLevel of LostSalesOrderUpTo.Asymptotic.Backorder. Both are reused, not redefined.d (t-1). AIM is a deterministic recursion on the path, and depend on only. Levels are real numbers, and is evaluated at nonnegative levels.A lattice is the set of integer combinations of linearly independent vectors in . Many computational problems — factoring polynomials over , simultaneous diophantine approximation, integer programming in fixed dimension, breaking knapsack cryptosystems, and the analysis of lattice-based cryptography — reduce to finding a good basis of a given lattice: one whose vectors are short and nearly orthogonal. In 1982 A. K. Lenstra, H. W. Lenstra, Jr. and L. Lovász gave a polynomial-time algorithm that turns any basis into a reduced one, now called the LLL algorithm (Math. Ann. 261, 1982). It was the key step of their polynomial-time factoring algorithm for , and it has since become a standard tool of computational number theory, combinatorial optimization and cryptanalysis.
This mission formalizes the algorithm itself, as described in (1.15) of the paper, and the paper's proof (1.23) that it terminates and returns a reduced basis of the input lattice. A companion mission of the same series treats the properties of reduced bases ((1.6)–(1.12)); a third treats the factoring application (Sect. 2).
Let be linearly independent and ; the form a basis for . The Gram–Schmidt vectors and coefficients are defined by
The basis is reduced if for and for .
The algorithm keeps a current basis and a subscript , starting at . While it performs one step:
The algorithm stops when . Before and after every step the situation (1.16)–(1.17) holds: the first vectors satisfy both conditions of reducedness among themselves.
The termination proof uses the Gram determinants (), the potential , and the minimum .
For every basis of ():
every reachable state with admits a step, and every reachable state has a reduced basis for .
For with , : the number of case-1 steps satisfies ; the identities (1.27)–(1.29) making the common denominators; and throughout.
The termination theorem is what makes reduced bases computable: the bounds of (1.6)–(1.12) on reduced bases are useful only because the algorithm produces such a basis from any input, and the factoring algorithm of Sect. 3 calls it as a subroutine. The explicit count is the step bound behind the paper's operation count (1.26).
On the formal side, Mathlib has Gram–Schmidt orthogonalization and Minkowski's convex body theorem, but no lattice basis reduction. A verified LLL implementation exists in Isabelle/HOL (the Archive of Formal Proofs entry A verified LLL algorithm, 2018), with its own algorithm description and representation. No Lean 4 formalization of the paper's algorithm or its termination proof exists, as far as could be determined. The result is proved; what is open here is its formalization.
The naive termination argument — "each case-1 step makes a vector shorter" — fails: case 1 can lengthen , and moves back and forth. The paper's argument needs a potential that decreases by a fixed factor in case 1 and is invariant in case 2, the identity to see that only moves, and a lower bound on depending only on . That lower bound rests on the Hermite-type estimate that a lattice of rank with Gram determinant has a nonzero vector with , which is not in Mathlib and must be derived from the geometry of numbers for sublattices of lower rank. The invariant (1.16)–(1.17) requires tracking how the Gram–Schmidt data of the first vectors change under a swap and under the size reductions of case 2.
is EuclideanSpace ℝ (Fin n), with Lean indices for the paper's ; is Mathlib's unnormalised InnerProductSpace.gramSchmidt, and is (1.3) verbatim. A state is a pair with stored as the paper's subscript; and are recomputed from , so the update formulae (1.22) are consequences, not definitions. One step is a relation: "the integer nearest to " is any integer with , so every tie rule is covered. The loop of case 2 picks the largest bad index , as on the page, and runs until (1.21) holds. The relation follows the text of (1.15), not Fig. 1 (which never visits and stops at ). The standing hypotheses are and linear independence of the input basis.
A trivializing formalization is excluded: termination alone would hold for a relation that never fires, so the goal also asserts that a step exists at every reachable state with , and a sorry-free sanity file exhibits both cases firing for . The goal does not mention , or , which appear only in milestones.
Not formalized: the operation count and binary-length bound of (1.26), which need a cost model; the bounds (1.30)–(1.34) on intermediate states and the bounds "throughout the course of the algorithm" on p. 524, which concern states inside a step; and Remark (1.37). Contributions welcome: a reusable Hermite-constant bound , Gram determinant identities, and invariance of Gram determinants under unimodular changes.
A multicommodity flow problem asks to route several commodities simultaneously through a capacitated network, each from its own source to its own sink. For a single commodity, the max-flow min-cut theorem of Ford and Fulkerson says that the largest routable flow equals the capacity of the smallest separating cut. For many commodities the natural analogue fails: the max-flow can be strictly smaller than the min-cut, already for four commodities (Okamura and Seymour, 1981). Leighton and Rao asked how large the gap can be, and showed that for uniform demands it is at most logarithmic in the number of nodes. The result turned the min-cut, an NP-hard quantity, into something approximable by a linear program, and became the basis of the first polylogarithmic approximation algorithms for sparsest cut, balanced cut, minimum feedback arc set, crossing number and VLSI layout (Leighton–Rao, J. ACM 1999).
Timeline:
A network is a finite set of nodes with a capacity for every pair; the pair is an edge when . For with complement , the cut capacity is the total capacity of the edges joining to . As in the paper, the network is assumed connected: for every nonempty proper .
In the uniform multicommodity flow problem (UMFP) every unordered pair of nodes is a commodity with demand one. A routing of value sends units between every pair simultaneously, so that the total flow of all commodities over each edge, in both directions together, is at most its capacity. The max-flow is the largest such (the concurrent max-flow).
The min-cut (sparsest cut) of the UMFP is
the minimum over cuts of the cut capacity divided by the demand separated by the cut. The quantity is the ratio cost of the cut.
The milestones use the dual objects. A distance function assigns a nonnegative length to each edge; is then the shortest-path distance, , and the total weight is . The distance constraint (5) is , summed over unordered pairs. A set of nodes has radius at most if some centre reaches all its nodes by walks inside the set of length at most . Throughout, .
for every uniform multicommodity flow problem: there is one absolute constant such that for every connected network with nodes. The goal fixes no constant, so it is the form any improved argument would still prove.
and : Theorem 2 with the constant its proof produces.
The theorem says that the LP relaxation of uniform sparsest cut has integrality gap , and the expander example of §2.1 (Theorem 1) shows this is tight. Combined with the cut-finding argument, it gives an -approximation for sparsest cut and, through the paper's Section 3, approximation algorithms for balanced separators, minimum cut linear arrangement, crossing number, VLSI layout area, feedback arc set and the emulation of networks. Region-growing decompositions of the kind in Lemma 3 reappear in low-diameter decompositions, multicut (Garg–Vazirani–Yannakakis), and metric embedding.
The result is proved; no machine-checked proof of it is known. A formalization would provide: concurrent multicommodity flow and its LP dual on finite graphs, the uniform sparsest cut, a verified region-growing decomposition, and the max-flow min-cut gap theorem itself. The LP-duality milestone, which the paper cites rather than proves, is a reusable piece of flow theory in its own right.
The upper bound is a counting argument. The lower bound is the content. The natural idea, rounding an optimal dual distance function by a threshold and cutting the long edges, does not work: the paper notes (p. 797) that no thresholding rule is known that always yields a good cut, because edges with large distance need not form a sparse cut. Any argument must convert the fractional dual into a single cut while losing only a factor against the total weight , which requires a global property of the distance function rather than the lengths of individual edges. The LP-duality step needs a correct dual for the concurrent flow problem with shortest-path distances, which Mathlib does not provide off the shelf.
V is a Fintype with decidable equality; capacities are a symmetric nonnegative real function vanishing on the diagonal, and the graph is the simple graph of pairs with positive capacity. Goal-level statements assume 2 ≤ Fintype.card V and connectivity in the form for every nonempty proper (the paper's standing assumption, p. 789).Contributions welcome: proofs of any milestone; a general LP-duality theorem for concurrent multicommodity flow, reusable for the product and directed variants; and a general region-growing lemma.
A component may be exposed to shocks that arrive at random times. Its chance of lasting for a given time depends both on how often shocks arrive and on how likely it is to survive successive shocks. Reliability calculations often begin with the latter, discrete sequence, while replacement and life-testing questions concern the resulting lifetime distribution. Esary, Marshall, and Proschan study how a property imposed on the shock sequence appears in the continuous lifetime law. Their Theorem 3.1 gives several such inheritance results; this mission targets its increasing-hazard-rate assertion (Esary, Marshall, and Proschan 1973, Theorem 3.1).
An increasing hazard rate (IHR) means that the remaining life of a component that has survived to age becomes stochastically shorter as increases. This is a concrete way to express wear-out. The paper treats “increasing” as weakly increasing throughout, so a constant hazard rate is included (Esary, Marshall, and Proschan 1973, pp. 628, 631).
Shocks arrive according to a homogeneous Poisson process with rate . Let be the probability that the component survives the first shocks. The sequence starts at and satisfies for the target theorem. The probability of failure on the st shock is . At a nonnegative time , the chance of exactly shock arrivals is . The survival function of the component is therefore the Poisson mixture
and the paper sets for . At positive times its density is . The failure-on-shock sequence and the positive-time density are both part of the mission because the paper compares their shape as well (Esary, Marshall, and Proschan 1973, (2.1)–(2.3)).
A nonnegative sequence is PF₂ here when its successive ratios decrease weakly, wherever those ratios are defined. For the survival probabilities this says decreases with . A survival function is IHR when, for each , the survival ratio decreases with age wherever it is defined. These are the discrete and continuous conditions connected by the target (Esary, Marshall, and Proschan 1973, Definition 2.3 and p. 631).
The goal is Theorem 3.1(3.2):
It covers any nonnegative, weakly decreasing shock-survival sequence with and a positive Poisson rate. It does not fix a finite number of shocks or a special survival law (Esary, Marshall, and Proschan 1973, p. 632).
The milestone list includes the positive-time density formula (2.3), the upper bound in (2.5), the derivative estimate from the proof of (3.1), and that proof's sign-change claim for . It culminates in Theorem 3.1(3.1), which says that PF₂ failure-on-shock probabilities give a PF₂ positive-time density. These are statements made explicitly by the authors and form the neighboring shape result and the estimates cited in the proof of the IHR goal (Esary, Marshall, and Proschan 1973, pp. 628–629, 632–633).
The mission also poses, outside the milestone list, the other inheritance results of the same section and of §6 whose formulation uses the same objects:
where is the condition of Murthy and Lientz, strictly weaker than PF₂. Theorem 6.1 specializes to independent shock magnitudes, (exponential, IHR or DHR as is constant, decreasing or increasing in ), and Theorem 6.2 shows that a random threshold, , always gives a logarithmically convex density on (Esary, Marshall, and Proschan 1973, pp. 632, 634, 647).
The target makes a discrete reliability assumption useful for continuous-time decisions. One may model or estimate the sequence from how the component responds to successive shocks and then infer an ageing property of its lifetime under Poisson arrivals. The conclusion is about residual lifetime at every age, not just its mean or one tail probability. The companion PF₂-density statement shows that the same transfer applies to failure-on-shock probabilities and the resulting continuous density (Esary, Marshall, and Proschan 1973, Theorem 3.1).
The 1973 results are proved in the paper. In this mission the Lean statements compile as open theorems; their mathematical proofs are still to be formalized. A completed development would make the Poisson-series model, its density, and the discrete-to-continuous shape claims reusable in later formalizations of shock and wear models. The other missions in this paper's series consider cumulative damage, first passage under wear, and random thresholds using related ideas.
The survival function mixes infinitely many shock counts. Each count has its own time-dependent Poisson weight, so a decreasing ratio of adjacent terms does not give the desired comparison of survival ratios by a termwise inequality. The paper invokes a variation-diminishing property of a totally positive Poisson kernel for the corresponding shape arguments (Esary, Marshall, and Proschan 1973, p. 633). A formal proof must also justify differentiation and rearrangement of the infinite series, including sequences that reach zero after finitely many shocks.
The Lean model uses real-valued functions for , , and , with the shock count indexed from zero. The Poisson mixture is the definition of ; no random lifetime is introduced in place of it. The value for negative time follows (2.1). IHR is expressed for all real ages by cross-multiplying the survival-ratio comparison. With , this includes the boundary at zero without an atom there. PF₂ sequence and density conditions are also cross-multiplied. This gives the paper's ratio statements wherever denominators are positive and retains the natural zero-survival cases without using real division by zero.
The source treats as probabilities, takes , and restricts variables to avoid zero denominators; Lean states the rate, nonnegativity, weak monotonicity, and the ratio convention explicitly. Formula (2.3) is represented by the derivative identity at positive time. The bound (2.5) is , equivalent to the hazard-rate statement wherever survival is positive. The sign-change milestone excludes a strict positive–negative–positive pattern at increasing positive times, matching the authors' “at most two, in the order negative, positive, negative” wording. These conventions prevent an empty IHR statement or a trivial result caused by totalized division.
A complete proof needs reusable facts about convergence and differentiation of Poisson-weighted series and about preservation of sign patterns under the Poisson kernel. Contributions to that infrastructure, the density and hazard estimates, and the PF₂ transfer are in scope, as are the further results above. For those, the reversed classes are stated on the life-distribution domain: DHR compares ages only, because Theorem 3.2 allows , an atom at the origin; a logarithmically convex density is the reversed cross-multiplied PF₂ inequality for on . Mean residual lives and mean lives are computed in (they are infinite when ), and their ratios are taken only where . In Theorem 6.1 only the numbers enter, and "exponential" includes the rate ; in Theorem 6.2 the shock and threshold laws are probability measures on with no mass on . The paper's further remark that a survival function needs is not imposed: none of the theorems uses it.
Pricing a financial derivative, estimating a risk measure, or computing any expected functional of a stochastic differential equation (SDE) by simulation runs into two errors at once: the statistical error of averaging finitely many sampled paths, and the discretisation bias of replacing the exact SDE solution by a numerical scheme with a positive timestep. With the Euler scheme and independent paths, the mean-square error behaves like , so a root-mean-square accuracy requires paths of steps each: a cost of order .
Giles' Multilevel Monte Carlo path simulation (Operations Research 56(3), 2008) showed that combining simulations on a geometric hierarchy of timesteps reduces this cost to order for the Euler scheme with a Lipschitz payoff, and to , the cost of an unbiased estimator, when the level differences have fast-decaying variance. The two-level case is due to Kebaier (2005), who reduced the cost to order ; Heinrich's multilevel method for parametric integration (2001) is a precursor. The paper's Theorem 3.1 is stated abstractly, in terms of four rate conditions, and has since been applied to SDEs, SPDEs, Markov chains and nested simulation; the survey of Giles (Acta Numerica 2015) traces this development.
Fix an integer refinement factor and a horizon , and let the timestep of level be , . On a probability space, let be the quantity of interest (in the paper, a functional of the solution of an SDE driven by a Brownian path) and its approximation with timestep . Since
the method estimates each term independently. For each level and sample size , is an estimator of () or of () built from samples, with computational complexity . The multilevel estimator is , its total complexity is , and its mean-square error is .
The hypotheses are four rate conditions, with constants and : (i) (weak convergence order ); (ii) equals or (unbiasedness of each level); (iii) (variance decay rate ); (iv) (cost proportional to samples times steps).
There is a constant such that for every there are and with
The constant is uniform in ; its value is not part of the goal.
The milestones are the displayed steps of the paper's proof, in its order: the choice of the finest level and the resulting two-sided bound (6) on ; the bound on the squared bias; the geometric bound (7) on ; and, for each of the three regimes , , , a choice of with a bound on the variance (using the geometric bounds (8) and (9) in the last two) and an explicit cost bound with an explicit constant . In case the bound on the number of levels is a separate milestone.
The theorem turns the multilevel idea into a complexity statement: whenever a discretisation has weak order and its level corrections have variance decay , the cost of accuracy is known up to a constant. It identifies as the parameter governing the method, explains where the effort is spent (coarse levels for , fine levels for ), and is the template that later multilevel analyses (Milstein schemes, multi-index Monte Carlo, randomised MLMC) follow and refine.
The result is proved in the paper and widely reused. To our knowledge it has no machine-checked proof. The mission produces one: a Lean statement of the abstract theorem and of each step of the proof, with the paper's explicit constants. Its probabilistic content is light (linearity of expectation, the bias-variance decomposition, Bienaymé's identity for independent variables); most of the work is careful real analysis with ceilings, logarithms and real powers.
No single step is deep; the difficulty is bookkeeping under exact constants. The obvious argument "choose , choose " is asymptotic. The theorem demands, for every , an exact bound with a constant independent of . This forces the integer ceilings in and to be controlled explicitly (each ceiling adds one sample per level, whose total cost is (7)), the number of levels to be bounded by a multiple of , and the three geometric series to be summed with constants independent of . The strict inequality is not delivered by the paper's own choice in case , where both halves give only ; a solver must adjust the sample sizes.
, and the level estimators are arbitrary real random variables on a probability space ; the SDE and its discretisation enter the theorem only through (i)–(iv), so they are not modelled. This makes the statement more general, not weaker. Expectations are Bochner integrals and is Mathlib's variance. The conventions are:
Real.rpow, is Int.ceil for and Nat.ceil for (whose arguments are positive).A formalization in which the cost is defined as , in which (ii)–(iv) hold only for one fixed sample size, or in which the MSE and cost bounds are proved for different and , is a different and weaker theorem and is ruled out by the statement.
Infrastructure needed: geometric-series bounds with real ratios, floor and ceiling estimates for logarithms, and Bienaymé's identity (Mathlib's IndepFun.variance_sum). The bias-variance decomposition for variables is reusable beyond this mission. Proofs of individual milestones, and alternative proofs of the goal, are welcome.
Retailers selling several related products can change prices as inventory runs down. A sale of one product changes the stock available in later periods, while changing its price also shifts demand toward or away from the other products. Dong, Kouvelis, and Tian study these linked decisions for substitute product variates under a multinomial logit customer choice model. Their 2009 article gives an exact characterization of the optimal dynamic price vector when each in-stock variate can have its own price. The characterization separates a product's inventory opportunity cost from a margin shared across all products, which makes the result more informative than an opaque Bellman maximization.
The mission isolates Theorem 1 of that article. The paper also studies restricted policies that require a unified price or fixed prices for some variates; those results are separate missions in this series. The present target concerns the fully flexible dynamic policy of §3.1, with the model and conventions of §2.
There are product variates, indexed by , with finite quality parameters . Time is the number of periods remaining, so it counts down to zero. The inventory state has nonnegative integer coordinates, and is the set of variates still in stock. At most one customer arrives during a period, with probability satisfying . Inventory is not replenished. The retailer chooses a finite, nonnegative price for each in-stock variate. An out-of-stock variate receives the paper's null price and contributes no demand.
An arriving customer chooses among the in-stock variates and the no-purchase option. The multinomial logit model assigns deterministic utility to variate and utility to no purchase, with positive scale . Its probabilities are
Let be the maximum expected revenue from state with periods remaining and zero terminal value . A sale of variate moves the inventory to . Its marginal inventory value is when . For a continuation value , the one-period objective is current expected sales revenue plus the expected continuation revenue after a sale or no sale. The Bellman value takes its supremum over all finite nonnegative price vectors. Equation (5) rewrites that objective as , where is the probability-weighted marginal revenue.
Theorem 1 asks for a unique common margin satisfying
For every in-stock variate, the price must be feasible and attain the Bellman maximum. The margin also satisfies . These claims hold for every inventory state, including an empty in-stock set. They are the main target of Theorem 1, equations (9)–(10).
For each , let be the unique margin equation root at the same inventory state , with periods remaining. The remaining clause of Theorem 1 states
The milestones track the paper's equation (5) and Steps 1–5 of its Appendix A argument: marginal inventory value, the mapping between prices and choice probabilities, concavity in probability coordinates, existence of the margin, optimal choice probabilities, and the one-period value identity.
The result turns a coupled dynamic program into a precise pricing characterization. It says that differences in optimal prices across products reflect differences in their marginal inventory values; the remaining margin is common. The value identity quantifies the expected revenue earned over the remaining horizon, and the explicit maximizer removes ambiguity about whether the Bellman supremum is attained. These conclusions support the paper's comparisons with restricted pricing policies and its later discussion of how quality and inventory scarcity affect prices Dong, Kouvelis, and Tian (2009).
The result is proved in the article. This mission contributes a Lean statement of the full theorem, its model, and seven named intermediate targets. The draft declarations compile against the pinned Mathlib environment; their proofs remain open. A complete formalization would provide reusable finite MNL choice probabilities, inverse price and probability identities, and a Bellman model for substitute-product inventory. The paper's economic conclusions should be recovered from those formal statements, rather than from a weakened existence claim.
The direct one-period objective in the price vector is not quasiconcave, as the paper notes on p. 323, so a local condition on prices alone does not establish global optimality. The price vector also ranges over an unbounded set, and a supremum could conceal a boundary or attainment issue. Finally, one extra unit of stock changes future probabilities across all products, not just the revenue of that product. These interactions make nonnegative marginal inventory value and the global optimality assertion substantive parts of the result. The probability-space objective is concave on its positive domain, but the printed Appendix A claim of strict concavity on the full domain is stronger than that function permits; uniqueness concerns the normalized choice-probability slice.
Lean represents products by Fin n, inventories by functions Fin n → ℕ, and time by a natural number counting remaining periods. The model assumes and . The set filters positive inventory coordinates; an out-of-stock variate is removed from every choice-probability sum, so its null price need not be encoded as a finite real. The objective's no-sale continuation term is counted once, following equations (5) and (22), despite the ambiguous bracket placement in printed equation (3). In-stock prices are finite and nonnegative. Off-stock coordinates of the displayed candidate vector are set to zero and do not affect demand.
Lean's natural-number subtraction in is used only for , where it subtracts exactly one unit. The Bellman value uses a real sSup, whose default on a badly bounded set could otherwise obscure the theorem. The goal and final milestone therefore require an explicit maximizing price vector and equality between the value and its objective. The margin root is stated as unique and every root is covered; it is not hidden behind a choice operator. Equation (11) quantifies over all roots for at one fixed , not along a sample path. No assumption that or is nonempty is added to the goal. The price–probability mapping and interior optimality milestones assume nonempty where the paper's positive-simplex argument requires it.
A complete development needs finite-sum algebra, real exponential and logarithm facts, concavity on products of real function spaces, and boundedness and attainment facts for the Bellman objective. The MNL probability and inverse-map facts can serve later pricing models; the dynamic value and marginal-stock lemmas serve inventory-control formalizations. Contributions that prove these statements or isolate reusable analytic lemmas are within scope. The statement must retain both the Bellman maximizer and the value identity, so a default sSup value cannot turn the goal into a trivial equality.