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?
Linear programming asks for the best value of a linear objective subject to linear equations and inequalities. Primal-dual interior-point methods seek feasible primal and dual solutions while keeping every constrained coordinate positive. The resulting pair has a measurable gap between its objective values, so an algorithm can stop when the gap is below a chosen precision. Mizuno, Todd, and Ye studied methods that adjust the length of each step according to the current point. Their technical report gives a predictor–corrector algorithm whose worst-case iteration count grows on the scale of the square root of the number of variables times the requested precision parameter Mizuno, Todd, and Ye, Cornell ORIE Technical Report No. 944, pp. 6–9.
The result matters to readers who need a mathematical guarantee for an adaptive step rule. The algorithm takes one predictor step that reduces the gap and then one corrector step that recenters the pair. Its step length is defined by remaining inside a specified neighborhood, rather than by a fixed schedule. The theorem connects that local rule to a global termination bound.
Fix an integer of variables, an arbitrary number of equality constraints, a real matrix , and vectors and . The primal problem minimizes over , . Its dual problem maximizes over , . The dual slack is . The development reuses a published general-form LP model and specializes it to this pair.
The strictly feasible pairs are the pairs satisfying the two feasibility systems for some dual multiplier , with every coordinate of and strictly positive. The multiplier is allowed to vary with the pair. Write , , and for the vector of ones. The duality measure is . For , the Euclidean central-path neighborhood is
The search direction at with parameter solves the three equations , , and . A step of length yields . Algorithm 1 begins in . It takes a predictor direction with to the greatest step whose entire path remains in , then takes one full corrector direction with . The resulting pair starts the next iteration. The algorithm stops when ; its starting gap is at most report, pp. 4 and 6–7.
For every real precision parameter , every run following Algorithm 1 from an allowed starting pair reaches the stopping threshold at some iteration with
The paper states the iteration order as . The explicit ceiling records the count given by its proof without allowing an unspecified constant to depend on the LP instance report, Theorem 1, pp. 8–9.
The supporting targets are equations (4)–(5), Lemma 1(a), Lemma 2(a)–(b), Lemma 3, Lemma 4, and the contraction displayed in the proof of Theorem 1. They cover the duality measure along a step, bounds on the scaled second-order term, preservation of the inner neighborhood, the predictor step length, and the per-iteration reduction. The milestone list follows the order in which these facts enter the report's analysis report, pp. 4–9.
Theorem 1 gives a stopping guarantee for a fully specified adaptive predictor–corrector method on a feasible primal-dual LP pair. In particular, the requested precision can grow while the iteration bound scales with , rather than with , in this neighborhood model. It also gives a quantitative reason to track two neighborhoods: the predictor may leave the inner one, while the corrector brings the iterate back for the next round.
The report proves this mathematical claim, but this mission does not assert that its proof has already been machine checked. A completed formalization would supply reusable Lean definitions for strictly feasible LP pairs, Euclidean centrality, search directions, and algorithmic step relations. Solvers may formalize the report's argument or another proof of the same statements; the audited goal and milestones fix the mathematical contract.
The predictor direction is aimed at reducing the duality measure, but a long step can move the componentwise products away from their common average or make a coordinate nonpositive. The corrector recenters the pair, yet its effect must be controlled in the same Euclidean neighborhood. A gap decrease alone therefore does not imply that another iteration can be taken. The central difficulty is to establish both a nonzero admissible predictor length and preservation of strict feasibility and centrality under the full corrector step.
Vectors are functions on Fin n, and is a finite matrix. The report's indices correspond to Lean indices . The norm in and in Lemmas 1–2 is explicitly : Lean's default norm on functions is a supremum norm. All powers of two use real exponents, and is natural logarithm. The hypothesis gives meaning to ; no sign condition on is imposed, since for the starting pair already meets the stopping test.
The source's “largest” predictor step is represented as an attained greatest element of the admissible set, with admissibility required throughout the step interval. Some interior points have admissible intervals without a greatest member. In particular, at there may be no continuing run under this literal algorithm rule; the goal retains and makes this limitation explicit. The denominator in Lemma 4 can vanish. The formal lower bound uses its limiting value in that case, avoiding a zero returned by Lean's total division. The separate contraction milestone assumes , because its printed lower bound on the predictor length fails at .
The definitions keep primal feasibility, an existential dual multiplier, coordinatewise strict positivity, and the three direction equations visible. A sequence is constrained by the transition relation whenever its gap exceeds ; values after stopping play no role. These conditions exclude trivial encodings in which the gap threshold is built into the run or centrality is measured with the wrong norm. The remaining work includes Euclidean finite-sum estimates, positivity along steps, and the iteration-count argument. The LP specialization and norm infrastructure can be reused in further interior-point developments.
Manufacturers of perishable goods must decide how much inventory risk to leave with retailers. A retailer who pays for every ordered unit may order less than is best for the manufacturer and retailer together; a generous return policy changes that incentive. Pasternack studies this question in a single-period setting, with a fixed selling price, uncertain demand and goodwill costs when customers cannot be served. The article identifies two familiar endpoint policies that fail: no returns, and unlimited returns reimbursed at the full wholesale price. It then investigates partial credit as a way to align the order decisions. Pasternack (1985)
The target here is the article's paired Theorems 1 and 2. They concern one retailer and one manufacturer, and their conclusion is about the order quantity the retailer chooses. The model does not ask the retailer to choose the selling price, nor does it compare realized profits for one particular demand outcome. The value of the result lies in ruling out two whole classes of pricing and return terms before considering how to divide the gains from a coordinated channel. Pasternack (1985), pp. 169–171
A manufacturer produces at unit cost and charges the retailer a wholesale price . The retailer orders units before observing demand , then sells at a fixed retail price . Unsold units have salvage value . A return policy gives the retailer a credit for a fraction of the order: permits no returns and permits returns of every leftover unit. The retailer incurs goodwill cost for each unmet unit of demand; the manufacturer bears the additional cost , and is the total goodwill cost. The paper assumes and . Pasternack (1985), pp. 169–170, (1)–(2)
Demand is described by a density on the nonnegative reals and distribution function . From the same order and demand outcome, the paper computes three expected profits: for an integrated company store, for the independent retailer, and for the manufacturer. Their definitions are equations (3), (6) and (8). An optimal order maximizes the relevant expected profit over nonnegative . The paper calls the channel coordinated when the retailer chooses a system-optimal order, as if the manufacturer operated the store directly. The formal model compares the sets of all such optimal orders, so it also handles a distribution whose CDF is flat over an interval. Pasternack (1985), pp. 170–171, (3), (6), (8)–(10)
The integrated company's optimal-order equation (5) supplies the benchmark:
The retailer's optimal-order equation (7) includes both and . Substituting the integrated benchmark gives equation (10), the common comparison used for the two endpoint policies. The first three milestones formalize these conditions, including existence of an integrated optimum. The last two milestones record the separate calculations in the appendix for full-credit returns and no returns. Pasternack (1985), pp. 170–171, 175
The mission goal combines Theorems 1 and 2 as the article does immediately after stating them. With or with , every system-optimal order fails to be retailer-optimal:
The disjointness claim is read separately for each endpoint policy. It says more than merely finding one order on which the firms disagree: neither endpoint policy can induce the retailer to choose a system optimum. Pasternack (1985), Theorems 1–2 and following paragraph, p. 171
The result separates a policy that reimburses all unsold stock at full wholesale price from one that offers no return option. Both may be simple to administer, but neither aligns the retailer's stocking choice with the integrated company's choice under the article's cost ordering. The result makes the paper's subsequent search for partial-credit terms substantive: the coordinating policy lies away from these two endpoints. It does not say that either endpoint always gives a loss, or that a retailer cannot make a profit. The claim concerns the order that maximizes expected channel profit. Pasternack (1985), pp. 171–172
The known result is proved in the article, but its definitions and theorem statements have not been machine-checked as part of this mission. Formalization gives a reusable account of the paper's piecewise expected profits, feasible order quantities and return fraction, and makes explicit the conditions under which the endpoint conclusions hold. Related proved platform statements include Snyder and Shen's wholesale coordination and wholesale under-ordering. They are not imported: their contract data require , while Pasternack's retailer has no separate own unit cost and the article does not require nonnegative salvage value.
The claim is sensitive to the demand model. If demand is deterministic, its CDF has a jump, and an order exactly equal to demand can be optimal under both the integrated profit and unlimited full-credit returns. The paper assumes a demand density; continuity of the CDF is therefore material to Theorem 1. Flat parts of a continuous CDF pose a different issue: a theorem identifying just one optimum would lose some orders, so the milestone conditions identify whole sets of maximizers. Pasternack (1985), p. 170, definition of and (4)–(7)
The no-return case also depends on the meaning of the manufacturer's additional goodwill cost. The paper names as a cost but does not print a separate nonnegativity inequality. If it were allowed to be negative, the appendix's contradiction with could disappear. The formalization states , along with , and identifies this convention openly. Pasternack (1985), pp. 170, 175
Lean uses a probability measure supported on with finite first moment in place of a named density . The theorems assume that has no atoms, giving the continuous CDF needed by the paper's first order conditions. The profit definitions retain the piecewise formulas of (3), (6) and (8), including the thresholds and . Adjacent pieces agree at their boundaries. The fixed retail price and the fraction match the paper's setting. The cost ordering is split between fixed costs and an admissible policy, because the theorem compares particular policy choices.
Only is feasible. An optimal-order predicate includes this membership as well as maximality, and coordination compares complete argmax sets. The goal explicitly asserts that a system optimum exists, preventing a vacuous conclusion about orders when there are none. At the retailer profit is independent of , so the goal quantifies over every credit without imposing an unused bound on it. The denominator is positive under and . Contributions that develop the optimal-order characterizations, the substitution identity, or the endpoint contradictions within these conventions directly support the goal.
A manufacturer of a perishable good (newspapers, magazines, bread, seasonal fashion, printed books) sells through a retailer who must commit to an order before demand is known. Unsold units lose most of their value; unmet demand costs goodwill. When the retailer alone bears the risk of leftovers, it orders less than an integrated firm would, and the channel as a whole earns less. This inefficiency is the double marginalization of the newsvendor problem, and return policies, under which the manufacturer buys back unsold units, are the instrument publishers and other suppliers of perishable goods actually use against it.
Barry Alan Pasternack's paper Optimal Pricing and Return Policies for Perishable Commodities (Marketing Science, 1985) was the first to show, in a single-period newsvendor model, which return policies restore the integrated firm's order quantity. It became the starting point of the literature on supply-chain contracts: buy-back contracts are now a textbook chapter (Cachon 2003; Snyder and Shen, Fundamentals of Supply Chain Theory), and the paper's result is the standard example of a contract that coordinates a channel while letting the two firms split the profit.
A manufacturer produces at unit cost . A retailer sells at the fixed retail price . Leftover units are salvaged at per unit. Each unit of unmet demand costs the retailer a goodwill penalty and the manufacturer an additional penalty ; write . The data satisfy .
The manufacturer chooses a policy : the retailer pays per unit ordered and may return up to the fraction of its order for a credit per unit. The paper assumes
Demand is random with distribution function . Three expected profits are defined as functions of the order : , equation (3), the profit of a company store in which the manufacturer sells directly; , equation (6), the independent retailer's profit under the policy; and , equation (8), the manufacturer's profit when the retailer orders . An optimal order for a profit function is a maximizing it over . The policy coordinates the channel when the retailer's optimal orders are exactly the company store's optimal orders: the decentralized channel then produces the integrated firm's quantity.
The Lean development uses the same letters: Costs carries ; Costs.Admissible K c1 c2 R is (1)–(2) with ; EPT, EPR, EPM are (3), (6), (8); IsOptimalOrder and Coordinates are the two notions just defined; is cdf D for a demand law D.
A policy which allows for unlimited returns at partial credit will be system optimal for appropriately chosen values of and . Precisely, for every price with there is a credit with
such that the policy coordinates the channel for every continuous demand distribution on with finite mean. The credit is chosen before, and independently of, the demand law.
The result. Theorem 3 says that a buy-back contract with full returns at a partial credit aligns the retailer's incentives with the channel's, and that the coordinating credit depends only on costs. The second point carries the paper's practical conclusion: a manufacturer selling one product to many retailers with different demand distributions can post one price and one return credit and still have every retailer order its system-optimal quantity. The one-parameter family of coordinating pairs then splits the channel profit between the firms. The companion mission (Optimal Pricing and Return Policies for Perishable Commodities II) formalizes the negative results, Theorems 1 and 2: neither full credit with unlimited returns nor a no-returns policy coordinates.
Formalizing it. The paper's proofs are first-order conditions and a short algebraic argument. A machine-checked version adds three things. It makes the analytic content explicit: existence of the system optimum, global optimality of the first-order conditions for an arbitrary atomless demand law, and the quantifier structure "one credit for all demand laws". It repairs a gap: the printed argument for establishes only , which suffices only when , although the claim holds for all . And it gives a reusable newsvendor layer with returns. Related results are proved on Prove2Me in a different model: Snyder–Shen's SupplyChainTheory.buyback_coordinates (Theorem 14.4) and SupplyChainTheory.buyback_profit_identities. They are not referenced here, because their contract data require a retailer cost , which excludes Pasternack's retailer (no own cost), and because they fix the buy-back price and derive the wholesale price, with no range claim.
The algebraic core, milestone 5, is short. The work sits in the analytic milestones. Differentiating under the integral sign in (3) and (6) needs the integrands' piecewise structure and the absence of atoms; the global-maximum claim needs concavity of the expected profits on , including the boundary . Coordination is a statement about sets of maximizers, not about one first-order condition: when is flat at the critical fractile, the optimal orders form an interval, and showing that the retailer's maximizers coincide with the system's requires the monotonicity of the retailer's marginal profit, strict where increases. The naive reading "both first-order conditions hold at " proves one inclusion only.
Demand is a probability measure D on with D (Iio 0) = 0 and finite mean (IsDemand), and is cdf D. The paper's density is the hypothesis NullSingletonClass D (no atoms), imposed on each theorem that uses it. The expected profits are Lean integrals of the paper's piecewise integrands, written with if. The goodwill costs satisfy , implicit in the paper. is a fraction in . Optimal orders are maximizers over that are themselves . Coordination is equality of the retailer's and the company store's sets of optimal orders. The denominator is positive under these assumptions, so no division is degenerate.
The goal is not the algebraic statement "there is solving (11)": that is milestone 5. A formalization of Theorem 3 must conclude Coordinates, a statement about the maximizers of the actual profit functions (3) and (6), and must place the quantifier over demand laws inside the existence of .
A complete development needs: differentiation of parametric integrals with piecewise-linear integrands, concavity of the newsvendor profit, the intermediate value theorem for continuous distribution functions, and the critical-fractile characterization. The newsvendor layer (milestones 1 and 2) is reusable for any single-period contract model. Proofs of the milestones, alternative proofs (for example via the identity under (11), which also removes the no-atoms hypothesis), and the profit formulas (12)–(14) at the coordinated optimum are all welcome.
Simulation, Monte Carlo integration and randomized algorithms consume long streams of numbers that should behave like independent uniform draws. A deterministic generator with finite state is eventually periodic, so its period is the first figure of merit: a stream cannot be longer than its cycle. G. Marsaglia and A. Zaman, A new class of random number generators (Ann. Appl. Probab. 1 (1991)), introduced the add-with-carry and subtract-with-borrow generators. They keep machine words plus one carry bit, use only additions or subtractions of words, and still reach periods such as when the base is near (p. 465). The paper's mechanism for this is number-theoretic: the generated digits are the base- digits of a fraction written backwards, so the period of the generator is the period of a repeating base- expansion, i.e. the multiplicative order of modulo .
Generators of this family were used widely in the following decades (Lüscher's RANLUX generator in lattice field theory is built on subtract-with-borrow), and later work showed that they are equivalent to linear congruential generators with modulus (Tezuka, L'Ecuyer and Couture 1993). This mission treats the add-with-carry generator. A companion mission treats subtract-with-borrow.
Fix a base and two lags and with . A state (or seed vector) is
where each is a base- digit and is the carry bit. The digit is the oldest one. The add-with-carry map (p. 465) is
and the generated sequence of a seed is . Reading off the last digit of each state gives a digit stream obeying , with the carry updated at each step. The two trivial seeds are and . The modulus of the generator is
For and , the -th base- digit of after the point is . The order is the least with , and is a primitive root of a prime when .
Let be prime, and let be any seed other than the two trivial seeds. Then is a periodic point of and
This is the italic summary of p. 472 ("whatever the seed vector, except for the two trivial seeds, the add-with-carry and subtract-with-borrow sequences become periodic after a few iterations of the generating function, and the periods are the order of the base for the appropriate modulus"), with the claim of §4.2 (p. 467) and its proof (p. 468). The goal fixes no particular , , and does not assume that is a primitive root. When it is, the period is , the value announced in §2.
The result. The goal reduces the period of the generator, a property of a dynamical system on states, to the multiplicative order of one residue. That is the computation the paper performs in §6 to certify its recommended generators, and it is how one chooses : search for primes and check the order of . Milestone 5 is stronger than the goal. It needs no primality and identifies the whole output stream, not only its period, with the expansion of a fraction. That identification is what later work used to relate carry generators to linear congruential generators with modulus . Milestone 6 answers the paper's "periodic seed" puzzle: it says exactly which seeds lie on their own cycle.
Formalizing it. The results are proved in the paper, the general §4.1 facts are classical, and the method-specific rules of §4.5 (milestone 6) are stated there without proof. None of it is machine-checked on Prove2Me or, to our knowledge, in Mathlib, which has orderOf and ZMod but no theory of base- expansions of rationals. The mission produces a checked link from a concrete integer recurrence to modular arithmetic. That link can serve as a template for other carry-based and lagged generators.
The obvious argument says the digit recurrence is linear, so the period divides something like the order of a companion matrix. This fails because of the carry: is not linear over , and the state does not live in a group in any evident way. The link to the order of modulo goes through an identity between a finite digit string and a fraction (milestone 5). Stating it with exact indices is itself delicate: the digits run in reverse order, the fraction depends on the string's length, and the trivial seed , whose digits are those of , has to be excluded.
A second difficulty is the preperiod. A seed need not lie on its own cycle (p. 472), so the period must be measured after the transient. Bounding that transient by (milestone 4) and characterising the periodic seeds (milestone 6) are separate combinatorial facts about the carry. The paper states the second without proof.
CarryRNG.AWC. Lags are a structure Lags with fields r, s and proofs of and . A state is a structure with digits x : Fin r → Fin b and carry c : Fin 2, so holds by typing. Lean index is the paper's : x 0 is (the digit the step drops), and the partner digit is index . step is defined directly from the two-case formula of p. 465, not through . The digit stream out is one-based: the seed digits for , then the last digit of . digit b m k j is the exact integer formula above, used for only.Function.minimalPeriod. It is at non-periodic points, so the goal's equation with the positive also asserts periodicity. A divisibility or inequality form would be vacuous and is not used. For digit sequences, "period " is stated as " is a period iff ".minimalPeriod along an orbit. Proofs of any milestone are welcome, as are primality and order certificates for milestone 8 as separate lemmas.A single processor receives jobs over time, each with a known amount of work, and may interrupt a job at any moment to work on another. Which rule should decide what to process? For the number of jobs waiting or in service, the answer is the Shortest Remaining Processing Time (SRPT) rule: at every moment, work on the job in system that is closest to completion. Its optimality is pathwise. It holds for every sequence of arrival times and processing times, not on average under a probabilistic model, so it applies to any single-server queue whatever the distribution of interarrival and processing times. By Little's law it also minimizes mean response time, which is why SRPT and its approximations are the reference policy in the analysis of size-based scheduling for web servers and networks (Harchol-Balter et al., 2003).
Timeline:
An arrival stream is a sequence of pairs , , of real numbers: is the arrival time and the processing time of job . A schedule is a family of measurable functions , with meaning that the processor works on job at time . No job is processed before it arrives ( for ), and the processor works on at most one job at a time.
The remaining processing time of job at time is
and its completion time is
or if the job never receives its processing time. The set of jobs in system at time is , and is its cardinality.
A schedule follows SRPT if, at every time with , the processor works on a job with for all . Ties may be broken arbitrarily.
For every locally finite arrival stream, every SRPT schedule and every schedule of the same stream,
The goal has no constants and no distributional assumptions. It is the statement quoted on p. 687 and concluded at the end of the PROOF on p. 689.
All five come from the PROOF on p. 689. They compare an original schedule with a revised schedule .
The result. The goal is a sample-path dominance. Each consequence for averages follows by taking expectations or time averages: SRPT minimizes the mean number in system and, through Little's law (Little, 1961), the mean response time in every G/G/1 queue with known job sizes. It makes SRPT the benchmark against which other preemptive disciplines, size-based or size-oblivious, are measured.
Formalizing it. The statement has been proved on paper since 1968 and given a complete proof in 1978. No machine-checked proof of it is known to this mission. A formalization contributes three things: a precise continuous-time model of preemptive single-server schedules with measurable service indicators and possibly infinite completion times; checked proofs of the exchange steps of the 1968 letter, each of which needs a hypothesis the letter leaves implicit; and a checked proof of the pathwise optimality theorem itself.
The letter argues that a non-SRPT schedule contains an interval on which SRPT is violated, and that swapping service on that interval improves the schedule. The first step fails for measurable schedules. A schedule can violate SRPT on a set of positive measure that contains no interval (a fat Cantor set), or only on a null set. So the "interval of non-SRPT behaviour" need not exist, and a single interchange does not turn an arbitrary schedule into an SRPT one. Repeating interchanges also gives no obvious termination or limit argument, because the improvements can accumulate at a point. The goal therefore cannot be reached by formalizing the letter's induction literally. The milestones are the letter's local claims, which are true under the hypotheses stated with them. The goal needs an argument that compares an SRPT schedule with an arbitrary one at every time directly.
All declarations live in the namespace SchrageSRPT.Opt. Jobs are indexed by ℕ from , and times, arrival times and processing times are real. A schedule is δ : ℕ → ℝ → ℝ with values in , each δ n measurable, before arrival, and at most one job served at a time. The letter's is stated as "two served jobs are equal", not as a series. Assumption (I) of the letter (the arrival stream does not depend on the discipline) is encoded by comparing schedules of one fixed stream. Assumption (II) (preemption wastes no work) is the formula for , which has no setup term. Completion times take values in WithTop ℝ, with for a job that never completes. A job is in system on . is Set.ncard, and the goal assumes local finiteness ( is finite for every ) so that it is a genuine count. SRPT is the verbal rule of p. 687, required at every .
Two encodings would trivialize the goal, and both are ruled out. The displayed condition of p. 688 (" for implies ") is satisfied by the schedule that never works, so it is not used as the definition of SRPT. The competitor class is every schedule of the stream: it is not restricted to work-conserving schedules, to finitely many jobs, or to schedules in which every job completes.
The milestones add disclosed hypotheses that the letter uses silently:
The counting milestone uses the half-open interval, since the letter's closed right endpoint is a slip.
A complete development needs:
All of this is reusable for other continuous-time preemptive scheduling results. Contributions are welcome in particular for this infrastructure, for proofs of the milestones, and for a complete proof of the goal.
Weighted voting bodies often combine a few large blocs with a mass of small, unorganized voters: shareholders' meetings with a handful of large holders and a dispersed float, legislatures with party blocs and independents. The Shapley value measures each participant's voting power as the probability of being pivotal — the one whose arrival first turns a losing coalition into a winning one — when participants arrive in a uniformly random order. For many small voters this computation becomes a combinatorial problem whose size grows with the number of voters.
Milnor and Shapley (RAND RM-2649, 1961; revised as Mathematics of Operations Research 3(4), 1978) replaced the small voters by a continuum, the ocean, and obtained explicit formulas for the power of the large voters. The memorandum is the second of a RAND series on values of large games; the first (L. S. Shapley and N. Z. Shapiro, Values of Large Games, I: A Limit Theorem, RM-2648, 1960) proves the limit theorem for finite games with many small players on which the oceanic model rests. This mission formalizes the part of the memorandum that leads to explicit closed forms for the values of interior oceanic games (§2, §4, §5).
There are major players with weights , and . The ocean is the interval with Lebesgue measure, carrying total weight . In the oceanic game with quota , a coalition wins when the weight of its major players plus times its share of the ocean is at least .
The random order is modelled by a uniform random point of the cube : major player is inserted into the ocean at position , and is the set of major players placed before position . Player is pivotal when
and the value of player is the probability of (2.4), i.e. the volume of the set where it holds. The combined value of the ocean is (2.5).
With the quota as a variable, has values , , and the pivot location is a random, nondecreasing, piecewise linear function of with expectation . Adding a major player of weight gives the game .
The game is interior when
that is, the ocean alone wins and the major players together lose. With , define for , the analogous product over for , and the integers , , i.e.
In an interior game, with ,
Both identities are part of the goal. The values do not depend on within the interior range.
Further items, not milestones: the Corollary (5.5), Theorem 3 (averaged over all quotas, each value equals the player's share of the total weight), Theorem 4 (small players behave like ocean), and (5.8) with its footnote ( is the nearest integer to and counts derangements).
Theorem 6 turns the voting power of the large blocs, a priori a probability over a continuum of orderings, into a finite multilinear polynomial in the ratios . Table 1 of the memorandum lists the cases , and the theorem gives every . Its coefficients are signed derangement numbers. The Corollary (5.5) states that a major player's value per vote equals the ocean's value per vote in the game without that player.
The memorandum's arguments are short and partly heuristic: "E commutes with the derivative", the disjointness of the pivot sets is "obvious", and the induction for Theorem 6 relies on the symmetry of the value in the major players, which is never stated. A formalization makes each of these steps precise, including the measure-zero exceptions and the quota ranges. To our knowledge none of these results has a machine-checked proof; Mathlib has the Lebesgue measure on cubes, interval integrals and derangement numbers, but no game-theoretic value with a continuum of players.
The values are volumes of regions of cut out by inequalities whose shape depends on the order of the coordinates, so a direct computation splits into order cells, with the quota entering each. The paper's route avoids this by passing through the random function , Theorem 2 and the Lemma; that route needs differentiation under the integral sign for a function that is only piecewise linear in , with kinks at random locations, and an exact bookkeeping of the interval of integration when the quota approaches the ends of . Theorem 6 is then an induction on that uses Theorem 5 for every player in turn, so it also needs the invariance of under a relabelling of the major players.
Fin m ( is allowed; then ). The probability of an event is the Lebesgue volume of its intersection with ; no probability space is built.HasDerivAt), and for the Lemma, as on p. 14.Fin.snoc as index Fin.last m.A complete development needs: measurability of the pivot sets and of in , the structure of as a piecewise linear function of , differentiation of , and invariance of the values under permutations of the major players. The pivot-set and infrastructure is reusable for the companion mission on limits of finite weighted majority games. Contributions of any of the milestones, of the symmetry lemma, and of the non-milestone items are welcome.
An isometric model of a graph assigns vectors to vertices so that vector distances reproduce shortest-path distances exactly. The choice of norm matters: a graph that needs many Euclidean coordinates may admit a smaller realization under a different norm. Linial, London, and Rabinovich used this freedom to study the dimension of graph metrics and related geometric questions in their 1995 paper on graph embeddings (Linial–London–Rabinovich, 1995). The complete graph is the first calibration point for the invariant. Every two distinct vertices are equally far apart, so the question becomes how many pairwise equidistant points an arbitrary real normed space of dimension can contain.
The answer is a sharp base-two logarithm. It separates the role of dimension from the particular shape of a norm's unit ball. In particular, a cube equipped with the supremum norm supplies many equidistant vertices, while no norm in the same dimension can accommodate more. Establishing both directions gives a reference case for more complicated graph metrics in the paper's Section 5.
A finite pseudometric space has a finite point set and a distance that is symmetric, vanishes on the diagonal, and satisfies the triangle inequality. Distinct points may have distance zero, as the paper explicitly allows. A norm on is nonnegative, vanishes only at the zero vector, is absolutely homogeneous, and satisfies the triangle inequality. It induces the distance between vectors.
An isometric embedding of into a -dimensional normed space is a map with for every pair. The isometric dimension is the least for which such a norm and map exist. The norm may depend on and ; it is part of the realization rather than a fixed background choice. Lemma 5.1 of the paper states that every -point metric space has an isometric realization in , so this least dimension is taken over a nonempty set (Linial–London–Rabinovich, p. 229).
The complete graph has an edge between every pair of distinct vertices. Its shortest-path distance is zero from a vertex to itself and one between distinct vertices. An isometric realization of is therefore a collection of points whose pairwise distances are exactly one. The paper's Section 5 treats connected graphs, so this mission takes . Its convention is that every logarithm has base two.
The foundational target is the paper's finite embedding statement:
It establishes the domain on which the least-dimension definition has its intended meaning. The remaining milestones isolate the geometric assertions used for complete graphs: a difference-body inclusion, separation of the interiors of certain convex-hull translates, and a cardinality bound for equilateral points in .
The goal is Proposition 5.4 (Linial–London–Rabinovich, p. 231):
The lower bound applies to every real norm on . The upper bound has the more specific target . Both inequalities, including and dimension zero, are part of the mission.
The equation determines the optimal dimension for an equilateral finite metric space when the norm is unrestricted. It also bounds the size of an equilateral set in every -dimensional real normed space by , with equality attainable by vertices of a binary cube under the supremum norm. For graph metrics, it gives a precise baseline against which dimension bounds for trees, cubes, and other connected graphs can be compared. The surrounding section of the paper uses the same geometric vocabulary for those other families (Linial–London–Rabinovich, Section 5).
The mathematical result is proved in the 1995 paper. This mission asks for machine-checked Lean proofs of the specified statements. The local declarations presently encode open proof obligations; compilation checks their types and imports, but does not establish the theorems. A completed development would provide a reusable interface for finite isometric dimension and for equilateral configurations under arbitrary finite-dimensional norms.
The easy direction uses points of a binary cube. The difficult direction must hold uniformly over every possible norm, whose unit ball need not be round or smooth. A direct coordinate count cannot assume that vectors have bounded entries in a prescribed basis. The paper formulates its argument through the convex hull of an equilateral configuration and a comparison of translated sets (Linial–London–Rabinovich, p. 231). Its printed volume line also leaves a degenerate case: if that convex hull has zero volume in the ambient space, cancellation of gives no numerical bound. A complete formal proof must account for such configurations without weakening the theorem to full-dimensional sets.
The Lean representation of is the function space Fin d → ℝ. A norm is an explicit function with all norm axioms, including definiteness and absolute homogeneity. Isometric dimension takes the infimum over dimensions admitting such a norm and an exact distance-preserving map. The complete graph is Mathlib's ⊤ : SimpleGraph (Fin n); its graph distance is converted to a real number. This distance is the discrete zero-or-one metric. The lower bound quantifies over every explicit norm. The cube milestone uses the supremum norm on finite real coordinate vectors. Convex hulls and interiors use the standard topology of this finite-dimensional vector space, which every norm induces.
The formal goal assumes , matching the paper's connected-graph convention; remains included, with dimension zero. The logarithmic expression is Nat.clog 2 n, the ceiling of the base-two logarithm, rather than a floor or a real logarithm. The source uses no unspecified asymptotic constant in Proposition 5.4 or its listed milestones. The empty point space is allowed in the general finite embedding lemma; its pairwise claim is vacuous, while the nonempty cases carry the intended content. The dimension definition is only used for realizable finite distances, so a totalized infimum's value on an unrealizable function has no role in the target.
The exact norm axioms and exact distance equality prevent shortcuts through seminorms, truncated distances, or a weaker distortion bound. The cardinality theorem retains lower-dimensional affine configurations; assuming positive ambient volume would discard part of the result. A complete development needs finite pseudometric geometry, the supremum norm, convex hulls and interiors, and a dimension-sensitive measure argument. Those components are useful beyond this graph. The paper's independent results on degrees, trees, cubes, and other graph families, as well as algorithmic running-time claims elsewhere in the article, are outside this mission.
Discounted Markov decision problems are solved in practice by two classical schemes. Value iteration (successive approximations) is cheap per step but contracts the error only by the discount factor per step, which is slow when is close to . Policy iteration (Howard, 1960) converges in few steps, but each step solves a linear system for the value of the current policy. Puterman and Brumelle (Mathematics of Operations Research, 1979) showed that policy iteration is Newton's method applied to the optimality equation.
Puterman and Shin (Management Science 24, 1978) interpolated between the two schemes: replace the exact policy evaluation by steps of successive approximation. This is modified policy iteration of order . For it is value iteration; as it approaches policy iteration. The paper proves that every order converges and bounds its rate. The scheme remains a standard algorithm in dynamic programming (Puterman, Markov Decision Processes, Wiley 1994, §6.5), and it appears in reinforcement learning as "optimistic" or "generalized" policy iteration.
Timeline. Howard (1960): policy iteration for finite problems. Puterman–Brumelle (1979, circulated earlier): policy iteration as Newton–Kantorovich iteration, and the support inequality for the optimality operator. van Nunen (1976) and van Nunen–Wessels: convergence of related value-oriented methods in a different framework. Puterman–Shin (1978): convergence of modified policy iteration of every order from a starting point with , and the rate bound formalized here.
is a set of states with a -algebra. A family of policies is given. Each is a transition operator: a Markov kernel assigning to each state a probability distribution on . Each policy also has a one-period reward , and the rewards are uniformly bounded: . The discount rate satisfies .
is the Banach space of bounded measurable functions with . A kernel acts on by . For linear on , .
The optimality equation is
The paper assumes throughout that the maximum in (1) is attained for every , by a single policy at every state.
For , the truncated Neumann series is . Modified policy iteration of order runs the recursion
where attains the maximum in (1) at . A solution of exists and is unique. denotes a policy attaining the maximum at . The proofs also use the operators and the set .
If and , then for every
The mission also contains four further theorems that are not milestones: Corollary 2 (asymptotic rate at most when ), Proposition 2 (monotonicity in the order ), the representation (6) , and Proposition 1 (policy iteration as Newton's method).
The result. Bound (8) gives two guarantees. Every order of modified policy iteration converges at least as fast as value iteration, with factor per step. Once the improving policies stabilize near an optimal one, the factor approaches , the factor of value-iteration steps. This justifies spending cheap evaluation sweeps per policy improvement instead of solving a linear system. It also underlies the analysis of the many later variants: action elimination, asynchronous and approximate versions, and optimistic policy iteration in reinforcement learning.
Formalizing it. The theorems are proved on paper. As far as the platform's library shows, none of them is machine-checked: existing items cover value iteration and exact policy iteration for finite state spaces. This mission formalizes the whole chain on general measurable state spaces with Markov kernels, including the support inequality and the comparison operators . Corollary 2 is stated as an upper bound only, because the equality printed on the page fails in degenerate runs (see the item's note).
The obvious route to a rate is the contraction argument for value iteration: is monotone and a -contraction, so its iterates converge geometrically. For that argument does not transfer to the map . The truncated series is taken for the policy chosen at the current point, so the map changes with , and it is not monotone in general. The van der Wal–van Nunen example on p. 1133 of the paper shows that iterates of a higher order need not dominate those of a lower order from the same start. Moreover, without the condition the iterates need not even increase. A rate for (4) is therefore not a corollary of a fixed-point theorem for a single operator.
Formally, a second layer of difficulty is the setting itself. Everything happens in the space of bounded measurable functions on a general measurable space. So every operator applied to an iterate must be shown to preserve boundedness and measurability, and the maxima over policies are suprema over an arbitrary index set.
The Lean development (namespace ModPolicyIter.Conv) represents:
P i : Kernel S S with a measurable reward c i, ;IsBM (measurable and bounded), with supNorm v = ⨆ s, |v s|;The standing assumptions of §2 are carried by the model fields; items using a maximizer assume either global attainment (MaxAttained) or an explicit maximizing policy. A run of (4) is a sequence of functions paired with a sequence of policies, each policy a maximizer at the current iterate. Only is assumed; that later iterates lie in is part of the proofs.
Deviations from the page, all disclosed in the items:
The goal must not be trivialized by assuming , the support inequality, the sandwich of Corollary 1, or anything about . These are milestones to be proved, and none of them is a hypothesis of the goal.
Reusable infrastructure includes Markov kernels as operators on bounded measurable functions (positivity, , measurability of ), completeness of , and the Banach fixed point theorem on . The first of these serves any discounted dynamic-programming mission on general state spaces. Contributions of any milestone, or of helper lemmas about these operators, are welcome.
Prediction with expert advice asks a master algorithm to combine the binary predictions of a pool of prediction algorithms, trial after trial, so that it makes few more mistakes than the best member of the pool, without any probabilistic assumption on the data. Littlestone and Warmuth's Weighted Majority Algorithm WM (Littlestone and Warmuth 1994) keeps a weight per member, predicts with the weighted vote, and multiplies the weights of the wrong members by a factor after each of its own mistakes. Its mistake bound is of order , where is the number of mistakes of the best member on the whole sequence.
That bound compares the master with a single fixed member. In many applications the member that predicts well changes over time: one algorithm is accurate for a while, then a second one, then a third. Against a shifting target of this kind, WM can do badly, because the weight of a member that was wrong for a long time has become so small that it takes many mistakes to recover it. Section 3 of the paper introduces the variant WML, which never decreases a weight that is already small relative to the total, and proves that it pays only a logarithmic cost per change of target. This was the first result of what is now called tracking the best expert; it was later refined by Herbster and Warmuth's Fixed-Share algorithm (Herbster and Warmuth 1998).
Timeline. 1989: a conference version of the paper appears at FOCS. 1994: the journal version, the source of this mission, gives Lemma 3.1 and Theorem 3.1 in their present form. 1998: Herbster and Warmuth's Tracking the Best Expert generalizes the shifting bound to other loss functions.
A run takes place over trials . In trial each member of the pool predicts , the master predicts , and the label is revealed. The predictions of the pool and the labels are arbitrary.
The master keeps weights , the weights at the beginning of trial . Let be the total weight and the total weight of the members predicting . WML has parameters and :
With this is WM. Write for the number of mistakes of the master and
which lies in for the stated parameter ranges.
Split the sequence into consecutive segments , with trials in , and let be the smallest number of mistakes any single pool member makes on . If and every initial weight is at least times the total initial weight, then
The partition is arbitrary and unknown to the algorithm; the bound holds for all partitions simultaneously.
The single-segment case, , together with the statement that the weight floor survives the run: if every initial weight is at least times the total, then
and every final weight is at least times the total final weight.
On every mistake trial, .
The result. Theorem 3.1 shows that an online algorithm with no knowledge of when or how often the best predictor changes can compete with the best sequence of predictors, at a price of mistakes per segment. The with says that a segment never costs more than its length. The bound is the template for later tracking and adaptive-regret results in online learning and for algorithms whose weights are kept bounded away from zero.
Formalizing it. The result is proved in the paper; no machine-checked proof of a shifting-target bound exists on Prove2Me or, to our knowledge, in Mathlib. This mission produces a formal model of WML in which ties are arbitrary (a run is a relation, so the bounds cover every tie-breaking rule), the per-mistake contraction, the single-sequence bound with its preserved invariant, and the segment bound. The model of trials, majority votes and mistake counts is reusable for the other algorithms of the paper.
The standard argument for WM compares the decrease of the total weight with the final weight of the best member. For a shifting target this fails twice. First, the best member of a later segment may have been wrong during all earlier segments; under WM its weight has shrunk by per mistake, and the master has to make many mistakes before that member regains influence. Second, the floor that prevents this also prevents some wrong members from being penalized, so the total weight shrinks by less on each mistake than under WM. The statement has to control both effects at once, and the per-segment accounting has to restart from whatever weights the previous segments left behind. A natural first idea, applying the single-sequence bound to each part of an arbitrary (interleaved) partition, does not work: for interleaved subsequences the inequality is false, and the theorem is about consecutive segments.
The pool is Fin n with ; trials are Fin T; binary values are Bool; weights are real, w : ℕ → Fin n → ℝ, with w t the weights at the beginning of trial , w 0 the initial and w T the final weights. A run is the relation IsWMLRun β γ x ρ w lam; it fixes positive initial weights, the majority rule with arbitrary ties, and the update, whose threshold is strict and uses the total weight at the beginning of the trial. Logarithms are natural logarithms; the base cancels in every ratio. The minimum over the pool is an infimum in ℕ over Fin n. Segments are given by monotone boundaries b : Fin (k+1) → ℕ with b 0 = 0 and b (Fin.last k) = T; empty segments are allowed and contribute .
The paper allows for the algorithm, but then the bounds read . In Lean, n / 0 = 0, so the bounds assume ; the contraction milestone holds for and is stated so. The hypothesis is kept as stated in the paper, not replaced by . A trivializing formalization, such as fixing the tie-breaking rule, dropping the strict weight test, letting the floor hypothesis be unsatisfiable, or allowing interleaved subsequences (which makes the goal false), is ruled out: a run exists for every input from every positive initial weights, and equal initial weights satisfy the floor.
Contributions welcome: proofs of the three statements, and lemmas on restricting a WML run to a block of trials, which the goal needs and which apply to any segment-wise analysis.
A single machine must process jobs, each with a processing time and a deadline, and some jobs must be finished before others may start. The first question of any planner is whether the deadlines can be met at all. Without precedence constraints the answer is classical: Jackson's rule (J. R. Jackson, 1955, reported by W. E. Smith, 1956) says that all jobs can be completed on time if and only if they are completed on time when sequenced by earliest deadline first. Precedence constraints break this rule, because the earliest-deadline order may put a job before one of its required predecessors.
E. L. Lawler and J. M. Moore (Management Science 16 (1969) 77–84) repair the rule by replacing each deadline by a modified deadline that accounts for the deadlines of the job's successors. Their §2 Theorem says that a single sequence, the one in increasing order of modified deadlines, decides feasibility. They use it as the first step of their dynamic programming method for sequencing with deadlines and precedence constraints: because the sequence does not depend on processing times, the jobs to be scheduled on time can always be taken in this one fixed order.
There are jobs . Job has a processing time and a deadline . A sequence lists every job exactly once; the machine starts at time and processes the jobs in the order of , one after another, without idle time. The completion time of job is the sum of the processing times of and of all jobs before it in . Job is on time in if .
Precedence constraints are a partial order on the jobs (reflexive, antisymmetric, transitive). If and , job must precede job ; such a is a successor of , and every job counts as one of its own successors. A sequence is consistent with if no job appears before a job that must precede it. The jobs are numbered so that implies .
For a number the modified deadline of job is
the earliest deadline among and its successors, plus a tie-breaking term. The paper takes to be "a small number"; here that means and whenever .
Let be the sequence in which increases. Then
The Theorem reduces a question over all sequences consistent with to the evaluation of one sequence, and the sequence depends only on the deadlines and on , not on the processing times. This independence is what the paper's later sections rely on: it lets a subset-selection dynamic program (Eq. (1) of the paper) process jobs in a fixed order. Without precedence constraints ( the identity) the Theorem is Jackson's rule. The operational form, "always take next, from among the available jobs, a job which has a successor with the earliest possible deadline", is a list-scheduling rule of the same kind as the backward rule of Lawler (1973) for .
The result has been proved on paper since 1969. As far as is known it has no machine-checked proof. This mission produces a formal proof of the Theorem and of the exchange step behind it, stated on the same sequence and completion-time model as the platform's existing single-machine scheduling missions.
The obvious argument is the exchange argument for Jackson's rule: swap an adjacent pair that is out of order and check that nothing becomes late. Two things fail without care. First, the swap must not violate precedence; this is why the deadline of a job is replaced by the minimum over its successors. Second, after the swap, job completes when job used to complete, but need not be at least : one must find a successor of that is later in the sequence, on time, and due no later than . That step uses the smallness of : with a large the tie-breaking term outweighs a difference of deadlines, and the Theorem fails (three jobs without precedence, , , ). Finally, the exchange step must be turned into a terminating transformation of an arbitrary feasible sequence into , a bubble-sort argument over lists.
Fin n, 0-based: the Lean job j is the paper's job , and the tie-break is . Processing times and deadlines are real.MooreLateJobs.Shared.IsSchedule and MooreLateJobs.Shared.completionTime (a duplicate-free list of all jobs; start at time , no idle time). Idle time never helps meet a deadline, so this loses nothing. Consistency with is the published LawlerPrec.MinMax.IsFeasible.insert j {k | ρ j k}, which is nonempty; for the reflexive of the paper this is ("considering a job to be one of its own successors").Related platform items: Jackson's rule for unrestricted jobs is already posed as MooreLateJobs.NumLate.jackson (Moore 1968) and is not re-posed here; Lawler's theorem is posed as LawlerPrec.MinMax.sequencing_theorem. Contributions welcome: general list-exchange lemmas (adjacent swaps, bubble-sort termination toward a sorted list) are reusable well beyond this mission.
Labor markets match workers to firms, and the terms of each match (the salary) are negotiated along with the match itself. A firm's output depends on the whole team it hires, so a firm cares about sets of workers, not individual workers one at a time. Kelso and Crawford (1982) asked when such a market has a stable outcome, the core, in which no firm and group of workers can agree on terms that all of them prefer, and when a simple decentralized auction finds one.
Their answer is the gross-substitutes condition: raising some workers' salaries never makes a firm withdraw an offer from a worker whose salary has not risen. Under it, an ascending process in which firms make offers and workers reject all but their favorite reaches a core allocation. This condition became the standard hypothesis for the existence of Walrasian equilibrium with indivisible goods (Gul and Stacchetti 1999), it is the hypothesis behind matching with contracts (Hatfield and Milgrom 2005), and the process is the ancestor of ascending auction designs.
Timeline.
There are finitely many workers and firms , with at least one firm. Worker 's utility of working for firm at salary is , strictly increasing and continuous in . Firm 's gross product from hiring the set is , and its profit at the salary vector is
is the set of profit-maximizing . Each pair has a starting salary . The assumptions (p. 1486) are (MP) for ; (NFL) ; and (GS): if and , some contains .
In the discrete market with unit , firm may pay worker only , . An allocation sends each worker to a firm at a salary ; it is individually rational (D1) if and every firm's profit is nonnegative. It is a (discrete) core allocation (D3) if it is individually rational, pays permitted salaries, and no firm , set and permitted salaries satisfy for all and .
The salary-adjustment process (pp. 1488–1489), verbatim:
R1. Firms begin facing a set of permitted salaries . Permitted salaries at round , , remain constant, except as noted below. In round zero, each firm makes offers to all workers; this is costless by (MP).
R2. On each round, each firm makes offers to the members of one of its favorite sets of workers, given the schedule of permitted salaries . That is, firm makes offers to the members of , where maximizes . Firms may break ties between sets of workers however they like, with the following exception: Any offer made by firm in round that was not rejected must be repeated in round . By (GS), the firm sacrifices no profits in doing this, since (by R4) other workers' permitted salaries cannot have fallen, and the salary of a worker who did not reject an offer remains constant.
R3. Each worker who receives one or more offers rejects all but his or her favorite (taking salaries into account), which he or she tentatively accepts. Workers may break ties at any time however they like.
R4. Offers not rejected in previous periods remain in force. If worker rejected an offer from firm in round , ; otherwise . Firms continue to make offers to their favorite sets of workers, taking into account their permitted salaries.
R5. The process stops when no rejections are issued in some period. Workers then accept the offers that remain in force from the firms they have not rejected.
"The salary-adjustment process R1–R5 converges in finite time to a discrete core allocation in the discrete market for which it is defined." Formally, under the assumptions above:
Theorem 1 gives the existence of a core allocation in every discrete market satisfying (MP), (NFL) and (GS), with no convexity of production and arbitrary complementarity within the limits of (GS). It is the step from which the paper derives the existence of a strict core allocation of the continuous market (Theorem 2, by letting the unit shrink), and with additional no-ties assumptions the firm-optimality of the process's outcome (Theorem 4) and the comparative statics of entry and exit (Theorem 5).
The result is proved in the paper and has been reproved in more general settings; it has no machine-checked proof known to us. Nothing of this paper was on Prove2Me before this series. Related platform work, credited but not reused: the Gale–Shapley deferred-acceptance development (GS62CollegeAdmissions.*, proved), the no-money ancestor of this process; and the Shapley–Shubik assignment game (AssignmentGame.CoreLP), whose core the process approximates when production is additively separable. Neither states anything about this process. This mission is mission 1 of a series of seven on the paper: 2 (strict core of the continuous market), 3 (one-sided coalition formation), 4 (firm-optimality), 5 (comparative statics), 6 (gross substitutes and decreasing returns), 7 (a market without a core). Each states its own model.
The process is quantified over all tie-breakings, so no single computation settles it; the statements are about every sequence of rounds consistent with R1–R5. Two points carry the content. First, R2 imposes a constraint that may not be satisfiable: a firm must repeat its unrejected offers and choose a profit-maximizing set. Without (GS) no such set need exist and the process is not defined. Second, the core property at the stopping round compares the outcome with coalitions using salaries the process never reached; the comparison is with salaries on the discrete grid only, and it is false if coalitions may use salaries below or off the grid. Termination is not automatic either: the process may continue after a round without rejections, salaries are real numbers, and no bound on the number of rounds is given.
Lean representation, in namespace KelsoCrawford.Process:
Market W F carries u, y, σ; workers and firms are finite types, with [Nonempty F] (the paper's ; with no firms and some worker no run exists).Allocation assigns every worker to a firm (no unemployment, as in the paper's ).GrossSubstitutesOn (M.y j) (M.gridVectors δ j) for each firm: the discrete (GS), since the paper notes that a discrete market may satisfy (GS) while its continuous version does not.M.grid δ .Run records salaries, offers and tentative choices per round; IsRun is R1–R4, Stopped is R5's "no rejections", outcome is R5's allocation.Explicit readings of the paper's phrases:
The existence of a run is part of the goal: without it, statements about all runs would be vacuous. Fixing a tie-breaking rule would turn the statements into claims about a single run and is ruled out; so are the strict core D2 (false here because of ties at the grid) and an integer grid below (false for improving coalitions). Proofs of the milestones and reusable infrastructure for ascending processes are welcome.
A many-server queue in which customers arrive at the epochs of a renewal process and are served for exponential times is the basic model of a telephone exchange, a call centre, or a bank of identical machines. Its continuous-time queue-length process is not Markovian unless the arrivals are Poisson, so Erlang's birth–death formulas for M/M/s do not apply. In 1953 D. G. Kendall showed how to analyse such systems by the method of the imbedded Markov chain: observe the system only at the arrival epochs, where the number of customers present does form a Markov chain, and read the equilibrium behaviour off that chain (Kendall 1953).
Timeline:
Customers arrive with independent inter-arrival times of law on and mean , . There are servers and a single queue served first come, first served. Service times are independent of one another and of the input, negative-exponential with mean , . The relative traffic intensity is .
The state of the imbedded chain at an arrival epoch is the number of persons found ahead (waiting or in service) by the arriving customer. Its transition matrix of eq. (8) is given in three blocks, written with the death-process probabilities of (9)–(10), the probabilities of (11)–(12), and the Poisson probabilities of (13)–(14):
The key function is
The queue size met by an arrival is . The waiting time is, given , the sum of independent exponential variables of mean .
When the chain has a limiting distribution , and with the root of in and ,
with both conditioning events of positive probability. The goal fixes no constant beyond those the theorem names: and are determined by , and .
Theorem IV says that, whatever the input law and the number of servers, the part of the equilibrium waiting-time law away from zero is exponential and the part of the queue-size law away from zero is geometric, both governed by the single number . All equilibrium quantities of GI/M/s (Theorems II–III and the delay distribution) then reduce to computing from a one-dimensional equation and the finitely many 's from a triangular linear system. This is the standard textbook treatment of G/M/c queues and the template for many later matrix-geometric results.
The results are proved in the paper, partly by appeal to Feller's theory of denumerable chains and to "tedious but elementary" verifications. None of them is machine-checked. The mission formalizes the paper's chain of argument: the explicit transition matrix, its stochasticity, the reduction of the invariance equations, the passage from a summable invariant vector to the limiting distribution, and the computation of the laws of and from it. The single-server special cases are posed separately on the platform (QueueingFundamentals.GM1.arrival_point_geometric, GM1.waiting_time_cdf, GM1.arrival_point_means, GM1.mean_waiting_times, FosterQueues.GIM1.gim1_classification); they do not cover .
The obvious route is to guess the geometric tail and check it against the balance equations. For this works, but the rows of the block involve the convolution integral (11), and the equations for couple the geometric tail to the boundary terms . Showing these are solvable, and that the row sums of the three-block matrix equal one, requires handling (11) explicitly. The second obstacle is the limit theorem itself: an invariant vector does not, by itself, give . That step needs Feller's dichotomy for irreducible aperiodic denumerable chains, which Mathlib does not provide. Finally, the conditional waiting-time law requires summing an Erlang mixture with geometric weights in closed form.
The queue process itself is not formalized. The chain is defined by its transition matrix (8)–(14), and by the Erlang mixture of p. 349, as the paper derives both by a modelling argument. A chain is any TransitionMatrix P of the published Markov-chain vocabulary with P.p = gimsMatrix s A b; states are -based. "Ergodic" is Feller's: Aperiodic ∧ PositiveRecurrent. The limiting distribution is asserted as Tendsto (P.stepProb n i j) atTop (𝓝 (π j)) for all , not as a stationary vector. The input law satisfies the published IsInterarrivalLaw A a⁻¹ (a probability measure carried by , integrable, mean ), and is the published serviceProb A (s/b) n. Conditional laws are stated multiplied out, together with positivity of the conditioning probabilities. Every series identity is stated with HasSum.
Trivializing formalizations are ruled out: is tied to on rather than free; is the limiting distribution of , asserted to exist, not a probability vector handed to the statement; the conditioning events are asserted to have positive probability; the matrix is the GI/M/s matrix, not the GI/M/1 one; and the 's of Theorems II–III are characterized by the invariance equations, never defined from .
A complete development needs: Feller's limit theorem for irreducible aperiodic positive recurrent chains (reusable well beyond this mission), Foster's sufficiency criterion (referenced, open), Fubini for the stochastic-matrix identities, parametric interval integrals for the block , and Erlang distribution functions. Contributions to the general Markov-chain milestones are as welcome as those specific to GI/M/s.
A lattice in is the set of integer combinations of linearly independent vectors. Many problems in algorithmic number theory, cryptography and integer programming reduce to finding a short nonzero vector of a lattice, or a few short independent ones. Finding the shortest vector exactly is hard, but in 1982 A. K. Lenstra, H. W. Lenstra, Jr. and L. Lovász introduced a notion of reduced basis that can be computed in polynomial time and whose vectors are provably short up to a factor depending only on the dimension (Lenstra, Lenstra, Lovász 1982). Their paper used it to factor polynomials in in polynomial time; the same reduction (now called LLL) became a standard tool for simultaneous Diophantine approximation (the paper's own (1.39)), for H. W. Lenstra's integer programming algorithm in fixed dimension (Lenstra 1983), and for cryptanalysis of knapsack and RSA variants.
What makes a reduced basis useful is a set of explicit inequalities proved in Section 1 of the paper, before any algorithm appears. They compare the lengths of the basis vectors with the lattice determinant and with arbitrary lattice vectors, with constants such as and . This mission formalizes those inequalities.
Let and let and be the ordinary inner product and Euclidean length on . Vectors form a basis for a lattice when they are linearly independent over and . The determinant of is
the written as columns (1.1). The Gram–Schmidt vectors and coefficients () are defined inductively by
the are pairwise orthogonal and not normalised. The basis is reduced if
and
The first condition is a size condition on the coefficients; the second (the Lovász condition) says that swapping and would not shrink the -th Gram–Schmidt length by more than the factor (pp. 516–517).
Let be a reduced basis for and let be linearly independent. Then
The statement quantifies over every reduced basis and every independent family of lattice vectors. Its case is Proposition (1.11).
In the order of the paper's proofs (pp. 517–518):
The rest of Proposition (1.6) and the remark after it: (proof of (1.6)); (1.8) ; (1.9) ; and Hadamard's inequality (1.10) for an arbitrary basis.
Proposition (1.11) says the first vector of a reduced basis approximates a shortest nonzero lattice vector within the factor ; (1.12) extends this to all of the first basis vectors, so that is within of the -th successive minimum of (the remark after (1.12)). These are the guarantees on which the paper's factoring algorithm rests: in Section 2 a reduced basis of a lattice built from a -adic factor yields, through (1.11) and (1.12), an irreducible factor of the polynomial. Inequality (1.9) gives simultaneous Diophantine approximation in polynomial time, and (1.8) bounds how far a reduced basis is from orthogonal.
All of these results are proved in the paper and in textbooks. Verified LLL developments exist in Isabelle/HOL (Bottesch et al., A verified LLL algorithm, AFP 2018), but Mathlib, the library this platform builds on, has neither the reduced-basis predicate of (1.4)–(1.5) nor these bounds. A Lean development produces a reusable definition layer for lattices with the paper's conventions, Gram–Schmidt length estimates, and Hadamard's inequality in determinant form, which the other missions of this series (the reduction algorithm and the factoring application) build on.
The estimates on Gram–Schmidt lengths are single-variable inductions once (1.5) has been rewritten using orthogonality. The step that does not follow from a direct estimate is (1.12): the vectors are arbitrary independent lattice vectors with no relation to the basis order, so a bound on each by a single Gram–Schmidt length does not by itself say which it controls. A naive argument that pairs with fails. The determinant statements need the link between Mathlib's matrix determinant of the columns and the Gram–Schmidt lengths, which Mathlib does not state in this form.
is EuclideanSpace ℝ (Fin n) (abbreviated Vec n), a basis is a family b : Fin n → Vec n, the lattice is Submodule.span ℤ (Set.range b), and "basis for " is linear independence over together with equality of that span with . The vectors are Mathlib's unnormalised InnerProductSpace.gramSchmidt, and is (1.3) verbatim. is the absolute determinant of the column matrix; it is not defined as , which would make the first companion statement true by definition. Section 1 begins "Let be a positive integer", so every statement carries .
Lean indices run from to : the paper's is Lean's b ⟨i-1, _⟩, an exponent at paper index is at Lean index , and the pair of (1.5) is . Exponents , and are real powers. The maximum in (1.12) is a Finset.sup' over the nonempty index set of the , and the statement is empty at , as on the page.
Every statement about a reduced basis also assumes linear independence: the reducedness inequalities alone hold for degenerate dependent families, whose Gram–Schmidt vectors vanish, and would make the targets trivial. The goal does not assume (1.7), (1.13) or any ordering of the ; those appear only as milestones. Proofs of the milestones and companions, and general lemmas on Gram–Schmidt and determinants that would belong in Mathlib, are welcome.
A correlated equilibrium (Aumann 1974) describes play in a game where a mediator draws a profile of recommended actions from a joint distribution and tells each player only that player's own recommendation; the distribution is an equilibrium when no player gains, on average, by departing from the recommendation. Correlated equilibria are the natural outcome of regret-minimizing learning dynamics and the solution concept underlying much of algorithmic game theory, so it matters in which games they are guaranteed to exist.
For finite games existence follows from Nash's theorem, since every Nash equilibrium is a correlated one. Hart and Schmeidler (1989) gave a direct proof based on linear duality, with no fixed-point theorem, and then extended it beyond finite games. This mission formalizes the last and most general of their three existence theorems: games with arbitrarily many players whose strategy spaces are compact Hausdorff spaces.
Timeline.
A game consists of a nonempty set of players, possibly uncountable; for each player a nonempty set of pure strategies; and for each player a payoff function on the set of strategy profiles . For a profile and a strategy , denotes the profile obtained from by replacing player 's coordinate with ; thus .
In this mission each is a compact Hausdorff space with its Borel σ-algebra , the profile space carries the product topology, and is the Borel σ-algebra of . The product σ-algebra generated by the is contained in , and the inclusion may be strict when is not metrizable (the paper's footnote 13).
Let be a probability measure on . Think of as the mediator's distribution; player learns the coordinate of the drawn profile. A deviation of player is a -measurable map that replaces each recommendation by an action. The measure is a correlated equilibrium with respect to and when, for every player and every deviation ,
The left side is the expected gain from obeying the recommendation instead of following .
If every is compact Hausdorff and every is continuous on with the product topology, then
"Countably additive" in the paper's statement is automatic: is a measure.
An optional milestone records the remark on p. 23 that, for a finite strategy set , condition (4) for player is equivalent to the earlier condition (3), one inequality per recommendation and alternative .
The result. Theorem 3 guarantees correlated equilibria, with a genuine (countably additive) probability measure, in every continuous game on compact strategy spaces, however many players there are. It also justifies taking to be the full Borel σ-algebra rather than the smaller product σ-algebra, so that every Borel-measurable deviation rule is allowed. Nash existence under the same hypotheses (Fan 1952, Glicksberg 1952) implies existence of correlated equilibria too, but through a fixed-point theorem; the proof here uses only finite-dimensional duality and compactness.
Formalizing it. The theorem is classical and its proof is published; nothing here is open. To our knowledge no machine-checked proof of Theorem 3, or of any existence result for correlated equilibria in infinite games, exists. Finite-game existence results are on the platform (AGT.nash_existence; the correlated-equilibrium encodings of Aumann 1987 and Foster and Vohra 1997, and AGT.swap_regret_correlated_equilibrium). The formalization would add reusable measure-theoretic tools on compact products: the regular cluster point of a net of probability measures, the regularity of marginals, and uniform partitions for continuous functions on a product.
The obvious argument is the one that proves Theorem 2: approximate the game by finite games , take correlated equilibria , extract a weak-* cluster point , and pass the inequalities of to the limit. Passing to the limit works only for integrands that are continuous in , because is a cluster point against continuous functions only. The integrand of (4) is , and is merely Borel measurable, so this integrand need not be continuous and the limit step fails. Restricting to continuous deviations would avoid the difficulty but would prove a weaker theorem. Two further points need care: on a non-metrizable product the Borel σ-algebra is larger than the product σ-algebra, and the f-sets ordered by inclusion are not a directed set.
The profile space is a type synonym Profile S of ∀ i, S i carrying the product topology and the instance borel (Profile S), so measures on live on the Borel σ-algebra and not on Mathlib's product σ-algebra MeasurableSpace.pi (). The pair is Function.update s i t. Players form a type ι with Nonempty ι; each S i is nonempty, compact and Hausdorff with BorelSpace (S i); payoffs are h : ι → Profile S → ℝ with each h i continuous. Deviations are all maps ζ : S i → S i with Measurable ζ.
The predicate IsCorrelatedEq h μ requires IsProbabilityMeasure μ and, for each player and measurable deviation, both integrability of the integrand and nonnegativity of its integral. The integrability clause prevents a trivializing reading in which a non-integrable integrand, whose Lean integral is , satisfies (4) vacuously; restricting deviations to continuous maps, or using the product σ-algebra, would also change the theorem and is ruled out.
The f-set net is indexed by the f-sets containing a fixed profile , which are directed; the paper's "ordered by inclusion of the sets " over all f-sets is not directed, and anchoring repairs this without affecting any statement of the paper. A correlated equilibrium of is encoded by its finite support and weights (IsFSetCE). The special case is stated for a regular cluster point of the given by these constructed objects, not for an arbitrary measure.
A complete development needs Banach–Alaoglu or the compactness of probability measures on a compact space, the Riesz–Markov–Kakutani representation (RealRMK), regularity of measures (Measure.Regular), Urysohn's lemma, and uniform continuity on compact spaces, all available in Mathlib in some form. Proofs of any milestone, including the general-purpose milestones 2, 3 and 5, are welcome.
The contact process is the basic model of an infection spreading on a lattice: each infected site recovers at a constant rate, and each healthy site becomes infected at a rate that depends on how many of its neighbours are infected. It was introduced by T. E. Harris in Contact Interactions on a Lattice (Ann. Probab. 2, 1974), and it became one of the central examples of interacting particle systems, alongside the voter model and the stochastic Ising model (Liggett, Interacting Particle Systems, 1985, Ch. VI). Its main question is whether a finite infection dies out with probability one or survives forever with positive probability, and how that answer depends on the rates.
Harris's paper gives the first answers. It shows that, under natural conditions on the rates, the probability of survival is monotone, subadditive and submodular as a function of the initial set, and it uses these properties to prove a condition for certain extinction: Theorem 7.1. For the linear contact process (recovery rate , infection rate per infected neighbour) the condition is . Holley obtained Theorem 7.1 by different methods at about the same time (footnote 4, p. 981); Holley and Liggett (Ann. Probab. 3, 1975) later developed the duality theory of such processes.
Let be the -dimensional integer lattice, . Sites are neighbours, , if ; is the set of the neighbours of . A configuration is a finite set of infected sites; is the set of all of them, , and means and has a neighbour in .
The parameters are a recovery rate and infection rates . The contact process started from a finite set is the continuous-time Markov chain on that leaves at rate
and jumps to () at rate and to () at rate (4.5). The empty set is absorbing. Write for its transition function, for the transition matrix of its imbedded jump chain, and
The process is increasing, subadditive or submodular if, for all and , respectively , , or ((5.2)–(5.4)).
If
then
Theorem 7.1 gives a computable sufficient condition for extinction that holds in every dimension and for every non-linear infection law satisfying it. For the linear process it gives the lower bound on the critical infection rate; the paper's §9 shows conversely that the process survives for large , so the critical rate is non-trivial. The monotonicity, subadditivity and submodularity theorems of §§5–6 are the comparison tools on which much of the later theory of attractive spin systems was built, and Lemma 5.8 is the prototype of comparison between processes with ordered rates.
The results are proved in the paper, and the proof of Theorem 7.1 is half a page once §§5–6 are available. No machine-checked version of the contact process, of its comparison theorems, or of Theorem 7.1 is known to exist. A formalization produces a continuous-time Markov chain with unbounded rates and an absorbing state on a countable state space, its minimal transition function, a non-explosion criterion, first-step analysis for absorption probabilities, and coupling arguments for monotone comparison. The companion mission Contact Interactions on a Lattice II treats Theorem 7.6, the integrability of the expected size, on the same model.
The obvious argument is first-step analysis on singletons and pairs, (7.2) and (7.3). It fails as it stands because (7.3) involves of every three-point set , and no finite system of first-step equations closes; some inequality between survival probabilities of nested sets is needed, and the milestones record the one the paper uses. Submodularity, subadditivity and monotonicity are not consequences of the rates by direct computation: the paper proves each by building several contact processes on one probability space (Tables 1–4), which in a formal development means constructing couplings of chains with unbounded rates and checking that each marginal has the right law. The reduction from general to the linear case also needs the comparison Lemma 5.8, another coupling. Finally the rates grow linearly in , so uniformization does not apply and non-explosion (Theorem 4.3) must be proved before transition probabilities are known to sum to one.
The process is the countable-state chain of §4, not the Feller process on all subsets of of §2: sites are Fin d → ℤ, configurations are Finsets, and is the minimal transition function of the rates (4.4)–(4.5), defined as the increasing limit of Feller's backward recursion. There is no measure-theoretic process object; and enter only through . Consequently Theorem 4.1 ( is stochastically closed) is built in, and every statement is made for finite initial sets, including those the page makes for arbitrary ((5.2)–(5.4), Lemma 5.8); for infinite the page itself notes .
The committed conventions:
Trivializing formalizations are ruled out: the survival probability is not taken from an arbitrary semigroup or a uniformization (the rates are unbounded); is not a real infimum or limUnder, whose junk value would make the goal free; is indexed by the number of infected, not vacant, neighbours, and forbids spontaneous infection; and (7.2) is stated for every site and every neighbour, not for one fixed pair.
A complete development needs: non-explosion for chains with linearly growing rates; the Chapman–Kolmogorov and strong Markov properties of the minimal chain at jump times; lattice symmetries (translations and coordinate reflections) acting on the chain; and couplings of several contact processes realised as one chain on a product type space. The chain infrastructure and the coupling lemmas are reusable beyond this mission, in particular by its companion. Contributions to any milestone are welcome, including proofs of the milestones under the paper's hypotheses by methods other than Harris's.
Telephone exchanges, call centers, hospital wards and cloud server pools are queues with a large number of parallel servers. For such systems two classical approximations pull in opposite directions. Holding fixed and letting the traffic intensity gives the conventional heavy-traffic limit, in which almost every customer waits. Letting grow with fixed below one gives a limit in which almost nobody waits. Real systems sit in between: a positive fraction of customers wait, and waits are short. Halfin and Whitt (Operations Research 29 (1981) 567–588) identified the scaling that produces this middle regime and the limit laws it yields. The scaling is now called the Halfin–Whitt or quality-and-efficiency-driven (QED) regime, and it underlies square-root staffing: run servers for an offered load of Erlangs. Borst, Mandelbaum and Reiman (Operations Research 52 (2004) 17–34) built staffing rules for large call centers on it.
Timeline. Erlang (1917) gave the delay probability of the M/M/s queue. Iglehart (1965) proved diffusion limits for M/M/s queues with the number of servers growing and the traffic intensity fixed. Halfin and Whitt (1981) proved that the delay probability has a limit strictly between 0 and 1 exactly when converges to a positive constant (their Proposition 1), derived the limit of the stationary queue length (Theorem 1), and extended the process-level limit to GI/M/s queues. Later work extended the regime to many-server queues with general service times and abandonment.
An M/M/s queue has Poisson arrivals at rate , servers, and exponential service times with rate . Its traffic intensity is . The number of customers in the system (waiting or in service) is a birth–death process on with birth rate and death rate in state . When , converges in distribution to , whose law is the unique probability distribution solving the balance equations of this chain. The probability of delay is the Erlang-C formula.
The mission studies a sequence of such queues: queue has servers, the fixed service rate , and arrival rate with and . Its stationary queue length is , and the scaled queue length is
Throughout, and denote the standard normal distribution function and density, and for
The standing assumption of the paper's Section 2 is the heavy-traffic condition
Under (2.2), with ,
The limit is exponential with rate above zero and a normal law truncated at zero below it, with masses and .
and for with ,
Theorem 1 is the stationary half of the Halfin–Whitt regime. It turns the Erlang-C formula, a ratio of sums with terms that is opaque for large , into a two-parameter description of congestion: is the fraction of customers who wait, is the scaled safety margin of servers, and the conditional laws above give the distribution of the number waiting and of the number of idle servers. Proposition 1 and Theorem 1 are what square-root staffing rules evaluate; Corollary 1 supplies the mean and variance used in the paper's numerical approximations.
All results of this mission are proved in the paper, by direct calculation from (1.1)–(1.3), Stirling's formula and the central limit theorem for Poisson variables. None has a machine-checked proof. Proposition 1 and the two Section 1 facts are posed on the platform as open theorems from the Gross et al. queueing textbook series; this mission adds the conditional and local limits, the weak-convergence theorem and the moment results on the same definitions, so that a closed development would give a fully checked derivation of the Halfin–Whitt limit from the balance equations.
The stationary law is explicit, so nothing here needs a stochastic process. The difficulty is analytic and uniform: each statement is a limit of ratios of sums of or infinitely many terms, below and a geometric tail above , in which and at linked rates. The lower half needs a central limit theorem for Poisson laws whose parameter moves with and is evaluated at a moving point; the local limits (2.10) and (2.12) need Stirling's formula with explicit control of to second order. Weak convergence then needs tightness, or a direct argument from the conditional limits, and the moment limits need uniform integrability, which the fixed- moment recursions do not give by themselves. Holding fixed, or taking limits in and one after the other, gives degenerate answers ( or ); the two limits must be taken together.
The Lean development lives in the namespace HalfinWhitt81.Stationary. The law of is a sequence p n : ℕ → ℝ satisfying IsSteadyState (fun _ => lam n) (mmcDeath μ n) (p n) of the referenced definition QueueingFundamentals.BirthDeath.Balance (nonnegative, summing to one, solving the balance equations of the M/M/n chain); the Erlang-C formula and are erlangC and halfinWhittAlpha of QueueingFundamentals.BirthDeath.Erlang, and , are Mathlib's cdf (gaussianReal 0 1) and gaussianPDFReal 0 1. These, and the three open theorems for (1.1)–(1.3), (1.2) and Proposition 1, come from the Gross et al. (2008) series and are referenced, not restated. The related Borst–Mandelbaum–Reiman items (DimCallCenters.*.lemma_4_1, for the continuous extension of Erlang-C) state a different result and are not used.
Conventions committed to:
p n (probLE, probGE, probEqInt); a conditional probability with is the ratio ; is Int.floor, with for ;The goal cannot be met trivially: the law of is the M/M/n steady state, not a free sequence; the limit measure is asserted to exist together with its three properties and the convergence, so no vacuous "for every " reading is possible; and the statement alone is Proposition 1, already posed.
A complete development needs: the closed form of the M/M/n steady state, Poisson central limit and local limit theorems with a moving parameter, Stirling's formula with error terms, a criterion for weak convergence from convergence of distribution functions, and uniform integrability for the moments. The Poisson limit theorems and the weak-convergence criterion are reusable beyond this mission. Proofs of the referenced open theorems, of individual milestones, and alternative routes to Theorem 1 (moment convergence, or the process-level limit) are all welcome.
Many stochastic systems have an accumulated cost or passage time that grows with the length of an observation window. Splitting a window at an intermediate time gives an upper bound on the total, even when it does not give an equality. First-passage percolation and products of random matrices are examples discussed by Kingman (1973). A central question is whether the cost per unit time settles to a long-run rate on almost every sample path.
Hammersley and Welsh introduced subadditive stochastic processes in 1965. Kingman's 1968 theorem established the almost-sure limit for the stationary process considered here. His 1973 paper restated the result, identified the limit's expectation, and set out the process model and related formulations used in later applications. The 1973 article explicitly attributes the proof of Theorem 1, its maximal inequality, and its decomposition to the 1968 work; this mission formalizes the statements as presented in the 1973 paper.
Fix a probability space . For integers , let be a measurable random variable. Think of as the accumulated quantity over the interval from to . Condition S₁ is subadditivity: whenever . The stronger equality defines an additive process.
Condition S₂ says that shifting every interval one time unit forward leaves the joint distribution of the whole family unchanged. It concerns the law of as a single countable path. The one-dimensional statement that each has a distribution depending only on is called S₂′ in the paper; it does not replace S₂. Condition S₃ says that every positive-time variable is integrable and that, for some real , its mean satisfies for all . A subadditive process satisfies S₁, S₂, and S₃.
The associated mean growth rate is . The time index starts at one in this infimum because division by zero would introduce an unrelated value. S₃ gives a finite lower bound; the subadditive mean relation makes this infimum the limit of . Kingman also considers the invariant σ-field : events determined by the entire path and unchanged by the shift . It records the part of the process that can remain random in the limiting rate. Source: §§1.1–1.2, pp. 883–885.
For every subadditive process there is an integrable real random variable such that
These are three distinct claims: almost-sure convergence, convergence in mean, and an identity for the limit's expectation. The limit need not be a constant. The milestone list also covers the convergence of the means, the maximal inequality (1.2.5), the decomposition (1.2.6), the measure-preserving formulation (1.3.4)–(1.3.5), and the representation through in (1.2.4). Each statement comes from the 1973 paper, §§1.1–1.3.
For a measure-preserving map , condition Sᴱ concerns integrable functions with for and a linear lower bound on their expectations. It yields an integrable with almost surely and in mean. Neither invertibility nor ergodicity of is assumed. Source: §1.3, p. 886.
The theorem assigns a finite sample-path growth rate to an entire class of stationary subadditive systems. It also ties the average of that rate to the infimum of the normalized expected values. The equality is useful when a system's finite-window means are easier to estimate than its individual long-run paths. The invariant σ-field statement explains why a stationary system can have different rates on different paths without contradicting the mean identity. Kingman's examples show how the same framework reaches percolation and matrix products.
The result is mathematically proved, as the 1973 article states. The remaining work here is a machine-checked development of its process model and the displayed results. A published Prove2Me item, PalmQueueing.Ergodic.kingman_subadditive, is open and concerns an ergodic bijective flow with a constant possibly infinite limit; it does not supply this nonergodic finite-limit theorem or convergence in mean. The draft statements in this mission compile with proof placeholders. No machine-checked proof of these new statements is claimed.
Subadditivity gives bounds when intervals are joined, but it does not express as a sum of identically distributed increments. The ordinary additive ergodic theorem therefore does not immediately give convergence for . Nor does convergence of the expectations alone force convergence on individual paths or in mean. The process may also have a nonconstant limit: stationarity is a joint-law condition, not an ergodicity assumption that erases invariant information. These are the gaps the formalization must close without strengthening the hypotheses. Source: §§1.1–1.3.
Lean represents as a function of two natural-number indices and a sample point, but every condition and conclusion uses only . S₁ and the Sᴱ cocycle inequality follow the paper's pointwise displays; random-variable equality in the decomposition is stated almost surely at each valid index pair. Measurability of each valid coordinate is explicit. S₂ compares two probability measures on the full countable path space, so equality of individual marginals cannot satisfy it. The probability measure is normalized, and S₃ requires Bochner integrability to keep every mean finite. The constant is a real infimum over positive times, used only under S₃. The goal's limit is real and integrable; Kingman's separate Theorem 2 treats a possible value of and belongs to another mission.
The invariant σ-field is the pullback of the path-space shift-invariant σ-field. Its measurability claim is made through an almost-everywhere equal version, since almost-sure limits are insensitive to changes on null sets. Conditional expectation uses this explicit sub-σ-field. All limits in this mission take positive integer time to infinity. The Sᴱ definition requires measure preservation but no inverse and no ergodicity. Thus neither a marginal-law substitution for S₂ nor an ergodic constant-limit specialization can trivialize the target.
A complete proof can reuse Mathlib's measure theory, conditional expectation, product measurable spaces, measure-preserving maps, and subadditive-sequence results. The two process definitions, the invariant σ-field interface, and auxiliary statements are useful to later formalizations of stationary growth models. Contributions that prove the stated results or develop general-purpose lemmas for these objects fit the mission.
Population models often allow each individual to produce a new individual or die at rates that change over time. Seasonal conditions, exposure to an epidemic, and changing conditions in a laboratory population all make a constant rate a restrictive assumption. In Kendall's 1948 paper, the question is how the entire distribution of the population size evolves when the per-individual birth and death rates are prescribed functions of time. The distribution matters even when its mean is known: a population can have a stable expected size while still having a substantial chance of extinction. Kendall presents the varying-rate model as a generalization of the constant-rate process discussed by Feller in 1939 (Kendall 1948, §1).
This mission concerns Kendall's solution for a population descended from one ancestor. It includes the explicit distribution, the forward equations that connect it to the birth and death model, and the formulas for its mean, variance, and chance of eventual extinction. The paper has no numbered theorems; its results are identified here by its equation numbers and printed pages.
At time , let be the number of individuals. Each individual gives birth at instantaneous rate and dies at rate , so a population of size moves to at rate and to at rate . Both rates are nonnegative. The initial state is . Write for the probability that . The forward equations in §2, (2)–(4), p. 2 are
The formula for reflects that a population already at zero cannot reproduce. The term vanishes at , as it must. The model is expressed through these real-valued probability functions; it does not require a sample-space construction of a stochastic process.
Define the integrated rate difference and the function by §2, (10a)–(11), p. 4:
Set and . Kendall's modified-zero geometric law is and for . The zero state has its own mass; the positive states form a geometric tail. For the nonnegative rates in this mission, and on , so the displayed formulas have their ordinary probabilistic meaning.
The goal is the full claim of §2, (8), (10a)–(12), pp. 3–4: the explicit starts from one ancestor, is nonnegative and sums to one for every , and satisfies the forward equations above. In symbols, the distribution part is
The milestones record the paper's intermediate statements in reading order: the rational generating function in (9); the pair of equations for and obtained from the generating-function equation (6); the equations for and ; the differential equation and integral representation of ; the alternate formulas (10b)–(10c); and the explicit expressions (12). Each is a statement made in the source, with the page and equation displayed beside its milestone.
The companion target from §3, (18)–(19), p. 6 writes and states
When has finite limit , the limiting extinction chance is . Companion statements also retain the mean , all three expressions for the variance in (14c), the criterion that extinction has zero chance exactly when vanishes identically, and the necessary divergence of for almost-sure extinction (Kendall 1948, pp. 4, 6–7).
The geometric law supplies every finite-time population probability from the rate functions. Its zero mass yields an extinction probability without taking limits of an unspecified process, while its first two moments quantify expected growth and fluctuations. The extinction criterion distinguishes a population that dies out with probability one from one that retains a positive chance of survival even when its eventual mean behavior is simple. The variance formulas give later sections of Kendall's paper a way to compare rate schedules with the same expected population (§§3, 6).
The result was proved in the 1948 paper. The work here is to state its model and conclusions precisely in Lean, preserving the initial condition, normalization, boundary state, and time-dependent rate conventions. The current files are theorem statements with proof placeholders; a successful build checks their syntax and types, not the mathematical proofs. Once proved, the definitions and the moment and extinction statements can also support formal work on time-dependent branching and population models.
Knowing the expected population is insufficient to determine the distribution. The forward equation for each couples it to both neighboring states, producing an infinite system. A direct finite truncation would change the birth rate at its upper boundary and would therefore no longer be Kendall's model. The zero state also behaves differently from positive states: a purely geometric law on all does not capture its mass. The generating function has a rational form, but its time dependence must still agree with the forward system for every state and with a normalized probability law. The extinction statement adds an improper integral, whose finite and divergent regimes require distinct limits.
Lean represents as continuous functions that are nonnegative for . The paper calls the rates specified functions and assumes their nonnegativity; global continuity is an explicit convenience for the two-sided derivatives and interval integrals. Only nonnegative time appears in the probabilistic statements. The oriented intervalIntegral from zero to represents every finite integral. HasDerivAt expresses each derivative, and HasSum expresses both normalization and the moment and generating-function series. The law lives on natural-number states, with handled separately. The coefficient at state is the real number , not an implicit extension to a negative state.
The positivity of on nonnegative time must follow from the rates. The definitions are total Lean real functions, so a result that relies on a division states the hypotheses that keep its denominator nonzero. The limit expresses divergence of the paper's improper integral. No uniqueness of solutions to the forward equations is included, because the cited passage does not establish that claim. The goal requires the explicit law to solve the forward equations and to be a probability law; merely expanding its generating function would leave the population model unformalized. Contributions that prove the formulas, establish the required positivity and convergence facts, or develop reusable lemmas for time-dependent linear birth and death equations all fit the scope.
The traveling salesman problem is NP-hard in general, so special cost structures under which it can be solved exactly in polynomial time are of lasting interest in combinatorial optimization and scheduling. One of the earliest and most cited such cases comes from sequencing on a machine whose condition is described by a single real number: a furnace temperature, a knife setting, a fill level. Each job must start at a prescribed state and leaves the machine in another, and changing the state between consecutive jobs costs money or time. Finding the cheapest cyclic order of the jobs is a traveling salesman problem with asymmetric costs.
P. C. Gilmore and R. E. Gomory solved this problem exactly in 1964 (Oper. Res. 12(5), 655–679) with an algorithm of simple steps. Their construction became the standard example of a solvable TSP case: it is the starting point of the survey literature on polynomially solvable TSPs (Gilmore, Lawler and Shmoys 1985; Burkard, Deineko, van Dal, van der Veen and Woeginger 1998), and it appears in the no-wait flow shop literature, where two-machine no-wait scheduling reduces to exactly this cost structure.
There are jobs . Job must be started when the state of the machine is and leaves the machine in state ; the jobs are numbered so that implies . Two cost densities satisfy : raising the state through costs per unit, lowering it costs per unit. The changeover cost of having job follow job is
A permutation of the jobs assigns to each job its successor and has cost . It is a tour if for every nonempty proper subset of the jobs, i.e. if it is a single cycle through all jobs.
A permutation ranks the if implies . The interchange swaps and ; applying it to gives (first , then ), which exchanges the successors of and , at cost . The graph links and for every ; a spanning tree of is a minimal set of additional arcs that makes it connected, with cost . Node is of type 1 if and of type 2 otherwise.
Given a minimal cost spanning tree of made of arcs , the tour is obtained from by executing the interchanges , , first those of type 1 in decreasing order of , then those of type 2 in increasing order of .
This is the paper's main theorem. It fixes no constant and no special form of ; it asserts that the specific tour produced by the algorithm is optimal among all tours.
In the order the proof uses them:
Off the goal's path: Theorem 7, a minimal tour for is minimal for .
The theorem shows that a traveling salesman problem whose costs come from a one-dimensional state is solved by three polynomial steps: sorting (an optimal assignment), a minimum spanning tree over candidate arcs, and a prescribed sequence of interchanges. It is the base case for a family of later results on solvable TSPs and for the two-machine no-wait flow shop, where it gives an exact polynomial algorithm.
The result has been proved since 1964. No machine-checked proof of it is known to exist. The proof in the paper argues largely from figures ("evident geometrically"), and its statement of Theorem 3 lists the interchanges in an order that contradicts its own proof: executed in the printed order, the paper's numerical example yields a tour of cost 39 instead of the optimum 34. A formal proof settles which order is correct and fills in the geometric steps. Partial contributions are useful: the permutation facts (Lemmas 1, 8 and Theorem 2) are independent of the cost model and reusable.
The obvious argument fails at two points. First, interchanges do not commute in cost: once one interchange is executed, the cost of the next one depends on the new successors, so the cost of is not simply plus the tree cost for an arbitrary execution order. Showing that the specific order of Lemma 5 avoids all interference requires tracking how type-1 and type-2 nodes behave as interchanges are applied. Second, optimality is not a local statement: an arbitrary tour is not reachable from by tree interchanges, so the lower bound needs the separate underestimate and a counting argument relating every tour to a spanning tree of . Neither step follows from general minimum spanning tree theory.
Jobs are Fin (n + 1) (), so the paper's job is index ; the adjacent arc is indexed by q : Fin n and joins q.castSucc and q.succ. Permutations are Equiv.Perm (Fin (n + 1)), and is ψ * Equiv.swap i j (Mathlib's composition, "first , then "). Costs are real; (1) uses oriented interval integrals and (17) set integrals.
Explicit readings of the paper's loose phrases:
The order of is that of the proof of Lemma 5 and of steps T2–T4 (p. 673), not the order printed in Theorem 3.
Trivializing formalizations are ruled out: the goal quantifies over all tours, not over permutations (that is Theorem 1) nor over tours reachable from ; is constructed from and , not taken as an arbitrary tour of the right cost; is both inclusion-minimal and cost-minimal; and the costs keep both branches of (1) with general densities, not . The TSP items already on the platform concern symmetric or metric distances with tours as visiting orders, a different model, and are not reused.
Needed infrastructure: cycle structure of permutations under transpositions (Mathlib's Equiv.Perm.SameCycle), connectivity of finite simple graphs, interval integrals of locally integrable functions. Contributions to any milestone are welcome; the purely combinatorial ones (Lemmas 1, 8, Theorem 2, Lemma 7) are independent of the integrals.
Freedman's inequality bounds the probability that a martingale with increments bounded above by reaches a level before its accumulated conditional variance exceeds : the bound is (D. A. Freedman, On Tail Probabilities for Martingales, Ann. Probab. 3 (1975) 100–118, Theorem (4.1), doi:10.1214/aop/1176996452). It is the standard tool for concentration of martingales whose variance is random, and it is used throughout online learning, bandit theory and the analysis of randomized algorithms.
The same paper shows that the exponent cannot be improved in general. For a martingale with increments bounded by in absolute value, Freedman's estimate (1.10) bounds from below the probability that level is crossed while the conditional variance used is still below . The analytic core of that lower bound is isolated in the paper as Proposition (4.10), p. 109: a statement about a single nonnegative random variable whose Laplace transform is controlled from both sides. The paper calls its proof "disappointingly hard". This mission formalizes Proposition (4.10) and the steps of its proof.
Let be a probability space. For real put (Definition (1.2), p. 101)
Both are nonnegative and equal near . Fix and a nonnegative random variable . The two Laplace-transform bounds are, for every ,
In the paper is the conditional variance accumulated up to the first time the martingale reaches ; for that variable (4.11a) and (4.11b) are Theorems (1.12) and (1.8). Here is abstract. The hypotheses are consistent: the first-passage time of standard Brownian motion to level has , and since for , it satisfies both bounds.
The parameter conditions (4.12) on positive reals are
The proof uses the notation (4.14): , , , , the five intervals , , , , , and the terms
In Lean these objects are FreedmanTail.LowerTail.e, f, LaplaceUpper, LaplaceLower, ParamConditions, phi, lamStar, kStar, NStar, I1–I5 and eta.
Under (4.11a)–(4.11b) for all and (4.12a)–(4.12c),
In the order of the proof:
The result. Proposition (4.10) converts two-sided control of a Laplace transform into a lower bound for a left tail, with an explicit constant and an explicit range of validity. Applied to the crossing variance it gives Freedman's lower bound (1.10) for , which matches the exponent of the upper bound of Theorem (4.1) up to the term . That is the statement that Freedman's inequality is sharp in the regime , .
Formalizing it. The proposition is proved in the 1975 paper; no machine-checked proof is known. Mathlib contains Chernoff-type upper bounds and the layer-cake formula, but no lower tail bound derived from two-sided Laplace-transform control. The mission produces a self-contained, constant-explicit Tauberian-type lemma for nonnegative random variables, usable without any martingale structure. The companion missions of this series formalize Theorem (4.1) and the Laplace bound (1.8); together they would give the sharpness statement for martingales.
The obvious route is to invert the Laplace-transform bounds directly. A lower bound on does not by itself bound from below: the mass that makes the Laplace transform large could sit at small values of or be spread over a wide range. Without (4.11a) the conclusion fails, and with it every contribution from values of away from must be shown negligible at a precision of order , where is large. The main term is smaller than the total by the factor , so every error term must be estimated with constants explicit enough to stay below it. The thresholds (4.12b)–(4.12c) are what make all of these comparisons hold at once.
The probability space is a measurable space Ω with a measure P and [IsProbabilityMeasure P]. is a measurable function Ω → ℝ with W ω ≥ 0 for every ω. The expectations in (4.11) are Bochner integrals of and ; for these integrands lie in , so they are integrable and the integrals are genuine expectations. Probabilities are P.real {ω | W ω < x}, with the strict event as on the page. The integrals in are Lebesgue integrals over and over the intervals ; the integrand is a nondecreasing function of times , hence measurable and, as , integrable.
Conventions and corrections, each also disclosed in the items:
A trivializing formalization is ruled out: the hypotheses are satisfied by the Brownian first-passage time above, the parameter conditions hold for instance at , , , and no integral in a hypothesis or conclusion can take a default value .
Needed infrastructure: Markov's inequality and the layer-cake formula (both in Mathlib), the identity for , and elementary estimates of and of the convex function of (4.21). The layer-cake identity and the left-tail bound (4.18) are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the unnumbered steps (4.20)–(4.30).
The source is the published article in The Annals of Probability (a scanned copy); page numbers are the journal's.
Many problems in mechanics and optimal control are posed as the minimization of a convex functional of the form , where is a differential operator and is non-smooth: an obstacle, a friction term, a plasticity threshold. Splitting the variable, , separates the linear operator from the non-smooth function, and a Lagrange multiplier for the constraint turns the problem into a sequence of two simpler ones: a linear system in and a pointwise nonlinear problem in . The scheme that alternates between the two and then updates the multiplier is now called the alternating direction method of multipliers (ADMM). It is one of the standard algorithms of large-scale convex optimization, statistics and imaging (Boyd, Parikh, Chu, Peleato and Eckstein, 2011).
Gabay and Mercier (IRIA report RR-126, 1975; Comput. Math. Appl., 1976) gave a convergence proof of this method in Hilbert space, for a stepsize anywhere in , where is the penalty parameter of the augmented Lagrangian.
Timeline.
and are real Hilbert spaces; and are the inner product and norm of , the norm of . is a continuous linear operator and is a continuous linear functional on , with value at . The dual of is identified with . The function is a sum where
The problem is
and a solution is a point where this value is finite and minimal. The Lagrangian and augmented Lagrangian are, for and ,
The modified dual algorithm (3.4) starts from any and, for ,
denotes the orthogonal projection of onto the range , which is closed by (2.5).
For and every stepsize with
every run of the algorithm satisfies
where is the unique solution of . The multipliers need not converge.
and its sum over . 7. for . 8. (3.22)–(3.23): a contraction-plus-summable-forcing recursion for , and the scalar lemma that such recursions tend to . 9. and for .
The theorem says that ADMM converges without any step-size tuning beyond , and that the primal iterates converge in norm in infinite dimension, which is what makes the method usable for finite element discretizations of variational problems (the companion mission on internal approximations treats the discretization). It covers obstacle problems, Bingham fluids and elasto-plastic torsion, where is an indicator or a non-differentiable norm.
The result is proved in the 1975 report. To our knowledge it has no machine-checked proof. Formalizing it adds a library-level convergence theorem for ADMM in Hilbert space with -valued convex functions, a saddle-point existence theorem for linearly constrained convex problems, and the energy estimate (3.19) as a reusable lemma. The formalization also fixes two defects of the printed text (see Formalization scope): a sign in Step 1 and a qualification hypothesis that is too weak.
The energy estimate (3.19) only controls the multiplier through its component in , and only the -error through . The natural first idea, a Lyapunov function in alone that decreases at each step, does not work for : the component obeys a separate recursion whose contraction factor is below one only for , and whose forcing term must be shown summable from the -estimate. The existence of a multiplier, i.e. of a saddle point, is a separate difficulty: it needs the subdifferential chain rule in infinite dimension, under a constraint qualification.
Lean conventions:
InnerProductSpace ℝ with CompleteSpace; multipliers are elements of ; is a StrongDual ℝ V.f₁' at every point (HasGradientAt) that is continuous; "weakly continuous on finite-dimensional subspaces" is then automatic.EReal, with IsProperFn, IsConvexFn, IsSubgradient from the published InertialFB.IFB.ConvexAnalysis and Mathlib's LowerSemicontinuous. No subtraction in EReal occurs: the variational inequalities (3.6), (3.9) are stated as subgradient inclusions, and the Lagrangians as a real part plus .Bornology.IsBounded (Set.range λ).Corrections to the printed text, each explained in the item's statement:
Ruled out: the solution is a hypothesis of the goal, so the hypotheses must not be contradictory. They are met by , , , , , and a proper excludes the degenerate reading in which every point "solves" with value .
A complete development needs: existence of minimizers of coercive convex l.s.c. functions on a Hilbert space; the subdifferential sum and chain rules under a continuity qualification; orthogonal projections onto closed ranges; and elementary facts about summable sequences. The saddle-point theory (Theorems 2.1–2.2) and the scalar lemma (3.23) are reusable beyond this mission. Proofs of any milestone are welcome, as are proofs of the goal by a different route.
For sums of independent bounded random variables, the inequalities of Bernstein and Bennett bound the probability of a large deviation by an exponential in the deviation and the variance (Bennett 1962; Hoeffding 1963). Many processes met in probability, statistics and learning theory are not sums of independent terms but martingales or supermartingales: sequential estimators, stochastic approximation iterates, the regret of an online algorithm. For them the relevant scale is not a fixed variance but the conditional variance accumulated along the path, which is itself random.
David A. Freedman's paper On Tail Probabilities for Martingales (Ann. Probab. 3 (1975) 100–118) extended the Bernstein–Bennett inequality to this dependent case, with the conditional variance in place of the variance and with a bound that holds simultaneously for all times. The result, now called Freedman's inequality, is the standard tool for martingale concentration with variance-sensitive rates and is used throughout bandit and reinforcement-learning analyses, random-graph arguments and stochastic optimization. This mission formalizes that theorem, (4.1) of the paper, together with the chain of lemmas the paper uses to prove it.
Let be a probability space and an increasing sequence of sub--fields of (a filtration). Let be real random variables with measurable with respect to . Define
Freedman treats as an intrinsic clock: read at time rather than , the process resembles Brownian motion. The paper's condition (3.4) is
so is a supermartingale whose increments are bounded above by ; no lower bound is assumed. The auxiliary functions are and , with time first and position second. A stopping time takes values in with , and is allowed.
In Lean these are FreedmanTail.Bernstein.S, V, T (on Filtration ℕ m, with V given by Mathlib's condVar) and FreedmanTail.Bernstein.e, Q.
Under (3.4), for all and ,
The first bound is of Bennett type, the second of Bernstein type. The event is a union over all times; the bound does not depend on any horizon.
In the order the paper's proof uses them:
The inequality bounds the probability that a supermartingale ever reaches level before its accumulated conditional variance exceeds . Since it holds for all times at once, fixed-horizon versions follow immediately, as do versions with stopping times, and with a peeling argument over it gives the variance-adaptive confidence sequences used in sequential testing and in the analysis of algorithms. Freedman's paper uses it to derive the law of the iterated logarithm for martingales; later work uses it wherever a martingale's conditional variance is much smaller than the square of its increment bound.
The theorem has been proved for fifty years. What this mission adds is a machine-checked statement and proof of the full infinite-horizon form under the one-sided hypothesis (3.4), together with the exponential supermartingale and the optional-stopping bound (3.3) as reusable lemmas. Prove2Me already has fixed-horizon Bernstein-form consequences for martingale differences; the infinite-horizon Bennett form under (3.4) does not appear in Mathlib or on the platform.
The naive route of applying Markov's inequality to at a fixed gives a bound for one time only and requires a deterministic bound on . Taking a union over all loses everything. The content of the theorem is that the random clock and the supremum over time can both be absorbed, which requires an exponential process compensated by the random and an optional-stopping bound for stopping times that may be infinite with positive probability. The process need not be uniformly integrable, and the increments have no lower bound. A second, smaller, difficulty is the variance form of (3.5): the bound uses rather than , which is strictly sharper when and is needed to compensate with conditional variances.
Lean conventions this mission commits to:
X : ℕ → Ω → ℝ used from index (X 0 is never read), so , and carry the paper's indices. The filtration is Mathlib's Filtration ℕ m, and " is -measurable" is StronglyMeasurable[ℱ n] (X n) for .condVar (ℱ (n - 1)) (X n) P. Mathlib sets a conditional expectation of a non-integrable function to , so every increment is assumed square integrable (MemLp (X n) 2 P). This is the one hypothesis added to the page. Under (3.4) the page also allows increments of infinite variance, for which its is ; the formalization narrows the class of processes and leaves every conclusion as printed. Milestone (3.5) likewise assumes , which is the case the page reduces to.Supermartingale.Ω → WithTop ℕ with IsStoppingTime; is . In (3.3) the integral over is a lower Lebesgue integral in , so the bound does not presuppose integrability, and , are read only on .A fixed-horizon statement (, or ), a martingale hypothesis , or a two-sided bound would each be a strictly weaker theorem than (4.1) and is not an acceptable formalization of the goal.
The development needs exponential supermartingales compensated by conditional variance, optional stopping for stopping times that may be infinite, and elementary real analysis of . The real-analysis milestones (3.1), (3.2) and the two calculus steps are independent and reusable; (3.5) is a self-contained moment-generating-function bound; the supermartingale and (3.3) are reusable for every exponential-supermartingale argument. Contributions to any milestone, and alternative proofs of the goal, are welcome.
Reliability theory classifies life distributions by how they age. A device whose remaining life, once it has survived to age , is stochastically shorter than the life of a new device is called new better than used (NBU). The NBU class, together with the classes IHR (increasing hazard rate) and IHRA (increasing hazard rate average), organizes much of the theory of maintenance and replacement: Marshall and Proschan showed that the NBU property is what makes certain replacement policies beneficial, and Barlow and Proschan's monographs build the statistical theory of reliability on these classes.
A question that runs through this literature is where such ageing properties come from physically. Esary, Marshall and Proschan (Ann. Probability 1973) answer it for shock models: a device is hit by shocks arriving in time as a Poisson process, each shock adds a random amount of damage, and the device fails when the accumulated damage exceeds its threshold. Section 4 of their paper treats a fixed threshold and shows that the life is IHRA for every damage law. Section 5, the subject of this mission, lets the threshold itself be random, which models the variation between individual items of a production lot. It then asks which ageing properties of the threshold law are inherited by the life distribution, and which are forced if the inheritance is to hold whatever the damage law.
All distributions are laws of non-negative random variables. For a distribution on with for (a damage law), denotes the -fold convolution of , with the point mass at ; thus for independent .
A threshold law is a distribution with for ; write for its survival function. If the threshold is independent of the damages, the probability of surviving shocks is
If shocks arrive as a Poisson process of rate , the device's life distribution has survival function
A survival function is NBU if for all ; it is IHR if is non-increasing in for each , and IHRA if is non-increasing in . The discrete analogue of NBU for the sequence is submultiplicativity, .
For a threshold law with for :
the quantifier ranging over every damage law ; and if is NBU, then for every damage law and every the life distribution of (5.2) is NBU.
Theorem 5.1 (the life is exponential for every iff is exponential) and Theorem 5.2 (b), (c) (an IHR threshold makes non-increasing for every ; non-increasing for every forces to be IHRA) are posed as companion statements from the same section.
Theorem 5.3 is a characterization: the NBU class is exactly the class of threshold laws for which the cumulative-damage mechanism preserves the discrete NBU property under every damage law. Combined with Theorem 3.1 (3.5), it gives a physical derivation of NBU life distributions: an item with an NBU random strength, subject to Poisson shocks with arbitrary i.i.d. non-negative damage, has an NBU life. Theorems 5.1 and 5.2 place the exponential and the IHR/IHRA classes in the same framework, and the authors record that whether an IHRA threshold suffices in Theorem 5.2 (b) is left unresolved.
The results are proved in the paper. No machine-checked version is known to exist; this mission produces one. A complete development also supplies reusable infrastructure: convolution powers of laws on as Mathlib measures, Poisson mixtures of a sequence, and the ageing classes of p. 631 as predicates on survival functions.
The equivalence couples a property of one function, , to a family of inequalities indexed by every damage law, and the left side is about convolutions while the right side is pointwise. Two points make the statement harder than it looks. First, (5.1) as printed is , whereas the paper's proof works with ; the two agree only when and have no common discontinuities, and they can disagree as soon as has an atom where has one, a case the left side of the equivalence includes. A formal proof cannot invoke that convention. Second, the second sentence of the theorem passes through a Poisson series (5.2) whose terms involve the whole sequence , so the NBU property of is a statement about a power series in , not about any single .
Measure.conv power with , and is the mass of .Contributions welcome: proofs of the milestones, a library for Poisson mixtures and convolution powers of laws on , and the extra items of §5.
Many models in probability, statistical physics and the theory of stochastic networks are interacting particle systems: infinitely many sites, each in state 0 or 1, each updating at random according to the states of a few other sites. A basic question about such a system is ergodicity: does it have a unique stationary distribution, and does its law converge to it from every initial configuration? For infinite systems the question is hard, because the state space is uncountable and standard Markov chain arguments do not apply.
Holley and Liggett (Ann. Probab. 3 (1975), 643–663) introduced a class of such systems, the proximity processes, which arise from a coupling of more general weakly interacting systems (the settings of Vasershtein (1969), Dobrushin (1971) and Chover (1974)), and showed that each proximity process is dual to a process of finite sets, the branching process with interference. Duality turns a question about an infinite-dimensional process into a question about a process whose states are finite sets. The paper uses it to give short proofs of ergodicity criteria and, in its §5, to study the invariant measures of the voter model. Duality of this kind became one of the main tools of the field; see Liggett, Interacting Particle Systems (Springer, 1985).
This mission formalizes the discrete-time half of the paper: the duality theorem (1.6) and its first applications, Corollary (3.1) and Corollary (4.1).
Let be a countable set of sites and the set of configurations , with the product -algebra. For , is the set of occupied sites.
The data of the model are, for each site , a sequence of finite subsets of and a probability distribution on .
The proximity process is the Markov chain on whose transition function is the product measure
where puts mass on . In words: each site independently picks an index with probability and becomes exactly when the set contains an occupied site. denotes the law at time started from .
The branching process with interference (b.p.i.) is the Markov chain on the collection of finite subsets of with transition function
the sum over all sequences with : each particle at splits into particles on with probability , and particles landing on the same site merge. denotes probabilities for the chain started at .
For , .
For all , and ,
The proof is an induction on whose steps are four displayed identities on p. 647:
and the point mass on the all-zero configuration is the only stationary distribution; along the way, (3.5): .
The duality identity expresses every finite-dimensional "all vacant" probability of the proximity process, which determine its law, through a chain on finite sets. Consequences in the paper: a sufficient condition for convergence to the all-zero configuration (Corollary (3.1)), which in the nearest-neighbour example on gives ; the sharper range , i.e. , for that example (Corollary (4.1)), which the interference term makes possible; and, in continuous time, the analysis of the invariant measures of the voter model.
The results are classical and proved; a search of Prove2Me and Mathlib found no machine-checked proof of any of them. A formalization contributes a Lean model of an infinite-product Markov kernel on with its -step laws, a model of a set-valued branching chain, and the duality between them, which are reusable for other duality arguments (contact process, voter model, coalescing random walks).
The two sides of (1.7) are defined independently and live on different spaces. The left side is the time- law of a chain on the uncountable space , obtained by iterating an infinite product kernel; the right side comes from a transition matrix on the countable set of finite subsets of , whose entries are themselves infinite sums over sequences indexed by a finite set. Neither side can be computed in closed form beyond , so no direct evaluation proves the identity for general .
Two technical points stand in the way of a naive argument. Evaluating a product kernel on a cylinder event and integrating it against a previous law requires the kernel to be measurable in , a statement about cylinder sets of an infinite product that a hand proof passes over. And the natural recursion for -step probabilities of the b.p.i. adds the new step at the end, while the comparison with the proximity process needs information about the first step; the two orders agree only by a Chapman–Kolmogorov argument over a countable state space with -valued sums. Corollary (4.1) further needs quantitative estimates of survival probabilities for specific initial sets on .
All objects are in the namespace HolleyLiggett.Duality, in one definitions file.
Bool (true = 1), is Config I := I → Bool with the product -algebra, is Finset I.[Countable I], N : I → ℕ → Finset I (finite sets) with N i 0 = ∅, and f : I → PMF ℕ (probability distributions). A finite collection is the case for .Measure.infinitePi of the two-point measures; the -step law is proxLaw, iterating Measure.bind from the point mass at . Measurability of the kernel is a true fact that solvers must prove; it is not assumed.bpiProb follow the last-step recursion . All probabilities are in ℝ≥0∞, and each over sequences is an unconditional sum over ↥F → ℕ.The continuous-time duality (Theorem (2.12)), Corollaries (3.9) and (4.15) and the voter model of §5 are out of scope. Contributions welcome: the measurability and probability facts for proxStep, Chapman–Kolmogorov for bpiProb, and proofs of the milestones.
Newton's method for a nonlinear system , with , solves the linear system at every step. For large systems that solve is itself iterative (a Krylov method such as GMRES), and it is stopped early. The resulting inexact Newton methods, introduced by Dembo, Eisenstat and Steihaug (SIAM J. Numer. Anal. 19 (1982)), accept any step with , where the forcing term controls how accurately the linear system is solved. Their theory is local: it applies once the iterates are near a solution with invertible derivative.
Practical solvers (Newton–Krylov codes in large-scale simulation, nonlinear solver libraries such as PETSc's SNES and SUNDIALS' KINSOL) combine such inexact steps with a globalization, most often backtracking along the step. Eisenstat and Walker (SIAM J. Optim. 4 (1994)) gave the global convergence theory for this combination: what can be said about the iterates from an arbitrary starting point, with no assumption that a solution exists or that is invertible anywhere.
Timeline. Dembo, Eisenstat and Steihaug (1982) proved local convergence of inexact Newton methods. Dembo and Steihaug (Math. Program. 26 (1983)) studied truncated Newton methods for unconstrained minimization. Brown and Saad (1990) studied globalized Newton–Krylov methods with line searches and model trust regions, under the inner-product norm. Eisenstat and Walker (1994) gave the general framework treated here, for an arbitrary norm. Their 1996 paper (SIAM J. Sci. Comput. 17) proposed the forcing-term choices that are now standard.
Let be with an arbitrary norm , and let be continuously differentiable with derivative . A point is a limit point of if every ball contains for infinitely many .
Algorithm GIN (global inexact Newton method). Fix . At each , find a level and a step with
and set . Condition (2.1) says that reduces the norm of the local linear model by the factor . Condition (2.2) asks that itself decrease by a fixed fraction of that predicted reduction.
Algorithm MR (minimum reduction method). Fix and . At step , choose and a curve with for (5.1). Start at . While (2.2) fails for , replace by for some . Then set .
Algorithm INB (inexact Newton backtracking). Choose and an inexact Newton step at level . While (2.2) fails, shorten the step, , and raise the level, . INB is MR with the backtracking curve (6.1).
An algorithm does not break down if it produces an infinite sequence of iterates, in particular if every while-loop exits.
If Algorithm INB does not break down and is a limit point of at which is invertible, then
The statement assumes no solution, bounded level set, Lipschitz derivative or particular norm. The last clause says that backtracking eventually stops, so the local rate is governed by the forcing terms .
In attack order:
Further items, which are not milestones: Corollary 6.2 (exact Newton with backtracking takes full Newton steps eventually), Theorem 5.2 for Algorithm TL, Lemma 3.1 (existence of acceptable GIN steps), and Proposition 2.1 (the Goldstein–Armijo alpha condition implies (2.2) in the Euclidean norm).
The result. Theorem 6.1 is the global convergence guarantee for the inexact Newton backtracking method that Newton–Krylov solvers implement. It separates three outcomes: the iterates diverge, they accumulate only at points where is singular, or they converge to a solution with invertible derivative and eventually take the unmodified inexact Newton steps. In the third case the local theory of Dembo, Eisenstat and Steihaug applies from some iteration on, so the forcing terms alone set the convergence rate. Theorem 5.2 is the template: §§6–8 of the paper derive the convergence of backtracking, equality-curve and dogleg-type methods from it by verifying (5.6).
Formalizing it. The results are proved on paper and none of them has a machine-checked proof that we know of. The mission produces a library of algorithm-run predicates with explicit while-loops for inexact Newton methods. It also checks the paper's reduction chain (INB is a run of MR, MR is a run of GIN) and the global convergence theorems in an arbitrary finite-dimensional norm.
The obvious argument fails at both ends. Sufficient decrease (2.2) alone gives monotonicity of , but not convergence of the iterates. On the page, admits sequences satisfying (2.2) with both as limit points. Convergence of to needs , and nothing in the algorithm states this. In Theorem 5.2 it has to be derived from the exit level of the while-loop, which depends on a neighbourhood of where the linearization error is uniformly controlled. A solver must combine a limit-point argument (only infinitely many iterates are near , not all of them) with the loop's worst-case backtracking factor . The invertibility of enters only through the bound (5.6) for the backtracking curve, which must be established uniformly in .
[NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]). This is exactly " with an arbitrary norm". Fin n → ℝ (sup norm) and EuclideanSpace would each fix one norm. Only Proposition 2.1 assumes an inner product space, as the page does.fderiv ℝ F, with ContDiff ℝ 1 F (the paper's standing assumption). Invertibility is ContinuousLinearMap.IsInvertible, and is ContinuousLinearMap.inverse.IsGINRun, IsMRRun, IsINBRun, plus IsTLRun, IsENBRun). The steps and levels the algorithm says to "find" or "choose" are data constrained only by the stated conditions. A while-loop is recorded by its number of passes and factors . Every trial before the last fails the loop's test and the last one passes it. Termination is part of the run.MapClusterPt xstar atTop x. "For all sufficiently large " is ∀ᶠ k in atTop. The paper's "whenever is sufficiently near [and is sufficiently large]" is ∃ Γ, ∃ δ > 0, [∃ K,] ∀ k [≥ K], x k ∈ ball xstar δ → …. precedes ("independent of "), and the " large" clause appears only in (3.2), where the page has it.F = id on ) confirms that the INB, GIN and ENB run predicates and the goal's hypotheses are satisfiable, so the goal is not vacuous.