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.
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?
Nonlinear conjugate gradient methods minimize a smooth function using only function values, gradients and a handful of vectors of storage. That makes them a standard tool for large-scale unconstrained optimization, where quasi-Newton matrices do not fit in memory. Each method is fixed by a scalar , and the classical choices (Fletcher–Reeves, Polak–Ribière–Polyak, Hestenes–Stiefel) have been analysed by many authors. Their convergence proofs normally require the strong Wolfe line search, and often a bounded level set. Many other unconstrained methods, by contrast, are proved convergent under the weaker standard Wolfe conditions.
In 1999 Y. H. Dai and Y. Yuan (SIAM J. Optim. 10 (1999) 177–182) proposed a new formula,
the numerator of Fletcher–Reeves over the denominator of Hestenes–Stiefel. They proved that the resulting method converges whenever every step satisfies the standard Wolfe conditions, under assumptions on that do not include a bounded level set. The method is now known as the Dai–Yuan method.
Timeline.
Write , , , . The inner product of is and the Euclidean norm. Fix line-search constants .
A step along a direction from is a standard Wolfe step if
and a strong Wolfe step if (1.7) holds together with (1.8).
Algorithm 2.1 starts at with and stops if . At iteration it picks a standard Wolfe step , sets , stops if , and otherwise sets
Assumption 3.1 at requires three things. First, is bounded below on . Second, is continuously differentiable on a neighbourhood of the level set . Third, there is with
In the Lean development these objects are levelSet, Assumption31 f x1 N L, StdWolfe, StrongWolfe, betaDY, IsDYIteration, IsDYRun, IsDYRunStrong, IsDescentWolfeMethod and LiminfGradZero, all in DaiYuanCG.Conv.Setting.
Under Assumption 3.1 at , a run of Algorithm 2.1 either terminates at a stationary point or satisfies
The goal is the non-terminating branch: for every implies (3.7).
A companion item, not a milestone, states §4's observation (p. 181): under strong Wolfe steps, and .
The result. Theorem 3.3 answers the question posed in §1 of the paper, whether some conjugate gradient method converges under the standard Wolfe conditions, and it does so without a bounded level set. Weakening the line search matters in practice: a standard Wolfe step is easier to find than a strong one, and the convergence theory now matches what quasi-Newton codes already had. The descent property (3.9) holds at every iteration without any restriction on other than .
Formalizing it. The theorem has a complete published proof; nothing here is open. To our knowledge neither the theorem nor the Zoutendijk condition under these hypotheses has a machine-checked proof. The mission produces three things: a formal Wolfe line-search vocabulary over EuclideanSpace; a Zoutendijk lemma whose assumptions are local to a neighbourhood of the level set, so other descent methods can reuse it; and the Dai–Yuan convergence proof itself.
The algebra of (2.5)–(3.17) is short. The analytic difficulty is in Lemma 3.2. The Lipschitz bound (3.1) applies only on , so it cannot be applied to an arbitrary step until the iterates are known to lie there. The finite decrease at each step must also control an infinite series, which is why the global lower bound on matters. A global Lipschitz constant or a bounded level set would simplify this issue. Both are assumptions the paper does not make, and §4 points out that avoiding the bounded level set is part of the result.
A second point is that is only well defined because (1.10) gives once is a descent direction. Descent of in turn depends on the value of through (2.5), so these properties depend on each other across iterations.
EuclideanSpace ℝ (Fin n) and is Mathlib's gradient f x. All sequences are maps ℕ → _ indexed from ; index is unconstrained and never used.Summable or ¬ Summable of the terms shifted to start at .Policy gradient methods search directly over parameterized policies of a Markov decision process (MDP) by gradient ascent on the expected discounted reward. They are among the most widely used methods in reinforcement learning, yet the value is a nonconcave function of the parameters, and until recently little was known about whether, or how fast, such methods reach a globally optimal policy. Agarwal, Kakade, Lee and Mahajan (arXiv:1908.00261v5, JMLR 22(98), 2021) give a systematic answer for tabular and function-approximation settings.
This mission formalizes one of their central results. Under the softmax parameterization, plain gradient ascent converges to optimal values only asymptotically (their Theorem 5.1, rate unknown): parameters can diverge and policies become nearly deterministic early, which stalls progress. Adding a log barrier regularizer, equivalent to a relative-entropy penalty towards the uniform policy, keeps action probabilities away from zero, and the paper shows that this yields an iteration count polynomial in every problem quantity. The result is the "softmax + log barrier" row of the paper's Table 1 and a reference point for later analyses of entropy-regularized policy gradient (for example Mei et al., 2020; Cen et al., 2021).
A finite MDP consists of finite sets (states) and (actions, nonempty), a transition kernel , rewards and a discount factor . A policy assigns a probability distribution over actions to every state. Its value is , and for a distribution over states . The action value is and the advantage is . An optimal policy maximizes at every state simultaneously; .
The discounted state visitation distribution is . Given a start distribution used by the algorithm, the distribution mismatch coefficient is .
The softmax policy with parameter is . For the log barrier regularized objective is
and gradient ascent with step size is . Write .
Let for all (for example the mismatch coefficient), , , and . Starting from a parameter whose softmax policy is uniform (e.g. ),
The corollary shows that a first-order method on a nonconcave objective reaches an -optimal policy in a number of steps polynomial in , , , and the mismatch coefficient, with no dependence on the MDP's structure beyond these quantities. Theorem 5.2 is of independent use: it certifies any approximately stationary point of the regularized objective, however it was found, as approximately optimal for the original problem. The dependence on makes precise why the exploratory start distribution matters.
The results are proved in the paper; none of them is machine-checked. A formal development adds a checked softmax policy gradient formula on an infinite-horizon discounted MDP, a checked smoothness bound for the regularized objective, the nonconvex gradient-method rate in Euclidean space, and a corrected statement of the corollary (see the next sections). Lemma 3.2 and Lemma C.1 are reused across the other missions of this series.
The value function is not concave in and its gradient vanishes where policies become deterministic, so the standard route "small gradient implies near-optimal" fails for the unregularized objective. With the regularizer, the link between stationarity and optimality has to hold with explicit constants that do not degrade as policies approach the boundary of the simplex, which is where the unregularized argument breaks down. The second obstacle is smoothness: is an infinite discounted sum of products of transition probabilities, and its Hessian must be bounded uniformly in by , which in Lean means differentiating a tsum of matrix-power–like terms in . The policy gradient formula itself requires the same interchange of differentiation and infinite summation.
States and actions are finite types; is nonempty. Parameters live in EuclideanSpace ℝ (S × A), so is the norm and is Mathlib's gradient. The MDP layer (transition kernel, policy, occupation probabilities, , , optimal policy) is the published FoundationsML.ReinforcementLearning library, and , , are defined on top of it. Standing assumptions are those of §3: a kernel, , , probability distributions, optimal at every state.
Conventions committed to:
Two corrections of the printed corollary. The printed statement allows "any initial ", but its proof uses , valid for a uniform initial policy and false in general; the formal goal assumes a uniform start. The printed contradicts the proof, which takes from Lemma D.4, ; the formal goal uses the latter, with the same iteration count.
The goal is not trivialized by its encoding: the hypotheses fix the run completely from , and , they are jointly satisfiable (a sorry-free check exhibits a one-state, two-action MDP with an optimal policy and ), and the conclusion concerns the unregularized value of the iterates. Theorem 5.2, Lemma D.4 and Theorem E.1 are milestones, not hypotheses of the goal.
Infrastructure that a complete development needs, and that is reusable beyond this mission: differentiability of discounted values in the policy parameters and the policy gradient theorem for the softmax class; Hessian bounds for softmax; the descent lemma and the rate of gradient methods for smooth nonconvex functions on Euclidean space. Contributions to any of these, or proofs of single milestones, are welcome.
A seller with distinct items faces consumers, each of whom wants at most one item. Choosing item prices to maximise revenue in this setting is the unit-demand envy-free pricing problem, introduced by Rusmevichientong and studied in algorithmic game theory and revenue management since the mid-2000s. Optimal prices are hard to compute in general, so the guarantees of simple pricing rules matter. The simplest such rule is uniform pricing: put one price on every item and choose to maximise revenue.
Aggarwal, Feder, Motwani and Zhu (ICALP 2004) and Guruswami, Hartline, Karlin, Kempe, Kenyon and McSherry (SODA 2005) analysed uniform pricing; in the min-buying model it recovers a fraction of the optimum, a bound Berbeglia and Joret attribute to Aggarwal et al. Berbeglia and Joret (arXiv:1606.01371, Algorithmica 2020) observed that the min-buying problem is a special case of assortment optimisation under a regular discrete choice model, and that uniform pricing then coincides with the revenue-ordered assortments heuristic. Their general guarantee for that heuristic yields a second bound for uniform pricing, in terms of the spread of the valuations rather than the number of consumers. This mission formalizes that bound (Corollary 4.7) together with the reduction it rests on (Theorem 4.6).
Unit-demand min-pricing (). There are items and consumers , . Consumer is interested in a set and has a valuation . Given a price assignment , consumer buys a cheapest item of if its price is at most , and nothing otherwise. The seller's revenue is
the optimum is , and uniform pricing earns . Write and for the extreme valuations.
Regular choice models. A finite product set carries choice probabilities for , , with no-purchase probability . The model is regular if (i) all probabilities are nonnegative, (ii) for , (iii) , and (iv) for and every . With revenues , an assortment earns and . If are the distinct revenues and , revenue-ordered assortments earn .
The reduction. From a instance the paper builds , , and , where spreads probability one over the set of pairs with , and minimal among the pairs of whose item lies in .
The bound is the paper's "approximates the optimum revenue to within a factor of , ", stated in product form.
The corollary gives a uniform-pricing guarantee that is independent of the number of consumers and items: when valuations lie within a factor of each other, a single price recovers a fraction of the optimum, which improves on whenever . More broadly, Theorem 4.6 places inside the class of regular choice models, so every guarantee proved for revenue-ordered assortments under regularity transfers to uniform pricing.
All results here are proved in the paper. Nothing in this mission is formalized elsewhere as far as a search of the platform shows: there is no regular choice model, no problem and no revenue-ordered guarantee on Prove2Me. The mission produces the reduction as reusable infrastructure, a machine-checked version of the paper's Lemma 4.5 (whose appendix proof is an informal repair argument), and the first formal guarantee for uniform pricing.
The reduction is where the work sits. Regularity hinges on the no-purchase case of axiom (iv): enlarging an assortment can only make nonempty, never empty, and this must be checked for the specific sets whose definition depends on the whole of . The revenue identities require tracking the minimum over of a price function obtained from an assortment, including items absent from , which receive the paper's "" price. Lemma 4.5 is needed to make the optimum of the uncountable pricing problem coincide with that of a finite assortment problem, and the statement is about a supremum over a continuum of price vectors whose attainment is not obvious. Theorem 3.2 has to relate the optimum to threshold sets of an arbitrary regular model, where products may share revenues and the optimal assortment need not be a threshold set.
The naive route of comparing uniform pricing to the optimum directly, consumer by consumer, does not give a bound in terms of ; the reduction to a regular model is what supplies it.
X and M, with Nonempty M (). Valuations satisfy as a field of the instance; the paper says "non-negative", but its reduction () and its ratio need positivity.Finset C; RO is a maximum over the threshold sets only. Distinct revenues are sorted 0-based (Fin k), with handled as a separate case.Real.log applied to ratios .A retailer with a large catalogue but a limited display (a web page, a shelf, a search result) must decide which assortment of products to show each arriving customer. Customers choose among the displayed products or leave without buying, and the retailer does not know their preferences in advance; it learns them only from the purchases it observes. This is the MNL-Bandit problem of Agrawal, Avadhanula, Goyal and Zeevi (arXiv:1706.03880v2; Operations Research 67(5), 2019), in which customer choices follow the multinomial logit model, the workhorse of revenue management and marketing.
The same paper gives an epoch-based upper-confidence-bound policy whose regret is at most of order (its Theorem 1). This mission formalizes the matching lower bound, the paper's Theorem 2: under a constraint that at most products be displayed, no policy can have regret smaller than order on every instance. Lower bounds of this kind are what certify that an algorithm is near-optimal rather than merely good.
Timeline. The square-root lower bound for -armed bandits goes back to Auer, Cesa-Bianchi, Freund and Schapire (2002), presented in the survey of Bubeck and Cesa-Bianchi (arXiv:1204.5721, 2012). Rusmevichientong, Shen and Shmoys (2010) and Sauré and Zeevi (2013) minimized regret under MNL choice with explore-then-exploit policies, obtaining and bounds for instances whose best and second-best assortments are well separated. Agrawal et al. (2017–2019) proved the instance-independent lower bound formalized here; Chen and Wang (2017) later obtained when .
There are products. An instance consists of a no-purchase weight , attraction parameters with , and revenues . At each period the seller offers an assortment and observes a choice , where means no purchase. Under the multinomial logit (MNL) model,
and choices are independent across periods given the offered sets. The expected revenue of is .
A policy chooses from the past assortments and choices, possibly at random. It satisfies the -cardinality constraint if always. Its regret over periods is
where maximizes over assortments of at most products.
A randomized instance is a probability distribution over instances with common known revenues and a common no-purchase weight; the regret against it is averaged over the hidden attraction parameters, the choices and the policy's randomization.
There is an absolute constant such that for all , and there is a finitely supported randomized instance, chosen before the policy, such that every policy respecting the -cardinality constraint satisfies
The constant is not fixed; any positive value suffices.
The paper proves Theorem 2 in two cases.
Items 1–3 serve the case , which the paper reduces to a multi-armed bandit through the instance of Definition 5.2 ( products in groups of , one hidden group with larger attraction). Items 4–5 serve the case through the two-point instance of Definition E.1.
The theorem shows that the growth of regret in assortment learning cannot be improved, and that the dependence on the number of products is polynomial: when the display size is fixed, the UCB policy of the same paper is optimal up to logarithmic factors (Remark 4). It separates what learning under the MNL model costs from what the combinatorics of the assortment adds, and the reduction it uses, simulating an assortment algorithm inside a bandit algorithm, is reusable for other choice-model bandits.
The result is proved in the paper, with its proof in Appendix E. To our knowledge neither the theorem nor its lemmas have been machine-checked. A formal proof has to repair several printed slips: Lemma 5.1's hypotheses do not exclude close to , where the bound fails; the proof of Lemma E.2 uses a form of Pinsker's inequality with a wrong constant; Lemma E.1 states one direction of the divergence and computes the other; and the constants of the case do not match. The formal statements here carry the corrected hypotheses, each disclosed in its note.
The obvious argument fails at the reduction. The bandit lower bound is a statement about algorithms that pull one arm per round, while an assortment policy offers products at once and sees a choice among them. Transferring the bound requires simulating MNL feedback from Bernoulli coins (Algorithm 2 of the paper), whose loop has a random length, and then relating the regret of the simulated assortment algorithm over a random number of calls to the bandit regret over pulls. The paper does this in expectation, and the constants have to be tracked through the random horizon.
A second difficulty is that the lower bound must hold for every policy, including randomized ones, against a single randomized instance fixed in advance. Bounding the regret of each deterministic policy separately is not enough unless the instance does not depend on the policy, which the statement requires. The change-of-measure steps (Lemmas E.2 and E.5) need a chain rule for the divergence between laws of adaptively generated histories.
Products, periods and arms are 0-based (Fin n); a choice is Option (Fin n) with none the no-purchase alternative. Histories have finite length , laws of histories are explicit products of policy weights and MNL (or Bernoulli) probabilities, and every expectation is a finite sum, so no measurability or integrability side conditions arise. The no-purchase weight is explicit (Definition 5.2 has ). is a maximum over the finite, nonempty family .
Policies are behavioural: at every history they give a probability vector over assortments, which by Kuhn's theorem covers the paper's admissible policies with external randomization. The randomized instance is a finite list of instances with nonnegative weights summing to one; every support point has the same revenues and no-purchase weight, which are known to the seller. The quantifiers are in the paper's order: the constant first, then , then the randomized instance, then every policy. A formalization with the policy quantified before the instance, with allowed, with varying known revenues across hidden support points, or with only deterministic policies, would be weaker and is ruled out.
Hypotheses added to the printed statements: and in Theorem 2 (the claim fails for and ); , , in Lemma E.1; , , in Lemma E.2; , , in Lemma 5.1. Lemmas E.4 and E.5 use Definition E.1's , with and so the instance is defined. Lemma E.5 is stated, as in its proof, for deterministic policies.
The development reuses three published definitions: the MNL revenue ChoiceCDLP.MNL.mnlObjective, the Bernoulli divergence RegretBandits.Stochastic.klBern, and the discrete Kullback–Leibler divergence FoundationsRL.GeneralDM.klDivDiscrete (valued in ). Proved platform results useful to solvers include Pinsker's inequality (BanditAlgorithm.pinsker_inequality_total_variation), the Bernoulli bound (BanditAlgorithm.bernoulli_relative_entropy_le_sq_div_of_add_le_one) and a divergence decomposition for bandits. A chain rule for the divergence of finite adaptive histories, and a formal version of the simulation of Algorithm 2, would be reusable beyond this mission; both are welcome as supporting lemmas.
Bound constrained minimization asks for a low value of a smooth objective while each variable stays between prescribed lower and upper limits. Such limits occur in nonlinear optimization models even when the objective itself has no special convexity. Coleman and Li's interior reflective method was designed to approach a solution from inside those limits while using curvature information from a Newton system. Its local convergence claim explains what the method does after an iterate reaches the neighborhood of a suitably regular solution. The source is Coleman and Li (1994), especially Section 6 and Theorem 13.
The local result is distinct from a claim about finding that neighborhood. An algorithm can have excellent behavior near a solution without being guaranteed to reach it from every starting point. This mission isolates the precise local claim for the method in Fig. 11, including its reflected motion at a bound. It also records a regularity correction: the paper's stated twice continuous differentiability assumption alone does not imply a quadratic rate.
Let be the objective and let describe a box . A lower bound may be and an upper bound may be . The strict interior consists of points satisfying for every coordinate. Write and .
The method's scaling vector selects a bound according to the sign of . If , it uses when is finite and otherwise. If , it uses when is finite and otherwise. Put . The first order equation is . At an interior point, Fig. 11 chooses a scaled Newton direction from and sets , where is the scaled Hessian plus the diagonal correction in (2.5).
A reflective path follows and folds a coordinate back into the box whenever it crosses a finite bound. For a bounded coordinate this folding repeats after later crossings. The accepted value obeys and produces another strict interior point. Fig. 11 prints the rule as ; the squared scaling is a second disclosed correction, explained below. The iteration is .
At a candidate limit point , nondegeneracy says that any coordinate with lies strictly between its bounds. The free coordinates are those strictly between bounds. The second order sufficient conditions used here require that is feasible, , and the Hessian quadratic form is positive on every nonzero direction supported on the free coordinates. Section 6 also defines a finite family whose allowed coordinate choices come from (6.4). Coleman and Li, pp. 193–194 and 211–213 give these definitions and the local algorithm.
The supporting targets establish that the family vanishes at and has regular Jacobians there, that a scaled Fig. 11 direction is a Newton step for one family member, and that the reflected displacement is close to that direction. Lemma 12 makes the closeness quantitative at the coordinates that are active at . Theorem 11 states the corresponding abstract local Newton result for a finite family of maps. These are the five milestones of the mission, ordered from the model and abstract estimate through the step and path estimates.
The goal is the corrected local form of Theorem 13. For a fixed bound on the permitted step size deviation, a common neighborhood and constant work for every Fig. 11 run starting there:
The radius and are chosen before the run. A companion statement asserts that, when , a nearby interior point begins at least one run satisfying the algorithm's conditions.
The theorem gives a local rate for a feasible Newton method that can meet and reflect from finite bounds. It connects the behavior of the actual reflected iterates to Newton systems whose Jacobians are regular near . This matters when the solution is on the boundary: convergence of an unconstrained Newton step by itself says nothing about whether the iterates remain feasible. Theorem 13 is a known paper result, and this mission asks for a machine checked proof of its corrected statement. None of this mission's seven draft theorems has a proof in the proposal; the published box definition is reused as an existing platform object.
The correction is mathematically material. In the one dimensional problem with no finite bounds and , the objective is and meets the paper's nondegeneracy and second order conditions. Fig. 11 with reduces to ordinary Newton iteration, whose error is of order rather than . The source's proof invokes the Lipschitz Jacobian condition (6.5) of Theorem 11; the goal therefore assumes the Hessian is locally Lipschitz at . This changes the literal hypotheses of the printed Theorem 13 and is disclosed in each relevant item.
The step-size rule needs a second correction. The proof on p. 212 asserts and so . On with and , however, , the Newton step is , and obeys the printed rule while giving . The run predicate therefore bounds by , which is as the proof needs and is still computable without knowing . Coleman and Li, Theorems 11 and 13 are the source of the two compared claims.
The scaling changes its coordinate formula when a gradient component changes sign, while the reflective path changes direction at each finite bound. A direct Newton estimate for an unreflected step does not control the displacement taken by Fig. 11. The finite family and the active-coordinate breakpoint estimate make the local statement precise across those choices. The abstract rate also needs a uniform regularity estimate for every member of that family. Twice continuous differentiability gives continuity of the Hessian, but it does not supply the linear modulus of continuity needed for a quadratic error bound.
The variables are Euclidean vectors indexed by ; the paper's first iterate is Lean's sequence index zero. Bounds use extended reals, while all distances, derivatives and norms use real Euclidean space. A published definition supplies ; this mission defines the strict interior, scaling, diagonal Newton correction, reflective map, run, nondegeneracy and second order condition, and the family . The bounded-interval reflection uses the paper's repeated folding, including steps beyond the first breakpoint. Division in Lemma 12 is accompanied by a nonzero Newton component, and Newton directions are solutions of linear equations rather than values of a possibly undefined inverse.
The paper's standing assumption says that the initial sublevel set is compact and that is on an open set containing . The local statements retain the smoothness clause and omit compactness because no local conclusion uses it. The sole added regularity hypothesis in the goal is local Lipschitz continuity of at ; the run predicate uses the corrected step-size rule . The existence companion requires : if it were zero, the only allowed step size could hit a bound exactly. Neither the goal nor the run predicate assumes the iterates are already close after the start, that they converge, or that the scaled step is a Newton step for a chosen ; those are the claims to establish. A feasible interior start is required, so a box with an empty strict interior has no run. Contributions on the general finite family Newton estimate, active-coordinate ratio, reflected path, and existence of interior runs are all directly useful to the goal.
Nearest neighbor searching asks for a data structure that stores points and, given a query point , returns a point of closest to . It underlies classification, vector quantization, data compression, pattern recognition and similarity search in databases. In dimension , exact methods either use space growing like or answer queries in time close to linear in , so practical systems settle for an approximate answer: a point whose distance to is within a factor of the true nearest distance.
Arya, Mount, Netanyahu, Silverman and Wu (J. ACM 45 (1998), 891–923) gave the first structure for this problem that is simultaneously of linear size, built in time, and answers -approximate queries in time for any fixed , with . The structure, the balanced box-decomposition tree (BBD-tree), and the priority search on it became the basis of the ANN library of Mount and Arya.
Timeline. Arya and Mount (SODA 1993) studied approximate nearest neighbor queries in fixed dimensions; the conference version of this paper (SODA 1994) gave an optimal algorithm; the journal version (1998), which the paper itself describes as differing from the conference version by a single balanced structure without auxiliary data structures (p. 897), is the one formalized here. Later work, for example by Har-Peled, Indyk and Motwani (2012), addressed the exponential dependence on .
Points are vectors in . For an integer the distance is , and for it is . A rectangle is a product of closed intervals; its size is the length of its longest side. A box is a rectangle with positive sides whose aspect ratio, longest over shortest side, is at most .
A cell consists of an outer box and an optional inner box ; as a point set it is , or the closure of . Its size is the size of . The inner box must be sticky for the outer one: in every coordinate, each of the two gaps between the inner and the outer interval is either or at least the width of the inner interval.
A BBD-tree subdivides a root box by two operations. A fair split cuts a cell by a hyperplane into a low and a high child; a shrink cuts it by a shrinking box into an inner child (outer box ) and an outer child (outer box unchanged, inner box ). Throughout, every box has aspect ratio at most , a parent's inner box lies entirely within one child (within the inner child of a shrink), and inner boxes are sticky. The cells at the leaves are the leaf cells; they cover the root box and have disjoint interiors.
The distance from to a cell is . Each leaf cell carries an associated data point in its outer box. The search enumerates the leaf cells in nondecreasing order of distance from , processes each by comparing its point with the closest point seen so far, and terminates at the first cell whose distance from exceeds . The goal bounds , the number of cells that did not cause termination, which is the count the paper's proof bounds ("the number of cells visited up until termination", p. 912).
For every valid BBD-tree, every Minkowski metric , every , every query point and every sorted enumeration of the leaf cells,
The packing constraint (Lemma 4, p. 908): for , the number of leaf cells of size at least meeting an open ball of radius is at most
Its proof has three stated steps, each a milestone: an ball of radius lies in an axis-parallel cube of side ; at most interior-disjoint boxes of side at least meet such a ball; and the leaf cells of size at least meeting the ball can be replaced by as many interior-disjoint boxes of size at least meeting it. The proof of Lemma 5 contributes two more: the diameter of a rectangle is at most (indeed ) times its longest side, and every visited cell has size at least , where is the distance to the last cell that did not cause termination.
A companion statement records the correctness of the termination rule: the closest point processed is a -approximate nearest neighbor.
Lemma 5 is the explicit content of the query bound of Theorem 1(i): each visited cell costs time to enumerate and process, so the query takes time, with no dependence on beyond the logarithm. Lemma 4 is the property of the subdivision on which this rests, and it is used again for the -nearest-neighbor variant (Lemma 6) and for approximate range searching with the same tree.
The results are proved on paper and widely cited; none has a machine-checked proof. The mission produces checked versions of the packing constraint and of the cell-count bound for an abstract BBD-tree, defined by its invariants rather than by a particular construction algorithm, so that any construction meeting the invariants inherits the bound. It also exposes two places where the printed argument needs care: the open versus closed ball in Lemma 4, and the step in Lemma 5 that applies Lemma 4 to cells within distance of , which touch the closed ball of radius .
The counting step of Lemma 4 is asserted on the page ("the densest packing of axis-aligned rectangles of side length at least is realized by a regular grid"), and a formal argument must replace that sentence with a genuine counting argument. The replacement step is the geometric core: the outer box of a leaf cell with an inner box overlaps every leaf cell inside that inner box, so outer boxes cannot be counted directly, and without stickiness many nested inner boxes could crowd against one face of a cell. Applying Lemma 4 inside Lemma 5 is not immediate either: the visited cells lie within distance of , so they meet the closed ball, while Lemma 4 concerns the open ball, and a naive enlargement of the radius changes the ceiling exactly when is an integer.
Points are Fin d → ℝ, the metric index is an element of ℕ∞ with , and the distance is defined explicitly by the formula above. Rectangles are pairs of corner vectors; boxes have positive sides and aspect ratio at most . A cell's point set is the closure of the outer box minus the inner box, as the paper's "cells are considered to be closed" requires; an inner box equal to its outer box is excluded. A BBD-tree is an inductive tree of splits and shrinks with a validity predicate expressing the §2.1 invariants relative to the root cell; the root may be any box rather than the paper's hypercube, and the construction algorithms of §2.2–§2.5 are not formalized.
The enumeration is a list of (leaf cell, associated point) pairs that is a permutation of the leaf cells, sorted by distance from , with each point in its cell's outer box. A cell is processed before its own termination test, and counts the cells processed before the cell whose test fires (all cells if none fires). Lemma 4 and its counting step use the open ball of property (d). Theorem 1's time and space claims, Lemmas 1–3 on the construction, and the -nearest-neighbor Lemma 6 are out of scope.
This convention follows the proof of Lemma 5, which takes to be the distance to "the last leaf cell that did not cause the algorithm to terminate" and bounds the cells up to that one. If the cell whose test fires is also counted, the printed bound can be exceeded by one: a valid one-dimensional tree with needs three processed cells against . The formal goal therefore states the bound for the cells that did not cause termination, which is what the proof establishes; consequently at most cells are processed in total.
The goal must not be trivialized: the enumeration must contain every leaf cell (an empty enumeration would give ), it must be sorted, cells must be closed sets rather than outer boxes minus open inner boxes (which leaves isolated boundary points and makes the goal false), and no size bound or packing fact may be assumed in the goal.
Contributions welcome: proofs of the milestones in any order, general lemmas on distances and interior-disjoint boxes (reusable beyond this mission), and a construction of valid BBD-trees from the paper's midpoint or middle-interval rules.
A convention is a pattern of behaviour that is customary because everyone expects everyone else to follow it: driving on the right, or which party yields at a narrow bridge. Peyton Young's The Evolution of Conventions (Econometrica 61 (1993) 57–84) asks how such a pattern can emerge from decentralized play. The players have limited memory and limited information, and nobody coordinates them. The paper's model, adaptive play, is now a standard dynamic of learning in games. It is the starting point of the stochastic-stability theory of equilibrium selection (Foster and Young 1990; Kandori, Mailath and Rob 1993), which builds on the perturbation theory of Freidlin and Wentzell (1984).
This mission covers the first half of the paper: §3 (the model) and §4 (convergence when the players make no mistakes). Before mistakes can be added and stochastically stable conventions selected, the unperturbed process must be shown to settle at all. Theorem 1 gives the condition under which it does.
Let be a game with finitely many players , a finite nonempty strategy set for each player, and payoffs for strategy tuples . Write for with player 's strategy replaced by .
If is weakly acyclic and , then for every best-reply distribution and every initial state ,
Theorem 1 identifies a class of games, the weakly acyclic ones, in which boundedly rational players who best-reply to small random samples of the past almost surely lock in to a strict pure equilibrium. The paper's examples of weakly acyclic games (p. 63) are pure coordination games and games with common interests in which no two strategy tuples are payoff equivalent. Absorption is in behaviour, not just in empirical frequencies. Example 2 shows that this fails for fictitious-play-like complete sampling, so the sampling ratio is a real ingredient. The absorbing states identified in the first milestone are the states among which the stochastic-stability analysis of the paper's later sections selects.
The result is proved in the paper. To the best of our knowledge no machine-checked version exists. The mission asks for a formal proof of Theorem 1 and its milestones for an arbitrary best-reply distribution. That generality is the paper's own: non-uniform sampling is explicitly allowed. A formal proof also pins down the memory bookkeeping in the paper's proof (look-backs of , and periods), which the text checks only in words.
Adaptive play is a finite Markov chain. The obvious route through the generic theory of absorbing chains requires showing that a convention is reachable from every state, and that is where the argument becomes delicate. A best-reply path in the game cannot be followed directly: each player only sees a random sample, and the players who are not moving must keep playing their old strategies. The proof gets around this by having the non-moving players keep sampling older parts of the history, so those parts must still be in memory. This is what forces the bound . A uniform, state-independent constant is then needed to turn reachability into almost-sure convergence.
Players form a finite type ι, strategies a family of finite nonempty types S i, and payoffs u : ι → (∀ i, S i) → ℝ. A state is Fin m → ∀ i, S i with position 0 the oldest play. A best-reply distribution is any p : ∀ i, H → S i → ℝ with the stated support. All statements quantify over every such p. Adaptive play is a Matrix H H ℝ, and "converges almost surely to a convention" is stated through matrix powers. That is equivalent to almost-sure absorption because conventions are absorbing. The condition is in ℕ. is an sInf on ℕ that is never empty under weak acyclicity.
The display (1) on p. 62 reads "the right-most element of ". The formalization uses the right-most element of the successor , the only reading under which the rule is meaningful.
The goal cannot be satisfied trivially. The sampling law is not fixed, the conclusion is a limit equal to from every initial state (not "with positive probability" or "along some path"), and the hypotheses are jointly satisfiable, for example by a coordination game with uniform sampling. A best reply to a sample uses the joint empirical distribution of the sampled plays, not independent marginals.
A complete development needs elementary Markov-chain facts about matrix powers and absorbing sets, plus combinatorics of shifted histories. These parts are reusable for any finite-memory learning dynamic. Proofs of individual milestones are welcome independently.
Related platform work: stochastic fictitious play in potential games (StochFictPlay.*, Hofbauer–Sandholm 2002) and calibrated learning to correlated equilibrium (CalibratedCE.*, Foster–Vohra 1997) formalize other learning dynamics. The perturbed process and the selection of risk-dominant conventions are the subject of the sibling missions The Evolution of Conventions II and III.
Many models in economics, biology and computer science are finite Markov chains that have several absorbing states or recurrent classes, so their long-run behaviour depends on where they start. Adding a small amount of noise (mistakes, mutations, experimentation) makes the chain irreducible, and the noisy chain then has a unique stationary distribution. As the noise vanishes, that distribution concentrates on some of the original recurrent classes. The stochastically stable states are the ones that keep positive weight in the limit; they are the states the system spends nearly all its time in when the noise is small but nonzero.
H. Peyton Young's The Evolution of Conventions (Econometrica, 1993) proved a general finite-state characterization of these states, which he used to select among the equilibria of coordination games under adaptive play. The characterization rests on the theory of small random perturbations of Freidlin and Wentzell (1984), developed for diffusions, and on a combinatorial lemma of theirs expressing stationary distributions through spanning trees. Kandori, Mailath and Rob (1993) characterized the limit distribution by spanning trees on the whole state space for their model of learning with mutations; Young's Lemma 1 generalizes their Theorem 1 (p. 78), and his Lemma 2 reduces the computation to the much smaller graph of recurrent classes. Foster and Young (1990) introduced stochastic stability for evolutionary dynamics, and the equilibria it selects in games coincide with the risk-dominant equilibria of Harsanyi and Selten (1988).
Let be a finite set and the transition matrix of a Markov chain on . A state is reachable from if for some ; is recurrent if every state reachable from can reach back; the recurrent communication classes are the communication classes of recurrent states.
A family of Markov chains on is a regular perturbation of if for all :
The exponent is the resistance of the transition . The graph has vertex set and an edge when for all small , weighted by .
For , a -tree is a spanning tree of edges of in which every has a unique directed path to . The potential of is
For classes , is the least resistance of a path in from to . On the complete directed graph with vertices and edge weights , the stochastic potential of is the least total weight of a -tree in .
If is the stationary distribution of for , then as , where is a stationary distribution of , and
Theorem 4 turns a limit of stationary distributions into a finite optimization: compute least-resistance paths between the recurrent classes, then a minimum-weight arborescence on the reduced graph. The answer depends only on the orders of magnitude of the perturbations, not on their exact values, which is what makes the result usable when the noise model is known only qualitatively. It underlies the equilibrium-selection results of the same paper (risk dominance in coordination games, Theorem 3) and much of the later stochastic evolutionary game theory literature.
The result is proved in the paper, with the tree formula imported from Freidlin and Wentzell. As far as is known, none of it is formalized: Mathlib has irreducible and primitive nonnegative matrices but neither the Markov chain tree formula, aperiodicity, recurrent classes of a finite chain, nor minimum arborescences. A complete development would produce these as reusable components.
The first idea is to take the limit in : compactness and (7) give that every limit point of is stationary for , but has many stationary distributions, so this neither proves convergence nor identifies the support. Both come from the tree formula, which makes a ratio of sums of products whose orders of magnitude are read off from the resistances; the absence of cancellation (all terms are nonnegative) is essential. The second difficulty is Lemma 2: an optimal -tree on the whole state space must be transformed, by the paper's tree surgery on junctions (pp. 80–83), into something comparable with a -tree on the class graph without increasing its resistance. The easy inequality glues optimal paths and zero-resistance trees together; the reverse inequality is where the work lies.
States form a Fintype X with decidable equality; chains are real matrices Matrix X X ℝ, row stochasticity is Matrix.rowStochastic, irreducibility is Mathlib's Matrix.IsIrreducible, and aperiodicity (every state has period 1) is defined in the mission. The family is a function ℝ → Matrix X X ℝ constrained only on ; all limits are one-sided (), is the real power, and "" is a real limit . Distributions are row vectors and stationarity is . Trees are parent maps with edges pointing toward the root. Potentials, class resistances and stochastic potentials are infima in EReal, where an empty infimum is ; under the hypotheses all of them are finite.
The goal quantifies over every regular perturbation, not a parametric family such as , and over every family of stationary distributions of the (unique by (6)). The recurrent classes are computed from , not supplied as data, and is computed on the class graph with weights ; defining as for some would make Lemma 2 definitional and is ruled out.
Contributions welcome: the Markov chain tree formula and the uniqueness of stationary distributions for irreducible finite chains (both reusable well beyond this mission), recurrence and the support of stationary distributions, and the arborescence surgery of Lemma 2.
StochFictPlay.* (Hofbauer and Sandholm 2002, stochastic fictitious play) and CalibratedCE.* (calibrated learning and correlated equilibrium).Economic lot sizing asks when to produce goods across a finite planning horizon when demand in each period is known. Producing in a period incurs a fixed setup charge and a marginal cost per unit, while goods may be produced before the period in which they are needed. Such a decision has to balance paying another setup charge against producing more units earlier. The model is a standard setting for studying how dynamic programming and linear optimization describe the same planning decision. Wagelmans, Van Hoesel and Kolen study faster algorithms for this model and, in Section 4, connect the optimal lot-sizing cost to a greedy solution of a dual program Wagelmans et al. (1992).
The dual connection is useful in its own right. It supplies a certificate for the cost returned by the forward dynamic program: a feasible dual vector attains that cost. The paper allows demand to vanish in some periods, which makes the dual values at those periods free and forces care in defining the dynamic program. The mission targets precisely that case.
There are periods . Demand and setup cost are nonnegative for the periods in the horizon. The marginal production cost is any real number. Write for cumulative demand from through . Values at period zero and beyond the horizon are bookkeeping only; every optimization constraint concerns periods .
The forward lot-sizing cost describes the least cost of serving periods under the zero-inventory property cited by the paper. Its recursion starts with . If , no new production is needed and . If , the last production setup may occur at some , giving
This piecewise definition matters even when only one period has zero demand. Taking the displayed minimum at would charge a setup that need not occur.
Program D′ chooses free real values to maximize , subject to
“Free” means there is no nonnegativity constraint on . The paper obtains D′ from the dual of the linear relaxation of its simple plant location formulation, using the variables of Formulation III Wagelmans et al., pp. S147, S152–S153. The mission takes D′ as the defined optimization problem.
The greedy forward rule visits periods in increasing order. At a period with , the chosen value is the minimum of the upper bounds left by the constraints indexed :
When , the rule places no restriction on . This matches the paper's statement that it may be assigned an arbitrary value. One concrete recursive vector in the definitions sets each such value to zero, but the goal covers every assignment.
The goal says that every vector satisfying the greedy rule is feasible for D′, agrees with the dynamic-programming cost at every prefix, and is optimal among all feasible D′ vectors:
The milestone path follows the Section 4 statements: feasibility of the greedy vector; decreasing greedy values across positive-demand periods; the prefix upper bound for any feasible dual vector; and Equation (2), which expresses a greedy prefix value using a minimizing production period. Equation (2) is stated with the induction hypothesis that appears immediately before it in the paper. The goal combines these claims without treating the desired value identity as a hypothesis.
The result identifies a dual certificate whose value matches the forward lot-sizing cost. It also explains why a greedy forward assignment can solve D′ despite each constraint linking the current value with all later periods. The full-horizon identity recovers the cost , and the comparison with every feasible vector makes the word “optimal” precise. The paper additionally says that this dual computation directly provides an optimal primal solution; this mission does not encode that reconstruction because it would require the primal formulation and its correspondence to Wagelmans et al., p. S153.
A formal proof would provide a reusable finite-horizon certificate theorem for this dual formulation and a careful treatment of empty and zero-demand prefixes. The paper's result is already proved mathematically. The Lean files in this proposal state the goal and its milestones; their theorem proofs remain to be supplied by solvers. Related platform goals about the convex hull of other lot-sizing formulations and the Federgruen–Tzur forward algorithm concern different objects, so they are credited as neighboring work rather than imported as this theorem.
A current greedy value is limited by every earlier production index, and feasibility must still hold for the entire horizon, not merely for the constraints truncated at the current period. Equality with also has to survive periods with zero demand, where the dual coordinate is unrestricted but its weighted contribution vanishes. The forward recurrence has a separate branch at exactly those periods. A formulation that assumes every demand is strictly positive would avoid the delicate case and would miss a feature the authors explicitly retain.
Lean represents the horizon by natural-number indices and the demand, setup, marginal-cost and dual sequences by functions . Finite sums use closed intervals; the sum before period uses , so it is empty when . Minima are over the nonempty finite set , only when . The horizon has empty sums and no constraints. The cost and dual values are real, with no sign condition on or .
Several informal phrases are made explicit. “The solution is feasible” means every D′ constraint through holds. “Optimal” includes feasibility, every prefix identity, and comparison with every feasible dual vector. “Can be given an arbitrary value” is represented by no greedy-rule condition at zero demand; the theorem quantifies over all vectors that satisfy the positive-demand conditions. The paper states monotonicity for consecutive nonzero-demand periods; the milestone uses any two positive-demand periods, skipping zero-demand positions so it holds for every choice of their dual values. The weak-duality milestone spells out the paper's reference to “duality and the structure of D′” as an inequality for each feasible vector and prefix.
The identification of with the optimum of the primal lot-sizing model relies on the zero-inventory property cited by the authors and is not separately formalized. Neither the equivalence of Program D and D′ nor the recovery of a primal production plan is an item here. The paper's running-time claims, including for the greedy forward algorithm and for its backward algorithm, are outside the scope: the paper does not fix a machine model or constants for them. A definition of as the optimum of D′ would make the value identity circular; the proposal defines it by the paper's forward recursion instead. The backward algorithm of pp. S153–S155 belongs to a separate development.
Economic lot sizing asks how to meet a known sequence of demands while deciding when to set up production and how much to carry forward. It is a basic deterministic inventory problem: a setup has a fixed cost, production has a per-unit cost, and inventory may be held for later demand. Recomputing every possible next production period in the standard backward dynamic program takes a quadratic number of candidate comparisons. Wagelmans, Van Hoesel and Kolen use the geometry of cumulative-demand points to identify which candidates can affect the minimum. Their Section 2 gives the threshold rule targeted here. Wagelmans, Van Hoesel and Kolen (1992)
The paper notes independent related work by Aggarwal and Park and by Federgruen and Tzur. The published Prove2Me items for Federgruen and Tzur formalize a forward recursion and its minimal optimal predecessor lists. They address the same planning problem through different state variables; the backward value and efficient periods of this mission are new objects. Wagelmans, Van Hoesel and Kolen (1992), p. S145
A planning horizon consists of periods , with , and an extra terminal period . In period , a known demand must be met without backlogging. The final demand is positive, ; a trailing zero-demand period could otherwise be deleted. A production setup costs , and every unit produced in that period has a marginal cost . The sign of is unrestricted. Holding costs have been absorbed into these transformed marginal costs, as in Section 1 of the paper. Define the remaining demand , with . If production at covers demand until the next production period , then units are produced. Wagelmans, Van Hoesel and Kolen (1992), pp. S146–S147
The backward value starts at and follows Equation (1). At positive demand, it minimizes over . When , skipping setup and using is an additional choice. The paper identifies with the optimal cost from onward using the cited zero-inventory property. This mission takes Equation (1) as the definition of ; it does not formalize the separate equivalence with the original production-plan formulations. Wagelmans, Van Hoesel and Kolen (1992), p. S147
For a fixed , plot the finite points for . Their lower convex envelope is a piecewise linear graph. Its endpoints and places where its slope changes are breakpoints; the corresponding period indexes form the efficient set . Write for the next larger index in . The consecutive-point ratio is . These objects have no optimization over production policies hidden in their definitions. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S150
Proposition 1 says every candidate outside can be removed without changing the minimum:
The endpoint and slope claims establish the geometry used in this reduction. Proposition 2 compares neighboring efficient periods using and . Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S149
The selected period is the first efficient index whose ratio falls below the current marginal cost, with the terminal period as fallback:
The goal asserts that the full candidate minimum is attained there and that the algorithm's resulting assignment equals :
This states the mathematical choice and value; it does not assert a time bound. Wagelmans, Van Hoesel and Kolen (1992), pp. S149–S150
The result reduces a finite dynamic-programming minimum to the vertices of a lower envelope and gives an explicit threshold for choosing a minimizing vertex. It explains which future production period the backward recursion may select even when marginal costs are negative or some intermediate demands are zero. The paper uses ordered slopes to implement the selection efficiently; a solver proving the statements here establishes the mathematical correctness of that selection independently of a particular list representation. Wagelmans, Van Hoesel and Kolen (1992), pp. S148–S150
The paper's result is proved in print. The Lean statements are open proof obligations in this proposal. A complete development would add reusable finite lower-envelope facts, including vertex dominance and the order of adjacent slopes, as well as a machine-checked treatment of the zero-demand tie convention. The previously published forward-algorithm items do not supply these backward-recursion facts.
A candidate point can have a smaller value than a neighboring point yet still fail to minimize for a given . Comparing raw values alone therefore cannot identify the selected period. The lower envelope must retain exactly the points that can support a line of slope , and their consecutive ratios must be ordered. Zero demand creates repeated abscissae; without a representative rule, a ratio may have denominator zero and the successor is ambiguous. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S150
Periods are natural numbers starting at ; is the terminal sentinel. Demands, setup costs, marginal costs and values are real numbers. Finite minima use attained Finset.inf', with nonempty domains. The effective score omits the common setup cost . No sign restriction is imposed on . The efficient set is determined by a finite chord test for lower-envelope vertices: points on a chord are excluded, and at identical abscissa and height the earliest period is retained. This makes explicit the paper's zero-demand replacement convention on p. S150. The successor is used only on nonsentinel efficient periods; there its denominator is positive. Wagelmans, Van Hoesel and Kolen (1992), pp. S147–S150
The algorithm's printed Iterations use where is required; the Lean statement uses , matching the preceding display and the numerical table. The zero-demand branch explicitly includes skipping setup. The selector is the ratio-threshold rule, rather than an argmin, and the efficient set is the actual lower-envelope vertex set rather than all periods. A finite zero-demand example and Tables I–II are used as verification data. The paper's bound, the binary-search implementation, the amortized list updates, the Wagner–Whitin specialization and the final production-plan construction are outside this mission: they require additional algorithm-state and cost-model statements. Wagelmans, Van Hoesel and Kolen (1992), pp. S149–S152
The (s, S) policy is the standard control rule for a single item reviewed periodically: when the inventory position reaches or drops below a reorder level , order enough to bring it up to the order-up-to level . Under a fixed ordering cost and fairly general holding and shortage costs, some (s, S) policy minimizes the long-run average cost among all policies (Veinott 1966). That makes computing the best (s, S) pair a routine subproblem in inventory software, in multi-echelon heuristics, and in textbooks.
Before 1991 the available methods searched a box of candidate pairs. Veinott and Wagner (1965) bounded the optimal and and compared policies within the bounds. Later methods (Johnson, Management Science 15, 1968; Bell, SIAM J. Applied Mathematics 18, 1970; Federgruen and Zipkin 1984) used policy iteration or partial enumeration. Zheng and Federgruen (1991) gave an exact search that walks a monotone staircase path through the grid, and showed it costs about as much as evaluating a single policy. The procedure is the one presented in standard inventory texts such as Zipkin's Foundations of Inventory Management (2000).
One-period demands are i.i.d. and integer valued, with , , and . An order costs . is the one-period expected cost when a period starts at inventory position . The paper assumes only:
Write and for the smallest and largest minimizers of . The renewal density and renewal function are
For integers , the long-run average cost of the (s, S) policy is
A pair is an optimal policy if for all integers . The optimal cost is the value of any optimal policy. For fixed , is an optimal reorder level if for all .
The algorithm (§3, p. 659) starts at any minimizer of .
For every demand law with , every , every satisfying the two assumptions, and every minimizer of , the algorithm terminates. On termination, with final values ,
The milestones are the results the paper's justification of the algorithm (p. 659) rests on, in the order it uses them:
The result. Theorem 1(a) makes the exact optimum of the (s, S) problem as cheap to compute as the cost of one policy, for any with unimodal. No convexity is needed, and lead times, random lead times of the Zipkin type, and linear purchase costs are allowed. Its bounds (Lemma 2) and the monotone staircase structure of the search also underlie later work on continuous review, discounting and approximation.
Formalizing it. The theorem is proved on paper. As far as we know, none of the results in this mission has a machine-checked proof: the platform's Veinott–Wagner items concern a different (discounted, convex) model. Formalizing it produces a verified correctness proof of a widely implemented algorithm, and checks the paper's lemmas at their edge cases. Two of the printed statements need repair: Lemma 1(b) and Lemma 3(a) (see the scope section).
Optimality is claimed over all pairs , an infinite set, but the algorithm visits only a monotone path. The proof therefore has to show that every pair it skips is no better. For a fixed , the skipped reorder levels are handled by the unimodality of (Lemma 1). The skipped order-up-to levels are handled by the one-comparison test of Lemma 3(a), and those above the stopping point by the bound of Lemma 2(b). An argument from joint convexity or joint unimodality of in is not available. The paper uses no structure of beyond what Lemmas 0–3 state, and these hold only under the side conditions written in them.
Lemma 2(b)'s printed proof leaves the class of (s, S) policies (it uses a randomized order-up-to level). The limit at may be finite, so need not be attained for every . Lattice demands, for which vanishes somewhere, create ties between adjacent reorder levels. Each of these breaks a naive transcription of the paper's argument.
VeinottWagnerSS.RenewalCost.DemandDist with the extra hypothesis . All costs are real.Queueing analysis constantly moves between two kinds of long-run averages: the fraction of time a system spends in some set of states, and the fraction of arriving customers who find it there. Waiting-time formulas for the M/G/1 queue, blocking probabilities in loss systems and many decomposition arguments rest on the claim that, when arrivals form a Poisson process, the two coincide. This property is known as PASTA, Poisson Arrivals See Time Averages. It is used throughout queueing theory, inventory theory and the analysis of communication networks, usually without proof.
Before 1982 the property had been proved under strong extra structure:
Let be a probability space. On it live a process , the state of a system, with values in an arbitrary measurable space, and a Poisson process at rate , counting customer arrivals in . The interaction between and is unspecified: arrivals may change the state.
Fix a set of states with for every , and define
is the fraction of time in that is in . is the number of arrivals up to who find in , and is the fraction of arrivals who do.
The paths of are assumed left continuous with right-hand limits w.p. 1, so that an arrival is not counted as already present at its own arrival epoch. is assumed jointly measurable in . The single structural assumption is the Lack of Anticipation Assumption (LAA):
for each , and are independent.
The paper's proof of (6) uses this independence for every event of , the σ-field generated by . The mission therefore states Theorems 1–2, (6), Lemma 1, (10) and Lemma 2 under lack of anticipation with respect to : for each , is independent of . This implies the printed LAA. The printed LAA together with independent increments does not give (6) or Lemma 1, because pairwise independence of the future from the past of and from the past of is not independence from their joint past.
Under lack of anticipation (with respect to , see above), for every random variable ,
The limit may be random, and the theorem asserts nothing about whether either average converges. It asserts only that the two converge together, to the same limit.
The proof in §2 passes through the following statements, which form the milestone list:
For a Poisson process with bounded, integrable rate and , where , the same equivalence holds with replaced by the rate-weighted average . Display (12), , is its analogue of (3).
Theorem 1 justifies replacing customer averages by time averages, and conversely, in any model where arrivals are Poisson and the system does not anticipate them. Examples are queue-length distributions seen by arrivals in M/G/c systems, blocking probabilities in Erlang loss models, and state probabilities at arrival epochs in networks with Poisson external input. It needs no ergodic theory of the observed process: convergence of one average has to be established separately, by whatever means suit the model, and the theorem transfers it to the other. Lemma 2 also implies versions of PASTA under weaker modes of convergence (Remark 6).
The result has been proved for four decades and is textbook material. What this mission adds is a machine-checked proof. No formalization of Theorem 1 in a proof assistant is known. A complete development would also contain machine-checked versions of several standard facts not yet available in Mathlib:
The naive argument conditions on the arrival epochs and claims that each arrival "samples" the state at a uniformly random time. This fails because arrivals influence the state: after an arrival, a queue-length process is no longer independent of the arrival stream. LAA only says that the future increments of are independent of the past of . The difficulty is to turn this one-sided independence into an almost-sure statement about long-run averages, along every path and at all times rather than only at fixed ones.
On the technical side, the expected-value identity (3) needs a limit of grid sums. That limit relies on left continuity: without it, satisfies LAA with but . The passage from expectations to a strong law needs a martingale structure and a second-moment bound, and the interpolation between grid times needs a pathwise argument.
Welcome contributions:
All of these are useful well beyond this mission.
The multi-armed bandit problem asks how to allocate effort sequentially among independent projects, only one of which can be worked on at a time, so as to maximise expected total discounted reward. It is the model behind research planning, clinical-trial allocation and job scheduling, and it is the prototypical example of a Markov decision problem whose state space grows exponentially in yet whose optimal policy is simple. Gittins and Jones (1974) and Gittins (1979) showed that each project can be given an index computed from that project alone, and that it is optimal always to engage a project of largest index. P. Whittle's 1980 paper gave a short proof of this theorem by attaching a retirement option to the process, and extended it to projects with individual horizons.
Timeline:
There are projects. Project has a state in a measurable space . Engaging project in state earns the expected reward and moves its state by a Markov kernel ; the other projects' states do not change. Rewards are discounted by , , and bounded:
The operator evaluates engaging project for one step.
In the -process one may also retire at any time for the reward . Its value solves (4), and the value of the single-project -process solves (9).
With per-project horizons, project may be operated at most more times. A project with is active, and lowers by one. The single-project value satisfies and
is the maximal expected reward of the -process under these limits. The index is the infimal with , and is the Gittins index. Finally
and is attained by the policy that, at , engages a project maximising when this maximum exceeds , and otherwise retires. The Lean goal has three conjuncts: , every measurable index rule (any tie-breaking) earns , and no feasible measurable Markov policy earns more than .
Theorem 1 reduces an -project problem, whose state space is a product, to one-dimensional retirement problems. The formula (13) shows more than optimality of the index rule: the derivative of the multi-project value in is the product of the single-project derivatives, so the multi-project value is computable from the projects separately. The finite-horizon version gives an inductive argument that avoids the interchange arguments of earlier proofs, and the infinite-horizon identity (12) follows from it.
The result is classical and proved. What this mission adds is a machine-checked version in a generality not yet on the platform: heterogeneous projects (each with its own kernel and reward on its own measurable space), a retirement option, and per-project horizons. The platform already has a proved index theorem for identical arms sharing one kernel and reward without retirement, BanditAlgorithm.gittins_index_theorem (Lattimore–Szepesvári, Theorem 35.9), single-arm retirement values in charge form (GittinsFiniteRetirementValue), and open Beta–Bernoulli special cases from Bäuerle–Rieder (MDPFinance.InfiniteHorizonApplications.proposition_7_6_7, proposition_7_6_9, theorem_7_6_10). None of these states Theorem 1, formula (13) or formula (12).
The obvious approach, value iteration on the product state space, gives existence of an optimal policy but says nothing about its structure. The content of Theorem 1 lies in the identity of a multi-dimensional value with an integral of a product of one-dimensional derivatives. Verifying it requires differentiating single-project values in (they are convex, but have a kink exactly at the index, where the choice of one-sided derivative matters), an integration by parts against a Stieltjes measure in , and an exchange of the expectation over the next state with the -integral. The exhausted projects () and the boundary need separate care in every step.
Fin N (0-based; the paper uses ). State spaces are arbitrary measurable spaces; no finiteness or countability is assumed. Kernels are Markov, rewards measurable and bounded as in (1), and (β = 0 is allowed). and are any constants satisfying (1).s : Fin N → ℕ; is Function.update s i (s i - 1) and is only applied to active projects.index takes the junk value 0 there; every use (the index rule, , ) ranges over active projects only.Option (Fin N) (none = retire), feasible (they engage only active projects) and measurable (each decision set is measurable), so that their expected rewards are well defined. The index rule allows arbitrary tie-breaking; the goal quantifies over every such rule.A complete development needs measurability of the recursive values, convexity of in with one-sided derivatives, Lebesgue–Stieltjes integration by parts, and Fubini for kernels. Convexity of finite-horizon retirement values and the integration-by-parts identity are reusable beyond this mission. Contributions to any milestone, and sorry-free lemmas on these ingredients, are welcome.
Many iterative algorithms update only part of a vector at a time. In a parallel implementation, one processor may read a value written several rounds earlier by another processor. Random observations also perturb each update. John N. Tsitsiklis's 1994 paper gives conditions under which such an asynchronous stochastic iteration still converges. The paper develops the result to analyze Q-learning, where state-action values are revised from sampled costs and successor states. Its general theorem also applies to iterative fixed-point calculations beyond that application.
The central issue is that a processor can choose which component to update after seeing the past, and its input can be stale. A convergence theorem that presumes a fixed update schedule or current data would miss both features. The paper's Assumptions 1–3 describe when delays, sampling noise, and random step sizes remain compatible with almost-sure convergence. Assumption 5 gives a weighted maximum norm contraction for the iteration map. Theorem 3 combines these conditions into the target of this mission.
Fix a positive integer and write for the vector after round . Let be the map whose fixed point the iteration seeks. For component , the step size lies in , the noise is , and is the time from which component was read. Thus has coordinates . With when component is idle, all rounds obey the single update equation
All quantities live on a probability space with law . The increasing filtration represents information available when the step sizes and delays are selected, before the round's noise is observed. Assumption 1 says every timestamp tends to infinity almost surely: no fixed old value remains in use forever. Assumption 2 makes the initial state, chosen step sizes, delays, and noise measurable at the specified times; the noise has conditional mean zero, and its conditional second moment is bounded by a deterministic affine function of the largest squared iterate seen so far. Assumption 3 requires, for each component, divergent total step size and a square-summable step-size sequence, with a deterministic bound on all squared partial sums.
For a vector with strictly positive coordinates, the weighted maximum norm is . Assumption 5 provides and such that for every . Assumption 6, used in the boundedness milestone, requires the related growth bound for some real . The weighted norm permits different component scales.
Theorem 1 is the main intermediate target. Under Assumptions 1, 2, 3, and 6, it asserts
The bound may depend on the sample path. Lemmas 1–3 of the paper are milestones in its analysis: a scalar noisy recursion converges, its tails become uniformly small, and the pathwise bounds in the contradiction step hold.
The goal is Theorem 3, under Assumptions 1, 2, 3, and 5:
This theorem does not assume bounded iterates or Assumption 6 separately. Its proof uses Theorem 1 after deriving the needed growth bound from the contraction condition. Lemma 8 is the remaining milestone, comparing the coordinate iterates to an auxiliary deterministic recursion and a noise tail.
The result gives a fixed-point convergence guarantee when coordinates update at different times, delays can vary, and update choices can depend on past observations. In the paper's Q-learning application, these features describe exploratory sampling and possible parallel computation with old state-action values. For discounted problems, the associated Q-learning map contracts in the maximum norm, so Theorem 3 supplies the convergence step once the stochastic assumptions are checked (Tsitsiklis 1994, §7).
The mathematical results were proved in 1994; this mission asks for machine-checked proofs of their formal statements. Its reusable output would include a model of asynchronous noisy iteration, a scalar martingale-noise convergence lemma with random conditional variance bounds, and a precise interface between weighted contractions and pathwise convergence. The goal and milestone theorem files are currently statements with proof holes, while the definition file compiles without one.
A coordinate's next value depends on a vector assembled from observations at several earlier times. A direct estimate against the current error therefore does not close: the stale coordinates can reflect larger past errors. The noise condition is also tied to the largest iterate seen so far, so a deterministic global variance bound is unavailable before boundedness has been established. These two dependencies make the ordinary synchronous contraction argument insufficient. The scalar noise result and the pathwise comparison lemmas isolate the conditions needed for the boundedness and convergence statements.
Vectors are functions Fin n → ℝ, with ; the source labels coordinates , while Fin n starts at zero. Function order is componentwise. The model sets on idle rounds and uses the paper's unified update equation. It does not store the sets of update times separately. The delay values on idle rounds are left arbitrary because they do not affect the update; the source chooses the current time there. All step sizes lie in , and all delays are at most the current time, on every sample path.
The probability law is a probability measure. The filtration consists of increasing sub-σ-algebras. The iterate sequence is explicitly assumed adapted in the main theorems, matching the paper's use of and its running maximum as -measurable random variables. Conditional moment assumptions use integral inequalities over measurable sets, allowing generalized conditional expectations when the noise need not have a finite unconditional second moment. The conditional upper bound is required nonnegative almost surely, as the original inequality entails. Divergence and square summability use partial sums, so a non-summable series cannot receive a default value.
The maximum norm is the finite supremum of coordinate absolute values, and the weighted norm divides by the strictly positive coordinates of . Almost-sure boundedness means a path-dependent finite bound on every coordinate and time. Pathwise Lemmas 3 and 8 are stated on a retained sample path, with the auxiliary quantities and hypotheses established at their locations in the paper; Lemma 8 uses the proof's translated and rescaled coordinates. These conventions rule out an empty coordinate type, junk integrals, and a vacuous boundedness claim. Contributions to the stated lemmas, their probabilistic infrastructure, and the final convergence proof are within scope.
Q-learning (Watkins, 1989) learns the optimal action values of a Markov decision problem from sampled transitions, without a model of the transition probabilities. At each step only one state–action pair is updated, with a noisy estimate of the Bellman operator evaluated at possibly outdated values of the other pairs. Watkins and Dayan (1992) gave a first convergence proof for discounted problems. Tsitsiklis (1994) and, independently, Jaakkola, Jordan and Singh (1994) placed Q-learning inside the theory of stochastic approximation: the Robbins–Monro scheme of iterating with decreasing stepsizes and zero-mean noise, here in an asynchronous form where different components are updated at different times using delayed information, as in the distributed iterations of Bertsekas and Tsitsiklis (1989).
Tsitsiklis's paper proves convergence with probability 1 under two structural hypotheses on the iteration mapping : a weighted maximum-norm contraction (Theorem 3), which covers discounted Q-learning, and monotonicity (Theorem 2), which covers undiscounted (stochastic shortest path) problems, whose Bellman operator is monotone but in general not a contraction. This mission formalizes the monotone case.
A mapping with components is given, and the goal is to solve . Time is discrete, . The iterate evolves by
where is a stepsize ( when component is not updated), is noise, and are delays: the update of component may read component as it was at an earlier time. All quantities are random variables on a probability space with an increasing sequence of σ-fields , the history up to the choice of the stepsizes at time .
Vector inequalities are componentwise and is the vector of ones. The paper's assumptions are:
In Lean the algorithm is the structure AsyncSA.Monotone.Algorithm with fields F, x, α, w, τ, and the assumptions are Assumption1–Assumption4.
Under Assumptions 1–4, if is bounded with probability 1, then
Boundedness is a hypothesis, not a conclusion: for monotone it must be established separately (the paper does so for Q-learning in §7). The bound may differ between sample paths.
Theorem 2 is the convergence result for asynchronous stochastic approximation driven by a monotone mapping whose fixed point is unique. Its main application is Q-learning for stochastic shortest path problems with improper policies excluded, and more generally any learning scheme whose expected update is a monotone, sup-norm nonexpansive operator in the sense of (7) (dynamic programming operators are the standard examples). The same pattern, an a.s. bounded iterate plus a monotone mean map, recurs in later analyses of asynchronous and distributed learning algorithms.
The result has a published proof but, as far as the platform's catalog shows, no machine-checked one: there is no formalized asynchronous stochastic approximation theorem, and no formal Lemma 1 for random stepsizes and random conditional-variance bounds. A complete development provides the scalar almost-sure convergence lemma, the deterministic envelope argument for monotone maps, and the pathwise comparison steps, each of which is reusable.
The noise has a conditional variance that grows with the iterate, so it is neither bounded nor integrable a priori, and the stepsizes are random and chosen adaptively. The classical deterministic-bound argument for Lemma 1 does not apply directly. The iteration is not a contraction in any norm, so there is no Lyapunov function giving a geometric decrease, and the delays mean that the mapping is evaluated at a vector no single time index describes. Convergence has to be propagated from the deterministic envelopes to the random iterate through a sequence of random times, one envelope at a time, and each step requires the noise accumulated after a random time to be small uniformly in the remaining horizon.
Fin n (0-based); vectors are Fin n → ℝ with the componentwise order, so Monotone F is Assumption 4(a) exactly. is r • 1.CondMeanZero, CondSqLe): for every -set on which is integrable, and in . Mathlib's condExp is not used: it is for non-integrable functions and would make the noise assumptions vacuous.tsum, which is for non-summable sequences. The constants are chosen before the almost-sure quantifier; the bound on is chosen after it.Adapted).tsum for the series, a deterministic bound on , or a second unrelated ) is ruled out by the choices above.Contributions welcome: a general almost-sure convergence theorem for Robbins–Monro recursions with generalized conditional moments (Lemma 1 and its tail version ), and lemmas on monotone maps satisfying (7).
Policy improvement is one of the two classical ways of solving a Markov decision problem: start from a policy, compute its return, and change the decision wherever another action looks better against that return. Howard (1960, Dynamic Programming and Markov Processes) introduced it for finite state and action spaces, and Blackwell (1965) proved it for discounted problems on Borel spaces. A related routine combines two given policies instead of improving one: at each state, follow whichever policy has the larger return there. Eaton and Zadeh (1962, J. Basic Eng. Ser. D 84, 23–29) proved that this combination of two stationary policies is at least as good as both in the negative case with finite state and action spaces (as credited on p. 889 of Strauch's paper).
Strauch's paper Negative Dynamic Programming (Ann. Math. Statist. 37 (1966) 871–890) treats the negative case: all one-stage returns are non-positive (costs) and there is no discounting. This case covers stochastic shortest-path and optimal-stopping problems with positive costs, where expected total returns may be and the contraction arguments of the discounted case are not available. Section 9 of the paper shows that both improvement routines remain valid there, for arbitrary randomized history-dependent policies on Borel spaces, and that they fail in the positive case (Examples 4.2 and 9.1 of the paper).
Timeline:
The state space and the action space are non-empty Borel sets. The law of motion is a probability kernel from to , and the return is a Borel function with whose one-step expectation is finite at every . There is no discounting ().
A policy chooses the -th action from a probability kernel that may depend on the whole history . The expected return from the initial state is
the sum of the expected one-stage returns. For a terminal reward that depends on the history , is the expected return of following for stages and then receiving .
Given two policies and , their continuation returns at a history are
the expected returns from stage on if , respectively , is used from on with its own kernels fed the full history. The switching policy uses on and on its complement. In Lean these objects are contReturn, IsSwitch, wmax (for ), InH (for ) and I, in the namespace NegativeDP.Switching.
For all policies , the switching rule defines a policy , and every such satisfies
With and the switching policy:
Theorem 9.2 (Howard): if then . Corollary 9.1: the switching theorem for Markov policies, comparing and at the current state. Corollary 9.2 (Eaton–Zadeh): for stationary , the rule where and elsewhere satisfies .
Theorem 9.3 yields an improvement step that needs only the returns of two policies, not an optimality equation or a value function. Its Markov and stationary forms give policy-combination results usable for stochastic shortest-path and positive-cost problems, and together with Theorem 9.2 they justify policy-iteration schemes in the negative case on general state spaces. Example 9.1 of the paper shows that no comparable routine exists in the positive case, so the sign assumption is essential.
The results are proved in the paper. No machine-checked version of any of them exists, for the negative case or on Borel spaces; the related items on Prove2Me treat finite or discounted models. This mission produces the statements in Lean over Blackwell's published model of history-dependent plans, a construction of continuation returns from an arbitrary history, and terminal rewards that depend on the whole history.
The argument of the discounted case, which passes to the limit through the vanishing tail , is not available: with the terminal term does not vanish, and returns may be . Comparing and at the current state only is not enough either: for history-dependent policies the continuation returns depend on the whole history, and the switching set must be shown to be Borel in the history before the switching rule is even a policy. The induction also requires integrating extended-real terminal rewards against the history law and identifying the integral of the one-step operator with the next-stage expected return.
DiscountedDP.Stationary.Plan (one Markov kernel per decision, on Hist S A n). Decisions are numbered from in Lean, so Lean's index is the paper's stage .EReal values computed as minus the lintegral of the loss ; Bochner integrals and toReal are never used, so a return of is not silently turned into . is the sum of stage expectations, equal to by monotone convergence.IsSwitch, not constructed. A statement "every switching policy satisfies the bound" would hold vacuously if no plan satisfied the rule; the goal therefore also asserts that a switching plan exists, which is the content of the paper's "define by". The same pattern is used in Corollaries 9.1 and 9.2 (the rule defines a measurable decision rule).Contributions welcome: measurability of continuation returns in the history (needed for the existence part), the identification of the history law with the continuation law from the initial state, and a Chapman–Kolmogorov identity for the continuation kernels. These are reusable in any development on history-dependent policies over Borel spaces.
Many sequential decision problems accumulate costs that are never recovered: inventory holding and shortage costs, waiting times, the expected number of steps until a target is reached. Written as rewards, these are non-positive rewards summed over an infinite horizon without discounting. Ralph Strauch's paper Negative Dynamic Programming (Ann. Math. Statist. 37 (1966), doi:10.1214/aoms/1177699369) is the foundational treatment of this negative case on general Borel state and action spaces. It complements Blackwell's treatment of the discounted case (Blackwell 1965) and of the positive bounded case (Blackwell 1964, mimeographed), and it sets out which conclusions of the discounted theory survive when rewards are non-positive and undiscounted.
A central question in that theory is how simple an optimal policy can be taken to be. A policy may in principle randomize and consult the entire past history. Strauch showed that in the negative case, whenever an optimal policy exists, an optimal stationary one exists, using one measurable decision rule at every stage. This mission formalizes that result together with the reduction from general policies to semi-Markov ones on which its proof rests.
Timeline. Blackwell (1965) proved that in the discounted case a stationary optimal policy exists whenever an optimal policy does, and gave an example showing that Markov policies need not suffice on Borel spaces. Strauch (1966) proved the corresponding statement for the negative case and proved that semi-Markov policies, which remember the initial state as well as the current one, are enough.
A negative dynamic programming problem consists of non-empty Borel sets (states) and (actions), a law of motion , which is a probability kernel from to , and a Borel return function with
There is no discounting. A policy chooses the action at stage from a probability kernel , where is the history. A policy is Markov if for Borel maps , semi-Markov if for Borel , and stationary, written , if for one Borel rule . Random Markov and random semi-Markov policies draw from kernels in , respectively .
The expected total return from the initial state is
the optimal return is over all policies, and is optimal if for every . For a Borel rule , the operator acts on non-positive Borel functions by
The namespace is NegativeDP.Stationary. The objects above are Problem, Plan, I, In, vstar, IsOptimal and T.
Theorem 8.3 reduces a search over all randomized, history-dependent policies to a search over single measurable decision rules, whenever an optimal policy exists at all. It underlies policy iteration and the stationary-policy conclusions of the later negative-programming literature, and it shows that the negative case behaves like the discounted case on this point. In the positive case only a weaker statement holds. The reduction of §4 (Theorems 4.1–4.3) is reused throughout the paper: Theorem 8.1 on -optimal Markov policies starts from Theorem 4.3, and the value-iteration results of §9 use Lemma 3.1 and Theorem 5.1.
All results in this mission are proved in the paper. None of them has a machine-checked proof that we know of. The closest formal result is part 2 of Bertsekas's Proposition 7, formalized in an abstract monotone-mapping model (MonotoneDP.Increase.prop7_optimal_stationary_criterion). There, policies are sequences of selectors, so it contains neither the measure-theoretic reduction from randomized history-dependent policies nor Borel state spaces. The formal work here is to build the law of the controlled process on Borel spaces, carry out the conditional-distribution argument of Theorem 4.1, and combine it with the operator calculus of §5.
The obvious argument starts from an optimal , takes its first decision rule , and shows that is optimal. That fails for a general , because its first action may be randomized and its later actions may depend on the entire history. One first needs Theorem 4.3, which says a non-random semi-Markov policy is at least as good. That theorem needs two things. One is Theorem 4.1, which replaces a history-dependent policy by one built from conditional distributions of actions, and this requires disintegration of measures on Borel spaces. The other is the measurable selection of Lemma 2.1, which the paper takes from Theorem 2 of Blackwell and Ryll-Nardzewski 1963, applied stage by stage, with Theorem 4.2 to pass to the limit. On Borel spaces Markov policies are not enough (Blackwell's example, Example 4.1 of the paper), so the semi-Markov step cannot be skipped. Returns can equal , and every limit exchange has to respect that.
Borel sets are non-empty standard Borel types and Baire functions are measurable functions. The return is real-valued, non-positive and integrable under for every . Returns live in the extended reals. , , and all integrals of non-positive functions are computed as minus lower Lebesgue integrals of the corresponding losses in , so a return of is never collapsed to . is the sum of stage expectations, which equals the paper's expectation of the total return by monotone convergence. is the supremum over every randomized history-dependent plan. Restricting it to Markov or stationary policies would make the goal weaker, and that encoding is ruled out. Only the negative case (, ) is formalized. Results the paper labels "D, P, N" or "D, N" appear here in their N form.
Explicit choices:
Hist S A n is the paper's and the plan's kernel κ n is .Infrastructure needed: the law of the controlled process (built here by iterated kernel composition, as in the published DiscountedDP.Stationary model), disintegration of kernels on standard Borel spaces, a measurable selection theorem of Blackwell–Ryll-Nardzewski type, and monotone convergence for lower integrals. The disintegration and selection results are reusable well beyond this paper. Contributions to Theorems 4.1 and 4.3 are especially welcome, since missions II–IV of this series build on them.
School and university timetabling is one of the oldest applications of combinatorial optimization. In his invited review An introduction to timetabling (European Journal of Operational Research, 1985), D. de Werra opens with the class–teacher model: classes meet teachers for a prescribed number of one-period lectures, and the lectures must be placed into periods or days so that no class and no teacher is overloaded. Every richer timetabling model of the review (preassignments, unavailabilities, course scheduling) is built on top of this one, and the review keeps returning to its graph-theoretic reading as an edge-colouring problem in a bipartite multigraph.
The model comes in three levels of demand. The daily problem asks for a clash-free timetable. The weekly problem asks for an assignment of lectures to days within daily load limits. The balanced weekly problem asks, in addition, that the load of every class and every teacher be spread as evenly as possible over the week, and that the lectures of each class–teacher pair be spread evenly too. The last one is the practical requirement that a teacher should not have all four lectures with one class on Monday.
Timeline (as cited in the review).
There are classes and teachers . The requirement matrix is an matrix of nonnegative integers: is the number of lectures class must have with teacher . Write for the total load of class and for that of teacher . For nonnegative integers and , and are the floor and ceiling of the rational .
A schedule over periods or days is an array of nonnegative integers (, , ) that places every lecture exactly once:
In the Lean development these are IsCT1 R p x, IsCT2 R p a b x and IsCT3 R p x, with the floor and ceiling written lo s p and hi s p and the totals rowSum R i, colSum R j.
The statement fixes no constant: it asserts that perfectly balanced weekly timetables always exist.
The result. Proposition 2.3 says that the balancing requirement costs nothing: whatever the requirement matrix, the week can be organised so that each class and each teacher has an essentially constant daily load and each class–teacher pair is spread evenly. It contains König's edge-colouring theorem (take at least the maximum degree, so every daily load is at most one) and the weekly Proposition 2.2 as special cases. Combined with Proposition 2.1 applied to each day, it reduces weekly timetabling to independent daily problems, which is the decomposition the review recommends ("one may start by solving the weekly problem … and then solve separately the resulting daily problems", p. 154). In graph language it is the existence of equitable edge colourings of bipartite multigraphs, a standard tool in scheduling and in the theory of edge colourings.
Formalizing it. All results of this mission are classical and proved in the literature; none of them is formalized on the platform. Mathlib contains Hall's marriage theorem but not König's edge-colouring theorem for bipartite multigraphs, and not balanced or equitable colourings. A complete development gives a machine-checked König edge-colouring theorem in matrix form, the matrix-rounding step with simultaneous row, column and entry bounds, and the balanced-colouring theorem itself.
Each family of constraints alone is easy: spreading a single number evenly over days, or a single row total, is a matter of division with remainder. The difficulty is that one array must satisfy (1), (8), (9) and (10) simultaneously, so that the per-entry roundings must add up to correct roundings of every row total and every column total on every day. Rounding each entry independently breaks the row and column constraints, and greedy day-by-day choices can leave a remainder that no longer fits the bounds. The crux is integrality: the rational average satisfies every bound on every day, but the problem asks for integers, and an integral one-day slice must round all entries, all row totals and all column totals consistently.
Classes, teachers and days are Fin m, Fin n, Fin p; and are natural-number valued, which is the paper's " integer". Constraint (4) of CT1 is written . Floors and ceilings are Nat.floor and Nat.ceil of the rational quotient. In (8) and (9) they are applied to the row and column totals, never summed entrywise. The minimum number of days uses Finset.sup, whose empty value is , and is stated as an equivalence ("solvable over days iff ") rather than as an infimum.
Disclosed choices:
The formalization does not admit a trivial reading: CT3 requires all four constraint families at once, (1) is an equality, and the sanity checks show both that the Figure 1 data satisfy CT3 and that CT1 is not satisfiable for and .
Useful infrastructure, reusable beyond this mission: integral flows with lower bounds, or total unimodularity of bipartite incidence matrices; König's edge-colouring theorem for bipartite multigraphs; floor and ceiling arithmetic for natural-number quotients. Proofs of any milestone, alternative proofs of the goal, and a sorry-free proof of the Figure 1 instance are all welcome.
Q-learning is the basic model-free algorithm of reinforcement learning: an agent that does not know the transition probabilities or the reward structure of a controlled Markov process learns the optimal action values from experience alone, by a one-line update applied after every observed transition. It was introduced in C. J. C. H. Watkins' 1989 thesis, and the convergence theorem posed here is the one proved in C. J. C. H. Watkins and P. Dayan, Technical Note: Q-Learning, Machine Learning 8 (1992), 279–292 (doi:10.1023/A:1022676722315). Every later analysis of tabular temporal-difference control, and much of deep reinforcement learning's vocabulary, starts from this algorithm.
Timeline.
A finite controlled Markov process has a finite state set , a finite nonempty action set (the same in every state), mean rewards and transition probabilities . Rewards received steps later are discounted by with . The optimal action-value function is the unique solution of the Bellman optimality equation
In the -th episode the agent observes a state , performs an action , observes the next state and a reward of mean , and updates its table with a learning rate :
from given initial values . Episodes need not form a single trajectory. Writing for the episode of the -th visit to , the learning-rate condition is
The proof uses the action-replay process (ARP): from the recorded episodes one builds a finite-horizon process with states (a real state and a level ), in which taking at replays a randomly chosen earlier episode that tried in , emitting its reward and dropping to the level below that episode. Its expected one-step reward is and its aggregated transition probabilities are .
Given bounded rewards , learning rates and (3),
A further item states that the optimality equation has exactly one solution for .
The result. The theorem is the first guarantee that an agent can find optimal behaviour in an unknown finite Markov decision process from samples, with a per-step cost independent of the model. It is the template for convergence results on SARSA, TD(), double Q-learning and asynchronous value iteration, and it is the reference point against which finite-sample rates and function-approximation counterexamples are measured.
Formalizing it. The theorem has been proved since 1992–1994; this mission asks for a machine-checked proof. Two parts are reusable beyond Q-learning: the almost-sure convergence of scalar stochastic averaging with adapted steps (a Robbins–Siegmund type statement), and the perturbation bounds for finite-horizon values of Markov chains (B.1, B.4). The paper's own assembly in §3.2 bounds the error for each fixed action sequence and then passes to optimal behaviour; that passage is not justified on the page, so a complete development may route the final step differently. The milestones are the paper's lemmas as stated, with the corrections listed below.
The update touches one table entry at a time, at random times chosen by the agent, and its target depends on the current estimates, so the iteration is neither a plain average nor a contraction applied synchronously. Treating each entry as a separate Robbins–Monro average fails because the targets move with the other entries. The paper's device is to recognize as exact optimal values of the ARP (Lemma A), which turns the analysis into showing that the ARP, viewed from a high level, behaves like the real process for many steps; the probabilistic content is then concentrated in Lemma B.3, and the deterministic content in B.1, B.2 and B.4.
Everything lives in the namespace QLearning.Convergence, with one definitions module QLearning.Convergence.Setting. Conventions:
Fintypes with decidable equality, is nonempty, and is Finset.sup'. The process is a structure with R x a and P x a y , rows nonnegative and summing to .IsOptimalQ M γ Q (the optimality equation), which has exactly one solution (separate item); it is not defined by a limit or a choice.qIter … 0 .Trivializing formalizations are ruled out: the optimality predicate is satisfiable, conditional expectations are taken only of bounded measurable variables, the goal is the almost-sure statement under the probability model above rather than a pathwise or fixed-schedule one, and the ARP's optimal value is a supremum over policies, not the Q-learning recursion.
The development needs finite Markov chain values and contraction arguments (available in Mathlib in pieces), conditional expectations and almost-sure convergence for adapted sequences (Mathlib's martingale library), and the ARP construction above. Proofs of any milestone, alternative routes to the goal, and reusable lemmas on stochastic averaging are welcome. §4's extensions (absorbing undiscounted processes, multiple updates per episode) and equation (4) are not posed.
An assembly system must coordinate the production of components that meet at a common downstream item. A shortage of any required component can delay the finished product, while producing a component too early incurs holding cost. In Rosling's 1989 study, the central question is whether optimal decisions for such a tree can be understood using the simpler theory of a pure series inventory system. The paper proves an equivalence when the initial inventory positions are in a condition it calls long-run balance. That equivalence gives a precise route from an assembly network to serial inventory control without discarding its lead times or its discounted costs.
There are items in a tree rooted at end item . Every item has one immediate successor ; one unit of each component is needed for an end unit. Let be the production or delivery lead time of item . The total lead time is the sum of lead times on the path from to the end item, with , and the equivalent lead time is . Items are indexed so that is nondecreasing. These definitions and indexing conditions are in §§1–2 of the paper.
At the beginning of each period , outstanding orders arrive, the controller chooses the post-order echelon position , and then demand for the end item occurs. The pre-order position is , while is the position of predecessor from orders old enough to arrive after its lead time. A decision is feasible when for every immediate predecessor of . Decisions depend only on demands already observed. The demands are independent and identically distributed, nonnegative, and have a density and a finite positive mean.
The discounted Problem P charges echelon holding cost for item and a shortage coefficient for the end item. Its discount factor is . The objective is the expectation of the sum over periods of the holding charges and the expected end-item shortfall over demands, with a constant independent of the policy. The paper's Assumption requires every and . The system is in long-run balance in period when positions of adjacent items, compared at the same age relative to total lead time, satisfy equation (5):
The equivalent series system has successor , lead time , the same demand law and shortage coefficient, and holding coefficient . Theorem 2 states that its optimal policies and those of the assembly system agree when the assembly system is initially in long-run balance. In the formal statement, the first inclusion is unconditional; the reverse inclusion is conditional on Problem P attaining an optimum:
The target includes Lemmas 1 and 2, Theorem 1, Corollary 1, and the cost identity displayed in the proof of Theorem 2. Lemma 1 limits excess production, Lemma 2 gives a production lower bound, Theorem 1 describes when long-run balance is reached and preserved, and Corollary 1 uses the adjacent series position in that result. Each is stated at the strength given on pp. 568–569 of the paper.
Theorem 2 identifies the same policy choices in a tree assembly problem and a series problem whose stages have modified lead times and holding coefficients. It makes the serial interpretation exact for initially balanced systems and supports the paper's later discussion of series-system calculations. The statement is an equivalence of optimal policies, rather than just an equality of numerical values, so both the feasible-policy comparison and the cost comparison matter.
The theorem and its supporting results are proved in the 1989 paper; they have not been machine-checked in this development. A complete formalization would supply a reusable account of finite-history inventory policies, random demand histories, echelon positions, and extended-real discounted objectives. The published serial model SupplyChainTheory_multiechelon represents a different stage-indexed system; the assembly tree, its initial pipeline, and Problem P still need their own definitions. The paper's order-up-to Corollary 2 relies on an extension of earlier serial results and is outside this target.
The first natural comparison is to replace the tree's predecessor constraints with adjacent-item constraints. Those feasible sets are not equal for arbitrary states: positions at different total lead times can cross, and initial orders placed before period 1 affect the earliest periods. Long-run balance controls the necessary position comparisons, but equation (5) is empty for an item with . The printed proof also uses a middle inequality outside the range covered by equation (5) when an equivalent lead time vanishes. A faithful statement must account for these boundary cases without defining the series problem through the assembly problem's optimal policies.
Items use the paper's indices , with and . Lean period is paper period ; the policy sees exactly earlier demands. The common demand law is a probability measure on the reals, concentrated on nonnegative values, absolutely continuous with respect to Lebesgue measure, integrable, and of positive mean. The law of demand over periods is the pushforward of a finite product law under summation. Feasibility and the optimal-policy bounds are almost-sure statements, so changes on null histories do not alter them. Pathwise balance results quantify over one nonnegative demand path.
Initial positions include the orders placed before period 1. Their ages are monotone and obey the predecessor constraints inherited from that past. In addition to the paper's initial long-run balance, a separate boundary condition carries the missing comparison when . Discounting is restricted to : at the paper specifies average cost through a separate limiting prescription. The formal cost lies in the extended reals and is computed from its positive and negative parts; under the Assumption, feasible policies have a finite negative part. The policy-independent constant of equation (2) is omitted from both systems. “Optimal” means feasible and no more costly than every feasible policy, never a default value of an empty infimum.
The series system is built as a second instance of the same model, using the paper's successor, lead-time, and holding-coefficient transformations. Its cost and constraint (3) are then computed by the shared definitions. Contributions toward the lead-time identities, almost-sure policy comparisons, finite-time balance theorem, and extended-real cost identity are all part of the scope.
Spare-parts provisioning for repairable ("recoverable") items is a classical inventory problem: aircraft components fail, are sent to repair, and a stock of spares covers the units in the repair pipeline. Sherbrooke's METRIC model (Sherbrooke 1968), developed at RAND for the U.S. Air Force, measures the performance of a stock level by the expected number of backorders, the average number of unfilled demands outstanding at a random time. Every allocation computed by METRIC is driven by this quantity, and in particular by how it depends on the mean demand of each item.
For a new item that mean is not known. Air Force practice at the time produced a single engineering estimate of mean demand and computed backorders from it as if it were exact. In the section Demand Prediction (pp. 138–139) Sherbrooke argues that this practice is biased in one direction: under Poisson demand and any positive spare stock, the point estimate always understates expected backorders whenever the true mean is genuinely uncertain. This is his reason why a Bayesian treatment of demand is "of fundamental importance for all items, not merely low-demand items". The mission formalizes that claim and the computation behind it.
Fix one item. Its spare stock is stock on hand plus on order plus in repair, minus backorders; under one-for-one replenishment it is constant. Let the number of units in resupply at a random time be Poisson distributed with mean :
The expected backorders at spare stock are, by the paper's eq. (2),
In eq. (2) the mean is (customer rate times mean resupply time); on p. 138 it is the mean demand over a unit time interval. Only the mean enters, so it is written as one parameter . In Lean this is SherbrookeMetric.PointEstimate.backorders s lam, built on the published Poisson probabilities ServiceParts.StockLevels.poissonPmf.
Uncertain mean demand. The true mean takes the values , ( finite), with probabilities , . The point estimate is the mean of this distribution, , and the expected backorders accounting for the uncertainty are . The paper's example (p. 138) takes with probability each, so ; its procedure (p. 139) discretizes a gamma prior to five to ten values.
If two distinct values both carry positive probability, then for every spare stock
and for the two sides are equal for every prior. The goal fixes no constants and no particular prior.
and second derivative for . 2. Strict convexity, p. 139: for , is strictly convex on . 3. The worked example, p. 138 (off the goal's path): and .
The result. Expected backorders are the objective METRIC minimizes, item by item, subject to a budget. If the objective is evaluated at a point estimate, every item with uncertain demand looks better stocked than it is, and since the size of the error varies by item, the marginal comparisons that drive the allocation are distorted. The inequality is the quantitative statement behind the paper's recommendation to compute backorders as a posterior mixture over possible mean demands. It also says that an underestimate of demand costs more than an overestimate of the same size when backorders are the objective. For the bias vanishes because is linear.
Formalizing it. The paper proves the statement in one line ("it is easy to show") by differentiating twice. No machine-checked version exists. A formal proof needs termwise differentiation of the Poisson backorder series, a closed form for its second derivative, and the passage from a positive second derivative to strict convexity and then to a strict finite Jensen inequality under a nondegenerate prior. The resulting facts about are reusable in any Poisson inventory model (base-stock, policies, METRIC and VARI-METRIC). Convexity of in the stock level , the paper's eq. (3), is a different statement; it is already posed on the platform as ServiceParts.StockLevels.backorder_differences (compound Poisson demand) and is not repeated here. The definition of the Poisson probabilities is the published ServiceParts.StockLevels.Basic (Muckstadt 2005).
Each step is classical, but none is a one-liner in Lean. The series is an infinite sum whose terms depend on both through and through , so differentiating it twice under the summation sign requires a uniform summability bound for the derivative series on a neighbourhood of . The tempting shortcut of reasoning with deriv alone fails: deriv returns at points of non-differentiability, so a formula for deriv (deriv B) says nothing about smoothness, and the milestone is stated with HasDerivAt for this reason. The strict inequality further needs strict convexity, not just convexity, and a hypothesis that the prior is not concentrated on one value: with a one-point prior both sides coincide.
tsum over of for and otherwise. The family is summable for every real ; no statement relies on the tsum junk value.deriv alone (vacuous at non-differentiable points) does not meet the target.Service organizations keep repairable spare parts at a depot and at operating bases. Stock has a purchase or holding cost, while insufficient stock leaves backorders. Craig Sherbrooke's METRIC study describes how to evaluate such a system and distribute additional units among item types. Its fifth computational stage compares the reduction in expected backorders from the next unit with the cost of that unit. The comparison is delicate because the backorder function after optimizing the depot–base split can fail to be convex as a function of total item stock, even though a fixed depot-stock version is convex. Sherbrooke therefore introduces a convex extension before applying marginal analysis (Sherbrooke 1968, pp. 134–135).
This mission isolates the theorem in the paper's Appendix. It concerns abstract item functions with the properties needed for the allocation rule, so the result can be studied independently of the queueing assumptions and the FORTRAN procedure that produced those functions in METRIC. The paper supplies a proof of the Appendix theorem; the mission seeks a machine-checked formalization of its precise mathematical content (Sherbrooke 1968, pp. 140–141).
There is a finite collection of items indexed by . A decision assigns each item a stock level , where is permitted. Item has a unit cost and a real-valued function representing the backorder contribution associated with stock level . In the METRIC application, is obtained after choosing the best allocation of units between depot and bases. The Appendix theorem uses only that is nonincreasing and has a finite lower bound. “Decreasing” is read weakly: the paper's justification says that adding a unit “cannot exceed” the backorders at the previous level (Sherbrooke 1968, p. 136).
For a function , write . The function is discretely convex when at every level. The lower convex hull , written in the paper, is the greatest discretely convex function at or below . It follows the lower boundary of the convex hull of the points ; a point above that boundary is lowered, while a contact point keeps its original value (Sherbrooke 1968, pp. 135–136, 140). The existing ServiceParts.StockLevels.Basic definition supplies and for real stock-level functions; this mission reuses it.
The original objective is the separable sum
For each item, conditions (12) select the first level where adding another unit no longer lowers the convexified cost:
The second condition is automatic at , following the paper's convention (Sherbrooke 1968, p. 140, Eqs. (11)–(12)).
The Appendix goal is that each item's conditions (12) have exactly one solution and that the vector formed from those solutions minimizes the original, possibly nonconvex objective:
The milestone list follows the Appendix's claims: the lower boundary is a convex minorant; its marginal changes approach zero; (12) has a solution and that solution is unique; it minimizes the convexified single-item cost; and the selected level is a contact point where . The final comparison is with , not just with the objective formed from (Sherbrooke 1968, pp. 140–141).
The theorem licenses the paper's marginal allocation rule even when an item's original backorder function has nonconvex points. The rule can use a convex lower boundary to identify a level, yet the resulting allocation is optimal for the original function. Without the contact-point conclusion, optimality of the modified objective alone would not give that guarantee. The theorem is stated for any finite number of independent items with the listed properties, so it is reusable beyond the specific depot–base model (Sherbrooke 1968, pp. 134–136, 140–141).
The paper proves the result informally. This mission's definitions and theorem statements compile locally as open Lean goals; they do not yet constitute a machine-checked proof. A related published Prove2Me result, ServiceParts.Allocation.allocOpt_correct, proves correctness of an allocation algorithm for piecewise-linear functions assumed convex. It does not address the convexification or contact claim here. The platform's posed ServiceParts.StockLevels.optimal_stock_criterion and greedy_fill_rate_optimal concern other marginal criteria and likewise do not settle this Appendix theorem. A successful development would provide reusable Lean infrastructure for lower convex envelopes of integer sequences, their forward differences, and separable finite allocations.
A one-step marginal comparison on the raw is insufficient when its forward differences can fall and then rise: an apparent local stopping point need not minimize the full sequence. Replacing by a convex minorant restores ordered marginal changes, but a minimizer of a smaller function need not minimize the original function. The central burden is therefore the exact relation between the lower boundary and the original points at a level selected by the strict condition in (12). Ties in the objective add a second precision issue: the selected level is unique under the rule even when the objective has more than one minimizer (Sherbrooke 1968, pp. 135, 140–141).
Stock levels are natural numbers, item contributions and costs are real, and the item type is finite; the empty item type is allowed, making both the sum and the coordinatewise statement trivial. The functions are nonincreasing and bounded below, as in the Appendix. The lower hull is a pointwise real supremum over all discretely convex minorants. Its defining family is nonempty and bounded at each point under the lower-bound hypothesis, which every hull theorem carries. The hull is therefore fixed by the input function rather than supplied as an arbitrary minorant. The goal compares every vector in , without a budget restriction. The formalization does not use a default value for : the predecessor condition applies only to positive stock levels.
The paper prints with at least one positive cost. Its existence assertion fails when a particular : for , a bounded, decreasing, convex sequence, the first inequality of (12) never holds. The goal and existence milestone therefore require for every present item. The paper's phrase “unique optimizing” is interpreted as uniqueness of the stock vector determined by (12), together with its optimality. It cannot assert uniqueness among all minimizers: with , , and for , levels and tie. The proof's own wording identifies (12) as the unique selection rule (Sherbrooke 1968, p. 140).
The formalization contains separate definitions for discrete convexity, the greatest lower hull, conditions (12), and objective (11). It welcomes proofs and general lemmas about convex integer sequences and finite separable sums. The METRIC computation, empirical Air Force data, equations (7)–(9), and the discussion of Lagrangian versus combinatorial solutions are context rather than goals of this mission. A definition that simply sets , or a conclusion that minimizes only the hull objective, would omit the theorem's content.
A finite dynamic program with total reward is the basic model of sequential decision making without discounting: a system moves among finitely many states, a decision maker picks an action in each state, collects a reward, and the system moves on or stops. The quantity of interest is the expected total reward of a policy, summed over the whole (possibly infinite) horizon, and the question is whether a simple policy — one that uses the same decision rule at every step — is as good as any other.
For discounted or strictly substochastic models the answer has long been known. Shapley (1953) showed by successive approximations that, when every transition matrix has row sums strictly below one, some stationary policy maximizes the total reward among stationary policies; Howard (1960) gave the policy-improvement method for finding one; Blackwell (1962) showed that the maximum over all policies is attained among stationary ones. All of these rest on a contraction hypothesis .
Veinott's 1969 paper (DOI 10.1214/aoms/1177697379), best known for its sensitive discount optimality criteria, opens in §2 by proving these classical results under the much weaker hypothesis that each stationary policy is transient, and without requiring the transition weights to be substochastic at all. Partial results in this direction were due to Eaton and Zadeh, Derman, and Denardo. The total-reward model without a contraction assumption covers stopping problems, shortest-path type problems and models in which "transition weights" are not probabilities (growth factors, populations), which is why the generalized model is of independent interest.
There are states . In state a finite nonempty set of actions is available; taking action earns the real reward and assigns the transition weight to each state . No bound on is assumed. The set of decision rules is ; for , is the vector and the matrix .
A policy is a sequence of decision rules. The policy is stationary; uses first and then follows ; repeats the first rules of forever and is called periodic. Let and . The policy is transient if converges, and then its vector of total returns is
The one-step comparison measures the gain from deviating to for one step. Vectors are compared coordinatewise, and means , . For a matrix , and is its spectral radius. Finally and , both coordinatewise.
If every stationary policy is transient, there is with
The hypothesis concerns only the finitely many stationary policies; the conclusion compares against every policy, stationary or not.
Corollary 6 is the existence half of the theory of total-reward Markov decision processes: it says that the search for an optimal policy can be restricted to the finite set of stationary policies, and, together with Corollary 2 and Theorem 1, that such a policy is characterized by the optimality equation and by the absence of one-step improvements. Corollary 4, which the paper's introduction singles out as the section's main new result, shows that transience of the finitely many stationary policies already forces transience of every policy, uniformly; this is what makes well defined for all policies. Hoffman's Lemma 3 converts transience into a contraction in a rescaled norm, the device behind geometric convergence of value iteration (Corollary 3 of the paper).
On the formal side, Mathlib has matrices, summability and spectral radii but no total-reward decision model. These results are proved in the 1969 paper and are standard in the textbook literature on Markov decision processes; none of them has a machine-checked proof that we know of. Related platform items concern other models: the stochastic shortest path results of Bertsekas and Tsitsiklis (a cost model with a termination state, stochastic rows and an infinite-cost assumption on improper policies) and Blackwell's discounted model; neither covers nonnegative, non-substochastic weights.
Without a contraction, the standard argument — is a contraction, so it has a unique fixed point attained by a stationary policy — has nothing to start from: may exceed one for every , and the transition weights need not be probabilities, so no probabilistic coupling or stopping-time argument applies directly. Transience of each stationary policy is a statement about finitely many matrix powers , whereas the goal concerns infinite products of different matrices , whose behaviour is not controlled by the spectral radii of the factors in general. Passing from the stationary policies to all policies is the step where the obvious argument fails.
The Lean development fixes these conventions.
St; actions are a family of nonempty finite types A : St → Type, so is the dependent function type (s : St) → A s, not a common action set.Program St A with real rewards and nonnegative weights; no row-sum bound is part of the structure. Only 5° of Corollary 4 assumes .ℕ → F, indexed from : π 0 is . "All policies" means all such sequences.Summable of in the entrywise topology. is a tsum; it is the genuine series exactly for transient policies.spectralRadius ℂ of the complexified matrix, valued in .Finset.sup' over the finite set .A trivializing formalization is ruled out: the goal and Theorem 1 do not assume the competing policies transient (that would hide Corollary 4 inside the hypothesis), and since a non-summable tsum is , no statement compares of a policy whose transience is not either assumed or implied by the hypotheses. The hypothesis "every stationary policy is transient" is satisfiable (for instance when all weights are zero) and is not implied by any row-sum bound.
A complete development needs Neumann series for nonnegative matrices, the Perron–Frobenius-type fact that a nonnegative matrix with spectral radius below one has a nonnegative , and finite-dimensional spectral theory relating to . These are reusable well beyond this mission; contributions of such lemmas, and of proofs of the milestones in any order, are welcome.
A firm that holds a single stock of a product often serves customers of different priority: military and civilian requisitions, contract and spot customers, emergency and routine orders for spare parts. When stock runs short, it must decide not only how much demand to satisfy but whose. Satisfying a low-priority order now may leave the firm unable to serve a high-priority order that arrives later in the same replenishment cycle. Inventory rationing asks for the optimal rule.
Veinott (Optimal policy in a dynamic, single product, nonstationary inventory model with several demand classes, Operations Research 13 (1965)) studied a model with demand classes, but fixed in advance the rule that a lower class is served only when every higher class has been served in full, and gave conditions on the costs under which that rule is optimal. Topkis (Management Science 15 (1968), 160–176) dropped the fixed rule and characterized the optimal rationing policy within a replenishment period. Theorem 1 of that paper is the target of this mission. It extends the author's earlier two-class analysis; the two-class case was later partly rediscovered by Evans and by Kaplan. Critical-level rationing policies of this kind are a standard object in the later literature on multi-class inventory systems.
A period between two replenishments is divided into intervals, indexed backwards: interval has intervals after it, so the period starts in interval and ends in interval . Demand comes in classes , with class the most important. At the start of interval the firm holds stock and faces the outstanding demand vector : the backlog carried in plus the new demand , whose law on has finite means. Demands of different intervals are independent.
The firm chooses the vector of demand left unsatisfied, with , so that units remain in stock, where . It pays the penalty and the holding cost . A fraction of the unsatisfied demand is carried into the next interval: , with meaning complete backlogging and lost sales. At the end of interval the salvage cost is charged. The standing assumptions are:
The minimal expected cost of the last intervals and its expectation satisfy
with .
For a class , with its unit vector, the critical rationing level is if is strictly decreasing on , and is the smallest minimizer of on otherwise. With , the rationing level policy leaves unsatisfied
In words: going down from class , it serves as much of each class as it can without letting the stock fall below that class's critical level.
Suppose for every . Then
In attack order:
A companion item states the paper's remark that with a linear ordering cost the optimal order is .
Theorem 1 reduces the -dimensional rationing decision in each interval to numbers, which are computed from one-dimensional convex minimizations. Under complete or no backlogging this is the structural result that the rest of the paper builds on: the monotonicity of the levels in time (Theorem 2), the reduction of the backlog case to a single-interval problem (Theorem 3), and the multi-period ordering policy (Theorem 4). The hypothesis on is sharp in the sense the paper shows: for an example on pp. 165–166 has no optimal policy of this form.
The theorem is proved in the paper, but no part of it is machine-checked. A formal development would contribute a reusable treatment of finite-horizon dynamic programs whose value function is defined by an infimum and an expectation over an orthant, with convexity and continuity propagated through the recursion. It would also contribute the comparative statics of critical-level policies.
The obvious argument proves optimality of the rationing level policy by induction from convexity alone. That is not enough. Convexity gives a one-dimensional problem in (by (6) and Lemma 4). But identifying its minimizer with the class-wise critical levels requires the marginal value of class- demand to be independent of the demand of the less important classes, which is part (c). Part (c) is false when , so the induction must carry (a), (b) and (c) together and use at every step. A second difficulty is analytic: is an infimum and an expectation, and before any structural argument starts the value functions must be shown to be finite, attained, continuous and integrable on the closed orthant (Lemma 2).
Fin n; the paper's class is index , so class is the largest index and (b) is Antitone. Intervals are natural numbers counted backwards, as in the paper. Vectors are Fin n → ℝ with the pointwise order.sInf), and by a Bochner integral against . Every statement about , is restricted to and (or ). Lemma 2's attainment and integrability conjuncts are what identify these values with the paper's.WithTop ℝ, with . They are specified by the predicate IsCriticalLevel: strictly decreasing for , smallest minimizer otherwise. They are never computed by a real sInf, which would give the junk value when no minimizer exists.A Markov decision process with the average cost criterion asks for a policy that minimizes the long-run expected cost per unit time. The criterion is the natural one for inventory, queueing and maintenance systems that run indefinitely without a meaningful discount rate, and it is the standard benchmark in the theory of controlled Markov chains (Arapostathis et al. 1993, Hernández-Lerma and Lasserre 1996). Unlike the discounted criterion, it has no contraction to work with, and an average-optimal policy may fail to exist.
The classical route to average optimality is the vanishing discount approach: solve the -discounted problem, which is well behaved, and let . Schäl's paper gives conditions on a model with a general (Borel) state space under which this limit produces an average-optimal stationary policy.
Timeline. Taylor (1965) and Ross (1968) used the vanishing discount approach with equicontinuity via Arzelà–Ascoli. Sennott (1989) proved, for countable state spaces, that pointwise bounded relative discounted values yield an average cost optimality inequality and an average-optimal stationary policy. Schäl (1993, this mission) extended this to standard Borel state spaces under two alternative compactness–continuity conditions, (W) and (S). Later work, e.g. Feinberg, Kasyanov and Zadoianchuk (2012) and Feinberg and Liang (2022), weakened the compactness assumptions and studied when the inequality becomes an equation.
The model consists of standard Borel spaces (states) and (actions); nonempty action sets whose graph is measurable; a transition law ; and a measurable one-step cost . A policy chooses, at each stage , a randomized action that may depend on the whole history and lies in with probability one. A stationary policy is a measurable with .
For a policy and initial state , is the expected total cost of the first stages, and
A policy is average optimal if for every . The General Assumption is .
For , is the expected total -discounted cost, , , and is the relative discounted value function. The quantities and are the upper and lower limits of as . Condition (B) requires for each .
Condition (W): is locally compact with countable base, the are compact and is upper semicontinuous, is weakly continuous on the graph of , and is lower semicontinuous there. Condition (S): the are compact, and for each fixed , is setwise continuous and is lower semicontinuous on .
Under the General Assumption, (B), and (W) or (S):
Moreover, for every sequence and every choice of -discount-optimal stationary policies , some average-optimal is a limit of them: under (W), with from , and ; under (S), .
The theorem gives existence of an average-optimal stationary policy on a general state space from checkable model conditions plus pointwise bounds on relative values, without assuming a solution of the average cost optimality equation. It also identifies the optimal average cost as the Abelian limit of discounted values, and says how to compute an optimal policy: as a limit of discount-optimal ones. §4 of the paper verifies (B) through entrance-time bounds and applies the theorem to Assaf's invariant problem and to a finite-capacity inventory model.
The result is a published theorem; none of it is machine-checked. Formalizing it requires the measure-theoretic layer of Borel dynamic programming (canonical path measures of history-dependent policies, discounted optimality equations, measurable selection of minimizers and of accumulation points) and Fatou lemmas for varying measures. These components are reusable for any Borel-space MDP. Related platform work: the Feinberg–Liang average-cost optimality equation under an additional equicontinuity assumption is posed separately (FeinbergLiang.ACOE.acoe_of_assumptionEC); it is a different theorem.
The naive argument takes a pointwise limit of as in the relative optimality equation (2.2). Under (B) the family is only bounded pointwise, so no subsequence need converge, and even a pointwise lower limit loses the continuity needed to pass to the limit when is only weakly continuous. The generalized lower limit repairs this, but then the limit has to be realized along measurably chosen states and indices, and the limiting actions must be selected measurably as accumulation points. The second obstacle is that only an inequality survives, with the constant ; turning it into average optimality needs the Tauberian comparison of Lemma 1.2.
The model reuses the published FeinbergLiang.ACOE.MDP (history-dependent randomized policies, the Ionescu-Tulcea path measure, , , ) with its constant lower = 0, and a local definition file adds action sets, admissibility, , , , , , , and Conditions (W), (S), (B). Committed conventions:
CondW: the topology on generates its σ-algebra and is locally compact, second countable and Hausdorff, hence metrizable; the metric of §3 is a metric-space instance. Under (S) no topology on is used, and the lower limit is (the discrete metric).A formalization that assumes an average cost optimality inequality or equation, or that assumes the existence of the limit , proves Proposition 1.3 rather than the goal; the goal derives the inequality from (W) or (S), (B) and the General Assumption alone. Contributions to the shared infrastructure (Markov property of the canonical process, measurable selection theorems such as Brown–Purves, Fatou lemmas for varying measures) are welcome as separate theorems. §4 of the paper (entrance-time bounds for (B)) is outside this mission.