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.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Bounded-depth Frege systems are the proof systems of propositional logic in which every formula of a proof has depth bounded by a fixed constant ; the resulting system is written . They are the proof-theoretic counterpart of the circuit class and of the bounded arithmetic theories and its relatives: short -proofs of a family of tautologies correspond to proofs of the corresponding first-order statement in bounded arithmetic. Lower bounds for are among the strongest lower bounds known for any natural proof system.
A basic structural question is whether the depth hierarchy is strict in a strong sense. It is known that one extra level of depth can give an exponential speed-up, but in all known separations the tautologies themselves have depth growing with . J. Krajíček asked whether there is a single fixed depth at which tautologies witnessing the separation of from exist for every (Open Problem Garden, F_d versus F_{d+1}; [Krajíček 1995, p. 243]). The question is closely related to conservativity relations among bounded arithmetic theories.
Timeline.
Formulas. A formula is in negation normal form over variables : a literal or , a conjunction or a disjunction of any finite number of formulas. The depth of a literal is , and the depth of or is (so clauses have depth and CNFs depth ). The size is the number of symbols (literals and connectives). A tautology is a formula true under every assignment. The negation of a formula is obtained by De Morgan's laws.
The system . Lines of a proof are sequents: finite lists of formulas, read as their disjunction. The rules are: (axiom) any containing both and ; () from for every infer ; () from infer ; (weakening) from infer any containing every member of ; (cut) from and infer . An -proof of is a sequence of sequents, each following from earlier ones by a rule (lines may be reused), in which every formula has depth at most , and which contains the sequent consisting of alone. Its size is the total size of all formulas in it.
Write for a family of tautologies of depth at most with . It requires exponential -size if for some and all large every -proof of has size at least .
The goal takes the weaker of the two upper bounds allowed by the problem (quasi-polynomial); the polynomial version implies it.
A positive answer would show that the extra power of depth over depth is visible already on formulas of a fixed, small depth, in particular that the hierarchy of bounded-depth Frege systems does not collapse on (for example) CNF tautologies. Through the correspondence with bounded arithmetic it bears on conservativity of theories of increasing quantifier complexity over a fixed class of low-complexity statements. A negative answer would say that for low-depth tautologies the bounded-depth Frege hierarchy collapses up to quasi-polynomial size.
Status: the goal is open. Milestones 1–2 are standard; milestones 3–4 are published theorems that, to the best of current knowledge, have no machine-checked proofs. Formalizing them requires switching-lemma machinery that would be reusable across proof complexity.
The known lower bounds for go through switching lemmas that simplify depth- formulas under random restrictions. In the known separations of from the hard tautologies have depth growing with . Keeping the formulas at one fixed depth while ranges over all values requires a lower-bound argument whose strength depends on the depth of the proof lines alone, uniformly in ; the switching-lemma arguments used for depth-dependent separations do not directly provide this.
Formulas are the Lean inductive type FdVersusFdSucc.Formula over variables ℕ, with conjunctions and disjunctions of lists (so and [] is true and or [] is false). Depth counts literals as . is the dag-like one-sided sequent calculus described above; sequents are lists, weakening is by list inclusion. Proof size counts symbols of all formulas in all lines. Exponential lower bounds are asked only for all sufficiently large indices. The goal quantifies over : for no -proof of a depth- formula exists, so "every " cannot be meant literally. A family whose formulas have depth would satisfy the lower bound vacuously; this is excluded because the formulas must have depth at most . The size condition rules out finite families.
Contributions welcome: proofs of soundness and completeness, a formalized switching lemma, and the classical lower bounds.
Rendezvous search asks how two agents who cannot communicate should move so as to meet as quickly as possible. It was introduced as a mathematical problem by Alpern (The rendezvous search problem, SIAM J. Control Optim. 1995) and developed systematically in Alpern and Gal's monograph The Theory of Search Games and Rendezvous (Kluwer, 2003). Besides its game-theoretic interest, it is a model for coordination without prior agreement: robots or searchers that must find each other with no shared map or orientation.
The simplest non-trivial domain is the line. Even there, the version in which both agents must follow the same strategy remains open, and it is listed on the Open Problem Garden with importance "High".
Timeline:
Two players are placed on the real line at distance ; player I starts at and player II at . Each player has a private sense of "forward", fixed by an independent fair coin, so neither knows in which direction the other lies. Both move with speed at most .
A feasible path is a function with and for , describing a player's position in its own frame. A mixed strategy is a probability distribution over feasible paths, realised as a probability space and a random path whose position at each fixed time is measurable.
If player I follows with orientation and player II follows with orientation , their positions are and . The meeting time is
For strategies with independent randomisations, the expected meeting time averages over , and the four equally likely orientation pairs. The symmetric rendezvous value and the asymmetric rendezvous value are
An integer zigzag is a path that on each interval , , moves with velocity or ; denotes the infimum of over strategies supported on integer zigzags.
This is the Han–Du–Vera–Zuluaga conjecture and answers the Open Problem Garden question. A formal disproof is equally valuable.
The value measures the cost of symmetry in the most basic rendezvous problem: when roles can be pre-assigned, while the best known symmetric strategies need about . Determining exactly would settle a problem that has been open since 1995 and would calibrate numerical methods (linear and semidefinite relaxations over discretised strategies) used for related search games.
None of these results is formalized. The milestones are proved on paper; formalizing them requires a measure-theoretic treatment of mixed strategies over path space, a rigorous version of the discretisation argument, and certified numerical bounds. The goal itself is open.
The obvious approach is to optimise over finitely many turning times, but a symmetric strategy must be randomised (any deterministic symmetric strategy fails to meet with probability , when both players face the same way), so the optimisation is over probability distributions on infinite paths and the objective is a quadratic, non-convex function of the distribution. Truncating to finite horizons gives upper bounds by explicit strategies, but lower bounds require controlling all strategies, including those that delay indefinitely, and the known gap – has resisted closing.
All values live in and expectations are Lebesgue integrals of non-negative functions; a strategy that fails to meet with positive probability has value . Sample spaces range over a fixed universe, which loses no generality. Paths are required to be -Lipschitz on with , and positions at fixed times are measurable, so meeting times are random variables. The four orientation pairs are weighted equally. The infimum in ranges over all such strategies, not only over integer zigzags; the restriction appears only in . A trivializing reading (e.g. a meeting time of or an unrestricted speed) is excluded: by construction every strategy pair has expected meeting time at least .
Contributions are welcome on: measurability of hitting times for continuous processes, the discretisation argument, explicit strategies with certified expected meeting times, and certified lower-bound certificates.
A large family of random growth models, interacting particle systems and directed polymers in one space dimension share a common, non-Gaussian fluctuation theory: observables of size fluctuate on the scale (instead of the central-limit scale ), with spatial correlations on the scale . This family is the Kardar–Parisi–Zhang (KPZ) universality class, named after the 1986 physics paper of Kardar, Parisi and Zhang. The KPZ universality conjecture (Open Problem Garden, posted 2020, importance "High") asks for a central limit theorem for this class: any one-dimensional growth model with a smoothing mechanism, short-range noise and slope-dependent ("lateral") growth should exhibit KPZ fluctuations.
KPZ fluctuations have been proved only for models with exact algebraic structure, such as the corner growth model / totally asymmetric exclusion process (Johansson, 2000) and the polynuclear growth model (Prähofer–Spohn, 2002). The Open Problem Garden entry describes ballistic deposition (Vold, 1959) as a concrete growth model with the KPZ features. Corwin's survey states the prediction that its column heights fluctuate like and notes that "this prediction has not been proved" (Corwin 2012, §1.1.1). Ballistic deposition has no known exact solvability, so it tests universality itself rather than one integrable instance of it.
Timeline.
The gap between and is open; the predicted order is .
Columns are indexed by . Each column carries an independent rate-one Poisson clock: on a probability space the inter-arrival times , , are independent and -distributed, and the -th ring of column (counting from ) is at time .
Random deposition. The height of column at time is the number of rings of its clock in . Columns are independent and is Poisson with mean .
Ballistic deposition (nearest-neighbour model, flat initial surface). Write for the height of column at time , with . When the clock of column rings at time , a unit block falls in column and sticks at the first point of contact, so
and all other columns are unchanged. On the finite substrate only clocks in ring and columns outside stay at height ; the finitely many rings in are applied in time order. The height on is the monotone limit . The next-arrival height is . This is the model of Penrose (2008) with and the nearest-neighbour displacement function, and the model (1) of Sudijono (2026) with .
This is the statement "the column height fluctuates around its mean like " (Corwin 2012, §1.1.1; Sudijono 2026, §1). The constants are left unspecified because they are model-dependent.
The predicted scaling limit: converges in law to the Tracy–Widom GOE distribution for some model-dependent .
A proof of the goal would establish the KPZ exponent for a growth model without exact solvability, which is the content of the universality conjecture as opposed to its integrable special cases. For ballistic deposition only is currently known.
On the formal side, the milestones are known results with published proofs; formalizing them requires a library for continuous-time interacting particle systems on (graphical constructions, monotone couplings, finite speed of propagation), subadditive ergodic theory, and concentration inequalities for Poisson-driven processes. These pieces are reusable for first-passage percolation and other growth models. The goal itself is open.
The standard tools give the wrong exponents. Bounded-difference concentration applied to a last-passage representation fails because adding one clock ring can change future heights by an unbounded amount (Sudijono 2026, §1); martingale hitting-time arguments reach only the diffusive bound . Lower bounds of Pemantle–Peres type reach only , as in first-passage percolation, where the analogous gap is also open. The exact formulas (determinantal structure, Bethe ansatz) behind the proved instances of KPZ fluctuations are not available for ballistic deposition.
The model is encoded on a general probability space with inter-arrival times τ : ℤ → ℕ → Ω → ℝ satisfying IsPoissonClocks P τ (measurability, mutual independence over ℤ × ℕ, each law expMeasure 1). The finite-substrate process boxHeight τ L t ω sorts the rings in lexicographically by (time, column) and folds the update rule bdStep; bdHeight τ t x ω : ℕ∞ is the supremum over . Real-valued statements use bdHeightReal, which is bdHeight cast to ℝ with the value on the event ; this event is null (Milestone 2), so the convention does not affect any distributional statement. Ties between rings and non-divergent arrival times are null events and receive junk values. Variances are Mathlib's variance, which returns for non-square-integrable variables; the lower bound in the goal therefore also forces square-integrability, so the goal cannot hold vacuously. Moments in Milestone 2 are lower Lebesgue integrals in , so they are not trivialised by non-integrability.
Contributions welcome: the graphical construction and its basic properties (monotonicity in and , a.s. finiteness), the duality with seed-grown deposition, subadditivity of hitting times, and the Poisson CLT.
Structural stability asks when the qualitative behaviour of a dynamical system survives small perturbations. A diffeomorphism of a closed manifold is structurally stable if every diffeomorphism close enough to is topologically conjugate to : some homeomorphism of the manifold satisfies , so that carries orbits of onto orbits of . Systems that model physical phenomena are only known up to small errors, which is the original reason for interest in this notion (Andronov–Pontryagin, 1937).
In the 1960s Smale introduced Axiom A, a uniform-hyperbolicity condition on the nonwandering set, and showed that it yields a detailed description of the dynamics (spectral decomposition, symbolic dynamics). Palis and Smale conjectured that structural stability forces this hyperbolic structure. The conjecture appears on the Open Problem Garden as the Stability Conjecture (openproblemgarden.org/op/c_r_stability_conjecture, rated Outstanding): any structurally stable diffeomorphism is hyperbolic. The same page describes the higher-regularity case as one of the most important and difficult problems in dynamical systems.
Timeline.
For every the "only if" direction remains open.
Let be a closed manifold: a compact Hausdorff smooth manifold without boundary, of dimension . For an integer , is the set of diffeomorphisms , with the topology: is close to when, in finitely many charts and on compact sets, and its derivatives of order are uniformly close to those of .
For every closed manifold , every and every ,
The case is Mañé's theorem; the cases are open.
The result. A positive answer would give a dynamical characterization of structural stability in every regularity: together with the theorems of Robbin and Robinson (Axiom A plus strong transversality implies stability), it would show that structurally stable diffeomorphisms are exactly the hyperbolic ones with transverse stable and unstable manifolds. Every structurally stable system would then inherit Smale's spectral decomposition and its symbolic models. In the topology this picture is complete (Mañé); in higher regularity it is not known whether a structurally stable system can fail to be hyperbolic.
Formalizing it. The mission produces a common Lean vocabulary for hyperbolic sets, Axiom A, and structural and -stability of diffeomorphisms of closed manifolds, compatible with the existing topology and nonwandering-set definitions on the platform. The proved cases (Anosov, Franks, Mañé, Palis) are milestones whose formal proofs would be new contributions; the goal itself is open for .
The known proof rests on perturbation tools that work only in the topology: Franks' lemma (realizing any small change of the derivative along a periodic orbit by a -small perturbation), Pugh's closing lemma and Mañé's ergodic closing lemma. In the topology, , a perturbation that changes the derivative by a fixed amount on a small ball has large higher derivatives, so these local constructions are not -small; Gutierrez's examples on the torus show that the local perturbation schemes used for the closing lemma cannot work in the topology. Whether periodic points are even dense in for a structurally stable is a case of the closing problem, itself open.
[TopologicalSpace M] [T2Space M] [CompactSpace M], a ChartedSpace structure over EuclideanSpace ℝ (Fin n) and IsManifold (𝓡 n) ∞ M (smooth, no boundary). is ClosingLemma.Diff n M r with the weak topology ClosingLemma.crTopology r (published definition ClosingLemma_DiffeoCrTopology); on compact it coincides with the strong topology. is a natural number with ; is not covered.PughClosingLemma.nonwanderingSet (published definition PughClosingLemma_nonwandering).mfderiv and an arbitrary continuous Riemannian metric (Bundle.ContinuousRiemannianMetric on the tangent bundle); since is compact, the choice of metric only changes . Continuity of the splitting is not assumed, being a consequence of the estimates. A periodic point is hyperbolic when its finite orbit is a hyperbolic set, which is equivalent to the eigenvalue condition.A basic aim of the theory of dynamical systems is to describe the long-term behaviour of typical orbits of typical systems. In the 1960s Smale's programme hoped that hyperbolic (structurally stable) systems would be dense, so that the asymptotic behaviour of a dense set of systems would be described by finitely many hyperbolic pieces. This hope fails: there are open sets of diffeomorphisms none of which is hyperbolic. Jacob Palis proposed a replacement global picture, in which hyperbolicity is replaced by a statistical requirement: for a dense set of systems, the asymptotics of Lebesgue-almost every orbit is captured by finitely many attractors. The problem appears on the Open Problem Garden (page), rated Outstanding, with the monograph of Bonatti, Diaz and Viana as reference.
Timeline.
The conjecture is open in general.
Let be a compact, connected, boundaryless smooth manifold of dimension . For let be the space of diffeomorphisms of and the space of vector fields, both with the topology (uniform convergence of the maps and of their derivatives up to order in charts).
For a diffeomorphism and , the -limit set is the set of accumulation points of the forward orbit , ; for a flow it is the set of accumulation points of as . The basin of a set is
Following the source, is an attractor if it is invariant (, resp. for all ), transitive (some point of has a forward orbit dense in ), and has positive Lebesgue measure. A set has Lebesgue measure zero in if its image in every chart has Lebesgue measure zero in ; this notion does not depend on the smooth atlas.
For every there is a dense set such that every has finitely many attractors with
and likewise there is a dense set such that the flow of every has finitely many attractors whose basins cover Lebesgue-almost all of .
The result. A positive answer would give a dense set of systems whose statistical behaviour is completely described by finitely many invariant pieces, providing a global substitute for the failed density of hyperbolicity. It underlies Palis' companion conjectures on the existence of finitely many physical (SRB) measures and their stochastic stability.
Formalizing it. The full conjecture is open. The mission produces a reusable formal language for diffeomorphisms and vector fields of compact manifolds, density, Lebesgue-null sets on manifolds, -limit sets, basins and attractors, together with formal statements of the classical cases (circle diffeomorphisms; Peixoto's theorem on orientable surfaces).
The obvious route — perturb to a hyperbolic system and invoke the Axiom A theory — fails because hyperbolic systems are not dense in dimension for diffeomorphisms (Newhouse phenomenon, robust homoclinic tangencies and heterodimensional cycles). One must control systems near which non-hyperbolic phenomena persist on open sets, where generic systems can have infinitely many sinks, and still find dense subsets with finitely many attractors. Even in the classical cases the proofs require the full machinery of hyperbolic critical elements, stable manifolds and the Kupka–Smale theorem.
EuclideanSpace ℝ (Fin n) and a manifold structure IsManifold (𝓡 n) ∞ M; the model has no boundary, so is boundaryless.M ≃ₘ^r⟮𝓡 n, 𝓡 n⟯ M; vector fields are sections (x : M) → TangentSpace (𝓡 n) x, of class when is into the tangent bundle.omegaLimit along atTop. Transitivity means the closure of a forward orbit of a point of equals .A central question in smooth dynamics is how much of the long-term behaviour of a system is captured by its periodic orbits. Every periodic point is nonwandering (each of its neighbourhoods returns to itself under some iterate), but a nonwandering point need not be periodic. The closing lemma asks whether this gap can be removed by an arbitrarily small perturbation: given a nonwandering point of a diffeomorphism , is there a diffeomorphism , as close to as desired, for which is a periodic point?
The answer controls the generic picture of dynamics. Pugh's General Density Theorem, which rests on the closing lemma, says that for a generic diffeomorphism of a closed manifold the periodic points are dense in the nonwandering set. Results of this kind underlie the -generic theory of dynamical systems (stability conjectures, generic properties of homoclinic classes). Whether the same holds for smoother perturbations is open; the question appears on the Open Problem Garden (closing lemma for diffeomorphisms, rated Outstanding) and is Problem 10 on Smale's 1998 list of mathematical problems for the next century.
Timeline.
For general diffeomorphisms and every the problem remains open.
Let be a closed manifold: a compact Hausdorff smooth manifold without boundary, of dimension . For , is the set of diffeomorphisms of .
The topology on is defined through charts. For , smooth charts and of , a compact set with , and , the basic set
collects the diffeomorphisms whose local representative has all derivatives of order at most uniformly within of those of on . These sets generate the (weak) topology; on a closed manifold it coincides with the Whitney topology.
For a map , a point is nonwandering if every neighbourhood of satisfies for some ; the set of such points is the nonwandering set . A point is periodic for if for some .
For every closed manifold , every , every and every :
A closing lemma for would give, through the same Baire-category argument as in Pugh's work, a General Density Theorem: -generic diffeomorphisms would have periodic points dense in the nonwandering set. Much of the -generic theory would then become available in the smoother topologies used in smooth ergodic theory, where distortion estimates need at least regularity.
On the formal side, the mission produces a reusable definition of the topology on diffeomorphism groups, which Mathlib does not currently provide. The case is a theorem (Pugh 1967) without a machine-checked proof; formalizing it, and the compatibility of the two topologies, are concrete sub-goals. The case is open, so a proof of the goal would be a new mathematical result.
A perturbation that makes an almost-returning orbit close up must move the orbit by a distance comparable to how close it comes back. With control, the perturbation can be spread over many iterates, and its size stays small because derivatives are only constrained to first order. For , the norm of a bump of displacement supported on a set of diameter scales like , and spreading the perturbation along the orbit no longer keeps it small. Gutierrez's examples show that the local perturbation schemes that work for do fail in the topology, so the natural first idea of copying Pugh's argument is ruled out.
EuclideanSpace ℝ (Fin n) and a manifold structure (IsManifold (𝓡 n) ∞ M), assumed compact and Hausdorff. Because the model space has no corners, has no boundary.Diffeomorph (𝓡 n) (𝓡 n) M M r, with a natural number.ClosingLemma.crTopology r is generated by Hirsch's basic sets, using charts of the maximal atlas and Fréchet derivatives of order of the local representatives at points of . The goal quantifies over all neighbourhoods of for this topology.PughClosingLemma.nonwanderingSet, shared with the existing statements of Pugh's theorems; periodic points are Mathlib's Function.periodicPts (period at least ).Infrastructure that would help: a usable API for the topology (basic neighbourhoods, compatibility under change of charts, the Baire property of ), and local perturbation lemmas (bump-function perturbations of the identity supported in a chart, with estimates). Contributions of these as separate lemmas are welcome.
A decision maker is time-inconsistent when the plan that is optimal today stops being optimal tomorrow. The standard source is non-exponential discounting: a reward units of time ahead is weighted by , and unless is exponential the relative weight of two future dates changes as time passes. Hyperbolic and pseudo-exponential discount functions, which fit experimental and group-decision data better than exponential ones, all have this property. For such an agent "optimal control" is not a meaningful target, and the literature instead looks for equilibrium policies: plans that no current self wants to deviate from, given that all future selves follow the plan.
In discrete time the definition is unambiguous: a policy is an equilibrium if deviating at the current step alone does not help. In continuous time there is no "current step", and the usual definition, due to Ekeland and Lazrak (2006), compares the payoff of the plan with that of a deviation on a short interval through a first-order condition as . Huang and Zhou (arXiv:1809.09243, Math. Oper. Res. 2021) call this a weak equilibrium, introduce a strong equilibrium that requires the deviation to be unprofitable for every small , and study both for a controlled finite-state Markov chain.
A natural question is whether continuous-time equilibria are the limits of the discrete-time ones as the time step shrinks. This mission formalizes the paper's answer (§5.1): limits of discrete equilibria are always weak equilibria. The paper's Example 5.1 shows they need not be strong.
The state space is . A continuous-time Markov chain on is controlled through its generator : in state the row is chosen from an admissible set , and the control space is . A payoff function gives the reward at time-distance from now, in state , under row . The standing assumptions are continuity of on and, for each , integrability over of (condition (2.3)). The expected payoff from state is
and . With the generator that uses on and afterwards, is a weak equilibrium if for all and . The first-order quantity is .
Discretization. Fix a mesh . A transition matrix (rows in the probability simplex ) has generator , the admissible matrices are , and the discrete payoff is . The discrete value is , and is a discrete equilibrium if for all and , where uses at time and afterwards. The continuation values are . Theorem 5.2 additionally assumes (5.8): for some , is nonincreasing on .
Let , let be an equilibrium of the problem with mesh , , and suppose is continuous on . If along a subsequence, then
The theorem justifies the weak-equilibrium notion from discrete time: whatever a time-inconsistent agent does on a fine time grid, the continuous-time limit satisfies the first-order condition (3.10). Combined with the paper's discrete existence result (Theorem 5.1) and compactness of , it yields weak equilibria by approximation (Remark 5.3). It also locates the gap between the two notions: the limit is weak but in general not strong.
The result is proved in the paper; nothing about it is open. No part of it has a machine-checked proof. A formal development adds a checked Euler-scheme comparison between and for generator matrices, a dominated passage to the limit for Riemann sums of the payoff, and continuity of the payoff in the generator, each reusable for other finite-state continuous-time control problems.
The obvious argument is to divide the discrete one-step inequality (5.12) by and let . Its algebraic part is immediate. The difficulty is the convergence of the discrete continuation values , which are infinite sums along a discrete chain with transition matrix , to the continuous payoff , an integral along the continuous chain with generator . Three errors must be controlled at once: the discrete chain against the chain sampled from (the difference of -th powers grows with ), the Riemann sum against the integral (needs uniform continuity of jointly in and ), and against . The tail of the infinite sums is not controlled by (2.3) alone: integrability of a majorant does not make its samples on a grid summable, which is why (5.8) is assumed. A second subtlety concerns the last step: the paper passes from (3.10) to the weak-equilibrium property through Theorem 3.1, which assumes a condition (3.3) that Theorem 5.2 does not. The conclusion is still true without (3.3), but no numbered statement of the paper provides that step.
Fin N; rows are Fin N → ℝ with the sup norm, generators and transition matrices are Matrix (Fin N) (Fin N) ℝ with the product topology.tsum). No Markov process is constructed.In a prophet inequality a gambler sees the realizations of independent nonnegative random variables one at a time and must decide irrevocably, at each step, whether to stop and keep the current value. Her performance is compared with that of a prophet who sees everything in advance and takes the maximum. The ratio between the two is the standard benchmark for online selection, and through the correspondence between threshold stopping rules and posted prices it governs the efficiency of sequential posted-price mechanisms in algorithmic mechanism design.
The constant depends on the order in which the values arrive. In adversarial order the best guarantee is (Krengel and Sucheston; Samuel-Cahn). For independent and identically distributed values it is about (Hill and Kertz 1982 gave the upper bound; Correa, Foncea, Hoeksma, Oosterwijk and Vredeveld 2017 proved it tight). The prophet secretary problem sits between these two: the distributions may differ, but the values arrive in a uniformly random order.
Timeline.
Before this bound no separation between the prophet secretary problem and the i.i.d. prophet inequality was known.
An instance with variables is a family of laws on . The values are independent. A permutation of , uniform and independent of the values, fixes the arrival order: at time the gambler sees which variable arrives and its value .
A strategy decides at each time whether to stop. The decision may use the observed history and an independent seed , uniform on , and must depend on them measurably. These are the randomized stopping times of the gambler's information. The gambler knows the distributions, so a strategy may be chosen after the instance. The reward is : the value at the first stop, and if she never stops. The value of a strategy is , and the prophet's value is .
A strategy guarantees if on every instance.
The §5 instance has variables, for and . Each of equals with probability and otherwise, and . For , the time- rule accepts a value whenever one appears, and accepts exactly when it arrives at time or later.
For every there is an instance with on which every strategy satisfies
The instance comes first and all strategies second. This is what "no strategy can guarantee more than " means once strategies may depend on the distributions. Universally quantifying a fixed strategy first would describe a weaker gambler.
At the ratio of milestones 4 and 1 tends to .
The bound shows that random order with non-identical distributions is strictly harder for the gambler than i.i.d. values: the constant cannot exceed , which is below . It improves the bound of Azar, Chiplunkar and Kaplan and extends it from deterministic distribution-insensitive algorithms to all strategies, including randomized ones that know the distributions. With the guarantee of the same paper, it brackets the optimal prophet secretary constant in . Later work raised the lower end, but the exact value is still open.
The result is proved in the paper. It is not formalized anywhere we know of, and no prophet secretary statement exists on the platform. Formalizing it means writing down a general model of randomized stopping strategies in random order, which other random-order results can reuse. The heart of the proof is a dynamic-programming argument that is easy to state informally and has never been machine-checked. The finite- bound of milestone 4, with an explicit constant in place of , is also a welcome contribution.
Computing the value of one good strategy on the §5 instance is routine (milestone 3). The goal, though, quantifies over every strategy, including randomized ones that observe identities and the whole history. The paper's sentence "Solving the dynamic programming, the algorithm picks the value if and only if it appears at time or later" carries the whole reduction. It requires:
Bounding a few natural strategies does not suffice. The asymptotic analysis must also be made uniform in the strategy, so that a single constant in works for all of them.
Fin (n+1), and is Fin.last n.Measure.pi μ.volume.restrict (Icc 0 1)).ENNReal.ofReal of the reward, so no integrability hypotheses appear.Strategy N) is the class of all measurable decision rules on the full observed history plus an independent seed, and it is quantified after the instance. Restricting it to threshold rules, time- rules or deterministic rules would make the goal a different, weaker theorem; that restriction is ruled out. The class is nonempty, and its measurability requirement is satisfiable: jRule carries its proof.Reusable infrastructure includes the random-order stopping model, the reward of the first stop, and the dynamic-programming reduction for a single deterministic variable. Contributions are welcome on any milestone, and on an explicit in milestone 4.
In many dynamic decision problems the criterion an agent uses today is not the one it will use tomorrow. The standard example is non-exponential discounting: if a payoff received periods from now is weighted by and is not geometric, then the plan that is optimal from today's point of view will be abandoned by the agent's future selves. Such problems are called time-inconsistent, and since Strotz (1955) the usual response is to look not for an optimal plan but for an equilibrium: a plan that no future self wants to deviate from, given that all later selves follow it.
Huang and Zhou (arXiv:1809.09243v3, Math. Oper. Res. 2021) study this for finite-state Markov chains, mainly in continuous time. Section 5 of their paper turns to discrete time. On a finite horizon a discrete-time equilibrium is built by backward induction; on an infinite horizon there is no last period to start from, and, as the authors note, "little is known about the existence and characterization of equilibria, even in discrete time" (p. 15). Their Theorem 5.1 gives a general existence result for this case. This mission formalizes it.
Let and . A time-homogeneous Markov chain on is controlled by choosing its transition matrix ; the -th row is the distribution of given . Rows live in the probability simplex
For each state a set of admissible rows is given, and .
A payoff is continuous, and is the reward periods from now when the chain is at and uses row . The dependence on , the time difference from the present, is what makes the problem time-inconsistent. It is assumed that
The value of from state is , and is the same with the clock shifted by one.
For the concatenation uses for the step at time and for every later step. A matrix is an equilibrium (Definition 5.1) if
the self at time cannot gain by a one-step deviation, given that all later selves use .
If every is nonempty, convex and closed and every is concave on , then
The result. Theorem 5.1 says that infinite-horizon, discrete-time, finite-state time-inconsistent control always admits an equilibrium under convexity and concavity alone: no discounting structure, no stationarity of in , and no compactness beyond what provides. Remark 5.2 of the paper shows that concavity of cannot simply be dropped: with strictly convex time- payoffs, a two-state example has no equilibrium. The discrete-time model is also the bridge to the continuous-time theory: Theorem 5.2 of the same paper (a companion mission) shows that limits of equilibria of time-discretizations are weak equilibria in continuous time.
Formalizing it. The result is proved on paper in one page. The formalization produces a machine-checked existence theorem whose definitions make the probabilistic content explicit (the value is written through the marginals of the chain), together with a reusable decomposition (5.4) and continuity of the shifted value in the transition matrix. None of this is formalized elsewhere on the platform; Kakutani's theorem, the one external ingredient, is.
Backward induction, the standard construction of discrete-time equilibria, has no starting point on an infinite horizon, so existence cannot be obtained by a recursion. The value is an infinite sum of products of matrix powers with , and its regularity in the transition matrix is not automatic: each term is continuous, but passing limits through the sum, and exchanging it with the finite sum over states in (5.4), needs the uniform tail control of (5.2) combined with the stochasticity of every power . Without concavity of the statement fails (Remark 5.2, p. 16, gives a two-state counterexample), so any argument must use it. Finally, the referenced fixed-point theorem is stated on Euclidean space, while the controls are matrices.
Fin N (state of the paper is index ); rows are Fin N → ℝ; transition matrices are Matrix (Fin N) (Fin N) ℝ with the product topology.tsums. A tsum of a non-summable family is in Lean; here (5.2) and the stochasticity of make every sum absolutely convergent, and no summability hypothesis appears in any statement.tsums, a linear homeomorphism between Matrix (Fin N) (Fin N) ℝ and EuclideanSpace ℝ (Fin (N*N)) to apply the referenced Kakutani theorem. The first two are reusable for any finite-state Markov reward model. Proofs of the milestones in any order are welcome.An agent that interacts repeatedly with an unknown Markov decision process must trade exploration against exploitation. The dominant design principle for provably efficient reinforcement learning has been optimism in the face of uncertainty: UCRL2 (Jaksch, Ortner & Auer, 2010) and REGAL (Bartlett & Tewari, 2009) build confidence sets around the unknown model and act according to the most favourable model in them. Computing that optimistic policy can be expensive, and confidence sets built separately for every state–action pair can be loose.
Posterior sampling for reinforcement learning (PSRL), proposed by Strens (2000), replaces optimism by randomization: at the start of each episode it samples one MDP from the posterior distribution and follows the optimal policy of that sample. It is the reinforcement-learning analogue of Thompson sampling for bandits. Osband, Russo & Van Roy (2013) gave the first regret guarantee for PSRL, and with it the first regret guarantee for an RL algorithm not based on optimism. Their argument transfers the Bayesian-regret analysis of Thompson sampling by Russo & Van Roy (2014) from bandits to MDPs.
Timeline:
A finite-horizon MDP has states, actions and horizon . Choosing action in state yields a reward drawn from a distribution on , with mean , and moves the state to with probability . Every episode starts from a state drawn from the initial distribution . A policy maps a state and a step to an action, and its value is the expected total mean reward from step on,
A policy is optimal for if it maximizes for every and ; denotes a fixed choice of optimal policy for each .
The true MDP is random with prior . In episode , PSRL samples from the posterior given the history of all earlier states, actions and rewards, and follows for steps. With , the regret of episode and the cumulative regret are
In Lean, MDPs are indexed by a parameter in a measurable space (MDPFamily), the value is value F θ π j with 0-based steps, and the run is the structure PSRLRun.
There is an absolute constant such that, for all , every prior , every measurable optimal-policy selector, every PSRL run with and every ,
This is the paper's statement. It does not fix the constant, which the paper's appendix computes with errors.
Theorem 1 holds for every prior, with no assumption on the MDP class beyond finiteness and bounded rewards. It shows that a single posterior sample per episode, rather than an optimistic search over a confidence set, already achieves the rate of the optimistic algorithms. The reduction it rests on (Lemma 1 and Theorem 2) applies to any problem in which the agent can sample from the posterior.
The theorem has a paper proof but, as far as is known, no machine-checked proof. A formalization adds three things. First, an exact model of the episodic Bayesian setting, with posterior sampling stated as a conditional law. Second, corrected versions of two steps: the factor in (8), which the page's argument does not justify as printed, and the square-root sum of Appendix B, which is false as printed. Third, reusable pieces: a path-defined finite-horizon value with its dynamic programming equation, a conditional-expectation form of the posterior-sampling identity, and deterministic counting lemmas for visit counts.
The proof combines three kinds of argument, each with its own obstacle in Lean.
Model. States and actions are Fin S and Fin A. Steps and episodes are 0-based: Lean step j is the paper's step , and Lean episode k is the paper's episode , with . MDPs are a measurable family over a parameter space Θ: transition rows satisfy the published IsTransitionKernel, and reward laws are Markov kernels supported on . The initial distribution is fixed. The value is defined from the state laws along the trajectory, not by the Bellman recursion.
The run. PSRLRun consists of measurable random elements on a probability space. Posterior sampling, the reset from , rewards and transitions are stated as conditional expectations of indicators. Three assumptions the paper leaves implicit are made explicit:
The optimal-policy selector is any measurable map that is optimal at every step.
Constants and corrections. is one absolute constant, quantified before every other object; a constant that depends on , , , the prior or would make the goal trivial, because the regret is at most . Milestone 7 uses the factor , which the page's chain proves, where the page prints , and milestone 9 uses where the page prints the false bound ; both corrections are disclosed in the statements.
Ruled out. The value is not defined by the recursion, which would make Lemma 2 definitional. Measurability is required, so the expectations are not junk zeros. The posterior-sampling clause concerns indicators of only, so it does not already contain Lemma 1.
Needed infrastructure. Conditional expectations with respect to -algebras generated by random elements; finite-horizon Markov chain laws; Weissman's inequality and Hoeffding's inequality at random sample sizes; elementary bounds on . The counting milestones (8, 9) and Lemma 2 are self-contained and a good place to start. Proofs of the conditioning steps (milestones 1, 2, 4) are reusable for any posterior-sampling analysis.
Data-driven control asks for a controller computed directly from measured trajectories of an unknown system, without first identifying a model. When the measurements are corrupted by noise, many systems explain the same data, and a controller is acceptable only if it works for all of them. Van Waarde, Camlibel, Eising and Trentelman (arXiv:2203.12959) model the noise by a quadratic matrix inequality (QMI). The set of systems consistent with the data is then itself the solution set of a QMI, and the design question becomes whether one QMI implies another. Their Theorem 5.1 gives a necessary and sufficient linear matrix inequality (LMI) for the existence of a common stabilizing controller, with no rank or Slater-type assumption on the data. It improves van Waarde, Camlibel, Mesbahi, IEEE TAC 2022, Thm. 14, which needed a generalized Slater condition.
The LMI of Theorem 5.1 has size and unknowns. Section 5.2 of the paper removes the controller variable: Theorem 5.3 gives an LMI of size in the Lyapunov matrix and one scalar , and then writes a stabilizing controller as a closed-form expression in and the data. This mission formalizes that reduction and the Section 3 results on QMI solution sets that it rests on.
All matrices are real. is the set of symmetric matrices, () means symmetric positive semidefinite (definite), and is the Moore–Penrose pseudo-inverse. For , partitioned with of size and of size ,
and is the same set with . The generalized Schur complement is , and is the class of with , and . For , and .
Data. An unknown system produces and ; and are the first and last columns of . The noise matrix is unknown but satisfies for a given . The consistent systems are
The data are informative for quadratic stabilization if there are and with for all .
With and : the data are informative if and only if some , satisfy
and then
stabilizes every . Under and the same holds with strict inequalities, , and . The goal states all four parts.
Theorem 5.3 separates the computation of a Lyapunov matrix from the computation of the controller. The LMI drops from size to and loses the entries of . A controller then follows from by one explicit formula, with no second optimization. The noise class covers energy bounds, bounds on individual samples, noise confined to a known subspace, and exact data, so the result applies where earlier conditions requiring or a Slater point fail.
The Section 3 results are general facts about QMIs: an explicit parameterization of all solutions, also when the solution set is unbounded, and the identification of the image of a solution set under a linear map. They are reusable wherever QMIs appear in robust control: Petersen's lemma, the elimination lemma, dissipativity analysis.
All results are proved in the paper, with the exception of the proof of Theorem 3.5, which is only described as similar to that of Theorem 3.4. None is formalized. The work here is the formal development: a pseudo-inverse calculus for real matrices, generalized Schur complements, matrix square roots in the Loewner order, and the block-matrix identities of Section 5.
The QMI reformulation of the stabilization problem is short. The difficulty lies in degenerate matrices. is typically singular, so every step works with pseudo-inverses, kernel inclusions and generalized Schur complements, and identities that are routine for invertible blocks need range conditions. The closed-form gain (5.10) comes from a block pseudo-inverse formula for a positive semidefinite matrix whose blocks may all be singular, and checking it requires tracking which ranges contain which. The strict statements need a separate argument: a strict inequality does not pass to without full column rank of , which is why Theorem 3.5 and Corollary 3.7 assume it.
The first idea, to eliminate from (5.5) by completing the square, runs into the same singular blocks: the minimizing involves pseudo-inverses of data-dependent matrices whose ranges are not controlled by the LMI alone.
Lean conventions:
PosSemidef (which includes symmetry); is PosDef.A⁻¹, which returns on singular matrices, appears only in (5.11a) and in , where the matrices are invertible.CFC.sqrt in the Loewner order. Kernel inclusions are stated on vectors. Full column rank of is rank W = p.The statements of Theorems 5.1 and 5.3 carry the hypothesis that the data were generated by some , i.e. ; the paper assumes this when it says the data are generated by (2.1) with noise model (2.3). Without it, informativity holds vacuously and the equivalences fail. "Stabilizing gain" is asserted with the of the LMI: the Lyapunov inequality and for every . Corollaries 3.6 and 3.7 print the hypothesis , which is dimensionally impossible; it is read as . The printed dimensions in Lemma A.2 are corrected to those its formula requires.
A formalization in which Σ may be empty, or in which is replaced by the total inverse, would make the goal vacuous or false. Both are ruled out above.
Theorem 5.1 is restated here as a milestone. It is also the goal of the companion mission IV, and solvers may prove it there.
Reusable infrastructure is welcome as separate contributions: uniqueness and the basic identities of the matrix pseudo-inverse; the generalized Schur complement criterion for positive semidefiniteness of a block matrix; Douglas-type factorization (Lemma A.1); square roots of positive semidefinite matrices commuting with pseudo-inverses.
Finsler's lemma (P. Finsler, 1937) states that for symmetric matrices , the quadratic form is positive on every nonzero with if and only if for some real . Together with the S-lemma of Yakubovich it is one of the basic tools for converting a statement about all vectors satisfying a quadratic constraint into a single linear matrix inequality (LMI) in a multiplier, which can then be checked by semidefinite programming. Both results are used throughout robust control, where uncertainty is described by quadratic constraints.
In data-driven control the unknown object is a matrix, not a vector: the system matrices consistent with noisy measurements form a set of the form
and a controller has to work for every element of such a set. H. J. van Waarde, M. K. Camlibel, J. Eising and H. L. Trentelman (arXiv:2203.12959, SIAM J. Control Optim. 2023) develop matrix-valued versions of the S-lemma and of Finsler's lemma for exactly this purpose. Their matrix S-lemma (Theorem 4.7) requires a Slater-type condition: must have a positive eigenvalue. This mission concerns the complementary case in which has no positive eigenvalue, where the inequality defining degenerates into an equality and a Finsler-type statement is needed.
All matrices are real. For a symmetric matrix , () means positive semidefinite (definite); means . is the Moore–Penrose pseudo-inverse, the unique matrix with , and , symmetric.
Fix integers and . A symmetric matrix is partitioned as
with of size and of size , and likewise . For write , and define
The generalized Schur complement is , and the class consists of the symmetric with , and . For , the condition is equivalent to having no positive eigenvalue; then . Finally, set
First, if for some , then . Second, if , and , then
A companion item formalizes Example 4.9 (p. 13): for and all hypotheses except the one on hold, the inclusion holds, and no works.
The theorem turns an inclusion between two sets of matrices, a statement quantified over infinitely many , into feasibility of a scalar-multiplier LMI. In the paper it is one of four matrix S-lemma variants (Theorems 4.7, 4.8, 4.10, 4.11) that together cover the cases arising in data-based control: whether the data-consistent set has a Slater point, and whether the conclusion is non-strict or strict. Theorem 4.8 is the variant for noise models whose quadratic description has no interior, for instance exact equality constraints on the noise. Example 4.9 shows that the kernel hypothesis on is genuinely needed, so the statement marks the boundary of when the lossless reduction holds.
The paper gives a complete proof. No machine-checked proof of this theorem, of the matrix S-lemma, or of Finsler's lemma in matrix form is known to exist, in Lean or elsewhere. Formalizing it produces reusable infrastructure: the Moore–Penrose pseudo-inverse of real matrices with its Penrose identities, the generalized Schur complement criterion for positive semidefiniteness of a block matrix, and congruence manipulations of block matrices, none of which is currently in Mathlib in this form.
The "if" direction is a one-line computation. For the "only if" direction the classical vector Finsler lemma is not directly applicable: it concerns vectors with , while the hypothesis here only controls matrices with , which is a much smaller family when , and the conclusion is non-strict. The natural first idea, applying the vector S-lemma, fails because has no positive eigenvalue, so its Slater condition is violated. Instead one must exploit the structure of : the pseudo-inverse appears because and are typically singular, and every manipulation must track kernels and ranges exactly.
The blocks are indexed by arbitrary finite types ι (size ) and κ (size ); a matrix in is Matrix (ι ⊕ κ) (ι ⊕ κ) ℝ, its blocks are toBlocks₁₁ etc., and is Matrix κ ι ℝ. is Mathlib's PosSemidef, which includes symmetry. The pseudo-inverse is defined by Hilbert's choice among matrices satisfying the four Penrose conditions; since such a matrix exists and is unique, this is the pseudo-inverse and not a junk value. Kernel inclusions are stated with matrix–vector products.
One hypothesis is added and disclosed: (Nonempty ι) in the second statement of Theorem 4.8 and in the milestones that need it. The proof picks a nonzero vector of , and at the equivalence is false (, , ). The first statement keeps a real multiplier of any sign; the second requires , as printed. The hypothesis together with makes nonempty, so the inclusion is never vacuous; a formalization in which could be empty, or in which were replaced by the inverse (which is on singular blocks in Lean), would not be this theorem.
Needed infrastructure: existence and uniqueness of the Moore–Penrose pseudo-inverse (needed to work with the definition at all), symmetry of for symmetric , the generalized Schur complement criterion for , and positive semidefiniteness under congruence by an invertible matrix. These lemmas are reusable beyond this mission and contributions of them are welcome, as are proofs of the companion Example 4.9.
A linear set of the projective line is the set of points spanned by the nonzero vectors of an -subspace . The extremal ones, the maximum scattered linear sets, are given by scattered polynomials over , and each such also gives an -linear maximum rank-distance (MRD) code of minimum distance (Sheekey, Adv. Math. Commun. 10, 2016). Rank-distance codes are used in network coding, and linear sets appear in the study of semifields, blocking sets and two-intersection sets.
Linear sets and codes are classified up to equivalence: two linear sets are the same object if a collineation of the line, an element of , maps one onto the other. The question is therefore not only whether new scattered polynomials exist but how many inequivalent linear sets they produce.
Let be an odd prime, , , , , and let be the finite field of order . Its subfield is .
A -polynomial is a map with (qpoly). It is scattered (IsScatteredPoly) if for all , forces with .
The graph of is (graph). A point of is the set of all -multiples of a nonzero (point), and the linear set of is the point set
For a field automorphism and an invertible matrix over , the map ( acting on coordinates, act) is an element of ; with it is in . Two subsets are GL- or ΓL-equivalent (GLEquiv, GammaLEquiv) if such a map sends onto . Two point sets are PGL- or PΓL-equivalent (PGLEquiv, PGammaLEquiv) if the induced map on points, , sends one onto the other.
The family. For ,
(hSet), and . For and , is scattered and is a maximum scattered linear set (Theorem 3.1).
For , the number of -classes met by the sets , , satisfies
It is stated as: some of at least that size has pairwise -inequivalent . The goal fixes the paper's constants; the proof on p. 26 in fact counts classes exactly in terms of class sizes, so a sharper bound is a natural follow-up.
The result. Theorem 5.1 shows that maximum scattered linear sets of , and hence -linear MRD codes, exist in numbers exponential in up to equivalence, whereas each previously known infinite family yields at most times a function of classes (Table 1, p. 3). Remark 5.4 draws the consequence that the family is new. Its intermediate results, the classification of the - and -equivalences between the (Theorem 4.2) and the reduction of -equivalence to sets of quotients, are the standard tools for any later classification of this family.
Formalizing it. The theorem has a complete published proof; none of it is machine-checked. The platform has no action of or on the projective line, no linear sets of as point sets, and no coefficient identities for -polynomials defining the same linear set. The mission produces these, then the class counts. Lemma 2.2 is a result of an earlier paper (Csajbók–Marino–Polverino 2018) cited without proof, so formalizing it means formalizing part of that paper too.
Equality of two linear sets is equality of sets of points, which says nothing directly about the polynomials: different -polynomials can define the same linear set (all with do). The obvious idea, that -equivalent linear sets come from -equivalent subspaces , fails in general (p. 3), so the count cannot be read off Theorem 4.2. The step that needs the restriction is the comparison of coefficients in the -polynomial identities, which for is open (Remark 5.5). A second difficulty is bookkeeping: the exponents , , the negative powers of and the case split on must all be tracked through every identity.
CharP F p, p prime, Odd p (" odd"), q = p ^ r with 0 < r, and Fintype.card F = q ^ (2 * t). is the exponent of , as in Theorem 5.1, so . Lemma 2.2, (37) and the step are stated for general and Fintype.card F = q ^ n, without " odd", as printed.x ^ q ^ i; negative powers of are field quotients (h / h ^ q ^ (t+1) for ), exact since on . Natural-number subtractions , , , , are exact in the stated ranges.Fin 2 → F; points are sets of scalar multiples; linear sets are sets of points. Equivalences are stated as images of sets under with a unit and a ring automorphism.A risk measure assigns a number, typically a capital requirement, to a random financial loss. When a total loss is shared among agents, each judging its share by its own risk measure , the smallest achievable aggregate risk is the inf-convolution
It describes optimal risk sharing in insurance, reinsurance and among the desks of a financial institution, and it is the basic object of the risk-sharing literature (Delbaen 2012; Rüschendorf 2013).
Regulatory risk measures such as Value-at-Risk (VaR) and Expected Shortfall depend only on the upper tail of the loss distribution. Liu and Wang (2021) formalized this as tail risk measures. Embrechts, Liu and Wang (2018) showed that the inf-convolution of VaRs and Range-VaRs is again of the same type with summed levels, and Liu, Wang and Wei (2020) showed that inf-convolutions of law-invariant risk measures are law-invariant under weak conditions. Theorem 3 of Liu, Mao, Wang and Wei (2022) unifies these observations for arbitrary tail risk measures. This mission is drawn from the authors' SSRN version of January 16, 2022.
Fix an atomless probability space : every event of positive probability contains an event of strictly smaller positive probability. Positive values of a random variable are losses. Write . For the left and right VaR are
The domain is , the essentially bounded random variables.
For the tail of beyond its -quantile is the random variable with distribution function (display (6) of the paper). A functional is a -tail risk measure if whenever and have the same law. For this is law-invariance. The functional is monotone if a.s. implies , and (sup-norm) continuous from above if whenever a.s. and .
The allocations of are , and is the infimum above over . It takes values in .
Let be an -tail risk measure with , , and suppose one of is monotone and continuous from above. Then
The theorem says that tail-dependence survives optimal risk sharing, and it quantifies how much: the aggregate looks at a tail of probability at most the sum of the individual ones. The parameter is sharp, since and has smallest tail parameter . Consequently, results proved for tail risk measures (representations through law-invariant functionals of the tail, existence of optimal allocations) apply to the outcome of a risk-sharing market, not only to its participants. The hypotheses are weak: no convexity, no translation invariance, and only one agent needs monotonicity and a mild continuity.
The result is proved in the paper; its proof relies on two results it cites but does not state, Lemma 1 and Theorem 2 of Liu, Wang and Wei (2020), and on Corollary 1 of Embrechts, Liu and Wang (2018). None of the three, and no part of the theory of tail risk measures or inf-convolutions on probability spaces, is formalized on the platform or in Mathlib as far as a search found. A formalization therefore has to build the cited results as well; milestones 2, 3 and 5 isolate them in the form used.
Tail-invariance of each concerns one share at a time, while the inf-convolution is a constraint on the sum of the shares: modifying a share below its quantile breaks the budget . The obvious argument, applying the tail property of each to its share of and of , fails because an allocation of does not induce an allocation of when but . Even when an allocation of cannot in general be transported to an allocation of exactly. This is why the theorem needs an atomless space and a continuity hypothesis on one agent, and why the cited law-invariance result is the hardest part to formalize.
All objects live in the namespace TailRiskSharing.TailConv, in one definitions file. Conventions:
NoAtoms).EReal, so it can be , and monotonicity and the tail property are stated for that EReal-valued functional without assuming finiteness.The goal cannot be satisfied trivially: the tail parameter is and never a number above 1, the inf-convolution is not truncated to a real value, and none of the hypotheses is vacuous (constant functionals satisfy all of them). Contributions are welcome for each cited result as reusable lemmas: the quantile subadditivity of Embrechts et al., monotonicity of an inf-convolution, and law-invariance of inf-convolutions on atomless spaces.
A linear set of a projective space over a finite field is the set of points spanned by the nonzero vectors of a subspace over a subfield. They have been used to construct and characterize semifields, rank-metric codes, translation spreads, translation ovoids, two-intersection sets and the blocking sets for which Lunardon introduced them (Polverino 2010; Lavrauw–Van de Voorde 2015). On the projective line the extremal objects, the maximum scattered linear sets, are equivalent to scattered polynomials over , and each scattered polynomial gives an -linear maximum rank-distance (MRD) code of minimum distance (Sheekey 2016). Rank-distance codes are studied in network coding theory (p. 2).
Scattered polynomials are scarce. Before this paper, only three families were known for infinitely many :
Longobardi, Marino, Trombetti and Zhou construct a fourth family, defined for every even and odd . This mission formalizes that construction, Theorem 3.1 of the paper.
Let be an odd prime, , , and . Let be the finite field of order . For , write for its subfield of order , the set of with .
A -polynomial over is a map with . It is -linear. Its graph is an -dimensional -subspace of , and it defines the linear set of .
The polynomial is scattered when, for all ,
Equivalently, has the maximum size .
Fix with . The paper's polynomial is
The proof splits it as with
and it also uses the -linear maps and . The Lean development uses the same letters: psi, Lmap, Mmap, Rmap, Tmap, IsScatteredPoly, qpoly, graph.
For odd, , , and every with ,
The result. Theorem 3.1 produces, for every odd and even , maximum scattered linear sets of and MRD codes of with minimum distance . For the polynomials are those of Bartoli, Zanella and Zullo. If were allowed in , then and would reduce to the Longobardi–Zanella polynomials (p. 6). The second half of the paper (Theorem 5.1, a companion mission) shows that for the family contains a number of -inequivalent members that grows exponentially in . Every previously known family contributes fewer than classes.
Formalizing it. The theorem has a complete published proof. No scattered polynomial, linear set of the projective line or linearized-polynomial kernel computation is formalized on the platform, and none appears in Mathlib. The work is to formalize the paper's proof: the semilinear-algebra lemmas of §3 and the case analysis that follows them. The milestones are reusable statements about -polynomials of seen as an -plane.
Writing out coefficient by coefficient gives a system in and with exponents that does not separate directly. The paper's route goes through two -direct-sum decompositions of and two changes of -basis. Each identity involves negative powers of and holds only through and the parity of . The hypothesis enters only at the end, and a formalization must carry the arithmetic of the exponent towers modulo throughout. The tempting shortcut, checking the statement on a few small fields, proves nothing: the theorem is uniform in and .
CharP F p, p prime, Odd p, with (an explicit q with hq : q = p ^ r), and Fintype.card F = q ^ (2 * t). So is up to isomorphism, and no particular model is chosen.ScatCaps.LinearSets.subfieldOf F p r m.ScatCaps.LinearSets.IsScattered, which is equivalent to the cardinality definition of p. 1.h / h ^ q ^ (t+1). This is exact because forces . Natural-number subtractions in exponents (, , ) are exact in the stated ranges.IsFqSubspace, HasRank). A direct sum is stated as unique decomposition, and an -basis as unique representation with .Value-at-Risk (VaR) is the quantile-based capital requirement written into banking and insurance regulation (Basel, Solvency II). When several institutions, desks or subsidiaries each hold capital according to their own VaR, a natural question is how a total loss should be split among them so that the aggregate capital is as small as possible. This is the risk sharing problem, and its value is the inf-convolution of the agents' risk measures.
For VaR the problem is non-convex, so the convex-analytic toolbox of risk sharing does not apply. Embrechts, Liu and Wang (2018) solved it when every agent uses the left quantile: the inf-convolution of left VaRs at levels is the left VaR at level . The case of right quantiles, and of agents mixing the two versions, remained open. Liu, Mao, Wang and Wei close it in Theorem 1 of Inf-convolution, Optimal Allocations, and Model Uncertainty for Tail Risk Measures (Mathematics of Operations Research, 2022). This mission formalizes that theorem from the authors' SSRN version of 16 January 2022 (SSRN 3490348); all page and display numbers refer to that version.
Fix an atomless probability space : every event of positive probability contains an event of strictly smaller positive probability. A random variable is a measurable ; the set of all of them is , and a positive value of is a loss. Write . For a level ,
are the left and right VaR. They coincide unless is flat at height , in which case . For write .
Given agents with risk measures , the allocations of are (display (4)), and the inf-convolution is
An allocation attaining the infimum is optimal. A partition of is a family of measurable, pairwise disjoint events covering .
Let with and ; put if all and otherwise. Then
is optimal; 3. for every partition independent of with , the allocation (9) is optimal.
The result. Theorem 1 gives a closed form for quantile-based risk sharing among any number of agents with any mix of left and right quantiles. The answer is asymmetric: one right-quantile agent turns the whole convolution into a right quantile. Part 2 shows that the minimum is attained, and the optimal allocation has a simple shape: every agent holds an equal share of the capital, and the excess loss over the aggregate quantile goes to one agent at a time, chosen by the partition. Part 3 gives that partition explicitly when an independent randomization is available. The formulas are the base case for the paper's later results on tail risk measures (Theorems 2–4), where a VaR agent shares risk with an agent using a general tail risk measure.
Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of (7), is known. The mission produces a checked theory of left and right quantiles on a general probability space, of inf-convolution with values in , and of the explicit optimal allocation. The milestone (7) is itself a published theorem of another paper, cited and not reproved here, so formalizing it is part of the work.
The known left-quantile result does not transfer to right quantiles. A right VaR is characterized by a family of strict tail bounds, for every (display (10)), while a left VaR needs one non-strict bound (display (11)). The events have probability strictly below but may approach as , so the split of the left-quantile case, chosen once for a fixed event, does not keep each agent's share strictly below its level. This is why the right and mixed cases were open, and why the existence part (ii) depends on the atomlessness of the space. Passing from two agents to agents requires associativity of when intermediate values may be .
All objects are defined in one file, TailRiskSharing.VaRConv.Setting:
MeasureTheory.Measure with IsProbabilityMeasure and the classical atomless property, which is the paper's standing assumption (§2.1, p. 5). It is kept on every inf-convolution statement and on the goal, including part 3, where the paper notes (Remark 3) that it is not needed.EReal, never a real sInf. Statements of the form assert equality with a coerced real number.ProbabilityTheory.Indep between the σ-algebra generated by the partition and the σ-algebra generated by .A trivializing formalization is excluded: the inf-convolution cannot collapse to a junk value of a real infimum, the levels cannot degenerate to , and the agent count cannot be .
A complete development needs the basic quantile calculus (monotonicity and left-continuity of , translation and scaling rules), a splitting lemma for atomless spaces, and the associativity of inf-convolution. These are reusable for the rest of this paper's series and for any quantile-based risk sharing result. Proofs of milestones and of the general lemmas are welcome as separate contributions.
Nesterov's accelerated gradient method for smooth convex objectives, here called NAG-C, reaches function-value accuracy after gradient evaluations, which is optimal among first-order methods (Nesterov 1983; Nesterov 2004). In many uses the quantity of interest is not the function gap but the squared gradient norm : it is computable without knowing the optimal value, it serves as a stopping criterion, and it controls duality gaps when the objective is a dual function. Combining the function-value rate with -smoothness gives only .
Shi, Du, Jordan and Su (arXiv:1810.08907) derived high-resolution ODEs for accelerated methods, keeping terms of order that the earlier low-resolution limit of Su, Boyd and Candès (2016) discards. One of the discrete consequences is Theorem 6: unmodified NAG-C minimizes the squared gradient norm at the inverse cubic rate .
Timeline. Nesterov (1983) introduced the method and its rate. Nesterov (2012) established an lower bound for the squared gradient norm and matched it up to a logarithmic factor with a regularized scheme built on the strongly convex variant of the method, which takes as input. Ghadimi and Lan (2016) reached with a modified accelerated method that adds a sequence of iterates and a larger step size. Attouch and Peypouquet (2016) proved function values for a variant with momentum , . Shi, Du, Jordan and Su (arXiv 2018; Math. Program. 2021) proved the rate for NAG-C itself, through a Lyapunov function suggested by the high-resolution ODE.
Let carry the Euclidean inner product and norm . For , the class consists of the differentiable with
A point is a minimizer of when for every .
Given a step size and an initial point , NAG-C generates and, for ,
The velocity is , and the discrete Lyapunov function of the paper is
The last summand inside the norm, , is the gradient correction that the high-resolution ODE contributes and that the low-resolution analysis lacks.
For , a minimizer , and every ,
The goal is the paper's theorem with its printed constants and both of its claims.
In the paper's order of proof:
The result. With , Theorem 6 gives for the textbook method, with no restart, regularization or extra sequence. The rate is dimension-free and holds from the first iteration. It is a factor better than what the function-value rate gives, and it separates the high-resolution description of NAG-C from the low-resolution one: the paper explains the bound by the gradient correction in .
Formalizing it. The theorem is proved in the paper and, as far as the platform's catalogue shows, has no machine-checked proof. The mission produces a checked statement of NAG-C, its phase-space form and its Lyapunov function, which the other accelerated-method missions of this series (NAG-SC, the high-resolution ODEs) can mirror. Part of the paper's argument is a brute-force computation in Appendix C.1. A checked version would confirm the printed constants and ; tighter constants or cleaner small- arguments are welcome as separate theorems.
The obvious route goes through the function-value rate and the smoothness inequality . It stalls at for the gradient, and no rearrangement of the classical estimate-sequence argument yields more. The extra factor of comes from a Lyapunov function whose one-step decrease is weighted by , and that decrease must be extracted exactly. The bookkeeping involves the -dependent momentum , the identity coupling , and two gradients, and the cocoercivity of . The sign of the decrease is lost for , so the first iterates need a separate argument with explicit constants.
is EuclideanSpace ℝ (Fin n) and is Mathlib's gradient. The class is a structure in the paper's first-order form (, differentiability, the convexity inequality, the Lipschitz gradient) and the velocity is defined once, both in the shared definitions HighResODE.NAGSC.FunctionClass and HighResODE.NAGSC.Setting; this mission's definition file, HighResODE.NAGC.Setting, holds NAG-C as a predicate on two sequences indexed from and . Conventions:
Finset.inf'), never a real infimum that could collapse to .Milestones (4.5), (4.13) and (4.14) assume only and the NAG-C recursion, which is stronger than the page. The remaining items carry the hypotheses of Theorem 6 or, for pure arithmetic, none beyond . Needed infrastructure: elementary inner-product algebra, the cocoercivity inequality for , which is reusable for any smooth convex method, and finite telescoping sums.
Nesterov's accelerated gradient method is the standard example of a first-order method that is provably faster than gradient descent. On a -strongly convex function with -Lipschitz gradient, gradient descent reduces the objective gap by a factor per step, while the accelerated method achieves , the best possible rate for first-order methods (Nesterov, 2004/2013). The classical proof uses the estimate sequence technique, which certifies the rate but does not explain where the acceleration comes from.
Shi, Du, Jordan and Su (arXiv:1810.08907, published in Mathematical Programming, 2021) propose an explanation through high-resolution ordinary differential equations: continuous-time limits of the algorithms that keep terms of order in the step size . The heavy-ball method and Nesterov's method have the same low-resolution limit but different high-resolution limits; the extra term, a gradient correction , is what separates the two. From the high-resolution ODE of Nesterov's method the authors derive a discrete Lyapunov function and use it to give, in their words, the first Lyapunov-function-based proof of the accelerated linear rate of Nesterov's method for strongly convex functions. This mission formalizes that discrete result, Theorem 3 of the paper.
Timeline:
Let be the Euclidean norm on and the inner product. For , the class consists of differentiable functions with for all (convexity) and (an -Lipschitz gradient). For , the class consists of those with
Such an has a unique minimizer .
NAG-SC with step size starts from any and iterates
The velocity is , and the discrete Lyapunov function of the paper is
In Lean these are IsF1, IsS1, IsNAGSC, vel and lyap in the namespace HighResODE.NAGSC.
For and step size , the iterates of NAG-SC satisfy, for every ,
The statement mentions only , , the iterates and the constants; the Lyapunov function does not appear in it.
A further item, not a milestone, states that the resulting constant (p. 17) is less than five.
Theorem 3 recovers the optimal accelerated rate of NAG-SC, , with fully explicit constants: step size , rate and prefactor . The proof is a single Lyapunov inequality (Lemma 3.4) rather than an estimate sequence, and the same Lyapunov function, read in continuous time, explains acceleration through the gradient correction term. The heavy-ball method, which lacks this term, admits only a non-accelerated global rate under the same analysis.
The theorem is proved in the paper; nothing here is open. To our knowledge neither Theorem 3 nor its Lyapunov function has a machine-checked proof. The platform carries a formalization target for a different statement about Nesterov's method in the strongly convex case (Bubeck's Theorem 3.18, step , rate , constant ), which is not this theorem. A completed mission yields a checked discrete Lyapunov proof of acceleration, with every inequality of the paper's proof as a separate reusable statement.
The obvious approach, unrolling the two-step recursion and bounding it as a linear system, works only for quadratics and loses the constants. The Lyapunov route avoids this, but its core step, the first-difference bound (B.2), is a long computation in the appendix (pp. 51–56): the cross terms coming from the momentum and from the gradient difference must cancel exactly, and the small negative term of exists only to make them cancel. Lemma 3.4 then needs the comparison of four coefficient pairs between (3.15) and (3.16), which holds only because forces . Finally, the inequality is an elementary but unpleasant one-variable estimate.
EuclideanSpace ℝ (Fin n), with arbitrary; is Mathlib's gradient f.∀ z, f xs ≤ f z; the stationarity is not assumed separately.Real.sqrt, with and written as on the page.A formalization that let the NAG-SC predicate constrain only the -update, dropped the Lipschitz-gradient bound from the class, or left the step size as a free parameter unrelated to would make the goal false or vacuous; the statements here do none of these.
A complete development needs the standard smoothness facts for (the descent lemma, , co-coercivity), which are reusable well beyond this mission, followed by the algebra of (B.2). Contributions of proofs of individual milestones, in any order, are welcome.
Many nonconvex optimization problems in binary variables have a polynomial objective or polynomial constraints. The standard way to bring them into the reach of linear and mixed-integer programming solvers is to introduce one new variable per monomial and to study the convex hull of the resulting set of feasible 0/1 vectors, the multilinear polytope. Strong linear descriptions of this polytope translate directly into tighter relaxations in global solvers such as BARON, which is where the inequalities of this mission were tested (Del Pia and Khajavirad 2021, §2.5).
The multilinear polytope of a general hypergraph has no compact description, so the question is for which hypergraphs a given family of inequalities is enough. The quadratic case is classical: the Boolean quadric polytope of a graph (Padberg 1989) is described by its standard linearization exactly when the graph is a forest, and the odd-cycle inequalities are the first facets that appear on a cycle. For higher-degree monomials, Del Pia and Khajavirad showed in 2018 that their flower relaxation is exact if and only if the hypergraph is γ-acyclic. The 2021 paper introduces the stronger running intersection relaxation and asks the same question for it. This mission formalizes the necessary condition the paper proves: the relaxation cannot be exact unless the hypergraph is β-acyclic.
A hypergraph is a finite node set with a set of subsets of of size at least two (no loops, no parallel edges). Its multilinear set is
and the multilinear polytope is . The standard linearization is
An ordering of a multiset of sets is a running intersection ordering if each , , meets the union of its predecessors inside a single predecessor ; it induces and . A running intersection inequality has a center , neighbors () meeting such that admits a running intersection ordering, and nodes when these sets are nonempty:
with the number of connected components of . The running intersection relaxation is together with all these inequalities.
A β-cycle of length is a sequence of distinct nodes and distinct edges in which each lies in and and in no other ; is β-acyclic if it has none. For the subhypergraph has node set and edges .
The milestones follow the paper's proof, in order:
The result is one half of the paper's picture of when the running intersection relaxation is exact. Proposition 5 shows β-acyclicity is necessary; Theorem 3 of the paper shows that kite-free β-acyclicity is sufficient; Example 2 shows β-acyclicity alone is not. Combined with the 2018 characterization of the flower relaxation by γ-acyclicity, it places the running intersection relaxation strictly between two acyclicity notions and tells a solver designer that on hypergraphs with β-cycles some other family of cuts (for instance odd-cycle-type inequalities lifted from Padberg's) is unavoidable.
The intermediate results are reusable on their own. Lemma 5 is a general statement that multilinear polytopes of induced subhypergraphs are projections of faces, and Lemma 3 with the shortest-cycle structure step is pure hypergraph combinatorics.
The result is proved in the paper. No part of it, nor the multilinear polytope, nor the Boolean quadric polytope, is formalized in Lean or Mathlib as far as a search of the platform showed. Lemma 6 is stated in the paper without proof, and the two strictness cases are justified there by "it can be checked" and by a citation of Padberg; a formal proof closes these gaps.
The obvious argument exhibits a point of directly from a β-cycle of . This fails because a β-cycle of is surrounded by arbitrary other edges, which contribute running intersection inequalities that can cut off any candidate point. The paper's route is to pass to the subhypergraph induced by the cycle's nodes, and that step requires two facts with real content: the projection lemmas (Lemma 6 is an inclusion between relaxations defined by different families of inequalities), and the structure of , which holds only for a shortest β-cycle. A long β-cycle can have chords in .
Strictness on the two small families requires a point, or an inequality, separating from . That means controlling every running intersection inequality of the cycle, over all centers, neighbor sets, orderings and choices of , and also checking that the separating inequality is valid for .
Lean conventions:
α with decidable equality. Hypergraphs carry their node set and their edge set as Finsets, with every edge of size at least two.α ⊕ Finset α → ℝ, and every polytope of is pinned to zero off 's own coordinates, so polytopes of different hypergraphs, and the projection , live in one space.⊂ ( and ).There is one disclosed addition. Lemma 6 and the reduction step assume that has no isolated node. Without it both statements are false: since (8) has no lower bound on , a node isolated in is unbounded below in . The paper uses them only for , where the hypothesis holds. The goal itself carries no added hypothesis.
A trivializing formalization is ruled out. A relaxation missing some running intersection inequalities (a fixed ordering, a fixed , a fixed neighbor set) would make strictness easier, and an empty or mis-pinned relaxation would make the inclusion false. The definitions here take the full family.
A complete development needs:
The β-cycle and subhypergraph material and Lemma 5 are reusable beyond this mission. Contributions are welcome on any milestone, on alternative proofs of the two strictness cases (for instance by an explicit fractional point), and on a proof of Lemma 6.
Binary polynomial optimization asks to minimize a polynomial over . The standard way to attack it with linear programming is to introduce one variable for every monomial and to work with the convex hull of the resulting set of binary points. This convex hull, the multilinear polytope, is the object behind the cutting planes that global solvers such as BARON add at every node of a branch-and-bound tree, and in general its facets are as hard to describe as the original problem is to solve. The useful theory is therefore structural: which hypergraphs of monomials give multilinear polytopes with an explicit, combinatorial description.
A line of work by Del Pia and Khajavirad answers this for increasingly general classes of acyclic hypergraphs: Berge-acyclic and γ-acyclic hypergraphs via flower inequalities (SIAM J. Optim. 2018), sufficient conditions for decomposing multilinear sets (Math. Program. 2018), and, in the paper this mission formalizes (Math. Oper. Res. 2021), the running intersection inequalities, a generalization of flower inequalities that does not need γ-acyclicity. The paper reports that adding these cuts reduces BARON's root-node relaxation gap by more than 95% on most of 35 computer-vision instances.
A hypergraph has a finite node set and a set of subsets of , each with at least two nodes. Points live in , one coordinate per node and per edge. The multilinear set and multilinear polytope are
The standard linearization replaces each equation by its convex hull over the unit cube: , , and for .
An ordering of a family of sets is a running intersection ordering if each meets the union of its predecessors inside a single predecessor ; write and . Given a center edge and neighbor edges , , meeting such that the sets admit a running intersection ordering, and nodes wherever this set is nonempty, the running intersection inequality is
with the number of connected components of the hypergraph on with edges . The running intersection relaxation is together with all these inequalities.
A β-cycle is a cyclic sequence of distinct nodes and distinct edges in which lies in and and in no other edge of the cycle; is β-acyclic if it has none. A kite is three edges with , and ; is kite-free if it has none. is two-laminar if any two distinct edges sharing at least two nodes are strictly nested.
For every kite-free β-acyclic hypergraph without isolated nodes,
In attack order: validity of the inequalities (Proposition 1); heredity of β-acyclicity (Lemma 3); kite-free implies edge-induced subhypergraphs are two-laminar (Lemma 7); β-acyclicity as the running intersection property of every edge subset (Lemma 4); the explicit facet description of for two-laminar β-acyclic by system (20) (Proposition 6) and its consequence there (Corollary 3); the decomposition theorem for multilinear sets (Theorem 1); and five steps of the inductive proof of Theorem 3 in §5.3: is kite-free β-acyclic with one maximal edge fewer, the inductive step , Claim 14 on partial hypergraphs, the projection , and the Fourier–Motzkin step .
Theorem 2 (p. 1022), the polynomial-size extended formulation over the maximal edges, and the form (19) taken by running intersection inequalities in kite-free β-acyclic hypergraphs.
Theorem 3 gives a description of the multilinear polytope in the original space, by inequalities defined combinatorially from the hypergraph, for a class that strictly contains the γ-acyclic hypergraphs covered by flower inequalities. With Theorem 2 it implies that linear optimization and separation over are polynomial for kite-free β-acyclic hypergraphs, and that separation can be done without the ellipsoid method. The paper also shows (Proposition 5, a separate mission of this series) that β-acyclicity is necessary for , so the characterization sits close to the boundary of what such relaxations can achieve.
All results of this mission are proved in the paper; none is machine-checked. A complete development would be the first formal treatment of hypergraph acyclicity degrees and of multilinear polytopes, and would include a formal Fourier–Motzkin elimination argument on a structured polytope.
The inclusion is a validity check. The reverse inclusion is the content. A direct argument through integrality fails: for two-laminar β-acyclic hypergraphs, facets have general integer coefficients, so total unimodularity and balancedness arguments used for laminar hypergraphs do not apply. The decomposition step is also harder than in earlier work: the shared part of the two pieces may be an edge whose nodes are only partly covered by edges of one side, so a point cannot be written by pairing one vertex of each side. Finally, the induction lifts to , which has an extra variable, and the projection back must be shown to produce only running intersection inequalities, which requires recognizing every Fourier–Motzkin combination as one.
Nodes form a type α with Fintype and DecidableEq; a point is a function z : α ⊕ Finset α → ℝ, and every polytope of a hypergraph vanishes off that hypergraph's coordinates, so that polytopes of different hypergraphs, lifts and projections are literal sets in one space. Hypergraphs have no loops or parallel edges, as the paper assumes. Orderings are lists, 0-based. The relaxation quantifies over every center, every neighbor set, every running intersection ordering and every choice of the nodes ; the number of components counts isolated nodes and ignores loops. The standard linearization has no row , exactly as printed.
One hypothesis is added to the paper: no isolated nodes, on Theorem 3, Corollary 3, Theorem 2 and the inductive step. It is necessary: for , the point with and all other coordinates lies in but not in . No other result carries it.
A trivializing formalization is ruled out by construction: restricting the relaxation to one fixed ordering or choice of would make the goal false rather than easy, and the goal is an equality of sets, not an inclusion.
A complete development needs: convex hulls of finite sets of 0/1 points, hypergraph connectivity, β-acyclicity and the running intersection property (Lemma 4 is a classical database-theory theorem of Beeri, Fagin, Maier and Yannakakis), and Fourier–Motzkin elimination. The hypergraph acyclicity layer is reusable beyond this mission, including by the two other missions of this series. Proofs of any milestone, and of reusable lemmas on hypergraph acyclicity, are welcome.
The Kolmogorov–Čentsov continuity criterion is the standard way to prove that a random field has a continuous version: a moment bound on increments, , yields a modification whose paths are Hölder continuous of every order (Karatzas–Shreve 1991, §2.2; Revuz–Yor 1999, Ch. I). It is used for Brownian motion, Brownian sheets, solutions of stochastic PDEs, Gaussian free field approximations and many other random fields.
The classical statement says only that the Hölder constant is finite almost surely. Many applications need more: a bound on the tail whose constant depends only on the parameters and not on the particular field, so that the bound holds uniformly over a family of fields.
This mission formalizes such a quantitative version, Proposition 2.3 in §2.3 of J. Miller and S. Sheffield, Liouville quantum gravity and the Brownian map II: geodesics and continuity of the embedding (Ann. Probab. 2021). The authors state it, note that it follows "by carefully following the proof" of the classical criterion, and write the proof out (pp. 30–31). They apply it to the circle-average process of the Gaussian free field (Proposition 2.4, p. 33) and again in Lemma 5.12 (p. 63).
The paper's main theorems (the -Liouville quantum gravity sphere equipped with the QLE(8/3, 0) metric has the law of the Brownian map; continuity of the embedding) are not part of this mission. Their objects, among them the Gaussian free field, SLE, quantum surfaces, the QLE metric of Miller–Sheffield 2020 and the Brownian map, have no formal substrate in Mathlib or on the platform. Proposition 2.3 is a self-contained probabilistic tool that the paper proves in full, and it is statable today.
Fix a dimension . The index set is the cube with the Euclidean distance . A random field is a family of real random variables on a probability space . The field satisfies the Kolmogorov condition with constants if
A modification of is a field on the same space with for every . For , the -Hölder norm of a function on the cube is
The proof works on the dyadic grid , the points of the cube whose coordinates are integer multiples of , and on the set of adjacent pairs , which differ in exactly one coordinate, by . In Lean the cube is Cube d, and the grid and the pairs are dyadicGrid d k and IsAdjacentPair d k u v.
For every there is a constant , depending only on , such that every field satisfying (2.6) has one modification with, for every ,
The tail bound (2.8) is what makes the criterion usable for families of fields. In the paper, it bounds the modulus of continuity of the Gaussian free field circle averages at every scale with a single constant, which feeds the estimates on the Liouville quantum gravity metric. More generally, polynomial tails for Hölder norms with field-independent constants are the input to tightness arguments for sequences of random fields, to union bounds over many scales or many fields, and to moment bounds for Hölder norms.
The result itself is known: the authors derive it from the textbook proof, which they write out. What is missing is a machine-checked version. At the pinned Mathlib revision, ProbabilityTheory.IsKolmogorovProcess defines the hypothesis (2.6), but no continuity theorem is proved from it, qualitative or quantitative. The platform has an Open goal for the qualitative one-parameter theorem on , KolmogorovChentsov.exists_modification_holderOnWith_Icc, a different statement that the mission does not duplicate. A proof of this mission's goal would give the classical -parameter criterion on the cube (milestone 6) and its quantitative form together.
The probabilistic steps (2.9)–(2.12) are Markov's inequality and two union bounds. They become concrete once the adjacent pairs are counted: is of order , and summing over scales needs . Formalizing them requires care with suprema in and with outer measures of events that are not obviously measurable.
The central difficulty is the deterministic chaining claim and the passage from dyadic points to the whole cube. The paper calls the claim "not difficult to see", but its constant must be uniform over pairs of dyadic points of arbitrarily fine and unequal levels, and the obvious attempt, comparing values along the straight segment between two points, fails because the points of the segment are not dyadic, so the hypothesis says nothing about them. The second difficulty is the modification itself: one field must serve every at once, must agree with almost surely at every point, and the tail bound for the dyadic supremum must transfer to the Hölder norm over the whole cube, an uncountable supremum whose event is not obviously measurable.
Cube d, the subtype of EuclideanSpace ℝ (Fin d) with coordinates in , so is Euclidean. Because all constants are existential, the statements do not depend on the norm, but Euclidean is the default reading.IsKolmogorovProcess X P α (d + β) c₀ with c₀ : ℝ≥0, plus 0 < α, 0 < β, 0 < c₀. It reads (2.6) with the lower Lebesgue integral in , so it cannot hold through a junk value of a non-integrable expectation. It also requires each pair to be Borel measurable, which is the measurability included in "random field". The probability space is [IsProbabilityMeasure P].eHolderNorm γ, valued in . A real supremum, which is 0 on unbounded families and would make (2.8) trivially true, is ruled out. The supremum of (2.12) is likewise an ℝ≥0∞-valued ⨆, and its event is , not the weaker "some term is ".Type (universe 0).A complete development needs counting lemmas for the dyadic grid, a chaining lemma on dyadic points, and the extension of a uniformly Hölder function from a dense subset (Mathlib's HolderOnWith and uniform-continuity extension tools apply). The chaining lemma and the quantitative criterion are reusable for any Hölder-regularity argument on cubes. Contributions are welcome for each milestone independently and for an alternative proof of the goal through Mathlib's PairReduction chaining machinery.
Mathlib/Probability/Process/Kolmogorov.lean (the predicate IsKolmogorovProcess). https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Probability/Process/Kolmogorov.leanThe expected error of the randomized SVD with a Gaussian test matrix is times the optimal error (Halko–Martinsson–Tropp 2011, Theorem 10.5). The factor is for a standard Gaussian matrix : the quality of every Gaussian sketching method is governed by inverse moments of a Gaussian matrix — moments of its pseudoinverse, equivalently of the inverse of the Wishart matrix . The expected spectral error uses instead (Tropp–Webber 2023, Lemmas B.2–B.3), and deviation bounds use tail estimates for both norms (HMT Proposition 10.4). None of these inverse moments is available in Mathlib. This mission proves them.
A standard Gaussian matrix has independent entries; its law is . Throughout, is wide or square, , so that is almost surely invertible; is a Wishart matrix with degrees of freedom and is inverse-Wishart.
The pseudoinverse of a full-row-rank matrix is . Its norms are determined by the inverse Wishart matrix:
where is the Frobenius norm, the spectral norm (largest singular value) and the smallest of the singular values of . The letter denotes Euler's number.
For integer and ,
The case is , the spectral inverse moment at the heart of expected spectral-norm error bounds. It is the goal because it is the one inverse moment that is not an exact formula: its proof passes through Edelman's bound on the density of and an explicit integration, and it implies the expectation bound of HMT Proposition 10.2 by Jensen's inequality.
The results. Combined with the second-moment identity and block independence of Mission I, the Frobenius inverse moment gives the expected Frobenius error of the randomized SVD and of generalized Nyström; the spectral inverse moment gives the expected spectral error and the core-noise bounds of truncated sketching methods; the two tail bounds give the large-deviation statements of HMT §10.3. The second-order inverse-Wishart moments quantify the variance of , which Tropp–Webber use for concentration of the randomized SVD error.
Formalizing them. The inverse-Wishart mean and the second-order moments are classical multivariate-statistics formulas (Muirhead; von Rosen) with no Mathlib counterpart. The Chen–Dongarra tail requires the exact distribution of , or at least Edelman's density bound; the Frobenius tail is HMT's own argument through the bidiagonal (Householder) model of a Gaussian matrix and chi-square moment estimates. Every statement here is a proved theorem in the literature; none has a machine-checked proof.
There is no Wishart distribution in Mathlib. The direct approach — compute the density of and integrate — needs the Wishart density, a change of variables on the cone of positive-definite matrices, and the matrix-variate gamma function. The classical route to the mean avoids this: by rotational invariance has the same law as for every orthogonal , so its mean is a multiple of the identity, and the trace is -type quantities whose means are elementary; making "the diagonal entries of are reciprocals of variables" rigorous requires the Gram–Schmidt (QR) decomposition of a Gaussian matrix and the independence of its factors. The spectral inverse moment needs a lower-tail bound for of the exact order ; a union bound over rows loses a factor and does not give the stated constant. The naive attempt to bound by loses a factor as well.
is sampled from the product measure on arrays; is Mathlib's total matrix inverse, equal to on the null set where is singular, and is defined as (pinvR). Every inequality is stated together with integrability of its integrand, so the Lean convention that a non-integrable function integrates to cannot make a bound vacuous; identities with nonzero right-hand sides force integrability on their own but are also stated with it. The inverse-Wishart mean is stated entrywise. Tail bounds are inequalities between a measure in and of the real bound. Real powers with non-integer exponents are Mathlib's rpow; all bases are positive under the hypotheses. The spectral norm is Mathlib's operator norm. The sizes follow Tropp–Webber (); HMT's and conventions are translated in each item's source field.
Welcome contributions: a Wishart/inverse-Wishart library (QR decomposition of a Gaussian matrix, Bartlett decomposition, chi-square moments ), and the distribution of of a Gaussian matrix (Edelman).
Shared definitions: the items of this mission import Definitions.Def_GaussianMatrix_basic, a draft of Mission I; submit that proposal first so the import resolves at compile time.
Series: I. Rotation Invariance and Moment Identities · II. Inverse Moments of the Pseudoinverse · III. Extreme Singular Values and Concentration. All three missions share the definition bundle GaussianMatrix_basic, published with Mission I, and the namespace GaussianMatrix.
Online matching models a platform that must commit resources to requests as they arrive, without knowing the future. In revenue management the resources are items in limited supply and the requests are customers, and the firm also chooses the price. Ma and Simchi-Levi (arXiv:1905.04770, Oper. Res. 2020, DOI 10.1287/opre.2019.1957) give algorithms whose worst-case guarantee depends on the set of prices each item can be sold at, and show that the guarantee is tight.
Timeline of the deterministic (matching) case:
A firm sells items, one unit of each. Item has a price set with , and . Customers arrive one at a time. In the deterministic case, customer either would or would not buy item at price : . Let be the largest with , or if there is none. Assigning item to customer earns . An online algorithm sees only when customer arrives.
The benchmark is the LP (5): maximize subject to , and , with optimal value . Its dual (19) minimizes subject to and . An algorithm is -competitive if for every arrival sequence.
Booking limits. By Proposition 1 there are unique positive that sum to and satisfy
Set and . For let be the segment containing . The value function is
It increases continuously from to and equals at .
Multi-price Ranking (Algorithm 2). Each item draws an independent seed . Customer is assigned an available item maximizing , provided the maximum is strictly positive. Ties are broken arbitrarily. The analysis uses dual variables: when is assigned to , and ; all other dual variables are .
For every setup in the deterministic case with , every arrival sequence, every tie-breaking rule and every feasible of (5),
The theorem shows that one randomized rule achieves the optimal guarantee for every price set, and that the guarantee depends only on the price ratios. For one price, and the classical vertex-weighted result is recovered. With several prices the benchmark (5) is stronger, because the offline optimum may also choose prices, and the guarantee degrades gracefully: lies in and depends only on how far apart the prices are. Theorem 3 of the same paper shows that no online algorithm does better than when every item has price set , so the ratio is tight.
The results are proved in the paper, in §4 and App. C. As far as the platform's records show, they have not been formalized. A formalization adds three things on top of the paper. It machine-checks a randomized primal–dual argument whose expectations are integrals over . It makes precise the measure-zero conventions the paper uses: ties in (23), and at segment borders. It also gives a Lean model of a ranking algorithm with continuous seeds that sees only the present customer, which could be reused for related online algorithms.
The pointwise part (Lemma 2) is a direct computation from the booking-limit identity (7). The difficulty is Lemma 3. The constraint for a pair needs , but on a single sample path can be far below this: item may be taken by an earlier customer, or customer may take another item. The bound only holds after conditioning on the other seeds and comparing two coupled runs, one with item and one without. That comparison needs an invariant that holds at every step: the set of items still available in the run with contains the set in the run without . The invariant fails when ties are broken differently in the two runs, so the measure-zero set of ties must be handled explicitly. The conditional expectation of is then an integral of , which is discontinuous at the segment borders.
Fin n and customers Fin T, both 0-based. Prices are 1-based within an item, with pr r 0 = 0 for . Data at indices outside are never read.IsBookingLimits, unique by Proposition 1); on ; . Weak duality is stated for any and any inventories.A firm sells several products, each in limited supply. Customers arrive one at a time, and each product can be offered at one of a few prices. This is the setting of airline fare classes, hotel rate plans and e-commerce discounting. Because future demand is unknown, the firm must decide online whether to sell a unit now at a low price or keep it for a customer who may pay more later. The competitive ratio measures how much an online policy loses against an omniscient benchmark in the worst case.
Ma and Simchi-Levi (arXiv:1905.04770; Oper. Res. 2020, doi:10.1287/opre.2019.1957) give online algorithms whose competitive ratio depends on the price set 𝒫 of each item through a number F(𝒫), and prove that this dependence is the best possible. This mission formalizes the second half, the impossibility result: no online algorithm can beat F(𝒫).
Timeline of the single-price precursors:
A setup has n items. Each item has starting inventory k ∈ ℕ, k ≥ 1, and the same price set 𝒫 = {r⁽¹⁾ < … < r⁽ᵐ⁾}, with r⁽¹⁾ > 0 and r⁽⁰⁾ := 0.
An arrival sequence 𝒜 has T customers. For each customer t, item i and price j it gives a purchase probability p⁽ʲ⁾{t,i}. It is deterministic if every p⁽ʲ⁾{t,i} is 0 or 1.
When customer t arrives, an online algorithm offers at most one in-stock item at one price. It decides using only the setup, the past, and the present customer's probabilities. A deterministic customer buys exactly when p⁽ʲ⁾_{t,i} = 1. A sale earns r⁽ʲ⁾ and uses one unit. ALG(𝒮, 𝒜) is the total revenue. A randomized online algorithm picks a deterministic one at random, ω ↦ alg(ω) with ω ~ μ.
The benchmark OPT(𝒮, 𝒜) is the value of the linear program (5):
The booking limits α⁽¹⁾, …, α⁽ᵐ⁾ of Proposition 1 are the unique positive numbers summing to 1 with
The tight ratio is F(𝒫) = 1 − e^{−α⁽¹⁾}. For a single price F(𝒫) = 1 − 1/e. As r⁽ᵐ⁾/r⁽¹⁾ → ∞, F(𝒫) decreases.
For every k ≥ 1, every price set 𝒫 and every ε > 0, there are a setup with all items of inventory k and price set 𝒫 and a finite distribution over deterministic arrival sequences, with 𝔼[OPT] > 0, such that every (measurable) randomized online algorithm satisfies
The statement only asserts that such an instance exists; it does not fix the paper's construction.
The instance of §5 has n items and nk customers in n groups of k. The groups are ordered by a uniformly random permutation π: group g wants items π_g, …, π_n. The groups are split into m phases; phase j pays up to r⁽ʲ⁾ and contains a fraction β_j = B_j − B_{j+1} of the groups. The milestones are:
The theorem shows that the guarantees of the paper's online algorithms cannot be improved. Theorem 2 of the paper (Multi-price Ranking is F(𝒫)-competitive in the deterministic case) and Corollary 1 (Multi-price Balance tends to F(𝒫) as inventories grow) meet this bound, by Yao's minimax principle. So F(𝒫) is the exact competitive ratio for each price set. Without the theorem, the algorithms' ratios would only be lower bounds. The paper also shows (Proposition 2) that F(𝒫) exceeds the ratios of earlier approaches, so the tight value has practical bite.
The result is proved in the paper, with proofs in §5 and Appendix D, but not machine-checked. The formalization adds three things. First, an explicit treatment of rounding, which the paper sets aside as negligible for large n. Second, a corrected Lemma 5, which as printed is false for small τ. Third, a reusable model of online algorithms with deterministic arrivals and their randomized mixtures, and of the random-permutation instance.
The bound must hold for every online algorithm, including adaptive and randomized ones. An algorithm's decision can depend on everything it has seen, and the instance is averaged over n! permutations. So computing the best online algorithm's revenue directly is hopeless. The single-price instances of earlier work do not suffice either. On them all reasonable algorithms perform alike, whereas here the adversary's phase lengths must leave exactly one optimal way to ration inventory across phases. The upper bound on online revenue holds only asymptotically: the paper approximates harmonic sums by logarithms as n → ∞ and ignores the rounding of phase lengths. That is why the goal is in ε-form. Finally, the concave program that evaluates the bound has a closed-form optimum only when the candidate maximizer is nonnegative; Lemma 5 as printed omits this condition.
Lean conventions:
Fin n, Fin T); prices are 1-based functions ℕ → ℝ with r⁽⁰⁾ = 0 via price.IsBookingLimits, IsPhaseB), not chosen functions; Propositions 1 and 4 make them unique.alg : Ω → OnlineAlg n on any probability space. Its expected revenue is a Bochner integral, with measurability in ω assumed; without that the integral could be 0 and the bound trivial.Disclosed departures from the page:
The quantifier order is part of the theorem: the instance and distribution are fixed before the algorithm. A statement in which each algorithm gets its own hard instance is weaker and is not this theorem.
Needed infrastructure: finite sums over permutations, measure-theoretic expectation over the algorithm's randomness, harmonic-sum asymptotics, and one-dimensional concave maximization. The definitions of online algorithms and of the random-permutation instance are reusable for other Karp–Vazirani–Vazirani-type lower bounds. Contributions are welcome on any milestone. (35), Proposition 4 and (29) are elementary; (25) needs LP weak duality on the instance; Lemma 4 is the main work.
Many learning and estimation problems are solved by a group of computing agents that each hold part of the data and can talk only to their neighbours in a communication network. Each agent has a private cost , and the group wants a minimizer of the average without a central coordinator. In machine learning the agents usually cannot evaluate exact gradients either; they draw noisy stochastic gradients from samples, as in stochastic gradient descent (SGD).
Pu and Nedić (Math. Program. 187 (2021) 409–457) study distributed stochastic gradient tracking (DSGT), where each agent keeps an auxiliary variable that tracks the network-average gradient. With deterministic gradients, gradient tracking achieves linear convergence under a constant stepsize (Nedić, Olshevsky and Shi 2017; Qu and Li 2018). The question for the stochastic setting is whether a network of agents, each with noisy gradients, matches centralized SGD that averages samples per step. This mission is the second of two on the paper: it covers the diminishing stepsize and Theorem 2, which gives an rate whose leading constant does not depend on the network.
There are agents and a decision space with . Agent has a differentiable cost that is -strongly convex with -Lipschitz gradient (Assumption 2); denotes the minimizer of . A query of agent at a point returns , where is a random sample. The samples (agent , iteration ) are mutually independent, and for every fixed
(Assumption 1). Agents communicate through a nonnegative coupling matrix that is doubly stochastic, has some positive diagonal entry, and whose positive off-diagonal entries form a connected undirected graph (Assumptions 3–4). Write for the spectral norm of ; it is below (Lemma 1).
Stack the local variables as , let , and use the Frobenius norm, so that is the consensus error. DSGT (4) starts from an arbitrary deterministic and , and iterates
with stepsize .
Let and let satisfy condition (14) of the paper: exceeds and , and a second explicit inequality in and holds. Then there are constants , independent of , such that for all
The constants may depend on every datum of the run (network, costs, noise law, starting point, , ), but not on .
The leading term involves neither nor the graph: after a transient, the network-average iterate behaves like centralized SGD run on samples per step, and the error decreases as with the number of agents (Remark 3 of the paper). The consensus error decays one order faster, as . The result is a reference point for later analyses of stochastic gradient tracking, which refine the transient time and the dependence on the network.
The theorem is proved in the paper; to the best of current knowledge no part of it is machine-checked. A complete development formalizes the stacked stochastic model, the conditional-expectation estimates behind the linear system, the induction with tuned constants, and the elementary analytic bounds. Two steps of the printed proof need extra care (see Formalization scope), and repairing them is part of the work.
The estimate for the tracker error couples all three quantities: bounding requires and , and requires . A direct estimate of any single error therefore does not close, and the rate for cannot be read off from a scalar recursion until is known. The induction closes only for the constants of the paper and under condition (14), which must be checked to hold for all at once. The probabilistic estimates need independence of the samples across agents and times, since the variance bound for the averaged noise uses that the agents' noises are uncorrelated. Finally, the products and sums of real powers must be bounded uniformly in , including the regimes and .
Points of are EuclideanSpace ℝ (Fin p); stacked variables are functions Fin n → E p, and every matrix norm is the Frobenius sum , never the sup norm of the product type. is the Frobenius norm and the operator norm of Matrix.toEuclideanCLM applied to . The noise space is (the paper's ; is the stepsize offset). Expectations are Bochner integrals, and every bounded expectation comes with an integrability conjunct, so a non-integrable error cannot satisfy a bound by having integral . Powers with real exponents are Real.rpow.
Standing assumptions and additions, all stated in the items:
The constants of the goal are quantified after all data and before ; a statement with the constants chosen after would be trivially true and is not this theorem. The goal mentions only the iterates, , , and the constants of the page, not the auxiliary quantities of the proof.
Contributions welcome: proofs of the analytic milestones (products, sums), the conditional-expectation estimates behind (29), and the repair of the two gaps of the printed proof. The model definitions are shared with the companion mission on constant stepsizes.