Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Randomized load balancing asks how much a dispatcher gains from a little information. In the supermarket model, jobs arrive at servers and each job inspects a few servers chosen at random before joining one. With one random choice every server is an independent M/M/1 queue, and the expected time a job spends in the system is at load . With two choices it is exponentially smaller as . This "power of two choices" underlies the design of distributed schedulers, hashing schemes and server farms, where querying every server is too expensive but querying two is cheap.
Timeline:
Customers arrive as a Poisson stream of rate , , at FIFO servers. Each customer chooses servers independently and uniformly at random with replacement and joins the one holding the fewest customers; service times are exponential with mean . Let be the fraction of servers holding at least customers at time .
A state is a sequence of reals with , and . The empty state has and for . As the tails follow the limiting system
A trajectory is a map , , whose values are states and whose coordinates satisfy (1) (from the right at ). Throughout, is an integer.
The fixed point is , so , , . A customer arriving in state becomes the -th customer of its queue with probability and then waits for services, so the expected time it spends in the system is
The target constant is
For and , , and:
The hypothesis holds for every initial state that comes from a finite system.
The comparison against is the quantitative content of the power of two choices: the companion mission shows as , an exponential improvement. Corollary 2 is what connects that number to the dynamics: it says the fixed point's expected time is actually reached from realistic initial states, and is an upper bound from an empty start. Theorem 2's comparison argument and Theorem 3's weighted potential are reused across the mean-field analysis of load-balancing variants (threshold policies, heterogeneous servers, work stealing), so the formal statements here are templates for that literature.
All results are proved in the paper (Theorem 3's proof is written out for with a remark that it extends). None has a machine-checked proof that we know of. The work is formalizing the known arguments for all , including the parts the paper delegates to a citation: quasimonotone comparison for countable ODE systems in Theorem 2, and the upper right Dini derivative handling of in Theorem 3.
The system is infinite-dimensional, so standard finite-dimensional ODE comparison and Lyapunov theorems do not apply as stated. Theorem 2 rests on a monotonicity property (raising the initial tails raises them for all time) that the paper justifies by a coupling intuition and a citation to a comparison theorem for quasimonotone systems; that theorem must be supplied for -bounded countable systems. The plain distance is nonincreasing along trajectories but does not decay exponentially by a direct estimate; the weights must be built so that every coordinate's contribution to is dominated by , while staying geometrically bounded so that under the doubly exponential tails of Theorem 2. Exchanging with the infinite sum defining needs uniform tail control, which is again Theorem 2.
PowerTwoChoices.Limit; λ is lam : ℝ, with , in every theorem.x : ℕ → ℝ with x 0 = 1, nonnegative and antitone. A trajectory is s : ℝ → ℕ → ℝ, a state for every , with HasDerivWithinAt on Set.Ici 0 for each coordinate : right derivative at , two-sided for .l1Dist.Filter.atTop.tsum (a divergent series would make the upper bound free and the limit attainable by a junk ), dropping the summability condition in Lemma 2 ( is also a fixed point), choosing Theorem 3's weights after the trajectory, and stating anything for only.The learning with errors (LWE) problem underlies most of post-quantum public-key cryptography. Its hardness rests on Regev's reduction from worst-case lattice problems to LWE (Regev, J. ACM 2009). The reduction is iterative: it repeatedly turns samples of a discrete Gaussian on a lattice into samples of a narrower one. Its classical step, Lemma 3.11, needs the following fact. Adding continuous Gaussian noise to a discrete Gaussian sample gives, up to a small statistical distance, a continuous Gaussian. That fact is Claim 3.9 of the paper. Through Corollary 3.10 it turns a lattice point plus noise into an LWE-type sample with a periodic Gaussian error.
The tool behind it is the smoothing parameter of Micciancio and Regev (SIAM J. Comput. 2007). Above this width a discrete Gaussian on a lattice behaves like a continuous one. Claims of this type have since become standard in lattice-based cryptography: discrete Gaussian sampling, trapdoors, and the convolution theorems of Peikert (CRYPTO 2010).
This mission formalizes Claim 3.9 from the published J. ACM article (Article 34, 2009). The paper's main theorem, Theorem 3.1, is a quantum reduction about efficient algorithms. It is outside this series of missions.
Work in with the Euclidean norm and Lebesgue measure. For the Gaussian function is , its shift is , and is a probability density (Eqs. (4)–(5)). For a countable set , .
A lattice is the set of integer combinations of linearly independent vectors. Its dual is , and , where is the volume of a fundamental parallelepiped. For and , the discrete Gaussian is the distribution on the coset with mass at (Eq. (6)).
For the smoothing parameter is the smallest with (Definition 2.10).
The statistical distance of two densities is , with no factor , so it ranges in .
Let and . The distribution is obtained by sampling and adding independent noise with density . Its density is
If for some , then
A supporting item states the bridge used in both proofs: if , then .
Claim 3.9 is what makes Regev's iterative step classical. A discrete Gaussian sample, blurred by continuous noise, cannot be told apart from a continuous Gaussian of the combined width, except with probability . Corollary 3.10 projects this onto a direction and reduces it modulo 1 to obtain LWE samples with periodic Gaussian error . Without it, the reduction from lattice problems to LWE has no way to produce its error distribution. Claim 3.8, a milestone here, says that above the smoothing parameter the discrete Gaussian measure is almost invariant under shifts. It is the basic estimate of the theory.
The results are proved in the paper; none of them is formalized. Lean's Mathlib has lattices, their covolume, dual submodules and the Gaussian Fourier transform. The platform has the Poisson summation formula for lattices. This mission adds the smoothing parameter, discrete Gaussians on cosets, and the first machine-checked convolution theorem for discrete and continuous Gaussians. Later work, such as Corollary 3.10 or Peikert's general convolution theorem, can build on it.
Neither density is a finite object. is an infinite sum over a coset of a lattice, normalized by another infinite sum. A direct term-by-term comparison of with fails: the sum defining is a Gaussian sum over a shifted lattice, and its value genuinely varies with the position of relative to ; for narrow Gaussians the variation is of order one. The claim is that this oscillation is uniformly small, with a relative error that depends only on , not on , or . Two ratios of lattice sums must be bounded at once, uniformly in . The constant uses in an essential way, because must stay below .
The smoothing parameter is defined as a least element. That the least element exists, i.e. that the infimum is attained, is itself a statement about continuity and strict monotonicity of an infinite sum in its width.
EuclideanSpace ℝ (Fin n).Submodule ℤ with [DiscreteTopology L] [IsZLattice ℝ L].LinearMap.BilinForm.dualSubmodule (innerₗ _) L.ZLattice.covolume L.tsums. They are genuinely summable, so no summability hypothesis is added.Added hypotheses, each disclosed in the item.
Other conventions.
𝓕, , as on p. 34:20.Reusable beyond this mission: the Gaussian, coset-sum and smoothing-parameter definitions, Claim 3.8, and the shifted Fourier transform. Proofs of any milestone are welcome, and so are proofs of the summability and Schwartz facts for Gaussians on lattices that every milestone needs.
Airlines sell seats on a single flight in several fare classes. Discount classes book first, so the carrier must decide how many seats to protect for later, higher-paying passengers. The classical answer, from Littlewood's rule for two classes to the nested optimality conditions of Brumelle and McGill (1993), computes optimal protection levels from a forecast of the demand distribution of each class. Those forecasts must be built from censored booking data, which is where most of the practical difficulty lies.
van Ryzin and McGill (2000) observed that the optimality conditions themselves can drive an adaptive rule. After each flight one only records whether a fill event occurred (whether demand reached each protection level) and moves the levels by a stochastic-approximation step. No forecast and no optimization is needed. Their Theorem 1 asserts that this rule converges almost surely to the optimal protection levels, with an explicit mean-square rate. It is one of the standard references for model-free revenue management. The convergence proof combines Robbins–Monro theory, the Robbins–Siegmund supermartingale lemma and an induction over fare classes.
There are fare classes with fares and discount ratios . On a flight the class demands are independent, nonnegative and continuously distributed. Successive flights are independent with the same law.
A protection vector is . The fill events are
A vector is characterised by the optimality condition (3), for . The adjustments are , and their means are . From an arbitrary the algorithm updates
The interim protection levels are what the airline actually uses to control bookings. The updates themselves monitor .
Assume:
Then for ,
and there are and with
The exponent is left existential, as in the paper, so any improvement of the rate constant still proves the goal.
The milestones follow the paper's own proof, in attack order:
Theorem 1 says that the nested optimality conditions of Brumelle and McGill can be reached by observing binary fill events alone. It also says that the limit is automatically ordered, , so the interim levels coincide with the limit. The algorithm is distribution-free and needs neither demand forecasts nor uncensoring, which is why it is used in practice and as a baseline for later data-driven and learning-based revenue management.
The theorem is proved in the paper. As far as is known it has no machine-checked proof. Formalizing it requires a vector Robbins–Monro argument with coupled coordinates, the Robbins–Siegmund lemma, and an explicit polynomial rate. Two of the milestones are general probability facts reusable far beyond this mission: Lemma 1, and Robbins–Siegmund, which no platform item states yet. The formalization also corrects the record on two printed slips, described under Formalization scope.
Coordinate is not a Robbins–Monro process by itself. Its fill event depends on all of , so the drift of is perturbed by the errors of the lower coordinates. Applying a scalar convergence theorem coordinate by coordinate fails at this point. The perturbation has to be bounded via the Lipschitz assumption A3 and shown to be summable along the path, which uses the mean-square rate already established for class . The rate and the almost-sure convergence must therefore be carried through the induction together. The exponent halves at each class. A second difficulty is that A2 is only usable on a bounded set, so boundedness of the iterates (Lemma 3) has to come first and must be uniform.
Classes are indexed from in Lean (-indexed vectors whose index and indices above are never read). A flight's demand vector has the product law , and the sample path has the countable product of copies of it. Lean's iterate … n is the paper's , so the rate pairs it with . Continuity of a demand law is "every singleton is null". Expectations are Bochner integrals, and integrability is part of each rate conclusion. The fill event reuses the published NestedSeatAlloc.ProbCond.nestEvent.
Pinned and corrected statements:
Not posed: §4's modifications (projection onto the capacity, randomized integer levels, booking lead times) and the simulations of §5.
Contributions welcome: proofs of the general lemmas (Lemma 1, Robbins–Siegmund) stated for arbitrary probability spaces, measurability facts for the recursion, and the elementary Lemma 4.
Stable distributions were proposed as models of asset returns by Mandelbrot and Fama in the 1960s, because empirical returns show heavier tails than the normal law allows; Rachev and Mittnik's monograph Stable Paretian Models in Finance (2000) collects the later development. When the vector of per-share returns of assets follows a multivariate -stable law with , its distribution is determined by the stability index , a shift , and a finite Borel measure on the unit sphere, the spectral measure. The risk of a portfolio is then measured by the scale parameter of the return, and choosing an efficient portfolio becomes a deterministic optimization problem in .
In practice neither nor is known: both are estimated from data. Whether the optimal portfolio is robust to estimation error is therefore a practical question. Section 5 of Rachev and Römisch, Quantitative stability in stochastic programming: The method of probability metrics (Math. Oper. Res. 27(4), 2002; this mission follows the authors' preprint), answers it with an explicit modulus, as an application of the paper's general stability theory for stochastic programs under perturbations of the underlying probability measure.
Fix and equip with the Euclidean scalar product and norm .
For each there is such that
whenever and . The modulus is not fixed: it is whatever the growth of the unperturbed problem gives.
If is nonsingular, then (22) has a unique solution and for some and all sufficiently small .
The theorem bounds how far the optimal portfolios can move when the stability index and the spectral measure are both perturbed, with a modulus computed from the unperturbed problem alone. Combined with the companion, the efficient portfolio of a nonsingular spectral measure is unique and moves by at most . Since metrizes weak convergence on the compact sphere, any consistent estimator of in the weak topology, together with a consistent estimator of , yields consistent estimates of the optimal portfolio, and convergence rates for translate into rates for the portfolio. The paper notes (Example 5.3) that spectral measures of linear transformations of independent stable variables with a full-rank matrix are nonsingular, so the Hölder case covers the discrete spectral measures used in practice.
The result is proved in the paper; nothing here is open. To our knowledge none of it is machine-checked: Mathlib has strong convexity and the real power function but no stability theory of stochastic programs and no Fortet–Mourier metrics. The mission produces a checked proof of the result and a reusable formal treatment of the growth-function modulus in a concrete, fully explicit instance.
The obvious argument compares the optimal values of the two problems and concludes that a perturbed minimizer is nearly optimal for the unperturbed problem. Turning near-optimality into a distance bound requires the growth function and its generalized inverse; is defined by an infimum over a set that may be empty, and by a supremum that may be infinite, so this step has to be handled in extended arithmetic with care. A second difficulty is the term: the map must be shown to be -Lipschitz on the sphere uniformly over , which uses on the simplex. The change of exponent from to is controlled by a sharp calculus inequality whose constant needs . In the nonsingular case, the quadratic form must be shown to dominate , a compactness argument on the unit sphere of .
EuclideanSpace ℝ (Fin s) with coordinates indexed . The paper says "the (Euclidean) scalar product", so Euclidean norms are the paper's own.Metric.sphere 0 1. A spectral measure is a probability measure on with , and every integral is a set integral over . For the sphere is empty, no spectral measure exists, and every statement is vacuous, as in the paper.Metric.infEDist, to the empty set), and and take values in .Welcome contributions: the inequality on , strong convexity of on , and a general lemma converting a growth function and a uniform objective perturbation into a distance bound; the last is reusable for every stability result of the paper.
A stochastic program minimizes an expected cost under expected-value constraints, and the expectation is taken with respect to a probability distribution of the random data. In applications is rarely known: it is estimated from samples, replaced by a finite scenario tree, or chosen from a parametric family. Whether the optimal value and the optimal decisions of the approximate problem are close to those of the true problem therefore decides whether the approximation can be trusted. Quantitative stability asks for explicit bounds on the change of optimal values and solution sets in terms of a distance between and its perturbation .
S. T. Rachev and W. Römisch (Quantitative stability in stochastic programming: The method of probability metrics, Math. Oper. Res. 27(4), 2002; this mission follows the authors' preprint) organize this question around a single probability distance, built directly from the integrands of the problem. Their general results (Section 2) are then specialized to two-stage linear and mixed-integer programs, to chance constraints, to empirical approximations, and to a portfolio problem. This mission covers the general part: Proposition 2.1 and Theorems 2.2 and 2.3.
Let be a nonempty closed set, a closed set, and , , normal integrands: each epigraph is closed and the epigraphical mapping is measurable. For a Borel probability measure on the problem is
with feasible set , optimal value and solution set ; is the original measure.
For a nonempty set , the localized problem restricts to , with feasible set , value and solutions . The admissible measures are those under which for every and . The minimal information distance is
The constraints are metrically regular at if there are , with for near and small , where is the feasible set with right-hand sides . A nonempty set is a CLM set (complete local minimizing set) with respect to an open if it equals and lies in . The growth function is , with and .
Under the assumptions of Theorem 2.2 — ; and an open bounded neighbourhood of ; if , Lipschitz on ; metric regularity at every , — there are and with
The constants are existential: the goal fixes the shape of the estimate, not its constants.
Theorem 2.2 shows that the distance carries exactly the information about that the problem uses: any probability metric that dominates it inherits the Lipschitz estimate of optimal values. This is the mechanism by which the paper derives stability with respect to Fortet–Mourier metrics for two-stage programs, with respect to discrepancies for mixed-integer and chance-constrained programs, and convergence rates for empirical approximations via empirical-process bounds. Theorem 2.3 adds the solution sets: their deviation is controlled by , which is determined by the growth of the objective near ; quadratic growth yields Hölder continuity with rate (Remark 2.4).
The results are proved on paper. No machine-checked version of these stability theorems, of metric regularity for expected-value constraints, or of the minimal information distance exists on the platform. The formalization also settles the exact quantifier structure of Theorem 2.3: its printed form ("for each ") is true only for , and the mission states the δ-local form that the proof establishes.
The obvious argument compares the two problems pointwise in : the integrals differ by at most , so the optimal values should too. This works without constraints, but with the feasible sets themselves move, and a point feasible for need not be feasible for . Controlling this displacement needs metric regularity of the constraint system, which is only local, around each point of ; passing from local to uniform constants requires compactness of and a covering argument. A second difficulty is extended-real analysis: the integrands take the value , lower semicontinuity must come from Fatou's lemma under the integrability conditions defining , and the existence of localized solutions depends on this lower semicontinuity on the compact set .
and are EuclideanSpace ℝ (Fin m), EuclideanSpace ℝ (Fin s); the paper never fixes its norm, and every statement has existential constants, so the Euclidean norm is a faithful instance. Measures are Borel probability measures on the subtype . Integrals of extended-real integrands use the published DupacovaWets.Consistency.expect ( when ). The integrands are indexed by Fin (d+1), with index the objective. Values , and are infima in ( on empty sets; the paper's "min" in is read as an infimum); , and take values in ; distances to sets are extended distances (infinite to the empty set). Lower semicontinuity and closed graphs in Proposition 2.1 are stated sequentially, which is equivalent in the extended pseudometric space . The balls in (5) are closed balls.
Standing assumptions carried by every statement: nonempty and closed, closed, all normal integrands, and measures in . Every value estimate asserts that both optimal values are finite, so no bound holds through an convention, and the distance to an empty feasible set is , so metric regularity cannot hold vacuously. The one deliberate deviation from the page is the δ in the goal, explained above.
A complete development needs Fatou's lemma for extended-real integrands bounded below by an integrable function, measurability of infima of normal integrands, and Berge's stability theorem for parametric programs. The first two are reusable for every stochastic-programming mission on the platform. Contributions of these lemmas as separate theorems are welcome.
Many problems in statistics, signal processing and machine learning minimize the sum of a smooth function and a convex but nonsmooth one: -regularized least squares (the Lasso), bound-constrained problems, and group-sparse regression are standard examples. Tseng and Yun (Math. Program. Ser. B 117 (2009) 387–423) proposed the coordinate gradient descent (CGD) method for this class and proved that it converges linearly under a local Lipschitzian error bound, Assumption 2(a) of their paper. An assumption is only as useful as the list of problems known to satisfy it. Section 6 of the paper supplies that list, and this mission formalizes it.
Error bounds of this kind have a history in smooth constrained optimization. Luo and Tseng proved them for quadratic objectives over polyhedral sets (Luo–Tseng 1992, SIAM J. Optim.), for strongly convex functions composed with a linear map (Luo–Tseng 1992, SIAM J. Control Optim.), and for dual functionals of linearly constrained strictly convex programs (Luo–Tseng 1993, Math. Oper. Res.), and used them to derive linear rates for feasible descent methods (Luo–Tseng 1993, Ann. Oper. Res.). Tseng and Yun carry these results over to the nonsmooth problem (1) by reformulating it as a smooth problem over the epigraph of the nonsmooth part.
Throughout, carries the Euclidean norm . The problem is
where , is proper, convex and lower semicontinuous with effective domain , and is continuously differentiable on an open set containing .
The residual at is
the unique minimizer of a strongly convex function. A point is stationary if the one-sided directional derivative satisfies for every direction ; denotes the set of stationary points and the distance to it. A point is stationary exactly when its residual vanishes.
Assumption 2(a) asks that and that for every level there be constants with
Writing , problem (1) is equivalent to the smooth problem (41). Its projection residual at is the optimal solution of
is polyhedral if is the solution set of finitely many linear inequalities in ; is quadratic if with symmetric, not necessarily positive semidefinite. The four problem classes are:
Under C4, nonemptiness of is part of the conclusion. The constants are existential, so the goal does not depend on any particular estimate.
If is Lipschitz on with constant , there is depending only on with
If and C1, C2 or C3 holds, then for every there are with
where solves (42) with .
A further item, not a milestone, states the remark after Assumption 2 (p. 404) that Assumption 2(b) (stationary points with different objective values are uniformly separated) holds whenever is convex.
Theorem 4 is what makes the linear convergence theorem of the paper (Theorem 2, the subject of the second mission of this series) applicable. Through C1 it covers every problem with a quadratic and a polyhedral , including the Lasso and -regularized or bound-constrained quadratic programs, without convexity of . Through C2 it covers losses of the form with strongly convex, such as least squares , where itself is not strongly convex because may have a nontrivial kernel. These error bounds became a standard tool for linear rates of proximal and coordinate methods without strong convexity.
The paper's result is proved, but Lemma 7 is proved by citation: it applies three error bounds of Luo and Tseng to the reformulation (41). A complete formalization therefore requires those error bounds for smooth problems over polyhedral sets, which are not in Mathlib. To our knowledge none of the results of this mission has a machine-checked proof.
Lemma 6 and the C4 case of Theorem 4 are short inequality arguments. The difficulty is Lemma 7. The natural first idea, proving an error bound from strong convexity, fails for C1–C3: may be nonconvex (C1) or have a degenerate Hessian (C2, C3), and the objective of (41) is never strongly convex in . What replaces strong convexity is the polyhedral structure of , and the cited Luo–Tseng error bounds that exploit it are substantial results in their own right, each of which has to be established for a projection residual over a general polyhedron in .
is EuclideanSpace ℝ (Fin n), with indices . is the pair , its effective domain and its finite values there, with "proper, convex, lsc" given by the published ProxNewton.Inexact.IsProperClosedConvex. The value is never computed: every statement quantifies over , and membership in is x + d ∈ D ∧ P (x + d) ≤ ξ + δ. is a chosen minimizer of its subproblem, which at is the paper's unique one. The solutions of (42) enter through a predicate, and every bound is asserted for every optimal solution. Stationarity is the liminf form of . is the infimum distance. Assumption 2(a) quantifies over every real , which agrees with the paper's "" because the condition is vacuous below . In Lemma 6 the constant is quantified before the dimension and the data, so it depends on the Lipschitz constant only.
Explicit choices relative to the printed text:
A polyhedrality notion that admits only affine or constant , an Assumption 2(a) whose constants are chosen after , and a Lemma 7 whose residual is instead of the solution of (42) would all trivialize or change the statements. The encoding rules out each of them: polyhedral means a finite system of linear inequalities in , the constants precede , and Lemma 7 is stated for (42).
Welcome contributions: proofs of Lemma 6 and of the C4 case; Lipschitz continuity of polyhedral functions on their domain (Rockafellar–Wets, Example 9.35); the Luo–Tseng error bounds for affine variational inequalities and for composite strongly convex objectives over polyhedra, which can be reused well beyond this mission.
Functional limit theorems in queueing and applied probability are rarely proved from scratch. A limit theorem is established once for a primitive process, such as a random walk, a cumulative input or a renewal-reward process, and then transferred to the quantities of interest through the continuous mapping theorem: if in a function space and is continuous at almost every path of , then . The method works only if the functions in use are known to be continuous, and in which topology.
Ward Whitt's 1980 paper supplies these facts for composition, addition, the supremum, the reflecting barrier, the inverse or first passage time, and time reversal. This mission covers §7, the first passage time. Its role in applications is direct: the counting process of a renewal process is the first passage time of the partial-sum process. A limit theorem for cumulative work can therefore yield one for the number of completed jobs, and a limit theorem for a cumulative input can yield one for the time it takes to reach a level, when the mapping theorem's hypotheses hold.
Timeline. Skorohod (1956) introduced the topologies and on the space of right-continuous paths with left limits. Vervaat (1972) studied functional central limit theorems for processes with positive drift and their inverses, and Whitt (1971) studied weak convergence of first passage time processes. Whitt's 1980 paper restates continuity (Theorem 7.1) and adds the result: the map is continuous at every strictly increasing path (Theorem 7.2), although it is not -continuous on its whole domain.
A path is a function . It belongs to when it is right-continuous and has a left limit at every .
If , is strictly increasing, and in , then
The theorem says that every strictly increasing path is a continuity point of the first passage time map for . It fixes no constants, so a sharper variant of a milestone does not invalidate it.
The result. Theorem 7.2 lets functional limit theorems pass to first passage times when the limit has strictly increasing paths. The typical case is the fluid limit of a cumulative process, with . Together with the composition results of §3, it supports Theorem 7.3's centered inverse limit: if , , , has no positive jumps, and in , then in . This is one step from a central limit theorem for partial sums to one for counting processes. Theorem 7.4 shows a limitation: convergence of both the centered supremum and the centered inverse in forces a continuous limit.
Formalizing it. The results are proved and classical, but none of them has a machine-checked proof. The mission produces the topology on in Lean, the first passage time map with its basic properties, and the comparison between , and . That infrastructure is reused by every later formalization that goes through counting processes or the topology, including the planned wave of §§3–7 corollaries in this series.
The first passage time map is not -continuous. On p. 82 the paper gives paths in whose inverses converge only in : a flat stretch of the limit becomes a jump of , which the inverses of the approximating paths approach through two separate jumps. Inverting the time changes of the convergence cannot handle that split, because matches jumps one to one. The hypothesis that is strictly increasing excludes flat stretches of the limit. The technical weight lies in completed graphs and their parametric representations, which Mathlib does not have, and in the restriction to compact intervals at continuity points of the limit.
Ici 0. All convergences are sequential, which is equivalent because the spaces are metrizable (Theorem 2.6). Membership of every path in is part of each convergence.Contributions welcome: the general theory of parametric representations (existence, and the comparison with and ), which is reusable for any result. Alternative proofs of Theorem 7.2 that avoid are also welcome.
In a multihop radio network, links that are close to each other interfere, so only certain sets of links can transmit in the same time slot. Tassiulas and Ephremides (IEEE TAC 1992) modelled this as a constrained queueing system and asked which arrival rates any scheduler can sustain. Their answer has two halves. The first, Theorem 3.2, shows that a maximum-weight ("back-pressure") policy stabilizes the network for every rate vector in an explicit region , and that no stationary policy does better than its closure. The second, Theorem 4.1 and the subject of this mission, removes the restriction to stationary policies: outside the closure , every scheduler, however it uses the past, lets the queues grow without bound almost surely.
The pair of results is the origin of throughput-optimal scheduling in wireless and switched networks: max-weight scheduling in input-queued switches, back-pressure routing, and the Lyapunov-drift framework of network utility maximization all start from this region and this converse. The converse is what makes "throughput-optimal" a meaningful claim: it certifies that is a hard limit, not merely the limit of one policy class.
There are queues and servers (links). Server serves queue and sends each served customer to a queue or out of the system. Time is slotted and a service takes one slot. An activation set is a set of servers that may be active in the same slot; the constraint set is the family of all activation sets, and assumption C.1 says that every subset of an activation set is an activation set. The activation vector of a set is its indicator vector in , and is the convex hull of the activation vectors.
A history-dependent policy chooses, at the start of slot , an activation set as a function of the queue-length vectors , never activating more servers of a queue than it has customers. The queue lengths evolve by
where the arrivals are i.i.d. over , independent across queues, with finite second moments and means .
The routing matrix has if and if . A vector indexed by servers is an -admissible flow if . The region is the set of that admit such a flow and a point with wherever and wherever .
The proof uses the flow network : the queues plus an originator and a terminal , an edge of capacity for every queue, and an edge of capacity from to (or to ) for every server . A cut is a set of queues on the originator's side; its capacity is the total capacity of the edges leaving .
Theorem 4.1 closes the characterization of the throughput region of a constrained queueing network. With Theorem 3.2 it says that the set of sustainable rates is up to its boundary, for all policies and not only stationary ones, and that allowing schedules to depend on the entire history, on time, or on long-range planning cannot enlarge it. Every later throughput-optimality result for max-weight-type policies in switches and wireless networks cites this converse, and the region of "average activation vectors" is the standard capacity region of interference-constrained networks.
The result has been proved since 1992 and has not, to our knowledge, been machine-checked. A formalization adds a precise statement of the policy class (history-dependent, non-anticipating, never serving empty queues), a sample-path inequality (4.7) that is independent of probability and reusable for any arrival model, and a cut-based description of through Lemma 4.1 and Corollary 4.1.
The obvious argument fails at the policy class. For a stationary policy the queue-length process is a Markov chain and an instability argument can use its ergodic behaviour; a history-dependent policy has no such structure, and the time-average activation vector wanders in without converging. The argument must therefore find, for every possible average , a set of queues whose net inflow exceeds its outflow by a margin that does not depend on . That uniformity is the content of Lemma 4.1 and Corollary 4.1: it needs the max-flow/min-cut theorem on , the continuity of the mincut capacity in , the compactness of , and Lemma A.1 to bring a maximum flow back into . Comparing with the total service capacity, or using a single fixed cut, does not work: the bottleneck set of queues depends on how the policy spreads its activations.
Queues are Fin L and servers Fin N, indexed from 0. A server's destination is Option (Fin L), none meaning out of the system. is a Set (Finset (Fin N)); C.1 is a predicate, and every theorem that needs it also assumes (otherwise may be empty and no policy exists). Rate vectors are Fin L → ℝ, and includes . Service times are one slot, so . The goal's hypothesis is with defined from flows, as in the introduction of §IV; the printed theorem uses the closure of the stability region , which equals by Theorem 3.2 of the paper. A policy is a function from the history to the activation set of slot , required to choose sets in and to activate no more servers of a queue than it has customers; the queue dynamics are written in , where this requirement makes the subtraction exact. Arrivals are random vectors in , i.i.d. in time (iIndepFun, IdentDistrib), independent across queues, with integrable squares; is their mean, not a free parameter.
The statement does not hold vacuously: a one-queue, one-server example with constant arrivals of two customers per slot satisfies every hypothesis of the goal, including the existence of runs, and lies outside (checked in a sanity file). A formalization in which policies may see future arrivals, or may serve empty queues, or in which is unrelated to the arrival law, is a different theorem.
A complete development needs: the max-flow/min-cut theorem for finite networks with parallel edges (posed elsewhere on the platform in other encodings, not proved), continuity of a minimum of finitely many linear functions, compactness of a convex hull of finitely many points, and Mathlib's strong law of large numbers. The pathwise bound (4.7) and the cut lemmas are reusable for any interference-constrained network. Proofs of any milestone, and alternative routes to Lemma 4.1 (for instance through linear-programming duality), are welcome.
Temporal-difference learning estimates the future cost of a system from observed transitions. In a Markov model, a state has a distribution of possible successors and each transition carries a cost. An agent may approximate the future cost with a small number of basis functions rather than store one number per state. This is useful when the state set is large or countably infinite, but the sampling rule then matters: the states used to update the approximation need not arrive in the same proportions as visits to the underlying Markov chain.
Tsitsiklis and Van Roy distinguish sampling along the chain from drawing current states independently from a chosen distribution . Their 1996 LIDS report, §9 constructs an example where the latter version of TD(0) has a mean parameter vector whose norm grows without bound. The example applies to every sampling distribution on a countable state space with at least two states and every discount factor strictly between and . The mission formalizes that quantified counterexample, rather than selecting a particular two-state distribution.
Let be a finite or countably infinite set of states. A transition matrix assigns a probability distribution over next states to each current state . A transition cost is incurred when the chain moves from to , and discounts later costs. The cost-to-go is the expected sum of discounted costs along a chain started at . An invariant distribution satisfies .
A feature vector represents an approximate cost , where is learned. The weighted norm uses the weights , and projects onto the span of the features in that norm. The one-step operator sends to the expected immediate cost plus times the next-state value. These are the objects of §§2–4 of the report.
In -sampled TD(0), each current state is drawn independently from a probability distribution ; a successor is then drawn from row . Each new pair is independent of the earlier pairs. The parameter changes by
The step sizes satisfy the report's Assumption 4: they are chosen in advance, nonnegative and nonincreasing, their sum diverges, and the sum of their squares converges. Assumption 1 asks for a unique positive invariant law, finite stationary second moment of the transition costs, and finite cost-to-go from each state. Assumption 2 asks for linearly independent features with finite stationary second moments.
For every and , Theorem 3 asserts the existence of , , and a feature map satisfying Assumptions 1 and 2, together with a unique projected fixed-point parameter , such that for every ,
The expectation is over the independent state–successor samples. The target is the norm of the mean vector; it does not assert divergence of individual sample paths. The formal goal quantifies over every probability space carrying samples with the stated joint law, so a choice of representation for the random process does not change the theorem.
The milestones follow the claims in the proof of Theorem 3, pp. 24–25: existence of a full-support transition distribution; the one-feature construction and its assumptions; the general and specialized recurrences for ; a positive lower bound for their coefficient ; and unbounded growth from that lower bound. The numerical inequality retains the report's threshold and its explicit positive factor .
The theorem identifies a limit of using TD(0) with linear approximation when the current states are sampled according to a distribution unrelated to the chain's invariant law. The constructed Markov chain itself has a well-defined zero cost-to-go, and the approximation uses only one nonzero feature direction. Nevertheless, the mean of the parameter sequence diverges for every nonfixed initialization. Thus the issue is present even without noisy costs or a complicated feature space. The report contrasts this with its convergence result for the on-line algorithm under additional assumptions; the counterexample says that those conclusions cannot be transferred to arbitrary independent state sampling by changing only the sample source. Tsitsiklis and Van Roy, §9.
The report proves Theorem 3 on paper. This mission asks for a machine-checked proof of its full quantifier structure, including countably infinite state spaces and arbitrary . A completed development would supply reusable Lean interfaces for countable Markov kernels, path laws, weighted projections, independent state–successor samples, and expected stochastic recurrences. The proposal currently contains the statements and definitions; the theorem proofs are open.
The apparent simplicity of the one-dimensional example hides two issues. First, the statement is uniform over , including distributions that put zero mass on nearly every state. A proof must choose the two feature states in response to while preserving the strict positivity needed for growth. Second, the recurrence concerns , where depends on all earlier random pairs. The step at time uses a fresh pair, and the factorization of its mean requires that temporal independence, plus justified integrability. Writing a positive scalar coefficient alone does not establish divergence of the expected parameter sequence for the sampled process.
The Lean state space is a countable discrete measurable type with at least two elements. is a Markov kernel, its path law comes from the Ionescu–Tulcea construction, and the cost-to-go is the expectation of the discounted path sum. Weighted membership is expressed by summability of . The projection uses the inverse of the weighted Gram matrix under the independence and positive-mass assumptions that make it invertible. Only is needed here. The number of basis functions is existential, like the report's matrix , but must be at least one: an empty parameter space would leave the universal divergence clause with no nonfixed initializations. The report's own example has .
Assumption 1 includes uniqueness of , positive mass at each state, the stationary squared-cost moment, and absolute integrability of the cost-to-go. Assumption 2 includes linear independence and integrability of squared features. Assumption 4 retains square-summability even though the displayed growth argument uses the divergent first-power sum. The general mean recurrence assumes bounded costs and features so its integrals and countable sums are meaningful; the constructed example satisfies those bounds. The goal additionally states finite-time integrability of the parameter vector. The source indexes states by 1 and 2; the formalization uses two distinct states and records the proof's ordering and in the growth milestone. The goal's quantification over probability spaces is restricted to Lean's Type universe.
The general mean recurrence is written with the immediate cost outside the matrix factor multiplying . This follows the algorithm displayed on p. 24 and corrects two slips in the printed recurrence on p. 25: its next-state subscript and the placement of the mean-cost term. Contributions to the path-law facts, independent-sampling calculations, countable weighted sums, and scalar growth theorem all support the same fixed goal.
Many problems in statistics, signal processing and machine learning minimize the sum of a smooth loss and a convex, nonsmooth, separable regularizer: smooth optimization with -regularization, bound-constrained optimization, the group Lasso and, through duality, support vector regression are special cases listed in §1 of the paper discussed below. For such problems, methods that update one coordinate, or one small block of coordinates, at a time are often the method of choice, because each update is cheap and exploits separability.
Paul Tseng and Sangwoon Yun (Math. Program. Ser. B 117 (2009) 387–423) introduced the coordinate gradient descent (CGD) method for this class: at each iteration it minimizes a quadratic model of the smooth part plus the exact nonsmooth part over a chosen block of coordinates, then takes an Armijo step. Their paper proves global convergence (Theorem 1) and, under a local error bound, linear convergence (Theorems 2 and 3). This mission is the second of a three-mission series on the paper; it targets the linear convergence theorem for the cyclic (Gauss–Seidel-type) choice of blocks.
The analysis follows Luo and Tseng's error-bound framework for smooth constrained problems (Ann. Oper. Res. 46 (1993) 157–178), which established linear rates for feasible descent methods without strong convexity. Tseng and Yun extend that framework to a nonsmooth convex term.
Let carry the Euclidean norm , let , and for let be the subvector of coordinates in . The problem (1) is
where , is proper, convex and lower semicontinuous, and is continuously differentiable on an open set containing .
Given , a nonempty block and a symmetric positive definite matrix , the direction (6) is
The CGD method starts at , chooses at each iteration a block and a matrix , computes , and sets . The Armijo rule takes as the largest element of with
with and . The restricted Gauss–Seidel rule (12) asks for indices (the set ) such that the blocks used during each cycle are pairwise disjoint and cover . is block-separable with respect to if .
The analysis uses three assumptions: is -Lipschitz on (22); Assumption 1, with ; and Assumption 2. Writing for the set of stationary points of and for the full direction with , Assumption 2 says (a) and the local Lipschitzian error bound holds on every level set wherever ; (b) stationary points with different objective values are at least a fixed distance apart.
Under (22), Assumptions 1 and 2, the restricted Gauss–Seidel rule, block-separability of with respect to every , and Armijo steps with and :
No rate constant is fixed: the goal asserts the shape of the convergence, so it is not invalidated by sharper constants.
Lemma 4 (Hölder dependence of the subproblem's solution on its linear term), Lemma 5(a) (a per-block variational inequality), Lemma 5(b) (an explicit stepsize at which the Armijo test passes), Theorem 1(f) (Armijo stepsizes bounded away from zero, , ), and Theorem 2(a) (the residual at the start of a cycle is bounded by the step lengths of the cycle).
Theorem 2(b) gives a linear rate for a block coordinate method on a nonsmooth, possibly nonconvex composite problem without strong convexity: the rate follows from the error bound, which holds for a large class of problems studied in §6 of the paper (the third mission of this series).
The theorem is proved in the paper; none of it has been machine-checked, as far as a search of the Prove2Me library shows. Formalizing it requires a reusable treatment of extended-valued convex functions through their effective domains, of the coordinate-restricted proximal subproblem, and of the Armijo rule for composite objectives. The milestones Lemma 4 and Lemma 5 are self-contained facts about this subproblem and are reusable for other proximal coordinate methods.
The classical route to a linear rate, as in Luo and Tseng's smooth analysis, derives from the error bound, where is the limit value. With a nonsmooth this inequality is not available: the authors say so on p. 405, and work with in place of the quadratic term. A second obstacle is that the error bound controls the full residual , while each iteration only computes a block direction at a different point; relating the two over a cycle needs the disjointness of the blocks in the restricted rule and block-separability of . Neither the global analysis nor the error bound alone gives the rate.
is EuclideanSpace ℝ (Fin n), with 0-based coordinates. The extended-valued is encoded as a pair: its effective domain and its finite values on , with "proper convex lsc" given by the published definition ProxNewton.Inexact.IsProperClosedConvex; is never evaluated off , and every statement carries membership in explicitly. The direction is the unique minimizer of (6) when and (chosen by Classical.epsilon), and runs of the method carry the minimizer property itself. The Armijo rule takes the first admissible exponent . is a strictly increasing map with . Stationarity is for all , in liminf form. In Assumption 2, is the infimum distance and "for any " is "for every real " (equivalent, since the condition is empty below ). Q-linear convergence includes convergence of the sequence; R-linear convergence is with . The rates in the goal are along , as the paper states.
Explicit choices relative to the printed text:
A statement that replaces Assumption 2 by strong convexity, claims a rate along the whole sequence rather than along , or asserts the Q-linear contraction without convergence to a limit is not this theorem and is out of scope.
Lemma 1, the claim after (10), Lemma 3 and Theorem 1(a), which the proof also uses, are milestones of the first mission of this series and are not restated here. Theorem 3 (the same conclusion along the whole sequence for the Gauss–Southwell-q rule) is not included: its proof is omitted in the paper. Contributions welcome: proofs of the milestones, and general facts about the coordinate-restricted proximal subproblem (existence and uniqueness of , optimality conditions) that the milestones rely on.
Nonparametric regression estimates the regression function from i.i.d. observations without assuming a parametric form. The simplest such estimates are local averages: to predict at a point , average the responses of the sample points closest to . Nearest neighbor rules of this kind go back to Fix and Hodges (1951) for classification and are still a standard baseline in statistics and machine learning.
Before 1977, consistency results for such estimates assumed regularity of the distribution of : a density, continuity of the regression function, or bounded support. C. J. Stone's paper Consistent nonparametric regression (Ann. Statist. 5 (1977) 595–645) proved that suitable nearest neighbor estimates are consistent in for every joint distribution of with . This property, now called universal consistency, is the subject of the first chapters of Györfi, Kohler, Krzyżak and Walk, A Distribution-Free Theory of Nonparametric Regression (Springer, 2002), where Stone's theorem is the organising result.
This mission formalizes Theorem 2 of Stone's paper, the universal consistency of nearest neighbor weights. Mission I of the series formalizes the general criterion (Theorem 1) that the proof applies; mission III treats conditional quantiles.
Let be i.i.d. random vectors in with an arbitrary law . A weight function assigns to the query point and the sample numbers , . It is a probability weight function if and . Given i.i.d. pairs with real, the estimate of is
The sequence is consistent if, whenever the pairs are i.i.d. with the given law of , and , one has .
Scales and metrics. A scale is a nonnegative function , , and its pseudometric is
The choice gives the Euclidean metric; the sample standard deviations of the coordinates give a unit-free one. The sequence is regular (p. 599) with constants if for every coordinate of with a nondegenerate law, is bounded in probability for any two such coordinates, and condition (7) holds: interchanging and changes by a factor in whenever the th coordinates of do not all coincide.
Nearest neighbor weights. Let with and for . The weight of is
where is the number of other sample points strictly -closer to than and the number at the same distance: the th closest point receives , and tied points share the average of the coefficients of their ranks. The uniform -NN rule is for .
For every law of and every regular sequence of scales,
Uniform, triangular and quadratic -NN weights with , satisfy both conditions (Corollary 3).
Theorem 2 established that a local averaging estimate can be consistent with no assumption on the distribution of beyond the moment condition on . The same argument, through Theorem 1, became the standard template for proving universal consistency of kernel, partitioning and nearest neighbor estimates, and of the classification rules derived from them (Devroye, Györfi and Lugosi, A Probabilistic Theory of Pattern Recognition, 1996). The constant of Proposition 11 is an early instance of the cone-covering bound on how many points can have a given point among their nearest neighbors, a lemma that reappears throughout nearest neighbor theory.
The result is proved (1977), and textbook proofs exist. Mathlib contains no formalization of Theorem 2, of Stone's criterion, or of the cone-covering lemma. A formal development would supply reusable infrastructure: nearest neighbor weights with averaged ties, the exchangeability argument behind Proposition 11, and consistency of weighted averages for i.i.d. data encoded through kernels.
The obvious argument estimates by a continuity argument around , which needs a density or continuity of and is unavailable here. The difficulty is condition (1) of Stone's criterion: a single sample point may be a nearest neighbor of many query points, so is not obviously comparable to for arbitrary and arbitrary (atoms, singular parts, unbounded support). The bound must hold uniformly in and in the distribution, with a data-dependent metric whose scale changes when and are interchanged. Ties in , which have positive probability when has atoms, must be handled by the averaged weights (8), not by an index tie-break.
Points live in EuclideanSpace ℝ (Fin d). The i.i.d. sequence is the coordinate process of Measure.infinitePi, coordinate 0 being ; sample indices are 0-based, coefficients keep the paper's 1-based index. "Whenever the pairs are i.i.d." is encoded by quantifying over every Markov kernel (the conditional law of given ), with pairs distributed as and . Expectations of nonnegative quantities are lower Lebesgue integrals in ; convergence in probability is TendstoInMeasure; limits of probabilities are taken in .
Standing assumptions and additions, each disclosed in the item statements:
No statement corrects the print.
The goal is stated as consistency over all kernels and all , for an unrestricted law : it is not stated through Corollary 1's three conditions nor through , and no density, moment or support hypothesis on is present, so a proof cannot reduce to a special case.
A complete development needs: exchangeability of finite i.i.d. samples under the product measure, the finite cone cover of , the strong law of large numbers (Proposition 9's proof), and Stone's criterion (mission I). Contributions proving any milestone, the cone-cover existence lemma, or the transfer of exchangeability through infinitePi are welcome.
Many prediction tasks ask not for the mean of a response given covariates but for a quantile of its conditional distribution: a median that is robust to outliers, a high quantile that sets a safety stock or a value at risk, or a pair of quantiles that forms a prediction interval. Conditional quantiles are also the Bayes rules for piecewise linear loss, which makes them the decision-theoretic answer to asymmetric prediction costs.
C. J. Stone's 1977 paper Consistent nonparametric regression (DOI 10.1214/aos/1176343886) introduced a single framework for local averaging estimators (nearest-neighbor, kernel and related rules) built from weight functions, and proved that their consistency can be decided from simple conditions on the weights, for every distribution of . Section 7 of the paper extends the framework from conditional means to conditional quantiles: the same weights that estimate define a weighted empirical distribution of near , whose quantiles estimate the conditional quantiles. Theorem 3 says that consistency for the mean already gives one-sided consistency for the quantiles. This mission formalizes Theorem 3 and the results its proof rests on.
Let be independent -valued random variables with common law , and let be real responses such that the pairs are i.i.d. The conditional law of given is a probability measure on .
A weight function assigns to a point and a sample real weights , . A sequence is a sequence of probability weights if for every the weights are nonnegative and sum to . The weights define the regression estimate . The sequence is consistent if, whenever and ,
for every response with i.i.d. pairs as above. Consistency is a property of the weights and the law of alone.
The conditional distribution function is . For the lower and upper th conditional quantiles are
They coincide unless the conditional distribution function is flat at level . The weights estimate the conditional distribution function by , and the quantiles by
Write and .
For a consistent sequence of probability weights and ,
and if and , both convergences hold in . The theorem is one-sided on purpose: when the conditional quantile is not unique, and may oscillate inside .
Theorem 3 transfers every consistency result for conditional means to conditional quantiles at no extra cost. In particular, the nearest-neighbor weights of Stone's Theorem 2, which are consistent for every distribution of , give universally consistent one-sided estimates of conditional quantiles, and when the conditional th quantile is unique, the midpoint estimate is consistent (Corollary 5 of the paper). The theorem is also the input for the consistency in Bayes risk of approximate Bayes rules under piecewise linear loss (Theorem 4, Model 2), which connects nonparametric regression to data-driven decision making such as the newsvendor problem with covariates.
The result has been proved since 1977; it has no machine-checked proof that this mission is aware of. A formalization produces a reusable layer for distribution-free statistics in Lean: weighted empirical distributions, conditional quantiles defined from a Markov kernel, convergence in probability and in of statistics of an i.i.d. sequence, and the moment bounds of Propositions 14 and 15, which hold for every weight function and do not depend on the asymptotics.
The obvious argument fails because the conditional distribution function at is never estimated uniformly. Consistency controls the weighted average only for responses that are a fixed function of the pair; the event involves the random threshold , which varies with the target point while the sample responses are drawn at the sample points . Connecting the two requires a statement about the weights alone, Proposition 4, that holds for an arbitrary Borel function with no continuity or integrability; the conditional quantile function is in general neither continuous nor integrable.
A second difficulty is that convergence in probability does not give convergence in without uniform integrability, and the estimated quantiles are not averages of the . The bound in Proposition 15 must hold for each separately, with a constant independent of , for an estimator defined as an infimum.
Finally, the two-sided statement need not hold when the conditional distribution function has a flat stretch at level , which is why the paper asks for a unique conditional quantile in Corollary 5; a solver should not aim for it.
The i.i.d. sequences are the coordinate processes of infinite product measures, Measure.infinitePi, with coordinate the point (or the pair ) and coordinate the st sample; sample indices are 0-based. The response is given by its conditional law, a Markov kernel from to , and the joint law of a pair is . "Whenever the pairs are i.i.d." in the definition of consistency is a quantifier over all Markov kernels; every joint law with -marginal arises this way. This also provides the independent standard normal variables that the paper assumes on its probability space.
Committed conventions:
TendstoInMeasure.sInf/sSup. For a Markov kernel, , probability weights and , the defining sets are nonempty and bounded on the relevant side, so the values are the paper's; at the estimates are a junk value that no limit statement sees.Corrections and choices of range. Proposition 14 is printed for . The proof of Theorem 3 applies it for every , and the statement is posed for . Proposition 15 leaves unquantified and is posed for , the range Theorem 3 uses.
A goal stated through the probabilities of Proposition 13, or through truncated moments, would be a different and weaker theorem; the goal states convergence of the quantile errors and themselves, in probability and in . Swapping the negative and positive parts gives a false statement.
Corollary 1 (necessity) is a special case of Theorem 1, the goal of the first mission of this series; it is posed here as a milestone so that this mission is self-contained, and can be replaced by a reference once that mission is published. Contributions are welcome on any milestone, and on general infrastructure for Markov kernels, conditional distribution functions and quantiles, which is reusable beyond this mission.
Primal-dual interior-point methods are the standard algorithms for linear, second-order-cone and semidefinite programming. Their best-known variants keep the iterates in a narrow neighbourhood of the central path and take short or moderately long steps whose length is fixed in advance. Practical codes instead take long steps and recentre only when needed. Nesterov and Todd (SIAM J. Optim. 8 (1998) 324–364) developed a common theory of primal-dual methods for all self-scaled cones, the class that contains the nonnegative orthant, the second-order cone, the cone of positive semidefinite matrices, and their products. Section 7 of that paper analyses a predictor-corrector method whose neighbourhood is defined by the functional proximity measure , the conic version of the Tanabe–Todd–Ye potential. The predictor may move arbitrarily far from the central path, as measured by , and a Newton corrector brings the iterate back.
Timeline:
Let with the Euclidean inner product, and let be a closed convex cone that is pointed and has nonempty interior. Its dual cone is . A -self-concordant logarithmically homogeneous barrier for is a self-concordant function on that tends to at the boundary and satisfies and . Its conjugate is . is self-scaled if, for all , and . For and , the scaling point satisfies .
The problem is with dual , where is surjective. A triple is strictly feasible if , and both equality constraints hold. With the functional proximity measure is
and it vanishes exactly on the central path. The neighbourhood is . The affine-scaling direction solves , , . The centering direction solves the same system with right-hand side . One Newton step moves by , with , where is the uniform proximity measure and .
One iteration of Algorithm 7.1 starts from . It takes the largest predictor step along the affine-scaling direction with , then applies Newton steps until the iterate is back in .
Let with and . There are constants , depending only on and , such that one iteration of Algorithm 7.1 on any self-scaled cone satisfies
and the corrector reaches after Newton steps, where . The constants are left existential, as on the page.
In the paper's order, the milestones are:
Theorem 7.1 gives an iteration bound for a method whose predictor neighbourhood can be as wide as desired, with a bounded number of corrector steps per iteration. Inequality (7.3) also lets the step adapt to the problem: in the paper's normalisation the predictor step is at least of the order of the square root of the maximal feasible step. The same bounds apply to the narrow-neighbourhood predictor-corrector method of Section 6. One theorem covers linear, second-order-cone and semidefinite programming, with no reformulation through matrices.
The result is proved in the paper. No machine-checked proof of it, or of any of the self-scaled-barrier estimates it rests on, is known. Formalizing the proof produces a reusable library of local norms, σ-measures and third-derivative bounds for self-scaled barriers, and of the proximity measures of primal-dual methods.
A naive argument would bound the predictor step with the usual self-concordance estimate . That bound loses a factor and cannot give (7.2) or (7.3). What is needed is the sharper self-scaled bound (3.14), in which one factor is the smaller norm . It in turn depends on the cone being self-scaled: must be negative semidefinite for , and the scaling point must exist. The other obstacle is that the change of along the affine-scaling direction must be computed exactly, not just estimated. That is the parallelogram rule (Theorem 3.11), an identity special to self-scaled barriers. The corrector bound needs a lower bound on the Newton decrement that holds uniformly outside , which (4.28) supplies.
Spaces. The dual space is identified with through the inner product. Which local norm is meant is carried by the function used:
lnorm G v u and dnorm G v u, with or ;sigma C c u , with the cone and the centre fixed by the paper's four cases.Each two-form measure uses its first printed form.
Standing assumptions. Every statement assumes that is a proper cone and that is a -self-scaled barrier, and it also states , which the paper derives. The barrier includes explicit nondegeneracy of , which also follows from the other axioms. The conjugate is a supremum over and is only evaluated on . Assumptions (2.4)–(2.5) are implied by the strictly feasible points that the statements start from.
Scaling points, directions and steps are predicates given by their defining equations; nothing is computed by inverting a matrix.
Corrections to the page. Two printed slips are corrected, and both are disclosed:
Ruling out trivial versions. The goal does not assume any of the following; they are milestones, not hypotheses:
The constants are quantified before the cone, the barrier and the data, so they cannot depend on them. The predictor step is the largest step whose whole segment stays strictly feasible.
Out of scope. No self-scaled barrier, existence of scaling points (T*3.2 of [NT97]), or result of Nesterov–Nemirovskii is formalized here. These and the central-path duality theorem (Theorem 4.1) are external results. Proofs that build them are welcome, as is a non-vacuity witness for the goal on the orthant of .
A random discrete distribution is a random sequence of frequencies with . Such sequences model the relative sizes of species in a large population, of allele classes in population genetics, of cycles of a random permutation, of prime factors of a random integer, and of the excursion intervals of a Brownian motion or Bessel process. The two-parameter Poisson–Dirichlet family , , , contains Kingman's one-parameter law (Ewens sampling formula, random permutations) and the law of the ranked jumps of a stable subordinator. It is the reference prior in Bayesian nonparametrics (the Pitman–Yor process) and the reference model in the combinatorics of random partitions.
J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator (Ann. Probab. 25 (1997)), extend what was known for and to the whole family. This mission formalizes one of their results: an identity (Proposition 19, p. 867) that describes the law of the largest frequency under through the law of the largest frequency under .
Timeline. McCloskey (1965) showed that sampling from discovers the frequencies in the stick-breaking order of independent variables. Dickman (1930) found the distribution of the largest prime factor; Vershik (1986) recorded it as the case , of an equation of this form. Engen (1978) introduced the two-parameter stick-breaking scheme for . Perman, Pitman and Yor (1992) and Pitman (1996) proved that this scheme is the size-biased permutation of the ranked frequencies for the whole parameter range (Proposition 2 here). Pitman and Yor (1997) derived (52) for all , .
Fix and . Let be independent random variables, having the beta distribution , with density on for , . Break a stick of length one:
Let be the ranked values of the pieces . The law of is (Definition 1, p. 857); denotes probability for this construction.
A random variable is a size-biased pick from if for every : it is the frequency of the species of an individual drawn at random. A size-biased permutation continues the sampling without replacement, (2) and p. 857. A sample from is a random index with (113).
In Lean all sequences are ℕ → ℝ, 0-based (V ω 0 is ); the objects are stick, ranked, IsStickLaw, HasPD, IsSizeBiasedPick, IsSizeBiasedPerm, IsSample, deleteAt, insertAt in the namespace PoissonDirichlet.MaxDensity.
For , , the variable lies in almost surely and
The result. The law of under has no closed form. Identity (52) is a functional equation in the parameter: on the last factor equals one and the density is explicit; on it is expressed through the law of under on . Specialised to , it is Dickman's equation for the largest prime factor of a random integer and for the longest cycle of a random permutation. The size-biased tools of the milestones (Corollary 3, (6), Propositions 34 and 35) are the standard way to compute with and its partition structure.
Formalizing it. All results here are proved in the literature; none is formalized. Mathlib has the beta distribution, infinite product measures, independence and conditional expectation, but no random discrete distributions, no ranking of a countable sequence, and no size-biased sampling. The mission produces these objects and the first theorems about them: the identification of the stick-breaking scheme with the size-biased permutation of the ranked frequencies (cited by the paper, not proved there), the structural distribution, and the density identity.
The obvious obstacle is Proposition 2: the identification of the stick-breaking order with the size-biased order of the ranked values is a statement about conditional probabilities given an infinite sequence, it is only cited in the paper, and its proof (Perman–Pitman–Yor, Pitman) goes through exchangeable partitions or Poisson point processes. Everything else in the mission rests on it. A second obstacle is the events themselves: coincides with only because the pieces are almost surely distinct, and conditioning on needs the independence of the renormalised tail from , which is not a pointwise identity but a statement about infinite product measures. Reading (52) off the page as a pointwise identity of densities is not enough: densities are defined only almost everywhere.
The parameter range , of Definition 1 is a hypothesis of every statement; is included. A sequence "has the distribution" (HasPD) if it is a.e.-measurable and, for some law of independent beta variables as in Definition 1 (IsStickLaw), for every measurable . Ranked values are defined with Set.encard, so infinitely many large terms are never counted as zero. Conditional probabilities are conditional expectations of indicators; size-biased picks, permutations and samples are measurable random variables, an assumption the page makes implicitly. Expectations of nonnegative functions are lower Lebesgue integrals. The density identity is an equality of measures on Borel subsets of , with two probability spaces for the two parameter values. Indices are 0-based. Insertion (p. 881) is defined with the index for the shifted tail, where the page prints .
The formalization rules out the trivial readings: no Measure.map of a possibly non-measurable map (which would be the zero measure), no Set.ncard in the ranking, no Bochner integral of a possibly non-integrable function (whose value would be ), no limUnder, and no dropped parameter range. Corollary 3 quantifies over every pick from every sequence, not over the stick-breaking construction where it is the hypothesis. A sorry-free check shows that IsStickLaw is inhabited for every admissible , so HasPD is not vacuous.
Contributions are welcome at every level: measurability of ranked, the law of the renormalised stick tail (infinite product measures), Proposition 2 through exchangeable partitions, and the recursion of the uniqueness statement, which is pure measure theory. The definitions are reusable by the other missions of this series.
Random discrete distributions — a random sequence of nonnegative frequencies summing to one — model the relative sizes of species in a population, of cycles in a random permutation, of excursion intervals of a Markov process, and of clusters in Bayesian nonparametric models. The two-parameter Poisson–Dirichlet law is the family that contains Kingman's one-parameter law (Ewens sampling, random permutations) and the law of ranked excursion lengths of a stable subordinator. J. Pitman and M. Yor, The two-parameter Poisson–Dirichlet distribution derived from a stable subordinator (Ann. Probab. 25 (1997)), developed its distribution theory systematically. In Bayesian nonparametrics the same family appears as the Pitman–Yor process prior.
A basic quantitative question about any random discrete distribution is the size of its -th largest atom. This mission formalizes the paper's answer for : every moment as one explicit integral.
Timeline. The moment formula for (Corollary 18 below) was known before 1997 (references [63, 73, 25, 50] of the paper). The Laplace transform of under was obtained, in different settings, by Darling (1952) and Lamperti (1961) for and by Wendel (1964) for . Perman, Pitman and Yor (1992) proved that has density a constant times relative to . Pitman and Yor (1997) combined these into Proposition 17.
Fix and . Let be independent with , the law with density on . Break a unit stick:
and let be the ranked values of the . The law of is (Definition 1); denotes expectation under it.
For and the paper introduces
Under the local time exists almost surely. From one derives , (with ) and . Finally
The Lean declarations Xseq, pdConst, and expIntE are in PoissonDirichlet.Moments; the other objects come from the frozen shared PoissonDirichlet.Ratio and PoissonDirichlet.Wendel modules.
For , , with , and ,
Two consequences close the list: (50), , and Corollary 18, the formula
The ranked frequencies of have no tractable joint density; their one-dimensional laws are known only through transforms. Proposition 17 makes every moment of computable by a single quadrature, for all parameters at once. It yields the large- decay (50), in mean, and recovers the classical formula in the limit . The intermediate statements, the conditional Wendel formula and the joint moments , are used elsewhere in the paper (Proposition 16, Lemma 29).
All statements are proved in the 1997 paper, except Proposition 14, which the paper quotes from Perman, Pitman and Yor (1992). To our knowledge none of them has been machine-checked. A formal development would produce the first verified construction of the Poisson–Dirichlet family in Lean, together with reusable facts about stick-breaking with beta variables, ranked rearrangements of sequences, and the Laplace-transform representation of negative moments.
The identity (86) and the final integration are elementary. The difficulty lies upstream. The naive route, computing from the stick-breaking definition, fails: is the -th ranked value of the , and ranking destroys the product structure of the beta variables. The paper instead works under , where the ranked sequence is the normalized sequence of points of a Poisson random measure (equivalently, transformed arrival times of a unit Poisson process). Proposition 14 is itself a deep change-of-measure result about stable subordinators, and the existence of the local time is an almost sure limit theorem. Neither has any counterpart in Mathlib.
Sequences are indexed from in Lean: the paper's is V ω (n-1), and statements "for " quantify over k : ℕ with . is defined exactly as Definition 1, with independent beta coordinates (Mathlib's betaMeasure) and the ranked values defined with Set.encard. The law is stated through preimages, so no measurability of the ranking map is presupposed. The local time is carried as a random variable together with its defining almost sure limit (24). Expectations of quantities that may be infinite are lower integrals. The conditional expectation of Proposition 26 is stated through its defining property, for every nonnegative measurable test function of . The parameter ranges , (and at ) are hypotheses wherever the page has them. Two hypotheses are added and disclosed: in Proposition 17 and in Lemma 27. Without them the printed -integrals diverge and is evaluated at a pole or a negative argument, while the left sides are finite. Both follow from the printed hypotheses when (resp. ).
Trivializing encodings are ruled out: no law is written as an image measure of a possibly non-measurable map, no count uses Set.ncard, no limit uses limUnder, is not defined as , and every Bochner integral in a statement is of an integrable function under the stated hypotheses, so no statement holds because of a junk value .
A complete development needs: infinite products of beta laws, the ranked rearrangement and its measurability, the Poisson-process representation of (Proposition 10), and the change of measure of Proposition 14. These are reusable beyond this mission. Proofs of the general identity (86), of the gamma–independence milestone, and of Lemma 27 from its milestones are welcome independently.
A value for cooperative games assigns to every game a payoff vector, chosen by axioms rather than by bargaining. Shapley's value (1953) does this for finite games with side payments, and Aumann and Shapley (Values of Non-Atomic Games, 1974) extended it to games with a continuum of players, where it is given by a diagonal formula: a player's value is the average of their marginal worth along the diagonal from the empty coalition to the grand coalition. Aubin's Cooperative Fuzzy Games (Math. Oper. Res. 6(1), 1981, doi:10.1287/moor.6.1.1) brings this formula to finitely many players who may participate in coalitions at fractional rates, and characterises it by axioms in §8.
The result matters in cost allocation: the Aumann–Shapley price mechanism (Billera, Heath and Raanan 1978; Mirman and Tauman 1982) shares the cost of a bundle of products by exactly this diagonal formula, applied to a smooth cost function of the quantities produced. Theorem 8.1 is the finite-player, fuzzy-coalition version of the axiomatic justification behind that mechanism.
There are players . A fuzzy coalition is a vector , where is the rate at which player participates; an ordinary coalition is its indicator vector , and is the grand coalition.
A smooth fuzzy game is a coalitional worth function that is continuously differentiable and satisfies . These form the space , a Banach space under the norm .
A sequence of fuzzy values is a family of continuous linear operators satisfying three axioms.
The core of a game with side payments is the set of with and for every (§2 (4)).
There exists a unique sequence of fuzzy values, given by the diagonal formula
For every linear with ,
where is the transpose of . If is concave and positively homogeneous, then is the unique element of the core.
These are the steps of the proof in the paper (pp. 10–11), in attack order:
The result. Theorem 8.1 singles out the diagonal formula among all ways of valuing smooth fuzzy games, using only efficiency, anonymity and invariance under merging players into types. Property (5) shows that the value transforms correctly under every linear change of coordinates fixing the grand coalition. The core statement links the value to stability: for concave homogeneous games (for instance, market games), the value is the only allocation no fuzzy coalition can improve upon. Through Owen's extension, the classical Shapley value is recovered as a special case.
Formalizing it. The theorem is proved in the paper, briefly, and its proof leans on an unproved density claim and on a short appeal to atomicity. A formalization makes the uniqueness argument complete: in particular, how atomicity, which only allows nonempty types, determines the value of a monomial in which some player has exponent . No machine-checked version of the Aumann–Shapley diagonal formula or its axiomatisation is known to us. Mathlib has the Stone–Weierstrass theorem for continuous functions but no density of polynomials on a cube; the latter is reusable well beyond game theory.
Existence (milestones 1–2) is calculus: differentiation under the integral sign and the chain rule. The difficulty sits in uniqueness. The first idea, computing on monomials by symmetry alone, fails as soon as the exponents differ: symmetry relates only games that are permutations of each other. Atomicity relates games with different numbers of players, and its types must be nonempty, so a player with exponent cannot simply be merged away. Uniqueness on all of then needs density of polynomials in the norm, not merely the uniform norm: without continuity in the norm, linear maps that agree on polynomials can disagree elsewhere, and the theorem is false.
Fin n, fuzzy coalitions and payoff vectors are Fin n → ℝ, and the cube is Set.Icc 0 1 in the product order.Fin n → Fin m. The symbols are .Supermodularity.Cooperative.ShapleyValue, whose formula is (7) re-indexed by . The Cornet extension of the same remark is left out because it is not on the boundary of the cube.Infrastructure that a complete development needs, and that is welcome as separate contributions: approximation of functions on a cube by polynomials; differentiation under the integral sign for the diagonal integral; Euler's identity and the supergradient inequality for concave homogeneous functions.
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).
Random equations of the form , with a random function independent of , describe the stationary laws of many stochastic recursions: perpetuities in insurance and finance, the stationary law of ARCH-type volatility models, random difference equations , and the stationary workload of certain queueing and storage models. When acts like multiplication by a random variable for large , and for some , the solution has power-law tails: . This is the implicit renewal theorem of Goldie (Ann. Appl. Probab. 1991, Theorem 2.3), which recovers and extends Kesten's 1973 theorem on random difference equations.
A tail asymptotic alone says nothing about how fast approaches . For tail estimation, for the accuracy of extreme-quantile approximations used in risk management, and for second-order regular variation, the rate matters. Section 3 of the same paper answers this: under an exponential moment condition slightly beyond the Cramér condition, the error has an explicit second-order term determined by the zeros of , where is a tilted law of , plus a remainder .
Timeline: Kesten (1973) proved power tails for random difference equations; Grincevičius (1975) developed an implicit-renewal approach; Stone (1966) decomposed exponentially decaying renewal measures into an absolutely continuous part with explicit asymptotics and a finite part; Ganelius (1962) proved the Tauberian remainder theorem used to unsmooth; Goldie (1991) combined these into the rate result formalized here.
Let be a probability space carrying independent real random variables and . Fix with (the Cramér condition, (2.3)) and with (3.3).
The tilted law of is the probability measure on , computed on . Its transforms are for real and for complex ; for a function , . Convolution powers are , , and the renewal measure is . A law is spread out when some convolution power has a nonzero absolutely continuous component; (3.4) asks this of the conditional law of given .
Set and
with and defined the same way for the lower tail. The strip is , and denotes a positively oriented closed contour in enclosing every zero of in .
If, in addition, for some , with , absolutely continuous and , and on , then implies
with the analogous statement for ; and if with independent of , the integrability hypotheses may be replaced by . The theorem also asserts that is a spread-out probability measure.
Theorem 3.2 turns the first-order tail asymptotic of the implicit renewal theorem into an expansion: the second-order terms are finitely many terms of the form times oscillating factors, one family for each zero of with , and their form does not depend on the unknown law of . It applies to every random equation covered by the implicit renewal theorem once the stronger moment condition holds, including perpetuities and the random difference equation. Theorem 3.1 is of independent use: it is an explicit-rate version of Stone's decomposition of renewal measures with exponential moments.
The results are proved in the paper; none is formalized. Mathlib has the Fourier transform on the real line, convolution of measures, and rectangle Cauchy theorems, but no renewal theory, no Stone decomposition, and no Tauberian remainder theorem. Formalizing the mission produces a machine-checked renewal density expansion and a checked Beurling–Ganelius theorem, both reusable outside this paper.
The first-order theorem follows from the key renewal theorem applied to . That route gives no rate: the key renewal theorem has no remainder, and the integrability hypothesis yields but not , so a remainder cannot be read off directly even with a spread-out step law. The proof therefore works with a smoothed version of , where Stone's decomposition with the contour expansion of the renewal density gives an remainder, and has to unsmooth. Unsmoothing is the Tauberian step: it requires a one-sided regularity condition on the unsmoothed function, verified for and for the contour term, and costs half the exponent. The contour expansion itself requires showing that has finitely many zeros in the strip and handling their orders through residues.
All objects live in the namespace GoldieRenewal.Rates. Random variables are measurable maps on a probability space; almost surely; independence is IndepFun. Tail probabilities are real numbers P.real {ω | t < R ω}. Moments such as and are lower Lebesgue integrals in . The transforms and are Bochner integrals at complex arguments with the sign of the paper. Asymptotic statements use Asymptotics.IsBigO and IsLittleO along atTop.
The contour. A contour is the positively oriented boundary of an axis-parallel rectangle whose closure lies in and whose interior contains every zero of in ; the contour integral is the sum of the four edge integrals (RectangleIntegral, from the published ResidueCalcOnRectangles_defs). Expansions are stated for every such rectangle.
The variable in (3.8) and (3.10). The paper prints in the contour term, but its proof establishes the expansion in the logarithmic variable . The targets are stated with , which is what the proof gives. With the printed the contour term would decay exponentially and the statement would claim , which is not what is proved. Hypothesis (3.7) is printed with and is read with .
Excluded trivializations. The contour term may not be dropped; the hypotheses do not exclude zeros of in ; and the contour must enclose all zeros in the strip, not a chosen subset.
Theorem 9.6 is stated for a complex-valued kernel and a finite strip width ; the application with follows by restricting to a finite strip. Lemma 9.5 carries an added hypothesis that the density of has compact support, which the proof uses and the application provides.
Contributions welcome: renewal-measure infrastructure (convolution powers, Blackwell-type limits), Fourier analysis of measures at complex arguments, residue computations on rectangles, and Tauberian remainder theory. Each is reusable well beyond this paper.
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.
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:
A finite Markov chain describes a system that changes state according to fixed transition probabilities. For a chain that settles toward an equilibrium distribution, a central question is how quickly the effect of its starting state disappears. The logarithmic Sobolev constant supplies quantitative control of this convergence and, through hypercontractive estimates, also governs how the continuous-time transition operator changes the size of functions measured in different norms. Diaconis and Saloff-Coste's 1996 paper develops these relations for finite chains and uses them to study mixing on graphs and product spaces.
The constant can be hard to calculate directly. Its definition is an infimum over all nonconstant functions, while a particular Markov semigroup may admit an accessible bound from to at one time. Theorem 3.9 turns such an operator estimate into a numerical lower bound for the log-Sobolev constant. This mission formalizes that result, including both finite and the supremum-norm endpoint.
Let be a finite state space. A Markov kernel is nonnegative, with for every . A strictly positive stationary distribution satisfies and . The chain is reversible when for every pair of states. Its continuous-time heat semigroup is , acting on a function by . These conventions follow §§2.1–2.3 of the source paper.
For a real function on , write when is finite, and . The Dirichlet form is . The quadratic entropy functional is , with a zero contribution where . Write and .
The spectral gap in this mission is the variational constant , as in (2.4). The log-Sobolev constant is , as in (3.1). These definitions specify the quantities that Theorem 3.9 relates; in particular, is the paper's variational quantity, rather than an eigenvalue expression imported from a different convention.
Suppose , , and satisfy for every function . The paper's theorem asserts
It also covers : the hypothesis then uses , and the two fractions involving in the displayed bound become .
Theorem 3.10 replaces in the norm hypothesis with , where sends a function to its constant mean. Corollary 3.11 relates to , the first time at which every heat-kernel density is within of in :
The three milestones reproduce the interpolation estimate (3.6), the resulting entropy inequality, and the centering inequality (3.7). Theorem 3.10's printed finite- denominator contains ; its displayed proof and the use in Corollary 3.11 require . That proof also needs , which the page does not state and without which the printed statement fails on a four-state product chain. The formal companion records both corrections, while the main goal follows the printed Theorem 3.9 exactly.
Theorem 3.9 makes a norm bound at a chosen time useful beyond that time: it yields a bound on a functional inequality that holds for every function on the state space. Thus estimates obtained from an explicit heat kernel or another analytic method can be compared across chains using the same constant . The centered version and the bound for connect this functional viewpoint back to convergence from a point mass, as the paper explains in §3.4.
The mathematical results are proved in the 1996 paper. Here the remaining work is to give their finite-state objects, norm hypotheses, and constants machine-checked meanings, then formalize the proofs. The definition layer and the centering inequality have use beyond this mission: they can support other statements about entropy decay and heat-kernel convergence in the same paper.
A bound for in the same norm is too weak to recover the displayed lower bound: the information here is the change from an input to an output. The dependence of the exponent on time must retain the factors and exactly. The endpoint also requires a separate norm statement, since a real exponent cannot represent infinity. The centering inequality (3.7) is another substantial step; the paper points to earlier proofs rather than treating it as immediate.
The state space is a finite Lean type, the kernel a real matrix, and the invariant law a positive real-valued probability vector. Reversibility is detailed balance, and irreducibility is retained from the standing setting of §3.1. The heat semigroup uses the already published Poissonized heat kernel. Operator norms are represented by inequalities quantified over every real function. The finite- and conclusions are separate clauses of the goal. Time is real; makes explicit the positive-time convention used in §3.4. Theorem 3.10 carries the condition (and ) described above; Corollary 3.11 is stated without any extra condition.
The variational constants are real infima, the logarithms and real powers use Lean's total operations, and the supremum norm is a supremum over the finite state space. The stationary probability hypothesis rules out an empty state space; the operator hypothesis on the constant function forces in Theorem 3.9. These facts prevent the bound from arising from a zero norm, an empty operator test, an invalid logarithm, or an eigenvalue convention different from (2.4). Useful contributions include finite-state entropy inequalities, interpolation machinery, estimates for the heat operator, and proofs of the three stated milestones.
An oracle lets an algorithm ask for the value of a function without giving it a description of that function. An oracle lower bound isolates how many questions are needed, even when computation between questions is unrestricted. Bennett, Bernstein, Brassard and Vazirani used this viewpoint to compare classical and quantum access to randomly chosen functions and permutations. Their Theorem 3.6 states an almost-sure separation: relative to a random permutation oracle, a quantum machine using time cannot capture all of BBBV, Theorem 3.6. The same paper notes that its exponent may reflect the available argument rather than the true boundary BBBV, p. 12.
The finite statement behind that separation is a quantum query lower bound for a uniformly random permutation. It asks about one bit of the inverse image of a fixed string, rather than inversion of the whole permutation. This gives a sharply defined target with the paper's explicit query and error constants.
Let , and let be a permutation oracle of . Its inverse image of the all-one string exists and is unique. Define the language by putting in when the first bit of is . The paper observes that access to puts this language in both and : either possible bit of the inverse image can be witnessed by an input to the permutation BBBV, p. 10. This mission tests membership only at .
A -query quantum algorithm starts in a unit vector of a finite complex Hilbert space. A basis configuration records an optional length- query string, an answer register, and finite workspace. On a querying configuration , an oracle operation replaces the answer register by ; it leaves a nonquerying configuration unchanged. Each oracle operation is followed by an algorithm-chosen unitary. The final acceptance probability is the sum of the squared amplitudes of accepting basis configurations. A run decides a yes-or-no question if its acceptance probability is at least on a yes instance and at most on a no instance. These thresholds match the paper's bounded-error convention BBBV, §2 and §3.1.
For a state , the query magnitude is the total squared amplitude of basis configurations querying string . Thus for a unit state, and the magnitudes over all strings sum to at most . This is Definition 3.2 of the paper BBBV, p. 7.
The goal is the finite claim in the proof of Theorem 3.6. For every , every finite-workspace algorithm with queries, and a uniform permutation of ,
The milestones follow the statements used in the paper: Theorem 3.1 relates Euclidean distance between final states to their observed distributions; Theorem 3.3 bounds the effect of changing answers at queried strings; and the proof of Theorem 3.6 establishes the uniform transposition chain, the membership split, the expected query-magnitude estimate, and the expected final-state distance BBBV, pp. 7–11. The source text of each milestone is recorded with its page in the mission's milestone list.
The result identifies a concrete task that cannot be decided reliably with too few quantum oracle calls for a positive fraction of length- permutation oracles. The inverse image exists by definition, so the obstruction is the number of queries needed to learn its first bit. This is the quantitative part of the paper's relative separation for ; the passage to an almost-sure statement over countably many machines is described in the paper but lies beyond this mission's formal goal BBBV, pp. 10–12.
The theorem is proved on paper and is not claimed here as an open mathematical problem. Formalizing it produces reusable finite-dimensional machinery for quantum queries: an XOR oracle as a unitary basis permutation, query magnitude, a time-dependent hybrid oracle, and counting-based probability over finite permutation spaces. The milestone statements remain open Lean proof obligations in this proposal.
A direct comparison of an algorithm's run under two nearby permutation oracles requires knowing that the algorithm seldom queries the locations where those oracles differ. The distinguished preimage cannot simply be declared rarely queried: learning about it is exactly the task under study. The paper therefore studies a chain of random transpositions and a run whose oracle changes by step. The subtle point is that a string used in a later transposition is still uniform when the earlier query state is formed BBBV, pp. 10–11. The expected query-magnitude milestone states that point explicitly.
The Lean carrier of strings is . Algorithms use finite configuration types and EuclideanSpace ℂ; the query register is optional, and none represents configurations that make no length- query. An oracle answers with the full length- value by XOR in the answer register. The paper describes a Boolean oracle, but one full-value query can be simulated with Boolean queries and one Boolean query with two full-value queries. The latter direction transfers this lower bound to the paper's oracle at a changed constant. Answers at lengths other than are fixed and absorbed into the inter-query unitaries, as in the paper's finite-length argument. The full oracle quantum Turing machine, complexity classes as Lean objects, and the almost-sure conclusion are outside the model.
Probabilities and expectations are finite counting fractions. The chain samples a uniform and independent uniform , with ; this has the same joint law as the paper's conditional sampling order. The recurrence uses the paper's composition direction. The first-bit test requires , and any comparison to requires . The goal quantifies over every finite workspace and algorithm before sampling the permutation. A uniform function in place of a permutation, or a predetermined inverse image, would change the task and is excluded.
The paper's Theorem 3.3 prints a final-state bound that fails for a one-query XOR example; the milestone states the valid bound. Its baseline oracle may vary by step because the proof of Theorem 3.6 uses the hybrid run. The explicit constants , failure probability , and expected distance remain as printed. General finite-dimensional unitary and probability lemmas, together with a proof of the time-dependent hybrid bound, are welcome contributions. The finite query model and transposition-chain definitions are reusable in other oracle lower bounds.
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.
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.