All missions

Motivation

In ordinary statistical learning, a hypothesis is chosen from training data drawn from a distribution $P$ and judged by its risk under that same $P$. In practice the test distribution often differs from the training one: covariate shift, domain drift, adversarial perturbation of inputs. Distributionally robust learning replaces the risk at $P$ by the worst risk over a neighbourhood of $P$. When the neighbourhood is a ball in a Wasserstein distance, the perturbed distributions may move mass to nearby points of the instance space rather than only reweight the observed ones, which makes the model a natural description of small domain drifts and adversarial perturbations (Esfahani–Kuhn 2018, Gao–Kleywegt 2016, Sinha–Namkoong–Duchi 2018).

Lee and Raginsky (NeurIPS 2018) asked whether minimising the empirical version of this worst-case risk learns: does the empirical minimiser come close, in worst-case risk, to the best hypothesis of the class, at the usual $1/\sqrt n$ rate? Their §3.2 answers yes when every hypothesis is uniformly Lipschitz. Their §3.3, the subject of this mission, removes that assumption: one hypothesis with controlled growth is enough.

Setting

The instance space $\mathcal Z$ is a Polish metric space with metric $d_{\mathcal Z}$ and Borel $\sigma$-algebra; fix $p\ge1$. For Borel probability measures $P,Q$ on $\mathcal Z$, the $p$-Wasserstein distance is

$$W_p(P,Q)=\Bigl(\inf_{M}\ \mathbf E_M[d^p_{\mathcal Z}(Z,Z')]\Bigr)^{1/p},$$

the infimum over couplings $M$ of $P$ and $Q$. For a radius $\varrho>0$, $B^W_{\varrho,p}(P)=\{Q:W_p(P,Q)\le\varrho\}$ is the Wasserstein ball around $P$.

A hypothesis is a function $f:\mathcal Z\to\mathbb R$, read as a loss; a hypothesis class is a set $\mathcal F$ of them. The risk of $f$ under $Q$ is $R(Q,f)=\int f\,dQ$. The local worst-case risk and the local minimax risk are

$$R_{\varrho,p}(P,f)=\sup_{Q\in B^W_{\varrho,p}(P)}R(Q,f),\qquad R^*_{\varrho,p}(P,\mathcal F)=\inf_{f\in\mathcal F}R_{\varrho,p}(P,f).$$

Given i.i.d. samples $Z_1,\dots,Z_n\sim P$ with empirical distribution $P_n=\frac1n\sum_i\delta_{Z_i}$, the local minimax ERM is

$$\hat f\in\arg\min_{f\in\mathcal F}R_{\varrho,p}(P_n,f).$$

The standing assumptions are:

• Assumption 1. $\mathcal Z$ is bounded: $\mathrm{diam}(\mathcal Z)=\sup_{z,z'}d_{\mathcal Z}(z,z')<\infty$.
• Assumption 2. Every $f\in\mathcal F$ is upper semicontinuous with $0\le f(z)\le M$.
• Assumption 4. Some $f_0\in\mathcal F$ satisfies $f_0(z)\le C_0\,d^p_{\mathcal Z}(z,z_0)$ for all $z$, for some $C_0\ge0$ and $z_0\in\mathcal Z$.

The complexity of $\mathcal F$ is measured by the entropy integral $\mathfrak C(\mathcal F)=\int_0^\infty\sqrt{\log\mathcal N(\mathcal F,\|\cdot\|_\infty,u)}\,du$, where $\mathcal N$ is the covering number of $\mathcal F$ in the uniform norm.

Formalization targets

Goal: Theorem 3, display (11)

Under Assumptions 1, 2 and 4, for every $\delta\in(0,1)$, with probability at least $1-\delta$,

$$R_{\varrho,p}(P,\hat f)-R^*_{\varrho,p}(P,\mathcal F)\le\frac{48\,\mathfrak C(\mathcal F)}{\sqrt n}+\frac{24\,C_0(2\,\mathrm{diam}(\mathcal Z))^p}{\sqrt n}\Bigl(1+\Bigl(\frac{\mathrm{diam}(\mathcal Z)}{\varrho}\Bigr)^p\Bigr)+3M\sqrt{\frac{\log(2/\delta)}{2n}}.$$

Milestones

1. Proposition 4 (Gao–Kleywegt strong duality): $R_{\varrho,p}(Q,f)=\min_{\lambda\ge0}\{\lambda\varrho^p+\mathbf E_Q[\varphi_{\lambda,f}(Z)]\}$ with $\varphi_{\lambda,f}(z)=\sup_{z'}\{f(z')-\lambda d^p_{\mathcal Z}(z,z')\}$, in the bounded setting.
2. Lemma 2: the optimal dual multiplier of a minimiser of $R_{\varrho,p}(Q,\cdot)$ lies in $\Lambda=[0,\,C_0 2^{p-1}(1+(\mathrm{diam}(\mathcal Z)/\varrho)^p)]$.
3. (C.2): for an achiever $f^*$ of $R^*_{\varrho,p}(P,\mathcal F)$, $R_{\varrho,p}(P_n,f^*)-R_{\varrho,p}(P,f^*)\le\int\varphi_{\lambda^*,f^*}\,d(P_n-P)$.
4. (C.3): $R_{\varrho,p}(P,\hat f)-R_{\varrho,p}(P_n,\hat f)\le\sup_{\varphi\in\Phi}\int\varphi\,d(P-P_n)$, with $\Phi=\{\varphi_{\lambda,f}:\lambda\in\Lambda,f\in\mathcal F\}$.
5. (C.4): with probability at least $1-\delta/2$, the left side of (C.3) is at most $2\mathfrak R_n(\Phi)+M\sqrt{2\log(2/\delta)/n}$, where $\mathfrak R_n$ is the expected Rademacher average.
6. (C.5): with probability at least $1-\delta/2$, $R_{\varrho,p}(P_n,f^*)-R_{\varrho,p}(P,f^*)\le M\sqrt{\log(2/\delta)/(2n)}$.
7. Lemma 5: $\mathfrak R_n(\Phi)\le\frac{24}{\sqrt n}\mathfrak C(\mathcal F)+\frac{12C_0(2\,\mathrm{diam}(\mathcal Z))^p}{\sqrt n}(1+(\mathrm{diam}(\mathcal Z)/\varrho)^p)$.

The goal carries the paper's constants. The mission does not ask for sharper constants; a proof of the stated bound closes it.

Significance

The result. Theorem 3 is a generalisation guarantee for Wasserstein distributionally robust ERM that needs no uniform smoothness of the class. The uniformly Lipschitz assumption of the companion Theorem 2 fails for most classes of interest when $p>1$: a function with $\sup_{z,z'}(f(z')-f(z))/d^p_{\mathcal Z}(z,z')<\infty$ is constant (p. 6). Assumption 4 holds, for example, for regression with quadratic loss whenever the predictor class contains the zero predictor (p. 6). The second term of (11) decreases as $\varrho$ grows, which quantifies how a larger ambiguity set screens out non-smooth hypotheses (Remark 4).

Formalizing it. The theorem has a published pen-and-paper proof (Appendix C.5 of the arXiv version); it has no machine-checked proof. A formalization produces machine-checked statements of the dual characterisation of Wasserstein worst-case risk on a bounded Polish space, of a symmetrization-plus-McDiarmid uniform deviation bound for a parametrised class, and of a Dudley-entropy bound on a product class. The proof (C.5) on p. 16 starts from an achiever $f^*$ of $R^*_{\varrho,p}(P,\mathcal F)$, which need not exist; the goal is stated without that assumption, so a complete proof also handles the infimum.

Difficulty

The obvious argument decomposes the excess risk through $f^*$ and bounds $R_{\varrho,p}(P,\hat f)-R_{\varrho,p}(P_n,\hat f)$ by a uniform deviation over $\mathcal F$. That step fails: $R_{\varrho,p}(\cdot,f)$ is a supremum over a ball of measures, not an expectation, so it is not an empirical process in $f$. Passing to the dual makes it one, but the dual multiplier $\hat\lambda$ depends on the sample and has no a priori bound, so the class $\{\varphi_{\lambda,f}\}$ over all $\lambda\ge0$ is too large. Without uniform smoothness of $\mathcal F$ there is no obvious a priori bound on $\hat\lambda$, and the entropy of the resulting two-parameter class must still be controlled at rate $1/\sqrt n$. Strong duality itself (Proposition 4) needs the existence of optimal couplings and a measurable-selection argument on a Polish space; it is not in Mathlib.

Formalization scope

• $\mathcal Z$ is a MetricSpace with BorelSpace and PolishSpace instances; Assumption 1 is Bornology.IsBounded (Set.univ : Set 𝒵), and $\mathrm{diam}(\mathcal Z)$ is Metric.diam Set.univ. Throughout, $p\ge1$ and $\varrho>0$ (the paper's standing choice, p. 3).
• The Wasserstein distance and ball are the published definitions WassersteinLinOpt.Ball.wassersteinDist and wassersteinBall, which range over all Borel probability measures; on a bounded space this equals the paper's $\mathcal P_p(\mathcal Z)$ ball.
• Local risks, $\varphi_{\lambda,f}$, $\Lambda$, $\Phi$ and $\mathfrak R_n$ are real-valued suprema and infima, used only for classes bounded in $[0,M]$, where they are finite.
• The sample is a point of $\mathcal Z^n$ under $P^{\otimes n}$. "With probability at least $1-\delta$" means the outer measure of the failure set is at most $\delta$; this equals the probability when the set is measurable and is stronger otherwise.
• The ERM is a sample-indexed function $\hat f$ with hypotheses $\hat f(\omega)\in\mathcal F$ and minimality of $R_{\varrho,p}(P_n,\cdot)$. These hypotheses presuppose that an empirical minimiser exists, as (7) does. No measurability of $\hat f$ is assumed.
• The covering number is internal (centres in $\mathcal F$). $\mathfrak C(\mathcal F)$ is valued in $[0,\infty]$, and every bound containing it assumes $\mathfrak C(\mathcal F)<\infty$: otherwise the paper's bound is $+\infty$, while its conversion to a real number would be $0$.
• Proposition 4 is stated for bounded upper semicontinuous $f$ on bounded $\mathcal Z$, the only case the paper uses. The printed statement covers every usc $f$ and every $Q\in\mathcal P_p(\mathcal Z)$.
• (C.2) and (C.5) assume an achiever $f^*$, as printed; the goal does not.

The following formalizations would trivialize the goal and are ruled out: a bound for each fixed $f\in\mathcal F$ in place of $R^*_{\varrho,p}(P,\mathcal F)$; an $\hat f$ defined by Classical.choose of an unproved existence; a supremum over all measures instead of over the ball; and the real conversion of an infinite $\mathfrak C(\mathcal F)$.

The infrastructure is reusable beyond this mission: Wasserstein strong duality on Polish spaces (Proposition 4 specialises the general optimal-transport duality of Blanchet–Murthy 2019, whose transport-plan form is a proved theorem on the platform as ModelRiskOT.Duality.theorem_1); Dudley's entropy bound for sub-Gaussian processes indexed by infinite classes; and McDiarmid's inequality for suprema of empirical processes. Contributions of these general tools, as separate theorems, are welcome. Source: the arXiv v2 preprint, which is the NeurIPS 2018 camera-ready text followed by the supplementary appendices.

Selected references

• J. Lee, M. Raginsky, Minimax statistical learning with Wasserstein distances, NeurIPS 2018; arXiv:1705.07815v2. https://arxiv.org/abs/1705.07815
• R. Gao, A. J. Kleywegt, Distributionally robust stochastic optimization with Wasserstein distance, arXiv:1604.02199, 2016. https://arxiv.org/abs/1604.02199
• J. Blanchet, K. Murthy, Quantifying distributional model risk via optimal transport, Mathematics of Operations Research 44(2), 2019. https://doi.org/10.1287/moor.2018.0936
• P. Mohajerin Esfahani, D. Kuhn, Data-driven distributionally robust optimization using the Wasserstein metric, Mathematical Programming 171, 2018. https://doi.org/10.1007/s10107-017-1172-1
• A. Sinha, H. Namkoong, J. Duchi, Certifying some distributional robustness with principled adversarial training, ICLR 2018; arXiv:1710.10571. https://arxiv.org/abs/1710.10571
• R. M. Dudley, The sizes of compact subsets of Hilbert space and continuity of Gaussian processes, Journal of Functional Analysis 1, 1967. https://doi.org/10.1016/0022-1236(67)90017-1

Motivation

In statistical learning a hypothesis $f$ is chosen from a class $\mathcal F$ using $n$ samples drawn from an unknown distribution $P$, and its quality is measured by the risk $R(P,f) = \mathbf E_P[f(Z)]$. When the distribution at deployment time may differ from the one that generated the data (domain drift, adversarial perturbation, model misspecification), a natural replacement is the worst-case risk over a neighbourhood of $P$. Distributionally robust optimization with Wasserstein neighbourhoods takes these neighbourhoods to be balls in an optimal-transport distance, which compare distributions through the geometry of the instance space instead of through likelihood ratios. Wasserstein balls also contain distributions with support different from that of $P$, which divergence balls do not.

J. Lee and M. Raginsky, Minimax statistical learning with Wasserstein distances (NeurIPS 2018, arXiv:1705.07815), give generalization guarantees for the empirical version of this procedure, the local minimax ERM. Their analysis rests on the strong duality theorem of Gao and Kleywegt (arXiv:1604.02199), which turns the supremum over a Wasserstein ball into a minimization over one real multiplier $\lambda \ge 0$. This mission formalizes their Theorem 2, the excess-risk bound for a class of uniformly Lipschitz hypotheses, together with the steps of its proof. The source is the arXiv v2 preprint, which contains the NeurIPS camera-ready text and the supplementary appendices.

Setting

The instance space $\mathcal Z$ is a Polish space (complete separable metric space) with metric $d_{\mathcal Z}$, and it is bounded: $\operatorname{diam}(\mathcal Z) = \sup_{z,z'} d_{\mathcal Z}(z,z') < \infty$ (Assumption 1). Fix $p \ge 1$. The $p$-Wasserstein distance between Borel probability measures is

$$W_p(P,Q) = \Big(\inf_{M} \mathbf E_M\big[d^p_{\mathcal Z}(Z,Z')\big]\Big)^{1/p},$$

the infimum over couplings $M$ of $P$ and $Q$. For a radius $\varrho > 0$ the ball is $B^W_{\varrho,p}(P) = \{Q : W_p(P,Q) \le \varrho\}$.

The hypothesis class $\mathcal F$ consists of upper semicontinuous functions $f : \mathcal Z \to \mathbb R$ with $0 \le f \le M$ (Assumption 2). The local worst-case risk and the local minimax risk are

$$R_{\varrho,p}(P,f) = \sup_{Q \in B^W_{\varrho,p}(P)} R(Q,f), \qquad R^*_{\varrho,p}(P,\mathcal F) = \inf_{f \in \mathcal F} R_{\varrho,p}(P,f).$$

Given i.i.d. samples $Z_1,\dots,Z_n$ from $P$ with empirical distribution $P_n = \frac1n\sum_i \delta_{Z_i}$, the local minimax ERM is $\hat f \in \arg\min_{f \in \mathcal F} R_{\varrho,p}(P_n,f)$.

Assumption 3 asks that every $f \in \mathcal F$ be $L$-Lipschitz with one constant $L$: $f(z') - f(z) \le L\,d_{\mathcal Z}(z',z)$. The complexity of $\mathcal F$ is measured by the entropy integral

$$\mathfrak C(\mathcal F) = \int_0^\infty \sqrt{\log \mathcal N(\mathcal F,\|\cdot\|_\infty,u)}\,du,$$

where $\mathcal N(\mathcal F,\|\cdot\|_\infty,u)$ is the covering number of $\mathcal F$ in the uniform metric. The dual integrand of Gao–Kleywegt duality is $\varphi_{\lambda,f}(z) = \sup_{z'}\{f(z') - \lambda d^p_{\mathcal Z}(z,z')\}$.

Formalization targets

Goal: Theorem 2 (10)

Under Assumptions 1–3, for every $\delta \in (0,1)$, with probability at least $1-\delta$,

$$R_{\varrho,p}(P,\hat f) - R^*_{\varrho,p}(P,\mathcal F) \le \frac{48\,\mathfrak C(\mathcal F)}{\sqrt n} + \frac{48 L\cdot\operatorname{diam}(\mathcal Z)^p}{\sqrt n\cdot\varrho^{p-1}} + 3M\sqrt{\frac{\log(2/\delta)}{2n}}.$$

Milestones, in the order the proof uses them

1. Proposition 4 (8): $R_{\varrho,p}(Q,f) = \min_{\lambda\ge0}\{\lambda\varrho^p + \mathbf E_Q[\varphi_{\lambda,f}(Z)]\}$.
2. Lemma 1: the optimal dual multiplier satisfies $\tilde\lambda \le L\varrho^{-(p-1)}$.
3. (C.2): $R_{\varrho,p}(P_n,f^*) - R_{\varrho,p}(P,f^*) \le \int \varphi_{\lambda^*,f^*}\,d(P_n - P)$ for an achiever $f^*$.
4. (C.3) with $\Lambda = [0, L\varrho^{-(p-1)}]$ and $\Phi = \{\varphi_{\lambda,f} : \lambda \in \Lambda, f \in \mathcal F\}$: $R_{\varrho,p}(P,\hat f) - R_{\varrho,p}(P_n,\hat f) \le \sup_{\varphi\in\Phi}\int\varphi\,d(P - P_n)$.
5. (C.4): with probability at least $1-\delta/2$, $R_{\varrho,p}(P,\hat f) - R_{\varrho,p}(P_n,\hat f) \le 2\mathfrak R_n(\Phi) + M\sqrt{2\log(2/\delta)/n}$.
6. (C.5): with probability at least $1-\delta/2$, $R_{\varrho,p}(P_n,f^*) - R_{\varrho,p}(P,f^*) \le M\sqrt{\log(2/\delta)/(2n)}$.
7. The Rademacher bound of Appendix C.3: $\mathfrak R_n(\Phi) \le \frac{24}{\sqrt n}\mathfrak C(\mathcal F) + \frac{24L\operatorname{diam}(\mathcal Z)^p}{\sqrt n\,\varrho^{p-1}}$.

Significance

Theorem 2 says that robust ERM over a uniformly Lipschitz class is nearly optimal for the robust risk at the unknown distribution, with excess of order $1/\sqrt n$ and explicit constants. The dependence on $\varrho$ enters only through $\varrho^{-(p-1)}$; at $p = 1$ the bound does not depend on $\varrho$ and recovers the usual rate of ordinary ERM. The paper derives Corollaries 1 and 2 (regression with a Lipschitz link, and Gaussian-kernel classes) and the domain-adaptation bound of Theorem 4 from it. Lemma 1, which confines the dual multiplier to a fixed interval, is also used outside the theorem: Remark 3 proposes it as the search range for the fixed-$\lambda$ adversarial training of Sinha et al.

The result is proved in the paper; to our knowledge none of it has been machine-checked. What this mission adds is a verified version of a complete distributionally robust generalization argument: Gao–Kleywegt strong duality on a bounded Polish space, the multiplier bound, symmetrization and bounded differences for a class indexed by a function and a real parameter, and a Dudley entropy bound for that joint class. The paper's appendix states the Rademacher bound with a stray constant $C_0$ that belongs to a different assumption (Assumption 4); the milestone states the bound without it, which is what the proof gives and what the constant $48L$ of (10) needs.

Difficulty

The obvious route bounds $\sup_{f}|R_{\varrho,p}(P,f) - R_{\varrho,p}(P_n,f)|$ uniformly over $\mathcal F$. That needs uniform control of the dual multiplier for every $f$ and every empirical distribution, and without it the class $\{\varphi_{\lambda,f}\}$ is indexed by an unbounded $\lambda$, so its complexity is infinite. Lemma 1 resolves this only for the minimizers, which is why the argument is organized around $\hat f$ and an achiever $f^*$ rather than a uniform bound.

The formal difficulties are separate. Strong duality with attainment of the minimum is a measure-theoretic theorem about couplings on a Polish space (existence of optimal couplings, measurable selection of near-maximizers), none of which is in Mathlib for Wasserstein balls. The supremum over $\Phi$ must be shown measurable before its expectation means anything. Dudley's chaining bound over a separable, infinite index set is also missing from Mathlib in the form needed here. Finally, the theorem does not assume that $R^*_{\varrho,p}(P,\mathcal F)$ is attained, while the paper's proof uses an achiever $f^*$, so a complete proof needs an approximation argument that the paper does not write out.

Formalization scope

• $\mathcal Z$ is a MetricSpace with BorelSpace and PolishSpace instances, and Assumption 1 is Bornology.IsBounded (Set.univ : Set 𝒵). $\operatorname{diam}(\mathcal Z)$ is Metric.diam univ.
• $W_p$ and the ball are the published definitions WassersteinLinOpt.Ball.wassersteinDist and wassersteinBall. Membership in $\mathcal P_p(\mathcal Z)$ is automatic on a bounded space.
• The standing assumptions $p \ge 1$ and $\varrho > 0$ are binders of every item.
• Risks, the dual integrand $\varphi_{\lambda,f}$ and the Rademacher average are real suprema, infima and Bochner integrals. Under the binders each is over a nonempty set that is bounded on the relevant side, and each integrand is bounded and measurable.
• The covering number is the internal one (centres in $\mathcal F$), valued in $\mathbb N\cup\{\infty\}$, and $\mathfrak C(\mathcal F)$ is valued in $[0,\infty]$. Every item whose bound contains $\mathfrak C(\mathcal F)$ assumes $\mathfrak C(\mathcal F) < \infty$ and uses its real value. This is a disclosed pin: otherwise the bound is $+\infty$.
• Assumption 3 is ∀ f ∈ ℱ, ∀ z z', f z' - f z ≤ L * dist z' z, with one $L$ quantified before $\mathcal F$, and $0 \le L$ is a disclosed pin.
• The sample is ω : Fin n → 𝒵 with law Measure.pi (fun _ => P), and $n \ge 1$. "With probability at least $1-\delta$" means the outer measure of the failure set is at most $\delta$, for $0 < \delta < 1$.
• The ERM is a sample-indexed selection $\hat f$ with membership and minimality hypotheses, never Classical.choose. Such a selection exists exactly when empirical minimizers exist, which display (7) presupposes.
• "min" over $\lambda$ in Proposition 4 includes attainment, and the argmins of Lemma 1 and (C.2) are minimality hypotheses.

Trivializing formalizations are ruled out:

• Assumption 3 is not written with $L$ chosen after $f$, and $L \ge 0$ is not omitted.
• The stray $C_0$ is not in the Lean.
• The goal is about $R^*_{\varrho,p}(P,\mathcal F)$, not about a fixed competitor $f$.
• No probability is converted with toReal, and an infinite $\mathfrak C(\mathcal F)$ is never converted to $0$.

A complete development needs:

• Gao–Kleywegt duality for bounded upper semicontinuous losses;
• McDiarmid's and Hoeffding's inequalities on product measures;
• symmetrization;
• Dudley's entropy integral bound for sub-Gaussian processes indexed by a separable pseudometric space.

The last three are reusable well beyond this mission. Contributions of any of these as stand-alone results are welcome, as are proofs of the milestones.

Selected references

• J. Lee and M. Raginsky, Minimax statistical learning with Wasserstein distances, Advances in Neural Information Processing Systems 31 (NeurIPS 2018); arXiv:1705.07815v2. https://arxiv.org/abs/1705.07815
• R. Gao and A. J. Kleywegt, Distributionally robust stochastic optimization with Wasserstein distance, Mathematics of Operations Research 48(2), 2023; arXiv:1604.02199. https://arxiv.org/abs/1604.02199
• A. Sinha, H. Namkoong and J. Duchi, Certifying some distributional robustness with principled adversarial training, ICLR 2018; arXiv:1710.10571. https://arxiv.org/abs/1710.10571
• M. Talagrand, Upper and Lower Bounds for Stochastic Processes, Springer, 2014. https://doi.org/10.1007/978-3-642-54075-2

Motivation

Mean-field games were introduced by Lasry and Lions (2007) and by Huang, Malhamé and Caines (2006) as limits of stochastic differential games with many symmetric players, each interacting with the others only through the empirical distribution of their states. The limit replaces a game of $N$ coupled players by one representative player facing a deterministic flow of distributions that it must reproduce. That flow is the equilibrium condition. The limit object is easier to solve. Whether it says anything about the finite game it came from is a separate question: a mean-field equilibrium is useful only if the strategies it produces are nearly optimal for each of $N$ actual players.

Carmona and Delarue (SIAM J. Control Optim. 51, 2013) solve the mean-field game through the stochastic maximum principle. For drifts that are affine and costs that are convex, the equilibrium is the solution of a forward–backward SDE of McKean–Vlasov type. Its existence is the subject of the first mission of this series. This mission formalizes §4 of the paper. The strategies read off from that solution are an approximate Nash equilibrium of the $N$-player game, with an explicit rate in $N$.

Setting

The state space is $\mathbb R^d$ and the control space is $\mathbb R^k$, both with the Euclidean norm. Each player $i$ has a private state $U^i_t$, driven by its own $m$-dimensional Brownian motion $W^i$, the motions being independent. The dynamics are

$$dU^i_t = b(t, U^i_t, \bar\nu^N_t, \beta^i_t)\,dt + \sigma\,dW^i_t,\qquad U^i_0 = x_0,\qquad \bar\nu^N_t = \frac1N\sum_{j=1}^N\delta_{U^j_t},$$

where $b(t,x,\mu,\alpha) = b_0(t,\mu) + b_1(t)x + b_2(t)\alpha$ is affine and $\sigma$ is a constant matrix. Player $i$ chooses a strategy $\beta^i$, a process that is progressively measurable for the filtration of $(W^1,\dots,W^N)$ and satisfies $\mathbb E\int_0^T|\beta^i_t|^2dt<\infty$. It pays

$$\bar J^{N,i}(\beta^1,\dots,\beta^N) = \mathbb E\Big[g(U^i_T,\bar\nu^N_T) + \int_0^T f(t,U^i_t,\bar\nu^N_t,\beta^i_t)\,dt\Big].$$

The costs $f$, $g$ satisfy the paper's assumptions (A.1)–(A.7): joint convexity in $(x,\alpha)$ with strong convexity in $\alpha$, $C^{1,1}$ regularity, local Lipschitz continuity in the measure argument for the 2-Wasserstein distance $W_2$, and growth conditions.

On the mean-field side, let $(X_t,Y_t,Z_t)$ solve the McKean–Vlasov FBSDE (3.1), let $\mu_t = \mathbb P_{X_t}$, and let $u$ be the FBSDE value function. This is a function that is Lipschitz in $x$ with linear growth and satisfies $Y_t = u(t,X_t)$. Let $\hat\alpha(t,x,\mu,y)$ minimize the Hamiltonian $\langle b,y\rangle + f$ over $\alpha$, and let $J$ be the mean-field cost (4.1). The candidate strategies are

$$\bar\alpha^{N,i}_t = \hat\alpha\big(t, X^i_t, \mu_t, u(t,X^i_t)\big),$$

where $(X^1,\dots,X^N)$ solves the particle system (4.2): the dynamics above, with each player using this feedback against the frozen flow $\mu$. Each player needs only its own state.

Formalization targets

Goal: Theorem 4.2

There exist $c>0$ and positive numbers $(\epsilon_N)_{N\ge1}$ with $\epsilon_N\le cN^{-1/(d+4)}$ such that, for every $N\ge1$, every player $i$ and every admissible deviation $\beta^i$,

$$\bar J^{N,i}(\bar\alpha^{N,1},\dots,\beta^i,\dots,\bar\alpha^{N,N})\ \ge\ \bar J^{N,i}(\bar\alpha^{N,1},\dots,\bar\alpha^{N,N}) - \epsilon_N.$$

The constant and the sequence come before $N$, the player and the deviation.

Milestones

The milestones follow the proof, in attack order:

• Lemma 4.1 (Horowitz–Karandikar): $\mathbb E[W_2^2(\bar\mu^N,\mu)]\le CN^{-2/(d+4)}$ for i.i.d. samples from $\mu\in\mathcal P_{d+5}$.
• Well-posedness of (4.2).
• The moment bound (4.4).
• The transport inequality (4.13).
• Propagation of chaos (4.11) and its consequence (4.12) for the empirical measure.
• The equilibrium cost estimate (4.14): $\bar J^{N,i}(\bar\alpha) = J + O(N^{-1/(d+4)})$.
• For a deviation of bounded energy $\mathbb E\int|\beta^1|^2\le A$: (4.17), (4.20) and the lower bound (4.23), $\bar J^{N,1}\ge J - c_AN^{-1/(d+4)}$.
• The coercivity (4.25) for deviations of large energy.

Companion: Corollary 4.3

Large deviations are unprofitable for every player (4.27). A bounded deviation of one player keeps every player's cost above $J-\epsilon_N$ (4.28).

Significance

The theorem justifies the mean-field game as a model of large finite games. Solving one McKean–Vlasov FBSDE produces distributed closed-loop strategies. No player can improve its cost by more than $O(N^{-1/(d+4)})$ by deviating, even with a strategy that uses all players' noises. The rate gives a quantitative meaning to "large $N$". The milestones (4.11)–(4.12) are a quantitative propagation-of-chaos result for the particle system driven by the decoupling field. Such results are used on their own in the numerics and statistics of interacting particle systems.

The result is proved in the paper. No part of it has been machine-checked, as far as the platform's records show. The work that remains is to formalize the known proof. That needs Wasserstein estimates for empirical measures (Lemma 4.1, cited by the paper without proof), Gronwall arguments for SDE systems, and the optimality of the mean-field control (Theorem 2.2, the first mission's milestone, used here through $J\le J(\beta^1)$). Sharper rates are known in low dimension (Fournier and Guillin, 2015). They would be welcome as variants, but they are not the target.

Difficulty

The obvious argument compares the deviating player's cost with the mean-field cost of the same strategy. It fails in two places. The deviation changes the empirical measure that every other player sees, so the other players' states are no longer independent copies of $X$. It must be shown that one player of bounded energy moves the population's empirical measure by only $O(N^{-1/(d+4)})$ in $W_2$ ((4.17)–(4.20)). The second problem is that the deviation $\beta^1$ is adapted to the filtration of all $N$ Brownian motions, larger than the one in which the mean-field control problem is posed. The comparison $J\le J(\beta^1)$ must survive this enlargement. Finally, nothing bounds the energy of a deviation a priori. Deviations of large energy have to be excluded separately by a coercivity estimate ((4.25)), and only then can the rate be obtained uniformly.

Formalization scope

The data live on EuclideanSpace ℝ (Fin n), so every norm, $M_2$ and $W_2$ is Euclidean. Matrix norms are operator norms. $W_2$ is the published WassersteinDRO.Duality.wassersteinDistance 2, valued in $[0,\infty]$. Measures carry Mathlib's σ-algebra on Measure, which on probability measures on $\mathbb R^d$ coincides with the paper's Borel σ-field of weak convergence. The SDEs and BSDEs are the published Itô-process predicates of Peng (Peng1990.SMP.SolvesSDE, SolvesBSDE). Solutions also have almost surely continuous paths on $[0,T]$. The game filtration is generated by $(W^1,\dots,W^N)$ and augmented by the null sets. Players are indexed by Fin N, so the paper's player $1$ is index $0$.

The mean-field solution and the game live on two probability spaces. Only $\mu_t=\mathbb P_{X_t}$, $J$ and $u$ pass between them. The value function $u$ enters through its properties (3.3), the identity $Y_t=u(t,X_t)$ and joint measurability, as in Lemma 3.5. $\hat\alpha$ is the chosen minimizer of the Hamiltonian, with default $0$; by Lemma 2.1 the default is never used on $[0,T]\times\mathcal P_2$. The assumptions also contain a standing convention the page does not write: $f$ and $g$ are Borel measurable. Without it the expected costs would not be expectations of measurable integrands. Moments and expected energies are lower Lebesgue integrals in $[0,\infty]$. Costs are real expectations, finite under (A.5) for admissible strategies.

The statements exclude the trivializing readings:

• the flow is the law of the mean-field state, not an arbitrary flow;
• distances are Euclidean, not sup-norm;
• the empirical measure is used only for $N\ge1$;
• $W_2^2$ is never converted to a real number where it could be infinite;
• the constants $c$, $(\epsilon_N)$, $c_A$, $N_0$ sit exactly where the page's quantifiers put them;
• in a deviation the other players keep their processes $\bar\alpha^{N,j}$, while the empirical measure follows the new states.

The goal does not mention the decoupled copies or Lemma 4.1.

A complete development needs:

• Wasserstein estimates for empirical measures, which are reusable well beyond this mission;
• existence, uniqueness and moment bounds for Lipschitz SDE systems with measure-dependent drift;
• the stochastic-maximum-principle comparison of the first mission.

Contributions on any of these are welcome. Well-posedness of the deviated system (4.5) is used but is not stated on the page; a proof of it is also welcome.

Selected references

• R. Carmona and F. Delarue, Probabilistic analysis of mean-field games, SIAM J. Control Optim. 51(4):2705–2734, 2013. https://doi.org/10.1137/120883499
• J.-M. Lasry and P.-L. Lions, Mean field games, Japanese Journal of Mathematics 2:229–260, 2007. https://doi.org/10.1007/s11537-007-0657-8
• M. Huang, R. P. Malhamé and P. E. Caines, Large population stochastic dynamic games: closed-loop McKean–Vlasov systems and the Nash certainty equivalence principle, Communications in Information and Systems 6(3):221–252, 2006. https://doi.org/10.4310/CIS.2006.v6.n3.a5
• J. Horowitz and R. L. Karandikar, Mean rates of convergence of empirical measures in the Wasserstein metric, J. Comput. Appl. Math. 55(3):261–273, 1994. https://doi.org/10.1016/0377-0427(94)90033-7
• A.-S. Sznitman, Topics in propagation of chaos, École d'Été de Probabilités de Saint-Flour XIX, Lecture Notes in Math. 1464, Springer, 1991. https://doi.org/10.1007/BFb0085169
• N. Fournier and A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probab. Theory Related Fields 162:707–738, 2015. https://doi.org/10.1007/s00440-014-0583-7

Motivation

A mean-field game describes a population of agents whose individual dynamics and costs depend on the distribution of the population's states. In a large population, an individual agent has negligible influence on that distribution but still responds to it. The mathematical problem is to find a control whose induced state law agrees with the distribution used to choose the control. Carmona and Delarue's 2013 analysis formulates this matching condition through a coupled stochastic system. Mean-field games were introduced independently by Lasry and Lions (2006–2007), through a coupled Hamilton–Jacobi–Bellman/Fokker–Planck system of partial differential equations, and by Huang, Malhamé and Caines (2006). Carmona and Delarue replace the PDE system by a probabilistic one, which handles costs of quadratic growth and degenerate noise without a uniform ellipticity assumption. Its existence theorem supplies the state-dependent control used later in the paper to construct approximate Nash equilibria for finite-player games.

The article first treats a control problem with a prescribed flow of probability measures, then imposes the requirement that the flow equal the law of the resulting state process. This mission concerns that self-consistent system and the regularity of its backward component. Proposition 3.7, a companion target, adds a uniqueness conclusion under the paper's monotonicity condition.

Setting

Fix a horizon $T$, an initial state $x_0\in\mathbb R^d$, an $m$-dimensional Brownian motion $W$, and unrestricted controls $a\in\mathbb R^k$. The state $X_t$ has values in $\mathbb R^d$. Its drift is affine in state and control,

$$b(t,x,\mu,a)=b_0(t,\mu)+b_1(t)x+b_2(t)a,$$

where $\mu$ is a probability measure on $\mathbb R^d$ with finite second moment. The volatility $\sigma\in\mathbb R^{d\times m}$ is constant and uncontrolled. A running cost $f(t,x,\mu,a)$ and a terminal cost $g(x,\mu)$ determine the control problem.

The Hamiltonian is $H(t,x,\mu,y,a)=\langle b(t,x,\mu,a),y\rangle+f(t,x,\mu,a)$. Under convexity, it has a unique minimizer $\hat a(t,x,\mu,y)$. The forward-backward stochastic differential equation (FBSDE) couples a forward state $X$ to an adjoint process $Y$ and a noise coefficient $Z$. The forward equation uses the feedback $\hat a(t,X_t,\mu_t,Y_t)$; the backward equation has driver $\partial_xH$ and terminal condition $\partial_xg(X_T,\mu_T)$. The McKean–Vlasov requirement sets $\mu_t=\mathcal L(X_t)$ at every time, giving the system (3.1):

$$\begin{cases} dX_t=b\big(t,X_t,\mathcal L(X_t),\hat a(t,X_t,\mathcal L(X_t),Y_t)\big)\,dt+\sigma\,dW_t, & X_0=x_0,\\ dY_t=-\partial_xH\big(t,X_t,\mathcal L(X_t),Y_t,\hat a(t,X_t,\mathcal L(X_t),Y_t)\big)\,dt+Z_t\,dW_t, & Y_T=\partial_xg\big(X_T,\mathcal L(X_T)\big).\end{cases}$$

This law matching is the extra condition beyond solvability for a prescribed flow.

All seven standing assumptions of Theorem 3.2 are retained. (A.1)–(A.3) specify measurable, bounded affine drift and $C^{1,1}$ running costs with a positive control-convexity constant $\lambda$. (A.4) gives local boundedness, differentiability, and convexity of the terminal cost. (A.5) controls growth and dependence on the measure argument using the 2-Wasserstein distance $W_2$; (A.6) bounds the control gradient at zero; and (A.7) is a weak mean-reverting condition on the spatial gradients at Dirac laws. A measure flow is bounded when its second moments are uniformly bounded over $[0,T]$.

Formalization targets

The goal is Theorem 3.2. It asserts existence of $(X,Y,Z)$ solving the self-consistent system. For every solution, there is an FBSDE value function $u:[0,T]\times\mathbb R^d\to\mathbb R^d$ and a constant $c\ge0$ such that

$$\|u(t,x)\|\le c(1+\|x\|),\qquad \|u(t,x)-u(t,x')\|\le c\|x-x'\|,\qquad Y_t=u(t,X_t)\quad\text{a.s. for all }t\in[0,T].$$

It also gives $\mathbb E[\sup_{0\le t\le T}\|X_t\|^\ell]<\infty$ for every real $\ell\ge1$. The constant $c$ belongs to each solution; the theorem does not assert a single universal value for all models.

The milestone sequence follows the article's stated results: Lemma 2.1 characterizes the Hamiltonian minimizer; Theorem 2.2 and Proposition 2.5 compare controlled costs; Lemma 3.5 establishes a frozen-flow solution and a decoupling function; Proposition 3.8 handles bounded spatial gradients; Lemmas 3.9 and 3.10 state the approximation and stability results; and the first sentence of §3.7 records solvability under stronger state convexity. The companion Proposition 3.7 asks for uniqueness when the running cost separates into a measure-dependent and a control-dependent part and the measure-dependent costs satisfy the Lasry–Lions monotonicity inequalities.

Significance

A solution of the self-consistent FBSDE identifies a law flow consistent with the feedback chosen from that same law. The value function represents the adjoint state as a deterministic function of time and the forward state. Its linear growth and Lipschitz regularity control how feedback changes when states move. Those properties are used in the article's subsequent approximate-Nash analysis for the finite-player game; without them, its estimates cannot be stated in the same form. The moment conclusion gives the integrability needed for those comparisons.

The paper proves these results. The formalization task is to express its stochastic equations, probability laws, measure dependence, and analytic assumptions precisely enough that the known argument can be checked in Lean. The reusable outputs include a Euclidean mean-field control model, a finite-moment measure-flow interface, and a componentwise stochastic solution predicate compatible with published Brownian-motion and Itô-process definitions.

Difficulty

For a prescribed measure flow, the control problem produces a forward-backward system, but this does not by itself make the resulting state law equal to the prescribed flow. Standard Lipschitz contraction arguments may give short-time solvability; the theorem allows an arbitrary fixed horizon. The argument must also preserve control convexity and quantitative estimates while passing from models with bounded spatial gradients to the stated growth conditions. The adjoint value function must work simultaneously across the full time interval, and the theorem requires moment bounds of every order at least one.

Formalization scope

Lean uses EuclideanSpace ℝ (Fin d) for states and EuclideanSpace ℝ (Fin k) for controls, so all norms in the costs, moment conditions, and $W_2$ are Euclidean. A joint state-control norm is computed from the sum of the two squared Euclidean norms. Time uses $\mathbb R_{\ge0}$; measures with finite second moment use extended nonnegative moments, and $W_2$ is the published coupling-based definition. The measure-space sigma algebra is Mathlib's Giry sigma algebra, agreeing with the weak-convergence Borel sigma algebra on the probability measures here. Matrix bounds use operator norms.

The stochastic layer reuses published predicates for a standard Brownian motion, progressive $L^2$ processes, Itô integrals, SDEs, and BSDEs. The filtration is the Brownian filtration augmented by null sets. Peng's componentwise stochastic predicates use coordinate functions, so the Lean development converts between those and Euclidean states. Solutions include continuous trajectories and the square-integrability condition (2.14). The real cost expectations are used only in settings where the hypotheses ensure integrability. The Hamiltonian minimizer has a total-function fallback outside its existence domain, while Lemma 2.1 ensures that branch is never used in the theorems. Laws are formed only from measurable state variables. An arbitrary prescribed flow cannot replace the state law in the goal.

The following readings are fixed. (A.5)'s joint display for $(f,g)$ is two inequalities, one for $f$ and one for $g$ without the time and control arguments. Every assumption is imposed for $t\in[0,T]$ and for measures in $\mathcal P_2(\mathbb R^d)$ only; measurability of $f$, $g$ and $b$ is required on that domain. Gradients of $f$ and $g$ are computed from the functions, not supplied as separate data. A solution of (2.13) or (3.1) is a progressively measurable triple with a.s. continuous forward and adjoint paths satisfying (2.14). Costs are real expectations; under the theorem's hypotheses the integrands are integrable, so no default value of the integral is used. In Proposition 2.5 the term $\langle x_0'-x_0,Y_0\rangle$ is written as an expectation, equal to the page's term because $Y_0$ is a.s. constant for the augmented Brownian filtration.

The statements exclude the trivializing encodings: the flow in (3.1) is the law of the forward process in every coefficient, not a free flow; distances and moments use Euclidean norms, not the coordinate supremum norm; the minimizer is the minimizer of $H$, not a free feedback; moment and admissibility conditions are extended-valued integrals compared with $\infty$; and constants declared uniform by the article (Lemma 2.1's Lipschitz constant, Lemma 3.5's $c$, Lemma 3.10's $\lambda',c'_L$) are quantified before the data they are uniform over.

Definitions of the model and solution class, proofs of the eight source-indexed milestones, the goal theorem, and the companion uniqueness result are in scope. The result concerns the source's full class of models satisfying (A.1)–(A.7), rather than a convenient special case.

Selected references

• René Carmona and François Delarue, Probabilistic analysis of mean-field games, SIAM Journal on Control and Optimization 51(4), 2705–2734, 2013. DOI: 10.1137/120883499.
• Jean-Michel Lasry and Pierre-Louis Lions, Mean field games, Japanese Journal of Mathematics 2(1), 229–260, 2007. DOI: 10.1007/s11537-007-0657-8.
• Minyi Huang, Roland P. Malhamé and Peter E. Caines, Large population stochastic dynamic games: closed-loop McKean–Vlasov systems and the Nash certainty equivalence principle, Communications in Information and Systems 6(3), 221–252, 2006. DOI: 10.4310/CIS.2006.v6.n3.a5.
• Shige Peng, A general stochastic maximum principle for optimal control problems, SIAM Journal on Control and Optimization 28(4), 966–979, 1990. DOI: 10.1137/0328054.

Motivation

Complexity bounds for first-order methods (proximal gradient, forward–backward splitting, alternating minimization) rest on a quantitative description of how a function grows away from its set of minimizers. Two such descriptions are in common use. An error bound controls the distance to the minimizers by the function value; a Kurdyka–Łojasiewicz (KL) inequality controls the function value by the size of the subgradients, after a reparameterization $\varphi$. KL inequalities with an explicit $\varphi$ are what the convergence-rate analysis of descent methods needs (Attouch–Bolte 2009, Bolte–Sabach–Teboulle 2014), while error bounds with explicit constants are known for many concrete problem classes (Hölderian bounds for convex polynomials, Hoffman-type bounds, the bounds surveyed by Pang 1997).

Bolte, Nguyen, Peypouquet and Suter (arXiv:1510.08234v3, Math. Program. 165 (2017)) show that for convex functions on a Hilbert space the two notions coincide, with essentially the same function $\varphi$, as soon as $\varphi$ has a mild regularity property they call moderate behavior. This mission formalizes that equivalence (Theorem 5 of the paper) together with the subgradient-curve results its proof rests on.

Timeline:

• 1963: Łojasiewicz's gradient inequality for real-analytic functions; 1998: Kurdyka's extension to functions definable in o-minimal structures.
• 1973: Brézis (reference [23] of the paper) proves existence, uniqueness and regularity of solutions of $\dot\chi \in -\partial f(\chi)$ for convex lower semicontinuous $f$ on a Hilbert space; 1975: Bruck proves weak convergence of these curves to a minimizer.
• 2007–2010: Bolte, Daniilidis, Lewis (and Ley, Mazet) establish the nonsmooth KL inequality and relate it to the length of subgradient curves (Bolte–Daniilidis–Ley–Mazet 2010).
• 2016: the present paper proves the KL/error-bound equivalence for convex functions in Hilbert spaces.

Setting

Let $H$ be a real Hilbert space and $f : H \to (-\infty, +\infty]$ a proper, convex, lower semicontinuous function. Its minimizers form the set $S = \operatorname{argmin} f$, assumed nonempty, and $f$ is normalized so that $\min f = 0$. The subdifferential of $f$ at $x$ is

$$\partial f(x) = \{u \in H : f(y) \ge f(x) + \langle u, y - x\rangle \ \text{for all } y \in H\},$$

and $\operatorname{dom}\partial f$ is the set of points where it is nonempty. For $x \in \operatorname{dom}\partial f$, $\partial^0 f(x)$ is the element of least norm of $\partial f(x)$; for $x \notin \operatorname{dom}\partial f$ one sets $\|\partial^0 f(x)\| = +\infty$. The band $[0 < f < r_0]$ is $\{x : 0 < f(x) < r_0\}$, and $B(\bar x, \rho)$ is the ball of radius $\rho$ around $\bar x$.

A desingularizing function is an element of

$$\mathcal K(0, r_0) = \{\varphi \in C^0[0, r_0) \cap C^1(0, r_0) : \varphi(0) = 0,\ \varphi \text{ concave},\ \varphi' > 0\}.$$

$f$ satisfies the KL inequality on $[0 < f < r_0] \cap B(\bar x, \rho)$ with $\varphi$ if $\varphi'(f(x))\,\|\partial^0 f(x)\| \ge 1$ there, and the error bound with residual function $\varphi$ if $\operatorname{dist}(x, S) \le \varphi(f(x))$ there. $\varphi$ has moderate behavior if $s\varphi'(s) \ge c\varphi(s)$ on $(0, r_0)$ for some $c > 0$.

A subgradient curve issued from $x \in \overline{\operatorname{dom} f}$ is a curve $\chi_x : [0, \infty) \to H$ with $\chi_x(0) = x$ and $\dot\chi_x(t) \in -\partial f(\chi_x(t))$ for almost every $t > 0$; its length between $t$ and $s$ is $\operatorname{length}(\chi_x, t, s) = \int_t^s \|\dot\chi_x(\tau)\|\,d\tau$.

Formalization targets

Goal: Theorem 5 (p. 8)

Let $r_0 > 0$, $\varphi \in \mathcal K(0, r_0)$, $c > 0$, $\rho > 0$ and $\bar x \in S$. Then

$$\Big(\varphi'(f)\,\|\partial^0 f\| \ge 1 \text{ on } [0<f<r_0]\cap B(\bar x,\rho)\Big) \ \Longrightarrow\ \Big(\operatorname{dist}(\cdot, S) \le \varphi(f) \text{ on } [0<f<r_0]\cap B(\bar x,\rho)\Big),$$

and, if $s\varphi'(s) \ge c\varphi(s)$ on $(0, r_0)$,

$$\Big(\operatorname{dist}(\cdot, S) \le \varphi(f) \text{ on } [0<f<r_0]\cap B(\bar x,\rho)\Big) \ \Longrightarrow\ \Big(\varphi'(f)\,\|\partial^0 f\| \ge c \text{ on } [0<f<r_0]\cap B(\bar x,\rho)\Big).$$

Both directions form the single goal theorem.

Milestones

• Theorem 1 (Brézis, Bruck; p. 5): existence and uniqueness of the subgradient curve from each $x \in \overline{\operatorname{dom} f}$; $\frac{d}{dt}\chi_x(t^+) = -\partial^0 f(\chi_x(t))$ and $\frac{d}{dt}f(\chi_x(t^+)) = -\|\dot\chi_x(t^+)\|^2$ for all $t > 0$; $\|\chi_x(t) - z\|$ ($z \in S$) and $f(\chi_x(t))$ nonincreasing, with $f(\chi_x(t)) \to \min f$. Part v) (weak convergence) is not needed and is not stated.
• Theorem 27 (p. 25): for $\bar x \in S$, $\rho > 0$, $\varphi \in \mathcal K(0, r_0)$, the KL inequality on $B(\bar x, \rho) \cap [0 < f < r_0]$ is equivalent to

$$\operatorname{length}(\chi_x, t, s) \le \varphi(f(\chi_x(t))) - \varphi(f(\chi_x(s)))\quad (x \in B(\bar x,\rho)\cap[0<f\le r_0],\ 0 \le t < s),$$

and then $\chi_x(t)$ converges strongly to a minimizer.

Significance

Theorem 5 makes the computation of desingularizing functions a matter of proving error bounds. Since every semi-algebraic or subanalytic $\varphi$ has moderate behavior (Lemma 4 of the paper), any known error bound with such a residual function yields a KL inequality with the same function up to the constant $c$, and through the complexity theorem of §4 of the paper an explicit iteration bound for subgradient descent sequences. The paper uses this route to obtain the linear rate of ISTA for $\ell^1$-regularized least squares and complexity bounds for projection methods.

The result is proved in the paper; to our knowledge none of it is machine-checked. A formalization adds three things: a Lean development of the Brézis subgradient semiflow on a general real Hilbert space (cited, not proved, in the paper), a checked proof of the length estimate of Theorem 27, and the two directions of Theorem 5 on top of them. The semiflow results are reusable well beyond this paper: they underlie the continuous-time analysis of proximal and gradient methods.

Difficulty

Direction (ii) is elementary convex analysis. Direction (i) is not: the error bound is a statement about $\operatorname{dist}(x, S)$, while the hypothesis only constrains subgradients on a band, and the minimizer realizing the bound must be produced. The paper produces it as the strong limit of the subgradient curve from $x$, which requires the existence and regularity theory of the nonlinear evolution equation $\dot\chi \in -\partial f(\chi)$ in an infinite-dimensional Hilbert space (Theorem 1), the energy identity along the curve, and strong (not merely weak) convergence. In finite dimensions compactness would supply limit points; in a Hilbert space Bruck's theorem only gives weak convergence, and it is the length bound of Theorem 27 that upgrades it. Neither the semiflow nor absolutely continuous Hilbert-valued curves with their a.e. derivative calculus are developed in Mathlib to the extent this needs.

Formalization scope

• $H$ is [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]; $f : H \to$ EReal with the published GammaZero f (never $-\infty$, somewhere finite, convex epigraph, lower semicontinuous) and the published subdifferential subgrad. $\min f = 0$ is the hypothesis "$f \ge 0$ and $f$ attains $0$"; $S$ is argminSet f, $\operatorname{dist}(x, S)$ is Metric.infDist.
• $\mathcal K(0, r_0)$ is the published IsDesingularizer r0 φ for $\varphi : \mathbb R \to \mathbb R$; values outside $[0, r_0)$ are irrelevant, and $\varphi'$ is deriv φ, used only on $(0, r_0)$.
• "$\varphi'(f(x))\,\|\partial^0 f(x)\| \ge \kappa$" is formalized as "$\varphi'(f(x))\,\|v\| \ge \kappa$ for every $v \in \partial f(x)$", which encodes the convention $\|\partial^0 f(x)\| = +\infty$ off $\operatorname{dom}\partial f$. Balls are open.
• A subgradient curve is continuous on $[0, \infty)$, absolutely continuous on every compact subinterval of $(0, \infty)$ (and on every $[0, b]$ when $f(x) < +\infty$), and satisfies the inclusion at almost every $t > 0$; length is a $[0, +\infty]$-valued integral. Statements quantify over every curve from $x$; Theorem 1 makes this "the" curve.
• In Theorem 27 ii) the length bound is required whenever $f(\chi_x(t)) < r_0$, since $\varphi$ is undefined at $r_0$.
• A trivializing formalization is ruled out: the curve predicate is shown non-vacuous by the existence milestone (and is satisfied by $\chi(t) = x e^{-t}$ for $f(y) = y^2/2$ on $\mathbb R$), and the KL hypothesis quantifies over all subgradients, so it cannot be met by choosing a convenient one.
• Theorem indices and pages are those of the arXiv preprint version 3 (arXiv:1510.08234v3), not of the journal version.
• Welcome contributions: the Brézis theory (Theorem 1), possibly via the Moreau–Yosida approximation or the proximal (implicit Euler) scheme; calculus for absolutely continuous Hilbert-valued curves; proofs of Theorem 27 and of Theorem 5.

Selected references

• J. Bolte, T. P. Nguyen, J. Peypouquet, B. W. Suter, From error bounds to the complexity of first-order descent methods for convex functions, Math. Program. 165 (2017) 471–507; arXiv:1510.08234v3. https://arxiv.org/abs/1510.08234v3, https://doi.org/10.1007/s10107-016-1091-6
• H. Brézis, Opérateurs maximaux monotones et semi-groupes de contractions dans les espaces de Hilbert, North-Holland Mathematics Studies 5, 1973 (reference [23] of arXiv:1510.08234v3).
• R. E. Bruck, Asymptotic convergence of nonlinear contraction semigroups in Hilbert space, J. Funct. Anal. 18 (1975) 15–26. https://doi.org/10.1016/0022-1236(75)90027-0
• J. Bolte, A. Daniilidis, O. Ley, L. Mazet, Characterizations of Łojasiewicz inequalities: subgradient flows, talweg, convexity, Trans. Amer. Math. Soc. 362 (2010) 3319–3363. https://doi.org/10.1090/S0002-9947-09-05048-X
• H. Attouch, J. Bolte, On the convergence of the proximal algorithm for nonsmooth functions involving analytic features, Math. Program. 116 (2009) 5–16. https://doi.org/10.1007/s10107-007-0133-5
• J. Bolte, S. Sabach, M. Teboulle, Proximal alternating linearized minimization for nonconvex and nonsmooth problems, Math. Program. 146 (2014) 459–494. https://doi.org/10.1007/s10107-013-0701-9
• J.-S. Pang, Error bounds in mathematical programming, Math. Program. 79 (1997) 299–332. https://doi.org/10.1007/BF02614322

Why strong rates for non-monotone SDEs matter

Stochastic differential equations (SDEs) $dX_t=\mu(X_t)\,dt+\sigma(X_t)\,dW_t$ model physical, biological and financial systems whose drift $\mu$ often grows superlinearly: the stochastic Lorenz equation, the stochastic van der Pol and Duffing–van der Pol oscillators, Langevin dynamics. Solutions are rarely explicit, so they are simulated by time-stepping schemes. For multilevel Monte Carlo methods (Giles 2008) the cost of a simulation is governed by the strong convergence rate, the speed at which $\|X_t-Y_t\|_{L^r(\Omega)}$ tends to $0$ as the step size shrinks.

For superlinearly growing coefficients the classical Euler–Maruyama method diverges in $L^p$ (Hutzenthaler, Jentzen, Kloeden 2011). Tamed schemes repair this, and rate $\tfrac12$ was proved for them under a global monotonicity condition: $\langle x-y,\mu(x)-\mu(y)\rangle+\frac{p-1}{2}\|\sigma(x)-\sigma(y)\|^2\le c\|x-y\|^2$ for all $x,y$ (Hutzenthaler, Jentzen, Kloeden 2012; Sabanis 2016). Most of the examples above violate that condition. Before this paper no strong rate was known for any time-discrete scheme for a multidimensional SDE with non-globally monotone coefficients.

Timeline. 2011: divergence of explicit Euler for superlinear drifts. 2012: tamed Euler, rate $\tfrac12$ under one-sided Lipschitz drift and globally Lipschitz diffusion. 2012–2013: strong convergence without rates for non-globally monotone SDEs (stopped and tamed schemes). 2014: this paper (arXiv:1401.0295), rate $\tfrac12$ for the stopped-tamed Euler–Maruyama scheme under the conditions below; published in Ann. Probab. 48 (2020).

Setting

Fix $d,m\in\mathbb N=\{1,2,\dots\}$ and $T\in(0,\infty)$. On a probability space with a normal filtration $(\mathcal F_t)$, $W$ is a standard $m$-dimensional $(\mathcal F_t)$-Brownian motion. Matrices $A\in\mathbb R^{d\times m}$ carry the Hilbert–Schmidt norm $\|A\|_{HS}=(\sum_{ij}A_{ij}^2)^{1/2}$. Given coefficients $\mu:\mathbb R^d\to\mathbb R^d$ and $\sigma:\mathbb R^d\to\mathbb R^{d\times m}$, $X$ is an adapted continuous process with

$$X_t=X_0+\int_0^t\mu(X_s)\,ds+\int_0^t\sigma(X_s)\,dW_s,\qquad t\in[0,T].$$

The taming map is $\psi(v)=v/(1+\|v\|^2)$. The stopped-tamed Euler–Maruyama scheme with $N$ steps is $Z^N_0=X_0$ and

$$Z^N_{n+1}=Z^N_n+\mathbb 1_{\{\|Z^N_n\|<\exp(|\ln(T/N)|^{1/2})\}}\;\psi\Big(\mu(Z^N_n)\tfrac TN+\sigma(Z^N_n)\big(W_{(n+1)T/N}-W_{nT/N}\big)\Big).$$

The whole increment, drift and noise together, is tamed, and the scheme freezes once it leaves a ball whose radius grows slowly as $N\to\infty$.

The conditions use a Lyapunov-type function $U_0\ge1$ and a function $U_1\ge0$. The generator is $(\mathcal G_{\mu,\sigma}\varphi)(x)=\varphi'(x)\mu(x)+\frac12\sum_j\varphi''(x)(\sigma_j(x),\sigma_j(x))$, where $\sigma_j(x)$ is the $j$-th column of $\sigma(x)$. For partitions $\theta=(0=t_0<\dots<t_n=T)$ with mesh $|\theta|=\max_k(t_{k+1}-t_k)$, the same recursion run in continuous time on $[t_k,t_{k+1}]$ defines interpolations $Y^\theta$.

Formalization targets

Goal: Theorem 1.3

Let $c,r\in(0,\infty)$, $q_0,q_1\in(0,\infty]$, $\alpha\ge0$ and $p,q\in[2,\infty)$ with $\frac1p+\frac1{q_0}+\frac1{q_1}=\frac1r$. Let $\mu,\sigma,U_1$ be $C^1$ with polynomially growing derivatives. Let $U_0\in C^3$ satisfy $U_0\ge1$, $\sum_{i\le3}\|U_0^{(i)}\|\le cU_0^{1-1/q}$, $\|x\|^{1/c}\le c(1+U_0(x))$ and $\mathbb E[e^{U_0(X_0)}]<\infty$, and assume for $x\neq y$

$$\frac{\langle x-y,\mu(x)-\mu(y)\rangle+\frac{(p-1)(1+1/c)}{2}\|\sigma(x)-\sigma(y)\|_{HS}^2}{\|x-y\|^2}\le c+\frac{U_0(x)+U_0(y)}{2q_0Te^{\alpha T}}+\frac{U_1(x)+U_1(y)}{2q_1e^{\alpha T}},$$ $$(\mathcal G_{\mu,\sigma}U_0)(x)+\tfrac12\|\sigma(x)^*\nabla U_0(x)\|^2+U_1(x)\le\alpha U_0(x)+c.$$

Then there is $C\in[0,\infty)$ such that for all $N\in\mathbb N$,

$$\sup_{n\in\{0,\dots,N\}}\|X_{nT/N}-Z^N_n\|_{L^r(\Omega)}\le C\,N^{-1/2}.$$

The constant $C$ is not specified. Only the rate is asserted, and that is the stable content of the result.

Milestones

In the proof's order:

• Proposition 2.9: a pathwise Itô inequality for $\|X-Y\|^p$ between a solution and an arbitrary Itô process.
• Theorem 2.10: the perturbation estimate, which bounds $\|X_\tau-Y_\tau\|_{L^r}$ by an exponential moment of the monotonicity ratio times the local errors.
• Corollary 2.12 (= Theorem 1.2): the same estimate with $L^p$ local errors.
• Lemma 3.1: derivative bounds for $\psi$.
• Lemma 3.2: the error estimate on one partition for the scheme stopped at its first grid exit from a set $\mathcal O$.
• Proposition 3.3: $\sup_{t\le T}\|X_t-Y^\theta_t\|_{L^r}\le C|\theta|^{1/2}$ uniformly over all partitions $\theta$. Theorem 1.3 is its uniform-grid case.

Significance

Theorem 1.3 gives strong rate $\tfrac12$, and with it the complexity bounds of multilevel Monte Carlo, for SDEs with non-globally monotone coefficients. The paper's applications include the stochastic Lorenz equation with bounded noise, the stochastic van der Pol and Duffing–van der Pol oscillators, a model from experimental psychology and overdamped Langevin dynamics. The perturbation estimate, Theorem 2.10, is a separate tool. It compares a solution with any Itô process, so it also gives local Lipschitz dependence on the initial value and, in the paper's §3.2, rates for Galerkin approximations of SPDEs.

All results listed here are proved in the paper, and none has been machine-checked so far. This mission produces Lean statements of the goal and of every numbered step of its proof. The development needs Itô calculus for $\|x-y\|^p$, a localization argument, exponential-moment bounds via Lyapunov functions, and calculus for the taming map. Several of these pieces are reusable well beyond this paper.

Difficulty

The obvious argument is Gronwall's lemma applied to $\mathbb E\|X_t-Y_t\|^p$. It needs the global bound $\langle x-y,\mu(x)-\mu(y)\rangle\le c\|x-y\|^2$, which fails for the Lorenz and van der Pol drifts: there the one-sided Lipschitz "constant" grows with $|x|+|y|$. The difficulty is to control a random, state-dependent Gronwall exponent $\int_0^t[\text{ratio}(X_s,Y_s)]^+ds$. That requires exponential integrability of $U_0(X_t)$ and $U_1$ along both the solution and the scheme. For the scheme it holds only because of the taming and the stopping, and only up to an error of the right order.

Formalization scope

• Representation. States are EuclideanSpace ℝ (Fin d). Diffusion values are the published Diffusion d m, whose norm is the Hilbert–Schmidt norm the paper uses throughout. Time is $\mathbb R_{\ge0}$.
• Probability model. Solutions and Itô processes are the published SabanisEuler.Shared.IsSolution / IsItoProcess. The normal filtration is right-continuity plus completion, and $W$ is the published IsWienerMartingale, a Brownian motion on $[0,\infty)$. For $H=\mathbb R^d$, $U=\mathbb R^m$ the paper's cylindrical Wiener process is exactly such a Brownian motion. All processes are hypotheses; existence is never claimed.
• Finite-dimensional specialization. The paper states §2 for separable Hilbert spaces. Propositions 2.9, Theorem 2.10 and Corollary 2.12 are formalized for $H=\mathbb R^d$, $U=\mathbb R^m$, the only case the proof of Theorem 1.3 uses. Proposition 2.9 is further restricted to $\varepsilon\in(0,\infty)$. Proposition 2.5, Theorem 1.4 and the SPDE results of §3.2 are not part of the mission.
• Extended arithmetic. Every norm, moment and exponential moment lies in $[0,\infty]$, with $0\cdot\infty=0$, $0/0=0$, $1/0=\infty$ and $\exp(\infty)=\infty$. The monotonicity ratio is computed in extended reals, so $\varepsilon=\infty$ and $q_0=\infty$ are allowed. Predictable processes are predictable with respect to $(\mathcal F_t)$, and stopping times are taken with respect to the completed filtration.
• Ruling out trivial versions. The exponential-moment hypothesis is a Lebesgue integral in $[0,\infty]$, never a Bochner integral that would default to $0$. Stochastic integrals are pinned down by the published Itô-integral relation, never left as free witnesses. The classes $\mathcal C^1_{\mathcal P}$ (locally Lipschitz with polynomial constant) and $\mathcal C^3_{\mathcal D}$ of Proposition 3.3 are not replaced by $C^1$/$C^3$. A sorry-free check confirms that the goal's hypotheses are jointly satisfiable.
• Contributions welcome. Itô's formula for $C^2$ functions of two Itô processes, Burkholder–Davis–Gundy-type moment bounds for the scheme increments, and exponential-moment estimates from Lyapunov conditions (the paper relies on Cox, Hutzenthaler, Jentzen 2013). Each is reusable beyond this mission.

Selected references

• M. Hutzenthaler, A. Jentzen, On a perturbation theory and on strong convergence rates for stochastic ordinary and partial differential equations with non-globally monotone coefficients, arXiv:1401.0295v1, 2014; Ann. Probab. 48(1), 2020. https://arxiv.org/abs/1401.0295
• M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong convergence of an explicit numerical method for SDEs with nonglobally Lipschitz continuous coefficients, Ann. Appl. Probab. 22(4), 2012. https://doi.org/10.1214/11-AAP803
• M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong and weak divergence in finite time of Euler's method for SDEs with non-globally Lipschitz coefficients, Proc. R. Soc. A 467, 2011. https://doi.org/10.1098/rspa.2010.0348
• S. Sabanis, Euler approximations with varying coefficients: the case of superlinearly growing diffusion coefficients, Ann. Appl. Probab. 26(4), 2016. https://doi.org/10.1214/15-AAP1140
• S. Cox, M. Hutzenthaler, A. Jentzen, Local Lipschitz continuity in the initial value and strong completeness for nonlinear SDEs, arXiv:1309.5595, 2013. https://arxiv.org/abs/1309.5595
• M. B. Giles, Multilevel Monte Carlo path simulation, Oper. Res. 56(3), 2008. https://doi.org/10.1287/opre.1070.0496