Stochastic Systems

Why common noise changes the control problem

A controller may act on a large population of interacting particles while all particles also experience a shared random disturbance. In the population limit, the state of a representative particle depends on the distribution of states conditional on the common noise. The controller therefore influences both its own state and the conditional population law. The usual state variable for dynamic programming must carry that law, and a future decision may use only information available from common noise. Djete, Possamaï and Tan establish a dynamic programming principle for this setting in McKean–Vlasov optimal control: the dynamic programming principle, Theorem 3.2. Their result permits path dependent coefficients and merely Borel reward functions, so ordinary continuity arguments do not determine the value function's measurability.

The paper distinguishes a weak formulation, in which the stochastic basis varies with the control, from a strong formulation on a fixed space. This mission concerns the latter, restricted to controls predictable from common noise, under the paper's Lipschitz and growth Assumption 2.8. The companion mission treats the weak dynamic programming principle, Theorem 3.1. The present mission asks for a machine checked account of the strong formulation and of the transfer between its intrinsic, fixed space and canonical descriptions.

State, noise and admissible controls

Fix a horizon $T>0$. A state trajectory belongs to $\mathcal C^n=C([0,T],\mathbb R^n)$. The two driving noises are a $d$ dimensional idiosyncratic Brownian motion $W$ and an $\ell$ dimensional common Brownian motion $B$. The control space $U$ is nonempty and Polish. At time $s$, the controlled drift $b$ and diffusions $\sigma,\sigma_0$ may depend on the stopped state path $X_{s\wedge\cdot}$, the control $\alpha_s$, and the conditional law $\bar\mu_s$ of the stopped state and control given common noise. The running and terminal rewards are $L$ and $g$.

A $\mathbb B$ strong control has a continuous state satisfying the controlled stochastic equation, the conditional laws required by the paper, finite quadratic control energy, and an $\alpha$ predictable for the common noise filtration. Its reward $J(t,\gamma)$ is the expected running reward from $t$ to $T$ plus the terminal reward. The value $V_S^{\mathbb B}(t,\nu)$ is the supremum of these rewards over such controls from initial path law $\nu$. The initial law lies in $\mathcal P_2(\mathcal C^n)$, the laws with a finite second moment. The coefficient hypothesis uses the quadratic Wasserstein distance $W_2$ and one constant $C>0$ for both a Lipschitz bound and a quadratic growth bound. These conditions are Assumption 2.8 of the source paper, p. 8.

The paper also fixes a canonical probability space $\Omega^t$ carrying an initial path and Brownian increments after $t$. Its common noise predictable controls form $\mathcal A_2^{\mathbb B}(t,\nu)$. Proposition 2.10 says this fixed space computes the same value as the intrinsic strong formulation. The precise probability law on $\Omega^t$ is characterized by the initial stopped path law and independent standard Brownian increments; the paper does not choose a unique construction.

Formalization targets

The goal is Theorem 3.2, p. 10. It first asserts that the value on $[0,T]\times\mathcal P_2(\mathcal C^n)$ is upper semi analytic: each strict superlevel set $\{(t,\nu):V_S^{\mathbb B}(t,\nu)>c\}$ is analytic. For an initial pair $(t,\nu)$ and a stopping time $\tau\in[t,T]$ for the raw common noise filtration on $\Omega^t$, it then asserts

$$V_S^{\mathbb B}(t,\nu)=\sup_{\alpha\in\mathcal A_2^{\mathbb B}(t,\nu)} \mathbb E\!\left[\int_t^\tau L(s,X^\alpha_{s\wedge\cdot},\bar\mu_s^\alpha,\alpha_s)\,ds +V_S^{\mathbb B}(\tau,\mu_\tau^\alpha)\right].$$

Here $\mu_\tau^\alpha$ is the law of the stopped state conditional on information from common noise at $\tau$. The milestone sequence follows the paper's supporting results: strong solution existence and uniqueness (Theorem A.3(i)); equivalence of intrinsic and fixed space values (Proposition 2.10); induction of canonical rules from strong controls (the forward clause of Lemma 4.4(ii)); the canonical value identity (Corollary 4.6); the Wiener represented rule class and its value (Lemma 4.11); analytic rule graphs and value measurability (Lemma 4.12); and stability of a strong rule under conditioning at a stopping time (Lemma 4.13(i)). Each is a source indexed target, rather than an invented intermediate assertion.

What the result provides

The identity permits the value after a random common noise stopping time to be evaluated from the stopped conditional state law. This is the form needed to compare control decisions before and after a random observation time. Upper semi analyticity supplies measurable superlevel sets for the value even when $L$ and $g$ lack continuity. The paper proves these statements mathematically; the mission seeks their Lean formalization, not a new theorem about the underlying control problem.

A complete formalization would also provide reusable definitions of conditional measure valued flows, Brownian motion relative to a filtration over a shifted interval, a local Itô equation, and canonical martingale control rules. The two published Ethier–Kurtz definitions supply the local Itô relation and probability augmentation of a filtration. They are shared infrastructure rather than new statements of this paper.

Where the difficulty lies

The state law in the coefficients is conditional on common noise and changes with the control. A pathwise solution of the state equation must therefore remain consistent with its own conditional law. A naive argument that restarts an ordinary diffusion at $\tau$ does not establish that consistency for a restarted control. It also does not ensure that a restarted control remains predictable from common noise. The paper's canonical rule formulation and its conditioning and measurability results address those obstructions. The reward may be unbounded and extended real valued, so the expectation convention and its behavior at infinite positive and negative parts matter to the statement itself.

Formalization scope and conventions

Paths are continuous maps on compact real intervals with uniform norm; $\mathbb R^k$ is Mathlib's Euclidean space, including $k=0$. Probability measures carry weak convergence topology, and $\mathcal P_2$ is its finite second moment subtype. The product of path space and $U$ uses Mathlib's product metric; matrix norms are Frobenius. Supremums range over admissible controls, solutions and conditional law versions. They are EReal valued, so the empty supremum is $-\infty$. The signed expectation is positive part minus negative part with $\infty-\infty=-\infty$, as in the paper. The model fixes a Borel embedding of $U$ into $[0,1]$ and a cemetery control for invalid reconstructed paths.

The Lean statements pin the paper's implicit “well defined” stochastic integral to a pathwise square integrable local Itô relation and almost surely integrable drift. A conditional law equality stated for $d\mathbb P\otimes ds$ almost every pair is expressed in Fubini form. The localized processes printed in Definition 4.1 define its local martingale requirement. The terminal law and the stopped law in the target are quantified as versions of their stated conditional distributions. The fixed canonical law is any law satisfying the paper's initial distribution and Brownian conditions; the target is stated for every such family. These conventions rule out free conditional laws, arbitrary future stopping times, and a value that is $-\infty$ solely because a formalization made the control class empty. A full development must establish nonemptiness and version independence as part of the cited supporting theory.

The scope ends with Theorem 3.2 and the listed milestones. Lemma 4.13(ii), the more involved measurable selection and concatenation result, remains a future contribution. Theorem 3.4 uses a separate companion result; the Markovian corollaries and the heuristic Hamilton–Jacobi discussion of §3.3 are outside this mission.

Selected references

• M. F. Djete, D. Possamaï and X. Tan, McKean–Vlasov optimal control: the dynamic programming principle, arXiv:1907.08860v2, 2020; published in Annals of Probability 50(2), 2022. Preprint. This mission cites the preprint's page and theorem numbering.

Motivation

Join-the-shortest-queue (JSQ) is the basic load-balancing rule for a system of $n$ parallel single-server queues: every arriving customer joins a queue of minimal length. It is optimal in several senses for homogeneous servers and is the reference policy against which cheaper rules (power-of-$d$ choices, join-the-idle-queue) are measured. In the Halfin–Whitt regime, where the arrival rate is $n\lambda$ with $\lambda = 1-\beta/\sqrt n$ for a fixed $\beta>0$, Eschenfeldt and Gamarnik (arXiv:1502.00999) proved that the suitably centred and scaled numbers of queues of length at least one and at least two converge, on finite time intervals, to a two-dimensional reflected diffusion. Braverman (arXiv:1801.05121) justified the interchange of limits (the stationary distributions of the $n$-server chains converge to the stationary distribution of the diffusion). One ingredient of that result is that the diffusion is exponentially ergodic, so it has a unique stationary distribution that is approached at a geometric rate. This mission formalizes the analytic core of that ingredient: a Foster–Lyapunov drift condition for the diffusion's generator.

Timeline. Eschenfeldt and Gamarnik (2015) proved the process-level diffusion limit, the first analysis of JSQ in this regime. Mukherjee, Borst, van Leeuwaarden and Whiting (J. Appl. Probab. 53, 2016) showed that a class of load-balancing schemes shares the same diffusion limit. Braverman (arXiv 2018, v2 2019; Math. Oper. Res. 45(3), 2020) proved tightness of the scaled stationary distributions and exponential ergodicity of the limit, which together give the interchange of limits.

Setting

The state space is the closed quadrant $\Omega = (-\infty,0]\times[0,\infty)$. For $f:\Omega\to\mathbb R$ write $f_1 = \partial f/\partial x_1$, $f_2 = \partial f/\partial x_2$, $f_{11} = \partial f_1/\partial x_1$. On the boundary $\partial\Omega$ these are one-sided derivatives, and $C^2(\Omega)$ denotes the twice continuously differentiable functions in this sense.

The diffusion limit $Y=(Y_1,Y_2)$ solves

$$Y_1(t)=Y_1(0)+\sqrt2W(t)-\beta t+\int_0^t(-Y_1(s)+Y_2(s))\,ds-U(t),\qquad Y_2(t)=Y_2(0)+U(t)-\int_0^tY_2(s)\,ds,$$

with $W$ a standard Brownian motion and $U$ a nondecreasing regulator that increases only when $Y_1=0$. For $f\in C^2(\Omega)$ with the reflection condition $f_1(0,x_2)=f_2(0,x_2)$, its generator acts by

$$G_Yf(x)=(-x_1+x_2-\beta)f_1(x)-x_2f_2(x)+f_{11}(x),\qquad x\in\Omega .$$

The construction of the Lyapunov function uses an auxiliary integer $n\ge1$ and the fluid operator

$$Lf(x)=\Big(-x_1+x_2-\frac{\beta}{\sqrt n}\Big)f_1(x)-x_2f_2(x),$$

the generator of the deterministic fluid path $v_1'=-v_1+v_2-\beta/\sqrt n$, $v_2'=-v_2$. A smoothed indicator $\phi^{(\ell,u)}$ (a piecewise cubic that rises from $0$ at $\ell$ to $1$ at $u$) and two levels $\beta<\kappa_1<\kappa_2$ define the PDEs

$$Lf^{(1)}(x)=-\phi^{(\kappa_1/\sqrt n,\kappa_2/\sqrt n)}(-x_1),\qquad Lf^{(2)}(x)=-\phi^{(\kappa_1/\sqrt n,\kappa_2/\sqrt n)}(x_2),\qquad x\in\Omega,$$

each with the reflection condition. Their solutions are written explicitly in terms of the fluid hitting times $\tilde\tau^{(\kappa)}$ (through the Lambert W function) and $\tau$, and the curves $\Gamma^{(\kappa)}$ that split $\Omega$ into regions $S_0,\dots,S_3$.

Formalization targets

Goal: Theorem 4

For every $\beta>0$ there exist $c>0$, $d>0$, a compact set $K$ and $V\in C^2(\Omega)$ with $V\ge1$ on $\Omega$, $V(x)\to\infty$ as $|x|\to\infty$ in $\Omega$, and $V_1(0,x_2)=V_2(0,x_2)$, such that

$$G_YV(x)\le -cV(x)+d\,1(x\in K),\qquad x\in\Omega .$$

The constants are unspecified and depend only on $\beta$; the statement involves no $n$.

Milestones

1. (5.6)–(5.7): $\phi^{(\ell,u)}$ has an absolutely continuous derivative with $\phi'(\ell)=\phi'(u)=0$, $|\phi'|\le 4/(u-\ell)$ and $|\phi''|\le12/(u-\ell)^2$.
2. Lemma 10: $\tilde\tau^{(\kappa)}$ extends to $\{x_2=0\}$, vanishes on $\{x_1=-\kappa/\sqrt n\}$, and has explicit one-sided partial derivatives.
3. Lemma 11: the explicit $f^{(1)}$ is nonnegative, lies in $C^2(\Omega)$, and has explicit first partials.
4. Lemma 12: the explicit six-case $f^{(2)}$ is well defined, lies in $C^2(\Omega)$, and has the partials (C.8)–(C.9).
5. Lemma 8: for $\epsilon>0$, $\kappa_1=\beta+\epsilon$, $\kappa_2=\beta+2\epsilon$, both PDEs have $C^2(\Omega)$ solutions with

$$f^{(1)}\le\log2,\quad f^{(2)}\le\log2+\tfrac{\epsilon}{\beta}\ \text{on a box},\qquad |f^{(1)}_1|\le\tfrac{4\sqrt n}{\epsilon}\log2,\ |f^{(1)}_{11}|\le\tfrac{12n}{\epsilon^2}\log2,\ |f^{(2)}_1|\le\tfrac{\sqrt n}{\beta},\ |f^{(2)}_{11}|\le\tfrac{n}{\beta\epsilon}\big(1+4\tfrac{\beta+\epsilon}{\epsilon}\big).$$

Significance

By the criterion of Down, Meyn and Tweedie (Ann. Probab. 23, 1995, Theorem 5.2), a drift inequality of the form (5.2) with compact $K$ and $V\to\infty$ implies that the diffusion is positive Harris recurrent and exponentially ergodic in the $V$-norm (Theorem 3 and Corollary 1 of the paper). Together with tightness of the prelimit stationary distributions (mission 1 of this series), this gives convergence of the stationary distributions of the JSQ chains to that of the diffusion. That justifies approximating steady-state JSQ performance by the diffusion.

The construction itself is reusable. Solving the fluid-model PDE $Lf=-(\text{smoothed indicator})$ and exponentiating the solution is a general route from fluid stability to exponential ergodicity of a diffusion. This mission writes that route out for one reflected diffusion with explicit hitting-time formulas.

Status: the result is proved in the paper; no part of it has a machine-checked proof. Theorem 3 and Corollary 1 are not posed, because they rest on the cited Down–Meyn–Tweedie theory and on the existence of the reflected process, neither of which Mathlib has.

Difficulty

The reflecting boundary rules out the first candidates. The condition $V_1(0,x_2)=V_2(0,x_2)$ excludes exponentials of linear functions such as $e^{a(x_2-x_1)}$ unless $a=0$. The natural candidate from the fluid model, the exponential of the fluid time needed to reach a box, has a discontinuous integrand and is not in $C^2(\Omega)$, so $G_Y$ cannot be applied to it. The milestone functions $f^{(1)}$, $f^{(2)}$ are given piecewise across the curves $\Gamma^{(\kappa_1)}$, $\Gamma^{(\kappa_2)}$ and the lines $x_1=-\kappa_i/\sqrt n$, through implicitly defined hitting times. Three things are hard: $C^2$ regularity across these interfaces, the Lambert W asymptotics as $x_2\downarrow0$, and second-derivative bounds that hold uniformly on the unbounded domain $\Omega$ with the stated dependence on $n$ and $\epsilon$.

Formalization scope

• Points of $\Omega$ are pairs ℝ × ℝ, and $\Omega$ is Set.Iic 0 ×ˢ Set.Ici 0. Partials are fderivWithin ℝ f Ω in the coordinate directions, which are one-sided at boundary points. $C^2(\Omega)$ is ContDiffOn ℝ 2 f Ω.
• $G_Y$ is the generator formula of p. 16, and every statement applies it only to $C^2(\Omega)$ functions with the reflection condition. The process (2.1) and the extended generator are not constructed. $V\in C^2(\Omega)$ is part of the conclusion of Theorem 4, so a $V$ whose derivatives within $\Omega$ are undefined (and default to $0$) cannot satisfy (5.2) vacuously. Dropping $V\ge1$, $V\to\infty$, the compactness of $K$, or $c,d>0$ would make (5.2) trivial, and all four are kept.
• The auxiliary $n$ is an integer $n\ge1$; no relation between $\beta$ and $\sqrt n$ is assumed.
• The Lambert W function (principal branch) is defined locally, since Mathlib has none. $\tau$ takes values in WithTop ℝ, with $\infty$ when no solution exists, and its real value is used only where it is finite. $\nu^*$ (the curve $\Gamma^{(\kappa)}$) is the solution of a nonlinear system whose uniqueness is Lemma 5.
• Two printed misprints are corrected. Lemma 8's "for every $\epsilon>0$" is formalized with $\kappa_1=\beta+\epsilon$, $\kappa_2=\beta+2\epsilon$, the choice its proof makes; read literally, the printed statement is false. In (C.5) of Lemma 10 the identity $\tilde\tau_2=-\tilde\tau_1\tilde\tau$ is formalized as $\tilde\tau_2=\tilde\tau_1\tilde\tau$, which is what implicit differentiation gives.
• Lemmas 5, 6 and 9 (properties of $\Gamma^{(\kappa)}$, $\tau$ and $W$) are milestones of mission 1; here their objects are only definitions. Contributions proving those facts in this namespace, or general lemmas on the Lambert W function, are welcome.

Selected references

• A. Braverman, Steady-State Analysis of the Join-the-Shortest-Queue Model in the Halfin-Whitt Regime, Math. Oper. Res. 45(3), 2020; preprint arXiv:1801.05121v2, 2019. https://arxiv.org/abs/1801.05121, https://doi.org/10.1287/moor.2019.1023
• P. Eschenfeldt, D. Gamarnik, Join the Shortest Queue with Many Servers. The Heavy-Traffic Asymptotics, 2015 (Math. Oper. Res. 43(3), 2018). https://arxiv.org/abs/1502.00999
• D. Down, S. P. Meyn, R. L. Tweedie, Exponential and Uniform Ergodicity of Markov Processes, Ann. Probab. 23, 1671–1691, 1995. https://doi.org/10.1214/aop/1176987798
• D. Mukherjee, S. C. Borst, J. S. H. van Leeuwaarden, P. A. Whiting, Universality of Load Balancing Schemes on the Diffusion Scale, J. Appl. Probab. 53, 1111–1124, 2016. https://projecteuclid.org/euclid.jap/1481132840

Motivation

Mean field control studies the optimal control of a very large population of interacting agents through the limit in which the population is replaced by its distribution. The limit problem is a McKean–Vlasov (MKV) control problem: the dynamics and the cost of a representative agent depend on the law of its own state. Such problems arise in systemic risk, crowd motion, energy management and the planning of large distributed systems; the reference account is Carmona and Delarue, Probabilistic Theory of Mean Field Games with Applications I–II (Springer, 2018).

MKV control problems are rarely solvable in closed form, and grid-based numerical methods suffer from the dimension of the state. A practical alternative is to simulate a finite population on a time grid, parametrize the feedback control by a neural network, and minimize the simulated cost by stochastic gradient descent. Carmona and Laurière, Convergence analysis of machine learning algorithms for the numerical solution of mean field control and games: II — the finite horizon case (Ann. Appl. Probab. 32(6), 2022, doi:10.1214/21-AAP1715), quantify how close this computable proxy is to the true optimum. This mission formalizes the statement of their main result and of the propositions and lemmas its proof is built from.

Setting

Fix a horizon $T>0$, a state dimension $d$, a control dimension $k$ (controls take values in $A=\mathbb R^k$), an initial law $\mu_0$ on $\mathbb R^d$, a drift $b(t,x,\mu,\alpha)$, a volatility $\sigma(t,x,\mu)$ (not controlled), a running cost $f(t,x,\mu,\alpha)$ and a terminal cost $g(x,\mu)$; $\mu$ ranges over $\mathcal P_2(\mathbb R^d)$, the probability measures with finite second moment, compared with the Wasserstein distance $W_2$.

Problem 1 (the MKV problem). On a probability space carrying a $d$-dimensional Wiener process $W$ and an independent $X_0\sim\mu_0$, minimize over progressively measurable square-integrable controls $\alpha\in\mathbb A$

$$J(\alpha)=\mathbb E\Big[\int_0^Tf(t,X_t,\mathcal L(X_t),\alpha_t)\,dt+g(X_T,\mathcal L(X_T))\Big],\qquad dX_t=b(t,X_t,\mathcal L(X_t),\alpha_t)\,dt+\sigma(t,X_t,\mathcal L(X_t))\,dW_t,$$

where $\mathcal L(X_t)$ is the law of $X_t$.

Problem 3 (the $N$-agent problem). $N$ agents with independent Wiener processes $W^i$ and i.i.d. initial states $X^i_0\sim\mu_0$ use a common feedback function $v(t,x)$; the law is replaced by the empirical measure $\mu^N_t=\frac1N\sum_j\delta_{X^j_t}$, and the cost is $J^N(v)=\frac1N\sum_i\mathbb E[\int_0^Tf(t,X^i_t,\mu^N_t,v(t,X^i_t))\,dt+g(X^i_T,\mu^N_T)]$.

Problem 2 (the computable proxy). With $\Delta t=T/N_T$ and $t_n=n\Delta t$, the $N$ agents follow the Euler scheme

$$\check X^i_{t_{n+1}}=\check X^i_{t_n}+b(t_n,\check X^i_{t_n},\check\mu_{t_n},\varphi(t_n,\check X^i_{t_n}))\Delta t+\sigma(t_n,\check X^i_{t_n},\check\mu_{t_n})\Delta\check W^i_n$$

with i.i.d. Gaussian increments $\Delta\check W^i_n\sim\mathcal N(0,\Delta t\,I_d)$, and $\check J^N(\varphi)$ is the expected time-discretized cost. The feedback $\varphi$ ranges over $\mathbf N^\psi_{d+1,n_{\rm in},k}$, the one-hidden-layer neural networks from $(t,x)\in\mathbb R^{d+1}$ to $\mathbb R^k$ with $n_{\rm in}$ hidden neurons and activation $\psi$; $\psi$ is $2\pi$-periodic, of class $\mathcal C^3$, with $\hat\psi_1=\int_{-\pi}^{\pi}\psi(x)e^{-ix}\,dx\ne0$.

The standing assumptions (§2.2 and Appendix A of the paper) make $b,\sigma$ affine in $(x,\bar\mu,\alpha)$ (A1), make $f,g$ differentiable in $(x,\alpha,\mu)$ (in $\mu$ in the sense of the L-derivative) with Lipschitz derivatives (A2)–(A3), make $f$ strongly convex in $\alpha$ (A4), and add the regularity (B1)–(B3), (C1)–(C3). Under them the reduced Hamiltonian $b\cdot y+f$ has a minimizer $\hat\alpha(t,x,\mu,y)$, the Pontryagin forward–backward system has a solution $(X,Y,Z)$ with marginal flow $\mu_t$, and $Y_t=V(t,X_t)$ for a regular decoupling field $V$. The optimal feedback is $\hat v(t,x)=\hat\alpha(t,x,\mu_t,V(t,x))$.

Formalization targets

Goal: Theorem 3 (p. 4070)

$$\inf_{\alpha\in\mathbb A}J(\alpha)\ \ge\ \inf_{\varphi\in\mathbf N^\psi_{d+1,n_{\rm in},k}}\check J^N(\varphi)-C\Big(N^{-1/\max(d,4)}\sqrt{1+\ln(N)\mathbf 1_{\{d=4\}}}+n_{\rm in}^{-1/(3(d+1))}+\sqrt{\Delta t}\Big)$$

for a constant $C$ depending only on the data and on $\psi$, for all $N,n_{\rm in},N_T\ge1$.

The three steps

1. Proposition 7 (finite population): $\inf_\alpha J(\alpha)\ge J^N(\hat v)-c_1\sqrt{N^{-2/\max(d,4)}(1+\ln(N)\mathbf 1_{\{d=4\}})}$.
2. Proposition 8 (network class): some $\hat\varphi\in\mathbf N^\psi_{d+1,n_{\rm in},k}$ with bounded Lipschitz constants has $J^N(\hat v)\ge J^N(\hat\varphi)-K_2n_{\rm in}^{-1/(3(d+1))}$.
3. Proposition 15 (time step): $|J^N(\varphi)-\check J^N(\varphi)|\le C\sqrt{\Delta t}$ for regular feedbacks.

Supporting results

Lemma 18 (Lipschitz continuity of $\hat\alpha$), Proposition 10 (network approximation of a function and its first two $x$-derivatives at rate $n_{\rm in}^{-1/(2(d+1))}$ on $[0,T]\times\bar B_d(0,R)$), (C.2) (moment bounds uniform in $N$), Proposition 13 (stability of $J^N$ under feedbacks close on a ball), Lemma 19 (time regularity of the particle system) and Lemma 14 (strong error $CN\Delta t$ of the Euler scheme).

Significance

The theorem certifies the standard deep-learning approach to mean field control: the value computed by minimizing the simulated finite-population, discrete-time cost over networks is, up to an explicit error with separate rates for population size, network width and time step, no larger than the true MKV value. The rates also expose where the method loses: the $n_{\rm in}^{-1/(3(d+1))}$ term is a curse of dimensionality in the network step (Remark 11).

The result is proved in the paper (§3 and Appendices B–D); the proof of Proposition 7 is a modification of Carmona–Delarue, Vol. II, Theorem 6.17. None of it is formalized. A formal development would provide the first machine-checked bridge between a stochastic control problem of McKean–Vlasov type and a concrete learning architecture, and its intermediate results (moment and stability estimates for interacting particle systems, the strong error of an Euler scheme with constants independent of the number of particles, simultaneous approximation of a function and its derivatives by periodic networks) are reusable on their own.

Difficulty

Each step rests on research-level analysis. Proposition 7 needs the Pontryagin principle for McKean–Vlasov control, the propagation of chaos for the optimally controlled system, and the Fournier–Guillin rate for empirical measures, whose $\max(d,4)$ exponent and logarithmic correction at $d=4$ appear in the bound. Proposition 8 requires approximating the optimal feedback together with its first two derivatives in $x$, because the time-discretization step needs regularity of the approximating network; standard universal approximation results give no control of derivatives, and the available simultaneous approximation results hold only for periodic functions, which forces a localization to a ball whose radius must be balanced against the approximation rate. Proposition 15 cannot be obtained from classical Euler estimates for a system of $Nd$ equations, whose constants grow with $N$: the estimates must be done agent by agent through the empirical measure.

Formalization scope

$\mathbb R^d$ is Fin d → ℝ with the sup norm; every constant is existential, so all statements are norm-independent. Time is ℝ≥0 for processes. Solutions of (2.2) and (3.2) use the published Itô-process predicate Peng1990.SMP.IsItoProcess (for $X-X_0$, with continuous paths and the natural filtration of the initial data and the noise); the backward equation of the Pontryagin system uses Peng1990.SMP.SolvesBSDE; $W_2$ is the published WassersteinDRO.Duality.wassersteinDistance. Problem 2 is law-level: the Euler scheme is a deterministic map of initial positions and increments, integrated against $\mu_0^{\otimes N}\otimes\mathcal N(0,\Delta t I_d)^{\otimes NN_T}$; Lemma 14 couples it with the continuous system through the Brownian increments, as the paper does.

The hypotheses are bundled as Coeff ((A1)–(A4), (B1), (B3), (C1), with witnesses for every derivative; the L-derivative is the Fréchet derivative of the lift on $L^2([0,1])$) and DecouplingField ((2.6), existence of a solution of (2.7) on some Problem-1 space, $Y_t=V(t,X_t)$, (B2), (C2), (C3)). Disclosed readings: $g$'s L-convexity is (A4) without $\alpha$ and with right-hand side $0$; unique solvability of (2.7), uniqueness and Lipschitz continuity of $\hat\alpha$ are not assumed (the last is Lemma 18); Proposition 13 lets its constant depend on bounds for $|v(0,0)|,|w(0,0)|$, as its proof does; Proposition 15 reads the first bound of (3.16) as $C_1(1+|(t,x)|)$. Infima are stated pointwise ($\forall\alpha\,\forall\eta>0\,\exists\varphi$), never as a real ⨅, and $N,n_{\rm in},N_T\ge1$ throughout. The hypothesis bundle is not vacuous: a sorry-free check exhibits the model $b=\sigma=0$, $f=|\alpha|^2$, $g=0$, $\mu_0=\delta_0$ with $\hat\alpha=0$, $V=0$ satisfying every assumption on any Problem-1 space. Junk values cannot trivialize the goal: the costs are Bochner integrals whose integrability follows from the assumptions, so a non-integrable cost would only make the claimed inequality harder, never vacuous.

Contributions are welcome at every level: proofs of the milestones, in particular the self-contained Lemmas 14 and 19, (C.2) and Proposition 13; infrastructure for the L-derivative, Itô's formula for the published Itô processes, empirical-measure convergence rates, and trigonometric approximation of $\mathcal C^r$ periodic functions.

Selected references

• R. Carmona, M. Laurière, Convergence analysis of machine learning algorithms for the numerical solution of mean field control and games: II — the finite horizon case, Ann. Appl. Probab. 32(6) (2022), 4065–4105. https://doi.org/10.1214/21-AAP1715
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications I–II, Springer (2018). https://doi.org/10.1007/978-3-319-58920-6
• N. Fournier, A. Guillin, On the rate of convergence in Wasserstein distance of the empirical measure, Probab. Theory Relat. Fields 162 (2015), 707–738. https://doi.org/10.1007/s00440-014-0583-7
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4) (1990), 966–979. https://doi.org/10.1137/0328054

Motivation

Large systems of interacting diffusions — neurons, oscillators, agents in a network game, particles in a queueing or load-balancing model — are usually analysed through their mean-field limit: as the population grows, each particle interacts with the empirical law of the others, and the system is replaced by a single nonlinear (McKean–Vlasov) equation. The classical theory assumes that every particle interacts with every other one with the same strength. Real networks are heterogeneous and sparse: particle $i$ interacts with particle $j$ only through an edge of a random graph, and the number of neighbours of a particle is much smaller than the population size.

Bayraktar, Chakraborty and Wu (Ann. Appl. Probab. 33(5), 2023) describe the heterogeneity by a graphon and prove laws of large numbers and rates of convergence for such systems. This mission is the fifth of a series formalizing that paper. Its subject is the paper's quantitative result for not-so-dense graphs: when the edges are sampled from a Lipschitz graphon and then thinned by a sparsity factor $\beta_n$, the average mean-square distance between each particle and its graphon limit is of order $(n\beta_n)^{-1/q}$ for every $q>1$.

Setting

Let $I=[0,1]$ with Lebesgue measure. A graphon is a measurable symmetric function $G:I\times I\to[0,1]$. Fix a horizon $T>0$ and write $\mathcal C_d=C([0,T]:\mathbb R^d)$ with the norm $\|x\|_{*,T}=\sup_{0\le s\le T}|x_s|$.

One probability space carries, for every label $u\in I$, an initial state $X_u(0)$ with law $\mu_u(0)$ and a standard $d$-dimensional Brownian motion $B_u$, the whole family $\{X_u(0),B_u:u\in I\}$ being independent. The limit system (4.2) is a continuum of diffusions, one per label:

$$X_u(t)=X_u(0)+\int_0^t\!\int_I\!\int_{\mathbb R^d}b(X_u(s),x)\,G(u,v)\,\mu_{v,s}(dx)\,dv\,ds+\int_0^t\sigma(X_u(s))\,dB_u(s),\qquad \mu_{u,t}=\mathcal L(X_u(t)).$$

The particles are independent but not identically distributed; their laws are coupled through the $dv$-integral.

The not-so-dense $n$-particle system (4.1) uses the same initial states and Brownian motions at the labels $i/n$:

$$X^n_i(t)=X_{i/n}(0)+\int_0^t\frac{1}{n\beta_n}\sum_{j=1}^n\xi^n_{ij}\,b(X^n_i(s),X^n_j(s))\,ds+\int_0^t\sigma(X^n_i(s))\,dB_{i/n}(s),\qquad i=1,\dots,n.$$

The edges are percolated samples of $G$ (Condition 4.3): $\xi^n_{ij}=\xi^n_{ji}\sim\mathrm{Bernoulli}(\beta_nG(i/n,j/n))$, independent for $1\le i\le j\le n$ and independent of the noise. A particle has about $n\beta_n$ neighbours, which is why the interaction is scaled by $1/(n\beta_n)$.

The standing hypotheses are Condition 4.1 — $u\mapsto\mu_u(0)$ measurable with bounded second moments; $b$ bounded and Lipschitz; $\sigma$ bounded, Lipschitz and invertible with bounded inverse; $\beta_n\in(0,1]$ and $n\beta_n\to\infty$ — and Condition 2.3: on finitely many intervals $I_1,\dots,I_N$ covering $I$, the map $u\mapsto\mu_u(0)$ is Lipschitz in the Wasserstein distance $W_2$, and $G$ is Lipschitz on every block $I_i\times I_j$.

Formalization targets

Goal: Theorem 4.2

Under Conditions 2.3, 4.1 and 4.3, for each $q\in(1,\infty)$ there is $\kappa(q)\in(0,\infty)$ with

$$\frac1n\sum_{i=1}^n\mathbb E\big\|X^n_i-X_{i/n}\big\|_{*,T}^2\le\frac{\kappa(q)}{(n\beta_n)^{1/q}}\qquad\text{for all }n\in\mathbb N .$$

The constant depends on $q$ and on the data, never on $n$. The bound is on the average over particles, not on the maximum.

Milestones

1. Lemma 7.1: all moments of the coupling error are bounded uniformly in $n$ and $i$.
2. (7.10): $\mathbb E[\xi^n_{ij}|X^n_j(s)-X_{j/n}(s)|^2]\le\big(2\mathbb E|X^n_j(s)-X_{j/n}(s)|^2+\kappa(q)(n\beta_n)^{-1/q}\big)\beta_nG(i/n,j/n)$.
3. (7.15): the interaction error $R^{n,2}_s$ is at most $(\kappa/n)\sum_j\mathbb E|X^n_j(s)-X_{j/n}(s)|^2+\kappa(q)(n\beta_n)^{-1/q}$.
4. Theorem 2.1(b) for (4.2): $W_{2,T}(\mu_u,\mu_v)\le\kappa|u-v|$ for $u,v$ in one interval $I_i$.
5. §7.3 display: the discretization error $R^{n,4}_s$ is at most $\kappa/n^2$.

Significance

Theorem 4.2 gives an explicit rate for the convergence of a particle system on a sparse random graph to its graphon limit. Its companion, Theorem 4.1 (mission IV), proves the law of large numbers under weaker hypotheses but without a rate. The rate says that the effective sample size is $n\beta_n$, the typical degree, not $n$: graphs with $\beta_n\to0$ still approximate the graphon system as long as the degree grows. Results of this type justify replacing a large heterogeneous network by its graphon limit in control and game problems, such as graphon mean-field games, where the error of the replacement must be quantified.

The paper proves the theorem by hand; none of its results has a machine-checked proof. The formalization produces precise statements of the not-so-dense model, of the estimates of §7.1 that hold for any sparsity, and of the discretization bound, each usable on its own. The milestones (7.10) and (7.15) are the paper's key estimates for sparse interactions and are shared with mission IV.

Difficulty

The obvious approach is to compare each $X^n_i$ with $X_{i/n}$ by Gronwall's inequality, after bounding the difference of drifts. That step fails at the interaction term: the edge $\xi^n_{ij}$ and the error $X^n_j-X_{j/n}$ are dependent, because the edge enters the dynamics of particle $j$. A plain Cauchy–Schwarz bound loses a factor $1/\beta_n$ and gives nothing when $\beta_n\to0$. Estimates (7.10) and (7.15) quantify how weak this dependence is, and they are where the hypotheses that $\sigma$ is invertible with bounded inverse and that $n\beta_n\to\infty$ are needed. The discretization term needs the Lipschitz regularity of the limit laws in the label (Theorem 2.1(b)), itself a fixed-point estimate on a space of measure-valued maps.

Formalization scope

The Lean development uses Mathlib's unitInterval for $I$, Fin d → ℝ with its sup norm for $\mathbb R^d$ (all constants are existential, so the choice of norm does not matter), time ℝ≥0, and the path space $\mathcal C_d$ as continuous maps on $[0,T]$ with the sup norm. Brownian motions, Itô integrals and Itô processes are those of the published Peng1990.SMP.Stochastic; Wasserstein distances are the published WassersteinDRO.Duality.wassersteinDistance, valued in $[0,\infty]$. Particle $i$ is Lean's i : Fin n with label $(i+1)/n$.

Committed conventions:

• A solution of (4.2) has continuous paths, AE-measurable path maps, and path laws in the class $\mathcal M$ (measurable in $u$, bounded second moments); each $X_u$ is a strong solution for the filtration of $(X_u(0),B_u)$. A solution of (4.1) is a strong solution for the filtration of the edges, the initial states and the Brownian motions of the $n$ labels.
• The edges are $\{0,1\}$-valued, symmetric, with the diagonal included, mutually independent over $i\le j$, and independent of the σ-algebra of the noise.
• Condition 4.1(d) is required for $n\ge1$; the invertibility of $\sigma$ is that of a $d\times d$ matrix; the intervals of Condition 2.3 are order-connected subsets of $I$.
• Expectations of nonnegative quantities are lower Lebesgue integrals, so no expectation is silently $0$ for a non-integrable integrand.

The solution predicates are not vacuous: the zero-coefficient system $X_u(t)=X_u(0)$ satisfies both, Condition 4.1 and Condition 4.3 are satisfiable, and every statement quantifies over solutions rather than assuming the conclusion. The constant $\kappa(q)$ is chosen after $q$ and before $n$, so it cannot depend on $n$, and the bound is the paper's average over $i$, not a weaker or a stronger form. At $n=0$ both sides of every rate are $0$.

The paper's proofs are in its §5 (Theorem 2.1), §7.1 (Lemma 7.1, (7.10), (7.15)) and §7.3 (Theorem 4.2). Stochastic analysis at that level — Burkholder–Davis–Gundy and Rosenthal inequalities, Girsanov's theorem for these SDEs, Gronwall arguments for measure-valued fixed points — is mostly absent from Mathlib, and contributions of such infrastructure are welcome, as are proofs of any milestone.

Selected references

• E. Bayraktar, S. Chakraborty, R. Wu, Graphon mean field systems, Ann. Appl. Probab. 33(5):3587–3619, 2023. https://doi.org/10.1214/22-AAP1901
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60, 2012. https://doi.org/10.1090/coll/060
• B. Bollobás, C. Borgs, J. Chayes, O. Riordan, Percolation on dense graph sequences, Ann. Probab. 38(1):150–183, 2010. https://doi.org/10.1214/09-AOP478
• S. Peng, A general stochastic maximum principle for optimal control problems, SIAM J. Control Optim. 28(4):966–979, 1990. https://doi.org/10.1137/0328054

Motivation

Join-the-shortest-queue (JSQ) is the load-balancing rule in which each arriving job is sent to a server with the fewest jobs. It is a baseline in the design of server farms and data centers, and in the many-server Halfin–Whitt regime, where the load per server approaches one at rate $1/\sqrt n$, it combines near-full utilization with vanishing waiting. Eschenfeldt and Gamarnik (arXiv:1502.00999, 2015) proved that the suitably scaled JSQ process converges, over bounded time intervals, to a two-dimensional reflected diffusion; Mukherjee, Borst, van Leeuwaarden and Whiting (J. Appl. Probab. 53, 2016) gave the form of the result that Braverman quotes as Theorem 1. Process-level convergence over bounded time intervals says nothing about the stationary distribution. To conclude that the stationary distributions converge as well, one needs tightness of the scaled stationary distributions, uniformly in the number of servers $n$.

Braverman (arXiv:1801.05121, Math. Oper. Res. 45(3), 2020) supplied this, together with positive recurrence of the diffusion limit. This mission formalizes the first of the two main results, Theorem 2, and the chain of lemmas the paper uses to prove it.

Setting

There are $n$ identical servers, each with its own infinite buffer. Jobs arrive as a Poisson process of rate $n\lambda$ and service times are i.i.d. exponential with mean one. An arriving job joins a server with the fewest jobs, ties broken arbitrarily. The Halfin–Whitt regime is

$$\lambda = 1 - \beta/\sqrt n,\qquad \beta > 0 \text{ fixed}.$$

For $i \ge 1$, $Q_i$ is the number of servers with at least $i$ jobs. The process $Q = (Q_1, Q_2, \dots)$ is a continuous-time Markov chain on

$$S = \Big\{ q \in \{0,1,\dots,n\}^\infty \ \Big|\ q_i \ge q_{i+1},\ \textstyle\sum_i q_i < \infty \Big\}.$$

Its generator $G_Q$ sends $q$ to $q + e^{(i)}$ at rate $n\lambda$ when $q_1 = \dots = q_{i-1} = n > q_i$, and to $q - e^{(i)}$ at rate $q_i - q_{i+1}$. The fluid-scaled coordinates are $X_1 = (Q_1 - n)/n \le 0$, the negative of the fraction of idle servers, and $X_i = Q_i/n$ for $i \ge 2$. The diffusion-scaled coordinates are $\sqrt n X_i$. Expectations $\mathbb E$ are taken under a stationary distribution $\pi$ of the chain.

The proof works with functions on $\Omega = (-\infty, 0] \times [0, \infty)$ and with the first-order operator

$$Lf(x) = (-x_1 + x_2 - \beta/\sqrt n) f_1(x) - x_2 f_2(x),$$

where $f_i$ is the partial derivative in $x_i$, taken one-sided on $\partial\Omega$.

Formalization targets

Goal: Theorem 2

For each $\beta > 0$ there is a constant $C(\beta)$ such that for all $n \ge 1$ with $\beta < \sqrt n$ and every stationary distribution,

$$\mathbb E\big|\sqrt n X_i\big| \le C(\beta),\ \ i = 1, 2,\qquad \mathbb E\big|n X_i\big| \le C(\beta),\ \ i \ge 3.$$

The constant depends on $\beta$ only, not on $n$, the stationary distribution, or $i$.

Milestones, in the order the proof uses them

1. Lemma 1: $\mathbb E\,G_Q f(Q) = 0$ whenever $\mathbb E|f(Q)| < \infty$.
2. Lemma 2: $\mathbb E Q_1 = n\lambda$ and $\mathbb E Q_i = n\lambda\,\mathbb P(Q_1 = \dots = Q_{i-1} = n)$.
3. Lemma 3: the generator, applied to $f(x_1, x_2)$, equals $Lf(x) + (f_2 - f_1)(x)\lambda 1(x_1 = 0) + \varepsilon(x)$ with an explicit remainder $\varepsilon$ built from second weak derivatives.
4. Lemmas 5 and 6: the curve $\Gamma^{(\kappa)}$ and the hitting time $\tau(x)$ of the fluid model; existence and uniqueness, finiteness, derivative formulas and monotonicity in $\kappa$.
5. Lemma 7 and Lemma 4: for $\kappa > \beta$, the explicit function $f^*$ of (4.14) solves

$$Lf(x) = -\big((x_2 - \kappa/\sqrt n)\vee 0\big)\ \text{on } \Omega,\qquad f_1(0, x_2) = f_2(0, x_2),$$

with $f^*_{11}, f^*_{12}, f^*_{22} \ge 0$, vanishing second derivatives for $x_2 \le \kappa/\sqrt n$, and explicit upper bounds of order $\sqrt n/\beta$ above that level. 6. (3.18): $\mathbb E\big((X_2 - \kappa/\sqrt n)\vee 0\big) \le \frac{1}{\beta\sqrt n}\big(12 + \frac{6\kappa}{\kappa - \beta}\big)\mathbb P(X_2 \ge \kappa/\sqrt n - 1/n)$. 7. Theorem 2, (2.2): the $i = 1, 2$ half of the goal.

Significance

Theorem 2 shows that in steady state the number of idle servers and the number of servers holding two or more jobs are $O(\sqrt n)$ on average, and the number of servers holding $i \ge 3$ jobs is $O(1)$ on average, uniformly in $n$. Combined with the process-level limit and the positive recurrence of the limiting diffusion (Theorem 3, the companion mission), it yields Proposition 1: the diffusion-scaled stationary distribution converges to the stationary distribution of the diffusion. This justifies the diffusion as a steady-state approximation for JSQ.

The method is the generator-comparison or Stein's-method approach: a Lyapunov function solving a first-order PDE for the fluid model, with explicit bounds on its derivatives. It applies to other many-server systems, and the paper is an example of that approach on an infinite-dimensional chain whose diffusion limit is two-dimensional.

The result is proved in the paper; no machine-checked proof is known to exist. The work remaining is to formalize the known proof: the adjoint relation for a countable-state chain with bounded rates, the Taylor expansion of the generator, and the explicit analysis of $f^*$ through the fluid curves.

Difficulty

The obvious route is to bound $\mathbb P(Q_1 = \dots = Q_{i-1} = n)$ in Lemma 2 directly. The paper notes that no good handle on these probabilities exists. The PDE route needs a solution whose second derivatives are bounded by $O(\sqrt n)$. General results that give such bounds require a continuous fluid vector field, and the JSQ fluid model is discontinuous because of the reflection at $x_1 = 0$. So $f^*$ is constructed explicitly from the fluid paths, and its derivatives must be bounded by hand through the implicitly defined $\tau(x)$ and $\nu^*(x_1)$.

A second difficulty is dimensional: the chain is infinite-dimensional while the PDE is two-dimensional, so the remainder of Lemma 3 contains a term with $q_3$ that is controlled only by combining Lemma 2 with the monotonicity of $f^*_2$.

Formalization scope

• Model. States are functions ℕ → ℕ with 0-based indices: Lean q.1 i is the paper's $q_{i+1}$, so the goal's "$i \ge 3$" is Lean index $\ge 2$. Each state is bounded by $n$, nonincreasing and eventually zero. The generator genQ is the displayed formula on p. 6.
• Stationarity. No process is constructed. A stationary distribution is a probability $\pi$ on $S$ satisfying global balance $\pi G_Q = 0$, which characterizes stationarity for this chain with bounded rates. Such a $\pi$ exists, since the chain is positive recurrent for $\lambda < 1$ (Bramson 2011), so statements quantifying over it are not vacuous. Expectations are sums against $\pi$. Lemma 1 keeps its integrability hypothesis, and all other expectations are of bounded functions.
• Parameters. $\lambda = 1 - \beta/\sqrt n$ with $0 < \beta < \sqrt n$, so that $\lambda > 0$; $\lambda$ is free in Lemmas 1–2. Constants are quantified as $\exists C$ after $\beta$ and before $n$.
• Misprint. The printed Theorem 2 omits $\mathbb E$. Read as an almost-sure bound it is false, so the expectation version, which the paper proves, is the target.
• Derivatives. Points of $\Omega$ are pairs in ℝ × ℝ. Partial derivatives are named functions asserted to be one-sided derivatives along coordinate lines (HasDerivWithinAt on Set.Iic 0 or Set.Ici 0). Weak second derivatives are a.e. derivatives of absolutely continuous functions, in integral form on compact intervals. A "solution" of the PDE whose derivatives are the junk values of a derivative operator is thereby excluded. The PDE needs genuine derivatives, and Lemma 7 is about the explicit $f^*$ of (4.14), not about an arbitrary function.
• Fluid objects. $\nu^*, \eta^*$ are the components of the unique solution of (4.8). $\tau$ is valued in WithTop ℝ, with $\infty$ as ⊤, so a missing solution is never read as $0$. $f^*$ is an if cascade, and Lemma 7 states the agreement of its branches. $f^*$ is defined by the closed form (4.14), not through the fluid model (4.1).
• Not included. Lemma 9 (via the Lambert W function, which Mathlib lacks), the bootstrapping argument of App. A.4 (not a numbered result), Theorems 1 and 3, and Proposition 1.

Contributions of reusable infrastructure are welcome: the adjoint relation for countable-state chains with bounded rates, and FTC/Taylor lemmas for absolutely continuous first derivatives.

Selected references

• A. Braverman, Steady-State Analysis of the Join-the-Shortest-Queue Model in the Halfin–Whitt Regime, Math. Oper. Res. 45(3), 2020; arXiv:1801.05121v2. https://arxiv.org/abs/1801.05121
• P. Eschenfeldt, D. Gamarnik, Join the Shortest Queue with Many Servers. The Heavy Traffic Asymptotics, arXiv preprint, 2015. https://arxiv.org/abs/1502.00999
• D. Mukherjee, S. C. Borst, J. S. H. van Leeuwaarden, P. A. Whiting, Universality of Load Balancing Schemes on the Diffusion Scale, J. Appl. Probab. 53, 1111–1124, 2016. https://projecteuclid.org/euclid.jap/1481132840
• M. Bramson, Stability of Join the Shortest Queue Networks, Ann. Appl. Probab. 21, 1568–1625, 2011. https://doi.org/10.1214/10-AAP726
• S. Halfin, W. Whitt, Heavy-Traffic Limits for Queues with Many Exponential Servers, Oper. Res. 29(3), 1981. https://doi.org/10.1287/opre.29.3.567

Motivation

Large networks are often modeled through a graphon, a measurable function that records how likely two labeled vertices are to interact. For interacting diffusions, this lets one ask whether a finite random network has a predictable population limit. Bayraktar, Chakraborty and Wu study that question for graphon weighted systems, including graphs obtained by independently retaining potential edges with a sparsity parameter $\beta_n$. Their not-so-dense regime allows $\beta_n$ to decrease, provided the typical interaction scale $n\beta_n$ diverges. Theorem 4.1 is the paper's law of large numbers for this regime; its two conclusions distinguish convergence of the population's empirical law from mean-square closeness of each particle to a coupled graphon limit. Bayraktar, Chakraborty and Wu, 2023.

The authors present three main convergence results: continuity of the continuum graphon system in Section 2, a dense-system law of large numbers in Section 3, and the percolated-system law of large numbers in Section 4. Section 7 establishes the latter. The graphon and cut-metric framework used here follows the graph-limit treatment cited by the paper. Bayraktar, Chakraborty and Wu, 2023; Lovász, 2012.

Setting

Let $I=[0,1]$. A graphon is a symmetric measurable $G:I^2\to[0,1]$. The cut norm $\|W\|_\square$ measures the largest absolute integral of $W$ over a measurable rectangle $S\times U$. A sequence of step graphons $G_n$ approaches $G$ when $\|G_n-G\|_\square\to0$. The related operator norm $\|W\|_{\infty\to1}$ measures the effect of $W$ on bounded measurable functions. Remark 2.1 says cut convergence implies convergence in this operator norm. Bayraktar, Chakraborty and Wu, 2023, Remark 2.1.

Fix a dimension $d\ge1$ and horizon $T>0$. A label $u\in I$ has an initial state $X_u(0)\in\mathbb R^d$ and an independent $d$-dimensional Brownian motion $B_u$. The initial states are independent of each other and of the Brownian motions. The limiting graphon particle $X_u$ is a continuous path whose drift averages $b(X_u(s),x)G(u,v)$ against the time-$s$ laws of all labels $v$, and whose diffusion matrix is $\sigma(X_u(s))$. The time-$s$ law at label $v$ is $\mu_{v,s}=\mathcal L(X_v(s))$. The family of path laws $\mu_u=\mathcal L(X_u)$ is measurable in $u$ and has uniformly bounded second moments. Bayraktar, Chakraborty and Wu, 2023, (4.2).

For $n$ particles, label $i$ means $i/n$, with $1\le i\le n$. Each undirected edge weight $\xi^n_{ij}=\xi^n_{ji}$ is Bernoulli with mean $\beta_nG_n(i/n,j/n)$; diagonal weights are included. These edge variables are independent of the Brownian motions and initial states. The finite particle $X_i^n$ uses the same initial state and Brownian motion as $X_{i/n}$. Its drift is the sum of $\xi^n_{ij}b(X_i^n,X_j^n)$ divided by $n\beta_n$; its diffusion is $\sigma(X_i^n)$. The coefficients $b$ and $\sigma$ are bounded and Lipschitz, and $\sigma(x)$ is invertible with uniformly bounded inverse. Initial laws have uniformly bounded second moments, $0<\beta_n\le1$, and $n\beta_n\to\infty$. Bayraktar, Chakraborty and Wu, 2023, Conditions 4.1–4.2.

Formalization targets

Let $\mathcal C_d=C([0,T];\mathbb R^d)$, $\mu^n=n^{-1}\sum_{i=1}^{n}\delta_{X_i^n}$, and $\bar\mu=\int_I\mu_u\,du$. The main target, Theorem 4.1, first asserts convergence in probability in the weak topology on $\mathcal P(\mathcal C_d)$:

$$\mu^n\xrightarrow{\mathbb P}\bar\mu.$$

This uses Condition 2.2(a): on each of finitely many intervals covering $I$, the initial law varies continuously in Wasserstein distance $W_2$. If the graphon also satisfies Condition 2.2(b), its stated sectional continuity outside null sets, the theorem adds

$$\frac1n\sum_{i=1}^{n}\mathbb E\|X_i^n-X_{i/n}\|_{*,T}^2\longrightarrow0, \qquad \|x\|_{*,T}=\sup_{0\le s\le T}|x_s|.$$

The milestones record the paper's cut-to-operator observation, uniform coupling moments, the one-edge and two-edge estimates, the bound on the second interaction-error term, the quantitative coupling lemma, and the empirical law of large numbers for the independent limiting particles. The second displayed limit is conditional on 2.2(b); the first is not. Bayraktar, Chakraborty and Wu, 2023, Theorem 4.1.

Significance

The first conclusion identifies the population-level limit even when the sampled network has a decreasing edge-retention probability. It gives a deterministic law on path space, rather than only a limit at one time. The second conclusion is stronger: it compares each finite particle with the limiting particle built from the same initial state and Brownian motion, averaged over all labels. This comparison is available when the extra graphon continuity assumption holds. Bayraktar, Chakraborty and Wu, 2023, Theorem 4.1 and Remark 4.1.

The mathematical results were proved in the published paper. The present mission asks for machine-checked Lean proofs of its specified statements; the draft theorems themselves currently contain sorry. Reusable outputs would include the percolated-edge model, a path-law formulation of graphon diffusions, and estimates for random interactions that depend on the particle states they influence. The paper's proofs appear in Sections 5–7, with the sparse-system argument in Section 7. Bayraktar, Chakraborty and Wu, 2023.

Difficulty

The edge variables are independent of the driving noise, but a particle's state depends on its incident edges. Therefore an expression such as $\mathbb E[\xi^n_{ij}|X_j^n-X_{j/n}|^2]$ cannot be factored into the edge mean times the error moment. The same dependence affects pairs of edges in the squared interaction sum. Equations (7.10), (7.14), and (7.15) quantify the discrepancy. A second difficulty is that cut convergence controls integrals against fixed bounded tests, while the dynamics and their path laws supply tests that vary with the system. The paper's regularity conditions and quantitative estimates are needed to connect those forms of control. Bayraktar, Chakraborty and Wu, 2023, Sections 7.1–7.2.

Formalization scope

Lean represents $I$ by Mathlib's unit interval, $\mathbb R^d$ by Fin d → ℝ, and continuous paths by maps from $[0,T]$ into that vector space. The chosen vector and matrix norms are fixed sup-type norms; finite-dimensional norm equivalence preserves the limit statements and the estimates with existential constants. The horizon and dimension are explicitly positive. Particle index i : Fin n denotes the paper's $(i+1)$st particle, and empirical laws use positive sizes $n+1$ to avoid division by zero. Wasserstein distances use extended nonnegative reals, while nonnegative expectations use lower integrals.

The noise lives on one probability space. The continuum equation uses the natural filtration of its own initial state and Brownian motion. The finite equation uses the natural filtration of its edge array, sampled initial states, and Brownian motions. A solution carries a measurable continuous-path law family in the paper's class $\mathcal M$; this prevents a nonmeasurable pushforward or a default-zero integral from silently satisfying an equation. Edge symmetry, Bernoulli marginals, independence, and diagonal self-loops are explicit. The zero-coefficient system has a separate sorry-free Lean witness for both solution predicates, ruling out a vacuous solution concept.

The formalization uses the published Peng1990.SMP.Stochastic Itô interface and WassersteinDRO.Duality.wassersteinDistance definition. Contributions can prove the listed estimates, strengthen their reusable stochastic and measure-theoretic infrastructure, or connect this mission's local setting to the other graphon missions after their definitions are published. The auxiliary changed-measure particles of Section 7.1 are outside the initial milestone list. Bayraktar, Chakraborty and Wu, 2023, Sections 4 and 7.

Selected references

• E. Bayraktar, S. Chakraborty and R. Wu, Graphon mean field systems, Annals of Applied Probability 33(5):3587–3619, 2023. DOI.
• L. Lovász, Large Networks and Graph Limits, American Mathematical Society Colloquium Publications 60, 2012. DOI.

Motivation

Reflected backward stochastic differential equations describe processes that must remain above a prescribed obstacle. El Karoui, Kapoudjian, Pardoux, Peng and Quenez connect that probabilistic construction to a parabolic partial differential equation with an obstacle in their 1997 paper. A representation by a stochastic process is useful only if the associated differential equation identifies a definite function. The comparison result in Theorem 8.6 supplies that identification: within a specified growth class, two viscosity solutions cannot disagree. This mission isolates that deterministic uniqueness statement. The companion existence and stochastic representation result is Theorem 8.5 of the same paper.

Setting

Fix a terminal time $T>0$ and a spatial dimension $d\ge1$. At time $t\in[0,T]$ and point $x\in\mathbb R^d$, the drift $b(t,x)$ is a vector and the diffusion coefficient $\sigma(t,x)$ is a $d\times d$ matrix. Both are continuous and Lipschitz in $x$ uniformly over $t$. A continuous terminal payoff $g(x)$ has at most polynomial growth. The continuous generator $f(t,x,r,z)$ depends on a scalar value $r$ and a vector $z$; it has polynomial growth at $(r,z)=(0,0)$ and is Lipschitz in $(r,z)$. The continuous obstacle $h(t,x)$ has a polynomial upper bound and satisfies $h(T,x)\le g(x)$.

Write $a(t,x)=\sigma(t,x)\sigma(t,x)^\top$. The associated second order spatial operator is $L_t\phi=\tfrac12\operatorname{Tr}(aD^2\phi)+b\cdot D\phi$. The obstacle problem asks for a function whose terminal value is $g$ and whose interior value obeys

$$\min\{u-h,\,-\partial_tu-L_tu-f(t,x,u,Du\,\sigma)\}=0.$$

A parabolic superjet or subjet at an interior point is a triple $(p,q,X)$ of a time slope, spatial slope and symmetric second order matrix that bounds the function locally above or below by the associated quadratic expansion, up to $o(|s-t|+|y-x|^2)$. These jets let a continuous function satisfy the differential inequality without having ordinary derivatives. A viscosity subsolution uses superjets and a terminal upper bound; a viscosity supersolution uses subjets and a terminal lower bound. A viscosity solution satisfies both definitions.

Formalization targets

Uniqueness in the polynomial growth class

The goal is the paper's Theorem 8.6. Under the coefficient assumptions above and condition (27), every pair of continuous viscosity solutions with polynomial growth agrees on the entire closed time strip:

$$\bigl(u,v\text{ solve (24) and have polynomial growth}\bigr) \Longrightarrow u(t,x)=v(t,x)\quad\text{for every }(t,x)\in[0,T]\times\mathbb R^d.$$

Condition (27) gives a continuous modulus $m_R$ for the change in $f$ between bounded spatial points, with argument $|x-y|(1+|z|)$ and $m_R(0)=0$. The quantifiers include every radius $R>0$, every bounded scalar argument, and every gradient vector $z$. The milestone is Lemma 8.7, which controls the location and separation of the maximizers of the paper's doubled-variable function $\Phi_\alpha(t,x,y)=u(t,x)-v(t,y)-\alpha|x-y|^2/2$.

Significance

The theorem shows that the obstacle PDE has at most one solution in the natural class allowed by polynomially growing coefficients and payoffs. Together with Theorem 8.5, which identifies the reflected backward SDE value as a viscosity solution, and the growth estimate at the end of Section 8, it yields the paper's probabilistic representation of the unique solution. Theorem 8.6 alone asserts uniqueness, so it makes no existence claim.

The formal development provides reusable interfaces for parabolic jets, viscosity inequalities, the obstacle operator and uniform polynomial growth on a finite time strip. Those interfaces can serve other comparison theorems and other parabolic obstacle problems. The mathematical result is proved in the 1997 article; this mission asks for a Lean proof of its deterministic uniqueness statement. The proposal declares the theorem with a proof placeholder and includes the comparison lemma as an intermediate target.

Difficulty

The first obstruction is that the candidate solutions need only be continuous. Subtracting their PDE expressions directly would assume derivatives they may not possess. The paper instead uses viscosity jets, and its comparison argument invokes the theorem of sums from Crandall, Ishii and Lions' viscosity-solutions guide. The generator's spatial modulus must control a gradient argument that grows as the two spatial points approach each other. Lemma 8.7 provides the necessary separation limit for the maximizers. The argument also treats a polynomial growth class on all of $\mathbb R^d$, so a comparison confined to one fixed bounded ball would not establish the stated result.

Formalization scope

Lean uses nonnegative real time and functions on $\mathbb R^d$ represented by Fin d → ℝ. The terminal time and dimension are positive. Bounds with existential constants use the finite-dimensional sup norm, which is equivalent to the Euclidean norm in the paper. The displayed quadratic form, $\operatorname{Tr}(aX)$ and $q\sigma$ are written by coordinate sums, so their signs, factor $\tfrac12$, and matrix order are exact. The obstacle is bounded only above in the data assumptions, exactly as condition (22) states. Condition (27) is imposed only on uniqueness, not folded into the definition of viscosity solution.

Jets are taken at $0<t<T$ through a one-sided little-$o$ bound in the relative neighborhood of the interior strip. The terminal equality comes from the two terminal inequalities; the viscosity tests impose no separate condition at $t=0$. The printed text calls $S(d)$ “symmetric nonnegative matrices,” but the proof of Theorem 8.6 uses arbitrary symmetric matrices produced by the theorem of sums. The formal definition therefore uses all symmetric matrices and records this correction for review.

The mission permits every continuous solution of polynomial growth. It does not restrict candidates to smooth, bounded or stochastic-representation functions. The companion reflected SDE construction, penalization limit and existence theorem are outside this mission's goal; the general stochastic interface Peng1990.SMP.Stochastic is listed as series context but is not imported by the deterministic statements. Useful contributions include the comparison proof, the lemma on doubled-variable maximizers, and reusable lemmas about jet transformations and the matrix trace inequality.

Selected references

• N. El Karoui, C. Kapoudjian, É. Pardoux, S. Peng and M.-C. Quenez, Reflected solutions of backward SDE's, and related obstacle problems for PDE's, The Annals of Probability 25(2), 1997, pp. 702–737. DOI.
• M. G. Crandall, H. Ishii and P.-L. Lions, User's guide to viscosity solutions of second order partial differential equations, Bulletin of the American Mathematical Society 27(1), 1992, pp. 1–67. DOI.