Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Optimal portfolio liquidation asks how a trader should unwind a position of shares over a horizon when trading moves prices. Since Almgren and Chriss (2001) the standard model charges a quadratic cost for trading at rate (temporary impact) and a risk penalty on the open position, and imposes the liquidation constraint . When many traders liquidate at once, each one's costs also depend on the others' aggregate trading rate through a permanent impact term . Fu, Graewe, Horst and Popier (arXiv:1804.04911) model this as a mean field game (MFG) with common noise and prove that, under a weak-interaction condition, the game has a unique equilibrium.
The liquidation constraint makes the problem singular: the value function blows up at , and the equilibrium is described by a forward-backward system whose decoupling field satisfies a Riccati BSDE with terminal value . A natural question is whether the constraint can be replaced by a finite penalty on the unliquidated position, a non-singular problem of the type studied in the MFG literature, and whether the penalized equilibria approach the constrained one as . Section 4 of the paper answers this at the level of values. In the single-agent case, singular terminal conditions of this type were studied by Ankirchner, Jeanblanc and Kruse (SIAM J. Control Optim., 2014) and Graewe, Horst and Séré (Stochastic Process. Appl., 2018), references [3] and [28] of the paper.
Fix , an -dimensional Brownian motion whose first coordinate is common noise, and an initial position independent of . Let be the filtration of and that of , both augmented. The coefficients are bounded, nonnegative, -progressive processes, with and bounded below by positive constants. Write , , for the essential supremum of and the essential infima of and , for the essential supremum of , and . Assumption 2.3 adds the weak-interaction condition: some satisfies and .
Given an aggregate rate , a trading rate yields the position . The constrained problem minimizes
over with ; its value is . The penalized problem (4.1) drops the constraint and minimizes
over all , with value . An equilibrium is a fixed point .
The constrained equilibrium is given by the FBSDE (2.3), , , , , decoupled as where
The penalized equilibria are given by the FBSDE (4.2) with , decoupled by , the solution of the same Riccati BSDE with . The solutions live in weighted spaces: with norm , and the penalized analogue with weight . Assumption 4.1 requires a constant with for all , almost surely.
Under Assumptions 2.3 and 4.1, with the constrained equilibrium and the penalized ones,
The result is a consistency statement between two models of liquidation. Penalized models are what a numerical scheme or a standard MFG solver can handle, since their FBSDEs have finite terminal data. Theorem 4.6 says that equilibrium values computed with a large penalty approximate the value of the hard-constrained game, and Lemma 4.5 says the same for positions and trading rates. Without it, a penalized model would be an unrelated object rather than an approximation of the constrained one.
The result is proved in the paper; it is not formalized anywhere. A machine-checked development would need, beyond the paper, the theory of quadratic BSDEs with finite and singular terminal values, conditional mean-field FBSDEs with common noise, and conditional essential infima of control problems. The milestones isolate reusable pieces: the monotone approximation of a singular Riccati BSDE (Lemma A.3) and uniform estimates in -dependent weighted spaces (Lemma 4.4).
The obvious argument compares the two problems control by control: the constrained optimizer is admissible for the penalized problem, so up to the change of . The reverse inequality is where it fails. The penalized optimizer leaves a residual position , and its cost has to be compared with the singular one, whose weight explodes at . Controlling this requires estimates uniform in in spaces whose weights degenerate as , and the bare exponent of the constrained problem is not enough to make the boundary terms vanish. Assumption 4.1, which upgrades the state to , is what closes the gap. In addition, the aggregate rate changes with , so both the controls and the cost functional move at once.
Time is ; processes are real-valued functions of ; is the -dimensional with coordinate the common noise. Stochastic integrals and BSDEs come from the published definition Peng1990.SMP.Stochastic. BSDEs on are imposed on every , ; is a.s. Conditional expectations inside drivers are -progressive versions of integrable processes. Weighted norms are computed in . The explicit readings are:
A trivializing formalization would quantify over all solutions of the penalized MFG (claiming a uniqueness the paper does not state) or define by a pointwise infimum over all controls (which is or junk); both are ruled out above. Contributions toward BSDE comparison principles and quadratic BSDE well-posedness on this stochastic-integral layer are welcome and reusable.
A trained feed-forward neural network with ReLU activations, , is a piecewise linear function of its input. Many tasks ask for an optimization over such a network with its weights held fixed: verifying that no small perturbation of an image changes its classification, finding adversarial examples, or embedding a learned model of demand or cost inside a decision problem ("predict, then optimize"). The standard way to solve such problems exactly is mixed-integer programming (MIP): each neuron is written as a small set of linear constraints with one binary variable, and the network is the composition of these neuron formulations. How strong each neuron formulation is decides how fast branch-and-bound can close the gap.
The formulation used in the literature up to 2018 is the big-M formulation. It is valid but weak. This mission formalizes the main result of Anderson, Huchette, Tjandraatmadja and Vielma, IPCO 2019 extended abstract (arXiv:1811.08359v2), which gives the strongest possible formulation of a single ReLU neuron that uses the original variables and one binary variable only.
Timeline. Big-M formulations of ReLU networks were used by several groups in 2017–2018 for verification and adversarial analysis (see §1.2 of the paper). Balas's disjunctive programming (1985, 1998) and the multiple choice formulation of piecewise linear functions (Vielma and Nemhauser, Math. Program. 2011) give an ideal formulation of the neuron that needs a copy of the input variables. Anderson et al. (2019) project out that copy and obtain the formulation (6) below; a longer journal version (Math. Program. 2020, with W. Ma) develops the analysis further, including interactions between neurons.
Fix , a weight vector , a bias , and bounds with for every . The neuron computes for the affine function on the box . Its graph is
The sign-adjusted bounds are , when , and , when . Then and are the maximum and minimum of on , and . Strict activity means : the neuron is neither always off nor always on. The paper assumes throughout that and that strict activity holds.
A set of points with , read together with the constraint , is a formulation of the graph if lies on the graph exactly when for some ; is then its LP relaxation. The formulation is ideal if every extreme point of has .
The big-M formulation (3) is , , , . The formulation of Proposition 1 is
Proposition 1 says that the convex hull of the graph, lifted with one binary variable, is described by (6a), (6b) and the bounds, with no auxiliary continuous variables. Optimizing a linear function over the LP relaxation of (6) therefore gives the tightest convex relaxation available for a single neuron, and Proposition 3 gives a separation routine linear in , so the exponential family can be added on demand to a big-M model. The paper's experiments (§3, not formalized) report that separating over (6b) solves smaller MNIST verification instances faster than Gurobi's default cut generation by a factor of 7.
The result is proved in the paper; nothing here is open. To our knowledge none of these statements has a machine-checked proof. The work this mission asks for is the formalization of the known proof: an ideality statement for the multiple choice formulation, a Fourier–Motzkin projection carried out for an arbitrary index set with general-sign weights, and the passage from a hull identity to integrality of extreme points.
The formulation half of Proposition 1 is a short case analysis on ; the content is ideality. The obvious attempt, characterizing the extreme points of the LP relaxation of (6) directly, is impractical: the polytope is cut out by inequalities, and showing that every point with fractional is a proper convex combination of feasible points means handling all patterns of tight inequalities of (6b) at once. Ideality of the extended formulation (5) is classical and passes to its projection onto , but that only helps once the projection is known to be exactly the LP relaxation of (6): it has to be computed for an arbitrary index set, and every inequality it produces must be shown to be one of (6a), (6b), the bounds, or implied by them. Weights of both signs must be handled throughout: the page treats negative weights by a change of variables, and a formal development has to carry the sign-adjusted bounds through every step.
Inputs are Fin η → ℝ, so indices are 0-based; points are (Fin η → ℝ) × ℝ × ℝ. A formulation is encoded by its LP relaxation (with ) and the predicate " iff for some "; ideality is ∀ p ∈ Set.extremePoints ℝ R, p.2.2 = 0 ∨ p.2.2 = 1. are defined by their closed forms, and a companion theorem proves that they are the maximum and minimum. In (6b) and (7c), "" ranges over all indices outside , zero weights included. The system (7) is stated with , i.e. after undoing the page's substitution ; for it is the page's display. The LP relaxation of (5) is represented both in its lifted space and projected to , with the copies quantified existentially in the latter, and constant is scaled by in (5b) and by in (5c).
The goal carries both standing assumptions of §1.3 ( and strict activity) and nothing else. Milestones that do not need strict activity omit it, which makes them stronger. Example 2 includes the page's boundary: although its box then violates when , the example's three stated claims remain true.
Ideality is a statement about the LP relaxation, not about the set with : applied to the latter it would hold trivially, and a goal stating only that (6) is a formulation would omit the result's content. Both are ruled out by the statement of the goal.
A complete development needs: extreme points and convex hulls of polyhedra in product spaces (Mathlib), the hull of a union of two polytopes as a projection, Fourier–Motzkin elimination over an arbitrary finite index set, and finite-sum manipulations over subsets of . The Fourier–Motzkin and disjunctive-hull lemmas are reusable well beyond this mission; contributions of either are welcome, as are proofs of the companion results.
Source: the IPCO 2019 extended abstract, arXiv:1811.08359v2 (28 Feb 2019); all labels and pages refer to that version.
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 constraint satisfaction problem (CSP) asks whether variables can be assigned values so that every constraint, drawn from a fixed finite set of relations, holds. The algebraic approach to CSPs explains their complexity through polymorphisms, the operations that preserve all constraint relations; this programme culminated in the CSP dichotomy theorem of Bulatov and Zhuk (2017). A promise CSP (PCSP) pairs each relation with a weaker relation : given an instance that is promised to be satisfiable with the -constraints, one must distinguish it from instances that are not even satisfiable with the -constraints. Approximate graph colouring (is a 3-colourable graph 100-colourable?) and -SAT are PCSPs, and their complexity is not captured by the classical theory.
Brakensiek and Guruswami (arXiv:1704.01937) developed the polymorphism theory of PCSPs and classified the Boolean, symmetric, folded case.
Timeline.
Fix the Boolean domain . A promise relation of arity is a pair with , and a family is a finite set of promise relations, possibly of different arities. A function is a polymorphism of if, whenever , applying coordinate-wise gives a tuple in ; is the set of functions that are polymorphisms of every member of .
A relation is symmetric if it is closed under permuting coordinates. Every symmetric relation has the form , where is the Hamming weight. A function is folded if , and idempotent if and ; a family is folded (idempotent) if all its polymorphisms are. For odd the paper singles out three function families:
and their negations . Finally, is -fixing if some set of at most coordinates satisfies whenever vanishes on .
Let be a finite, folded, symmetric family. If there are odd with
then
No value of is fixed: the goal asserts only that one bound works for all arities.
The milestones follow the paper's proof:
Theorem 4.13 is the structural half of the paper's main dichotomy (Theorem 2.16): a folded symmetric Boolean PCSP is polynomial-time solvable if it has one of the six families as polymorphisms for every odd arity, and NP-hard otherwise. Hardness follows by feeding the -fixing structure into a Label Cover reduction (Theorem 5.3). Bounded "fixing" or junta-like structure of all polymorphisms is the standard route from algebra to NP-hardness for PCSPs. This theorem is the cleanest Boolean instance of it, and it underlies later classifications of symmetric Boolean PCSPs.
The result has been proved and published since 2018. To our knowledge none of it has been formalized. A formalization supplies a checked Boolean polymorphism toolkit (Hamming-weight relations, folding, idempotence, relaxations), checked closure computations under alternating-threshold and majority operations, and a uniform-constant Frobenius-type lemma. All of these can be reused by other Boolean PCSP missions.
The obvious argument fixes a polymorphism and bounds its relevant coordinates directly from a constraint that , or violates. This gives a bound that depends on the arity , and an -dependent bound is trivial ( always works). The work is in making the constant uniform. The proof has to replace by a single canonical promise relation that does not depend on , classify exactly which symmetric relations exclude and , and use an additive-combinatorics lemma whose constants depend only on that relation's arity. Its bounded version must hold with the same constants. The non-idempotent polymorphisms need a separate reduction through the negated family .
The domain is Bool (false ). A family is a pair of relational structures 𝔸 𝔹 : RelStruct τ ar Bool from the published definition PCSPBLPAff_Symmetric_Setting, with [Fintype τ] (finitely many relations) and 𝔸.rel R ⊆ 𝔹.rel R (promise). IsPolymorphism 𝔸 𝔹 f from that file is Definition 2.4. Coordinates are Fin L, so the 1-based sign of becomes . Anti-functions negate the output. Family properties (folded, idempotent, non-degenerate) quantify over polymorphisms of every arity . A folded or idempotent family has no nullary polymorphisms, so admitting changes nothing. The constants , , and are quantified before the arity and the function (respectively before ). A statement that lets the constant depend on or is trivially true and is not the goal.
Out of scope are the complexity conclusions: "PCSP() is NP-hard" (Theorems 2.16 and 5.3) and item 2 of Lemma 2.13 (transfer of tractability). The cited inputs for those conclusions are also out of scope: the PCP theorem with parallel repetition (Proposition 5.2) and Schaefer's theorem. No complexity predicate appears in any statement.
A complete development needs the following, with Mathlib's Nat.frobeniusNumber as a starting point for Lemma 4.9:
Contributions are welcome at any milestone, including separate proofs of the closure computations and of Lemma 4.9.
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.
Brands are routinely held responsible for the labour and environmental practices of their suppliers. A brand that is linked in public to a non-compliant supplier loses consumer willingness to pay, and firms answer this risk by auditing their suppliers. Supply networks are not trees, however: one supplier often serves several competing brands. Chen, Qi and Dawande (SSRN 2889889, Manufacturing & Service Operations Management, 2020) ask how the position of a supplier in such a network, and in particular its centrality (the number of buyers it serves), affects which suppliers get audited when buyers decide on their own, and when they audit jointly.
This mission formalizes the paper's answer for unilateral auditing by competing buyers (Sec. 4.2, Proposition 2). A companion mission treats joint auditing (Proposition 3).
Two buyers source from three suppliers: an independent supplier for each buyer , and a common supplier that serves both. Each supplier complies with social-responsibility standards with probability . In stage 1, buyer chooses an auditing effort on and on , and audits at most one of them: . Auditing a supplier with effort costs , with a fixed cost and ; effort means no audit and costs nothing.
A non-compliant supplier that passes the audits is discovered in public with probability . Hence causes damage to with probability , and causes damage to both buyers with probability , independently. A buyer with at least one exposed supplier suffers the MWTP damage : his demand intercept drops from to . Each exposed supplier is then paid per unit instead of , so a buyer with exposed suppliers has unit cost .
In stage 2 the buyers compete in quantities with inverse demands , (Dixit 1979; Singh and Vives 1984). Its equilibrium profit for is , in closed form (Lemma 1). Buyer 's ex ante expected profit is the expectation of over the eight damage outcomes, minus his audit costs; is symmetric. Three conditions on (p. 8) make all stage-2 quantities positive.
An equilibrium is a profile , , in which each buyer's strategy is a best response to the other's, with the tie-breaking rule of p. 10: a buyer who is indifferent between auditing and not auditing does not audit. Two explicit efforts, (eq. (1)) and (eq. (2)), are rational functions of the parameters; is a buyer's optimal effort on his independent supplier when the rival audits nobody, and is the symmetric solution when both audit their independent suppliers.
Assume and . There exist such that for every , writing , , , ,
In every equilibrium the common supplier receives zero effort.
Lemma 1 (stage-2 equilibrium), the OA.2 expected-profit display, the best-response function (OA-9) with and as its values, the dominance inequality (OA-11), Lemmas OA5 and OA6 (the two kinds of auditing equilibria and their threshold ranges), the monotonicity facts (OA-14)–(OA-15), Lemma OA7 (the order of the thresholds) and Lemma OA8 (no equilibrium audits ). The thresholds of the milestones are the explicit ones the proof defines in (OA-10), (OA-12), (OA-13).
The result separates network position from competition. Without downstream competition (, Proposition 1) there is a Pareto-dominant equilibrium in which one buyer audits the common supplier. With competition, Proposition 2 shows that the common supplier, the most central and therefore the most consequential source of risk, is never audited: auditing it would also protect the rival, who free-rides. This inefficiency is what motivates the paper's analysis of joint auditing (Proposition 3) and of social welfare (Proposition 4).
The result is proved in the paper, partly by omission: the e-companion leaves the proof of Lemma OA8 and the case to the reader. No machine-checked version exists. A formal proof would give a complete case analysis of a two-stage game with a discontinuous fixed cost, a constrained strategy set and a tie-breaking rule, and would check the paper's closed forms, several of which are printed with small slips.
The first-order conditions alone do not determine the equilibria. The fixed cost makes each buyer's payoff discontinuous at zero effort, so every candidate must be compared with no audit, and the best response is a choice among three regimes (audit , audit , audit nobody). Uniqueness claims therefore require excluding every profile in the constrained strategy set, including those where a buyer audits the common supplier, for which the paper gives no proof. The threshold comparisons rest on monotonicity in the rival's effort, and the expected profit is multilinear in the four efforts (plus the quadratic audit costs), with coefficients that are differences of squared Cournot quantities whose signs depend on the p. 8 conditions.
All objects live in the namespace SupplierAudit.Competition. The source is the authors' accepted manuscript on SSRN (2889889); main-text printed pages equal PDF pages, and e-companion page ec is PDF page .
Params carries and the standing assumptions , , , , , and the three conditions of p. 8. The theorems add (competition, Sec. 4.2). is a separate real argument and the goal quantifies over .CournotDuopoly). The model's stage-2 profit is the closed form for all ; Lemma 1 states that it is the game's unique equilibrium.A formalization in which equilibrium is plain Nash, efforts range over all of , a buyer may audit both suppliers, or "interior" is a hypothesis on the equilibrium efforts themselves would state a different (and in places false or vacuous) theorem; these are ruled out by the definitions above. Proofs of any milestone are welcome, as is reusable infrastructure for linear Cournot duopolies and for finite expectations over independent Bernoulli events.
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 .
Best-subset selection with ridge shrinkage, , is a mixed-integer program that statisticians want to solve to certified optimality at the scale of modern data ( up to features). Hazimeh, Mazumder and Saab (arXiv:2004.06152, Mathematical Programming 2022) built a branch-and-bound solver, L0BnB, whose node relaxations are solved in the primal space by active-set coordinate descent instead of by an interior-point method. Branch-and-bound prunes a node only with a valid dual bound, a certified lower bound on the node's relaxation value. A primal method returns an approximate minimizer, not such a bound, so the solver must turn an inexact primal point into a dual feasible point and needs to know how much is lost in doing so. This mission formalizes the paper's answer, its main theorem (Theorem 3).
Data are with columns , , and parameters . The reverse Huber penalty is for and for . The penalty equals if and otherwise. The reduced relaxation (5) is
Throughout, the columns of and have unit norm (the standing assumption of Section 3 of the paper).
Algorithm 2 (active-set coordinate descent) returns a point in the box such that the set
is empty: no coordinate outside the support wants to move. Write , , and let be an optimal solution of (5) with . The primal gap is .
The two duals of (5) (Theorem 2 of the paper) are, with ,
the latter under . The dual variables built from are , and . The dual points built from are , with a maximizer of (25) and a maximizer of under the constraints (27).
If , with when and when ,
If ,
The paper states these as (29) and (30); the goal states the expressions its proof establishes.
In the order the proof uses them: the closed-form coordinate updates (14) and (15); Proposition 3, ; the bound ; Lemma 2, which bounds coordinate by coordinate and makes it vanish off the support; inequality (53); the closed form (28) of ; the optimality conditions (58); the bound (57) on the support; and inequality (56).
The result. In both regimes the loss of the dual bound is controlled by the primal gap times the sparsity of the iterate, with constants depending only on and ; the number of features does not enter. Since L0BnB seeks solutions with , the cheap dual bound obtained from an inexact primal solution is nearly as good as the exact one, which is what allows pruning without an interior-point solve at every node. The paper notes that with plain coordinate descent in place of Algorithm 2 the same argument gives in place of .
Formalizing it. The result is proved in the paper; it has no machine-checked proof. The mission produces a checked version of the main theorem with explicit constants, a formal model of what "output of an active-set method" means for the analysis, and reusable closed forms for the boxed soft-thresholding updates of an - or reverse-Huber-penalized box-constrained least squares problem.
The bound is not a consequence of weak duality alone: weak duality says only that each dual value is below the primal optimum, and says nothing about how far the constructed dual point is from the dual optimum. The obvious estimate, a Lipschitz bound on or summed over all coordinates, gives a loss proportional to . Getting instead requires showing that the dual contribution of every coordinate outside vanishes exactly, which uses the emptiness of through Proposition 3 and the closed forms (14)–(15) of one-dimensional nonsmooth box-constrained problems. On the support, the loss must be bounded using the structure of and at coordinates where hits the box, which is where and (58) enter.
Indices are Fin p; norms are explicit sums; is Real.sign with ; is max a 0. The unit norms of the columns of and of are hypotheses, never built into the definitions, and each theorem assumes only the ones it uses. is any point of the box minimizing over the box. The output of Algorithm 2 is modelled by its two properties used in the paper: and ("" encoded as " is not a minimizer"); the iterations are not formalized. and are arbitrary maximizers satisfying (25) and (27). The dual variables (23)–(24) are defined by their formulas; their optimality (Theorem 2, a separate mission) is neither assumed nor needed, and the goal is an inequality between explicit numbers.
Instantiations of . (29) is stated as (55): becomes with decided by . (30) is stated as (59): becomes . The proof's final rearrangement of (29), which counts instead of , is not used.
A formalization that takes , or , that drops the hypothesis , or that replaces the constants by an existential "" would be trivial or a different statement; the goal quantifies over every optimal , every box-feasible with and every maximizer , , with the explicit constants above.
Needed infrastructure: one-dimensional convex minimization on an interval with piecewise penalties, Cauchy–Schwarz for finite sums, and first-order optimality conditions for box-constrained composite problems. Proofs of any milestone are welcome independently.
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 learning algorithm picks a hypothesis from a dataset ; its generalization error measures how far the empirical risk the algorithm sees is from the population risk it is judged by. Classical bounds control this error through the complexity of the hypothesis space (VC dimension, Rademacher complexity) or through the algorithm's stability. An information-theoretic approach instead controls it through how much the output reveals about the data. Russo and Zou (arXiv:1511.05219) introduced this view for adaptive data analysis, and Xu and Raginsky (arXiv:1705.07809) turned it into a general framework for learning algorithms; the framework underlies a large later literature on mutual-information and conditional-mutual-information generalization bounds.
Expected-value bounds of the form say nothing about a single run of the algorithm. A learner usually needs the error to be small with high probability. This mission formalizes Xu and Raginsky's high-probability result, Theorem 3, which gives a sample size sufficient for with probability at least under an information budget.
Timeline. 2016: Russo and Zou bound the expected bias of adaptively selected statistics by mutual information, for finite hypothesis classes. 2016: Bassily, Nissim, Smith, Steinke, Stemmer and Ullman (arXiv:1511.02513) introduce the "monitor technique" to convert expected bounds into high-probability bounds for differentially private and stable algorithms. 2017: Xu and Raginsky adapt the monitor technique to mutual information, obtaining Theorem 3 and its byproduct Theorem 4.
There is an instance space with an unknown probability measure , a hypothesis space , and a nonnegative loss . A learning algorithm is a Markov kernel : it receives a dataset of i.i.d. draws from and outputs a random . The joint law of data and output is .
The population risk and empirical risk of are
The empirical-risk vector is . For random variables with joint law , the mutual information is , the Kullback–Leibler divergence from the joint law to the product of the marginals. The algorithm's information budget is .
A real random variable is -subgaussian if for all . The standing assumption is that , , is -subgaussian for every ; a loss with values in qualifies with .
If , then for any and , every sample size
the probability being under .
The result. Theorem 3 shows that a sample complexity polynomial in and logarithmic in , the same order as for a data-independent hypothesis (where Chernoff–Hoeffding gives ), still suffices for a data-dependent one, provided the information budget is small relative to . It requires only subgaussian losses, whereas the earlier high-probability bounds of differential privacy apply to bounded losses or bounded-difference functions. Since , any algorithm with small input-output mutual information (the Gibbs algorithm, noisy empirical risk minimization, adaptive compositions of such) inherits the guarantee. Theorem 4 improves Russo and Zou's bound on the expected absolute error.
Formalizing it. The result is proved in the paper; to the best of current knowledge no machine-checked version exists. The mission produces a Lean statement of the theorem with the correct domain of validity (see the scope section), and its proof will require a reusable layer of measure-theoretic information theory: mutual information of joint laws, its additivity over independent pairs, the data-processing inequality, a bound by the logarithm of the number of values of a discrete variable, and the Donsker–Varadhan route from mutual information to expectations of subgaussian functions.
The obvious argument fails at the step from an expectation to a probability. Markov's inequality applied to Theorem 4 gives a sample size of order , quadratic in . A union-bound or Chernoff argument per hypothesis does not apply, because depends on and the deviation at the selected hypothesis is not a sum of independent terms. The paper's route runs independent copies and selects the worst one; the delicate part is bounding the information the selection itself adds, which needs the chain rule and data processing for mutual information on general (non-discrete) spaces, and an expectation bound that holds uniformly over every selection rule.
Lean conventions:
Fin n → Z with law Measure.pi, taken from the published LearnStability.Characterization.Setting (sampleLaw, risk, empRisk); the algorithm is a Markov kernel; the joint law is sampleLaw μ n ⊗ₘ κ.HasSubgaussianMGF of the centred loss with variance proxy .I ≤ ENNReal.ofReal ε. Expectations of nonnegative quantities (, ) are lower Lebesgue integrals; Lemma B.2's signed expectation is a Bochner integral whose integrand is integrable under the hypotheses.Fin m; the sign is a Bool read through sgn.Two printed slips are corrected in the Lean and disclosed in the item notes: the proof of Lemma B.2 claims is -subgaussian under the product of marginals (false; the centred version is), and (B.6) bounds the negative of the quantity in (B.4) ((B.7) is still correct).
The hypothesis is , not the stronger , and the goal mentions neither the parallel copies nor the monitor; a formalization that strengthened the hypothesis, dropped the measurability of the loss (so that the law of collapses to the zero measure and every mutual information is ), or allowed would be a weaker, vacuous or false statement.
Welcome contributions: chain rule and data processing for klDiv-based mutual information, additivity over independent products, the bound for finitely-valued outputs, and the Donsker–Varadhan decoupling lemma; these are reusable across the series and beyond.
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.
Second order dynamical systems with vanishing damping are continuous-time models of accelerated first-order methods. The system is the continuous limit of Nesterov's accelerated gradient method (Su, Boyd, Candès 2016), and its trajectories converge weakly to a minimizer of a convex when (Attouch, Chbani, Peypouquet, Redont 2018). Two modifications of this system have been studied separately. A Hessian-driven damping term damps oscillations and keeps the fast rates (Attouch, Peypouquet, Redont 2016). A Tikhonov regularization term with selects one minimizer, the one of minimum norm, and can turn weak convergence into strong convergence (Attouch, Chbani, Riahi 2018).
Boţ, Csetnek and László (arXiv:1911.12845v2, Math. Program. 2021) study the system with both terms. Their results split into two regimes according to how fast decays. This mission covers the slow-decay regime of §4.1, where and the trajectory approaches the minimum-norm minimizer in a weighted average sense.
Timeline. 2016: Su, Boyd and Candès derive the continuous model of Nesterov's method. 2016: Attouch, Peypouquet and Redont add Hessian-driven damping (, ) and prove fast rates and weak convergence. 2018: Attouch, Chbani and Riahi add Tikhonov regularization without Hessian damping and prove, among other results, strong ergodic convergence to the minimum-norm minimizer when . 2020: Boţ, Csetnek and László combine both terms and extend that ergodic result (their Theorem 4.2).
Let be a real Hilbert space, , , , and . The data satisfy the paper's General assumption:
A global -solution of system (5) is a twice continuously differentiable with
The set is nonempty, closed and convex, so it has a unique element of minimum norm, the minimum-norm minimizer . For the Tikhonov approximation curve is
the unique minimizer of a strongly convex function. Finally, measures the distance of the trajectory to , with derivative .
If and , then every global -solution satisfies
No rate and no constant is asserted, so the goal does not depend on any particular choice of .
The result shows that slow Tikhonov regularization still selects the minimum-norm minimizer when Hessian damping is added: the weighted time average of tends to zero and the trajectory comes arbitrarily close to infinitely often. The hypothesis is only , well below the threshold that the paper needs for its fast rates, and no growth condition on beyond the divergence of is imposed. It complements Theorem 4.4 of the same paper (a separate mission), which reaches full strong convergence under fast decay, , plus further conditions.
On the formal side, the theorem and its milestones are proved in the paper and in the cited literature, but none of them has a machine-checked proof. The work splits into an energy estimate for a nonautonomous second order ODE in a Hilbert space (Lemma 4.1), two facts about the Tikhonov curve that underlie the whole theory of Tikhonov regularization of convex problems (milestones 2 and 3), an integrated differential inequality (46), and a l'Hospital-type averaging step. The Tikhonov-curve facts are reusable for any formal treatment of viscosity selection and minimum-norm solutions.
The obvious attempt, a Lyapunov function that decreases along the trajectory and controls , fails because is not a stationary point of the perturbed system: in general. The distance to therefore need not decrease, and pointwise convergence is not available under the slow-decay hypothesis alone. The comparison point has to move along the Tikhonov curve , whose convergence to comes without a rate. The available bound controls only a weighted integral of corrected by , so the passage from (46) to the goal needs both and the divergence of the weight. In the formal setting the Tikhonov-curve limit is itself a nontrivial weak-compactness argument in a Hilbert space, which the paper does not spell out.
InnerProductSpace ℝ H, CompleteSpace H). is gradient g, and is the Fréchet derivative of gradient g at applied to . "Twice Fréchet differentiable" means and are differentiable; Lipschitz continuity on bounded sets is stated on every closed ball around the origin.Filter.liminf, whose value on an unbounded function is a default. is boundedness from above of the image of , and membership is integrability on .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.
Approximating an unknown probability measure by the empirical measure of an i.i.d. sample is the basic operation of statistics, Monte Carlo integration, quantization and particle approximations of nonlinear PDEs. The natural way to compare with on is an optimal-transport cost, because it metrizes weak convergence together with convergence of moments. For many applications the mean of this cost is not enough: one needs to know how unlikely a large deviation is, for a fixed sample size .
The main consumer in operations research is data-driven distributionally robust optimization. Mohajerin Esfahani and Kuhn (Math. Program. 171, 2018) build Wasserstein balls around whose radius is calibrated so that the true distribution lies inside with probability ; their finite-sample guarantee (their inequality (7), quoted from this paper for ) is exactly a concentration inequality of the kind proved here. On Prove2Me that inequality appears as the hypothesis Concentration7 of WassDDRO.Consistency.Setting; Theorem 2 of this mission is the statement that discharges it.
Timeline. Bolley, Guillin and Villani (PTRF 137, 2007) proved concentration inequalities for on non-compact spaces, under assumptions that often included functional inequalities for , and for rather large deviations. Boissard (Electron. J. Probab. 16, 2011) gave bounds in for empirical and occupation measures. Boissard and Le Gouic (arXiv:1105.5263) and Dereich, Scheutzow and Schottstedt (Ann. IHP 49, 2013) studied the mean speed of convergence; the latter introduced the multiscale bound used here and obtained sharp moment estimates for a limited range of parameters. Fournier and Guillin (arXiv:1312.2128, 2013; PTRF 162, 2015) gave moment bounds for all and under a -th moment (their Theorem 1, mission I of this series) and the concentration inequalities of their Theorem 2, the subject of this mission, under integrability conditions only.
Fix and give the Euclidean norm . Let be a Borel probability measure on and i.i.d. with law . For the transport cost between probability measures is
where is the set of couplings, measures on with marginals and (no root is taken). The moment conditions use
The proof works with a multiscale distance . For let be the partition of into dyadic cubes of side . For measures on ,
For measures on one cuts space into the shells , , rescales each to (the measure ), and sums the compact distances with weights . Lemma 5 bounds by . The splitting separates the fluctuation of the shell masses, , from the fluctuation inside the shells, . A Poisson measure with intensity (a Poisson() number of i.i.d. points) and enter the compact case.
Assume or , and one of (1) with ; (2) with ; (3) with . Then for all , ,
with , or according as , , , and under (1), under (2), under (3). The constants depend only on , the parameters of the condition, the value of the moment and .
In attack order: Lemma 5 (the coupling bound ); Lemma 9 (Poisson moment generating function and tails); Proposition 8 (concentration for in the Poissonized compact case); Lemma 11 ( for ); Proposition 10 (the compact case of Theorem 2, ); Lemma 12 (binomial deviations); Lemma 13 (the tail of ); display (6) ().
The result. Theorem 2 gives, for every dimension and every in its range, a deviation inequality whose small- part has the same dimension-dependent exponent as the mean rate of Theorem 1, and whose large- part is governed only by the tail of . Under exponential moments the tail is again exponential; under a polynomial moment it is polynomial, which is the correct order. It is the input for finite-sample confidence radii in Wasserstein DRO, for non-asymptotic guarantees in quantization and for propagation-of-chaos estimates.
Formalizing it. The theorem is proved (2013, published 2015) and widely cited; no machine-checked proof of it, or of any rate for the empirical measure in transport cost, exists in Mathlib or on Prove2Me. The work is formalizing the known proof: Poisson and binomial concentration (Lemmas 9, 12), the local Poisson bound (Lemma 11), Poissonization and depoissonization (Propositions 8, 10), and the shell decomposition (Lemma 13, display (6)). Lemmas 9, 11 and 12 are general probability facts useful well beyond this paper.
The obvious route is a bounded-differences (McDiarmid) inequality for . On it is not available: moving a single sample point changes the cost by an amount that is unbounded, and the measures allowed here have only exponential or polynomial moments. Even on a compact set it bounds the deviation from the mean rather than from , so it gives nothing below the mean rate, and it does not see the dimension-dependent exponent of . The bound must hold at all scales of the dyadic decomposition simultaneously, while the cell counts of a multinomial sample are dependent, and in the non-compact case the masses of far-away shells, which are rare events, must be controlled with a tail that degrades exactly as the moment condition allows.
is EuclideanSpace ℝ (Fin d) with ; the Euclidean norm matters, since involves the diameter of . The sample is under the product measure , and is the published WassersteinDRO.Duality.empiricalDistribution; couplings are the published WassersteinLinOpt.Ball.couplings. Costs, moments, , , and expectations are valued in (lower Lebesgue integrals and -valued series), so no bound can hold through a junk value of a divergent integral. Probabilities are the product measure applied to the event. is represented by its law, a Poisson() mixture of i.i.d. samples, as on p. 13. Poisson and binomial laws are Mathlib's poissonMeasure and binomial.
Constants: in each of the three parts, the condition's parameters, the moment value (resp. ) and are fixed before , and come after. A formalization with fixed before the constants would be trivial (the constants could absorb ), and one stating the goal as the sum of the bounds for and would assume the proof; the goal mentions neither , , nor .
Departures from the print, each disclosed in the statements: the page writes for ; Theorem 2 opens with "" but prints only for , , , so it is posed for or ; Proposition 8's "" is relaxed to that range (its proof does not use , and Theorem 2 needs it for every ) (Proposition 10 is posed, as printed, for every ); Lemma 12 assumes and a positive success probability, without which (a) and (b) are false. "Supported in " is -null complement of .
The definitions of , , Notation 4 and Lemma 5 duplicate those of mission I of the series and are to be merged later. Contributions on Poisson and binomial concentration, and on transport costs between discrete measures, are reusable and welcome.
Manufacturers increasingly sell directly to consumers while continuing to supply independent retailers, a practice known as supply chain encroachment. The direct channel competes with the retailer for the same consumers, and the conventional advice for easing that conflict is to sell different products in the two channels. Ha, Long and Nasiry (MSOM 18(2), 2016; authors' manuscript SSRN 3970373) study this advice in a model where the manufacturer chooses product quality herself. This mission formalizes their Section 5: when the manufacturer may offer one quality directly and another through the retailer, which channel gets the better product, when is differentiation worth it, and who gains from encroachment.
The model builds on two lines of work. With exogenous quality, Arya, Mittendorf and Sappington (Marketing Science, 2007) showed that encroachment can benefit both firms, through a lower wholesale price. Vertical differentiation with a convex cost of quality goes back to Mussa and Rosen (JET, 1978), Moorthy (1988) and Motta (1993), where differentiation lets firms segment the market. The paper combines the two and finds that, once quality is endogenous, the retailer never gains.
A market of size consists of consumers with types uniformly distributed on ; a consumer of type obtains surplus from a product of quality at price . A manufacturer sells a product of quality through her direct channel and a product of quality , with quality ratio , through a retailer. Producing one unit of quality costs (); every unit sold directly costs a further direct selling cost ; the retailer's selling cost is .
With quantities (direct) and (retailer), the market-clearing prices are, for (direct channel carries the higher quality),
and for (retailer carries the higher quality)
The profits are and .
The game has three stages: (i) the manufacturer chooses a wholesale price , the quality and the ratio ; (ii) the retailer orders ; (iii) the manufacturer chooses . Solutions are subgame-perfect equilibria. The manufacturer encroaches when on the equilibrium path. Fixing gives the uniform-quality game of §4.1. The benchmark of §3.2 has no direct channel; its equilibrium profits are and .
In every subgame-perfect equilibrium with ,
The statement makes no assumption on which quality the manufacturer chooses, on the size of or on the form of the equilibrium; the constants are the benchmark's.
The §6.1 benchmark in which both qualities go through the retailer (, ), Proposition 5 (the win–lose outcome against that benchmark), and the existence of an equilibrium. The threshold milestones assert existence for each cost, so their conclusions have an equilibrium to describe.
Proposition 4(ii) says that letting the manufacturer differentiate quality across channels does not change who wins: the manufacturer still gains from encroachment and the retailer still loses, although one might expect the retailer to benefit from not facing an identical product. Proposition 3 adds that differentiation, when used, puts the higher quality in the direct channel, and Proposition 4(i) shows that for intermediate selling costs the manufacturer prefers no differentiation at all, contrary to the monopoly intuition that segmentation always pays. Proposition 5 shows the conclusion persists against a benchmark in which the retailer already carries a two-product line.
The results are proved in the paper, in part with numerical verification (e.g. the bounds on in the proof of Proposition 3, and the location of and ). None of them has been machine-checked. A formal development would turn these numerical steps into proofs and would leave a reusable, explicit model of a three-stage Stackelberg game with a vertically differentiated linear demand.
The equilibrium analysis is not a single concave program. Backward induction produces closed forms only on regions (the retailer's order must leave the manufacturer a positive direct quantity, and the retailer's quantity must stay positive), and the manufacturer's stage-1 problem is a comparison across these regions and across , and . The profit of low-quality encroachment, , involves a square root in , and the paper controls its critical points by a case analysis on polynomial derivatives with numerically located crossing points (pp. 39–40). The thresholds and are defined implicitly by the equality of maximized profits. Comparing the equilibrium profit with therefore requires bounding a maximum taken over a piecewise-defined family, not evaluating one formula.
The game is defined in QualityEncroach.Differ.Game. Quantities are restricted to be nonnegative; the wholesale price is unrestricted, as in the paper; qualities satisfy , . The price formulas are used for all nonnegative quantities, as in the paper; the case, which the paper says "can be derived similarly", is that derivation. The equilibrium notion is subgame perfection written in one-shot-deviation form at every history, on and off the path. Benchmark profits appear as the constants , (and , ); separate items derive them from the benchmark games. Threshold statements give and depending only on , assert equilibrium existence at every , and say nothing at , where the paper's statements disagree. Lemma 1 and Claim 1 are stated about the paper's reduced-form profits, defined by the displayed formulas in QualityEncroach.Differ.Reduced; the item reduced_profit_high links for to the game. Claim 1 retains and quantifies only over positive qualities, so no reduced form is evaluated at .
The goal is about subgame-perfect equilibria of the game, not about the reduced forms: a proof that only compares closed-form profits does not prove it without the milestones linking those forms to equilibrium play. The goal is not vacuous only if an equilibrium with exists; the companion spe_exists asserts existence.
Contributions are welcome at every level: the benchmark and the quantity subgame are routine calculus on quadratics; Lemma 1(i)–(ii) are one-variable sign analyses; Claim 1, Lemma 1(iii), Proposition 3 and the thresholds require the case analyses of the appendix.
Mean field games, introduced independently by Lasry and Lions (Mean field games, Jpn. J. Math. 2007) and by Huang, Malhamé and Caines (2006), describe the Nash equilibria of games with a very large number of symmetric players, each of whom reacts only to the empirical distribution of the others. In the limit, an equilibrium is a fixed point: a flow of population laws such that the optimal response of a single representative player to that flow reproduces it.
Existence of such fixed points is typically obtained by compactness, and says nothing about whether the equilibrium is determined by the data. Uniqueness matters for the use of the model: a unique equilibrium can be computed, approximated, and compared across parameters, while multiple equilibria raise a selection problem. Lasry and Lions showed by counterexamples that uniqueness fails in general, and identified a monotonicity condition on the population-dependent part of the reward under which it holds; outside that condition, uniqueness is typically available only for short horizons and Lipschitz coefficients.
Carmona and Lacker (arXiv:1307.1152v2, 2014; Ann. Appl. Probab. 25(3), 2015) set up a weak formulation of mean field games in which the controlled state is obtained from a fixed driftless diffusion by a Girsanov change of measure, so that the coefficients may be merely measurable in the state and path dependent. This mission formalizes their uniqueness theorem (Theorem 3.8): the Lasry–Lions argument carried out in the weak formulation, through backward stochastic differential equations.
Fix a horizon , a dimension , the path space with the sup norm, and a measurable . Write for the probability measures on with . A control set is a compact convex subset of a normed space, and is the set of probability measures on with the weak topology.
On a probability space carrying an initial state and an independent -dimensional Brownian motion , filtered by the augmented filtration of , let solve the driftless state equation , . The admissible controls are the progressively measurable -valued processes. For and the measure has density
under which has drift . For a flow the reward is
A pair is a solution of the MFG (Definition 3.4) if some maximizes over , , and for almost every .
The Hamiltonian is , with maximum over and maximizer set . Assumption (U) asks that (U.1) the maximizer is unique; (U.2) does not depend on ; (U.3) ; and (U.4) the Lasry–Lions monotonicity condition
The standing assumptions (S) of the paper (measurability, continuity in , nonsingular , bounded , a -growth bound on , and a separation of ) are in force throughout.
Under (S) and (U), if and are solutions of the MFG, then
Definition 3.4 constrains only for almost every , so this is the strongest identification possible.
Theorem 3.8, combined with the existence theorem of the same paper (Theorem 3.5, the first mission of this series), gives existence and uniqueness of the equilibrium (Corollary 3.9) for coefficients that are only measurable and path dependent in the state, under a monotonicity condition and no Lipschitz or small-horizon requirement. Uniqueness is also what makes the approximation result of the paper (Theorem 4.2, the third mission) refer to the equilibrium.
The result is proved in the paper. It has not been machine-checked; no mean field game uniqueness theorem in a weak or Girsanov formulation is formalized in Lean or Mathlib. The formal development would contain, as reusable parts, the Doléans exponential of a bounded Itô integrand as a probability density, the change of Brownian motion under it, the comparison principle for BSDEs with Lipschitz drivers, and the Lasry–Lions monotonicity argument.
The argument compares two equilibria through two different measures and . The direct Lasry–Lions computation, which differentiates a pairing of a Hamilton–Jacobi–Bellman solution with a Fokker–Planck solution, is not available: there is no PDE, and the value functions are only known through BSDEs. The proof needs (a) that an optimal control maximizes the Hamiltonian along the adjoint process — the necessity half of the BSDE optimality criterion, which the paper uses without a displayed proof; (b) the representation of under each of the two measures, which requires that the stochastic integrals be true martingales under the changed measures; and (c) turning a strict pointwise inequality on a set of positive -measure into a strict inequality of expectations, which uses the equivalence .
The Lean development lives in the namespace WeakMFG.Uniqueness and builds on the published definition Peng1990.SMP.Stochastic (Brownian motion, Itô integrals, Itô processes, BSDEs). Conventions:
A formalization whose hypotheses contain the conclusion is ruled out: the goal assumes only that the two pairs are solutions in the sense of Definition 3.4 — no BSDE solution, no Hamiltonian maximization, no equality of densities is assumed. Uniqueness of is stated almost everywhere in time, and nowhere is equality of the two optimal controls as functions asked for.
Contributions welcome: the Doléans exponential and Girsanov's theorem for bounded drifts in the Itô layer, existence and comparison for Lipschitz BSDEs on a filtration enlarged by an independent initial condition, and the measurable maximum theorem for the Hamiltonian. These are reusable beyond this mission, in particular by the other two missions of the series.
How fast does the empirical measure of an i.i.d. sample approach the law it is drawn from? When distance is measured by optimal transport, the answer enters the analysis of statistical estimators built from empirical distributions, quantization of probability measures, Monte Carlo and particle approximations of nonlinear PDEs (McKean–Vlasov systems), and the radius calibration of Wasserstein ambiguity sets in data-driven distributionally robust optimization.
The question has a long history. Ajtai, Komlós and Tusnády (1984) found the rate for uniform samples in the unit square. Horowitz–Karandikar (1994), Rachev–Rüschendorf and Mischler–Mouhot gave bounds that were far from optimal outside the compactly supported case. Boissard and Le Gouic (2014) and Dereich, Scheutzow and Schottstedt (2013) introduced multiscale couplings; the latter obtained sharp moment bounds for , , under a moment condition . Fournier and Guillin (arXiv:1312.2128, Probab. Theory Relat. Fields 162, 2015) extended these bounds to every , every dimension and every moment order , with explicit dependence on the moment.
Fix and write for the Euclidean norm on . For probability measures on and , the transport cost is
where is the set of couplings, measures on with marginals and . The Wasserstein distance is for and for ; the statements here are about itself. The moment of order is .
Let be i.i.d. with law and let . The quantity of interest is .
The proof works through a multiscale distance. For , is the partition of into dyadic cubes of side . The dyadic shells are and . For measures on , , and for measures on ,
where is conditioned on and rescaled by .
In Lean, is EuclideanSpace ℝ (Fin d); , , are transportCost, moment, Dp (compact case Dcube) in FournierGuillin.Moment, valued in ℝ≥0∞. is the published WassersteinDRO.Duality.empiricalDistribution, and the published WassersteinLinOpt.Ball.couplings.
For and there is such that for every with and every ,
The constant is left unspecified, as in the paper.
Theorem 1 is the standard non-asymptotic rate for empirical measures in Wasserstein distance under moment assumptions alone. The three regimes are sharp for general laws: is attained by two-point laws, by the uniform law on a cube, and the term by heavy-tailed laws (examples on pp. 2–3 of the paper). It is the input to finite-sample guarantees for Wasserstein distributionally robust optimization, to propagation-of-chaos rates for particle systems, and to quantization error bounds.
The paper result is proved; it has, to our knowledge, no machine-checked proof. A formalization adds the multiscale coupling bound (Lemma 5), a reusable comparison between transport costs and dyadic mass differences, and binomial mean-deviation estimates for empirical measures, all of which serve other rates of convergence (the concentration bounds of Theorem 2 of the same paper rest on Lemma 5).
The obvious route bounds by a coupling on a single partition of fixed mesh and optimizes the mesh. This loses a logarithm or a power in every regime and cannot reach for or for : the error at all scales must be controlled simultaneously, which is what does. The step that requires work in Lean is Lemma 5: it builds an explicit coupling scale by scale inside and glues the shells together, and it must hold for arbitrary probability measures with possibly infinite cost. The remaining steps are careful summations of geometric series in and whose regimes depend on versus and on versus or .
Conventions: with the Euclidean norm (the paper's constant uses the diameter bound of , which holds for that norm); , , , a probability measure. The sample is a point of under the product measure , i.e. the first terms of the i.i.d. sequence. Expectations are lower Lebesgue integrals of -valued functions and all series of nonnegative terms are summed in , so no bound holds by a junk value of a non-integrable integrand or a non-summable series. Constants "depending only on " are quantified after and before and ; a statement with the constant chosen after would only assert finiteness and is ruled out.
Corrections of the print, disclosed in the items: the third case of Theorem 1 is printed with ; the remark below the theorem and Step 4 of the proof show the excluded value is (the two agree only for ), and the goal excludes . Step 1 is printed for but applied at ; it is stated for . The display defining says , but the paper uses it for all , and so does the definition.
Needed infrastructure: couplings and gluing of measures on products, dyadic partitions of boxes and their counting, binomial variance, and summation of geometric series with case analysis. Lemma 5 and the binomial estimates are reusable beyond this mission. Proofs of any milestone are welcome, as are alternative proofs of the goal.
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.
Douglas–Rachford splitting is a method for minimizing a sum of two convex functions when each function has an accessible proximal operator. Its iterates are easy to state, but the speed of convergence of the objective at an individual proximal point is less immediate than convergence of an averaged point or of a residual. For optimization models in which one summand has a Lipschitz continuous gradient, Davis and Yin give explicit objective-error bounds that depend on the proximal stepsize. Their paper compares these bounds with forward–backward splitting and shows that DRS has an objective rate at least as fast when the stepsize is sufficiently small.
The present mission formalizes the rate in Theorem 3.2 and the Appendix B estimates that state the relevant contraction, monotonicity and summability properties. The companion Theorem 3.3 concerns the squared fixed-point residual. Both results are proved in the 2015 arXiv version of the paper, which fixes the numbering and constants used here; the journal article appeared in Mathematics of Operations Research in 2017.
Let be a real Hilbert space. Let be proper, lower semicontinuous and convex, and let be convex and differentiable with a -Lipschitz gradient for some . The proximal map of a function at stepsize sends to the minimizer of . Write and , and let be the reflection associated with a proximal map .
The Peaceman–Rachford map is . The DRS run is the relaxed PRS run with relaxation parameter at every step:
Equivalently, . The initial is arbitrary. Let be a fixed point of , and put . The objective value compared in this mission is at for both summands: . These values are finite under the standing assumptions. The section's Assumption 5 requires the smoothness of and constant relaxation ; it applies to Theorems 3.2 and 3.3 even though their own sentences do not repeat it.
Let be the positive root of , and the positive root of . The first target bounds the best objective error at every :
For every , this best error is . When , the same first-case upper bound holds for each , and . The goal states all four clauses together. The paper prints , the positive root of . That threshold does not match the coefficient the proof needs to be nonpositive, and with it the first case fails: for , on , and the error is twice the bound. The mission states the theorem with the threshold the proof supports, the positive root of .
For and , the companion target is
The Appendix B milestones give the contraction of the smooth gradient at proximal points, a fundamental one-step inequality, monotonicity, the extremal admissible stepsize ratio, and two summability bounds. Their constants and indices match the printed displays (B.1), (B.4), (B.7), (B.8), (B.10) and (B.12).
The objective theorem gives a rate directly at the proximal point when the stepsize is below the smaller threshold. Outside that regime, it still gives a best-iterate rate for every positive stepsize, including the explicit correction term for larger . The residual theorem controls the change in the DRS state at the faster squared rate. These statements let later work compare DRS against other splitting methods using the same objective and residual quantities, rather than changing the point at which the objective is measured.
The paper proves these results (Theorem 3.2 with the corrected threshold ); their statements are not new conjectures. The formalization work is to connect extended-real convex functions, actual proximal minimizers, smooth gradients, infinite sums, finite minima, and little-o assertions in a single Lean development. The seven Appendix B milestones are also useful as separately importable facts about proximal splitting. A machine-checked proof is still needed for the draft theorems of this mission.
The familiar convergence of the DRS fixed-point residual does not by itself give the objective error at . An objective comparison involves the two different proximal points and the smooth gradient evaluated at successive . The large-stepsize regime changes the coefficient of the gradient increment and therefore changes the explicit bound. For the per-iterate conclusion, one must establish a monotone, summable quantity that dominates the objective error; a best-iterate estimate alone does not yield the stated nonergodic little-o claim. This explains why the mission retains the Appendix B estimates rather than replacing the goal with a generic statement.
The Lean carrier is a complete real inner-product space. The proper, closed, convex predicate for and the proximal-map predicate are imported from the published ThreeOpSplitting.ConvexRates.Problem definition; the published MoreauProx.Characterization.GammaZero supplies the subgradient notion used by the paper's surrounding analysis. The smooth is a real-valued function, with its actual gradient supplied by Mathlib's gradient and constrained by the imported smoothness predicate. Each proximal map is a function with the defining minimization property; the theorems do not assume an arbitrary map can stand in for a prox.
The fixed point is an explicit hypothesis, as in the paper. The two root constants are positive real numbers satisfying their defining cubics, never decimal approximations. A finite minimum ranges over ; infinite sums come with summability; asymptotic claims use genuine little-o. The condition protects the denominator in Theorem 3.3. The objective error is taken at , never at , and the goal contains no auxiliary monotonicity or summability assumption that would assert part of its proof. Further contributions that establish proximal finiteness, the Appendix B inequalities, and the rates themselves fit within this scope.