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.
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?
Formalize sample-path stability for a continuous-time, unit-rate, infinite-buffer single-server queue. Starting from cumulative arriving service work, define the reflected transient workload, the workload constructed from the infinite past, long-run offered load, and two-time stationarity. Prove that subcritical load forces finite-time coupling and consequently that every finite initial workload converges in its two-time finite-dimensional distributions to the stationary workload law.
Formalize sample-path Little's Law for deterministic continuous-time queueing trajectories, decomposed into area, sojourn, arrival-rate, boundary, and squeeze lemmas.
Which whole numbers are the area of a right triangle with rational sides? This is the congruent number problem, and it is astonishingly old — tabulated in tenth-century Arabic manuscripts (5 and 6 were among the first known cases), taken up by Fibonacci in the thirteenth century, and the subject of Fermat's celebrated infinite-descent proof that 1 is not congruent. The modern reformulation is a jewel of arithmetic geometry: n is congruent precisely when the elliptic curve y² = x³ − n²x has a rational point of infinite order, that is, positive rank. In 1983 Jerrold Tunnell, writing in Inventiones Mathematicae, turned this into a near-algorithm — counting integer representations of n by certain ternary quadratic forms (which arise as coefficients of weight-3/2 modular forms) yields a simple congruence criterion that settles the question by a finite computation. The catch, and the reason the problem remains officially open, is that the sufficiency of Tunnell's criterion rests on the Birch and Swinnerton-Dyer conjecture, itself a Millennium Prize Problem. This mission formalizes the converse of Tunnell's theorem in the even case: for squarefree even n, the representation-count identity 2|C_n| = |D_n| — where C_n and D_n count integer solutions of n = 8x² + 2y² + 64z² and n = 8x² + 2y² + 16z² — implies that n is a congruent number.
Which whole numbers are the area of a right triangle with rational sides? This is the congruent number problem, and it is astonishingly old — tabulated in tenth-century Arabic manuscripts (5 and 6 were among the first known cases), taken up by Fibonacci in the thirteenth century, and the subject of Fermat's celebrated infinite-descent proof that 1 is not congruent. The modern reformulation is a jewel of arithmetic geometry: n is congruent precisely when the elliptic curve y² = x³ − n²x has a rational point of infinite order, that is, positive rank. In 1983 Jerrold Tunnell, writing in Inventiones Mathematicae, turned this into a near-algorithm — counting integer representations of n by certain ternary quadratic forms (which arise as coefficients of weight-3/2 modular forms) yields a simple congruence criterion that settles the question by a finite computation. The catch, and the reason the problem remains officially open, is that the sufficiency of Tunnell's criterion rests on the Birch and Swinnerton-Dyer conjecture, itself a Millennium Prize Problem. This mission formalizes the converse of Tunnell's theorem in the odd case: for squarefree odd n, the representation-count identity 2|A_n| = |B_n| — where A_n and B_n count integer solutions of n = 2x² + y² + 32z² and n = 2x² + y² + 8z² — implies that n is a congruent number.
That the prime numbers, thinning out as they climb yet never quite vanishing, should nonetheless contain arithmetic progressions of every finite length is one of the most celebrated discoveries of twenty-first-century mathematics. Ben Green and Terence Tao proved it in 2004 (published in the Annals of Mathematics in 2008), resolving a question whose roots reach back to Lagrange and Waring around 1770 and which had crystallized in the Erdős–Turán conjecture. The primes have density zero, so Szemerédi's theorem — which guarantees long progressions only in positive-density sets — does not apply directly; the genius of the proof was a transference principle extending Szemerédi's theorem to sets sitting densely inside a 'pseudorandom' host, built from the sieve ideas of Goldston, Pintz, and Yıldırım. The result was a centerpiece of the citation for Tao's 2006 Fields Medal and opened a whole industry, including the Tao–Ziegler extension to polynomial progressions. Unusually for a headline problem, this theorem is already proved — which makes it an ideal flagship formalization mission: a deep, decomposable argument whose pieces, from Szemerédi's theorem to the transference principle, the community can rebuild and verify in Lean.
In a 1999 Vienna doctoral thesis, Gerhard Zauner conjectured that in every finite dimension d one can find d² unit vectors in complex d-space that are mutually as spread out as possible — any two sharing the same squared overlap 1/(d+1). Such a configuration, a symmetric informationally complete positive operator-valued measure (SIC-POVM), is the optimal minimal measurement for reconstructing an unknown quantum state, which is why the idea was rediscovered and named by Renes, Blume-Kohout, Scott, and Caves in 2004 and became central to quantum tomography, quantum cryptography, and the QBist reading of quantum mechanics. Geometrically these are maximal sets of complex equiangular lines; physically they are the most efficient quantum measurements; and, remarkably, they appear to be governed by deep number theory — recent work by Appleby, Flammia, Kopp, and others ties exact SICs to Stark units and Hilbert's twelfth problem on explicit class field theory. Exact solutions have been hand-built in scores of dimensions and numerical ones found in every dimension checked, yet a general existence proof remains out of reach. Formalizing Zauner's conjecture gives this problem — straddling quantum information, geometry, and algebraic number theory — a precise shared target.
First raised for two variables by Ludwig Kraus in 1884 and stated in full generality by Ott-Heinrich Keller in 1939, the Jacobian conjecture asks something that sounds almost like freshman calculus: if a polynomial map from complex n-space to itself has a Jacobian determinant equal to a nonzero constant, must it be invertible by another polynomial map? That constant-Jacobian condition is precisely the algebraic shadow of the inverse function theorem, yet producing a polynomial — not merely analytic — inverse has resisted every attack for over eighty years. Shreeram Abhyankar championed the problem because it can be stated 'using little beyond a knowledge of calculus,' and Stephen Smale placed it sixteenth on his 1998 list of problems for the new century. Its notoriety is sharpened by a graveyard of published 'proofs' that later collapsed. Deep reductions exist — Bass, Connell, and Wright showed in 1982 that the general case reduces to maps of degree three — and the problem is equivalent, through work of Tsuchimoto, Belov-Kanel, and Kontsevich, to the Dixmier conjecture on the Weyl algebra. A formal statement anchors this famously slippery problem so that progress can be verified rather than merely believed.
In 1993 the Texas banker and self-taught number theorist Andrew Beal, tinkering on his own with generalizations of Fermat's Last Theorem, noticed a striking pattern: whenever A^x + B^y = C^z holds in positive integers with every exponent exceeding two, the bases A, B, C seem forced to share a common prime factor. Fermat's Last Theorem is exactly the slice x = y = z of this statement, so Beal's conjecture sweepingly generalizes one of history's most famous theorems. Beal backed his question with money, raising the prize from 1,000,000, now held in trust by the American Mathematical Society. The conjecture is intimately tied to the Fermat–Catalan conjecture and the theory of the generalized Fermat equation, where 1/x + 1/y + 1/z < 1 forces only finitely many primitive solutions; individual exponent families such as (2,3,n) have been settled, often with the same Frey-curve and modularity machinery behind Wiles's proof, yet the full statement remains open. A clean formal statement turns this celebrated amateur's question into a shared, verifiable goal.
Life insurers and pension schemes promise cashflows whose payment depends on future events. A term assurance pays if the insured dies within a stated period. A pension pays when a member survives to an instalment date. A contingent survivor pension may continue after the member dies. These liabilities differ in the events triggering payment, but share one mathematical operation: discount the amounts payable and aggregate them to obtain a random present value. Expected present value is used in premium setting and liability valuation, while the second moment and variance quantify how much the discounted liability can vary.
The open textbook Life Contingencies: The Mathematics, Statistics, and Economics of Life Insurance, Chapter 3, §3.1, introduces uncertain discounted cashflows using indicators, and derives their expected values in equation (3.3). Its treatment also distinguishes independent indicators from indicators connected through death or survival. This mission establishes a finite-horizon generalisation of those identities that handles arbitrary dependencies among payment-triggering events.
Fix a measurable sample space with a probability measure . A finite set indexes distinct payment obligations. Each obligation has a non-negative integer payment date , a deterministic cashflow amount , and a measurable event that triggers payment. The deterministic discount function assigns a multiplier to each date. Write for the real-valued event indicator, equal to one on and zero otherwise.
The random present value is
The same date can support multiple obligations with distinct contingencies, such as member and survivor payments, pension tranches and expenses. The index distinguishes obligations even when their payment times coincide. Amounts may be positive, zero or negative and triggering events can be mutually exclusive, nested, independent or arbitrarily dependent. Finite schedules also allow no obligations. Each present value is bounded and has finite first and second moments because the schedule is finite, amounts are deterministic real numbers, and indicators are bounded.
The capstone theorem proves the expected present value, second moment and variance identities for the same random variable . The expected present value is
The second moment retains all dependence terms, including pairs of different obligations payable on the same date:
Consequently,
The finite identity for expected present value specialises the textbook's equation (3.3). The general joint-event second-moment identity extends its §3.1.1 discussion to arbitrary dependence. The goal combines all three formulas in a single result, with supporting milestone theorems for integrability, square-integrability, one-event expectation, the finite-schedule expectation formula, pairwise event interactions, the second moment and the variance.
A single reusable statement should allow a future mission to specify the trigger events and payment schedule of a policy and immediately obtain its discounted mean and variance. A life assurance can use disjoint death-year events, and an annuity can use nested survival-to-payment events. A guaranteed pension, deferred benefit, survivor pension or multiple-decrement model can use more general indicators. Later missions can also specialise the variance expression when events are known to be independent or mutually exclusive.
Examples of why the dependence assumptions matter. Write for each discounted obligation amount:
These specialisations use the same capstone rather than different definitions of actuarial present value.
The mathematical identities are established results of elementary probability and financial mathematics. The formalisation contribution is a stable actuarial cashflow interface connecting the relevant Lean measure-theoretic and probability results. It does not assert that the classical equations are newly discovered, or that general insurance reserving, stochastic interest rates or continuous-time survival models have already been formalised.
The event indicator is a bounded random variable, but its mathematical expectation is represented in Lean by integration against a measure. The development must reconcile the real-valued integrals with event probabilities represented as extended non-negative reals. Moreover, expanding the square of a finite random cashflow sum requires pairwise intersections without adding an independence assumption. The usual simplification that removes cross-terms is invalid for nested survival events or arbitrary dependent payment events.
The target also uses the real-valued variance from Mathlib. Its general API permits variables outside , so a faithful proof must establish square-integrability for the finite event-based present value rather than use any default value for an undefined or infinite variance.
The initial development is discrete-time and finite-horizon, with distinct payment obligations indexed by a finite set. Each obligation has a nonnegative integer payment time. Different obligations may have the same payment time. Discount multipliers and payments are deterministic real values; no positivity assumption is needed for the algebraic identities. Each trigger is a measurable event and the underlying measure is a probability measure. Empty index sets and zero or negative payments are included. The joint-event formula remains valid when the same outcome triggers more than one payment.
Use Mathlib's existing MeasureTheory.Measure, MeasurableSet, integration and ProbabilityTheory.variance rather than redefining them. A lightweight namespace ActuarialValuation should define the random present value and retain clear time and cashflow parameter names. Supporting results should be small and import only genuine mathematical dependencies. The formalisation uses a generic obligation index type and a payment-time function into the natural numbers. The event family and amounts are indexed by obligations rather than by time.
There is no finite-to-infinite inference in the target; infinite sums require separate convergence results. There are no mortality rates, hazard functions, Markov transition kernels or stochastic discount factors in this mission. Those are targets for later missions, building on the valuation layer.
A prophet inequality compares an online decision maker, who sees random values one at a time and must decide irrevocably, with a "prophet" who sees all values in advance. The classic result of Krengel, Sucheston and Garling (1977) and Samuel-Cahn (1984) says that for a single item and independent values a single threshold earns at least half of the expected maximum. In mechanism design the same inequalities describe posted-price mechanisms: a seller approaches buyers in sequence and offers each a menu of prices; each buyer takes the outcome it likes best. Such mechanisms are truthful, simple and online, so a prophet inequality for a feasibility constraint is a welfare guarantee for a practical selling procedure.
Before this paper, prophet inequalities were proved one constraint at a time (matroids, matroid intersections, polymatroids, unit-demand and combinatorial auctions), each with its own probabilistic argument. Dütting, Feldman, Kesselheim and Lucier (SIAM J. Comput. 49(3), 2020; conference version FOCS 2017) showed that a single extension theorem reduces all of them to a deterministic question about full-information instances.
There are agents . Agent has an outcome space containing a null outcome . An outcome profile is ; is with the outcomes of agents replaced by . The feasible profiles form a downward-closed set : removing outcomes keeps a profile feasible.
Agent 's valuation is drawn independently from a known distribution ; . The welfare of is , and is the largest welfare over a set of profiles. An outcome rule maps each valuation profile to a feasible profile.
A pricing rule assigns a price to outcome offered to agent when the partial allocation is , with price when cannot be feasibly added to . In the posted-price mechanism the agents are approached in index order; agent sees the prices given the allocation so far and takes an outcome maximizing its utility .
A set of profiles is exchange compatible with if for every and every . For a fixed valuation profile , a pricing rule is -balanced (Definition 3.1) with respect to and an exchange-compatible family if for every
Property (a) says the prices paid by cover the welfare blocks; (b) says that what remains available is not overpriced.
If every is -balanced with respect to one exchange-compatible family, post with and . Then the welfare of the mechanism satisfies
The steps of the paper's proof (pp. 549–550), in order: the prefix does not depend on ; the per-agent utility bound against a deviation drawn from an independent sample ; (3.1); the bound (3.2) from property (b); (3.3); the pointwise revenue bound from property (a); (3.4); and welfare = utilities + revenue. Two applications complete the list: Claim 3.3 (the single-item price is -balanced, which with the goal gives the classic factor 2) and the balancedness half of Theorem 4.2 for knapsack.
The theorem turns prophet inequalities into a deterministic design problem: to obtain a guarantee against any benchmark , it suffices to exhibit balanced prices for each fixed valuation profile. The paper uses it to rederive the single-item factor 2, to obtain guarantees for combinatorial auctions with bundles of size , a constant for knapsack, and bounds for MPH- valuations, sparse packing problems and multidimensional matroids. Because can be any (for example polynomial-time) algorithm, the guarantee is relative to what can be computed, not only to the optimum.
The result is proved in the paper. As far as is known, no part of it has a machine-checked proof; the platform holds no posted-price framework of this generality. A formal proof would provide a reusable model of sequential posted-price mechanisms over arbitrary outcome spaces and a checked reduction that later formalizations of the applications can invoke instead of repeating a probabilistic argument.
The obvious argument fixes the realized valuations and charges each agent's purchase against the welfare it blocks. That fails because the prices are averages over a hypothetical profile , not the prices of the realized instance, and the set of outcomes still available depends on everyone's random values. The proof needs an independent copy of the valuations and the fact that the allocation before agent does not depend on , so that and can be exchanged without changing the distribution. Formally, the run of the mechanism is a recursion over agents, the exchange is a measure-preserving swap of coordinates of a product measure, the optimal value is a supremum that need not be attained, and the family may be empty.
Agents are Fin n, 0-based; the index order is the order of Fin n. Outcomes are (X : Fin n → Type*) with a null profile nul. Valuation types V i are countable with the discrete σ-algebra (a disclosed restriction: the paper allows any distribution); this makes every function measurable and every bounded one integrable. A type w : V i values outcomes through val i w : X i → ℝ, with values in as on p. 547. The distribution is Measure.pi μ with every μ i a probability measure.
Prices are ℝ≥0∞-valued, ⊤ standing for ; the expected price is a Lebesgue integral in . Property (a) passes its real right side through ENNReal.ofReal, and no price sum is ever converted to a real number, so an infinite price is never read as . is the real supremum sSup of the welfare over , equal to on as in the proof of Claim 3.3. Exchange compatibility of the family is required at every profile, not only feasible ones. The pricing-rule condition " when infeasible" is imposed at feasible partial allocations, which is where the paper defines prices.
Two standing assumptions are disclosed. First, the null outcome is free: for feasible . Every pricing rule of the paper satisfies it, and without it the proof's deviation does not exist when . Second, the agents' behaviour is a choice rule that sees only the agent's own type and the allocation so far, assumed utility-maximizing (finite price, best utility among finitely priced outcomes) at every feasible partial allocation. The constant is written into the posted prices, not passed as a parameter.
A trivializing formalization is ruled out: the goal mentions only the run of the mechanism, the expected prices scaled by , balancedness and the two expectations. It does not assume the utility or revenue bounds, it does not let an agent's choice see other agents' types, and a supplementary check confirms that its hypotheses are jointly satisfiable. Milestones that involve the proof's deviation are stated for an arbitrary selector from , a generalization that avoids assuming that the supremum is attained. Theorem 4.2 is stated as -balanced, which is what its proof establishes; the printed "" is false.
Useful infrastructure, reusable beyond this mission: measure-preserving coordinate swaps for Measure.pi and products of product measures, ε-maximizer selection for bounded suprema, and induction principles for the sequential run. Contributions of proofs of individual milestones are welcome.
In a multi-armed bandit, a decision maker repeatedly chooses an arm, observes a reward, and tries to learn which arm has the highest average reward while losing little reward during learning. A policy that requires the number of future pulls in advance cannot be used unchanged when stopping time is uncertain. Perchet and Rigollet study successive elimination (SE), which removes poorly performing arms from a shrinking active set and can run without knowing the realized horizon. Their Theorem 2.1 bounds its expected regret when the horizon is random and independent of rewards Perchet and Rigollet, 2013, Theorem 2.1.
The static-bandit theorem also supplies a concentration and elimination analysis used in the paper's broader study of bandits with covariates. This mission isolates that theorem and the intermediate estimates that make its quantitative constant explicit. The paper proves the result in §2, with a concentration lemma in the Appendix; the goal here is a machine-checked statement and, eventually, a machine-checked proof of that known result.
There are arms. For each arm , the reward stack lists the rewards that successive pulls of that arm will reveal. Rewards lie in , are identically distributed along each arm, and have mean . The stacks are mutually independent. Arms are indexed so that , and the last arm, denoted , is uniquely best. Its gap from arm is . A gap is zero only for the best arm.
The policy works in rounds. At the start of round , a nonempty set is active. It pulls each arm in once, in increasing index order, and computes the mean from that arm's first rewards. It retains an arm when its mean is within of the largest active mean, where is an integer, , and
Concatenating the rounds gives the pull sequence . For a horizon , its regret is . If is random, independent of the reward stacks, and has mean , the paper studies . For a threshold , let be the largest arm gap strictly smaller than , or zero if none exists.
The goal is Theorem 2.1, for every positive threshold :
The in this formula counts suboptimal arms; there are arms in total. The paper writes under a convention that division by zero is infinite. The real-valued Lean goal states the informative positive-threshold case.
The milestones include the Appendix's maximal Hoeffding–Azuma inequality and Lemma A.1, which controls all empirical averages up to a fixed time. In §2 they continue with the stopping-round estimate (2.2), the empirical-gap tail (2.5), the bound for a false elimination of the best arm, and the final comparison for . Each has its own statement so that a proof of the goal can import the exact estimate it needs.
The bound separates the cost of learning arms with gaps above from the remaining regret represented by . It applies when the policy uses a tuning value but the number of pulls actually made is the random variable . Thus it gives a quantitative guarantee without asking the algorithm to know its stopping time in advance. Its constants and dependence on , , , and are explicit Perchet and Rigollet, 2013, §2.
The result is proved in the paper, while the Lean declarations in this proposal are open statements. Completing them would add a reusable formal account of elimination on a reward stack and of the Appendix's time-uniform concentration estimate. Mathlib and existing platform theorems contain related Hoeffding–Azuma tools, but this paper's peeling inequality, its particular stopping rule, and the random-horizon regret conclusion still require proofs in the stated model.
An ordinary concentration bound at one sample size does not control every round in which an arm could eliminate the best arm. Taking a naive union bound over all rounds loses the dependence on needed for the displayed regret constant. The Appendix instead states a maximal inequality and a bound that holds across a range of sample sizes. The regret calculation must then account for both kinds of error: removing the best arm and retaining a suboptimal arm for too long.
The stopping round depends on the gap through , which itself contains . Its upper bound, the event decomposition across ordered arms, and the final comparison of gap-dependent terms all retain the paper's exact constants. A proof that only establishes the asymptotic rate would not close this goal.
Lean uses Fin (K+1) with zero-based indices, so its last element is the paper's arm . The published stochastic-bandit definition supplies the mutually independent reward stack and arm means. The [0,1] bound, sorted means, and unique best arm are explicit assumptions. A separate martingale-difference definition supplies the Appendix's adapted, integrable sequence, including centering of its first term; the page's one-line definition leaves that first-step condition unstated. The concentration milestones require a nondegenerate interval : the displayed maximal exponent divides by , and Lemma A.1 is false at for a zero sequence and .
The SE policy is a function of observed rewards in the stack. It uses the end-of-round test described in the text and proof of §2, with equality retained, since Policy 1's pseudocode tests at a different point in the round. The active set starts with all arms and remains nonempty; the total Lean pull function has a fallback value that is unreachable under the theorem's parameters. The policy never reads the unknown means. Empirical means and are used only at positive rounds.
The horizon is measurable and integrable, has mean , and is independent of the entire reward stack. Since regret is bounded by the horizon, its expectation is a genuine integral rather than the default value of a non-integrable Lean integral. The positive-threshold condition avoids Lean's zero-valued division at . Finite maxima are taken over finite arm sets, and is kept distinct from the ordinary logarithm in the Appendix's bounds. The paper's printed in the logarithm of (2.7) and the final comparison is read as , consistently with (2.2) and Theorem 2.1. Contributions to the concentration lemmas, stopping-round analysis, elimination events, and final regret proof all fit this scope.
A queue layout of a graph places its vertices on a line and splits its edges into classes, called queues, so that inside one queue no edge is nested inside another. The minimum number of queues is the queue-number. Queue layouts were introduced by Heath, Leighton and Rosenberg (1992) and Heath and Rosenberg (1992) as the dual of stack layouts (book embeddings): reading the vertex order from left to right, the edges of one queue are opened and closed in first-in first-out order. Queue layouts are closely tied to track layouts and, through them, to three-dimensional grid drawings of graphs (§9 of the paper).
Whether planar graphs have bounded queue-number was asked by Heath, Leighton and Rosenberg in 1992 and stayed open for 27 years. The best general bounds before 2019 grew with the number of vertices: by Heath, Leighton and Rosenberg (1992), by Di Battista, Frati and Pach (2013), and by Dujmović (2015); for Euler genus , Dujmović, Morin and Wood (2017) had . Dujmović, Joret, Micek, Morin, Ueckerdt and Wood (arXiv:1904.04791, J. ACM 2020) proved that every planar graph has queue-number at most (Theorem 1), and extended the result to every graph embeddable in a fixed surface (Theorem 2) and to every proper minor-closed class (Theorem 3).
This mission is Theorem 2: graphs of Euler genus have queue-number at most . It is the second mission of a two-mission series; the first poses Theorem 1.
All graphs are finite and simple. A linear ordering of the vertex set is fixed. Two edges and with four distinct ends nest if (after renaming the ends). A queue is a set of edges no two of which nest. A -queue layout of is a linear ordering together with a partition of into queues, and means that a -queue layout exists.
A layering of is an ordered partition of such that every edge joins two vertices of the same or of consecutive layers. A BFS layering takes one root in each connected component and puts in layer . A BFS spanning tree of a connected graph rooted at is a spanning tree with for every . A path in is vertical if the distance to grows by exactly one at every step.
The Euler genus of the orientable surface with handles is , and that of the non-orientable surface with cross-caps is ; the Euler genus of a graph is the least Euler genus of a surface it embeds in (footnote 2 of the paper). Planar graphs are exactly the graphs of Euler genus . Combinatorially, an embedding of a graph is described by an embedding scheme: a cyclic order of the edges at each vertex (a rotation system) together with a sign on every edge (twisted or not). Tracing faces through the scheme gives a face count , and with vertices, edges and components the scheme has Euler genus .
The paper states Theorem 2 as and proves the explicit bound in §5. The goal poses that explicit bound, for every finite graph, connected or not.
The result. Theorem 2 settles boundedness of the queue-number for every class of graphs embeddable in a fixed surface, with a bound linear in the Euler genus. Through the connection between queue-number and track-number, the paper derives from it (§9, Theorems 54 and 58) that a graph of Euler genus with vertices has track-number and a three-dimensional grid drawing of volume , linear in for every fixed surface. It is also a step on the paper's route to Theorem 3 (proper minor-closed classes), since graphs on surfaces are the basic pieces of the Robertson–Seymour graph minor structure theorem. Lemma 21 is of independent use: it reduces a graph on a surface to a planar graph while controlling BFS layers.
Formalizing it. The result is proved; as far as is known it has no machine-checked proof. A formalization needs queue layouts, layerings, BFS layerings and vertical paths, and, independently of queues, a usable combinatorial theory of graphs on surfaces, which Lean's Mathlib does not have. The Euler genus definition of this mission (embedding schemes and face tracing) and Lemma 21 are reusable well beyond queue layouts.
The obvious reduction, deleting few vertices to make the graph planar, is not enough: a planar subgraph alone does not control how the deleted vertices interact with a queue layout. The deleted set must be thin in every BFS layer, and the planar remainder must carry a BFS layering compatible with the original one, which is what Lemma 21 provides. Its proof cuts the surface along a subgraph made of tree paths and must show that the cut graph is planar by an Euler-characteristic count over face-tracing data, and that distances from a new root agree with the old BFS distances. In Lean, the main obstacle is the surface side: Euler's formula for embedding schemes, the cutting operation on rotation systems, and the passage between the combinatorial notion of Euler genus and the drawing-based notion of planarity. The planar input, Lemma 18, is itself the whole of mission 1's argument (Theorem 15 with Lemmas 5 and 8).
SimpleGraph V on a finite type V : Type with decidable equality and adjacency.HasQueueLayout G k: an injective map ord : V → ℕ (the linear ordering) and an assignment of the edges of (G.edgeSet, not all unordered pairs) to Fin k such that no two edges in one queue nest; nesting uses strict inequalities, so edges sharing an end never nest. Queues may be empty.L : V → ℕ; a BFS layering takes one root per component. Vertical paths are nonempty lists indexed from with distance , .EulerGenusLE G g asks for an embedding scheme (rotation permutation of the darts, cyclic at every vertex, and a symmetric edge signature) whose Euler genus , computed in , is at most . The face count is half the number of face-tracing orbits plus the number of isolated vertices. Equivalence with footnote 2's topological definition is the Heffter–Edmonds–Ringel rotation principle and its non-orientable extension, with additivity over components; it is not part of the mission.RobertsonSeymour1986.GM5.IsPlanar: a crossing-free drawing in by simple arcs. "Euler genus iff planar" is a theorem connecting the two definitions, not built into either.Sym2 V would deny edgeless graphs a -queue layout; non-strict nesting would forbid adjacent edges in one queue; a drawing that tolerates crossings would make every graph planar; a face count without halving, or without isolated vertices, would make the Euler genus too small or too large (the sanity checks confirm has a scheme of Euler genus , a twisted one of genus , and two isolated vertices genus ).First-order hyperbolic systems of balance laws model open-channel flow (the Saint-Venant equations), gas pipelines, traffic and heat exchangers. In most of these applications the state can be acted on only at one end of the domain, so stabilizing an equilibrium is a boundary control problem. For systems without source term (), static boundary feedback built from a Lyapunov function works (Coron–Bastin–d'Andréa-Novel 2008); with a source term, Lyapunov functions of the diagonal form can fail (Bastin and Coron 2011, recalled in Remark 1 of the paper). Backstepping, introduced for parabolic equations by Krstic and Smyshlyaev, replaces the search for a Lyapunov function by an invertible integral change of variables that maps the linearized plant to a target system whose stability is evident.
Coron, Vazquez, Krstic and Bastin (arXiv:1208.6475v1, 2012; SIAM J. Control Optim. 51(3), 2013) design such a feedback for the linearization of a quasilinear system and prove that it stabilizes the nonlinear system locally in . This mission formalizes that main result, Theorem 4.1.
The state is on , , governed by
The standing assumptions (§2) are: , , are ; with on ; ; . Write and ; the paper treats .
The scaling , , , removes the diagonal of the linearization, which becomes with , , , and antidiagonal with entries , . The kernels solve a pair of first-order hyperbolic equations on the triangle with boundary data on its diagonal and on the edge ((3.32), (3.33), (3.36), (3.37)). The gain is .
The closed loop adds a dynamic extension:
with , , and , determined by the initial profile through two linear functionals , . The norm is on .
For every there are such that every classical solution with satisfying the compatibility conditions (4.16), (4.18) obeys
Write for the full kernel , , , and .
Theorem 4.1 shows that a feedback computed entirely from the linearization, by solving linear kernel equations, is a valid local stabilizer of the quasilinear system in , the natural space for classical solutions of quasilinear hyperbolic systems. The dynamic extension is what makes the result usable: without it, the static feedback imposes artificial compatibility conditions (4.17), (4.19) on the initial data.
The result is proved in the paper (§5 and Appendix B); none of it is machine-checked. A formal proof needs a rigorous treatment of the Volterra transformation and its inverse in , the three-level Lyapunov argument (, , ), and the comparison of these functionals with the norm. The formalization also records corrections to the printed formulas: the sign of in (4.1), the entries of in (4.7), the initial values (4.26), and the admissible decay rates (see below).
The obvious argument — the linear closed loop is exponentially stable, so the nonlinear one is locally stable — fails for hyperbolic systems: the nonlinear terms contain a derivative of the state, so they are not small in relative to , and an estimate does not close. One must control , and simultaneously, each with its own Lyapunov functional whose weight depends on the state, and exchange time derivatives for space derivatives through the equation, which is possible only while and stay small.
States are Fin 2 → ℝ, matrices Matrix (Fin 2) (Fin 2) ℝ, indices 0-based. A solution is one function (space first) with the PDE imposed on and the boundary conditions for ; this is the theorem restricted to classical solutions, since Mathlib has no Sobolev spaces. Global existence is not asserted. Coefficient functions are defined on all of with global regularity and sign conditions on . , norms are sums of norms, as on p. 11; uses .
Added or corrected relative to the page, all disclosed in the items:
Trivializing formalizations are ruled out: , and every milestone constant are quantified after the data and before the solution; the kernels are pinned down by all their equations and boundary conditions (unique by Theorem A.1 of the paper); the corrected , are the ones every classical solution has, so no small initial profile is excluded; and the norm contains .
Not formalized: Lemma 5.2 (its printed bound (5.38), , fails for profiles with small and large , and (5.37) compares a matrix with a scalar), and Lemmas B.1–B.4, B.7, B.8. Contributions of a reusable theory of Volterra integral transformations on with kernels, and of the comparison between sup and norms of solutions of hyperbolic systems, are welcome.
Maximizing a homogeneous polynomial over the unit sphere, , covers the largest stable set of a graph (degree three), the norm of a matrix (degree four) and the best separable state problem of quantum information. For quadratic it is an eigenvalue problem; for degree at least three it is NP-hard. The sum-of-squares hierarchy of Parrilo and Lasserre replaces " on the sphere" by " is a sum of squares of polynomials of degree at most on the sphere", giving upper bounds that are computable by a semidefinite program of size and decrease to . How fast they converge decides how large has to be for a given accuracy. Fang–Fawzi, §1–1.1
Timeline:
Write , , and . A matrix polynomial has a real polynomial in each entry, and is the real matrix of values. means that the symmetric matrix is positive semidefinite. A matrix polynomial is -sos on if there are finitely many matrix polynomials , each entry of total degree at most , with
For a scalar polynomial , is the least such that (a matrix) is -sos on , and is the minimum of on . The level value is when no such exists.
The milestones use three further objects. A harmonic decomposition of a homogeneous of degree is with homogeneous of degree and . is the least constant with for all such in all dimensions. The Gegenbauer coefficients of a univariate polynomial are its coefficients against the orthogonal polynomials for the weight on , equation (9). For of degree at most , the kernel error is
For every there are constants depending only on such that, for all and every matrix polynomial , homogeneous of degree with , symmetric at every , with on :
The goal fixes only the shape and the regime , and leaves the constants open.
They follow the paper's proof, in attack order:
Theorem 2 says how the level must grow with the dimension: suffices for relative error , where Reznick's analysis needs . Theorem 10 of the paper shows that, for , the kernel error of this technique really is of order . Independence of the matrix size gives certificates for polynomials that are bihomogeneous of degree on . The paper's Theorem 15 uses this, together with the DPS duality of the companion mission, to bound the convergence of the DPS hierarchy for separability. Fang–Fawzi, pp. 3, 10, 14
The theorem is proved in the 2019 preprint and was published in Mathematical Programming in 2021. No machine-checked proof of it or of its ingredients is known. Proving it formally takes reusable infrastructure: degree-bounded matrix SOS on the sphere, harmonic decomposition of homogeneous polynomials, Gegenbauer polynomials with their coefficients and the Funk–Hecke formula, and spectra of Jacobi matrices of orthogonal polynomials. The milestones also correct the printed text, as listed under Formalization scope.
Positive semidefiniteness of at each point of the sphere does not give a factorization with factors of prescribed degree, and Reznick's kernel only reaches error . Two estimates must be uniform at once. First, harmonic projection of a degree- form must be bounded in sup norm independently of ; the bound is easy, and the sup-norm bound is the content of Proposition 5. Second, the kernel error must be bounded throughout the regime , which comes down to the location of the largest zero of a Gegenbauer polynomial. The printed bounds on that zero and on in Proposition 7 are false in small dimensions, so the paper's explicit constants cannot be relied on.
Fin d → ℝ (0-based coordinates), and is the equation , not the sup-norm sphere. Matrix polynomials are matrices over MvPolynomial (Fin d) ℝ, evaluated entrywise, and homogeneity is entrywise.Measure.toSphere.Proofs of any milestone are welcome. So are reusable developments of Gegenbauer polynomials, spherical harmonics, the Funk–Hecke formula, Jacobi matrices, and Carathéodory-type finite quadratures that turn an integral of squares into a finite sum of squares.
The adjacency matrix of an Erdős–Rényi random graph contains a large deterministic mean as well as random fluctuations. The mean affects the largest eigenvalue, while the centered fluctuations determine much of the remaining spectrum. A local spectral law must describe both pieces at a resolution fine enough to distinguish eigenvalues within a narrow energy window. Erdős, Knowles, Yau and Yin established such estimates for a broader class of sparse symmetric matrices and their noncentered rank-one deformations in Spectral statistics of Erdős–Rényi graphs I. This mission formalizes the paper's Theorem 2.9, with the centered-matrix law and eleven intermediate results of the paper as milestones.
The paper treats the graph matrix through a model that also allows other sparse distributions. Its parameters and separate sparsity from the size of the deterministic mean. That separation matters: the normalized resolvent trace can obey a local semicircle law even when the deformation produces a distinguished top eigenvalue. The formal target therefore concerns the deformed matrix itself, rather than replacing it with the centered matrix.
For each size , let be a real symmetric random matrix. Entries indexed by the upper triangle are independent, centered, and have variance . Their higher moments obey
The sparsity parameter lies between and , and the logarithmic parameter satisfies , with and . Define and the noncentered matrix , where . The projection has every entry equal to . These are Definitions 2.1 and 2.2 of the source paper, pp. 5–6.
For a complex number with , the resolvents are and . Their normalized traces are and . The comparison object is the semicircle density and its Stieltjes transform . Put and for a fixed . These definitions appear in Section 2, pp. 7–9.
An -dependent event has -high probability when its failure probability is at most for all sufficiently large . The spectral estimates below refer to single events on which the claimed bound holds at every simultaneously.
Theorem 2.9 assumes and . Its first conclusion is that, with -high probability, every satisfies
Under the additional bound , its second conclusion controls every entry at every :
The constants are universal and positive. The probability exponent may depend on the fixed parameters named in the theorem. Both conclusions, including the extra condition on in the second, are retained from Theorem 2.9, pp. 9–10.
The milestones follow the paper's own sequence of numbered results.
The trace estimate gives quantitative control over spectral mass at local scales, including near the edges . The entrywise estimate says more: each resolvent entry is close to the diagonal semicircle approximation with an error that records both sparsity and finite-size effects. The paper's later results derive density-of-states and eigenvector statements from these local controls. Those consequences are outside this mission's goal.
The intended formal development supplies reusable definitions of sparse symmetric ensembles, high-probability events, semicircle transforms, and complex resolvents, followed by exact statements of the paper's estimates. Mathlib contains no local semicircle law, for Wigner or for sparse matrices, and no Stieltjes transform of the semicircle distribution; the local law, the large deviation bounds and the interlacing lemma are each reusable beyond this paper.
The deterministic rank-one comparison controls the normalized trace but does not by itself control each entry of . The entrywise estimate must account for the deformation and for fluctuations caused by sparse entries. Near the spectral edges, the stability scale of the semicircle transform changes with ; a bound that is uniform in the bulk does not automatically retain the paper's edge behavior. The theorem also asks for one event covering a continuum of values, so a collection of separate fixed- probability bounds has the wrong quantifier order. These are substantive parts of Sections 3–7, beyond algebraic manipulation of resolvents.
Lean represents all on one probability space and takes their entries to be real, symmetric, measurable random variables, independent in the upper triangle. Conditions involving and the moments hold for all sufficiently large ; this avoids impossible small- parameter bounds and matches the asymptotic theorem. The moment order is real, as in the paper. Each finite expectation has an explicit integrability condition. A single positive constant is used for the moment, sparsity, and deformation bounds: replacing several fixed constants by their maximum preserves all three inequalities.
Matrix indices use Fin N rather than the paper's . The resolvent is a complex matrix formed by coercing the real matrix before subtracting . Every result that uses it restricts eventually or explicitly; its inverse at a singular input is never used to make a claim. The semicircle transform is defined by the paper's integral, and uses Lean's nonnegative square root, implementing the positive part. The high-probability predicate evaluates the measure of arbitrary sets, so it can state the intersection over all without a separate measurability assumption on that intersection. Positive and positive square-root arguments follow eventually from the model and .
The deterministic Lemmas 3.2, 3.4, 3.10, 6.1 and 7.1 are stated for every real symmetric matrix and every with (Lemma 3.2 on ); the paper's is contained there. Minors keep the original index names, and is only used for . is the explicit expression of (3.15). Ordered eigenvalues are the sorted roots of the characteristic polynomial. Statements the paper makes "for fixed " (Lemmas 4.1, 7.7, Proposition 7.6) are uniform in : one threshold serves every . The unnamed constants , , are chosen after the fixed parameters and before the random matrices; the universal come first.
Trivializing encodings are ruled out: every resolvent is taken at , so the junk inverse of a singular matrix never enters; the model is satisfiable (independent Rademacher signs divided by with and satisfy it for large ); each event of the goal is one intersection over all , not a family of pointwise bounds; the constants appear in the paper's order; and the goal is about with allowed to be large, so it does not reduce to Theorem 2.8.
Part (iii) of Lemma 3.8 is not a milestone: the printed (3.22) omits the diagonal variance term , without which it fails for Rademacher variables with . Contributions of proofs of any milestone, and of the missing groundwork (Stieltjes transforms of measures, Schur complements of resolvents, moment bounds for sums of independent variables), are welcome.
Deciding whether a bipartite quantum state is entangled is a basic computational problem of quantum information theory, and it is NP-hard in general (Gurvits 2003). The most widely used family of tests is the DPS hierarchy of Doherty, Parrilo and Spedalieri (DPS 2002, DPS 2004): a sequence of semidefinite programs, indexed by an integer level , whose feasible sets shrink to the set of separable states. On the dual side, a matrix that is nonnegative on separable states is an entanglement witness, and certifying such witnesses is the problem of certifying nonnegativity of a biquadratic Hermitian form, a classical question in real algebraic geometry.
That the DPS hierarchy is, dually, a sum-of-squares hierarchy for these forms has been used repeatedly in the literature, but, as Fang and Fawzi note (arXiv:1908.05155v1, p. 4), without a formal and complete proof. Their Theorem 12 gives one. They then combine it with their sum-of-squares convergence rate on the sphere (Theorem 2 of the same paper) to recover the convergence rate of Navascués, Owari and Plenio 2009 for the DPS hierarchy.
Timeline:
Let and . A matrix on has entries (row , column ); is the space of Hermitian ones.
for all and all , with ranging over .
Theorem 12 makes the DPS hierarchy and the sum-of-squares hierarchy for biquadratic forms interchangeable. A convergence bound for one is a convergence bound for the other: the paper uses this to derive the DPS rate (Theorem 15) from a rate for sums of squares on the sphere, and conversely quantum de Finetti arguments give sum-of-squares bounds. Part (iii) separates the two notions of Hermitian sum of squares: dropping the partial transposes corresponds exactly to passing from real to complex sums of squares. This explains, for example, why (rsos but not csos) behaves differently in the two hierarchies.
The results are proved on paper; none is formalized. The mission produces a machine-checked statement and proof of the duality, together with the matrix-analytic infrastructure behind it: partial traces and partial transposes on , the symmetric projector, conic duality for semidefinite cones, and the passage between Gram matrices and sums of squares. Theorem 15 additionally depends on the sphere rate of the companion mission (Theorem 6 there) and on the unproved Lemma 13 and display (26) of the paper.
The inclusion of each sum-of-squares cone in the corresponding dual cone is a direct computation. The reverse inclusions are harder: a certificate involving arbitrary Hermitian polynomials must yield positive semidefinite matrices indexed by the prescribed tensor products, even though its square terms can mix different patterns of complex conjugation. Likewise, weak semidefinite duality alone does not show that every element of has the displayed finite certificate; limits of certificates may require a separate closedness argument. The symmetric-subspace condition adds another constraint because an extension must be supported on that subspace, not merely invariant under permutations.
Fin dA × Fin dB (Mathlib's Kronecker convention); is Fin dA × (Fin ℓ → Fin dB).Matrix.PosSemidef (which includes Hermitian). Dual cones are subsets of with the pairing .MvPolynomial over ) in the real and imaginary parts of ; csos is a finite sum of with complex polynomials in only. Swapping the two, or allowing complex in rsos, would change parts (ii) and (iii).No trivializing reading is available: the cones are defined by their page conditions, the dual cones keep the Hermitian constraint, and no degree bound or extra hypothesis is placed on the sums of squares. Welcome contributions include a general library for partial traces and transposes of multipartite matrices, the spanning property of in the symmetric subspace, and Gram-matrix characterizations of sums of squares of polynomials; all are reusable well beyond this mission.
A decision maker who must choose to minimize an expected cost rarely knows the distribution of the uncertain parameter ; what is available is a sample . Sample average approximation (SAA) replaces by the empirical distribution. Data-driven distributionally robust optimization (DRO) instead minimizes the worst case of the expected cost over a set of distributions built from the data, which protects against the error of the empirical distribution at small . Many such sets have been proposed: moment sets (Delage and Ye, 2010), -divergence balls (Ben-Tal et al., 2013), Wasserstein balls (Mohajerin Esfahani and Kuhn, 2018).
Bertsimas, Gupta and Kallus (arXiv:1408.4445v3; Mathematical Programming, 2018, doi:10.1007/s10107-017-1174-z) observe that each such set can be read as the confidence region of a statistical goodness-of-fit (GoF) test, and call the resulting method Robust SAA. A basic question for any such method is whether, as , its objective, optimal value and optimal solutions converge to those of the full-information problem. The paper answers it for all data-driven DROs at once, with a single property of the test.
The support of is closed, and is the set of Borel probability distributions on with the topology of weak convergence. The data are i.i.d. from an unknown . A data-driven uncertainty set (DUS) map assigns to each sample a set ; it is the confidence region of the test that rejects a hypothesis exactly when . Decisions lie in a closed set , the cost is , and the robust objective is the worst-case expectation
A test is uniformly consistent (Definition 3) if, for every data-generating , almost surely every sequence that does not converge weakly to lies outside for infinitely many . The admissible instances are those satisfying three assumptions: (1) is equicontinuous in uniformly over ; (2) is bounded, or is coercive in uniformly over a set of positive -probability and bounded below off ; (3) is bounded, or there is a growth function with whose expectation the DUS tracks: almost surely. The convergence conditions are (18) uniformly on compact subsets of ; (19) convergence of optimal values; and (20) every sequence of robust minimizers has a limit point, and all its limit points are true minimizers.
For a DUS map with nonempty sets,
The statement carries no rates and no constants; it is a characterization, so it does not depend on any particular test.
The result. Theorem 2 reduces the asymptotic analysis of a data-driven DRO to a property of a statistical test, which can be checked once per test rather than once per optimization model. The paper uses it to classify DUSs: the and G-tests on a finite support and the Kolmogorov–Smirnov, Kuiper, Cramér–von Mises, Watson and Anderson–Darling tests on the line are uniformly consistent (Theorems 4–5, separate missions of this series), while the test of marginals is not even consistent and so cannot give convergence for every cost. The necessity direction makes the property sharp: a weaker test always admits a well-behaved cost on which the DRO fails to converge. Theorem 3 explains the remaining cases where a DRO converges for one given cost.
Formalizing it. The result is proved in the paper (§10.5), but its proof leans on several standard facts used without detail: the portmanteau theorem, uniform integrability arguments from Billingsley's Convergence of Probability Measures, the Lévy continuity theorem with the Cramér–Wold device, and coercivity arguments carried over from the paper's Theorem 1. A machine-checked version would fix exactly which regularity of the cost these steps need; three such conditions are stated explicitly here (see the scope section). No part of the result is formalized elsewhere to our knowledge; the platform has no notion of a data-driven uncertainty set or of uniform consistency.
Uniform consistency is a statement about weak convergence, while (18)–(20) are statements about expectations of an unbounded, -dependent cost under the members of . Weak convergence controls expectations only of bounded continuous functions, so the "only if" side must recover convergence of from Assumption 3, which requires uniform integrability, and then upgrade pointwise convergence to uniform convergence on compacts and to convergence of minimizers when is unbounded. The tempting route through a single limiting minimization problem fails: the sets change with the sample, the worst case is a supremum over infinitely many distributions, and the minimizers of could escape to infinity unless coercivity on transfers to every member of . The "if" side needs, from the mere failure of uniform consistency, a single admissible cost whose worst-case objective detects every failure of weak convergence.
Points are EuclideanSpace ℝ (Fin d), distributions are ProbabilityMeasure ↥Ξ (whose topology is weak convergence), and the data live on the canonical product space with the product law, 0-indexed. "Almost surely" is ∀ᵐ, and in Definition 3 one null set serves every sequence . An expectation over a member of is when the integrand is not integrable, never Lean's default . Minima in (19)–(20) are infima in the extended reals, so the empty and unattained cases need no special treatment; (20) applies to sequences that are minimizers for all large .
Four hypotheses are added to the page, each used by the paper's own proof: every is nonempty (otherwise the worst case is and uniform consistency is vacuous); is continuous on ; the set of Assumption 2b is open; the growth function of Assumption 3b is continuous, with as fixed on p. 10 of the paper. Theorem 3 additionally assumes Assumption 2, which its proof uses. Proposition 4 assumes the rejection events are measurable. A formalization in which the worst case uses the raw Bochner integral, the supremum ranges over a possibly empty set, or (20) requires minimizers at would make the statements false or vacuous, and is ruled out.
A full development needs weak convergence and the portmanteau theorem (in Mathlib), uniform integrability and its relation to convergence of means under weak convergence, the strong law of large numbers for the growth function and the empirical measure, the Lévy continuity theorem in several dimensions (in Mathlib, via characteristic functions), and a countable convergence-determining class of bounded continuous functions. The uniform-integrability step and the path characterization of local uniform convergence (Proposition 9) are reusable beyond this mission. Contributions to any milestone are welcome; Proposition 9 is self-contained and deterministic.
Bayesian inference, statistical physics and machine learning all ask for samples from a probability distribution on whose density is known only up to a constant, . The unadjusted Langevin algorithm (ULA) is the Euler–Maruyama discretisation of the Langevin diffusion, whose invariant law is . It needs only gradients of , has no accept/reject step, and is therefore cheap in high dimension. Without the Metropolis correction, however, the chain does not leave invariant, so its usefulness rests on quantitative bounds: how far, in total variation, the law of the -th iterate is from , as an explicit function of the dimension , the step sizes and the regularity of .
Durmus and Moulines (arXiv:1507.05021, Ann. Appl. Probab. 27(3), 2017) gave such bounds for constant and decreasing step sizes. Earlier work of Dalalyan (arXiv:1412.7392, 2017) treated strongly log-concave targets with constant steps. Durmus and Moulines cover nonincreasing step sequences and, among other regimes, potentials that are only strongly convex outside a ball; this mission formalizes that case.
Write and for the Euclidean norm and inner product of . The total variation norm of a difference of probability measures is
which ranges in .
The potential satisfies two assumptions:
The point is a minimiser of , and .
The Langevin diffusion is , with a standard -dimensional Brownian motion. Its transition semigroup is .
ULA with step sizes is the chain
with i.i.d. standard Gaussian. Its one-step kernel is , and is the law of started at . Write , and let .
The explicit constants use
Let , and let be positive and nonincreasing with . Then for all and ,
The three constants are explicit:
The paper's proofs follow each statement in the body of the paper (§4.1, §4.12, §5, §5.1).
The theorem bounds the sampling error of ULA in total variation non-asymptotically, with a dimension-free contraction rate and constants polynomial in . With steps decreasing to zero and cumulative step size diverging, its bound gives convergence of to ; for constant steps, the paper reports iteration counts of order at a prescribed precision in Table 2. H3 covers log-concave targets whose potential can lack strong convexity inside a ball.
The result is proved in the paper but, as far as the platform's catalogue shows, not formalized anywhere. A formalization adds machine-checked versions of several reusable pieces:
The ULA chain is not reversible with respect to , so the spectral and Dirichlet-form tools of reversible MCMC do not apply to it directly. The bound must instead compare the chain with the continuous diffusion.
That comparison needs Girsanov's theorem on path space and a uniform control of along a time-inhomogeneous chain.
The rate of the diffusion itself is the second obstacle. Without global strong convexity, synchronous coupling gives no contraction inside the ball . An explicit rate requires a reflection coupling together with return-time estimates, and it has to be transferred through the time change between and .
The state space is the published EthierKurtz.SDEState d, i.e. EuclideanSpace ℝ (Fin d), and Brownian motion and strong solutions are the published EthierKurtz.IsStandardBrownian and EthierKurtz.SolvesBrownianSDE. The conventions are:
Measure.bind with the Gaussian kernel . Steps are indexed from , and for .Several hypotheses are added or read in a particular way, and each is disclosed in the item's statement:
The citations [20] (existence of solutions), [27] (Lindvall), [32] (Meyn–Tweedie) and Girsanov's theorem are used inside the proofs and are not restated.
The library work needed is substantial: Itô calculus for the reflection coupling, Girsanov's theorem, Pinsker's inequality in this norm, and generator–drift arguments for the moments of . Contributions of any of these as standalone platform theorems are welcome.
The newsvendor problem is the basic single-period inventory decision: a retailer orders units at unit cost before a random demand is observed, sells at unit price , and loses unsold units. When the demand law is known, the optimal order is a quantile of that law. In practice the law is rarely known, and a distributionally robust newsvendor instead hedges against the worst law in an ambiguity set of laws consistent with partial information.
Scarf (1958; reference [42] of arXiv:1806.05379) solved the case where only the mean and the variance of demand are known, and observed that for a range of small profit margins the robust newsvendor orders nothing. Demand data in retail and spare-parts settings are often heavy tailed: Pareto fits with exponent close to have been reported, so a finite mean is plausible while a finite variance is not. Das, Dhara and Natarajan (arXiv:1806.05379) therefore replace the variance by an -th moment for an arbitrary real . This mission formalizes their result that the zero-order phenomenon survives for every such .
Write the critical ratio as . A demand law is a probability measure on . Fix a real and two moments with
The ambiguity set is
the laws on with mean and -th moment . The worst-case expected shortage is
and the robust newsvendor problem (3.2) is
An optimal order quantity is a minimizer of this objective. Two thresholds appear:
In Lean these are ambiguitySet, worstCase, robustCost, eta0, q0 and IsOptimalOrder in the namespace HeavyTailNV.ZeroOrder.
, and
and the two-point law with mass at and the rest at lies in and attains the supremum. 2. Properties of (§2.1, p. 6): is non-increasing and convex, for , and as . 3. Display (3.10) (p. 14): for and ,
Proposition 3.2 shows that for every finite moment order , however high, there is a nonempty interval of critical ratios in which the robust newsvendor orders nothing, and it gives the threshold and the minimum positive order in closed form. For it recovers Scarf's zero-order region. The worst-case law associated with therefore carries a positive mass at zero demand, which is the low-service-level counterpart of the paper's heavy-tail result for high critical ratios (the companion mission of this series).
The results are proved in the paper: the proof of Proposition 3.1 follows the statement on pp. 12–13 and the proof of Proposition 3.2 is on p. 14. None of them has a machine-checked proof. Formalizing them requires a usable treatment of moment-constrained suprema over probability measures on , of the stop-loss transform , and of minimizers of convex functions on a half-line. These pieces recur across robust inventory and pricing models.
The closed form of Proposition 3.1 is the central step. The lower bound is a computation with a two-point law. The matching upper bound has to hold against every law in , including laws with unbounded support and non-integer . The paper obtains it from a dual certificate for the moment problem (3.3)–(3.4), and weak duality for this semi-infinite problem is not available off the shelf. The closed form also holds only on . To conclude anything about minimizers on all of , where no closed form is known for general (the dual leads to equations , p. 11), one needs convexity of on the whole line. Inspecting the objective on alone does not determine the global minimizers.
Measure ℝ with IsProbabilityMeasure F and F (Set.Iio 0) = 0. Moments are Bochner integrals, and the set requires Integrable (fun w => w) F and Integrable (fun w => w ^ α) F (real rpow), so that the moment equalities are genuine.sSup. Under the standing hypotheses , , the set is nonempty (it contains the two-point law of Proposition 3.1) and the expectations are bounded above by , so the value is not Lean's default for an empty or unbounded set. Every statement carries these standing hypotheses of (3.1); no other hypothesis is added except the range in (3.10), which is the paper's standing range of the critical ratio.HeavyTailNV.Tail.Model. This mission defines the thresholds, optimality predicate and two-point law in HeavyTailNV.ZeroOrder.Model. Contributions to the general moment-problem duality used by Proposition 3.1 are welcome and reusable well beyond this mission.Robust Sample Average Approximation (Robust SAA) is a data-driven approach to stochastic optimization proposed by Bertsimas, Gupta and Kallus (arXiv:1408.4445; Mathematical Programming (2018), doi:10.1007/s10107-017-1174-z). Instead of minimizing the empirical average of a cost, a decision maker minimizes the worst-case expected cost over a distributional uncertainty set: the set of distributions that a statistical goodness-of-fit (GoF) test does not reject at a chosen significance level, given the observed data. Each classical GoF test therefore produces its own robust optimization model.
Whether such a model behaves well as data accumulate depends on a property of the test. Theorem 2 of the paper shows that Robust SAA converges, in objective, optimal value and optimal solutions, for every admissible cost if and only if the underlying test is uniformly consistent. This mission concerns the univariate case: it asks for a proof that the five standard tests on the real line, those of Kolmogorov–Smirnov, Kuiper, Cramér–von Mises, Watson and Anderson–Darling, are uniformly consistent (Theorem 5, p. 14). The companion missions of the series treat the characterization (Theorem 2) and the discrete χ² and G-tests (Theorem 4).
Let be a probability distribution on , and let be independent draws from . As in §3.2 of the paper, is a continuous random variable: has no atoms. For a candidate distribution write for its cdf, and write for the sorted sample of size . With , the five statistics (8) are
For a statistic and a threshold , the confidence region (7) is : the distributions the test does not reject. A test is uniformly consistent (Definition 3, p. 13) if, for every data-generating , almost surely every sequence that does not converge weakly to is rejected infinitely often, i.e. for infinitely many . The Lévy metric between cdfs is , and denotes the empirical cdf.
For thresholds with for some constant and all ,
The statement fixes only the rate of the thresholds, which is all the paper's argument uses; it holds for any sequence with that rate, in particular for the tabulated quantiles .
The result. Together with Theorem 2 of the paper, Theorem 5 guarantees that Robust SAA built on any of these five univariate tests converges for every cost that is equicontinuous in the decision and satisfies the paper's growth conditions. It also feeds Proposition 5, which extends the guarantee to multivariate problems with separable costs by testing marginals. Without it, the univariate tests would carry only the finite-sample guarantee of Proposition 1 and no asymptotic one.
The formalization. The theorem is proved in the paper, but the published argument for the Watson test has a gap. Its last step asserts that whenever , which fails when stays bounded away from (at the expression tends to ). The Watson clause is believed true, but a complete proof needs a different argument. The Anderson–Darling step relies on a cited integral representation rather than an argument on the page. A machine-checked proof would close both points. No part of the theorem is formalized elsewhere, as far as a search of the platform shows.
The Kolmogorov–Smirnov case reduces to deterministic inequalities once the Lévy-metric picture is in place, but each of the other statistics controls only indirectly. The Cramér–von Mises statistic is an quantity, and an bound does not by itself control a supremum. What closes the gap is monotonicity of together with the rate of the threshold, so a threshold that merely tends to is not enough. The Watson statistic is invariant under cyclic rotation of the transformed sample on the circle , so a small leaves the centring term uncontrolled until the boundary constraints are used. The obvious attempt, bounding the centring term by alone, is the step that fails on p. 39.
Distributions are MeasureTheory.ProbabilityMeasure ℝ, with weak convergence as their topology. The cdf is Mathlib's ProbabilityTheory.cdf. The data are the coordinates of the canonical product space ℕ → ℝ under Measure.infinitePi, so the sample of size is . Order statistics are the sorted sample s ∘ Tuple.sort s, and every formula of (8) is written with the paper's 1-based index ( in Lean is the paper's ; is Fin.rev i).
Committed conventions:
IsContinuousLaw), although the paper's proof does not use it;Uniform consistency is quantified over all sequences inside the almost-sure event, as in Definition 3. A pointwise consistency statement for a fixed is a different and weaker theorem and does not count.
A full development needs the Lévy metric and its metrization of weak convergence on , the Glivenko–Cantelli theorem in Lévy form, and elementary order-statistic inequalities. The first two are reusable well beyond this mission. Contributions of independent value include a corrected proof of the Watson step, and a proof of the goal without the atomless hypothesis.
A decision made from sampled data can be sensitive to the distribution chosen to represent future uncertainty. Robust sample average approximation addresses this by optimizing against every distribution that passes a goodness of fit test, rather than against one fitted distribution. The resulting set of plausible laws is a data driven uncertainty set. Its finite sample coverage and its behavior as the sample grows serve different purposes: coverage protects against sampling error at a chosen sample size, while convergence asks whether the uncertainty set eventually stops admitting laws far from the true one. Bertsimas, Gupta, and Kallus distinguish these properties in their Robust Sample Average Approximation paper.
This mission concerns the two tests the paper assigns to a known finite support: Pearson's test and the G test. Both compare the empirical frequencies of the observed support points with the probabilities under a proposed law. Their confidence regions give concrete uncertainty sets for discrete data. The paper's Theorem 4 states that both tests have the stronger convergence property it calls uniform consistency. That property is used in its general characterization of when robust sample average approximation converges for every admissible cost function (Theorem 2 and Table 1, pp. 13–14).
Fix a known set of possible observations, labelled . A probability law on this support is specified by probabilities , each nonnegative and summing to one. A sample of size consists of independent observations from an unknown true law . Its empirical frequency at label is
To assess a hypothetical law with probabilities , Pearson's statistic and the G statistic are, in the paper's normalization,
The confidence region for each test is the set of hypothetical laws whose statistic is at most , where is fixed across sample sizes. An observed point to which assigns zero probability makes either statistic infinite. A term with zero empirical frequency contributes zero to the G sum, including when its hypothetical probability is zero. These conventions make the regions describe the same tests at the boundary of the probability simplex as they do in its interior (§3.1, p. 8; §10.6, p. 38).
A sequence of laws is weakly convergent to when expectations of every bounded continuous function converge. On this finite support, weak convergence can be measured by the total variation distance
The paper's Definition 3 calls a test uniformly consistent when, for every true law , almost surely every sequence that fails to converge weakly to lies outside the confidence region infinitely often (Definition 3, p. 13). The almost sure event applies to all such sequences at once; this is stronger than a statement about one fixed false hypothesis.
For the Pearson and G confidence regions and with fixed , the target is
Here has the quantifier order of Definition 3: every generating , almost every infinite sample, and every nonconvergent sequence . This is Theorem 4, p. 14. Its four milestone claims are the finite support description of weak convergence, almost sure convergence of empirical frequencies, and the paper's total variation bounds for and (§10.6, p. 38).
The result says that distributions retained by either test cannot remain persistently separated from the data generating law as the sample grows. In the paper's framework, that is the statistical condition needed for its general theorem to turn test based confidence regions into convergent robust optimization values and decisions under its separate assumptions on the cost and feasible set (Theorem 2, p. 13). Theorem 4 itself concerns the tests; it does not assume a cost function or assert optimization convergence directly.
The paper proves Theorem 4, so the open work here is its Lean formalization. A complete development would also leave reusable statements for finite probability vectors, their empirical frequencies under an infinite product law, total variation, and the boundary aware Pearson and G divergences. These pieces can support other discrete goodness of fit and distributionally robust optimization results. The mission does not claim that Theorem 4 already has a machine checked proof.
Pointwise convergence of empirical frequencies does not by itself state uniform consistency. The latter quantifies over all moving hypothetical laws on one almost sure sample event, including laws chosen differently at every . A direct argument about one fixed therefore does not address the target. The finite support makes weak convergence concrete, but the formal statement must still relate that topology to a finite total variation sum and keep the quantifiers in the order required by Definition 3.
The boundary of the probability simplex is another source of difficulty. Lean's real division and logarithm have default values at zero. Using those defaults in the test statistics would accept some laws that assign zero probability to an actually observed category. Both statistics must instead retain the paper's infinite penalty there. The G expression also contains individual logarithmic terms that may be negative before summation, so its extended value cannot be built by coercing each term directly to a nonnegative extended real.
The known support is represented by Fin n. Its members are labels for the paper's distinct points ; coordinates in Euclidean space are irrelevant to these tests. Laws use Mathlib's ProbabilityMeasure (Fin n) and its weak topology. The data are coordinates of the canonical infinite product law, with Lean index zero corresponding to the paper's first observation. The empty support has no probability law; all substantive instances have . The empty sample is defined by total operations but has no bearing on an eventual or infinitely often assertion.
Pearson's statistic lives in . The squared G statistic uses extended real arithmetic so finite negative summands can be combined with an infinite boundary term. Its region compares with , equivalent to the paper's at positive . The free stands for a fixed threshold constant, including the paper's chi square quantile; no particular quantile value is built into the theorem. This makes explicit the only property of that threshold used in §10.6: independence from .
Contributions may prove the four milestone statements, connect Mathlib's finite probability and strong law interfaces to the empirical frequencies, or establish finite support versions of Cauchy–Schwarz and Pinsker with the correct infinite boundary cases. A proof of the goal must use the stated regions and preserve simultaneous quantification over every moving sequence of laws; replacing uniform consistency by convergence of would remove its main claim.
A McKean–Vlasov control problem asks a planner to steer a stochastic differential equation whose coefficients depend not only on the current path of the state but also on its (conditional) distribution. Such problems describe the cooperative optimum of a large population of interacting agents: when each agent reacts to the empirical distribution of all others and a social planner chooses everybody's control, the limit as the population grows is a McKean–Vlasov control problem (Lacker 2017). When all agents are also exposed to a common noise (a shared source of randomness, such as a market factor), the relevant distribution is the conditional law of the state given that noise.
Bellman's dynamic programming principle (DPP) is the standard route from a control problem to its Hamilton–Jacobi–Bellman equation and to verification arguments. For McKean–Vlasov dynamics it fails in the naive state variable, because the problem is time-inconsistent; it can be recovered by taking the (conditional) law of the state as the state.
Timeline. Laurière and Pironneau (2014) and Bensoussan, Frehse and Yam (2013–2017) proved a DPP for densities of the state law. Pham and Wei (2017, SICON) proved a DPP over closed-loop controls in a Markovian setting with a common-noise filtration, under regularity assumptions; Pham and Wei (2018, ESAIM:COCV) treated the case without common noise. Bayraktar, Cosso and Pham (2018, Trans. AMS) obtained a randomised DPP, again Markovian and without common noise. Djete, Possamaï and Tan (2022) proved the DPP for the general non-Markovian problem with common noise, under Borel measurability of the coefficients only. This mission formalizes their DPP for the weak formulation.
Fix a horizon , dimensions , a nonempty Polish space of control values, a point and an exponent . Let with the uniform norm, the Borel probability measures on with the weak topology, and the path stopped at time . The coefficients are maps , and ; all are Borel measurable, and depend on the path and the measure only through their restrictions to (non-anticipative).
A weak control with initial condition consists of a probability space carrying two filtrations (the second models the common noise), a state , Brownian motions (idiosyncratic) and (common) on , a predictable -valued control , and measure-valued processes and , such that , an integrability condition of order holds, a compatibility condition between the two filtrations holds, and
The reward and the value function are
with and . Each weak control also carries , where is a Borel isomorphism of onto a subset of , and the continuous conditional-law process of given .
is upper semi-analytic (every superlevel set is analytic), and for every stopping time of the canonical filtration of with values in , setting ,
The canonical reformulation on with weak control rules (Definition 4.1): Lemma 4.4(i) (weak controls and weak control rules correspond), Corollary 4.6 (), Lemma 4.7 (analytic graphs, u.s.a.), Lemma 4.8 (stability under conditioning at a stopping time), Lemma 4.9 (dependence on the initial law only through ), (4.10) (moment truncation , analytic and u.s.a.) and Lemma 4.10 (universally measurable -optimal families and concatenation).
The result. The theorem gives the DPP for McKean–Vlasov control with common noise in a non-Markovian setting, with no regularity on the coefficients beyond Borel measurability and no integrability on the rewards. It is the starting point for the dynamic programming (HJB) equation on the space of probability measures, for the Markovian corollaries of §3.2 of the paper, and, through the equivalence of formulations in the companion work, for the strong formulations treated in the second mission of this series.
Formalizing it. The result is proved on paper; nothing of it is machine-checked. A formal development needs a working theory of weak controls with conditional laws, a controlled martingale problem on a space of measure-valued paths, and analytic-set measurability in continuous time. None of these exists in Mathlib, and the analytic-selection layer on Prove2Me (Bertsekas–Shreve, Chapter 7) is stated but not yet proved.
The obvious argument conditions an optimal-ish control on its information at the stopping time and pastes in near-optimal controls from the conditioned states. Each step fails without additional structure: is not known to be measurable, so is not obviously meaningful; conditioning a weak control on its information at need not yield a weak control, because the conditional-law constraint involves the common-noise filtration and a compatibility condition between filtrations; and choosing a near-optimal control for each conditioned state is a selection problem over an uncountable family of probability spaces. The state of the problem is a law, which is itself defined only up to null sets, so random-time evaluations such as need a continuous version.
The Lean development lives in the namespace MKVDPP.Weak. Conventions:
Type (universe 0).EthierKurtz.HasBrownianItoIntegral) of integrands that are a.s. square integrable on , taken against the shifted Brownian motions , ; no condition, which would shrink .The goal does not mention the canonical space , weak control rules or any selection; a formalization of that is empty, or a value function that is constant, would trivialize it. A sanity file exhibits a weak control in the degenerate case for every , so the structure is satisfiable.
Infrastructure a complete development needs: conditional laws and r.c.p.d. on Polish spaces, the predictable -algebra, stochastic integrals against a filtration, the Stroock–Varadhan martingale problem, Itô's formula, and analytic sets with the Jankov–von Neumann selection theorem. The analytic-selection results and the martingale-problem/SDE correspondence are reusable well beyond this mission. Contributions on any milestone, and on proving the referenced Bertsekas–Shreve selection theorems, are welcome. Out of scope: Theorem 3.4 (it rests on the companion paper), the Markovian results of §3.2, and the HJB discussion of §3.3.
A newsvendor chooses an order quantity before seeing demand. Unsold units have no salvage value, while demand above the order quantity cannot be filled. If the demand law is unknown but a few moments are known, the decision maker may minimize cost against the worst distribution consistent with those moments. Das, Dhara and Natarajan study this distributionally robust problem when the known moments are the first and an arbitrary real moment of order Das, Dhara and Natarajan, 2019. The high-demand tail matters especially when the cost ratio favors large orders. The mission asks what tail behavior is implicitly selected by the robust objective, even though each admissible distribution has a finite th moment.
The two-moment case goes back to Scarf's newsvendor bound. The paper extends the model to noninteger and gives lower and upper shortage bounds before proving its tail result. Its preprint is the pinned source for every statement here; the proof of each numbered result follows that result in the paper Das, Dhara and Natarajan, 2019, §§1, 3–4.
Let be the order quantity and let be random demand. The expected shortage under a demand law is , where . Fix , a positive mean , and a moment . The moment ambiguity set contains all probability laws supported on whose first moment is and whose finite th moment is . Its worst-case expected shortage is
For a critical ratio , the robust newsvendor minimizes over . This mission centers on ; the optimal-order threshold is treated in the companion mission. The ambiguity set and objective are the paper's (3.1)–(3.3) Das, Dhara and Natarajan, 2019, pp. 10–11.
A positive function is regularly varying with index if as for every . The notation is . For a probability law , its survival tail is ; means a tail parameter Das, Dhara and Natarajan, 2019, §4.1, p. 26.
The first target is Theorem 4.3(a):
It covers every , including . Scarf's piecewise formula (1.3), Proposition 3.3, and both parts of Proposition 3.4 supply the paper's cited bounds. Each upper bound retains its strict quantity threshold and its printed denominator Das, Dhara and Natarajan, 2019, pp. 3, 15, 19, 28.
The full goal, Theorem 4.3, also states that a nonnegative probability law exists outside with
Every moment of of order is finite, while every moment of order is infinite. The milestone list includes the properties of stated in §2.1 (non-increasing, convex, for , ), the single-law representation (2.1) and the two stated Karamata results used to characterize the tail Das, Dhara and Natarajan, 2019, pp. 6, 27–30.
A companion milestone is Proposition 4.1. For let be a robust optimal order quantity and the optimal robust cost. Then is optimal for the standard newsvendor with demand law , and
Das, Dhara and Natarajan, 2019, p. 30, (4.9). It is a consequence of the goal, not a step toward it.
The theorem connects a decision made against an entire moment class to a single effective law. That law matches the robust expected shortage for every admissible order quantity but has an infinite th moment, so it does not belong to the class being optimized over. This distinction explains why large robust orders behave as though demand were heavy tailed. The paper also uses the result to relate the robust optimal order quantity to the optimal cost at high service levels in Proposition 4.1 Das, Dhara and Natarajan, 2019, pp. 30–31.
The mathematical theorem was proved in the cited paper. This mission asks for a Lean proof of its exact statement and reusable formal results for moment-constrained probability laws, stop-loss transforms, and regular variation. No machine-checked proof of these particular statements is part of the present draft. The cited bounds and analytic results are posed as separate milestones so their hypotheses and constants remain inspectable.
Pointwise optimization over demand laws does not automatically give one law that attains the worst-case shortage for every . For a fixed , an extremal law may depend on , as Scarf's formula illustrates Das, Dhara and Natarajan, 2019, p. 3. The theorem asks for a single and then a precise tail index and a sharp moment cutoff. A generic upper bound on shortages would establish neither the representative law nor its infinite th moment. The regimes , , and have different cited upper-bound statements, yet the final theorem has no regime restriction.
Lean represents a demand law by a Borel measure on with probability mass one and zero mass below zero. Membership in requires both real moments to be integrable; this makes the moment equalities genuine rather than default values of a nonintegrable Bochner integral. Under and , the paper's two-point law (3.6) makes the ambiguity set nonempty. Its shortage values are bounded above by , so the real supremum defining is finite and meaningful. The strict thresholds in Propositions 3.3–3.4 keep their power denominators positive Das, Dhara and Natarajan, 2019, pp. 12, 15, 19.
Regular variation includes eventual positivity, excluding a zero-over-zero ratio from passing as a tail law. Infinite moments of are lower Lebesgue integrals in extended nonnegative reals. The existence of is asserted rather than built into a definition. Theorem 4.2(b)'s displayed limit has a negative sign in the preprint, although its nonnegative numerator and denominator require the positive value ; the formal statement uses the corrected sign. Its regularly varying tail integral is eventually positive, which ensures genuine finite tail integrals for large lower limits. Theorem 4.1 explicitly requires local integrability. Two encodings would trivialize the goal and are excluded: defining inside the statement (it is existential), and a regular-variation predicate satisfied by the zero function. The properties of and the representation (2.1) are stated for , the instance the paper uses, rather than for a general finite-mean ambiguity set. In Proposition 4.1 the optimal cost is the cost at the chosen optimizer, the statement holds for every selection of optimizers, and means that the ratio of the two sides tends to as . These analytic conventions and the probability and measure infrastructure can be reused beyond this mission. Contributions to any of the ten source milestones, including the difficult root assertion in Proposition 3.4(b), are welcome.
A controller may act on a large population of interacting particles while all particles also experience a shared random disturbance. In the population limit, the state of a representative particle depends on the distribution of states conditional on the common noise. The controller therefore influences both its own state and the conditional population law. The usual state variable for dynamic programming must carry that law, and a future decision may use only information available from common noise. Djete, Possamaï and Tan establish a dynamic programming principle for this setting in McKean–Vlasov optimal control: the dynamic programming principle, Theorem 3.2. Their result permits path dependent coefficients and merely Borel reward functions, so ordinary continuity arguments do not determine the value function's measurability.
The paper distinguishes a weak formulation, in which the stochastic basis varies with the control, from a strong formulation on a fixed space. This mission concerns the latter, restricted to controls predictable from common noise, under the paper's Lipschitz and growth Assumption 2.8. The companion mission treats the weak dynamic programming principle, Theorem 3.1. The present mission asks for a machine checked account of the strong formulation and of the transfer between its intrinsic, fixed space and canonical descriptions.
Fix a horizon . A state trajectory belongs to . The two driving noises are a dimensional idiosyncratic Brownian motion and an dimensional common Brownian motion . The control space is nonempty and Polish. At time , the controlled drift and diffusions may depend on the stopped state path , the control , and the conditional law of the stopped state and control given common noise. The running and terminal rewards are and .
A strong control has a continuous state satisfying the controlled stochastic equation, the conditional laws required by the paper, finite quadratic control energy, and an predictable for the common noise filtration. Its reward is the expected running reward from to plus the terminal reward. The value is the supremum of these rewards over such controls from initial path law . The initial law lies in , the laws with a finite second moment. The coefficient hypothesis uses the quadratic Wasserstein distance and one constant for both a Lipschitz bound and a quadratic growth bound. These conditions are Assumption 2.8 of the source paper, p. 8.
The paper also fixes a canonical probability space carrying an initial path and Brownian increments after . Its common noise predictable controls form . Proposition 2.10 says this fixed space computes the same value as the intrinsic strong formulation. The precise probability law on is characterized by the initial stopped path law and independent standard Brownian increments; the paper does not choose a unique construction.
The goal is Theorem 3.2, p. 10. It first asserts that the value on is upper semi analytic: each strict superlevel set is analytic. For an initial pair and a stopping time for the raw common noise filtration on , it then asserts
Here is the law of the stopped state conditional on information from common noise at . The milestone sequence follows the paper's supporting results: strong solution existence and uniqueness (Theorem A.3(i)); equivalence of intrinsic and fixed space values (Proposition 2.10); induction of canonical rules from strong controls (the forward clause of Lemma 4.4(ii)); the canonical value identity (Corollary 4.6); the Wiener represented rule class and its value (Lemma 4.11); analytic rule graphs and value measurability (Lemma 4.12); and stability of a strong rule under conditioning at a stopping time (Lemma 4.13(i)). Each is a source indexed target, rather than an invented intermediate assertion.
The identity permits the value after a random common noise stopping time to be evaluated from the stopped conditional state law. This is the form needed to compare control decisions before and after a random observation time. Upper semi analyticity supplies measurable superlevel sets for the value even when and lack continuity. The paper proves these statements mathematically; the mission seeks their Lean formalization, not a new theorem about the underlying control problem.
A complete formalization would also provide reusable definitions of conditional measure valued flows, Brownian motion relative to a filtration over a shifted interval, a local Itô equation, and canonical martingale control rules. The two published Ethier–Kurtz definitions supply the local Itô relation and probability augmentation of a filtration. They are shared infrastructure rather than new statements of this paper.
The state law in the coefficients is conditional on common noise and changes with the control. A pathwise solution of the state equation must therefore remain consistent with its own conditional law. A naive argument that restarts an ordinary diffusion at does not establish that consistency for a restarted control. It also does not ensure that a restarted control remains predictable from common noise. The paper's canonical rule formulation and its conditioning and measurability results address those obstructions. The reward may be unbounded and extended real valued, so the expectation convention and its behavior at infinite positive and negative parts matter to the statement itself.
Paths are continuous maps on compact real intervals with uniform norm; is Mathlib's Euclidean space, including . Probability measures carry weak convergence topology, and is its finite second moment subtype. The product of path space and uses Mathlib's product metric; matrix norms are Frobenius. Supremums range over admissible controls, solutions and conditional law versions. They are EReal valued, so the empty supremum is . The signed expectation is positive part minus negative part with , as in the paper. The model fixes a Borel embedding of into and a cemetery control for invalid reconstructed paths.
The Lean statements pin the paper's implicit “well defined” stochastic integral to a pathwise square integrable local Itô relation and almost surely integrable drift. A conditional law equality stated for almost every pair is expressed in Fubini form. The localized processes printed in Definition 4.1 define its local martingale requirement. The terminal law and the stopped law in the target are quantified as versions of their stated conditional distributions. The fixed canonical law is any law satisfying the paper's initial distribution and Brownian conditions; the target is stated for every such family. These conventions rule out free conditional laws, arbitrary future stopping times, and a value that is solely because a formalization made the control class empty. A full development must establish nonemptiness and version independence as part of the cited supporting theory.
The scope ends with Theorem 3.2 and the listed milestones. Lemma 4.13(ii), the more involved measurable selection and concatenation result, remains a future contribution. Theorem 3.4 uses a separate companion result; the Markovian corollaries and the heuristic Hamilton–Jacobi discussion of §3.3 are outside this mission.
Systems of two first-order hyperbolic equations with opposite transport speeds model open-channel flow (the Saint-Venant equations), gas pipelines, heat exchangers and traffic. In such systems one boundary is actuated, the other boundary reflects, and the coupling terms move energy between the two families of waves. Boundary feedback design for them is a standard problem of distributed-parameter control.
The backstepping method designs a feedback by means of an invertible Volterra integral transformation that turns the plant into a target system whose behaviour is known in closed form. Coron, Vazquez, Krstic and Bastin (arXiv:1208.6475; SIAM J. Control Optim. 51(3), 2013) carry out this design for a general linear hyperbolic system with spatially varying speeds and couplings, in §3 of their paper. The resulting linear feedback is the controller they later apply to a quasilinear system. This mission formalizes the linear result.
Timeline:
Let be functions on with , let be continuous, and let . The state solves
so travels to the right and to the left. The boundary conditions are and , where is the control. The norm is .
The kernels are functions on the triangle that solve
with and . The control law (3.48) is
The target system is with and , for . The direct transformation is (3.23), with the full kernel of (3.30)–(3.37). The inverse transformation is (3.38), with solving (3.40)–(3.47). The finite time is
For , every classical solution of the closed loop satisfies
Here depends on and the data but not on the solution.
The theorem shows that a single linear boundary feedback, computed once from the coefficients, drives every state of the system to zero in exactly the time . That time is the sum of the travel times of the two characteristic families across . Exponential stability at every rate follows. The same feedback, rescaled, is the controller of the paper's main result, Theorem 4.1: local exponential stabilization of a quasilinear system, the subject of mission 3 of this series. The well-posedness of the kernel equations, Theorem A.1, is mission 1.
The result is proved in the paper. As far as is known, none of it has been machine-checked. A formal proof needs Volterra transformations of vector-valued functions with differentiation under a variable-limit integral, explicit solutions of transport equations along characteristics, and estimates for integral operators with continuous kernels. These tools apply to backstepping designs well beyond this paper.
Proposition 3.1 and the two mapping statements are calculations: an integration by parts and the explicit solution along characteristics. The difficulty of Theorem 3.2 is the step "the transformation is invertible", which the paper's proof takes for granted. The goal hypothesizes only , so it is not enough to state the mapping and the inverse separately. The solver has to recover the full state from the target state: either build the remaining kernels and the inverse kernel , or argue directly from the closed subsystem. Both routes need existence or uniqueness for Goursat-type problems, which the paper proves only in Appendix A. A second, routine obstacle is that the uniform constant must be extracted from the finite-time interval using bounds on the kernels.
w : ℝ → ℝ → Fin 2 → ℝ, space first, with Lean index 0 for the paper's first component.Three trivializing readings are excluded. The constant is quantified after the data and before the solution, so it cannot depend on the solution. The finite-time claim is vanishing for every , with exactly (3.8), not for some unspecified time. The kernels are pinned down by all four of (3.32), (3.33), (3.36), (3.37). With coefficients a solution exists (the paper's Theorem A.2), and a sanity file checks that the hypotheses admit a non-zero closed-loop solution.
Welcome contributions: lemmas on differentiating , transport equations along characteristics, and the invertibility of Volterra operators with continuous kernels.
The paper's proofs are on pp. 3–5 (Proposition 3.1), p. 5 (§3.2), p. 6 (§3.3) and p. 7 (Theorem 3.2).