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?
Many problems in optimization and equilibrium modelling reduce to a system of nonsmooth equations with locally Lipschitz but not differentiable: reformulations of nonlinear complementarity problems, variational inequalities and Karush–Kuhn–Tucker systems through the function or piecewise smooth maps. Newton-type methods for such systems replace the Jacobian by a directional derivative or a generalized Jacobian and globalize with a line search on the residual .
Global convergence theory for these methods typically shows that every accumulation point of the iterates is a zero of (or a stationary point of ). That leaves open whether the whole sequence converges. L. Qi's 1993 paper in Mathematics of Operations Research (DOI 10.1287/moor.18.1.227) answers this with an attraction theorem: a zero with a nondegenerate directional derivative, once approached, captures the whole sequence of any descent method whose steps are controlled by the residual.
Timeline. Robinson (1987) introduced the B-derivative (as recounted on p. 229 of Qi's paper); Pang (1990, DOI 10.1287/moor.15.2.311) proposed the damped B-derivative Newton method and proved a global convergence theorem under strong conditions at the limit point; Han, Pang and Rangaraj (1992, DOI 10.1287/moor.17.3.586) gave two further globally convergent descent algorithms; Qi and Sun (1993, DOI 10.1007/BF01581275) developed the semismooth Newton method. Qi's 1993 §5 shows that, for convergence of the entire sequence to a zero, BD-regularity at that zero suffices for all three methods, without semismoothness.
Throughout, is locally Lipschitz and is the Euclidean norm. The directional derivative of at in direction is the one-sided limit
is directionally differentiable at if this limit exists for every , and B-differentiable at if moreover
is BD-regular at if it is directionally differentiable there and for every .
A descent direction method produces iterates with step sizes and directions , and is monotone in the residual:
A point is a limiting point of if some subsequence converges to it.
The damped Newton method (Algorithm 4.1) is the special case where solves and is chosen by the Armijo rule on .
Let be locally Lipschitz and B-differentiable, a descent direction method satisfying (5.1), and a limiting point of with and BD-regular at . If there are such that implies and
then
The result. Global convergence theorems for line-search methods usually stop at "every accumulation point is a zero". The attraction theorem upgrades that to convergence of the entire sequence whenever the zero is BD-regular, under assumptions that are checked locally and that hold for several algorithms at once. For the damped Newton method it removes the semismoothness assumption needed for the superlinear local theory, at the price of saying nothing about the rate. The same pattern (local error bound plus residual-controlled steps gives capture) recurs in the convergence analysis of Levenberg–Marquardt and projection-type methods.
Formalizing it. The result is proved in the paper; to our knowledge none of it has been machine-checked. The formalization needs the one-sided directional derivative and B-differentiability, the passage from BD-regularity to a uniform constant, and the trapping argument for sequences with cluster points. These pieces are reusable for any convergence proof of nonsmooth Newton-type methods.
The obvious argument says: near , steps are small because is small, so the iterates cannot leave. This fails as stated: a small residual at does not by itself prevent from being far from , and without a lower bound of in terms of the iterates could drift along a set where is small. The step that needs work is the error bound (5.5), which requires a uniform constant from the pointwise condition , valid in a whole neighbourhood of and not only along the directions the iterates happen to take. The set must also be chosen so that both its defining inequalities are preserved, which ties the radius to the residual through .
Points of are EuclideanSpace ℝ (Fin n); norms are 2-norms; is allowed. The directional derivative is the published one-sided NonsmoothNewton.Local.dirDeriv; every statement that evaluates it does so at a point where existence is assumed (BD-regularity, B-differentiability), so the junk value of an undefined limit never enters. "Limiting point" is a cluster point of the sequence, not its limit. Condition (5.2) is assumed only for iterates within of , as on the page.
Standing assumption and added hypotheses:
A trivializing formalization is ruled out: the goal does not assume that converges, that is bounded, that (5.2) holds globally, or that is semismooth; the hypotheses are jointly satisfiable (for , , , ).
Definitions needed: directional differentiability, B-differentiability, BD-regularity, and for Corollary 5.2 the norm function, the Armijo test (4.1) and runs of Algorithm 4.1. Contributions to the general theory of one-sided directional derivatives of locally Lipschitz maps (Lipschitz continuity and positive homogeneity of ) are welcome and will serve the companion missions of this series.
Adding a firm changes the offers available to workers; removing a worker changes the pool from which firms hire. In markets with salary bargaining, those changes can alter both assignments and pay. Kelso and Crawford asked whether the direction of the change can nevertheless be predicted at the outcome selected by their salary-adjustment process. Their 1982 paper studies firms that may hire groups of workers whose joint product need not be the sum of individual products. Theorem 5 gives two comparative-statics conclusions for that setting: a new firm leaves each worker at least as well off, and retaining a worker leaves each firm at least as well off.
The result follows the paper's finite-termination and firm-optimality results for the salary-adjustment process. Its comparison is specific to the process equilibrium under the no-ties conditions of Section 5; the paper does not claim that every core allocation moves in the same direction. This mission is the fifth of seven on the paper. Mission 1 concerns termination and the discrete core, mission 2 the continuous strict core, mission 3 a one-sided market, mission 4 firm optimality, mission 6 returns to workers and gross substitutes, and mission 7 the example without a core. The statements here are drafted independently of the other missions' unpublished declarations. None of this paper's statements was previously available on Prove2Me when the series was planned.
A market has a finite set of workers and a finite, nonempty set of firms. Worker 's utility from employment at firm for salary is . Firm produces from a set and earns profit . Workers care about their own firm and salary; the firm's product may depend on the whole set it hires. Every worker–firm pair has a starting salary , and permitted salaries increase by a common unit : for .
Each round of the salary-adjustment process records permitted salaries, offers from firms, and one tentatively accepted offer for each worker who receives any. Firms choose profit-maximizing sets of workers at current permitted salaries and repeat offers that were not rejected. A worker keeps a favorite available offer. A rejected worker–firm offer causes that pair's permitted salary to rise by next round. The process stops when no offer is rejected. An allocation assigns each worker one firm and a salary at that firm; an outcome is the allocation read from a stopping round. The paper calls this a process equilibrium.
An allocation is in the discrete strict core when each worker's salary is permitted and meets the starting salary, each firm's profit is nonnegative, and no firm together with a set of workers can make every participant weakly better off and at least one strictly better off using permitted salaries. The weaker discrete core excludes coalitions that make everyone strictly better off. The paper assumes workers' utilities are continuous and strictly increasing in salary; marginal product (MP) makes hiring an additional worker at the starting salary weakly profitable; no free lunch (NFL) sets the product of the empty set to zero; and gross substitutes (GS) lets a firm keep workers whose salaries did not rise when other workers' salaries increase. Section 5 adds no-ties conditions (NTW) for workers and (NTF) for firms relative to discrete-core allocations. These assumptions and their domains come from Sections 2 and 5.
The preliminary target is the paper's Corollary to Theorem 4: under these assumptions, all legal runs that stop have the same outcome. A second target is the new-firm-on-the-block process claim stated in the proof of Theorem 5: starting from the original market's final salaries, its outcome is a firm-optimal discrete strict core allocation of the augmented market.
The goal is Theorem 5. Write , and for stopping outcomes in the original market, the market augmented by one firm, and the market without one named worker. The two conclusions are
The first comparison concerns every original worker's utility. The second concerns every original firm's profit. The augmented market retains the original firms' technologies, utilities and starting salaries, and the diminished market restricts those data to workers other than the removed one. All three markets use the same and satisfy the conditions of Theorem 4.
The theorem gives a direction for the effects of entry and worker exit even though assignments and salaries may both change and a firm's product may depend on its entire workforce. The comparisons are individual: every worker is covered by the entry conclusion and every firm by the exit conclusion. Process uniqueness makes these comparisons well-defined despite the choices of favorite sets and favorite offers that a legal run may make.
The mathematical claims were proved in the 1982 paper; the Lean statements in this mission are open proof obligations. The formal development would give reusable finite-market definitions of demand, gross substitutes, core blocking, and an explicit adjustment run. It would also make precise how outcomes in markets with different agent sets are compared. The Corollary and the new-firm process result are separate proof targets. Completing them would support the goal while keeping the paper's two comparative-statics conclusions together.
Firm entry changes which firm can make the best offer, and worker exit changes which subsets of workers a firm can hire profitably. A direct pointwise comparison of old and new assignments has no fixed correspondence: a worker may switch firms and a firm may hire a different group. Comparing arbitrary strict-core allocations is also insufficient, because Theorem 5 concerns the specific outcome chosen by the adjustment process. The formal proof must account for all legal tie choices and show that the identified stopping outcomes have the required utility and profit order. The paper's proof uses two modified processes; its take-my-marbles process raises the removed worker's salary to a value that need not belong to the discrete salary grid on which (GS) was assumed. This is a genuine modeling boundary for that intermediate statement.
Workers and firms are finite Lean types, with at least one firm. Salaries, utilities and products are real-valued; is positive. An allocation assigns every worker to a firm, as the paper's does. Option F represents firm entry: some j is an original firm and none is the entrant. The diminished worker set is the subtype of workers unequal to the removed worker. Gross substitutes is imposed only on the grid vectors each market permits, and (NTW) and (NTF) quantify over discrete-core allocations. Each theorem's assumptions explicitly include utility regularity, MP, NFL, GS, NTW and NTF wherever the paper says “the conditions of Theorem 4.” Section 5 allows starting salaries to vary independently of unemployment utility, so the reservation-salary equation from Section 2 is not imposed.
“The equilibrium” is represented by the outcome at any stopping round of any legal run; the Corollary states why this does not depend on those choices. “Converges in finite time” in the new-firm milestone means that each legal continuation has some stopping round. NFB's initial offers are fixed to the old firms' final offers and an offer from the new firm to every worker, a reading of the first round that NFB1 leaves implicit. The take-my-marbles convergence claim is not drafted because its off-grid starting salary requires a separate convention or a stronger GS assumption. These commitments exclude a vacuous market condition, a continuous-price substitution for the discrete theorem, and a comparison of unrelated markets. Contributions that establish the Corollary, the NFB claim, or the three-market comparison under these definitions are welcome; lemmas about demand and core allocation can be reused across the series.
The probability that a sum of independent random variables exceeds a large level is a central quantity in large deviation theory. It appears, for example, when relating tail assumptions on individual summands to the tail of their sum. For summands with light (exponentially decaying) tails, exponential bounds are often effective. For heavier tails, a large value of the sum can instead be produced by one large summand. Nagaev's survey studies bounds that make the contribution of such summands explicit.
S. V. Nagaev's survey Large deviations of sums of independent random variables, Ann. Probab. 7 (1979) collects upper bounds of this type. Its best-known result, the Fuk–Nagaev inequality (Theorem 1.3, p. 749), bounds from above by plus an explicit term built from truncated moments. Upper bounds alone do not show that the one-summand term is necessary. At the end of §1 (pp. 758–759) the paper gives a complementary lower bound that needs neither identical distributions nor regular variation of the tails, only centred summands with finite variances. This mission formalizes that lower bound and the steps of its proof.
Timeline. Fuk and Nagaev (1971) proved truncation inequalities of this kind; the survey refers to that paper for the proofs of its Theorems 1.1 and 1.2 (p. 752). A. V. Nagaev (1969) obtained the asymptotics of Theorem 1.9 (p. 753) for identically distributed, centred summands with tails , , slowly varying; in the range where one summand dominates, the survey's own argument gives , display (1.46), p. 756. The lower bound treated here (1979, p. 759) drops both the identical-distribution and the regular-variation hypotheses in exchange for explicit constants (, and in place of ).
Let be a probability space and independent real random variables on it. The paper writes
Throughout, is the level (p. 747). For an index , the sum without the -th summand is
and the one-big-summand probability is
the probability that the sum reaches while is the only summand that does.
In the Lean development these are S n X, Sj n X j, Bn2 P X and Pj P X x j, in the namespace NagaevLD.LowerBound.
Assume for every and . Then for
The result. Set beside the Fuk–Nagaev upper bound, the lower bound shows that in the range the probability is at least a fixed fraction of a one-summand term, , for any centred summands with finite variances. It is valid for every and every family of independent, centred, square-integrable summands, with no asymptotic regime and no tail regularity. It is a non-asymptotic counterpart of the asymptotics for regularly varying tails, and it indicates that the term in upper bounds of Fuk–Nagaev type cannot be removed.
Formalizing it. The result is proved in the 1979 paper; the local Prove2Me catalogue search found no exact formal statement of this bound. A formal proof would produce a reusable lower bound for tails of sums of independent variables and the decomposition (1.57) into one-big-summand events, which applies to any family of real random variables.
The individual steps are short. The step that needs care is the bound on : it requires the event to be independent of the event , which is generated by the other summands. Deriving this from mutual independence of means grouping the summands into and its complement and passing to a function of the complementary block. The first Chebyshev bound similarly needs the variance of to equal , again by independence of a sub-family. A naive union bound for one alone does not give the sum over : the decomposition into the disjoint events of (1.57) is what makes the sum appear.
X : Fin n → Ω → ℝ on a probability space, measurable and mutually independent (iIndepFun); the paper's are X 0, …, X (n-1). Probabilities are P.real of sets, with , and exactly as printed.MemLp (X i) 2 P). Mathlib's variance returns for a variable that is not square integrable, so without this hypothesis could be while the summands have infinite variance, and the goal would be false. is stated as .Many security-relevant inputs are noisy and do not repeat exactly: fingerprint minutiae, iris codes, lists of personal preferences, the set of features extracted from a document. A cryptographic key derived from such an input must be reproducible from a later, slightly different reading, without storing the input itself. Dodis, Ostrovsky, Reyzin and Smith (SIAM J. Comput. 38(1), 2008; arXiv:cs/0602007) introduced secure sketches for this purpose: public helper data that lets the holder of a nearby reading recover the original exactly, while revealing as little as possible about it.
When the input is a set of features, the natural distance is the size of the symmetric difference. Juels and Sudan proposed the fuzzy vault for this setting (Des. Codes Cryptogr. 38, 2006). Section 6.2 of Dodis et al. gives a simpler, deterministic variant, the improved Juels–Sudan sketch (Construction 5), whose storage and entropy loss are both for -element subsets of an -element universe, independent of . The paper's Theorem 6.1 is the analysis of that construction. This mission formalizes it.
Laws and average min-entropy. A random variable is identified with its law. For a pair ,
which equals , the average min-entropy of §2.4: the negative logarithm of the best probability of guessing after seeing .
Secure sketches. Let be a set with an integer-valued distance . A pair of procedures is an average-case -secure sketch (Definitions 3 and 4) if
The difference is the entropy loss.
The metric. For a finite universe with , is the set of -element subsets of with .
Construction 5. Identify with a finite field of elements and let .
The Lean development names these charPoly, sketchCoeffs, sketch, pHigh, Step3Cond and recover, and the metric SDifS with distance sdifDist, in the namespace FuzzyExtractors.ImprovedJS.
For every finite field with elements, all and every real ,
The goal is uniform in : the entropy loss does not depend on the input distribution.
The paper's argument on p. 21 splits into four steps, each a milestone:
A fifth, off the goal's path, records Step 2's remark that the sketch consists of the first elementary symmetric polynomials of , up to sign.
The security half is the entropy bound: since takes at most values, (the paper cites its Lemma 3.1, which is posed in the first mission of this series and is not restated here).
The result. Theorem 6.1 gives a secure sketch for set difference whose sketch length and entropy loss are , which the paper shows is essentially optimal when (§6.2, via Lemma C.1 and a constant-weight code bound). It improves the original fuzzy vault, whose entropy loss the paper analyses in Appendix D and finds good only when the stored data is very large. Through the paper's generic composition with randomness extractors (Lemma 4.1), it yields fuzzy extractors for set-valued inputs in large universes, the regime of biometric feature sets.
Formalizing it. The theorem is proved in the paper; no machine-checked version exists on Prove2Me or, to our knowledge, elsewhere. A formal proof combines three pieces of reusable infrastructure: a probabilistic layer (average min-entropy of laws on arbitrary types, and the chain-rule-type bound for a function with few values), the combinatorics of symmetric differences of equal-size sets, and the algebra of Reed–Solomon unique decoding (a low-degree polynomial is determined by its values on enough points). Each of these is useful beyond this mission.
No step is deep; the difficulty is in the bookkeeping. The correctness argument relies on exact degree accounting: must agree with in every coefficient of degree at least , so that the remainder has degree at most , and the uniqueness count ("two candidates agree on at least points") requires the threshold to be at least ; the paper's sentence says "more than", which does not support the argument as written. The roots of must be shown to form exactly the set , with no multiplicities lost. The security half needs the average min-entropy of a joint law with a deterministic, -valued component bounded uniformly over all auxiliary variables, including those with infinite or uncountable range, where sums are infinite sums of extended nonnegative reals.
Conventions committed to in Lean:
PMFs; the procedures are kernels M → PMF S, here deterministic (PMF.pure). Average min-entropy is the joint form above, logarithms base 2, and the auxiliary ranges over an arbitrary ι : Type (a superset of the paper's ), never restricted to finite types.[Field 𝔽] [Fintype 𝔽], with = Fintype.card 𝔽; the paper's " is a prime power" is then automatic.degree < s - t, so when .A formalization that checks only correctness, drops or trivializes the entropy clause, or lets see itself, would not be Theorem 6.1. The goal states both clauses through the definition of an average-case secure sketch, with given only and the sketch.
Contributions welcome: proofs of the milestones, a general lemma bounding average min-entropy loss by the logarithm of the number of sketch values (the paper's Lemma 2.2(b) and Lemma 3.1), and Reed–Solomon uniqueness lemmas stated for reuse.
The Nelder–Mead simplex method (Nelder and Mead, 1965) minimizes a function using function values only. It is among the most widely used derivative-free methods in practice, built into standard numerical libraries, and for decades it had essentially no convergence theory. Lagarias, Reeds, Wright and Wright (1998) gave the first systematic analysis of the method with fully specified tie-breaking rules. Their results are limited to low dimensions, and the limits are genuine: McKinnon (1998) constructed strictly convex functions on with continuous derivatives on which the method converges to a point that is not the minimizer.
This mission formalizes the paper's two-dimensional analysis (§5) together with the general-dimension facts of §3 on which it rests. A companion series of missions treats the one-dimensional results of §4.
Fix coefficients of reflection , expansion , contraction and shrinkage with
A simplex in is a list of vertices , ordered so that ; is the best, the next-worst and the worst vertex, and . With , the trial points are ; reflection, expansion, outside and inside contraction use .
One iteration of Algorithm NM computes and then: accepts if ; if , accepts the better of and (the expansion point only if ); if , accepts if ; if , accepts if . If no point is accepted, it shrinks: every vertex is replaced by . An accepted point replaces and is inserted after every remaining vertex with value its own; after a shrink, the new vertices are reordered, with kept first if no new vertex beats it. A run is a sequence of simplices produced by successive iterations.
The edge matrix of a simplex is , the simplex is nondegenerate if , its volume is , and its diameter is . A function has bounded level sets if every is bounded. The standard method has , , .
For strictly convex on with bounded level sets and the standard coefficients, from any nondegenerate initial triangle,
The theorem does not claim that the triangles converge to a point, and the formalization does not claim it either.
Theorem 5.1 and Theorem 5.2 are among the few positive convergence statements for the Nelder–Mead method beyond dimension one. They show that on strictly convex functions in the plane the standard method cannot stall with a triangle of positive size; together with McKinnon's examples they delimit what can be proved: the simplices collapse, but not necessarily at the minimizer. The general-dimension lemmas of §3 (volume change, impossibility of shrinks on strictly convex functions, broken convergence) are used throughout the later literature on the method and its variants.
The results are proved on paper; no machine-checked proof of them is known. The formalization adds a precise, executable-in-principle definition of Algorithm NM with the paper's tie-breaking rules, and checked versions of statements whose printed form has small errors (see Formalization scope). The definition layer is reusable for any later work on simplex-based direct search.
The §3 lemmas are elementary but require bookkeeping of orderings, ties and change indices across iterations. The two-dimensional results are not. When the best vertex is eventually fixed (Lemma 5.1), the obvious measure of progress, the distance of the other vertices to it, is not monotone: reflections and outside contractions can move a vertex away, and contractions alternate in sign. Volume is also not monotone, because expansions double it. Lemma 5.2 and Theorem 5.2 depend on the precise acceptance rules: they are not known to hold for the original 1965 rule, which may accept an expansion point worse than the reflection point.
Points are EuclideanSpace ℝ (Fin n); a simplex is Fin (n+1) → E n with 0-based indices, so index 0 is , n-1 is and Fin.last n is . Runs are a relation: the paper leaves the ordering after a shrink partly open ("whatever rule"), so every theorem quantifies over all runs satisfying the iteration relation from an ordered start. Every theorem assumes (2.1) and a nondegenerate start; §3 lemmas assume exactly what each states about (bounded below, strictly convex, or nothing), and every §5 item assumes strict convexity and bounded level sets. Limits are asserted as existence of limits or taken as Tendsto hypotheses, never through a default-valued limit operator. Volume and diameter are a determinant and a finite maximum, never a supremum over an unbounded set.
Committed conventions and corrections:
A run relation that no sequence satisfies would make every theorem vacuous; it is satisfiable from every ordered start, and the hypotheses of the goal are jointly satisfied by and a concrete triangle (checked in Lean, not part of the mission). Welcome contributions: proofs of the §3 lemmas, which are independent of each other except through Lemma 3.3, and the reusable facts behind them (volume of a simplex under the Nelder–Mead moves, strict convexity along trial lines).
A forward equation evolves from an initial random value, while a backward equation is constrained by a terminal random value. When the two unknown processes appear in both equations, these boundary conditions can be incompatible. Such coupled systems occur in stochastic control, where a state moves forward and a cost or adjoint variable is determined backward. Antonelli's 1993 paper studies existence and uniqueness for a class of backward–forward stochastic differential equations and gives explicit examples showing why its smallness assumption on the coefficients cannot be discarded (Antonelli 1993, §§1 and 3).
This mission formalizes the first of those examples. It is a deliberately small two-equation system: both integrators are ordinary time, the coefficients are deterministic, and the Lipschitz constant is one. Nevertheless, the system has no solution when the time horizon reaches one. The claim identifies a genuine boundary for the paper's existence result rather than a failure caused by exotic stochastic integration. Antonelli presents it immediately after the existence theorem to show what can go wrong beyond the theorem's coefficient bound (Antonelli 1993, Theorem 3.1 and Example 1).
Fix a probability space and a filtration . The filtration satisfies the usual hypotheses: it is right-continuous, and contains every subset of every -null set. Let be a deterministic horizon. The initial random variable is -measurable, and the terminal random variable is -measurable. Both are integrable and strictly positive almost surely. These choices specialize the filtered space and input assumptions of §3 to Example 1 (Antonelli 1993, pp. 777, 785, 790).
The unknowns are two real-valued stochastic processes and . Their norm is
Thus a solution is a pair in of adapted processes satisfying a forward integral equation and a backward conditional-expectation equation almost surely at each time . Under the usual hypotheses every -class solution has such a representative, so this is the paper's solution class. The system uses and the constant input process . In this specialization, the measure used in the paper is , and the variation control process is (Antonelli 1993, (3.1)–(3.3), pp. 785–786).
The forward coefficient is and the backward coefficient is . Each has Lipschitz constant one with respect to . The absolute value is part of the example: it appears in the forward equation and does not appear in the backward equation (Antonelli 1993, (3.6)–(3.7), p. 790).
For every horizon and all data satisfying the assumptions above, there is no pair satisfying
This is Example 1's conclusion, including the boundary case (Antonelli 1993, pp. 790–791).
The milestones follow the four statements written in the example: representations of and in terms of each other, positivity and passage to the linear system (3.8)–(3.9), the martingale identity for their sum, and the identity for its constant mean . Their full text and page provenance are attached to the milestone list. The goal remains nonexistence for every ; it does not assert a particular formula for a solution.
The preceding existence theorem assumes a coefficient bound that becomes in this time-integrator case. Example 1 has and shows that the system can fail to have a solution as soon as that strict inequality fails. At , the obstruction is already present, so replacing by would lose part of the paper's conclusion (Antonelli 1993, p. 791).
A formalization would make the failure precise for the same solution class used by the paper. The current mission contains compile-checked Lean statements and definitions; the theorem proofs are still open. A complete development would also provide reusable statements about jointly measurable conditional-expectation versions, finite-horizon time integrals of processes, and martingales arising from coupled equations. These can support the paper's neighboring existence and nonsingular-example missions.
The main difficulty is the coupling between the two boundary conditions. The forward equation starts at , while the backward equation ends at ; neither equation can be treated as an independent ordinary differential equation. The absolute value in the forward coefficient also prevents the coupled system from being treated as a linear system at the outset. A second difficulty for Lean is that conditional expectation is defined only up to almost-sure equality at each fixed time, whereas the solution equations are equalities over time and probability together. The formal statement must connect these two kinds of almost-everywhere equality without strengthening the theorem to an identity at every time on every sample path.
Time is represented by , with only used in the norm. Time integration is Lebesgue integration on ; endpoints have zero mass. The norm is an extended nonnegative lintegral, so a nonintegrable process cannot be assigned the value zero by a real-valued integral's fallback convention. The random variable inside each conditional expectation is required to be integrable. The conditional-expectation process is a jointly measurable version whose value at each time agrees almost surely with the conditional expectation. The solution predicate asks, for each , that and be -measurable, that the two equations hold -almost surely, and that the time integrands be integrable along almost every path. Any -class solution can be replaced by such a representative, and the conditional-expectation version, so non-existence in this class is non-existence in the paper's class. For the Lipschitz coefficients in this example, finite norm gives pathwise integrability almost surely for the time integrals used in the equations.
The paper calls and “positive.” Here that means strictly positive almost surely. The weaker nonnegative reading would admit the zero pair when both data are zero and would falsify the target. Integrability of makes explicit §3's standing bound on the constant input process. The completeness and right-continuity of the filtration are also explicit. The solution class and equations are defined for general ; the restriction belongs only to the nonexistence theorem. For example, on a one-point probability space with , , the deterministic pair , solves the equations on . This rules out a definition that makes all solutions impossible by construction.
The development needs Mathlib's filtration, conditional expectation, probability measure, and integration APIs. Contributions proving the milestone statements or supplying reusable lemmas for their and martingale interfaces fit the mission. No semimartingale stochastic integral is required for this example.
A backward stochastic differential equation (BSDE) prescribes the terminal value of an adapted process instead of its initial value. Pardoux and Peng (1990) proved existence and uniqueness for Lipschitz coefficients, and BSDEs have since become a standard tool in stochastic control, mathematical finance and the probabilistic treatment of semilinear PDEs. El Karoui, Kapoudjian, Pardoux, Peng and Quenez (1997) introduced the reflected BSDE, whose solution is constrained to stay above a given obstacle process. Reflected BSDEs describe the price of American options in nonlinear markets (El Karoui, Pardoux and Quenez 1997), Dynkin games (Cvitanić and Karatzas 1996), and obstacle problems for parabolic PDEs.
In §7 of the 1997 paper the coefficient is assumed concave. Then the solution of the reflected BSDE is the value of a game: one player chooses a stopping time, the other chooses a control that sets the discount rate and the change of measure, and the value does not depend on which player moves first. This mission formalizes that statement (Theorem 7.2) and the results its proof uses.
Let carry a -dimensional standard Brownian motion , fix a horizon , and let be the natural filtration of augmented by the -null sets. Write for the square-integrable -measurable random variables, for the progressively measurable processes with , and for those with .
The data are a terminal value ; a coefficient , , , with for every and Lipschitz in with a constant ; and a continuous progressively measurable obstacle with and . A solution of the reflected BSDE is a triple of progressively measurable processes with , , , and
where is continuous, nondecreasing, and : pushes up only when touches .
For , is the set of stopping times with . When is concave, its conjugate is
The admissible controls are the bounded progressively measurable with . Each gives the affine coefficient , its reflected BSDE solution , the process solving , , and the payoff
For every and , , and
The last equality, the interchange of the two essential extrema, is the minimax content.
Theorem 7.2 identifies the solution of a nonlinear reflected BSDE with the value of a zero-sum game between a stopper and a controller. In finance, with the driver of a pricing rule under constraints or ambiguity, it says that the nonlinear price of an American claim is the worst case, over a family of discount rates and changes of measure, of linear American prices; and the stopper may announce the stopping rule first without changing the value. Concave drivers include the hedging equations with different borrowing and lending rates. The representation reduces questions about the nonlinear equation to a family of linear ones, which is how monotonicity, convexity and stability properties of nonlinear American prices are usually derived.
All four results and the goal are proved in the paper, with references to standard convex analysis and a measurable section theorem for two steps. None of them has a machine-checked proof. Mathlib has Brownian motion, filtrations, stopping times and conditional expectation, but no stochastic integral; the mission uses the Itô integral of the published Peng1990.SMP.Stochastic layer. A formal proof would give, beyond the theorem, a reusable comparison theorem for reflected BSDEs, a Snell-envelope representation for linear reflected BSDEs, and a measurable selection of supergradients along a process.
The inequality for each control is a direct consequence of comparison, since . The difficulty is the reverse inequality, which needs a single admissible control that attains the conjugate representation along the solution for almost every . Choosing a supergradient pointwise is easy; choosing it progressively measurable, bounded, and with square integrable is a measurable-selection problem. The interchange of ess inf and ess sup does not follow from a general minimax theorem: the family is not compact and the payoff is not convex–concave in any usable topology. It uses a specific stopping time, the first time touches , together with comparison on the random interval before it. Proposition 7.1 requires the linear change of variables , whose transformed equation lacks the square integrability of the original one, so the Snell-envelope argument has to be rerun with weaker moments.
L2F (progressive in place of predictable); and the obstacle condition are lower Lebesgue integrals in .MultiperiodRisk.Bellman.EssInf, and the essential supremum is its mirror image.Several formalizations of the goal would make it trivial, and each is ruled out. The conjugate is not a real-valued supremum, which takes a junk value when unbounded. The essential infimum over is not a pointwise infimum. The interchange of ess inf and ess sup is not dropped. The coefficient is a random field , not a deterministic or Markovian one.
The closing gloss of Theorem 7.2, that the triple is optimal, is not stated separately; milestone 4 is its control half. Contributions are welcome on a continuous version of the Itô integral, Itô's formula for products with , the Snell envelope in continuous time, and measurable selection of supergradients; all of these are reusable beyond this mission.
The Nelder–Mead simplex method (Nelder and Mead, 1965) is a derivative-free method for unconstrained minimization. It keeps a simplex of points in and replaces the worst vertex by a reflected, expanded or contracted trial point, using only comparisons of function values. It is one of the most widely used methods in practice, available in standard numerical libraries and scientific software, and it is also known for having very little supporting theory. McKinnon (1998) gave a strictly convex function in dimension 2 on which the method converges to a nonstationary point.
Lagarias, Reeds, Wright and Wright (1998) gave the first convergence results for the method as originally stated. In dimension 1 they proved that, for a strictly convex function with bounded level sets, both endpoints of the Nelder–Mead interval converge to the minimizer when (their Theorem 4.1). For the standard reflection coefficient they proved more: the convergence is eventually M-step linear, with a number of steps that depends only on the expansion and contraction coefficients (their Theorem 4.2). This mission formalizes that rate result and the move-sequence lemmas it rests on.
Let . A one-dimensional simplex is a pair of vertices ordered so that : is the best and the worst vertex. The method has four coefficients satisfying
This mission fixes , so (2.1) becomes , , . The trial points are
With , , and so on, one iteration is:
A shrink replaces by . The worst vertex is discarded and the accepted point joins ; it becomes the best vertex exactly when . Iterating from a nondegenerate initial pair () gives the run , and . A contraction means an outside or inside contraction.
Under each move multiplies the diameter by a fixed factor: for a reflection, for an expansion and for either contraction. The paper's bracketing index (its Lemma 4.2) is the first iteration with . Two integers control the move sequences after :
For all and there is an integer such that for every , every strictly convex with bounded level sets and every nondegenerate ordered , the index exists and
The goal fixes no value of ; the paper's proof gives one, but any depending only on and proves the theorem.
Theorem 4.2 is a rate statement for a method whose global behaviour is mostly unexplained. It shows that in dimension 1 with the method behaves like a bracketing line search: once the minimizer is bracketed, the interval shrinks geometrically, and the number of iterations per halving is bounded independently of and of the starting interval. With the standard coefficients , the value of constructed in the paper's proof is . The intermediate lemmas describe which move sequences the method can produce after the minimizer is bracketed.
The paper's results are proved; to our knowledge none of them has a machine-checked proof. This mission produces a formal model of the one-dimensional method with the paper's tie-breaking rules, and formal statements of the rate theorem and its supporting lemmas. Proving them is the remaining work, including the one-dimensional bracketing and proximity results of the paper's §4.2, which the proofs use and which are posed as a separate mission of this series.
The rate does not follow from a per-iteration bound: a reflection keeps the diameter and an expansion multiplies it by , so the diameter can grow for several consecutive iterations. A contraction-only argument fails for this reason. The theorem needs a bound on how long the method can avoid contracting and on how much expansion can happen between two contractions. Both bounds come from strict convexity applied along the line through the current interval, together with the location of the minimizer relative to the vertices (the proximity property of §4.2), and they must hold uniformly in . Making the constants uniform, so that and depend only on and , is the delicate part. Before no such control holds, which is why the theorem only speaks about .
The state is an ordered pair p : ℝ × ℝ with p.1 the best vertex and p.2 the worst vertex ; run f 1 χ γ σ p0 k is , and moveAt f χ γ σ p0 k is the type of iteration . The coefficient is substituted into the algorithm. The ordering rule is the paper's insertion rule (new point first iff , ties to the higher index); the printed formula contradicts the paper's own example on p. 118 and is read as its words describe. The expansion step accepts the better of and , the outside contraction is accepted on , the inside contraction on .
Standing assumptions carried by every statement: (2.1) with ; strictly convex on (StrictConvexOn ℝ Set.univ f); bounded level sets ( bounded for every ); and nondegenerate and ordered. Corollary 4.1 prints only ; the remaining conditions of (2.1) are the section's standing assumptions. is the natural-number ceiling ; is computed by a bounded search over , which loses nothing for . The uniformity of in Theorem 4.2 and of in Lemma 4.8 is encoded by quantifier order: they are chosen after and before , , .
The goal's conclusion includes the existence of the bracketing index (the paper's Lemma 4.2), so the halving claim cannot hold vacuously for a run that is never bracketed; a statement that lets depend on or is a different and much weaker theorem and is ruled out by the quantifier order.
A complete development needs: the one-dimensional facts about strictly convex functions (the paper's Lemma 4.1), the absence of shrink steps under strict convexity (Lemma 3.5 for ), the bracketing and proximity lemmas of §4.2, and the move-sequence and diameter-product arguments of §4.3. The model of the one-dimensional method and the convexity lemmas are reusable for the series' first mission (convergence of both endpoints). Proofs of individual milestones, and of the §4.2 lemmas as local results, are welcome.
A steady-state simulation produces a single long output path , and the quantity of interest is its long-run mean . The central difficulty of simulation output analysis is that the observations are correlated, so the classical confidence interval needs a consistent estimate of the time-average variance constant , which is hard to obtain. The method of standardized time series (STS), introduced by Schruben (1983) and put on a general footing by Glynn and Iglehart (Math. Oper. Res. 15 (1990)), avoids estimating : it divides the centred sample mean by a functional of the whole sample path that scales like , so that cancels in the limit. Batch means, the area estimator and other procedures used in simulation software are all instances of this construction.
Cancelling has a price. Glynn and Iglehart show (their Corollary 4.16) that every STS interval has asymptotic expected length at least , the length of the interval that knows , and (4.23) that this bound is the infimum over all admissible . This mission formalizes the next question the paper asks and answers: is the infimum attained? Proposition 4.26 says it is not, and the companion results quantify the residual randomness of the interval length.
is the space of continuous real functions on with the uniform metric and its Borel -algebra; , and . For , is the set of points at which is not continuous. On a probability space , is a standard Brownian motion, viewed as a random element of .
Assumption (2.1). There are finite constants and such that in , where
The class (2.3) consists of the measurable with
With and chosen so that , the interval (2.10) is an asymptotic confidence interval for , of width .
For every there is no such that, for some ,
By the paper's discussion before (4.25), attaining the lower bound of Corollary 4.16 with some requires (4.25); the goal therefore says that the bound is attained by no . The goal is stated in terms of (4.25) and not of the limit (4.24), so it does not depend on the expected-length machinery of Corollary 4.16.
The result closes the expected-length analysis of STS intervals: the bound is the exact infimum over but no single standardization reaches it, so every STS procedure is strictly worse, in expected length, than the interval with known . The companion results explain why: is never degenerate, so converges to a nondegenerate random limit and the interval length fluctuates at order , while intervals built on a consistent estimator of (the regenerative method, Proposition 4.34) fluctuate only at order . This is the quantitative trade-off a practitioner faces when choosing between STS and variance-estimation methods.
The paper's results are proved; none of them is formalized. The mission produces machine-checked versions of a support property of Wiener measure on (every path started at is in the support), which is reusable well beyond simulation, and of the deterministic step that turns such a support property into everywhere-discontinuity of a functional.
The goal's statement is elementary, but its proof needs a quantitative fact about Brownian paths: the law of charges every uniform ball around every path in . The natural first attempt, using that is continuous -almost everywhere and constant almost surely on , fails without this fact, because almost-sure statements say nothing about any particular path . Mathlib provides Brownian finite-dimensional laws and independent increments, but no small-ball or support estimate for Brownian motion in the uniform metric, so (4.27) has to be built from scratch. A second subtlety is that (4.25) is given for one only; the homogeneity (2.3i) is what upgrades it to all scales, and that upgrade is what makes the range of near unbounded.
Proposition 4.32 needs, in addition, the passage from weak convergence of to convergence of second moments under uniform integrability, in the space .
C(unitInterval, ℝ) with its sup norm; is dist. Mathlib has no measurable structure on it at this commit, so the Borel -algebra is declared in the mission's definitions file.IsBrownianReal. "Measurable" in means Borel measurable.The goal is a negation of an existence statement, so it would be trivially true if were empty or if the Brownian hypothesis were unsatisfiable. Neither holds: contains the batch-means functionals of the paper's Example 3.1 (p. 5), and the goal assumes nothing about small balls, (4.27) or continuity of . Those appear only as milestones.
Contributions welcome: the support theorem for Brownian motion in (milestones 1–2), any of the deterministic steps, and the moment-convergence argument of Proposition 4.32.
A retailer with limited shelf or screen space must choose which subset of its products to show each arriving customer. Which assortment earns the most depends on customer preferences, and those are unknown at first: the seller learns them from the purchases it observes. This is dynamic assortment selection, and it is a standard model in online retail and revenue management. Agrawal, Avadhanula, Goyal and Zeevi (Oper. Res. 67(5), 2019; preprint arXiv:1706.03880v2) study it under the multinomial logit (MNL) choice model as the MNL-Bandit problem. They propose an epoch-based upper-confidence-bound policy (Algorithm 1) that needs no prior knowledge of the parameters.
Their worst-case guarantee (Theorem 1) is regret of order . Many instances are easier than the worst case: the best assortment beats every other feasible assortment by a fixed margin. For such well-separated instances, earlier policies obtained logarithmic regret, but only when told a lower bound on that margin:
This mission formalizes the paper's §6.1, which shows that the same parameter-free Algorithm 1 adapts to the separation.
There are products with known revenues and unknown attraction parameters . The no-purchase option has weight . Offered an assortment , a customer buys with probability and buys nothing with probability (2.1). The expected revenue of is
Feasible assortments form a family defined by totally unimodular constraints (2.3). Assumption 4.1 asks that for all and that be closed under taking subsets.
A policy chooses from the past choices. The regret after customers is , where maximizes over (2.6).
Algorithm 1 works in epochs: epoch offers one assortment until a customer buys nothing. It keeps three statistics for each product :
The next epoch offers an assortment maximizing the MNL revenue computed with in place of .
The separation of an instance is the gap between the optimal and the second-best expected revenue among feasible assortments,
The analysis uses the threshold (6.2), with , and . It also uses good epochs: those in which every lies above and within the confidence width of Lemma 4.1.
There are absolute constants such that for every instance satisfying Assumption 4.1 with , every tie-breaking rule and every ,
The constants are not fixed, so the goal survives any improvement of them.
Under the cardinality constraint : .
The result. Theorem 3 shows that one policy is simultaneously near-optimal in the worst case (Theorem 1, , matched by the lower bound of Theorem 2 up to logarithms) and logarithmic on separated instances. It does so without being told , which the separation-based policies of Rusmevichientong et al. and Sauré–Zeevi require. Under a cardinality constraint, Corollary 6.1 matches the order of Sauré–Zeevi's bound.
Formalizing it. The theorem is proved in the paper (Appendix C), and no machine-checked version exists. A formal proof has to make several things precise:
Two printed details need care, and the formal statements fix them: Appendix C defines good epochs with "or" where both inequalities are meant, and Lemma 6.2's proof skips one case.
The counting part looks routine but depends on indexing. The bounds that are good at the end of epoch select the assortment of epoch , so "a good epoch offering a sub-optimal set" pairs two consecutive epochs. A per-product count of under-sampled epochs is then off by one per product, so the printed bound does not follow from the statement of Lemma 6.1 by counting alone.
The probabilistic part is the harder one. The per-epoch purchase counts are geometric with mean only conditionally on adaptively chosen assortments. The confidence statements must hold uniformly over a random number of samples, and the regret must be converted from customers to epochs, whose lengths are random and truncated at . A union bound over all epochs costs a factor , and that factor has to stay within the claimed .
Products are Fin N (0-based), and choices are Option (Fin N) with none the no-purchase option. A policy maps the past choices to an assortment. The law of a length- history is the product of MNL probabilities, so every expectation is a finite sum. Revenue is the published ChoiceCDLP.MNL.mnlObjective v r 1, and is a Finset.sup' over the nonempty family . Algorithm 1 is defined as an explicit state machine and never reads . Ties in its argmax are broken by an arbitrary selector, and every statement quantifies over all selectors.
Standing assumptions carried by every statement:
Disclosed conventions:
The constants are quantified before every other object. A constant depending on , or would make the theorem say only that regret is finite. The policy is pinned to Algorithm 1, not to any optimistic rule.
Contributions are welcome at every level:
Many games have several strict Nash equilibria, and equilibrium analysis alone does not say which one a population will settle on. Harsanyi and Selten (1988) proposed risk dominance as a selection criterion for games: of two strict equilibria, select the one whose basin is "larger" in a precise payoff sense. That criterion is axiomatic. H. Peyton Young's The Evolution of Conventions (Econometrica, 1993) derives a selection from a dynamic model instead: boundedly rational players with finite memory, incomplete information about the past and occasional mistakes. Its Theorem 3 says that, in games, the dynamic selection and risk dominance coincide.
Timeline.
A finite game has players with finite strategy sets and payoffs . Fix a memory and a sample size with . A state is the sequence of the last plays (strategy-tuples), oldest first; a successor of drops the oldest play and appends a new one. In each period each player draws a sample of of the recorded plays and chooses a best reply to it (maximizing total payoff against the sampled plays). The choice probabilities form a best-reply distribution: exactly when is a best reply to some sample of size . This gives adaptive play , display (1).
With mistakes, each player independently experiments with probability and then plays with probability . This gives the perturbed chain of display (2). It has a unique stationary distribution . A state is stochastically stable if . A convention is repetitions of a strict pure Nash equilibrium. With the longest shortest best-reply path to a strict equilibrium, a strict equilibrium is generically stable if its convention is stochastically stable for all sufficiently large and all with .
For a game in normal form, with Row's payoffs and Column's satisfying , , , , set
weakly risk dominates if .
This holds for every game in normal form, for every best-reply distribution and every admissible experimentation.
Theorem 3 gives a dynamic foundation for risk dominance: an equilibrium selection criterion defined from payoffs alone is the long-run outcome of a decentralized learning process with sampling and rare mistakes. It requires no symmetry between the two player roles. Theorem 2 makes stochastic stability computable: a limit of stationary distributions is reduced to a minimum-weight arborescence over recurrent classes. That reduction is what the computation, and later applications of the method to bargaining and contracting, rely on. The equivalence of the -form with the product form of Harsanyi and Selten is elementary algebra and is not a target here.
The results are proved in the paper. To our knowledge none of them has a machine-checked proof. The mission produces formal statements of the model (adaptive play, its perturbation, stochastic stability, resistance and stochastic potential) that are reusable for other stochastic-stability results. Closing the goal also requires formalizing Young's finite version of the Freidlin–Wentzell theorem, the subject of the companion mission The Evolution of Conventions II.
The paper's argument has two hard parts. The first is Theorem 2: identifying the limit of requires the Markov chain tree theorem (the stationary distribution of an irreducible chain as a ratio of sums over spanning in-trees) together with an order-of-magnitude analysis in . The second is the exact resistance . The page constructs a path with that many mistakes (Table 1), but the matching lower bound, that no combination of mistakes by both players does better, is only asserted. It needs an argument about the first period in which some player's best reply switches. A naive count of single-player mistake runs gives only the upper bound. The tie case of (5) also matters: equality makes strategy 2 a best reply, which is why the ceiling and not the floor appears.
Players are a finite type and strategies finite types. A state is Fin m → (∀ i, S i) with position 0 the oldest play. A sample is a set of positions, and a best reply maximizes the summed payoff against the sampled plays. Transition matrices are Matrix H H ℝ. Stochastic stability is a one-sided limit of the stationary distributions of , over the admissible range , . Resistances are natural numbers on successor pairs. Recurrent classes are the essential classes of , and -trees are parent maps on the set of classes that reach the root. "" is the natural-number inequality . In the game, players and strategies are Fin 2, with the paper's written as 0, 1.
Two corrected slips are recorded in the statements. On p. 68 the recurrent classes are "of " for , and on p. 77 "the process defined in (1)" is .
Trivializing formalizations are ruled out. Stochastic stability is defined from stationary distributions, not from resistances, and generic stability is defined from stochastic stability, not from versus . Both definitions quantify over every best-reply distribution and every admissible rather than a fixed sampling law. "Sufficiently large " is an eventual statement with a threshold, not "for some ".
A complete development needs Markov chain stationary distributions on finite spaces, the Markov chain tree theorem, limits of rational functions of , and the combinatorics of sampling in games. The perturbation theory (milestones 1–3) is reusable for any finite stochastic-stability model. Contributions to the tree theorem and to the two resistance computations are particularly welcome.
Related platform work: stochastic fictitious play (StochFictPlay.*, Hofbauer–Sandholm) and calibrated learning to correlated equilibrium (CalibratedCE.*, Foster–Vohra) study other learning dynamics in games. The sibling missions The Evolution of Conventions I (Theorem 1, convergence of adaptive play) and II (Theorem 4, regular perturbations of Markov chains) formalize the results this mission's milestones invoke.
The lost-sales inventory system with a positive lead time is one of the basic models of inventory theory. Demand that cannot be met from stock is lost rather than backlogged, and orders arrive a fixed number of periods after they are placed. Unlike the backlog system, where the inventory position is a sufficient one-dimensional state and a base-stock policy is optimal, the lost-sales system needs the whole pipeline of outstanding orders as its state, and its optimal policy has no simple form. Computing optimal policies by dynamic programming therefore runs into the size of an -dimensional state space.
Paul Zipkin's paper Old and New Methods for Lost-Sales Inventory Systems (Operations Research 56(5), 2008, doi:10.1287/opre.1070.0471) revisits this model, compares classical and new heuristics against optimal policies, and prepares the computation with a state-reduction result. Morton (1969, SIAM Review 11, Equation (83)) showed that under an optimal policy the state remains in a bounded set; Zipkin's §4 extends the argument to every policy in a class that contains the usual heuristics. This mission formalizes that section: the reduced state space , the policy class , and Claim 1, which says that states outside are transient.
Fix the lead time . The state is the -vector : is the stock on hand after this period's delivery, and () is the order that arrives periods later, so is the most recent order. Given the state , an order and a demand , the next state is
Demands in successive periods are independent with a common law on .
The pipeline partial sums are for and ; is the inventory position and the most recent order. A level vector is with . For a level vector ,
and is the set of stationary policies (an order in each state ) with for and for and . The vector base-stock policy with parameter is
equation (5) of the paper with a general in place of Morton's . Under a stationary policy , from an initial state and along a demand path , the state process is , with order and demand . In Lean these are next, v, IsLevelVector, Xs, Zs, vectorBaseStock and traj in the namespace LostSalesOldNew.StateReduction.
For a level vector , a policy , i.i.d. demands with law on and , and any initial state , almost surely
The paper's word is "transient"; the statement above says that every state outside , indeed the whole complement, is visited only finitely often.
A further item records the paper's remark that and are increasing in .
Claim 1 lets the dynamic program be solved on the compact set with policies restricted to , which is what makes the paper's exact computations (lead times up to four, §6) feasible. Since contains the vector base-stock policies and, for large enough, any policy that stops ordering in large states, the claim also says that every plausible policy eventually confines the state to a bounded set.
The result has a short proof in the paper and no machine-checked version. Formalizing it produces a reusable encoding of the lost-sales pipeline with general stationary policies, and makes explicit two points the paper leaves implicit: the probabilistic reading of "transient", and the demand condition under which the process must leave the complement of . Related platform material treats the backlog analogue (VeinottBaseStock.base_stock_level_absorbing, a base-stock level set is absorbing) and lost-sales dynamics under other conventions (CappedBaseStock_Model, from an empty initial state under capped base-stock policies with average cost); those formulations use another state convention and cost criterion and are not imported here.
The invariance step is algebra on partial sums. The content of the claim is the entrance step: outside the policy orders nothing, so the process can only reach through demand draining the stock and the pipeline. That requires the cumulative demand to diverge, which fails pathwise (demand identically zero leaves a state with fixed forever) and holds only almost surely, from independence and . The naive reading of "transient" as invariance alone, or as the pathwise statement with divergent demand assumed, misses this step.
Fin L → ℝ with in the goal; theorems quantify over nonnegative states. The vector is Fin.snoc x z; takes a natural-number index and vanishes at , so .Fin (L+1) → ℝ, antitone with nonnegative last entry. constrains ; constrains for .Measure.infinitePi (fun _ : ℕ => D). The hypothesis is added to the paper's assumptions; without it the claim is false.A complete development needs the partial-sum algebra of the pipeline, the second Borel–Cantelli lemma or the strong law for i.i.d. nonnegative sequences under Measure.infinitePi, and induction along traj. The pipeline encoding is shared with the second mission of this series (lead-time monotonicity). Proofs of any milestone and of the goal are welcome.
The lost-sales inventory system is the inventory model in which demand that cannot be met from stock is lost, not backlogged. It is the natural model for retail and for any setting where a customer who finds the shelf empty buys elsewhere. With a positive order lead time it is also one of the classical hard problems of inventory theory. In the backorder model the state collapses to a single number, the inventory position, and a base-stock policy is optimal. Under lost sales the whole pipeline of outstanding orders matters, the state is an -dimensional vector, and no simple policy is optimal.
Its structure has a long history:
Time is discrete. In each period the order due arrives, a new order is placed, demand occurs, and a holding or penalty cost is charged. The lead time is an integer. The original state records on-hand inventory followed by the orders in transit. Demands are independent with a common law . The costs are linear and stationary: unit procurement cost , unit holding cost , unit lost-sales penalty , and discount factor .
The transformed state is the vector of partial sums , , with the convention . It ranges over the cone
The transformed order is . With the all-ones vector, the state moves to
The one-period cost is on , where is the on-hand stock, and . With periods to go, the optimal cost functions are
A function is submodular on a set if for all , with the componentwise maximum and minimum. A function is L♮-convex if is submodular on . A function on is L♮-convex if is submodular in over , .
For every number of periods to go ,
The statement fixes no constants. It holds for every lead time, every demand law in the class below, and every cost vector.
The result. L♮-convexity of implies that is submodular and convex in the transformed state. L♮-convexity of yields, through Lemma 3 and Corollary 5 of the paper, that the optimal order is nonincreasing in and changes by at most when every component of increases by . These are exactly the Karlin–Scarf and Morton sensitivity results, obtained without derivatives. The same property underlies the paper's later results: the bounds on the optimal policy (§4), the monotonicity of cost in demand variability (§5), and the extensions to capacity limits, correlated demand and stochastic lead times (§6).
Formalizing it. The theorem is proved in the paper; nothing here is open mathematically. To our knowledge no machine-checked proof of L♮-convexity of an inventory value function exists. The mission produces three things:
The obvious argument works with ordinary convexity and submodularity in the original state . It stalls: the lost-sales transition is not linear, and the order enters only the last pipeline component, so the comparative statics Karlin and Scarf and Morton obtained by differentiation do not follow from convexity in . The paper's structure appears only in the partial sums . Submodularity alone, moreover, is not preserved by the step that minimizes over the order. The shift structure of L♮-convexity is what survives the minimization over (Lemma 2). Proving plain submodularity of on therefore does not close the induction.
A second difficulty is the end-of-period program. Writing the next state as the minimum of a program over a constraint set that is a sublattice requires checking the order-theoretic structure of the set together with the sign pattern of every term. The equality between the program's value and the recursion's one-period cost (milestone 3) is a property of the model's own value function, not of an arbitrary L♮-convex continuation.
A third difficulty is measure-theoretic. Preservation under expectation needs integrability and measurability of , and these come from the model rather than from the definitions.
Fin L → ℝ, indexed as in the paper. A helper returns for and at . A function is encoded on Fin (L+1) → ℝ with last. The objective of (4) is encoded on Fin (L+2) → ℝ with coordinates . The order is componentwise.DiscreteConvex.LConvexFunctions.*) works on with values in , a different domain and definition, and is not reused.Queueing models often represent work arriving to and leaving a server by a real-valued input path. The resulting workload cannot fall below a barrier. Functional limit theorems describe what happens to such paths under scaling, but a limit for the input path is useful only when it can be carried through the workload transformation. Ward Whitt’s 1980 paper studies several path transformations that occur in stochastic-process limits and states conditions under which their limits can be computed in Skorohod topologies. Section 6 treats the running supremum and a reflecting barrier, including paths with a linear drift that changes with the scaling index. This mission formalizes the three-regime reflection result, Theorem 6.4, and the source results on its dependency path. Whitt (1980)
The result is already proved in the paper. Its formal Lean statement remains an open proof target here. The mission is therefore concerned with formalizing the known theorem, including its exact jump conditions and convergence modes, rather than proposing a new queueing claim. Whitt (1980), pp. 80–81
A càdlàg path on a real interval is right-continuous and has a limit from the left wherever approaches a time from the left. The collection of such real-valued paths is . For a compact interval , the distance between and allows an increasing homeomorphism of time and measures the larger of its distance from the identity and the uniform distance between and . On a general interval, convergence is specified by restrictions to compact subintervals whose endpoints are continuity points of the limit or endpoints of . The paper uses complete separable metric spaces for general path-space results; Section 6 specializes to real-valued paths and intervals with as a closed left endpoint. Whitt (1980), pp. 70, 80
For and , define the running supremum and running infimum . The reflecting-barrier map is . This is the paper’s definition: it subtracts the full running infimum. The identity path is , and denotes the zero path. A path has no positive jumps if for each in ; no negative jumps reverses that inequality. Whitt (1980), pp. 80–81
The goal is Theorem 6.4. Suppose in and . Its three conclusions are
Here means uniform convergence on every compact subinterval. The goal keeps all three drift regimes together, as the printed theorem does. Its milestones are the finite-partition fact cited from Billingsley, the interval-splitting Lemma 2.2, continuity of addition at limits without shared discontinuities in Theorem 4.1, the running-supremum inequality in Theorem 6.1, the three-regime supremum theorem 6.2, and the paper’s explicit claim that is -continuous. Whitt (1980), pp. 71, 79–81
The theorem specifies which output path appears after reflection as the linear centering changes. Finite drift leaves a reflected limit with drift included; large positive drift leaves the centered input limit; large negative drift drives the reflected path uniformly to zero when upward jumps of the limit are excluded. The distinction between and the stronger compact-uniform mode in the last case is part of the result. These statements make the paper’s barrier transformation usable when an input-process limit is already known. Whitt (1980), Theorem 6.4
A completed formal development would establish reusable path-space components: a precise convergence interface for real intervals, a theorem about addition with disjoint discontinuities, and continuity properties of running extrema and reflection. The present Lean items state these results and compile with proof placeholders. No machine-checked proof of these mission theorems is claimed here. The milestone list follows the claims Whitt states or cites, so later proofs can be attached to the same mathematical targets. Whitt (1980), §§2, 4, 6
A uniform estimate alone does not establish a limit: separate paths may converge using different changes of time, and addition can fail when the limiting paths jump together. Whitt’s Theorem 4.1 gives continuity precisely at pairs with disjoint discontinuity sets. In the reflection theorem, a linearly growing drift also changes which extrema matter, and the sign of a jump decides whether the large-drift conclusion can hold. The negative-drift conclusion asks for compact-uniform convergence, which is stronger than merely retaining convergence. These are real constraints on the statement; dropping a jump condition or replacing by changes the theorem. Whitt (1980), pp. 78–81
Paths are total functions , but only their values on the stated interval count. The Lean definitions require càdlàg membership of both prelimit and limit paths in each convergence claim. A time change on is strictly increasing, continuous, and onto; this represents the paper’s increasing homeomorphism. Uniform and distances take values in the extended nonnegative reals, so an unbounded supremum cannot silently become zero. Continuity points use continuity within , and the discontinuity set likewise contains only points of . Sequential convergence is used because the paper’s spaces are metrizable. These choices encode the paper’s path-space conventions rather than imposing conditions on values outside . Whitt (1980), §§2, 4, 6
The compact form of Theorem 6.1 uses metric (2.1); the noncompact metric (2.2) is outside this mission’s definition layer. Theorem 4.1 retains the paper’s complete separable metric-space setting and metric compatibility of addition. Its measurability clause is omitted: this mission does not construct the Borel measurable space of , and a product measurable structure on all total functions would express a different claim. The source’s is used on both prelimit and limit paths; it is not replaced by a clipped running infimum. Whitt (1980), pp. 70, 78–81
The definition layer, the addition theorem, the running-extremum results, and the barrier continuity statement are welcome proof targets. The theorem’s centered-path hypothesis remains a genuine convergence assertion, and the jump conditions apply to the limit path only. A vacuous convergence predicate or an independently assumed conclusion would not represent this mission’s goal.
A processor can save energy by running slowly when work is light, but a deadline may force it to run faster. Yao, Demers, and Shenker formulated this tradeoff as an offline and online scheduling problem for a variable-speed processor in their 1995 FOCS paper. Their Average Rate Heuristic (AVR) uses only each job's arrival, deadline, and required work to set speed. This mission formalizes their quadratic-power analysis: AVR's worst-case energy is at least four and at most eight times the minimum possible energy. The authors prove these bounds in Theorem 2, rather than an exact value.
The question matters when an online scheduler must choose speed before seeing later jobs. Deadline feasibility alone does not measure energy: processing the same number of cycles at twice the speed for half as long can cost more when power grows superlinearly. The paper's model isolates that dependence in a power function , so the competitive guarantee measures the energy price of AVR's speed choices. The initial motivation, model, and heuristic are in §§1–4 of the paper.
Fix a nondegenerate time window . A finite job instance assigns each job an arrival time , deadline , and nonnegative required work in CPU cycles. Every job window lies inside . A schedule has nonnegative processor speed and selects at most one job at each time. Speed and job selection are constant between finitely many breakpoints. The schedule is feasible if each job receives its full work inside its own window:
For a power function , its energy is . An optimal schedule minimizes this quantity among feasible schedules. These definitions follow §2, p. 375. The intensity of an interval is the total work of jobs whose full windows it contains, divided by . An interval with maximum intensity is critical; Theorem 1 identifies the processor speed on that interval in an optimal schedule §3, p. 375.
Each job's density is , extended as a step function equal to on and zero elsewhere. AVR runs at speed and chooses the earliest-deadline available job. For quadratic power, its energy is
The competitive ratio is the least upper bound of over instances, where is the least feasible energy §4, p. 376, Eq. (2).
The goal is the paper's Theorem 2, p. 381:
The upper bound compares AVR with every feasible schedule. The lower bound says that every constant strictly below four is exceeded by the AVR-to-feasible-energy ratio on some instance. This formulation does not claim that one finite instance attains four.
The milestone path follows the paper: Theorem 1 characterizes optimal speed; Lemma 5.1 reduces to jobs of type A or B; Eq. (5) splits their costs; Lemma 5.2 and Eq. (7) control the A contribution; Lemmas 5.3–5.6 reduce the analysis to canonical instances; Lemma 5.8 supplies a matrix bound; Lemma 5.7 gives and ; Example 2 approaches the lower constant. These statements and their order come from §5, pp. 378–381. The paper also states a higher-power result, Theorem 3, for real :
That result is a companion item. The extended abstract leaves its full proof to a longer paper §6, pp. 381–382.
The upper bound guarantees that AVR's energy is controlled by a fixed multiple of the offline optimum for every finite job set, even though AVR sets speed from individual job densities. The lower family rules out a guarantee below four for this heuristic. Together they delimit the performance of AVR under quadratic power; they do not give its exact worst-case ratio. The A/B reductions and the tree-induced matrix estimate are useful mathematical interfaces for later analyses of interval-structured schedules.
The paper proves Theorem 2 in the mathematical sense. This mission supplies machine-checkable statements and definitions, with proofs left open for solvers. Closing it requires formal proofs of the reduction steps, the matrix estimate, and the limiting example, plus an explicit connection from the optimal-schedule analysis to comparison with every feasible schedule. No completed Lean proof is claimed here.
The simple calculation exposes overlap between job windows but does not say how that overlap compares with an optimal schedule. An optimal schedule may run jobs in a different order and may preempt them. The paper therefore changes the instance while preserving the optimal speed profile: it first separates cumulative execution into two types, then reduces to single execution intervals and specially aligned, nested windows. The matrix inequality controls the resulting expression. A pointwise comparison of AVR speed with optimal speed cannot replace these reductions, because an optimal schedule can concentrate work on critical intervals while AVR spreads each job's density across its entire window §5, pp. 377–381.
Jobs use Fin n, allowing the empty instance. The instance requires , , containment in the window, and . A schedule uses real-valued speed and an optional job label; none denotes no assigned job. Its piecewise-constant requirement is witnessed by finitely many increasing breakpoints. Values at breakpoints are unrestricted by the piecewise-constant clauses, and speed comparisons in the theorems are almost-everywhere statements. Job windows are closed, as printed; endpoints do not affect the integrals. A schedule may have positive speed while no job is assigned, since the source does not equate idleness with zero speed.
Every energy expression is a real interval integral. The schedule conditions ensure the integrands in theorem hypotheses are piecewise constant away from finitely many points. Density denominators are positive. An execution-speed quotient for a zero-work job can have zero denominator, in which case Lean returns zero; such a job contributes no executed work. The goal uses quantified comparisons with feasible schedules rather than a real infimum, and Lemma 5.6 uses all upper bounds on a nonempty canonical family rather than a real supremum. The lower bounds quantify over every smaller constant, avoiding a false attainment claim. These choices guard against default values for empty or unbounded extrema.
Theorem 1's printed convexity hypothesis is strengthened to strict convexity and nondecreasing power on nonnegative speeds: its stated speed uniqueness fails for a linear power function, and a decreasing power function rewards idle speed. This repair is explicit in that item's description. Existence of a quadratic optimum is included as a milestone from the algorithm of §3, although it is not a separately numbered theorem. Example 2 includes the variable exponent , the limiting ratios at and , and an eventual upper bound of four across the family. The A-job order resolves exact ties by index. For canonical and tree-induced nesting, intervals that meet only at an endpoint count as disjoint; this admits the paper's displayed four-interval matrix.
The development needs Mathlib's real interval integrals, finite sums, measures of intervals, matrix eigenvalues, and real-power limits. The finite schedule model, canonical-instance data, and tree-induced matrix interface can be reused beyond this particular ratio bound. Contributions may establish these interfaces' elementary properties, the paper's milestone theorems, or independent proofs of the goal, provided they preserve the stated job and schedule classes.
Functional limit theorems describe the behavior of entire time-indexed paths under scaling. In queueing and other stochastic models, a path of departures, workload, or accumulated input may be related to another path by reversing a finite observation window. To carry a limit theorem through that change of viewpoint, one needs to know how reversal acts on the topology of the path space. Ward Whitt's 1980 paper studies composition, reflection, first passage, and time reversal as maps that transfer functional limit theorems to derived processes (Whitt 1980).
The time-reversal result is a precise metric statement. Ordinary reversal preserves the Skorohod distance exactly. A version shifted to begin at the group identity satisfies a bound with constant two. These facts give continuity and, when the random paths satisfy the hypotheses, make reversal available to the continuous mapping theorem. Whitt's introduction explains how deterministic path continuity connects to stochastic-process limits (Whitt 1980, pp. 67–69).
Let be a complete separable metric group, written additively, with identity and metric . The metric is translation invariant: moving both points by the same group element leaves their distance unchanged. Let contain the càdlàg paths , meaning paths that are right continuous and possess left limits. Section 8 additionally requires , so the terminal value agrees with the value approached from earlier times. Let . These are the spaces Whitt fixes for time reversal (Whitt 1980, p. 83).
The uniform distance is . A time change is an increasing homeomorphism of onto itself; is the identity time change. The distance used in the paper is
Two paths may be close when their values can be matched after a small distortion of time. This is the paper's equation (2.1), rather than an unspecified equivalent metric (Whitt 1980, p. 70).
The reverse-time map reads the left limit at the reflected time:
The left limit is essential: the direct value places jumps on the wrong side and generally does not give a right-continuous reverse path. The terminal convention gives , so . Whitt also uses the reflected time change in the proof (Whitt 1980, pp. 83–84).
The goal is Whitt's Theorem 8.1. For every ,
The second inequality also applies when both paths lie in , since . The constant is the paper's printed constant, not a parameter to optimize in this mission (Whitt 1980, Theorem 8.1, p. 83).
The milestones record four claims from the theorem's proof: reversal preserves its path spaces and has inverse behavior on its natural domains; reflected time changes stay in ; reversal obeys exact and bounded uniform-distance relations; and reversal interacts with time changes through . Their descriptions reproduce the printed proof sentences. The proof calls the time-change cost a “minimum” once, although equation (2.1) and the displayed calculation use a maximum. The formal target follows equation (2.1) (Whitt 1980, pp. 70, 84).
An isometry preserves every distance, so ordinary reversal preserves convergent and Cauchy sequences in this metric. The bound for makes shifted reversal Lipschitz and therefore continuous. A functional limit theorem for input paths can then be translated into one for the corresponding reversed paths whenever the path-space hypotheses hold. The result is already proved in Whitt's paper; the open work here is a machine-checked development of its definitions, supporting claims, and metric theorem.
Formalizing the result also creates reusable interfaces for endpoint-constrained càdlàg paths, left-limit reversal, uniform path distance, and reflected time changes. Those interfaces may support later statements about reversed stochastic models. This mission does not assert weak convergence of probability laws or Borel measurability; those would require a separate measurable-space development for .
The immediate idea does not preserve càdlàg paths at jumps: a right-continuous jump becomes left-continuous. The correction uses left limits, but endpoint behavior then matters. Without , the shifted reverse path need not start at the identity. The assertion also concerns an infimum over all allowed time changes, so a uniform-distance statement alone does not establish the theorem. These are the points at which reflection of the time axis becomes a claim about the precise path-space topology (Whitt 1980, pp. 83–84).
Lean represents paths as total functions ; all path conditions, metrics, and equality claims read only . Càdlàg membership requires right continuity and left limits within the interval, with included in . Completeness and separability are explicit because the paper calls a complete separable metric space. The additive metric group is represented by an additive commutative group with an explicit translation-invariance hypothesis. This chooses the commutative reading exemplified by ; the paper uses additive notation but does not separately state commutativity.
The paper's is encoded by strict increase, continuity, and surjectivity on , which characterize increasing homeomorphisms there. The paper's is equation (2.1) on both sides of the goal. Lean uses extended nonnegative distances for and , avoiding the default value a real supremum can assign to an empty or unbounded set. The claims do not become trivial by dropping membership: it is an explicit hypothesis, and the zero path over satisfies it. A local, sorry-free check confirms that instance. Two easier statements are excluded on purpose: the goal is stated for the distance , not the uniform distance , and reads the left limit , not the value .
The proof's first sentence says the maps are one-to-one and onto. The map forgets an additive offset and is not injective on all of ; the formal milestone expresses involution for on and for the restriction of to . One identity printed for with also holds for every ; the formal milestone uses that broader domain and says so in its item description. Contributions are welcome for the left-limit and time-change infrastructure as well as the four listed statements and the goal.
An airline sells the seats of one flight leg at several fares. Cheap fares are usually booked well before departure and expensive ones close to it, so every early request poses the same question: is the certain revenue of selling a seat now worth more than the chance of selling it later at a higher fare? The policy that answers it is seat inventory control, a core problem of airline revenue management.
For two fare classes the answer is Littlewood's rule (1972): accept a low-fare request as long as the low fare is at least the high fare times the probability that high-fare demand would fill the remaining seats. Belobaba (1987) extended it heuristically to several classes through expected marginal seat revenue (EMSR) protection levels, which are not optimal in general. Wollmer (Operations Research 40(1), 1992) solved the multi-class problem exactly under the assumption that the classes book in order of increasing fare: he showed that an optimal policy is described by one critical value per fare class, computed by a short recursion, and accepts a request precisely when the number of empty seats exceeds the critical value of its class. Brumelle and McGill (Operations Research 41(1), 1993) and later work on nested booking limits reached optimality of static protection levels by other routes.
There are fare classes, numbered from the highest fare to the lowest, with fares
Class has a random demand , the number of its future booking requests, with probabilities , , . Seats form one pool, and denotes the number of empty seats. Lower classes book first: all requests of class arrive before those of classes . The paper assumes , so that a class 2 request is refused when one seat remains.
The optimal value is the expected revenue under an optimal policy when seats are empty and only classes may still book. It satisfies and
where is the number of class- requests accepted. The marginal seat value is for , and the critical values are
The critical-value rule for class rejects a class- request when and accepts it when ; it accepts of the class's requests.
For every class , is nonincreasing in . For every class , the critical value exists, for , the critical-value rule attains the maximum in the recursion for (and accepting more requests is strictly worse), and for every
The theorem reduces a dynamic program over all booking policies to one integer per fare class. The critical values are computed class by class from (2b) and (6), in a number of operations polynomial in the number of seats and classes, and the resulting policy is a nested booking limit that reservation systems can implement directly. The abstract states two further properties derived from it: the critical value decreases with the fare and is zero for the highest class.
The result is proved in the paper; it has no machine-checked proof. A complete formalization would give a verified account of the multi-class seat allocation problem with sequential booking, including the existence of the critical values, which the paper presupposes. The intermediate statements (the concavity-type property of and the closed form (6)) are reusable for nested-booking-limit results in related models.
The induction of the paper is short, but it relies on one property: must be nonincreasing for the threshold rule to be optimal for class , and the threshold rule must be optimal for to inherit the property. These two facts have to be carried together through the induction. The step at the threshold itself () behaves differently from the rest: there the marginal value drops strictly, and the argument above the threshold needs the maximality in (2b), not monotonicity alone. The existence of is not argued on the page: it requires bounding the marginal seat value away from for large without assuming that demands have finite mean. The proofs of Lemma 1 and Theorem 1 also contain index slips ( printed for ) that a formal proof must not reproduce.
All statements live in the namespace LowerFareFirst.Critical and rest on one definition module, LowerFareFirst.Critical.Model. Classes are natural numbers starting at ; fares are a sequence and demands a sequence of measurable maps on a probability space , of which only the entries are constrained. Probabilities are μ.real of events.
Committed conventions:
A complete development needs elementary facts about expectations of functions of an integer-valued random variable and finite maximization; nothing beyond Mathlib's measure theory. Proofs of any milestone are welcome, as are proofs of the abstract's remarks ( nonincreasing in the fare) as separate theorems.
A finite Markov decision process is usually solved under one of two criteria: the expected total discounted reward, for a fixed interest rate, or the long-run average reward. Neither is satisfactory when the interest rate is small and not known precisely. Blackwell (Blackwell 1962) showed that some stationary policy is optimal for every discount factor close enough to one, and that the average-reward criterion cannot tell apart policies with the same gain but very different transient rewards. Veinott's 1969 paper interpolates between these two: it introduces a hierarchy of -discount optimality criteria, indexed by , each more selective than the previous, and characterizes the stationary policies that meet each level through the Laurent expansion of the discounted return in the interest rate.
Timeline. Blackwell (1962) introduced the expansion of the discounted return near to first order and the criteria now called and discount optimality. Veinott (1966) gave a policy improvement method for the bias () criterion. Miller and Veinott (1969) gave the full Laurent expansion and a policy improvement algorithm for Blackwell optimality in the stochastic case. The present paper (1969) extends this to substochastic transition matrices and to negative interest rates in the transient case, defines the criteria, and proves Theorem 4, the subject of this mission.
There are finitely many states (the paper's ); in each state a finite nonempty action set . Action in state earns and leads to state with weight , where (the remaining mass is the probability of stopping). A decision rule picks one action per state; and are its reward vector and substochastic transition matrix, . A policy is a sequence of decision rules, is a stationary policy, and .
For an interest rate and , the discounted return is
For a substochastic , is the Cesàro limit of its powers and its deviation matrix.
A policy is discount optimal if, componentwise,
is the set of with discount optimal, and . The sign (interest rate approaching zero from below) is considered only in the transient case, where converges for every .
The Laurent coefficients of are and , ; with and , otherwise, the test quantities are
is the matrix with columns , and , where means that the first nonzero entry of every row of is positive and .
For and :
The two halves bracket between two finitely checkable conditions.
In the order the proof uses them: the Cesàro limit and (15); Lemma 5 (the reduced resolvent); Theorem 2 (the Laurent expansion ); Lemma 7 ( nonnegative, positive diagonal, nonsingular for small ); Theorem 3 (the expansion of ); (30)–(31) (the comparison identity); Lemma 8 (the expansion of the test quantity); Lemma 9 (the coefficient identity); the nonemptiness of ; the characterization ; Theorem 5 (lexicographic improvement).
Theorem 4 turns a criterion stated through limits over all, possibly non-stationary, policies into a finite test on one-step switches. It is what lets the policy improvement method of Miller and Veinott stop early when only an discount optimal policy is sought, rather than an (Blackwell) optimal one, and it recovers Blackwell's algorithm for and Veinott's 1966 algorithm for as the cases . The -discount hierarchy is the standard framework for sensitive optimality in Markov decision processes and underlies the average-overtaking and bias criteria used in later work.
The results are proved in the paper (Theorem 3 and Lemma 8 by reference to Miller–Veinott). None of them is formalized: the platform has the Cesàro limit matrix and the deviation matrix as definitions (from Blackwell 1962), and an open statement of their basic properties for stochastic matrices only. This mission adds the substochastic matrix theory of §3, the Laurent expansion of discounted returns with Veinott's normalization, and the lexicographic characterization of discount optimality.
The definition of compares with every policy, and the comparison is a liminf of a scaled difference of infinite series. The obvious route, comparing Laurent coefficients, applies only to stationary policies, whose returns have Laurent expansions; reducing the comparison with arbitrary policies to stationary ones requires the existence of an discount optimal stationary policy, which is a separate existence theorem. The second difficulty is that may be singular or zero and the chain may have several recurrent classes: Lemma 7 is what replaces an analysis of the chain structure in the inductive step of the proof.
Lean 4 with Mathlib, namespace VeinottSensitiveDP.Sensitive. States form a nonempty Fintype; each state has its own finite nonempty action type A s; policies are sequences ℕ → F with π 0 the paper's . All quantities are real. and are the published limitMatrix and deviationMatrix; their properties for substochastic matrices are milestones, not assumptions. is a tsum with Veinott's extra factor ; every theorem about it carries the hypotheses under which the series converges. The spectral radius is that of the complexified matrix. The sign is a real parameter , and statements for assume the transient case. The liminf in (27) is encoded as "for every , eventually ", which is the extended-real liminf. Matrices with columns are functions of an integer column index read on .
A trivializing formalization would define by comparison with stationary policies only, or directly as the lexicographic maximizers of ; here is defined by (27) against all policies, and the lexicographic characterization is a milestone.
Contributions welcome: proofs of the matrix results of §3 (reusable for any work on deviation matrices and Laurent expansions of Markov chains), of the Laurent expansions, and of the existence of discount optimal stationary policies.
Many optimization models combine a smooth loss with a convex penalty or constraint. The penalty can be nonsmooth: an absolute-value penalty encourages sparse solutions, while an indicator function enforces a feasible set. A coordinate gradient descent (CGD) method updates selected coordinates by minimizing a quadratic model and then applies a line search. Tseng and Yun studied this method for an extended-valued convex penalty, including penalties that separate by blocks of coordinates. Their global convergence result addresses a basic question for such an iteration: if its iterates have an accumulation point, must that point satisfy the first-order stationarity condition? The result and examples appear in Tseng and Yun (2009).
Coordinate updates are appealing when changing a small block is cheaper than changing the whole vector. Their convergence is delicate when the penalty is nonsmooth: a direction can be useful on one block without revealing whether the full point is stationary. The paper's Theorem 1(e) establishes a guarantee for a generalized Gauss–Seidel selection rule and a block-separable penalty. The authors note that this rules out cycling on Powell's coordinate-minimization example under their stated conditions Tseng and Yun (2009), p. 404.
Let , , and let be proper, convex and lower semicontinuous. Its effective domain contains precisely the points where is finite. Let be continuously differentiable on an open set containing . The objective is , with value outside . No convexity of is assumed.
At iteration , choose a nonempty set of coordinates and a positive-definite symmetric matrix . The search direction minimizes
The next iterate is . The Armijo rule tests the geometric sequence and takes its largest accepted member, using the paper's decrease quantity . Its parameters satisfy , , and . The accepted step obeys .
The generalized Gauss–Seidel rule means that some fixed number of consecutive coordinate sets covers every coordinate, starting at every iteration. The penalty is block-separable with respect to when it is the sum of a proper closed convex function of the selected coordinates and another of their complement. A point is stationary when it lies in and the one-sided directional derivative is nonnegative for every direction .
The goal is Theorem 1(e) Tseng and Yun (2009), p. 399. Under the CGD and Armijo rules, Assumption 1's uniform matrix bounds, a positive lower bound on the initial trial steps, block separability for each chosen coordinate set, and a finite upper bound on the accepted steps,
The mission milestones state the paper's Lemma 1, its Armijo existence claim after equation (10), Lemmas 2 and 3, and Theorem 1(a) and (b). They connect the direction subproblem, descent, stationarity and subsequence behavior to the goal. The theorem asserts stationarity of every cluster point; it does not assert that a cluster point exists or that the full sequence converges.
The result supplies a global first-order guarantee for a block update method even when the smooth part is nonconvex. It applies to extended-valued convex penalties, so the same statement covers both nonsmooth regularization and constraints represented by indicator functions. The bounded-window coverage condition allows varying coordinate sets rather than a fixed cyclic schedule Tseng and Yun (2009), Theorem 1(e).
The paper proves the theorem. This mission asks for a machine-checked Lean proof of that known claim and its selected supporting results. The reusable output includes a precise interface for an extended-valued penalty, the exact quadratic coordinate subproblem, Armijo backtracking with first accepted exponent, and the distinction between a convergent subsequence and a cluster point. The current draft statements compile with proof placeholders; they are proof obligations, not completed machine-checked results.
The descent bound alone controls decrease in objective value; it does not directly show that every coordinate has a vanishing stationarity residual. The coordinate set may vary at each iteration, and the penalty need only separate with respect to the current block. A cluster point may be reached along a subsequence that samples only one of those blocks. The argument therefore has to connect behavior along a convergent subsequence to nearby iterations within a full coverage window. The nonsmooth penalty also prevents replacing directional stationarity by a statement solely about an ordinary gradient.
Vectors use EuclideanSpace ℝ (Fin n) and its Euclidean norm; Fin n starts at zero, whereas the paper numbers coordinates from one. A penalty is represented by its effective domain and finite values on D+\inftyDd_H(x;\mathcal J)xDH$ positive definite. A CGD run records the chosen minimizers, so it does not rely on any unspecified value of that choice outside its valid inputs.
The Armijo predicate records the first successful geometric trial, including rejection of all earlier trials. The matrix bounds in Assumption 1 are quadratic-form bounds. Lemma 3 represents eigenvalue extremes by Rayleigh quotients on the selected coordinates; its generalized spectrum is that of the pair of principal submatrices. These extrema are used only with a nonempty block and positive-definite matrices. The paper's is represented by a remainder whose quotient by tends to zero from the right. In Lemma 1 the line segment remains in . A convergent subsequence is indexed by a strictly increasing map; a cluster point is represented separately by MapClusterPt.
No convergence of the entire iterate sequence is assumed. Stationarity requires the nonnegative directional derivative in every direction, not only the coordinates selected at one step. A valid development needs convex analysis of the subproblem, estimates for positive-definite quadratic forms, properties of lower semicontinuity and directional derivatives, and finite-dimensional subsequence arguments. Contributions proving those reusable facts and the named milestones are within scope.
Negative dynamic programming is the study of infinite-horizon sequential decision problems in which every one-stage reward is non-positive and nothing is discounted. Equivalently, a non-negative cost accumulates forever and the controller minimizes its expected total. Stochastic shortest-path problems, optimal stopping with a cost per step, and inventory or replacement models without discounting all have this form. The total cost of a policy can be infinite, and none of the contraction arguments of discounted dynamic programming apply.
Blackwell settled the discounted case on Borel state and action spaces (Blackwell 1965). There the optimal return is Borel measurable and is the unique bounded solution of the optimality equation. Strauch's paper (Strauch 1966) treats the negative case on the same Borel model. One of its main results is that the optimal return still satisfies the optimality equation, even though it need not be Borel measurable.
Timeline. Blackwell (1965): discounted case, Borel spaces. Blackwell (1967, Positive dynamic programming): positive bounded case. Strauch (1966): negative case on Borel spaces. The optimal return is absolutely measurable, -optimal Markov policies exist, and the optimality equation holds. Bertsekas and Shreve (1978, Stochastic Optimal Control: The Discrete-Time Case) later recast the theory with universally measurable policies, a lower semianalytic optimal cost, and Bellman's equation under (P), (N) and (D).
The states and actions are non-empty Borel sets. A law of motion is a probability kernel from to . The return is a Borel function with whose expectation is finite for every . A policy draws the th action from a kernel that may depend on the whole history. A Markov policy uses measurable maps , and a stationary policy uses one map at every stage. The expected return from the initial state is
and the optimal return is
the supremum over all policies. Write for the non-positive, extended real-valued Borel functions on . For and an action ,
denotes the same operator for a measurable rule in place of , and for a Markov policy . A policy is -optimal, for a probability on , if . The Lean development uses the same names: Problem, I, In, vstar, T, Ta, U, IsPEOptimal, Conserves.
The equation involves no constants and no regularity hypotheses on .
Optional extras: Corollary 6.1 and Theorems 6.3, 6.4, 6.5 and 8.4 (bounds and characterizations for Markov policies).
The result. The optimality equation is the entry point to every structural statement about optimal policies in the negative case. With it, a stationary policy whose rule attains the supremum in can be tested for optimality. Value iteration and policy improvement can be compared with . The gap between the negative case and the discounted and positive cases can be located precisely: in the negative case satisfies the equation, but it need not be its unique or extremal solution. Along the way the paper proves that is absolutely measurable and that nearly optimal Markov policies exist for every initial distribution. These two facts are used repeatedly in later Borel-space dynamic programming.
Formalizing it. The results are proved; none is machine-checked. A formal development would contain the first Lean treatment of a total-reward Markov decision process on Borel spaces with possibly infinite returns. It would include the policy-dependent law of the future via Ionescu-Tulcea, the measurability of the optimal return over all randomized history-dependent policies, and the Bellman equation for a non-measurable value function. Bertsekas–Shreve's version of the optimality equation (universally measurable policies) appears on the platform as a separate open statement. It concerns a different policy class and is not the statement posed here.
Two steps of the obvious argument fail. First, the classical proof of the optimality equation picks, at each next state , a policy that is -optimal from and concatenates. Without measurable selection this concatenation is not a policy. The set of where a given policy is -optimal need not be Borel, and itself need not be Borel measurable, so even needs justification. Second, the contraction argument of the discounted case is unavailable. does not contract, it conserves along with , and value iteration from can converge to a function strictly above . The paper's Example 6.1 shows that the limit of , the best return of generated Markov policies, and the best stationary return can all differ. Any argument has to work with policies that are only nearly optimal, and only outside sets of measure zero that depend on the initial distribution.
DiscountedDP.Stationary.Plan): randomized and history-dependent, one Markov kernel per decision, with decisions numbered from (Lean's π.κ n is the paper's ). Markov policies are MarkovPlan; "-generated" and are the published IsGenerated and IsGeneratedPlan.EReal and are computed as minus a lower Lebesgue integral (lintegral) of the non-negative loss. A Bochner integral is never used for a return: it would map to and make the goal false or vacuous.lintegral of a possibly non-measurable function, which equals the completion integral because is absolutely measurable (Theorem 7.1).IsNegM u. Theorem 5.2(b) assumes . " conserves " includes . Lemma 6.2 asserts that the limit defining exists. Theorem 6.2 states everywhere and where (the printed fails where the supremum is ). -optimality is "-almost everywhere". Absolute measurability is NullMeasurable for every probability measure. carries the Giry σ-field. The extra Theorem 8.4 reads the printed "" as "" (the strict reading is false).futureLaw), and the measurability lemmas for integrals against random measures. Contributions of measurable-selection and analytic-set results (projections of Borel sets are universally measurable; von Neumann selection) are welcome and needed.A binary classifier is learned from a sample of a distribution on , and its quality is measured by its excess classification risk over the Bayes classifier. Without assumptions on no learning method converges at a uniform rate, so every rate theorem rests on a condition that describes how hard is. Two such conditions are standard: Tsybakov's noise condition (Tsybakov 2004), which bounds the mass of the region where the label is close to a fair coin flip, and smoothness of the regression function .
Steinwart and Scovel (arXiv:0708.1838v1, the reprint of Ann. Statist. 35 (2007) 575–607) analyse support vector machines with Gaussian RBF kernels. Their rates rest on a new condition, the geometric noise exponent, which measures how much of the weighted measure lies close to the decision boundary. It is tailored to the approximation properties of the Gaussian kernel and is less familiar than the classical conditions. Theorem 2.6 of the paper connects it to them: an envelope condition on near the decision boundary, together with a Tsybakov exponent, yields an explicit geometric noise exponent. This mission formalizes that theorem.
Let be compact and let be a distribution on with marginal and regression function . The classes of are , and , all intersected with . The distance to the decision boundary is
with the Euclidean distance of to (equation (7), p. 7).
In Lean these are TsybakovNoise, GeometricNoise and Envelope, built on Tau, in the namespace FastRatesSVM.GeomNoise.
If has an envelope of order and Tsybakov noise exponent , then
Both clauses are stated, as one conjunction.
Theorem 2.6 makes the paper's learning rates usable under familiar assumptions. The main rate theorem of the paper (Theorem 2.8) is stated in terms of the geometric noise exponent; through Theorem 2.6 it becomes a rate in terms of a Tsybakov exponent and the order of an envelope, which is a Hölder-type behaviour of at the decision boundary. Example: with , , uniform and , the distribution has envelope order and Tsybakov exponent , hence geometric noise exponent .
The result is proved in the paper. As far as known, none of it is machine-checked: none of these noise conditions has a Lean formalization, on Prove2Me or in Mathlib. The mission produces the definitions themselves (the class decomposition, and the three noise conditions), which any later formalization of margin-based classification rates can import, and a formal proof of the implication. A companion mission of the same series formalizes the paper's rate theorem, which takes the geometric noise exponent as its hypothesis.
The case is elementary once the right splitting level is chosen: the expectation is split at a level of , and is then tuned to . Tuning it requires the asymptotics of the solution of a transcendental equation. This yields every exponent below the critical value , but not the critical value itself: a logarithmic factor is lost.
Reaching the critical exponent when is the substantial step. The paper does it with Hölder's inequality for Lorentz spaces and and an estimate of a nonincreasing rearrangement (display (32)). Mathlib has neither Lorentz spaces nor nonincreasing rearrangements, so this part either builds that infrastructure or replaces it with a direct layer-cake argument against the distribution function of . The obvious approach, the same splitting as for , does not work: it always loses the logarithm.
EuclideanSpace ℝ (Fin d) with , and a measurable version of the regression function with values in everywhere. Every Borel distribution on has this form, and the paper defines "for some choice of ".Metric.infDist gives . For Theorem 2.6 both readings give a true statement. Under the reading , the companion statements Theorem 2.7 and Lemma 4.1 are false for a version of with an empty class. The convention is chosen for agreement with the companion mission.lintegral), so a bound can never hold through a junk value of a non-integrable function.The source is arXiv:0708.1838v1, the reprint of the Annals article. Its printed page numbers equal the PDF page numbers, and every page cited here is that number.
The newsvendor problem is the basic single-period inventory model: a decision maker orders units at unit cost before a random demand is observed, sells units at price , and loses unsold units. Its optimal order is the critical fractile of the demand distribution . Laboratory experiments show that human subjects do not order . Schweitzer and Cachon (Management Science 46(3), 2000) gave subjects uniform demand on and found that the average order lay below for a high-margin product and above for a low-margin product: orders are pulled toward the center of the demand range.
Su (Manufacturing & Service Operations Management 10(4), 2008) explains this pattern with a model of bounded rationality: the decision maker does not pick the best order with certainty, but picks better orders more often, through a logit choice rule. This mission formalizes the first results of that paper, the case of uniform demand, where the logit order has an explicit law and the pull toward the center can be proved exactly. The source is the published MSOM 2008 article; all page numbers are its printed pages.
A decision maker with utility over an interval and bounded-rationality parameter makes a random choice with the logit density
and off (eq. (2), p. 571). Large means noisy choices; small concentrates the choice near the maximizer of .
In the newsvendor problem the price and unit cost satisfy . Demand has density and distribution function . The expected profit of ordering units is
and the optimal solution is its maximizer. The behavioral solution is the logit choice with utility over the decision domain , the smallest interval containing the support of (eq. (4), p. 572).
This mission takes uniform demand with : on and . The midpoint of the demand range is . Two parameters recur:
A truncated normal law on with parameters has density proportional to on and zero elsewhere (eq. (37), p. 586). Write and for the standard normal density and distribution function.
The goal is stated for every and every , with any maximizer of over ; it fixes only the sign of the bias, not its size.
Proposition 3 gives a single mechanism, noise in the choice of the order, that produces both directions of the bias observed by Schweitzer and Cachon: under uniform demand, a high-profit product () is underordered on average and a low-profit product () is overordered. Proposition 1 gives the full law of the boundedly rational order, which is what makes the model testable: the paper fits the truncated normal law to experimental order data and estimates (§5). Corollary 1 is the closed-form mean used in that fit and in Proposition 3.
These results are proved in the paper by direct computation; none of them has a machine-checked proof. The mission adds a checked development of the continuous logit choice model on an interval, of the truncated normal law and its mean, and of the uniform-demand newsvendor profit, together with exact statements of what the paper's informal phrases mean (see Formalization scope).
Each step is elementary on paper, but the formal content sits in the integrals. Expected sales must be computed as a piecewise integral to obtain eq. (5), and the maximizer must be identified over all of , not only on , which needs the profit outside the support as well. Proposition 1 is an identity between two normalized densities, so both normalizing integrals must be shown positive and finite. Corollary 1 requires the mean of a truncated Gaussian in terms of Mathlib's Gaussian density and distribution function, which is not in Mathlib. For Proposition 3, the natural shortcut "the mean of a truncated normal is " is false whenever , and it is exactly the asymmetry of the truncation that produces the bias.
All quantities are real numbers, with the paper's standing assumptions as hypotheses: , (the page states ; is read so that lies inside ), and (eq. (2) divides by ; , perfect rationality, is a limit, not a value of the formula). The decision domain is the closed interval ; the logit density is zero off it, and expectations are integrals over . The parameter is the positive square root of , and , are Mathlib's gaussianPDFReal 0 1 and the distribution function of gaussianReal 0 1.
Corrections and readings relative to the printed text:
The optimal solution in the goal is a hypothesis that maximizes over , never a variable set to a closed form by fiat; milestone 2 shows the hypothesis is satisfiable and identifies . No statement holds vacuously through a junk value: on with the logit normalizer is the integral of a continuous positive function over an interval of positive length, and the denominator of (8) is positive because .
Reusable beyond this mission: the logit density on an interval, the truncated normal density, and its mean formula. Proofs of any milestone, and of the mean of a truncated normal law in general, are welcome.
A service system with several servers can use a larger fraction of its capacity than a single-server system while still giving customers an acceptable wait. The design question is how much unused capacity is needed as the number of servers grows. Ward Whitt's study begins with a factory manager deciding whether to put four machines in one work area. It uses queueing models to connect the number of machines, their utilization, and the delays customers experience. The proposed utilization rule, , keeps the unused fraction proportional to as the number of servers changes (Whitt 1992, pp. 708–710).
The paper distinguishes the chance that a customer waits at all from the length of the wait once a delay occurs. That distinction matters when a staffing choice must control a long wait rather than merely the fraction of customers who wait. The exact result in §3.1 gives a benchmark for the paper's later approximations to more general arrival and service processes (Whitt 1992, pp. 719–720).
An queue has Poisson arrivals at rate , identical servers, independent exponential service times, unlimited waiting room, and first-come first-served service. Time is measured so that each server's service rate is one. The server utilization is . We consider and , so the queue has a stationary distribution. Let be the stationary probability that customers are in the system. Its state process is a birth–death process: arrivals occur at rate and departures from state occur at rate .
Let be an arriving customer's steady-state time in the queue before service begins. An arrival finding fewer than customers starts service at once. An arrival finding customers waits for service completions while all servers are occupied. In the formal model, the law of has an atom at zero of mass and, for each , a gamma component with shape , rate , and weight . The arrival-state weights use the Poisson-arrivals-see-time-averages property. This construction represents the FCFS waiting time independently of any claim about its eventual conditional distribution.
For an event of positive probability, denotes the conditional waiting-time law. The paper calls a customer delayed exactly when . The scale parameter is defined by the utilization equation ; because , this equation makes positive.
The supporting target is the §3.1 statement that a delayed customer's waiting time is exponential with rate , equivalently with mean :
The goal is Proposition 3.1 under the utilization equation. It records both the entire conditional tail and its mean, for every :
The goal also asserts , so these conditional quantities are defined. The scan of Proposition 3.1 prints the exponent without and the mean denominator with ; the statement here uses the values determined by the preceding exponential-law sentence and by the paragraph following the proposition (Whitt 1992, pp. 719–720).
The result gives an exact delay distribution for the Markovian multi-server system. With servers and the utilization equation held fixed, the conditional tail at any positive threshold and the mean wait of a delayed customer both depend on through . Thus the same rule that organizes the probability-of-delay discussion has a definite implication for customers who actually wait. It is also the exact comparison point for the paper's later, explicitly approximate analysis of general queues (Whitt 1992, §3.2).
Formalizing this result supplies a reusable representation of the stationary FCFS waiting-time law as a mixture of Erlang distributions, together with a precise connection between birth–death state probabilities and delay. The related platform items QueueingFundamentals.BirthDeath.mmc_steady_state and QueueingFundamentals.BirthDeath.erlang_c_formula state the stationary state probabilities and the probability of delay, respectively; both are open and neither states this waiting-time law. The open QueueingFundamentals.BirthDeath.halfin_whitt concerns the heavy-traffic limit for the case, a different target. The current result is known mathematically from Whitt's 1992 paper; this mission asks for its machine-checked proof in the specified model.
The conditional distribution is not immediate from an individual service time. A delayed arrival can encounter any queue length , so its waiting time is a gamma law whose shape varies with . The stationary probabilities provide the weights of infinitely many such components. Showing that this whole mixture has one exponential law requires a relation among the stationary tail probabilities and control of the infinite sum. The same mixture must have a well-defined first moment for the conditional mean formula.
Lean uses a natural number , a real arrival rate , and a real sequence satisfying the published QueueingFundamentals.BirthDeath.IsSteadyState predicate with constant birth rate and death rate . That predicate includes nonnegativity, total mass one, and the global balance equations. Its published definition is imported as a reference. Service rate is exactly one, as fixed in §2.1 of the paper. The conditional waiting-time law is a measure on real time, with a point mass at zero and a countable gamma mixture. The positive-time restriction of this measure expresses conditioning in the milestone; real measure values and an integral express the tail and mean in the goal.
The formal hypotheses spell out positive arrival rate, at least one server, and subcritical utilization. These make the stationary law and the positive exponential rate meaningful. The goal states positive delay probability before dividing by it. The waiting-time law is built from stationary queue lengths and service completions, rather than being defined as exponential; proving that it becomes exponential is the mathematical task. Solvers may develop reusable measure-mixture identities, stationary-tail facts, and gamma or exponential distribution results. The approximation formulas of §3.2 and the paper's numerical tables are outside this mission.
A network designer may need a cheap connection that keeps the number of links at each site within a local capacity. The minimum bounded-degree spanning tree problem asks for the cheapest spanning tree of a weighted, undirected graph whose vertex degrees respect prescribed upper bounds. The capacity constraints matter in settings where a low-cost tree alone can overload a few hubs. They also make the optimization problem difficult: even with unit edge weights and a bound of two at every vertex, feasibility includes the Hamiltonian path problem. Singh and Lau study the useful relaxation in which the returned tree may exceed each degree bound by one while its cost stays no greater than the best tree satisfying every original bound Singh–Lau 2007.
The weighted result settled the bounded-degree form of a conjecture discussed in their paper. Goemans had obtained a cost-preserving degree guarantee of ; an earlier unweighted local-search result attained a degree allowance but did not cover arbitrary real costs. Singh and Lau's Theorem 1.2 gives the allowance in the weighted setting, without assuming nonnegative costs or triangle inequalities Singh–Lau 2007, pp. 661–662. The platform's open WilliamsonShmoys.minimum_degree_tree_local_search_approximation concerns the related unweighted minimum-degree local-search problem, with a different objective and guarantee.
Let be a finite vertex set and a finite set of unordered, non-loop edges. A spanning tree connects every vertex without a cycle. Every edge has a real cost , so . Each vertex has an integer upper bound on its tree degree . A feasible original solution has for all .
The paper studies a broader connecting-tree problem. A forest is already selected; its connected components, including isolated vertices, are supernodes. The remaining graph has edges disjoint from . A set is an -tree if is a spanning tree. Degree bounds are active only at vertices in , and counts edges of , not edges of . The initial spanning-tree problem is the case and Singh–Lau 2007, p. 665.
For an edge set and vertex set , write for edges of with both endpoints in , and for edges of incident to . The LP-MBDCT relaxation has a nonnegative variable for each . It requires , requires for every nonempty union of supernodes, and requires for . Its objective is . At , , this is the spanning-tree LP in equations (1)–(5) Singh–Lau 2007, pp. 662, 665.
For every feasible initial LP, the paper's Figure 4 algorithm has a terminating run. Every possible run returns a spanning tree satisfying
In particular, is at most the cost of every spanning tree satisfying the original bounds, and thus at most the original optimum. Every run has at most iterations. The cost comparison against every LP-feasible vector states the stronger bound used by Theorem 4.2 Singh–Lau 2007, pp. 661, 666.
The connecting-tree theorem makes the same cost and degree guarantee for an arbitrary feasible state , with only for . The attack path follows the paper's numbered results: Lemma 4.3 describes tight constraints by a laminar family, Claim 4.5 classifies vertices with one excess token, Lemma 4.6 bounds tokens inside a laminar subtree, and Lemma 4.1 says each nonterminal basic solution has either a unit-valued edge or a removable degree constraint. Theorem 4.2 then supplies the general guarantee Singh–Lau 2007, pp. 666–667.
The result allows one unit of violation at each local degree bound while preserving the cost benchmark exactly. It applies even when negative edge costs make standard multiplicative cost ratios awkward. The connecting-tree statement is useful beyond the initial instance because it covers a forest already accumulated and a subset of degree constraints still active.
This mission formalizes the known 2007 result as an open Lean proof target; the paper proves the mathematics, while the declarations here currently have no machine-checked proofs. A completed development would provide a reusable account of a spanning-tree LP with forest contraction, basic solutions defined by tight rows, and a finite relational algorithm with all choices exposed. These objects could support the paper's lower-and-upper-bound extension and other iterative-rounding results.
Rounding an arbitrary fractional edge upward can increase cost beyond the LP benchmark. Restricting the algorithm to edges with value exactly one protects that benchmark, but a nonterminal basic solution need not present a unit-valued edge. The central structural question is then whether some active degree constraint can be removed with only a one-unit effect on the final degree. The tight subtour rows and degree rows overlap, so counting edges from the support alone is insufficient; Lemmas 4.3–4.6 resolve the dependency and token-counting issues that make the direct argument fail Singh–Lau 2007, pp. 666–667.
Lean represents edges as Sym2 V in finite sets, excluding diagonal edges. It represents LP vectors on all unordered pairs but requires zero values outside the current edge set. A forest is acyclic on the full vertex set. A compatible subtour set is a union of its connected components. Subtour right-hand sides are real numbers, so subtraction does not truncate at zero; the empty set is excluded because the literal row would make the LP infeasible. Degree bounds are integers so the algorithm's decrements are total. A basic feasible solution is determined uniquely by its tight equality rows among vectors supported on the current edge set. Linear independence in Lemma 4.3 is checked on the positive support.
Figure 4 is a relation because the LP optimum, a unit-valued edge, and a qualifying vertex may each be chosen in several ways. Its edge and vertex tests are mandatory when their conditions hold. The vertex test uses the support before deleting the selected edge and bounds after decrementing its endpoints, following the printed order. “The algorithm returns” is represented by existence of a run, an iteration bound on every step chain, and guarantees for every returned set. “Cost at most the LP optimum” means cost no greater than the objective at every feasible LP vector. “Polynomial time” is represented by the iteration count; the ellipsoid LP solver and separation-oracle complexity are outside this mission. Lemma 4.6's token distribution is expressed as its explicit counting inequality.
The goal asserts the Figure 4 output and its LP cost guarantee. Bare existence of a tree with cost at most the optimum and degrees at most would be witnessed by an original optimal tree and would lose the algorithmic theorem. A return guarantee without run existence would hold vacuously for a stuck relation. Contributions that prove the stated structural lemmas, establish the LP oracle's basic-optimum availability, or close the algorithm invariant are within scope. No existing platform item treats this bounded-degree LP and iterative-rounding algorithm under these conventions; the plain minimum-spanning-tree LP definition uses a different edge representation and no forest or degree constraints.
A many-server queue has identical servers, a stream of arriving customers, and a buffer in which customers wait when every server is busy. It models call centres, hospital wards and server farms, and the regime of practical interest is the Halfin–Whitt or quality-and-efficiency-driven regime, in which the number of servers grows with the arrival rate so that : servers are almost fully used, yet only a vanishing fraction of customers waits.
This mission formalizes that identity and the proposition that yields it.
Fix one realisation of the queue (Reed, §2, p. 6).
The number in system is (2.2):
Centring each indicator at its (conditional) mean produces the terms
and , the analogous centred sum (2.5) over the customers who entered service after time . is the conditional mean number in a queue fed by the same arrivals.
A sample path is non-idling if for every
that is, the customers waiting at time are exactly those who have arrived and not yet entered service. This holds for every first-come-first-served -server path that never idles a server while a customer waits; the paper uses it at the start of the proof of Proposition 2.1 (p. 8).
For a non-idling sample path and every ,
The result. Equation (2.8) is the paper's starting point for both of its limit theorems. Writing with shows that the number in system is the image of the infinite-server quantities under the regulator map of the paper's §3, the unique solution of . The fluid limit (Theorem 4.1, p. 12) and the diffusion limit (Theorem 5.1, p. 23) then follow from limit theorems for the infinite-server terms and the continuity of that map. Without (2.8), the -server queue has no closed equation in terms of quantities whose limits are known.
Formalizing it. The identity is proved in the paper on pp. 7–9; to our knowledge it has not been machine-checked. This mission produces a sample-path model of the queue (initial customers, arrivals, FCFS service order, waiting times) together with the decomposition of its number in system, reusable for other many-server results stated pathwise. The limit theorems 4.1 and 5.1 themselves are weak-convergence statements in the Skorohod space and are not part of this mission; the regulator map (Proposition 3.1) is the subject of a separate mission of this series.
The decomposition (2.7) is bookkeeping. The content is Proposition 2.1, which converts a sum over customers of tail differences into an integral, against , of the number of waiting customers at earlier times. The step that needs care is the change of viewpoint from "customer 's service time falls in a window of length " to "customer is waiting at time ", after which the sum over customers must be recognised, at each time , as the waiting count of the non-idling identity, with the arrivals counted up to rather than . A second point is the treatment of an atom of at : the half-open windows and the closed integration range must match, and for is used whenever a customer is still waiting.
Related platform items: WhittEfficiency.IS.* (the queue with Poisson arrivals, the infinite-server object behind ) and PalmQueueing.Palm.swiss_army_formula (a pathwise queueing identity of Palm calculus) are the nearest queueing results; neither is the object of this mission.