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 facility location plan decides which sites to open and which customers each site serves. Real facilities fail: plants are shut by strikes, warehouses by floods, distribution centres by power outages. When a customer's facility is down, she is served by a backup facility, or not served at all at a penalty. Reliable facility location chooses sites and backup assignments together, minimizing fixed costs plus the expected transportation and penalty cost over the random failures.
Snyder and Daskin (2005) introduced the level-assignment formulation in which every customer receives a ranked list of facilities, and they assumed all sites fail with the same probability. Cui, Ouyang and Shen (2010) allow each site its own failure probability , which is the realistic case: a site in a flood plain and a site inland do not fail equally often. Their compact mixed-integer program (RUFL) is the subject of this mission.
Timeline.
There are customers with demand rates , and candidate sites with fixed costs and failure probabilities ; failures are independent. Shipping one unit from to costs , and each unserved unit of customer costs a penalty . An emergency facility with index represents non-service: , and .
Each customer is assigned at levels , . Her level- facility serves her exactly when all her facilities at levels have failed. The variables are (site open), (facility is customer 's level- facility) and , the probability that serves at level . (RUFL) minimizes
subject to: at every level a customer has exactly one facility unless she has already reached the emergency facility (1b); only open sites are used, each at most once (1c); the emergency facility is assigned exactly once (1d); and the probabilities follow the transition equations
So if a customer's levels are , then .
Assume for every customer and for every regular site. In every optimal solution of (RUFL),
where .
Proposition 2 says that for a given set of facilities assigned to a customer, the optimal order of the levels depends only on the distances, not on the failure probabilities. A solution method may therefore sort each customer's assigned facilities by distance instead of searching over orders. The paper's Lagrangian subproblem (RSP) uses exactly this: "following a similar argument to Proposition 2" (§3.3.1, p. 13), its objective depends only on the set of facilities chosen, which is what makes the set function of Proposition 3 (a separate mission of this series) well defined. The proposition does not say that the nearest open facilities are the right ones: the paper's Example 1 (p. 11) shows a farther but more reliable facility can be optimal.
The result is proved in the paper; no machine-checked proof exists. The equal-probability special case is published on Prove2Me as SupplyChainTheory.rflp_ordered_assignments (Snyder–Shen Theorem 9.10), in a different model (one , no level cap). This mission adds the site-dependent case with a level cap, and it makes explicit two hypotheses the printed statement omits.
The exchange argument is short on paper, but its bookkeeping is exactly where a formal proof has to work. The paper's modified keeps the old values at unlisted indices, and that array does not satisfy the transition equations, so feasibility of the swapped solution has to be shown with the recomputed probabilities, level by level, including the fact that levels after are unchanged. The emergency case is dismissed in one sentence; its cost change must be computed. Finally, "" needs and ; the naive reading of the printed proposition, with allowed, is false, because a level-0 facility that never fails leaves all later levels with probability zero and in arbitrary order.
Indices are 0-based. Facilities are Fin (J+1) with the emergency facility Fin.last J; levels are Fin (R+1); the extended data , are definitions. , , are real arrays, with (1g) requiring , to be or . Constraint (1b) is printed with its first sum ending at ; it is formalized with the sum over all , the reading the paper's own explanation of (1b) gives. "Optimal" means feasible with objective at most that of every feasible solution; the feasible set is nonempty (send every customer to at level 0), so the goal is not vacuous. Proposition 2 carries the hypotheses and ; without them it is false, and a statement that dropped them would be unprovable rather than trivial. The level ranges over , the range in which level exists.
The development needs only finite sums and a recursion over levels; no measure theory is required. The recomputed probabilities transProb and the two moves swapY, emergencyUpY are reusable for any exchange argument on this formulation. Proofs of the milestones, of the goal, and of the equivalence of the transition equations with the closed product form are welcome.
A linear two-stage stochastic program with fixed recourse chooses a here-and-now decision before a random vector is observed, and pays a recourse cost afterwards. It is the basic model of stochastic programming, used in capacity planning, energy and supply-chain models. In practice the distribution of is never known exactly: it is estimated from data, replaced by a discrete scenario approximation, or perturbed for robustness. The question is how much the optimal value and the optimal decisions can move when is replaced by a nearby , and in which distance between probability measures "nearby" should be measured.
Rachev and Römisch (Math. Oper. Res. 27(4), 2002, doi:10.1287/moor.27.4.792.304; the mission cites the authors' preprint from edoc.hu-berlin.de) answer this with the method of probability metrics: they derive from the structure of the integrand a canonical distance on measures for each class of models. For linear two-stage programs the canonical distance is the Fortet–Mourier metric of order 2.
Timeline. Robinson and Wets (1987) studied qualitative stability of two-stage programs with respect to weak convergence of measures. Walkup and Wets (1969) had earlier established the piecewise-bilinear structure of the second-stage value function used here. Römisch and Schultz (1991) proved a quantitative stability result for two-stage programs with complete recourse in the Wasserstein metric . The present paper (published 2002) replaces complete recourse by relatively complete recourse plus dual feasibility, and by the metric , which it bounds by a multiple of (p. 13).
Let be a nonempty polyhedron and a polyhedron. Fix , an -matrix , and data , and an -matrix depending affine linearly on . The second-stage value is
with and . The integrand is when and , and otherwise. For a Borel probability measure on the problem is
with optimal value and solution set . Two assumptions are made: (A1) and for all ; (A2) has a finite second moment.
The Fortet–Mourier metric on , the probability measures on with finite second moment, is
For an open bounded , the growth function is , and with .
Under (A1), (A2), and an open bounded neighbourhood of , there are and such that for every with :
The constants are existential, so the goal does not depend on any particular estimate of them.
The theorem says that, under the two natural well-posedness conditions of linear recourse models, optimal values are Lipschitz continuous and solution sets move by at most , where only sees test functions with the local Lipschitz growth of the integrand. Since , the result contains the earlier stability theorem.
The results are proved in the paper, except Lemma 3.1, which it cites from Walkup and Wets (1969). None of them is formalized in Mathlib or on Prove2Me. A formalization would provide a checked model of the two-stage recourse function, the Fortet–Mourier metrics, and an end-to-end quantitative stability theorem for stochastic programs, none of which exist in Mathlib.
The obvious argument bounds by and then by . Two steps fail. First, the supremum ranges over all of , which may be unbounded, while lies in only for in a bounded set; the argument must localize to and then show, using convexity, that for close to the localized and global problems coincide. Second, the Lipschitz estimate in for requires the piecewise-bilinear structure of (Lemma 3.1) and a chaining argument across the polyhedral pieces of ; the integrand is not differentiable.
EuclideanSpace ℝ (Fin n). The paper never fixes its norm and all its constants are existential, so the Euclidean norm is a faithful instance. Second-stage vectors are coordinate vectors Fin k → ℝ; index sets are 0-based.DupacovaWets.Consistency.expect over restricted to .A dispatcher assigns each arriving job to one of servers. Sending it to a uniformly random server is simple but produces long queues near capacity; sending it to the globally shortest queue requires full state information. The power of choices sits between the two: each job samples servers at random and joins the shortest of them. Mitzenmacher's analysis of this supermarket model (IEEE TPDS 12(10), 2001) together with the balls-into-bins result of Azar, Broder, Karlin and Upfal (SIAM J. Comput. 29(1), 1999), established that a second random choice changes the behaviour of the system qualitatively. The idea underlies load balancers, hashing schemes and distributed schedulers.
This mission formalizes the paper's quantitative statement of that improvement in heavy traffic, the regime where the arrival rate per server approaches the service rate .
Customers arrive as a Poisson stream of rate with , service times are exponential with mean , and each customer joins the shortest of queues sampled uniformly with replacement. As the fraction of queues with at least customers follows a deterministic limiting system with fixed point . Corollary 2 of the paper shows that, for , the expected time a customer spends in that limiting system converges to
With a single choice the system is independent M/M/1 queues, and the expected time is
This mission takes these two formulas as its definitions; the limiting system itself and the convergence to are the subject of the companion mission (part I). The auxiliary function of Lemma 3 is
Throughout, is an integer and logarithms are natural.
The goal is a statement about the shape of the growth, not a constant: it pins the leading behaviour .
Theorem 4 makes "exponential improvement" precise. With one choice the expected time grows like as the load approaches capacity; with choices it grows like . It also quantifies the diminishing return of extra choices: going from to only divides the leading term by , while going from one choice to two changes its order. These constants are the benchmark against which later heavy-traffic analyses of join-the-shortest-of- policies are compared.
The result is proved in the paper (the limit clause; see Difficulty for the other clause). No machine-checked version is known to exist. The formalization yields a self-contained Lean development of the lacunary series near and of the base- product identity, both of which are classical analytic facts with uses outside queueing (lacunary power series, digit expansions).
The obvious approach compares with an integral, but the terms are not monotone images of a smooth function of a continuous index in a way that controls the error uniformly as : the number of terms close to grows like and each of them contributes nearly , so the error terms are of the same order as the quantity being measured. The difficulty is to obtain matching upper and lower bounds with constants tending to , uniformly as . Passing from Lemma 3 to Theorem 4 additionally requires controlling the change of variable inside the logarithm.
Theorem 4 as printed also contains a first clause, for all . It is false as printed near : while . The paper does not prove it, and this mission does not pose it.
lam), a natural number with the hypothesis on every statement. , and are real-valued definitions in one definition file.tsums; they converge for . Outside that range Lean's conventions (a divergent series sums to , , for ) produce meaningless values, so every statement either restricts to or or is a limit along .𝓝[<] 1; the limit uses Real.log.HasProd (unconditional convergence of finite subproducts), which for factors is the same as convergence of the partial products.A Markov decision process is specified by numbers: transition probabilities and rewards. In practice these numbers are estimated from data, elicited from experts, or produced by aggregating the states of a larger model, and in each case what is actually known is a range for each parameter rather than its value. Givan, Leach and Dean (Artificial Intelligence, 2000) introduced bounded-parameter MDPs (BMDPs) to reason about a whole family of MDPs at once: every transition probability is only known to lie in a closed interval. Their motivation was state-space aggregation, where grouping states with similar but not identical dynamics yields exactly such interval bounds, and the same object later reappeared as the interval or "box" uncertainty set of robust MDPs (Nilim and El Ghaoui, 2005; Iyengar, 2005) and of optimistic exploration in reinforcement learning (Strehl and Littman, 2008).
Over such a family, the value of a policy is no longer a number but an interval, and "optimal" needs a definition. This mission formalizes the paper's answer: two total orders on intervals, the corresponding optimal policies, and the Bellman-like equations their interval value functions satisfy.
An exact MDP has a finite set of states, a finite nonempty set of actions, transition probabilities with , a reward for each state and a discount rate . A policy is a map ; is the set of all policies. The value function is the expected discounted sum of rewards along the Markov chain with transitions . The operators
act on value functions . is the statewise order.
A BMDP gives for each an interval with , a reward and a discount rate . Its members are the exact MDPs with that and and with . The interval value of a policy is
Intervals are compared by the optimistic order, which compares upper bounds first and breaks ties by lower bounds, and the pessimistic order, which compares lower bounds first:
A policy is optimistically optimal if for all and ; pessimistically optimal is defined with . The optimal interval value functions are and .
At every state ,
and the same with in place of . The maximum over actions is for the total order on intervals: attained by some action and an upper bound for every action.
In the order the proof uses them: Theorem 3 (second sentence: is the unique fixed point of ); Theorem 6 (comparison: implies , and its three variants); Lemma 1 (every member's values and backups are bracketed by finitely many order-maximizing MDPs); Lemma 2 (statewise composition of member MDPs dominates, or is dominated by, both components); Theorem 7 (-maximizing and -minimizing MDPs exist among the order-maximizing ones); Corollary 1 ( and are a minimum and a maximum for ); Lemma 3 (statewise composition of policies improves the upper, resp. lower, bounds); Theorem 8 (optimistically and pessimistically optimal policies exist).
Theorem 9 is the interval analogue of the Bellman optimality equation. It is what makes the optimal interval value functions computable: the paper's interval value iteration algorithms and (Section 5) iterate exactly the right-hand sides of (25) and (26). The lower half of (26) is the max-min equation of robust dynamic programming with rectangular box uncertainty, and the upper half of (25) is the max-max equation behind optimistic planning; Theorem 9 states both, together with the tie-breaking second component, in one model. Theorems 7 and 8 are of independent use: a single member MDP is worst (or best) for a policy at all states at once, and the partial orders on interval value functions nevertheless have maxima over policies.
None of these results has a machine-checked proof. The platform has robust Bellman equations in other models (costs, general rectangular sets, a sup over nature) but nothing on BMDPs, interval value functions, or the orders and . The mission produces the paper's optimality theory end to end, from the comparison principle for exact MDPs to the two Bellman-like equations, on a model shared with the companion mission on interval policy evaluation.
The orders and are total on intervals but only partial on interval value functions, and they are lexicographic. The obvious construction of an optimal policy, switching statewise to whichever of two policies has the better interval, fails: the composed policy need not dominate either component in , because lower bounds can get worse at states where the upper bounds do not change (the paper says so explicitly, eq. (20)). Existence therefore needs a two-stage argument. A second obstacle is that and are defined statewise, as minima over an uncountable family; that one member attains them at every state simultaneously is a theorem (Theorem 7), and the Bellman-like equations rest on it. Finally, the inner minima in (25) act on , the lower bound of an optimistically chosen policy, which is not the componentwise best lower bound over policies; the equation couples the two components through the tie-break.
and are finite types, is nonempty; may be empty. An exact MDP is a structure with transition function F p α q , stochastic rows, reward and discount . is defined as the convergent series , not as a solution of (2). Rewards of the BMDP are tight, as the paper assumes from footnote 3 on; reward intervals are not formalized. Members of form a subtype of exact MDPs with the BMDP's and . The minima and maxima of Definition 3 and of (25)–(26) are the real infimum and supremum over that subtype, which is nonempty and on which values are bounded, so no junk value enters. Intervals are pairs (lower, upper); the orders (17) are spelled out. Policies are deterministic stationary maps , the paper's . An ordering of is a bijection Fin |Q| ≃ Q, and the index of Definition 1 is the largest index at which expression (9) does not exceed 1 (the page's phrase admits ties; only the largest index keeps the remaining mass inside its interval). Definition 8 is read as for an optimistically optimal , so the goal is quantified over all optimistically (pessimistically) optimal policies; Theorem 8 is the milestone that makes this quantification non-vacuous. Lemma 3 is stated as in the Appendix (p. 36): part (d) concerns , where p. 17 misprints .
A formalization in which members carry their own discount, rows need not sum to one, the minima range over all functions , or is the componentwise supremum over policies would make several statements false or trivial; each is ruled out above.
Contributions welcome beyond proofs of the milestones: a reusable theory of discounted policy evaluation for finite MDPs (the series representation, the fixed-point characterization, monotonicity of ), which other missions on finite MDPs can import.
Randomized load balancing asks how much a dispatcher gains from a little information. In the supermarket model, jobs arrive at servers and each job inspects a few servers chosen at random before joining one. With one random choice every server is an independent M/M/1 queue, and the expected time a job spends in the system is at load . With two choices it is exponentially smaller as . This "power of two choices" underlies the design of distributed schedulers, hashing schemes and server farms, where querying every server is too expensive but querying two is cheap.
Timeline:
Customers arrive as a Poisson stream of rate , , at FIFO servers. Each customer chooses servers independently and uniformly at random with replacement and joins the one holding the fewest customers; service times are exponential with mean . Let be the fraction of servers holding at least customers at time .
A state is a sequence of reals with , and . The empty state has and for . As the tails follow the limiting system
A trajectory is a map , , whose values are states and whose coordinates satisfy (1) (from the right at ). Throughout, is an integer.
The fixed point is , so , , . A customer arriving in state becomes the -th customer of its queue with probability and then waits for services, so the expected time it spends in the system is
The target constant is
For and , , and:
The hypothesis holds for every initial state that comes from a finite system.
The comparison against is the quantitative content of the power of two choices: the companion mission shows as , an exponential improvement. Corollary 2 is what connects that number to the dynamics: it says the fixed point's expected time is actually reached from realistic initial states, and is an upper bound from an empty start. Theorem 2's comparison argument and Theorem 3's weighted potential are reused across the mean-field analysis of load-balancing variants (threshold policies, heterogeneous servers, work stealing), so the formal statements here are templates for that literature.
All results are proved in the paper (Theorem 3's proof is written out for with a remark that it extends). None has a machine-checked proof that we know of. The work is formalizing the known arguments for all , including the parts the paper delegates to a citation: quasimonotone comparison for countable ODE systems in Theorem 2, and the upper right Dini derivative handling of in Theorem 3.
The system is infinite-dimensional, so standard finite-dimensional ODE comparison and Lyapunov theorems do not apply as stated. Theorem 2 rests on a monotonicity property (raising the initial tails raises them for all time) that the paper justifies by a coupling intuition and a citation to a comparison theorem for quasimonotone systems; that theorem must be supplied for -bounded countable systems. The plain distance is nonincreasing along trajectories but does not decay exponentially by a direct estimate; the weights must be built so that every coordinate's contribution to is dominated by , while staying geometrically bounded so that under the doubly exponential tails of Theorem 2. Exchanging with the infinite sum defining needs uniform tail control, which is again Theorem 2.
PowerTwoChoices.Limit; λ is lam : ℝ, with , in every theorem.x : ℕ → ℝ with x 0 = 1, nonnegative and antitone. A trajectory is s : ℝ → ℕ → ℝ, a state for every , with HasDerivWithinAt on Set.Ici 0 for each coordinate : right derivative at , two-sided for .l1Dist.Filter.atTop.tsum (a divergent series would make the upper bound free and the limit attainable by a junk ), dropping the summability condition in Lemma 2 ( is also a fixed point), choosing Theorem 3's weights after the trajectory, and stating anything for only.Measurements of Ethernet and Internet traffic in the 1990s showed that cumulative traffic is self-similar and long-range dependent: correlations of the input rate decay so slowly that they are not summable, and fluctuations at large time scales do not average out the way Poisson-type models predict (Leland et al. 1994). A widely accepted explanation is that the lengths of individual transmissions (file sizes, session durations) are heavy tailed, with infinite variance. Queueing and capacity-planning calculations then depend on which stochastic process approximates the cumulative input over long horizons.
Two approximations had been proposed: fractional Brownian motion, a Gaussian self-similar process with dependent increments, and α-stable Lévy motion, a heavy-tailed process with independent increments. Mikosch, Resnick, Rootzén and Stegeman (Ann. Appl. Probab. 12 (2002) 23–68) showed that both arise from the same models and that the answer depends on how fast the number of sources grows relative to the time scale. This mission formalizes their Gaussian answer for the superposition of ON/OFF sources: Theorem 4.
A single ON/OFF source alternates between ON-periods, during which it sends work at rate , and silent OFF-periods. The ON-periods are iid with law and the OFF-periods iid with law , both on , all independent, with means , and . The tails are regularly varying: for ,
with slowly varying ( for every ). So both periods have finite mean and infinite variance, and the ON-periods have the heavier tail.
To make the source stationary, a delay is used, where is Bernoulli with and have the integrated-tail laws . With the source's activity is
a stationary process with .
The -th model superposes independent copies , where is integer valued, non-decreasing and . The cumulative input is . With the quantile , the fast growth condition is
equivalently . The normalisation and limit constants are
A standard fractional Brownian motion is a mean-zero Gaussian process on with continuous paths and .
If Condition 2 holds, then
In the order of the paper's argument: the mean (p. 27); the covariance decay (2.5) ; Condition 2 (p. 61); the variance asymptotic (7.1) for ; Lemma 13, the one-dimensional limit ; the covariance limit (7.4); and the second-moment bound behind tightness (p. 63). (2.5) and (7.1) are cited by the paper from Heath–Resnick–Samorodnitsky and Willinger–Taqqu–Sherman–Wilson; they are stated here as the paper states them.
Theorem 4 justifies fractional Brownian motion as the model of aggregate traffic from many heavy-tailed sources in a single, simultaneous limit, replacing the iterated limit of earlier work, and it upgrades finite-dimensional convergence to weak convergence of paths. Functionals of the path, such as the supremum of that governs the buffer content of a fluid queue, therefore inherit Gaussian approximations. Together with Theorem 2 it shows that a single growth condition on decides between Gaussian and stable approximations.
The result is proved in the paper; it is not formalized anywhere. A formalization adds a machine-checked statement of the theorem and reusable developments of regularly varying functions, the stationary alternating renewal process, fractional Brownian motion, and convergence in .
The obvious route is a central limit theorem for , a sum of iid bounded terms; but the number of terms and their distribution change with , so one needs a triangular-array limit theorem whose variance condition rests on the exact asymptotic (7.1). That asymptotic in turn needs the covariance decay (2.5) of a single stationary source, which requires renewal theory for the alternating process with infinite-variance periods. Convergence of finite-dimensional distributions alone does not give the theorem: tightness in needs a moment bound on increments that is uniform in for small time lags, which requires Potter-type bounds for the regularly varying function .
atTop on . Each model has its own probability space carrying independent sources; the theorems hold for every such family. Lean's X n, Y n are the paper's , and Lean's sources are the paper's . Time in the normalised process runs over .Telephone call centers are large service systems: hundreds of agents answer callers who wait in a queue and hang up when their patience runs out. Staffing them is a trade-off between the cost of agents and the quality of service, and in large centers both the efficiency (agents busy almost all the time) and the service level (most callers answered almost immediately) can be high at once. Garnett, Mandelbaum and Reiman (M&SOM 4(3), 2002) study the simplest model that captures customer abandonment, the Erlang-A or queue, and derive approximations for it in the regime where the number of agents is large.
Their Theorem 2 is the process-level justification of these approximations: the queue-length process, centred at the number of agents and scaled by its square root, converges to a one-dimensional diffusion. The steady-state performance formulas of the paper (delay probability, abandonment probability, waiting times) are computed from this diffusion and its stationary law.
Timeline.
Fix a service rate . For each the -th system has statistically identical agents, Poisson arrivals of rate , exponential service times of rate , an unlimited waiting room served first come, first served, and exponential patience of rate for every caller. A caller whose wait in queue reaches their patience abandons and does not return. The number of callers in the system, , is a birth–death process on with birth rate and death rate in state . Its initial value is an arbitrary random variable.
The traffic intensity is . The centred and scaled process is
When it counts waiting callers and when it counts idle agents, both in units of .
For and , the drift is the piecewise-linear function
and the limit diffusion solves , where is a standard Brownian motion independent of . The noise is additive, so this means: has continuous paths and for all . Below it behaves like an Ornstein–Uhlenbeck process with restraining force , above like one with restraining force .
Assume
and for a probability law on . Then
where is the solution of with , and this solution is unique in law.
On every probability space with a standard Brownian motion and an independent initial value , the equation has a solution adapted to , and any two solutions with the same and initial value are indistinguishable.
The infinitesimal expectation and variance of at the point , as displayed on p. 224, satisfy
The result. Theorem 2 is the basis for the paper's QED (quality- and efficiency-driven) approximations , which give explicit formulas for the probability of delay, the probability of abandonment and the waiting-time distribution in terms of , and . Unlike the case, may be of either sign: abandonment keeps the system stable even when the offered load exceeds the number of agents. The resulting square-root staffing rule , with , is used in call-center practice.
Formalizing it. The result is proved in the paper by Stone's criteria for birth–death processes, with uniqueness of the limit equation delegated to the literature. No many-server process limit exists on Prove2Me or in Mathlib. A formal proof would give the first machine-checked heavy-traffic process limit for a many-server queue, and the infrastructure (Poisson time-change representation of a birth–death process, path-space weak convergence to a continuous diffusion, well-posedness of a Lipschitz additive-noise SDE) would serve every other diffusion limit in queueing theory.
The infinitesimal-moment computation is elementary; it identifies the limit but does not prove convergence. The hard step is the passage from generator convergence to weak convergence of processes on : tightness of in the Skorokhod space, which needs control of the jumps (of size ) and of the unbounded state space, and identification of every limit point as a solution of the equation, which needs uniqueness of the limit. A pointwise limit of the drifts at each fixed is not enough: the convergence has to be controlled locally uniformly along the paths. A finite-dimensional limit at fixed times is weaker than the theorem.
IsBrownianReal with every path continuous and every coordinate measurable. is independent of , which is implicit in the paper. The goal asserts existence of a solution with and uniqueness of its law; dropping the uniqueness clause, fixing to a point mass, restricting to , , , or the stationary case is a different theorem.Contributions welcome: a Poisson time-change existence theorem, tightness criteria in , well-posedness of Lipschitz SDEs with additive noise, and the martingale-problem approach to identifying limits.
This entry records a completed elementary result in the campaign on odd numbers as sums of primes: every odd natural number greater than 1 is a sum of at most 4401 primes. It illustrates how an additive density estimate can reduce the number of prime summands in a Schnirelmann argument.
For every natural number , if is odd and , there is a multiset of primes with and . Repeated primes are allowed. The bound applies to every such , not only sufficiently large integers.
The goal references the existing proved 4401 theorem. Its statement is the campaign template instantiated with 4401.
The two supporting references are the density bound and Mann's theorem, both already proved.
Let and . The density estimate gives . Mann's theorem gives , so yields density at least . The sumset cover argument then produces 4400 odd prime summands, with one additional 3 to obtain the required parity. Explicit sums of 2s and 3s handle the remaining small and medium ranges. These steps are included in the accepted goal proof; they are not unfinished milestones.
All three referenced theorems have ACCEPTED proof submissions under the account moona3k, are marked Proved, and use Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. No new Lean statement or duplicate theorem is introduced by this proposal.
The density theorem's published source credits an extraction from the accepted 6101 proof. Mann's theorem is the classical additive density theorem of H. B. Mann; the accepted formalization follows the Dyson transform presentation cited in its theorem record. This entry assembles those existing results into the 4401 bound.
The 4401 bound was an intermediate improvement on 6101. It is not the current campaign frontier: the campaign now includes a proved bound of 27. This proposal preserves the earlier result and its proof route without claiming a new literature result or a new record.
Status: complete. This mission records a finished formalization rather than an open call for work. Every statement below, including the goal, was uploaded together with a proof that the platform has verified, so there is nothing left to prove.
The Lovász Local Lemma (LLL) is a basic tool of the probabilistic method. It shows that a collection of rare "bad" events can all be avoided simultaneously, even when the events are not independent, provided each event depends on only a few others. Its best-known application is to satisfiability: a -CNF formula in which every variable appears in few clauses has a satisfying assignment.
Quantum satisfiability (-QSAT) is the quantum analogue of -SAT. Clauses are replaced by projectors acting on qubits, and the question is whether some nonzero state is annihilated by all of them, equivalently whether the corresponding local Hamiltonian is frustration-free. Bravyi showed that -QSAT is -complete for , so sufficient conditions for satisfiability are of interest in quantum complexity theory and in many-body physics. Ambainis, Kempe and Sattath (arXiv:0911.1696, J. ACM 2012) proved a quantum version of the LLL in which probability is replaced by relative dimension, and derived a sufficient condition for -QSAT instances to be satisfiable.
Let be a nonzero finite-dimensional vector space. For a subspace , the relative dimension is
It plays the role of probability: subspaces replace events, intersection replaces conjunction, and replaces conditional probability.
Subspaces have dependency sets when, for every and every set of indices with and ,
In words, is independent, for relative dimension, of every intersection of subspaces outside its dependency set.
A -QSAT instance on qubits is a family of projectors , each acting on a set of qubits and extended by the identity on the others. It is satisfiable if a nonzero state lies in the kernel of every .
The formalization proves the local lemma once, for an abstract valuation: a real function on a bounded lattice that is nonnegative, monotone and modular, , with and . Relative dimension on subspaces and the uniform probability on subsets of a finite set are the two instances used.
Let be subspaces with dependency sets , and let satisfy for every . Then
All of these are proved on Prove2Me and can be found by name (tag quantum-lll):
QLLL.Valuation.lll.QLLL.quantum_lll_symmetric.QLLL.SAT.classical_lll, QLLL.SAT.classical_lll_symmetric.QLLL.SAT.sat_of_degree_le.QLLL.PiQSAT.inf_ker_extendOp_ne_bot on Mathlib's tensor product, and QLLL.QSAT.satisfiable_of_degree_le for orthogonal projectors.QLLL.SAT.exists_assignment_forall), and the local lemma for infinite index sets under a continuity hypothesis (QLLL.lll_iInf).The quantum local lemma gives a sufficient condition for -QSAT satisfiability that depends only on the local structure of the instance: the rank of the projectors and the number of projectors per qubit. It shows that the classical criterion survives the passage from events to subspaces, even though subspaces do not form a distributive lattice. Later work on constructive and tight versions, listed in the timeline, builds on this statement.
All results of this mission are proved and machine-checked. The Lean development was written as a complete formalization of the paper, and every statement here was uploaded together with a proof verified by the platform. What the mission adds is a reusable, Mathlib-based library: the local lemma for abstract valuations, its classical and quantum instances, -QSAT stated on Mathlib's tensor product of qubits, and linear algebra on intersections of tensor products of subspaces that Mathlib does not yet contain. Mathlib currently has no form of the Lovász Local Lemma.
The classical proof uses complements of events and the identity , together with the distributive law for events. Subspaces satisfy neither in general: the lattice of subspaces is modular but not distributive, and the orthogonal complement does not distribute over intersections. The argument has to be rebuilt from the properties of relative dimension that do hold. For -QSAT, the further difficulty is to show that constraints acting on disjoint sets of qubits are independent for relative dimension, which requires computing intersections and dimensions of tensor products of subspaces.
Conventions committed to in the Lean statements:
An infinite version of -QSAT is deliberately not included. Nonzero subspaces can have all finite intersections nonzero and zero total intersection, so the infinite statement has to be phrased with compatible families of density matrices, and the current Lean formulation does not yet restrict the constraints to positive operators.
The blueprint of the formalization, linking every paper statement to its Lean declaration, is at sattath.github.io/Quantum-Lovasz-Local-Lemma/blueprint. Natural extensions, outside the scope of this mission: the orthogonal-projector form of Corollary 16 on Mathlib's tensor product once inner products on -fold tensor products are available, Shearer-type conditions, and a measure-theoretic classical local lemma on general probability spaces.
This is my first contribution to Prove2Me, so the definitions, statements, proofs and descriptions may fall short of what an experienced contributor would produce. Some choices may be unidiomatic, some lemmas may duplicate Mathlib, and the split into entries could be better. Every proof is checked by Lean, so the theorems are correct as stated; the question is whether they are stated in the most useful way.
Schnirelmann showed around 1930, by elementary means, that some absolute constant makes every integer a sum of at most primes. For odd :
The campaign's earlier values ( down to ) came from Schnirelmann's method with every constant written out. The entry used the sharp singular-series weight in a pointwise sieve bound, and its large range stopped near because the pointwise bound loses the spread of the singular series. This entry replaces that large range by Riesel and Vaughan's weighted argument, which divides out the singular series exactly, using Dirichlet characters and the large sieve. Rosser–Schoenfeld's zero-based bound is replaced throughout by Chebyshev's elementary . No zeta- or -function zero input is used, and the result matches Vaughan's .
A representation of as a sum of at most primes is a finite multiset of primes summing to with at most elements counted with multiplicity. The Schnirelmann density of is (Mathlib: schnirelmannDensity).
This is the campaign template with the value filled in.
Let and . We show , then conclude with Mann's theorem. Let be the number of ordered pairs of odd primes with . Since , it suffices to show for large . Write and for the twin-prime constant.
TaoFivePrimes.siebert_prime_pair_bound), Cauchy–Schwarz gives . The kernel sum is a finite computation.MVSieve.primitive_character_large_sieve, MVSieve.large_sieve_weight_lower), with Chebyshev's bound in place of Rosser–Schoenfeld. This gives with room to spare.The argument reaches Vaughan's with no zeros of or -functions and no prime number theorem. New reusable components:
The Lean statement is the campaign template verbatim with in place of the value. The proof imports two platform theorems: RV27.middle_range (the small-shift range, ) and RV27.large_range (), and Schnir.basis_of_density (Mann's theorem). Those rest on TaoFivePrimes.siebert_prime_pair_bound, the PrimePairSieve nodes and the MVSieve large-sieve nodes.
PrimeNumberTheoremAnd (PrimeNumberTheoremAnd/IEANTN/Chebyshev.lean).Airlines sell seats on a single flight in several fare classes. Discount classes book first, so the carrier must decide how many seats to protect for later, higher-paying passengers. The classical answer, from Littlewood's rule for two classes to the nested optimality conditions of Brumelle and McGill (1993), computes optimal protection levels from a forecast of the demand distribution of each class. Those forecasts must be built from censored booking data, which is where most of the practical difficulty lies.
van Ryzin and McGill (2000) observed that the optimality conditions themselves can drive an adaptive rule. After each flight one only records whether a fill event occurred (whether demand reached each protection level) and moves the levels by a stochastic-approximation step. No forecast and no optimization is needed. Their Theorem 1 asserts that this rule converges almost surely to the optimal protection levels, with an explicit mean-square rate. It is one of the standard references for model-free revenue management. The convergence proof combines Robbins–Monro theory, the Robbins–Siegmund supermartingale lemma and an induction over fare classes.
There are fare classes with fares and discount ratios . On a flight the class demands are independent, nonnegative and continuously distributed. Successive flights are independent with the same law.
A protection vector is . The fill events are
A vector is characterised by the optimality condition (3), for . The adjustments are , and their means are . From an arbitrary the algorithm updates
The interim protection levels are what the airline actually uses to control bookings. The updates themselves monitor .
Assume:
Then for ,
and there are and with
The exponent is left existential, as in the paper, so any improvement of the rate constant still proves the goal.
The milestones follow the paper's own proof, in attack order:
Theorem 1 says that the nested optimality conditions of Brumelle and McGill can be reached by observing binary fill events alone. It also says that the limit is automatically ordered, , so the interim levels coincide with the limit. The algorithm is distribution-free and needs neither demand forecasts nor uncensoring, which is why it is used in practice and as a baseline for later data-driven and learning-based revenue management.
The theorem is proved in the paper. As far as is known it has no machine-checked proof. Formalizing it requires a vector Robbins–Monro argument with coupled coordinates, the Robbins–Siegmund lemma, and an explicit polynomial rate. Two of the milestones are general probability facts reusable far beyond this mission: Lemma 1, and Robbins–Siegmund, which no platform item states yet. The formalization also corrects the record on two printed slips, described under Formalization scope.
Coordinate is not a Robbins–Monro process by itself. Its fill event depends on all of , so the drift of is perturbed by the errors of the lower coordinates. Applying a scalar convergence theorem coordinate by coordinate fails at this point. The perturbation has to be bounded via the Lipschitz assumption A3 and shown to be summable along the path, which uses the mean-square rate already established for class . The rate and the almost-sure convergence must therefore be carried through the induction together. The exponent halves at each class. A second difficulty is that A2 is only usable on a bounded set, so boundedness of the iterates (Lemma 3) has to come first and must be uniform.
Classes are indexed from in Lean (-indexed vectors whose index and indices above are never read). A flight's demand vector has the product law , and the sample path has the countable product of copies of it. Lean's iterate … n is the paper's , so the rate pairs it with . Continuity of a demand law is "every singleton is null". Expectations are Bochner integrals, and integrability is part of each rate conclusion. The fill event reuses the published NestedSeatAlloc.ProbCond.nestEvent.
Pinned and corrected statements:
Not posed: §4's modifications (projection onto the capacity, randomized integer levels, booking lead times) and the simulations of §5.
Contributions welcome: proofs of the general lemmas (Lemma 1, Robbins–Siegmund) stated for arbitrary probability spaces, measurability facts for the recursion, and the elementary Lemma 4.
Regev's On Lattices, Learning with Errors, Random Linear Codes, and Cryptography (J. ACM 56(6), 2009, Article 34; doi:10.1145/1568318.1568324) introduced the Learning with Errors (LWE) problem and built a public-key cryptosystem on it. The source for this mission is that published J. ACM article. The paper's main theorem, a quantum reduction from worst-case lattice problems to LWE, is outside this series; this mission formalizes a self-contained piece of finite combinatorics from §5.
In the cryptosystem the public key is a list of LWE samples, and a bit is encrypted by adding up a uniformly random subset of them. Semantic security rests on one fact: if the public key were truly uniform, the sum of a random subset of it would be close to uniform, so the ciphertext would carry no information about the bit. Claim 5.3 (p. 34:36) makes this precise for an arbitrary finite abelian group . It is a special case of the leftover hash lemma of Impagliazzo and Zuckerman (1989), in which the family of functions indexed by is a universal hash family. Variants of the same statement appear in the security proofs of most lattice-based encryption schemes that use random subset sums, including the dual-Regev and GPV-style constructions.
Let be a finite abelian group, written additively, with elements, and let be an integer. For and the subset sum is the sum of the with (the empty subset gives ). The distribution of the sum of a uniformly random subset of is
The paper defines the statistical distance of two densities as , with range , and notes that the same definition applies to discrete random variables (p. 34:14). The distance of from the uniform distribution on is therefore
with no factor . Expectations and probabilities over refer to a uniform choice of , that is, the uniform distribution on all tuples, repetitions allowed: .
In Lean these objects are RegevLWE.SubsetSum.subsetSum, P, statDistUniform and expectG.
Both sentences of the claim are in the goal. The second is what the security proof (Lemma 5.4, p. 34:37) uses: for all but a fraction of public keys, the random subset sum is within of uniform. The constants are exactly as printed.
The result. Claim 5.3 is the step in the security proof of Regev's cryptosystem that removes the public key from the picture: once the key is replaced by uniform samples (by the LWE assumption), the claim shows that an encryption is statistically close to uniform, independently of the encrypted bit. The parameter choice of Lemma 5.4 is exactly what makes negligible for . Without the claim the cryptosystem would have a hardness assumption but no reduction from it.
Formalizing it. The claim is proved, with a complete argument in the paper; nothing here is open. To our knowledge no machine-checked proof of this statement, or of the leftover hash lemma for subset-sum hash families over a general finite abelian group, exists in Mathlib or on the platform. A formal proof gives a reusable, constant-exact statement of the subset-sum leftover hash lemma with the paper's normalization of statistical distance. The four milestones are standard facts about finite averages and collision probabilities that recur in many cryptographic security proofs.
There is no deep step; the work is in organizing finite counting arguments without loss. Two points need care. The collision fact holds for every pair only because the coefficients lie in : for a general linear form over a group with torsion, a nonzero coefficient vector need not give a uniformly distributed sum, so an argument that treats the coefficients as arbitrary integers fails. And passing from the bound to the expected distance requires the exchange of expectation and square root in the right direction (concavity), which is easy to misapply. The bound must hold for every finite abelian group and every , including and , with no asymptotic slack.
[AddCommGroup G] [Fintype G] [DecidableEq G]; , and is allowed (then is the point mass at and the claim holds). No hypothesis is added to the paper's statement: holds for every group.Fin l → Bool; ranges over all functions Fin l → G, so the uniform choice of is over all tuples with repetition, not over -element subsets of .Real.sqrt (Real.sqrt x).A simulation metamodel is a cheap surrogate for an expensive stochastic simulation: after running the simulation at a few design settings, one predicts the mean response at settings never simulated. Kriging, the interpolation method of geostatistics and of the design and analysis of computer experiments (DACE; Sacks, Welch, Mitchell and Wynn 1989; Santner, Williams and Notz 2003), treats the unknown response surface as a realization of a random field and predicts by the best linear predictor. Kriging was developed for deterministic computer codes, where an observation is the exact response. A stochastic simulation returns the response plus sampling noise, and the noise may be correlated across settings when the experimenter uses common random numbers (CRN).
Ankenman, Nelson and Staum, Stochastic Kriging for Simulation Metamodeling (Proc. 2008 Winter Simulation Conference, pp. 362–370), extend kriging to this setting. The mission formalizes §2 of that paper: the form of the optimal linear predictor, called stochastic kriging, and the formula for its mean squared error, which shows how much the simulation noise costs. The source used throughout is the WSC 2008 proceedings paper, not the later Operations Research 58(2) 2010 article, whose numbering differs.
Fix a probability space and a set of design settings . On replication at setting the simulation outputs (display (3), with constant trend)
The constant is the overall mean. is a mean-zero random field, the extrinsic uncertainty imposed by the modeller. is mean-zero sampling noise, the intrinsic uncertainty of the simulation; its variance may depend on , and noises at different settings may be correlated (CRN). All of these have finite second moments, and the field is uncorrelated with the noise.
An experiment design runs replications at each of design points . The data are the sample means (4)
and the target at a point is the noise-free response .
Write . Then is the matrix of these covariances at the design points, is the vector , and is the covariance matrix of the averaged noises . A linear predictor (5) is with arbitrary weights ; its mean squared error is . The optimal MSE is the infimum of this quantity over all weights.
There is a rule , assigning a positive definite matrix to every pair of positive definite matrices, such that in every model as above with and , and at every ,
The bracket is the usual kriging MSE. The goal also states that strictly exceeds it whenever . The matrix is existential and depends only on the two covariance matrices, not on .
If , the stochastic kriging predictor
is of the form (5), attains the smallest MSE among all predictors of that form, and is the only one that does.
Display (7) quantifies the price of simulation noise. With exact observations the best achievable error is the kriging MSE; with noisy observations it is larger by a positive definite form in the cross-covariance vector. Every point that is correlated with the design therefore loses accuracy. The two examples make this concrete. In (10) the MSE increases with the intrinsic correlation , which is why the paper concludes that common random numbers, a standard variance-reduction device for comparing systems, do not help prediction. Display (14) is the baseline against which the paper measures the cost of estimating the noise variance. The conditional-expectation statement shows that under Gaussian assumptions stochastic kriging is optimal among all predictors, not only linear ones.
The results are classical in substance: they are the best-linear-prediction formulas of second-order random-field theory, applied to data whose covariance is . The paper states them without proof ("we can show"). No machine-checked version exists. Formalizing them yields a reusable, measure-theoretic best-linear-predictor theorem for random vectors defined from a model rather than postulated, together with the Loewner-order fact behind the positive definiteness of .
The algebra is short; the difficulty is in deriving the second-moment structure from the model, not assuming it. The covariance of must be computed from the sample-mean definition, using bilinearity of covariance over finite sums of square-integrable variables, and shown to equal . The cross-covariance with must be shown to equal . The MSE of an arbitrary affine predictor then has to be written as a quadratic in , and its infimum identified.
A first idea is to take "a random vector with mean and covariance " as the hypothesis. That proves a different, more abstract statement and leaves the model's content unproved.
For the second line of (7), the positive definiteness of does not follow from a scalar argument. It is a matrix inequality, for , and it fails without : when the two lines coincide.
X; design points are x : Fin k → X, so the paper's index is i.val + 1. Replication is index j - 1 of a sequence ε : ℕ → X → Ω → ℝ.covariance. The optimal MSE is an infimum over all of , with no unbiasedness constraint and no sign constraint.Infrastructure needed and reusable beyond this mission:
Contributions to any of these are welcome.
Stochastic simulation models of queues, supply chains and manufacturing systems are often too slow to run at every input setting of interest. A metamodel fitted to a moderate number of simulation runs then stands in for the simulation, for instance inside an optimization or a sensitivity analysis. Kriging, developed in geostatistics and in the design and analysis of deterministic computer experiments (DACE), predicts an unknown response surface by treating it as a realization of a Gaussian random field. Deterministic kriging interpolates its data exactly, which is wrong for stochastic simulation, where each run returns the response plus sampling noise.
Ankenman, Nelson and Staum's stochastic kriging separates the two sources of uncertainty: the extrinsic uncertainty of the unknown surface and the intrinsic uncertainty of the simulation output. Its optimal predictor requires the intrinsic noise variances, which are never known in practice and are replaced by sample variances computed from the same replications. This mission formalizes the paper's first key result: this plug-in step introduces no prediction bias.
The source is the Winter Simulation Conference 2008 proceedings version of the paper (pp. 362–370). The later Operations Research 58(2) (2010) article numbers its results differently and is not the reference here.
Fix a probability space and design variables . On replication at setting the simulation returns
where is a constant trend, is a mean-zero random field on (the unknown surface) and is the noise of replication . The quantity to predict at any point , simulated or not, is the noise-free response .
An experiment design is a list of pairs , , with distinct design points and replications at . The data are summarized by the sample means , collected in the vector , and the sample variances
The extrinsic covariances are the matrix and the vector .
Assumption 1. is a stationary Gaussian random field: all its finite-dimensional laws are multivariate normal with mean , the covariance is with and , and the covariance matrix at finitely many distinct points is positive definite. At each design point the noises are i.i.d. with ; noises at different design points are independent (no common random numbers); and the whole noise family is independent of .
The intrinsic variance at a design point is estimated by , giving and the plug-in stochastic kriging predictor
Under Assumption 1, with replications at every design point, the prediction error is integrable and
Theorem 1 says that the practitioner's shortcut, estimating the noise variances from the replications and plugging them into the optimal predictor, keeps the predictor unbiased; the cost of not knowing the intrinsic variance is paid entirely in mean squared error. This is what makes the paper's subsequent comparison of the plug-in MSE with the known-variance MSE the right measure of the penalty for estimation.
None of these statements has a machine-checked proof, and Mathlib has neither the chi-squared law of the normal sample variance nor the independence of the normal sample mean and sample variance. A complete development produces these classical facts of normal sampling theory for the first time in Lean, together with a reusable model of noisy observations of a Gaussian random field.
The predictor is a nonlinear function of the data: its weight vector is random and depends on the same replications as . Linearity of expectation therefore does not apply directly: the obvious argument, which treats the weights as constants, fails, and the dependence between the estimated variances, the sample means and the field has to be controlled exactly. The joint independence structure of Assumption 1 — across replications, across design points, and between noise and field — is load-bearing; a weaker pairwise or pointwise independence does not suffice. Integrability of the error must also be established, since the weights depend on random variances.
Design points are indexed by Fin k (the paper's is i.val + 1) and lie in EuclideanSpace ℝ (Fin d); replication of the paper is index j - 1 of a sequence, so sums run over Finset.range. The field is M : EuclideanSpace ℝ (Fin d) → Ω → ℝ with Mathlib's IsGaussianProcess; covariances are ProbabilityTheory.covariance; stationarity is with . The noise law is HasLaw … (gaussianReal 0 (V (x i))); independence is one iIndepFun over the family indexed by Fin k × ℕ plus one IndepFun between that whole family and the whole field. The variance function is ℝ≥0-valued with assumed; replication counts satisfy wherever appears and where only means appear. The chi-squared law is gammaMeasure (ν/2) (1/2).
The covariance quantities and in (13) are the true ones; only is estimated, and is built from the same replications as . A formalization in which is deterministic or independent of the data, in which the matrix may be singular (Lean's Matrix.inv returns there, reducing the claim to ), or in which the expectation is asserted without integrability, would trivialize the goal and is ruled out: positive definiteness of at distinct design points is part of Assumption 1, and integrability is part of the conclusion. may coincide with a design point.
A complete development needs: the law of linear images of independent Gaussian vectors; independence of the sample mean and the residual vector for i.i.d. normal samples (Cochran's theorem); the chi-squared law of the normal sample variance; the strong law of large numbers for the sample variance; and a measurability and boundedness argument for the random weight vector. The normal-sampling results are reusable well beyond this mission and are welcome as separate contributions.
A correlated equilibrium (Aumann 1974) is a probability distribution over strategy profiles of a game such that no player gains by deviating from a recommended strategy, given the recommendation. It is the solution concept of choice when players can condition on common signals, and its set is a convex polytope defined by linear inequalities, which makes it computationally tractable in a way that Nash equilibrium is not. A natural question in learning in games is whether simple adaptive behaviour by individual players, each using only their own payoffs and the observed history, leads to it.
Hart and Mas-Colell (2000) answer this with regret matching: each player switches away from their last action with probabilities proportional to the regret for not having played other actions in the past. They show that if every player uses this rule, the empirical distribution of play converges almost surely to the set of correlated equilibria. The procedure and its analysis became standard references for no-regret learning, internal (swap) regret, and the counterfactual-regret-minimization algorithms used in large imperfect-information games.
Timeline. Foster and Vohra (1997) obtained convergence to correlated equilibria by calibrated forecasting. Fudenberg and Levine (1999) gave conditionally consistent procedures with the same consequence. Hart and Mas-Colell (2000) gave the regret-matching procedure (2.2), in which a player's probabilities depend on regrets only, together with a Blackwell-approachability variant (their Theorem A, the subject of the companion mission 2 of this series).
A finite game has a finite set of players , a finite strategy set for each player, and payoffs on . A probability distribution on is a correlated -equilibrium if for every player and all
a correlated equilibrium is the case .
The game is played at , producing a history . For the regret of player is
the average gain player would have had by playing every time they played . Fix with for every , where and . Under regret matching (2.2), if player last played , then at they play each with probability and repeat with the remaining probability; the first-period mixed actions are arbitrary, and given the history the players randomize independently. The empirical distribution of play is .
Almost surely, converges to the set of correlated equilibria:
This is convergence to a set, not to a point; the paper notes that need not converge.
They follow the Appendix proof:
The squared distance satisfies a block recursion (M1). The cross term is rewritten through the transition probabilities (M2) and compared with a stationary auxiliary process (M3–M5). It then factors into a difference of consecutive matrix powers (M6), which is small (M7). This gives
Along this gives a.s. (M9–M10), and then a.s. (M11). A companion item states the strong law for dependent variables that M10 cites.
The result. The Main Theorem shows that correlated equilibrium is reached by uncoupled play: each player needs only their own payoff function and the history of play, and nothing about the others' payoffs. Steps M10–M11 give more than the goal, namely that every player's internal regrets vanish almost surely. The procedure underlies later work on swap regret, calibrated learning and regret-minimization algorithms for extensive-form games.
Formalizing it. The result is proved in the paper. As far as a search of the platform and the local index shows, it has no machine-checked proof. The mission asks for one, following the paper's eleven steps. Several pieces are general and reusable: a bound on consecutive powers of a stochastic matrix with positive diagonal (LEMMA, proof of M7); a perturbation bound for multi-step transition probabilities (LEMMA, proof of M4); and a strong law of large numbers for martingale differences with general normalizing sequences, which Mathlib does not have in this form.
The natural approach is Blackwell approachability: show that the expected regret vector moves toward the nonpositive orthant in one step. It fails here. The one-step condition holds when a player uses an invariant distribution of , which is the procedure of Theorem A, but regret matching uses a row of instead. The cross term of the one-step recursion therefore does not vanish.
The proof has to work over blocks of periods. Within a block the players' choices are not independent given , because the transition probabilities change with time. The paper therefore compares the play with a process whose transitions are frozen at time . The matrix-power estimate cannot use convergence of , since only the diagonal of is known to be positive and may be reducible or periodic in its off-diagonal structure. The block length must also balance the errors and , which is why the subsequence appears.
Players form a Fintype ι, strategies form Fintypes S i, each nonempty, and a profile is a function ∀ i, S i. is Mathlib's stdSimplex. Time is 0-based: play τ is , and a history is a tuple Fin t → ∀ i, S i. Regrets, , and are deterministic functions of a finite history. Every statement has , because the Lean value at is a default. A play of a behaviour profile on a probability space (IsPlay) is a sequence of profile-valued random variables with measurable level sets whose conditional law given any history of positive probability is the product of the players' mixed actions. Statements quantify over every probability space carrying a play, and conditional quantities given assume . The auxiliary -process is encoded by its explicit law, a power of the product transition matrix. The paper's (footnote 34) is a constant chosen after the game, and and before the initial play, the probability space and the play. Distances on are sup distances.
The hypotheses are exactly footnote 5's: and , with one for all players. The goal requires every player to follow (2.2). If other players may play arbitrarily the statement is false (§4(d)), so IsPlay constrains all of them. The goal is stated with an existential correlated equilibrium at distance less than , not with a distance to a possibly empty set, so no encoding makes it vacuous.
Disclosed choices:
Contributions are welcome at every milestone. The two LEMMAs and the strong law are self-contained and independent of the game.
Many problems in statistics, signal processing and machine learning minimize the sum of a smooth function and a convex but nonsmooth one: -regularized least squares (the Lasso), bound-constrained problems, and group-sparse regression are standard examples. Tseng and Yun (Math. Program. Ser. B 117 (2009) 387–423) proposed the coordinate gradient descent (CGD) method for this class and proved that it converges linearly under a local Lipschitzian error bound, Assumption 2(a) of their paper. An assumption is only as useful as the list of problems known to satisfy it. Section 6 of the paper supplies that list, and this mission formalizes it.
Error bounds of this kind have a history in smooth constrained optimization. Luo and Tseng proved them for quadratic objectives over polyhedral sets (Luo–Tseng 1992, SIAM J. Optim.), for strongly convex functions composed with a linear map (Luo–Tseng 1992, SIAM J. Control Optim.), and for dual functionals of linearly constrained strictly convex programs (Luo–Tseng 1993, Math. Oper. Res.), and used them to derive linear rates for feasible descent methods (Luo–Tseng 1993, Ann. Oper. Res.). Tseng and Yun carry these results over to the nonsmooth problem (1) by reformulating it as a smooth problem over the epigraph of the nonsmooth part.
Throughout, carries the Euclidean norm . The problem is
where , is proper, convex and lower semicontinuous with effective domain , and is continuously differentiable on an open set containing .
The residual at is
the unique minimizer of a strongly convex function. A point is stationary if the one-sided directional derivative satisfies for every direction ; denotes the set of stationary points and the distance to it. A point is stationary exactly when its residual vanishes.
Assumption 2(a) asks that and that for every level there be constants with
Writing , problem (1) is equivalent to the smooth problem (41). Its projection residual at is the optimal solution of
is polyhedral if is the solution set of finitely many linear inequalities in ; is quadratic if with symmetric, not necessarily positive semidefinite. The four problem classes are:
Under C4, nonemptiness of is part of the conclusion. The constants are existential, so the goal does not depend on any particular estimate.
If is Lipschitz on with constant , there is depending only on with
If and C1, C2 or C3 holds, then for every there are with
where solves (42) with .
A further item, not a milestone, states the remark after Assumption 2 (p. 404) that Assumption 2(b) (stationary points with different objective values are uniformly separated) holds whenever is convex.
Theorem 4 is what makes the linear convergence theorem of the paper (Theorem 2, the subject of the second mission of this series) applicable. Through C1 it covers every problem with a quadratic and a polyhedral , including the Lasso and -regularized or bound-constrained quadratic programs, without convexity of . Through C2 it covers losses of the form with strongly convex, such as least squares , where itself is not strongly convex because may have a nontrivial kernel. These error bounds became a standard tool for linear rates of proximal and coordinate methods without strong convexity.
The paper's result is proved, but Lemma 7 is proved by citation: it applies three error bounds of Luo and Tseng to the reformulation (41). A complete formalization therefore requires those error bounds for smooth problems over polyhedral sets, which are not in Mathlib. To our knowledge none of the results of this mission has a machine-checked proof.
Lemma 6 and the C4 case of Theorem 4 are short inequality arguments. The difficulty is Lemma 7. The natural first idea, proving an error bound from strong convexity, fails for C1–C3: may be nonconvex (C1) or have a degenerate Hessian (C2, C3), and the objective of (41) is never strongly convex in . What replaces strong convexity is the polyhedral structure of , and the cited Luo–Tseng error bounds that exploit it are substantial results in their own right, each of which has to be established for a projection residual over a general polyhedron in .
is EuclideanSpace ℝ (Fin n), with indices . is the pair , its effective domain and its finite values there, with "proper, convex, lsc" given by the published ProxNewton.Inexact.IsProperClosedConvex. The value is never computed: every statement quantifies over , and membership in is x + d ∈ D ∧ P (x + d) ≤ ξ + δ. is a chosen minimizer of its subproblem, which at is the paper's unique one. The solutions of (42) enter through a predicate, and every bound is asserted for every optimal solution. Stationarity is the liminf form of . is the infimum distance. Assumption 2(a) quantifies over every real , which agrees with the paper's "" because the condition is vacuous below . In Lemma 6 the constant is quantified before the dimension and the data, so it depends on the Lipschitz constant only.
Explicit choices relative to the printed text:
A polyhedrality notion that admits only affine or constant , an Assumption 2(a) whose constants are chosen after , and a Lemma 7 whose residual is instead of the solution of (42) would all trivialize or change the statements. The encoding rules out each of them: polyhedral means a finite system of linear inequalities in , the constants precede , and Lemma 7 is stated for (42).
Welcome contributions: proofs of Lemma 6 and of the C4 case; Lipschitz continuity of polyhedral functions on their domain (Rockafellar–Wets, Example 9.35); the Luo–Tseng error bounds for affine variational inequalities and for composite strongly convex objectives over polyhedra, which can be reused well beyond this mission.
A backward stochastic equation determines its current value from a conditional expectation of future values. A forward equation determines its current value from past values. Coupling the two makes existence depend on more than integrability of the data: the feedback between the past and future can prevent a solution. Antonelli's 1993 paper studies this interaction in an space for equations driven by bounded variation processes, motivated in part by recursively defined stochastic utility in finance (Antonelli 1993, pp. 777–778).
The paper first gives an existence and uniqueness condition for a coupled system. It then tests the size of that condition with two examples. The first uses a singular coefficient matrix; the second, targeted here, uses a nonsingular linear coupling. This distinction matters because the failure of existence in the first example could otherwise be attributed to the singular matrix. The second example places the obstruction at a particular time horizon while retaining a linear map with Lipschitz constant one (Antonelli 1993, pp. 791–792).
Fix a complete probability space with a right-continuous filtration , where . At time , describes the information available. Let be an integrable, strictly positive, -measurable random variable. Let be a strictly positive, bounded, -measurable random variable. Both positivity statements are almost sure.
The unknowns are real-valued stochastic processes and . The forward equation starts from and accumulates :
The backward equation sets equal to the conditional mean, given current information, of a future integral and the terminal input:
These are equations (3.10)–(3.11) of the paper. Their coefficient functions are and , each with Lipschitz constant for the paper's sum norm on pairs. The associated linear coefficient matrix is nonsingular. A solution is sought in for each component: the expected time integral of its absolute value is finite, and the equations hold in that space. This is the same integrability regime used to state the coupled system in §3 (Antonelli 1993, p. 785).
The terminal value is the random variable . Conditional-expectation processes in the intermediate identities are denoted and . Jointly measurable versions are used when these processes appear inside time integrals.
For any positive horizon, the paper derives an equation for in terms of , a weighted future integral of , and . With the sign consistent with the preceding display, the identity is
The printed equation (3.12) places inside the negative conditional expectation. That is inconsistent with both the preceding display and the next closed form; the formal statement uses the consistent sign and records the discrepancy (Antonelli 1993, p. 792).
The remaining intermediate targets are the paper's closed form for , equation (3.13) for , and the terminal-mean relation:
The last identity is stated without division, so it also has meaning when . These identities give the milestones in the order they occur on p. 792.
At the specific horizon , the coupled equations have no solution:
Strict positivity makes the right side of the mean identity positive, while its left side vanishes. The statement is a nonexistence result for the same broad solution class as the paper, rather than a claim about a narrower pathwise class.
Example 2 shows that a nonsingular coupling can still lose existence at a finite horizon. Thus the obstruction exhibited by the earlier singular example is not explained by singularity alone. The example also marks a limitation of replacing the paper's smallness condition with the assumption that the Lipschitz constant is merely finite. At and , the product exceeds one, as the paper notes (Antonelli 1993, p. 791).
A completed formalization would connect conditional expectations, jointly measurable time-indexed versions, and integration in in a reusable Lean development. The paper proves the mathematical result. This mission asks for machine-checked statements and proofs of its intermediate identities and nonexistence conclusion; it does not claim that the result is an open mathematical problem.
The main challenge is that the equations are equalities of integrable processes, not pointwise equalities at every time and outcome. A value assigned to by an arbitrary representative of an class is uncontrolled, so the terminal value must instead be reconstructed from the forward integral. Conditional expectations are defined only up to almost-sure equality at each time, yet the subsequent formulas integrate their time-indexed versions. This requires a jointly measurable version and careful movement between almost-sure statements at fixed times and statements.
There is also a printed sign inconsistency in (3.12). Propagating that sign would contradict the later sine-cosine formula. Finally, the paper's quotient formula for cannot be used at , because its denominator vanishes there. The undivided mean identity is the meaningful target at the critical horizon.
Time is represented by , and all integrals over time use ; for Lebesgue measure this agrees with the paper's ordinary time integrals. The ambient probability measure is a probability measure, and the filtration satisfies right continuity and completion at time zero. The two unknown processes are jointly measurable and have finite lower-integral norms. A solution uses a jointly measurable version of the conditional-expectation process, with each conditional-expectation argument explicitly integrable. The terminal is defined from and , independently of an arbitrary endpoint value of .
The source calls and positive; the formalization reads this as strict positivity almost surely, because allowing both to vanish admits the zero solution. is integrable as required by the standing assumption on in §3; remains bounded as Example 2 states. The four intermediate identities are stated for general , while only the main result fixes . Their process equalities hold in , and the terminal identity holds almost surely. This keeps the target from becoming true simply because endpoint representatives can be chosen freely.
The needed development includes product measurability, conditional expectation, Fubini's theorem, time integration, and the trigonometric identities in the closed form. The and version definitions can be reused for other coupled systems with deterministic time integrators. Contributions that establish the intermediate identities under the stated integrability assumptions, or develop the corresponding measurable-version tools, support the goal directly.
In the periodic-review inventory model with lost sales, demand that cannot be met from stock is lost rather than backordered. With a positive order lead time the state of the system is a vector of length : on-hand stock plus the orders still in the pipeline. This model is standard in retail, where a customer facing an empty shelf buys elsewhere. Its optimal policy is not a base-stock policy and depends on the whole pipeline vector, which makes it much harder to analyse than the backorder model.
A basic question for any stochastic inventory model is how its optimal cost responds to uncertainty in demand. For the backorder model it is classical that more variable demand costs more (Song 1994). Zipkin's paper (Oper. Res. 56(4), 2008, 937–944) recasts the lost-sales model in a transformed state in which the optimal cost functions are L-convex. Its §5 uses this structure to prove the lost-sales analogue: if demand becomes more variable in the convex order, the optimal cost does not decrease. The paper presents this as new in the lost-sales setting.
Timeline of the structural results the mission rests on:
The order lead time is a positive integer . The cost factors are the unit procurement cost , the unit holding cost , the unit lost-sales penalty and the discount factor . Demands in different periods are independent and nonnegative, with a common law. The paper treats states and orders as continuous.
Transformed state. A state is a vector , where is the stock on hand plus all orders due to arrive or more periods hence, and by convention. So is the inventory position and is the stock on hand. The state space is
The action is , where is the order quantity, and is the all-ones vector. After demand , the next state is
Costs and recursion. The end-of-period holding and penalty cost is , and its expectation given on-hand stock is . The optimal cost functions satisfy
with . This is the paper's recursion (1)–(2), written in the state .
Program (4). Fix a demand . Choosing the next stock level , with and , gives
Here is the leftover stock and the unmet demand.
Parametric demand. The demand depends on a real parameter , with law , and is the optimal cost under . A random variable is smaller than in the convex order if for every convex for which both expectations exist. This forces equal means and a variance that does not decrease.
If is increasing in with respect to the convex order, then for all and all ,
Theorem 11 is a comparative-statics statement: replacing demand by a mean-preserving spread cannot lower the optimal cost from any starting state, at any horizon. It justifies valuing variance reduction in lost-sales systems, for example forecasting or demand pooling, without solving the high-dimensional dynamic program. The induction pattern of the proof transfers to other parametric questions about the model; §6 of the paper notes that the parametric analysis remains valid in several extensions.
The paper proves Theorem 11 in a few lines on top of Theorem 4. No machine-checked proof of the result or of its structural prerequisites is known: neither the lost-sales recursion in the transformed state nor its convexity is formalized. A complete development checks the measure-theoretic steps the paper leaves implicit: that the optimal costs are finite, the existence of the expectations, and the passage from convexity in on to the convex order's test functions on .
The argument looks immediate: the costs are convex, so the convex order should apply directly. It does not. The function to which the convex order must be applied is the end-of-period cost as a function of demand. In recursion (1) that function is , where the next state depends on through the kink . Convexity of alone does not make this composition convex in . The paper avoids the issue by passing to program (4), where the amount of demand filled is a decision. That requires two facts: that selling as much as possible is optimal (milestone 1), and that the program is jointly convex in state, action and demand (milestone 3), which needs convexity of on all of (milestone 2). A second difficulty is analytic: the optimal costs are defined by infima and expectations, and one must show that these are finite and integrable before any order comparison applies.
Fin L → ℝ with 0-based indices matching the paper. is the helper vext. is the set of antitone, nonnegative vectors.fbar … (μ φ) k v.StochasticOrders.Convex.ConvexOrder (Shaked–Shanthikumar (3.A.1)), applied to the identity on . Equal means are a consequence and are not assumed.Ruled out. Value functions that collapse to a junk constant would make Theorem 11 trivially true. This is excluded because the recursion is defined, not assumed, and every cost and demand hypothesis is imposed for every . Replacing the convex order by "variance nondecreasing", by the increasing convex order, or by test functions convex only on changes the theorem and is not accepted.
Infrastructure and contributions. A complete development needs:
The model file is shared in shape with the series' missions 1 (L-convexity) and 2 (policy bounds), and its convexity lemmas are reusable for other parametric comparisons of the lost-sales model. Proofs of any milestone, and alternative arguments that bypass program (4), are welcome.
Network design problems often ask for a cheap spanning tree in which no vertex is overloaded: in multicast and overlay networks the degree of a node bounds the number of copies it must forward, and in physical networks it bounds the number of ports. The minimum bounded degree spanning tree problem asks for a minimum-cost spanning tree whose degrees respect given bounds. Deciding whether a graph has a spanning tree of maximum degree 2 is already the Hamiltonian path problem, so exact solutions are out of reach, and the question becomes how little the bounds and the cost must be relaxed.
Some problems also impose lower bounds: a vertex that must serve as a hub, or a leaf-avoidance requirement, asks for degree at least . Singh and Lau (STOC 2007) showed that the iterative rounding method they used for upper bounds extends to both kinds at once: a spanning tree of cost at most the LP optimum whose degree at every vertex lies in .
Timeline. Fürer and Raghavachari (1994) found a spanning tree of maximum degree at most in the unweighted case. For costs, Goemans (FOCS 2006) obtained cost at most OPT with degrees at most . Singh and Lau (STOC 2007) improved this to , which is the best possible additive violation unless P = NP, and gave the extension to lower and upper bounds formalized here. The journal version appeared in J. ACM 62(1), 2015.
Let be a finite simple graph with edge costs ; no sign or triangle inequality is assumed. Let be a forest on with no edge in common with . A set is an -tree if is a spanning tree of , and is the number of edges of at . Integer lower bounds are given on and integer upper bounds on . The minimum bounded degree connecting tree problem asks for a cheapest -tree with on and on ; with it is the spanning-tree problem.
The supernodes are the vertex sets of the components of , isolated vertices included, and is the family of unions of supernodes. For , and are the edges with both endpoints in , the edges with exactly one endpoint in , and . The linear relaxation LP-MBDCT minimizes subject to
MBDCT Algorithm2 (Figure 5 of the paper) repeats: if is a spanning tree, stop; otherwise take a basic optimal solution , delete the edges with , move one edge with (if any) into and lower and by one at its endpoints, and otherwise remove from and one vertex whose support degree is at most two.
For every well-formed instance whose LP is feasible, MBDCT Algorithm2
The statement fixes no constants beyond the paper's , and it is uniform over every choice of basic optimal solution, 1-edge and removed vertex.
In the order the proof uses them: Lemma 5.3 (a basic solution is determined by a laminar family of tight sets and tight lower and upper degree rows, with ); Claims 5.4, 5.7, 5.8 and 5.9 (special supernodes, cut sizes, the value on the edges between the members of , and when a set is special); Lemma 5.6 (every set of keeps at least three tokens, exactly three only if it is special or ); and Lemma 5.1 (a basic solution has an edge with or a vertex of with support degree two).
The theorem gives, in one algorithm, a tree that is no more expensive than the LP lower bound and whose degrees miss both bounds by at most one. For the pure upper-bound problem it implies the guarantee, which cannot be improved to unless P = NP, since a Hamiltonian path is the case . With lower bounds it also covers prescribed minimum degrees.
The result is proved in the paper; no machine-checked proof of it, or of any iterative rounding analysis, is known to exist. No platform item treats bounded-degree spanning trees or iterative rounding; the nearest related item is the open Williamson–Shmoys minimum-degree spanning tree local-search goal, which concerns a different, unweighted problem. Formalizing this mission requires the extreme-point structure of the spanning tree polytope with degree constraints (uncrossing to a laminar family), the token counting argument, and the induction over the algorithm's recursion, all of which are reusable for other iterative rounding results.
The obvious argument rounds an optimal LP solution once. It fails: an optimal vertex may be entirely fractional, and no single rounding keeps both the cost and the degrees. The algorithm instead re-solves the LP after each change, and its correctness rests on Lemma 5.1, that every extreme point of the current LP has an integral edge or a vertex with support degree two. That lemma is a counting statement about extreme points: the rank bound from a laminar basis must be contradicted by a token distribution. With upper bounds only, every set of the laminar family can collect four tokens. With lower bounds a set may collect only three, and the proof must characterize those sets (special sets, Definition 5.5) and show by linear independence that the remaining cases cannot occur. A second difficulty is that the guarantee concerns the final tree after many iterations, so the degree accounting must survive the changes of , , , and along the run.
Vertices form a Fintype; edges are elements of Sym2 V with no loops, and , are finite sets of edges with acyclic and disjoint from . LP vectors are functions on Sym2 V that vanish off . Right-hand sides are computed in , degree bounds are integers, and the subtour rows range over nonempty (at the literal row would make the LP empty). A basic solution is a feasible that is the only vector on satisfying with equality every constraint tight at , including the tight rows . Supernodes are never contracted: the paper's contraction of a supernode with one active vertex is a proof device, and all of §5.1's notions are stated on the original instance.
The paper's loose phrases are made explicit as follows.
Two trivializations are ruled out. Existence of a cheap tree with degrees in is not the target: the statement is about the algorithm's outputs and quantifies over all of them. And a run that never terminates does not satisfy the goal, which requires a run to exist and every run to be bounded.
Contributions are welcome at every level: the laminar uncrossing argument (Lemma 5.3), which is reusable for any spanning-tree LP with degree rows; the counting claims; and the invariants of the recursion.
Many problems in statistics, signal processing and machine learning minimize the sum of a smooth loss and a convex, nonsmooth, separable regularizer: smooth optimization with -regularization, bound-constrained optimization, the group Lasso and, through duality, support vector regression are special cases listed in §1 of the paper discussed below. For such problems, methods that update one coordinate, or one small block of coordinates, at a time are often the method of choice, because each update is cheap and exploits separability.
Paul Tseng and Sangwoon Yun (Math. Program. Ser. B 117 (2009) 387–423) introduced the coordinate gradient descent (CGD) method for this class: at each iteration it minimizes a quadratic model of the smooth part plus the exact nonsmooth part over a chosen block of coordinates, then takes an Armijo step. Their paper proves global convergence (Theorem 1) and, under a local error bound, linear convergence (Theorems 2 and 3). This mission is the second of a three-mission series on the paper; it targets the linear convergence theorem for the cyclic (Gauss–Seidel-type) choice of blocks.
The analysis follows Luo and Tseng's error-bound framework for smooth constrained problems (Ann. Oper. Res. 46 (1993) 157–178), which established linear rates for feasible descent methods without strong convexity. Tseng and Yun extend that framework to a nonsmooth convex term.
Let carry the Euclidean norm , let , and for let be the subvector of coordinates in . The problem (1) is
where , is proper, convex and lower semicontinuous, and is continuously differentiable on an open set containing .
Given , a nonempty block and a symmetric positive definite matrix , the direction (6) is
The CGD method starts at , chooses at each iteration a block and a matrix , computes , and sets . The Armijo rule takes as the largest element of with
with and . The restricted Gauss–Seidel rule (12) asks for indices (the set ) such that the blocks used during each cycle are pairwise disjoint and cover . is block-separable with respect to if .
The analysis uses three assumptions: is -Lipschitz on (22); Assumption 1, with ; and Assumption 2. Writing for the set of stationary points of and for the full direction with , Assumption 2 says (a) and the local Lipschitzian error bound holds on every level set wherever ; (b) stationary points with different objective values are at least a fixed distance apart.
Under (22), Assumptions 1 and 2, the restricted Gauss–Seidel rule, block-separability of with respect to every , and Armijo steps with and :
No rate constant is fixed: the goal asserts the shape of the convergence, so it is not invalidated by sharper constants.
Lemma 4 (Hölder dependence of the subproblem's solution on its linear term), Lemma 5(a) (a per-block variational inequality), Lemma 5(b) (an explicit stepsize at which the Armijo test passes), Theorem 1(f) (Armijo stepsizes bounded away from zero, , ), and Theorem 2(a) (the residual at the start of a cycle is bounded by the step lengths of the cycle).
Theorem 2(b) gives a linear rate for a block coordinate method on a nonsmooth, possibly nonconvex composite problem without strong convexity: the rate follows from the error bound, which holds for a large class of problems studied in §6 of the paper (the third mission of this series).
The theorem is proved in the paper; none of it has been machine-checked, as far as a search of the Prove2Me library shows. Formalizing it requires a reusable treatment of extended-valued convex functions through their effective domains, of the coordinate-restricted proximal subproblem, and of the Armijo rule for composite objectives. The milestones Lemma 4 and Lemma 5 are self-contained facts about this subproblem and are reusable for other proximal coordinate methods.
The classical route to a linear rate, as in Luo and Tseng's smooth analysis, derives from the error bound, where is the limit value. With a nonsmooth this inequality is not available: the authors say so on p. 405, and work with in place of the quadratic term. A second obstacle is that the error bound controls the full residual , while each iteration only computes a block direction at a different point; relating the two over a cycle needs the disjointness of the blocks in the restricted rule and block-separability of . Neither the global analysis nor the error bound alone gives the rate.
is EuclideanSpace ℝ (Fin n), with 0-based coordinates. The extended-valued is encoded as a pair: its effective domain and its finite values on , with "proper convex lsc" given by the published definition ProxNewton.Inexact.IsProperClosedConvex; is never evaluated off , and every statement carries membership in explicitly. The direction is the unique minimizer of (6) when and (chosen by Classical.epsilon), and runs of the method carry the minimizer property itself. The Armijo rule takes the first admissible exponent . is a strictly increasing map with . Stationarity is for all , in liminf form. In Assumption 2, is the infimum distance and "for any " is "for every real " (equivalent, since the condition is empty below ). Q-linear convergence includes convergence of the sequence; R-linear convergence is with . The rates in the goal are along , as the paper states.
Explicit choices relative to the printed text:
A statement that replaces Assumption 2 by strong convexity, claims a rate along the whole sequence rather than along , or asserts the Q-linear contraction without convergence to a limit is not this theorem and is out of scope.
Lemma 1, the claim after (10), Lemma 3 and Theorem 1(a), which the proof also uses, are milestones of the first mission of this series and are not restated here. Theorem 3 (the same conclusion along the whole sequence for the Gauss–Southwell-q rule) is not included: its proof is omitted in the paper. Contributions welcome: proofs of the milestones, and general facts about the coordinate-restricted proximal subproblem (existence and uniqueness of , optimality conditions) that the milestones rely on.
A G/GI/N queue has identical servers, a general arrival process, a first-come-first-served waiting room and i.i.d. service times with a general distribution of mean . In the Halfin–Whitt regime the number of servers grows while the traffic intensity approaches at rate ; this is the standard asymptotic model for large call centers, where a positive fraction of customers wait but waiting times are short. Halfin and Whitt (Oper. Res. 1981) obtained a diffusion limit for exponential service times. Reed (arXiv:0912.2837, Ann. Appl. Probab. 2009) proved the corresponding limit for general service times: the centred and scaled queue length converges (Theorem 5.1) to the solution of a nonlinear stochastic convolution equation, (5.33) below.
Equation (5.33) is written in terms of an infinite-server limit, and it is not evident from its form that it reduces to the Halfin–Whitt diffusion when service is exponential. Section 5.5 of the paper gives a second representation, Corollary 5.2, in which the convolution against is replaced by a convolution against the renewal function of . With exponential service the renewal function is , and the representation becomes the Halfin–Whitt diffusion. This mission formalizes Corollary 5.2 and the renewal-theoretic steps of its proof.
Timeline. Halfin–Whitt (1981): exponential service, diffusion limit. Reed (2009): general service with finite mean; Corollary 5.2 links the general limit back to 1981. Karlin–Taylor (1975) and Ross (1983): the renewal-type equation and the renewal equation that the proof cites.
Let be a probability measure on with mean (the service-time law), its distribution function and its tail. The equilibrium distribution is
Let be the -fold convolution of (the law of the th renewal epoch ). The renewal measure is and the renewal function is , the expected number of renewals by time .
A path is càdlàg on if it is right continuous at every with finite left limits at every ; only its values on matter. Fix a càdlàg driving path (in the paper , (5.40)) and . Write and . The two equations are
All Stieltjes integrals are over the closed interval .
For every service law , every càdlàg and every :
and (5.41) has a càdlàg solution that is unique on among càdlàg paths.
The result. Corollary 5.2 expresses the many-server diffusion limit as an equation that is linear in the driving process and whose only nonlinearity is the idle-server term . This is how the paper verifies that its general-service limit agrees with Halfin and Whitt's for exponential service, and the paper's sequel interprets the integral term as the limiting idle time of the servers. Uniqueness in (5.41) also yields the paper's remark that , the solution of (5.41).
The formalization. The result is proved in the paper, but only partly written: the printed proof shows that the solution of (5.33) satisfies (5.41), while the converse and the uniqueness are asserted. The mission states both. It also produces, independently of queueing, the renewal measure of a law on with possible atoms, its finiteness on bounded sets, the renewal equation and the solution of renewal-type equations, and the identity ; none of these is in Mathlib or published on the platform. To our knowledge nothing in this mission has a machine-checked proof.
The forward direction is formal once (5.42)–(5.43) is available, but (5.42)–(5.43) itself needs the renewal measure to be finite on bounded intervals when may have an atom at , and the uniqueness half needs an argument that does not assume the kernel has mass below one on any window starting at . The converse direction, (5.41) (5.33), cannot be read off the printed proof, because (5.41) is not an equation of renewal type in . The uniqueness of (5.41) is not a contraction argument either: the atom of at has mass , which may exceed , so a naive Picard estimate on fails.
negPart.BellmanDP.Inventory.renewal_equation_exists_unique (a renewal equation with a density kernel of mass below ); ChenWhitt93.Reflection.Basic (càdlàg paths on ). Reusable output: the renewal measure, (5.39) and (5.42)–(5.43) serve any renewal-theoretic development. Alternative proofs of the converse and of uniqueness are welcome.Nonparametric regression estimates the regression function from i.i.d. observations without assuming a parametric form. The simplest such estimates are local averages: to predict at a point , average the responses of the sample points closest to . Nearest neighbor rules of this kind go back to Fix and Hodges (1951) for classification and are still a standard baseline in statistics and machine learning.
Before 1977, consistency results for such estimates assumed regularity of the distribution of : a density, continuity of the regression function, or bounded support. C. J. Stone's paper Consistent nonparametric regression (Ann. Statist. 5 (1977) 595–645) proved that suitable nearest neighbor estimates are consistent in for every joint distribution of with . This property, now called universal consistency, is the subject of the first chapters of Györfi, Kohler, Krzyżak and Walk, A Distribution-Free Theory of Nonparametric Regression (Springer, 2002), where Stone's theorem is the organising result.
This mission formalizes Theorem 2 of Stone's paper, the universal consistency of nearest neighbor weights. Mission I of the series formalizes the general criterion (Theorem 1) that the proof applies; mission III treats conditional quantiles.
Let be i.i.d. random vectors in with an arbitrary law . A weight function assigns to the query point and the sample numbers , . It is a probability weight function if and . Given i.i.d. pairs with real, the estimate of is
The sequence is consistent if, whenever the pairs are i.i.d. with the given law of , and , one has .
Scales and metrics. A scale is a nonnegative function , , and its pseudometric is
The choice gives the Euclidean metric; the sample standard deviations of the coordinates give a unit-free one. The sequence is regular (p. 599) with constants if for every coordinate of with a nondegenerate law, is bounded in probability for any two such coordinates, and condition (7) holds: interchanging and changes by a factor in whenever the th coordinates of do not all coincide.
Nearest neighbor weights. Let with and for . The weight of is
where is the number of other sample points strictly -closer to than and the number at the same distance: the th closest point receives , and tied points share the average of the coefficients of their ranks. The uniform -NN rule is for .
For every law of and every regular sequence of scales,
Uniform, triangular and quadratic -NN weights with , satisfy both conditions (Corollary 3).
Theorem 2 established that a local averaging estimate can be consistent with no assumption on the distribution of beyond the moment condition on . The same argument, through Theorem 1, became the standard template for proving universal consistency of kernel, partitioning and nearest neighbor estimates, and of the classification rules derived from them (Devroye, Györfi and Lugosi, A Probabilistic Theory of Pattern Recognition, 1996). The constant of Proposition 11 is an early instance of the cone-covering bound on how many points can have a given point among their nearest neighbors, a lemma that reappears throughout nearest neighbor theory.
The result is proved (1977), and textbook proofs exist. Mathlib contains no formalization of Theorem 2, of Stone's criterion, or of the cone-covering lemma. A formal development would supply reusable infrastructure: nearest neighbor weights with averaged ties, the exchangeability argument behind Proposition 11, and consistency of weighted averages for i.i.d. data encoded through kernels.
The obvious argument estimates by a continuity argument around , which needs a density or continuity of and is unavailable here. The difficulty is condition (1) of Stone's criterion: a single sample point may be a nearest neighbor of many query points, so is not obviously comparable to for arbitrary and arbitrary (atoms, singular parts, unbounded support). The bound must hold uniformly in and in the distribution, with a data-dependent metric whose scale changes when and are interchanged. Ties in , which have positive probability when has atoms, must be handled by the averaged weights (8), not by an index tie-break.
Points live in EuclideanSpace ℝ (Fin d). The i.i.d. sequence is the coordinate process of Measure.infinitePi, coordinate 0 being ; sample indices are 0-based, coefficients keep the paper's 1-based index. "Whenever the pairs are i.i.d." is encoded by quantifying over every Markov kernel (the conditional law of given ), with pairs distributed as and . Expectations of nonnegative quantities are lower Lebesgue integrals in ; convergence in probability is TendstoInMeasure; limits of probabilities are taken in .
Standing assumptions and additions, each disclosed in the item statements:
No statement corrects the print.
The goal is stated as consistency over all kernels and all , for an unrestricted law : it is not stated through Corollary 1's three conditions nor through , and no density, moment or support hypothesis on is present, so a proof cannot reduce to a special case.
A complete development needs: exchangeability of finite i.i.d. samples under the product measure, the finite cone cover of , the strong law of large numbers (Proposition 9's proof), and Stone's criterion (mission I). Contributions proving any milestone, the cone-cover existence lemma, or the transfer of exchangeability through infinitePi are welcome.
A dynamic programming problem in Blackwell's sense describes a controller who observes the state of a system, picks an action, collects a return, and watches the system move at random to a new state, forever. Blackwell treated the discounted case, with a bounded return and a discount factor below one (Blackwell 1965), and the positive bounded case. Strauch's paper (Strauch 1966) studies the third case, the negative case: the return is non-positive and there is no discounting. Equivalently, a non-negative cost is minimized over an infinite horizon. This is the setting of stochastic shortest-path, optimal stopping with costs, and many inventory and search problems in which the total cost may be infinite.
In the negative case two standard tools of the discounted theory break down. An optimal policy need not exist, and the natural algorithm, value iteration from the zero function, need not converge to the optimal return. Strauch's §9 gives a condition on the action sets, essential finiteness, under which both are restored. The introduction (p. 872) summarizes the finite case: "In the negative case, … if A is finite, there is an optimal policy (Section 9)." In the later terminology of Bertsekas and Shreve (1978), Strauch's negative case is their positive-cost model, for which value iteration from zero is known to require such finiteness or compactness conditions.
The state space and the action space are non-empty Borel sets. The law of motion is a probability measure on depending measurably on . The return , collected when action is taken in state and the next state is , is a Borel function with and for every .
A policy chooses the th action at random, with a law depending measurably on the whole history . A Markov policy is a sequence of measurable maps ; the stationary policy uses one map at every stage. The expected return from the initial state is
the sum of the expected stage returns. The optimal return is , over all policies, and is optimal if at every state.
For a measurable and a non-positive Borel , the operator of is
and the operator of a Markov policy is , with the operator of . Value iteration is the sequence .
Actions and are equivalent at if and . is essentially finite by if there is a partition of into Borel sets such that for every action is equivalent at to one of . A finite is essentially finite by any Markov policy whose first rules are the constant rules.
If is essentially finite by and is the operator of , then
Both parts are kept together, as printed. The goal fixes no constants and no rate.
where is the set of -generated policies (each rule equal to on the th piece of a Borel partition). 2. Proof of Theorem 8.4, p. 887. pointwise. 3. Proof of Theorem 9.1, p. 887, first step. Under essential finiteness, is non-increasing and for every policy . 4. Proof of Theorem 9.1, p. 887, second step. Under essential finiteness, .
Inside the proof of Theorem 9.1 the paper writes for ; the mission writes for it and reserves for .
An optional extra item states the introduction's special case: if is finite, an optimal policy exists (§1, p. 872).
Theorem 9.1 gives, in the negative case, both a computational and an existential conclusion. Value iteration from zero computes the optimal return, so the optimal total cost of an essentially finite problem is the limit of the optimal finite-horizon costs. An optimal policy exists and can be taken stationary, so the controller needs only a single measurable decision rule. Without a hypothesis of this kind neither conclusion holds in the negative case; Example 6.1 of the paper exhibits a problem where the limit of value iteration, the best return among generated policies, and the best stationary return all differ.
The result is proved in the paper. What the mission adds is a machine-checked statement and, eventually, proof of it on general Borel spaces, with the return allowed to equal . Blackwell's discounted analogue already has a published statement on Prove2Me (DiscountedDP.Stationary.theorem7b_optimal_stationary), in a bounded-return model; the negative case is a separate statement in a separate model. No formalization of the negative case is known to exist.
The discounted proof rests on the contraction property of in the supremum norm, and in the negative case that property is missing: returns are unbounded below and there is no discount. The obvious argument, " decreases to some , and is the optimal return because finite-horizon play approximates infinite play", fails at the second step. The finite-horizon optimum can stay strictly above the infinite-horizon optimum, because a policy can postpone a cost beyond every fixed horizon; this is exactly the gap Example 6.1 exhibits. Closing it needs the essential finiteness of the actions together with the reduction of arbitrary policies to Markov ones (milestone 2), whose proof in the paper passes through the measurable-selection results of §7–§8.
EReal and are computed as minus the lintegral of the loss , which keeps the value . is the sum over stages of the expected stage loss, which equals the paper's integral over futures by monotone convergence.EReal.Policies, Markov policies, stationary policies and -generated rules come from the published definitions DiscountedDP.Stationary.Model, .Return and .Operators; the negative model is defined locally because the published Problem has a bounded return and a discount factor below one. A complete development needs the Ionescu-Tulcea construction of the history laws (already encoded as iterated composition products), monotone convergence for kernels, the measurable-selection step behind milestone 2, and a pigeonhole argument over the essentially finite action classes. The model and the Markov-reduction milestone are reusable by the other missions of this series. Proofs of any milestone, and alternative routes to milestone 2, are welcome.
Many prediction tasks ask not for the mean of a response given covariates but for a quantile of its conditional distribution: a median that is robust to outliers, a high quantile that sets a safety stock or a value at risk, or a pair of quantiles that forms a prediction interval. Conditional quantiles are also the Bayes rules for piecewise linear loss, which makes them the decision-theoretic answer to asymmetric prediction costs.
C. J. Stone's 1977 paper Consistent nonparametric regression (DOI 10.1214/aos/1176343886) introduced a single framework for local averaging estimators (nearest-neighbor, kernel and related rules) built from weight functions, and proved that their consistency can be decided from simple conditions on the weights, for every distribution of . Section 7 of the paper extends the framework from conditional means to conditional quantiles: the same weights that estimate define a weighted empirical distribution of near , whose quantiles estimate the conditional quantiles. Theorem 3 says that consistency for the mean already gives one-sided consistency for the quantiles. This mission formalizes Theorem 3 and the results its proof rests on.
Let be independent -valued random variables with common law , and let be real responses such that the pairs are i.i.d. The conditional law of given is a probability measure on .
A weight function assigns to a point and a sample real weights , . A sequence is a sequence of probability weights if for every the weights are nonnegative and sum to . The weights define the regression estimate . The sequence is consistent if, whenever and ,
for every response with i.i.d. pairs as above. Consistency is a property of the weights and the law of alone.
The conditional distribution function is . For the lower and upper th conditional quantiles are
They coincide unless the conditional distribution function is flat at level . The weights estimate the conditional distribution function by , and the quantiles by
Write and .
For a consistent sequence of probability weights and ,
and if and , both convergences hold in . The theorem is one-sided on purpose: when the conditional quantile is not unique, and may oscillate inside .
Theorem 3 transfers every consistency result for conditional means to conditional quantiles at no extra cost. In particular, the nearest-neighbor weights of Stone's Theorem 2, which are consistent for every distribution of , give universally consistent one-sided estimates of conditional quantiles, and when the conditional th quantile is unique, the midpoint estimate is consistent (Corollary 5 of the paper). The theorem is also the input for the consistency in Bayes risk of approximate Bayes rules under piecewise linear loss (Theorem 4, Model 2), which connects nonparametric regression to data-driven decision making such as the newsvendor problem with covariates.
The result has been proved since 1977; it has no machine-checked proof that this mission is aware of. A formalization produces a reusable layer for distribution-free statistics in Lean: weighted empirical distributions, conditional quantiles defined from a Markov kernel, convergence in probability and in of statistics of an i.i.d. sequence, and the moment bounds of Propositions 14 and 15, which hold for every weight function and do not depend on the asymptotics.
The obvious argument fails because the conditional distribution function at is never estimated uniformly. Consistency controls the weighted average only for responses that are a fixed function of the pair; the event involves the random threshold , which varies with the target point while the sample responses are drawn at the sample points . Connecting the two requires a statement about the weights alone, Proposition 4, that holds for an arbitrary Borel function with no continuity or integrability; the conditional quantile function is in general neither continuous nor integrable.
A second difficulty is that convergence in probability does not give convergence in without uniform integrability, and the estimated quantiles are not averages of the . The bound in Proposition 15 must hold for each separately, with a constant independent of , for an estimator defined as an infimum.
Finally, the two-sided statement need not hold when the conditional distribution function has a flat stretch at level , which is why the paper asks for a unique conditional quantile in Corollary 5; a solver should not aim for it.
The i.i.d. sequences are the coordinate processes of infinite product measures, Measure.infinitePi, with coordinate the point (or the pair ) and coordinate the st sample; sample indices are 0-based. The response is given by its conditional law, a Markov kernel from to , and the joint law of a pair is . "Whenever the pairs are i.i.d." in the definition of consistency is a quantifier over all Markov kernels; every joint law with -marginal arises this way. This also provides the independent standard normal variables that the paper assumes on its probability space.
Committed conventions:
TendstoInMeasure.sInf/sSup. For a Markov kernel, , probability weights and , the defining sets are nonempty and bounded on the relevant side, so the values are the paper's; at the estimates are a junk value that no limit statement sees.Corrections and choices of range. Proposition 14 is printed for . The proof of Theorem 3 applies it for every , and the statement is posed for . Proposition 15 leaves unquantified and is posed for , the range Theorem 3 uses.
A goal stated through the probabilities of Proposition 13, or through truncated moments, would be a different and weaker theorem; the goal states convergence of the quantile errors and themselves, in probability and in . Swapping the negative and positive parts gives a false statement.
Corollary 1 (necessity) is a special case of Theorem 1, the goal of the first mission of this series; it is posed here as a milestone so that this mission is self-contained, and can be replaced by a reference once that mission is published. Contributions are welcome on any milestone, and on general infrastructure for Markov kernels, conditional distribution functions and quantiles, which is reusable beyond this mission.
Random partitions of the positive integers are the common language of population genetics, Bayesian nonparametrics and the theory of coalescent processes. When a sample of genes, customers or particles is grouped into classes, the grouping is a partition, and in most models its law is exchangeable: it does not depend on the labels. The best-known example is the Ewens sampling formula of population genetics (Ewens 1972); Kingman's representation theory (Kingman 1978) describes all exchangeable random partitions of .
Pitman's two-parameter family of exchangeable partitions, the partitions (Pitman 1995; Pitman and Yor 1997), contains Ewens' family as and is the partition counterpart of the two-parameter Poisson–Dirichlet distribution. Theorem 12 of Pitman 1999 shows that two natural random operations act on this family in a dual way: merging blocks of an partition according to an independent exchangeable partition (coagulation) and splitting each block of an partition by independent exchangeable partitions (fragmentation) produce the same joint law of a fine and a coarse partition. The paper uses it to describe the Bolthausen–Sznitman coalescent (Bolthausen and Sznitman 1998).
Timeline. 1972: Ewens' sampling formula, the case . 1978: Kingman's correspondence between exchangeable partitions and random mass partitions. 1995: Pitman introduces exchangeable partition probability functions and the formula (15). 1997: Pitman and Yor study the two-parameter Poisson–Dirichlet law. 1999: this paper proves the coagulation–fragmentation duality (Theorem 12) and its sharper converse, by reduction to an identity between explicit formulas. The duality is treated again in Pitman's lecture notes Combinatorial Stochastic Processes (2006).
A partition of a set is a collection of disjoint nonempty blocks whose union is the set. Write for the partitions of and for those of ; the restriction of to keeps the nonempty sets . carries the -algebra generated by the . Writing lists the blocks in increasing order of least elements.
A random partition of is exchangeable with EPF if for every and every partition of ,
For and the EPF is
with factors of and cancelled before evaluation when or . An partition is an exchangeable random partition with EPF .
Coagulation (Definition 5): for and , the -coagulation of has blocks . is a -coagulation of if, given , it is the -coagulation of for an independent with EPF . Fragmentation (Definition 11): is a -fragmentation of if, given , restricted to the -th block of equals restricted to that block, for independent with EPF . In Lean these are coag, frag, pdEPF and IsEPFLaw in LambdaCoalescent.CoagFrag.Setting.
For , , , the following are equivalent: (i) is an partition and is a -coagulation of ; (ii) is an partition and is an -fragmentation of . Formally, with laws of EPFs :
for every measurable .
Theorem 12 identifies one law of a nested pair of exchangeable partitions from both ends. Read from (i) to (ii), it shows that coagulating an partition by an independent partition yields an partition; read backwards, that an partition fragmented by partitions yields an partition. Through Kingman's correspondence it gives Corollary 13 on Poisson–Dirichlet laws, and with it connects the two-parameter family with Ewens' family. In the paper it is the tool for describing the Bolthausen–Sznitman coalescent through Poisson–Dirichlet laws. The sharper form shows the parameter relations (64) are forced.
The theorem has been proved since 1999. What this mission adds is a machine-checked development: exchangeable random partitions of with their EPFs, the coagulation and fragmentation kernels, and the reduction of identities between laws on to identities between finite-dimensional formulas. None of these objects is in Mathlib, and no formalization of the duality is known.
The algebraic heart, the EPF identity, is a finite computation with rising factorials. The difficulty is measure-theoretic and combinatorial. A law on must be pinned down by its values on the cylinder events . Computing under the coagulation kernel requires that the blocks of meeting are exactly the first blocks in order of least elements, and that the induced partition of has law given by the EPF; under the fragmentation kernel it requires the independence of the and that the restriction of an exchangeable partition to an arbitrary finite set (not an initial segment ) is governed by the same EPF. The converse in Lemmas 34 and 35 needs the bookkeeping that the formula on refining pairs exhausts total mass. Lemma 9 is an existence theorem for a projective family of laws, which the paper cites rather than proves.
A partition of is an equivalence relation on Lean's (PInf := Setoid ℕ), a partition of one on Fin n; labels shift by one, which preserves the order of least elements, and block indices are 0-based. The -algebra on PInf is generated by the coordinates , equivalently by the . Coagulation is stated with (Definition 5's case ). The EPF is the cancelled form
equal to (15) for ; this is needed because at . Conditional laws "for all " are encoded as joint laws, and equalities of laws are stated on preimages of measurable sets, so no Measure.map of an unproved-measurable map appears. Fragmenting partitions are one sample of Measure.infinitePi (fun _ => κ). In the sharper form, is written as , since PAR allows .
Not formalized: the stick-breaking characterization (12)–(13) in Lemma 9, Corollary 13 and Kingman's correspondence, and the auxiliary fact "", which as printed fails at .
A formalization in which no measure satisfies IsEPFLaw (pdEPF α θ) would make Theorem 12 and Lemmas 34–35 vacuous; Lemma 9 rules this out and must be proved for the parameters used, not assumed.
Infrastructure needed: cylinder-set uniqueness on PInf, the law of the restriction of an exchangeable partition to a finite set, block enumeration by least elements, and rising-factorial algebra (ascPochhammer). The partition, EPF and kernel definitions are reusable for any work on exchangeable partitions, Chinese restaurant processes or -coalescents. Proofs of Lemma 9, of Lemmas 34–35 and of the EPF identity are each welcome as independent contributions.