Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Queueing control problems (admission control, routing, service-rate selection, flow control) are naturally posed as Markov decision chains with a denumerably infinite state space, such as the number of customers in a buffer, and are usually judged by their long-run average cost per unit time. When the state space is finite, Chapter 6 of Sennott's book shows that an average cost optimal stationary policy always exists. On a countable state space this fails: Section 7.1 of the book gives examples in which no average cost optimal policy exists, and one in which no stationary policy comes within a given distance of the minimum average cost. The question addressed by this mission is under which verifiable conditions on the discounted value functions a countable-state model has a constant minimum average cost and an optimal stationary policy.
Timeline, following the book's bibliographic notes (p. 163). The book names Taylor (1965) and Derman (1966) as earlier pivotal work and Ross (1968), and his 1983 textbook, as the direct predecessor. Sennott (1989, Operations Research 37) weakened Ross's assumptions to cover models with unbounded costs, and proved the main result of Section 7.2; the (SEN) assumptions of Chapter 7 are the cleaner version of Sennott (1993). Cavazos-Cadena (1991) gave the example, adapted as Example 7.3.1 of the book, showing that under these assumptions the optimality inequality can be strict. The weaker (H*) assumptions of Section 7.7 appear, in a slightly different form, in Sennott (1995). Part (iv) of Theorem 7.2.3 is new in the book.
A Markov decision chain (MDC) has a countable state space , for each state a finite nonempty action set , a nonnegative finite cost , and transition probabilities with . A policy chooses the action at time at random according to a distribution that may depend on the whole history ; a stationary policy always chooses in state .
For an initial state , the -horizon cost is , the average cost is , and the minimum average cost is over all policies. A policy is average cost optimal if . For the discounted value function is . All these quantities lie in .
Fix a distinguished state and put . The (SEN) assumptions are:
A limit function is a pointwise limit of along some sequence . If is a stationary policy realizing the discount optimality equation , a limit point is a stationary policy with for large , for each , along some .
Under (SEN), there is a finite constant independent of ; limit functions exist, satisfy and the average cost optimality inequality (ACOI)
every stationary policy realizing the minimum is average cost optimal with and ; every limit point of discount optimal stationary policies is average cost optimal and satisfies the corresponding inequality for an associated limit function; and the average cost of any optimal policy is a limit, not only a limit supremum.
Theorem 7.2.3 is the existence theorem the rest of Chapter 7 builds on (p. 128): the ACOE results of Section 7.4, the (BOR) and (CAV) sufficient conditions of Section 7.5, and the worked queueing models of Section 7.6 all work under (SEN) and invoke it. It justifies computing an average cost optimal policy for a queueing model as a limit of discount optimal policies, and it shows that the minimum average cost is the Abelian limit of the normalized discounted value.
The results are proved in the book and in Sennott (1989, 1993, 1995), but none of them has a machine-checked proof: Mathlib has no Markov decision processes, and the platform's average cost results concern finite state spaces or Borel models with different assumptions. The formalization produces a general-policy, countable-state MDC development with extended-real values, reusable by the later missions of this series.
On a finite state space the relative value functions are bounded and the Abelian limit can be controlled directly. Here is bounded above only by a function that may be unbounded, so passing to the limit in the discounted optimality equation cannot use dominated convergence, and in general only an inequality survives in the limit; Example 7.3.1 shows that the inequality in the ACOI can be strict. Showing that a policy realizing the ACOI is optimal requires control of for a function that is unbounded above, and part (iv) requires comparing the limit inferior and limit superior of Cesàro averages for an arbitrary, possibly history-dependent optimal policy.
The state space is any countable type ([Countable S]); actions form a type with finite nonempty Finset action sets; costs are ℝ≥0; transition probabilities, costs over time and value functions are ℝ≥0∞. Policies are general: randomized and history dependent, with histories encoded as finite state and action sequences and the process law built by an explicit recursive product. Finite horizon costs have terminal cost , as the chapter prescribes.
The relative value is computed in EReal, never through a truncated real subtraction: a state with gives , so (SEN2) cannot hold through a junk value, and (SEN1) is a bound by a finite constant that itself forces . Sums and expectations of real functions are extended reals, computed as positive part minus negative part; they are never Bochner integrals and never default to when not summable. The limit is the filter 𝓝[<] 1. Limit functions and limit points follow Definition 7.2.2 literally, over arbitrary sequences in , and the (SEN), (H), (H*) sets are predicates carrying their witnesses and .
A development that bounds only as a free function, rather than the one built from the infimum over all policies, or that quantifies only over stationary policies in , proves a different and weaker theorem and does not count.
Needed infrastructure: the law of the controlled process under a general policy, monotone and Fatou-type limit interchanges for countable sums, the Abelian inequality (Proposition 6.1.1 of the book), and the existence and optimality of discount optimal stationary policies (Theorem 4.1.4). The MDC layer and these two results are shared with other missions of the series; contributions to them are welcome.
Service parts (spares for aircraft, machines, and networks) are typically managed item by item with a one-for-one replenishment policy, the policy: every unit withdrawn to meet a demand triggers an order for one replacement, so the inventory position stays at the stock level . A firm stocking thousands of such items at one location has to choose all the stock levels together, trading a budget on inventory investment against a service measure. Chapter 3 of Muckstadt, Analysis and Algorithms for Service Parts Supply Chains (Springer 2005, DOI 10.1007/b138879) sets up the three standard service measures (fill rate, ready rate, expected backorders), shows which of them have the convexity that optimization needs, and solves two multi-item stocking problems: minimum expected backorders under an investment budget, by Lagrangian relaxation justified by Everett's theorem, and maximum average fill rate, by a greedy marginal-analysis rule.
The Lagrangian method goes back to Everett (Operations Research 1963); the search for the multiplier in one-constraint problems of this kind is Fox and Landi (Operations Research 1970); the compound Poisson model is Feeney and Sherbrooke (Management Science 1966). The same separable Lagrangian structure underlies the multi-echelon METRIC-type models later in the book.
A single item is stocked at one location, demand not met from stock is backordered, and customer orders arrive as a Poisson process of rate . An order is for units with probability , where and the mean order size is finite (compound Poisson demand; simple Poisson demand is ). Resupply times have mean . The steady-state probability that units are in resupply is
where is the probability that orders total units. In this mission is the definition of the model, not a consequence of Palm's theorem. The mean lead-time demand is , and the book also writes .
For a stock level :
Forward differences are and ; discrete convexity means .
With items, unit costs and budget , Problem 4 (3.40) is
For a multiplier , the item-wise criterion defines as the least with , and .
For every , each exists and
for every vector of nonnegative integer stock levels. That is, is optimal for Problem 4 at budget . This is what the book asserts by combining Theorem 10 (p. 57, with the remark on p. 58) and the criterion of p. 61, and it is the basis of its bisection algorithm (p. 63). The goal fixes no numerical constant.
The goal reduces a coupled integer program over thousands of items to one scalar search: for a fixed multiplier each item is solved by a single scan of its distribution function, and each multiplier yields a point on the exact efficient frontier of expected backorders against investment. Milestone 8 does the same for fill rates on the region where they are concave, and milestone 1 explains why that region, , is imposed in practice. Milestone 4 is the identity that turns an investment budget into the constraint of Problem 4.
All results are proved in the book (Theorem 10 with a complete proof; the others by short derivations, the greedy optimality by a sketch). None of them is formalized, as far as the platform shows: there is no Everett-type Lagrangian sufficiency theorem, no compound Poisson backorder function, and no discrete marginal-analysis optimality result. The mission produces a reusable layer for later chapters: the compound Poisson steady-state law with its backorder function, and the Lagrangian machinery the book reuses for multi-echelon systems.
The algebra of first differences is elementary; the difficulties are elsewhere. is an infinite series whose convergence rests on the finiteness of the mean order size, and exchanging the difference with the sum, and identifying with , requires manipulating a doubly infinite sum over order counts and convolution powers. Existence of requires that the compound Poisson probabilities sum to one. For milestone 8 the obvious argument ("greedy is optimal for concave separable objectives") fails for knapsack constraints with unequal costs at arbitrary budgets; it holds only at the budgets the greedy run generates, and only on the region where every is concave; dropping the floor constraints makes it false.
Stock levels are natural numbers; probabilities, rates, costs and multipliers are reals. The compound Poisson law is a structure with fields , an order-size distribution with , , , and summable (the finite mean is added: without it is infinite). Expected on-hand inventory is the finite sum . Items are indexed by an arbitrary finite type (nonempty where a maximum over items is taken).
Pinnings and deviations, each stated in the item's Formalization Note:
A trivializing formalization is ruled out: the goal is stated for the book's own backorder function built from the compound Poisson law, not for an arbitrary convex function nor for a defined through its differences.
Welcome contributions: summability and normalization lemmas for the compound Poisson law, a general discrete Lagrangian lemma for separable objectives, and proofs of the milestones in any order.
Stochastic quasigradient (SQG) methods minimize an expectation over a constraint set when neither nor its gradient can be computed, only random vectors whose conditional mean is (close to) a subgradient. They are the workhorse of stochastic programming and, under the name stochastic gradient descent, of large-scale statistical learning. The classical convergence theory, going back to Robbins and Monro (1951) and to Ermoliev's quasi-Féjer analysis, asks the stepsizes to be chosen in advance with , , . Uryasev, in Chapter 18 of Numerical Techniques for Stochastic Optimization (Ermoliev and Wets, eds., 1988), points out that such programmed rules are slow in practice, and that practitioners want adaptive stepsizes computed on line from the observed directions.
Timeline:
Let be nonempty, convex and compact, its diameter, and convex on an open convex set , with subdifferential . The projection is the point of nearest to . On a probability space, the SQG method generates
from , where the direction is a stochastic quasigradient: with , a bias , and the -algebra induced by .
The adaptive stepsize rule of the chapter is, for fixed , and ,
The step grows when consecutive moves point the same way and shrinks otherwise. The weighted (Cesàro) averages are
The sequence is Cesàro convergent when converges to the solution set.
Chapter 17 (Pflug) uses the same method for over a closed convex , with from i.i.d. and stepsizes adapted to .
Under (18.15), (18.16) and (18.17), almost surely,
and if a.s., then and all accumulation points of are minimizers, almost surely.
Theorem 2 is a convergence guarantee for a stepsize rule that is computed from the run itself. It needs no square summability of the steps, and it tolerates a nonvanishing bias at a cost linear in the bias. This is the regime of practical SQG codes; §18.4–18.5 of the chapter discuss implementation and numerical experiments. Theorem 1 isolates the reason: Cesàro convergence needs only and . It also allows a stepsize that depends on the current direction, provided consecutive steps have ratio tending to .
The volume proves none of the probabilistic results in full. Theorem 1 of Chapter 18 is cited from Uryasev's earlier report. Theorem 2 has an outline proof that reduces it to Theorem 1. Chapter 17 gives a sketch through the Robbins–Siegmund lemma. None of these results is formalized. The mission produces machine-checked statements of all of them, with the misprints of the page resolved, and it separates the pathwise part of the Theorem 2 argument (steps 1 and 2, which are deterministic) from the martingale part (Theorem 1).
The obvious route to a.s. convergence is the quasi-Féjer or Robbins–Siegmund argument. It controls and needs , which is exactly what is not available here. The averaged analysis has to show that the martingale term is almost surely, and that is , when the stepsizes are themselves random. Under condition (2) of Theorem 1, is not even measurable with respect to the -algebra of the conditional expectation. So , and the standard decomposition breaks. For the adaptive rule, the stepsizes are coupled to the iterates through the exponent. Neither nor is given, and both must be derived path by path.
is EuclideanSpace ℝ (Fin n). Sequences are indexed from . Chapter 17 is shifted by one against the page: its , , become indices . Conditional expectations are Mathlib's condExp with respect to the history -algebras of the definition file. Every bound is written out as "for every , eventually ", or in (18.17) as a bound with . Expectations of squared norms are lower Lebesgue integrals. The deterministic proof steps (items 5 to 8) are stated for one sample path.
Readings of the page, each recorded in the item's Formalization Note:
No explicit constants replace an O(·) or an unspecified "C": every constant appears in the book's statements.
A trivializing formalization states Theorem 2 for arbitrary stepsizes satisfying (18.10)–(18.13), which is Theorem 1 again. Here the stepsizes are tied to the iterates by (18.5), and the of (18.17) is the of the rule.
Needed infrastructure: a Robbins–Siegmund almost-supermartingale lemma, which Mathlib does not have; a strong law for martingale differences with random weights (Kronecker's lemma in its stochastic form); nonexpansiveness of the projection onto a closed convex set; and nonemptiness of the subdifferential of a finite convex function on an open set. The first two are reusable across stochastic approximation. Contributions of any of the milestones, or of these lemmas as separate theorems, are welcome.
Decisions under uncertainty are often required to satisfy a constraint that depends on a random parameter , and requiring it for every possible is usually too conservative or infeasible. The scenario approach replaces the unknown distribution of by independent samples (scenarios) and enforces only the sampled constraints; its generalization theorem (Campi and Garatti, 2008) bounds the probability that the resulting decision violates a fresh constraint.
Enforcing all sampled constraints can still be costly: a few unusual scenarios may dominate the solution. A practitioner therefore often discards of the sampled constraints, optimally, greedily or at random, and re-solves. The question is what guarantee survives: the removed constraints were chosen by looking at the data, so the solution is biased towards points of higher risk. Campi and Garatti (2011) answered it with a bound that holds for every removal procedure. This mission formalizes that answer as it is presented in Chapter 3, Section 3.3 and Chapter 5, Section 5.3 of the textbook Introduction to the Scenario Approach (Campi and Garatti, SIAM/MOS 2018), together with its explicit corollary, Theorem 1.2. Applications include chance-constrained control, portfolio selection and prediction, where discarding scenarios trades a controlled amount of risk for a better cost.
A decision ranges over (in Lean, EuclideanSpace ℝ (Fin d)), with a closed convex domain and a linear cost . An uncertain parameter takes values in a measurable space with probability , and each determines a closed convex constraint set . The violation probability of a decision is
Given independent samples with joint law , the scenario program minimizes over . For a set of indexes, the program without the constraints in minimizes the same cost over ; its solution is written . A removal procedure selects, as a function of the whole sample, a set of indexes, and denotes the solution of the program without them. The procedure is required to output a solution that violates exactly the removed constraints (with probability one): a removed constraint that turns out to be satisfied is reinstated and another is removed. Two standing assumptions are used throughout: Assumption 3.4, that and every are convex and closed, and Assumption 3.6, that for every sample size and every sample the scenario program has exactly one solution.
For , under Assumptions 3.4 and 3.6, for every removal procedure and every ,
The bound depends on the problem only through , and on the removal procedure not at all. For it is Theorem 3.7.
Theorem 3.9 certifies every constraint-removal heuristic at once. Since the guarantee is the same for optimal, greedy and random removal, a user may pick the removal strategy purely for cost, and may inspect several values of before choosing, paying only a union bound over the values tried (Section 3.3). Theorem 1.2 turns the bound into an explicit rate: when is held fixed, the violation exceeds the empirical risk by a margin of order , only slightly worse than the rate for estimating the probability of a fixed event. The result also shows that the violation after removal concentrates around the target level, which is the basis of the book's comparison between sampling-and-discarding and simply using fewer scenarios (Example 3.10).
Theorem 3.9 is proved in the literature for general (Campi and Garatti, 2011); the textbook proves it for . To our knowledge no part of the scenario approach has a machine-checked proof. A formal development would supply the first verified version of the removal bound, a Lean treatment of solution maps of random convex programs, and reusable combinatorial and binomial-tail estimates.
The removed set is chosen after seeing the data, so the kept constraints are not an independent sample and Theorem 3.7 cannot be applied to directly. The argument must pass through all fixed index sets and account for the event that the removed constraints are violated; a plain union bound that ignores this event loses a factor and does not give (3.13). For a fixed index set, the probability that the removed scenarios are all violated involves the distribution of , which is only known to be dominated by a Beta law, so a stochastic-domination argument for the increasing function is needed. In general dimension the combinatorial constant comes from a sharper counting than the two-dimensional computation of Section 5.3, and that argument is in the cited paper rather than in the book.
Decisions live in EuclideanSpace ℝ (Fin d), samples of size are maps Fin m → Δ with law Measure.pi (fun _ => P) for a probability measure P, and the violation is the real number (P {δ | θ ∉ Θδ δ}).toReal. Events over samples are compared in ℝ≥0∞ with ENNReal.ofReal of the book's right-hand side. The removal procedure is an arbitrary map I : (Fin N → Δ) → Finset (Fin N) with (I ω).card = k, and θk is a map that, for every sample, solves the program without the constraints in I ω, and violates each of them with probability one. The following implicit hypotheses of the book are written as binders:
∀ᵐ ω ∂ℙ^N), the book's own hypothesis on p. 65, so (5.11) is an inclusion up to a null set as on the page; requiring the violation for every sample would be unsatisfiable for (on a sample with all equal a kept constraint coincides with a removed one) and would make the results vacuous;Theorem 1.2 is stated in the constraint formulation of Chapter 3, to which the book says it "straightforwardly generalizes" (p. 20), with the hypotheses of Theorem 3.9 from which Section 3.3.1 derives it. Eq. (5.14) and the closing display of Section 5.3 are stated for only, as in the book.
A trivializing formalization is excluded: the removal procedure is universally quantified, the solutions are exact minimizers rather than arbitrary feasible points, and the event is the strict ; a statement for one fixed rule, or with unconstrained, would be a different theorem.
A complete development needs: product measures and Fubini over Fin N → Δ, reindexing of the kept constraints as a sample of size , the Beta form of the binomial tail (the platform's binomial_upper_tail_eq_incomplete_beta is available), and stochastic domination for monotone integrands. Solution-map and violation infrastructure is shared with the sibling missions of this series. Contributions on any milestone, including the general- counting argument of the cited paper, are welcome.
The scenario approach turns an optimization problem under uncertainty into a finite, data-driven program: sample instances of the uncertain parameter, optimize against all of them, and certify how often the resulting design fails on a new instance. Its main guarantee (Theorem 3.7 of Campi and Garatti's Introduction to the Scenario Approach) bounds the probability of failure by a binomial tail in and in the number of optimization variables. To reach a failure level with confidence , the number of scenarios grows roughly like (Theorem 1.1 of the book). The product of and is what makes medium- and large-scale designs expensive: each scenario is one more constraint in the program that has to be solved.
FAST (Fast Algorithm for the Scenario Technique), introduced by Carè, Garatti and Campi in Operations Research 62 (2014), removes that product. It solves the program with a moderate number of scenarios and then, instead of re-optimizing, raises the returned cost level until it covers further scenarios. The book presents the algorithm and its guarantee, Theorem 8.5, in §8.3, and refers to the paper for the proof. This mission formalizes that guarantee.
Timeline:
Let be a measurable space carrying a probability measure , and let be a real loss of a decision under the uncertain parameter . As a standing assumption of the book, is convex for every .
Given scenarios drawn independently from , the scenario program (1.4) is
Its solution is and its optimal value . Assumption 3.6 requires that for every and every sample the solution exist and be unique. The pair has components, and is the number that enters every bound.
The risk (Definition 8.2) of a decision with cost level is
the probability that a new instance costs more than promised. It is the violation of the epigraphic constraint .
FAST takes independent scenarios. It solves (1.4) with the first of them, obtaining . In the detuning step it then sets
the smallest level that covers every scenario seen. The output is with .
For every ,
No relation between and is required. When the sum equals and the bound reads .
The first stage is an ordinary scenario program with scenarios. For ,
that is, is dominated by a distribution (recalled on p. 90).
For , makes the right-hand side of (8.5) at most (p. 95).
The result. Theorem 8.5 makes the guarantee of the scenario approach cheap to obtain. With (the book suggests ) and , the total number of scenarios is . This is additive in and rather than multiplicative, and the added scenarios cost only function evaluations, not a larger optimization. The price is suboptimality: is in general higher than the value a classical scenario program with the same confidence would return.
Formalizing it. The result is proved on paper, in the cited 2014 article; the book states it without proof. No part of the scenario theory has been machine-checked on this platform, as far as a search of the catalog shows. The mission produces a checked two-stage bound whose first stage is the loss-function form of Theorem 3.7, which is reusable by every mission of the series that works with program (1.4). The rule is an elementary but explicit sample-size certificate.
The obvious route treats the detuning step as a fresh scenario program with scenarios and applies Theorem 3.7 to it. That fails: is not the solution of that program, and Theorem 3.7 with scenarios gives a bound that is not of the product form (8.5). The level depends on all scenarios at once, including those that determined , and the map is monotone but need not be continuous, so the event is not a simple event about the new scenarios. Underneath the goal sits Theorem 3.7 itself, which is the main theorem of the book and whose proof occupies Chapter 5.
Lean representation:
EuclideanSpace ℝ (Fin n); the book's is written , never with natural-number subtraction.ω : Fin m → Δ with law Measure.pi (fun _ => P), and the same defines the risk. FAST draws one sample ω : Fin (N₁ + N₂) → Δ; its first stage is ω ∘ Fin.castAdd N₂.Finset.sup' over a nonempty index set. runs over all scenarios, not over the new ones only.(P {δ | c < ℓ ν δ}).toReal, with the strict inequality of Definition 8.2 and the strict event of (8.5). Probabilities of sample events are compared in ℝ≥0∞ through ENNReal.ofReal.νstar from samples to decisions, with the hypothesis that νstar ω₁ solves the program for every sample ω₁.Hypotheses the book leaves implicit, stated explicitly:
A formalization that bounds only the new scenarios is ruled out, because is defined as a maximum over all scenarios. So is one that takes as a free variable or drops Assumption 3.6: the goal is stated for the output of FAST as the book defines it.
A complete development needs the scenario program in loss form, product-measure conditioning on , and Theorem 3.7. The loss-form Theorem 3.7 is the reusable piece. Proofs of the milestones and of intermediate conditioning lemmas are welcome.
A retailer who restocks a perishable product every period faces the newsvendor problem: order too much and each leftover unit costs , order too little and each unmet unit of demand costs . If the demand distribution were known, the optimal order would be a quantile of it. In practice the distribution is unknown and has to be learned from sales data, and sales data are censored: when the shelf empties, the retailer records that demand was at least the stock level, not what demand actually was. What the retailer can observe therefore depends on what it ordered, which ties estimation and ordering together.
Huh, Levi, Rusmevichientong and Orlin (Oper. Res. 59(4), 2011) proposed a nonparametric answer. Each period, estimate the demand distribution from past censored sales with the Kaplan–Meier estimator of survival analysis (Kaplan and Meier, 1958) and order the estimated optimal quantile. They proved that the orders converge almost surely to the optimal set. Earlier data-driven newsvendor results either assumed uncensored demand (Levi, Roundy and Shmoys, 2007) or used stochastic approximation (Burnetas and Smith, 2000) and piecewise-linear cost approximation (Godfrey and Powell, 2001). A by-product of the analysis is a consistency theorem for the Kaplan–Meier estimator when the censoring levels depend on the past observations. Classical consistency results assume censoring independent of the data.
Demands are independent copies of a nonnegative integer-valued random variable on a probability space . Write . With , the critical ratio is . For the -quantile and the upper -quantile are
and is the newsvendor quantile, . Every integer order in minimises the expected one-period cost. The two quantiles coincide exactly when .
In period the retailer stocks , observes the sales and the indicator (: uncensored), and may depend only on earlier observations. From observations the Kaplan–Meier estimator of is
with a factor read as when its denominator is . The source writes it as a product over the sorted observations, with uncensored observations placed before censored ones at equal values. The two forms agree.
The KM-myopic policy with initial order orders . In each later period it orders
where is the estimator built from the past observations. When that set is empty (the largest past observation is censored and the estimate there still exceeds ), the policy orders twice the largest past observation. The convergence radius is .
In Lean, all of this sits in the namespace KMNewsvendor: survival, critRatio, quantile, upperQuantile, kmSurv, kmOrder (with kmSales, kmUncensored) and radius.
If and , then for almost every demand path there is with
This is the source's own "that is" reading of a.s., and it implies that display.
Items 4–6 and the goal carry the added hypotheses and (see Formalization scope).
The goal says that a policy which sees only censored sales, and assumes no parametric form for demand, eventually orders an optimal quantity on almost every sample path. Consequently its long-run average cost equals the optimal expected cost of a newsvendor who knows the distribution. Theorem 2 stands on its own as a statement about survival analysis: the Kaplan–Meier estimator stays consistent when censoring is adaptive, i.e. when each censoring level is chosen after seeing earlier outcomes, as in sequential experiments and learning algorithms. Lemma 1, a strong law along predictably chosen indices, is the probabilistic tool behind both.
The results are proved in the source. None is known to be formalized. Mathlib has the strong law for i.i.d. sequences (ProbabilityTheory.strong_law_ae) but nothing on Kaplan–Meier estimation, censored data or the newsvendor model. A complete development would give the first machine-checked analysis of an adaptive inventory policy and reusable Kaplan–Meier consistency results.
The observations are not i.i.d. The censoring level of each period is chosen from earlier data, so which demands are seen exactly is random and depends on the past. Classical consistency proofs for the Kaplan–Meier estimator assume independent censoring and do not apply. Mathlib's strong law applies to a fixed sequence, not to a subsequence whose indices are stopping times of the demand process. Showing that the selected demands are again i.i.d. with law is the heart of Lemma 1. The step from estimator consistency to order convergence then needs a self-reinforcing argument, since estimates are consistent only up to levels the policy keeps reaching. In the case of a non-unique optimum, the source's proof of Lemma 3 uses the law of the iterated logarithm, which Mathlib does not have.
Demands are D : ℕ → Ω → ℕ with Measurable, iIndepFun and IdentDistrib (D t) (D 0), under a probability measure (Lemma 1 takes real-valued demands, as in the source). Time is -based: Lean period is the source's period . The order of Lean period reads only the demands of periods . The policy is a deterministic function kmOrder r y₁ dem n of the demand path. The initial order , which the source leaves unspecified, is an explicit parameter. "Almost surely" is ∀ᵐ ω ∂μ, and "" is ∀ᵐ ω ∂μ, ∃ᶠ t in atTop, …. Predictability ("-measurable") is the Doob–Dynkin form: the variable equals a measurable function of the first coordinates. "" becomes integrability of . Theorem 2 is stated for every integer satisfying , because the source's maximum need not exist there.
Added hypotheses. As printed, Theorem 1, Lemma 2 (ii), Corollary 1 and Lemma 3 are false. If (positive probability when ), or if , then from the second period on every observation is and the policy orders forever, although whenever . For example, with uniform on and (the source's own §6.2 instance), . These four statements therefore assume and , and nothing else is added. Lemma 1, Theorem 2 and Lemma 2 (i) are stated as printed, for every . The policy is not modified: the variants of the source's §4 (a fictitious observation at a known upper bound, and similar) are different policies.
Trivializing readings are excluded. The quantiles are the least integers with the defining property, and the sets are nonempty because . The Kaplan–Meier estimator follows the source's tie-break, so it does not ignore censoring. Almost-sure and infinitely-often statements are not weakened to convergence in probability or to per-period probabilities.
Needed infrastructure: stopping-time subsequences of i.i.d. sequences, product-limit algebra for the grouped estimator, and a law of the iterated logarithm (or another route to Lemma 3). The first two are reusable well beyond this mission, and contributions to any of them are welcome.
Two-player turn-based stochastic games (2TBSGs) model a zero-sum contest on a finite graph with random transitions: in each state one player chooses an action, pays its cost, and a lottery chooses the next state. The minimizer and the maximizer both evaluate the total discounted cost. The model contains Markov decision processes (one player), simple stochastic games, mean-payoff and parity games (as limits or reductions), which makes it central to algorithmic game theory, verification and operations research. Shapley introduced discounted stochastic games in 1953 (PNAS).
The standard algorithm for solving them is strategy iteration, the two-player generalization of Howard's policy iteration (1960): improve player 1's strategy greedily against the best response of player 2, and repeat. Whether any algorithm solves 2TBSGs in strongly polynomial time was open for decades.
Timeline. Howard (1960) introduced policy iteration for MDPs. Rao, Chandrasekaran and Nair (1973) described strategy iteration for discounted stochastic games. Littman (1996) gave a polynomial but not strongly polynomial bound via value iteration. Ye (2011, Math. of OR) proved that policy iteration for discounted MDPs with a fixed discount factor is strongly polynomial, using the linear programming formulation of MDPs. Hansen, Miltersen and Zwick (2010, arXiv:1008.0530; J. ACM 2013) extended the bound to strategy iteration for 2TBSGs, where no LP formulation is available, and improved Ye's bound. Friedmann (2009) showed that without discounting, or with the discount factor as part of the input, strategy iteration can take exponentially many iterations.
A game has a finite set of states, split into the states of player 1 (the minimizer) and of player 2 (the maximizer), a finite set of actions of both players, and a discount factor . Each action has a source state , a probability distribution over next states, and a cost . Every state has a nonempty set of actions.
A positional strategy of player picks one action for every state ; a profile is a pair , viewed as a map . With and , the value vector
is the expected total discounted cost from each initial state. Vectors are compared componentwise. A profile is optimal when each strategy is an optimal counter-strategy against the other, from every initial state simultaneously. All optimal profiles share one value vector .
The Strategy-Iteration algorithm starts from a strategy of player 1. In round it takes an optimal counter-strategy of player 2, evaluates , and lets choose in every state an action minimizing over . Ties are broken in favour of . It stops at the first with .
For every game, every map returning optimal counter-strategies, and every run from any initial strategy, the termination index exists, is optimal, and
For a fixed this is iterations. The explicit constant is the paper's statement, and the goal states it rather than the form.
The milestone list follows the paper's lemma chain: Shapley's existence theorem (Thm 2.8); the linear-algebra form of values (Lemma 3.2); the modified costs and their properties (Lemmas 3.6, 3.7); the flux vectors (Lemmas 3.10, 3.12); the contraction of the value iteration operator and geometric convergence (Lemmas 4.2, 4.8); monotonicity, correctness and the rate of strategy iteration (Lemmas 5.1, 5.2, 5.3, 5.5); and the combinatorial core (Lemmas 6.2, 6.3, 6.4).
The result. The theorem gives the first strongly polynomial algorithm for 2TBSGs with a fixed discount factor. The iteration count depends only on , and , not on the bit length of the costs or probabilities. With the map is trivial and the theorem is the MDP bound for Howard's policy iteration, improving Ye's bound. Together with Friedmann's lower bounds, it settles the complexity of strategy iteration: strongly polynomial for a fixed discount factor, exponential otherwise.
Formalizing it. The result is proved on paper; none of it is formalized in Lean. A formal development produces a reusable matrix-based theory of finite discounted games: value vectors through Neumann series, modified costs as potential transformations, the min/max Bellman operator as a sup-norm contraction, and the optimality certificate. These are the tools of discounted MDP theory, stated here for two players.
The obvious argument for termination is that the values strictly decrease, so no strategy repeats. That bounds the number of iterations only by the number of strategies, which is exponential in . Value-iteration convergence gives a geometric rate for but no bound independent of the numerical data. What is needed is a combinatorial event: within every block of about iterations, some action leaves the strategy for good. Ye's version of this step used LP duality, which has no counterpart for two players, so the game-theoretic substitutes (flux vectors, modified costs) have to carry it. In Lean, a further difficulty is the bookkeeping of an algorithm with an oracle, a tie-breaking rule and a termination index.
TBSGStrategyIteration.Game): Fintype states and actions, S1 : Finset S (so is its complement), src, stochastic rows P, real costs c, and 0 < γ < 1; every is nonempty. The state set may be empty.Strat1 G, Strat2 G (positional, on the owner's states), Profile G = Strat1 G × Strat2 G.value G π is the tsum (always summable here). valueWith allows other cost vectors, for the modified values and the flux vectors (Definition 3.8, taken literally).S → ℝ, against every alternative strategy.‖·‖ on S → ℝ is Mathlib's sup norm. is written out as . is Real.logb (1/γ).IsRun): an infinite sequence with (a) greedy for , and (b) whenever is itself greedy. Clause (b) is Figure 1's "if possible ", and the paper's per-state tie-breaking rule implies it. Without it the algorithm may cycle. The oracle is an arbitrary map with the hypothesis that each is an optimal counter-strategy against . The number of iterations is the first with (IsTerminationIndex).Contributions welcome: the Neumann-series identity for (Lemma 3.1 as substrate), the optimality condition, and the counting argument of Theorem 6.5. The definitions are reusable for any finite discounted MDP or turn-based game mission.
Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds Palm calculus. Chapter 2 settles when a queue has a stationary regime. Chapter 3 is called simply Formulas, and it is what the first two chapters were for: it computes.
The pattern is always the same. A quantity of interest is observed two ways — from a clock fixed in time, and from an arriving customer — and Palm calculus converts between them. Little's law, the Pollaczek–Khinchin formula and the rate conservation principle are all instances.
Theorem 3.3.1 (p.211) is the one that says when the two views coincide.
This classical result of queueing theory states, in rough terms, that if the arrival point process is Poisson, operational characteristics of the system computed just before arrival times and at arbitrary times are the same (Poisson Arrivals See Time Averages). Some care must be exercised in the application of this principle, and we now give a precise statement, in the
θ_t-framework.
E⁰_A[f(Z(0))] = E[f(Z(0))] (3.3.1)
for every F_t-predictable, flow-compatible {Z(t)} and every non-negative measurable f,
whenever A admits the constant F_t-intensity λ; and, under ergodicity,
lim_N (1/N) Σ_{n=1}^N f(Z(T_n)) = lim_T (1/T) ∫_0^T f(Z(s)) ds . (3.3.2)
The "some care" is the word predictable. PASTA is false without it: an arrival that changes the
state it then observes does not see the time average, and that is exactly what predictability —
measurability for the F_t-predictable σ-field, generated by the sets (a,b] × A with A ∈ F_a —
rules out.
The hypothesis is the constant F_t-intensity, not "A is Poisson". By Watanabe's theorem the two
are equivalent, but that equivalence is a remark on the page and not part of this theorem.
§3.4 derives formulas from conservation equations. Applying the rate conservation principle of
Chapter 1 to Y(t) = e^{iuW(t)} in a GI/GI/1/∞ queue gives Takács' formula
iu E[e^{iuW(0)}] = λ E⁰_A[e^{iuW(0−)}] (E[e^{iuσ_0}] − 1) + iu(1 − ρ) , (3.4.44)
an identity between a stationary expectation and a Palm expectation of the workload just before
an arrival. One substitution turns it into a closed form — and that substitution is PASTA. When the
arrivals are Poisson, E⁰_A[e^{iuW(0−)}] = E[e^{iuW(0)}], and
E[e^{iuW(0)}] = iu(1 − ρ) / ( iu − λ(Ψ_σ(u) − 1) ) , (3.4.45)
the Pollaczek–Khinchin characteristic function formula. The most quoted formula in single-server queueing theory is one application of this mission's goal theorem.
§3.1 carries Little's formula to fluid queues. Lemma 3.1.1 is the set identity that turns the fluid workload into an integral against the arrival measure — the same two instants described from the server's side and from the arrivals' side.
§3.2 applies Campbell's formula to rare events. Lemma 3.2.1 gives a closed form, in a
countable-state Markov chain, for the mean time to make an excursion to a rare set and return; its
two expressions count the same cycle rate from the two ends. Theorem 3.2.1 generalizes
Keilson's asymptotic equivalence to a stationary θ_t-compatible process, replacing cycles by
thinnings of the entrance processes of two disjoint sets.
§3.5 applies the stochastic intensity integration formula to a superposition of on-off fluid sources. Lemma 3.5.1 identifies a conditional expectation with a Palm expectation through Papangelou's theorem — the mean workload while a source is idle equals the mean workload that source sees when it wakes. Lemma 3.5.2 measures the gap between the two Palm expectations of the workload taken with respect to a source's start process and its fluid process.
Nothing here is on the platform or in Mathlib. The nearest platform item,
queueing_general_littles_law, is Stidham's deterministic sample-path law; its own docstring
disclaims probability, expectation, stationarity, ergodicity and FIFO. Baccelli's L = λW is the
Palm identity for a stationary ergodic marked point process, derived from the inversion formula
(1.2.25) — an identity between an expectation under P and a Palm expectation under P⁰_N, not a
pathwise limit. Different framework, different hypotheses, and neither implies the other.
Mathlib has filtrations and adapted processes but no predictability in the form this chapter needs, and no stochastic intensity.
(3.3.1) is an equality in [0, ∞] for every non-negative
measurable f. (3.3.2) asserts that, P-almost surely, both averages converge in [0, ∞] to one
common limit, so both limits exist. Predictability is measurability for the predictable σ-field
P(F_t) of p.55. The concrete form Z(t,ω) = v(t, θ_t ω) of (1.8.1) is not used as the hypothesis,
because for a general history it is strictly weaker. The hypothesis is the constant F_t-intensity,
E[A(a,b] | F_a] = λ(b − a), and not "A is Poisson".u, and for
u ≠ 0 respectively. Their hypotheses are the page's: σ_n is independent of W(T_n−) under
P⁰_A, E⁰_A[e^{iuσ_0}] = E[e^{iuσ_0}], P(W(0) = 0) = 1 − ρ, and ρ < 1. The workload is a
measurable, flow-compatible solution of Lindley's equation. (3.4.45) adds PASTA's hypotheses for
{W(t−)}, and it asserts that its denominator is non-zero.E_α R. The chain is irreducible, F is non-empty,
and hitting times are counted from time 0.E⁰_{F_n(→A)}[τ(F_n)] · Λ_n → 1. Its hypotheses are the section's standing ones: P is
flow-invariant, {X(t)} is flow-compatible, and A and every F_n are regular and disjoint.P⁰_{A^i} is the Palm probability of the random measure A^i, and the workload is
the stationary solution of the fluid-queue equation. Lemma 3.5.1 is an identity in [0, ∞].
Lemma 3.5.2 assumes that E⁰_{A^i}[W(0)] and the expectation defining C_i are finite.A formalization that makes Palm probability an opaque measure with the formulas as axioms, or that weakens predictability to adaptedness, trivializes this mission or makes it false, and is out of scope.
Chapter 2 of Baccelli and Brémaud's Elements of Queueing Theory asks when a queue has a stationary regime. §§2.1–2.4 answer it for the single-server and multiserver queues by Loynes' monotone construction. §§2.5 and 2.11 answer it for the general object those constructions are instances of: a stochastic recurrence
W_{n+1} = h(W_n, ξ_n),
driven by a sequence {ξ_n} compatible with an ergodic shift θ. Two questions arise, and this
mission is about both.
§2.5.3 treats the finite-state case. An ergodic transition matrix on E = {1, …, r} has a
stationary law π, and the classical way to sample it is to run the chain and wait. That gives a
sample whose law converges to π and is never equal to it.
Coupling from the past (Propp and Wilson, 1996) does better. Run one chain from every state,
all sharing a single array {ξ_k(i)} of i.i.d. uniforms indexed by time and current state, started
further and further in the past. Once two chains meet they stay together, so eventually all r
coalesce before time 0 — and Theorem 2.5.1 says the common value they reach has the
distribution π exactly. Theorem 2.5.2 makes it practical: if the updating function
preserves a partial order with a least and a greatest state, and a single uniform sequence drives
every chain, the two extremal chains funnel all the others and their coalescence suffices.
Neither theorem is a statement about a program. Each says that a random variable is almost surely
finite, and that another has a distribution equal to π.
§2.5.4 treats the general case, through Borovkov's idea. An event A_n is renovating of length
m when, on it, W_{n+m} = Φ(ξ_n, …, ξ_{n+m-1}) — the sequence's value m steps ahead forgets
where it came from. Theorem 2.5.3 turns a condition on how often renovating events occur into
the existence of a finite stationary solution Z with Z ∘ θ = h(Z, ξ), and into strong
backwards coupling: W_n ∘ θ^{-n} is not merely convergent to Z but equal to it after a
finite random index.
Corollary 2.5.1 makes the limit independent of the initial condition — one stationary regime,
reached from every starting point. Theorem 2.5.4 is the converse: for ℝ₊^K-valued recurrences
with a constant initial condition, strong backwards coupling produces renovating events. So the
method characterises stability rather than merely detecting it.
§2.11 treats the multidimensional case, where the state is a vector and the natural models are
monotone and homogeneous. Theorem 2.11.1, due to Crandall and Tartar, is the key that unlocks
it: under homogeneity, monotone and non-expansive are the same property. That is what puts these
models within reach of Kingman's subadditive ergodic theorem, and Theorem 2.11.2 collects the
payoff — asymptotic growth rates γ̄ and γ_ exist, both almost surely and in L¹, and do not
depend on the initial condition.
Queueing folklore has a rule of thumb for the stability of an open network: saturate the queues
fed by the external stream, measure the departure intensity µ of the saturated system, and
declare the network stable when λ < µ. The book is careful that this saturation rule "does
not hold for all systems".
Theorem 2.11.3 (p.166), "the main result on the stability region", proves it for Monotone-Homogeneous-Separable networks:
If lim Z_{[-n,0]} → ∞ a.s., then λ γ(0) ≥ 1. If λ γ(0) > 1, then lim Z_{[-n,0]} → ∞ a.s.
Here γ(c) is the growth rate of the network fed by the scaled process cN, so c = 0 places
every arrival at the origin: γ(0) is exactly the saturated system's rate, and µ = γ(0)⁻¹.
Two implications, with a gap between ≥ 1 and > 1 that the book leaves open — as it leaves open
the critical case ρ = 1 of Loynes' theorem. Closing it would assert more than is proved.
Nothing here is on the platform or in Mathlib. There is no coupling from the past, no theory of
renovating events, and no Crandall–Tartar theorem. Order/Hom/* has monotone maps and
Topology/MetricSpace/* has LipschitzWith 1, which is the right ambient notion for
non-expansiveness in the sup-norm, but the equivalence between them under homogeneity is absent.
(P⁰, θ) is
ergodic and {ξ_n} is compatible with θ. The relation Z ∘ θ = h(Z, ξ) holds P⁰-a.s.{W_n^{[C]}}, the sequence its proof on p.119 builds the renovating
events for. The page prints {W_n^{[0]}} in the conclusion, and that version is false. Corollary
2.5.1 uses the renovating condition of (2.5.14), W_{n+m} = Φ(ξ_n, …, ξ_{n+m-1}), where the
page prints W_n.ℝ^K-valued random initial condition Y, under the book's linear lower bound
E[X_n^{[0]}] > −Cn.T_0 = 0,
T_n ∘ θ = T_{n+1} − T_1, ξ_n ∘ θ = ξ_{n+1}, E⁰τ_n = λ^{-1}, E⁰Z_n < ∞. The map X
satisfies (2.11.16) (it depends only on the points and marks in the index window) and the four
framework assumptions for every point process. γ(0) is the a.s. limit of
Z_{[-n,-1]}(0·N)/n. Dropping the marks would reduce the theorem to deterministic service,
and dropping the link between the points and θ makes the second implication false. Neither
is done.≥ 1 and > 1 left
open.The Euclidean projection of a vector onto the simplex — the nonnegative vectors whose entries sum to a fixed radius — is a subroutine of first-order methods whose iterates must stay probability vectors or nonnegative budgets: portfolio optimization, multispectral unmixing, image segmentation, constrained least squares and many machine-learning models. Through a classical reduction the same routine projects onto the ball, the feasible set of -constrained sparse regression. Because the projection is called once per iteration, often on vectors of millions of entries, the exact algorithms that compute it have been studied for half a century.
A short timeline. Held, Wolfe and Crowder (1974) gave the sorting-based method: sort the entries, find the number of active entries, compute a threshold. Michelot (1986) gave a variable-fixing method that repeatedly averages the surviving entries and discards those below the average, without sorting. Kiwiel (2008) and Duchi, Shalev-Shwartz, Singer and Chandra (2008) popularized partition-based methods with expected linear time. Condat (Math. Program. 2016) proposed a Gauss–Seidel-like variant of Michelot's method that updates the threshold after every entry read instead of after every full pass; it is exact, needs no sorting and is empirically the fastest of the family. Its correctness is argued in one paragraph of the paper; the argument has not been machine-checked.
Fix an integer , a vector and a real . The simplex of radius is
and the ball of radius is . The Euclidean projections are and , where is the Euclidean norm. In Lean, "" is the predicate IsSimplexProjection a y x: and for every ; IsL1Projection is the same for .
The projection onto has the thresholding form for a unique real , so computing amounts to computing .
Condat's Proposed Algorithm (Fig. 2 of the paper) keeps a list of candidate entries, an auxiliary list and a running value :
In Lean this is the total function condatAlgorithm a (List.ofFn y), returning .
For every , , , if the algorithm returns then
No assumption is made on the order or distinctness of the entries of .
The goal certifies a routine used inside many optimization solvers: for every real input, the algorithm returns the exact projection, and the reported is the size of its support. The milestones are reusable facts about simplex and -ball projection in their own right — the thresholding characterization (Proposition 2.2), the bracket and monotonicity of the root function, and the two reductions between and — on which the correctness of the sorting, heap, partition and Michelot methods reviewed in the paper also rests.
All of these results are proved on paper (Propositions 2.1 and 2.2 are classical and cited by the author; the algorithm's correctness is argued in Sect. 3). None of them is formalized in Mathlib, which has the standard simplex (radius 1, as a set) and the abstract Hilbert-space projection theorem but no thresholding formula and no projection algorithm. The mission turns the paper's argument into a checked proof about a transcription of Fig. 2 that can be read line by line against the figure.
The algorithm mixes three different updates of — an incremental mean when an entry is added (with counted before the addition in step 2.1 and after it in step 3.1), a reset to , and a removal update — and a loop whose termination depends on strictly decreasing. The paper's argument relies on invariants that are stated informally: equals outside the reset, never exceeds , is a sub-multiset of that contains every entry larger than once the cleanup pass is done, and at every division. The first idea, to argue directly that the first pass already finds , fails: in general it does not, and the reset of step 2.3 temporarily breaks the mean invariant, which is exactly why step 3 exists. The thresholding characterization itself needs the optimality conditions of a constrained quadratic problem, available in Mathlib only as the abstract variational inequality for projections onto closed convex sets.
Vectors are Fin N → ℝ, and the squared Euclidean distance is the explicit sum (Mathlib's norm on Fin N → ℝ is the sup norm and is not used). Every theorem assumes exactly the paper's standing hypotheses and . Projections are predicates, not chosen minimizers. The algorithm reads as the list ; lists keep repeated values; step 4's loop is a do-while encoded by well-founded recursion on , so the function is total without an iteration bound and termination is part of the definition. is compared with the number of indices with . The only placeholder is the empty input (), which the paper excludes and every theorem excludes by hypothesis.
A formalization in which the algorithm's output is defined as "the of Proposition 2.2", or as a sorting method or Michelot's method instead of Fig. 2, or in which the loop is cut off by a fuel bound, would make the goal trivial or different; the definition here transcribes Fig. 2 step by step, and the goal quantifies over every input.
A complete development needs: the thresholding characterization via first-order optimality conditions on ; elementary facts about the piecewise-linear function ; and loop invariants for the three passes of the algorithm, stated on lists with multiplicity. The simplex and -ball facts are reusable for any later mission on projection algorithms (sorting, heap, partition, Michelot). Contributions welcome: proofs of any milestone, lemmas relating List.ofFn sub-multisets to index sets, and invariant lemmas for the individual steps of Fig. 2.
Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory builds a calculus for stationary queues. Chapter 2 asks the prior question: when is there a stationary queue at all?
The G/G/1/∞ queue is one server at unit rate, infinite waiting room, fed by a stationary marked
point process {(T_n, σ_n)} — arrival epochs and required service times. Its workload W(t), the
service still owed by the server, obeys Lindley's equation between arrivals:
W(t) = (W(T_n−) + σ_n − (t − T_n))⁺, t ∈ [T_n, T_{n+1}). (2.1.6)
Nothing in that equation says a solution exists on the whole line, let alone a stationary one. The
answer is a sharp criterion in the traffic intensity ρ = λE⁰_A[σ_0].
Theorem 2.1.1 (p.80), which the book calls "the fundamental result of stability". Under
ρ < 1 there is a unique finite workload process on all of ℝ, compatible with the flow, and
it is given explicitly by the Loynes supremum
W(0) = sup_{n ≤ 0} ( T_n + Σ_{i=n}^{0} σ_i )⁺ , (2.1.12)
with W(T_n−) = 0 for infinitely many negative and infinitely many positive n (2.1.13). If
ρ > 1 there is no finite stationary workload process at all.
Each half earns its place. The supremum is what "the Loynes construction" means: look back from the
origin, take the work brought by customers n, …, 0 less the time −T_n since elapsed, and
maximise over how far back you look. The ρ > 1 half is what turns ρ < 1 from a sufficient
condition into a criterion. The critical case ρ = 1 is an explicit non-result in the book — there
"may or may not" be a stationary workload — and is deliberately absent from the statement.
§2.2 proves the theorem by Loynes' monotone scheme on the Palm space, and two of its steps are worth stating in their own right.
Lemma 2.2.1 (p.87) is the uniqueness engine: a non-negative, a.s. finite Z with
Z − Z∘θ ∈ L¹(P⁰) has E⁰[Z − Z∘θ] = 0. Applied to the difference of two stationary solutions, it
forces that difference to be invariant, and ergodicity then forces it to be zero.
Theorem 2.2.1 (p.90) runs the argument backwards. Its section is titled "Queueing Proof of the Ergodic Theorem", and it is exactly that: the queueing construction yields the pointwise ergodic theorem, in the ratio form
lim_n ( Σ_{i=0}^n σ∘θ^{-i} ) / ( Σ_{i=0}^n τ∘θ^{-i} ) = E⁰[σ]/E⁰[τ], P⁰-a.s.
Mathlib has the mean (von Neumann) ergodic theorem and no pointwise one, so this is absent substrate rather than a restatement.
The multiserver queue (§2.3). With s servers and the least-loaded-server rule, the state is
the ordered workload vector obeying the Kiefer–Wolfowitz recurrence, and the criterion becomes
E⁰[σ] < s E⁰[τ] (Theorem 2.3.1, p.93). Here uniqueness fails: p.94 exhibits a two-point space
with a whole interval of stationary solutions. What survives is that the solution set is bracketed
— M_∞ is minimal, and V^∞_∞ is the largest finite solution (Theorem 2.3.2, p.95).
Coupling (§2.4). Theorem 2.4.1 (p.99) is what "reaches the stationary regime" means: if a
sequence couples with a θ-compatible one, then the law of its whole shifted trajectory converges
in variation to the stationary trajectory's. The proof is one inequality,
|P̃_{X,k} − P̃_{Z,k}| ≤ P(N > k), and the finiteness of the coupling time.
The fluid queue (§2.7). Theorem 2.7.1 (p.131) replaces customers by two θ_t-compatible
random measures, the arrivals A and the service capacity C, and recovers the Loynes supremum
W(t) = sup_{u ≤ t}(A_{u,t} − C_{u,t}) under λ < µ — as the minimal solution, the book
claiming no uniqueness here.
ρ = λE⁰_A[σ_0] takes values in [0, ∞], so an input with E⁰_A[σ_0] = ∞ has ρ = ∞ and
falls under the non-existence half rather than being read as ρ = 0.E⁰[σ]/E⁰[τ] of Theorem
2.2.1, the threshold s E⁰[τ] of Theorem 2.3.1, and the fluid supremum (2.7.7).θ_t-compatible workload processes; maximality
in Theorem 2.3.2 is among measurable finite solutions; the coupling time of Theorem 2.4.1 is a
random variable. A formalization that dropped the explicit supremum, or the ρ > 1 half, would
trivialize the goal and is ruled out.None of it is on the platform or in Mathlib. The nearest platform item,
single_server_queueing_convergence_of_subcritical, presupposes a stationary workload and proves
two-time finite-dimensional convergence to it; Theorem 2.1.1 constructs that workload, proves it
unique, gives it in closed form, and adds the non-existence half. Different conclusion, different
generality, different Mathlib revision.
Chapter 1 of Baccelli and Brémaud's Elements of Queueing Theory has two halves. The first builds
Palm calculus from the Matthes definition of P⁰_N and reaches the Swiss army formula. This
mission is the second: §§1.6, 1.8 and 1.9, which supply the two things the rest of the book runs
on.
§1.6 states, in its own words, "the ergodic theory results to be used later in this book". Five of them, and the book proves none: Birkhoff's pointwise ergodic theorem in discrete (Theorem 1.6.1) and continuous time (Theorem 1.6.4), Kingman's sub-additive ergodic theorem (Theorem 1.6.2), and the extremal characterizations of ergodicity in both settings (Theorems 1.6.3 and 1.6.5) — ergodicity is exactly the impossibility of splitting an invariant probability into two distinct ones.
They are quoted, but they are not decoration. Kingman's theorem is what produces the asymptotic
growth rates of Theorem 2.11.2 and the constant γ(c) on which the saturation rule rests.
Birkhoff's theorem is what makes the time average in PASTA's (3.3.2) a well-defined object, and
what the fluid Loynes theorem invokes for lim_{u→−∞}(A_{u,0} − C_{u,0}) = −∞.
None of the three analytic ones exists in Mathlib. Analysis/InnerProductSpace/MeanErgodic is the
mean (von Neumann, L²) theorem, not almost-everywhere convergence, and there is no sub-additive
ergodic theorem at all. The platform has neither.
§1.8 introduces the stochastic intensity: a point process N admits the (P, F_t)-intensity
{λ(t)} when E[N(a,b] 1_A] = E[(∫_a^b λ(t)dt) 1_A] for A ∈ F_a. Around it sits the notion of a
predictable process — one measurable with respect to the strict past.
Theorem 1.8.1 is the structural fact that makes predictability usable. For the internal history of a marked point process, every predictable process has the concrete form
Z(t, ω) = v(t, θ_t ω), v(t, ·) F_{0−}-measurable. (1.8.1)
That is why mission IV can take this form as PASTA's hypothesis rather than constructing a predictable σ-field: Theorem 1.8.1 says nothing is lost.
Theorem 1.8.2 (p.61), §1.8.4, Watanabe's characterization of Poisson processes. For a
history F_t = F_t^N ∨ G and a G-measurable, locally integrable {λ(t)}, if N admits the
F_t-intensity {λ(t)} then N is a G-conditional Poisson process:
E[ e^{iuN(a,b]} | G ∨ F^N_a ] = exp{ (e^{iu} − 1) ∫_a^b λ(t) dt } . (1.8.12)
A stochastic intensity that carries no information beyond G forces the process to be Poisson
conditionally on G, with the compensator as the parameter — and the conditional characteristic
function is the exact Poisson one, not an approximation. With G trivial and λ constant this is
the ordinary Poisson process, which is the equivalence Remark 3.3.1 of Chapter 3 invokes to explain
the name PASTA. The book: "This result plays a role in queueing theory, especially for proving
that some streams in a queueing network are or are not Poissonian."
§1.9 asks whether the stochastic intensity is the same under P and under P⁰_N — whether the
two probabilities describe the same dynamics. Theorem 1.9.1 says yes, on ℝ₊: the same process
{λ(t)} serves both.
Theorem 1.9.2 is Papangelou's theorem, and it is the deepest statement of the section: N
admits a stochastic intensity if and only if P⁰_N ≪ P on F_{0−}, and then
λ(t) = (μ ∘ θ_t)λ with μ the Radon–Nikodým derivative. A dynamic property and a static one turn
out to be the same thing.
Theorem 1.9.3 is Mecke's characterization: N is Poisson exactly when P ≡ P⁰_N on
F_{0−}. The view from a point of the process and the view from a deterministic instant agree on
the strict past precisely when the process has no memory. It follows in one line from the two
theorems before it.
Four of the five missions in this series import the Chapter 1 substrate; this one adds the two pieces they need from its second half — ergodic theory and the stochastic intensity. Nothing here is on the platform, and Mathlib has filtrations and adapted processes but no predictability in this form, no stochastic intensity, no pointwise ergodic theorem and no Kingman.
Every result is stated in the book's strength, with the book's standing definitions as binders.
A discrete flow is a bijective, measurable, P⁰-preserving map (p.46); a continuous flow is jointly
measurable in (t, ω) (p.3, clause (a)). A history compatible with the flow satisfies
θ_t F_s = F_{s−t} (p.57), and an F_t-intensity is a non-negative, measurable, locally
integrable, adapted process (p.58). The limits of Theorems 1.6.1, 1.6.2 and 1.6.4 are asserted to
exist; Kingman's constant h̄ lies in ℝ ∪ {−∞} and is identified with
inf_n (1/n) E⁰[h_n], the means being extended reals so that E⁰[h_n] = −∞ is not read as 0.
Theorems 1.6.3, 1.6.5, 1.9.2 and 1.9.3 are equivalences, and Theorem 1.9.2 carries the closed form
λ(t) = (μ ∘ θ_t)λ with μ = dP⁰_N/dP on F_{0−}. The goal's conclusion is the exact conditional
characteristic function (1.8.12); a formalization that only asserted some conditional Poisson law,
or conditioned on G alone, would not be this theorem.
A public facility (a fire station, a hospital, a server) is to be placed on a road network, and the people it serves report their own locations. When the planner wants to minimise the distance to the farthest user (the minimax or egalitarian objective, in the sense of Rawls), each user has an incentive to misreport so as to pull the facility towards themselves. Mechanism design without money asks which location rules make truthful reporting a dominant strategy, and how much of the optimal objective such rules must give up. Procaccia and Tennenholtz (EC 2009) introduced this approximation viewpoint for points on a line; Schummer and Vohra (J. Econom. Theory 2002) characterised the strategyproof deterministic rules on networks.
Alon, Feldman, Procaccia and Tennenholtz (Math. Oper. Res. 2010) study the minimax on general networks. Choosing a fixed agent's location (dictatorship) is strategyproof and loses at most a factor 2 on any network. On a circle they give a randomized strategyproof mechanism with ratio . On trees a simple randomized mechanism achieves . This mission is about their matching negative result: on trees, no strategyproof randomized mechanism does better than .
A network is a metric space whose points are the vertices of a graph and every point inside its edges; the distance is the length of the shortest path. There are agents; a location profile is . A randomized mechanism maps each profile to a probability distribution over , the location of the facility. An agent at bears the cost , and the maximum cost of for the profile is
The mechanism is strategyproof (SP) if no agent can lower its own cost by reporting another point: for all , and , . The benchmark is the best deterministic location, .
The network of the theorem is the tree : an edge of length joins two roots and ; below each root hangs a complete -ary tree of depth whose edges from level to level have length . The profiles used are the paper's : puts agents on each root, and moves the agents at a chosen left vertex on level to its children, equally.
For , , with , and every SP randomized mechanism on for agents, there is a profile with and
The paper states the bound as ; the displayed form is what its proof establishes (p. 526), and , turn it into the form.
The result. Dictatorship already achieves ratio on every network, and on trees the best known SP mechanism improves this only to . Theorem 4.1 shows that this is essentially optimal: randomization, which buys a factor on the circle, buys almost nothing on trees once the tree is allowed to branch widely. It separates two natural network classes by their strategyproof approximability, and the paper notes that trees of bounded branching factor escape the construction, which leaves that class as the open case.
Formalizing it. The result is proved in the paper and has no machine-checked proof. The mission produces a checked lower bound for all SP randomized mechanisms on a continuous network, quantified over arbitrary probability measures and arbitrary deviations, together with a reusable model of facility location with strategic agents on a metric network and an explicit construction of a weighted metric tree.
The bound holds against every mechanism, so no mechanism is analysed: the only handle on is the SP inequality, applied along a chain of unilateral deviations whose length is the number of agents moved. The chain must be organised so that the bound on one expected distance survives each level of the tree, and the pointwise geometric inequality on the tree must be turned into a bound on expectations under an arbitrary distribution that may put mass inside edges. The final comparison needs the exact optimum of a specific profile and exact arithmetic on the resulting ratio. Restricting the facility to vertices, or assuming the mechanism is anonymous or continuous, would change the class of mechanisms and is not allowed.
HardTree m k, the tree realised isometrically inside (one coordinate per edge), with the subspace metric (equal to shortest-path length on the embedded tree) and the Borel σ-algebra. Edge interiors are points of the space. Vertices are vertex s w for a side s and a word w over Fin m.Fin n; a mechanism is any function (Fin n → HardTree m k) → ProbabilityMeasure (HardTree m k); strategyproofness quantifies over every profile, agent and point of the tree. No measurability, anonymity or continuity of is assumed. cost and mc are Bochner integrals of bounded continuous functions; is optMc, an infimum over all points.A facility — a fire station, a server, a meeting point — must be placed on a network, and every user of the network reports where they are. When the planner cares about the worst-off user, the objective is the minimax: minimize the largest distance from the facility to a user. The reports are private information, so a user may misreport a location to pull the facility towards itself. Approximate mechanism design without money, proposed by Procaccia and Tennenholtz (2009), asks how close to optimal a mechanism can stay when no user ever benefits from lying.
On a line the picture is complete. A deterministic strategyproof mechanism cannot beat ratio 2 for the minimax, and a randomized one cannot beat 3/2. The left-right-middle (LRM) mechanism attains 3/2 (Procaccia and Tennenholtz, 2009). Networks with cycles are harder: the extreme agents that LRM needs do not exist on a circle. Alon, Feldman, Procaccia and Tennenholtz (2010) give a randomized strategyproof mechanism on the circle whose ratio is again 3/2, which is best possible. They also show that on trees no randomized strategyproof mechanism does much better than dictatorship. This mission formalizes the circle result, Theorem 3.1 of that paper.
The circle has circumference one and carries the arc-length distance . There are agents; agent has a location , and is the location profile. A randomized mechanism maps each profile to a probability distribution over , the location of the facility. Agent 's cost and the maximum cost of are
A mechanism is strategyproof if for every profile , every agent and every misreport , . It is a -approximation for the minimax if for every .
The agents are on one semicircle if a closed arc of length contains all of them. The antipodal point of is . Mechanism 3.1 works as follows:
In Lean the circle is AddCircle (1 : ℝ), a profile is x : Fin n → AddCircle (1 : ℝ), the
deviated profile is Function.update x i x', and the definitions are cost, mc,
IsStrategyproof, IsApproximation, OnSemicircle, lrm, rc and mech31 in the namespace
StrategyproofMinimax.Circle.
that is, for all , , and ,
The constant is the paper's own and is optimal.
The four deviation lemmas A.2, A.6, A.8 and A.9 together are the strategyproofness half of the goal.
The theorem closes the randomized minimax question on the circle: the ratio 3/2 matches the lower bound that already holds on a line, so cycles cost nothing once randomization is allowed. This contrasts with the tree result of the same paper, where no randomized strategyproof mechanism beats . Mechanism 3.1 is also an example of something that is not true in general: combining two strategyproof mechanisms by a case split on the profile usually breaks strategyproofness at the boundary between the cases, and here it does not. Any characterization of randomized strategyproof mechanisms on networks, an open problem the paper raises, has to account for such hybrids.
The result is proved on paper, in the paper's Appendix A. It has no machine-checked proof. A
formalization also produces reusable pieces: facility-location mechanisms and their costs on a
metric space, LRM on an interval, and cost computations for finitely supported distributions on
AddCircle.
A deviation can move the profile across the boundary between the two regimes: from one semicircle
to not one semicircle, or back. Strategyproofness of LRM and RC separately therefore does not give
strategyproofness of the hybrid; the four regime-crossing cases need separate arguments, which
compare an LRM cost with an RC cost directly. RC's outcome depends on every agent's antipodal point,
so a single deviation removes one cut point and inserts another; its effect on the deviator's cost
has to be controlled across the whole partition. Even the semicircle-to-semicircle case is not
inherited from the line: the deviation can change which semicircle is used, and with it which
agents are extreme. On the formal side, every cost is an integral against a finitely supported
measure on AddCircle, and the case analysis runs through arc-length distances that wrap around.
Measure (AddCircle 1). lrm, rc and mech31 are explicit finite sums of
Dirac masses whose weights sum to one. cost and mc are Bochner integrals of continuous
bounded functions against these finite measures, so they are always the true expectations.∃ c, ∀ i, ‖x i - c‖ ≤ 1/4: a closed arc, so agents spread over exactly
a half circle are on one semicircle.Fin.snoc x y.lrm fixes it: it uses
the semicircle centred at for the least index for which this centre covers all agents.Contributions welcome: API for integrals against finite sums of Dirac masses on AddCircle,
lifting of arcs of length at most to intervals of , and LRM strategyproofness on
an interval.
Anosov flows are the model of uniformly hyperbolic, chaotic continuous-time dynamics: a nonsingular vector field on a closed manifold is Anosov when the tangent bundle splits as , with uniformly contracted and uniformly expanded by the derivative of the flow. They are structurally stable, so one can hope to classify them up to topological equivalence. In dimension three this classification is far from complete: it is not known which closed 3-manifolds carry Anosov flows, nor how many inequivalent Anosov flows a given manifold can carry.
The classical examples — suspensions of hyperbolic toral automorphisms and geodesic flows of hyperbolic surfaces — are rigid (Plante; Ghys). Non-algebraic examples were built by Franks–Williams (a nontransitive Anosov flow, 1980), Handel–Thurston, Goodman, Fried, Bonatti–Langevin, Fenley, Barbot and others. Several of these examples glue together neighbourhoods of hyperbolic sets along their boundaries. Béguin, Bonatti and Yu (Geom. Topol. 21 (2017)) turned this into a general theory, and used it to answer questions of Katok and of Barbot–Fenley.
A plug is a compact 3-manifold with boundary and a nonsingular C¹ vector field transverse to . The boundary splits into the entrance boundary (where points inwards) and the exit boundary . The maximal invariant set consists of the points whose orbit stays in for all times. The plug is hyperbolic if is a hyperbolic set with one-dimensional strong stable and strong unstable bundles. The entrance lamination and the exit lamination are one-dimensional laminations of the boundary surfaces. The plug has filling MS laminations when every component of (and of ) is a strip: a disc whose accessible boundary consists of two leaves asymptotic to each other at both ends.
A diffeomorphism is a strongly transverse gluing map if and are transverse and cut into squares with sides alternately on leaves of the two laminations. Gluing then gives a closed manifold with an induced vector field . Two triples and are strongly isotopic if they are joined by a continuous path of such data.
Theorem 1.5 lets one build Anosov flows on closed 3-manifolds by gluing hyperbolic plugs. Proposition 1.6 gives a combinatorial criterion for the result to be transitive. Together they answer a question of Katok (Theorem 1.9) and questions of Barbot and Fenley on manifolds with several hyperbolic JSJ pieces supporting transitive Anosov flows (Theorem 1.13). They also show that transitive Anosov flows admit no fully canonical decomposition into finitely many transverse tori (Theorem 1.15). The results are proved in the source paper. None of them is formalized, and Mathlib has no theory of hyperbolic sets for flows, stable manifolds or laminations. A formal proof therefore needs a substantial amount of reusable smooth dynamics.
The glued vector field is generally not hyperbolic: perturbing the gluing map can create solid tori of parallel periodic orbits. The difficulty is to choose the gluing map (and the vector field within its topological equivalence class) so that cone fields on are mapped into themselves by the return map. The return map is the composition of the crossing map of the plug with the gluing map. Contraction and expansion must therefore be controlled simultaneously along two transverse invariant foliations. The paper achieves this after reducing to plugs with an affine Markov partition. The naive approach — fixing and trying to verify hyperbolicity — fails in general (Question 1.4 of the paper remains open).
EuclideanHalfSpace 3 with a structure; closed manifolds are compact, Hausdorff and BoundarylessManifold, and connected where the paper's statements concern a single manifold. Orientability is given by an atlas with positive Jacobians.flowMap X t x is when the orbit is undefined.Interior-point methods are, together with the simplex method, the standard algorithms for linear programming, and the primal–dual path-following method is the form in which they are implemented in most solvers. Unlike the simplex method, it is a one-phase method: it can start from any point whose primal and dual variables are strictly positive, feasible or not, and drives infeasibility and complementarity to zero simultaneously. The question every user of such a method eventually asks is how fast these three measures of non-optimality decrease.
Chapter 18 of R. J. Vanderbei, Linear Programming: Foundations and Extensions (4th ed., Springer 2014, DOI 10.1007/978-1-4614-7630-6) defines the method from scratch (Fig. 18.1, p. 273) and proves a rate statement, Theorem 18.1 (pp. 277–279): as long as the step lengths stay bounded below and the iterates stay bounded, the primal and dual infeasibilities decay geometrically, and so does the complementarity, at a slower rate. This mission formalizes that theorem and the one-step identities and estimates it is built from. It is the fifth mission of a series on the book; the missions are independent of each other.
Let be a real matrix, , . The primal problem is to maximize subject to , ; the dual is to minimize subject to , . A primal–dual point is a quadruple with , ; it is strictly positive, , if every component is. Write for the diagonal matrices of and for the all-ones vector. The norms are and .
At a point the three measures of progress are the primal infeasibility , the dual infeasibility , and the complementarity . Fix parameters and . One iteration of the method, from a strictly positive point, sets , takes any solution of the Newton system
computes the step length
(with when all ratios vanish), and moves to . This is Fig. 18.1 with the shorter step (18.7) the book adopts for its analysis. Along a sequence of iterates, superscripts denote the quantities at the -th iterate, and is the step length computed there.
If , is real, and for all one has , , , then for all , with ,
The one-step identities for the infeasibilities, (18.8) and (18.9); the one-step complementarity estimate
under ; and the recursion (18.11). Two unnumbered statements complete the picture: every iteration has and keeps the point strictly positive, and at any strictly positive point the duality gap satisfies (§18.5.3).
Theorem 18.1 separates the convergence question for the path-following method into two parts: a rate statement that holds whenever steps stay long and iterates stay bounded, and the remaining question of when those two conditions hold. It also explains an effect seen in practice: the infeasibilities fall by the factor per iteration while the complementarity, and hence (by the duality-gap estimate) the gap , falls only by . The book stresses that the result is partial, because it does not show that the step lengths remain bounded away from zero; that requires modifications of the method and of the starting point that the book does not carry out.
All statements here are proved in the book. The mission's contribution is a machine-checked version, with the constant of the complementarity bound made explicit. Neither Mathlib nor the platform contains a formal proof of this theorem or a formalization of the infeasible-start primal–dual iteration it concerns; the platform's existing path-following result concerns a different, feasible-start short-step method in equality form.
The infeasibility identities are linear and follow from the first two Newton equations. The complementarity is where the Newton system linearizes a bilinear equation, so the new complementarity contains a second-order term that has no sign. Bounding it requires relating the size of the step to the size of the current iterate through the specific form of the step-length rule (18.7); the rule (18.6) of Fig. 18.1, with signed ratios, does not give such a bound. The multi-step estimate then couples two geometric sequences with different rates, and keeping the constant independent of the horizon is what makes the statement non-trivial.
Vectors are Fin n → ℝ and Fin m → ℝ, is a Matrix (Fin m) (Fin n) ℝ, and points and step directions are a structure PDPoint m n with fields x w y z. The sup-norm is ⨆ j, |v j| (the maximum; 0 for an empty vector). The step length is written with the explicit case when all ratios vanish, since Lean's r / 0 = 0 would otherwise give . An iteration is a relation between the current point, a step direction and the next point: the current point is strictly positive, the direction is some solution of the Newton system (uniqueness, which the book asserts under a full-rank assumption, is not assumed), and the next point is current direction. The hypotheses , (pp. 272–273) are stated in every theorem; is an arbitrary real number and a natural number. As in the book, the hypotheses of Theorem 18.1 range over , so the iteration from index is part of the data.
Explicit constants. The book's Theorem 18.1 asserts only "there exists a constant ". Because is fixed, that existential is satisfied trivially by , and a statement with would be empty. The goal therefore uses the constant the book's proof establishes (p. 279, last display): . Eq. (18.11) is stated with the book's written out.
The formalization needs only finite sums, dot products and matrix–vector products from Mathlib; the definitions of the iteration are reusable for other analyses of the same method (Chapters 19–22 of the book). Contributions are welcome for each milestone separately.
Minimum-cost network flow problems are the largest special class of linear programs met in practice: transportation, distribution, assignment, communication and electric networks, facility location and financial planning all reduce to moving material along the arcs of a directed network from supply nodes to demand nodes at least cost. Chapter 14 of R. J. Vanderbei's Linear Programming: Foundations and Extensions (4th ed., Springer 2014, DOI 10.1007/978-1-4614-7630-6) develops the network simplex method, and closes with two structural facts that explain why this class is special: simplex bases are spanning trees of the network, and a network problem with integer supplies has integer basic solutions. Vanderbei then uses integrality to prove a classical theorem of combinatorics, König's theorem on regular bipartite graphs. Chapter 15, §5 treats the maximum-flow problem on the same objects and proves the Max-Flow Min-Cut Theorem.
The combinatorial results are older than linear programming. D. König proved in 1916 that every regular bipartite graph has a perfect matching (Math. Ann. 77). The Max-Flow Min-Cut Theorem is due to Ford and Fulkerson (1956, Canad. J. Math. 8) and, independently, Elias, Feinstein and Shannon (1956). The integrality of network bases is the total unimodularity of incidence matrices, known since the 1950s (Hoffman and Kruskal, 1956).
A network has a finite set of nodes and a set of directed arcs . Node carries a supply (negative values are demands) with , and arc carries a cost . The flow on arc is the decision variable. The node–arc incidence matrix has in the column of an entry in row , in row , and elsewhere. The network flow problem (14.1) is
A flow satisfying is balanced; a balanced flow with is feasible. Paths ignore arc directions; the network is connected if every two nodes are joined by a path, which is assumed throughout Chapter 14. A spanning tree is a set of arcs that, on all of and without directions, is connected and has no cycle. Fixing a root node and deleting its row gives the matrix . A set of arcs is a basis if its columns form an invertible square submatrix of , and a basic feasible solution is a feasible flow vanishing off some basis.
For maximum flow, a source , a sink and finite upper bounds are given; all and an extra arc of infinite capacity is added. A feasible flow satisfies , and flow balance. A cut is a node set with , , and its capacity is .
If girls and boys are such that every girl knows exactly boys and every boy knows exactly girls (knowing being symmetric), then there is a bijection from girls to boys with
both extrema attained.
The goal is independent of the network definitions in its statement; the milestones are the book's route to it (14.1, 14.2) and the chapter's other duality theorem on the same objects (15.8, 15.1).
König's theorem is the base case of matching theory: it gives perfect matchings in regular bipartite graphs, hence edge colourings of bipartite graphs with colours, and via Birkhoff–von Neumann-type arguments the decomposition of doubly stochastic matrices. The Integrality Theorem is the reason assignment, transportation and shortest-path problems can be solved as linear programs without an integrality constraint. Theorem 14.1 is the correspondence the network simplex method is built on. Max-Flow Min-Cut is the prototype of combinatorial min–max theorems.
All four theorems are classical and proved. This mission adds machine-checked versions in the book's own formulation: the incidence matrix with Vanderbei's sign convention , bases as square submatrices of with a chosen root, and maximum flow as a circulation through an added return arc. The platform already has network integrality, a tree-solution characterisation and max-flow min-cut in the Bertsimas–Tsitsiklis formulation and a Keller–Trotter max-flow statement; none is stated in this form, and Mathlib has Hall's marriage theorem but no regular-bipartite corollary.
The combinatorial content is small; the difficulty is in the passage between matrices and graphs. Theorem 14.1 needs both directions: the book shows that a spanning tree gives a triangularisable, hence invertible, submatrix and leaves the converse (independent columns form a spanning tree) as an exercise, which requires showing that any cycle, including a pair of antiparallel arcs, yields a linearly dependent set of columns and that acyclic arcs span. The book's proof of König's theorem applies the Integrality Theorem to the girl–boy network, which need not be connected, while Chapter 14 assumes connectedness throughout: the statement of 14.2 does not apply to it verbatim. The step "a feasible problem has a basic optimal solution" is also used and is not stated in the chapter.
Fintype with decidable equality; arcs are a Finset (N × N), so parallel arcs are excluded as in the book, and IsNetwork excludes loops. Flows are real functions on ordered pairs; only their values on arcs matter.Fin n, knowing is one relation between girls and boys, and is a hypothesis: the book's proof divides by , and for the claim is false. No connectedness is assumed.A formalization of the goal as a matching of size in some larger graph, or with the degree conditions on one side only, would be a different theorem; the conclusion is a bijection between exactly the girls and the boys using only acquainted pairs.
Useful infrastructure, reusable beyond this mission: the incidence matrix and its total unimodularity, the undirected graph of an arc set. Proofs of König's theorem through Hall's theorem (Mathlib Finset.all_card_le_biUnion_card_iff_exists_injective) are welcome alongside the book's route.
Countable-state Markov chains are the standard model of queues with unbounded buffers, but any numerical computation of their long-run behaviour works on a finite state space. The usual remedy is truncation: restrict the chain to a finite set and redistribute the probability of leaving back into it. Whether the steady state probabilities and average costs of the truncated chains converge to those of the original chain depends on how that probability is redistributed. Gibson and Seneta studied this question for the stationary distributions of chains without costs (Gibson and Seneta, J. Appl. Prob., 1987). Sennott extended it to chains with costs and expected first passage costs (Sennott, Adv. Appl. Prob. 29, 1997; ZOR Math. Meth. Oper. Res. 45, 1997), and used it as the basis of the approximating sequence method for average-cost Markov decision chains (Sennott, 1999, Chapter 8). This mission covers Appendix C, Sections C.4–C.5 of the 1999 book, the Markov-chain results that the book's average-cost approximation theorems use.
A Markov chain with costs on a denumerable state space has transition probabilities with and a finite nonnegative cost at each state. For a set and a start , is the first passage time to . The taboo probability is the probability of moving from to in steps with no intermediate state in . The expected visits count the visits to at times . The mean first passage time is , infinite when is missed with positive probability. The first passage cost is . A state is positive recurrent when , and the steady state probability is . On a positive recurrent class the average cost is . The chain is standard when and for every . Such a chain has one positive recurrent class with , and every other state is transient.
An approximating sequence (AS) consists of increasing nonempty finite sets with and, for each , a chain on with the same costs and transition probabilities . The quantities of are written , , and . An AS is conforming (for a standard ) if, for large , is unichain with in its positive recurrent class, and and for all . It is conforming on if and on .
An augmentation type approximating sequence (ATAS) keeps the original probabilities inside and redistributes the probability of each excluded target according to an augmentation distribution on :
It sends excess probability to if every is concentrated on .
For a standard chain and a finite nonempty ,
and if it is also conforming on . No rate of convergence and no constants are involved, and need not contain .
The result. Conformity is the hypothesis under which the book's approximating sequence method works for average-cost queueing control (Chapter 8). The method computes optimal policies for finite truncations and passes to the limit. That argument needs the first passage times and costs to a distinguished state to converge along the chains induced by fixed policies. Propositions C.5.2 and C.5.3 turn this analytic requirement into conditions on the truncation scheme that can be checked in practice: send the overflow to a fixed finite set, or to states from which reaching is no more expensive. Examples C.4.4 and C.4.7 of the book show that an arbitrary approximating sequence can fail. The limit of the steady state probabilities can be a strict multiple with . First passage costs can converge to the wrong value even when the steady state probabilities converge.
Formalizing it. The results are proved in the book, some in abbreviated form ("the proof for the costs is similar and is omitted"). The Prove2Me library had no statement on truncation or augmentation of countable Markov chains when this mission was drafted (September 2026). A formalization supplies the omitted cost arguments, makes the passage between bounds and limits in explicit, and produces a reusable library of first passage quantities for countable chains.
The lower bounds of Propositions C.4.2 and C.4.5 are the routine part. The difficulty is the matching upper bound: in , a first passage that leaves is restarted elsewhere, which can lengthen it without bound. Taking limits termwise in the first passage equation fails, because no dominating function is available and mass can escape to infinity. Example C.4.4 exhibits exactly this. Unichain structure is also not automatic: may have several recurrent classes, or a recurrent class not containing , and ruling this out is part of the conclusion rather than an assumption.
The Lean development works in SennottDP.ChainASM. A chain is a structure MC S with P : S → S → ℝ≥0∞, ∑' j, P i j = 1 and C : S → ℝ≥0. Theorems assume [Countable S] [Infinite S], matching the book's denumerable state space. Taboo probabilities, expected visits, , , and are defined as sums in . is infinite whenever is missed with positive probability. The average cost is the of the Cesàro cost averages.
An AS is a structure carrying , the finite sets (as Finset S) and . is built as an MC on the subtype of , and a set is read in as . Quantities of are lifted to functions of and of states of with the value where they are undefined ( or a state outside ). For fixed states this affects finitely many , and all statements are limits, s or eventual equalities. All convergence is in . The conformity predicate includes the standing assumption that is standard. The positive recurrent class of a standard chain is the communicating class of .
A trivializing formalization is excluded: the AS of Example C.4.4, whose positive recurrent class excludes , is not conforming under these definitions. The ATAS predicate requires the augmentation distributions to be probability distributions and to reproduce exactly by (C.27).
A complete development needs first passage decompositions for countable chains, the renewal-reward identity , and dominated and Fatou-type limit theorems for sums (the book's Appendix A). The first passage library and the lifted-quantity conventions can be reused by the average-cost approximation chapters. Contributions of intermediate lemmas are welcome, especially the finite-state unichain facts of Section C.3 and the identities of Propositions C.1.4 and C.2.2.
Proposition C.5.5 (lower Hessenberg chains, from Gibson and Seneta) is stated in the book without proof and without naming the distinguished state, and is not included.
Chapter IX of von Neumann and Morgenstern's Theory of Games and Economic Behavior asks when a game played by many participants is really several separate games played side by side. The authors' motivation (41.1) is methodological: the general theory of the -person game becomes unmanageable as grows, and one way to gain insight into large games is to isolate classes of games that can be analysed exactly. The first such class consists of games whose players fall into groups that have no dealings with each other — the book's example is the internal economies of two countries whose connections are disregarded (41.2.4). Such a game is the composition of its constituents, and the question of the chapter is how to recognise a composite game from its characteristic function alone and how far a given game can be decomposed.
The answer (§43) is a structure theorem. The groups of players that can be split off form a Boolean algebra of sets; its atoms, the minimal splitting sets, form a partition of the set of players, the decomposition partition ; and every splitting set is a union of blocks of . The book remarks (41.3.3) that the splitting condition (41:7) is exactly Carathéodory's criterion of measurability, transported from measures to characteristic functions. The mission formalizes §43, together with the criterion (42:G) of §42 on which it rests.
Let be a finite set of players. A characteristic function is a real number for every subset (every coalition, including the empty set and ). Write . From 42.4.1 on the book works in the domain of constant-sum games, whose characteristic functions are, by (42:D), exactly the functions satisfying
For with complement , the game is decomposable with respect to and if there are constant-sum games on the players and on the players with for all — formula (41:3). The -constituent is the game on with for (41:4).
A splitting set (43.1) is a satisfying (41:6),
The game is indecomposable if and are its only splitting sets (43.3.1). A minimal splitting set is a splitting set none of whose proper subsets is splitting (43.3.2), and is the system of all minimal splitting sets. The game is inessential (42:F) if it is strategically equivalent to the zero game, i.e. for all , for some reals (the transformation (42:5)).
For every satisfying (42:6:a)–(42:6:c):
The goal combines the partition property and the characterization of all splitting sets; it is the book's own summary of §43.3 and does not presuppose that is a partition.
In attack order: the criterion (42:G) (decomposability (41:6) (41:7)); the closure properties (43:A) (complements), (43:B) (, ), (43:C) (intersections and unions); (43:D) (splitting sets of a constituent) and (43:E) (a constituent is indecomposable iff its set is minimal); (43:F), (43:G) separately; (43:I) (a minimal splitting set is disjoint from, or inside, any splitting set); the restatement (43:H*) ( splits iff every block of lies inside or outside ); and the two extreme cases (43:J) ( = all singletons iff the game is inessential) and (43:K) ( iff the game is indecomposable).
The decomposition partition is canonical: every constant-sum game splits uniquely into indecomposable constituents, and (43:E) identifies them as the constituents on the blocks of . The two extreme cases (43:J), (43:K) show that inessentiality and indecomposability are opposite ends of one scale. Chapter IX uses this structure in §§44–47, where solutions of decomposable games are related to solutions of their constituents ((46:A)–(46:I)); a formal decomposition partition is the prerequisite for that later work, and a candidate follow-up mission.
The results are classical and proved in the book. The mission's contribution is a machine-checked version: a formal definition layer for splitting sets of a set function on a finite set, the Boolean-algebra closure, and the atomic decomposition. The combinatorial core — that the sets satisfying a Carathéodory-type additivity condition form a Boolean algebra of a finite set, whose atoms partition it — is reusable outside game theory (for instance for finitely additive decompositions of set functions). No machine-checked version of these results is known to exist; they are formalized here for the first time as far as a search of the platform shows.
The individual steps are elementary, but the obvious argument for the key closure property (43:C) fails: to show that is splitting one cannot simply add the identities (41:6) for and for , since a pair , is not of the form those identities control, and may be nonempty — the book's footnote on p. 354 singles out overlapping splitting sets as the case its proof is really about. Likewise (43:D) is not a tautology: that a set self-contained within a self-contained set is self-contained in the whole game has to be proved (footnote 1, p. 355). Formally, the main work is bookkeeping of set identities and the passage between subsets of (players of the constituent) and subsets of .
ι with decidable equality (the book's ; in Chapter IX players are also named ). Coalitions are Finset ι, and are the complement Sᶜ in , and is a function Finset ι → ℝ.IsConstantSum), the chapter's domain from 42.5.3 on ("in the remainder of this chapter we will continue to consider constant-sum games", p. 353). is arbitrary: the statements are not restricted to zero-sum games, which would be a weaker special case. (43:K) additionally assumes nonempty ([Nonempty ι], the book's ); every other statement holds without it. (43:E) assumes , since the book's constituent is a game and has at least one player.↥J, ↥Jᶜ; the -constituent is restricted to subsets of ↥J. Sums of sets are unions; "disjunct" is Disjoint.decompositionPartition v is the set of minimal splitting sets; that it is a partition is proved, not assumed. An aggregate of minimal splitting sets is a finite family A, its sum A.sup id; the empty aggregate gives .Finset ι and their atoms, which would shorten (43:F)–(43:H).Consider the classical error-correcting problem. An input vector (the plaintext) is encoded as by a coding matrix with , and an unknown, arbitrary vector of errors corrupts the result, so that only is observed. Can be recovered exactly, and by an algorithm whose running time is polynomial in ? Candès and Tao (2005) answer both questions at once: if a matrix annihilating satisfies a restricted orthonormality condition, then is the unique solution of the convex program , which is a linear program, whenever at most entries of are corrupted, whatever their positions and values. Read for the matrix alone, the same theorem says that minimization (basis pursuit) returns the sparsest solution of an underdetermined linear system. That statement is the mathematical core of compressed sensing, and the restricted isometry constants introduced in this paper became the standard tool of the field.
Timeline. Donoho and Huo (2001), followed by Elad–Bruckstein, Donoho–Elad and Gribonval–Nielsen, proved the equivalence of and minimization for matrices formed by concatenating two orthonormal bases, for sparsity of order , through incoherence. Candès, Romberg and Tao (2004) and Candès and Tao (2004) obtained recovery with overwhelming probability for random matrices at sparsity of order . Donoho (2004) showed for Gaussian matrices that a constant, unspecified fraction of nonzero entries can be tolerated. The present paper (December 2004, published 2005) gives a deterministic sufficient condition, , valid for every matrix, and specializes it to Gaussian matrices with explicit numerical values of the tolerable fraction. Later work, for instance Candès (2008) with the condition , sharpened the sufficient condition; those later results are not part of this mission.
Let be a real matrix with columns , and let be the linear span of these columns. For an index set and real coefficients , write . A vector is supported on when for all ; with this convention is just the product . Norms are the Euclidean norm and the norm .
Definition 1.1. For an integer , the -restricted isometry constant is the smallest quantity such that
for all of cardinality at most and all real coefficients . The -restricted orthogonality constant is the smallest quantity such that
for all disjoint with and . The paper writes for . These numbers measure how far the columns of are from an orthonormal system when only linear combinations of at most columns are considered.
The two optimization problems are
A vector is the unique minimizer of one of these problems when it is feasible and every other feasible vector has a strictly larger objective value.
Let be a real matrix of full rank with , and a real matrix with . Let satisfy
If where is supported on a set of size at most , then is the unique minimizer of .
Let satisfy (1.10) for , and let be supported on a set with . Then is the unique minimizer of with .
Theorem 1.5 is the companion of Theorem 1.4 for the decoding problem, and the mission's milestones are the four lemmas the paper proves on the way: Lemma 1.2 (the numbers control the numbers), Lemma 1.3 (uniqueness of sparse representations under ), and the two dual sparse reconstruction properties, Lemma 2.1 ( version) and Lemma 2.2 ( version).
The result. The guarantee is deterministic and uniform: one condition on , checkable in principle from the matrix alone, ensures that a single linear program recovers every sufficiently sparse vector, with no probability of failure. In the decoding reading, a fixed fraction of the ciphertext can be corrupted arbitrarily and the plaintext is still recovered exactly by convex optimization. The paper shows in its Section 3 that Gaussian matrices satisfy (1.10) with overwhelming probability at explicit values of , and in Section 5 that the same hypothesis yields near-optimal recovery of compressible signals from few measurements; both are consequences of the deterministic core formalized here.
Formalizing it. The theorems are proved in the paper, and no machine-checked proof of them exists. Prove2Me holds a formalization of a different restricted-isometry sufficient condition taken from a textbook (HighDimProb.SparseRecovery.rip_implies_exact_recovery); it uses a different definition of the isometry constant and a different hypothesis, so nothing there can be reused as is. This mission produces the definitions of and exactly as in Definition 1.1, the dual-certificate lemmas, and the two theorems, in a form that later missions on compressed sensing can import. The probabilistic Theorem 1.6, Lemma 3.1 and Corollary 1.7, and the compressible-signal Theorem 5.1, are not targets: see the scope section for why.
The whole proof rests on a dual certificate: a vector with for and for . Given such a , the argument of Section 2.2 is a short chain of inequalities. The first idea every newcomer has is ; this interpolates the signs on and, by restricted orthogonality, its inner products off are small in an sense, but not in the sense required. That is exactly Lemma 2.1: the bound holds only outside an exceptional set of at most indices. Lemma 2.2 removes the exceptional set by an infinite alternating iteration, prescribing values on the previous exceptional set while keeping the values on fixed, and summing a geometrically convergent series.
Two points deserve attention from solvers. First, the paper's proof of Lemma 2.2 prescribes values on sets of size up to () at each step, while the per-step factors it quotes, , are what Lemma 2.1 gives for a set of size ; a proof of the printed constant in (2.4) has to account for this, and the hypothesis of Theorem 1.4 leaves room for a proof with slightly worse per-step factors. Second, Lemma 2.1 is printed with in its bound on the exceptional set, while the inequality (2.3) its proof establishes gives ; the mission states the lemma with , which coincides with the printed form in the case used by Lemma 2.2.
Matrices are Matrix (Fin p) (Fin m) ℝ; a coefficient vector on is a vector in Fin m → ℝ supported on the finite set , and is F.mulVec c. The Euclidean and norms and the inner product are explicit finite sums, so every statement can be checked by hand against the paper. is the span of the columns.
The constants and are the infimum of the set of nonnegative (resp. ) satisfying the defining inequalities for all admissible sets and coefficients. This set is nonempty, closed and bounded below, so the infimum is attained and is the paper's smallest quantity; on the paper's domain the smallest such quantity is nonnegative, so the extra clause only fixes a harmless value in degenerate cases such as . The definitions are total in , and each theorem carries the paper's domain conditions (, and , or as needed) as explicit hypotheses. The hypotheses are satisfiable, since a matrix with orthonormal columns has , so none of the statements is vacuous.
"Unique minimizer" is a strict inequality against every competitor. "Full rank" for the matrix with is injectivity of ; both are standing assumptions of the paper's Section 1.1 and appear as hypotheses of Theorem 1.5. In Lemma 2.1, "a constant depending only on " is a positive function of the real number , quantified before all other data.
Out of scope, with the reason for each: Theorem 1.6 refers to a threshold "given in Section 3.5", which the paper does not contain, and to "overwhelming probability" with unspecified constants; Lemma 3.1 is proved only for and "large enough", with an unspecified threshold and an term quoted from the literature; Corollary 1.7 rests on Theorem 1.6; Theorem 5.1 has an unspecified constant and is explicitly not proved in the paper. A future mission can add these once precise statements are fixed.
Contributions that are welcome: proofs of the four milestone lemmas and of the two theorems; reusable lemmas on the attainment and monotonicity of the constants, on the Gram matrix and its inverse under , and on the duality inequality of Section 2.2. Statements that weaken the hypotheses (for instance to ) belong to a separate mission.
In a Walrasian pure exchange economy, agents trade a fixed stock of commodities, and a price vector is a general equilibrium when aggregate excess demand vanishes. Existence of equilibrium (Arrow–Debreu, 1954) says nothing about how prices reach it. The classical tâtonnement model of Samuelson (1947), , is not derived from any optimization principle, and Scarf (1960) gave economies in which it is not globally stable; see also Smale's survey Dynamics in General Equilibrium Theory (JSTOR 1817235) and the chaotic tâtonnement examples of Bala–Majumdar (JSTOR 25054664).
Lindgren (doi:10.3390/analytics1010003) proposes instead that the economy as a whole chooses a price path by dynamic programming: it minimizes a running cost combining a quadratic transaction cost for price changes and the agents' aggregate minimal expenditure. From the resulting Hamilton–Jacobi–Bellman (HJB) equation the paper derives an evolution equation for the price velocity and a condition under which the value function acts as a Lyapunov function: the equilibrium is approached when price adjustments are large enough. This mission formalizes those derivations.
There are commodities and agents. Prices are vectors , and the paper's implicit summation is written . Agent has an expenditure function (minimal cost of reaching a fixed utility level), and the market weighs agents with constants ; the aggregate expenditure is
The economy controls the price velocity and minimizes the cost functional (eq. (7))
whose value function is . The Hamiltonian (eq. (8)) is
the optimal policy (eq. (9)) is , and the HJB equation (eq. (10)) reads
Here always denotes the gradient with respect to prices. Shephard's lemma identifies the Hicksian demand of agent with . For the stability analysis the paper runs time forward, which reverses the sign of the HJB equation: .
If is and solves the time-reversed HJB equation, and the price path follows the optimal policy , then on any interval on which
the function is strictly decreasing; if moreover , it is strictly positive on .
The paper's contribution is the claim that price dynamics derived from an optimization principle are nonlinear and only conditionally stable, with stability requiring sufficiently fast price changes; the author connects this to volatility clustering in financial time series. The derivations in the paper are formal calculations with the regularity of left implicit. Formalizing them pins down exactly which smoothness assumptions each step needs (for instance, eq. (12) uses equality of mixed partial derivatives, hence a value function), and which facts are imported from outside (the HJB equation itself, Shephard's lemma). The resulting statements are reusable calculus facts about HJB equations with quadratic control cost.
Each step is a short computation on paper; the formal difficulty is in the calculus infrastructure: partial derivatives of functions on , symmetry of second derivatives, the chain rule along a curve, and turning a pointwise negative derivative into strict monotonicity on a closed interval. The HJB equation is taken as a hypothesis on rather than derived from the definition of the value function, because the paper asserts it without proof and a rigorous derivation would require viscosity-solution theory.
All declarations live in the namespace LindgrenPriceDynamics. Prices are functions Fin l → ℝ; partial derivatives are Fréchet derivatives applied to standard basis vectors, and time derivatives are one-variable derivatives in the time argument. The value function is a function J : ℝ → (Fin l → ℝ) → ℝ whose joint regularity is stated for the uncurried map on ℝ × (Fin l → ℝ). The standing assumption is kept; positivity of and is not needed by any stated conclusion and is not imposed. Prices are not restricted to the positive orthant. The goal's large-velocity hypothesis is satisfiable (e.g. , , with small on a bounded interval), so the goal is not vacuous.
The mean value problem, also called Smale's mean value conjecture, was posed by Stephen Smale in 1981 in his study of the complexity of root-finding algorithms for polynomials (Smale 1981). For a real differentiable function the mean value theorem produces, between two points, a point where the derivative equals a difference quotient. For a complex polynomial no such point need exist on a segment, and Smale asked for a substitute in which the special point is a critical point of the polynomial (a zero of its derivative). Estimates of this kind control how far Newton-type iterations can move, which is where Smale's original interest came from. The problem appears in lists of unsolved problems in mathematics, including Smale's own list of problems for the next century.
No absolute constant is known that works in every degree.
Let be a polynomial with complex coefficients of degree , and write for its derivative. A critical point of is a complex number with ; since , is a nonconstant polynomial of degree , so has at least one and at most distinct critical points. Fix a complex number that is not a critical point, . For every critical point we then have , and the difference quotient
is well defined. The question is how small this quotient can be made, relative to , by choosing the critical point well.
For every complex polynomial of degree and every with there is a critical point of with
The same with replaced by ; the example shows this constant cannot be lowered.
The result itself. A positive answer gives a sharp, degree-independent mean value inequality for complex polynomials: for every non-critical point, some critical value is reachable along a chord whose slope is at most the local derivative. Bounds of this type feed into the analysis of Newton's method and of path-following root finders, and into the study of how critical values of a polynomial are distributed relative to its values. The conjecture is part of a family of open extremal problems on the geometry of critical points, alongside Sendov's conjecture.
Formalizing it. The goal and the optimal-constant form are open. The milestones are published theorems, none of which is known to have a machine-checked proof. Formalizing Smale's bound and Tischler's special cases would put the classical tools of the subject (critical points of polynomials, univalent function estimates, root location) on a formal footing that later attempts can reuse.
The obvious strategies control the quotient through one critical point at a time: for instance, bounding by integrating along the segment from to . Such estimates lose a constant factor that depends on how the critical points are spread out, and the known uniform arguments all pass through distortion theorems for univalent functions, whose constants lead to close to . Reaching requires using all critical points simultaneously, and no argument doing this in every degree is known. The equality case , in which every critical point is equally bad, shows that any successful argument must be sharp for polynomials with maximally symmetric critical configurations.
Polynomials are elements of ℂ[X] (Mathlib's Polynomial ℂ); the degree is natDegree, the derivative is Polynomial.derivative, evaluation is Polynomial.eval, and the roots of are the multiset P.roots (counted with multiplicity). A critical point is a c : ℂ with P.derivative.eval c = 0. The absolute value is the norm ‖·‖ on ℂ, and the constants and are computed in ℝ from the cast of natDegree.
Every statement assumes . This is the standard normalization and is essential in Lean: division by zero returns , so without it the choice would make the inequality trivially true whenever is itself a critical point. With the hypothesis, every critical point differs from and the quotient is a genuine difference quotient.
Crane's bound is stated as the existence, for each degree , of a constant strictly below that works for all polynomials of degree exactly ; this is equivalent to the best constant in degree being strictly below that value.
A complete development needs basic facts on critical points of complex polynomials (existence, the Gauss–Lucas theorem), and, for the classical bounds, results from the theory of univalent functions such as the Koebe quarter theorem and coefficient estimates. These are reusable well beyond this mission. Contributions of any milestone, of supporting lemmas, and of partial results in fixed small degree are welcome.
This mission formalizes N. Monod, Groups of piecewise projective homeomorphisms, Proceedings of the National Academy of Sciences 110 (2013) 4524–4527, doi:10.1073/pnas.1218426110: the groups of piecewise projective homeomorphisms of the line are non-amenable and have no free subgroups whenever .
The paper opens with the Banach–Tarski paradox and von Neumann's notion of amenability: "Tarski readily proved that amenability is the only obstruction to paradoxical decompositions. However, the known paradoxes relied more prosaically on the existence of non-abelian free subgroups. Therefore, the main open problem in the subject remained for half a century to find non-amenable groups without free subgroups" (p. 1). That problem, the so-called von Neumann conjecture, was answered by Ol'shanskii around 1980, with Tarski monsters. Monod's groups give "straightforward torsion-free counter-examples", "so simple that many additional properties can be established" (p. 1).
Monod's groups are close relatives of Thompson's groups: Thurston's model identifies Thompson's group with piecewise maps of the line with rational breakpoints (p. 2). Whether is amenable is a notorious open problem, and whether is amenable is Monod's Problem 12 (p. 2).
The projective line is OnePoint ℝ, on which acts through by Möbius transformations (mob, using Mathlib's action on OnePoint). For a subring of (A : Subring ℝ; is ⊥, is ⊤), P A is , the set of fixed points of hyperbolic elements (trace of absolute value greater than ).
A homeomorphism of is piecewise in with breakpoints in (IsPiecewiseProjOn A E f) when, off some finite subset of , it agrees near every point with a Möbius transformation from . Monod's (Gpp) is the group generated by the homeomorphisms piecewise in , with breakpoints anywhere, and (Hpp) is its stabilizer of (fixInf). For a subring , (G A) is the subgroup of generated by its elements that are piecewise in with breakpoints in (IsPiecewiseProj A), and (H A) is its stabilizer of ; is H ⊥. GRat is the subgroup of generated by its elements piecewise in with breakpoints in , and HRat its stabilizer of : the rational-breakpoint variants of and (p. 2).
Amenability is Garrido.IsAmenable (a finitely additive left-invariant probability measure on all subsets), and "no non-abelian free subgroup" is Chou.NoFreeSubgroupOfRankTwo; both are published definitions, in the bundles Garrido_Amenability and Chou_Classes. Co-amenable subgroups (IsCoamenable), inner amenability (IsInnerAmenable) and pointwise stabilizers (fixSubgroup), all on p. 3, are defined in the bundle in the same style.
A relation is amenable for a measure (IsAmenableRel μ R, p. 2) when it has a left invariant mean in the sense of Connes–Feldman–Weiss: a positive, unital map from bounded measurable functions on to functions on , linear up to -null sets and invariant under the partial transformations of . volP1 is the Lebesgue measure class on .
The goal is Theorem 1, "The group is non-amenable if " (p. 1), introduced as "the main result of this article". The proof (p. 2) passes to a countable dense subring of , compares the orbits of and on (Proposition 9), and concludes from two facts about measured equivalence relations: the orbit relation of an amenable group's action is amenable, and, by a theorem of Carrière and Ghys, the orbit relation of on is not.
The milestones are, in the paper's order: consists exactly of the elements of piecewise in with breakpoints in ; ; preserves orientation, is left-orderable and torsion-free; Proposition 9; the countable dense subring; the orbit relation of a measurable action of an amenable group is amenable; the orbit relation of on is not amenable (Carrière–Ghys, external); Lemma 13 and Theorem 14 leading to Theorem 2 ( has no free subgroups); Corollary 3; Proposition 6 (bi-orderability); Lemma 16, Proposition 7 (co-amenability of pointwise stabilizers), Proposition 15 and Proposition 5 (inner amenability); and Thurston's identification of the rational-breakpoint variants of and with and .
The result. Theorem 1 and Theorem 2 together make , for instance , a torsion-free counterexample to the von Neumann conjecture, with finitely generated examples (Corollary 3). The groups are concrete enough to carry many further properties (Propositions 5–7).
Formalizing it. Nothing on amenability of groups of homeomorphisms of the line, or on measured equivalence relations, is in Mathlib. Amenability and Følner's theorem are on this platform from Garrido I, the Banach–Tarski paradox from Garrido II, Brin–Squier's theorem from its own mission, and Thompson's and (CannonFloydParry, CannonFloydParry_T) from the Cannon–Floyd–Parry missions.
The algebraic half, Theorem 2 and Propositions 5–9, follows Brin–Squier and elementary dynamics on the circle. The analytic half is the passage through measured equivalence relations in the proof of Theorem 1. The mission defines amenability of a relation as Connes–Feldman–Weiss do, by an invariant mean valued in , which is the form under which an amenable group's orbit relation is amenable without extra set-theoretic hypotheses. The step taken from the literature, that the orbit relation of on is not amenable for countable and dense, rests on Carrière–Ghys's theorem and on Zimmer's theory of amenable actions (Adams–Elliott–Giordano). The milestone is proved (Monod.not_isAmenableRel_mob) by an elementary route that needs neither: a ping-pong argument in that contradicts an invariant mean directly.
OnePoint ℝ and acts through Matrix.SpecialLinearGroup (Fin 2) A; since acts trivially the orbits are those of .OnePoint ℝ, each defined as the subgroup generated by the maps the paper describes; the milestones state that is exactly its set of such maps and that .volP1).This mission formalizes Geoghegan's conjecture that Thompson's group is not amenable, in the form stated by Cannon, Floyd and Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. (2) 42 (1996), §4, p. 227 (doi:10.5169/seals-87877), together with the landmark results of the literature on the question.
A discrete group is amenable when it carries a finitely additive, translation-invariant probability measure on all of its subsets. Groups containing a non-abelian free subgroup are not amenable, and the question whether every non-amenable group contains one (the von Neumann problem) made Thompson's group the first natural candidate for a counterexample: it contains no non-abelian free subgroup, and it is not elementary amenable. Geoghegan conjectured in 1979 that is not amenable; several announced solutions in each direction did not survive. In 2026 OpenAI released a proof that is not amenable, with a Lean formalization; adapted to this mission's definitions, it is the solution of the goal.
Timeline.
Let UI be the unit interval . Thompson's group (CannonFloydParry.F) is the group, under composition, of the order-preserving homeomorphisms of that are piecewise linear with finitely many breakpoints, every breakpoint a dyadic rational and every slope a power of . It is generated by two elements and finitely presented (Cannon–Floyd–Parry, Corollary 2.6 and Theorem 3.4).
A mean on a set is a function from the subsets of to with , for disjoint , and . A group is amenable (Garrido.IsAmenable G) when it carries a mean with for all and , where . This is equivalent to the definition Cannon, Floyd and Parry give on p. 227, whose means take values in .
The milestones use four further notions, defined precisely in the definitions item and in their own statements:
The question was open until 2026. OpenAI's proof of the conjecture (see the timeline), transferred to CannonFloydParry.F and Garrido.IsAmenable, proves this statement.
The milestones are results from the literature, stated as their sources state them: has no non-abelian free subgroup (Cannon–Floyd–Parry, Corollary 4.9) and is not elementary amenable (Theorem 4.10), and Følner's criterion, all three already proved and linked as references; Moore's tower lower bound on Følner sets of ; Kaimanovich's theorem that random walks on with finitely supported strictly non-degenerate steps are not Liouville; Chornyi's reformulation of amenability of as extensive amenability of its action on the dyadic rationals; Stankov's embedding of into Monod's ; Monod's theorem that is not co-amenable in ; and the theorem of Juschenko, Matte Bon, Monod and de la Salle that a subgroup of Monod's group of piecewise-projective homeomorphisms of the line is amenable if and only if its action on the line is extensively amenable.
Monod's Problem 12 asks whether is amenable; it is stated as ¬ Garrido.IsAmenable (Monod.H ⊥), where ⊥ is the smallest subring of , namely ; this is parallel to the goal. Through Stankov's embedding, the proof of the goal proves it. By the theorem of Juschenko, Matte Bon, Monod and de la Salle, it is equivalent to the statement that the action of on the line is not extensively amenable; that theorem is proved on this platform, through the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn), and for the subgroups of also in a sharper form, with extensive amenability on the set of possible breakpoints only (the breakpoint criterion).
The result. A proof of the conjecture would make a finitely presented, torsion-free, non-amenable group with no non-abelian free subgroup, with a concrete description as a group of homeomorphisms of the interval. A disproof would make an amenable group that is not elementary amenable, and by Moore's theorem one whose Følner sets are at least tower-sized.
Formalizing it. Corollary 4.9 and Theorem 4.10 of Cannon–Floyd–Parry are formalized and proved on this platform and enter as references. Chornyi's corollary is proved here; its "if" direction is proved directly, by establishing the case that Chornyi applies of the Juschenko–Matte Bon–Monod–de la Salle criterion. Moore's theorem is formalized and published together with the lemmas of its proof, and the milestone here has a solution that reduces it to that statement. Kaimanovich's theorem, Stankov's embedding, Monod's 2023 theorem and the theorem of Juschenko, Matte Bon, Monod and de la Salle are proved here as well, the last through the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn). The definitions of Følner sets, harmonic functions on groups and extensive amenability are reusable beyond this mission.
The obstructions to amenability that settle the question for most groups are absent here: has no non-abelian free subgroup, and its elementary structure is well understood. In the other direction, the usual constructions of invariant means fail: by Moore's theorem any Følner set of is at least tower-sized, so no explicit search can exhibit one, and by Kaimanovich's theorem the finitely supported random walks on are not Liouville, so the random-walk route to amenability through a trivial Poisson boundary is closed.
Lean representation and conventions.
UI; and are subgroups of the homeomorphisms of OnePoint ℝ. Groups of maps multiply by composition, ; statements from sources that write the product in the other order are restated for this convention, with the equivalence explained in their natural-language statements.What is left out.
What a development needs. Thompson's group and its dyadic action (Cannon–Floyd–Parry §4), its tree diagrams and presentations, and amenability, Følner's criterion and the closure properties of amenable groups (Garrido I) are published and proved on this platform, as are Monod's groups and the isomorphism (Monod.contDiff_and_exists_mulEquiv_HRat_F). Mathlib has Følner filters for measurable groups and Schreier graphs of quivers, but no random walks on groups; the proofs of the landmarks here supply what they need, and the germ-groupoid theorem of Juschenko, Nekrashevych and de la Salle (GermGroupoid.isAmenable_of_isExtensivelyAmenableOn) is reusable beyond this mission. Reductions of the goal or of Problem 12 to new, sharper statements are welcome, as is a disproof of either.
A periodic point of a map is a point with for some . A nonwandering point is a much weaker form of recurrence: every neighbourhood of eventually returns to meet itself, for some . Every periodic point is nonwandering, but a nonwandering point need not be periodic, and the orbit of such a point may never come back to exactly.
Pugh's closing lemma asserts that this gap can be closed by an arbitrarily small change of the system: if is nonwandering for a diffeomorphism of a compact manifold, then some diffeomorphism , as close to as desired in the topology, has as a periodic point (Wikipedia, "Pugh's closing lemma"). The result was proved by C. C. Pugh in 1967 (Pugh 1967), in the same paper as the General Density Theorem: for a -generic diffeomorphism the periodic points are dense in the nonwandering set. The source article describes the lemma as establishing a close relationship between chaotic and periodic behaviour and notes that it underlies some autonomous convergence theorems. The article also points to Smale's problems as related material.
Let be a compact smooth manifold of dimension , Hausdorff and without boundary. Write for the set of diffeomorphisms : bijections such that and are continuously differentiable. For , denotes its tangent map on the tangent bundle.
The topology on is the coarsest topology for which is continuous, where the space of continuous self-maps of carries the compact-open topology. Two diffeomorphisms are -close when they, and their derivatives, are uniformly close.
For a map of a topological space:
For every and every ,
Milestones 1–4 are elementary background facts that are not stated in the source article; milestone 5 is the second theorem named in the title of the source's reference.
The result. The closing lemma turns a topological recurrence property into periodicity after a -small perturbation. Combined with genericity arguments it gives the General Density Theorem, so that for generic diffeomorphisms the whole nonwandering set is the closure of the periodic orbits. It is one of the basic perturbation tools of generic dynamics.
Formalizing it. The theorem is classical and proved in the literature. The drafter is not aware of a machine-checked proof. A formalization needs the topology on diffeomorphism groups, local perturbation lemmas in charts and the combinatorics of the closing argument. None of these is currently available in Mathlib as far as the drafter knows.
The first idea is to take the returning piece of orbit near and push it back to with a small local perturbation. This fails in the topology. Moving a point by distance with a bump supported in a ball of radius costs size about , and the return may happen at a distance comparable to the size of the only available ball. The perturbation then fails to be -small. The derivative along the return can also distort any fixed neighbourhood shape without bound. Controlling this distortion is the central difficulty.
BCWCentralizer_Basic. is M ≃ₘ^1⟮𝓡 d, 𝓡 d⟯ M, and the topology is induced by into C(TangentBundle, TangentBundle) with the compact-open topology. On a compact manifold this is the usual topology.PughClosingLemma_nonwandering, shared by all statements. It is reusable for any topological dynamics mission.Welcome contributions: a general theory of the topology on (for example, that it is Baire), local perturbation lemmas, and proofs of the milestones.