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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. A high-probability approximation guarantee is a separate claim requiring an explicit probability bound. The optimum includes entangled states. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
Conditional value-at-risk (CVaR) is the expected loss in the worst fraction of outcomes. Rockafellar and Uryasev showed that, for a finite set of scenarios, minimizing CVaR is a linear program whenever the loss is linear in the decision (Rockafellar–Uryasev 2000; 2002). That linear program needs the scenario probabilities, and in practice they are estimates. Zhu and Fukushima (2009) replace the single distribution by a set of distributions and minimize the worst-case CVaR over that set. The resulting problem, (16)–(20) below, contains a maximization over distributions inside a constraint, which no standard solver accepts directly.
This mission treats the first of the two cases the paper works out explicitly: the scenario probabilities are only known to lie in a box around a nominal distribution. Proposition 2 of the paper shows that the worst-case problem is then equivalent to a single problem, (24)–(30), with finitely many explicit constraints. The tool is linear programming duality applied to the inner maximization.
A decision is chosen from a set . The random vector takes one of values , and is the loss of decision in outcome . A distribution over the scenarios is a vector . Vectors are compared componentwise, is the all-ones vector, and is the confidence level.
The box uncertainty set (21) is built from a nominal distribution and bounds :
Problem (16)–(20) minimizes over subject to
By Theorem 2 of the paper its optimal value is the minimum of the worst-case CVaR over .
For fixed , the worst case over the box involves the linear program (22) and its dual (23):
Problem (24)–(30) minimizes over subject to ,
and the same constraints , . A point solves a problem when it is feasible and no feasible point has a smaller .
and both maxima are attained.
Proposition 2 makes worst-case CVaR minimization under box uncertainty computable with standard software. When is linear in and is a polyhedron, (24)–(30) is a linear program whose size grows only linearly in , and when is convex in and is convex it is a convex program. The robust portfolio models of §3 of the paper rest on this reformulation. Setting recovers the Rockafellar–Uryasev linear program (Remark 2 of the paper).
Proposition 2 is proved in the paper. As far as is known, neither it nor the duality pair (22)–(23) has a machine-checked proof; this mission would supply one. The development also exercises LP duality for a specific bounded-variable program, one with a single equality constraint, in a form that can be reused by other robust-optimization reformulations over boxes.
The obvious argument says "replace the max by its dual". Two steps need care. First, the inner maximum is over a polytope that may be empty, and the substitution of (18) by (26)–(28) is correct only when the box is nonempty; it must be shown that an optimal solution of either problem forces the box to be nonempty. Second, the equivalence is a statement about optimal solutions, not feasible ones, so both directions need the comparison of objective values over all feasible points of the other problem. The printed proof assumes in each direction that some optimal solution with a smaller objective exists, where only a feasible one is available; the argument must be run with feasible points. Strong duality for (22)–(23) is a genuine LP duality theorem: Mathlib does not provide it in this form, and it must be derived from a general duality or Farkas-type result.
Vectors are Fin S → ℝ and Fin n → ℝ, compared pointwise, with zero-based indices. Dot products are ⬝ᵥ, and is ∑ k, η k. Points of the three problems are structures (Var16, Var24, Dual23) with fields named as in the paper. The factor is (1 - β)⁻¹, and every theorem assumes .
Committed readings:
IsMinOn). Feasibility alone would make the proposition trivial and is ruled out.Needed infrastructure: LP strong duality for the pair (22)–(23), derivable from Mathlib's Farkas lemma or from LP duality theorems already on the platform; finite sums and dot products. Proofs of the milestones, of the goal from the milestones, and of a general bounded-variable LP duality lemma are all welcome.
Not in scope: the ellipsoidal case (31)–(40), Remark 2, and the portfolio instances of §3.
The lost-sales inventory system with a positive lead time is one of the basic models of inventory theory. Demand that cannot be met from stock is lost rather than backlogged, and orders arrive a fixed number of periods after they are placed. Unlike the backlog system, where the inventory position is a sufficient one-dimensional state and a base-stock policy is optimal, the lost-sales system needs the whole pipeline of outstanding orders as its state, and its optimal policy has no simple form. Computing optimal policies by dynamic programming therefore runs into the size of an -dimensional state space.
Paul Zipkin's paper Old and New Methods for Lost-Sales Inventory Systems (Operations Research 56(5), 2008, doi:10.1287/opre.1070.0471) revisits this model, compares classical and new heuristics against optimal policies, and prepares the computation with a state-reduction result. Morton (1969, SIAM Review 11, Equation (83)) showed that under an optimal policy the state remains in a bounded set; Zipkin's §4 extends the argument to every policy in a class that contains the usual heuristics. This mission formalizes that section: the reduced state space , the policy class , and Claim 1, which says that states outside are transient.
Fix the lead time . The state is the -vector : is the stock on hand after this period's delivery, and () is the order that arrives periods later, so is the most recent order. Given the state , an order and a demand , the next state is
Demands in successive periods are independent with a common law on .
The pipeline partial sums are for and ; is the inventory position and the most recent order. A level vector is with . For a level vector ,
and is the set of stationary policies (an order in each state ) with for and for and . The vector base-stock policy with parameter is
equation (5) of the paper with a general in place of Morton's . Under a stationary policy , from an initial state and along a demand path , the state process is , with order and demand . In Lean these are next, v, IsLevelVector, Xs, Zs, vectorBaseStock and traj in the namespace LostSalesOldNew.StateReduction.
For a level vector , a policy , i.i.d. demands with law on and , and any initial state , almost surely
The paper's word is "transient"; the statement above says that every state outside , indeed the whole complement, is visited only finitely often.
A further item records the paper's remark that and are increasing in .
Claim 1 lets the dynamic program be solved on the compact set with policies restricted to , which is what makes the paper's exact computations (lead times up to four, §6) feasible. Since contains the vector base-stock policies and, for large enough, any policy that stops ordering in large states, the claim also says that every plausible policy eventually confines the state to a bounded set.
The result has a short proof in the paper and no machine-checked version. Formalizing it produces a reusable encoding of the lost-sales pipeline with general stationary policies, and makes explicit two points the paper leaves implicit: the probabilistic reading of "transient", and the demand condition under which the process must leave the complement of . Related platform material treats the backlog analogue (VeinottBaseStock.base_stock_level_absorbing, a base-stock level set is absorbing) and lost-sales dynamics under other conventions (CappedBaseStock_Model, from an empty initial state under capped base-stock policies with average cost); those formulations use another state convention and cost criterion and are not imported here.
The invariance step is algebra on partial sums. The content of the claim is the entrance step: outside the policy orders nothing, so the process can only reach through demand draining the stock and the pipeline. That requires the cumulative demand to diverge, which fails pathwise (demand identically zero leaves a state with fixed forever) and holds only almost surely, from independence and . The naive reading of "transient" as invariance alone, or as the pathwise statement with divergent demand assumed, misses this step.
Fin L → ℝ with in the goal; theorems quantify over nonnegative states. The vector is Fin.snoc x z; takes a natural-number index and vanishes at , so .Fin (L+1) → ℝ, antitone with nonnegative last entry. constrains ; constrains for .Measure.infinitePi (fun _ : ℕ => D). The hypothesis is added to the paper's assumptions; without it the claim is false.A complete development needs the partial-sum algebra of the pipeline, the second Borel–Cantelli lemma or the strong law for i.i.d. nonnegative sequences under Measure.infinitePi, and induction along traj. The pipeline encoding is shared with the second mission of this series (lead-time monotonicity). Proofs of any milestone and of the goal are welcome.
The lost-sales inventory system is the inventory model in which demand that cannot be met from stock is lost, not backlogged. It is the natural model for retail and for any setting where a customer who finds the shelf empty buys elsewhere. With a positive order lead time it is also one of the classical hard problems of inventory theory. In the backorder model the state collapses to a single number, the inventory position, and a base-stock policy is optimal. Under lost sales the whole pipeline of outstanding orders matters, the state is an -dimensional vector, and no simple policy is optimal.
Its structure has a long history:
Time is discrete. In each period the order due arrives, a new order is placed, demand occurs, and a holding or penalty cost is charged. The lead time is an integer. The original state records on-hand inventory followed by the orders in transit. Demands are independent with a common law . The costs are linear and stationary: unit procurement cost , unit holding cost , unit lost-sales penalty , and discount factor .
The transformed state is the vector of partial sums , , with the convention . It ranges over the cone
The transformed order is . With the all-ones vector, the state moves to
The one-period cost is on , where is the on-hand stock, and . With periods to go, the optimal cost functions are
A function is submodular on a set if for all , with the componentwise maximum and minimum. A function is L♮-convex if is submodular on . A function on is L♮-convex if is submodular in over , .
For every number of periods to go ,
The statement fixes no constants. It holds for every lead time, every demand law in the class below, and every cost vector.
The result. L♮-convexity of implies that is submodular and convex in the transformed state. L♮-convexity of yields, through Lemma 3 and Corollary 5 of the paper, that the optimal order is nonincreasing in and changes by at most when every component of increases by . These are exactly the Karlin–Scarf and Morton sensitivity results, obtained without derivatives. The same property underlies the paper's later results: the bounds on the optimal policy (§4), the monotonicity of cost in demand variability (§5), and the extensions to capacity limits, correlated demand and stochastic lead times (§6).
Formalizing it. The theorem is proved in the paper; nothing here is open mathematically. To our knowledge no machine-checked proof of L♮-convexity of an inventory value function exists. The mission produces three things:
The obvious argument works with ordinary convexity and submodularity in the original state . It stalls: the lost-sales transition is not linear, and the order enters only the last pipeline component, so the comparative statics Karlin and Scarf and Morton obtained by differentiation do not follow from convexity in . The paper's structure appears only in the partial sums . Submodularity alone, moreover, is not preserved by the step that minimizes over the order. The shift structure of L♮-convexity is what survives the minimization over (Lemma 2). Proving plain submodularity of on therefore does not close the induction.
A second difficulty is the end-of-period program. Writing the next state as the minimum of a program over a constraint set that is a sublattice requires checking the order-theoretic structure of the set together with the sign pattern of every term. The equality between the program's value and the recursion's one-period cost (milestone 3) is a property of the model's own value function, not of an arbitrary L♮-convex continuation.
A third difficulty is measure-theoretic. Preservation under expectation needs integrability and measurability of , and these come from the model rather than from the definitions.
Fin L → ℝ, indexed as in the paper. A helper returns for and at . A function is encoded on Fin (L+1) → ℝ with last. The objective of (4) is encoded on Fin (L+2) → ℝ with coordinates . The order is componentwise.DiscreteConvex.LConvexFunctions.*) works on with values in , a different domain and definition, and is not reused.Conditional value-at-risk (CVaR) is the standard coherent measure of tail risk in portfolio selection and risk-averse optimization: for a confidence level it is, roughly, the expected loss in the worst fraction of outcomes. Its practical appeal comes from the representation of Rockafellar and Uryasev (2000, 2002), which writes CVaR as the minimum over a scalar threshold of a convex function, so that minimizing CVaR over decisions becomes a single convex (often linear) program.
That representation presupposes that the distribution of the uncertain data is known exactly. In practice the scenario probabilities are estimated, and decisions that are optimal for the estimate can perform poorly under a nearby distribution. Zhu and Fukushima (Oper. Res. 57(5), 2009) study the worst-case CVaR: the largest CVaR over a set of distributions that the decision maker considers plausible. For a finite scenario model they show (Theorem 2) that when the plausible set of probability vectors is compact and convex, the worst-case CVaR again has a min–max representation in the threshold . This is what makes worst-case CVaR minimization tractable: under box uncertainty it becomes a linear program and under ellipsoidal uncertainty a second-order cone program (§2.2.1–2.2.2 of the paper).
A decision incurs the loss , where is random. In the discrete model takes the finitely many values , the scenarios, with probabilities , where and . Fix a confidence level and write . The Rockafellar–Uryasev function for the distribution is
and the CVaR of the loss at under is
The distribution is not known; it is only known to lie in an ambiguity set of probability vectors. The worst-case CVaR at is
In the Lean development these objects are WorstCaseCVaR.Discrete.G, cvar and wcvar, with the scenarios given as ys : Fin S → (Fin m → ℝ) and as a set P of vectors Fin S → ℝ.
If is a nonempty compact convex set of probability vectors, then for each
with the inner maximum attained for every and the outer minimum attained at some . The statement fixes no constants and no particular ambiguity set.
Theorem 2 converts a supremum over distributions of a minimum over thresholds into a minimum over thresholds of a worst case of a function that is affine in . Minimizing over decisions is therefore the single minimization problem (16)–(20) of the paper in the variables , whose only nonstandard constraint is . For box and ellipsoidal ambiguity sets that constraint is dualized into linear or conic constraints, which gives the robust portfolio models of §§2.2.1–3 of the paper. The same exchange of and underlies many later distributionally robust CVaR models.
The result is proved in the paper (appendix, p. 1167) and is not open. The mission produces a machine-checked proof of it, which to our knowledge does not exist. Mathlib contains Sion's minimax theorem (Sion.exists_isSaddlePointOn), which covers Lemma 1; what is missing is the CVaR-specific part: the convexity of in , the reduction of the threshold to a compact interval uniform over , and the passage from the compact interval back to all of .
The obvious approach applies a minimax theorem directly to on . That fails because is not compact, and minimax equalities on a noncompact factor can fail; the threshold must first be confined to a bounded interval, and the interval must work for every simultaneously. After the exchange on the interval, the minimum over the interval has to be identified with the infimum over all of , which needs the min-max inequality on the unrestricted line. A second subtlety is attainment: every "min" and "max" in the statement is a claim that an extremum exists, and in the real-valued formalization each must be exhibited rather than read off from a supremum.
Conventions committed to in the Lean statements:
Fin S; probability vectors are elements of stdSimplex ℝ (Fin S).No vacuous version of the goal is admissible: the ambiguity set must be nonempty and consist of probability vectors, and the minimum over must be witnessed.
The development needs only finite sums, convexity on and on the simplex, compactness of and of closed intervals, and Mathlib's minimax theorem. The reduction to a bounded interval and the min-max inequality are reusable for other finite-scenario CVaR results. Proofs of any milestone are welcome, as are alternative proofs of the goal that avoid the interval reduction.
Conditional value-at-risk (CVaR) is the standard coherent measure of tail risk in portfolio selection, insurance and stochastic programming. Its practical appeal comes from a variational formula of Rockafellar and Uryasev (J. Risk 2000; J. Banking Finance 2002): CVaR at level is the minimum over a scalar of a convex function, so that minimizing CVaR over decisions becomes a single convex program, a linear program when the distribution is given by scenarios.
The formula needs the distribution of the random returns, and in practice that distribution is estimated and uncertain. Zhu and Fukushima (Oper. Res. 57(5), 2009) introduce the worst-case CVaR: the supremum of CVaR over a set of candidate distributions. They show it is again a coherent risk measure and that, for several natural choices of , minimizing it remains a tractable convex program. This mission formalizes the first of these results, for the set of all mixtures of finitely many given distributions, a model used in robust statistics and in finance to describe returns under several market regimes.
A decision and a random vector determine a loss . A confidence level satisfies (in applications ). Write .
For a probability distribution of under which is integrable, the Rockafellar–Uryasev function is
and CVaR is its minimum over :
Fix likelihood distributions on and let be the probability simplex. The ambiguity set is the set of mixtures
and the worst-case CVaR of is
Write for the function (1) with , with , and for the function (1) of the mixture .
For every with integrable under every ,
with the minimum attained. The supremum over infinitely many distributions on the left becomes a minimum of the pointwise maximum of functions on the right.
The milestones follow the paper's appendix proof (pp. 1166–1167) in order:
An additional item states Corollary 1: minimizes over exactly when minimizes over and minimizes .
The result. Theorem 1 makes worst-case CVaR under mixture uncertainty no harder to optimize than ordinary CVaR. Since each is jointly convex in when is convex in , is convex, and Corollary 1 turns robust CVaR minimization into one convex program in ; with sampled scenarios it is a linear program (the paper's (10)–(15)). It is the starting point for the paper's robust portfolio models (§3), whose ambiguity sets are mixtures of a few estimated return distributions.
Formalizing it. The theorem is proved in the paper; no machine-checked version exists. A formal proof contributes a measure-theoretic treatment of the Rockafellar–Uryasev function for arbitrary distributions (the paper argues with densities and appeals to Remark 1 for the general case), a reusable statement that the minimizer set of is a compact interval, and a worked instance of the minimax theorem in Mathlib (Sion) applied to a problem with an unbounded variable.
The obvious argument is to exchange and in , since the function is convex in and affine in . Minimax theorems for this exchange need compactness of one of the two sets, and the variable ranges over all of . The step that has to be supplied is a localization: all minimizers in , for every at once, lie in one compact interval determined by the minimizer sets of the components. This in turn requires knowing that each has a nonempty bounded minimizer set, which uses and integrability of the loss: at the minimizer set can be a half-line and the localization fails. A second point is attainment: the outer supremum over is a maximum only because the inner minimum depends continuously on .
Fin m → ℝ (not densities); Remark 1 of the paper extends all results to general distributions, and a density is a special case. Decisions are Fin n → ℝ, the loss is f : (Fin n → ℝ) → (Fin m → ℝ) → ℝ, and the likelihood distributions are P : Fin l → Measure (Fin m → ℝ) with indices zero-based and [NeZero l].stdSimplex, and WCVaR is the supremum of the image of .min and max in the paper is stated as attained, with an explicit minimizer or as IsGreatest/IsLeast; no real sInf or sSup is evaluated on an empty or unbounded set, so no statement can hold through Lean's junk value .A processor can save energy by running slowly when work is light, but a deadline may force it to run faster. Yao, Demers, and Shenker formulated this tradeoff as an offline and online scheduling problem for a variable-speed processor in their 1995 FOCS paper. Their Average Rate Heuristic (AVR) uses only each job's arrival, deadline, and required work to set speed. This mission formalizes their quadratic-power analysis: AVR's worst-case energy is at least four and at most eight times the minimum possible energy. The authors prove these bounds in Theorem 2, rather than an exact value.
The question matters when an online scheduler must choose speed before seeing later jobs. Deadline feasibility alone does not measure energy: processing the same number of cycles at twice the speed for half as long can cost more when power grows superlinearly. The paper's model isolates that dependence in a power function , so the competitive guarantee measures the energy price of AVR's speed choices. The initial motivation, model, and heuristic are in §§1–4 of the paper.
Fix a nondegenerate time window . A finite job instance assigns each job an arrival time , deadline , and nonnegative required work in CPU cycles. Every job window lies inside . A schedule has nonnegative processor speed and selects at most one job at each time. Speed and job selection are constant between finitely many breakpoints. The schedule is feasible if each job receives its full work inside its own window:
For a power function , its energy is . An optimal schedule minimizes this quantity among feasible schedules. These definitions follow §2, p. 375. The intensity of an interval is the total work of jobs whose full windows it contains, divided by . An interval with maximum intensity is critical; Theorem 1 identifies the processor speed on that interval in an optimal schedule §3, p. 375.
Each job's density is , extended as a step function equal to on and zero elsewhere. AVR runs at speed and chooses the earliest-deadline available job. For quadratic power, its energy is
The competitive ratio is the least upper bound of over instances, where is the least feasible energy §4, p. 376, Eq. (2).
The goal is the paper's Theorem 2, p. 381:
The upper bound compares AVR with every feasible schedule. The lower bound says that every constant strictly below four is exceeded by the AVR-to-feasible-energy ratio on some instance. This formulation does not claim that one finite instance attains four.
The milestone path follows the paper: Theorem 1 characterizes optimal speed; Lemma 5.1 reduces to jobs of type A or B; Eq. (5) splits their costs; Lemma 5.2 and Eq. (7) control the A contribution; Lemmas 5.3–5.6 reduce the analysis to canonical instances; Lemma 5.8 supplies a matrix bound; Lemma 5.7 gives and ; Example 2 approaches the lower constant. These statements and their order come from §5, pp. 378–381. The paper also states a higher-power result, Theorem 3, for real :
That result is a companion item. The extended abstract leaves its full proof to a longer paper §6, pp. 381–382.
The upper bound guarantees that AVR's energy is controlled by a fixed multiple of the offline optimum for every finite job set, even though AVR sets speed from individual job densities. The lower family rules out a guarantee below four for this heuristic. Together they delimit the performance of AVR under quadratic power; they do not give its exact worst-case ratio. The A/B reductions and the tree-induced matrix estimate are useful mathematical interfaces for later analyses of interval-structured schedules.
The paper proves Theorem 2 in the mathematical sense. This mission supplies machine-checkable statements and definitions, with proofs left open for solvers. Closing it requires formal proofs of the reduction steps, the matrix estimate, and the limiting example, plus an explicit connection from the optimal-schedule analysis to comparison with every feasible schedule. No completed Lean proof is claimed here.
The simple calculation exposes overlap between job windows but does not say how that overlap compares with an optimal schedule. An optimal schedule may run jobs in a different order and may preempt them. The paper therefore changes the instance while preserving the optimal speed profile: it first separates cumulative execution into two types, then reduces to single execution intervals and specially aligned, nested windows. The matrix inequality controls the resulting expression. A pointwise comparison of AVR speed with optimal speed cannot replace these reductions, because an optimal schedule can concentrate work on critical intervals while AVR spreads each job's density across its entire window §5, pp. 377–381.
Jobs use Fin n, allowing the empty instance. The instance requires , , containment in the window, and . A schedule uses real-valued speed and an optional job label; none denotes no assigned job. Its piecewise-constant requirement is witnessed by finitely many increasing breakpoints. Values at breakpoints are unrestricted by the piecewise-constant clauses, and speed comparisons in the theorems are almost-everywhere statements. Job windows are closed, as printed; endpoints do not affect the integrals. A schedule may have positive speed while no job is assigned, since the source does not equate idleness with zero speed.
Every energy expression is a real interval integral. The schedule conditions ensure the integrands in theorem hypotheses are piecewise constant away from finitely many points. Density denominators are positive. An execution-speed quotient for a zero-work job can have zero denominator, in which case Lean returns zero; such a job contributes no executed work. The goal uses quantified comparisons with feasible schedules rather than a real infimum, and Lemma 5.6 uses all upper bounds on a nonempty canonical family rather than a real supremum. The lower bounds quantify over every smaller constant, avoiding a false attainment claim. These choices guard against default values for empty or unbounded extrema.
Theorem 1's printed convexity hypothesis is strengthened to strict convexity and nondecreasing power on nonnegative speeds: its stated speed uniqueness fails for a linear power function, and a decreasing power function rewards idle speed. This repair is explicit in that item's description. Existence of a quadratic optimum is included as a milestone from the algorithm of §3, although it is not a separately numbered theorem. Example 2 includes the variable exponent , the limiting ratios at and , and an eventual upper bound of four across the family. The A-job order resolves exact ties by index. For canonical and tree-induced nesting, intervals that meet only at an endpoint count as disjoint; this admits the paper's displayed four-interval matrix.
The development needs Mathlib's real interval integrals, finite sums, measures of intervals, matrix eigenvalues, and real-power limits. The finite schedule model, canonical-instance data, and tree-induced matrix interface can be reused beyond this particular ratio bound. Contributions may establish these interfaces' elementary properties, the paper's milestone theorems, or independent proofs of the goal, provided they preserve the stated job and schedule classes.
Functional limit theorems describe the behavior of entire time-indexed paths under scaling. In queueing and other stochastic models, a path of departures, workload, or accumulated input may be related to another path by reversing a finite observation window. To carry a limit theorem through that change of viewpoint, one needs to know how reversal acts on the topology of the path space. Ward Whitt's 1980 paper studies composition, reflection, first passage, and time reversal as maps that transfer functional limit theorems to derived processes (Whitt 1980).
The time-reversal result is a precise metric statement. Ordinary reversal preserves the Skorohod distance exactly. A version shifted to begin at the group identity satisfies a bound with constant two. These facts give continuity and, when the random paths satisfy the hypotheses, make reversal available to the continuous mapping theorem. Whitt's introduction explains how deterministic path continuity connects to stochastic-process limits (Whitt 1980, pp. 67–69).
Let be a complete separable metric group, written additively, with identity and metric . The metric is translation invariant: moving both points by the same group element leaves their distance unchanged. Let contain the càdlàg paths , meaning paths that are right continuous and possess left limits. Section 8 additionally requires , so the terminal value agrees with the value approached from earlier times. Let . These are the spaces Whitt fixes for time reversal (Whitt 1980, p. 83).
The uniform distance is . A time change is an increasing homeomorphism of onto itself; is the identity time change. The distance used in the paper is
Two paths may be close when their values can be matched after a small distortion of time. This is the paper's equation (2.1), rather than an unspecified equivalent metric (Whitt 1980, p. 70).
The reverse-time map reads the left limit at the reflected time:
The left limit is essential: the direct value places jumps on the wrong side and generally does not give a right-continuous reverse path. The terminal convention gives , so . Whitt also uses the reflected time change in the proof (Whitt 1980, pp. 83–84).
The goal is Whitt's Theorem 8.1. For every ,
The second inequality also applies when both paths lie in , since . The constant is the paper's printed constant, not a parameter to optimize in this mission (Whitt 1980, Theorem 8.1, p. 83).
The milestones record four claims from the theorem's proof: reversal preserves its path spaces and has inverse behavior on its natural domains; reflected time changes stay in ; reversal obeys exact and bounded uniform-distance relations; and reversal interacts with time changes through . Their descriptions reproduce the printed proof sentences. The proof calls the time-change cost a “minimum” once, although equation (2.1) and the displayed calculation use a maximum. The formal target follows equation (2.1) (Whitt 1980, pp. 70, 84).
An isometry preserves every distance, so ordinary reversal preserves convergent and Cauchy sequences in this metric. The bound for makes shifted reversal Lipschitz and therefore continuous. A functional limit theorem for input paths can then be translated into one for the corresponding reversed paths whenever the path-space hypotheses hold. The result is already proved in Whitt's paper; the open work here is a machine-checked development of its definitions, supporting claims, and metric theorem.
Formalizing the result also creates reusable interfaces for endpoint-constrained càdlàg paths, left-limit reversal, uniform path distance, and reflected time changes. Those interfaces may support later statements about reversed stochastic models. This mission does not assert weak convergence of probability laws or Borel measurability; those would require a separate measurable-space development for .
The immediate idea does not preserve càdlàg paths at jumps: a right-continuous jump becomes left-continuous. The correction uses left limits, but endpoint behavior then matters. Without , the shifted reverse path need not start at the identity. The assertion also concerns an infimum over all allowed time changes, so a uniform-distance statement alone does not establish the theorem. These are the points at which reflection of the time axis becomes a claim about the precise path-space topology (Whitt 1980, pp. 83–84).
Lean represents paths as total functions ; all path conditions, metrics, and equality claims read only . Càdlàg membership requires right continuity and left limits within the interval, with included in . Completeness and separability are explicit because the paper calls a complete separable metric space. The additive metric group is represented by an additive commutative group with an explicit translation-invariance hypothesis. This chooses the commutative reading exemplified by ; the paper uses additive notation but does not separately state commutativity.
The paper's is encoded by strict increase, continuity, and surjectivity on , which characterize increasing homeomorphisms there. The paper's is equation (2.1) on both sides of the goal. Lean uses extended nonnegative distances for and , avoiding the default value a real supremum can assign to an empty or unbounded set. The claims do not become trivial by dropping membership: it is an explicit hypothesis, and the zero path over satisfies it. A local, sorry-free check confirms that instance. Two easier statements are excluded on purpose: the goal is stated for the distance , not the uniform distance , and reads the left limit , not the value .
The proof's first sentence says the maps are one-to-one and onto. The map forgets an additive offset and is not injective on all of ; the formal milestone expresses involution for on and for the restriction of to . One identity printed for with also holds for every ; the formal milestone uses that broader domain and says so in its item description. Contributions are welcome for the left-limit and time-change infrastructure as well as the four listed statements and the goal.
A binary classifier is learned from a sample of a distribution on , and its quality is measured by its excess classification risk over the Bayes classifier. Without assumptions on no learning method converges at a uniform rate, so every rate theorem rests on a condition that describes how hard is. Two such conditions are standard: Tsybakov's noise condition (Tsybakov 2004), which bounds the mass of the region where the label is close to a fair coin flip, and smoothness of the regression function .
Steinwart and Scovel (arXiv:0708.1838v1, the reprint of Ann. Statist. 35 (2007) 575–607) analyse support vector machines with Gaussian RBF kernels. Their rates rest on a new condition, the geometric noise exponent, which measures how much of the weighted measure lies close to the decision boundary. It is tailored to the approximation properties of the Gaussian kernel and is less familiar than the classical conditions. Theorem 2.6 of the paper connects it to them: an envelope condition on near the decision boundary, together with a Tsybakov exponent, yields an explicit geometric noise exponent. This mission formalizes that theorem.
Let be compact and let be a distribution on with marginal and regression function . The classes of are , and , all intersected with . The distance to the decision boundary is
with the Euclidean distance of to (equation (7), p. 7).
In Lean these are TsybakovNoise, GeometricNoise and Envelope, built on Tau, in the namespace FastRatesSVM.GeomNoise.
If has an envelope of order and Tsybakov noise exponent , then
Both clauses are stated, as one conjunction.
Theorem 2.6 makes the paper's learning rates usable under familiar assumptions. The main rate theorem of the paper (Theorem 2.8) is stated in terms of the geometric noise exponent; through Theorem 2.6 it becomes a rate in terms of a Tsybakov exponent and the order of an envelope, which is a Hölder-type behaviour of at the decision boundary. Example: with , , uniform and , the distribution has envelope order and Tsybakov exponent , hence geometric noise exponent .
The result is proved in the paper. As far as known, none of it is machine-checked: none of these noise conditions has a Lean formalization, on Prove2Me or in Mathlib. The mission produces the definitions themselves (the class decomposition, and the three noise conditions), which any later formalization of margin-based classification rates can import, and a formal proof of the implication. A companion mission of the same series formalizes the paper's rate theorem, which takes the geometric noise exponent as its hypothesis.
The case is elementary once the right splitting level is chosen: the expectation is split at a level of , and is then tuned to . Tuning it requires the asymptotics of the solution of a transcendental equation. This yields every exponent below the critical value , but not the critical value itself: a logarithmic factor is lost.
Reaching the critical exponent when is the substantial step. The paper does it with Hölder's inequality for Lorentz spaces and and an estimate of a nonincreasing rearrangement (display (32)). Mathlib has neither Lorentz spaces nor nonincreasing rearrangements, so this part either builds that infrastructure or replaces it with a direct layer-cake argument against the distribution function of . The obvious approach, the same splitting as for , does not work: it always loses the logarithm.
EuclideanSpace ℝ (Fin d) with , and a measurable version of the regression function with values in everywhere. Every Borel distribution on has this form, and the paper defines "for some choice of ".Metric.infDist gives . For Theorem 2.6 both readings give a true statement. Under the reading , the companion statements Theorem 2.7 and Lemma 4.1 are false for a version of with an empty class. The convention is chosen for agreement with the companion mission.lintegral), so a bound can never hold through a junk value of a non-integrable function.The source is arXiv:0708.1838v1, the reprint of the Annals article. Its printed page numbers equal the PDF page numbers, and every page cited here is that number.
The newsvendor problem is the basic single-period inventory model: a decision maker orders units at unit cost before a random demand is observed, sells units at price , and loses unsold units. Its optimal order is the critical fractile of the demand distribution . Laboratory experiments show that human subjects do not order . Schweitzer and Cachon (Management Science 46(3), 2000) gave subjects uniform demand on and found that the average order lay below for a high-margin product and above for a low-margin product: orders are pulled toward the center of the demand range.
Su (Manufacturing & Service Operations Management 10(4), 2008) explains this pattern with a model of bounded rationality: the decision maker does not pick the best order with certainty, but picks better orders more often, through a logit choice rule. This mission formalizes the first results of that paper, the case of uniform demand, where the logit order has an explicit law and the pull toward the center can be proved exactly. The source is the published MSOM 2008 article; all page numbers are its printed pages.
A decision maker with utility over an interval and bounded-rationality parameter makes a random choice with the logit density
and off (eq. (2), p. 571). Large means noisy choices; small concentrates the choice near the maximizer of .
In the newsvendor problem the price and unit cost satisfy . Demand has density and distribution function . The expected profit of ordering units is
and the optimal solution is its maximizer. The behavioral solution is the logit choice with utility over the decision domain , the smallest interval containing the support of (eq. (4), p. 572).
This mission takes uniform demand with : on and . The midpoint of the demand range is . Two parameters recur:
A truncated normal law on with parameters has density proportional to on and zero elsewhere (eq. (37), p. 586). Write and for the standard normal density and distribution function.
The goal is stated for every and every , with any maximizer of over ; it fixes only the sign of the bias, not its size.
Proposition 3 gives a single mechanism, noise in the choice of the order, that produces both directions of the bias observed by Schweitzer and Cachon: under uniform demand, a high-profit product () is underordered on average and a low-profit product () is overordered. Proposition 1 gives the full law of the boundedly rational order, which is what makes the model testable: the paper fits the truncated normal law to experimental order data and estimates (§5). Corollary 1 is the closed-form mean used in that fit and in Proposition 3.
These results are proved in the paper by direct computation; none of them has a machine-checked proof. The mission adds a checked development of the continuous logit choice model on an interval, of the truncated normal law and its mean, and of the uniform-demand newsvendor profit, together with exact statements of what the paper's informal phrases mean (see Formalization scope).
Each step is elementary on paper, but the formal content sits in the integrals. Expected sales must be computed as a piecewise integral to obtain eq. (5), and the maximizer must be identified over all of , not only on , which needs the profit outside the support as well. Proposition 1 is an identity between two normalized densities, so both normalizing integrals must be shown positive and finite. Corollary 1 requires the mean of a truncated Gaussian in terms of Mathlib's Gaussian density and distribution function, which is not in Mathlib. For Proposition 3, the natural shortcut "the mean of a truncated normal is " is false whenever , and it is exactly the asymmetry of the truncation that produces the bias.
All quantities are real numbers, with the paper's standing assumptions as hypotheses: , (the page states ; is read so that lies inside ), and (eq. (2) divides by ; , perfect rationality, is a limit, not a value of the formula). The decision domain is the closed interval ; the logit density is zero off it, and expectations are integrals over . The parameter is the positive square root of , and , are Mathlib's gaussianPDFReal 0 1 and the distribution function of gaussianReal 0 1.
Corrections and readings relative to the printed text:
The optimal solution in the goal is a hypothesis that maximizes over , never a variable set to a closed form by fiat; milestone 2 shows the hypothesis is satisfiable and identifies . No statement holds vacuously through a junk value: on with the logit normalizer is the integral of a continuous positive function over an interval of positive length, and the denominator of (8) is positive because .
Reusable beyond this mission: the logit density on an interval, the truncated normal density, and its mean formula. Proofs of any milestone, and of the mean of a truncated normal law in general, are welcome.
A service system with several servers can use a larger fraction of its capacity than a single-server system while still giving customers an acceptable wait. The design question is how much unused capacity is needed as the number of servers grows. Ward Whitt's study begins with a factory manager deciding whether to put four machines in one work area. It uses queueing models to connect the number of machines, their utilization, and the delays customers experience. The proposed utilization rule, , keeps the unused fraction proportional to as the number of servers changes (Whitt 1992, pp. 708–710).
The paper distinguishes the chance that a customer waits at all from the length of the wait once a delay occurs. That distinction matters when a staffing choice must control a long wait rather than merely the fraction of customers who wait. The exact result in §3.1 gives a benchmark for the paper's later approximations to more general arrival and service processes (Whitt 1992, pp. 719–720).
An queue has Poisson arrivals at rate , identical servers, independent exponential service times, unlimited waiting room, and first-come first-served service. Time is measured so that each server's service rate is one. The server utilization is . We consider and , so the queue has a stationary distribution. Let be the stationary probability that customers are in the system. Its state process is a birth–death process: arrivals occur at rate and departures from state occur at rate .
Let be an arriving customer's steady-state time in the queue before service begins. An arrival finding fewer than customers starts service at once. An arrival finding customers waits for service completions while all servers are occupied. In the formal model, the law of has an atom at zero of mass and, for each , a gamma component with shape , rate , and weight . The arrival-state weights use the Poisson-arrivals-see-time-averages property. This construction represents the FCFS waiting time independently of any claim about its eventual conditional distribution.
For an event of positive probability, denotes the conditional waiting-time law. The paper calls a customer delayed exactly when . The scale parameter is defined by the utilization equation ; because , this equation makes positive.
The supporting target is the §3.1 statement that a delayed customer's waiting time is exponential with rate , equivalently with mean :
The goal is Proposition 3.1 under the utilization equation. It records both the entire conditional tail and its mean, for every :
The goal also asserts , so these conditional quantities are defined. The scan of Proposition 3.1 prints the exponent without and the mean denominator with ; the statement here uses the values determined by the preceding exponential-law sentence and by the paragraph following the proposition (Whitt 1992, pp. 719–720).
The result gives an exact delay distribution for the Markovian multi-server system. With servers and the utilization equation held fixed, the conditional tail at any positive threshold and the mean wait of a delayed customer both depend on through . Thus the same rule that organizes the probability-of-delay discussion has a definite implication for customers who actually wait. It is also the exact comparison point for the paper's later, explicitly approximate analysis of general queues (Whitt 1992, §3.2).
Formalizing this result supplies a reusable representation of the stationary FCFS waiting-time law as a mixture of Erlang distributions, together with a precise connection between birth–death state probabilities and delay. The related platform items QueueingFundamentals.BirthDeath.mmc_steady_state and QueueingFundamentals.BirthDeath.erlang_c_formula state the stationary state probabilities and the probability of delay, respectively; both are open and neither states this waiting-time law. The open QueueingFundamentals.BirthDeath.halfin_whitt concerns the heavy-traffic limit for the case, a different target. The current result is known mathematically from Whitt's 1992 paper; this mission asks for its machine-checked proof in the specified model.
The conditional distribution is not immediate from an individual service time. A delayed arrival can encounter any queue length , so its waiting time is a gamma law whose shape varies with . The stationary probabilities provide the weights of infinitely many such components. Showing that this whole mixture has one exponential law requires a relation among the stationary tail probabilities and control of the infinite sum. The same mixture must have a well-defined first moment for the conditional mean formula.
Lean uses a natural number , a real arrival rate , and a real sequence satisfying the published QueueingFundamentals.BirthDeath.IsSteadyState predicate with constant birth rate and death rate . That predicate includes nonnegativity, total mass one, and the global balance equations. Its published definition is imported as a reference. Service rate is exactly one, as fixed in §2.1 of the paper. The conditional waiting-time law is a measure on real time, with a point mass at zero and a countable gamma mixture. The positive-time restriction of this measure expresses conditioning in the milestone; real measure values and an integral express the tail and mean in the goal.
The formal hypotheses spell out positive arrival rate, at least one server, and subcritical utilization. These make the stationary law and the positive exponential rate meaningful. The goal states positive delay probability before dividing by it. The waiting-time law is built from stationary queue lengths and service completions, rather than being defined as exponential; proving that it becomes exponential is the mathematical task. Solvers may develop reusable measure-mixture identities, stationary-tail facts, and gamma or exponential distribution results. The approximation formulas of §3.2 and the paper's numerical tables are outside this mission.
J. G. Wardrop's 1952 paper Some theoretical aspects of road traffic research (DOI 10.1680/ipeds.1952.11259) introduced the two criteria that still organise traffic assignment. When a flow of traffic can choose between several routes from one origin to one destination, the paper (p. 345) considers two ways the traffic might divide:
The first is now called Wardrop's first principle, or user equilibrium: no driver can shorten their trip by switching route. The second, Wardrop's second principle, is the system optimum: it "minimizes the vehicle-hours spent on the journey". The gap between the two is the quantity later studied as the price of anarchy of selfish routing (Roughgarden and Tardos, J. ACM 2002), and the marginal-cost characterisation of the system optimum underlies congestion pricing (Beckmann, McGuire and Winsten, Studies in the Economics of Transportation, 1956).
This mission formalizes the paper's solution of criterion (2) on parallel routes, section (2) Minimum Average Time, pp. 345–347. Mission II of the same series treats criterion (1) on the same model.
A total additional flow is divided among alternative routes . Route carries an additional flow and has journey time, equation (22),
where is the journey time on route with no additional flow and is the additional flow at which its speed would fall to zero (routeTime b p i x). A feasible split of is a vector with for every and (IsFeasible p Q q).
The number of additional vehicles on route at an instant is , and (totalExtra b p q). The average journey time is, equations (25)–(26),
(avgTime b p Q q). Criterion (2) asks for a feasible split with for every feasible split (IsMinAvgTime b p Q q).
The marginal journey time of route is , the rate at which grows when flow is added to that route. For a threshold , (usedSet b ε) is the set of routes whose marginal time at zero flow lies below ; with the routes labelled so that it is the paper's "first routes".
For and , every split minimizing admits a threshold with , where , such that
A companion theorem states that a minimizing split exists whenever .
The closed forms give the system-optimal assignment on parallel routes with the travel-time law (22) explicitly: which routes carry traffic, how much, and the resulting average time. Together with the equal-times solution (23)–(24) of mission II they quantify, for this model, how much average time selfish route choice costs; the paper's Fig. 8 compares the two numerically and finds the difference small in its example. The marginal-time conditions (27)–(28) are the parallel-route instance of the general statement that a system optimum is an equilibrium with respect to marginal costs.
The derivation on pp. 346–347 is a first-order argument that the paper does not make rigorous: it assumes a minimizer exists, that it satisfies the stationarity condition, and leaves (32)–(33) to "a few lines of algebra". This mission produces the rigorous version, including existence. No machine-checked statement of (27)–(33) is on the platform; the related platform items on Wardrop equilibria concern the Beckmann potential and atomic congestion games, not the system optimum of this model.
The stationarity condition (27) comes from moving an infinitesimal flow between two routes in use. Turning this into a theorem needs the one-sided version at unused routes, since is a boundary point and the condition there is an inequality, and needs the constraint to be preserved by the perturbation. The step "only the first routes will be in use" is the converse direction: a route with that carries no flow must be shown to contradict minimality, not just to violate the equal-marginals equation.
Existence is not a compactness argument on a closed set: the feasible set is open in the direction , where , and that coercivity has to be used. The algebra from (31) to (32)–(33) is routine once the set and the value of are fixed.
Routes are indexed by Fin D; all quantities are real. The standing hypotheses are , , and ; without the last the feasible set is empty and every statement about a minimizer is vacuous, and with the average time is undefined. Feasibility requires , of the minimizer and of every competitor: at Lean evaluates as , which would let a "minimizer" place flow at capacity for free. The paper's labelling is not assumed; "the first routes" is . Marginal times are written in the closed form (29), and milestone 1 identifies that form with the derivative via HasDerivAt. Minimality is stated for , the paper's criterion, not for .
Corrected slip. The paper prints the denominator of (33) as . The formalization uses : from (31), , and . The printed form is not dimensionally consistent and gives wrong flows, e.g. for , , . Equation (32) is correct as printed.
The goal cannot be satisfied trivially: the threshold is existential and the flows and are pinned to explicit formulas, and the companion existence theorem shows the hypothesis IsMinAvgTime is met for every admissible . The route time and feasible split come from the shared WardropTraffic.EqualTimes.Setting definition; this mission adds the total and average time and criterion (2). Proofs of any item, including the existence theorem and a uniqueness statement (the objective is strictly convex), are welcome.
Call centers, hospital wards, telephone exchanges and server farms all face the same staffing question: given an arrival rate , how many servers are needed to keep congestion at a fixed level? A widely used answer is the square-root staffing rule
where the grade of service sets the congestion level. It says that the safety capacity above the offered load grows like the square root of the load, which is the quantitative form of the economy of scale of large service systems.
Whitt (Management Science 38(5), 1992, pp. 708–723) explains the rule through an associated infinite-server (IS) model, in which every customer starts service immediately on arrival. If the number of busy servers in the IS model is Poisson with mean , its mean and variance are both , so the event "more than servers busy" has roughly constant probability when is a fixed multiple of . The Poisson law of is therefore the probabilistic fact on which the heuristic rests. This mission formalizes that fact as proved in §2.4–§2.5 of the paper: first for deterministic unit service times (M/D/∞), then for service times taking finitely many values with mean (M/G/∞ with finite support).
Timeline:
Time is measured in units of the mean service time. Let be i.i.d. exponential random variables with rate , the interarrival times, and let be the -th arrival epoch. The arrival counting process is the number of with , the number of arrivals in . This is a Poisson process of rate .
Customers are numbered ; customer arrives at , is served at once, and has service time . Following the paper (proof of Proposition 2.3, p. 712), an arrival at time is counted and a departure at time is not, so customer is present at iff . The number of busy servers is
For the M/G/∞ case fix classes with probabilities and values . Each customer carries a class label , the labels are i.i.d. with and independent of the interarrival times, and . The class- busy count is .
If and , then
The law depends on the service-time distribution only through its mean.
A companion item, Proposition 2.1 (p. 710), states that (2) implies and , connecting (2) to the utilization equation .
The goal is the step that turns the IS heuristic from a special case into a statement about general service: since is Poisson with mean whatever the finite service-time law of mean , the square-root rule derived from M/D/∞ applies unchanged to M/G/∞, and the paper uses this to argue that -server congestion is nearly insensitive to the service distribution beyond its mean when is large.
The results are classical and proved; none has a machine-checked proof on Prove2Me. Formalizing them adds:
ServiceParts.Palm.units_in_resupply_poisson_finite_time and ServiceParts.Palm.palm_theorem, which treat service times with a density.The open item QueueingFundamentals.Foundations.poisson_count_cdf (the marginal law ) is related but distinct from milestone 2, which concerns the increment over .
The paper's arguments are short, but each hides a probabilistic fact that is not elementary from the definitions. The increment law of milestone 2 requires the memoryless property at the deterministic time : the residual time to the next arrival after must be shown exponential and independent of the past, which is a statement about a random index (the number of arrivals by ), not about a fixed interarrival time. Splitting (milestone 4) requires a joint computation over all classes at once: the class counts are built from the same arrival epochs, so their independence is a genuine property of Poisson processes, false for general renewal arrivals, and cannot be obtained one class at a time. The overlapping windows of different classes make this unavoidable.
QueueingFundamentals.Foundations.ArrivalProcess: IsExpInterarrivals μ lam T (measurable, mutually independent, exponential with rate lam), arrivalTime, countingProcess. The Poisson process is not postulated through an increment-law axiom; a definition with such a field would make milestones 2 and 3 a projection and is ruled out.IsMarkedPoisson adds measurable, i.i.d. class labels J : ℕ → Ω → Fin m with P(J k = i) = p i, independent of the interarrival sequence. Service time of customer k is d (J k). Labels, not values, distinguish classes, so equal d i are not merged.Set.ncard, which is on an infinite set. Milestone 1 carries the hypothesis that only finitely many arrivals occur by , and the decomposition is stated almost surely. Poisson laws are stated pointwise, , avoiding pushforwards of possibly non-measurable maps.Fin m. The constraint forces , and the label law forces and . Added hypotheses: (service times are nonnegative) and, in Proposition 2.1, (the paper's grade of service).IndepFun.hasLaw_add_poissonMeasure. These are reusable well beyond this mission.A network designer may need a cheap connection that keeps the number of links at each site within a local capacity. The minimum bounded-degree spanning tree problem asks for the cheapest spanning tree of a weighted, undirected graph whose vertex degrees respect prescribed upper bounds. The capacity constraints matter in settings where a low-cost tree alone can overload a few hubs. They also make the optimization problem difficult: even with unit edge weights and a bound of two at every vertex, feasibility includes the Hamiltonian path problem. Singh and Lau study the useful relaxation in which the returned tree may exceed each degree bound by one while its cost stays no greater than the best tree satisfying every original bound Singh–Lau 2007.
The weighted result settled the bounded-degree form of a conjecture discussed in their paper. Goemans had obtained a cost-preserving degree guarantee of ; an earlier unweighted local-search result attained a degree allowance but did not cover arbitrary real costs. Singh and Lau's Theorem 1.2 gives the allowance in the weighted setting, without assuming nonnegative costs or triangle inequalities Singh–Lau 2007, pp. 661–662. The platform's open WilliamsonShmoys.minimum_degree_tree_local_search_approximation concerns the related unweighted minimum-degree local-search problem, with a different objective and guarantee.
Let be a finite vertex set and a finite set of unordered, non-loop edges. A spanning tree connects every vertex without a cycle. Every edge has a real cost , so . Each vertex has an integer upper bound on its tree degree . A feasible original solution has for all .
The paper studies a broader connecting-tree problem. A forest is already selected; its connected components, including isolated vertices, are supernodes. The remaining graph has edges disjoint from . A set is an -tree if is a spanning tree. Degree bounds are active only at vertices in , and counts edges of , not edges of . The initial spanning-tree problem is the case and Singh–Lau 2007, p. 665.
For an edge set and vertex set , write for edges of with both endpoints in , and for edges of incident to . The LP-MBDCT relaxation has a nonnegative variable for each . It requires , requires for every nonempty union of supernodes, and requires for . Its objective is . At , , this is the spanning-tree LP in equations (1)–(5) Singh–Lau 2007, pp. 662, 665.
For every feasible initial LP, the paper's Figure 4 algorithm has a terminating run. Every possible run returns a spanning tree satisfying
In particular, is at most the cost of every spanning tree satisfying the original bounds, and thus at most the original optimum. Every run has at most iterations. The cost comparison against every LP-feasible vector states the stronger bound used by Theorem 4.2 Singh–Lau 2007, pp. 661, 666.
The connecting-tree theorem makes the same cost and degree guarantee for an arbitrary feasible state , with only for . The attack path follows the paper's numbered results: Lemma 4.3 describes tight constraints by a laminar family, Claim 4.5 classifies vertices with one excess token, Lemma 4.6 bounds tokens inside a laminar subtree, and Lemma 4.1 says each nonterminal basic solution has either a unit-valued edge or a removable degree constraint. Theorem 4.2 then supplies the general guarantee Singh–Lau 2007, pp. 666–667.
The result allows one unit of violation at each local degree bound while preserving the cost benchmark exactly. It applies even when negative edge costs make standard multiplicative cost ratios awkward. The connecting-tree statement is useful beyond the initial instance because it covers a forest already accumulated and a subset of degree constraints still active.
This mission formalizes the known 2007 result as an open Lean proof target; the paper proves the mathematics, while the declarations here currently have no machine-checked proofs. A completed development would provide a reusable account of a spanning-tree LP with forest contraction, basic solutions defined by tight rows, and a finite relational algorithm with all choices exposed. These objects could support the paper's lower-and-upper-bound extension and other iterative-rounding results.
Rounding an arbitrary fractional edge upward can increase cost beyond the LP benchmark. Restricting the algorithm to edges with value exactly one protects that benchmark, but a nonterminal basic solution need not present a unit-valued edge. The central structural question is then whether some active degree constraint can be removed with only a one-unit effect on the final degree. The tight subtour rows and degree rows overlap, so counting edges from the support alone is insufficient; Lemmas 4.3–4.6 resolve the dependency and token-counting issues that make the direct argument fail Singh–Lau 2007, pp. 666–667.
Lean represents edges as Sym2 V in finite sets, excluding diagonal edges. It represents LP vectors on all unordered pairs but requires zero values outside the current edge set. A forest is acyclic on the full vertex set. A compatible subtour set is a union of its connected components. Subtour right-hand sides are real numbers, so subtraction does not truncate at zero; the empty set is excluded because the literal row would make the LP infeasible. Degree bounds are integers so the algorithm's decrements are total. A basic feasible solution is determined uniquely by its tight equality rows among vectors supported on the current edge set. Linear independence in Lemma 4.3 is checked on the positive support.
Figure 4 is a relation because the LP optimum, a unit-valued edge, and a qualifying vertex may each be chosen in several ways. Its edge and vertex tests are mandatory when their conditions hold. The vertex test uses the support before deleting the selected edge and bounds after decrementing its endpoints, following the printed order. “The algorithm returns” is represented by existence of a run, an iteration bound on every step chain, and guarantees for every returned set. “Cost at most the LP optimum” means cost no greater than the objective at every feasible LP vector. “Polynomial time” is represented by the iteration count; the ellipsoid LP solver and separation-oracle complexity are outside this mission. Lemma 4.6's token distribution is expressed as its explicit counting inequality.
The goal asserts the Figure 4 output and its LP cost guarantee. Bare existence of a tree with cost at most the optimum and degrees at most would be witnessed by an original optimal tree and would lose the algorithmic theorem. A return guarantee without run existence would hold vacuously for a stuck relation. Contributions that prove the stated structural lemmas, establish the LP oracle's basic-optimum availability, or close the algorithm invariant are within scope. No existing platform item treats this bounded-degree LP and iterative-rounding algorithm under these conventions; the plain minimum-spanning-tree LP definition uses a different edge representation and no forest or degree constraints.
A many-server queue has identical servers, a stream of arriving customers, and a buffer in which customers wait when every server is busy. It models call centres, hospital wards and server farms, and the regime of practical interest is the Halfin–Whitt or quality-and-efficiency-driven regime, in which the number of servers grows with the arrival rate so that : servers are almost fully used, yet only a vanishing fraction of customers waits.
This mission formalizes that identity and the proposition that yields it.
Fix one realisation of the queue (Reed, §2, p. 6).
The number in system is (2.2):
Centring each indicator at its (conditional) mean produces the terms
and , the analogous centred sum (2.5) over the customers who entered service after time . is the conditional mean number in a queue fed by the same arrivals.
A sample path is non-idling if for every
that is, the customers waiting at time are exactly those who have arrived and not yet entered service. This holds for every first-come-first-served -server path that never idles a server while a customer waits; the paper uses it at the start of the proof of Proposition 2.1 (p. 8).
For a non-idling sample path and every ,
The result. Equation (2.8) is the paper's starting point for both of its limit theorems. Writing with shows that the number in system is the image of the infinite-server quantities under the regulator map of the paper's §3, the unique solution of . The fluid limit (Theorem 4.1, p. 12) and the diffusion limit (Theorem 5.1, p. 23) then follow from limit theorems for the infinite-server terms and the continuity of that map. Without (2.8), the -server queue has no closed equation in terms of quantities whose limits are known.
Formalizing it. The identity is proved in the paper on pp. 7–9; to our knowledge it has not been machine-checked. This mission produces a sample-path model of the queue (initial customers, arrivals, FCFS service order, waiting times) together with the decomposition of its number in system, reusable for other many-server results stated pathwise. The limit theorems 4.1 and 5.1 themselves are weak-convergence statements in the Skorohod space and are not part of this mission; the regulator map (Proposition 3.1) is the subject of a separate mission of this series.
The decomposition (2.7) is bookkeeping. The content is Proposition 2.1, which converts a sum over customers of tail differences into an integral, against , of the number of waiting customers at earlier times. The step that needs care is the change of viewpoint from "customer 's service time falls in a window of length " to "customer is waiting at time ", after which the sum over customers must be recognised, at each time , as the waiting count of the non-idling identity, with the arrivals counted up to rather than . A second point is the treatment of an atom of at : the half-open windows and the closed integration range must match, and for is used whenever a customer is still waiting.
Related platform items: WhittEfficiency.IS.* (the queue with Poisson arrivals, the infinite-server object behind ) and PalmQueueing.Palm.swiss_army_formula (a pathwise queueing identity of Palm calculus) are the nearest queueing results; neither is the object of this mission.
Temporal-difference learning, TD(), is the basic algorithm of reinforcement learning for estimating the expected discounted cost of a Markov chain from observed transitions (Sutton, 1988). On large or infinite state spaces it is run with a linear function approximator: the cost-to-go is represented as a weighted sum of fixed basis functions, and the algorithm updates the weights. With a lookup table (one basis function per state) its convergence follows from general results on contraction mappings. With function approximation that argument breaks down. Before 1996 there were only results on convergence in the mean (Dayan, 1992), sketches restricted to linearly independent feature vectors , and counterexamples in which related algorithms diverge.
Tsitsiklis and Van Roy (MIT report LIDS-P-2322, 1996; IEEE Trans. Automatic Control 42(5), 1997) proved that on-line TD() with linear function approximation converges with probability 1 on finite or countably infinite ergodic chains. They identified the limit as the fixed point of a projected Bellman-type operator and bounded its error. This analysis is the reference point for later results: finite-time bounds for linear TD, the off-policy divergence examples, and the gradient-TD family.
Timeline:
A Markov chain lives on a finite or countably infinite state space , with transition matrix . A transition from to costs , and is a discount factor. The cost-to-go is
Basis functions give the feature vector and the approximation , written as a vector over .
Starting from an arbitrary , TD() with and step sizes forms the eligibility vector and the temporal difference , and updates .
Let be the invariant distribution, , , and . Write for the -orthogonal projection onto . The operator averages -stage truncated costs:
for , and . The paper makes four assumptions:
Under Assumptions 1–4: ; for every , TD() converges with probability 1, from every initial state and every , to a vector ; is the unique solution of
and
Theorem 1 says that TD(), run on-line along a single trajectory, converges for every , and that its limit has a precise meaning: the fixed point of the projected operator. The error bound shows that as the limit approaches the best approximation , and that for smaller the error can grow by at most a factor . The analysis also explains the failures of related schemes: the projection and the contraction must use the same norm, , which holds only when states are sampled along the chain.
The result is proved on paper. To our knowledge no part of it has been machine-checked; it is not in Mathlib or on this platform. This mission produces:
The obvious approach treats TD() as a noisy version of the deterministic iteration . It fails at the noise. The increments are driven by the Markov process , not by independent samples. They are not martingale differences, and on an infinite state space they are unbounded. The standard ODE method with martingale-difference noise therefore does not apply, and the bias from Markov dependence must be controlled through the mixing and growth conditions of Assumption 3. The algorithm also starts with rather than in steady state, so the steady-state identities of Lemmas 6–8 must be transferred to the actual trajectory. The contraction argument needs care for a different reason: is a nonexpansion of only because is the invariant distribution of the same chain that defines .
is a countable type with the discrete -algebra, a Markov kernel (, the kernel power), and the path law of the chain is Mathlib's Ionescu–Tulcea measure Kernel.trajMeasure. Standing conventions:
Lean's integral of a non-integrable function and sum of a non-summable series are . A trivializing formalization is excluded by stating every expectation and series with its integrability or summability: "well defined and finite" is always a conjunct or a hypothesis, never left to junk values.
The development needs the following:
Contributions are welcome at every level: proofs of the deterministic lemmas, a construction of the stationary chain from and (showing that the steady-state hypotheses are satisfiable), and a proof of Theorem 2 or a stronger stochastic approximation result that implies it.
A committee that chooses one alternative by voting would like a procedure under which nobody gains by misreporting their preferences. Gibbard (Econometrica 41, 1973) and Satterthwaite (J. Econ. Theory 10, 1975) showed that, once at least three outcomes are possible, the only voting procedures with this property are dictatorial. The theorem is the starting point of the theory of strategy-proof mechanisms and of implementation theory.
Most proofs, including the main argument of Satterthwaite's paper, assume strict ballots: no voter is indifferent between two distinct alternatives. Real ballots, and most economic models of preferences, allow indifference. The last section of Satterthwaite's paper carries the theorem over to ballots that are arbitrary weak orders, by decomposing a voting procedure into a tie-breaking function followed by a strict voting procedure. This mission formalizes that extension.
Timeline. Gibbard (1973) proved the impossibility for game forms; the 1974 discussion paper formalized here proved it for strict ballots by induction on the number of voters (Theorem 1), allowing the range of the procedure to be a proper subset of the alternatives, and extended it to weak orders (Theorem 1′). Later short proofs (Barberà 1983; Benoît 2000; Reny 2001) also treat strict ballots.
A committee is a finite set of individuals and a finite set of alternatives. A weak order on is a complete and transitive relation, with read " is preferred or indifferent to "; its strict part is iff and not . The weak orders form . A strong order is a weak order with no indifference between distinct alternatives; the strong orders form . A ballot set is .
A voting procedure is a map . Its range is , with . A strict voting procedure is a map .
is strategy-proof if there are no ballot set , individual and ballot with
For a strict procedure, ballot sets and substituted ballots are strong orders.
is dictatorial if some individual exists such that, for every ballot set , the outcome is among the -maximal elements of : for all .
A tie-breaking function is a map that keeps every strict preference: if then implies . It is regular if there are fixed strong orders such that every indifference , is broken as breaks it.
For and , every strategy-proof voting procedure on weak-order ballots is dictatorial:
The converse fails once indifference is admissible: a dictator's ties may be broken by a manipulable rule, such as a Borda count of the other ballots (pp. 10–11). The goal is therefore a one-way implication.
The result shows that allowing voters to express indifference does not escape the Gibbard–Satterthwaite impossibility: the dictatorial conclusion survives, and only the equivalence is lost. It is the form of the theorem most directly applicable to economic environments, where preference domains usually contain indifference, and the decomposition of Lemma 9 is the device by which strict-ballot results are transferred to weak-order ballots throughout §6 of the paper, including the weak-order version of Arrow's theorem.
The theorem is proved and classical. What is not yet available is a machine-checked proof of the weak-order version with a range that may be a proper subset of the alternatives. The strict, full-range case is proved on the platform (AGT.gibbard_satterthwaite, on strict total orders with a surjective rule); the strict case with an arbitrary range of size at least three is the goal of the companion mission on strict committees. This mission adds the decomposition of Lemma 9 and the extension to indifference.
The obvious route is to restrict a strategy-proof to strict ballot sets, apply the strict theorem, and conclude. Two steps fail. First, the restriction's range may a priori be smaller than , so the hypothesis need not transfer. Second, knowing that is dictatorial on strict ballot sets says nothing directly about ballot sets with indifference: one needs, for each , a strict refinement of with , and the refinement of one individual's ballot may depend on the others' ballots. Lemma 9's second sentence is exactly the existence of such refinements, and the tie-breaking function it produces is generally not regular.
Lean commits to the following conventions, all in the definitions file StrategyProofArrow.WeakGS.Basic:
ι and A; and are their cardinalities. The theorems state or as printed, and where the paper's standing committee assumption is all that applies (Lemma 9). is automatic.Set.range v.A trivializing formalization would measure manipulation by the weak relation instead of its strict part, which makes "strategy-proof" nearly unsatisfiable and the goal vacuous; the definitions use the strict part, and a sorry-free check confirms that a strategy-proof procedure with range of size 3 exists.
A complete development needs the strict Gibbard–Satterthwaite theorem with partial range (milestone 1) and the refinement construction of Lemma 9. The weak-order and tie-breaking vocabulary is reusable for the weak-order Arrow theorem of the companion mission. Proofs of any milestone, and alternative proofs of the goal that bypass Lemma 9, are welcome.
In a wireless multihop network, a switch, or a parallel computer, transmissions interfere: two links that share a receiver, or two crossbar paths that share a port, cannot be active in the same time slot. The scheduler must choose, slot by slot, a set of links that may operate together and decide which traffic each one carries. The basic question is which arrival rates a network can sustain at all, and whether a single scheduling rule sustains every one of them without knowing the rates.
Tassiulas and Ephremides answered both questions in 1992 for a general slotted model with interference constraints, multihop routing and several traffic classes (IEEE Trans. Automat. Control 37(12):1936–1948). Their policy, here called , weighs each link by the largest queue-length difference it can reduce and activates a maximum-weight feasible set. It is the origin of the max-weight and back-pressure scheduling rules that later became standard in switch scheduling (McKeown, Mekkittikul, Anantharam and Walrand, 1999) and in stochastic network optimization (Georgiadis, Neely and Tassiulas, 2006).
A constrained queueing network has nodes, servers (links) and customer classes. Server moves customers from its origin node to its destination node . Class leaves the network on reaching a node of its destination set ; at every other node it has a queue , whose length at the end of slot is .
The constraint set is the family of sets of servers that may be active in the same slot. Assumption C.1 says that every subset of an activation set is an activation set. In each slot a stationary policy, given the state , chooses a set of servers in and the class each active server serves; an activation rule never activates more servers of queue than there are customers . The class of all such rules is . An activated server completes its service with probability , independently. New arrivals are i.i.d. over slots, independent across queues and of the services, with finite second moments and means . Under a stationary rule the vector is a Markov chain on .
The chain is stable (Definition 3.1) if, from every transient state, it enters a closed communicating class with probability one, and every state of a closed communicating class is positive recurrent. The stability region of a policy is the set of rate vectors for which the system is stable under ; the stability region of the system is .
A family is an -admissible flow if it satisfies flow conservation, at every queue; is its total flow through server . With the convex hull of the indicator vectors of the activation sets,
The system stability region is pinned between and its closure, and policy , whatever its tie-breaking, stabilizes every rate vector in . Inclusions are not strict.
An optional item states the claim of Remark 1: if , then for every .
Theorem 3.2 shows that a throughput-optimal stationary policy exists, which is not obvious: stability regions of different policies need not be nested, so a policy whose region contains all the others has to be exhibited. It also describes the system stability region by a deterministic flow condition, , which can be checked without simulating any policy. The same drift argument underlies the stability proofs of max-weight switch schedulers, back-pressure routing and the drift-plus-penalty method.
The result is proved in the paper, with a proof sketched in places (Theorem 3.1 is called "a trivial extension of Foster's criteria", Lemma A.1 is omitted, Lemma 3.3 is argued by ergodicity in a paragraph). As far as a search of the platform shows, none of these statements has a machine-checked proof: Foster's criterion is posed on the platform only for irreducible chains on , and the back-pressure results already posed concern fluid models of other networks. A complete formal development would supply the reducible-chain Foster criterion, the convex-geometry lemma on , the quadratic drift computation and the ergodic converse.
The obvious argument is a quadratic Lyapunov drift bound, but it does not go through as is in three places. First, the drift bound needs a direction of decrease from every large state: the largest queue must be connected to a destination through servers that can actually be activated, which is where assumption C.2 and the topology of enter (A.21)–(A.24). Second, stage 3 of defers some activations to respect the rule "no service for nonexisting customers", so the chosen schedule is not exactly maximum-weight and the loss has to be bounded uniformly. Third, the chain is in general reducible, so Foster's criterion for irreducible chains does not apply; the extension must show that every closed class meets the finite exceptional set and that transient states are left almost surely. The converse, Lemma 3.3, needs a law-of-large-numbers argument for an arbitrary stationary rule on a positive recurrent class, together with compactness of acyclic flows (Lemma 3.1).
Nodes, servers and classes are Fin L, Fin N, Fin J (0-based). is a Set (Finset (Fin N)); a queue is a pair with , and a state is a function from queues to . A multiclass activation vector assigns to each server an optional class. The transition matrix of the queue-length chain is written out explicitly as a sum over arrival vectors and Bernoulli service outcomes; Definition 3.1 is stated through this matrix (first-entry probabilities, essential states, positive recurrence), with values in .
Conventions committed to, and hypotheses added relative to the page:
A formalization in which asks for stability under one convenient arrival law, or in which negative rates are admitted, or in which is one fixed tie-break, would be a different theorem; the definitions rule each of these out.
Infrastructure needed: hitting probabilities and positive recurrence for countable chains (reusable beyond this mission), convex hulls of finite point sets, a cycle-cancelling bound for multicommodity flows, and the ergodic theorem for positive recurrent chains. Proofs of any milestone, and reusable lemmas on countable Markov chains, are welcome.
A d.c. program minimizes a difference of two convex functions. Many nonconvex problems of practical interest have this form: every function with a locally Lipschitz gradient on is d.c., the class is closed under finite sums, products and finite suprema, and constrained problems enter through indicator functions. Pham Dinh Tao and Le Thi Hoai An (SIAM J. Optim. 8 (1998)) use this structure to build the DCA, an algorithm for the trust-region subproblem , a basic step of trust-region methods in nonlinear optimization. The algorithm rests on a duality theory for d.c. programs, which §3.1 of the paper sets out. This mission is the global half of that theory.
Timeline.
Let with its canonical inner product , and identify the dual space with . Functions take values in . A function is in if it is convex, lower semicontinuous, never , and finite at some point. Its effective domain is , and its conjugate is
For , the subdifferential is the set of with for all . For the -subdifferential is
Given , the d.c. program and its dual are
with the convention . Throughout, the paper assumes the inclusions
and denote the solution sets of (P) and (D).
For every ,
The result. Theorem 3.1(i) characterizes global minimizers of a nonconvex function by inclusions between convex objects. It is a certificate of global optimality that uses only convex analysis. Parts (iii) and (iv) say that a solution of either program yields a solution of the other through a subgradient. This is the mechanism of the DCA, which alternates , . The paper notes that condition (i) is hard to use in an algorithm and that the DCA rests on local conditions instead. The global condition remains the reference statement that the local theory and the DCA approximate.
Formalizing it. All results here are classical and proved on paper. Parts (iii) and (iv) are proved in references the paper cites, not in the paper itself. None of them has a machine-checked proof on the platform. The mission provides a Lean layer for d.c. programming on : the convention-respecting difference, the -subdifferential, the standing assumptions, and the primal and dual solution sets. Missions II and III of the series reuse this layer for local optimality and for the convergence of the DCA.
The paper's proof is short, but each step uses a fact that needs separate work. The duality requires the biconjugation for , and an exchange of two infima in the extended reals under the convention . The step (7) ⇔ (8) has a hidden case: a point of . Ruling it out needs for , a nontrivial property of lower semicontinuous proper convex functions. The obvious approach, computing with real numbers, fails because , , and all take the value , and the extended-real arithmetic of Lean does not follow the paper's convention.
EuclideanSpace ℝ (Fin n). Functions are EReal-valued.ThreeOpSplitting.ConvexRates.IsProperClosedConvex, is InertialFB.IFB.IsSubgradient, and the conjugate is CondatPD.FinDim.conj, an extended-real supremum over all of .dcSub, which returns when the first term is . , and are defined through it.intrinsicInterior, and the "in this case" inclusions into and .EReal-valued functions on EuclideanSpace in the conventions of CondatPD.FinDim.conj, nonemptiness of -subdifferentials, and the extended-real infimum exchange. These are reusable well beyond d.c. programming.A single server shared by several classes of jobs must decide, at every moment, which class to work on. When each class incurs a linear delay cost per unit of waiting time and needs mean service time , the classical rule (serve the waiting class with the largest ) minimizes expected cost in many settings, from the M/G/1 queue to discrete-time models (Buyukkoc, Varaiya and Walrand, Adv. Appl. Probab. 1985). Linear costs are a strong restriction: in telecommunications, manufacturing and service systems the penalty for delay often grows faster than linearly, and with convex costs the static priority order of the rule is no longer optimal.
Van Mieghem (Ann. Appl. Probab. 1995) proposed the generalized rule: with nondecreasing convex delay costs and marginal costs , serve the class with the largest index evaluated at its current delay or workload. The paper proves that, in heavy traffic, this dynamic index policy is asymptotically optimal among all scheduling policies, including policies whose scaled workloads do not converge. This mission formalizes that result and the chain of propositions it rests on.
There are job classes. In the th system, the th class- job arrives after an interarrival time and needs service . counts class- arrivals in and counts class- completions within units of server time. A policy is an allocation , where is the time in spent on class . From it come the headcount , the workload (work present in class ), the class-FIFO delay of a job arriving at , and the cumulative cost . Feasible policies are continuous, nondecreasing and work conserving.
The th system runs on and is studied at the diffusion scale: , , likewise, and . Arrival and service processes expand as and . Assumption 1 asks that these terms converge, with rates , , and that the system is in heavy traffic: , where and is the traffic intensity. Assumption 2 asks that the costs scale, , and Assumption 3 that be strictly convex and .
The scaled total workload has a policy-independent limit , with the one-dimensional reflection map. The key static problem splits a total among classes:
Under Assumptions 1–3, for feasible policies with
the costs and delays converge,
Lemma 1 and Proposition 2 (jumps (33)–(34), first-order allocation (27), total workload (32), boundedness, equivalences (35)); Proposition 3 (); Proposition 4 (Little's law); Proposition 5 (converging policies); uniqueness and continuity of (§4.1); the Kuhn–Tucker characterization (46)–(50); and Proposition 6, the lower bound
Proposition 6 is what makes Proposition 7 an optimality statement; it is a separate milestone and not part of the goal.
The result. Proposition 7 identifies a simple, myopic index rule that is optimal at the diffusion scale for every time simultaneously, for arbitrary convex delay costs and nonstationary rates. It extends the rule beyond linear costs, links it to the "hug the optimal workload curve" policies of heavy-traffic control, and shows that the instantaneous allocation problem (43) is all that matters asymptotically. Later work on Brownian control of multiclass queues and on convex-cost scheduling (Mandelbaum and Stolyar 2004) builds on this.
Formalizing it. The paper's proofs are short and informal at several points, and the formalization makes these points explicit: the domain of every uniform limit, the policy class, and the reading of . No part of this paper has a machine-checked proof. A completed mission would give a verified heavy-traffic analysis of a multiclass single-server queue at the sample-path level, the first on the platform with a deterministic diffusion scaling and an explicit reflection map.
The obvious route is to show that converges and then pass to the limit in the cost. That fails for the lower bound: Proposition 6 must cover policies whose class workloads never converge (polling-type policies), so it cannot use compactness of and must instead compare the cost of an arbitrary split of with the optimal split, locally in time. For the goal, (51) controls only the indices, so the convergence of must be extracted from (51) through the inverse marginal costs, the convergence of the total workload, and the Kuhn–Tucker conditions of (43). Delay convergence then needs a uniform control of over windows of length , and cost convergence needs the convergence of the costs applied to delays of order .
Lean namespace GenCMu.HeavyTraffic. The development is deterministic and works one sample path at a time; the stochastic version (Proposition 8) is not part of this mission. Conventions committed to:
Fin d; job indices start at ; every "→" between functions is uniform convergence ((11)), on unless stated; is written as "eventually bound ".A trivializing formalization is ruled out: no theorem assumes the convergence of or , the uniqueness of minimizers, or the lower bound, and the joint satisfiability of all hypotheses has been checked in Lean for .
Needed infrastructure: sample-path reflection-map estimates, counting/partial-sum inversion with uniform errors, parametric convex optimization (Berge's theorem for (43)), and Riemann-sum arguments for the lower bound. The reflection-map and inversion lemmas are reusable beyond this mission. Contributions to any milestone are welcome. The definitions are frozen, so a proof that needs a different definition should be raised in the discussion.
An arbitrator who must choose among collective options for a group of players usually does not know the players' private characteristics. The arbitrator can only ask, and a player who expects to profit from a false answer may give one. Before designing any procedure, the arbitrator therefore needs to know which expected-payoff allocations can be reached at all once strategic misreporting is taken into account.
Myerson (1979) answers this for Bayesian collective choice problems with finitely many types. Restricting attention to mechanisms that simply ask each player for their type, and that make honest answers optimal, loses nothing: every expected-payoff allocation that any mechanism can produce in equilibrium is already produced honestly by such a direct mechanism, and conversely. This is the revelation principle in the form used throughout Bayesian mechanism design. It is what makes incentive-compatibility constraints the starting point for auction design, bilateral trade, and the bargaining solution in the second half of the same paper.
Timeline. Gibbard (1973) gave the dominant-strategy form of the principle. Rosenthal (Review of Economic Studies, 1978) studied arbitration of two-party disputes under uncertainty; Myerson notes that Theorem 2 could be derived as a corollary of Rosenthal's Theorem 3. Dasgupta, Hammond and Maskin (1979) gave general Bayesian implementation results in the same year. Myerson's Theorem 2 states the principle as an equality of interim payoff sets over all finite response sets. Myerson (1982) later extended it to principal–agent problems with moral hazard.
A Bayesian collective choice problem has a nonempty finite set of players , a nonempty finite set of types for each player, a nonempty finite set of collective choices, utilities depending on the choice and on the true type profile , and a probability distribution on type profiles. With the marginal of type , a player of type assigns the conditional probability to profiles with , and to the others.
A choice mechanism on response sets (nonempty finite sets of possible answers) is a function with for every response profile . On the standard response sets , the payoff of type who reports while the others are honest is
The mechanism is Bayesian incentive-compatible if for all . Its honest allocation is the vector with coordinates , indexed by the disjoint union of the . The incentive-feasible set is
On general response sets, a response plan is a probability distribution over for each type . Plans give type the payoff
They form a response-plan equilibrium for if no type of any player gains by switching to any other response plan . The equilibrium-feasible set collects over all choice mechanisms , on all nonempty finite response sets, and all response-plan equilibria for .
Both inclusions are asserted for every Bayesian collective choice problem. says equilibrium behaviour under any mechanism can be replicated honestly by an incentive-compatible direct mechanism. says honest reporting is itself an equilibrium of every incentive-compatible mechanism.
The result. Theorem 2 reduces a search over all communication protocols, an unbounded family of response sets and mixed reporting behaviours, to a finite system of linear inequalities in on a fixed finite domain. Combined with Theorem 1 of the paper, which shows is a nonempty compact convex set, it justifies applying a bargaining solution to rather than to some larger, ill-defined set of attainable outcomes. The same reduction underlies the use of incentive constraints in optimal auctions, bilateral trade and correlated-type mechanism design.
Formalizing it. The result is classical and its proof is short, but it is a statement about all finite response sets at once, and the equality of two sets of payoff vectors is sensitive to the conventions: which plans are allowed as deviations, where the conditioning happens, and whether the induced mechanism is a genuine probability distribution. A machine-checked version pins these down. To our knowledge no formal proof of this finite Bayesian revelation principle exists. The platform has related, unproved items in other models: MechanismDesign.Robust.revelation_principle (Börgers, Prop. 10.2, on a countable Harsanyi type space with PMF lotteries; one inclusion, outcome equivalence) and single-agent, quasi-linear and dominant-strategy revelation principles from the same book. None of them is the statement here.
The mathematics consists of finite sums, but the bookkeeping is the obstacle. Milestone 1 requires exchanging a sum over response profiles with a product over players and using that each plan sums to one. Milestone 2 requires recognizing a lie in as a particular whole response plan in : the plan that, at every type, behaves as type would. Because vanishes off , only its value at matters. For milestone 3, a mixed deviation from honesty has to be bounded by the best pure misreport, a convex-combination argument over . Identifying the side of the goal also needs instances on an existentially chosen family of types.
All objects live in MyersonBargaining.Revelation. Players form a nonempty finite type ι; types A i, choices C and response sets S i are nonempty finite types in Type. Mechanisms and plans are real-valued functions with the probability constraints as predicates (IsChoiceMechanism, IsResponsePlan), event first and condition second: π c s, σ i s a. Allocation vectors are functions on Σ i, A i. The paper's loose phrases are read as follows:
S : ι → Type and its instances;The product in (12) is printed with ; it is formalized with , as the paper's own induced mechanism on p. 66 uses. Milestone 1 is stated for arbitrary response plans, not only for equilibria. Section 6's numerical example is not formalized.
A trivializing formalization is ruled out explicitly: fixing in , restricting deviations to pure plans, or stating only would each change the theorem, and none is done.
A complete development needs finite sums over dependent product types (Fintype.piFinset, Finset.prod_univ_sum), Function.update on dependent families, and nothing beyond Mathlib. The two definition modules (the model and the response-plan objects) are reusable by any finite Bayesian mechanism-design formalization. Proofs of any milestone, alternative proofs via Rosenthal's argument, and cleaner restatements as lemmas about stochastic matrices are welcome.
A random walk in a random environment uses transition probabilities selected once for each site, rather than probabilities resampled at every step. Even when the site environments are independent and identically distributed, the walker revisits the same local bias whenever it returns to a site. Its long-time motion can therefore differ sharply from that of a walk with a single averaged right-step probability. Solomon’s 1975 paper established the recurrence and speed classification for this one-dimensional model and then examined a two-value example in which some sites are one-way mirrors: the walker can pass through them to the right but cannot cross them to the left. The example isolates how a sequence of random intervals between mirrors produces slow growth and phase-dependent limit laws Solomon 1975, §2.
The present mission concerns §2 of that paper, pp. 10–20. Its central question is how far the walker has traveled after steps when the mean crossing time reaches or exceeds the critical threshold. At criticality, a logarithmic correction replaces ordinary linear speed. Above criticality, the paper gives limits along subsequences whose logarithmic fractional parts approach a fixed phase.
Let be a probability space and let , , be independent, identically distributed random variables in . The environment is the complete sequence . Conditional on a fixed environment, a nearest-neighbour walk starts at and, from site , moves to with probability and to with probability . The annealed probability averages the conditional path law over the environment. In Lean this joint law is specified on every finite path cylinder together with every measurable event of the whole environment, so it determines the dependence between and .
Fix and . Solomon’s example has with probability and with probability . Equivalently, the left-to-right odds ratio takes values and . A site with is a one-way mirror. Write and let be the position of the th mirror strictly to the right of zero. Let be the first time the walk reaches site , with if it never does. For , means the logarithm in base , and is the fractional part.
The parameters used below are
When , the paper specifies a probability law on by its Laplace transform
Here also denotes that law’s distribution function at . The bilateral series converges in the supercritical parameter range. The source’s notation uses the same letter for a distribution and its distribution function; the Lean development keeps these roles separate as a measure and its value on .
The first clause of Theorem (2.20) is the critical growth law. If , then
The second clause describes the supercritical case. If , , and , then for each ,
Both clauses are the goal. The milestones record the transform identity of Lemma (2.5), its approximation and scaling limits in Lemmas (2.6)–(2.7), the mirror passage-time limits of Lemma (2.10), and the ordinary passage-time limits of Theorem (2.18). The fractional part in the goal uses base ; the two passage-time results use base , exactly as printed Solomon 1975, pp. 12–19.
The critical law identifies the constant in the growth scale . The supercritical law shows that a single power normalization does not erase the logarithmic phase of the environment: the limiting distribution depends on the phase approached by the chosen subsequence. These assertions describe the position itself, rather than only the time needed to reach a distant site. They complement the paper’s general speed theorem by resolving the zero-speed behavior in a concrete model Solomon 1975, Theorems (1.16) and (2.20).
The results are proved in the 1975 paper; the open work here is machine checking their definitions, statements, and proofs. The development also yields reusable interfaces for a nearest-neighbour chain specified by cylinder probabilities, first-passage times that can be infinite, and Laplace-transform arguments for random time changes. The mission’s statements currently compile locally with proof placeholders, so they are formalization targets rather than machine-checked theorems.
The one-way mirrors create independent, identically distributed blocks of crossing times, but those times have tails governed by the random spacing between mirrors. At , their accumulation produces a logarithmic correction; at , the underlying geometric scales preserve the fractional part of a logarithm. An ordinary law of large numbers for passage times therefore cannot supply both limits. Moreover, a limit for passage times to the random mirror positions does not immediately give a limit for passage times to deterministic sites, and converting a passage-time limit into a position limit requires control of the inverse time change. The source separates these tasks across the milestone results Solomon 1975, pp. 11–20.
The Lean environment is the pinned Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. The position and environment are integer-indexed; time is natural-number-indexed. The one-way-mirror parameter range is , , . The strict bounds on make both atom probabilities meaningful and the logarithm base valid. The source uses these bounds implicitly. All probabilities concern the annealed joint law, not an arbitrary process with the same one-time marginals.
First-passage times are extended natural numbers, with infinity on paths that never hit the target. The real-valued limits convert finite passage times to real numbers; under the stated model, infinite passage times form a null event. The location of a nonexistent next mirror is assigned zero for a total Lean function, again only on a null event in this model. The Laplace transform of an infinite passage time is defined as zero. Convergence in probability uses TendstoInMeasure; convergence in law is expressed by convergence of distribution functions at continuity points. The limit-law family is constrained to probability measures supported on with the exact transform (2.12), preventing a degenerate or unrelated choice of .
A complete proof needs measurable cylinder laws, independence of the mirror gaps, hitting-time and transform calculations, asymptotics of one-sided and bilateral series, distributional convergence from Laplace transforms, and inversion from passage time to position. Work on any of these components is in scope. The statement keeps both source regimes and every constant; replacing the joint walk law by independent marginals or choosing an arbitrary limit distribution would change the theorem.
Many quantities in operations research accumulate over time in a system that periodically starts afresh: the cost incurred by an inventory system that returns to the same stock level, the work completed by a server between successive moments it empties, the reward collected by a machine between repairs. The basic question about such a quantity is its long-run rate: does the amount accumulated by time , divided by , settle down, and to what?
W. L. Smith's 1955 paper Regenerative stochastic processes (DOI 10.1098/rspa.1955.0198) introduced the class of cumulative processes to answer this question, and §5·3 of the paper proves the answer, Theorem 7, which Smith calls "the ergodic theorem": the long-run rate equals the expected accumulation per cycle divided by the expected cycle length. In later textbooks this is the renewal–reward theorem, the standard tool for computing long-run averages of regenerative systems in queueing, inventory and reliability models.
Timeline. Doob (1948) proved the strong law for renewal counting processes (Trans. AMS 63). Smith (1955) defined cumulative processes by conditions (C1)–(C2) and proved Theorem 7 under a first-moment condition on the variation per cycle, together with central limit theorems (Theorems 9–10) for the same processes.
Fix a probability space .
A renewal process is a sequence of independent, identically distributed, non-negative random variables that are not zero with probability one, i.e. . Write . In this mission the delay is , the regeneration epochs are , and the counting variable
is the number of regenerations in (the paper's "greatest integer such that "). The forward variable measures how far is from the regeneration epoch .
Let be a real-valued process with . Its cycle increments are , , and . On a path of bounded variation on every finite interval, the variation process is the total variation of the path over ; the cycle variations are , and .
The process is a cumulative process when
If is a cumulative process, , , and , then
The statement fixes no rate and no constant; it is the exact limit of the paper.
The ergodic theorem turns a question about a whole sample path into a question about one cycle. Once a system is shown to regenerate, its long-run average cost, throughput or utilization is the ratio of two one-cycle expectations, which can often be computed in closed form. This is how long-run averages are evaluated for -type queues, inventory policies and alternating-renewal reliability models, and it is the first step in average-cost analyses of regenerative Markov decision processes. Lemma 8, with , also controls the error term in Smith's central limit theorem for cumulative processes.
The result is classical and proved. As far as the platform and Mathlib are concerned, it is not formalized: Mathlib has the strong law of large numbers for i.i.d. sequences (ProbabilityTheory.strong_law_ae) but no renewal counting process, no renewal strong law, and no renewal–reward theorem. A complete development gives machine-checked versions of all three, stated for real time and for cycle lengths that may vanish with positive probability.
The obvious argument writes as and applies the strong law to each factor. This fails in two places. First, is not a sum of whole cycles: the cycle containing is only partly completed, and its contribution has to be shown negligible. The increment does not control it, because may oscillate inside a cycle and return; it is the variation that bounds the partial contribution, which is why the hypothesis is on rather than on . Second, the strong law is a statement about a deterministic index , while here the index is random and depends on the cycle lengths, which need not be independent of the increments. Transferring almost-sure convergence through the random index requires almost surely, which in turn uses .
Time is real: every limit is along in (Filter.atTop on ℝ), and "with probability one" is an almost-everywhere statement placed outside the limit. Random variables are real-valued. The renewal process is the structure IsRenewalProcess (cycle lengths measurable, mutually independent, identically distributed, non-negative everywhere, ); and are explicit hypotheses holding at every sample point. Moments are Bochner integrals guarded by integrability hypotheses: is integrability of , is integrability of . The positivity is never assumed; it follows from .
The count is a cardinality; on the null event where infinitely many epochs lie below it takes the value , and finiteness is never assumed. The variation process is Mathlib's eVariationOn of the path over , set to on paths that are not of bounded variation, exactly as the paper prescribes.
Condition (C1) is read literally: only the increments are i.i.d., and no independence between cycle lengths and increments is assumed. In addition the cycle variations are assumed identically distributed; the paper's notation presupposes this. The statement is not trivialized by a stronger model: taking to be a Lévy process, or a deterministic multiple of , would make the theorem immediate and is not what is formalized.
Two misprints of the paper are corrected in the formal statements and kept in the verbatim milestone text: (5·3·4) prints the limit as , which must be ; and the proof bound (5·3·1) uses alone, where the interval also meets cycle .
Needed infrastructure: a renewal counting process in continuous time with its strong law; a lemma that almost-sure convergence of a sequence passes to a random index tending to infinity; the comparison for paths of bounded variation. All three are reusable well beyond this mission (renewal–reward arguments, regenerative simulation, average-cost Markov decision processes). Contributions of any milestone, and of these general lemmas as separate theorems, are welcome.
Nonparametric regression estimates the conditional mean of a real response given a predictor without assuming that it belongs to a finite-dimensional family. Most practical estimators of this kind are local averages: kernel estimators (Nadaraya 1964, Watson 1964), nearest-neighbor rules (Cover and Hart 1967), and their many variants all predict at a point by a weighted average of the observed responses, with weights that depend only on the predictors.
C. J. Stone's 1977 paper in the Annals of Statistics (DOI 10.1214/aos/1176343886) asked when such a rule is consistent: when it converges to the true regression function in for every joint distribution of with , without smoothness or moment assumptions beyond that. Its Theorem 1 answers the question in terms of five conditions on the weights alone. The result is the standard starting point for distribution-free regression theory; it is the first theorem of the monograph of Györfi, Kohler, Krzyżak and Walk (2002), where it is called Stone's theorem, and it underlies the universal consistency of nearest-neighbor, kernel and partitioning estimates.
Let be a probability measure on and let be independent with law . A sequence of weights assigns to each and each point real numbers
The weights are nonnegative if every and probability weights if in addition .
When are i.i.d. with real valued, the estimate of is
The sequence is consistent if, for every such joint distribution with -marginal and every with ,
The five conditions of Theorem 1 are:
and conversely, if is consistent, then (4) and (5) hold; if moreover for all , then (3) holds; and if and (2) holds, then (1) holds. The goal is the full theorem, both directions, as one statement.
The result. Theorem 1 reduces a statement about all joint distributions of to properties of the weights under the law of alone. For probability weights, conditions (2) and (4) hold automatically, and (1), (3), (5) become necessary and sufficient (Corollary 1). This is how Stone proves that nearest-neighbor weights with suitably vanishing coefficients are universally consistent (Theorem 2 of the paper), and how consistency transfers to estimators of conditional quantiles and to approximate Bayes rules in classification and decision problems (Sections 7–8). Condition (1), the only condition that is not a convergence statement, is the one that later work on kernel and partitioning estimates had to verify by geometric covering arguments.
Formalizing it. The theorem is proved in the paper and in textbooks; it has no machine-checked proof that we know of. A formalization produces a reusable criterion: any later development of local-averaging estimators can discharge consistency by checking five conditions about the predictor distribution. The supporting propositions are of independent use: Proposition 1 is an approximation lemma for weighted empirical averages, and Proposition 7 is a uniform-boundedness principle for sequences of positive operators on .
The sufficiency half combines three ingredients that have to fit together at the level of measure theory: approximation of an arbitrary function by continuous functions with compact support, uniformly over through condition (1); a variance computation for the noise term that conditions on the predictors; and a truncation argument to pass from bounded responses and to all . The natural first idea, to apply a weak law of large numbers to , fails because the weights are dependent on all of and are not identically distributed.
The necessity half needs separate arguments for each condition: a test-function argument with bounded continuous for (3), a contradiction argument summing a sequence of functions for (1), and a Gaussian anti-concentration argument for (5), which is where the auxiliary normal variables of the paper enter.
TendstoInMeasure. Sample indices are -based. Conditions on individual are stated for .Weighted voting models assign a coalition a win when its combined vote reaches a quota. The Shapley value measures a player's contribution by averaging the change it makes when added to every possible predecessor coalition. This is straightforward to define for a finite list of voters, but a voting body may contain a few major holders and a very large population of individually small holders. A calculation made for a finite approximation should then have a stable meaning as the small holdings are divided more finely. Milnor and Shapley's oceanic game gives that question a precise form and asks whether its major-player values agree with the limits of finite weighted majority games. Milnor and Shapley, RAND RM-2649 (1961).
The question matters whenever a finite voting model is used to represent a diffuse electorate or ownership base. Without a continuity result, the measured power of a major voter could depend on how an otherwise identical mass of minor votes was artificially split. The memo's Theorem 1 establishes the required stability under an explicit small-weight condition. The result is a known theorem from the 1961 memorandum; the task here is its Lean formalization, including the mathematical objects that make its statement meaningful.
Fix a finite set of major players, with nonnegative weights . The ocean is a continuum of individually insignificant voters represented by the unit interval , with total weight . A coalition's vote is its major-player weight plus times the Lebesgue measure of its oceanic part. It wins when that vote reaches a quota . The formal development uses Fin m for and real weights; the underlying voting rule is the one in §2 of the memorandum. Milnor and Shapley, §2.
To assign a value to a major player, insert each major player independently and uniformly into the ordered ocean. A position vector lies in the cube . Write and . Major player is pivotal when the predecessor weight is below the quota and adding reaches it, in the memo's weak-boundary form
The oceanic major-player value is the probability of this event. Since the insertion positions are uniform, it is also the -dimensional Lebesgue volume of the corresponding set . Equalities at boundary positions have zero volume. Milnor and Shapley, (2.3)–(2.4), pp. 4–5.
At stage , the finite approximation has the same major players, followed by minor players with nonnegative weights . Its quota and major weights are and . A coalition has value one if its weight is at least , and zero otherwise. The finite-game value is the Shapley value of that coalition function. The published Shapley-value definition is reused for this general finite-game object; only the quota game and its oceanic limit are defined for this mission. Milnor and Shapley, Appendix (A.1), (A.4).
The principal target says that if quotas and major weights converge, the total minor weight tends to , and every minor weight becomes small, then each major-player value converges:
This is Theorem 1, equations (3.1)–(3.2), of the memorandum. Its conclusion refers to the pivotal-probability definition of above. Milnor and Shapley, Theorem 1, p. 6.
The milestone list follows three statements present in the source: equation (3.4) partitions by the predecessor set ; equations (3.5)–(3.6) give the volume of each part as a one-variable integral with clamped endpoints; and Appendix (A.1)–(A.3) states the finite-game limit as a sum of those integrals. Their shared expression is
The appendix's limit statement concerns ; Theorem 1 concerns . Both are separate targets in the formalization. Milnor and Shapley, §3 and Appendix.
The theorem makes the major-player value independent of a particular fine division of the minor vote, provided the total minor weight and the other parameters converge as stated. The same oceanic game can therefore stand for many finite approximating sequences. The integral expression also gives a precise comparison point between finite Shapley values and the geometric definition by pivotal volume. Milnor and Shapley, §1 and Theorem 1.
The mathematical result is proved in the cited memorandum, and its appendix recapitulates a limit theorem from the preceding work in the series. The formalization work is to state and prove these known claims over Lean's finite index types, Lebesgue measure, integrals, and limits. Reusable components include the quota-game characteristic function and the interface between a finite Shapley value and a changing number of minor players. The mission does not claim that the historical theorem is open, nor that these target statements already have machine-checked proofs.
The number of minor players changes with , so the finite Shapley sum does not have a fixed set of coalitions. Merely taking a limit term by term in that sum does not justify its limit: the number and weights of the terms also change. The condition that the largest minor weight tends to zero controls a triangular family of games, while the oceanic definition is a measure of a geometric pivotal event. Matching the two descriptions requires care at the quota boundaries and at intervals that may be empty. These are the central issues represented by the appendix milestone and by equations (3.4)–(3.6). Milnor and Shapley, §3 and Appendix.
The Lean model uses Fin m for major players and Fin (n l) for minor players at stage , concatenated with majors first. It uses a real-valued quota characteristic function, the published finite Shapley-value definition, and product Lebesgue volume on the cube for uniform insertion positions. The predecessor relation is strict, , exactly as in §2; the complementary cell relation is weak. The pivotal inequalities follow (2.4), and the oceanic value is defined from their volume. Defining it as would make the comparison demanded by Theorem 1 empty, so that equality remains a theorem-level obligation.
The source defines oceanic games with , , and . The finite approximants are read as weighted majority games with nonnegative weights; that condition is explicit in Lean. No sign condition is imposed on the stage quotas , since (3.2) states none (only the limit satisfies ). The statement does not impose the footnote's upper bound because Theorem 1 only concerns major-player values, which are zero in a null game. An empty minor list is permitted at an early stage. Rather than taking the maximum of an empty list, Lean says that for each , all minor weights are eventually at most ; with nonnegative weights this is the paper's vanishing-maximum condition. A positive limiting ocean weight also excludes an eventually empty minor population.
The integral in (A.3) is a set integral over the stated intersection of closed intervals, so an empty intersection contributes zero. For (3.5), the endpoints are clamped to . The condition ensures is nonnegative before it is represented as a natural-number exponent. Contributions that strengthen the measure-theoretic partition, the cell-volume computation, or the varying-population finite limit are within scope; a proof may use other intermediate lemmas while keeping the sourced target statements unchanged.
Many quantities in queueing, inventory and reliability models are additive functionals of a regenerative process: the total work processed by a server up to time , the cost accumulated by an inventory policy, the time a machine spends broken. Each such quantity grows by independent, identically distributed amounts over the cycles between successive regeneration points. W. L. Smith called these cumulative processes in Regenerative stochastic processes (Proc. R. Soc. Lond. A, 1955), the paper that introduced the term "regenerative process" and laid out its limit theory. Long-run averages of such quantities are estimated by simulation and by statistical observation of real systems. Confidence intervals for these estimates, and the regenerative method of simulation output analysis, rest on the central limit theorem for cumulative processes. When several quantities are estimated at once (a ratio of two rewards, a vector of costs), they rest on its joint version for several cumulative processes driven by the same regenerations.
Timeline:
On a probability space , let be independent, identically distributed, non-negative random variables with (a renewal process), and . The regeneration epochs are (), and is the number of epochs in (in Smith's words, the greatest with , where ). Write .
A real process with is a cumulative process if (C1) its cycle increments , , are i.i.d., and (C2) with probability one its paths have bounded variation on every finite interval. The variation process has increments . Moments are written and .
cumulative processes are based on the same sequence of regeneration points when the cycle vectors are i.i.d. in . Put . The covariance matrices are
If and for every , then as
and if in addition ,
Theorem 10 is the multivariate central limit theorem for regenerative processes. Its second assertion with and the delta method gives the asymptotic normality of ratio estimators , the basis of the regenerative method of simulation output analysis. With , Corollary 9·1 recovers Feller's central limit theorem for renewal processes, which Smith points out (p. 9). The first assertion, with the random centring , needs only , which matters for heavy-tailed cycle lengths.
The results are classical and proved, and none of them is formalized. Mathlib has the central limit theorem for i.i.d. real sums with a deterministic number of terms and multivariate Gaussian laws, but no random-index central limit theorem, no renewal counting process and no regenerative process. A formal development would supply Anscombe's theorem (useful well beyond renewal theory, for sequential analysis and random sums), the renewal strong law and a reusable model of cumulative processes.
The obvious argument writes as the sum of the first cycle increments plus a remainder and applies the classical central limit theorem. This fails at two points. First, the number of summands is random and depends on the summands themselves (cycle lengths and rewards are typically dependent), so the classical theorem with a deterministic index does not apply and conditioning on destroys the i.i.d. structure. Anscombe's theorem is needed exactly for this; it requires control of the partial sums uniformly over a window of indices around , not at a single index. Second, the remainder over the incomplete cycle at time must be shown negligible on the scale using only a second moment of the cycle variation; Lemma 8 does this almost surely. For the vector statement, the scalar theorem must be lifted to convergence in distribution in with a possibly degenerate covariance matrix, where the scalar theorem's hypothesis can fail along some directions.
Fin M); cycle lengths are a sequence with .eVariationOn) of the path on , set to for all on paths of infinite variation, as Smith allows.TendstoInDistribution to multivariateGaussian 0 a on EuclideanSpace ℝ (Fin M). The matrices and are defined as covariance matrices, hence positive semidefinite, so the limit is a genuine (possibly degenerate) Gaussian law and not Mathlib's Dirac fallback for non-PSD input.cdf (gaussianReal 0 1) α for every real . The paper's implicit and are explicit hypotheses; without them the quotients are in Lean and the statements would be false.Integrable hypotheses, never encoded through the value of an integral.Contributions welcome: a proof of Anscombe's theorem from Mathlib's central limit theorem; the renewal strong law from strong_law_ae; measurability lemmas for and ; the Cramér–Wold step.