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?
Many problems in signal processing, machine learning and power systems have the form of a convex objective that is a sum of a smooth coupled term and nonsmooth block-separable terms, minimized subject to linear equality constraints that couple blocks of variables: basis pursuit, demand response control in smart grids, and distributed estimation are the examples of Hong, Chang, Wang, Razaviyayn, Ma, Luo. The alternating direction method of multipliers (ADMM) handles two blocks well, but for blocks the directly extended Gauss–Seidel ADMM can diverge (Chen, He, Ye, Yuan, 2016), and convergence proofs for multi-block schemes usually need strong convexity or extra correction steps.
The block successive upper-bound minimization method of multipliers (BSUM-M) is the paper's answer: each block is updated by minimizing a local upper bound of the augmented Lagrangian, which makes the subproblems simple (for instance closed-form proximal steps), and the multiplier is updated by a dual gradient step with a small or diminishing stepsize. The main theorem shows that this scheme converges to primal and dual optimal solutions for any number of blocks without strong convexity, under an error bound.
The variable is , , with the Euclidean norm . Problem (1.1) is
Under the standing Assumption A, with strictly convex and continuously differentiable and any matrix; is a mixed norm with nonnegative weights; each is a compact polyhedron and ; the problem is feasible and the dual optimal value is attained.
For , the augmented Lagrangian is , the augmented dual is , and . For , denotes the point of nearest to .
Assumption B concerns the approximation functions : each upper-bounds along block , is tight with matching gradient at , is continuous, strongly convex in with a uniform modulus , and has an -Lipschitz gradient in .
BSUM-M (1.12). From and any , for :
for in order, with the Gauss–Seidel point .
The proximal gradient is with . The error bound asks for with for all and all .
Under Assumptions A and B and the error bound, there is such that for stepsizes that are either constant with , or satisfy and , every BSUM-M run satisfies
and every limit point of is a primal and dual optimal solution. The threshold is not specified; no rate is claimed.
Lemma 2.3(1) (one sweep decreases by ), Lemma 2.5(1) (dual gap decrease), Lemma 2.6(1) (primal gap bound), Lemma 2.4(1) (the proximal gradient at is ) and Lemma 2.1 (differentiability of , , and Lipschitz continuity of on superlevel sets).
The theorem gives a convergent multi-block method of multipliers whose block subproblems may be replaced by any majorizer satisfying Assumption B, such as a linearized proximal step. It covers the cyclic Gauss–Seidel order, where the direct multi-block ADMM can fail, and it does not require strong convexity of (the matrix need not have full column rank). The paper's randomized variant (part 2 of the same theorem) is a separate mission.
The result is proved in the paper (the proof of part 1 is described as following the steps written out for part 2). It has not been machine-checked. Formalization adds a verified account of the potential-function argument for a primal-dual method with inexact block updates, and checks three printed statements that need correction (see the scope section): a formal proof settles them.
The obvious approach is to treat BSUM-M as an inexact dual gradient ascent on , but a single Gauss–Seidel sweep does not compute , so the dual step uses a gradient at the wrong point. Controlling that error requires relating the primal step length to the distance from , which fails without an error bound: is not strongly convex, need not be a singleton, and the proximal gradient can be small far from . The cyclic order adds a second gap: block is linearized at , not at . With a constant stepsize the dual ascent must not outrun the primal descent, which is where the smallness threshold enters.
Citation basis: the arXiv preprint arXiv:1401.7079v1 (28 Jan 2014); every index refers to that version, not to the revised journal version (Mathematics of Operations Research, 2020).
Representation: blocks are indexed by Fin K with ; the block space is PiLp 2 of Euclidean spaces (the Euclidean norm, not the sup norm). is real valued and on all of , which specializes the paper's extended-valued . , and are real infima and suprema over nonempty compact sets, where they are attained. The algorithm is a predicate on sequences indexed from ; argmin steps are minimality conditions, the minimizer being unique. The initial point is required to lie in . "Sufficiently small" is an existential threshold quantified before the stepsizes and the run. is the distance from to . Limit points are cluster points of the joint sequence; boundedness of is neither assumed nor concluded.
Interpretations and corrections, each labelled in the item's statement:
The error bound is a hypothesis of the goal, as in the paper, and is not derived from Assumption A: the paper's Lemma 2.2 does not hold under Assumption A alone. A formalization that makes the hypotheses unsatisfiable, drops the run's dependence on , or lets depend on the run is not this theorem. A sanity check that the hypotheses are satisfiable (a one-block instance with a constant run) is part of the drafting record.
Infrastructure needed: proximity operators of convex functions restricted to polyhedra and their nonexpansiveness; Danskin-type differentiability of a parametric minimum over a compact set; smoothness of the augmented dual; elementary convergence lemmas for nonnegative sequences with summable decrements. These pieces are reusable for other augmented Lagrangian and ADMM analyses. Proofs of the milestones are welcome independently of the goal.
On a Riemannian manifold, a lower bound together with a dimension bound can be read off from the heat flow alone. This is the Bakry–Émery curvature-dimension condition : Bochner's inequality for the iterated carré du champ. The condition makes sense for any diffusion: weighted manifolds, infinite-dimensional Gaussian spaces, and limits of manifolds where no Ricci tensor exists. For this reason it is one of the two main routes to synthetic curvature bounds, the other being the optimal-transport conditions of Lott–Villani and Sturm. Bakry–Émery 1985; Bakry–Gentil–Ledoux 2014.
Ambrosio, Gigli and Savaré prove that, on metric measure spaces, for the Cheeger energy is equivalent to the transport condition . Their first step (§2.2) is to state for an abstract Dirichlet form, in a weak form and under minimal regularity, and to show that the usual ways of writing it are equivalent. That equivalence, Corollary 2.3, is the subject of this mission. Every later section of the paper and the remaining missions of this series use one of its forms. arXiv:1209.5786v4, §2.2, pp. 14–20.
Let be a measurable space with a -additive measure .
For set
By continuity, this extends to , . The set consists of those for which has a density , the carré du champ. The iterated form is
Along the heat flow, for and , set
and . Finally , , and .
Let and . The following are equivalent:
Any of them implies . Condition (iii) is the paper's definition of (Definition 2.4).
The result. Condition (i) is the classical Bochner inequality. (iii) is the form that survives limits and is used as a definition. (iv), (v) and (vi) are pointwise estimates for the heat flow: the reverse and the local Poincaré inequalities, and the Bakry–Émery gradient bound . Section 3 of the paper uses (vi) to obtain Lipschitz regularization and to identify the intrinsic distance. Section 4 uses (iii) with to prove the property. The conclusion means that a form automatically admits a carré du champ on its whole domain, so -calculus is available without extra assumptions.
Formalizing it. The equivalences are classical for smooth diffusions with an algebra of nice functions. The paper's contribution is to prove them for an arbitrary strongly local Dirichlet form, where no such algebra is assumed. The result is proved; it is not formalized. The mission produces a Lean interface for Dirichlet forms, their heat flows, the extended and , and the six conditions. Proofs of the milestones and of the goal are open.
The obvious argument differentiates twice and reads off . That requires , and to be smooth enough for every term to be defined. For a general only the first derivative exists, as on , and only through the continuity extension (2.20). The weak forms must therefore be reached by truncation and semigroup mollification.
The passage from the integrated inequality (iv) to the existence of the density is not a computation either. It needs a Daniell-type construction of a measure from a positive functional on . The converse directions, from (iv) or (vi) back to (iii), require a second-order Taylor expansion in time of quantities whose regularity is only that of Lemma 2.1.
MemLp f 2 m, and every predicate is invariant under a.e. equality. takes values in , with off . The completion of is not modelled.Proofs of any milestone are welcome. Each proved milestone is usable independently: Lemma 2.2, (2.30) and (2.31) are real-variable statements.
A McKean–Vlasov stochastic differential equation, or distribution dependent SDE, is an SDE whose coefficients depend on the law of the solution itself:
where is the law of . Such equations describe the limit of large systems of interacting particles (mean-field limits), and they are the probabilistic side of nonlinear Fokker–Planck equations: by Itô's formula the time marginals solve a Fokker–Planck equation whose coefficients depend on .
Most existence theory for McKean–Vlasov SDEs assumes that the coefficients are continuous, often Lipschitz, in the measure argument for a Wasserstein distance. That excludes the Nemytskii-type dependence , where is the density of evaluated at the current position. This dependence appears in models of nonlinear diffusion and porous media, where the diffusion speed depends on the local concentration. V. Barbu and M. Röckner (arXiv:1808.10706, Ann. Probab. 2020) reverse the usual direction: they first solve the nonlinear Fokker–Planck equation in by nonlinear semigroup theory and then construct the SDE from its solution.
Earlier results covered the case , as recorded in Remark 4.2 of the paper. Benachour, Chassaing, Roynette and Vallois (Ann. Sc. Norm. Sup. Pisa, 1996) treated , , . Blanchard, Röckner and Russo (Ann. Probab. 38, 2010) and Barbu, Röckner and Russo (Probab. Theory Relat. Fields, 2011) treated , with irregular , the latter in the degenerate case. Barbu and Röckner (SIAM J. Math. Anal. 50, 2018) treated a maximal monotone with a drift satisfying (H3)′.
Let , , and let , . The nonlinear Fokker–Planck equation (3.1) is
Two sets of hypotheses are considered. (H1)–(H3) (nondegenerate): is , bounded, with bounded -gradient, symmetric; for some ; is bounded, , and . (H1)′–(H3)′ (degenerate): the coefficients do not depend on , and the quadratic form above is only nonnegative.
The equation is written as an evolution equation in , with the operator taken in the sense of distributions and domain . An operator is m-accretive if is onto with a contractive inverse for every . A mild solution is the uniform limit of the implicit Euler scheme . The paper calls a mild solution a weak solution of (3.1).
The SDE of the main theorem is
with measurable and .
If and satisfy (H1)–(H3) or (H1)′–(H3)′ and is a probability density, then (3.1) has a mild solution with , and for every there is a weak solution of (4.1) on with
The theorem gives weak existence for a class of distribution dependent SDEs whose coefficients are not continuous in the measure for any weak or Wasserstein topology: they are defined only on measures with a density and read that density at one point. The same construction gives a probabilistic representation of the nonlinear Fokker–Planck equation, which identifies its solutions as one-dimensional time marginals of a stochastic process and is the starting point for particle approximations.
The proofs are written in the literature. This mission formalizes them: the theory of a quasilinear elliptic operator in divergence form, the Crandall–Liggett generation theorem, and the passage from a Fokker–Planck solution to an SDE through the superposition principle. None of these is in Mathlib. The m-accretive operator layer and the superposition step are reusable well beyond this paper.
The natural first idea, a fixed point on the measure argument as in the Lipschitz McKean–Vlasov theory, fails: the map is not continuous in any topology for which the law map of an SDE is compact, and it is not even defined at measures without density. The paper therefore solves the PDE first. There the obstacle is that is nonlinear in the highest-order term and, under (H1)′–(H3)′, degenerate. Its resolvent has to be built from solutions on balls under extra smoothness. Its contraction comes from a sign-function argument that needs the monotonicity of . Approximation arguments then remove (K) and the nondegeneracy. On the SDE side, the superposition principle needs a solution of the linear equation that is weakly continuous and consists of probability measures. Mass conservation and positivity of the semigroup supply exactly that.
is EthierKurtz.SDEState d, with indices Fin d (0-based) and Lebesgue measure volume. is MeasureTheory.Lp ℝ 1 volume. Coefficients are functions , of the point and of a real number. The degenerate case uses coefficients constant in , and the operator of (3.42) is then literally . Operators are graphs X → X → Prop, and no resolvent is ever chosen. Mild solutions require that the Euler scheme can be run for all small steps, so the notion is not vacuous. Distributional derivatives are always moved onto smooth compactly supported test functions. uses the published weak derivative HunterPDE.Shared.HasWeakDeriv, and means "in and zero outside ". The SDE is the published EthierKurtz.IsWeakSDESolution on with coefficients switched off after . Its coefficients are evaluated on a jointly measurable version of the density, which must equal the law of .
Deviations from the page, all disclosed in the statements:
A trivializing formalization is ruled out: the goal asserts the existence of the mild solution as well as the SDE for every mild solution, a mild solution must come from a run of the scheme, and the constant of Lemma 3.3 is fixed before the data. Contributions are welcome at every layer, especially general results on m-accretive operators and the Crandall–Liggett theorem, estimates for quasilinear elliptic equations, and the superposition principle.
Large traders who must unwind a position by a deadline face a trade-off between trading fast, which moves prices against them, and trading slowly, which exposes them to price risk. When many traders liquidate at once, each one's execution price also depends on the aggregate selling rate of the others. Fu, Graewe, Horst and Popier (arXiv:1804.04911) model this as a mean field game (MFG) with common noise and a hard liquidation constraint: every position must be zero at the terminal time . Single-player liquidation with this constraint leads to backward equations with singular terminal values (Ankirchner, Jeanblanc and Kruse, SIAM J. Control Optim. 2014; Graewe, Horst and Séré, Stoch. Proc. Appl. 2018). Earlier MFG models of execution (Cardaliaguet and Lehalle, Math. Financ. Econ. 2018; Carmona and Lacker, Ann. Appl. Probab. 2015) allow no liquidation constraint. This mission formalizes the paper's first main result: the constrained game has a unique equilibrium under a weak-interaction condition.
Fix and a probability space carrying an -dimensional Brownian motion , where is the one-dimensional common noise, and an initial portfolio independent of . Let be the filtration of and that of , both augmented by null sets. The cost coefficients are bounded nonnegative -progressive processes (interaction), (risk aversion) and (temporary impact), with bounded away from zero.
A player's trading rate produces the position . The admissible strategies are . Given an -progressive aggregate rate , the cost is
and is its essential infimum over . A process solves the MFG (1.7) if some optimal strategy given satisfies for a.e. .
The equilibrium is described by the conditional mean-field FBSDE (2.3):
Solutions are sought in weighted spaces: if , and if is essentially bounded. The weak-interaction condition (Assumption 2.3) asks for with , and . The decoupling uses the solution of the singular Riccati BSDE , .
Under Assumption 2.3 the FBSDE (2.3) has a unique solution
is optimal, is the optimal position, is the unique solution of the MFG (1.7), and
The milestones follow the paper's proof: Fact 2.2 on the weighted spaces; Lemma A.1, existence and uniqueness of with the bounds (A.1), and ; the decay estimate (2.9), ; Lemma 2.5, an a priori estimate for the decoupled system (2.11) with homotopy parameter ; Lemma 2.6, explicit unique solvability at ; Lemma 2.7, the continuation step ; Proposition 2.8, unique solvability of (2.3) with (2.10) and a norm bound; the boundary limit (2.15); and Proposition 2.9, optimality, the equilibrium property and the value formula.
The theorem gives a complete equilibrium description for constrained liquidation with many players and stochastic, partially common market data: the equilibrium rate is the conditional expectation of the decoupled feedback rate given the common noise, and its value is explicit in terms of the Riccati solution. It is the basis of the paper's other two results, the -Nash property of the equilibrium in the -player game (Theorem 3.3) and the approximation by penalized games (Theorem 4.6), which are separate missions in this series.
The result is proved in the paper; none of it is machine-checked. A formal development would contain the first formal treatment of BSDEs with singular terminal value and of a conditional (common-noise) mean-field FBSDE. Shorter proofs of individual steps, in particular of the a priori estimate and the continuation step, are welcome.
The obvious approach fails at the terminal time. Standard FBSDE theory requires a terminal condition for ; here only is known, and is undetermined. The decoupling coefficient blows up like , so the driver of the equation for is singular, and the classical monotonicity method of Hu–Peng and Peng–Wu, applied to in unweighted spaces, does not close. The paper works instead with weighted norms that encode the rate at which and vanish at , and runs the continuation on the triple . The mean-field term is a conditional expectation given the common-noise filtration, not an expectation, so it remains random and has to be controlled pathwise in the weighted norms.
Time is ℝ≥0; processes are real valued and has coordinates, coordinate being . The Itô calculus is the published definition Peng1990.SMP.Stochastic (standard Brownian motion, , Itô integrals, BSDEs in integrated form). The explicit choices:
ℝ≥0∞.The interaction term must stay conditioned on : conditioning on makes it itself and collapses the game. The constraint and the admissibility condition cannot be dropped either. The degenerate instance satisfies all hypotheses but decouples the game.
A complete development needs the following, all reusable beyond this mission: martingale representation for the augmented filtration ; existence of progressive versions of conditional expectation processes; Doob's inequality on ; and linear BSDE solution formulas.
A trader who must sell a large position within a fixed horizon faces a trade-off: selling fast moves the price against her (temporary price impact), selling slowly exposes her to price risk. Since Almgren and Chriss, this optimal liquidation problem has been studied as a stochastic control problem with a terminal state constraint: the remaining position must be zero at the horizon . When many traders liquidate at the same time, each trader's sales also depress the price that the others receive (permanent price impact), and the problem becomes a game.
Fu, Graewe, Horst and Popier (arXiv:1804.04911v3) study this game in the mean-field limit. Their §2 constructs a mean-field equilibrium through a singular conditional mean-field FBSDE. Their §3, the subject of this mission, justifies the limit: the strategies computed from the mean field game are an approximate Nash equilibrium of the finite game with traders, with an error of order . Without such a result, the mean-field equilibrium describes a model nobody plays; with it, the equilibrium is a usable approximation for large but finite markets.
The approximation of -player games by mean field games goes back to Huang, Malhamé and Caines (2006) and Lasry and Lions (2007); Carmona and Delarue (SIAM J. Control Optim. 51, 2013) proved an -Nash property for a McKean–Vlasov class with state interaction and a rate . The present game differs in three respects: players interact through their controls (the average trading rate), there is a common noise observed by all, and each player's state must reach zero at time .
A single probability space carries a one-dimensional Brownian motion (the common noise, which drives the benchmark price and is observed by every player), for each player a -dimensional Brownian motion (the private noise), and i.i.d. initial portfolios with law ; all of these are mutually independent. Player observes , , and chooses a trading rate ; her position is and must satisfy . Given the profile , her conditional cost is
where (permanent impact), (temporary impact) and (risk aversion) are nonnegative bounded processes. Under Assumption 3.1 they are the same deterministic measurable functionals of for every player, so the players are statistically identical.
In the mean field game, the average is replaced by a process adapted to the common-noise filtration , and an equilibrium is a with for the representative player's best response . The paper characterizes it through the FBSDE (2.3),
with ; the optimal rate is . Player 's mean-field strategy comes from the same FBSDE with her own data.
For a positive function with , where , and admissible sets , there is a function , independent of and , with
The goal asserts only the shape of the bound, not its constant.
The result turns the mean-field equilibrium of §2 into a statement about the finite market: when all traders use their mean-field strategies, a trader who deviates can save at most in conditional expected cost. The error bound depends on the trader's own initial position only through , and the rate is dimension-free, in contrast with the rates of state-interaction games, because the interaction runs through the empirical mean of the controls rather than through an empirical measure.
The paper's proof of Theorem 3.3 is short but rests on several facts it states without proof: the Yamada–Watanabe-type Lemma 3.2 (whose proof is referred to other papers), the identification (3.2) of a common conditional mean, and the moment bound (3.3) attributed to Proposition 2.8. This mission makes each of these a separate machine-checkable statement. As far as we know, none of these results, nor any optimal-liquidation mean field game, has a machine-checked proof.
The estimate (3.5) is a law-of-large-numbers bound for the average of processes that are not independent: all of them depend on the common noise . The obvious argument, expanding the square and using independence, fails as stated; the cross terms vanish only conditionally on , and only once one knows that every is the same measurable functional of . That is Lemma 3.2, a Yamada–Watanabe-type statement for a singular FBSDE with a conditional mean-field term, which needs strong uniqueness of the FBSDE in the class and is the main technical step. The terminal constraint makes the backward component singular at ( blows up like ), so standard Lipschitz FBSDE theory does not apply. Finally, the deviation is constrained only through a conditional second-moment bound , and the comparison with the mean-field cost uses the optimality of (Proposition 2.9) against .
Everything is stated on one probability space carrying all players, with players indexed by ; the -player game uses players (the paper's , shifted by one). Time is and the processes are real valued. Choices made explicit:
The development reuses the Itô-calculus definitions of Peng1990.SMP.Stochastic (standard Brownian motion, , Itô integrals, BSDEs). Contributions useful beyond this mission: conditional independence given a common noise for functionals of independent inputs, a Yamada–Watanabe argument for FBSDEs, and conditional Cauchy–Schwarz bounds for time integrals. Proofs of any milestone, and of the facts from §2 they rely on, are welcome.
Many quantities in stochastic control, mathematical finance and stochastic differential games depend on the whole past of a Brownian path rather than on its current position: the price of an Asian or lookback option, the value of a control problem with delay, the solution of a non-Markovian backward stochastic differential equation (BSDE). For Markovian problems the value is a function and solves a parabolic PDE, and the theory of viscosity solutions (Crandall, Ishii and Lions) gives existence, uniqueness and stability without any smoothness. For path-dependent problems the value is a functional of the path, and the corresponding equation is a path-dependent PDE (PPDE), written with the horizontal and vertical derivatives introduced by Dupire (SSRN 1435551) and developed into a functional Itô calculus by Cont and Fournié (arXiv:1002.2446). Classical solutions of PPDEs rarely exist, so a weak notion is needed.
Timeline:
Fix and . Let be the space of continuous paths with , the canonical process, the filtration it generates, the Wiener measure and . On the pseudometric is . For , is the space of continuous paths on vanishing at , with Wiener measure , and the space of càdlàg paths on . The concatenation follows up to and then , and .
A functional on has the Dupire derivatives , the derivative under a bump of the path, and , the right derivative in time along the stopped path. is the class of functionals that agree on continuous paths with some whose derivatives , , exist and are bounded and -continuous.
The equation is the semilinear PPDE
For , and are the infimum and supremum of expectations under the Girsanov measures , . A bounded -continuous is a viscosity -subsolution if at every with for every test function that touches from above in the sense
where is a class of stopping times with open level sets. Supersolutions use and . A viscosity subsolution is an -subsolution for some , the same at every point. The candidate solution is , where solves the BSDE with terminal value and generator under .
Under Assumption 4.2 ( bounded, progressively measurable, continuous in , uniformly continuous in , Lipschitz in ; bounded and uniformly continuous) and Assumption 4.4 (an extension of to càdlàg paths, continuous and Lipschitz), for every viscosity subsolution and supersolution ,
and consequently is the unique viscosity solution with terminal condition .
In the order the proof uses them: Example 2.5 (hitting times lie in ); Proposition 5.4 ( is uniformly continuous); Theorem 4.3 ( is a viscosity solution); Lemma 5.7 (partial comparison when one of is smooth) and its form under the weaker condition (5.11); the bound of (6.3) between the Perron envelopes
Lemma 6.3 (classical solutions built from an ODE with random coefficients); and Theorem 6.1, .
Theorem 4.6 makes the definition of the paper a well-posed one: existence (Theorem 4.3) without uniqueness would allow any number of solutions, and the comparison principle is what identifies the BSDE value as the solution. It gives a path-dependent nonlinear Feynman–Kac formula, characterising non-Markovian BSDEs analytically, and it is the template on which the fully nonlinear theory, path-dependent games and non-Markovian control were later built.
The result is proved, in this paper, and the proof is not known to have been machine-checked. The formalization contributes a precise Lean account of the definitions (Dupire derivatives through extensions to càdlàg paths, the stopping-time class , Girsanov measures, the piecewise class ) and a checked proof of comparison. Pieces of independent value are a functional Itô formula for functionals, Girsanov's theorem on the canonical space, comparison for BSDEs, and optimal stopping under the nonlinear expectation .
The classical proof of comparison doubles variables and uses the Crandall–Ishii lemma, which rests on local compactness of the state space; is infinite-dimensional and not locally compact, so that route fails. The paper instead proves comparison when one side is smooth (Lemma 5.7), and then shows that the Perron envelopes and , built from piecewise-smooth super- and subsolutions, coincide. That equality needs an approximation of an arbitrary square-integrable BSDE integrand by processes that are piecewise differentiable in time with uniformly continuous derivative, so that the resulting functionals lie in (Lemmas 6.3–6.5). The partial comparison relies on optimal stopping under , which the paper treats with heuristic arguments in Remark 3.11 and references to later work, so that step will need its own development.
Time is with a fixed horizon ; paths take values in Euclidean and are constant after . is encoded as continuous paths vanishing on and as càdlàg paths constant on , so . Filtrations are the raw ones generated by the canonical process. The Wiener measure is a hypothesis on finite-dimensional laws, and is its image under the shift. The stochastic integral and BSDE solutions are those of the platform definition Peng1990.SMP.Stochastic.
Conventions and readings, all disclosed in the items:
No trivializing reading is available: the test functions are exactly the functionals satisfying (3.6), the measures exactly the Girsanov measures with , and the stopping times exactly . A test set that is too large makes sub- and supersolutions scarce and the comparison principle weaker, a test set that is too small makes them abundant and the principle false, and neither is the case here.
The source is arXiv:1109.5971v2, the IMS electronic reprint of the Annals of Probability article; its printed page numbers equal the PDF's. Lemmas 6.4 and 6.5 (the approximation of ) are part of the proof but not stated as items. Contributions welcome: the functional Itô formula, Girsanov on , BSDE comparison and stability, and the optimal stopping theory under .
Mean field games (MFGs) were introduced by Lasry and Lions (Jpn. J. Math. 2007) and by Huang, Malhamé and Caines (Commun. Inf. Syst. 2006) as limits of stochastic differential games with many symmetric players whose interaction runs through the empirical distribution of their states. An MFG is a fixed point problem for one representative player facing a flow of measures, and it is much easier to analyse than an -player game. The justification for studying it is a converse statement: a solution of the MFG should yield strategies that are nearly optimal for every player of the finite game when is large. Results of this type were proved by Huang, Malhamé and Caines for linear-quadratic models and by Carmona and Delarue (SIAM J. Control Optim. 2013) in the strong formulation with Lipschitz data.
Carmona and Lacker (arXiv:1307.1152v2; Ann. Appl. Probab. 25(3), 2015) set up MFGs in a weak formulation: controls change the law of the state through a Girsanov density instead of entering the state equation. This allows measurable, path-dependent data and controls that need only be progressively measurable. Their Theorem 4.2 is the finite-player approximation in this generality. This mission formalizes it.
Let with the sup norm, and fix a measurable weight . is the set of probability measures on with , carrying the topology : the weakest topology making continuous for every measurable with . The control set is a compact convex subset of a normed space, and carries the weak topology.
The data are a volatility , a drift , a running reward and a terminal reward , where is a whole path, and . On a probability space with an initial value and an independent Wiener process , let solve , . A control (an -valued progressive process) and a measure define a new probability with density
under which has drift . The reward is . A pair is a solution of the MFG (Definition 3.4) if some maximizes and reproduces the input: and for a.e. . Under the standing assumptions the optimal control is a function of the path, the closed-loop control.
The -player game. On a probability space with independent Wiener processes and i.i.d. initial values , let solve (the drift has no mean field term under (F.1)). The distributed controls are : each player uses only their own state. A deviation is any process that is progressively measurable for the filtration of all states (full information). A profile changes the probability to , with density the Doléans exponential of . Player then receives
with and .
Under (S), (C) and (F), there is a sequence , , such that for all , and ,
No rate is claimed; the theorem asserts only that the gain from deviating vanishes uniformly over players and deviations.
Theorem 4.2 states the sense in which an MFG solution solves the finite game. It covers path-dependent and merely measurable coefficients, interaction through the law of the controls, and full-information deviations against distributed strategies. In the paper it underlies the applications of §6: the price impact model, where Proposition 6.1 adds the rate , and the flocking model. The result is qualitative: it gives no rate in general.
The result is proved in the paper. No machine-checked proof of it or of its lemmas exists on the platform. The mission produces a formal statement layer for weak-formulation MFGs: path space, with , Girsanov densities over Itô versions, Definition 3.4, and the -player game. It then asks for the formal proof of the theorem. Missions 1 and 2 of this series (existence and uniqueness of MFG solutions) use the same model encoding. The strong-formulation result of Carmona and Delarue is a separate statement with a separate model and is not part of this mission.
The obvious route replaces by and by in and appeals to the law of large numbers. This fails for two reasons. First, the expectation is taken under , which depends on the deviation , and may depend on all players' states. The convergence therefore has to be uniform over a class of measures and requires uniform integrability of the densities. Second, is neither metrizable nor separable. Continuity in does not reduce to sequences, and dominated convergence does not hold for nets, so the almost sure convergence of empirical measures does not by itself transfer to the rewards. The remaining step asks whether full information helps the deviating player against the limiting environment. It is not a direct consequence of the optimality of in the mean field problem, which is posed over a smaller filtration.
Fin d → ℝ. is C(Set.Icc 0 T, Fin d → ℝ) with its Borel σ-field. Time is ℝ≥0; only matters.ProbabilityMeasure A with the weak topology and its Borel σ-field. Progressive measurability uses the canonical filtration on .Peng1990.SMP.Stochastic Itô layer. "Strong solution" therefore includes square integrability, and .⨆.Two readings of the goal would make it trivial, and the statement excludes both. If were allowed to depend on or , the bound would carry no content. If the deviation were evaluated under the undeviated measure instead of , the game would be a different one. (F.4) is genuine continuity, not the sequential continuity of (E).
A complete development needs:
The Girsanov and BSDE comparison results are reusable well beyond this mission and are welcome as separate contributions, as are proofs of Lemma 5.6 and of the bound.
A mean field game describes the Nash equilibria of symmetric players whose states interact only through their empirical distribution, in the limit . The law of large numbers for the equilibria — convergence of the empirical measure of the -player equilibrium to the mean field equilibrium — was proved in the diffusion setting by Cardaliaguet, Delarue, Lasry and Lions through the master equation (arXiv:1509.02505), and refined by Delarue, Lacker and Ramanan into fluctuation estimates and a central limit theorem in a companion paper (Electron. J. Probab. 2019). The next question is the size of rare deviations: the probability that the -player equilibrium empirical measure flow stays near a flow different from the mean field limit decays exponentially in , and the exponent is a rate function. Delarue, Lacker and Ramanan (arXiv:1804.08550) prove such a large deviation principle (LDP), including the case of a common noise affecting all players, for which no LDP was previously known even for McKean–Vlasov particle systems.
Timeline. Dawson and Gärtner (1987) proved the LDP for the empirical measure flows of weakly interacting diffusions without common noise, with time-independent coefficients and deterministic initial states, using the action functional adopted here. Budhiraja, Dupuis and Fischer (Ann. Probab. 2012) gave a weak-convergence proof for the empirical measure of paths. For mean field games, master-equation methods gave limit theorems, including LDPs, for finite state spaces without common noise (Cecchin–Fischer, arXiv:1704.00984; Cecchin–Pelino, arXiv:1707.01819; Bayraktar–Cohen, arXiv:1707.02648), and Lacker and Ramanan proved an LDP for static games (arXiv:1702.02113). The present paper (arXiv v1, 2018; Ann. Probab. 2020) treats diffusion-based games, with common noise.
On a filtered probability space live a -dimensional Brownian motion (the common noise), independent -dimensional Brownian motions , and i.i.d. initial states with law . The whole initial-state family is independent of the joint noise family, as specified for (6.1). Player of controls
with running cost and terminal cost . With the Hamiltonian , its minimizer and , a classical solution of the Nash system (2.6) gives the equilibrium states
The master equation (2.8) is a PDE for on involving derivatives in the measure argument. Assumption A asks for Lipschitz (with exponent for the Wasserstein metric), non-degenerate , moments of , classical solutions of the Nash systems, and a classical solution of the master equation with bounded derivatives; B or B′ controls .
The state space is : flows of probability measures with finite first moment, continuous for the 1-Wasserstein distance , with the uniform metric . The rate function uses the drift and the Dawson–Gärtner action functional
with over test functions, and off absolutely continuous paths. With common noise, the drift is shifted along the mean path: is for the drift , , and
where is the orthogonal projection onto the image of . is relative entropy.
If , A and B or B′ hold, and for every , then for open , compact and closed ,
Exponential equivalence of the Nash flows and the McKean–Vlasov particle flows (Corollary 6.1); a weak LDP for the noises and initial states (Proposition 6.15); uniform continuity of the McKean–Vlasov solution map (Lemma 6.16); the shifted action (Lemma 6.4); identification of the contracted entropy (Lemma 6.17); the weak LDP for general weakly interacting systems with common noise (Theorem 6.8) and its transfer to the Nash flows (Theorem 6.13); compactness after centering (Proposition 6.11); removal of the -relaxation on compacts, and the full LDP without common noise (Proposition 6.10); explicit forms of (Proposition 6.5, Theorem 6.6). A companion item states Theorem 3.9: without common noise, a full LDP with the good rate function .
The result quantifies how unlikely atypical equilibrium behaviour is in large games: rare macroscopic deviations of the equilibrium empirical measure flow cost , and the rate function makes explicit that the common noise moves the mean of the population for free in the directions of the image of . When the rate function has non-compact level sets, which is why the principle is weak and why the closed-set bound carries the -relaxation.
The proof transfers the LDP from the McKean–Vlasov particle system to the Nash system through the master equation, a method that applies beyond this model. Nothing in this paper is formalized: there is no large deviation principle, no Wasserstein space of measure flows, no derivative on Wasserstein space and no mean field game on the platform. A formal development produces reusable definitions (weak and full LDPs, the Dawson–Gärtner action functional, ) and checked proofs of the contraction and exponential-equivalence steps. The exponential estimate behind Corollary 6.1 (Theorem 4.3) is the companion mission's milestone and rests on estimates quoted from the companion central-limit-theorem paper.
The obvious route — exponential equivalence plus the Dawson–Gärtner LDP for the particle system — fails twice. The particle drift is time-dependent and the initial states are random, which the classical results do not cover; and with common noise there is no LDP to transfer. The proof instead freezes the noise: it proves a weak LDP for the pair (empirical measure of initial states and idiosyncratic paths, common noise path), which needs Sanov's theorem in the topology and the Brownian support theorem, and contracts it through the McKean–Vlasov solution map. The contraction principle requires the rate function to be good, and it is not when ; uniform continuity of the solution map and the -enlargements replace goodness.
Time is with ; paths are continuous maps on , and solutions of the SDEs are path-valued, adapted, and satisfy the integral equations almost surely. Players are indexed from . Probability measures with finite -th moment are guarded by an explicit predicate, and is the published WassersteinDRO.Duality.wassersteinDistance, kept in . Derivatives in , , are genuine derivatives; derivatives in the measure are normalized flat-derivative witnesses. Relative entropy is Mathlib's klDiv. Logarithms of probabilities are in ; open, closed and compact sets are those of the uniform metric, and is a supremum over . The action functional is an infimum over all distributional time derivatives, with test functions and distributions from Mathlib. The common-noise paths are -dimensional.
Standing assumptions are carried explicitly: the filtered space and noises of §2.3, joint independence of initial states and noises from §6.1, Assumption A (with the Borel measurability of ), B or B′, where the paper assumes it, and, for §6, Condition 6.3 and non-degenerate . Two disclosed additions: Theorems 3.9, 3.10 and 6.13 assume bounded (Condition 6.3(2) requires it; Assumption A does not imply it), and Theorem 6.13 assumes . The solutions of the Nash systems, the master equation and the SDEs are hypotheses; existence is not posed.
A rate function identically or , or bounds over a restricted family of sets, would trivialize the statements: the seminorm is a supremum over all test functions, exactly off absolutely continuous flows, and the bounds quantify over every open, compact or closed set. A complete development needs Sanov's theorem in , the Brownian support theorem, the contraction principle, Dawson–Gärtner's analysis of distribution-valued paths, and stochastic calculus for the particle systems; each of these is reusable, and contributions to any of them are welcome.
A manufacturer that sells through a retailer can also open a direct sales channel. The direct channel lets the manufacturer reach consumers, but it competes with the retailer, whose orders generate wholesale revenue. The manufacturer can further choose whether the two channels carry products of the same quality. These decisions interact because quality changes both consumer demand and the retailer's response. Ha, Long and Nasiry study this interaction in a sequential supply-chain game. Their fixed-quality-cost extension asks what happens when a high-quality design can be converted into a lower-quality variant without paying a separate production cost for each unit (Ha, Long and Nasiry, §6.2).
The main result is specific to this cost regime. With a cost per unit that rises with quality, different products can be attractive across the channels; with the paper's one-time cost of creating quality, Proposition 6(i) asserts equal qualities when the direct channel makes positive sales. This mission targets that fixed-cost proposition in the authors' manuscript, including its game and the reduced-profit claims used in the e-Companion (Ha, Long and Nasiry, pp. 20, 36–37).
The market has mass one of consumers, indexed by a taste for quality uniformly distributed on . A consumer buying a product of quality at price receives surplus . The manufacturer offers quality through her own direct channel and quality through the retailer. The ratio therefore records which channel has higher quality. The manufacturer pays a fixed cost of quality , with , and a direct selling cost per unit. The retailer has zero selling cost. Unlike a unit production cost, this fixed cost is paid once and does not scale with either channel's quantity (Ha, Long and Nasiry, pp. 7–8, 20).
The manufacturer first chooses wholesale price and qualities . After observing them, the retailer chooses its order . The manufacturer observes that order and chooses her direct quantity . When , market-clearing prices are
When , the retailer's product has higher quality, and the corresponding prices are
The manufacturer receives wholesale revenue plus direct-channel revenue, less the direct selling cost and fixed quality cost. The retailer receives its retail margin times . Encroachment means on the equilibrium path, rather than the mere existence of a direct channel (Ha, Long and Nasiry, pp. 8, 11, 15, 36).
For a subgame-perfect equilibrium of the fixed-cost game, the goal is Proposition 6(i):
The formal statement assumes . At , the high-direct-quality reduced profit is independent of , so the printed claim fails to force ; this is a substantive qualification of the manuscript's standing convention. The goal concerns the complete game, with contingent actions at every decision node, rather than only the closed-form optimization problem (Ha, Long and Nasiry, pp. 20, 36).
The milestone list follows the authors' two quality regimes. The e-Companion gives best responses, wholesale prices, and reduced profits in each regime. In the high-direct-quality regime, Claim 3 concludes that an optimum with positive direct sales has . In the low-direct-quality regime, Lemma 2 concludes that an optimum either has or lies at no encroachment. The latter alternative is outside the strict encroachment-feasible set used by the Lean milestone. Footnote 2 supplies a one-variable sign inequality used in the analysis of that regime (Ha, Long and Nasiry, pp. 36–37).
Proposition 6(i) determines the manufacturer's quality choice conditional on active direct sales: both channels carry quality . It narrows the set of equilibrium outcomes that the fixed-cost model can support and distinguishes the role of a one-time design cost from the paper's earlier variable-cost model. The paper states a separate profit comparison in Proposition 6(ii); this mission does not formalize it because the e-Companion omits its proof and the fixed-cost no-encroachment benchmark for that comparison is not stated (Ha, Long and Nasiry, pp. 20, 37).
A complete Lean development would connect the reduced-profit calculations on page 36 to subgame-perfect play in the three-stage game, and establish the optimization claims over their stated feasible sets. The definitions of two-quality inverse demand, contingent strategies, and nodewise optimality are reusable for related channel games. The goal and milestones here are draft statements, without machine-checked proofs of their economic conclusions.
The manufacturer chooses quality and wholesale price before the retailer's order, yet the direct quantity is chosen only after that order. Consequently, the retailer's payoff depends on the manufacturer's continuation response, and the first-stage choice must account for both later decisions. The reduced profit also changes at , where the higher-quality channel switches. A calculation for one regime alone does not establish the full-game claim. The strict region matters: its boundary represents no encroachment and supports a different alternative in Lemma 2 (Ha, Long and Nasiry, p. 36).
Lean uses real wholesale prices and qualities, positive and , and nonnegative quantities. Wholesale price has no sign restriction in the manuscript. The market has unit size and the retailer's selling cost is zero. The two inverse-demand expressions are applied to all nonnegative quantities, following the paper's algebraic game model. A profile contains a stage-one action, a retailer order rule for every observed , and a direct-quantity rule for every observed . Subgame perfection requires feasible best replies at every such history, including histories off the equilibrium path. Fixed cost is , paid once, while is a per-unit selling cost.
The reduced profits and are used only on their respective open encroachment-feasible domains, where the displayed denominators are positive. Claim 3 is stated for a joint maximizer in ; keeping fixed while moving to can leave that feasible set. Lemma 2 excludes the no-encroachment boundary in its Lean statement. Neither reduced profit replaces the full-game payoff in the goal. Contributions that connect the subgame formulas to arbitrary equilibrium profiles, prove the sign inequality, or establish the two optimization results are within scope (Ha, Long and Nasiry, pp. 36–37).
Linear convergence of first-order methods is usually proved through an error bound: near a solution, the distance to the solution set is controlled by the size of a computable residual, such as the length of a proximal-gradient step. For the prox-linear method, which minimizes a composition of a nonsmooth outer function with a smooth map by repeatedly solving the subproblem obtained from linearizing , Drusvyatskiy and Lewis showed in §5 of their paper (arXiv:1602.06661, Theorem 5.10) that the error bound is equivalent to subregularity of the subdifferential , a property of the objective alone and closely tied to quadratic growth. That result needs convex and finite-valued.
Many composite models violate both assumptions: constraints enter as indicator functions ( off a set), and outer functions such as truncated or concave-composite penalties are nonconvex. §8 of the paper extends the equivalence to closed, extended-real-valued, prox-regular . This mission formalizes that extension (Theorem 8.11) together with the results of §8 its proof rests on.
Fix a -smooth map and a closed (lower semicontinuous) function , and consider
The linearized function is and, for , .
Subgradients are built in three layers (Definition 8.1). A vector is a proximal subgradient of at ( finite) if for some and all near . The limiting subdifferential collects limits of proximal subgradients with ; is stationary if . The horizon subdifferential collects limits of with , , .
The map is transverse to at , written , if (8.3). The stationary point map is the set of stationary points of , and the prox-gradient mapping is ; both are set-valued.
A set-valued map is subregular at with constant if for near (Definition 5.7), and metrically regular around if the same holds with replaced by every near (Definition 8.3). A closed is prox-regular at for if the quadratic minorant holds uniformly for near with near and near (Definition 8.7). Finally, a -attentive localization of around is a map agreeing with near whenever is near and is near ; a -attentive localization of agrees with at points near with near , and one of has the form with such a localization of (Definition 8.10).
Assume , , Lipschitz around , and prox-regular at for every with . Let (i) be "some -attentive localization of is subregular at " and (ii) "some -attentive localization of is subregular at ". Then
and, when is convex, is subregular at if and only if is, for every . The constants of subregularity are left existential: the goal asserts the shape of the equivalence, not a particular constant.
Subregularity of at is exactly the error bound property of the prox-linear step, the hypothesis under which linear convergence arguments run. Theorem 8.11 says that, for the attentive parts of the graphs, this property is equivalent to subregularity of , which does not refer to any algorithm or step size. It therefore covers constrained composite problems (indicator functions ), nonconvex prox-regular penalties, and, in the convex case, removes the finite-valuedness assumption of Theorem 5.10.
The results are proved in the paper, partly by citation to Dontchev, Lewis and Rockafellar and to Lewis and Wright's analysis of prox-linear subproblems (arXiv:0812.0423). None of them is formalized: Mathlib has no proximal, limiting or horizon subdifferential, no metric regularity, and no prox-regularity. A formalization supplies these notions, checks the constant-chasing in Theorems 8.9 and 8.11, and fixes the precise quantifier order the prose leaves implicit.
The obvious route, copying the §5 argument, fails at its first step: §5 starts from the inequalities , and when takes the value one of , can be finite while the other is infinite, so no such inequality holds. Theorem 8.6 replaces it by a comparison after perturbing , which needs the stability of metric regularity (Theorem 8.4) and the epigraphical description of subgradients. A second obstacle is that collects stationary points of nonconvex subproblems, so it is set-valued and possibly empty; the proofs need prox-regularity that is uniform over the family (Proposition 8.8) and a local existence result for to obtain the threshold . The limiting-subdifferential calculus (the chain rule under transversality) is itself a substantial piece of variational analysis.
Points are in EuclideanSpace ℝ (Fin n); , , and are EReal-valued. Standing assumptions on every statement: is (ContDiff ℝ 1 c), is lower semicontinuous and never (the page's closed functions are only ever evaluated where finite or ; this is a disclosed addition). is fderiv ℝ c x and its adjoint. "" requires finite. , so (sub)regularity inequalities are stated for every element of , and metric regularity carries nonemptiness of ; is the existence of a subgradient of norm at most . and are sets defined by stationarity, never a chosen minimizer. Two printed slips are corrected and disclosed: in Definition 8.10 (2) the neighbourhood is a neighbourhood of , and in Theorem 8.11 the threshold satisfies (with the converse would be vacuous). "When is convex" is the convexity inequality in , with the theorem's other hypotheses kept.
A trivializing formalization is ruled out: subregularity always includes , a constant and a neighbourhood, so the content of (i) and (ii) cannot collapse into the trivial existence of a localization (any map is a localization of itself); and distances to empty sets are never junk zeros.
A complete development needs the three subdifferentials and their basic calculus (sum rule with a smooth function, chain rule under transversality, closedness of the limiting subdifferential), metric regularity and its perturbation stability, Ekeland's variational principle (on the platform as EkelandVP.General.ekeland_variational_principle), and a local existence result for stationary points of the subproblems. The subdifferential and regularity layer is reusable well beyond this mission. Proofs of any milestone, and of supporting lemmas on the variational-analysis substrate, are welcome.
Mean field games (Lasry–Lions 2006–2007; Huang–Malhamé–Caines 2006) describe Nash equilibria of games with a very large number of symmetric players, each interacting with the others only through the empirical distribution of their states. When all players are also exposed to a common noise, the equilibrium is no longer described by a forward–backward pair of PDEs but by a single equation on the space of probability measures, the master equation. The master equation is the object that lets one prove convergence of -player equilibria to the mean field limit (Cardaliaguet–Delarue–Lasry–Lions 2019), so a global classical solution is the starting point of that theory.
Global well-posedness requires a monotonicity condition; without one, uniqueness of equilibria fails. Before this paper, global results were known under the Lasry–Lions monotonicity condition and for separable Hamiltonians , and under displacement convexity in deterministic potential games (Gangbo–Mészáros 2022). Gangbo, Mészáros, Mou and Zhang (Ann. Probab. 50 (2022)) prove global well-posedness for nonseparable Hamiltonians under displacement monotonicity, a condition that is different from Lasry–Lions monotonicity and that has a natural extension to Hamiltonians depending jointly on .
Let be the Borel probability measures on with finite second moment, with the 2-Wasserstein distance . For , the Lions derivative is characterized by
The class consists of continuous for which , , , , and exist and extend to jointly continuous functions of all their arguments.
The data are a horizon , a common-noise intensity with , a Hamiltonian and a terminal cost . The master equation on is
with the nonlocal operator
where are independent with law . A classical solution is a satisfying the equation on and the terminal condition.
is displacement monotone (2.16) if for all square-integrable with and an independent copy ,
The Hamiltonian is displacement monotone (Definition 3.4) if a bilinear form built from , and a correction is nonpositive, with for every bounded Lipschitz map . Assumptions 3.1 and 3.2 impose regularity and bounds on and ; Assumption 3.5 imposes the two monotonicity conditions.
Under Assumptions 3.1, 3.2 and 3.5, the master equation on has a classical solution with bounded , , , , and it is the only classical solution in that class:
The theorem gives global classical well-posedness of the master equation with common noise for a class of Hamiltonians that need not be separable and data that need not be Lasry–Lions monotone. A classical solution is what the convergence analysis of -player games and the construction of approximate equilibria take as input. Theorem 4.1, displacement monotonicity propagating backward along the equation, is the central structural fact; Theorem 5.1 converts it into an a priori Lipschitz bound in that is uniform in time, which is what allows local solutions to be continued.
The result is proved in the paper; nothing in this mission is open mathematically. No part of it is formalized anywhere. The mission produces a formal statement of the master equation, its classical solutions and the displacement monotonicity conditions, plus targets for a machine-checked proof. Calculus on Wasserstein space with Lions derivatives is absent from Mathlib, so even Lemma 2.1 requires new infrastructure.
Local well-posedness holds for any regular data; the obstacle is continuing the solution to the whole interval. The length of the local interval depends on the Lipschitz constant of the terminal data in , and without a uniform-in-time bound on that constant the local intervals can shrink to zero. Lasry–Lions monotonicity is not available here, and for nonseparable it has no obvious analogue. Any argument that controls this constant has to work with second-order Lions derivatives, which needs full regularity in the measure variable. That regularity is itself only known on short intervals.
EuclideanSpace ℝ (Fin d). is a subtype of measures, so functions of are defined only on . is the published WassersteinDRO.Duality.wassersteinDistance with , converted to a real number.A large stochastic game has one state process per player. Each player's feedback changes with the empirical distribution of all states, so a finite population remains coupled even when the idiosyncratic Brownian motions are independent. A useful quantitative question is whether a statistic of the entire collection of equilibrium trajectories can deviate substantially from its mean as the population grows. Delarue, Lacker, and Ramanan answer this for smooth closed-loop mean-field games in their large-deviations and concentration paper. Their result concerns the equilibrium state paths themselves, rather than only a fixed-time empirical measure.
The paper is part of a two-paper limit theory. Its companion central-limit paper supplies the Nash-to-McKean–Vlasov estimates quoted here as Theorems 4.1 and 4.2. The concentration argument also uses transport inequalities: Gozlan's dimension-free characterization explains the quadratic transport assumption on the initial law, while Djellout, Guillin, and Wu provide a transport principle for diffusion path laws. The present mission records the paper's main concentration theorem and four of its explicit intermediate targets.
Fix a horizon and a positive state dimension . Player has a continuous state path . The empirical measure of a vector is ; the same formula applies to paths. The norm on is , and the product norm relevant to this mission is .
The game is posed on a filtered probability space with a common Wiener process , independent idiosyncratic Wiener processes , and i.i.d. initial states of law . The action space is Polish. A drift , running cost , and terminal cost specify the control problem. The Hamiltonian minimizes over actions; a selected minimizer defines and .
Classical solutions of the -player Nash system (2.6) determine the feedback in the equilibrium state equation (2.7). A classical solution of the master equation (2.8) determines the comparison particle equation (4.1). Both equations retain common-noise terms in their definitions. The goal sets the common-noise coefficient to zero. Assumption A imposes Hamiltonian attainment, Lipschitz , nondegenerate idiosyncratic diffusion, an initial moment above order four, and the stated classical solutions. Either B or B′ controls the selected running cost; B′ also bounds and as specified on pp. 8–9.
The goal is Theorem 3.4. If satisfies the quadratic transport inequality for every with finite second moment, then constants exist such that, for , , and every 1-Lipschitz on the product path space,
The four milestones retain the paper's two main comparison layers. Theorem 4.3 controls both the path-space Wasserstein distance between the Nash and comparison empirical measures and their synchronous squared path distance by for . Theorem 5.3 gives a dimension-uniform transport inequality and concentration bound for the law of a Lipschitz SDE in the coordinatewise product-supremum norm. Equation (5.7) bounds the change in a 1-Lipschitz path expectation when the deterministic initial vector changes. Theorem 5.4 gives for the interacting comparison system. The labels, constants, and domains follow the pinned preprint, pp. 12 and 16–20.
Theorem 3.4 supplies a finite-population tail estimate for every 1-Lipschitz observable of the entire equilibrium path vector. The first term becomes small at a population-dependent scale, while the second term has a rate independent of the number of players. This is stronger information than convergence of the empirical measure alone: it applies to path-dependent statistics and includes explicit deviation probabilities Theorem 3.4.
The mathematical statements are proved in the source paper, subject to its assumptions; Theorems 4.1 and 4.2 that support its comparison result are proved in the companion paper. The work here is to give these claims faithful machine-checkable statements and ultimately machine-checked proofs. The present draft is a set of open Lean theorem statements with sorry, so it asserts no completed formal proof. A completed development would also make its definitions of empirical path laws, Wasserstein continuity, flat derivatives, and interacting SDE solutions reusable for other mean-field models.
Independent-noise concentration cannot simply be applied to the Nash state paths. A player's drift depends on the empirical state measure and on a derivative of the -player Nash solution, so changing one input can change every trajectory. The master equation describes a comparison system, but using it requires matching the Nash and master feedbacks on the same filtered probability space. The regularity in Assumptions A, B, and B′ is substantial: the master field has first and second derivatives in both space and measure, with uniform bounds. A formal proof must also preserve the exact path norm and the population-independent placement of constants. The SDE transport theorem's uniformity over dimensions is particularly consequential for Theorem 5.4 §§4–5.
State vectors use finite-dimensional Euclidean spaces; time uses nonnegative reals and only is evaluated. A continuous path is a ContinuousMap on that interval with its supremum norm. Finite products use PiLp 2; the scalar-coordinate version of the norm is used for Theorem 5.3. Players are indexed from zero, corresponding to the paper's indices , and every theorem requires . Probabilities and entropy are extended nonnegative values. Transport distances stay extended until a finite-moment hypothesis justifies their real value.
The filtered Wiener processes, i.i.d. initial states, Borel coefficients, Polish action space, Nash and master PDEs, and either B or B′ are represented explicitly. The master equation is imposed on ; its spatial gradient is also required on , as Assumption A(5) specifies. A flat measure derivative is a normalized witness satisfying (2.2), while spatial derivatives are actual Fréchet derivatives. SDE solutions are path-valued processes satisfying coordinate Itô integral relations; solution families are supplied as hypotheses, since their existence is asserted by the source. Expectations appearing in the conclusions are stated integrable, so a default zero integral cannot satisfy a tail bound accidentally. The model cannot be replaced by arbitrary paths or a vacuous solution predicate: the Nash and comparison paths must satisfy their respective equations with the same noises and initial states.
The mission includes Theorem 4.3, Theorem 5.3, (5.7), and Theorem 5.4. The quoted Theorems 4.1 and 4.2, the general transport equivalence of Theorem 5.1, and tensorization in Theorem 5.2 remain useful later contributions, with their original hypotheses and conclusions intact. The printed constant in the “moreover” clause of Theorem 5.1 is omitted because it is dimensionally incorrect; no substitute assertion is placed in this mission.
Many problems in statistics, signal processing and machine learning minimize a smooth loss plus a nonsmooth regularizer over a set with manifold structure: sparse principal component analysis over the Stiefel manifold, sparse blind deconvolution over the sphere, and clustering and dictionary-learning models with orthogonality constraints. In Euclidean space the standard method for such composite problems is the proximal gradient method, whose rate for convex problems is classical (Beck–Teboulle 2009). Huang and Wei (arXiv:1909.06065v4, Mathematical Programming 2021) propose a Riemannian proximal gradient method (RPG) that solves its proximal subproblem on the tangent space and returns to the manifold through a retraction. They prove three things about it: global convergence, an rate under a convexity notion adapted to retractions, and local rates under a Riemannian Kurdyka–Łojasiewicz property. This mission covers the second result, Theorem 3.2.
Earlier Riemannian proximal methods either required the exponential map and parallel transport, or solved a Euclidean proximal problem in the ambient space (Chen, Ma, So, Zhang 2020, ManPG). Theorem 3.2 is stated for a general retraction, with an explicit constant.
Let be a finite-dimensional Riemannian manifold, with inner product and norm on each tangent space . A retraction is a family of smooth maps with and . The problem is
where is differentiable with Riemannian gradient , and is continuous and possibly nonsmooth.
For a function on a real inner-product space , the Clarke generalized directional derivative is . The generalized subdifferential is . A point is stationary for if .
Given a constant , the RPG method (Algorithm 1) produces iterates and steps as follows. Set
Choose a stationary point of on with , and set .
The assumptions involve the sublevel set and two notions defined with respect to on a set :
Assumption 3.1 asks that be bounded below and compact. Assumption 3.3 provides an open on which is -retraction-smooth and retraction-convex and is retraction-convex. Assumption 3.4 bounds how far the retraction is from Euclidean: for all ,
Finally, .
Let , suppose Assumptions 3.1, 3.3 and 3.4 hold, and let be any accumulation point of . Then for every
The constants are those of the paper.
Theorem 3.2 extends the function-value rate of the proximal gradient method to manifolds and general retractions. The constant is explicit: it combines the initial distance with a correction proportional to , which measures how far the retraction is from Euclidean. In the Euclidean case one can take , and the bound reduces to the classical one. The rate concerns , which the iteration bound of Theorem 3.1 (the norm of ) does not control.
The result is proved in the paper. None of it is formalized, and no machine-checked version of the Euclidean proximal-gradient rate is on the platform either. A formalization would supply the first checked version of Clarke stationarity on tangent spaces, of the retraction-based convexity and smoothness notions, and of a rate proof for a nonsmooth Riemannian algorithm. These pieces carry over to other retraction-based methods, such as the accelerated variants of §4 of the paper.
The arithmetic of the rate proof is a telescoping sum, so the work lies elsewhere. First, Lemma 3.4 needs a usable form of the stationarity condition : a subgradient of at equal to . This requires a sum rule for the Clarke subdifferential of a function plus a locally Lipschitz one, on a tangent space whose norm comes from the Riemannian metric rather than from the model space. Second, the gradient of at has to be identified with through . In Mathlib this mixes manifold derivatives (mfderiv) with Fréchet derivatives on a space carrying two equivalent norms. Third, it has to be shown that the iterates and the accumulation point remain in , so that Assumptions 3.3 and 3.4 apply at every step.
Theorem numbers and pages are those of arXiv:1909.06065v4. is a smooth manifold modelled on a finite-dimensional real inner-product space , with Mathlib's RiemannianBundle on the tangent bundle. All norms and inner products on are the Riemannian ones. Retractions and gradients are the published RiemOpt.BFGS.IsRetraction and RiemOpt.FR.IsGradient. The Clarke derivative is an EReal-valued limit superior along . Algorithm 1 is modelled as a run (sequences , with the three defining properties), and every statement holds for every run. Indices start at , accumulation points are cluster points of the sequence, and the bounds divided by are stated for .
The formalization commits to the following readings:
A single for all in (3.10) would make retraction-convexity force to be affine, and the theorem would only cover affine problems. That reading is excluded. Statements with the case , where Lean's makes (3.16) false, are excluded as well.
Contributions welcome: a Clarke sum rule for plus locally Lipschitz functions, the identification of the Fréchet derivative of at with the Riemannian gradient, and the five milestones in order. The Clarke layer and the derivative identification are reusable beyond this mission.
Every square-integrable martingale of a Brownian filtration is a stochastic integral, (Itô's representation theorem). The classical theorem gives no formula for . In hedging, is the replicating strategy of a claim. In filtering and stochastic control it is the quantity one has to compute. The Clark–Haussmann–Ocone formula identifies through the Malliavin derivative . That derivative is anticipative, defined only up to null sets, and acts on the Wiener space rather than on the observed path.
Cont and Fournié (arXiv:1002.2446, Ann. Probab. 2013) develop a nonanticipative alternative from Dupire's functional Itô calculus (Dupire 2009). The integrand of the representation is a vertical derivative , computed pathwise from a functional representation of the martingale. Their main structural result is that this derivative, first defined on regular functionals, extends to all square-integrable stochastic integrals and inverts the Itô integral there. This mission formalizes that extension.
Timeline:
Fix a horizon and a dimension . A path is a map . A path is cadlag on if it is right-continuous there with left limits. The stopped path is , and the vertical perturbation shifts the value at time by while keeping on . Paths with values in the positive semidefinite matrices carry the density of the quadratic variation.
A nonanticipative functional depends only on . Its vertical derivative is the gradient at of . Its horizontal derivative is the right derivative of along the flat extension. The class consists of functionals with the following properties:
All functionals also satisfy (10), .
Assumption 5.1. is a standard -dimensional Brownian motion, and
with adapted to . The density of is cadlag and adapted. The working filtration is , the completed natural filtration of , right-continuous on .
The spaces involved are:
The operator is closable on . Its closure is a bijective isometry
and is the unique element of with
In particular in . The adjoint identity (55),
is a separate item.
The theorem identifies the integrand of the martingale representation of any square-integrable -martingale as a limit of pathwise derivatives. On regular functionals, those derivatives are computed by perturbing the endpoint of the observed path. The integrand is therefore adapted by construction, and it can be approximated by finite differences. This is the basis of the paper's general representation formula (Theorem 5.9) and of its comparison with Malliavin calculus (Theorem 6.1, ). The isometry also gives the structure of a Hilbert space on which is a weak derivative. This is a nonanticipative counterpart of the Wiener–Sobolev space .
The results are proved in the paper; none of them has a machine-checked proof. Neither Mathlib nor the platform has a square-integrable Itô integral with its isometry, a functional Itô calculus, or a martingale representation theorem. A complete development would provide the first formal statement and proof of a martingale representation formula with an explicit, nonanticipative integrand. The path-space and layers are reusable for any work on path-dependent functionals.
The proof of the goal is short once its inputs are available, but each input is substantial.
A tempting shortcut is to define on as the inverse of the Itô integral. That makes (56) a tautology and erases the link with the pathwise derivative, so the closure must be built from .
Time is , statements are made on , and functionals are defined on all paths, with every quantifier over path space restricted to cadlag pairs. The derivatives of a functional are explicit witnesses tied to it by HasDerivWithinAt and HasFDerivAt, so a derivative is never a junk value. The distance uses the max norm on (sup norm on vectors, entrywise sup norm on matrices) and appears only through explicit bounds.
The formal setting makes these hypotheses explicit:
In dimensions, means . The square-integrable Itô integral is a relation, defined through simple dyadic integrands and an almost-surely continuous integral process on . This continuity selects the stochastic integral version from the limits at fixed times. The derivative of each test process is required to belong to , as Definition 5.4 states. Theorem 5.2 integrates by dyadic left Riemann sums in probability (EthierKurtz.itoStepSum). Corollary 4.4 is stated for , because the printed version fails at .
The statements must not be trivialized. The closure of is a relation, and its existence, uniqueness up to -null sets, isometry and surjectivity are all conclusions, never definitions. Expectations of squares are lower integrals in , and every real expectation in (51), (53) and (55) comes with its integrability as part of the conclusion. is not reduced to , because . A derivative witness cannot be chosen freely, because it is tied to .
Contributions are welcome on:
The martingale optimal transport problem asks for a coupling of two probability measures on that is the law of a one-step martingale and minimizes an expected cost. It arises in robust finance, where the marginals are the risk-neutral laws of an asset at two dates implied by option prices, and model-independent price bounds for exotic options are the extreme values of the problem (Beiglböck, Henry-Labordère, Penkner 2013; Galichon, Henry-Labordère, Touzi 2014).
Beiglböck and Juillet (arXiv:1208.1509v2, Ann. Probab. 44(1), 2016) construct a canonical martingale coupling, the left-curtain coupling, which plays the role that the monotone (quantile) coupling plays in classical transport. Its construction rests on one object, the shadow of a measure in another, and on one structural property of it: shadows are associative. This mission formalizes that property, Theorem 4.8 of the paper, together with the chain of results in §2.3 and §4.1–4.3 on which it rests.
Let be the set of finite Borel measures on with finite first moment, of any total mass. For :
If , a shadow of in is a measure with (i) , (ii) , and (iii) for every satisfying (i) and (ii). Lemma 4.6 of the paper shows that it exists and is unique; it is written . It is the least spread-out part of into which can be transported by a martingale. An atom is a measure with .
In the Lean development these objects are InM, ConvexLE, ExtConvexLE, potential, ConvergesInM and the predicate IsShadow ν μ η, in the namespace MartOT.Shadow.
For with ,
Theorem 4.8 is what makes the left-curtain coupling well defined and consistent. That coupling is the martingale plan which, for every , sends onto (Theorem 4.18). Associativity says that the parts of assigned to and to fit together into the part assigned to , so the family of shadows defines a single coupling. The uniqueness of left-monotone martingale plans and the optimality of the left-curtain coupling for the costs with strictly convex, both later results of the paper, rest on it.
The result is proved in the paper. As far as is known it has no machine-checked proof. This mission produces a statement of it, and of the supporting results, in terms of measures of arbitrary finite mass with no reference to a chosen shadow function. A complete development would give Lean a theory of the convex order on finite measures through potential functions, which is reusable well beyond martingale transport.
For finitely atomic measures the identity follows by adding one atom at a time (Lemmas 4.12, 4.13, 4.16), but even the single-atom step needs a monotonicity property of shadows of atoms in varying targets (Lemma 4.11), and that property comes from their explicit description through quantile functions. The general case cannot be obtained by a direct manipulation of the minimality property (iii): minimality of and of separately says nothing obvious about minimality of their sum among measures dominating , because a competitor for the sum need not split into competitors for the summands. The paper passes to the limit along convex-order approximations, which requires a continuity property of the shadow (Proposition 4.15) in the topology of .
MeasureTheory.Measure ℝ with membership in stated explicitly (InM: finite measure, identity integrable). Masses are arbitrary; nothing is normalized to probability measures.EReal through the published ModelRiskOT.Duality.extIntegral (positive minus negative part), never as Bochner integrals, so a non-integrable test function cannot produce a junk value. The extended convex order uses lower Lebesgue integrals of nonnegative functions.IsShadow ν μ η, never a function built by choice. Every statement about quantifies over all shadows, which with existence and uniqueness (Lemma 4.6, a milestone) is the paper's statement. Uniqueness is part of the conclusion of Lemma 4.6 and is not assumed elsewhere.IsShadow ν (γ1 + γ2) (η1 + η2).Martingale optimal transport asks for the cheapest way to couple two given laws and on by a one-step martingale: a pair with , and . The problem arises in mathematical finance, where and are the risk-neutral laws of an asset at two maturities, implied by quoted vanilla option prices, and the extremal values of over all such couplings are model-independent price bounds for the exotic payoff (Beiglböck, Henry-Labordère, Penkner 2013; Galichon, Henry-Labordère, Touzi 2014). In classical optimal transport on the line, a single coupling, the monotone (quantile) coupling, is optimal for a whole family of costs. Beiglböck and Juillet (arXiv:1208.1509, Ann. Probab. 2016) identify its martingale counterpart, the left-curtain coupling , and determine costs for which it is optimal.
This mission formalizes one of those optimality results, Theorem 6.3: for product costs with strictly convex and decreasing, is the unique optimizer.
Let be the set of finite Borel measures on with finite first moment. For the convex order means for every convex ; it forces equal mass and equal mean. The extended convex order asks this only for nonnegative convex .
A transport plan from to is a measure on with marginals and ; the set of them is . It is a martingale transport plan, , if is -integrable and
that is, the conditional law of given has barycentre for -almost every . For a cost the cost of a plan is , the value is , and is optimal if it belongs to and attains this infimum.
For a plan and , the measure is where sends the left part of . Given , the shadow is the measure with and that is -below every other such measure. The left-curtain coupling of is the plan with
It sends every left part of to the most concentrated part of that can receive it by a martingale.
Let be finite measures, strictly convex, strictly decreasing, , and assume . Then
Theorem 6.3 gives a class of costs for which the martingale transport problem has an explicit, cost-independent solution, and does so with uniqueness and without any regularity of beyond monotonicity. In the financial reading, every payoff of the form with these shape properties has its model-independent lower price bound attained by one and the same model, the left-curtain martingale, which depends only on the marginals. The result complements Theorem 6.1 of the same paper (costs with strictly convex), proved by a different, variational route.
The theorem is proved in the paper. No machine-checked version is known: neither the left-curtain coupling nor shadows nor martingale optimal transport on appears in Mathlib or on the platform. A formalization produces the shadow construction, the left-curtain coupling as a Lean object with its characterization, and the comparison principle " has the -least targets", all of which are reused by the other results of the series (uniqueness of the left-monotone plan, Theorem 6.1, the support bounds of §7).
The obvious argument compares costs plan by plan, but the convex order of two measures alone does not order the integrals of a strictly convex strictly: that forces requires representing as a martingale image of (Strassen's theorem on ) and the equality case of Jensen's inequality, with care about infinite integrals. The second obstacle is the passage from "equal targets for almost every level of " to "equal plans": the superlevel sets of a strictly decreasing are half-lines that may be open or closed at the jumps of , so the targets must be controlled for both kinds of half-line, and a null set of levels must be bridged by monotonicity of . Existence of shadows (Lemma 4.6) is itself a nontrivial construction through potential functions .
Measures are Mathlib Measure ℝ and Measure (ℝ × ℝ) with the Borel σ-algebras. and are finite, not necessarily probability, measures, as the theorem states; membership in is part of ConvexLE. Integrals that may be infinite take values in EReal, through the published ModelRiskOT.Duality.extIntegral (). is encoded by the characterization above with bounded test functions . The shadow and the left-curtain coupling are predicates (IsShadow, IsLeftCurtain); their existence and uniqueness are milestones, never built into definitions. "Optimal" is minimality of cost over martingale plans; attainment is not assumed.
Two hypotheses are read into the printed statement. "Decreasing" is strict: with all martingale plans have the same cost , and for uniform on , uniform on there are infinitely many of them. is added, as the proof assumes a plan of finite cost; otherwise every plan is optimal. A formalization in which is merely some plan, the cost is a Bochner integral (which is for non-integrable integrands), or optimality is taken among all plans rather than martingale plans would not be Theorem 6.3. Theorem 4.18 is stated for finite measures of equal mass, the generality Theorem 6.3 needs. Strassen's theorem is already posed on the platform (PalmQueueing.Ordering.strassen_cx) and is not restated.
A complete development needs the convex order on finite measures, shadows, the left-curtain coupling, a layer-cake identity for product integrands and the equality case of the convex order for strictly convex test functions. The shadow and left-curtain layers are reusable across the whole series; contributions to any milestone, and to general lemmas on the convex order of finite (not only probability) measures, are welcome.
Many problems in statistics, signal processing and machine learning minimize a smooth loss plus a nonsmooth regularizer over a set that is a manifold rather than a vector space: sparse principal component analysis over the Stiefel manifold, sparse blind deconvolution over the sphere, low-rank recovery over fixed-rank matrices. In Euclidean space the standard tool for with smooth and nonsmooth is the proximal gradient method, whose convergence theory (stationarity of limit points, an bound on the number of iterations to reach an -small step, an rate under convexity) is classical (Beck–Teboulle 2009).
Huang and Wei (arXiv:1909.06065, Mathematical Programming 2021) proposed the Riemannian proximal gradient method (RPG): at each iterate the proximal subproblem is posed on the tangent space, the nonsmooth term is pulled back through a retraction, and the next iterate is obtained by retracting the computed step. Unlike the earlier ManPG method of Chen, Ma, So and Zhang (2020), which uses the Euclidean proximal mapping of an embedding space, RPG is defined intrinsically on any manifold with a retraction. Its global convergence theorem is the subject of this mission.
Let be a finite-dimensional manifold with a smooth Riemannian metric on each tangent space , with norm . A retraction is a smooth map , , with and . The vector transport by differentiated retraction is ; denotes its adjoint for the two metrics and the adjoint of its inverse.
The problem is
with continuously differentiable, Riemannian gradient , and continuous, possibly nonsmooth. For the Riemannian Clarke subdifferential is defined through the pull-back on the Hilbert space :
A point is stationary if .
Algorithm 1 (RPG). Given and a constant , for let
choose that is a stationary point of with (condition (3.1)), and set .
Assumption 3.1. is bounded below and is compact. Assumption 3.2. is -retraction-smooth on : (inequality (3.2)).
For every run of Algorithm 1: if then is stationary. Under Assumptions 3.1 and 3.2, has an accumulation point, every accumulation point is stationary, and for every some iterate with index at most
satisfies .
Theorem 3.1 is the basic convergence guarantee of RPG: the method is a descent method without any convexity of , its limit points satisfy the first-order necessary condition , and the number of iterations needed to make the step small is explicit, with the same dependence as in the Euclidean case. It underlies the further analyses of the same paper (the rate under retraction convexity and the Kurdyka–Łojasiewicz analysis) and of later Riemannian proximal methods.
The theorem is proved on paper; no machine-checked version exists. Formalizing it requires a Clarke subdifferential on tangent spaces, its calculus (sum rule with a function, chain rule through a local diffeomorphism) and its closedness along convergent sequences on a manifold. None of these is in Mathlib. They are reusable well beyond this paper by any Riemannian nonsmooth optimization method.
The descent inequality and the iteration bound are elementary once Lemma 3.1 is available. The difficulty is the stationarity of accumulation points. The subproblem's optimality condition (3.8) lives in the tangent space at and involves a subgradient of at ; to pass to the limit, the gradients and subgradients must be compared across different tangent spaces, which is what the inverse-adjoint transport and Lemma 3.2 do. This needs joint continuity of the retraction and its differential on the tangent bundle and continuity of the metric, and then a closedness property of the Riemannian Clarke subdifferential that the paper cites from Hosseini, Huang and Yousefpour (2018, Theorem 2.2(c)) and that a complete development must prove. A pointwise argument at a fixed base point does not suffice, because the base points move.
Theorem numbers and pages are those of arXiv:1909.06065v4. The manifold is modelled on a finite-dimensional real inner-product space and carries a RiemannianBundle with a smooth metric (IsContMDiffRiemannianBundle). Retraction, differentiated-retraction transport and Riemannian gradient are the published definitions RiemOpt.BFGS.Setting and RiemOpt.FR.Setting; joint smoothness of on the tangent bundle is added, as on p. 4. The Clarke limit superior is taken in EReal along , so it never takes a default value. Accumulation points are MapClusterPt, and "in at most iterations" is an index . A run of Algorithm 1 is any sequence of iterates and steps satisfying (3.1); the step is a selection, not a function of the iterate.
Two hypotheses are explicit in the Lean statements. Each pull-back is locally Lipschitz, which p. 5 requires for the subdifferential to be defined. is , because the proof applies Lemma 3.2 to . Assumption 3.2 is stated in the form the proof of Lemma 3.1 uses: (3.2) at every for every tangent vector. Definition 3.1 read literally only constrains with , and under that reading Lemma 3.1 fails: a nonconvex can send far outside . The paper's own sufficient condition gives the strengthened form.
The formalization must not trivialize stationarity. The subdifferential is defined from the Clarke derivative of the pull-back alone. It does not involve or ContinuousLinearMap.inverse, so is a genuine condition. The run hypotheses are satisfiable, for instance on with , , , , .
Welcome contributions: the Clarke calculus on a real Hilbert space (sum rule, chain rule through a map, upper semicontinuity), local invertibility of near the zero section, and the closedness of the Riemannian subdifferential on the tangent bundle.
Adam (Kingma and Ba, 2015, arXiv:1412.6980) is one of the most widely used optimizers for training neural networks. It is a stochastic gradient method that keeps exponential moving averages of the stochastic gradients and of their coordinatewise squares, rescales both by bias-correction factors, and divides the first by the square root of the second. Its original convergence analysis was shown to be flawed (Reddi, Kale and Kumar, 2018, arXiv:1904.09237), and in the regime in which practitioners actually run it, with a constant step size, the iterates do not converge.
Barakat and Bianchi (arXiv:1810.02263, SIAM J. Math. Data Sci. 3(1), 2021) describe what constant-step Adam does instead: as the step size tends to zero, with the averaging parameters tending to one at rates proportional to , the interpolated iterates follow a deterministic non-autonomous ordinary differential equation. This mission formalizes that statement, Theorem 4.3 of the paper, together with the lemmas of its proof (§8.1).
Let with points , and its subset with coordinatewise. A random sample with law on a measurable space enters through an integrand with gradient in . The objective is and the second-moment map is .
Given a step size , parameters , in and , the Adam map sends to
coordinatewise. The constant-step iterates are and , driven by iid samples with law . The interpolated process is the piecewise linear function with .
The parameters satisfy and as , with . The limiting Adam ODE is , , where for
The vector field is singular at . A global solution is a continuous map , continuously differentiable on , that satisfies the equation for every .
Under the paper's assumptions (Assumptions 2.2 to 2.5, 4.1, and 4.2 ii) with ),
where is the global solution of the Adam ODE from .
The theorem justifies the continuous-time model of Adam that the rest of the paper studies. The convergence of the ODE to critical points of (Theorem 3.2) and its rates (Theorem 3.4) say something about the algorithm only through this approximation. It also isolates the role of the bias correction: the initial condition and the singular factors are exactly the trace of the debiasing step. The result is also the first step towards the long-run statement, Theorem 4.5, which bounds the time the iterates spend away from the critical points as .
The result is proved on paper. To the knowledge of the mission, none of it is machine-checked: there is no formal statement of Adam's dynamics on Prove2Me. A complete development would give a checked instance of the ODE method for a non-autonomous, non-Lipschitz limit field and a non-homogeneous Markov chain. The surrounding stochastic-approximation library (truncation by stopping, uniform integrability, tightness of interpolated processes, identification of limits by uniqueness) applies to other adaptive methods, such as RMSProp and AdaGrad variants, whose limits have the same structure.
The standard argument for constant-step stochastic approximation assumes a time-homogeneous mean field that is locally Lipschitz. Neither holds here. The mean field depends on the iteration index through the bias-correction factors . Its limit blows up as , and it is not Lipschitz in near . A direct Gronwall comparison between the iterates and the ODE therefore fails at the origin of time, which is exactly where the iterates start.
The iterates are also not known to be bounded. Moment bounds are only available while the debiased iterate stays in a ball. This forces the truncation and an argument that the truncation is asymptotically never triggered. That argument needs uniform-in-time bounds on the ODE solution (Proposition 7.6) and uniqueness of the solution (Proposition 7.12), and both rest on a Lyapunov function specific to the case .
E d × E d × E d with E d = EuclideanSpace ℝ (Fin d). The paper's is the Euclidean norm of , written zNorm, not Mathlib's max norm on products.iIndepFun. Every with has law , and is unused.𝓝[>] 0). The event is written as , which is the same event.A trivializing formalization is ruled out. and are universally quantified before the limit and do not depend on . The limit is in , not in at fixed ; constant-step Adam does not converge in . The solution is tied to the , , , of the stochastic model. All hypotheses are satisfiable, for example by with equiprobable.
A complete development needs:
Contributions to any of these, including reusable statements about interpolated processes, are welcome.
A distributionally robust decision evaluates a rule against every data distribution within a specified transport budget of a baseline law. The budget is a modeling choice: increasing it expresses more uncertainty about the data. A robust objective value can increase with that budget, but the value alone does not describe how the adverse distribution changes. For a fixed linear decision, Blanchet, Murthy, and Zhang identify the worst-case distribution and ask what happens to each observation as the budget increases. Their Theorem 7 gives a sample-wise answer in a small-radius regime: adverse observations move along straight lines, and their distance from the original observations grows monotonically.
This matters when a robust solution is interpreted through its adverse scenarios. The result says that two nearby ambiguity budgets do not produce unrelated worst-case data sets. They produce a coherent family of transported observations whose directions are determined by the sign of the loss derivative. The theorem is a structural property of an optimal-transport ambiguity set, beyond a bound on its optimal value. It appears in a paper that also develops dual formulas and iterative optimization schemes for the same model Blanchet, Murthy, and Zhang, 2022.
Let take values in with baseline law . A decision belongs to a convex set and incurs loss . At each source point , a positive-definite matrix defines the transport cost
The matrix may depend on , so movement can be cheaper in different directions and at different observations. The model requires lower semicontinuity of and almost-sure lower and upper spectral bounds for . A distribution is within the ambiguity ball of radius when it can be coupled with at expected cost at most . The worst-case objective is the supremum of over that ball. In Lean, the equivalent coupling formulation records a joint law with first marginal , second marginal , and cost at most .
The paper reduces the worst-case calculation to a dual objective , where prices the transport budget. Its pointwise term is the supremum over a scalar of the function in display (7). The set of maximizing scalars is . A scalar maximizer produces a transported observation
Assumptions 2–4 require a convex loss with controlled growth, a fourth moment of , bounded second derivatives of the loss, a nondegenerate loss derivative, and compactness of . The statement here also uses Assumption 5, local strong convexity with a positive-probability nondegeneracy condition. The paper’s proof of Theorem 7 uses that condition through its small-radius strong-convexity result Theorems 4 and 7.
For each fixed , the goal asserts that there is a common threshold and a family such that the law of is the unique worst-case distribution for every . For any pair , it asserts, -almost surely,
Consequently,
The goal keeps the uniqueness and primal attainment clauses together with these comparisons. The milestones follow the paper’s prerequisites: the optimizer and curvature bounds of Proposition 9, the unique worst-case law of Theorem 6(e), uniqueness of the dual minimizer at small radius, and the sign of the pointwise maximizer. Each has its own statement so solvers can use it elsewhere.
The theorem gives a consistent interpretation of changes in the ambiguity radius. If the loss increases locally in the decision direction, an adverse observation moves farther in that direction; if the loss decreases, it moves farther in the opposite direction; at a stationary score it stays put. The corresponding displacement norm is monotone for each radius pair, almost surely. This is stronger than monotonicity of the worst-case objective value: it describes the geometry of a family of optimizers, not only their values.
The paper proves the result in §5.4. The work of this mission is to formalize its hypotheses, optimality claims, and sample-wise inequalities in Lean. The published ModelRiskOT.Duality coupling definitions already give a reusable primal interface; this mission adds the state-dependent quadratic cost, the scalar dual model, its small-radius regions, and the comparative-statics statements. The proof obligations remain open in this draft. Their formalization would also make the dual optimizer bounds and the deterministic transport representation reusable in later optimal-transport DRO developments.
The worst-case value being monotone in does not force a particular worst-case distribution, or each observation in one, to move monotonically. The theorem needs a unique worst-case law and a coherent choice of pointwise maximizers as varies. The scalar maximizer depends on both the radius and the dual price, while the optimal dual price itself changes with the radius. The paper’s small-radius conditions keep this joint variation controlled. Without uniqueness, two optimal laws could differ even at the same radius, and a sample-wise comparison would have no fixed object to compare.
The result also involves several layers of almost-sure reasoning. Spectral bounds on hold only outside a null set; the relevant maximizer and its transported law must be measurable enough to define pushforwards and expectations. These conditions must be carried through the theorem without silently replacing an almost-sure claim by a pointwise one.
Vectors use EuclideanSpace ℝ (Fin d), and the baseline is a Borel probability measure. The decision set is convex and compact and is explicitly nonempty. Assumption 1 gives positive definiteness of everywhere, lower semicontinuity of the cost, and almost-sure uniform spectral bounds. The loss satisfies Assumptions 2–5. The fourth moment in Assumption 2 and the bounds on control the integrals used by the dual theory. A positive ambiguity radius is required whenever its square root appears.
The dual terms and use extended-real values, since the pointwise supremum can be infinite. The worst-case value is a supremum over feasible couplings, with signed loss integrated using the published extended-real integral. A graph coupling witnesses attainment, and every optimal coupling must have the same second marginal. This ties the family to the actual worst-case distribution rather than an arbitrary monotone scalar field. Almost-everywhere measurability of and the transport map is part of the conclusion.
The radius varies inside the goal. The threshold is chosen before any radius pair, and the comparisons are stated almost surely for each pair. The paper prints Theorem 7 under Assumptions 1–4 while referring to and invoking Theorem 4, which uses Assumption 5; this mission includes Assumption 5 explicitly. It also reads the singleton clause of Theorem 6(e) almost surely, because its threshold is an essential supremum, and uses a non-strict lower curvature bound in Proposition 9(b), as its proof permits. Contributions on the small-radius dual theory, measurable maximizers, primal attainment, and the radius comparisons are all within scope.
Many quantities in stochastic analysis and mathematical finance depend on the whole past of a process, not only on its current value: running maxima, averages, integrals against the quadratic variation, payoffs of path-dependent options, conditional expectations of path functionals. The classical Itô formula describes the evolution of for a smooth function of the current state; it says nothing directly about a process that depends on the path .
In 2009 Dupire proposed two pathwise derivatives for such functionals, a horizontal (time) derivative obtained by freezing the path and a vertical (space) derivative obtained by bumping its endpoint, and a change-of-variable formula built on them (Dupire 2009). Cont and Fournié gave this calculus a rigorous framework and proved the functional Itô formula for continuous semimartingales (Cont and Fournié, Ann. Probab. 2013; preprint arXiv:1002.2446v5). The companion paper (Cont and Fournié, J. Funct. Anal. 2010) gives a pathwise version in the spirit of Föllmer. The formula underlies the martingale representation results of the same paper and the later theory of path-dependent PDEs.
Fix a horizon . A path is a cadlag function on ; denotes the -valued ones and the paths with values in the positive semidefinite matrices. For a path :
A nonanticipative functional assigns a real number to each pair , measurably for the -algebra generated by the evaluations of the paths (Definition 2.1). Paths at different times are compared with the distance (9),
is left-continuous (, Definition 2.4) if is close to whenever is -close to ; it is boundedness preserving (, Definition 2.5) if it is bounded on sets of paths with values in a compact set. The horizontal derivative is
and the vertical derivative is the gradient at of ; is the vertical derivative of . (Definition 3.6) is the class of left-continuous with continuous at fixed times, left-continuous, and .
On a filtered probability space satisfying the usual hypotheses, is a continuous -valued semimartingale and its quadratic covariation has a density, (3), with cadlag, adapted, -valued. has predictable dependence on when (10).
For every verifying (10) and every , almost surely,
Theorem 4.1 shows that a path-dependent process is a semimartingale whose decomposition is computed from the jet along the path of . It contains the classical Itô formula () and covers functionals such as , and . Downstream it yields the identification of the martingale part of , the intrinsic character of the vertical derivative of an adapted process (Corollary 4.4), and the representation of smooth martingales (Theorem 5.2), which is the subject of the second mission of this series.
The result is proved in the paper. No machine-checked proof of it exists; the classical multidimensional Itô formula itself is an open goal on this platform (EthierKurtz.ito_formula). This mission produces a formal definition layer for functional Itô calculus (stopped paths, the metric , the regularity classes, pathwise derivatives) and a formal statement of the formula with its supporting lemmas.
The obvious argument fails at its first step: a path functional cannot be differentiated along the path of . The horizontal derivative freezes the path and the vertical derivative bumps only its endpoint; neither is a perturbation of in the direction of its own increments, so the chain rule behind the classical Itô formula has nothing to act on. A second obstruction is regularity: is only cadlag, the derivatives of are only left-continuous or continuous at fixed times for , and the paths at which they must be evaluated live on intervals of different lengths. Any limit procedure therefore needs uniform control of cadlag paths in the sup norm, which fails across their jumps, together with convergence theorems for stochastic integrals whose integrands are only locally bounded. Finally, the classical Itô formula, which is a special case, is itself not yet formalized.
Time is with horizon , and every statement concerns . Paths are functions on ; a path on is represented by its stopped version , which also serves as the horizontal extension. Functionals are defined on all path pairs and are required to be nonanticipative (); every continuity, boundedness and differentiability condition quantifies only over pairs cadlag on with positive semidefinite , as in the paper. The norm on pairs (vector, matrix) is the largest absolute value of the entries; "" is an explicit bound, so unbounded suprema never count. The derivatives are witnesses tied to by one-sided and Fréchet derivative statements, which makes them unique; free derivative witnesses, a functional that is not nonanticipative, and conditions over non-cadlag paths are each excluded. Definition 2.1's measurability is part of the class: without it Theorem 2.7 fails.
The semimartingale is with continuous, adapted, of bounded variation, and a continuous local martingale componentwise (the published EthierKurtz.IsSourceLocalMartingale); (3) uses the published EthierKurtz.HasCrossVariation. The Itô integral in (30) is the limit in probability of dyadic left Riemann sums (the published EthierKurtz.itoStepSum): the goal states that these sums converge to the remaining terms of (30). This is the a.s. identity, not a weakening, because limits in probability are unique; it is not a junk limit, because the integrand is left-continuous up to a -null set, adapted and locally bounded. The -integrals have bounded integrands by , so the Bochner integrals are genuine.
A complete development needs: cadlag path lemmas (A.1–A.3), stopping times of jumps, the predictable -algebra (in Mathlib), the classical Itô formula, and dominated convergence for stochastic integrals. The cadlag lemmas and the path-space layer are reusable beyond this mission. Proofs of any milestone, of the classical Itô formula, and of the stochastic-integral convergence theorems are welcome.
An online retailer does not show its catalogue at once. Products are arranged on a sequence of pages, and a consumer looks at the first few pages and then chooses among what she has seen, or leaves. Where a product is placed therefore decides whether it is considered at all. Gallego, Li, Truong and Wang (Operations Research, 2020) call the placement decision product framing. They show that the optimal framing problem is NP-hard even with two pages and a multinomial logit choice model, and give polynomial-time framing algorithms with constant performance guarantees.
The paper builds on the assortment optimization literature, where a seller chooses one set of products to offer under a choice model, and on work in which consideration sets depend on how products are presented. Davis, Topaloglu and Williamson (2015) studied a sequential assortment problem in which products are added over time. Two of their results, on how per-product revenue behaves when products are removed, are the structural inputs of this mission. Aouad and Segev (2016) studied a variant with one product per page under the MNL model, in which every product must be displayed.
There are products , and product earns unit revenue . The products are placed on pages, each holding at most products, and a product may be left undisplayed. A consumer views the first pages, where is random with law and tail , independent of the framing. Her consideration set is the set of products on pages .
A choice model gives, for each consideration set , purchase probabilities with for and . The expected revenue of is . The optimal framing value is
the maximum over all placements with at most products per page (problem (1)). The cardinality-constrained assortment problem is (problem (2)), and is the best revenue from a consumer who sees pages.
The analysis rests on three assumptions:
The algorithm NEST(), for , first takes an optimal solution of (2) with bound . Then, for down to , it chooses of size whose per-product revenue is at least that of . Page displays , and pages after stay blank. is the expected revenue of this framing, and .
The goal holds under A1, A2 with and A3, for every run of NEST(), . Here .
The milestones are the numbered results the proof of Theorem 3 uses, in the order it uses them:
taken over NBUE tails and functions that are increasing with decreasing and . Proposition 3 states . 7. Lemma 7 and Corollaries 5–6, comparing NBUE with an exponential variable of the same mean. 8. The evaluation for exponential with mean . 9. The bound .
Theorem 3 gives a constant-factor guarantee for a problem that is NP-hard under the same assumptions. The constant does not depend on the choice model beyond A1, on the number of pages, or on the page capacity, and the paper shows it is tight relative to the upper bound (Proposition 4, in the geometric limit). NEST needs only a cardinality-constrained assortment oracle, which exists in polynomial time for the MNL and nested logit models. The same bound-revealing program, problem (5), is reused in the paper for joint framing and pricing (Theorem 7).
The paper proves the result in full. No part of it has been machine-checked. The mission formalizes the model and states the guarantee and every intermediate result. The proofs combine finite combinatorics (Lemmas 1 and 2, Proposition 1) with a comparison of a discrete NBUE law against the exponential distribution, and that comparison is reusable for other approximation analyses with the same structure. The equality of the exponential integral with connects to Mathlib's hasSum_zeta_two.
The upper bound (Theorem 2) and the lower bound (Proposition 1) are each elementary. The difficulty is to compare them uniformly over all choice models and all NBUE page-count laws. The ratio of to depends on the whole function and the whole law of , and the worst case cannot be read off from any single instance. Replacing the instance by the program (5) removes the choice model. Bounding the program still requires an optimization over distributions, and its value is attained only in a limit (Proposition 4).
The comparison with the exponential law goes through the increasing convex order. Here is a discrete law on and the comparison variable is continuous. The function to which Lemma 7 is applied is increasing and convex only on , so a formal argument has to track the domain.
Theorem numbers and pages are those of the authors' accepted manuscript (49 pp.), which differ from the journal typesetting. The conventions are:
Fin n. Pages are the naturals , kept 1-based, with .Fin n → ℕ: page means "not displayed", and each page holds at most products. is the maximum over the finite, nonempty set of feasible framings.expMeasure with rate . The independence in Corollary 6 is encoded by iterated integrals.NEST makes arbitrary choices, so a run is a predicate on its output. Theorem 3 is stated for every family of runs, and a separate milestone shows that runs exist. The value is the expected revenue of the framing the run actually displays, not the closed form , whose equality with it is part of the proof of Proposition 1. A formalization that quantified over some run, that defined by that closed form, or that assumed Lemma 2 for would not be Theorem 3.
Program (5) is stated with its tail variable and law , . The page's typos are corrected in the statements and recorded in the notes: "" in (5), and the right-hand side of Corollary 5. Proposition 2 is formalized in its existential reading: some optimal solution of (5) has constant .
A complete development needs:
The exponential comparison and the integral are reusable beyond this mission. Proofs of any milestone are welcome, including alternative proofs of Lemmas 1 and 2 from A1.
Adam (Kingma and Ba, 2015, arXiv:1412.6980) is the default optimizer for training deep neural networks. At each step it keeps exponential moving averages and of the stochastic gradients and of their coordinatewise squares, corrects both for their initialization at zero (the bias-correction or debiasing step , ), and moves the iterate by . Despite its use, its convergence theory for nonconvex objectives was thin; the original convergence argument was later shown to be flawed (Reddi, Kale and Kumar, 2018, arXiv:1904.09237).
Barakat and Bianchi (arXiv:1810.02263v4, SIAM J. Math. Data Sci. 3(1), 2021, doi:10.1137/19M1263443) study Adam through the ODE method: when the stepsize tends to zero and the averaging constants satisfy , , the interpolated iterates follow a deterministic non-autonomous differential equation, the continuous-time Adam ODE. Everything else in the paper (convergence of the trajectory, rates under a Łojasiewicz condition, tracking by the constant-step iterates, almost-sure convergence of a decreasing-step variant) presupposes that this ODE is well posed from Adam's initialization. This mission formalizes that well-posedness result, Theorem 3.1 of the paper.
Let and , with points ; set , and . The data are reals , a function (the objective) and a map (in the paper, and , the mean squared gradient). All vector operations are coordinatewise. The Adam vector field is, for ,
and (ODE) is . The factors and are the continuous-time debiasing. A global solution with initial condition is a continuous map , continuously differentiable on , satisfying (ODE) for every , with .
The proof works with the regularized equations : for , and for , where . The fields are extended to by replacing with , and denotes the set of solutions on , . The Lyapunov function is with , and its limit is . The debiasing map is .
The hypotheses are those of §7 of the paper: is with locally Lipschitz gradient (Assumption 7.1) and coercive (Assumption 2.3); is locally Lipschitz (Assumption 7.2) with coordinatewise (Assumption 2.4); and (Assumption 2.5).
For every there is a global solution of (ODE) with initial condition such that
and any two global solutions with initial condition coincide on .
Theorem 3.1 makes the continuous-time Adam trajectory a well-defined object. The paper's convergence theorem for this trajectory (Theorem 3.2), its rate under a Łojasiewicz condition (Theorem 3.4) and the tracking result for the constant-step iterates (Theorem 4.3) are all stated about "the" solution, and the semiflow used for the asymptotic pseudotrajectory argument rests on the same uniqueness. The bound of Proposition 7.6 also gives the cost decrease , which the authors read as evidence that the bias correction makes early Adam steps safe.
The result is proved in the paper, and as far as is known nothing here has been formalized; no statement about this ODE exists on the platform. The mission formalizes the statement and the numbered lemmas of its proof. A complete development would also be a worked example of existence for an ODE whose field is neither continuous in time at nor Lipschitz in space, by regularization, compactness and passage to the limit.
Off-the-shelf theory does not apply. Cauchy–Lipschitz fails because contains , which is not Lipschitz at , and the initial condition has . Cauchy–Peano fails because blows up as : the factor behaves like . The obvious remedy, shifting time by , gives solutions , but passing to the limit needs bounds uniform in , both on the trajectory and on how far stays from zero. Uniqueness then has to be proved by a Grönwall argument whose coefficient is not integrable at , so the initial behaviour of solutions must be controlled to second order. Solutions from initial conditions with , need not exist at all (p. 5), so the special initialization is essential, not cosmetic.
Vectors are EuclideanSpace ℝ (Fin d) and states are triples; Lean's norm on the product is the maximum of the three Euclidean norms, which changes no boundedness, compactness or continuity statement. and are abstract functions satisfying Assumptions 7.1, 7.2, 2.3 and 2.4, as in §7 of the paper. Under Assumption 2.2 the expectation-defined and of (2.2) satisfy these, so the goal implies the theorem as printed. Coercivity is Tendsto F (cocompact _) atTop. Solutions are maps constrained only on : uniqueness is agreement on , never ∃! over all functions. The field is evaluated only at , where Lean's (1 - exp 0)⁻¹ = 0 cannot interfere. ranges over WithTop ℝ≥0 ( is and selects ), and over WithTop ℝ. The solution sets are -valued with the extension, as on p. 12, so positivity of is a theorem (Lemma 7.4), not an assumption.
A notion of solution without the differential equation, with it only away from on a set like , or with a derivative not tied to would make existence trivial. The definitions here require at every , continuity at and the exact initial value.
Mathlib provides Picard–Lindelöf, Grönwall-type bounds and Arzelà–Ascoli, but no Cauchy–Peano theorem; a reusable Peano existence theorem with maximal-interval extension would be a valuable contribution beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of the goal.
A McKean–Vlasov or mean-field stochastic differential equation is an SDE whose coefficients depend on the law of the solution itself. Such equations describe the limit of large systems of weakly interacting particles (Kac's kinetic models, McKean's propagation of chaos) and are the state dynamics of mean-field games and mean-field control. For a classical diffusion the expectation of a terminal payoff is a function of time and state and solves a linear parabolic PDE (the Feynman–Kac connection). For a mean-field diffusion the same expectation depends on time, on the state and on the current law of the population, so the associated PDE lives on , an infinite-dimensional space of probability measures. Buckdahn, Li, Peng and Rainer (arXiv:1407.1215, Ann. Probab. 2017) prove that this value function is the unique classical solution of its PDE, using the derivative with respect to measures introduced by P.-L. Lions in his Collège de France lectures.
Timeline. McKean (1966) introduced the equations; Sznitman (1991) gave the propagation-of-chaos theory. Buckdahn, Djehiche, Li and Peng (2009) and Buckdahn, Li and Peng (2009) studied mean-field backward SDEs and the associated PDEs in a form where the law enters only through the coefficients. Lions (2007–2012 lectures, notes by Cardaliaguet 2013) introduced differentiation on through lifts to . Carmona and Delarue (arXiv:1303.5835, 2013; arXiv:1404.4694, 2014) developed the Itô formula on the Wasserstein space and the master equation for mean-field games. The present paper (2014) proves the classical-solution result for the decoupled forward equation under second-order regularity of the coefficients in .
Let be a complete probability space carrying a -dimensional Brownian motion , let , and let be a sub--field independent of that is rich: every is the law of some . Here is the set of probability measures with finite second moment, with the 2-Wasserstein distance , the infimum over couplings of and . The filtration is .
Given Lipschitz coefficients , , a time , and , the processes and solve on
The second process depends on only through , so for the value function is a function on .
A function has Lions derivative if its lift on is Fréchet differentiable with derivative . The classes and ask for one or two such derivatives (together with derivatives in and in the extra variable ), all bounded and Lipschitz. Hypothesis (H.2) asks that and be bounded and that every component be in .
Under (H.2) and , belongs to and is the unique solution in that class of
The goal also records that does not depend on the choice of with a given law.
In the order the proof uses them: the second-order expansion on (Lemma 2.1); symmetry of mixed derivatives (Lemma 4.1); the substitution identity and flow property (3.4)–(3.5); the stability estimate (Lemma 3.1) and its consequence that depends only on (Remark 3.1); first- and second-order regularity of in (Lemmas 5.1, 5.2) and in (Lemma 6.1); the mean-field Itô formulas (Proposition 6.1, Theorem 6.1); the martingale identity (6.15); and uniqueness (6.19)–(6.20). A companion theorem states the existence and pathwise uniqueness of solutions of both SDEs under Lipschitz coefficients.
The result is a Feynman–Kac representation on the Wasserstein space: it identifies the expectation functional of a McKean–Vlasov diffusion with the unique classical solution of a second-order PDE in , of the type that appears as the master equation of mean-field games and as the dynamic-programming equation of mean-field control. It gives a mean-field Itô formula for functions of the state and of the law, which is the basic tool for verification arguments in these problems.
All results of the mission are proved in the paper, which takes the well-posedness of the SDEs from Carmona and Delarue. None is formalized: the platform has the Itô integral as an definition, but no Itô isometry, no Burkholder–Davis–Gundy inequality, no SDE existence theorem and no Itô formula (the classical Itô formula is posed separately as an open goal). Formalizing the mission produces a calculus on in Lean, together with existence, stability and flow results for McKean–Vlasov equations.
The obvious route, differentiating in by the chain rule, fails because is not a map between finite-dimensional spaces: the measure derivative of requires Fréchet differentiability of in , the identification of the derivative through a family of auxiliary linear SDEs indexed by a point , and estimates uniform in . A second difficulty is that the second-order expansion on has remainder of order , not , so the Itô formula is not a direct Taylor argument in and needs a partition argument with control of each increment. A third is regularity in time: is differentiable in only after the Itô formula has been applied to , and the time derivative must again be bounded and Hölder. The paper writes its proofs for and and leaves some estimates to the reader, so a solver must supply them.
Time is ℝ≥0, is EuclideanSpace ℝ (Fin d), measures are Measure (E d), and every condition on a measure argument is quantified over only. is the real value of the published WassersteinDRO.Duality.wassersteinDistance 2, finite on . Brownian motion, the Brownian filtration and the Itô integral are the published Peng1990.SMP objects, and the null sets are ReflectedBSDE.Existence.nullSigma. The standing assumptions of §3 are hypotheses of every statement: completeness, , independence of and , richness of , and the Lipschitz condition (stated even where (H.2) implies it). Matrices carry the Frobenius norm.
Solutions of (3.1) and (3.2) are processes in satisfying the integral equation at every almost surely, with for Itô integrals of . Statements about take solution families as hypotheses; the companion well-posedness theorem states that such families exist, and a sanity file shows that zero coefficients with constant solutions and satisfy every hypothesis. The decoupled equation takes a random initial value, so (3.4) needs no measurable selection in .
Derivatives in , and are genuine (HasGradientAt; HasDerivWithinAt on , one-sided at the ends). Derivatives in are witness functions with the Fréchet property of the lift, the lift being taken on the paper's own rich space; this rules out the trivializing reading in which every function is differentiable because the underlying space carries only Dirac laws. The subscript bounds the derivatives, not the function, except that (H.1)/(H.2) also require and themselves to be bounded on : this is the of (H.1) ii), read uniformly in as the paper's proofs use it, and without it the bounded time derivative of fails (e.g. ). The class additionally requires the derivatives entering the Itô formula to be jointly continuous in for ; this is the reading of the letter , and satisfies it. over an independent copy is the integral against the corresponding law. Where the page writes or without , the bounded classes the paper defines are used. The uniqueness statement ranges over every function of the class with its own derivatives.
A complete development needs the Itô isometry and BDG inequality for the published integral, Gronwall's inequality, strong existence for McKean–Vlasov SDEs, -differentiability of SDE solutions with respect to the initial condition, and a classical multidimensional Itô formula. The Lions-derivative calculus and the Wasserstein estimates are reusable for any mean-field mission. Contributions to any of these pieces are welcome.
In ordinary statistical learning, a hypothesis is chosen from training data drawn from a distribution and judged by its risk under that same . In practice the test distribution often differs from the training one: covariate shift, domain drift, adversarial perturbation of inputs. Distributionally robust learning replaces the risk at by the worst risk over a neighbourhood of . When the neighbourhood is a ball in a Wasserstein distance, the perturbed distributions may move mass to nearby points of the instance space rather than only reweight the observed ones, which makes the model a natural description of small domain drifts and adversarial perturbations (Esfahani–Kuhn 2018, Gao–Kleywegt 2016, Sinha–Namkoong–Duchi 2018).
Lee and Raginsky (NeurIPS 2018) asked whether minimising the empirical version of this worst-case risk learns: does the empirical minimiser come close, in worst-case risk, to the best hypothesis of the class, at the usual rate? Their §3.2 answers yes when every hypothesis is uniformly Lipschitz. Their §3.3, the subject of this mission, removes that assumption: one hypothesis with controlled growth is enough.
The instance space is a Polish metric space with metric and Borel -algebra; fix . For Borel probability measures on , the -Wasserstein distance is
the infimum over couplings of and . For a radius , is the Wasserstein ball around .
A hypothesis is a function , read as a loss; a hypothesis class is a set of them. The risk of under is . The local worst-case risk and the local minimax risk are
Given i.i.d. samples with empirical distribution , the local minimax ERM is
The standing assumptions are:
The complexity of is measured by the entropy integral , where is the covering number of in the uniform norm.
Under Assumptions 1, 2 and 4, for every , with probability at least ,
The goal carries the paper's constants. The mission does not ask for sharper constants; a proof of the stated bound closes it.
The result. Theorem 3 is a generalisation guarantee for Wasserstein distributionally robust ERM that needs no uniform smoothness of the class. The uniformly Lipschitz assumption of the companion Theorem 2 fails for most classes of interest when : a function with is constant (p. 6). Assumption 4 holds, for example, for regression with quadratic loss whenever the predictor class contains the zero predictor (p. 6). The second term of (11) decreases as grows, which quantifies how a larger ambiguity set screens out non-smooth hypotheses (Remark 4).
Formalizing it. The theorem has a published pen-and-paper proof (Appendix C.5 of the arXiv version); it has no machine-checked proof. A formalization produces machine-checked statements of the dual characterisation of Wasserstein worst-case risk on a bounded Polish space, of a symmetrization-plus-McDiarmid uniform deviation bound for a parametrised class, and of a Dudley-entropy bound on a product class. The proof (C.5) on p. 16 starts from an achiever of , which need not exist; the goal is stated without that assumption, so a complete proof also handles the infimum.
The obvious argument decomposes the excess risk through and bounds by a uniform deviation over . That step fails: is a supremum over a ball of measures, not an expectation, so it is not an empirical process in . Passing to the dual makes it one, but the dual multiplier depends on the sample and has no a priori bound, so the class over all is too large. Without uniform smoothness of there is no obvious a priori bound on , and the entropy of the resulting two-parameter class must still be controlled at rate . Strong duality itself (Proposition 4) needs the existence of optimal couplings and a measurable-selection argument on a Polish space; it is not in Mathlib.
MetricSpace with BorelSpace and PolishSpace instances; Assumption 1 is Bornology.IsBounded (Set.univ : Set 𝒵), and is Metric.diam Set.univ. Throughout, and (the paper's standing choice, p. 3).WassersteinLinOpt.Ball.wassersteinDist and wassersteinBall, which range over all Borel probability measures; on a bounded space this equals the paper's ball.The following formalizations would trivialize the goal and are ruled out: a bound for each fixed in place of ; an defined by Classical.choose of an unproved existence; a supremum over all measures instead of over the ball; and the real conversion of an infinite .
The infrastructure is reusable beyond this mission: Wasserstein strong duality on Polish spaces (Proposition 4 specialises the general optimal-transport duality of Blanchet–Murthy 2019, whose transport-plan form is a proved theorem on the platform as ModelRiskOT.Duality.theorem_1); Dudley's entropy bound for sub-Gaussian processes indexed by infinite classes; and McDiarmid's inequality for suprema of empirical processes. Contributions of these general tools, as separate theorems, are welcome. Source: the arXiv v2 preprint, which is the NeurIPS 2018 camera-ready text followed by the supplementary appendices.
Distributionally robust optimization (DRO) replaces the expected loss of a decision under a baseline distribution by its worst case over all distributions that are close to . When closeness is measured by an optimal transport cost, the worst case over this infinite-dimensional ball has a one-dimensional dual: by Theorem 1 of Blanchet, Murthy and Zhang (arXiv:1810.02403v3, Math. Oper. Res. 47(2), 2022), building on the strong duality of Blanchet and Murthy (arXiv:1604.01446),
The robust problem thus becomes a joint minimization of the dual objective over . Whether that minimization is a convex program, and on which set the objective is finite, decides whether first-order methods such as the stochastic gradient schemes of the same paper apply at all. This mission formalizes the paper's answer, Theorem 2.
The data take values in with law , a Borel probability measure. A decision is a vector in a convex set , the loss is for , and is the transport budget.
The transport cost is the state-dependent Mahalanobis cost for a map from to positive definite matrices. Assumption 1: is lower semicontinuous (1a), and for -almost every , with (1b). Write .
Assumption 2: is convex, its growth exponent
is finite, and .
For , and define, as in display (7),
the robust loss , its set of maximizers , and the dual objective
The effective domain is , and with the threshold the paper sets and inside .
Under Assumptions 1 and 2, is proper and convex: on ; for each some has ; and for , ,
Lemma 3 is stated with constants depending only on (and the fixed data), as its proof produces them and as the paper's later arguments integrate bound (b) over .
Theorem 2 is the structural fact behind the paper's algorithms: with Theorem 1 it turns a minimax problem over probability measures into a convex minimization in real variables, on which the paper's strong convexity results (Theorems 3–5) and its stochastic gradient schemes are built. Lemma 1 identifies the effective domain up to its boundary, which tells an algorithm where the dual multiplier must lie, and Lemma 3 gives the growth control of the robust loss used throughout the appendix.
The results are proved in the paper; none of them has a machine-checked proof. The mission produces a Lean statement of the dual objective as an extended-real integral and of its convexity and properness, reusable by the other missions of this series (strong convexity near the optimizers, worst-case distributions, comparative statics in ), and contributions of formal proofs of the milestones and the goal.
The objective takes the value on part of its domain: Lemma 1(b) shows that below the threshold, so the naive reading " is a real convex function" is false, and convexity must be handled for functions with values in , including the conventions at the endpoints of the segment. Properness requires a bound on that is integrable in , so the constants of Lemma 3 must not depend on ; a bound that is only pointwise finite does not suffice. The identity (25) relates a supremum over to a supremum over through a change of the dual variable, and the two multipliers must be kept apart. Finally, the expectation in is an integral of an extended-real function whose measurability is not assumed but has to be derived from Assumption 1.
is EuclideanSpace ℝ (Fin d) and parameters live in EuclideanSpace ℝ (Fin d) × ℝ. is an EReal supremum; is the published ModelRiskOT.Duality.extIntegral, with lower Lebesgue integrals. is a real infimum and uses the real essential supremum; both are used only under Assumptions 1–2, which make them meaningful. Convexity of extended-real maps is written as the explicit inequality in EReal, since ConvexOn does not apply.
Standing assumptions carried by every statement: a probability measure, , convex (the paper's standing assumption). Conventions committed to: "for any " in Lemmas 1–2 is every , not almost every; Lemma 2 assumes only Assumption 1a and the convexity of ; the identity (25) is stated with the old multiplier written as ; the typo "" in Lemma 1 is read as ; the goal's "finite somewhere" is stated for each , so the goal is vacuous only when . The fourth-moment condition of Assumption 2 is kept as printed.
A trivializing formalization is ruled out: "proper" is not encoded as "finite everywhere" (false by Lemma 1(b)), and pointwise convexity of (Lemma 2) is a milestone, not the goal, which is about the expectation .
A complete development needs: positive definite matrices and the quadratic minimization behind (25); continuity of convex functions and growth bounds; lower Lebesgue integrals of extended-real functions and their monotonicity and additivity; measurability of a supremum over of continuous functions. The definitions layer is shared with the other four missions of this series. Proofs of any milestone and of the goal are welcome.