Stochastic Systems

Motivation

Large networks of neurons are often modelled as systems of coupled stochastic differential equations: each neuron carries a low-dimensional state (a membrane potential and recovery variables, as in the FitzHugh–Nagumo model), receives synaptic input from the other neurons with a transmission delay, and is perturbed by noise. Because the number of neurons is large, one studies the mean-field limit: as the population grows, each neuron should evolve independently of every other fixed neuron, driven by its own noise and by an averaged population input. This asymptotic independence is called propagation of chaos, and the limiting single-neuron equation is a McKean–Vlasov equation.

Mehri, Scheutzow, Stannat and Zangeneh (arXiv:1805.01654v3, Ann. Appl. Probab. 2020, DOI 10.1214/19-AAP1499) prove propagation of chaos for a model combining features that earlier work treated separately: monotone (one-sided Lipschitz) local dynamics, general path-dependent delays, Lévy-type jump noise, spatial structure with several subpopulations, and a random environment (disorder). Earlier mean-field results for neuronal networks were obtained under global Lipschitz assumptions (Quiñinao and Touboul 2015; Touboul 2014, two papers), for locally Lipschitz coefficients (Baladron, Fasoli, Faugeras and Touboul 2012, with the clarification note of Bossy, Faugeras and Talay 2015) and for one-sided Lipschitz coefficients (Luçon and Stannat 2014; Touboul 2012); with jump noise, only under global Lipschitz or gradient-type local dynamics (Andreis, Dai Pra and Fischer 2018). This mission formalizes the paper's second main result, Theorem 1.8. The first mission of the series formalizes the well-posedness of the McKean–Vlasov equation (Theorem 1.5).

Setting

Neurons sit at positions $r$ in a bounded set $\Gamma\subset\mathbb R^k$, partitioned into $P$ measurable subpopulation regions $\Gamma_\alpha$. The $N$-th network consists of a finite set $\mathcal A_N\subset\Gamma$ of $N$ positions, and neurons of subpopulation $\alpha$ carry the weight $1/\mathcal S_{\mathcal A_N,\alpha}$. The state $X^{r,\mathcal A_N}_t\in\mathbb R^d$ of the neuron at $r$ solves the network equation (1)

$$dX^{r,\mathcal A_N}_t=f\,dt+g\,dW^r_t+\int_U h\,\tilde N^r(dt,d\xi)+\sum_{\alpha=1}^P\frac{1}{\mathcal S_{\mathcal A_N,\alpha}}\sum_{\tilde r\in\mathcal A_N\cap\Gamma_\alpha}\Big[\theta\,dt+\beta\,dB^{r,\alpha}_t+\int_U\eta\,\tilde N^{r,\alpha}(dt,d\xi)\Big],$$

where $f,g,h$ are evaluated at $(t,r,X^{r,\mathcal A_N}_{t-},\omega')$ and $\theta,\beta,\eta$ at $(t,r,\tilde r,X^{r,\mathcal A_N}_{t-},X^{\tilde r,\mathcal A_N}_{(t-\tau)^-:t^-},\omega')$, the last argument being the path of the presynaptic neuron over the delay window $[t-\tau,t]$. The noises $W^r$, $B^{r,\alpha}$ are independent Brownian motions, $\tilde N^r$, $\tilde N^{r,\alpha}$ independent compensated Poisson random measures with intensity $dt\otimes\nu$, and $\omega'$ is a random disorder with expectation $\mathcal E$. Each neuron starts from a path $z^r$ on $[-\tau,0]$.

Given a finite measure $\mathcal R$ on $\Gamma$ with $\mathcal R(\Gamma_\alpha)=1$, the McKean–Vlasov equation (6) describes a continuum of neurons $X^r$, $r\in\Gamma$, whose interaction is $\sum_\alpha\int_{\Gamma_\alpha}\tilde{\mathbb E}[\theta(t,r,r',X^r_{t-},\tilde X^{r'}_{(t-\tau)^-:t^-},\omega')]\mathcal R(dr')$, with $\tilde X$ an independent copy of $X$ (and likewise for $\beta$, $\eta$). The mean-field equation (5) for a neuron $r$ of the network has the same form, with $X^r$ replaced by a process $\bar X^r$ that starts from the same $z^r$ and is driven by the same noises $W^r, B^{r,\alpha}, \tilde N^r,\tilde N^{r,\alpha}$ as neuron $r$ of the network, while the interaction is computed from the law of the solution of (6).

Formalization targets

Goal: Theorem 1.8

Under Hypothesis 1.6 and the chaotic initial condition (the $z^r$ are independent, with $z^r$ distributed as $\hat z^\alpha$ for $r\in\Gamma_\alpha$),

$$\lim_{N\to\infty}\mathcal E\sup_{t\in[-\tau,T],\,r\in\mathcal A_N}\mathbb E\big|X^{r,\mathcal A_N}_t-\bar X^r_t\big|^2=0 .$$

The theorem asserts convergence without a rate, which is the stable form of the result.

Milestones

1. Proposition 1.2: the network equation (1) is well posed.
2. Lemma 1.7: positions in one cell $\Gamma^{m,\varepsilon}_\alpha$ of the partition of Hypothesis 1.6 have solutions of (6) within $C_2(t,\omega')\varepsilon$ in mean square.
3. Display (18): the first moment estimate for $X^{r,\mathcal A_N}-\bar X^r$, in terms of the fluctuation terms $I^\theta_\alpha$, $I^\beta_\alpha$, $I^\eta_\alpha$.
4. The bound (p. 20) of each $I$-term by $6(\cdots)C_2(t,\omega')$.
5. The Gronwall bound (p. 21) with constant $36$, at a fixed disorder.
6. The bound (p. 21) after integration over the disorder, with a constant $C(T)$ independent of $\varepsilon$ and $N$.

The proof also uses Lemma 1.4 (the moment bound $C_1$ for solutions of (6)), which is a milestone of the first mission of this series and is not restated here.

Significance

Theorem 1.8 justifies replacing a large, spatially structured network of delayed, jump-driven neurons by a single McKean–Vlasov equation indexed by position. The limit is the object on which neural field models and their bifurcation analysis are built; the theorem identifies the hypotheses on the spatial distribution of neurons (condition (10): the neuron counts per cell, normalized by the weights, converge to $\mathcal R$) under which that replacement is valid in a random environment.

The result is proved in the paper; no machine-checked proof exists. Formalizing it requires a coherent Lean layer for strong solutions of delay SDEs with jumps, mean-field interaction terms, Poisson random measures with product marks, and independence of countable families of drivers. The intermediate bounds of §3 are explicit and quantitative, and each is a self-contained target.

Difficulty

The interaction of the network is an empirical average over finitely many neurons, while the limit uses an expectation over a continuum of positions. The difference splits into three errors of different nature: a fluctuation term, whose control requires that the limit processes $\bar X^{\tilde r}$ of distinct neurons be independent (which holds only because each is driven by its own noise and starts from an independent initial condition); a spatial discretization error within each cell, which requires a quantitative regularity of the solution of (6) in the position variable; and a counting error between the neuron counts and the measure $\mathcal R$. A naive comparison of the network with (6) directly, without the coupled processes $\bar X^r$ of (5), gives no pathwise relation and does not work. The coefficients are only one-sided Lipschitz in the local variable, so moment bounds must come from monotonicity rather than from global Lipschitz estimates, and the disorder enters the constants through exponentials whose integrability is exactly assumption (H6).

Formalization scope

Positions are EuclideanSpace ℝ (Fin k), states EthierKurtz.SDEState d, and subpopulations Fin P (0-based). Neurons carry labels in ℕ with an injective position map, so $\mathcal A_N$ is a finite set of labels and $\bigcup_N\mathcal A_N$ is countable. Brownian integrals are the published EthierKurtz.HasBrownianItoIntegral per coordinate, compensated jump integrals the published JacodTodorov10.LLN.HasCompInt, and all Poisson measures of the network form one (𝓕_t)-Poisson random measure on a product mark space. Integrands are cut off after the horizon $T$. All expectations, suprema and the disorder expectation $\mathcal E$ are taken in $[0,\infty]$, so no statement can be satisfied by a junk value of a real integral or supremum; (H6) states the boundedness of its supremum explicitly. The copy $\hat X$ enters only through its law: the solution of (6) lives on its own probability space and the mean-field terms are expectations over it.

Conventions and corrections, all disclosed in the items: the theorem is stated for every family of solutions of (1), (5) and (6) (hypotheses), not for "the" solutions; (H1′) is printed with $x-y$ and is read as $x-\tilde x$; $I^\eta_\alpha$ carries the expectation of (17), which the display on p. 20 omits; the second Gronwall inequality on p. 21 (constant $144$) drops a factor of $C_1$ and is not posed; the coefficients' path argument carries the product σ-algebra; the filtration satisfies the usual conditions (Appendix A); the solution class of (6) is a bound for every time. The solution notions are not trivializing: every stochastic integral is tied to the given noise by a published predicate, the mean-field terms are computed from the solution of (6) itself, the limit processes share the network's noise and initial conditions, and the finite constant of the integrated bound is quantified before $\varepsilon$ and $N$.

Reusable beyond this mission: the strong-solution predicate for jump SDEs with delay, the noise predicates for countable families of drivers, and the network and mean-field interaction terms. Contributions toward a stochastic calculus for these predicates (Itô's formula for $|X|^2$ with jumps, Gronwall arguments with left limits) are welcome.

Selected references

• S. Mehri, M. Scheutzow, W. Stannat, B. Z. Zangeneh, Propagation of chaos for stochastic spatially structured neuronal networks with delay driven by jump diffusions, Ann. Appl. Probab. 30 (2020); arXiv:1805.01654v3. https://arxiv.org/abs/1805.01654
• J. Baladron, D. Fasoli, O. Faugeras, J. Touboul, Mean-field description and propagation of chaos in networks of Hodgkin–Huxley and FitzHugh–Nagumo neurons, J. Math. Neurosci. 2:10 (2012). https://doi.org/10.1186/2190-8567-2-10
• M. Bossy, O. Faugeras, D. Talay, Clarification and complement to "Mean-field description and propagation of chaos in networks of Hodgkin–Huxley and FitzHugh–Nagumo neurons", J. Math. Neurosci. 5:19 (2015). https://doi.org/10.1186/s13408-015-0031-8
• J. Touboul, Propagation of chaos in neural fields, Ann. Appl. Probab. 24(3):1298–1328 (2014); arXiv:1108.2414. https://arxiv.org/abs/1108.2414
• J. Touboul, Spatially extended networks with singular multi-scale connectivity patterns, J. Stat. Phys. 156(3):546–573 (2014).
• C. Quiñinao, J. Touboul, Limits and dynamics of randomly connected neuronal networks, Acta Appl. Math. 136(1):167–192 (2015).
• E. Luçon, W. Stannat, Mean field limit for disordered diffusions with singular interactions, Ann. Appl. Probab. 24(5):1946–1993 (2014).
• J. Touboul, Limits and dynamics of stochastic neuronal networks with random heterogeneous delays, J. Stat. Phys. 149(4):569–597 (2012).
• L. Andreis, P. Dai Pra, M. Fischer, McKean–Vlasov limit for interacting systems with simultaneous jumps, Stoch. Anal. Appl. (2018).

Motivation

The Kolmogorov–Čentsov continuity criterion is the standard way to prove that a random field has a continuous version: a moment bound on increments, $\mathbf E|X_u - X_v|^\alpha \le c_0|u - v|^{d+\beta}$, yields a modification whose paths are Hölder continuous of every order $\gamma < \beta/\alpha$ (Karatzas–Shreve 1991, §2.2; Revuz–Yor 1999, Ch. I). It is used for Brownian motion, Brownian sheets, solutions of stochastic PDEs, Gaussian free field approximations and many other random fields.

The classical statement says only that the Hölder constant $M$ is finite almost surely. Many applications need more: a bound on the tail $\mathbf P[M \ge t]$ whose constant depends only on the parameters $\alpha, \beta, c_0$ and not on the particular field, so that the bound holds uniformly over a family of fields.

This mission formalizes such a quantitative version, Proposition 2.3 in §2.3 of J. Miller and S. Sheffield, Liouville quantum gravity and the Brownian map II: geodesics and continuity of the embedding (Ann. Probab. 2021). The authors state it, note that it follows "by carefully following the proof" of the classical criterion, and write the proof out (pp. 30–31). They apply it to the circle-average process of the Gaussian free field (Proposition 2.4, p. 33) and again in Lemma 5.12 (p. 63).

The paper's main theorems (the $\sqrt{8/3}$-Liouville quantum gravity sphere equipped with the QLE(8/3, 0) metric has the law of the Brownian map; continuity of the embedding) are not part of this mission. Their objects, among them the Gaussian free field, SLE$_6$, quantum surfaces, the QLE metric of Miller–Sheffield 2020 and the Brownian map, have no formal substrate in Mathlib or on the platform. Proposition 2.3 is a self-contained probabilistic tool that the paper proves in full, and it is statable today.

Setting

Fix a dimension $d \in \mathbb N$. The index set is the cube $[0,1]^d$ with the Euclidean distance $|u - v|$. A random field is a family $(X_u)_{u \in [0,1]^d}$ of real random variables on a probability space $(\Omega, \mathcal F, \mathbf P)$. The field satisfies the Kolmogorov condition with constants $\alpha, \beta, c_0 > 0$ if

$$\mathbf E\big[|X_u - X_v|^\alpha\big] \le c_0 |u - v|^{d+\beta} \qquad \text{for all } u, v \in [0,1]^d. \tag{2.6}$$

A modification of $X$ is a field $Y$ on the same space with $\mathbf P[Y_u = X_u] = 1$ for every $u$. For $\gamma > 0$, the $\gamma$-Hölder norm of a function $f$ on the cube is

$$M_\gamma(f) = \sup_{u \ne v} \frac{|f(u) - f(v)|}{|u - v|^\gamma} \in [0, \infty].$$

The proof works on the dyadic grid $\mathcal D_k$, the points of the cube whose coordinates are integer multiples of $2^{-k}$, and on the set $\widetilde{\mathcal D}_k$ of adjacent pairs $\{u, v\} \subseteq \mathcal D_k$, which differ in exactly one coordinate, by $2^{-k}$. In Lean the cube is Cube d, and the grid and the pairs are dyadicGrid d k and IsAdjacentPair d k u v.

Formalization targets

Goal: Proposition 2.3 (p. 30)

For every $\gamma \in (0, \beta/\alpha)$ there is a constant $c_1(\gamma) > 0$, depending only on $d, \alpha, \beta, \gamma, c_0$, such that every field satisfying (2.6) has one modification $Y$ with, for every $\gamma \in (0, \beta/\alpha)$,

$$\forall \omega\ \exists M > 0:\ |Y_u(\omega) - Y_v(\omega)| \le M|u - v|^\gamma \ \ \forall u, v, \tag{2.7}$$ $$\mathbf P\big[M_\gamma(Y(\omega)) \ge t\big] \le c_1(\gamma)\, t^{-\alpha} \qquad \text{for all } t \ge 1. \tag{2.8}$$

Milestones (attack order)

1. (2.9), p. 30: $\mathbf P[|X_u - X_v| \ge \delta] \le c_0 \delta^{-\alpha}|u - v|^{d+\beta}$.
2. (2.10), p. 31: for $\{u, v\} \in \widetilde{\mathcal D}_k$, $\mathbf P[|X_u - X_v| \ge t2^{-\gamma k}] \le c_0 t^{-\alpha} 2^{-k(d+\beta-\alpha\gamma)}$.
3. (2.11), p. 31: $\mathbf P[\max_{\widetilde{\mathcal D}_k} |X_u - X_v| \ge t2^{-\gamma k}] \le c_1 t^{-\alpha}2^{-k(\beta-\alpha\gamma)}$, with $c_1$ uniform in $k$, $t$ and the field (this $c_1$ is not the one of (2.8)).
4. (2.12), p. 31: $\mathbf P[\sup_k \max_{\widetilde{\mathcal D}_k} 2^{\gamma k}|X_u - X_v| \ge t] \le c_2 t^{-\alpha}$.
5. Closing claim of the proof, p. 31: a deterministic statement. If $2^{\gamma k}|f(u) - f(v)| \le t$ for all adjacent pairs at all levels, then $|f(u) - f(v)| \le c_3 t|u - v|^\gamma$ for all dyadic $u, v$, with $c_3$ depending on $d, \gamma$ only.
6. (2.7), p. 30: the classical criterion alone, a modification that is $\gamma$-Hölder for every $\gamma \in (0, \beta/\alpha)$.

Significance

The tail bound (2.8) is what makes the criterion usable for families of fields. In the paper, it bounds the modulus of continuity of the Gaussian free field circle averages at every scale with a single constant, which feeds the estimates on the Liouville quantum gravity metric. More generally, polynomial tails for Hölder norms with field-independent constants are the input to tightness arguments for sequences of random fields, to union bounds over many scales or many fields, and to moment bounds for Hölder norms.

The result itself is known: the authors derive it from the textbook proof, which they write out. What is missing is a machine-checked version. At the pinned Mathlib revision, ProbabilityTheory.IsKolmogorovProcess defines the hypothesis (2.6), but no continuity theorem is proved from it, qualitative or quantitative. The platform has an Open goal for the qualitative one-parameter theorem on $[0, \infty)$, KolmogorovChentsov.exists_modification_holderOnWith_Icc, a different statement that the mission does not duplicate. A proof of this mission's goal would give the classical $d$-parameter criterion on the cube (milestone 6) and its quantitative form together.

Difficulty

The probabilistic steps (2.9)–(2.12) are Markov's inequality and two union bounds. They become concrete once the adjacent pairs are counted: $|\widetilde{\mathcal D}_k|$ is of order $d\,2^{dk}$, and summing over scales needs $\gamma < \beta/\alpha$. Formalizing them requires care with suprema in $[0,\infty]$ and with outer measures of events that are not obviously measurable.

The central difficulty is the deterministic chaining claim and the passage from dyadic points to the whole cube. The paper calls the claim "not difficult to see", but its constant must be uniform over pairs of dyadic points of arbitrarily fine and unequal levels, and the obvious attempt, comparing values along the straight segment between two points, fails because the points of the segment are not dyadic, so the hypothesis says nothing about them. The second difficulty is the modification itself: one field $Y$ must serve every $\gamma < \beta/\alpha$ at once, must agree with $X$ almost surely at every point, and the tail bound for the dyadic supremum must transfer to the Hölder norm over the whole cube, an uncountable supremum whose event is not obviously measurable.

Formalization scope

• Index set: Cube d, the subtype of EuclideanSpace ℝ (Fin d) with coordinates in $[0,1]$, so $|u - v|$ is Euclidean. Because all constants are existential, the statements do not depend on the norm, but Euclidean is the default reading.
• Hypothesis (2.6): Mathlib's IsKolmogorovProcess X P α (d + β) c₀ with c₀ : ℝ≥0, plus 0 < α, 0 < β, 0 < c₀. It reads (2.6) with the lower Lebesgue integral in $[0,\infty]$, so it cannot hold through a junk value of a non-integrable expectation. It also requires each pair $(X_u, X_v)$ to be Borel measurable, which is the measurability included in "random field". The probability space is [IsProbabilityMeasure P].
• Hölder norm: $M_\gamma$ is eHolderNorm γ, valued in $[0,\infty]$. A real supremum, which is 0 on unbounded families and would make (2.8) trivially true, is ruled out. The supremum of (2.12) is likewise an ℝ≥0∞-valued ⨆, and its event is $\{t \le \sup\}$, not the weaker "some term is $\ge t$".
• Uniformity: the constants $c_1$ of (2.8) (a function of $\gamma$), $c_1$ of (2.11), $c_2$ and $c_3$ are quantified before the probability space and the field. A version in which the constant may depend on the field, or one with a different modification for each $\gamma$, is a weaker theorem and is ruled out. The probability space ranges over Type (universe 0).
• Conventions: (2.7) holds for every $\omega$ (the paper states it for the modification itself). Probabilities of events not shown measurable are outer measures. The dyadic level $k$ ranges over $\mathbb N$ including $0$. Adjacent pairs are ordered, which doubles a count that the constants absorb. The milestones add $t > 0$ and $\delta > 0$, which the paper leaves implicit, and carry $\gamma \in (0, \beta/\alpha)$ from (2.10) on. The constants may depend on $d$, which the paper's list "$\alpha, \beta, \gamma, c_0$" leaves implicit.

A complete development needs counting lemmas for the dyadic grid, a chaining lemma on dyadic points, and the extension of a uniformly Hölder function from a dense subset (Mathlib's HolderOnWith and uniform-continuity extension tools apply). The chaining lemma and the quantitative criterion are reusable for any Hölder-regularity argument on cubes. Contributions are welcome for each milestone independently and for an alternative proof of the goal through Mathlib's PairReduction chaining machinery.

Selected references

• J. Miller, S. Sheffield, Liouville quantum gravity and the Brownian map II: geodesics and continuity of the embedding, Ann. Probab., 2021 (accepted manuscript, Apollo repository, University of Cambridge). https://doi.org/10.1214/21-AOP1506
• J. Miller, S. Sheffield, Liouville quantum gravity and the Brownian map I: the QLE(8/3, 0) metric, Invent. Math. 219(1), 75–152, 2020. https://arxiv.org/abs/1507.00719
• I. Karatzas, S. E. Shreve, Brownian Motion and Stochastic Calculus, 2nd ed., Graduate Texts in Mathematics 113, Springer, 1991. https://doi.org/10.1007/978-1-4612-0949-2
• D. Revuz, M. Yor, Continuous Martingales and Brownian Motion, 3rd ed., Grundlehren der Mathematischen Wissenschaften 293, Springer, 1999. https://doi.org/10.1007/978-3-662-06400-9
• Mathlib, Mathlib/Probability/Process/Kolmogorov.lean (the predicate IsKolmogorovProcess). https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Probability/Process/Kolmogorov.lean

Motivation

Networks of conductance-based neurons, such as FitzHugh–Nagumo networks, are modelled by systems of stochastic differential equations in which each neuron interacts with the others through synapses, and the signal from one neuron reaches another only after a transmission delay. Biological neurons sit at positions in space, belong to a few distinct subpopulations, are driven by Brownian and Poisson (jump) noise, and vary from one to another; the last feature is modelled by a random disorder parameter. When the number of neurons tends to infinity, the state of a typical neuron is expected to follow a McKean–Vlasov equation: an SDE whose coefficients depend on the law of its own solution. S. Mehri, M. Scheutzow, W. Stannat and B. Z. Zangeneh (arXiv:1805.01654; Ann. Appl. Probab. 30 (2020), DOI 10.1214/19-AAP1499) prove that this limit equation is well-posed, with coefficients that are only monotone (one-sided Lipschitz), a general delay, jump noise, spatial structure and disorder all at once, and then prove propagation of chaos towards it.

Earlier work, as surveyed on p. 3 of the paper, covered parts of this setting: global Lipschitz coefficients (Quiñinao and Touboul 2015, and the paper's references [10, 11]), locally Lipschitz coefficients (Baladron, Fasoli, Faugeras and Touboul 2012, with the clarification of Bossy, Faugeras and Talay 2015 on the localization by hitting times; the same issue affects Touboul 2012), one-sided Lipschitz coefficients with diffusive noise (Luçon and Stannat 2014), and Lévy noise under global Lipschitz assumptions or gradient-type local dynamics (Andreis, Dai Pra and Fischer 2018). The paper constructs the solution by an Euler approximation, which, by the authors' account, had not been applied to McKean–Vlasov equations before.

Setting

Fix dimensions $d$ (state), $m$, $n$ (noise), $k$ (space), a delay $\tau > 0$ and $P \ge 1$ subpopulations, located at pairwise disjoint measurable regions $\Gamma_1,\dots,\Gamma_P \subset \mathbb R^k$ whose union $\Gamma$ is bounded. A finite Borel measure $\mathcal R$ on $\Gamma$ with $\mathcal R(\Gamma_\alpha) = 1$ describes the spatial distribution of neurons. A disorder probability space $(\Omega',\mathcal F',\mathbb P')$ is fixed. On a filtered probability space $(\Omega,\mathcal F,(\mathcal F_t),\mathbb P)$ there are an $m$-dimensional Brownian motion $W$, $n$-dimensional Brownian motions $B^1,\dots,B^P$, Poisson random measures $N, N^1, \dots, N^P$ on $[0,\infty)\times U$ with intensity $dt\otimes\nu$ ($\nu$ σ-finite; $\tilde N = N - dt\otimes\nu$), all independent, and initial paths $\hat z^\zeta \in L^2(\Omega;\text{Càdlàg}([-\tau,0];\mathbb R^d))$.

For a path $y$, write $y_{(t-\tau)^-:t^-}$ for the segment $u\mapsto y_{(t+u)^-}$, $u\in[-\tau,0]$. The equation is

$$dX^r_t = f(t,r,X^r_{t-},\omega')dt + g(\cdot)dW_t + \int_U h(\cdot,\xi)\tilde N(dt,d\xi) + \sum_{\alpha=1}^P\int_{\Gamma_\alpha}\tilde{\mathbb E}\big[\theta(t,r,r',X^r_{t-},\tilde X^{r'}_{(t-\tau)^-:t^-},\omega')\big]\mathcal R(dr')dt$$ $$+ \sum_{\alpha=1}^P\int_{\Gamma_\alpha}\tilde{\mathbb E}[\beta(\cdots)]\mathcal R(dr')dB^\alpha_t + \sum_{\alpha=1}^P\int_{\Gamma_\alpha}\int_U\tilde{\mathbb E}[\eta(\cdots,\xi)]\mathcal R(dr')\tilde N^\alpha(dt,d\xi),\qquad X^r_t = \hat z^\zeta_t\ (r\in\Gamma_\zeta,\ t\in[-\tau,0]), \tag{6}$$

where $\tilde X$ is an independent copy of the solution $X$ and $\tilde{\mathbb E}$ its expectation. The local dynamics $f, g, h$ satisfy the monotonicity and growth conditions (H1)–(H3) of Hypothesis 1.1 with locally integrable random rates $L_t(\omega')$, $K_t(\omega')$, $\tilde K_t(R,\omega')$; the synaptic coefficients $\theta, \beta, \eta$ are Lipschitz (H4) and of linear growth (H5) in $(x, y)$, with rates $\bar L_t(\omega')$, $\bar K_t(\omega')$, the path variable measured through a probability measure $\lambda$ on $[-\tau,0]$. In Lean, the model is the definition module NeuroMV.WellPosed.Setting: Space, Coeffs, Hyp1_1, Noise/IsNoise, IsStrongSol6, InClass and the constant C1 of (7).

Formalization targets

Goal: Theorem 1.5 (p. 7)

For every $T>0$ there is a process $X^r_t(\omega;\omega')$, measurable in $(r,\omega',\omega)$, such that for $\mathbb P'$-almost every $\omega'$, $X(\omega')$ is a strong solution of (6) on $[-\tau,T]$,

$$X(\omega') \in L^\infty\big([-\tau,T],dt;L^2(\Omega\times\Gamma,\mathbb P\otimes\mathcal R;\mathbb R^d)\big),$$

and every other strong solution $Y$ in that class satisfies $\int_\Gamma\mathbb E|X^r_t - Y^r_t|^2\mathcal R(dr) = 0$ for all $t\in[-\tau,T]$.

Milestones

1. Theorem A.2 (p. 23): well-posedness of the general path-dependent delay SDE (20) with jumps under the monotonicity Hypothesis A.1, joint measurability in $(t,\omega,\omega')$, the moment bound (22), and convergence of the Euler approximation (21).
2. The scheme (11) exists and is measurable (p. 9), and satisfies the uniform bound (12): $\sup_{t\in[-\tau,T]}\mathbb E|X^{n,r}_t|^2 \le C_1(T,\omega')$.
3. Claims (iv) and (v) (p. 10): the schemes are Cauchy in probability uniformly on $[0,T]$, and their limit solves (6).
4. Lemma 1.4 (p. 6): every solution in the class satisfies $\sup_{s\in[-\tau,t]}\mathbb E|X^r_s|^2 \le C_1(t,\omega')$.
5. Uniqueness (pp. 16–17): two solutions in the class agree in $L^2(\Omega\times\Gamma)$ at every time.

Significance

Theorem 1.5 makes the infinite-population limit of the network well defined; the second main result of the paper, Theorem 1.8, proves that the network converges to it in $L^2$. The theorem applies to coefficients that are only monotone in the state, which covers the cubic nonlinearity of FitzHugh–Nagumo neurons (Example 1.3), and to synaptic weights of conductance type driven by jump noise. Theorem A.2, proved in the appendix, is a well-posedness and Euler-convergence result for monotone stochastic delay equations with jumps and random coefficients, stated by the authors as new in this generality; it is reusable beyond this paper.

The results are proved in the paper; none of them has a machine-checked proof. The mission produces a Lean statement of the limit equation with the published Brownian and compensated Poisson integral relations, and invites formal proofs of the scheme estimates, the Cauchy property, the identification of the limit, the moment bound and uniqueness.

Difficulty

Under monotone coefficients there is no global contraction, so the Picard iteration that proves McKean–Vlasov well-posedness under Lipschitz assumptions does not apply. Localization by stopping times, the standard replacement for SDEs with monotone coefficients, does not localize the mean-field terms, which depend on the law of the solution at all positions; mishandling this step is the gap that Bossy, Faugeras and Talay pointed out in earlier work, and the acknowledgements (p. 30) record that the first version of this paper contained an unjustified application of the moment estimate of Lemma 1.4. A priori bounds must therefore be uniform in the approximation, and the limit of the mean-field stochastic integrals must be identified, with jumps and delay present. A second difficulty is measurability: the mean-field integrals require the solution to be measurable in the position $r'$, and the theorem asserts measurability in $(r,\omega')$.

Formalization scope

• Representation. Positions are EuclideanSpace ℝ (Fin k), states EthierKurtz.SDEState d, matrices Matrix (Fin d) (Fin m) ℝ with the Hilbert–Schmidt norm; subpopulations are Fin P, 0-based. Processes are indexed by ℝ on $[-\tau,T]$; drivers by ℝ≥0. Path segments are functions ℝ → ℝ^d read on $[-\tau,0]$ with the product (cylinder) σ-algebra; the paper's sup-norm Borel σ-algebra is larger, so joint measurability of the coefficients for the cylinder σ-algebra is a mild added requirement.
• Noise and integrals. Brownian integrals are the published EthierKurtz.HasBrownianItoIntegral, compensated jump integrals the published JacodTodorov10.LLN.HasCompInt, coordinatewise, with integrands cut off after $T$. All Poisson measures are one JacodTodorov10.LLN.IsFPoisson measure on a product mark space, equivalent to independent measures $N, N^\alpha$. Independence of the initial data from the drivers is encoded by $\mathcal F_0$-measurability.
• Mean field. The copy $\tilde X$ enters only through its law, so $\tilde{\mathbb E}$ is an expectation over $X$ itself; the mean-field integrands are required to be integrable on $\Gamma_\alpha\times\Omega$. Expectations and suprema are in $[0,\infty]$; Bochner integrals carry integrability clauses.
• Hypotheses. Hypothesis 1.1 (H1)–(H5) and the regularity of p. 2; (H6) is omitted from every item, because it involves the network data of (1) only and the proof never uses it. The class $L^\infty$–$L^2$ is a bound for every $t$ rather than a.e. $t$.
• Every position. The goal requires the integral identity at every $r\in\Gamma$, as (6) is posed; §2 proves it for $\mathcal R\times\mathbb P'$-a.e. $(r,\omega')$ (p. 16), and on the remaining null set of positions (6) is an ordinary delay SDE solved by Theorem A.2 — a step the paper leaves implicit. Claim (v) keeps the $\mathcal R$-a.e. reading.
• No trivialization. The stochastic integrals are the published relations tied to $W$, $B^\alpha$, $N$, $N^\alpha$, not free processes; the mean-field terms are computed from the solution's own segments; the solution class is non-empty for zero coefficients (a sorry-free check accompanies the mission); and the scheme and limit are the paper's, not new processes with their own noise.
• Not stated. Claims (i)–(iii) of §2 (the remainder estimate and the a priori bounds before the stopping time) are not separate items.
• Welcome contributions. Itô's formula for jump diffusions in this encoding, Gronwall-type lemmas in $[0,\infty]$, stability of the published integral relations under convergence in probability, and the monotone delay SDE theory of Appendix A are all reusable beyond this mission.

Selected references

• S. Mehri, M. Scheutzow, W. Stannat, B. Z. Zangeneh, Propagation of Chaos for Stochastic Spatially Structured Neuronal Networks with Delay driven by Jump Diffusions, arXiv:1805.01654v3, 2019; Ann. Appl. Probab. 30, 2020. https://arxiv.org/abs/1805.01654, https://doi.org/10.1214/19-AAP1499
• J. Baladron, D. Fasoli, O. Faugeras, J. Touboul, Mean-field description and propagation of chaos in networks of Hodgkin–Huxley and FitzHugh–Nagumo neurons, J. Math. Neurosci. 2:10, 2012.
• M. Bossy, O. Faugeras, D. Talay, Clarification and complement to "Mean-field description and propagation of chaos in networks of Hodgkin–Huxley and FitzHugh–Nagumo neurons", J. Math. Neurosci. 5:19, 2015.
• E. Luçon, W. Stannat, Mean field limit for disordered diffusions with singular interactions, Ann. Appl. Probab. 24(5):1946–1993, 2014.
• C. Quiñinao, J. Touboul, Limits and dynamics of randomly connected neuronal networks, Acta Appl. Math. 136(1):167–192, 2015.
• J. Touboul, Limits and dynamics of stochastic neuronal networks with random heterogeneous delays, J. Stat. Phys. 149(4):569–597, 2012.
• L. Andreis, P. Dai Pra, M. Fischer, McKean–Vlasov limit for interacting systems with simultaneous jumps, Stoch. Anal. Appl., 2018.
• W. Liu, M. Röckner, Stochastic Partial Differential Equations: An Introduction, Universitext, Springer, 2015.

The bibliographic data of the last seven entries are taken from the reference list of the paper (pp. 30–31).

Motivation

Mean-field games describe large populations of identical agents who interact only through the distribution of their states. Each agent solves a stochastic control problem in which the population appears through a deterministic flow of distributions, and an equilibrium requires that this flow coincide with the distribution the agents generate themselves. The theory goes back to Huang, Malhamé and Caines (2006) and Lasry and Lions (2007) in continuous time. In discrete time, Saldi, Başar and Raginsky (SIAM J. Control Optim. 2018) proved existence of equilibria for risk-neutral agents with discounted costs on Polish state spaces.

Risk-neutral agents care only about expected cost. Many applications in engineering and finance call for agents that also penalize the variability of their cost. A standard way to model this is the exponential (risk-sensitive) criterion $E[\exp(\lambda\cdot\text{cost})]$ with risk factor $\lambda>0$. Its theory for single-agent Markov decision processes goes back to Howard and Matheson (1972) and Jacobson (1973), and Bäuerle and Rieder (Math. Oper. Res. 2014) treat general utilities. Saldi, Başar and Raginsky (arXiv:1808.03929, Math. Oper. Res. 2020) carry the discrete-time mean-field program over to this criterion. This mission covers its first main result: existence of a mean-field equilibrium (Theorem 1).

Setting

The state space $\mathsf X$ and the action space $\mathsf A$ are Polish, and $\mathsf A$ is compact. $\mathcal P(E)$ denotes the probability measures on $E$, with the topology of weak convergence and its Borel σ-field. The model consists of:

• a stochastic kernel $p(\cdot\,|\,x,a,\mu)$ on $\mathsf X$ given $\mathsf X\times\mathsf A\times\mathcal P(\mathsf X)$;
• a one-stage cost $c(x,a,\mu)\in[0,K]$;
• an initial law $\mu_0$, a discount factor $\beta\in(0,1)$ and a risk factor $\lambda>0$.

A Markov policy is a sequence $\pi=(\pi_t)_{t\ge0}$ of kernels $\pi_t(da\,|\,x)$. A policy in general is allowed to depend on the whole history $(x(0),a(0),\dots,x(t))$. Given a measure flow $\mu=(\mu_t)_{t\ge0}\subset\mathcal P(\mathsf X)$, a generic agent evolves as

$$x(0)\sim\mu_0,\qquad a(t)\sim\pi_t(\cdot\,|\,\text{history}),\qquad x(t+1)\sim p(\cdot\,|\,x(t),a(t),\mu_t),$$

and pays the risk-sensitive cost

$$J_\mu(\pi)=E^\pi\Big[\exp\Big(\lambda\sum_{t=0}^\infty\beta^tc(x(t),a(t),\mu_t)\Big)\Big].$$

For a Markov policy, $\Lambda(\pi)$ is the flow of state laws it generates: it starts at $\mu_0$ and satisfies $\mu_{t+1}(\cdot)=\int p(\cdot\,|\,x,a,\mu_t)\,\pi_t(da|x)\,\mu_t(dx)$. A pair $(\pi,\mu)$ is a mean-field equilibrium if $\mu=\Lambda(\pi)$ and $\pi$ minimizes $J_\mu$ over all policies.

Assumption 1 asks for the following:

• (a) $c$ is continuous with $\|c\|\le K$;
• (b) $p$ is weakly continuous in $(x,a,\mu)$;
• (c) $\mathsf A$ is compact;
• (d) there are $\alpha\ge0$ and a continuous moment function $w\ge1$ (compact sets $K_n\uparrow\mathsf X$ with $\inf_{x\notin K_n}w(x)\to\infty$) with $\int w(y)\,p(dy|x,a,\mu)\le\alpha w(x)$;
• (e) $\int w\,d\mu_0<\infty$.

Formalization targets

Goal: Theorem 1 (p. 10)

Under Assumption 1 there are a Markov policy $\pi$ and a flow $\mu$ with

$$\mu=\Lambda(\pi)\qquad\text{and}\qquad J_\mu(\pi)=\inf_{\sigma\in\Pi}J_\mu(\sigma).$$

Milestones

In the paper's order of proof:

1. Proposition 1: Markov policies achieve the optimal value.
2. Lemmas 1–3: the finite- and infinite-horizon optimal value functions $J^n_k(\cdot,\lambda\beta^k)$ and $J_k(\cdot,\lambda\beta^k)$ of the nonhomogeneous MDP of a fixed flow are bounded and continuous. They satisfy the dynamic programming equation $T_kJ_{k+1}(\cdot,\lambda\beta^{k+1})=J_k(\cdot,\lambda\beta^k)$, and

$$\big\|J^n_k(\cdot,\lambda\beta^k)-J_k(\cdot,\lambda\beta^k)\big\|\le\frac{\lambda K}{1-\beta}e^{\frac{\lambda\beta^kK}{1-\beta}}\beta^{n+1}.$$

3. Theorem 2: a Markov policy is optimal if and only if it almost surely selects minimizers in the dynamic programming equation.
4. Propositions 2–5 and Lemma 4: equilibria are fixed points of a set-valued map $\Gamma$ on state–action flows in $\Xi=\prod_t\{\nu:\nu_1(w)\le\alpha^tM\}$; the optimal value functions depend continuously on the flow; and the graph of $\Gamma$ is closed in $\Xi\times\Xi$.

Significance

The result. Theorem 1 is what makes the second main result of the paper meaningful. That result, Theorem 3 and the second mission of this series, states that the equilibrium policy is an $\varepsilon$-Markov–Nash equilibrium of every $N$-agent game with $N$ large enough. Equilibria of finite risk-sensitive games with many agents are rarely computable, so a mean-field equilibrium gives an approximately optimal decentralized policy that ignores the other agents' states. Along the way, the paper proves results on nonhomogeneous risk-sensitive MDPs that it describes as "mostly absent and dispersed in the literature": uniform finite-to-infinite horizon bounds and a characterization of optimal Markov policies. These results are useful outside game theory.

Formalizing it. The result is proved on paper. No part of it, nor of the risk-neutral precursor, has a machine-checked proof. Formalization produces a verified theory of nonhomogeneous risk-sensitive MDPs on Polish spaces, a verified closed-graph argument for the mean-field map, and an exact record of the hypotheses. The paper omits or cites several steps: Proposition 1, Proposition 2, Lemma 2, the conditional optimality (8) and the nonemptiness and convexity of $\Gamma(\nu)$. A formalization has to supply them.

Difficulty

The obvious route is Banach's fixed point theorem for the dynamic programming operator, as in risk-neutral discounted MDPs. It fails here: the cost is multiplicative, and the operator $T_k$ is not a contraction. Uniform convergence of value iteration has to come from the explicit tail bound of Lemma 3 instead.

The second obstacle is the fixed point itself. The natural map, from a flow to the flows of its optimal policies, is set-valued and lives on an infinite product of spaces of measures. Kakutani–Fan–Glicksberg applies only after three steps:

• re-encoding the problem on state–action flows (the map $\Gamma=C\cap B$);
• proving compactness of $\Xi$ through the moment function (tightness);
• proving that the graph of $\Gamma$ is closed (Proposition 4).

The last step requires the optimal value functions to vary continuously with the flow (Proposition 5) and a portmanteau argument for sets defined by optimality conditions. None of this machinery (the Kakutani–Fan–Glicksberg theorem in locally convex spaces, Prokhorov compactness via moment functions, continuous convergence) is in Mathlib in the required form.

Formalization scope

$\mathcal P(E)$ is a type synonym of Mathlib's ProbabilityMeasure E with the weak topology and its Borel σ-field. The kernel $p$ is a Mathlib Kernel on $\mathsf X\times\mathsf A\times\mathcal P(\mathsf X)$. Policies are sequences of Markov kernels, and history-dependent policies take $(\mathsf X\times\mathsf A)^t\times\mathsf X$ as input. The law $P^\pi$ is built with the Ionescu–Tulcea kernel Kernel.trajMeasure, one coordinate $(x(t),a(t))$ per time step. Time is $0$-based.

Standing hypotheses on every statement:

• $\mathsf X$ and $\mathsf A$ are Polish and Borel;
• $\mathsf A$ is compact and nonempty (used tacitly by the paper);
• $\beta\in(0,1)$, $\lambda>0$, and $c\ge0$ is measurable;
• Assumption 1.

For §4.2 the pair $(\alpha,w)$ defining $\Xi$ is an explicit argument. In §4.1, "policy" means Markov policy, as the paper states on p. 11. The conditional expectations "given $x(k)=x$" are expectations for the chain started at time $k$ in $x$. Lemma 1 is stated with $\zeta_{k,n}=\sum_{t=k}^n\beta^t$, the quantity its proof uses; the page prints $\sum_{t=k}^n\beta^k$.

The goal asks for a Markov equilibrium policy that is optimal against all history-dependent policies, at least as strong as Definition 3. Optimality is "$\le$ the cost of every policy", not an infimum, so it has no junk case. The cost is a genuine integral: with $c\ge0$ bounded, the integrand lies in $[1,e^{\lambda K/(1-\beta)}]$, so no policy is trivially optimal. The moment-function predicate has no infimum, so compact $\mathsf X$ is admitted.

Contributions are welcome at every level:

• risk-sensitive dynamic programming on Borel spaces (reusable for any MDP);
• the Kakutani–Fan–Glicksberg theorem in locally convex spaces;
• Prokhorov compactness from moment functions;
• measurable selection and disintegration of state–action measures.

Selected references

• N. Saldi, T. Başar, M. Raginsky, Discrete-time Risk-sensitive Mean-field Games, arXiv:1808.03929v2, 2018; published as Approximate Markov-Nash Equilibria for Discrete-Time Risk-Sensitive Mean-Field Games, Math. Oper. Res. 45(4), 2020. https://arxiv.org/abs/1808.03929
• N. Saldi, T. Başar, M. Raginsky, Markov–Nash Equilibria in Mean-Field Games with Discounted Cost, SIAM J. Control Optim. 56(6), 2018. https://doi.org/10.1137/17M1112583
• N. Bäuerle, U. Rieder, More Risk-Sensitive Markov Decision Processes, Math. Oper. Res. 39(1), 2014. https://doi.org/10.1287/moor.2013.0601
• O. Hernández-Lerma, J. B. Lasserre, Discrete-Time Markov Control Processes: Basic Optimality Criteria, Springer, 1996. https://doi.org/10.1007/978-1-4612-0729-0
• C. D. Aliprantis, K. C. Border, Infinite Dimensional Analysis, 3rd ed., Springer, 2006. https://doi.org/10.1007/3-540-29587-9

Motivation

Mean field games describe large populations of agents who interact symmetrically: every agent sees the same average of all the others. Many populations interact instead along a network, where each agent responds only to its neighbours. Lacker and Soret (arXiv:2005.14102v2, 2021; Math. Oper. Res. 2022) study a linear-quadratic stochastic differential game on a finite graph that is simple enough to solve explicitly on every vertex-transitive graph, and then ask what happens to the equilibrium as the graph grows. The question is the network analogue of the classical convergence problem for mean field games: does the $n$-player equilibrium have a limit, and does that limit depend on the graph only through a small amount of information?

The answer of the paper is that the limit is governed by the empirical eigenvalue distribution of the graph Laplacian. Dense graph sequences (degrees tending to infinity) all have the same limit, the mean field game; sparse ones (bounded degrees) have limits that depend on the graph, through its spectrum. This mission formalizes that large-graph limit theorem, Theorem 2.6 of the paper. Mission I of the series formalizes the explicit equilibrium on a fixed transitive graph (Theorem 2.5), on which this mission builds.

Setting

Let $G$ be a finite simple graph on vertex set $\{1,\dots,n\}$ with adjacency matrix $A_G$ and degree matrix $D_G$. Its Laplacian is $L_G = D_G^{-1}A_G - I$. $G$ is transitive if every vertex can be mapped to every other one by a graph automorphism; such a graph is regular, of degree $\delta(G)$, and $L_G$ is then symmetric with eigenvalues $\lambda^G_1,\dots,\lambda^G_n\in[-2,0]$. The empirical eigenvalue distribution is $\mu_G = \frac1n\sum_i\delta_{\lambda^G_i}$.

Fix a horizon $T>0$, a volatility $\sigma>0$ and a weight $c>0$. Player $v$ controls the state

$$dX_v(t) = \alpha_v(t,\boldsymbol X(t))\,dt + \sigma\,dW_v(t),\qquad t\in[0,T],$$

driven by independent Brownian motions, with Markovian feedback controls $\alpha_v$, and pays

$$J_v = \tfrac12\,\mathbb E\Big[\int_0^T|\alpha_v(t,\boldsymbol X(t))|^2dt + c\,\Big|X_v(T) - \tfrac1{\deg(v)}\sum_{u\sim v}X_u(T)\Big|^2\Big].$$

On a transitive graph without isolated vertices, Theorem 2.5 gives an explicit Nash equilibrium: with $Q_G(x) = \det(I - xL_G)^{1/n}$ and $f_G$ the solution of $f_G' = c\,Q_G'(f_G)$, $f_G(0) = 0$ on $[0,T]$, the feedback is $\alpha^G_i(t,\boldsymbol x) = -e_i^\top P_G(t)\boldsymbol x$ with $P_G(t) = -f_G'(T-t)L_G(I - f_G(T-t)L_G)^{-1}$. The resulting equilibrium state process $\boldsymbol X^G$ is Gaussian, and the value is $\mathrm{Val}(G) = \frac1n\sum_v J_v$.

For a probability measure $\mu$ define $Q_\mu(x) = \exp\int_{[-2,0]}\log(1-x\lambda)\,\mu(d\lambda)$, so that $Q_{\mu_G} = Q_G$.

Formalization targets

Goal: Theorem 2.6

Let $(G_n)$ be finite transitive graphs without isolated vertices, $|G_n|\to\infty$, with $\boldsymbol X^{G_n}(0) = 0$, and suppose $\mu_{G_n}\to\mu$ weakly for a probability measure $\mu$. Then (1) the ODE $f_\mu' = c\,Q_\mu'(f_\mu)$, $f_\mu(0) = 0$ has a unique solution on $[0,T]$; (2) for every vertex sequence $k_n$ and $t\in[0,T]$,

$$\mathrm{Law}\big(X^{G_n}_{k_n}(t)\big)\to\mathcal N\big(0,V_\mu(t)\big),\qquad V_\mu(t) = \sigma^2\int_0^t\int_{[-2,0]}\Big(\frac{1-\lambda f_\mu(T-t)}{1-\lambda f_\mu(T-s)}\Big)^2\mu(d\lambda)\,ds;$$

(3) the empirical measure $\frac1{|G_n|}\sum_i\delta_{X^{G_n}_i(t)}$ converges weakly in probability to $\mathcal N(0,V_\mu(t))$; (4)

$$\lim_{n\to\infty}\mathrm{Val}(G_n) = -\frac{\sigma^2}2\log\int_{[-2,0]}\frac{-\lambda}{1-\lambda f_\mu(T)}\,\mu(d\lambda).$$

Milestones

The milestones are the statements the paper's proof (§3, §6, §7.1) relies on: the stability of $f_\mu$ in $\mu$ (Proposition 3.2, last sentence); the finite-graph variance formula (2.7); monotonicity and concavity of $f_\mu$ (Proposition 3.3, first sentence); correlation decay (Proposition 2.12) for distinct vertices; the relation between degrees and the spectral limit (Lemma 7.1); the Gaussian Poincaré bound (7.3) and the concentration (7.1) of the empirical measure; and the spectral form (2.9) of the value.

Significance

Theorem 2.6 reduces the large-population behaviour of a network game to one spectral object. For complete graphs $\mu = \delta_{-1}$ and the limit is the mean field game; for sparse sequences such as cycles, tori, or random regular graphs, $\mu$ is a non-degenerate measure and the limiting variance and value differ from the mean field ones. The theorem thereby gives a quantitative criterion for when a mean field approximation of a network game is accurate, and it shows propagation of chaos in both regimes: in the dense case because interactions are weak, in the sparse case because typical players are far apart in the graph.

The result is proved in the paper; none of it has been machine-checked. A complete formalization requires a Lean account of Gaussian laws of linear SDEs with additive noise, of weak convergence of spectral measures of graph Laplacians, and of a Gaussian Poincaré inequality, none of which is currently in Mathlib in the needed form. Each of these is reusable well beyond this mission.

Difficulty

Parts (2) and (4) follow from the finite-graph formulas once $f_{G_n}\to f_\mu$ uniformly, but that convergence requires stability of a nonlinear ODE whose vector field is defined through the spectral measure, uniformly over a class of measures. The harder step is (3). Convergence of one player's law does not imply convergence of the empirical measure: the players are correlated, and on sparse graphs every player has a bounded number of strong neighbours, so the correlations do not vanish uniformly. Bounding them requires an estimate that decays in the graph distance and in the degree, and combining it with the growth of graph balls, which is controlled differently in the dense and in the sparse regime. The usual mean field route is closed: unless the graph is complete, the state vector is not exchangeable, so propagation-of-chaos arguments based on exchangeability do not apply.

Formalization scope

The Lean development lives in namespace GraphLQGame.Asymptotics.

• Vertices $\{1,\dots,n\}$ are Fin n; a graph sequence is G : ∀ k, SimpleGraph (Fin (N k)) with $N_k\to\infty$.
• $L_G$ is the random-walk Laplacian above, not Mathlib's lapMatrix. $\mu_G$ is built from the real roots of the characteristic polynomial of $L_G$, with multiplicity.
• Weak convergence of measures on $\mathbb R$ is convergence of $\int h\,d\mu_k$ for every bounded continuous $h$. Weak convergence in probability of the empirical measure is convergence in probability of $\int h\,dm^{G_n}(t)$ for every bounded continuous $h$.
• A state process is a pathwise strong solution of (2.1) on its own probability space, driven by a standard Brownian motion and adapted to its completed filtration. Statements about several graphs are statements about laws.
• Costs are $[0,\infty]$-valued lower integrals; the value is computed after asserting finiteness.
• In $P_G$, $f_G'(T-t)$ is written as its ODE value $c\,Q_G'(f_G(T-t))$. ODE solutions are constrained on $[0,T]$ (or on $\mathbb R_+$ for Propositions 3.2 and 3.3), with uniqueness stated on that domain.
• The Gaussian law $\mathcal N(0,V)$ is gaussianReal 0 V.toNNReal; $V_\mu(t)\ge0$.

The goal quantifies over every solution $f_{G_n}$, $f_\mu$ and every equilibrium state process, and also asserts that the graph ODE solutions and the state processes exist, so it cannot be discharged vacuously. Proposition 2.12 is stated for distinct vertices: as printed, (2.17) is also claimed for $u = v$, where it fails on complete graphs of large degree; the off-diagonal case is the one the proof of Theorem 2.6 uses. Theorem 2.5 (mission I) is not restated here; a solver proves what is needed of it.

Contributions are welcome at every level: Gaussian laws of linear SDEs, spectral measures of graph matrices, ODE stability, a Gaussian Poincaré inequality, and the milestones themselves.

Selected references

• D. Lacker, A. Soret, A case study on stochastic games on large graphs in mean field and sparse regimes, arXiv:2005.14102v2, 2021; published in Math. Oper. Res., 2022, https://doi.org/10.1287/moor.2021.1179. https://arxiv.org/abs/2005.14102
• F. Chung, Spectral Graph Theory, CBMS Regional Conference Series in Mathematics 92, AMS, 1997. https://doi.org/10.1090/cbms/092
• S. Boucheron, G. Lugosi, P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013 (Theorem 3.20, Gaussian Poincaré inequality). https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
• 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

Why mean field approximations on graphs need a threshold

Mean field games (MFGs) describe the limit of symmetric stochastic differential games as the number of players tends to infinity, when every player interacts with the empirical distribution of all the others. Their main practical use is the converse direction: an equilibrium of the limiting game supplies a simple, decentralized control that is an approximate Nash equilibrium of the game with finitely many players. For the complete graph, where everybody interacts with everybody, this is classical, with the standard rate $O(1/\sqrt n)$ (Carmona and Delarue, Probabilistic Theory of Mean Field Games, Vol. II, §6.1; Huang, Malhamé and Caines 2006, Theorem 12), as recalled on p. 10 of the paper.

Many interacting systems are not complete graphs: players see only their neighbours in a network. The question is then how dense the network must be for the mean field approximation to remain valid. Lacker and Soret (arXiv:2005.14102v2) answer it exactly for a linear-quadratic "flocking" game, where explicit computations are possible. This mission formalizes their Theorem 2.11, which applies to every finite graph, with no transitivity or regularity assumed.

Setting

Let $G$ be a finite simple graph on the vertex set $V=\{1,\dots,n\}$; $u\sim v$ means $u$ and $v$ are adjacent and $\deg_G(v)$ is the number of neighbours of $v$. Fix a horizon $T>0$, a volatility $\sigma>0$ and a cost weight $c>0$. Each player $v\in V$ controls a real state $X_v$ through

$$dX_v(t)=\alpha_v(t,\boldsymbol X(t))\,dt+\sigma\,dW_v(t),\qquad t\in[0,T],$$

where $W_1,\dots,W_n$ are independent standard Brownian motions and $\boldsymbol X=(X_u)_{u\in V}$. A Markovian control $\alpha_v\in\mathcal A_G$ is a Borel function of time and the full state $\boldsymbol X(t)\in\mathbb R^V$, of linear growth. The cost of player $v$ under a profile $\boldsymbol\alpha=(\alpha_u)_{u\in V}$ is

$$J_v(\boldsymbol\alpha)=\frac12\,\mathbb E\Big[\int_0^T|\alpha_v(t,\boldsymbol X(t))|^2\,dt+c\,\Big|X_v(T)-\frac1{\deg_G(v)}\sum_{u\sim v}X_u(T)\Big|^2\Big],$$

and $\frac12\mathbb E[\int_0^T|\alpha_v|^2dt+c|X_v(T)|^2]$ for an isolated vertex: each player wants to end near the average of its neighbours at minimal quadratic effort. For a vector $\boldsymbol\varepsilon\in\mathbb R^V_+$, a profile is a Markovian $\boldsymbol\varepsilon$-Nash equilibrium if no player $v$ can lower its cost by more than $\varepsilon_v$ by switching unilaterally to another control $\beta\in\mathcal A_G$, written $(\beta,\boldsymbol\alpha^{-v})$.

The mean-field control is

$$\alpha^{\mathrm{MF}}(t,y)=\frac{-cy}{1+c(T-t)},\qquad \alpha^{\mathrm{MF}}_v(t,\boldsymbol x)=\alpha^{\mathrm{MF}}(t,x_v):$$

each player looks only at its own state, as if its neighbours' average were frozen at its mean.

Formalization targets

Goal: Theorem 2.11

Define $\epsilon^G_v=\sigma^2\frac{cT}{1+cT}\sqrt{\frac{cT(2+cT)}{\deg_G(v)}}$ if $\deg_G(v)\ge1$ and $\epsilon^G_v=0$ if $\deg_G(v)=0$, and with the minimal degree $\delta(G)=\min_v\deg_G(v)$,

$$\epsilon_G=\sigma^2\frac{cT}{1+cT}\sqrt{\frac{cT(2+cT)}{1\vee\delta(G)}}.$$

Then, with zero initial states, the state equation for $(\alpha^{\mathrm{MF}}_v)_{v\in V}$ has a solution, and

$$(\alpha^{\mathrm{MF}}_v)_{v\in V}\ \text{is an } \epsilon^G\text{-Nash equilibrium and an } \epsilon_G\text{-Nash equilibrium on } G.$$

Milestones

1. Lemma 7.2: $\alpha^{\mathrm{MF}}$ is optimal for the one-player problem $\min\frac12\mathbb E[\int_0^T\beta^2dt+c|Y(T)|^2]$, $dY=\beta\,dt+\sigma dW$, over all progressively measurable $\beta$.
2. Isolated vertices (p. 40): $J_v(\boldsymbol\alpha)=\inf_\beta J_v(\beta,\boldsymbol\alpha^{-v})$ when $\deg_G(v)=0$.
3. (7.7): under $\alpha^{\mathrm{MF}}$, $(X_u(T))_u$ are i.i.d. $N(0,\sigma^2T/(1+cT))$, so the neighbour average has second moment $\sigma^2T/(\deg_G(v)(1+cT))$.
4. Steps (1), (2), (3) (p. 41): a lower bound on $J_v(\beta,\boldsymbol\alpha^{-v})$, an energy bound for deviations no worse than the zero control, and the comparison with $J_v(\boldsymbol\alpha^{\mathrm{MF}})$.
5. (7.5): for $\deg_G(v)\ge1$ and every admissible $\beta$, $J_v(\beta,\boldsymbol\alpha^{-v})\ge J_v(\boldsymbol\alpha)-\epsilon^G_v$.

Significance

The result. Theorem 2.11 gives an explicit threshold for the mean field approximation on networks: along any sequence of graphs whose minimal degree diverges, the decentralized control $\alpha^{\mathrm{MF}}$ is an $\epsilon_{G_n}$-Nash equilibrium with $\epsilon_{G_n}\to0$, and the vector form says more: if the average of $(1\vee\deg_{G_n}(v))^{-1/2}$ over vertices tends to zero, the per-player errors vanish on average (the paper's (2.16)). The rate $\deg_G(v)^{-1/2}$ quantifies how the accuracy of the approximation depends on denseness. In the same paper, transitive graphs whose degrees stay bounded lead to equilibria that do not agree with the mean field one, so a denseness condition cannot be dropped.

Formalizing it. The theorem is proved in the paper; to our knowledge no part of it is machine-checked. A formal development needs, beyond the statement, a verification argument for a one-dimensional linear-quadratic control problem with additive noise, Gaussian computations for linear SDEs driven by Brownian motion, and the comparison of costs between the equilibrium system and a system with one deviating player. The one-player result (Lemma 7.2) and the Gaussian facts of (7.7) are reusable well beyond this mission.

Difficulty

The obvious argument compares a deviating player with an isolated player and treats the neighbour average as noise independent of the deviation. Two things stand in the way. The cost of player $v$ couples its terminal state with the neighbours' average through a cross term $\mathbb E[\frac1{\deg_G(v)}\sum_{u\sim v}X_u(T)\,Y_v(T)]$, and the deviation $\beta(t,\boldsymbol Y(t))$ may look at the neighbours' states, so the cross term does not vanish; it has to be bounded through the size of the deviation's energy. And an arbitrary deviation has no a priori energy bound: one is available only for deviations that do at least as well as the zero control, which is why the argument passes through a (near-)optimal deviation. Lemma 7.2 itself requires a verification theorem over all progressively measurable controls, not only feedback ones.

Formalization scope

The Lean development lives in the namespace GraphLQGame.DenseApprox and uses the shared encoding of this series:

• vertices are Fin n (the paper's $\{1,\dots,n\}$ become $\{0,\dots,n-1\}$), the state space is EthierKurtz.SDEState n, and $G$ is any SimpleGraph (Fin n); isolated vertices are allowed;
• controls are Borel with linear growth on $[0,T]$ only; their values at other times are never used, and the formula for $\alpha^{\mathrm{MF}}$ outside $[0,T]$ is evaluated with Lean's total division;
• a solution of the state equation is a pathwise strong solution carrying its own probability space and an $n$-dimensional standard Brownian motion; costs are $[0,\infty]$-valued lower Lebesgue integrals, and the Nash inequality is required for every solution of the profile and of each deviation (faithful by strong uniqueness);
• $T,\sigma,c>0$ are the standing assumptions of §2.1;
• initial states are zero. The printed theorem does not mention $X(0)$; the paper fixes non-random initial states that are "in many cases" zero, and the whole proof is for $X(0)=0$. With non-zero initial states the claim fails in general, so this is a disclosed hypothesis;
• the goal also asserts that the state equation for $\alpha^{\mathrm{MF}}$ has a solution, so the Nash property cannot hold vacuously; Lemma 7.2 is stated over every continuous adapted solution of its SDE, and Step (2) carries, as an explicit hypothesis, the comparison with the zero control that its proof uses.

A formalization in which $\alpha^{\mathrm{MF}}$ is compared only with deviations depending on the player's own state, or in which the costs are Bochner integrals that vanish when not integrable, would be trivially or wrongly satisfied; both are ruled out by the encoding above.

Welcome contributions: the verification argument for Lemma 7.2, the Gaussian law of linear SDEs with additive noise, and proofs of the three steps. Related missions in this series: I (an explicit Nash equilibrium on transitive graphs) and II (large-graph limits).

Selected references

• D. Lacker, A. Soret, A case study on stochastic games on large graphs in mean field and sparse regimes, arXiv:2005.14102v2, 2021; Math. Oper. Res. 47 (2022). https://arxiv.org/abs/2005.14102
• R. Carmona, F. Delarue, Probabilistic Theory of Mean Field Games with Applications II, Springer, 2018. https://doi.org/10.1007/978-3-319-56436-4
• M. Huang, R. P. Malhamé, P. E. Caines, Large population stochastic dynamic games: closed-loop McKean–Vlasov systems and the Nash certainty equivalence principle, Commun. Inf. Syst. 6 (2006), 221–252. https://doi.org/10.4310/CIS.2006.v6.n3.a5
• H. Pham, Continuous-time Stochastic Control and Optimization with Financial Applications, Springer, 2009 (verification theorem, Theorem 3.5.2). https://doi.org/10.1007/978-3-540-89500-8

Motivation

Mean field games describe Nash equilibria of large populations in which every player interacts with every other player symmetrically, through the empirical distribution of all states. Many systems of interest are not of this kind: agents in a network interact only with their neighbours, and the interaction structure is a graph rather than a complete graph. Understanding when equilibria on large graphs behave like mean field equilibria, and when they do not, requires models in which the equilibrium on a finite graph can be computed exactly.

Lacker and Soret (arXiv:2005.14102v2, Math. Oper. Res. 2022) introduced such a model: a linear–quadratic flocking game on an arbitrary finite graph, in which each player steers a Brownian particle and pays a terminal penalty for being far from the average of her neighbours. For vertex-transitive graphs they solved the game in closed form, up to a scalar ODE, with an equilibrium that depends on the graph only through the spectrum of its Laplacian. This mission formalizes that finite-graph result, Theorem 2.5 of the paper. Its large-graph consequences are the subject of missions II and III of this series.

Setting

Let $G$ be a finite simple graph on vertices $V=\{1,\dots,n\}$, with adjacency matrix $A_G$ and degree matrix $D_G$. When $G$ has no isolated vertices its random-walk Laplacian is

$$L_G := D_G^{-1}A_G - I .$$

$G$ is transitive if for every two vertices $u,v$ there is a graph automorphism mapping $u$ to $v$. A transitive graph is regular, so its Laplacian $L_G = A_G/\delta(G) - I$ is symmetric, with eigenvalues in $[-2,0]$.

Fix a horizon $T>0$, a noise level $\sigma>0$ and a cost constant $c>0$. Each vertex $v$ is a player with state

$$dX_v(t) = \alpha_v(t,X(t))\,dt + \sigma\,dW_v(t),\qquad t\in[0,T],$$

driven by independent Brownian motions $W_v$, from a non-random initial state $X(0)=x_0\in\mathbb R^V$. A Markovian control $\alpha_v$ is a Borel function of time and the full state vector with at most linear growth. Player $v$ minimises

$$J_v = \tfrac12\,\mathbb E\Big[\int_0^T|\alpha_v(t,X(t))|^2\,dt + c\,\Big|X_v(T)-\frac{1}{\deg(v)}\sum_{u\sim v}X_u(T)\Big|^2\Big].$$

A profile $(\alpha_v)_v$ is a Markovian Nash equilibrium if no player can lower her cost by switching unilaterally to another Markovian control.

The equilibrium is built from

$$Q_G(x) := \det(I-xL_G)^{1/n},\qquad f_G'(t) = c\,Q_G'(f_G(t)),\ f_G(0)=0,$$ $$P_G(t) := -f_G'(T-t)\,L_G\big(I-f_G(T-t)L_G\big)^{-1},\qquad \alpha^G_i(t,x) := -e_i^\top P_G(t)x .$$

Formalization targets

Goal: Theorem 2.5

For a finite transitive graph $G$ without isolated vertices:

1. $Q_G$ is well defined and continuously differentiable on $\mathbb R_+$, and the ODE has a unique solution $f_G:[0,T]\to\mathbb R_+$.
2. $(\alpha^G_i)_i$ is a Markovian Nash equilibrium for every initial state.
3. For every $t\in(0,T]$, the equilibrium state $X(t)$ is Gaussian with

$$\mathbb E X(t) = (I-f_G(T-t)L_G)(I-f_G(T)L_G)^{-1}x_0,\qquad \mathrm{Cov}\,X(t) = \sigma^2(I-f_G(T-t)L_G)^2\int_0^t(I-f_G(T-s)L_G)^{-2}\,ds .$$

4. The average equilibrium cost satisfies

$$\frac1n\sum_{v}J_v = \frac{|P_G(0)x_0|^2}{2\,\mathrm{Tr}\,P_G(0)} - \frac{\sigma^2}{2}\log\frac{\mathrm{Tr}\,P_G(0)}{n\,f_G'(T)} .$$

All four parts are in the goal statement.

Milestones

The milestones follow the paper's proof in §2.2, §3 and §4.

• Graph-spectral facts. Transitive graphs are regular with symmetric $L_G$ (§2.2). The spectrum of $L_G$ lies in $[-2,0]$ (Remark 2.4). The eigenvalue distribution $\mu_G$ has mean $-1$ ((3.2)), and $Q_G = Q_{\mu_G}$ (§2.3).
• The ODE. Bounds on $Q_\mu$ and its first two derivatives (Proposition 3.1), and well-posedness of $f_\mu' = cQ_\mu'(f_\mu)$ with explicit bounds (Proposition 3.2).
• Symmetry. Commutation of $L_G$ with automorphism matrices, and constancy of the diagonal of equivariant matrices (Lemma 4.1).
• The Riccati system. The properties of $P_G(t)$ (§4.4 (i)–(iii)), the reduction of the Nash PDE system to matrix Riccati equations (Lemma 4.2), and the verification that the explicit $F^i = (\mathrm{Tr}\,P/n)^{-1}Pe_ie_i^\top P$ solve them (§4.4).
• Law and value. The fundamental matrix $\exp(-\int_s^tP) = (I-f(T-t)L)(I-f(T-s)L)^{-1}$ (§4.5) and the averaged value identity (§4.6).

Significance

The result. Theorem 2.5 is one of the few explicit Nash equilibria of a stochastic differential game on a non-complete graph. Two features of it are not visible in mean field theory. The equilibrium controls are nonlocal: each player reacts to the whole state vector, not only to her neighbours. The whole equilibrium (law, value, controls) depends on the graph only through the spectrum of $L_G$. The second feature drives the paper's later results. Weak convergence of the eigenvalue distributions $\mu_{G_n}$ yields limits of the equilibrium, and these separate the dense regime, where the mean field approximation is valid, from the sparse regime, where it is not.

Formalizing it. The result is proved in the paper; nothing here is open. No machine-checked version of it or of its ingredients exists: the random-walk Laplacian of a graph, linear–quadratic stochastic differential games, verification theorems for Nash systems, and Gaussian laws of linear SDEs with time-dependent coefficients. The mission produces a checked statement of the equilibrium together with reusable layers: spectral facts about $D^{-1}A - I$, an ODE analysis for $Q_\mu$, and a Riccati reduction for quadratic Nash systems.

Difficulty

Three steps resist a direct approach.

• The verification theorem. The paper passes from a classical solution of the Nash system (4.1) to a Nash equilibrium by appeal to a standard verification argument. Over the full class of Borel controls with linear growth, this requires Itô's formula for the quadratic value functions, together with integrability of the deviated state processes.
• The Riccati system. The $n$ coupled matrix equations (4.6) have no general closed-form solution. The explicit solution exists only because transitivity forces $e_i^\top P(t)e_i = \mathrm{Tr}(P(t))/n$ for every $i$. That identity has to be derived from the action of the automorphism group (Lemma 4.1), not from regularity alone.
• The law of the state. It requires solving a linear SDE with a time-dependent matrix and identifying its Gaussian law, a step for which the library has little support.

Formalization scope

Lean conventions:

• Vertices. The vertex set is Fin n, so the paper's $1,\dots,n$ become $0,\dots,n-1$. The state space is the platform's EthierKurtz.SDEState n (Euclidean $\mathbb R^n$).
• The Laplacian. $L_G$ is the random-walk Laplacian $D^{-1}A-I$, not Mathlib's $D-A$.
• Time and controls. Time is real. Controls are Borel on $\mathbb R\times\mathbb R^n$ with linear growth on $[0,T]$; their values off $[0,T]$ are never used.
• Solutions of (2.1). A solution is a pathwise strong solution on a probability space that the solution itself carries, adapted to the completed Brownian filtration. Costs are compared across solutions; this is faithful because (2.1) has a unique strong solution.
• Costs are $[0,\infty]$-valued lower Lebesgue integrals. They are converted to reals only after their finiteness is asserted.
• Existence of the equilibrium state. The goal also asserts that the equilibrium state equation has a solution, so that the Nash property cannot hold vacuously.
• Derivatives. $f_G'(T-t)$ is written as its ODE value $cQ_G'(f_G(T-t))$. The ODE is solved on $[0,T]$ with one-sided derivatives at the endpoints, and uniqueness is agreement on $[0,T]$.
• Matrix conventions. Covariance integrals are entrywise. Gaussian laws are Mathlib's multivariateGaussian.
• Added hypotheses. $0<n$ is added to three milestones that are false on the empty graph.

A formalization that fixes $x_0=0$, restricts deviations to linear controls, drops the existence of the equilibrium state process, or replaces $L_G$ by $D-A$ is not this theorem.

Infrastructure that a complete development needs:

• symmetric-matrix spectral calculus for $L_G$ and for the matrix functions $(I-xL)^{-1}$ and $\log(I-xL)$;
• differentiation under the integral for $Q_\mu$;
• Picard–Lindelöf and Grönwall on $\mathbb R_+$;
• Itô's formula for quadratic functions of a diffusion with additive noise;
• the Gaussian law of $\int_0^t M(t,s)\,dW_s$ for deterministic $M$.

The spectral, ODE and Riccati layers are reusable beyond this mission. Proofs of individual milestones are welcome; so are general verification theorems for linear–quadratic games.

Selected references

• D. Lacker, A. Soret, A case study on stochastic games on large graphs in mean field and sparse regimes, arXiv:2005.14102v2, 2021; Math. Oper. Res. 47(2), 2022. https://arxiv.org/abs/2005.14102
• F. Chung, Spectral Graph Theory, CBMS Regional Conference Series in Mathematics 92, AMS, 1997. https://doi.org/10.1090/cbms/092
• 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
• A. Veretennikov, On strong solutions and explicit formulas for solutions of stochastic integral equations, Math. USSR-Sb. 39(3), 1981. https://doi.org/10.1070/SM1981v039n03ABEH001522