Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A Markov decision process with finitely many states and actions is usually run either with a discount factor or under the long-run average criterion. Without discounting, the total return over an infinite horizon is typically infinite, and the average return per period ignores everything that happens in any finite stretch of time: two policies with equal gain (average return per period) can differ by a fixed amount of income forever, and the average criterion cannot tell them apart. Finer, undiscounted criteria that break such ties are a standard topic of the MDP literature (Puterman, Markov Decision Processes, Ch. 10), and the paper of this mission is one of their starting points.
Timeline. Howard (1960) introduced policy iteration for the average-return problem. Blackwell (1962) expanded the discounted return of a stationary policy near as , defined 1-optimal ("nearly optimal") policies, and showed that the stationary 1-optimal policies are exactly those that maximize the gain and then the bias . Veinott (1966), the source of this mission, gave a finite algorithm for such policies and, in §5, a characterization of the same set by an undiscounted criterion: comparing the Cesàro averages of the finite-horizon total returns. Later work (Veinott 1969) developed the hierarchy of -discount optimality criteria from this starting point.
There are finitely many states and a finite set of actions; in state , action earns the income and moves the system to state with probability . A decision rule chooses an action in each state; is the vector with entries , and is the Markov matrix with entries . A policy is a sequence of decision rules, with , and is the stationary policy that uses every period.
The limit matrix exists for every Markov matrix. The gain and bias of are
Vectors are compared coordinatewise. The decision rules of maximal gain form
and those of maximal bias among them form
Finally, the -period total expected return of a policy , starting from each state, is
For every ,
where the inequality is coordinatewise and the limit is taken in .
The result. Theorem 7 gives the set , defined through the discount-factor expansion, an interpretation that involves no discounting at all: maximizes gain and then bias exactly when, from every starting state, its Cesàro-averaged finite-horizon returns are in the limit at least those of every other stationary policy. Combined with Theorem 4 it identifies the stationary 1-optimal policies with the stationary policies that are optimal under this average-overtaking comparison. The paper records a consequence (an optimal policy in the average-overtaking sense (26) that is stationary is 1-optimal) and conjectures the converse; that remark and conjecture are not part of this mission.
Formalizing it. The results are proved in the paper (Theorems 3 and 4 are Blackwell's). None of them is formalized: the Blackwell expansion (Theorem 3) is an open item on Prove2Me, referenced here, and Theorem 4, the -step identity, (27), (28) and Theorem 7 have no machine-checked proof. A complete development gives the first formal treatment of Cesàro-averaged finite-horizon returns of a finite MDP and their relation to gain and bias.
The paper calls Theorem 7 "an immediate consequence of the representation (28)". For the direction "the limit condition implies " this is accurate: a state where would drive the average to , so , and then the constant terms give the bias comparison over . The converse is where the obvious argument stops. It must hold for every , including ; at a state where for such a , (28) needs , and the definition of only compares biases with gain-maximal rules. That inequality comes from 1-optimality of (Theorem 4) together with the expansion of Theorem 3, not from (28). Proving (27) itself requires the Cesàro convergence and the identity , which rest on Blackwell's Lemma 1 about Markov matrices.
The development builds on the published Lean model of Blackwell (1962): Model (states St, actions Act, incomes, transition law), Policy (indexed from , so π 0 is ), Qn, V, IsNearlyOptimal (= 1-optimal), limitMatrix, and the closed forms x, y. Conventions:
limitMatrix uses terms rather than Veinott's ; the limit is the same.The shared module defines and ; this chunk defines . Contributions are welcome for any milestone, and in particular for reusable lemmas about Cesàro means of powers of a Markov matrix, which the proofs of (27) and (28) and Blackwell's Lemma 1 share.
Assembly systems — components purchased from outside, assembled into subassemblies, and those into an end product facing random customer demand — are the standard model of material requirements planning under uncertainty. Rosling's paper (Oper. Res. 37(4), 1989) shows that, under a cost assumption, the optimal policies of such a system are those of an equivalent series system, so that the Clark–Scarf decomposition of serial systems (Clark and Scarf, 1960) applies to assembly systems.
The cost assumption of the main results requires every echelon holding cost to be positive. In §4 Rosling replaces it by a weaker Generalized Assumption (GA), which allows some echelon holding costs to be negative, and then argues with Theorem 4 that GA "covers all cases of practical interest for a long-run analysis". Part (i) of Theorem 4 is the first step of that argument: when GA(i) fails strictly for some item, the model is degenerate, because its minimal cost is . This mission formalizes that statement.
There are items ; item is the end item. Every item has exactly one immediate successor with , and , so the items form a tree rooted at the end item. Write for the set of all successors of , for the set of all its predecessors, and for its immediate predecessors. Item has a lead time , and its total lead time is , ; the items are indexed so that .
Time runs in periods . The demands for the end item are independent, identically distributed, nonnegative, with a density and a finite mean . In period a policy chooses the echelon inventory positions after ordering as functions of the demands already observed. The position before ordering is , and the echelon stock on hand after arrivals is ; positions referring to periods before are read off given initial data . Problem P asks for a policy satisfying
that minimizes
where is the echelon holding cost of item , the backlogging cost, the installation holding cost of the end item, the discount factor and the density of the demand over periods.
The quantity of interest is the discounted echelon holding cost of item and its predecessors,
GA(i) asks it to be positive for every item.
If for some item
then the minimal cost of Problem P is unbounded below: for every real there is a feasible policy whose cost is a real number less than .
Theorem 4(i) explains why the Generalized Assumption is the natural boundary of the theory: a strict violation of GA(i) makes Problem P meaningless, since no policy is optimal and the infimum is . Together with parts (ii) and (iii) of Theorem 4 it reduces every case of interest to systems satisfying GA, for which Rosling's series-system results apply. The quantity in the condition is the natural "net value of stockpiling" of a subsystem, and the same exchange — buy more of a subsystem early and hold it forever — is the basic perturbation behind many optimality arguments for multi-echelon systems.
The result is proved in the paper, in a few lines. To our knowledge neither Theorem 4 nor the assembly model of Problem P has been machine-checked. A formalization adds a precise statement of what "the minimal cost is unbounded below" means for a stochastic infinite-horizon problem with an extended-real cost, and the definitions of the assembly model — product tree, total lead times, echelon positions, history-dependent policies, constraint (3) and objective (2) — which other statements of the same paper need.
The algebra of the cost increase is a geometric series. The work lies elsewhere. First, the one-more-unit policy must be shown feasible for every item of the subsystem in every period, including the boundary items: the successor of , whose constraint loosens, and predecessors with zero lead time. Second, the cost of a policy is an expectation of an infinite discounted sum whose terms have no sign; the cost increase can only be added to a cost that is finite, and the argument needs a feasible policy of finite cost to start from, which the paper takes for granted. Third, for the end item the extra units also change the expected backlog term of (2), which the printed display omits, so the end item needs a separate bound.
Measure.infinitePi) of a probability measure on with , Lebesgue, integrable and .In the extended reals, : a policy whose positive and negative cost parts are both infinite gets the value . The goal therefore asks for policies of real cost below every bound; a formalization that only exhibits a policy of cost would be trivially true and is ruled out. Milestone 2 is stated for , where the backlog term is unchanged.
Needed infrastructure: lower Lebesgue integrals of discounted sums under the infinite product measure, linearity of the cost under a deterministic perturbation, and the finiteness of the cost of the "never order" policy (whose decisions decrease linearly in the accumulated demand). Contributions of general lemmas on discounted costs of history-dependent policies under infinitePi are welcome and reusable.
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.
Demand for many products is not stationary: it rises and falls with the economy, the season, a product's life cycle or a customer's state. Song and Zipkin (1993) (DOI 10.1287/opre.41.2.351) model this by a world-driven demand process: an exogenous Markov chain (the "state of the world") whose current state sets the rate of a Poisson demand stream. The model contains the classical stationary inventory model as the case of one world state, and it is a standard example of a Markov-modulated decision problem in operations research.
For stationary demand with a fixed order cost, optimal policies go back to Scarf (1960) for finite horizons and Iglehart (1963) for the infinite horizon; Veinott (1966) bounded the optimal parameters by quantities computed from the one-period cost alone. This mission formalizes the extension of both results to the fluctuating-demand model (§3.2 of the paper). A companion mission treats the linear order-cost case, in which a world-dependent basestock policy is optimal.
The world is a continuous-time Markov chain on a countable set with generator , , and bounded rates. While , unit demands arrive at Poisson rate ; shortages are backlogged. An order arrives after a random lead time , independent of the world and the demand. The inventory position is on-hand stock minus backorders plus stock on order.
Costs: a fixed cost per order and a unit cost , both paid on arrival; a holding cost rate and a penalty cost rate ; a discount rate . With , the discounted costs are and . If is the demand during a lead time from world state and ,
Uniformization at a rate turns the problem into a discrete-time dynamic program with , and the myopic cost . For a terminal cost the -stage costs satisfy the recursion (10):
where if and . Throughout, Assumption 1, , holds and . The terminal cost is the optimal cost of the linear model (); its is written , and is the smallest minimizer of .
A function is -convex (Definition 2) if for all and all integers . The policy with parameters orders up to when and the world is in state , and does not order otherwise. With the smallest minimizer of and , the paper defines
Let be the smallest minimizer of and the largest with . For every the sequence has limit points; for any choice of limit points , the world-dependent policy with these parameters is optimal for the infinite-horizon discounted problem, and
Lemma 4 (uniform bounds on the iterates); Theorem 3 (-convexity of , and optimality of an rule for each -stage problem); Lemmas 5 and 6 (difference comparisons); Theorem 4 (the bounds above for every ); Theorem 5(a)–(d) (convergence of , , the property of limit points, and the optimality equation (2)).
The result shows that the classical structure survives Markov modulation of demand with an infinite world space and stochastic lead times: a stationary policy whose two parameters depend only on the current world state is optimal over the infinite horizon. The bounds of Theorem 6 locate those parameters in an interval computed from the myopic cost and the linear model alone, uniformly in the horizon.
The results are proved in the paper, except that Theorem 5 refers to Iglehart (1963) and Lemma 4 to Song's thesis. To our knowledge none of them has a machine-checked proof. A formalization would also produce reusable machinery: -convexity on the integers, the Scarf-type inductive argument with a countable world state, and the passage from finite-horizon to infinite-horizon optimality for a nonnegative-cost Markov decision process with unbounded costs.
The one-period cost is unbounded in and the world space may be infinite, so the usual contraction argument for discounted dynamic programs does not apply. Convergence of needs the uniform bound of Lemma 4. Optimality of the limit policy needs a separate argument, because a pointwise limit of rules need not exist: the parameter sequences are only known to have limit points. The lower bounds and hold only because the terminal cost is the linear model's optimal cost, which makes the difference comparisons of Lemma 6 possible; the paper notes that Lemma 6 depends on this choice of .
All definitions live in the namespace SongZipkinFluct.FixedCost. Inventory positions and order-up-to levels are integers. The demand law is defined through uniformization at rate , as an exact series representation of the Markov-modulated Poisson count, and the lead time is a probability law on independent of the rest. The standing conventions , , and are hypotheses of the model. Assumption 1 and are hypotheses of each theorem.
The iterates are defined by the recursion (10), with the minimum written as an infimum over integers . and are the suprema over , which are finite and equal the limits by Lemma 4 and Theorem 3. Every minimizer and every extremal integer (, , , , , , , , ) is passed through its defining property, never through sInf/sSup on . The goal also asserts that all of them exist, so its hypotheses can be met. A limit point of an integer sequence is a value taken infinitely often.
Optimality is over all deterministic history-dependent feasible policies and from every initial state. Costs are valued in , and a policy's cost is the supremum of its finite-horizon discounted costs in the uniformized problem (1). Restricting the comparison to or stationary policies would trivialize the goal and is ruled out. -convexity is the integer version of Definition 2, not convexity over -scalars.
Welcome contributions: -convexity calculus on , convergence of the uniformized demand series, Lemma 4, and an Iglehart-type limit argument for countable-state Markov decision processes with nonnegative costs.
A single stock of one product often serves customers of different importance: emergency and routine orders for spare parts, contract and spot customers, high- and low-priority patients for a blood bank. When stock runs low, the question is not only how much to order but how much of the remaining stock to hand to the less important customers now, and how much to hold back for more important demand that may still arrive. Stock rationing policies answer this question with critical rationing levels: demand of a class is served only while the stock stays above that class's level.
Topkis (1968) studied this problem as a finite-horizon dynamic program with demand classes, nonstationary costs and demands, and an arbitrary degree of backlogging. His Theorem 1 shows that, when each interval has either complete backlogging or none, a policy given by critical levels is optimal. This mission concerns his Theorem 3, which treats the case of complete backlogging: the critical levels of a class do not depend on what happens in the classes below it.
Timeline. Veinott (1965) considered demand classes but imposed the policy with all critical levels equal to . Topkis's 1966 report treated , partially duplicated independently by Evans (1968) and by Kaplan's 1966 report "Stock Rationing", in which, according to Topkis, the result of Theorem 3 was used implicitly. Topkis (1968) extended the analysis to classes and stated Theorem 3 explicitly.
A period is divided into intervals, indexed backwards: interval is followed by further intervals, and interval is the first. There are demand classes; class is the most important. In interval a random demand vector with law and finite means arrives; demands in different intervals are independent. Given the stock and the outstanding demand (backlog plus new demand), the decision is the vector , , of demand left unsatisfied; the stock drops to . A penalty and a holding cost are charged, and the backlog carried into the next interval is , with for complete backlogging. At the end of the period a salvage cost is charged.
The standing assumptions are: convex and continuous on ; convex and continuous on ; convex and continuous on with ; and . The minimal expected cost satisfies the recursion (1):
With the -th unit vector, the critical rationing level is if is strictly decreasing on , and is the smallest minimizer of that function on otherwise. denotes a right derivative.
Assume and that the demands of different classes are independent in each interval. Fix a class . Then for two instances of the model that differ only in the penalties of the classes and in the demand distributions of the classes ,
(a) the marginal quantities
coincide, and
(b) the critical rationing levels coincide.
The result. Theorem 3 reduces the size of the problem. Under complete backlogging, class 1 demand does not influence any critical rationing level, and the class- critical levels can be found from a problem with only the classes , with a degenerate demand distribution for class . Since computing the levels requires tabulating functions of several variables, which Topkis calls prohibitive for large , this is the observation that makes the levels of the most important classes computable.
Formalizing it. The theorem is proved in the paper by a short sketch that points to two case formulas, (16) and (17), to Theorem 1 (c), and to an interchange of expectation and right derivative. A machine-checked proof would supply the induction, the case analysis and the interchange in full. No formalization of any part of Topkis's paper is known: the result is proved on paper, not formalized.
The obvious argument is an induction on showing that itself does not depend on the lower classes. It fails: does depend on the penalties and demands of every class, since lower-class demand is still served and penalized. Only certain directional derivatives are invariant, and these derivatives depend on the critical levels of every class and on the optimal rationing decision, which themselves change from one instance to the other unless the invariance is already known for the previous interval. The derivatives are one-sided, may be at the boundary, and must be passed through an expectation.
The Lean development, in namespace TopkisRation.Backlog, fixes these conventions:
Fin n (class of the paper is index ); intervals are natural numbers counted backwards; vectors are ordered pointwise;sInf for the infimum and the Bochner integral for , and every statement restricts to , ;sInf;"Does not depend on" is stated with two instances , that agree on every datum the conclusion uses except the freed ones: the same , , , the same and the same for in intervals , and the same class- marginal law for in every interval. The penalty of class itself is not freed. Data of intervals beyond and the ordering cost are unconstrained. Part (b) is stated for arbitrary critical levels of the two instances; existence of critical levels is part of the paper's §1 and is not assumed away, so (b) is not vacuous. The goal does not assume the p. 173 claim, the case formulas (16)–(17), or Theorem 1. Encoding "does not depend" as "is a function of the remaining data" is ruled out.
Needed infrastructure: one-sided derivatives of convex functions and their monotone limits, interchange of right derivative and expectation for convex integrands, and the convexity and rationing-policy results of §1 (Theorem 1, Lemma 2). These are reusable for the other missions of this series. Contributions welcome: proofs of the milestones, a formal version of (16)–(17), and the existence of critical levels.
Many decision problems under uncertainty take the form of minimizing an expected cost over a convex feasible set, where is a random parameter whose distribution can be sampled but not integrated in closed form. Evaluating even approximately can cost exponentially many evaluations of in the dimension of , so the classical deterministic notion of an approximate solution is unusable. A practical alternative, going back to Nemirovski and Yudin, asks for a random output whose expected objective value is close to the optimum: . Stochastic subgradient methods achieve this; Nesterov's paper Primal-dual subgradient methods for convex problems (Math. Program. 120 (2009)) shows that the same guarantee holds for a stochastic version of his method of simple dual averages, a scheme that aggregates all past subgradients in the dual space instead of taking projected steps with decreasing step sizes.
Dual averaging has since become a standard tool in stochastic and online convex optimization (regularized dual averaging, AdaGrad's primal-dual variant, distributed dual averaging). Section 6 of Nesterov's paper is the original statement of its expected-accuracy guarantee.
Let be a finite-dimensional real vector space with an arbitrary norm and dual space with dual norm . Let be closed and convex, and let be a prox-function of : continuous on and strongly convex on with convexity parameter ,
with prox-center and . For and the point is well defined. The scalar sequence is given by and for .
The stochastic problem is given by a probability space and a cost with well defined on , and a minimizer of over with . Assumption 1: each is convex on . Assumption 2: a stochastic oracle returns a subgradient of at , and for all , .
The method of stochastic simple averages (SSA, (6.3)) fixes , starts from and , and for draws a fresh independent sample and sets
Its deterministic counterpart, the method of simple dual averages (SDA, (2.21)), is the same recursion with arbitrary answers in place of . The quality of the points is measured by the gap . Write and for the expectation over these independent samples.
For every ,
Theorem 7 gives an explicit, non-asymptotic bound on the expected optimality gap of the averaged SSA point. Since , the bound is , the optimal rate for nonsmooth stochastic convex optimization with bounded subgradients. Two features distinguish it from the classical stochastic subgradient bound: it holds in an arbitrary norm with a non-Euclidean prox-function (for example the entropy on the simplex with the norm), and the feasible set need not be bounded, since only enters. The constant is explicit and can be tuned to .
The result is proved in the paper; to our knowledge no machine-checked proof of Theorem 7 or of the dual averaging bounds of the paper exists. A formalization yields a reusable verified analysis of dual averaging in a general normed space, a template for expectation bounds over i.i.d. sample paths of an adaptive algorithm, and checked constants.
The pathwise part is a consequence of the deterministic Theorem 2, which itself rests on the general Dual Averaging bound (the companion mission's Theorem 1) and on the strong convexity estimates for . The probabilistic part looks routine on paper but is where formal arguments break: the iterate is a function of , and the identity requires measurability of the whole run and a Fubini argument on the product space. Measurability of the run in turn depends on continuity of the argmin map , and integrability of and of the gap is not assumed but must be derived from the uniform bound and the boundedness of the iterates. Pathwise bounds alone do not suffice: (6.5) controls the gap on each sample, not .
Theorem numbers and page numbers refer to source.pdf, the author's revised CORE discussion-paper version (September 2005) of the Math. Program. article; printed pages equal PDF pages.
StrongDual ℝ E with the operator norm, and is s x. Strong convexity is Mathlib's StrongConvexOn Q σ d, which is exactly (1.8); .ℝ → StrongDual ℝ E → E with the hypothesis that lies in and minimizes for every ; no choice function is used.A complete development needs the deterministic dual averaging analysis (Lemma 1, Lemma 2, Theorem 1 of the paper, restated here only through Theorem 2), measurability and continuity of , and Fubini on finite products of probability spaces. The dual averaging lemmas and the product-measure lemmas for adaptive sample paths are reusable beyond this mission. Proofs of any milestone, and supporting lemmas on measurability of the SSA run, are welcome.
A firm that holds a single stock of one product often faces demand from several classes of customers that differ in importance: emergency and routine orders for spare parts, contract and spot customers, high- and low-priority users of a military supply system. When stock runs low it can pay to refuse a less important demand now in order to keep stock for a more important demand that may arrive later. Veinott (Operations Research 13 (1965), 761–778) studied a dynamic inventory model with several demand classes but required the specific policy that serves every class whenever stock is available. Topkis (Management Science 15 (1968), 160–176) treated the dynamic version, in which demands arrive over the intervals of a period between two procurements, and showed that the optimal rationing policy has a simple form described by one critical rationing level per class and interval.
This mission concerns how those critical levels move over time. The paper's Theorem 2 gives a condition under which, without backlogging, the levels are monotone in the interval index, so that rationing is at least as strict early in the period as late in it. It is the second of four missions on the paper; the first establishes the critical-level policy itself (Theorem 1).
A period is divided into intervals, indexed backwards: interval has intervals after it, so interval is the first and interval 1 the last. There are demand classes, class the most important. At the start of interval the demand vector is observed; demands of different intervals are independent, and each class has a finite mean. With backlog and stock , one decides the vector of outstanding demand left unsatisfied, , using units of stock, so the stock at the end of the interval is . A fraction of the unsatisfied demand is carried as backlog into the next interval: is complete backlogging, none.
The costs are a penalty with (Assumption (C)), a holding cost continuous and convex on (Assumption (A)), and a salvage cost at the end of the period, with , convex and continuous and bounded below (Assumption (B)). Here denotes the right derivative. The optimal costs satisfy the recursion (1)
with .
With the -th unit vector, the critical rationing level is if is strictly decreasing on , and the smallest minimizer of on otherwise. Under the paper's Theorem 1 the rationing level policy , with , is optimal: class is served from stock only while the stock stays at or above .
Let , , , and for . If
The result says that, in intervals without backlogging, the stock reserved against a class is never larger late in the period than early in it, provided the class's penalty in the earlier interval plus the eventual marginal holding cost does not exceed its penalty in the later interval. Together with Theorem 1 it reduces the dynamic rationing problem to a family of one-dimensional critical numbers with a known order in both the class and the time index. The paper's example on p. 170 shows that the analogous monotonicity fails with backlogging, so the hypothesis is essential.
The paper's proofs are complete but informal: they interchange expectation and right-derivative limits, and rest on Lemma 2 (convexity and attainment) and Theorem 1 (c). No part of this paper has been machine-checked. This mission produces formal statements of Theorem 2 and the three lemmas it rests on; contributions that formalize the known proofs, or that settle whether the extra hypothesis on earlier backlogging fractions (below) can be dropped, are equally in scope.
The central difficulty is Lemma 7, the comparison of the marginal value of stock in two consecutive intervals. The value functions are defined through an infimum and an expectation, so they are convex but not differentiable, and the minimizer in (1) changes regime each time the stock crosses a critical level; differentiating (1) directly is not available. Right derivatives may also be at , and statements about them have to survive an interchange of expectation and a one-sided limit. The lemma depends on the optimal policy of Theorem 1, which is the subject of the first mission of this series. The claim of Lemma 7 is false when and (p. 168), so no argument can ignore the case split.
Fin n (paper class is index ); intervals are natural numbers counted backwards; vectors are Fin n → ℝ with the pointwise order.sInf and the Bochner integral, and every statement restricts to , , where the paper's Lemma 2 (proved in the first mission of the series) makes the infimum finite and attained and the integrand integrable.derivWithin, which would return where the right derivative is . Sums of right derivatives are taken in EReal.Model.Standing; (B)'s limit condition is read as " is bounded below".WithTop ℝ satisfying the defining predicate (strictly decreasing ⇒ , otherwise the smallest minimizer); the theorem holds for any such choice. Their existence is a milestone of the first mission; a sanity check exhibits a model in which all hypotheses of Theorem 2 hold with .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 is a walk whose step probabilities are sampled once at each site and then reused whenever the walk returns there. Repeated visits therefore reveal the same local bias instead of drawing a fresh probability. This makes the walk different from an ordinary random walk with a single averaged step probability. Solomon's 1975 paper asks how the random environment changes the long-run direction and speed of a one-dimensional nearest-neighbor walk. Its Section 1 gives the speed law and the associated limits for first passage times. These results distinguish escape at a nonzero linear rate from escape or recurrence at zero linear rate. Solomon (1975)
The question matters whenever a particle repeatedly crosses the same heterogeneous medium. Averaging the local right-step probabilities predicts the drift of a homogeneous comparison walk, but it does not generally predict the speed in the sampled medium. Sites with a small right-step probability can hold up the walk through repeated excursions. The formula in Theorem (1.16) quantifies this effect using a moment of the ratio of left-step to right-step probability. Solomon (1975), pp. 7–8
An environment is a sequence of numbers in . In a fixed environment, a walk at site moves to with probability and to with probability . It starts at . For the random environment, the variables are independent and identically distributed. First the environment is sampled; then the walk moves according to the fixed probabilities at its sites. The probability law that averages over both choices is the annealed law . The mission's model records this law through every finite path cylinder, jointly with every measurable event concerning the environment. Solomon (1975), pp. 1–2
Write for the ratio of leftward to rightward probability. At the endpoints, when and when . Let and ; either may be infinite. For an integer site , the passage time is the first positive time at which visits , with if the site is never reached; put . The positive ladder times are where the passage times are finite. Their joint sequence, rather than individual identically distributed variables alone, is relevant to the speed law. Solomon (1975), pp. 5–7
The goal is the complete three-case statement of Theorem (1.16). All limits below hold almost surely. If , then
If , the symmetric limits are
In the remaining case, , both normalized passage times tend to infinity and tends to zero. The reciprocal inequality is understood in the extended nonnegative reals, including . The milestone list follows the paper's supporting statements: a transience observation, a fixed-environment mean passage-time identity, a separated-block independence lemma, stationarity and ergodicity of ladder times, and the annealed mean ladder-time formula. Solomon (1975), pp. 3, 5–7
The theorem gives a numerical asymptotic speed in either direction when the corresponding ratio has mean below one. It also identifies a zero-speed regime through explicit conditions on the two reciprocal moments. The passage-time clauses say more than the final speed alone: they describe the time required to reach distant positive and negative sites and distinguish a finite linear time scale from an infinite one. The same section compares the speed with that of a homogeneous walk obtained by replacing every local probability with ; the random environment can slow the walk. Solomon (1975), pp. 7–8
Solomon proved these results in 1975. This mission asks for machine-checked proofs of the known statements and a reusable Lean description of the annealed nearest-neighbor model. The fixed-environment chain, first passage times, and the shift law of a sequence of ladder times are useful interfaces for further formal work on random media. No proof of these draft statements is claimed by the mission proposal. Solomon (1975)
The direct attempt to apply an ordinary law of large numbers to the step increments does not fit the model: those increments are not strictly stationary in a nonconstant environment. The walk revisits previously sampled site probabilities, so a later increment depends on the path's history through the sites it has encountered. The paper points out this obstruction before introducing ladder times. An additional issue is that a passage time need not be finite, and the means and may also be infinite. Any argument that converts these quantities to ordinary real numbers too early loses the zero-speed cases. Solomon (1975), pp. 5, 7
Lean represents sites by and time indices by . A probability space carries the jointly sampled environment and path. The environment lies in pointwise and is independent and identically distributed across all integer sites. The path law is fixed by its joint finite-dimensional cylinder probabilities, which express the annealed construction from the paper. In particular, the path cannot be chosen independently of the environment merely because its one-step marginal probabilities look right. This rules out a trivializing model that forgets the dependence between the sampled medium and the walk.
The ratios , their reciprocal and their expectations take values in . Passage times take values in , and normalized passage-time limits are expressed in extended nonnegative reals. The position ratio has a real limit. The theorem permits both endpoint probabilities, and , and imposes no nondegeneracy assumption. Each convergence statement is almost sure. The ergodicity milestone concerns the full joint law of the sequence under the left shift; shift preservation supplies strict stationarity. Solomon (1975), pp. 1–2, 5–7
A complete development needs measure-theoretic probability, the fixed-environment chain and annealed cylinder law, extended-valued integration and first passage times, and ergodic theory for the ladder-time shift. The model and passage-time interfaces can be reused in later one-dimensional random-environment results. Contributions proving the listed milestones, sharpening their interfaces without changing their meaning, or supplying general probability lemmas used by the known proof are within scope.
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.
Robertson and Seymour introduced tangles in Graph Minors. X (J. Combin. Theory Ser. B 52 (1991) 153–190) as the precise obstruction to tree-decompositions of small width: a graph has a tangle of large order exactly when it has no tree-decomposition of small width. A tangle points to a highly connected region of a graph without naming its vertices, by designating for every low-order separation which side is the "small" one. Large grids, large clique minors and surface embeddings with high representativity all induce tangles.
A graph usually contains several such regions. The structure theory of the Graph Minors series needs to look at all of them at once: to decompose a graph along a tree so that each highly connected region sits at its own node, and any two regions are separated as cheaply as possible. Section 10 of the paper provides that decomposition, and its later versions ("tree of tangles" theorems) have become a standard tool in structural graph theory, in matroid theory and in abstract separation systems (see Diestel, Hundertmark and Lemanczyk, Profiles of separations: in graphs, matroids and beyond, Combinatorica 39 (2019), and Carmesin, Diestel, Hundertmark and Stein, Connectivity and tree structure in finite graphs, Combinatorica 34 (2014)). This mission formalizes the original 1991 statement for hypergraphs.
A hypergraph has a finite vertex set , a finite edge set and an incidence relation; an edge may have any number of ends. A subhypergraph is given by a vertex set and an edge set, closed under taking ends of its edges; , , act on both sets. A separation is a pair of subhypergraphs with and ; its order is .
A tangle of order is a set of separations of order such that (i) of every separation of order , one of , is in ; (ii) no three members of satisfy ; (iii) for . Two tangles are indistinguishable if one contains the other, and a separation distinguishes from if and .
A tree-decomposition assigns a subhypergraph to each node of a tree , so that the cover , are pairwise edge-disjoint, and whenever lies on the path from to . An edge of , with components of , makes the separations and , where . Two separations cross unless one of four nestings holds ( and , or the analogous three); a set of separations is laminar if no two members cross.
A tie-breaker maps separations into a linearly ordered set so that (i) exactly when or ; (ii) or ; (iii) separations of smaller order get smaller -order. Given , the -distinction is the separation of minimum -order distinguishing from . A separation is -robust if for every separation of the hypergraph , one of , has -order at least , and doubly -robust if is -robust too.
Let , , be mutually distinguishable tangles in (each with its own order) and a tie-breaker. Then there is a tree-decomposition with such that
and (ii) for , each edge of the – path in whose separations have the smallest -order on that path makes the - and -distinctions, the first with 's side first.
The theorem gives a single decomposition for all tangles at once: any family of pairwise distinguishable tangles is displayed by a single tree-decomposition, with each tangle "living" at its own node (property (i)) and every pair separated by its cheapest distinction (property (ii)). The paper derives from it that a hypergraph has at most maximal tangles ((10.4), p. 184), and Section 11 uses the same machinery to build tree-decompositions whose pieces "almost" carry a local structure, a step used in the later Graph Minors papers.
None of these statements is formalized in any proof assistant as far as a search of the Prove2Me library shows; the platform has simple-graph tree-decompositions with vertex bags (from Graph Minors V), which are a different object from the hypergraph tree-decompositions here. The mission produces machine-checked statements of the tangle-tree theorem in its original hypergraph form, together with the lemma chain the authors use. The remaining work is a formal proof of each item; (9.1) is "left to the reader" in the paper and therefore needs an argument written from scratch.
The naive approach takes, for every pair of tangles, a separation of minimum order distinguishing them, and tries to arrange these separations in a tree. That fails: minimum-order distinguishing separations for different pairs may cross, and no tree-decomposition makes two crossing separations. Ties among minimum-order separations must be broken consistently across all pairs at once, and even a laminar family of distinctions does not obviously yield a tree whose nodes correspond one-to-one to the tangles, as property (i) and demand.
V, E; every theorem assumes [Finite V] [Finite E] (the paper's "all hypergraphs in this paper are finite", p. 154). Subhypergraphs are pairs of a vertex set and an edge set closed under ends.IsTangle G θ 𝒯 includes . In (10.3) the tangles have independent orders .SimpleGraph on Fin n that is a tree. In the goal, node is , which encodes with the distinct; the hypothesis is the paper's.Two-stage stochastic programming with recourse models a decision taken in two steps: a first-stage decision is fixed before a random outcome is observed, and a recourse decision is taken afterwards, once is known. The model goes back to Dantzig (1955) and Beale (1955) and is the basic template of stochastic optimization in operations research: capacity planning before demand is known, production before prices are revealed, reservoir management before inflows are observed.
When the outcome space is not finite, the recourse is a function , and the problem must specify the class of functions it ranges over. Rockafellar and Wets (Pacific J. Math. 62 (1976) 173–195) develop the duality theory of the convex case with recourse functions that are measurable and essentially bounded (), the setting in which the dual multipliers and their interpretation as prices become available. Their §3 asks whether that restriction loses anything: whether minimizing over recourses gives the same first-stage problem as minimizing, scenario by scenario, the best attainable second-stage cost.
Let be a probability space. The data are closed convex nonempty sets , , finite convex functions on (), and functions , (), finite and jointly convex in for each , and measurable in for each , summable for and bounded for . These are the paper's standing assumptions.
With , the essential objective of the problem is
where if and for all , and otherwise, and if and for all , and otherwise. Integrals of extended-real functions follow the paper's convention (2.4): the ordinary integral (real or ) when the integrand is majorized by a summable function, and otherwise.
Two first-stage problems are compared:
The hypothesis of the general result uses , the Euclidean distance from the origin to the feasible recourses ( if there are none), and calls intrinsically feasible when . A normal convex integrand on is lower semicontinuous, convex and proper in for each , with a measurability condition given by a sequence of measurable functions dense in each .
If is bounded, then for every
the two first-stage problems have the same minimizers, and the infimum over is attained for each .
If is essentially bounded for every intrinsically feasible , then for all , , and the minimizers coincide. Boundedness of is a special case of this hypothesis.
The Corollary of Theorem 2 (p. 188), that minimizes iff some minimizes , is included as a further statement.
The theorem justifies the modelling choice behind the paper's duality theory: when the second-stage constraint set is bounded, restricting recourse to essentially bounded measurable functions changes neither the optimal value nor the optimal first-stage decisions, and an optimal recourse function exists for every first stage. The duality theory of the companion mission (Theorem 3 of the same paper) is developed in that setting, so the two results together describe the problem completely in the bounded case. Proposition 1, the interchange of infimum and integral for normal integrands, is a basic tool of stochastic programming and of the calculus of variations, used well beyond this paper.
The results are proved in the 1976 paper, relying on Rockafellar's earlier work on normal integrands and measurable selections. None of them has a machine-checked proof. Mathlib has the Lebesgue and Bochner integrals, spaces and the measurable-selection prerequisites in partial form; it has no normal integrands, no extended-real integral convention of this kind, and no interchange theorem. A formal development produces those as reusable components.
The inequality is immediate. The reverse inequality requires, from the pointwise infima , a single recourse function that is measurable, essentially bounded and nearly optimal in almost every scenario. Choosing a near-minimizer separately for each gives no measurability at all: the content is a measurable choice, and that needs the normality of and the measurability of the multifunctions of feasible and of optimal recourses. Essential boundedness is a second, independent obstacle: without a bound on every feasible recourse may be unbounded, and the infimum over can then exceed . Attainment in Theorem 2 needs, in addition, compactness of the argmin sets, which comes from the boundedness of and lower semicontinuity.
is Fin n → ℝ; indices are Fin m; and are Mathlib's Lp (Fin n → ℝ) p σ, so recourse functions are almost-everywhere classes and the second-stage constraints hold almost surely. is a probability measure in every theorem. All extended-real quantities (, , , , , , , , , ) take values in EReal, and every infimum is the complete-lattice infimum, so an empty infimum is . The integral convention (2.4) is the published definition DupacovaWets.Consistency.expect: when the positive part has infinite integral (for a measurable function, exactly when it has no summable majorant), and otherwise the difference of the lower Lebesgue integrals of the positive and negative parts. in is the Euclidean length, not the sup norm. "Gives the minimum" is "has value the value at every point". Measurability of a multifunction is the published definition DupacovaWets.Consistency.IsMeasurableMultifunction ( measurable for every closed ). The standing assumptions are fields of the structure Problem.
The integral of an extended-real function must not be replaced by a Bochner integral of its real part, which would turn values into and make meaningless; and the infima must not be real sInf, which returns on unbounded sets.
Reusable beyond this mission: the notion of a normal convex integrand on a finite-dimensional space, and Proposition 1. Contributions of measurable-selection infrastructure (Kuratowski–Ryll-Nardzewski type theorems, measurability of distance functions of closed-valued multifunctions) are welcome as supporting lemmas. The mission "Stochastic Convex Programming: Basic Duality 1" formalizes the duality theorem of the same paper on the same model.
Burn-in is the final reliability test of integrated circuits: boards loaded with chips are held in an oven at elevated temperature for a minimum specified time, so that marginal devices fail before shipment. An oven holds several boards at once, and a load may stay in the oven longer than its specification but never shorter. Lee, Uzsoy and Martin-Vega (Oper. Res. 40(4), 1992) model such an oven as a batch processing machine and study the resulting scheduling problems. Burn-in is often the bottleneck of the test stage, which is why throughput (makespan) and due-date performance on several ovens in parallel are of practical interest.
This mission covers the paper's makespan result for parallel ovens. On ordinary identical parallel machines, Graham (SIAM J. Appl. Math. 17, 1969) proved that the LPT rule (list the jobs longest first and give each to the machine that frees up first) has worst-case ratio on machines. The paper shows that the same factor holds for batch machines once the jobs are first grouped into full batches of the longest jobs.
There are jobs with processing times , all available at time , and identical batch processing machines. Each machine processes up to jobs at the same time. A batch is a set of at most jobs processed together; once started it cannot be interrupted or joined, and its batch time is that of its longest job,
A schedule forms the jobs into disjoint nonempty batches covering all jobs, assigns each batch to a machine, and runs every machine's batches back to back from time . The makespan is the largest machine load, the total batch time on a machine. The problem of minimizing it is written , and denotes its optimal value, over every way of forming batches (any sizes up to , any grouping) and every assignment. For it is the classical problem .
Algorithm BLPT.
is the resulting makespan.
For the optional lateness result, each job also has a due date . The maximum lateness of a schedule is , is its value under BLPT, its optimum and .
It is claimed for every run of BLPT, whatever order the algorithm gives to equal processing times and equal batch times.
Proposition 3 gives a constant-factor guarantee for a strongly NP-hard problem. The guarantee does not depend on , whereas arbitrary batch list scheduling only gets (Proposition 1 of the same paper). For one machine the factor is , so BLPT is then exact. Proposition 2 is a structural statement: it fixes the batch composition of an optimal schedule before any assignment decision. It turns the batch problem into an ordinary parallel-machine problem, so other results for transfer as well. Proposition 5 carries the guarantee over to maximum lateness, measured relative to because may be negative.
All results are proved in the paper, Proposition 3 by a one-line appeal to Proposition 2 and Graham. This mission produces machine-checked versions of the reduction and the bound. Graham's LPT bound itself is not formalized anywhere on the platform. Its proof here is a reusable result about the published list-scheduling definitions, independent of batching.
The obvious argument is "batch as in Step 1, then apply Graham". It has two gaps. First, ranges over all batchings, and an optimal schedule need not use full batches or consecutive jobs. The exchange argument behind Proposition 2 has to move jobs between batches, possibly on different machines, without increasing any machine's load. Ties among equal processing times also have to be handled, since the claim is made for every longest-first ranking. Second, Graham's bound is not on the platform and has to be proved. It is a finite combinatorial statement, but its known proofs are not short. Proposition 5 additionally needs the bound for sub-instances formed by a prefix of the batches.
Jobs are Fin n, 0-based. Processing times are real, p : Fin n → ℝ with 0 < p j; due dates (Proposition 5 only) are d : Fin n → ℝ with 0 ≤ d j. A batching is a list of nonempty, pairwise disjoint Finsets of size at most B covering every job. The batch time is the maximum of p over the batch.
Machine loads, assignments, the per-batching optimum and list scheduling reuse the published definitions NumStochOpt.ListScheduling.ListSchedule (firstAvailable, lsLoads, listMakespan) and NumStochOpt.ListScheduling.Makespan (machineLoad, makespan, optMakespan) from the Rinnooy Kan–Stougie mission, applied to the sequence of batch times (padded with zeros beyond the last batch, which these definitions never read). is the infimum of optMakespan over all valid batchings, never only over the consecutive ones of Step 1, which would assume Proposition 2.
Explicit readings of the paper's phrases:
p;List.toChunks B of that list;Proposition 5 adds the hypothesis , which the paper's proof uses but does not print. It also makes positive, so the printed ratios are well defined. Running times and the paper's other algorithms are out of scope.
A statement with restricted to consecutive batches, a sorry-free bound obtained from a degenerate or empty-job reading, or a BLPT fixed to one convenient tie-break would trivialize or weaken the goal and is ruled out by the statements as posed. Welcome contributions: Graham's LPT bound on the published list-scheduling definitions (reusable for any work), the exchange lemma behind Proposition 2, and the permutation invariance of optMakespan under reordering of items.
Multistage decision problems under uncertainty are often modelled by a finite set of scenarios: each scenario fixes one possible future, and for it a deterministic problem can be solved. What makes the problem stochastic is the requirement that decisions may depend only on information available at the time they are taken. Rockafellar and Wets (WP-87-119, 1987; journal version Math. Oper. Res. 16 (1991) 119–147) proposed the progressive hedging algorithm, which solves the scenario problems separately with a penalty and a price term and blends their solutions step by step into a single policy that respects the information constraints. The method is a standard decomposition scheme of stochastic programming and is implemented in solver libraries such as PySP and mpi-sppy.
For convex problems the paper proves convergence through the theory of the proximal point algorithm. Many practical scenario models are not convex (integer-like penalties, nonconvex costs). For that case the paper proves one result, Theorem 6.1: the algorithm cannot be expected to find a global minimum, but whenever it converges, its limit is a stationary point. This mission formalizes that result.
Let be a finite set of scenarios with probabilities , . A decision is a vector , split into blocks taken at times . For each scenario there is a scenario subproblem
Throughout, every is nonempty and closed, every is locally Lipschitz, and the sets are bounded.
A policy is a map . Policies form a space with inner product and norm . For each time the scenarios are partitioned into bundles of scenarios indistinguishable at time . A policy is implementable, , when each is constant on every bundle of ; it is admissible, , when for all . The aggregation operator replaces by its conditional expectation over the bundle of ; , and . With the problem is
Progressive hedging with parameter keeps and . It sets , computes for every from
and updates . In the nonconvex case, is only required to be -locally optimal: optimal among the points of within Euclidean distance of it, for a fixed .
denotes Clarke's generalized gradient of a locally Lipschitz and Clarke's normal cone to a closed set .
If and , then , and
moreover is a local minimizer of , which is (P) with replaced by , and .
Theorem 6.1 is the paper's only guarantee outside convexity. It says that progressive hedging, run with local solvers on nonconvex scenario subproblems, cannot converge to a point that fails the first-order conditions, and that the limiting price system is a Lagrange multiplier for the nonanticipativity constraint . It needs no constraint qualification, unlike the general necessary condition of Theorem 4.1: the multiplier is produced by the algorithm. This is the basis for using progressive hedging as a heuristic for nonconvex and mixed-integer stochastic programs.
The result is proved in the paper; to our knowledge it has not been machine-checked. A complete formalization would give checked statements of the scenario model (, , , with the weighted inner product), of the algorithm with inexact local subproblem solutions, and of Clarke's optimality conditions for problems with separable structure. The convex convergence theory of the same paper is the subject of the companion mission Scenarios and Policy Aggregation in Optimization Under Uncertainty 1.
The local optimality of is relative to a ball centred at the iterate, which moves. Passing to the limit requires a radius that is uniform in and in the norm of ; this is what provides, and it only covers points strictly inside the limiting ball: a point of at distance exactly from may lie outside every ball around the iterates. The step from local optimality to the multiplier condition uses Clarke's necessary condition for minimization over a closed set and the sum rule for a Lipschitz function plus a smooth one; neither is in Mathlib. Theorem 4.1 needs, in addition, a calculus rule for normal cones of an intersection under a qualification condition, and the transfer of Clarke's objects between with the weighted inner product and the individual scenario spaces.
is EuclideanSpace ℝ (Fin n). A policy is a function S → EuclideanSpace ℝ (Fin n). The weighted inner product and norm of are explicit definitions (ip, pnorm); Lean's built-in norm on policies (the sup norm) is used only for topological notions: convergence of the iterates and "locally optimal" without a radius, which do not depend on the norm. The radii are in the weighted norm, the radius in the Euclidean norm of . Time blocks are a monotone map from coordinates to periods; bundles are the classes of a setoid on for each period. The standing assumptions are fields of the model structure, so every theorem carries them. Indices are 0-based and sequences are indexed by ; the run starts from and . Theorem 4.1 is stated in its decomposed form (4.4), scenario by scenario.
Clarke's generalized gradient and normal cone are the published platform definitions ClarkeGradients.Shared.generalizedGradient (convex hull of limits of gradients) and ClarkeGradients.FlowInvariance.normalCone (closure of the cone generated by the generalized gradient of the distance function); for locally Lipschitz functions and closed nonempty sets these are the objects the paper uses.
Formalizations that trivialize the statement are excluded: Theorem 6.1 carries no convexity hypothesis and no constraint qualification, the -balls are not measured in the sup norm, and the run predicate is satisfiable (the model files come with a sanity check exhibiting a run).
Useful infrastructure, reusable beyond this mission: Clarke's necessary condition for local minimization of a Lipschitz function over a closed set, the sum rule with a function, products of normal cones, and basic facts about (an orthogonal projection onto for the weighted inner product). Contributions of any of these are welcome.
Semiconductor burn-in tests hold several jobs in an oven at once. A production planner must decide which jobs share each oven run and in what order those runs take place. A job may become available only after earlier manufacturing steps, and a due date marks when its test should finish. The planning objective here is to minimize how many jobs finish after their due dates. Lee, Uzsoy, and Martin-Vega studied this batch scheduling problem and gave a dynamic program for the case of equal processing times and compatible release and due-date orders (Lee, Uzsoy, and Martin-Vega 1992, §4, pp. 770–771).
There are jobs and one batch processing machine with capacity . Job has release time , due date , and processing time . In the main problem every processing time equals a common value . A batch is a nonempty set of at most jobs. Its processing time is the longest processing time among its members; it begins only after all its jobs have been released and the previous batch has finished. Processing is uninterrupted. A schedule is an ordered list of disjoint batches that covers every job. Each batch starts at the earliest time allowed by these conditions.
The completion time of job in schedule is the completion time of its batch. A job is on time when and tardy when . Write and let be the minimum of over all valid complete batch schedules. Tardy jobs still belong to a schedule and consume machine time. An on-time batch is one whose every member is on time.
For the structural lemmas, agreeable release times and due dates mean that implies . For the dynamic program, jobs are indexed so that both and are nondecreasing. A batch is in batch-EDD order relative to later batches when no job in it has a later due date than a job in a later batch. A batch of consecutive jobs contains exactly an index interval. These are the paper's Lemmas 4 and 5 and Definition 1 (pp. 767, 770).
Lemma 4 asserts that some optimum has an initial list of wholly on-time batches in batch-EDD order, followed by batches containing only tardy jobs. Lemma 5 asserts that some optimum has every wholly on-time batch made of consecutive indexed jobs. These are existence statements about schedules of all jobs; neither restricts the feasible schedules over which is defined.
Let be the table defined by Algorithm DP3 for the first jobs and a selected count of on-time jobs. Its boundary values are and for . For , it takes the minimum of and the eligible transitions that append a batch of jobs, . A transition uses and is eligible when that completion time does not exceed . The main target is
The maximum includes zero, which is always feasible in the table. The printed range begins at one and has no value when every job is tardy. This is the corrected boundary reading of the displayed answer on p. 771 (source).
The paper also gives a variant for jobs available at time zero, with nondecreasing processing times and due dates. Its transition replaces the release-time maximum and common by . The corresponding correctness statement is a further milestone (p. 771).
The structural results connect the optimization over arbitrary complete batch schedules to the restricted arrangements represented by the table. DP3 correctness then identifies the number of tardy jobs from finite table entries, including instances with no on-time job. The variable-time extension covers the related case where each job has its own duration but all jobs are available together.
The paper proves these results informally; this mission leaves their Lean proofs open. A complete formalization would supply reusable definitions of batch schedules, release-limited completion times, tardy-job counts, and a finite dynamic program with an explicit infinite value. The machine-checked statements and the local instance check establish the interface for that work, while the structural and correctness theorems remain solver targets.
The objective ranges over every valid batching and every processing order. The table examines an indexed prefix and places the last on-time batch among consecutive jobs. Establishing that the table's choices preserve the full optimum requires the existence statements in Lemmas 4 and 5. Reordering jobs is delicate because delaying a batch can change release feasibility and can make an earlier on-time job late. Equal due dates also require care: a due-date order alone need not put the latest release of a proposed batch at its last index.
Jobs use Fin n, with index zero representing the paper's job 1; the table's is a prefix length. Data and completion times are natural numbers, matching the paper's integer-data setting; in the table is WithTop ℕ. The schedule model uses nonempty batches of cardinality at most , pairwise disjointness, and complete coverage. A batch starts at the maximum of its latest release and the preceding completion time. This earliest-start convention is sufficient for minimizing the regular tardy-job objective. The empty job set is included: its empty schedule has zero tardy jobs.
The strict implication makes the paper's loose “agreeable” condition precise without forcing equal due dates for tied release times. For the recurrence, both release times and due dates are nondecreasing in job index, including their ties. This ensures that is the last batch's latest release and its earliest due date. The variable-time version similarly indexes by nondecreasing processing times and due dates, so the last job gives the batch duration. The table uses a minimum over exactly the paper's range , with an empty range giving . Zero is included in the final maximum. Tardy jobs are scheduled in the underlying optimum; defining the optimum as an on-time subset or defining the table as that optimum would erase the two structural claims.
This mission covers correctness only. The paper's running-time statement and the bisection procedure are outside the formalization because they would need a specified computational cost model. The paper's FBEDD remark for this objective is also excluded: a three-job instance contradicts it. Contributions to the open theorem proofs, schedule-existence facts, and reusable batch scheduling lemmas are welcome.
A coalescent models a collection of ancestral lineages merging as time runs backward. If every event joins exactly two lineages, a single pairwise merger rate describes the finite system. Pitman’s 1999 paper asks which rates permit an event to join any number of blocks, while still giving one process on partitions of all positive integers. This matters when a sample of any finite size must be a restriction of the same population model: specifying a chain separately at every sample size is insufficient unless the chains agree when labels are removed. The paper supplies an exact answer in terms of a finite measure on the unit interval. See Pitman (1999), Theorem 1 and §3.1.
Let be the partitions of and the partitions of the positive integers. A partition records which labels belong to the same block. The map restricts a partition to . A partition refines when every block of is contained in a block of . Thus blocks can merge as time grows, but never split.
A -valued process is a coalescent here when its paths refine with time and each finite restriction has right-continuous step-function paths. For a partition of with blocks, each unordered choice of blocks, , merges into one block at rate . Different choices are different possible transitions, each with that rate; the rate is not multiplied by the number of choices. The finite chain’s generator records these transition rates, with each diagonal entry the negative sum of the other entries in its row. Its transition matrix after time is .
An array is consistent when, for every and every initial partition of , restricting the -label chain to gives the same process law as the -label chain started at the restricted partition. A finite nonnegative Borel measure on supplies a rate array through an integral. The point mass at zero is included: because for natural powers, it gives pairwise mergers while higher-order merger rates vanish. These definitions follow Pitman (1999), pp. 1871–1872 and Lemma 18.
The goal is the existence-and-rates part of Theorem 1. For every nonnegative array , a coalescent with these finite-chain merger rates exists from every if and only if there is a finite nonnegative measure on such that
The statement asks for one measure representing every rate in the infinite array, and a process from every initial partition. It fixes neither a particular measure nor a sample size. This is Theorem 1, equation (1).
The milestone list follows §3.1: adjacent-size restrictions suffice to check consistency; consistency is equivalent to
and the nonnegative normalized array relation
is equivalent to a representation for . The final milestone states the uniqueness as well as the existence of the representing measure: equation (1) is a bijection between consistent arrays and finite measures. These are the claims in Lemma 18 and its proof, p. 1882.
The characterization turns an infinite family of nonnegative rates into one finite measure, and says exactly when finite chains at different sample sizes can be restrictions of a common partition process. The bijection also makes the measure identifiable from the rates. Without consistency, a chain specified at one size can change its law when an unobserved extra label is added; there would be no single process on with those restrictions.
Pitman proved these results in 1999. The mission concerns machine-checking their statements and, eventually, their proofs. The current Lean items are open theorems with compiled statements; they do not yet have machine-checked proofs. The reusable part of a complete development would include finite partition generators, restriction of continuous-time Markov chains, and the moment representation for normalized nonnegative arrays. These tools also apply to other consistent families of random combinatorial structures.
Checking that each defines a finite-state chain does not by itself construct a process on partitions of all integers. Deleting one label can change which apparent merger occurs in the smaller chain, so the rates must satisfy a precise identity across adjacent sizes. Even once those identities hold, the conclusion requires one joint law whose finite restrictions agree for all sizes and times, with right-continuous paths. The representation step must recover a genuine finite measure, including possible mass at zero, and must prove uniqueness; a mere numerical fit for finitely many entries cannot establish the theorem.
The Lean partition type is Setoid (Fin n) at finite size and a type synonym of Setoid ℕ at infinite size. The paper’s positive labels are shifted to zero-based labels, preserving their order. The measurable structure on infinite partitions is generated by pairwise equivalence coordinates, equivalently by finite restrictions; finite partition spaces use the discrete measurable structure. The process path predicate requires refinement at every pair of ordered times and right continuity of every finite restriction. Finite-chain laws are specified at all finite collections of times through , so a process cannot qualify merely by having the right initial state or a single marginal.
The measure is represented on with zero mass outside [0,1]x^0=1x=02\le k\le b$, and the zero measure is allowed. The Fin 0 restriction is an additional tautological boundary case introduced by Lean’s natural numbers. The process sample space is a small Lean type, and the law is a probability measure on it.
Only the characterization sentence of Theorem 1 is targeted. Its later assertions about the strong Markov property, Feller semigroup, Skorohod path-space law, and weak continuity of the law map are outside this mission. Contributions toward those properties would need further path-space infrastructure. The formalized foundations and milestones can also support the paper’s Poisson construction and its later results, but those are separate targets.
Many problems of optimization and equilibrium reduce to a system of nonsmooth equations with locally Lipschitz but not differentiable: nonlinear complementarity problems written as , variational inequalities through the normal map, and Karush–Kuhn–Tucker systems of constrained programs. Newton's method in its classical form needs the Jacobian of , which does not exist at the points of interest. Two kinds of generalized Newton methods replace it: one uses an element of a generalized Jacobian, the other uses the directional derivative and solves for the step.
J.-S. Pang (Newton's method for B-differentiable equations, Math. Oper. Res. 15 (1990), doi:10.1287/moor.15.2.311) globalized the second kind with an Armijo line search on the merit function , the damped Newton method, and proved that its accumulation points are zeros of under suitable conditions. Three questions were left open: does the whole sequence converge to one point, how fast, and when does the line search accept the full step? L. Qi (Convergence analysis of some algorithms for solving nonsmooth equations, Math. Oper. Res. 18 (1993) 227–244, doi:10.1287/moor.18.1.227) answered all three in his Theorem 4.3, under semismoothness and a regularity condition on the B-subdifferential. This mission formalizes that theorem and the results it rests on.
Timeline:
Write with the Euclidean norm, and let be locally Lipschitz. The norm function is .
The directional derivative of at in direction is the one-sided limit . is B-differentiable at if exists for every and (2.1).
Let be the set where is differentiable. The B-subdifferential is the set of all limits with , (2.12). Its convex hull is Clarke's generalized Jacobian . is strongly BD-regular at if every is nonsingular. is semismooth at if over , , exists for every (2.6). The directional derivative is semicontinuous of degree 2 at if for all in a neighbourhood of (2.5).
The damped Newton method (Algorithm 4.1) fixes , , . Given with , it takes a solution of the generalized Newton equation
lets be the first nonnegative integer with
and sets , .
Take . Let be B-differentiable, let be a run of Algorithm 4.1 with for all , and let be an accumulation point of with , at which is semismooth and strongly BD-regular. Then
The goal fixes no rate constant; it asserts convergence of the whole sequence, superlinearity and the eventual unit step.
Theorem 4.3 is an attraction result: a regular zero that the damped iteration merely visits infinitely often captures the whole sequence, and from then on the method is the pure (undamped) directional Newton method with its fast local rate. Together with Pang's global theorem it gives a globally convergent method whose tail is superlinear, the standard template later followed by semismooth Newton methods for complementarity and variational inequality problems. Corollary 4.4 turns the theorem into a diagnostic: the behaviour of the step sizes decides whether a limit point solves the equation.
The theorems are proved in the paper. As far as a search of the platform shows, none of them, and no damped Newton method for B-differentiable equations, has a machine-checked proof. Formalizing them requires a reusable layer of nonsmooth analysis (directional derivatives of locally Lipschitz maps, the B-subdifferential and its local uniform invertibility) that other missions on semismooth Newton methods can import.
The local step of the obvious argument, "near the Newton step is accurate, so the Armijo test passes with ", needs two facts that are not automatic. First, the generalized Newton equation involves the nonlinear map , not a matrix; the error estimate of Corollary 3.4 goes through a representation with , together with a uniform bound on for near . Second, the Armijo test involves , whose value along a Newton direction has to be identified as . A further subtlety is global: an accumulation point only guarantees that the iterates come close to infinitely often, and the argument must show that once they are close enough they never leave, which needs the invariant ball of (4.5) and the fact that the step is exactly there.
is EuclideanSpace ℝ (Fin n) (all norms are 2-norms, as in the paper), allowed. Every statement assumes locally Lipschitz (the paper's standing assumption of §1). The B-subdifferential, semismoothness and the directional derivative are the published definitions NonsmoothNewton.Shared.bJac, NonsmoothNewton.Local.SemismoothAt and NonsmoothNewton.Local.dirDeriv. Since dirDeriv takes a default value where the limit does not exist, (3.12) is encoded as the existence of the one-sided limit with value . Nonsingularity is an explicit two-sided inverse. A run of Algorithm 4.1 records , and the minimality of ; without the minimality any would do and " eventually becomes 1" would not be the paper's claim. An accumulation point is a cluster point of the sequence; superlinear convergence is .
Added hypotheses, disclosed in each item:
The theorems are not vacuous: runs of Algorithm 4.1 exist (for the Armijo test passes at ), and a statement in which the line search index is not the first passing one, or in which is a default value, would not be the paper's theorem.
Contributions welcome: proofs of the milestones, in particular the representation and the local uniform invertibility of (Lemma 2.6), which are reusable well beyond this mission.
Workers can form groups and produce an output that they divide through salaries. A group may object to a proposed allocation when it can pay all of its members at least as much and one member more. The central question is whether any allocation survives every such objection. Kelso and Crawford's 1982 paper gives a sufficient condition based on how an imaginary firm would demand workers as their salaries change. This is useful when production depends on combinations of workers, yet there is no actual employer side to the market.
The one-sided result belongs to a seven-mission series: 1, the salary-adjustment process; 2, continuous-salary core existence; 3, this one-sided theorem; 4, firm-optimality; 5, comparative statics; 6, returns to workers; and 7, the no-core example. Each mission can be read independently. None of Kelso and Crawford's results was on Prove2Me before this series. The paper itself notes that Theorem 3 is similar in spirit to Shapley's core-existence result but logically independent: Shapley's convex-game condition concerns second differences of a characteristic function, whereas this theorem uses a condition on input demand. Kelso and Crawford, footnote 3.
Let be a finite set of workers, with . A coalition technology assigns a real output to each worker set . A one-sided allocation consists of a partition of all workers and one real salary for each worker. The parts of are disjoint and cover . Each worker has a utility that is continuous and strictly increasing in salary, so salary comparisons express the same preferences as utility comparisons.
The paper's individual rationality condition D1′ asks for nonnegative salaries and one aggregate resource constraint:
It does not require each partition block to finance its own salaries. An improving coalition is a worker set with salaries for every , a strict inequality for at least one member, and . A D1′ allocation is in the strict core D2′ when no improving coalition exists. The empty coalition cannot improve because it contains no member whose salary could rise. These are equations (12)–(15) on pages 1492–1493 of the source paper.
To state gross substitutes (GS), imagine identical firms, each with production . At a salary vector , a firm's profit from employing is ; a demanded set maximizes this profit over all worker subsets. GS says that if salaries rise coordinatewise from to , then for every demanded set at there is a demanded set at containing all workers of the old set whose salaries stayed unchanged. The requirement is over all real salary vectors, as in the continuous market of Section 2.
Assume nonnegative marginal production (MP′), no free lunch (NFL), and GS for the identical fictitious firms:
The goal is the exact existence statement
Theorem 3 appears on page 1493 of Kelso and Crawford. Its two milestones are claims from the proof: every dummy firm has zero profit at a fictitious-market strict-core allocation, and that allocation induces a one-sided strict-core allocation. Mission 2 targets the paper's Theorem 2, which supplies existence of the fictitious-market allocation; this mission does not pose a duplicate specialized version of it.
The theorem ensures that workers can be partitioned and paid without any group being able to make at least one of its members strictly better off while preserving every member's prior salary. It turns a condition on a firm's reactions to wage increases into stability of a market containing no firms. The result also identifies a concrete boundary for the core-existence argument: the paper later constructs a market without GS that has no core allocation in its two-sided setting. Kelso and Crawford, Section 6.
The theorem is proved in the 1982 paper; this mission asks for machine-checked statements and proofs of its one-sided definitions, the two transfer claims, and Theorem 3. The local Lean files compile as open statements, and a concrete one-worker instance checks that MP′, NFL and GS can hold together. That local check is not a proof of Theorem 3. The definition of GS for a finite demand problem can be reused beyond this mission, but the dummy-firm construction and the one-sided D1′–D2′ predicates follow this paper's conventions.
A strict-core allocation of a two-sided market controls coalitions containing a firm, while D2′ is expressed entirely through worker coalitions. The fictitious market has more firms than workers, which forces at least one firm to employ nobody. The proof must connect that observation to every firm's profit and then translate a one-sided improving coalition into a two-sided improvement. Individual rationality also has to preserve the paper's aggregate budget condition. Merely assigning each worker to a firm or showing nonnegative firm profits would leave these links unproved.
Workers form an arbitrary finite type; the empty case is included. The fictitious firms have type Fin (m + 1), so their count is strictly greater than the worker count even when . Salaries and output are real. In the fictitious market, every firm uses the same , each worker's utility at every firm is , and reservation salary is zero, matching unemployment utility . The milestones retain arbitrary strictly increasing continuous functions ; Theorem 3 does not quantify over them because D1′ and D2′ compare salaries directly. Theorem 3's GS condition ranges over all real salary vectors, not a discrete salary grid.
Mathlib finite partitions contain nonempty parts. The paper permits empty indexed groups, but NFL makes them contribute zero output. The allocation model assigns every worker to one firm, and strict blocking allows any worker coalition, including the empty set, although strict improvement excludes that case. D1′ uses one total salary bound; a per-group bound would change the theorem. D2′ requires a strict gain in a worker's salary, not merely slack in the production budget. No vacuous regularity condition, fixed special technology, or restriction to a single worker is part of the mission goal.
Contributions are welcome on the finite partition interface, properties of profit-maximizing demand under GS, the zero-profit claim, and the transfer from fictitious firms to worker coalitions. The shared market and demand definitions are kept in their own module so they can be consolidated with the other missions of this paper.
Two stationary random sequences can have identical distributions at each individual time while differing in their dependence across time. Comparing only their one-time marginals therefore misses a feature relevant to stochastic-process comparison. Ornstein's measures the cost of matching two whole stationary processes: it minimizes the expected discrepancy at one time over joint laws that are themselves stationary. Kamae, Krengel, and O'Brien use stochastic order to replace that optimization over pairs of processes with an optimization over a single common lower process in Theorem 8 of their 1977 paper. This mission formalizes that identity and the stationary coupling results supporting it.
A two-sided path with values in a space is a sequence . The shift sends to the path whose coordinate is . A probability law on paths is stationary, written , when . A law on pairs of paths is jointly stationary, written , when it is invariant under . Its first and second marginals are denoted and . These are the objects defined at the start of Section 8.
When has a partial order, paths are ordered coordinatewise: means for every integer . For probability laws on any such space, write if for every bounded, measurable, increasing real function . Thus stochastic order compares laws through all bounded increasing observations, including observations that depend on several time coordinates. The paper introduces this order on a partially ordered Polish space whose order graph is closed and whose measurable sets are Borel sets in Section 1.
For real-valued paths, is the value at time zero. If the time-zero values under stationary laws and are integrable, define Ornstein's distance by
The stationary constraint on is part of the definition. It asks for a matching of the full processes, even though the cost is evaluated at one coordinate. The paper notes that this formula is equivalent to Ornstein's original definition for the processes considered here on p. 910.
The ordered special case is Lemma 3: if , then
The main target is Theorem 8, equation (18). For stationary real process laws with finite first moments at time zero,
The supremum ranges over stationary laws of whole paths, ordered on the full coordinatewise path space. The milestone list includes Theorem 7's stationary monotone coupling, Lemmas 2 and 3, and three claims made inside the proof of Theorem 8: the triangle inequality , which the paper asserts without proof ("since is a distance"), the attainment of the infimum defining , and the fact that the law of the coordinatewise minimum of an optimal stationary coupling lies below both and . These are the statements from the paper that delimit the target.
The identity expresses a distance defined through stationary joint distributions using only stationary laws below both inputs in stochastic order. It therefore links a coupling cost to an order-theoretic optimization. In the ordered case, Lemma 3 evaluates the distance directly from the difference of means. The authors point out that the general formula replaces an infimum over laws on a product path space by a supremum over laws on one path space on p. 911.
The 1977 results are proved on paper; these mission statements are open Lean proof targets. A completed formalization would supply reusable definitions for stationary path laws, stationary couplings, stochastic order on path spaces, and , together with checked statements about their interaction. It would also make the closed-order and first-moment conditions explicit at every point where a subsequent result uses them. The separate mission for Theorem 1 contains the general coupling characterization that the paper invokes in Theorem 7.
The cost in inspects only time zero, but admissibility of a coupling involves every time coordinate at once. An arbitrary coupling of the time-zero marginals need not extend to a stationary coupling of the two processes. The stationary-coupling existence statement must preserve both full path marginals and the coordinatewise order. On the optimization side, taking an infimum in the real numbers is justified only after the coupling class is shown nonempty and its costs are finite; attaining the infimum requires more than those two facts. These are the obstacles made explicit by Theorem 7 and the proof of Theorem 8.
The Lean path space is , with Mathlib's product topology, Borel measurable structure, and coordinatewise order. The shift sends coordinate to the old coordinate . For Theorem 7, carries the paper's standing assumptions: it is Polish, its order is a closed partial order, and its measurable structure is Borel. Measurability of quantified functions is explicit, following the paper's convention that sets and functions under discussion are measurable. Theorem 8 and its Section 8 milestones specialize to .
The real-valued definition of takes the infimum over jointly stationary probability couplings with the specified full path marginals. Under the target's finite-first-moment hypotheses, the product coupling makes this class nonempty, every displayed cost is integrable, and costs are bounded below by zero. The goal states the supremum with an explicit finite least upper bound. It considers common lower laws with an integrable time-zero coordinate: such laws give the finite values intended by the paper, and this restriction does not remove the optimal value. These choices exclude totalized integrals and default real infima or suprema from supplying a spurious identity. Theorem 7's support condition is concentration on the closed set of ordered path pairs.
Reusable contributions include general facts about stationary measures on countable products, measurable coordinatewise order and meet maps, and stationary coupling compactness. The target specifically requires the order to test bounded increasing functions on the full path space; replacing it with a comparison of time-zero marginals would give a different claim. Likewise, dropping the joint stationarity constraint from the definition of would turn it into the Kantorovich (Wasserstein-1) distance of the time-zero marginals, a different and in general smaller quantity; the formalization keeps that constraint. The source is the published Annals of Probability version; throughout this mission printed page PDF page .
In a population divided into many species, a ranked frequency is the fraction belonging to the th most common species. The Poisson–Dirichlet distribution is a model for such random ranked frequencies. It also arises from ranked jumps of a stable subordinator, which gives the model its connection to random interval partitions. Pitman and Yor's 1997 paper develops both descriptions and studies quantities derived from the ranked sequence. Its §7.3 asks how much of the remaining total mass belongs to the th ranked component when is large. This is the chain factor , the quantity studied here. These interpretations and the result are in Pitman and Yor (1997).
For , the paper first analyzes the tail ratio under through Proposition 11 and its Laplace transform. Proposition 14 relates to that base law by a local-time density. The limiting behavior in Proposition 44 combines those two themes. The paper states both an almost-sure limit and a Gaussian fluctuation limit, but the variance printed for the latter conflicts with the variance of displayed immediately before it. The mission retains the paper's almost-sure assertion as its goal and records the corrected fluctuation assertion separately. Pitman and Yor (1997), pp. 863–865, 890–891.
Choose and . Let be independent random variables, where has the beta distribution with parameters . Its density on is for parameters . Form the stick-breaking lengths
Sort these lengths in decreasing order, retaining multiplicities. The law of the resulting sequence is , exactly Definition 1 of the paper. Pitman and Yor (1997), p. 857.
For that ranked sequence, define the tail ratio and chain factor
The distinction between and the original independent factors matters: the former is computed after ranking and is generally dependent across indices. The paper also uses the function for . It appears in the Laplace transform of . Pitman and Yor (1997), pp. 863–865, 890.
The central target is Proposition 44, display (150): for and ,
The milestones state the distribution and Laplace transform of from Proposition 11(ii), its mean , the almost-sure limit of under , and Proposition 14's change-of-measure formula. The Gaussian companion records the central limit theorem for and the corrected version of Proposition 44's display (151):
The printed variance in (151) is . It differs from the variance forced by the preceding central limit theorem: and the derivative of at give . At , the corrected and printed values are and . The verbatim milestone text preserves the paper's wording; the companion theorem discloses the correction. Pitman and Yor (1997), pp. 890–891.
Display (150) identifies the almost-sure scale of the ranked chain factor: behaves like a deterministic constant divided by . This makes the order of magnitude precise for every permitted , despite the dependence among ranked components. The companion fluctuation statement gives a distributional scale around that limit and exposes a numerical inconsistency in the printed version. Neither conclusion is simply a statement about the independent beta factors ; the paper compares the two sequences precisely because they have different limiting distributions. Pitman and Yor (1997), p. 891.
The result is proved in the paper, while its statements and their supporting definitions still need a machine-checked development. A completed formalization would make the ranked-frequency law, the tail-ratio limit, and the local-time change of measure available as separately reusable results. It would also settle the corrected variance at the level of a precise probability-law statement rather than silently adopting the paper's printed constant.
The tempting shortcut is to use Proposition 11(ii), which says that each has the law of a sum of independent copies of , and invoke a strong law. That information concerns each one-dimensional law separately; it does not exhibit the whole sequence as partial sums of a single independent sequence. Almost-sure convergence is a statement about their joint coupling, so the shortcut leaves a gap. The Gaussian conclusion raises a different issue: its limit must survive the change from to , and its variance must be consistent with the displayed variance of . These are the two substantive tasks beyond the calculation of the Laplace transform. Pitman and Yor (1997), pp. 864, 890–891.
Lean represents a random ranked sequence as on a probability space. Its index means the paper's . Thus the goal uses , and the tail-ratio milestones use . The paper's Definition 1 is represented by independent beta coordinate laws followed by a decreasing ranking. The ranking counts multiplicity using extended cardinality, so an infinite set of terms above a threshold cannot acquire a finite fallback count. The law of the ranked sequence is expressed through measurable preimages. This avoids treating a nonmeasurable ranking map as a zero measure through Measure.map.
All targets retain ; the targets also retain . The beta law and integrals use these parameter ranges. Real expectations state integrability or square integrability where needed, preventing a nonintegrable Bochner integral or variance from supplying a fallback zero. The nonnegative change-of-measure identity uses extended nonnegative integrals, and its local time is identified by the almost-sure limit rather than by an arbitrary extra weight or a limit operator with a default value. The Gaussian variances are positive on this parameter range, despite being represented by nonnegative real parameters in Mathlib. The formalization must use the actual tail ratio of the sequence, not an independently assigned factor process.
The reusable infrastructure includes the ranked-value operation, the stick-breaking law, convolution powers, the tail-ratio and chain-factor definitions, and the bridge between and . Contributions that establish these interfaces or prove the displayed mean, strong law, and central limit assertions directly against them are within scope. Pitman and Yor (1997), Definition 1, Propositions 11, 14, 44.
Labour markets match workers to firms that hire teams: a firm's output depends on the whole set of workers it employs, while each worker holds one job. A salary agreement is stable when no firm and group of workers can renegotiate among themselves to the benefit of all of them. Shapley and Shubik (1971) showed that such stable outcomes exist when each firm hires at most one worker and utility is transferable; Crawford and Knoer (1981) extended this to general utilities, still one-to-one. Kelso and Crawford (1982) let firm size be endogenous and identified the condition under which existence survives: workers must be gross substitutes for every firm. Their condition later became the standard assumption for existence of Walrasian equilibrium with indivisible goods (Gul and Stacchetti, 1999) and the basis of matching with contracts (Hatfield and Milgrom, 2005).
This mission is the second of a seven-mission series on the paper: 1, the salary-adjustment process; 2, existence of a strict core with continuous salaries (this mission); 3, one-sided coalition formation; 4, the firm-optimal allocation; 5, comparative statics; 6, gross substitutes versus nonincreasing returns; 7, a market with no core. Each mission is self-contained. Nothing of this paper was on Prove2Me before this series.
There is a finite set of workers and a nonempty finite set of firms. Worker 's utility of working for firm at salary is , strictly increasing and continuous in . Firm 's gross product when it hires the set is , and its profit at the salary vector is
The reservation salary is defined by , worker 's utility of unemployment. Section 2 of the paper assumes, for every firm :
An allocation assigns each worker to a firm at salary ; firm hires . It is individually rational (D1) if and for all . A firm , a set and salaries improve upon it if for and , with at least one inequality strict; they strictly improve upon it if all are strict. A strict core allocation (D2) is an individually rational allocation no coalition improves upon; a core allocation (D3) is one no coalition strictly improves upon. In the continuous market coalitions may use any real salaries; in the discrete market of unit all salaries lie on the grids .
Under regular utilities, (MP), (NFL), the reservation-salary relation and (GS) on all real salary vectors,
The goal fixes no grid, no constant and no particular technology.
Theorem 2 gives existence of a stable assignment of workers to firms with salaries, for arbitrary technologies under which workers are gross substitutes, without any convexity or divisibility of labour. Because the core and the competitive equilibrium coincide in this model when salaries are divisible (p. 1487), it is also an existence theorem for competitive equilibrium in a market with indivisible workers; the example of mission 7 shows that it fails without (GS). The Shapley–Shubik assignment game is the special case , with at most one worker per firm.
The result has been proved since 1982; it has not been machine-checked. Prove2Me holds a formalization of the Shapley–Shubik assignment game (AssignmentGame.CoreLP), whose core-existence theorem is a different model and is not yet proved, and Murota's gross-substitutes axioms for demand on , which concern one price per good rather than firm-specific salary vectors over sets of workers. Neither supplies this market or Theorem 2.
Discrete core allocations exist at every unit , so the natural first idea is to take a sequence of them as and pass to a limit. A limit of discrete core allocations need only be a core allocation of the continuous market in the weak sense D3, and a coalition that improves upon the limit may need salaries off every grid; nothing in the discrete statements controls how much a coalition gains, so the blocking coalitions of the continuous market may vanish on the grids. The required control has to be uniform over all individually rational allocations, which form an infinite set, while each blocking comparison involves the utilities of several workers and a nonadditive technology. A second obstacle is in the paper's notation: the gain (8) uses the salary with , which need not exist when is bounded.
Workers and firms are arbitrary finite types; every theorem assumes at least one firm (the paper's ), since with no firm and some worker no allocation exists. Salaries, utilities, outputs and profits are real numbers. An allocation has no unemployment, as in D1. The reservation salaries are data, and the paper's definition of enters as the hypothesis ; it is assumed on the goal and on milestones 2 and 3, where the discretization step needs every improving salary to be at least . Milestone 1 assumes neither this relation nor continuous (GS). The standing assumptions of p. 1486, which Theorem 2's sentence does not repeat, are hypotheses of the goal.
Explicit readings of the paper's phrases: "continuous market" means coalitions may use any real salary; "bounded above zero" is one valid for every individually rational allocation, stated without by quantifying over admissible coalition salaries; "the unit of measurement smaller than " is with and the division in ; the discrete market's salaries are , , the paper's integer salaries starting at (R1, R4) with a general unit.
Trivializing formalizations are ruled out: the goal assumes (GS) on all real vectors rather than on one grid (a stronger theorem the paper does not prove), its conclusion is the strict core D2 rather than the weaker core D3, and its hypotheses are satisfiable (a one-worker, one-firm market satisfies all of them).
A complete development needs finite optimization over sets of workers, a compactness argument over the individually rational salary schedules of each assignment, and the existence of discrete core allocations (the existence form of Theorem 1, mission 1). Proofs of the milestones, of the equivalence of D2 and D3 in the continuous market, and lemmas on finite demand correspondences reusable across the series are welcome.
How likely is a sum of independent random variables to exceed a large level ? If the summands have exponential moments, the classical answer is a Bernstein- or Hoeffding-type bound, exponentially small in . Many quantities met in statistics, queueing, insurance mathematics and the analysis of algorithms have only finitely many moments, and then no exponential bound can hold: the tail of the sum is at least as heavy as the tail of the largest summand. The Fuk–Nagaev inequality is the standard answer for this situation. It bounds by a polynomial term, which accounts for one summand being large, plus a Gaussian term, which accounts for the bulk of the sum.
The inequality was proved by D. Kh. Fuk and S. V. Nagaev in 1971 (Fuk–Nagaev 1971). S. V. Nagaev's survey of 1979 in the Annals of Probability states it as Theorem 1.3 and gives a complete proof, together with its corollaries (1.23) and (1.24). The form (1.24), , is the version quoted in the later literature on heavy-tailed sums, empirical processes and high-dimensional statistics, where it is the usual replacement for Bernstein's inequality under polynomial moments.
Let be independent real random variables on a probability space, with distribution functions , and let . Fix a level , truncation levels (positive numbers), and a number .
The truncated summands are if and if , with sum . The paper writes , and for sums of truncated means, second moments and absolute moments of order , the arguments being the truncation levels. The three used here are
For , and , write and define
Finally and .
In Lean these are the definitions S, Xt, St, muY, B2Y, AY, Atplus, Bn2, P4, P5, P6 of NagaevLD.FukNagaev.Setting.
Suppose , , and . Write (1.4) for and (1.6) for . Then
and if (1.6) holds together with or , then . The page prints the last case as "if, instead of (1.6), …"; the proof on p. 752 proves it "if, in addition", and this is what is stated.
The milestones follow the proof: the truncation inequality (1.8); the exponential Chebyshev bound with factorisation (1.9); Lemma 1.4, the cumulant bounds (1.10) and (1.11) for a variable bounded above, with the intermediate estimates (1.13) and (1.16); the bounds (1.17) and (1.18) for ; the equivalence of (1.4) with ; (1.19), under (1.4); under (1.6); and (1.20), .
Corollary 1.7 (1.23): for , , ,
Corollary 1.8 (1.24): for , , ,
Theorem 1.3 makes no assumption on the summands beyond independence and finiteness of the truncated moments; no centring, no identical distribution, no bound on the summands. The free parameters , , let a user trade the polynomial term against the Gaussian term. Corollary 1.8 is the form used for moment bounds of sums (-th moment inequalities of Rosenthal type follow by integrating it in ), for maximal inequalities, and for concentration of empirical processes indexed by heavy-tailed classes.
The result has been proved since 1971 and is not open. As far as a search of the Prove2Me catalog and of Mathlib shows, it has not been formalized: Mathlib has the exponential Chebyshev bound and the moment generating function of independent sums, but no tail inequality for sums of heavy-tailed summands. This mission produces a checked proof of the theorem in the paper's exact form, of the cumulant bound of Lemma 1.4, and of both corollaries with their explicit constants and .
The obvious argument, Chernoff's bound applied to , fails at once: without exponential moments is infinite for every . Truncating the summands repairs this, but the bound then depends on the choice of the exponent , and no single choice works for all parameters. The proof splits into cases according to the relative position of three numbers, and the minimisers , of two convex functions, and every case needs its own estimate of the cumulant of a variable bounded above. The bookkeeping of strict and non-strict inequalities across these cases is exactly what (1.7) and (1.7a) assert, and the printed text has a misprint at that point.
The corollaries need a separate step: Corollary 1.7 requires , which follows from centring only because truncation removes positive mass, and Corollary 1.8 requires combining the Chebyshev bound for with the truncated moment so that the two polynomial terms add to exactly .
X : Fin n → Ω → ℝ on a probability space, measurable and mutually independent (iIndepFun); index stands for the paper's . , , and are hypotheses ( follows from the others when ).variance is outside . On the page an infinite second moment makes each bound trivial; in Lean it would be replaced by and the statements would become false.cond_1_4, which includes the case , and (1.6) is cond_1_6, which requires . For the two are exact complements. If , and the exponential term of (1.23) take the page's limiting value , and so does the exponential term of (1.24) when ; Lean's would otherwise make them .