Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Large systems of interacting diffusions — neurons, oscillators, agents in a network game, particles in a queueing or load-balancing model — are usually analysed through their mean-field limit: as the population grows, each particle interacts with the empirical law of the others, and the system is replaced by a single nonlinear (McKean–Vlasov) equation. The classical theory assumes that every particle interacts with every other one with the same strength. Real networks are heterogeneous and sparse: particle interacts with particle only through an edge of a random graph, and the number of neighbours of a particle is much smaller than the population size.
Bayraktar, Chakraborty and Wu (Ann. Appl. Probab. 33(5), 2023) describe the heterogeneity by a graphon and prove laws of large numbers and rates of convergence for such systems. This mission is the fifth of a series formalizing that paper. Its subject is the paper's quantitative result for not-so-dense graphs: when the edges are sampled from a Lipschitz graphon and then thinned by a sparsity factor , the average mean-square distance between each particle and its graphon limit is of order for every .
Let with Lebesgue measure. A graphon is a measurable symmetric function . Fix a horizon and write with the norm .
One probability space carries, for every label , an initial state with law and a standard -dimensional Brownian motion , the whole family being independent. The limit system (4.2) is a continuum of diffusions, one per label:
The particles are independent but not identically distributed; their laws are coupled through the -integral.
The not-so-dense -particle system (4.1) uses the same initial states and Brownian motions at the labels :
The edges are percolated samples of (Condition 4.3): , independent for and independent of the noise. A particle has about neighbours, which is why the interaction is scaled by .
The standing hypotheses are Condition 4.1 — measurable with bounded second moments; bounded and Lipschitz; bounded, Lipschitz and invertible with bounded inverse; and — and Condition 2.3: on finitely many intervals covering , the map is Lipschitz in the Wasserstein distance , and is Lipschitz on every block .
Under Conditions 2.3, 4.1 and 4.3, for each there is with
The constant depends on and on the data, never on . The bound is on the average over particles, not on the maximum.
Theorem 4.2 gives an explicit rate for the convergence of a particle system on a sparse random graph to its graphon limit. Its companion, Theorem 4.1 (mission IV), proves the law of large numbers under weaker hypotheses but without a rate. The rate says that the effective sample size is , the typical degree, not : graphs with still approximate the graphon system as long as the degree grows. Results of this type justify replacing a large heterogeneous network by its graphon limit in control and game problems, such as graphon mean-field games, where the error of the replacement must be quantified.
The paper proves the theorem by hand; none of its results has a machine-checked proof. The formalization produces precise statements of the not-so-dense model, of the estimates of §7.1 that hold for any sparsity, and of the discretization bound, each usable on its own. The milestones (7.10) and (7.15) are the paper's key estimates for sparse interactions and are shared with mission IV.
The obvious approach is to compare each with by Gronwall's inequality, after bounding the difference of drifts. That step fails at the interaction term: the edge and the error are dependent, because the edge enters the dynamics of particle . A plain Cauchy–Schwarz bound loses a factor and gives nothing when . Estimates (7.10) and (7.15) quantify how weak this dependence is, and they are where the hypotheses that is invertible with bounded inverse and that are needed. The discretization term needs the Lipschitz regularity of the limit laws in the label (Theorem 2.1(b)), itself a fixed-point estimate on a space of measure-valued maps.
The Lean development uses Mathlib's unitInterval for , Fin d → ℝ with its sup norm for (all constants are existential, so the choice of norm does not matter), time ℝ≥0, and the path space as continuous maps on with the sup norm. Brownian motions, Itô integrals and Itô processes are those of the published Peng1990.SMP.Stochastic; Wasserstein distances are the published WassersteinDRO.Duality.wassersteinDistance, valued in . Particle is Lean's i : Fin n with label .
Committed conventions:
The solution predicates are not vacuous: the zero-coefficient system satisfies both, Condition 4.1 and Condition 4.3 are satisfiable, and every statement quantifies over solutions rather than assuming the conclusion. The constant is chosen after and before , so it cannot depend on , and the bound is the paper's average over , not a weaker or a stronger form. At both sides of every rate are .
The paper's proofs are in its §5 (Theorem 2.1), §7.1 (Lemma 7.1, (7.10), (7.15)) and §7.3 (Theorem 4.2). Stochastic analysis at that level — Burkholder–Davis–Gundy and Rosenthal inequalities, Girsanov's theorem for these SDEs, Gronwall arguments for measure-valued fixed points — is mostly absent from Mathlib, and contributions of such infrastructure are welcome, as are proofs of any milestone.
A vendor holding a finite stock of a product must set prices over time without knowing how many customers will come. Each price does two things: it earns revenue now, and through the sales it generates it reveals information about demand that improves future prices. This tension between earning and learning is central in revenue management with demand uncertainty, in retail markdown pricing, and in online selling. Optimal Bayesian policies for such problems are characterized by a Hamilton–Jacobi–Bellman equation that has no closed-form solution, so practice relies on heuristics, and the question is which heuristics come with guarantees.
Farias and Van Roy introduced decay balancing and proved that, for exponentially distributed reservation prices and a Gamma prior on the arrival rate, it earns at least one third of the optimal expected discounted revenue, uniformly over all problem parameters (V. F. Farias, B. Van Roy, Dynamic Pricing with a Prior on Market Response, Operations Research 58(1):16–29, 2010, doi:10.1287/opre.1090.0729). They describe it as the first heuristic for problems of this type with a uniform performance guarantee. This mission formalizes that guarantee and the chain of results leading to it. The source is the authors' manuscript of January 20, 2009 (MIT DSpace); its printed page numbers coincide with the PDF page numbers, and all theorem and page numbers below refer to it.
Customers arrive according to a Poisson process with rate . Each has an independent reservation price with density and tail ; a customer facing price buys one unit if it is available and is at most his reservation price, and otherwise leaves. The hazard rate is . Assumption 1 (p. 5) asks that be differentiable with support and that be non-decreasing. The exponential law with mean has .
The vendor starts with units and a Gamma prior on with shape and rate (density , mean ). After sales the posterior is Gamma with and , so the state is . A policy sets the price; the expected discounted revenue at rate is
the supremum over all measurable non-negative policies. With known, the same problem has value . Assumption 2 (p. 9) asks that be differentiable in .
Decay balancing uses the approximation , , and posts the price solving the balance equation (5), p. 13,
The optimal price solves the same equation with in place of . The constant
measures the cost of uncertainty for a prior of shape .
For exponential reservation prices with mean , every , , , :
In attack order:
Theorem 2 gives a guarantee that depends only on the coefficient of variation of the prior. Theorem 3 removes even that dependence for exponential reservation prices: whatever the inventory, prior, discount rate and price scale, decay balancing loses at most a factor of three. The analysis also yields reusable facts about Bayesian pricing: knowing the rate helps (), the decay-balance characterization of optimal prices, and comparison with a vendor who does not learn.
All results are proved in the source, using Dynkin's formula, an HJB verification argument (Appendix E) and a coupling of sales processes. None of them is machine-checked. The mission asks for a formal development of the known proofs.
The obvious route to Theorem 3 would chain Theorem 2 at the initial state. That fails because blows up as , so for a diffuse prior Theorem 2 gives no constant bound. The paper instead compares the two systems only up to the first sale, after which the shape parameter is at least . This needs two things: a coupling in which the optimal system never sells first, and Lemma 12, which bounds the value of one extra unit without a decreasing-returns property in (none is known). Lemma 12 itself rests on a numerical inequality involving the Lambert function.
At the foundational level, neither Mathlib nor the platform has a counting process whose intensity is a random rate times a state-feedback price. Defining and faithfully is part of the mission.
Reusable pieces are the Gamma–Poisson sales process in the b-clock, the incomplete Gamma function, and the known-rate pricing problem. Proofs of any milestone, of the p. 6 revenue identity, and of Assumptions 1–2 for the exponential law are welcome.
Related platform work in other models: Gallego–van Ryzin known-demand pricing (GVRPricing), Talluri–van Ryzin (RevenueManagement), Bitran–Caldentey (PricingRM.DetHeuristic), and the Bayesian bounds of Satia–Lave (SatiaLave.Bayes).
Betweenness centrality measures how much of the communication in a network passes through a node. Freeman's original measure (Freeman 1977) counts the fraction of shortest paths between each pair of nodes that pass through it, and Brandes' algorithm (Brandes 2001) made it computable on large graphs. Variants replace shortest paths by maximum flows (Freeman, Borgatti and White 1991), random walks (Newman 2005) or load-splitting rules (Goh, Kahng and Kim 2001), and group variants measure the traffic that passes through a set of nodes (Everett and Borgatti 1999).
Dolev, Elovici and Puzis (technical report 2009, J. ACM 2010) define routing betweenness centrality (RBC): given the actual routing scheme of a communication network and its traffic matrix, the RBC of a node is the expected number of packets that pass through it. Each of the measures above is a special choice of routing scheme. The application is the placement of traffic monitors: the RBC of an ordered sequence of monitors is the expected number of packets sampled by all of them in order, which measures, for example, redundant inspection along a path.
Let be a finite set of nodes. A routing scheme assigns to every source , current node , next node and target a number , the probability that forwards to a packet with source address and target address . Routing decisions are independent. The scheme is assumed to be
A route from to is a sequence of nodes from to whose every hop has positive forwarding probability; its probability is the product of the hop probabilities. For nodes and a sequence :
A traffic matrix gives the number of packets sent from to , and sampling rates give the fraction of passing packets a monitor at samples. The target dependency is , and the RBC of the sequence of distinct nodes is
For a source-oblivious scheme and a sequence of distinct nodes, ,
The right side is the value returned by the paper's Algorithm 6. The identity contains no running time and no constant: it states the exact equality the algorithm relies on.
The goal reduces the RBC of a sequence of monitors to arithmetic on precomputed single-node quantities, instead of a pass over the routing graph of every source–target pair. This is what makes repeated evaluation of candidate monitor sequences, as in greedy or search-based placement, affordable on large networks. Eqs. (1) and (9) are the recursions behind the paper's algorithms for the RBC of single nodes; Eq. (9) replaces the loop over all source–target pairs by a loop over targets.
The paper's proof of Lemma 1 is an argument about conditional probabilities of informally described events. A formalization fixes what "the probability that a packet passes through " means, as a sum over a finite set of routes, and checks the factorization against that definition, including the corner cases the prose passes over: sequences with repeated nodes, a first node equal to the source or to the target, and the source in the sum over all sources. No machine-checked version of these identities is known.
Dependency chaining is a Markov property: after the packet reaches , its future does not depend on its past. The obvious argument splits every route through into a prefix ending at and a suffix starting there. Two points need care. First, the suffix must be a route of a packet with source , which is where source-obliviousness enters; for source-dependent routing the lemma is false. Second, the prefix probabilities must sum to while the suffix probabilities sum to one, which requires that no packet is lost: this is where totality of the forwarding probabilities and loop-freeness (every walk reaches the target in at most steps) are needed. The passage from Lemma 1 to the goal then requires the sum over all sources, including , where Lemma 1 does not apply.
Nodes form a type V with [Fintype V] [DecidableEq V]; probabilities, traffic and sampling rates are real numbers; sequences are Lean lists, indexed from . Routes are repetition-free lists, and every dependency is a finite sum over them; no infinite sums, suprema or measure theory are used. The definitions file bundles the standing assumptions in IsRoutingScheme and source-obliviousness in IsSourceOblivious.
The paper's probabilities are informal. The following readings are explicit:
Defining by the recursion (3) or the product (16), the target sequence dependency by (17), or the sequence RBC as the sum over targets of the chained product would make the goal true by definition; every dependency here is a sum of route probabilities, and the RBC of a sequence is the double sum of Eq. (4).
The running-time claims of the paper are out of scope. Lemma 2 of the paper (p. 17) is false as printed for a nonempty monitor set and is not posed. Contributions welcome: proofs of the milestones, a general lemma that the total route probability from any node is one under a total loop-free scheme (reusable for absorbing Markov chains on finite DAGs), and the prefix–suffix decomposition of routes.
Bounded-confidence opinion dynamics model a population in which each agent repeatedly moves its opinion towards the opinions of those agents whose views lie within a fixed distance of its own. Introduced in discrete time by Krause (1997) and studied as the Hegselmann–Krause model, these systems are a standard test case for multi-agent coordination with state-dependent communication: who talks to whom depends on the current state, so the interaction graph changes over time and the linear consensus theory does not apply. Simulations show that opinions settle into clusters that are further apart than the confidence radius, and that the distances between clusters are larger than the radius would force. Explaining those distances is a long-standing question in the area (Lorenz 2007).
Blondel, Hendrickx and Tsitsiklis (SIAM J. Control Optim. 2010) study the continuous-time version, first for finitely many agents and then for a continuum of agents. The continuum model is the limit of a large population and captures the intercluster distances observed in simulations. This mission formalizes the continuum part of the paper, Section 3: well-posedness for regular initial opinions, convergence to clusters, and the intercluster distance bound of Theorem 6.
Agents are indexed by with Lebesgue measure. An opinion function gives the opinion of agent . Write for the bounded measurable opinion functions and for the nondecreasing bounded ones. For , is the set of whose increase rate is at least for all , and the set with rate at most . A function is regular if it lies in for some ; the uniform profile is regular.
Two agents are connected when their opinions differ by less than . The interaction operator is
Given an initial condition , a solution of (3.2) is a measurable , , with each and
The differential form (3.1) is .
is the set of nondecreasing whose distinct values are pairwise more than apart; the set of nondecreasing whose values, for almost every pair of agents, are equal or at least apart. A fixed point is an for which (3.2) started at has the unique solution . A cluster of is a value held by a set of agents of positive measure , its weight.
For a regular , a solution of (3.2), and almost everywhere: any two distinct clusters of satisfy
and agrees almost everywhere with a member of that is a fixed point.
Theorem 6 turns the qualitative picture "opinions freeze into clusters at least one unit apart", which already follows from Theorem 5, into a quantitative statement depending on the cluster weights: two clusters of equal weight are at least apart, and a light cluster can sit closer to a heavy one. This matches the intercluster distances observed in simulations of large populations and yields Corollary 1 of the paper, a necessary condition for the stability of an equilibrium in the sense. Theorem 4 is of independent interest: the right-hand side of (3.1) is discontinuous in the state, a two-valued initial profile admits two different solutions, and well-posedness holds only under the slope bounds.
The results are proved in the paper. Nothing in this mission has a machine-checked proof yet. Formalizing it means building a small theory of integral equations with a state-dependent, discontinuous kernel on -type spaces of opinion profiles: a contraction argument on short intervals, its continuation, monotone convergence of partial integrals, and an a.e. limit argument with Fatou's lemma and Fubini.
The obvious route to Theorem 4, Picard–Lindelöf, fails: is not Lipschitz on , because a small perturbation of opinions can switch the connection indicator on a set of positive measure. Lemma 1 restores the Lipschitz property only at functions with a positive increase rate, so existence and uniqueness require a contraction on a carefully chosen set of profiles together with a proof that the dynamics keep the increase rate positive (Lemma 2), and a continuation argument whose step size shrinks as the lower slope decays. For Theorem 6, convergence alone gives only ; the extra term comes from agents trapped between two clusters, whose existence relies on the continuity in of every , which the a.e. limit does not have.
Opinion functions are ℝ → ℝ, and only their values on Set.Icc 0 1 matter; a trajectory is x : ℝ → ℝ → ℝ with x t α , time real with . Lebesgue measure on is volume.restrict (Set.Icc 0 1), and uses its product measure. The slope conditions are written multiplied out for . Explicit readings of the paper's phrases:
Tendsto … atTop (𝓝 l) to a real limit; "except possibly for a countable set": a countable exceptional set; "a.e.": almost everywhere for Lebesgue measure on .A trivializing formalization is ruled out: clusters are distinct with positive weight, regularity requires a positive lower slope, the solution predicate forbids the junk value of a non-integrable time integral, and is checked to be regular, so no hypothesis is vacuous.
The development needs an integral-equation solution theory for a discontinuous kernel, the Banach fixed point theorem (Mathlib ContractingWith), Grönwall-type estimates, countability of discontinuities of monotone functions, Fatou's lemma and Fubini. Lemmas 1 and 2 and the lower bound in Theorem 4 are reused by the companion mission on the discrete-to-continuum approximation (Theorem 7). Contributions are welcome on every milestone, and in particular on the slope estimates, which are self-contained.
Many problems in statistical learning, signal processing and distributed optimization minimize a sum of a large number of convex components over a convex set: a data-fit term per sample plus a regularizer or constraint per sample. When is large, a method that processes one component per iteration is often far cheaper per step than one that evaluates the whole sum. Incremental methods do exactly this. The incremental subgradient method of Nedić and Bertsekas (SIAM J. Optim., 2001) takes a subgradient step on one component at a time; the incremental proximal method replaces some of these steps by proximal steps, which are more stable and are cheap when a component has a closed-form proximal map (an term, an indicator of a simple set).
Bertsekas, Incremental Proximal Methods for Large Scale Convex Optimization (Report LIDS-P-2847, MIT, 2010, revised 2011; Math. Program. 129 (2011), doi:10.1007/s10107-011-0472-0), combines the two: each component is split as , with a proximal step on and a subgradient step on , followed by a projection. The paper analyzes two ways of choosing the component at each iteration, a fixed cyclic order and a randomized order. This mission covers the randomized order (§4 of the paper); its companion mission covers the cyclic order.
Let be a nonempty closed convex set and let , , be convex. The problem is
with optimal value , possibly , and optimal set , possibly empty. is the Euclidean projection on and a subgradient of at .
At iteration a component index is drawn and, with stepsize , one of three updates is applied:
The implicit equations are proximal steps: in (42), minimizes over . The randomized order means that is uniformly distributed over and independent of the past history (Assumptions 3(a), 4(a)). The growth conditions (Assumptions 3(b), 4(b)) ask for a constant bounding, with probability 1 and for every component , the norms of the subgradients used by the step that would be taken if were , and the decrease of , along that step by times its length.
If and , then
and if in addition and , then with probability 1 the iterates converge to some (which may depend on the sample path).
Proposition 9 says that a randomized incremental method with a diminishing stepsize solves the problem exactly, almost surely, under conditions that do not require differentiability, bounded level sets, or strong convexity. Propositions 7 and 8 quantify the constant-stepsize regime: the error bound is , smaller by a factor of than the worst case of the cyclic order (Proposition 4 of the paper). This is the paper's argument for randomization, and the same comparison recurs in the later literature on stochastic and incremental methods.
The results are proved in the paper. As far as known, none of them is machine-checked: Mathlib has conditional expectation, filtrations and Doob's martingale convergence theorem, but not the Robbins–Siegmund almost-supermartingale theorem in the form used here, and no incremental or stochastic proximal method has a formal convergence proof on the platform. The mission produces a formal model of a randomized algorithm with implicit (proximal) steps, a formal Robbins–Siegmund special case, and a complete a.s. convergence proof that other stochastic-approximation formalizations can reuse.
The deterministic estimate behind (58) is the one of the cyclic analysis with the sampled component in place of the cyclic one. The new difficulty is the conditioning step: needs the step that would be taken for each component to be a function of the past, and to be independent of it, and both must be stated so that the conditional expectation is that of an integrable function. The obvious route from (59) to part 2 of the goal fails: (59) gives, for each , an event of probability 1, and is in general uncountable, so the events cannot be intersected directly. Part 1 must also handle , where no point of is available.
EuclideanSpace ℝ (Fin n); components are indexed by Fin m (), with .EReal, so is represented and the and statements are in EReal.A formalization in which the would-be steps may depend on , or in which is only assumed uniform, would let a step pick its component adversarially; the measurability and independence hypotheses rule this out, and none of the hypotheses is unsatisfiable (a sorry-free instance with is checked locally).
Needed infrastructure: the Robbins–Siegmund special case (Proposition 2), conditional expectation of a function of an independent uniform index and a past-measurable quantity, and existence of a countable dense subset of a closed set in . The supermartingale theorem and the conditioning lemma are reusable beyond this mission. Proofs of the milestones, of the goal, and of reusable lemmas about projections and proximal steps are welcome.
A finite-sum optimization problem asks for one vector that performs well across many component objectives. In empirical risk minimization, each component can represent the loss from one data point. A full gradient uses every component, whereas a stochastic gradient uses one component and can be much cheaper per step. The latter carries sampling noise, so a method must control that noise while moving toward the optimum. Allen-Zhu's Katyusha paper gives a direct accelerated stochastic method for this setting. Its strongly convex result, Theorem 2.1, bounds the expected objective error of a specified algorithm after a specified number of epochs.
The problem is relevant when the number of terms is large enough that a full gradient at every iteration is costly, but individual component gradients and proximal steps remain practical. Katyusha combines a periodically refreshed full gradient with individual component gradients. The paper's result concerns the actual returned snapshot of Algorithm 1, Option I, whose weighted averaging rule matters to the claim. Formalizing a generic noisy gradient method would leave the paper's central algorithmic guarantee unstated.
Let be differentiable functions, with . Their finite-sum objective is . A real-valued regularizer gives the composite objective
Each is convex and smooth: its gradient is Lipschitz in the Euclidean norm. The regularizer is strongly convex, with , in the paper's convention that the quadratic term has coefficient . The comparison point minimizes the full objective .
Algorithm 1 starts from and keeps three vectors: a snapshot , a proximal sequence , and another proximal sequence . In each epoch it computes . At a current point , it samples uniformly from and forms the gradient estimator
The algorithm then makes two proximal updates using and . Its next snapshot is a weighted average of the new values, with weights for . The iterates and persist between epochs. In the theorem's run the epoch length is , and , , and . The output after epochs is .
For every starting point and minimizer of , the target is the paper's two-case expected bound:
The expectation is over every independent uniform index sampled by the run. The two regimes meet at the threshold where the algorithm's minimum defining changes branch. The milestone list follows Lemmas 2.3–2.7 and the displayed one-epoch inequalities of Section 2.2. It includes the variance bound, the proximal estimates, and the two regime-specific epoch estimates that feed the final theorem.
The theorem gives an accelerated linear reduction of the expected composite-objective error under the paper's strong convexity assumptions. It identifies how the rate depends on component count , smoothness , strong convexity , and epoch count . The author also translates the result into an iteration-complexity statement and uses it as a basis for later reductions and generalizations in the paper. The objective-error theorem is the stable mathematical claim formalized here; the complexity paraphrase is outside this mission's Lean goal.
Allen-Zhu proved Theorem 2.1 in the paper. The Lean declarations in this proposal are targets with proof placeholders, not machine-checked proofs of Katyusha's convergence. Completing them would produce a checked account of the exact algorithm, its finite probability space, and the conditional inequalities for an epoch. The finite-sum and proximal-point definitions reused here are already published in the SAGA formalization; Katyusha's weighted snapshot and coupling statements require their own development.
The estimator is unbiased, but that fact alone does not give the claimed acceleration. Its variance depends on the snapshot and current point, and a direct descent estimate retains a variance penalty. The bound in Lemma 2.4 expresses that penalty through a smooth convex gap which can have either sign before it is combined with other terms. The two proximal sequences and the snapshot therefore have to be accounted for together. Across an epoch, the iterates are averaged with nonuniform weights, while and themselves are carried into the next epoch. Replacing the snapshot with the final value or with a uniform average changes the algorithm and the theorem.
The two rate cases also reflect different parameter values. When , is determined by a square root; above that threshold it is fixed at . A proof of only one branch would omit part of the source result. Treating the sampled indices as a single arbitrary path would ask for a false pathwise guarantee, whereas stating the result for a favorable path would lose the expectation bound.
Vectors are EuclideanSpace ℝ (Fin d) and component indices are Fin n, translating the paper's one-based to a zero-based finite type. The goal fixes as Algorithm 1 does; the conditional one-epoch statements admit any positive . The number of epochs can be zero, in which case the output is the initial snapshot. The objective is real-valued. Thus may be nondifferentiable but does not include extended-valued indicator functions. The component gradient fields are required to be the actual gradients of their functions, and the comparison point minimizes , not merely .
A proximal map is an explicit argument constrained, for every , to minimize the proximal objective of the given . The run computes the paper's two proximal updates with that map. The expectation is the finite uniform average over all sequences, equivalent to independent uniform samples. It never quantifies over a convenient sequence. These links prevent a vacuous or unrelated encoding of the method.
The paper writes both rates using . Its Section 2.2 bounds yield the concrete coefficient in the square-root regime and in the regime; these are the expressions in the Lean goal. For Case 1 the rate is represented by division by , a positive denominator. For Case 2 it is . The statement retains both conclusions at their stated boundary. The one-step lemmas average only a fresh sampled index with the current state fixed, and the epoch statements average the current epoch's indices.
The development needs finite sums and finite expectations, Euclidean smooth and strong convexity facts, proximal minimizer inequalities, and algebra of the weighted snapshot. The finite-sum objective, averaged gradient, proximal-point predicate, and finite index expectation are shared definitions; the Katyusha run, progress value, potential, and epoch inequalities are specific to this algorithm. Contributions proving the milestone statements, establishing existence and uniqueness of the proximal map under these assumptions, or improving reusable proximal and finite-expectation lemmas are within scope.
Reflected backward stochastic differential equations describe processes that must remain above a prescribed obstacle. El Karoui, Kapoudjian, Pardoux, Peng and Quenez connect that probabilistic construction to a parabolic partial differential equation with an obstacle in their 1997 paper. A representation by a stochastic process is useful only if the associated differential equation identifies a definite function. The comparison result in Theorem 8.6 supplies that identification: within a specified growth class, two viscosity solutions cannot disagree. This mission isolates that deterministic uniqueness statement. The companion existence and stochastic representation result is Theorem 8.5 of the same paper.
Fix a terminal time and a spatial dimension . At time and point , the drift is a vector and the diffusion coefficient is a matrix. Both are continuous and Lipschitz in uniformly over . A continuous terminal payoff has at most polynomial growth. The continuous generator depends on a scalar value and a vector ; it has polynomial growth at and is Lipschitz in . The continuous obstacle has a polynomial upper bound and satisfies .
Write . The associated second order spatial operator is . The obstacle problem asks for a function whose terminal value is and whose interior value obeys
A parabolic superjet or subjet at an interior point is a triple of a time slope, spatial slope and symmetric second order matrix that bounds the function locally above or below by the associated quadratic expansion, up to . These jets let a continuous function satisfy the differential inequality without having ordinary derivatives. A viscosity subsolution uses superjets and a terminal upper bound; a viscosity supersolution uses subjets and a terminal lower bound. A viscosity solution satisfies both definitions.
The goal is the paper's Theorem 8.6. Under the coefficient assumptions above and condition (27), every pair of continuous viscosity solutions with polynomial growth agrees on the entire closed time strip:
Condition (27) gives a continuous modulus for the change in between bounded spatial points, with argument and . The quantifiers include every radius , every bounded scalar argument, and every gradient vector . The milestone is Lemma 8.7, which controls the location and separation of the maximizers of the paper's doubled-variable function .
The theorem shows that the obstacle PDE has at most one solution in the natural class allowed by polynomially growing coefficients and payoffs. Together with Theorem 8.5, which identifies the reflected backward SDE value as a viscosity solution, and the growth estimate at the end of Section 8, it yields the paper's probabilistic representation of the unique solution. Theorem 8.6 alone asserts uniqueness, so it makes no existence claim.
The formal development provides reusable interfaces for parabolic jets, viscosity inequalities, the obstacle operator and uniform polynomial growth on a finite time strip. Those interfaces can serve other comparison theorems and other parabolic obstacle problems. The mathematical result is proved in the 1997 article; this mission asks for a Lean proof of its deterministic uniqueness statement. The proposal declares the theorem with a proof placeholder and includes the comparison lemma as an intermediate target.
The first obstruction is that the candidate solutions need only be continuous. Subtracting their PDE expressions directly would assume derivatives they may not possess. The paper instead uses viscosity jets, and its comparison argument invokes the theorem of sums from Crandall, Ishii and Lions' viscosity-solutions guide. The generator's spatial modulus must control a gradient argument that grows as the two spatial points approach each other. Lemma 8.7 provides the necessary separation limit for the maximizers. The argument also treats a polynomial growth class on all of , so a comparison confined to one fixed bounded ball would not establish the stated result.
Lean uses nonnegative real time and functions on represented by Fin d → ℝ. The terminal time and dimension are positive. Bounds with existential constants use the finite-dimensional sup norm, which is equivalent to the Euclidean norm in the paper. The displayed quadratic form, and are written by coordinate sums, so their signs, factor , and matrix order are exact. The obstacle is bounded only above in the data assumptions, exactly as condition (22) states. Condition (27) is imposed only on uniqueness, not folded into the definition of viscosity solution.
Jets are taken at through a one-sided little- bound in the relative neighborhood of the interior strip. The terminal equality comes from the two terminal inequalities; the viscosity tests impose no separate condition at . The printed text calls “symmetric nonnegative matrices,” but the proof of Theorem 8.6 uses arbitrary symmetric matrices produced by the theorem of sums. The formal definition therefore uses all symmetric matrices and records this correction for review.
The mission permits every continuous solution of polynomial growth. It does not restrict candidates to smooth, bounded or stochastic-representation functions. The companion reflected SDE construction, penalization limit and existence theorem are outside this mission's goal; the general stochastic interface Peng1990.SMP.Stochastic is listed as series context but is not imported by the deterministic statements. Useful contributions include the comparison proof, the lemma on doubled-variable maximizers, and reusable lemmas about jet transformations and the matrix trace inequality.
Classical mean-field theory describes diffusions that interact symmetrically, each feeling the empirical average of all the others, and shows that as every particle behaves like an independent copy of a single McKean–Vlasov process. Many systems of interest are not symmetric: neurons, agents in a financial network, or oscillators interact through a graph, and particles in different parts of the graph feel different neighbourhoods. A graphon is the limit object of dense graph sequences (Lovász, Large Networks and Graph Limits, AMS 2012), and it is the natural way to describe the interaction structure of such systems in the limit.
Bayraktar, Chakraborty and Wu (Ann. Appl. Probab. 33(5), 2023) study a continuum of diffusions indexed by labels whose interaction is weighted by a graphon, and prove laws of large numbers and rates of convergence for -particle systems on graphs sampled from the graphon. This mission targets their uniform rate of convergence for weights sampled from a Lipschitz graphon (Theorem 3.2).
Write with Lebesgue measure. Fix a horizon and let with .
On one probability space, are i.i.d. -dimensional Brownian motions and are independent initial states with laws , independent of the Brownian motions. Given a graphon and coefficients , the graphon particle system (2.1) is
with . The particles are independent but not identically distributed, and their laws are coupled through the -integral.
The -particle system (3.1) uses the same randomness at the labels :
so particle and the continuum particle at share their initial state and Brownian motion.
The hypotheses are:
Under Conditions 2.1, 2.3 and 3.2 there is such that
The result. Theorem 3.2 gives a quantitative propagation of chaos for heterogeneous interactions: with weights sampled from a blockwise Lipschitz graphon, every particle of the finite system, not just an average particle, is within in root-mean-square path distance of the continuum particle with the same label. The rate matches the classical mean-field rate (e.g. Sznitman 1991), so heterogeneity of the interaction costs nothing in the exponent. The same estimate covers the deterministic weighted graph and the random graph sampled from (in the annealed sense), and it is the dense counterpart of Theorem 4.2 for percolated graphs.
Formalizing it. The result is proved in the paper (§6.3); it has no machine-checked proof. A formal development would produce a reusable account of graphon particle systems and their finite- approximations: graphon-weighted McKean–Vlasov drifts, couplings through shared noise, and the decomposition of the interaction error into a Lipschitz feedback term, a law-of-large-numbers term and a Riemann-sum discretization term.
The obvious approach is to compare with directly and close a Gronwall inequality. The difficulty is that the comparison involves the empirical, graph-weighted average of the other particles, which is neither the graphon average nor an average of independent terms. Three different errors must be controlled simultaneously and uniformly in : the feedback of all particles' errors into particle , the fluctuation of a sum of independent but non-identically distributed terms whose weights may themselves be random, and the error of replacing an integral over labels by a sum over the grid . The last needs regularity of the law in the label , which is itself a theorem about the graphon system (Theorem 2.1(b)) and fails at block boundaries of , where only the small number of boundary cells saves the rate. Averaging over , as in the law of large numbers of Theorem 3.1, is not enough: the goal bounds the maximum.
Fin d → ℝ with the sup norm; matrices are measured entrywise. All statements are norm-invariant because every constant is existential. Particle is Lean's i : Fin n with label ; time is ℝ≥0; is Mathlib's unitInterval.Peng1990.SMP.Stochastic definitions; an SDE with random initial value is stated as an Itô process for . Each continuum particle uses the natural filtration of ; the -particle system uses the natural filtration of the weights, initial states and Brownian motions at the labels.WassersteinDRO.Duality.wassersteinDistance 2, valued in ; expectations of nonnegative quantities are lower Lebesgue integrals.Sequential decisions often have costs whose timing matters. A controller may choose an action now, observe a random next state, and choose again. Ordinary expected-cost minimization averages the sum of the costs. A risk-sensitive criterion first applies an increasing function to the total cost and then takes its expectation. The curvature of changes how uncertain costs affect the ranking of policies: convex utility penalizes variability in a cost-minimization problem, while concave utility has the opposite tendency. Bäuerle and Rieder study this criterion for controlled Markov processes with general continuous increasing utility, rather than fixing an exponential function. Their finite-horizon discounted result is Theorem 3.6, pp. 10–12 of the authors' manuscript.
Discounting gives early and late costs different weights. For linear , the remaining expected cost can be described using only the current physical state. For general , the effect of a future cost also depends on what has already been paid and on the discount weight currently attached to the next cost. The mission targets the paper's finite-horizon treatment of these two additional quantities. The infinite-horizon problem is a separate part of the paper.
The state space and action space are Borel spaces. At state , the nonempty set contains the actions that may be chosen. If action is selected, the next state has distribution and the stage cost is . The cost is measurable and bounded between positive constants and . The discount factor satisfies , and is continuous and strictly increasing. The paper imposes its compactness and continuity conditions (CC) on , , , and ; these are stated in the model item and correspond to §2, pp. 3–4.
A history policy chooses measurably from the states and actions observed through time . Starting from , it induces a law for the state-action trajectory. The first stages incur the discounted cost , with . The paper minimizes over every admissible history policy. The inverse utility appearing in the paper's original certainty-equivalent criterion can be omitted when selecting a minimizer because is strictly increasing §2, p. 3; §3.3, p. 10.
The extended state is . Its coordinates record the current physical state, accumulated cost, and current discount weight. Define and . A measurable extended-state decision rule chooses an action in . The paper's operator integrates a continuation value at ; takes the infimum of the same integral over equations (3.8)–(3.9), pp. 10–11.
The first target identifies the cost iteration of any sequence of extended-state rules :
The second target is the paper's value iteration for the infimum over all history policies, together with membership of every in its regularity class :
The goal is Theorem 3.6(c): minimizers of exist, and their stage-dependent history rules attain the original objective for every . At stage , the rule uses at the current state, the observed sum , and . “Optimal” compares against all admissible history policies, including those that use more of the history than these three quantities.
Theorem 3.6 gives a finite sequence of minimum-operator evaluations for a problem whose utility of total cost is not additively separable in the physical state alone. Its policy statement also identifies which observable quantities an optimal controller needs to retain. Together, these results relate the original history-dependent problem to an extended-state Markov decision problem §3.3, pp. 10–12.
The paper proves these statements. This mission asks for machine-checked definitions and proofs of the finite-horizon discounted theorem, including the comparison with all admissible history policies. The model layer and the finite-dimensional expectation construction can support later formalizations of other risk-sensitive objectives. The mission itself has no completed proof at the drafting stage.
The extra discount coordinate is essential: after one action, the next cost enters utility with weight , not . Keeping only accumulated cost would describe a different process. The other demanding point is the policy comparison. An iteration over extended-state decision rules has to establish the value of an infimum over arbitrary measurable history policies. Regularity and measurable selection must also be maintained at each step under (CC). The proof of Theorem 3.6 invokes the corresponding total-cost argument from Theorem 3.1, pp. 5–6; the formal development must supply the precise discounted version.
Lean represents and as Borel subsets of Polish spaces, with standard Borel measurable structures. The controlled process is a separate reusable definition containing , , and history policies; the risk-sensitive model adds , , and . The admissible graph is Borel and every section is nonempty. A history is a chronological finite list of earlier state-action pairs and a current state. Each rule is defined on all lists, but only admissible lists of the matching length are visited. The transition kernel is total as a Lean object, and its values outside are irrelevant.
Policy values use nested kernel integrals representing the finite-dimensional marginals of the path law. They are defined from the cost and utility, so the Bellman recursion remains a theorem. The optimized value is an infimum over the subtype of measurable, admissible infinite history policies. The real infimum is meaningful here because this policy class is nonempty under (CC) and finite-horizon costs keep utility bounded on the relevant interval. The extended state uses real coordinates restricted to and ; its transition stays in that domain. “Increasing” in means componentwise nondecreasing in . A minimizer is an admissible measurable rule satisfying on the entire extended domain.
The source's proof sentence that preserves is recorded with explicit integrability of each one-step continuation. For an arbitrary real-valued member of on an unbounded state space, the source's conditions alone do not ensure a finite real expectation. This domain condition prevents Lean's zero value for a nonintegrable real integral from turning the assertion into a different one. It does not narrow the finite-horizon values appearing in the goal. Contributions toward finite-dimensional expectation identities, kernel integrability, the regularity of , and measurable minimizer selection are within scope.
Mean field games describe the limit of symmetric stochastic differential games with players as . A basic question of the theory is which mean field equilibria are limits of Nash equilibria of the -player games. For closed-loop equilibria, in which each player's control may depend on the states of all players, this question was open in general until D. Lacker, On the convergence of closed-loop Nash equilibria to the mean field game limit (arXiv:1808.02745, Ann. Appl. Probab. 2020). That paper shows that limits of closed-loop -Nash equilibria are weak mean field equilibria, a class that can be strictly larger than the classical (strong) one.
Section 7.3 of the paper gives an explicit game in which the difference is visible. It has exactly three strong equilibria (Lacker, Probab. Theory Related Fields 165, 2016, Proposition 3.6, cited as [43] in the paper) and infinitely many weak ones. The weak equilibria form a family indexed by a switching time , and for they are not mixtures of strong equilibria (Remark 7.1). Proposition 7.2, the subject of this mission, treats : the natural symmetric feedback is an -player approximate Nash equilibrium, and its population mean selects the equal mixture of the two strong equilibria rather than the third one, . The selection mechanism is regularization by noise: the mean of the population solves an ill-posed ODE, and the small noise of the -player system picks out a particular random solution (Trevisan, Electron. Commun. Probab. 18, 2013, cited as [57] in the paper).
Fix a horizon . In the mean-sign game each of players controls a real state
with controls and independent standard Brownian motions . The mean process is , the mean of the empirical measure . Player maximizes the expected terminal reward
that is, , , with , and initial law .
A Markovian control of player is a Borel function of time and the current states of all players. A profile is a Markovian -Nash equilibrium if no player can raise their payoff by more than by switching to another Markovian control while the others keep theirs (Definition 2.1).
With for , , , the sign feedback (7.13) with is
the same for every player. Finally on (7.11).
For the profile :
The goal also asserts that the -player system under has a solution, so that the equilibrium property cannot hold vacuously.
Proposition 7.2 is a concrete instance of the paper's main theme. Theorem 2.7 says that limits of closed-loop equilibria are weak equilibria; this example exhibits explicit, symmetric, Markovian approximate equilibria whose limit is a genuinely random equilibrium (the sign of the mean is a fair coin), selected by noise among infinitely many candidates, and it identifies the limiting law of the population mean exactly. The paper states that the analogous claim for , where the limit would be a weak equilibrium that is not a mixture of strong ones, is not resolved; a formal treatment of the case makes the structure of that question precise.
Nothing of this proposition is machine-checked. Formalizing it requires weak solutions of SDEs with discontinuous drift, Nash equilibria over Markovian feedback controls, and weak convergence of laws on path space, all stated so that the junk values of Lean's total functions never enter. The objects defined here (the -player game with quantified weak solutions, its payoffs and Markovian -Nash equilibria) are shared with the other missions of this series.
The obvious argument for compares player 1's payoff under a deviation with . A deviation changes the drift of the mean only by , but the dynamics of the mean, , is ill-posed in the limit: the ODE , , has infinitely many solutions . Continuity of the solution map, the usual tool, is unavailable, and one must instead identify the limit law, which comes from the vanishing noise, and show that it is unchanged by the deviation. The second difficulty is that the payoff is unbounded, so convergence of laws does not give convergence of payoffs without a uniform integrability estimate. The proof in the paper is short, but relies on a cited result on the vanishing-noise limit and on a compactness argument in a weak topology for the deviating controls.
EuclideanSpace ℝ (Fin 1) (the platform's EthierKurtz.SDEState 1) and its coordinate is y 0. Controls are real, .Real.sign (), and the control vanishes at , both as printed.Contributions welcome: the existence of weak solutions for bounded measurable Markovian drifts, the vanishing-noise limit of , and Girsanov-type change-of-measure estimates are all reusable beyond this mission.
A directed polymer in random environment is a random walk path reweighted by a random potential that is refreshed at every time step. It is a basic model of a one-dimensional object (a polymer, an interface, a flux line) pinned by impurities, and a discrete version of the KPZ universality class in dimension . A central question is localization: whether the walk's endpoint at time , under the random Gibbs measure, concentrates on a few sites or spreads out like a simple random walk.
For a fixed disorder law there is a critical inverse temperature (Comets–Yoshida, Ann. Probab. 2006). In the low-temperature phase the endpoint has atoms of positive mass, in the Cesàro sense, at a positive fraction of times (Carmona–Hu 2002, Comets–Shiga–Yoshida 2003); in the high-temperature phase it does not. Atoms alone say nothing about geometry: the mass could sit on a few sites that are far apart. Bates and Chatterjee (arXiv:1612.03443v5, Ann. Probab. 2020) prove that in the low-temperature phase the mass also sits on a region of bounded diameter at a positive fraction of times, in every dimension and for every disorder law with exponential moments. Before this, geometric localization was known only for the integrable log-gamma polymer in dimensions (Comets–Nguyen 2016).
Fix . Let be i.i.d. real random variables with law , not supported on a single point, such that for (assumption (1.1)), where is the inverse temperature. For a nearest-neighbour path of length from the origin, its weight is . The endpoint distribution is the total weight of paths ending at divided by the total weight of all paths. The partition function is and the free energy is . The limit exists, and is characterised by for and for .
For and let be the set of probability mass functions on that give mass greater than to some set with .
The proofs work on the space of partitioned subprobability measures: functions on with , modulo translations of each copy of , with a metric that makes compact. The update induces a Markov kernel on ; is its set of invariant probability measures and the minimisers of a free-energy functional . On the mission uses the functionals , the support number (number of copies carrying mass), (the least diameter of a region of one copy with mass ), and , where is the mass of copy .
If , then for every there are and , depending only on , such that
If , then for every and every ,
The goal fixes no constants: and are only asserted to exist.
The theorem shows that the low-temperature phase is detected by the shape of the endpoint distribution, not only by its largest atom: positive-density geometric localization holds if and only if . The determinism of and makes the statement uniform over all environments with the given law. The conditional results 5 and 6 reduce full-density and favourite-region localization to a single property of the limit set , which is open.
The result is proved on paper; nothing in it is machine-checked. A formalization would produce a checked development of the compact space , of the Markov kernel , and of the variational characterisation of the free energy, which also underlies the companion mission on asymptotic pure atomicity of the same paper.
The obvious approach, tracking in , fails because mass escapes to infinity: the sequence has no convergent subsequence in any space of probability measures on . The paper's compactification keeps pieces of mass that drift apart as separate copies, so a limit point can split one copy's mass over several. The semicontinuity of , and (Lemma 7.1) only goes one way for this reason, and positivity of the localized fraction needs the separate identity of Lemma 7.2, which uses strict convexity and the non-degeneracy of . Theorem 5.3 already requires the full variational machinery of §4 (convergence of empirical measures to ), which is the companion mission's subject.
Points are Fin d → ℤ, cells are ℕ × (Fin d → ℤ), and paths are sequences of signed coordinate steps. The environment is a family of independent measurable random variables, each with law , on an arbitrary probability space. The phases are encoded through Theorem A as () and (), with computed under the canonical product environment. Elements of are represented by their representatives, with the topology generated by -balls (no quotient). In the goal, and are chosen before the probability space. Part (a) is stated for all and part (c) for , as printed.
Trivializing encodings are ruled out: requires total mass exactly ; and take values in so that an empty infimum is ; is computed in so that ; the sum in is taken in ; avoids a real infimum over ; is non-degenerate; and the phase hypotheses are limits that exist.
A complete development needs: the metric space and its compactness, the measurability and continuity of , the Wasserstein space (here through the published RWPI.SqrtLasso.transportCost), and the convergence (Theorem 4.9) together with at high temperature (Theorem 5.2), both posed in the companion mission. Contributions to any milestone, and to the shared infrastructure of , are welcome.
Heat flow gives an analytic way to describe how functions spread on a space. Optimal transport gives a metric way to describe how probability measures move on the same space. On a smooth Riemannian manifold, a lower Ricci curvature bound constrains both motions. The problem addressed by Ambrosio, Gigli and Savaré is to identify the corresponding relationship when the underlying space need not be a manifold. A Dirichlet form can specify a heat flow even when there are no smooth coordinates, while a Wasserstein distance can measure transport between probability measures. Theorem 4.17 connects these two descriptions for Riemannian energy measure spaces.
The paper proves the implication from the Bakry–Émery condition to the Riemannian curvature-dimension condition . Its printed theorem is an equivalence; the paper cites the reverse implication from earlier work in the proof on p. 58. This mission targets the implication established here, with the source's exact assumptions.
Let be a complete, separable metric space with a Borel measure . A Dirichlet form assigns a nonnegative energy to square-integrable functions, is quadratic and lower semicontinuous, and decreases under normal contractions. Its associated heat flow evolves a function over time. The associated carré du champ measures the energy density of a function. Functions with energy density at most one define an intrinsic distance
For the Riemannian energy measure space in this mission, this intrinsic distance is the metric of . The structure also requires the paper's upper regularity and continuous-representative properties. The growth condition controls the measure of large balls. In the condition, a weak second-derivative inequality for the heat flow has curvature parameter and no finite-dimensional correction term. These assumptions are stated at the start of §4 and govern the §4 milestones even when an individual theorem does not repeat them. See Definitions 3.6 and 3.16 and the opening of §4.
Write for the probability measures with finite second moment, for their quadratic Wasserstein distance, and for entropy relative to . The heat flow has a dual action on measures. The target asks for a curve from every that satisfies the following evolution variational inequality against every of finite entropy, at every :
The definition also includes full support, local finiteness, the exponential growth condition, and the length-space property. See Definition 3.1.
The goal is the forward implication of Theorem 4.17:
Three milestones supply central results from the paper. The final assertions of Theorem 3.17 give the dual measure flow and its absolute continuity after positive time. Corollary 3.18 identifies with the contraction on probability densities. A companion item, Theorem 4.8, gives an entropy bound for when has finite second moment:
The third milestone, Theorem 4.16, bounds the distance and entropy at the heat-evolved endpoint of a regular curve :
The milestone list follows the source labels and constants in §4.
The conclusion turns an analytic curvature bound on a heat semigroup into a transport statement about entropy on probability measures. It therefore identifies a concrete set of Dirichlet-form hypotheses under which the heat evolution has the metric behavior demanded by . The result applies in the paper's metric measure setting, where the space may lack a smooth tensor calculus. The conclusion carries convergence from every initial measure in and the inequality for all finite-entropy comparison measures.
The mathematical implication is proved in the cited paper. The proposed Lean statements are open proof targets: their declarations compile with placeholders, and no machine-checked proof of this implication is asserted here. A complete development would connect Dirichlet-form calculus, probability measures, entropy, and Wasserstein geometry in reusable interfaces. The dual-flow and regular-curve definitions are especially useful beyond this theorem.
The heat flow is initially specified on square-integrable functions, whereas the target is an inequality for probability measures, including measures without an initial density. A bound on by itself controls functions almost everywhere; it does not immediately produce the pointwise dual flow or the right derivative of required by Definition 3.1. The action estimate also begins with regular curves, while the target quantifies over every initial measure in . These changes of domain and regularity are the central mathematical obstacles; simply renaming the heat semigroup as a measure flow leaves the target unjustified.
Lean uses real-valued function representatives for , with almost-everywhere congruence in the Dirichlet form and heat flow. Measures use the Borel sigma algebra. The source uses its -completion; the formalization treats quantities invariant under -almost-everywhere equality, and this convention is explicit in the definition layer. The metric is complete and second countable, and its equality with is part of the energy-measure-space predicate. A sigma-finiteness instance is carried where entropy or measure operations need it; it follows from the source's measure-growth setting. The dual flow and the extension are bound by predicates that specify their action on densities. The mollifier for a regular curve is bound by the conditions of (2.17), while the action is the infimum of squared admissible speeds, which equals the integral of the squared metric derivative.
Wasserstein costs use , and entropy uses extended real values. Theorem 4.8 restricts to positive numbers, so the ball mass and used in its formula have the intended domain. Theorem 4.16 also uses , making meaningful, including at . The goal requires an EVI flow beginning at each and the inequality at every positive time; allowing a vacuous flow or checking only almost every time would not express Definition 3.1. Contributions may establish the milestone statements and the companion Theorem 4.8, develop the omitted intermediate estimates from §4, or prove the goal from the source's full argument.
Mean field games (Lasry–Lions 2006, Huang–Malhamé–Caines 2006) describe Nash equilibria of stochastic differential games with very many symmetric players. In this description each player interacts with the others only through the empirical distribution of their states. The mean field game is meant to be the limit of the -player games as . Making that link rigorous has two halves:
For closed-loop equilibria, where players react to the observed states of all others, both halves are harder than for open-loop equilibria. A single player's deviation changes the feedback of the whole system.
This mission covers the converse half of D. Lacker, On the convergence of closed-loop Nash equilibria to the mean field game limit (arXiv:1808.02745v1, 2018; Ann. Appl. Probab. 30(4), 2020).
Timeline.
Fix a horizon , a compact convex action set in a real normed space, an initial law and coefficients
The -player game.
with independent Brownian motions and i.i.d. initial states of law .
The mean field game. A flow is a strong MFE if some Borel feedback satisfies two conditions:
A strong RMFE is the relaxed analogue.
The assumptions are:
Under Assumptions A, B and C, if is a strong MFE, there are two families of objects:
such that
The goal asserts no rate, so any quantitative improvement still implies it.
The result. Theorem 2.11 says that the strong MFE is a faithful idealization: every classical mean field equilibrium is approximately realized by Markovian feedback equilibria of large finite games. No continuity of the equilibrium feedback and no master equation are required. Together with the paper's main limit theorem (mission 1 of this series), it locates strong MFE inside the set of limits of closed-loop equilibria. The paper's Section 2.4 explains why the same converse is open for weak MFE.
Formalizing it. The result is proved on paper but has no machine-checked proof. A complete development would produce several reusable pieces:
None of these is in Mathlib.
The obvious argument has every player use , invokes the McKean–Vlasov limit, and passes optimality to the limit. It fails at two places:
Representation.
EuclideanSpace ℝ (Fin d).ProbabilityMeasure with the weak topology and the Borel -field.Set.Icc 0 T with the compact-open (uniform) topology.Committed choices.
Ruled out. Because equilibria quantify over solutions, a profile whose state system has no solution would be an equilibrium vacuously. For this reason every existence conclusion (the goal, Theorem 3.10, Proposition 3.4(a)) also asserts that the chosen profiles have solutions, and strong (R)MFE requires the equilibrium SDE to have one.
Infrastructure. A complete proof needs Girsanov's theorem, strong existence for SDEs with bounded measurable drift, measurable selection, tightness on path space, and total-variation propagation of chaos. Each is reusable well beyond this mission, and contributions of any of them are welcome. Proposition 3.4(b), the weak half of Proposition 3.7, and Theorem 2.7 are outside this mission.
Sparse recovery asks when a vector with few nonzero coordinates can be reconstructed from fewer linear measurements than unknowns. A related geometric question asks how many faces of a high-dimensional cross-polytope survive a random linear projection. The two questions meet at the same threshold: uniqueness of a minimum-one-norm solution corresponds to a face of the projected cross-polytope. For Gaussian measurement matrices this threshold was known before the work of Bayati, Lelarge and Montanari, from Donoho's face-counting analysis (Donoho 2006); the same curve was later identified as the transition of approximate message passing (Donoho, Maleki and Montanari 2009). Their 2015 paper establishes the same weak-neighborliness curve for a broader class of independent sub-Gaussian entries with a nonzero Gaussian component. The result addresses the universality question posed for these projections: does the asymptotic transition depend on the full entry distribution or only on broad features of the matrix law?
The mathematical theorem is established in that paper. This mission records its statement in Lean and leaves the machine-checked proof open. The relevant statement is Theorem 2 on page 5 of the pinned arXiv version 2, rather than a claim about every random projection without a Gaussian component.
The cross-polytope is the unit ball for the coordinate one-norm in :
For an matrix , the projected polytope consists of all with . Write for the number of nonempty faces of whose affine dimension is . The weak neighborliness level of a random sequence means that, for every , the ratio converges in probability to one, while the analogous ratio with converges in probability to zero. Both limits belong to the definition; the first alone would record only survival below a candidate threshold.
The matrices have rows for a fixed sampling ratio . Within each matrix, the entries are independent, centered, unit-variance, and sub-Gaussian with one scale factor independent of . They also admit a decomposition , where and the entries of are independent standard normal variables, jointly independent of . The theorem imposes no independence between matrices with different values of Bayati–Lelarge–Montanari, Theorem 2.
Let and be the density and distribution function of a standard normal random variable. The paper defines its phase boundary through a positive parameter :
Footnote 3 states that decreases from one to zero on the nonnegative half-line, so each has exactly one positive parameter. The goal, Theorem 2, says that whenever , the sequence has weak neighborliness in probability. The Lean theorem spells out this parameter relation; it does not apply an inverse function at an argument outside a proved range.
The milestone list covers the two scalar results identifying the boundary, a deterministic condition for exact recovery, and the compressed-sensing transition. With standard normal and , the scalar function is
Lemma 8 gives its unique positive minimizer and its minimum value. Lemma 9 relates that minimum to both sides of the boundary. The scalar state evolution , with and soft thresholding, has slope at the origin and is concave (Lemma 7). Lemma 10 shows that a two-time correlation map satisfies on . Theorem 10, cited from Bürgisser and Cucker, bounds the probability that a Gaussian-perturbed rectangular matrix has a small least singular value:
Lemma 5 gives a recovery condition based on an approximate dual certificate and singular-value bounds. Theorem 8 states that minimum-one-norm recovery succeeds with probability tending to one below the boundary and fails with probability tending to one above it Bayati–Lelarge–Montanari, pp. 39–41, 60–61.
The goal would certify that the same face-count transition applies to every entry law in the stated class, including laws that are not identically distributed across the matrix. The conclusion is geometric: it counts faces of an actual projected one-norm ball. The recovery milestone provides a second way to state the threshold for sparse signals. Together they make the normalization and the two sides of the transition explicit, so future variants can compare their assumptions and conclusions with a fixed formal statement.
No machine-checked proof of Theorem 2 or of the selected milestones is known. The declarations are open Lean statements over explicit definitions. A complete development would formalize the known argument in the paper, including the probabilistic estimates and the bridge from recovery probabilities to face counts. Sharper results that remove the Gaussian component would be separate theorems with their own hypotheses.
The count of surviving faces depends on many supports and sign patterns simultaneously. Matching means and variances of matrix entries does not make their finite-dimensional face counts equal. Likewise, controlling recovery for one fixed signal does not immediately control the fraction of all faces. Near the boundary, exact recovery also requires uniform singular-value information for many column submatrices. These are the points where elementary concentration for a single entry or a single support is insufficient. The source paper treats the geometric statement and the recovery transition under a Gaussian-component condition; a proof that silently assumes full Gaussianity would miss its universality claim.
Vectors are functions on Fin n, and every one-norm is an explicit sum of absolute values. The squared Euclidean norm is a sum of coordinate squares; the default norm on Fin n → ℝ is not used for it. Face counts reuse the published Grunbaum2003.faceCount definition, with dimension for nonnegative ; negative dimensions have zero nonempty faces. The two limits in weak neighborliness use convergence in measure, which expresses convergence in probability here. The printed lower ratio has a zero denominator for , so that limit is stated for . Ratios at small may involve zero denominators, but the asymptotic assertion concerns arbitrarily large .
Theorem 2 uses variance one and an Gaussian component. Theorem 8 instead uses variance and an component, exactly as printed. Sub-Gaussianity uses Mathlib's moment-generating-function predicate for all real parameters; this is the operative two-sided reading of the paper's stated scale condition. The scalar Gaussian expectation in is accompanied by an explicit integrability conclusion in Lemma 8, excluding Lean's zero value for a nonintegrable integral. The restricted least singular value is the infimum of output norms on unit column vectors. This gives zero when a wide submatrix has a kernel and is the bound needed by Lemma 5. The state-evolution map is written as a function of , and its derivative at is a right derivative. In Lemma 10 the law of is the three-atom mixture on , with the split of the mass between the two infinite atoms left free. The page's clause is stated for , since the derivative equals at . Theorem 10 quantifies and , which the page leaves implicit.
The random-matrix predicates require measurability, independence within each , the stated marginal laws, and independence of from . They leave the matrix law otherwise arbitrary. The weak-neighborliness predicate contains both face-ratio limits and ; neither the goal nor a milestone defines the threshold by assuming its conclusion. A full proof needs reusable facts about Gaussian integrals, independence of finite arrays, random face counts, restricted singular values, and the relation between projected faces and unique one-norm recovery. Contributions establishing those facts or closing any of the listed theorem statements are within scope.
Mean field games (MFG) were introduced by Lasry and Lions (2007) and by Huang, Malhamé and Caines (2006) as limits of stochastic differential games with many symmetric players. The model is only meaningful if equilibria of the -player games actually converge to equilibria of the limit game. That convergence depends on what information the players use. For open-loop equilibria, where controls are functions of the noise, it was established in general by Lacker (2016) and Fischer (2017). For closed-loop equilibria, where a player's control is a feedback on the observed states of all players, the deviation of one player changes the state processes of all others, and the only general results before this paper (Cardaliaguet, Delarue, Lasry and Lions, 2019) required a unique MFE and a smooth solution of the master equation.
Timeline:
Fix a dimension , a horizon , a compact convex control set in a normed space, an initial law on , and bounded continuous functions , , , where ranges over the probability measures with the weak topology (Assumption A). Assumption B asks that be convex for each .
In the -player game, player picks an admissible closed-loop control : a measurable, non-anticipating function of time and of the paths of all states. The states solve
with independent Brownian motions and i.i.d. initial states of law , and player receives . A closed-loop -Nash equilibrium is a profile from which no player gains more than by a unilateral deviation. The random empirical measure flow is an element of .
A function of , with a measure flow, is semi-Markov if it depends on only through . A weak MFE is a filtered probability space carrying a random flow , a Brownian motion and a state with , with independent, a semi-Markov control driving , optimality of against every semi-Markov alternative (the alternative state being driven by the same and ), and the consistency condition . When is deterministic this is the usual (strong) MFE.
Under Assumptions A and B, if , , and is a closed-loop -Nash equilibrium of the -player game, then
and every subsequential limit in law is the law of the flow of a weak MFE. No constant and no rate is asserted.
Without convexity (Theorem 3.9) the same holds with weak relaxed MFE, and Proposition 3.7 identifies weak relaxed MFE flows with weak MFE flows under Assumption B. The proof path of Section 5 is: tightness of the path-space empirical measures (Lemma 5.1), a projection lemma (Lemma 5.2), the realization of a randomized Fokker–Planck equation by a semi-Markov relaxed control (Lemma 5.3), identification of the limiting dynamics with the limiting average value (Theorem 5.4), approximation of relaxed by continuous controls (Lemma 5.5), and the limit of unilateral deviations (Proposition 5.6). Two supporting results come from Section 2.1 (well-posedness of the -player system) and Appendix A (Corollary A.7).
The theorem shows that the mean field game is the correct limit of closed-loop -player games without any uniqueness assumption, which is the regime where the master-equation method is unavailable. The price is the limit object: a weak MFE, whose measure flow may be random and whose control may depend on the past of the flow. The paper also shows (Proposition 7.2) that this randomness genuinely occurs, so the result cannot be strengthened to strong MFE in general. Combined with the converse (Theorem 2.11, mission 2 of this series), it characterizes which MFE arise as closed-loop limits.
The result is proved in the paper; nothing in it is machine-checked. A formalization produces a checked definition of closed-loop -player games and of weak semi-Markov MFE, which are reusable for any MFG convergence result, and it would make explicit the measurability bookkeeping (semi-Markov controls, completed filtrations, conditional laws) that the paper outsources to its appendices.
The obvious argument fails at the deviation step. In the open-loop setting a deviating player leaves the other players' states unchanged; here the other players' feedback controls react to the deviation, so the state of every player changes. The paper's way around this is to identify the limit with semi-Markov controls and show that the value of a deviation can be approximated by -player deviations of a specific form; making this work requires relaxed controls, a measurable projection onto the filtration of the (random) flow, and well-posedness of SDEs with bounded measurable drift and random coefficients. A newcomer's first idea, passing the Nash inequality to the limit with Markovian limit controls, does not work, because the limit flow is random and the limit control must see its past.
EthierKurtz.SDEState d; Brownian motion is the platform's EthierKurtz.IsStandardBrownian. is Mathlib's ProbabilityMeasure with the weak topology and the Borel -field of that topology. Paths and flows are continuous maps on with the uniform topology.NSol is inhabited and the weak MFE predicate is satisfiable (checked for ), so neither the hypotheses nor the conclusion of the goal holds vacuously; the conclusion asserts the existence of a weak MFE with the limiting flow law, not a property of an arbitrary one.A lower bound on Ricci curvature can be expressed in two ways that make sense far beyond smooth manifolds. The Eulerian way bounds the gradient of the heat semigroup: Bakry and Émery's -calculus gives . The Lagrangian way bounds how heat flow moves probability measures in optimal transport distance: . On Riemannian manifolds the two are equivalent (von Renesse–Sturm 2005). Kuwada (2010) showed that the equivalence is a general duality between a pointwise gradient bound with a constant and -contraction with the same constant, valid on length metric measure spaces.
Ambrosio, Gigli and Savaré (arXiv:1209.5786v4, Ann. Probab. 2015) needed this duality in a setting with no doubling or Poincaré inequality, where the semigroup comes from an abstract Dirichlet form and is only defined almost everywhere. Their §3.2 builds the dual semigroup on probability measures and proves the contraction (Theorem 3.5). Combined with their Theorem 3.17 it gives Corollary 3.18, the step that links the Bakry–Émery condition to -contraction and, later in the paper, to .
Let be a complete separable metric space with a Borel measure of full support such that for every ball (condition (MD)). The space is a length space if is the infimum of the lengths of curves joining to (3.2).
A Dirichlet form on is a lower semicontinuous quadratic form with dense domain that does not increase under normal contractions; it is strongly local if whenever and have disjoint supports. Its heat flow solves in . It is mass preserving if (2.12).
denotes bounded Lipschitz functions, the slope, and the Borel probability measures. The Wasserstein cost is
Two hypotheses on the semigroup, with bounded on every :
for . Under (3.15) the map extends uniquely to a weakly continuous dual semigroup , and is the pointwise version of (Proposition 3.2).
Under (MD), the length property, (2.12), (3.15) and (3.16), for every and ,
The constant is left free; the goal is the duality itself, not a particular curvature bound.
The theorem turns a pointwise, infinitesimal estimate on functions into a global estimate on measures. In the paper, with it gives the -contraction of the heat flow under (Corollary 3.18). That contraction is an ingredient of the identification of the heat flow with the gradient flow of the entropy (Theorem 4.17). The argument of §3.2 avoids doubling and local Poincaré assumptions on the metric measure space (p. 26), which is what makes it usable for the general Energy measure spaces of the paper.
The result is proved in the literature: in Kuwada's paper, and in the form posed here in §3.2 of the source. As far as a search of the Prove2Me catalogue shows, none of it is formalized: there is no Wasserstein distance on a general metric space, no dual semigroup of a Dirichlet form, and no Hopf–Lax semigroup on metric spaces. The mission asks for formal proofs of the known argument; the dual semigroup, Lemma 3.3 and the Hopf–Lax estimates are reusable on their own.
The semigroup acts on classes, while (3.16) and the contraction are statements at every point; the bridge is the pointwise version , which exists only through the dual semigroup and its weak continuity. The direct approach, applying the gradient bound along a geodesic between and , fails because is not a supremum over Lipschitz functions of a linear quantity. The route goes through the quadratic Kantorovich duality and the Hopf–Lax semigroup on a metric space, neither of which is available in Mathlib, and through limits of integrals against varying measures . Passing from Dirac masses to arbitrary needs a measurable selection of optimal plans.
IsHeatSemigroup, IsDualSemigroup), not constructions. IsDualSemigroup requires for probability densities and weak continuity on , which determines on . Choosing as anything else (e.g. the identity) does not satisfy the predicate, so the goal is not trivialized that way. Dropping the length property would change the statement.Contributions welcome: the quadratic Kantorovich duality on Polish spaces, Hopf–Lax calculus on length spaces, measurable selection of optimal plans, and the portmanteau-type Lemma 3.3.
There are two standard ways to do analysis on a non-smooth space. The first starts from an energy: a Dirichlet form on , its heat semigroup and its carré du champ . This is the setting of Bakry–Émery -calculus and of the curvature-dimension condition . The second starts from a metric measure space : slopes of Lipschitz functions, the Cheeger energy, Wasserstein distances, and the synthetic Ricci bounds and of Lott–Villani and Sturm.
Moving between the two requires a dictionary. A Dirichlet form defines a distance, the intrinsic distance (Biroli–Mosco, Sturm). That distance defines a Cheeger energy. The question is whether the energy rebuilt from is the energy we started from. Ambrosio, Gigli and Savaré answer this in §3.3 of their paper on the Bakry–Émery condition and Riemannian Ricci bounds (arXiv:1209.5786, Ann. Probab. 2015). Their answer is the identification used in the main theorem of the paper, .
Timeline:
Let be a set with a σ-additive measure . A Dirichlet form is a lower semicontinuous quadratic form with for every 1-Lipschitz with , and with dense domain . It is strongly local when whenever a.e. for a constant . A function belongs to , with carré du champ , if for all bounded .
Let be the set of continuous with a.e. The intrinsic distance is
An Energy measure space (Definition 3.6) is a strongly local Dirichlet form on a Polish space with a fully supported Borel measure such that is a finite complete distance inducing , and a continuous has its truncations in .
On the metric side, is the slope, and the Cheeger energy is
Condition (MD) asks that be complete and separable, , and balls have finite measure. Condition (ED) asks that every be 1-Lipschitz for (ED.a), and that every Lipschitz with and bounded support lie in (ED.b). is upper-regular (Definition 3.13) if every in a dense subset of is an limit of bounded continuous with bounded upper semicontinuous and .
For an Energy measure space,
and in this case .
The identification lets every metric notion be applied to an energy structure. Once it holds, the Wasserstein gradient flow of the entropy, the formulation and all make sense for the energy. That is the route by which the paper proves that on a Riemannian Energy measure space implies , the converse of the earlier result. Theorem 3.12 gives the one-sided inequality under the single condition (ED.b), and (3.41) says the energy density is the squared minimal weak gradient. Mass preservation is a standing hypothesis of several other results of the paper, and here it comes for free.
All of these results are proved in the paper, partly by citation: the mass-preservation clause rests on [6, Theorem 4.20], and the length property uses a midpoint criterion from Burago–Burago–Ivanov. None of them has a machine-checked proof. Mathlib has no Dirichlet forms, no Cheeger energy and no theory of length spaces built from curve length. This mission produces precise Lean statements of the paper's identification theorem and of the lemmas its proof uses, so that the metric–energy dictionary can be built up and proved one piece at a time.
The inequality is the easy direction once (3.32) is available. Proving (3.32) means bounding the energy density of the Hopf–Lax inf-convolution pointwise by . Only finite minima over a countable dense set lie in , so the bound has to pass to the limit through the lower semicontinuity (2.10) of .
The reverse inequality needs the opposite move: from an -a.e. bound to a pointwise bound on the metric slope at every point. That step is Proposition 3.11. It needs to be upper semicontinuous and to be a length distance. Without upper semicontinuity, an a.e. bound says nothing about the slope at a given point. The obvious idea, testing against the Lipschitz functions given by (ED.b), produces only lower bounds on and cannot give . That is why upper regularity is the exact condition. The length property (Theorem 3.10) is itself proved by contradiction from a Lipschitz test function built from two disjoint balls. On a space that is not locally compact, this needs a completeness argument rather than Hopf–Rinow.
Representation. Elements of are functions . is off , and every predicate is invariant under -a.e. equality. The σ-algebra is Borel (BorelSpace), standing in for its -completion. The topology is the topology of the metric of , and condition (b) of Definition 3.6 says that this metric equals . Completeness and separability are typeclass binders. The carré du champ is a predicate on a density, never a chosen function. Slopes, , and curve lengths take values in . The curve length is the total variation, which agrees with . The truncation profile of (3.27) is a parameter with the properties the paper fixes. "Dense in " means dense for the norm . The minimal weak gradient is required to be nonnegative, which makes its two characterizing conditions determine it. Mass preservation is stated on , with part of the conclusion. In Theorem 3.9 the printed "distance on " is read as a distance on .
Ruling out trivializations. The Cheeger energy is defined from slopes of bounded Lipschitz functions and never through . Upper regularity is Definition 3.13 with a dense approximating set, not the identity .
Infrastructure. A complete development needs carré du champ calculus for strongly local forms (chain rule, (2.9), (2.10)), the Hopf–Lax semigroup on metric spaces, relaxation and minimal weak gradients, and the midpoint characterization of length spaces. Mathlib has none of these, and all of them can be reused beyond this mission. Contributions of any of these pieces, and proofs of individual milestones, are welcome.
Curvature bounds on a smooth Riemannian manifold control diffusion and the behavior of probability measures. Metric measure spaces extend these questions to limits that need not be smooth. A useful curvature condition must continue to hold when a sequence of spaces converges. Ambrosio, Gigli, and Savaré prove that their analytic Bakry–Émery curvature-dimension condition has this stability property for Riemannian energy measure spaces under Sturm–Gromov–Hausdorff convergence Ambrosio–Gigli–Savaré, Theorem 5.8. The result connects a condition stated through heat flow and Dirichlet forms with convergence stated through distances between probability measures.
The article's §5.2 first defines the convergence of spaces and of functions living in different spaces, then states the stability theorem. This order matters: the measure changes with the space, so ordinary convergence of functions on one fixed measured space cannot express the claim Ambrosio–Gigli–Savaré, Definitions 5.4 and 5.6.
A metric measure space consists of a complete separable metric space and a measure . The class contains probability measures with finite second moment. The squared Wasserstein distance is the infimum of the mean squared transport cost over couplings of and .
A sequence Sturm–Gromov–Hausdorff converges to when there is a complete separable ambient metric space and distance-preserving embeddings , including , such that . The embeddings need not be onto. This definition compares measures on different spaces after placing them in one ambient space; it does not assume that the original spaces coincide Ambrosio–Gigli–Savaré, Definition 5.4.
An energy measure space has a strongly local Dirichlet form , its associated heat flow , a carré du champ , and an intrinsic distance agreeing with . The Cheeger energy is the relaxed integral of one half the squared local slope. A Riemannian energy measure space also has the upper-regularity and continuous-representative properties of Definition 3.16. The paper writes in this situation Ambrosio–Gigli–Savaré, Definitions 3.6 and 3.16 and Theorem 3.14.
The Bakry–Émery condition bounds a second-order expression involving the heat flow, the carré du champ, curvature parameter , and dimension parameter . The formalization uses the paper's weak distributional form (2.33), writing ; represents . This is the same and for every source space and for the limit Ambrosio–Gigli–Savaré, Definition 2.4 and (2.33).
Remark 5.5 asserts that the Cheeger energy is invariant under an isometric embedding. Lemma 5.7 supplies two criteria (squared norms, or entropies of bounded densities) for convergence of scalar functions across changing measures and shows that continuous maps of linear growth preserve this convergence. Lemma 5.9 says that, in the RCD setting, both heat-flow outputs and their generators converge. These are the mission's formal milestones Ambrosio–Gigli–Savaré, pp. 63–66.
For Riemannian energy measure spaces with and , Theorem 5.8 asks for
The goal includes the assertion that the limit energy is a Dirichlet form; quadraticity is part of the conclusion. It covers finite and with the same statement Ambrosio–Gigli–Savaré, Theorem 5.8.
The theorem permits analytic curvature-dimension bounds to survive convergence even when the carrier spaces, measures, and spaces vary. Without a stability statement, a bound verified separately on approximating spaces would give no such bound for their metric measure limit. The theorem also ensures that the limit Cheeger energy retains the quadratic structure required for the Riemannian theory Ambrosio–Gigli–Savaré, Theorem 5.8 and its proof.
The result is proved in the cited paper. The remaining work here is a machine-checked development of its definitions and proof, including the convergence of heat flows and generator terms across changing measures. The statements in this proposal are proof targets; they are not presented as already machine-checked. The definitions of SGH convergence and graph-law convergence can also support other stability questions for metric measure spaces.
The difficulty is that each acts on a different , while is an inequality involving the semigroup, its generator, and integrals against . Convergence of the underlying measures alone does not imply convergence of those functions or of their squared terms. In particular, pointwise convergence on a common carrier is not even a statement available before choosing embeddings and representatives. The paper's separate notion of function convergence addresses this gap Ambrosio–Gigli–Savaré, Definitions 5.4 and 5.6 and Lemma 5.9.
Lean keeps the spaces indexed by : Xn n, m n, E n, and P n. The goal uses SGH convergence as an existential ambient realization, rather than assuming the paper's common-space reduction (5.10). The source heat flows and the truncation profile are named by their defining properties; they are the paper's determined objects. The limit heat flow is not assumed to exist: the conclusion is stated for every family satisfying the heat-flow characterization of . Functions represent classes, and the common Setting layer records almost-everywhere invariance. The measurable spaces are Borel; the paper's completed measurable structures are represented through measurable versions and almost-everywhere relations.
The formal goal assumes that has full support on . Definition 3.6 requires this, while §5.2 explicitly warns that the ambient SGH limit may fail to be fully supported. The full-support condition makes the theorem refer to the intended limit carrier. The goal does not assume that the limit already is a Riemannian energy measure space or satisfies .
Function convergence uses graph laws on . The chosen product metric is Mathlib's max metric; any fixed finite product metric yields the same convergence in this setting. The squared Wasserstein distance is extended nonnegative, so a missing finite coupling does not turn into a false real value. The limit energy is defined as , with no free energy parameter. Measurable representatives are explicit when forming pushforwards. Lemma 5.9 is stated on a common, fully supported RCD carrier; this narrows its ambient application and is recorded for review. Contributions to the Cheeger-energy invariance, changing-measure function convergence, heat-flow stability, and final BE passage are all within scope.
Textbook quantum theory starts from postulates about Hilbert spaces, density matrices and completely positive maps, none of which has an evident operational meaning. A long line of work, from Birkhoff–von Neumann quantum logic through Ludwig, Hardy (quant-ph/0101012), Dakić–Brukner and Masanes–Müller (arXiv:1004.1483), asks whether the formalism can instead be derived from principles that speak only about preparations, measurements and their statistics.
Chiribella, D'Ariano and Perinotti (Phys. Rev. A 84, 012311 (2011), arXiv:1011.6451) give such a derivation for finite-dimensional quantum theory. Five axioms (causality, perfect distinguishability, ideal compression, local distinguishability, pure conditioning) describe a broad class of information-processing theories containing classical theory; one further postulate, purification, singles out quantum theory. The paper builds on the framework of operational-probabilistic theories of the same authors (Phys. Rev. A 81, 062348 (2010)).
An operational-probabilistic theory (OPT) has systems , a composite system for every pair, and, for each pair , tests: finite families of transformations from to . Tests with no input are preparation tests (families of states ), tests with no output are observation tests (families of effects ). Composing a preparation test with an observation test yields a joint probability distribution , and parallel composition multiplies probabilities. After identifying objects with the same statistics, the states of span a real vector space of finite dimension , effects are linear functionals on it, and transformations are linear maps. denotes the normalized (deterministic) states.
Standard notions are then defined operationally: refinement and coarse-graining, pure states and atomic effects/transformations (only trivial refinements), completely mixed states (refined by every state), reversible transformations, the face of a state, and perfectly distinguishable families (there is an observation test with ). The informational dimension is the common size of all maximal perfectly distinguishable families of pure states.
For every theory satisfying the six principles and every system , there is a real-linear isomorphism with
and , the size of every maximal family of perfectly distinguishable pure states. In words: the normalized states of every system are exactly the density matrices on .
In the order of the paper: Theorem 6 (maximal distinguishable sets and completely mixed states), Lemma 16 (atomicity of composition), Theorem 8 (pure state / atomic effect duality), Lemma 32 (the informational dimension is well defined), Corollary 15 (), Theorem 9 with Lemma 10 (the invariant state is the uniform mixture of any maximal set), Theorem 10 (spectral decomposition), Theorem 12 (), Theorem 13 (the Bloch ball and for ), Theorem 16 (superposition principle).
The result shows that, inside a class of theories defined by operational requirements, the density-matrix formalism is forced by purification. The intermediate results are of independent interest: an operational spectral theorem (Theorem 10), the dimension formula (Theorem 12) that replaces Hardy's "simplicity" axiom, and the derivation of the qubit Bloch ball (Theorem 13). Corollary 52 of the paper upgrades the goal to transformations (all completely positive trace-non-increasing maps), using a cited result of the 2010 framework paper; it is not part of this mission's goal.
The paper is a physics article with diagrammatic proofs and several steps delegated to the earlier framework paper. A formalization makes every framework assumption explicit and checks the derivation end to end; no machine-checked development of operational-probabilistic theories is known to the proposer.
The derivation never assumes a Hilbert space, so the matrix representation must be built from the principles: first qubits (via the Bloch ball classification, which uses the classification of compact subgroups of ), then projections on faces, the superposition principle and finally a coordinate system on -level systems in which positivity of all states can be checked. Each step relies on many operational lemmas (Choi isomorphism, teleportation, uniqueness of purification up to channels) that in the paper are proved diagrammatically or cited.
Lean namespace InfoDerivQT. A theory is a structure OPT already in quotiented, finite-dimensional form: is modelled as , effects as linear functionals, transformations as linear maps, and tests as families indexed by finite types. The framework records the circuit rules used throughout the paper: the probability rule, product rule, coarse-graining, identity, sequential composition with classical control, classical randomization, rescaled preparations, parallel composition of all kinds of tests, conditioning on one side of a bipartite state, swap and associator, closedness of the state set, and spanning of states and effects. Because transformations are identified with their action on single-system states, this encoding is faithful in the presence of local distinguishability (Eq. (5) of the paper), which every target assumes. The trivial system is not modelled. The six principles are bundled in OPT.SatisfiesPrinciples; quantum theory is a model, so the hypothesis is satisfiable. The choice of framework axioms is the main point for audit: a missing circuit rule could make a target false, an extra one could exclude intended theories.
Contributions welcome: proofs of the milestones, a formal check that finite-dimensional quantum theory is a model of SatisfiesPrinciples, and the Choi isomorphism and teleportation lemmas of Secs. IV and IX as further milestones.
In an -player stochastic differential game each player controls the drift of its own diffusion and is rewarded through a running and a terminal payoff that depend on its own state and on the empirical distribution of all states. A player's strategy can be closed-loop (path-dependent), reacting to the whole observed history of all states, or Markovian (in the engineering literature, "feedback perfect state"), reacting only to the current states and the time. The two lead to two equilibrium notions. A Markovian equilibrium is the object produced by the classical PDE approach (a Nash system of parabolic equations), and it is the natural object for mean field game approximations. A closed-loop equilibrium is the economically more convincing notion, because it rules out profitable deviations to any strategy a player could actually implement.
D. Lacker's paper On the convergence of closed-loop Nash equilibria to the mean field game limit (arXiv:1808.02745v1, 2018; Ann. Appl. Probab. 30(4), 2020, doi:10.1214/19-AAP1541) proves limit theorems for closed-loop equilibria as . Its Proposition 2.2, the subject of this mission, shows that under a convexity condition going back to Filippov and Roxin, the Markovian equilibria form a subset of the closed-loop ones. The limit theorems for closed-loop equilibria then apply to Markovian ones as well.
Fix a horizon , a dimension , a number of players , a control set in a real normed space, an initial law on , and functions
Assumption A: is compact and convex, and are bounded and jointly continuous. Assumption B: for each the set is convex; this holds, for instance, if is affine and concave in .
Write . An admissible control is a Borel, non-anticipative map ; the set of these is . A Markovian control is a Borel map , used as ; the set is . A profile drives the states
with independent Brownian motions and i.i.d. initial states of law . Player receives
For , a closed-loop -Nash equilibrium is a profile in with for all ; a Markovian -Nash equilibrium is a profile in with the same inequality, the supremum taken over only.
Under Assumptions A and B, for every ,
The proposition makes the two equilibrium notions comparable: since a priori a Markovian equilibrium is tested only against Markovian deviations, there is no reason for it to survive path-dependent deviations, and without convexity it need not. Under Assumption B, every result about closed-loop equilibria (in the paper: tightness of the empirical measure flows and identification of their limits as weak mean field equilibria, Theorem 2.7) covers Markovian equilibria too, and in particular those built from classical solutions of the Nash system.
The result is proved in the paper; nothing in this mission is open mathematics. To our knowledge none of it is formalized. The mission produces a machine-checked formulation of the -player game with weak solutions, both equilibrium notions, and the comparison; the Markovian projection theorem is a general result of stochastic analysis, used well beyond game theory (local volatility calibration, mimicking theorems), with no formal proof in any proof assistant that we know of.
The obvious attempt is to replace a closed-loop deviation by its "Markovian average", the conditional expectation of the control given the current state. This fails twice. First, and are nonlinear in the control, so averaging the control changes both drift and reward; the convexity of is what allows a single Markovian control to reproduce the conditional drift exactly while not losing reward, and producing it requires a measurable selection that is jointly measurable in time and state. Second, replacing the drift changes the law of the whole state process, so it is not clear that the payoff can be compared at all. Only the one-dimensional time marginals are preserved, and proving that requires the Markovian projection theorem, whose proof rests on uniqueness for a Fokker–Planck equation with merely bounded measurable drift. Neither ingredient is in Mathlib, which has no stochastic differential equations, Girsanov theorem, or Itô formula.
NSol) bundles its own probability space (in Type), filtration, independent Brownian motions jointly forming an -dimensional -Brownian motion, adapted continuous states, i.i.d. initial states of law independent of the noise, and the empirical flow. is evaluated on a given solution, and each -Nash condition is required for every solution of the equilibrium profile and every solution of the deviated profile. This equals the paper's definition because solutions exist and are unique in law (Girsanov, p. 6); proving the goal therefore requires constructing solutions where needed.EthierKurtz.IsStandardBrownian on , made an -Brownian motion by adaptedness and independent increments; is EthierKurtz.SDEState d.NeZero n), , , measurability of every process and control, and the completed filtration of for the strong solution in Theorem 2.14 (platform EthierKurtz.completedBrownianPast). Coefficients and controls take a real time argument, constrained only on .Needed infrastructure: weak solutions of SDEs with bounded drift (Girsanov), strong existence for bounded measurable drift (Veretennikov), Fokker–Planck uniqueness, measurable selection, and disintegration of measures depending measurably on a parameter. The Markovian projection theorem and the Girsanov existence of -player solutions are reusable beyond this mission. Contributions toward any of these are welcome.
Many large convex problems in signal processing, networking and statistics have a separable objective coupled by linear constraints: blocks of variables, each with its own nonsmooth regularizer and its own feasible set, tied together by . The alternating direction method of multipliers (ADMM) is the standard tool for such problems when . For the direct extension of ADMM can diverge, as shown by Chen, He, Ye and Yuan (2016), and convergence guarantees for multi-block variants typically require strong convexity or extra correction steps.
Hong, Chang, Wang, Razaviyayn, Ma and Luo propose the block successive upper-bound minimization method of multipliers (BSUM-M), which updates each primal block by minimizing a local upper bound of the augmented Lagrangian, followed by a dual gradient step, and prove that it converges for any number of blocks without strong convexity of the objective. They also analyse a randomized version, RBSUM-M, in which each iteration updates a single randomly chosen block, primal or dual. Randomized block selection matters when data or computation are distributed and not every block is available at every step. This mission formalizes the randomized half of their main theorem; the cyclic half is a separate mission.
Let with , and consider
The standing assumptions (Assumption A) are: with strictly convex and continuously differentiable; with nonnegative weights; each is a compact polyhedron; the problem is feasible and its primal and dual optimal values are attained.
For the augmented Lagrangian and augmented dual function are
and is the set of minimizers of over . The method works with approximation functions (Assumption B): majorizes in block , touches it with matching gradient at , is strongly convex with modulus and has an -Lipschitz gradient.
RBSUM-M. Fix probabilities summing to 1. At iteration draw with probability . If , take a dual step ; otherwise replace block by
leaving the other blocks and unchanged. The analysis uses the block steps (the minimizer above, computed for every ), the dual step , the gaps , , and the proximal gradient . The error bound with constant is for all and .
Under Assumptions A and B and the error bound, if the stepsizes are either constant and sufficiently small, or satisfy , , then with probability 1
where is the point of nearest to , and every limit point of is a primal and dual optimal pair. The threshold for "sufficiently small" is existential and depends only on the problem data, the , the error-bound constant and .
In the order of the paper: Lemma 2.1 (differentiability of , , the -Lipschitz bound); Lemma 2.3(2) (expected decrease of ); Lemma 2.4(2) (proximal gradient bounded by the block and dual steps); Lemmas 2.5(2) and 2.6(2) (expected change of the dual and primal gaps); and from the proof of Theorem 2.1, (2.24)–(2.25) (expected change of ), (2.28) (constraint violation), (2.29) (the descent estimate with explicit coefficients) and (2.40) (one-step change of ).
The result shows that a randomized, single-block-per-iteration primal-dual method converges almost surely to primal-dual optimal solutions of a multi-block linearly constrained problem, under assumptions that allow a rank-deficient , nonsmooth group-sparse regularizers, and inexact (majorized) block subproblems. The potential function and the way the error bound converts it into a supermartingale estimate are reused in later analyses of multi-block and randomized ADMM-type methods.
The result is proved in the paper; to our knowledge it has no machine-checked proof. Formalizing it produces a checked convergence proof for a randomized augmented-Lagrangian method, a reusable formal treatment of the augmented dual function of a convex program with compact polyhedral constraints, and a precise record of the conventions under which the published statements hold (see the scope section).
The obvious route is to show that decreases. It does not: a dual step increases by , and without strong convexity there is no direct control of the distance to the solution set. The argument has to combine the primal and dual gaps into one potential, bound the residual term through an error bound that holds without strong convexity, and then pass from a conditional-expectation inequality to almost-sure convergence. Under diminishing stepsizes the supermartingale argument only yields , and upgrading this to a limit needs a separate pathwise argument on how fast can move.
Blocks are EuclideanSpace ℝ (Fin (n k)) and the full vector lives in PiLp 2, so norms are Euclidean. is real-valued on all of . The augmented dual function is (the page's (1.9) prints an unconstrained minimum of plus penalty; the constrained reading is the one Lemma 2.1 and (2.19) use). The prox in the proximal gradient includes the constraint set , which is what the proof of Lemma 2.4 needs; the error bound of Lemma 2.2 is a hypothesis of the goal, in its global form on , and is not derived. Lemma 2.2 itself is not part of the mission.
Conditional expectations given are written as the explicit average over the random index, at every state; this is because the index drawn at iteration is independent of . The goal is stated on an arbitrary probability space carrying mutually independent indices with law , for every run from a deterministic start , . Iterations are indexed from as on the page.
Two printed statements are corrected and labelled in their items: Lemma 2.1 asserts (not each ) constant over , and Lemma 2.6(2) uses where the page prints . Statements are not trivialized: the setting is satisfiable (for instance , , , , , ), the stepsize threshold precedes the probability space and the run, and the solution sets entering distances are nonempty under Assumption A. A formalization in which the error bound or the gap bounds are assumed in a form that already contains the conclusion would not count.
A complete development needs: Danskin-type differentiability of and the -smoothness of the augmented dual; first-order optimality and nonexpansiveness of the prox of ; and the Robbins–Siegmund almost-supermartingale convergence theorem in Mathlib's conditional expectation framework, together with a bridge from the explicit index average to condExp. The last two are reusable well beyond this mission. Contributions to any of the milestones, or to these general lemmas, are welcome.
Theorem numbers, equation numbers and page numbers in this mission refer to arXiv:1401.7079v1 (printed page = PDF page − 1); the journal version renumbers them.
In an optimal stopping problem the value function and the gain function agree on the stopping set , and on the continuation set . The smooth fit principle says that, at the boundary between them, meets with matching first derivatives. Smooth fit is one of the boundary conditions in the free-boundary problems that characterise optimal stopping boundaries. It is behind the integral equations for the early-exercise boundary of the American put and for many problems in sequential analysis and finance (Peskir & Shiryaev, 2006). On a finite horizon the value depends on the remaining time, and continuity of the time derivative across is the step that justifies the local time-space calculus applied to (Peskir, 2005).
Before De Angelis & Peskir (2020) such continuity results were proved problem by problem, or under sign conditions that the main examples do not satisfy: on the stopping set and globally, which fails for the American put. Their paper gives two general results. Theorem 8 covers the space derivative, and Theorem 15, the subject of this mission, covers the time derivative on a finite horizon. Both are stated for a strong Markov process realised as a stochastic flow, and both rest on probabilistic regularity of the boundary.
Fix a horizon and . The process is the time-space process . Its first coordinate is time, and is a stochastic flow on a probability space with a right-continuous filtration , adapted to it, with . Its paths are right-continuous with left limits, it is left-continuous over stopping times, and it is strong Markov. The flow is continuous in the space variable if, outside one null set, is continuous for every .
Given continuous functions , and of , write . The value function is
over stopping times bounded by the remaining time . The sets are and inside , and . The problem is well posed if the expected payoffs are integrable and the first entry time into is optimal.
The first hitting time of a set is . A point is probabilistically regular for if . The generator (2.14) acts in the space variable, with diffusion matrix , drift , killing rate and jump measure . Its coefficient formula is tied to the flow by the right derivative at zero of the killed spatial semigroup applied to . The function appears in the hypotheses.
Assume well-posedness, (5.9) ( continuous on and on ), (5.10) () and (5.11) (Lipschitz continuity of and in , uniformly in ), and a continuous flow. Assume the local conditions (5.12)–(5.13) and probabilistic regularity for at every . Then
The result. Theorem 15 turns a probabilistic property of the boundary, which can be checked through sample-path arguments, into the analytic smooth-fit condition in time. Continuity of across is the hypothesis that the change-of-variable formula with local time on curves and surfaces requires. That formula yields the free-boundary integral equations for optimal stopping boundaries. The theorem needs no sign condition on or and no strong Feller property. The time-space process is never strong Feller, which is exactly why the earlier strong Feller route to boundary regularity does not apply here.
Formalizing it. The result is proved in the paper; nothing here is open mathematics. As far as is known no part of it has been machine-checked. Mathlib has stopping times and conditional expectation, but no stochastic flows, no generators of jump diffusions and no optimal stopping in continuous time. A complete development formalizes the proof on pp. 20–23 together with the upper semicontinuity of hitting times of open sets (Lemma 4 and Corollary 6 of the paper, posed in the companion mission on the space derivative).
The infinite-horizon argument (Theorem 13, via Theorem 8) perturbs the starting point and reuses the optimal stopping time of the unperturbed problem. On a finite horizon this fails in the time variable. Shifting the start from to shortens the remaining horizon, so the stopping time optimal for is no longer admissible for . A first-order comparison of payoffs therefore cannot be used. The proof truncates the stopping time and controls the truncated part, which is the role of the identity (5.12) and of the window in (5.13). The convergence of the optimal stopping times has to come from regularity of for the interior and continuity of the flow, not from the strong Feller property.
EuclideanSpace ℝ (Fin m) with . Time is ℝ≥0. Points of the time-space domain are pairs in ℝ × EuclideanSpace ℝ (Fin m), and is Set.Icc 0 T ×ˢ univ.WithTop ℝ≥0) with , and are capped by the horizon.ContinuousOn on .Contributions welcome: the hitting-time lemmas (upper semicontinuity of under a continuous flow), dominated-convergence lemmas for the truncated stopping times, and the two halves (5.17) and (5.20).
An optimal stopping rule chooses when to end a stochastic process in order to collect a terminal reward, possibly after earning or paying a running reward. The resulting value function often solves a free-boundary problem: the state space splits into a region where stopping is optimal and one where continuing is better. Smoothness inside either region does not by itself say what happens where the regions meet. This mission concerns the global first spatial derivative of that value function at the optimal stopping boundary.
De Angelis and Peskir proved that a probabilistic condition on the boundary, together with regularity of the process as a spatial flow and explicit integrability bounds, gives continuous differentiability of the value function across the boundary. Their result applies to standard Markov processes with right-continuous paths and left limits, including jump processes; it is not restricted to diffusions or to a constant discount rate. The source is De Angelis and Peskir, arXiv:1812.04564v2, Theorem 8.
Let , let , and let be a stochastic flow: the same probability space carries a path starting from every state . Time is nonnegative. One right-continuous filtration makes every path adapted and is used for every stopping rule. The process is strong Markov, has right-continuous paths with left limits, is left continuous over stopping times, and starts from . Expectations and probabilities written and in the paper are the expectation and probability of the flow under one measure .
The continuous data are a nonnegative discount rate , a terminal reward , and a running reward . The discount accumulated along the path from is . For every finite-valued stopping time of the common filtration, define
This is the infinite-horizon problem (2.1). It is well posed here when all admissible payoffs are integrable and the first entry time into the stopping set is an almost surely finite optimal stopping time. These conditions ensure that is a real, attained supremum rather than a default value of Lean's real supremum or integral. Define the stopping set , the continuation set , and the boundary relevant to the theorem as . For a state set , the first entry time is and the first strictly positive hitting time is . Both may be infinite.
A boundary point is probabilistically regular for if . It is Green regular for when as through , for every . The paper obtains Green regularity by either strong Feller continuity with probabilistic regularity for , or spatial continuity of the flow with probabilistic regularity for . Lemma 1 and Corollaries 2–3 give the first route; Lemma 4 and Corollaries 5–6 give the second. All six statements use an arbitrary closed , as in Section 3 of the source. Source: §§2–3, pp. 3–11.
The milestone results first establish the two boundary regularity routes. In particular, approaching through , the first route gives in probability; the second gives and almost surely. Equations (4.16) and (4.19) then bound, respectively, the lower and upper limits of each coordinate derivative by . The pointwise part of Theorem 8 concludes
The mission goal is the final sentence of Theorem 8. If the theorem's local hypotheses hold at every , then
The hypotheses include the discounted generator representation (2.14) from the problem setup, continuity and interior regularity of , global regularity of , one positive Lipschitz constant for both and , a spatial flow, the four local bounds (4.4)–(4.7) with one radius at each boundary point, and one of the two probabilistic regularity alternatives. The goal retains all dimensions , all nonnegative continuous discount rates, and the source's full class of standard Markov flows. Source: §2.5 and Theorem 8, pp. 7, 11–12.
The conclusion identifies the derivative of the value function on both sides of the stopping boundary. It strengthens a derivative match along a single direction or a chosen sequence into continuous differentiability on the whole state space. This is relevant to free-boundary formulations of optimal stopping, where interior regularity can be available from a Dirichlet or Poisson problem while boundary regularity remains the missing step. The authors describe that distinction in their discussion of smooth fit and global differentiability. Source: §2.5, p. 8.
The mathematical theorem is proved in the 2020 paper. In this mission, the definitions and statements compile as Lean declarations, while the theorem proofs remain to be formalized. A complete development would supply reusable arguments about hitting times, semicontinuity of hitting probabilities, stochastic flows, and limits of derivatives near a stopping boundary. Those components would also support the paper's finite-horizon spatial and temporal results.
The value is a supremum over stopping rules. Differentiating the reward for a fixed stopping time does not automatically differentiate that supremum, because the optimal time depends on the initial state. Near the boundary, even continuity of the value does not control the duration of the optimal rule from neighboring states. The paper's probabilistic regularity conditions address that duration, while (4.4)–(4.7) provide the integrability needed to pass to derivative limits. A direct appeal to interior differentiability leaves the boundary itself untreated. Source: §§3–4.1, pp. 9–15.
The state space is EuclideanSpace ℝ (Fin d) with ; Fin d indices are the paper's coordinates shifted by one. Balls are open Euclidean balls. Time is , and the entry and hitting times live in so an unattained hit has its intended value. The flow is the process; no separate family of measures is introduced. One common filtration is used for all initial states and is right-continuous. Its finite stopping times are the full admissible class, not only hitting times.
The value uses Bochner expectations and real Lebesgue time integrals. Well-posedness records integrability for every admissible payoff and optimality and almost sure finiteness of . The generator clause acts on smooth functions in the domain of the discounted transition semigroup; it retains the paper's diffusion, drift, killing, and jump terms. The boundary is , and approach through continuation points is expressed by the within-set neighborhood filter. Pointwise continuous differentiability means a Fréchet derivative at equal to and convergence of along ; the goal uses global ContDiff. The local bounds retain all independently indexed starting states and coordinates. Their uncountable suprema are represented by integrable common majorants, with timewise measurable envelopes for the suprema inside time integrals. This convention excludes default integral values from nonmeasurable or nonintegrable expressions.
A formalization restricted to Brownian motion, one dimension, zero or constant discount, continuous paths, bounded rewards, or only one boundary regularity branch would state a different theorem. Contributions toward measurable hitting-time events, the two Section 3 regularity chains, the envelope bounds, and the derivative comparison are welcome.
Optimal portfolio liquidation asks how a trader should unwind a position of shares over a horizon when trading moves prices. Since Almgren and Chriss (2001) the standard model charges a quadratic cost for trading at rate (temporary impact) and a risk penalty on the open position, and imposes the liquidation constraint . When many traders liquidate at once, each one's costs also depend on the others' aggregate trading rate through a permanent impact term . Fu, Graewe, Horst and Popier (arXiv:1804.04911) model this as a mean field game (MFG) with common noise and prove that, under a weak-interaction condition, the game has a unique equilibrium.
The liquidation constraint makes the problem singular: the value function blows up at , and the equilibrium is described by a forward-backward system whose decoupling field satisfies a Riccati BSDE with terminal value . A natural question is whether the constraint can be replaced by a finite penalty on the unliquidated position, a non-singular problem of the type studied in the MFG literature, and whether the penalized equilibria approach the constrained one as . Section 4 of the paper answers this at the level of values. In the single-agent case, singular terminal conditions of this type were studied by Ankirchner, Jeanblanc and Kruse (SIAM J. Control Optim., 2014) and Graewe, Horst and Séré (Stochastic Process. Appl., 2018), references [3] and [28] of the paper.
Fix , an -dimensional Brownian motion whose first coordinate is common noise, and an initial position independent of . Let be the filtration of and that of , both augmented. The coefficients are bounded, nonnegative, -progressive processes, with and bounded below by positive constants. Write , , for the essential supremum of and the essential infima of and , for the essential supremum of , and . Assumption 2.3 adds the weak-interaction condition: some satisfies and .
Given an aggregate rate , a trading rate yields the position . The constrained problem minimizes
over with ; its value is . The penalized problem (4.1) drops the constraint and minimizes
over all , with value . An equilibrium is a fixed point .
The constrained equilibrium is given by the FBSDE (2.3), , , , , decoupled as where
The penalized equilibria are given by the FBSDE (4.2) with , decoupled by , the solution of the same Riccati BSDE with . The solutions live in weighted spaces: with norm , and the penalized analogue with weight . Assumption 4.1 requires a constant with for all , almost surely.
Under Assumptions 2.3 and 4.1, with the constrained equilibrium and the penalized ones,
The result is a consistency statement between two models of liquidation. Penalized models are what a numerical scheme or a standard MFG solver can handle, since their FBSDEs have finite terminal data. Theorem 4.6 says that equilibrium values computed with a large penalty approximate the value of the hard-constrained game, and Lemma 4.5 says the same for positions and trading rates. Without it, a penalized model would be an unrelated object rather than an approximation of the constrained one.
The result is proved in the paper; it is not formalized anywhere. A machine-checked development would need, beyond the paper, the theory of quadratic BSDEs with finite and singular terminal values, conditional mean-field FBSDEs with common noise, and conditional essential infima of control problems. The milestones isolate reusable pieces: the monotone approximation of a singular Riccati BSDE (Lemma A.3) and uniform estimates in -dependent weighted spaces (Lemma 4.4).
The obvious argument compares the two problems control by control: the constrained optimizer is admissible for the penalized problem, so up to the change of . The reverse inequality is where it fails. The penalized optimizer leaves a residual position , and its cost has to be compared with the singular one, whose weight explodes at . Controlling this requires estimates uniform in in spaces whose weights degenerate as , and the bare exponent of the constrained problem is not enough to make the boundary terms vanish. Assumption 4.1, which upgrades the state to , is what closes the gap. In addition, the aggregate rate changes with , so both the controls and the cost functional move at once.
Time is ; processes are real-valued functions of ; is the -dimensional with coordinate the common noise. Stochastic integrals and BSDEs come from the published definition Peng1990.SMP.Stochastic. BSDEs on are imposed on every , ; is a.s. Conditional expectations inside drivers are -progressive versions of integrable processes. Weighted norms are computed in . The explicit readings are:
A trivializing formalization would quantify over all solutions of the penalized MFG (claiming a uniqueness the paper does not state) or define by a pointwise infimum over all controls (which is or junk); both are ruled out above. Contributions toward BSDE comparison principles and quadratic BSDE well-posedness on this stochastic-integral layer are welcome and reusable.
A trained feed-forward neural network with ReLU activations, , is a piecewise linear function of its input. Many tasks ask for an optimization over such a network with its weights held fixed: verifying that no small perturbation of an image changes its classification, finding adversarial examples, or embedding a learned model of demand or cost inside a decision problem ("predict, then optimize"). The standard way to solve such problems exactly is mixed-integer programming (MIP): each neuron is written as a small set of linear constraints with one binary variable, and the network is the composition of these neuron formulations. How strong each neuron formulation is decides how fast branch-and-bound can close the gap.
The formulation used in the literature up to 2018 is the big-M formulation. It is valid but weak. This mission formalizes the main result of Anderson, Huchette, Tjandraatmadja and Vielma, IPCO 2019 extended abstract (arXiv:1811.08359v2), which gives the strongest possible formulation of a single ReLU neuron that uses the original variables and one binary variable only.
Timeline. Big-M formulations of ReLU networks were used by several groups in 2017–2018 for verification and adversarial analysis (see §1.2 of the paper). Balas's disjunctive programming (1985, 1998) and the multiple choice formulation of piecewise linear functions (Vielma and Nemhauser, Math. Program. 2011) give an ideal formulation of the neuron that needs a copy of the input variables. Anderson et al. (2019) project out that copy and obtain the formulation (6) below; a longer journal version (Math. Program. 2020, with W. Ma) develops the analysis further, including interactions between neurons.
Fix , a weight vector , a bias , and bounds with for every . The neuron computes for the affine function on the box . Its graph is
The sign-adjusted bounds are , when , and , when . Then and are the maximum and minimum of on , and . Strict activity means : the neuron is neither always off nor always on. The paper assumes throughout that and that strict activity holds.
A set of points with , read together with the constraint , is a formulation of the graph if lies on the graph exactly when for some ; is then its LP relaxation. The formulation is ideal if every extreme point of has .
The big-M formulation (3) is , , , . The formulation of Proposition 1 is
Proposition 1 says that the convex hull of the graph, lifted with one binary variable, is described by (6a), (6b) and the bounds, with no auxiliary continuous variables. Optimizing a linear function over the LP relaxation of (6) therefore gives the tightest convex relaxation available for a single neuron, and Proposition 3 gives a separation routine linear in , so the exponential family can be added on demand to a big-M model. The paper's experiments (§3, not formalized) report that separating over (6b) solves smaller MNIST verification instances faster than Gurobi's default cut generation by a factor of 7.
The result is proved in the paper; nothing here is open. To our knowledge none of these statements has a machine-checked proof. The work this mission asks for is the formalization of the known proof: an ideality statement for the multiple choice formulation, a Fourier–Motzkin projection carried out for an arbitrary index set with general-sign weights, and the passage from a hull identity to integrality of extreme points.
The formulation half of Proposition 1 is a short case analysis on ; the content is ideality. The obvious attempt, characterizing the extreme points of the LP relaxation of (6) directly, is impractical: the polytope is cut out by inequalities, and showing that every point with fractional is a proper convex combination of feasible points means handling all patterns of tight inequalities of (6b) at once. Ideality of the extended formulation (5) is classical and passes to its projection onto , but that only helps once the projection is known to be exactly the LP relaxation of (6): it has to be computed for an arbitrary index set, and every inequality it produces must be shown to be one of (6a), (6b), the bounds, or implied by them. Weights of both signs must be handled throughout: the page treats negative weights by a change of variables, and a formal development has to carry the sign-adjusted bounds through every step.
Inputs are Fin η → ℝ, so indices are 0-based; points are (Fin η → ℝ) × ℝ × ℝ. A formulation is encoded by its LP relaxation (with ) and the predicate " iff for some "; ideality is ∀ p ∈ Set.extremePoints ℝ R, p.2.2 = 0 ∨ p.2.2 = 1. are defined by their closed forms, and a companion theorem proves that they are the maximum and minimum. In (6b) and (7c), "" ranges over all indices outside , zero weights included. The system (7) is stated with , i.e. after undoing the page's substitution ; for it is the page's display. The LP relaxation of (5) is represented both in its lifted space and projected to , with the copies quantified existentially in the latter, and constant is scaled by in (5b) and by in (5c).
The goal carries both standing assumptions of §1.3 ( and strict activity) and nothing else. Milestones that do not need strict activity omit it, which makes them stronger. Example 2 includes the page's boundary: although its box then violates when , the example's three stated claims remain true.
Ideality is a statement about the LP relaxation, not about the set with : applied to the latter it would hold trivially, and a goal stating only that (6) is a formulation would omit the result's content. Both are ruled out by the statement of the goal.
A complete development needs: extreme points and convex hulls of polyhedra in product spaces (Mathlib), the hull of a union of two polytopes as a projection, Fourier–Motzkin elimination over an arbitrary finite index set, and finite-sum manipulations over subsets of . The Fourier–Motzkin and disjunctive-hull lemmas are reusable well beyond this mission; contributions of either are welcome, as are proofs of the companion results.
Source: the IPCO 2019 extended abstract, arXiv:1811.08359v2 (28 Feb 2019); all labels and pages refer to that version.