Partial Differential Equations

Motivation

Systems of many particles that interact through a singular pair potential and are subject to independent noise appear in plasma physics (Coulomb interactions), in vortex models of fluids, in models of collective behaviour and in the analysis of training dynamics of wide neural networks. When the number of particles $N$ is large, the empirical measure of the system is expected to follow a deterministic nonlinear partial differential equation, the mean-field limit. For singular interactions the classical coupling arguments, which need Lipschitz forces, do not apply. The modulated-energy method of Serfaty (Duke Math. J. 2020) and its extensions by Duerinckx, Nguyen, Rosenzweig and Serfaty (NRS21, arXiv:2107.02592) give quantitative convergence for Riesz-type potentials $|x|^{-s}$, but with rates that degrade exponentially in time.

M. Rosenzweig and S. Serfaty (arXiv:2108.09878v1, 2021) show that additive noise improves this: the expected modulated energy grows at most polynomially in time for sub-Coulombic potentials (their Theorem 1.1, the subject of the first mission of this series), and stays bounded uniformly in time when the potential is globally superharmonic (their Theorem 1.2, the subject of this mission). Uniform-in-time propagation of chaos had been known for smooth or convex interactions; this result covers singular, non-gradient interactions on the whole space.

Setting

Fix $d\ge3$, an exponent $0\le s<d-2$, a diffusion strength $\sigma>0$ and a $d\times d$ matrix $\mathbb M$ with $\mathbb M\xi\cdot\xi\le0$ for all $\xi$. The particle system is

$$dx^t_i=\frac1N\sum_{j\ne i}\mathbb M\nabla\mathsf g(x^t_i-x^t_j)\,dt+\sqrt{2\sigma}\,dW^t_i,\qquad i=1,\dots,N,$$

started from pairwise distinct points $x^0_N=(x^0_1,\dots,x^0_N)$ and driven by independent standard Brownian motions $W_1,\dots,W_N$ in $\mathbb R^d$. The potential $\mathsf g$ is admissible: it satisfies ten assumptions (i)–(x) on symmetry, blow-up at $0$, superharmonicity near $0$, derivative bounds of order $|x|^{-s-k}$, a doubling property, a Fourier transform comparable to $|\xi|^{-(d-s)}$, an extension to $\mathbb R^{d+m}$ when $d-4<s$, a Calderón–Zygmund property in the cases $s=d-2k$, and $\mathbb M:\nabla^{\otimes2}\mathsf g\ge0$. The model case is $\mathsf g(x)=|x|^{-s}$.

The mean-field equation is

$$\partial_t\mu=-\operatorname{div}(\mu\,\mathbb M\nabla\mathsf g*\mu)+\sigma\Delta\mu,\qquad\mu|_{t=0}=\mu^0,$$

for a probability density $\mu^0\in L^\infty$, solved in the mild (Duhamel) sense in $C([0,\infty);L^1\cap L^\infty)$. Closeness of the empirical measure $\mu_N^t=\frac1N\sum_i\delta_{x^t_i}$ to $\mu^t$ is measured by the modulated energy

$$F_N(x_N,\mu)=\int_{(\mathbb R^d)^2\setminus\triangle}\mathsf g(x-y)\,d\Big(\frac1N\sum_{i=1}^N\delta_{x_i}-\mu\Big)^{\otimes2}(x,y),$$

where the diagonal $\triangle$ is removed. The potential is globally superharmonic if $\Delta\mathsf g\le0$ on all of $\mathbb R^d\setminus\{0\}$ ("$r_0=\infty$" in assumption (iii)).

Formalization targets

Goal: Theorem 1.2 for $0<s<d-2$

For globally superharmonic admissible $\mathsf g$ and every $d/(s+2)<p\le\infty$ there are $\beta_p>0$ (depending on $s,d,p$), $C>0$ (depending on $s,d,\sigma,\mathbb M,\mathsf g,\|\mu^0\|_{L^\infty}$), $C_p>0$ and $N_0$ such that for all $t\ge0$ and $N\ge N_0$,

$$\mathbb E\big(|F_N(x^t_N,\mu^t)|\big)\le C\big(|F_N(x^0_N,\mu^0)|+C_pN^{-\beta_p}\big).$$

The right side does not depend on $t$. The case $s=0$ of the paper's display (1.19) is not part of the goal (see Formalization scope).

Milestones

The proof combines an inequality for the time derivative of the expected modulated energy (Proposition 6.3), lower bounds for the energy and for the diffusion term (Remarks 5.10, 5.11, Proposition 5.12, Remark 5.13, Corollary 5.14), a commutator estimate for the transport term (Proposition 5.15), and decay of $\|\mu^t\|_{L^p}$ (Remark 3.4, Proposition 3.8), with the potential estimates of Lemma 2.3 and Remark 2.5.

Significance

A uniform-in-time bound means that the mean-field description is valid on time scales that do not shrink as the accuracy requirement grows. Combined with the control of negative Sobolev norms by the modulated energy, it yields uniform-in-time convergence in law of the empirical measure and, for chaotic initial data, uniform-in-time propagation of chaos at an explicit rate, for singular interactions such as sub-Coulombic Riesz gases with dissipative or conservative dynamics.

The result is proved in the paper. No part of it, nor of the modulated-energy method, is formalized in any proof assistant. A formalization would produce a reusable library: Riesz potentials and their $L^1$–$L^p$ interpolation, heat-type decay of nonlinear Fokker–Planck equations, smeared potentials and electric-energy lower bounds, renormalized commutator estimates, and a pathwise treatment of interacting diffusions with additive noise. The milestones are independent statements and can be proved separately.

Difficulty

The obvious Gronwall argument on the modulated energy fails twice. First, $F_N$ is not nonnegative; it is bounded below only up to errors involving $\|\mu\|_{L^\infty}$, and the lower bounds near the singularity need the smearing of point charges on spheres. Second, the error terms produced when the commutator and diffusion terms are bounded must be integrable on $[0,\infty)$; with the estimates of the general (local superharmonicity) case they grow linearly in time. Global superharmonicity removes an $\eta^2$ error term and lets every error carry a power of $\|\mu^t\|_{L^\infty}$, which decays like $(\sigma t)^{-d/2}$ by the Carlen–Loss method; for $s=0$ long-range effects still produce growth, which is why that case is excluded. Itô's formula cannot be applied directly to the singular energy and requires a truncation, whose stochastic integrals are removed in expectation only in the limit.

Formalization scope

All objects live in the Lean namespace RieszMF.Global and in one definitions module. Space is EuclideanSpace ℝ (Fin d); derivatives are iteratedFDeriv (operator norm), gradient and the Laplacian of Mathlib. The committed conventions:

1. Fourier conditions (vi) and (1.17) are read away from the origin: a function $\hat{\mathsf g}$ with $\int\mathsf g\,\mathcal F\varphi=\int\hat{\mathsf g}\varphi$ for Schwartz $\varphi$ vanishing near $0$.
2. Assumption (iv) has a constant $C_k$ for each $k$; quantities singular at $0$ are required for $x\neq0$ only; (ix) is stated componentwise with an $L^2$-bounded operator represented by the kernel off the support.
3. Global superharmonicity is $\Delta\mathsf g\le0$ on $\mathbb R^d\setminus\{0\}$, together with (1.15)–(1.16) on all of $\mathbb R^{d+m}\setminus\{0\}$ when $d-4<s$; (v) and (vii) keep a finite radius.
4. Doubling condition (vii) for $s>0$ is read as $\mathsf g(y)<c_s\mathsf g(x)$ whenever $|y|\ge2|x|$, $x\ne0$, with $c_s<1$. The page prints $\mathsf g(x)<c_s\mathsf g(y)$, which contradicts the blow-up (ii) and would leave no admissible potential, so the goal would hold vacuously. The model potential $|x|^{-s}$ satisfies the reading used here.
5. The particle system is the pathwise integral equation (no Itô integral is needed for additive noise), with continuous paths and no collisions almost surely; the Brownian family is $N\cdot d$ jointly independent standard real Brownian motions.
6. The mild formulation of (1.5) requires every integral to converge absolutely and continuity in $L^1\cap L^\infty$.
7. Expectations of $|F_N|$ are lower Lebesgue integrals, and Proposition 6.3 moves positive and negative parts across the inequality, so no integrability is presupposed and no $\infty-\infty$ arises.
8. Constants are quantified after exactly the objects they may depend on: $\beta_p$ after $s,d,p$; $C$ after $\sigma,\mathbb M,\mathsf g$ and $\|\mu^0\|_{L^\infty}$; $C_p$ and $N_0$ after $p$; all before $\mu^0$, $N$, the configuration, the probability space and $t$.

Restriction. The goal is Theorem 1.2 for $0<s<d-2$ only, where the paper's time factor $1+(t^{1/\sigma}\log(1+t))\mathbf 1_{s=0}$ equals $1$. For $s=0$ the proof yields a factor of order $t^{C/\sigma}$ rather than the printed $t^{1/\sigma}\log(1+t)$; the logarithmic case is covered by the first mission of this series.

Excluded trivializations. A statement in which $C$ is chosen after $\mu^0$, $N$ or the configuration, in which a divergent integral is read as $0$, in which the solution classes are empty, or which uses $N=0$ or a division by zero is not a formalization of the theorem; the statements here avoid each of these.

Contributions are welcome on any milestone, on the existence of solutions in the classes used (which shows the hypotheses are satisfiable), and on general infrastructure (Riesz potentials, sphere averages, heat-kernel estimates) that other missions can reuse.

Selected references

• M. Rosenzweig, S. Serfaty, Global-in-time mean-field convergence for singular Riesz-type diffusive flows, arXiv:2108.09878v1, 2021; Ann. Appl. Probab. 33(2), 2023. https://arxiv.org/abs/2108.09878
• Q.-H. Nguyen, M. Rosenzweig, S. Serfaty, Mean-field limits of Riesz-type singular flows, Ars Inveniendi Analytica, 2022. https://arxiv.org/abs/2107.02592
• S. Serfaty, Mean field limit for Coulomb-type flows, Duke Math. J. 169(15), 2020. https://doi.org/10.1215/00127094-2020-0019
• M. Duerinckx, Mean-field limits for some Riesz interaction gradient flows, SIAM J. Math. Anal. 48(3), 2016. https://doi.org/10.1137/15M1042620
• E. A. Carlen, M. Loss, Optimal smoothing and decay estimates for viscously damped conservation laws, with applications to the 2-D Navier–Stokes equation, Duke Math. J. 81(1), 1995. https://doi.org/10.1215/S0012-7094-95-08110-1

Motivation

Systems of $N$ particles that interact through a singular pair potential and are driven by independent noise are used to model vortices in viscous fluids, collective motion of micro-organisms, aggregation phenomena and, more recently, the training dynamics of wide neural networks and stochastic gradient methods. When $N$ is large, one expects the empirical measure of the particles to be close to the solution of a deterministic nonlinear PDE, the mean-field limit. Proving this with an explicit rate is difficult when the interaction is singular, because the classical coupling arguments need a Lipschitz force.

The modulated-energy method (Duerinckx 2016, Serfaty 2020, Nguyen–Rosenzweig–Serfaty 2021) measures the distance between the particles and the limit through a renormalized Coulomb/Riesz energy and closes a Gronwall argument on it. Rosenzweig and Serfaty (arXiv:2108.09878) extended it to systems with additive noise in the sub-Coulombic range. This mission formalizes their first main result, Theorem 1.1: the expected modulated energy grows at most linearly in time (polynomially for logarithmic interactions). A companion mission covers their uniform-in-time Theorem 1.2.

Setting

Fix $d\ge3$ and $0\le s<d-2$. Positions live in $\mathbb R^d$ with Lebesgue measure. A $d\times d$ real matrix $\mathbb M$ satisfies $\mathbb M\xi\cdot\xi\le0$ for all $\xi$ (gradient flows $\mathbb M=-\mathbb I$, Hamiltonian flows $\mathbb M$ antisymmetric, and mixtures). The interaction potential $\mathsf g:\mathbb R^d\to\mathbb R$ is admissible: it satisfies ten assumptions (i)–(x), with model cases $\mathsf g(x)=-\log|x|$ ($s=0$) and $\mathsf g(x)=|x|^{-s}$ ($0<s<d-2$). In short: $\mathsf g$ is even, blows up at $0$, is superharmonic on a punctured ball $B(0,r_0)\setminus\{0\}$, is smooth off the origin with $|\nabla^{\otimes k}\mathsf g(x)|\le C_k|x|^{-(s+k)}$ (plus a logarithm when $s=k=0$), has a Fourier transform comparable to $|\xi|^{s-d}$, has a doubling property near $0$, admits a superharmonic extension to $\mathbb R^{d+m}$ when $d-4<s$, has a Calderón–Zygmund kernel condition when $s=d-2k$, and satisfies $\mathbb M:\nabla^{\otimes2}\mathsf g\ge0$.

The particle system (1.1) is

$$dx^t_i=\frac1N\sum_{j\ne i}\mathbb M\nabla\mathsf g(x^t_i-x^t_j)\,dt+\sqrt{2\sigma}\,dW^t_i,\qquad x^t_i|_{t=0}=x^0_i,$$

with distinct initial points, $\sigma>0$, and $W_1,\dots,W_N$ independent standard Brownian motions in $\mathbb R^d$. The mean-field equation (1.5) is

$$\partial_t\mu=-\operatorname{div}(\mu\,\mathbb M\nabla\mathsf g*\mu)+\sigma\Delta\mu,\qquad\mu|_{t=0}=\mu^0,$$

for a bounded probability density $\mu^0$, solved in the class $C([0,\infty);\mathcal P(\mathbb R^d)\cap L^\infty(\mathbb R^d))$. The modulated energy (1.6) is

$$F_N(x_N,\mu)=\int_{(\mathbb R^d)^2\setminus\triangle}\mathsf g(x-y)\,d\Big(\frac1N\sum_{i=1}^N\delta_{x_i}-\mu\Big)^{\otimes2}(x,y),$$

the diagonal $\triangle$ being removed to discard the infinite self-interaction of each particle.

Formalization targets

Goal: Theorem 1.1

There are $\beta>0$ depending on $s,d$ only and, for every $\sigma$, $\mathbb M$, admissible $\mathsf g$ and value of $\|\mu^0\|_{L^\infty}$, a constant $C>0$ and a threshold $N_0$ such that for all $N\ge N_0$ and $t\ge0$

$$\mathbb E\big(|F_N(x^t_N,\mu^t)|\big)\le C\Big(1+t+t^{\frac{\sigma+C}\sigma}\mathbf 1_{s=0}\Big)\Big(|F_N(x^0_N,\mu^0)|+N^{-\beta}\Big).$$

The exponent $\beta$ and the constant are left unspecified, as in the paper.

Milestones

In the order the proof uses them:

1. Lemma 2.3 and Remark 2.5: $L^\infty$ bounds for Riesz potentials and for $\nabla^{\otimes k}\mathsf g*f$.
2. Remark 3.4, Proposition 3.9 and Proposition 3.8: $L^p$ monotonicity, the sharp log-Sobolev inequality, and heat-equation decay $\|\mu^t\|_{L^q}\lesssim(\sigma t)^{-\frac d2(\frac1p-\frac1q)}\|\mu^0\|_{L^p}$.
3. Proposition 4.5: the particle system has a unique strong solution whose particles never collide, obtained as the limit of smoothly truncated systems.
4. Remarks 5.2, 5.3 and Proposition 5.4: lower bounds on $F_N$ through smeared point charges.
5. Corollary 5.6: the diffusion term $\iint(-\Delta\mathsf g)\,d(\mu_N-\mu)^{\otimes2}$ is bounded below by $-C(1+\|\mu\|_{L^\infty})N^{-\min\{2,d-s-2\}/\min\{s+4,d\}}$.
6. Proposition 5.7: the renormalized commutator estimate.
7. Proposition 6.3: the expected Itô inequality for $F_N$.

Significance

The theorem is a quantitative mean-field limit for singular interactions with additive noise on the whole space, covering conservative and dissipative dynamics at once. Since $F_N$ controls a negative-order Sobolev distance between $\mu_N^t$ and $\mu^t$, it gives convergence of the empirical measure, at a rate in $N$ that deteriorates at most linearly in $t$ for $s>0$. Its proof isolates estimates (the $L^p$ decay of the nonlinear equation, the sign of the diffusion term, the commutator bound) that are reused for the uniform-in-time result of the companion mission.

The paper's results are proved; none of them has a machine-checked proof. Formalizing the theorem requires the modulated-energy machinery (smeared charges, Fourier positivity, commutator estimates), a Carlen–Loss decay argument, and an Itô-free treatment of the stochastic system. The milestones of §§2–3 are classical harmonic analysis (Riesz potentials, the Gross–Carlen log-Sobolev inequality) and are of independent use.

Difficulty

A direct Gronwall argument on $\mathbb E|F_N|$ fails twice. The diffusion term $\sigma\iint\Delta\mathsf g\,d(\mu_N-\mu)^{\otimes2}$ has no sign for a general configuration, because the singularity of $\Delta\mathsf g$ at the origin is integrated against a signed measure with atoms; its control needs a second modulated-energy estimate for $-\Delta\mathsf g$, which is a potential of order $s+2$ and may be super-Coulombic, hence the extension of assumption (viii). The commutator term requires $\|\nabla u^t\|_{L^\infty}$, and bounding it by $\|\mu^0\|_{L^\infty}$ alone produces exponential growth in time; the polynomial bound needs the time decay of $\|\mu^t\|_{L^\infty}$, which for a nonlinear, non-divergence-free drift is not given by comparison with the heat equation. Finally, the Itô computation for $F_N$ along the singular dynamics needs truncation and stopping times, since $\mathsf g$ is not $C^2$ at collisions.

Formalization scope

All objects are defined in one module RieszMF.Linear.Setting. Space is EuclideanSpace ℝ (Fin d) with Lebesgue measure; derivatives are iteratedFDeriv with operator norms, $\Delta$ is Mathlib's Laplacian, and the Fourier transform is Mathlib's $\int e^{-2\pi ix\cdot\xi}\varphi(x)\,dx$. Assumption (iv) is read with a constant $C_k$ for each $k$; (vi) and (1.17) as Fourier transforms paired with Schwartz functions vanishing near the origin; (iii) pointwise on the punctured ball; one radius $r_0$ for (iii), (v), (vii), (viii); $m\ge1$ in (viii). Assumption (vii) for $s>0$ is printed as $\mathsf g(x)<c_s\mathsf g(y)$ for $|y|\ge2|x|$, which together with (ii) is unsatisfiable; it is stated as $\mathsf g(y)<c_s\mathsf g(x)$.

The solution of (1.5) is a mild solution (3.1) in $C([0,\infty);L^1\cap L^\infty)$ with continuity in the $L^1+L^\infty$ norm, with each $\mu^t$ a probability density; every integral of (3.1) is required to converge. Because the noise is additive, a solution of (1.1) is a measurable process whose paths almost surely are continuous, never collide, and satisfy the integral equation with the Brownian path; no stochastic integral appears. Brownian motions are Mathlib's IsBrownianReal coordinates, jointly independent over all $N\cdot d$ coordinates. Expectations are lower Lebesgue integrals of nonnegative quantities, and Proposition 6.3 is stated in $[0,\infty]$ with positive and negative parts on opposite sides, so no $\infty-\infty$ and no default value of a divergent integral enters.

The constants follow the paper's dependency lists: $\beta$ depends on $s,d$ only and is chosen before $\sigma,\mathbb M,\mathsf g$; $C$ and $N_0$ are chosen after $\sigma,\mathbb M,\mathsf g,r_0$ and $\|\mu^0\|_{L^\infty}$, before the data, $N$, the configuration, the probability space and $t$. A formalization with constants chosen after $\mu^0$, $N$ or the configuration, with $N=0$, with a junk-zero integral in $F_N$ or in (3.1), or with an empty solution class does not count. Corollary 5.6 is posed exactly under its printed assumptions, although its proof for $0\le s\le d-4$ uses the superharmonicity of $-\Delta\mathsf g$, which those assumptions do not list.

Contributions welcome: proofs of the milestones, a Lean development of Riesz potentials and of the sharp log-Sobolev inequality on $\mathbb R^d$, and the well-posedness of the mean-field equation that the goal takes as a hypothesis (Proposition 3.1 and its global continuation, not posed here).

Selected references

• M. Rosenzweig, S. Serfaty, Global-in-time mean-field convergence for singular Riesz-type diffusive flows, arXiv:2108.09878v1, 2021; Ann. Appl. Probab. 33(2), 2023. https://arxiv.org/abs/2108.09878
• Q. H. Nguyen, M. Rosenzweig, S. Serfaty, Mean-field limits of Riesz-type singular flows with possible multiplicative transport noise, arXiv:2107.02592, 2021. https://arxiv.org/abs/2107.02592
• S. Serfaty, Mean field limit for Coulomb-type flows, Duke Math. J. 169(15), 2887–2935, 2020 (appendix with M. Duerinckx). https://arxiv.org/abs/1803.08345
• E. Carlen, M. Loss, Optimal smoothing and decay estimates for viscously damped conservation laws, with applications to the 2-D Navier–Stokes equation, Duke Math. J. 81(1), 1995. https://doi.org/10.1215/S0012-7094-95-08110-1
• L. Gross, Logarithmic Sobolev inequalities, Amer. J. Math. 97(4), 1975. https://doi.org/10.2307/2373688

Motivation

Many stochastic models evolve on two time scales: a fast component that equilibrates quickly and a slow component driven by it. Planetary motion, climate models, geophysical flows and intracellular reaction networks are standard examples, and multiscale numerical methods for them approximate the slow component by a reduced equation. Such approximations are only useful with an error bound, and for the fully coupled case, where the fast and slow equations each depend on both components and the slow equation contains a large fluctuating drift, rates of convergence were missing.

Röckner and Xie (Ann. Probab. 49 (2021) 1205–1236) treat this case with only Hölder continuous coefficients and obtain explicit rates in four regimes. This mission poses the first regime, the classical averaging principle.

Timeline. Papanicolaou, Stroock and Varadhan (1977) proved the diffusion approximation for $\alpha_\varepsilon=\beta_\varepsilon=\gamma_\varepsilon$ with a compact fast state space and time-independent coefficients. Pardoux and Veretennikov (2001, 2003, 2005) treated a noncompact homogeneous case with $c\equiv0$ and $\alpha_\varepsilon=\gamma_\varepsilon$ by martingale problems and the Poisson equation. Rates for the averaging principle when $c=H\equiv0$ were obtained by several authors, e.g. Givon (2007) and Liu (2010). Röckner and Xie (2021) give rates for the fully coupled system with Hölder coefficients in all four regimes.

Setting

Let $x\in\mathbb R^{d_1}$ (fast) and $y\in\mathbb R^{d_2}$ (slow), $d_1,d_2\ge1$. For small parameters $\alpha_\varepsilon,\beta_\varepsilon,\gamma_\varepsilon>0$ tending to $0$, with $\alpha_\varepsilon^2/\beta_\varepsilon\to0$, the two-scale system (1.4) is

$$dX^\varepsilon_t=\alpha_\varepsilon^{-2}b(X^\varepsilon_t,Y^\varepsilon_t)dt+\beta_\varepsilon^{-1}c(X^\varepsilon_t,Y^\varepsilon_t)dt+\alpha_\varepsilon^{-1}\sigma(X^\varepsilon_t,Y^\varepsilon_t)dW^1_t,$$ $$dY^\varepsilon_t=F(t,X^\varepsilon_t,Y^\varepsilon_t)dt+\gamma_\varepsilon^{-1}H(t,X^\varepsilon_t,Y^\varepsilon_t)dt+G(t,X^\varepsilon_t,Y^\varepsilon_t)dW^2_t,$$

with $X^\varepsilon_0=x$, $Y^\varepsilon_0=y$ and independent Brownian motions $W^1,W^2$.

Freezing $y$ gives the frozen equation $dX^y_t=b(X^y_t,y)dt+\sigma(X^y_t,y)dW^1_t$ (1.7), with generator $\mathscr L_0(x,y)=\sum_{ij}a^{ij}\partial^2_{x_ix_j}+\sum_ib^i\partial_{x_i}$, $a=\sigma\sigma^*/2$, and invariant probability measure $\mu^y$. A function is centered if its $\mu^y$-average vanishes for every $y$. The standing assumptions are: (Aσ), uniform nondegeneracy of $\sigma\sigma^*$; (Ab), $\lim_{|x|\to\infty}\sup_y\langle x,b(x,y)\rangle=-\infty$; (AG), uniform nondegeneracy of $GG^*$; (AH), $H$ is centered; and (2.7), the analogue of (Ab) for $b+\kappa c$, $\kappa>0$ small.

The averaged coefficients of Regime 1 are $\hat F_1(t,y)=\int F(t,x,y)\mu^y(dx)$ and $\hat G_1=(\int GG^*(t,x,y)\mu^y(dx))^{1/2}$, and the averaged equation (2.9) is $d\hat Y^1_t=\hat F_1(t,\hat Y^1_t)dt+\hat G_1(t,\hat Y^1_t)dW^2_t$, $\hat Y^1_0=y$.

Regularity is measured in weighted Hölder classes: $C^{\delta,\vartheta}_p$ (index $\delta$ in $x$, $\vartheta$ in $y$, polynomial growth in $x$), its bounded version $C^{\delta,\vartheta}_b$, the time-dependent $C^{\vartheta/2,\delta,\vartheta}_p$, the class $L^\infty_p$ of measurable functions of polynomial growth, and $C^{2+\vartheta}_b(\mathbb R^{d_2})$ for test functions.

Formalization targets

Goal: Theorem 2.3(i)

In Regime 1, $\alpha_\varepsilon/\gamma_\varepsilon\to0$ and $\alpha_\varepsilon^2/(\beta_\varepsilon\gamma_\varepsilon)\to0$, assume $b,\sigma\in C^{\delta,\vartheta}_b$, $F,H,G\in C^{\vartheta/2,\delta,\vartheta}_p$ with $\vartheta\in(0,2]$, $c\in L^\infty_p$ and $\alpha_\varepsilon^\vartheta/\gamma_\varepsilon\to0$. Then for every $T>0$ and $\varphi\in C^{2+\vartheta}_b$,

$$\sup_{t\in[0,T]}\big|\mathbb E\varphi(Y^\varepsilon_t)-\mathbb E\varphi(\hat Y^1_t)\big|\le C_T\Big(\frac{\alpha_\varepsilon^\vartheta}{\gamma_\varepsilon}+\frac{\alpha_\varepsilon^2}{\gamma_\varepsilon^2}+\frac{\alpha_\varepsilon^2}{\beta_\varepsilon\gamma_\varepsilon}\Big).$$

Milestones

1. Lemma 4.1: mollification in $(t,y)$ at scales $n^{-2}$ and $n^{-1}$ costs $n^{-\vartheta}$ and gains $n^{2-\vartheta}$ on $\partial_t$ and $\nabla_y^2$.
2. Lemma 4.2: for centered $f$, $\mathbb E\int_0^tf(s,X^\varepsilon_s,Y^\varepsilon_s)ds\le C_t(\alpha_\varepsilon^\vartheta+\alpha_\varepsilon^{\vartheta\wedge1}\alpha_\varepsilon/\gamma_\varepsilon+\alpha_\varepsilon^2/\beta_\varepsilon)$.
3. Lemma 4.4(i): in Regime 1, $\mathbb E\,\gamma_\varepsilon^{-1}\int_0^tf\,ds\le C_t(\alpha_\varepsilon^\vartheta/\gamma_\varepsilon+\alpha_\varepsilon^2/\gamma_\varepsilon^2+\alpha_\varepsilon^2/(\beta_\varepsilon\gamma_\varepsilon))$.
4. Lemma 5.1 ($k=1$): $\hat{\mathcal G}_1=\hat G_1\hat G_1^*/2$ is uniformly nondegenerate and $\hat F_1,\hat{\mathcal G}_1\in C^{\vartheta/2,\vartheta}_b$.

Significance

The result. The theorem gives a rate for the weak error of the averaging principle under Hölder regularity only, and the rate depends only on the regularity in the slow variable $y$, not on $\delta$. It covers the fully coupled case, in which the slow equation contains the singular drift $\gamma_\varepsilon^{-1}H$, and it identifies the extra condition $\alpha_\varepsilon^\vartheta/\gamma_\varepsilon\to0$ under which this drift averages out. For $c=H\equiv0$ it reduces to the rate $\alpha_\varepsilon^\vartheta$ (Remark 2.5), optimal for $\vartheta=2$. Error bounds of this kind are what heterogeneous multiscale methods need to be quantitative.

Formalizing it. The result is proved in the paper; nothing in it is machine-checked. A formalization needs an Itô calculus for weak solutions, the elliptic Poisson equation in $x$ with parameter $y$ (the companion mission's Theorem 2.1), and the parabolic Kolmogorov equation of the averaged SDE. The two fluctuation lemmas are stated for general centered functions and are reusable for other limit theorems.

Difficulty

The obvious argument writes $\mathbb E\varphi(Y^\varepsilon_T)-\mathbb E\varphi(\hat Y^1_T)$ through the Kolmogorov equation of the averaged SDE and Itô's formula, which leaves $\mathbb E\int_0^T(\mathscr L_1-\hat{\mathscr L}_1)\tilde u\,ds$ and $\gamma_\varepsilon^{-1}\mathbb E\int_0^TH\cdot\nabla_y\tilde u\,ds$. Both integrands are centered but only Hölder continuous in $(t,y)$, so the standard corrector argument, which applies Itô's formula to the solution of the Poisson equation along $(X^\varepsilon,Y^\varepsilon)$, needs derivatives in $t$ and $y$ that do not exist. The term with $\gamma_\varepsilon^{-1}$ is a central-limit-scale fluctuation, which is why its control needs the regime conditions. Existence and regularity of the averaged coefficients also have to come from the Poisson equation, since $\mu^y$ is not explicit.

Formalization scope

Spaces are EuclideanSpace ℝ (Fin d). Coefficients are $b,c:\mathbb R^{d_1}\times\mathbb R^{d_2}\to\mathbb R^{d_1}$, $\sigma$ a $d_1\times d_1$ matrix, $F,H:\mathbb R_+\times\mathbb R^{d_1}\times\mathbb R^{d_2}\to\mathbb R^{d_2}$, $G$ a $d_2\times d_2$ matrix. The Itô layer (Brownian motion, Itô integral, Itô processes, SDE solutions) is the published Peng1990.SMP.Stochastic. A solution of (1.4) is a weak solution: any filtered probability space, any Brownian motion for that filtration, any progressive process satisfying the integral equation. The theorem compares every weak solution of (1.4) with every weak solution of (2.9). The paper does not prove existence for (1.4), so the statement is conditional on solutions, as it is used in the paper. A sanity file shows the parameter hypotheses are consistent ($\alpha_\varepsilon=\varepsilon$, $\beta_\varepsilon=\gamma_\varepsilon=\varepsilon^{1/2}$) and that (2.7) holds for a bounded dissipative drift.

Committed conventions and readings of the page:

• $\mu^y$ is any family of probability measures that are infinitesimally invariant for $\mathscr L_0$ with $a=\sigma\sigma^*/2$, the generator of (1.7). Under the standing assumptions this is the unique invariant measure.
• (2.7) is read with $\kappa=\alpha_\varepsilon^2/\beta_\varepsilon$, the factor that actually multiplies $c$ in the fast drift, for all small $\kappa>0$.
• $\hat G_1$ is any measurable matrix field with $\hat G_1\hat G_1^*=\int GG^*\,d\mu^y$, which covers the printed square root.
• The Hölder classes include polynomial growth, constrain all lower $y$-derivatives, and take their constants uniformly in time, including in the time-Hölder clause.
• The constants $C_T$, $C_t$, $C_0$ exist after all data are fixed (coefficients, $\mu$, $T$, $\varphi$, $x$, $y$, the parameter functions) and before $\varepsilon$ or $n$.
• Lemma 4.1 takes $f$ on all of $\mathbb R$ in time, since (4.1) evaluates $f$ at negative times, and assumes the kernels have the finite moments $\int|r|^{\vartheta/2}\rho_1<\infty$, $\int|z|^\vartheta\rho_2<\infty$ that its proof uses; without them (4.2) fails for a Cauchy-type kernel.
• Solutions are Itô processes in the sense of the referenced layer: progressive, with $\sup_{t\le T}\mathbb E|Z_t|^2<\infty$ and square-integrable diffusion integrands.
• Lemma 4.4(i) carries the Regime 1 limits of its label.
• Lemmas 4.2 and 4.4(i) are one-sided, as printed, and include integrability of the path integral in their conclusion.

A formalization in which the expectations are junk Bochner integrals, the constant depends on $\varepsilon$, or a single strong solution is fixed would be a different and weaker statement; the posed statements rule these out.

Not posed: Regimes 2–4 of Theorem 2.3 and Lemma 4.4(ii)–(iv). The printed $\hat G_3=\hat G_4$ differs by a factor $2$ in the $H\Phi^*$ term from the generator used in the proof, so a faithful statement needs a correction that is left to moderation. Regime 2 needs the Poisson solution $\Phi$ in the averaged drift. Lemma 5.2 is also not posed: as printed, $u_k(t,y)=\mathbb E\varphi(\hat Y^k_t(y))$ solves (5.1) only for time-independent coefficients, and its class $C^{(2+\vartheta)/2,2+\vartheta}_b$ has time index above $1$, which the paper's notations do not define. Contributions toward Itô's formula for these processes, the Poisson equation (companion mission 1) and parabolic Schauder theory are welcome.

Selected references

• M. Röckner, L. Xie, Diffusion approximation for fully coupled stochastic differential equations, Ann. Probab. 49(3) (2021) 1205–1236. https://doi.org/10.1214/20-AOP1475
• G. Papanicolaou, D. Stroock, S. R. S. Varadhan, Martingale approach to some limit theorems, Duke Turbulence Conference, Duke Univ. Math. Ser. III (1977).
• E. Pardoux, A. Yu. Veretennikov, On the Poisson equation and diffusion approximation. I, Ann. Probab. 29 (2001) 1061–1085. https://doi.org/10.1214/aop/1015345596
• E. Pardoux, A. Yu. Veretennikov, On Poisson equation and diffusion approximation. II, Ann. Probab. 31 (2003) 1166–1192. https://doi.org/10.1214/aop/1055425774
• E. Pardoux, A. Yu. Veretennikov, On the Poisson equation and diffusion approximation. III, Ann. Probab. 33 (2005) 1111–1133. https://doi.org/10.1214/009117905000000062
• D. Givon, Strong convergence rate for two-time-scale jump-diffusion stochastic differential systems, Multiscale Model. Simul. 6 (2007) 577–594. https://doi.org/10.1137/060673345
• D. Liu, Strong convergence of principle of averaging for multiscale stochastic dynamical systems, Commun. Math. Sci. 8 (2010) 999–1020.
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28 (1990) 966–979 (source of the Itô layer). https://doi.org/10.1137/0328054

Motivation

Poisson equations for the generator of an ergodic diffusion are a standard tool in stochastic averaging, homogenization and diffusion approximation: to show that a fast ergodic component averages out in a slow equation, one writes the fluctuation $f(X_t,Y_t)$ as $\mathscr L_0 u$ and applies Itô's formula to $u$. This requires a solution $u$ whose regularity is controlled in two variables at once: the fast variable $x$, in which the operator is elliptic, and the slow variable $y$, which enters as a parameter.

• Pardoux and Veretennikov (Ann. Probab. 2001, 2003, 2005) studied this equation in the whole space $\mathbb R^{d_1}$ and used it for diffusion approximation of slow–fast SDEs. In parts I and III the operator does not depend on the parameter, and the solution's regularity in $x$ is of Sobolev type; regularity in $y$ was obtained by differentiating the associated semigroup in the parameter (Röckner–Xie, Remark 2.2(iii) and p. 1213).
• Röckner and Xie (2021) prove optimal Hölder regularity in $x$ and show that regularity in $y$ follows from it, for fully coupled coefficients that depend on both variables and are only Hölder continuous. This mission formalizes that result (their Theorem 2.1) and the steps of its proof.

Setting

Fix $d_1,d_2\ge1$, a matrix field $a(x,y)=(a^{ij}(x,y))$ and a vector field $b(x,y)\in\mathbb R^{d_1}$ on $\mathbb R^{d_1}\times\mathbb R^{d_2}$. The frozen operator acts on functions of $x$ with $y$ held fixed:

$$\mathscr L_0(x,y)=\sum_{i,j=1}^{d_1}a^{ij}(x,y)\frac{\partial^2}{\partial x_i\partial x_j}+\sum_{i=1}^{d_1}b^i(x,y)\frac{\partial}{\partial x_i}.$$

The Poisson equation (1.1) is $\mathscr L_0(x,y)u(x,y)=f(x,y)$ for all $x\in\mathbb R^{d_1}$, for each parameter $y\in\mathbb R^{d_2}$.

The standing assumptions are:

• (Aσ): $a=\sigma\sigma^*$ is uniformly nondegenerate, i.e. $\lambda^{-1}|\xi|^2\le|a(x,y)\xi|^2\le\lambda|\xi|^2$ for some $\lambda>1$;
• (Ab): $\lim_{|x|\to\infty}\sup_y\langle x,b(x,y)\rangle=-\infty$, a weak recurrence condition.

Under these, for each $y$ the frozen diffusion $dX_t=b(X_t,y)\,dt+\sigma(X_t,y)\,dW_t$ has a unique invariant measure $\mu^y$. Since constants solve $\mathscr L_0u=0$, the equation is only solvable for centered right-hand sides, $\int f(x,y)\,\mu^y(dx)=0$ for every $y$ (1.3), and the solution is fixed by requiring it to be centered as well.

Regularity is measured in weighted Hölder classes. $f\in C^{\delta,0}_p$ ($0<\delta\le1$) means $|f(x,y)|\le C(1+|x|^m)$ and $|f(x_1,y)-f(x_2,y)|\le C(|x_1-x_2|^\delta\wedge1)(1+|x_1|^m+|x_2|^m)$, uniformly in $y$. $C^{\delta,\eta}_p$ adds $\eta$ derivatives in $y$, with a $(\eta-[\eta])$-Hölder top derivative. The subscript $b$ denotes the bounded version, and $C^{2+\delta,\eta}_p$ asks the same of $\nabla^2_xu$ together with growth bounds on $u$ and $\nabla_xu$.

Formalization targets

Goal: Theorem 2.1

If (Aσ), (Ab) hold and $a,b\in C^{\delta,\eta}_b$ with $0<\delta\le1$, $\eta\ge0$, then for every centered $f\in C^{\delta,\eta}_p$ there is a unique centered $u\in C^{2+\delta,\eta}_p$ with $\mathscr L_0u=f$. For some $C_0,m>0$,

$$|u|+|\nabla_xu|+|\nabla^2_xu|\le C_0(1+|x|^m),\qquad|\nabla^2_xu(x_1,y)-\nabla^2_xu(x_2,y)|\le C_0(|x_1-x_2|^\delta\wedge1)(1+|x_1|^m+|x_2|^m),$$

and, for $\eta>0$, $\|u(x,\cdot)\|_{C^\eta_b}\le C_0(1+|x|^m)$.

Milestones, in the order of the proof

1. The transfer formula for $\eta=1$ (Remark 3.3(ii), Lemma 3.2(i)): if $u\in C^{2+\delta,0}_p$ solves $\mathscr L_0u=h-\bar h$, then

$$\partial_y\int h(x,y)\,\mu^y(dx)=\int\Big[\partial_yh-\frac{\partial\mathscr L_0}{\partial y}u\Big](x,y)\,\mu^y(dx).$$

2. The increment formula (3.10) for $\eta\in(0,1)$ (Lemma 3.2(ii)), with $\bar h\in C^\eta_b$.
3. Theorem 2.1 for $\eta=0$: existence, uniqueness and the $x$-estimates (2.1)–(2.2).
4. Step 3: the right-hand side $\partial_yf-\partial_y\mathscr L_0\,u$ of the differentiated equation is centered.
5. Step 3: for $\eta=1$ the solution satisfies $\partial_yu\in C^{2+\delta,0}_p$ and $|\partial_yu|\le C(1+|x|^m)$.
6. Step 4: for $\eta\in(0,1)$, $|u(x,y_1)-u(x,y_2)|\le C(|y_1-y_2|^\eta\wedge1)(1+|x|^m)$.

Significance

The theorem supplies the corrector used in Theorem 2.3 of the same paper, the weak convergence rate of the slow component of a fully coupled multiscale SDE to its averaged limit. Its form, regularity in $y$ matching that of the data and no derivative of $\mu^y$ in $y$, is what lets the rates depend only on the regularity of the coefficients in the slow variable. The transfer formulas (3.9)–(3.10) also show that averaged coefficients $\bar h(y)=\int h\,d\mu^y$ inherit the $y$-regularity of $h$, a question that comes up in every averaging or homogenization limit.

The result is proved in the paper. None of it is formalized: Lean and Mathlib have no fundamental solutions of non-divergence elliptic operators, no Schauder theory and no invariant measures of diffusions. The mission poses the statements, so that the proof can be built in layers and the parts that do not depend on the Gaussian kernel bounds (the transfer formulas given a solution, the induction in Steps 3–4) can be proved separately.

Difficulty

Existence and the estimates (2.1)–(2.2) rest on the probabilistic representation $u=\int_0^\infty T_tf\,dt$ and on Gaussian bounds and ergodic decay for the fundamental solution $p_t(x,x';y)$ of $\mathscr L_0(\cdot,y)$ (Lemma 3.1, cited from Ladyzhenskaya–Solonnikov–Ural'tseva and Pardoux–Veretennikov II, Proposition 3). The coefficients are only Hölder in $x$, so the Hessian bound needs the cancellation $\int\nabla^2_xp_t\,dx'$ (3.3), not just a size estimate on $\nabla^2_xp_t$. The obvious approach to $y$-regularity, differentiating $T_tf$ or $\mu^y$ in $y$, needs derivatives of the invariant density in the parameter, which are hard to control. The paper's route, differentiating the equation and using the transfer formula to recenter, only works if the differentiated right-hand side is again centered. That centering is the content of Lemma 3.2.

Formalization scope

• $\mathbb R^d$ is EuclideanSpace ℝ (Fin d); $\nabla_x$, $\nabla^2_x$ are fderiv and iteratedFDeriv ℝ 2 in $x$, $\partial^j_y$ is iteratedFDeriv ℝ j in $y$, with operator norms. $y$-derivatives in the milestones are directional.
• (Aσ) includes symmetric positive semidefiniteness of $a$ (the content of $a=\sigma\sigma^*$). (Ab) is the $\forall M\,\exists R$ form.
• $\mu^y$ is a hypothesis: a family of probability measures, each infinitesimally invariant for $\mathscr L_0(\cdot,y)$ ($\int\mathscr L_0g\,d\mu^y=0$ for smooth compactly supported $g$). Under the assumptions this is the unique invariant measure of the frozen SDE (1.7); the SDE itself is not formalized. No moment bounds on $\mu^y$ are assumed, since they are consequences.
• Centering includes $\mu^y$-integrability, and every integral formula in a conclusion asserts integrability of its integrand, so no statement can hold through a junk zero integral.
• The classes include the polynomial growth bound and all lower $y$-derivatives; matrix coefficients are in $C^{\delta,\eta}_b$ entrywise; $\eta\ge0$ is real, split as $[\eta]+$ fractional part; a $y$-derivative is read as continuous ($C^k$ in $y$). The $C^\eta_b$ norm is in max form.
• Not posed: the clause that $C_0,m$ depend "only on $d_1,d_2$, $\|a\|_{C^{\delta,0}_b}$, $\|b\|_{C^{\delta,0}_b}$, $[f]_{C^{\delta,0}_p}$", which is false as printed ($[f]_{C^{\delta,0}_p}$ is a supremum over the unit ball, and $\lambda$ and the rate in (Ab) are missing), and the recursive constant $\mathcal K_\eta$ of (2.4)–(2.5). The constants exist for each fixed $(a,b,f)$. (2.1)–(2.2), printed under "Case η = 0", are asserted for every $\eta$.
• Uniqueness is stated for the whole class $C^{2+\delta,\eta}_p$, not only among solutions that satisfy the estimates. Without the invariance of $\mu^y$ for the same $a,b$, or without centering, the statement would be false; both are part of the hypotheses.
• Useful contributions beyond this mission: Hölder spaces with polynomial weights, fundamental solutions of non-divergence-form operators, invariant measures of elliptic diffusions, and the identification of infinitesimally invariant measures with invariant measures of the diffusion.

Selected references

• M. Röckner, L. Xie, Diffusion approximation for fully coupled stochastic differential equations, Ann. Probab. 49(3), 1205–1236, 2021. https://doi.org/10.1214/20-AOP1475
• E. Pardoux, A. Yu. Veretennikov, On the Poisson equation and diffusion approximation. I, Ann. Probab. 29(3), 1061–1085, 2001. https://doi.org/10.1214/aop/1015345596
• E. Pardoux, A. Yu. Veretennikov, On Poisson equation and diffusion approximation. II, Ann. Probab. 31(3), 1166–1192, 2003. https://doi.org/10.1214/aop/1055425774
• E. Pardoux, A. Yu. Veretennikov, On the Poisson equation and diffusion approximation 3, Ann. Probab. 33(3), 1111–1133, 2005. https://doi.org/10.1214/009117905000000062
• O. A. Ladyzhenskaya, V. A. Solonnikov, N. N. Ural'tseva, Linear and Quasi-linear Equations of Parabolic Type, AMS Translations of Mathematical Monographs 23, 1968. https://mathscinet.ams.org/mathscinet-getitem?mr=0241822

Motivation

Mean field control asks a central planner to steer a large population of interacting agents. Each agent's state follows a stochastic differential equation whose coefficients depend on the agent's own state and on the empirical distribution of the population; as the population grows, the system is described by a single McKean–Vlasov equation whose coefficients depend on the law of the solution itself. The planner's value is then a function $V(t,\mu)$ of time and of a probability measure, and its dynamic programming equation, the HJB master equation, is a partial differential equation on the Wasserstein space of measures.

C. Wu and J. Zhang (Ann. Appl. Probab. 30(2), 2020) develop a viscosity theory for such master equations in a path-dependent setting and apply it to McKean–Vlasov control with closed-loop controls, i.e. controls that depend on the observed state path rather than on the driving Brownian motion. Closed-loop information is the natural one when the noise is not observable, and it is the information structure relevant for games; but the value function is then not known to be smooth, so classical solutions are out of reach. This mission formalizes the paper's §5: the value function of the closed-loop problem with piecewise constant controls is a viscosity solution of the HJB master equation.

Setting

Fix $d\ge1$ and a horizon $T$. The path space is $\Omega=C([0,T],\mathbb R^d)$ with the uniform norm, the canonical process is $X_s(\omega)=\omega_s$, and $\mathbb F=(\mathcal F_t)$ is its natural filtration. $\mathcal P_2$ is the set of probability measures $\mu$ on $\Omega$ with $\mathbb E^\mu[\|X\|^2]<\infty$; $\mu_{[0,t]}$ is the law of the stopped path $X_{t\wedge\cdot}$. On $\Theta=[0,T]\times\mathcal P_2$ the pseudometric is

$$\mathcal W_2\big((t,\mu),(t',\mu')\big)=\big(|t-t'|+\mathcal W_2^2(\mu_{[0,t]},\mu'_{[0,t']})\big)^{1/2},$$

with $\mathcal W_2$ the 2-Wasserstein distance on laws of paths.

The data are a control set $A$ and coefficients $b(t,\omega,\mu,a)\in\mathbb R^d$, $\sigma(t,\omega,\mu,a)\in\mathbb R^{d\times d}$, $f(t,\omega,\mu,a)\in\mathbb R$, $g(\omega,\mu)\in\mathbb R$ satisfying Assumption 5.1: measurability and adaptedness, boundedness of $b,\sigma$ by $C_0$, Lipschitz continuity of $b,\sigma$ and uniform continuity of $f,g$ in $(\omega,\mu)$, local uniform continuity in $t$, and positive definiteness of $\sigma\sigma^\top$.

An admissible control $\alpha\in\mathcal A_t$ (5.3) is piecewise constant: $\alpha_s=\sum_{i<n}h_i\mathbf 1_{[t_i,t_{i+1})}(s)$ for a partition $t=t_0<\dots<t_n=T$, with $h_i:\Omega\to A$ $\mathcal F_{t_i}$-measurable. The controlled law $\mathbb P^{t,\mu,\alpha}\in\mathcal P_2$ agrees with $\mu$ on $[0,t]$ and solves, for a Brownian motion $B^\alpha$,

$$X_s=X_t+\int_t^s b\big(r,X_{r\wedge\cdot},\mathbb P^{t,\mu,\alpha}_{[0,r]},\alpha_r\big)dr+\int_t^s\sigma\big(r,X_{r\wedge\cdot},\mathbb P^{t,\mu,\alpha}_{[0,r]},\alpha_r\big)dB^\alpha_r,\quad s\in[t,T].$$

The value function (3.20) is

$$V(t,\mu)=\sup_{\alpha\in\mathcal A_t}\mathbb E^{\mathbb P^{t,\mu,\alpha}}\Big[g(X,\mathbb P^{t,\mu,\alpha})+\int_t^Tf(s,X,\mathbb P^{t,\mu,\alpha},\alpha_s)\,ds\Big],$$

and $V_0$ is the same supremum over the controls $\mathcal A^0_t$ (5.12) whose pieces depend on the path before $t$ only through finitely many values $X_{s_1},\dots,X_{s_m}$.

The HJB master equation (3.22) is $\mathbb LV=0$ with $\mathbb LV(t,\mu)=\partial_tV(t,\mu)+G(t,\mu,\partial_\mu V(t,\mu,\cdot),\partial_\omega\partial_\mu V(t,\mu,\cdot))$, where

$$G(t,\mu,Z,\Gamma)=\mathbb E^\mu\Big[\sup_{a\in A}\Big(\tfrac12\Gamma(X):\sigma\sigma^\top(t,X,\mu,a)+Z(X)\cdot b(t,X,\mu,a)+f(t,X,\mu,a)\Big)\Big].$$

Viscosity solutions (Definition 4.4) are defined by test functions $\varphi$ that satisfy a functional Itô formula on $[t,t+\delta]\times\mathcal P_L(t,\mu)$, where $\mathcal P_L(t,\mu)$ is the set of laws agreeing with $\mu$ on $[0,t]$ under which $X$ is a semimartingale on $[t,T]$ with drift and diffusion bounded by $L$, and touch $V$ from above or below at $(t,\mu)$ on that set.

Formalization targets

Goal: Theorem 5.8

Under Assumption 5.1, $V$ is finite on $\Theta$ and is a viscosity solution of (3.22).

Milestones

• $(4.1)$: $\sup_{\mathbb P\in\mathcal P_L(t,\mu)}\mathbb E^{\mathbb P}[\sup_{t\le s\le t+\delta}|X_{t,s}|^p]\le C_{p,L}\delta^{p/2}$.
• Remark 5.4(i): (3.18) has a unique solution, and it lies in $\mathcal P_L(t,\mu)$ for $L\ge C_0\vee\frac12C_0^2$.
• Remark 5.4(ii): the dynamic programming principle (3.21),

$$V(t_1,\mu)=\sup_{\alpha\in\mathcal A_{t_1}}\Big[V(t_2,\mathbb P^{t_1,\mu,\alpha})+\int_{t_1}^{t_2}\mathbb E^{\mathbb P^{t_1,\mu,\alpha}}[f(s,X,\mathbb P^{t_1,\mu,\alpha},\alpha_s)]ds\Big].$$

• Lemma 5.11: a coupling construction with an independent Brownian motion.
• Lemma 5.13: $|V_0(t,\mu)-V_0(t,\nu)|\le\rho(\mathcal W_2(\mu_{[0,t]},\nu_{[0,t]}))$ for a modulus $\rho$.
• Lemma 5.14: $V=V_0$.
• Theorem 5.7: $|V(t_1,\mu)-V(t_2,\nu)|\le C\rho(\mathcal W_2((t_1,\mu),(t_2,\nu)))+C[1+\mathcal W_2(\mu_{[0,t_1]},\delta_{\{0\}})][t_2-t_1]$, and uniform continuity when $f$ is bounded.

Significance

The result characterizes the closed-loop value function through a PDE on the space of path laws without assuming any smoothness of $V$. Combined with a comparison principle for (3.22), which the paper leaves open, it would identify the closed-loop and open-loop values (Remark 5.9). The regularity result (Theorem 5.7) is itself delicate: Example 5.6 shows that a natural restricted class of closed-loop controls produces a value function that is discontinuous in $\mu$, and the piecewise constant class (5.3) is chosen to avoid this.

The theorems are proved in the paper; none of them is formalized. A formalization would supply a machine-checked path from a path-dependent McKean–Vlasov control problem to its HJB master equation, together with reusable statements on weak solutions of path-dependent McKean–Vlasov equations, their uniform moment bounds, and the dynamic programming principle in the Wasserstein space.

Difficulty

Definition 4.4 requires $V\in C^0(\Theta)$, and the central difficulty is continuity in $\mu$. Closed-loop controls are functions of the observed path; changing the initial law from $\mu$ to $\nu$ changes the information available to the control, and when $\nu_{[0,t]}$ is degenerate a control adapted to $\mu$ cannot be written as a function of the $\nu$-path. The obvious argument, transporting an $\varepsilon$-optimal control for $\mu$ along an optimal coupling of $\mu$ and $\nu$, fails for exactly this reason (Example 5.6).

Formalization scope

Time is $\mathbb R_{\ge0}$ and every statement quantifies over $t\le T$ and $\mu\in\mathcal P_2$. Paths are continuous maps $[0,T]\to\mathbb R^d$ with the sup norm and Borel $\sigma$-algebra; $\mathcal W_2$ is the published WassersteinDRO.Duality.wassersteinDistance with $p=2$. Brownian motion and Itô integrals are the published EthierKurtz.IsStandardBrownian and EthierKurtz.HasBrownianItoIntegral.

Committed conventions:

• The control set $A$ is a nonempty Polish space with its Borel $\sigma$-algebra (the paper says "some appropriate set $A$"); this provides continuity in $a$, measurability of $h_i$ and of $\omega\mapsto\sup_aG_2$.
• "Progressively measurable in all variables" is joint measurability (Giry $\sigma$-algebra on laws) plus adaptedness in $\omega$ and $\mu$. The bound $|\sigma|\le C_0$ uses the Frobenius norm; the joint Lipschitz bound on $(b,\sigma)$ is two bounds with the same $L_0$. $\delta_{\{0\}}$ is the Dirac mass at the zero path.
• (3.18) is solved in the weak sense: a law with a semimartingale representation, carrying its own Brownian motion, whose characteristics are the controlled coefficients on $[t,T)$. $\mathcal P_L(t,\mu)$ is defined through the same representations.
• $V$ and $V_0$ are suprema in the extended reals over admissible pairs; statements that subtract values or use $V$ as a real function assert finiteness explicitly.
• Test functions carry their derivatives as witnesses; the Itô formula of Definition 4.2 is stated in drift form for every representation; "$\inf(\varphi-V)=0$" is read as $\varphi-V\ge0$ on the test set with equality at $(t,\mu)$, and the test function's data at $(t,\mu)$ are those at $(t,\mathbb P)$ for $\mathbb P\in\mathcal P_L(t,\mu)$.
• Statements are for general $d$; §5.3 of the paper argues for $d=1$ only.

The test classes are not vacuous: constant functions satisfy every clause of the test-function class, and Assumption 5.1 holds for $b\equiv0$, $\sigma\equiv I$, $f\equiv g\equiv0$. A formalization that makes $\mathcal P_L(t,\mu)$ or the admissible set empty, or that lets $V$ be $-\infty$, does not prove the theorem.

Needed infrastructure: weak existence and uniqueness for path-dependent McKean–Vlasov SDEs with Lipschitz coefficients; Burkholder–Davis–Gundy-type moment bounds; measurable selection on Polish spaces; couplings and gluing on $\mathcal P_2$ of a path space. The moment bound and the McKean–Vlasov well-posedness are reusable beyond this mission. Contributions to any milestone are welcome.

Selected references

• C. Wu, J. Zhang, Viscosity solutions to parabolic master equations and McKean–Vlasov SDEs with closed-loop controls, Ann. Appl. Probab. 30(2), 936–986, 2020. https://doi.org/10.1214/19-AAP1521
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications I, Springer, 2018. https://doi.org/10.1007/978-3-319-58920-6
• D. Lacker, Limit theory for controlled McKean–Vlasov dynamics, SIAM J. Control Optim. 55(3), 2017. https://doi.org/10.1137/16M1095895
• I. Ekren, N. Touzi, J. Zhang, Viscosity solutions of fully nonlinear parabolic path dependent PDEs: Part I, Ann. Probab. 44(2), 2016. https://doi.org/10.1214/14-AOP999