Stochastic Systems

Motivation

The ground-state energy of a mixed $p$-spin spin glass, $\mathsf{OPT}_N=\max_{\sigma\in\{\pm1\}^N}H_N(\sigma)/N$, converges almost surely to the infimum of the Parisi functional over non-decreasing order parameters (Auffinger–Chen 2017). El Alaoui, Montanari and Sellke (arXiv:2001.00904v1) study algorithms that find near-optimal configurations. They introduce incremental approximate message passing (IAMP) and show that, among a broad class of such algorithms, the best achievable energy is the infimum of the Parisi functional over a larger space of order parameters (their Theorem 4).

The upper bound in Theorem 4 is reduced, in Section 4 of the paper, to a stochastic optimal control problem. The energy reached by a message-passing algorithm becomes the objective of a control problem driven by a Brownian motion, with a terminal constraint and a variance constraint. The variance constraint is removed by a Lagrange multiplier $\tfrac12\xi''\gamma$. Proposition 4.1 states that the resulting Lagrangian value is exactly the Parisi functional $\mathsf P(\gamma)$. This mission formalizes that duality and the verification argument behind it (Section 7).

Setting

Mixture. Real coefficients $(c_k)_{k\ge2}$ define the mixture $\xi(t)=\sum_{k\ge2}c_k^2t^k$, with the standing assumption $\xi(1+\varepsilon)<\infty$ for some $\varepsilon>0$. Its derivatives $\xi'$, $\xi''$ are nonnegative and nondecreasing on $[0,1]$.

Order parameters. $\mathsf{SF}_+$ is the set of nonnegative step functions

$$\gamma=\sum_{i=1}^m\gamma_i\,\mathbb I_{[t_{i-1},t_i)},\qquad 0=t_0<t_1<\dots<t_m=1,\ \gamma_i\ge0 .$$

Put $\nu(t)=\int_t^1\xi''(s)\gamma(s)\,ds$.

Parisi PDE and functional. $\Phi_\gamma:[0,1]\times\mathbb R\to\mathbb R$ solves

$$\partial_t\Phi_\gamma+\tfrac12\xi''(t)\big(\partial_x^2\Phi_\gamma+\gamma(t)(\partial_x\Phi_\gamma)^2\big)=0,\qquad\Phi_\gamma(1,x)=|x| .$$

For $\gamma\in\mathsf{SF}_+$ it is given explicitly by the Cole–Hopf recursion: with $r(t)=\xi'(1)-\xi'(t)$ and $G\sim\mathsf N(0,1)$, for $t\in[t_{i-1},t_i)$,

$$\Phi_\gamma(t,x)=\frac1{\gamma_i}\log\mathbb E\exp\big\{\gamma_i\Phi_\gamma(t_i,x+\sqrt{r(t)-r(t_i)}\,G)\big\}.$$

The Parisi functional is $\mathsf P(\gamma)=\Phi_\gamma(0,0)-\tfrac12\int_0^1t\,\xi''(t)\gamma(t)\,dt$.

Control problem. Let $B$ be a standard Brownian motion. A control $u\in D[t,1]$ is a process on $[t,1]$, progressively measurable for the filtration of $(B_r)_{r\in[t,1]}$, with $\mathbb E\int_t^1\xi''(s)u_s^2\,ds<\infty$. The value is

$$\mathcal J_\gamma(t,z)=\sup_{u\in D[t,1]}\mathbb E\Big[\int_t^1\xi''(s)u_s\,ds+\frac12\int_t^1\nu(s)\big(\xi''(s)u_s^2-1\big)ds\Big]\quad\text{s.t.}\quad z+\int_t^1\sqrt{\xi''(s)}\,u_s\,dB_s\in(-1,1)\ \text{a.s.}$$

Candidate value function. With $\Phi^*_\gamma(t,z)=\inf_x\{\Phi_\gamma(t,x)-xz\}$,

$$V(t,z)=\Phi^*_\gamma(t,z)-\tfrac12\nu(t)z^2-\tfrac12\int_t^1\nu(s)\,ds .$$

Formalization targets

Goal: Proposition 4.1

$$\mathcal J_\gamma(0,0)=\mathsf P(\gamma)\qquad\text{for every }\gamma\in\mathsf{SF}_+ .$$

Milestones

1. Lemma 7.2 (a)–(e): $\Phi_\gamma(t,\cdot)$ is smooth for $t<1$, with derivatives jointly continuous on $[0,1)\times\mathbb R$ and $C^1$ in time where $\gamma$ is constant. The range of $\partial_x\Phi_\gamma(t,\cdot)$ is $(-1,1)$, it is strictly increasing, and $0<\partial_x^2\Phi_\gamma(t',x)\le C(t,\gamma)$ for $t'\le t$.
2. Envelope identities (proof of Lemma 7.3): $\partial_z\Phi^*_\gamma(t,z)=-x^*_t(z)$ and $\partial_z^2\Phi^*_\gamma(t,z)=-1/\partial_x^2\Phi_\gamma(t,x^*_t(z))$, where $x^*_t(z)$ is the unique root of $\partial_x\Phi_\gamma(t,x)=z$.
3. Lemma 7.3: $V$ solves the HJB equation

$$\partial_tV+\xi''(t)\sup_{\lambda\in\mathbb R}\Big\{\lambda+\frac{\lambda^2}{2}\big(\nu(t)+\partial_z^2V\big)\Big\}-\frac12\nu(t)=0,\qquad V(1,z)=0 .$$

4. Evaluation at the origin: $V(0,0)=\mathsf P(\gamma)$.
5. Proposition 7.1: $\mathcal J_\gamma(t,z)=V(t,z)$ for all $(t,z)\in[0,1]\times(-1,1)$.

Proposition 7.1 at $(0,0)$ together with milestone 4 gives the goal.

Significance

The result. By integration by parts (Eq. (4.4) of the paper), $\mathcal J_\gamma(0,0)$ bounds the value of the constrained control problem (4.2). That problem in turn bounds the asymptotic energy of every message-passing algorithm in the class of Theorem 4. Proposition 4.1 turns the bound into $\inf_{\gamma\in\mathsf{SF}_+}\mathsf P(\gamma)$, which is the analytic core of the optimality statement for IAMP. It is also an instance of a broader principle: the Parisi functional has a stochastic-control representation (Jagannath–Tobasco 2016).

Formalizing it. The result is proved in the paper; no machine-checked version exists. A complete formalization needs a verification theorem for a control problem with a state constraint ($M_1\in(-1,1)$), Itô's formula for a $C^{1,2}$ function that is only piecewise $C^1$ in time, and quantitative regularity of the Cole–Hopf solution. Each of these is reusable well beyond spin glasses.

Difficulty

The value function $\mathcal J_\gamma$ is not known to be smooth, and the dynamic-programming equation (4.6) is only heuristic. The proof therefore guesses a solution and verifies it. Two steps carry the difficulty.

First, the guess $V$ is a Legendre transform. Its regularity, and the sign $\nu+\partial_z^2V<0$ that makes the HJB supremum finite, rest on strict convexity and bounded curvature of $\Phi_\gamma(t,\cdot)$ (Lemma 7.2). These must be proved by induction through the Cole–Hopf recursion, including the steps with $\gamma_i=0$.

Second, the verification argument applies Itô's formula to $V(s,M^u_s)$, where $M^u$ is a martingale confined to $(-1,1)$ and $V$ is only $C^1$ in time between the jumps of $\gamma$. The boundary $\theta\to1$ needs a dominated-convergence argument, and attaining the supremum needs an explicit optimal feedback control built from an SDE.

Formalization scope

• Mixture. $\xi$ is a coefficient sequence $c:\mathbb N\to\mathbb R$ with $c_0=c_1=0$ imposed. $\xi'$ and $\xi''$ are explicit termwise series.
• Step functions. $\mathsf{SF}_+$ is represented by its data (breakpoints and values). $\gamma$ is extended by $0$ outside $[0,1)$; its value at $t=1$ never matters.
• Cole–Hopf. $\Phi_\gamma$ is defined by the recursion. When $\gamma_i=0$, the recursion uses its limit, the heat semigroup, instead of dividing by zero. Expectations over $G$ are integrals against gaussianReal 0 1.
• Derivatives. Space derivatives are deriv/iteratedDeriv. Time derivatives are right derivatives, because $\gamma$ jumps.
• Legendre transform. $\Phi^*_\gamma$ is a real infimum, used only for $|z|<1$, where it is bounded below.
• Brownian motion and filtration. $B$ is a Mathlib IsBrownianReal process on $\mathbb R_{\ge0}$, with each $B_r$ measurable. The filtration is $\mathcal F^t_s=\sigma(B_r:t\le r\le s)$.
• Stochastic integral. It is the $L^2$ Itô integral of the published definition Peng1990.SMP.IsItoIntegral (horizon $1$), whose integrability class is exactly $\mathbb E\int\xi''u^2<\infty$.
• Supremum. $\mathcal J_\gamma(t,z)=v$ is stated as "$v$ is the least upper bound of the objective values of admissible controls" (IsLUB), never as a real sSup. A default value of an empty or unbounded supremum therefore cannot make a statement trivially true.
• Disclosed hypothesis. Lemma 7.2, the envelope identities and Lemma 7.3 assume that $\xi$ is not identically zero (some $c_k\neq0$). For $\xi\equiv0$ one has $\Phi_\gamma(t,x)=|x|$ for all $t$, and these statements fail. Proposition 7.1, the evaluation at the origin and the goal need no such hypothesis.
• Lemma 7.3. The statement includes the inequality $\nu+\partial_z^2V<0$, which the page proves. This rules out reading the HJB supremum as a default value.

The paper's algorithmic results (Theorems 2–4, Corollary 2.2) are out of scope. They need the AMP and state-evolution machinery of Section 5 and Appendix A, and an informal model of computation. The optional bound (4.4) is not stated.

Welcome contributions include the regularity of Cole–Hopf solutions (Gaussian convolution, log-moment-generating functions), a general verification theorem for one-dimensional controlled martingales with a terminal state constraint, and Itô's formula for $C^{1,2}$ functions.

Selected references

• A. El Alaoui, A. Montanari, M. Sellke, Optimization of Mean-field Spin Glasses, arXiv:2001.00904v1, 2020. https://arxiv.org/abs/2001.00904
• A. Auffinger, W.-K. Chen, Parisi formula for the ground state energy in the mixed p-spin model, Ann. Probab. 45(6b), 2017. https://arxiv.org/abs/1606.05335
• A. Jagannath, I. Tobasco, A dynamic programming approach to the Parisi functional, Proc. AMS 144, 2016. https://arxiv.org/abs/1502.04398
• N. Touzi, Optimal Stochastic Control, Stochastic Target Problems, and Backward SDE, Fields Institute Monographs 29, Springer, 2012 (cited as [Tou12] in the paper; the verification argument of Section 7 follows its Theorem 4.1).

Motivation

A branching random walk is the simplest model of a population that both reproduces and moves: every particle dies and leaves a random cloud of children displaced relative to it. Its extreme particles control the speed of travelling waves in reaction–diffusion equations (the KPP/Fisher equation), the free energy of directed polymers on trees, the cover and hitting times of random walks on trees, and the maxima of log-correlated fields such as the two-dimensional Gaussian free field. The basic quantity is the position of the leftmost particle at time $n$.

Timeline.

• 1974–1976: Hammersley, Kingman and Biggins prove the law of large numbers $M_n/n\to\gamma$ for the minimum.
• 1978–1983: Bramson shows that for branching Brownian motion the maximum, centred at $\sqrt2\,t-\frac{3}{2\sqrt2}\ln t$, converges in law (Bramson 1983). Lalley and Sellke (1987, Ann. Probab. 15) identify the limit as a Gumbel law randomly shifted by the limit of the derivative martingale.
• 2004: Biggins and Kyprianou prove that the derivative martingale of a branching random walk converges to a limit that is non-trivial in the boundary case (Adv. Appl. Probab. 36).
• 2009: Hu and Shi (arXiv:math/0702799) and Addario-Berry and Reed (Ann. Probab. 37) find the logarithmic correction: $M_n-\frac32\ln n$ is tight. Bramson and Zeitouni (2009) obtain tightness around the median under tail assumptions.
• 2013: Aïdékon proves convergence in law of $M_n-\frac32\ln n$ for general non-lattice branching random walks, the result this mission formalizes (arXiv:1101.1810, Ann. Probab. 41 (2013)).

Setting

Let $\mathcal L$ be a point process on $\mathbb R$: a random, possibly infinite, collection of points. Start one particle at $0$. At time $1$ it dies and leaves children at the points of $\mathcal L$; each particle of generation $n$ then dies and leaves children at the points of an independent copy of $\mathcal L$, translated to its own position. Vertices of the genealogical tree $\mathbb T$ (a Galton–Watson tree) are labelled by finite words $u=(i_0,\dots,i_{k-1})$; $|u|=k$ is the generation, $u_j$ the ancestor at generation $j$, and $V(u)$ the position.

The paper works in the boundary case

$$\mathbf E\Big[\sum_{|x|=1}1\Big]>1,\qquad \mathbf E\Big[\sum_{|x|=1}e^{-V(x)}\Big]=1,\qquad \mathbf E\Big[\sum_{|x|=1}V(x)e^{-V(x)}\Big]=0,\tag{1.1}$$

and assumes throughout that $\mathcal L$ is non-lattice and that

$$\mathbf E\Big[\sum_{|x|=1}V(x)^2e^{-V(x)}\Big]<\infty,\qquad \mathbf E\big[X(\ln_+X)^2\big]<\infty,\qquad \mathbf E\big[\tilde X\ln_+\tilde X\big]<\infty,\tag{1.3–1.4}$$

with $X=\sum_{|x|=1}e^{-V(x)}$ and $\tilde X=\sum_{|x|=1}V(x)_+e^{-V(x)}$. The objects of the main theorem are the minimum $M_n=\min\{V(x):|x|=n\}$ (with $\min\varnothing=+\infty$) and the derivative martingale

$$D_n=\sum_{|x|=n}V(x)e^{-V(x)},$$

which converges almost surely to a limit $D_\infty\ge0$, strictly positive on non-extinction. A standard example: two children with i.i.d. normal displacements of mean and variance $2\ln2$.

Formalization targets

Goal: Theorem 1.1

There is a constant $C^*\in(0,\infty)$ such that for every real $x$,

$$\lim_{n\to\infty}\mathbf P\Big(M_n\ge\tfrac32\ln n+x\Big)=\mathbf E\Big[e^{-C^*e^xD_\infty}\Big].$$

The constant is not specified numerically. It is the product $C_1c_0$ of the constants below.

Milestones, in the order the proof uses them

1. Many-to-one lemma (2.1): $\mathbf E_a[\sum_{|x|=n}g(V(x_1),\dots,V(x_n))]=\mathbf E_a[e^{S_n-a}g(S_1,\dots,S_n)]$ for a centred random walk $S$.
2. Renewal function (2.13): the renewal function $R$ of the strict descending ladder heights of $S$ satisfies $R(x)/x\to c_0>0$.
3. Corollary 3.2 and Proposition 1.2: for the walk killed below $0$, $e^z\,\mathbf P(M_n^{\rm kill}<\frac32\ln n-z)\to C_1$, uniformly for $z\in[A,\frac32\ln n-A]$.
4. Global minimum bound: $\mathbf P(\exists u\in\mathbb T: V(u)\le-y)\le e^{-y}$.
5. Corollary 3.5: $\mathbf P(M_n\le\frac32\ln n-y)\le(1+c_{10}(1+y))e^{-y}$.
6. Proposition 4.1: $\frac{e^z}{z}\mathbf P(M_n<\frac32\ln n-z)\to C_1c_0$, uniformly on the same window.
7. Derivative martingale: $D_n\to D_\infty$ a.s., $D_\infty\ge0$, $D_\infty>0$ a.s. on non-extinction.
8. (5.2): $\sum_{u\in\mathcal Z[A]}V(u)e^{-V(u)}\to D_\infty$ a.s. as $A\to\infty$, where $\mathcal Z[A]$ is the set of particles absorbed at level $A$.

Significance

The theorem identifies the limit law of the extreme particle: $M_n-\frac32\ln n$ converges in law, on the event of survival, to a Gumbel variable shifted by $-\ln(C^*D_\infty)$. It is the input for the study of the whole extremal process of the branching random walk seen from its leftmost particle (Madaule, J. Theoret. Probab., 2017), and it is the discrete-time counterpart of the Bramson and Lalley–Sellke results that later work on log-correlated fields takes as its template. The $\frac32$ correction and the role of the derivative martingale are the signature of the boundary case, and of log-correlated extremes generally.

The result is proved and published. It has not been formalized: Mathlib has no branching processes, no Galton–Watson trees with positions, no renewal theory, and no derivative martingale. This mission produces the first machine-checkable statement of the convergence-in-law theorem and of the intermediate results it rests on. A complete development would also give reusable formal versions of the many-to-one lemma and of renewal theory for ladder heights.

Difficulty

The first-moment computation through the many-to-one lemma gives the wrong centring. It predicts that the minimum sits near $\frac12\ln n$, because the expected number of particles below a level is dominated by rare realisations. The true centring $\frac32\ln n$ only appears after restricting to particles whose ancestral path stays above a barrier, and this restriction requires random-walk estimates (ballot theorems and local limit theorems for walks conditioned to stay positive) that hold uniformly in a window of starting points. A second difficulty is that the limit must be identified, not only shown to exist. Tightness and subsequence arguments do not give the factor $D_\infty$; the identification needs the precise tail $C_1c_0\,z\,e^{-z}$ of Proposition 4.1, with a known constant, and the almost-sure behaviour of the sum over the stopping line $\mathcal Z[A]$.

Formalization scope

• Point process. The law $L$ of $\mathcal L$ is a probability measure on configurations $(N,p)\in\mathbb N_\infty\times(\mathbb N\to\mathbb R)$, where the points are $p_i$ for $i<N$.
• Tree. Labels are List ℕ. The branching random walk is any family $(\xi_u)_{u}$ of independent measurable configurations of law $L$ on a probability space. Every theorem holds for every such realisation, and a canonical realisation exists (product space).
• Assumptions. Every expectation in (1.1), (1.3), (1.4) is a lower Lebesgue integral of a $[0,\infty]$-valued sum. The signed condition in (1.1) is "the expectations of $\sum V_+e^{-V}$ and $\sum V_-e^{-V}$ are equal and finite". Non-lattice means: there are no $a\in\mathbb R$ and $d>0$ with all points a.s. in $a+d\mathbb Z$.
• Which assumptions where. The goal and §§3–5 assume all of them. The many-to-one lemma and the global minimum bound assume only (1.1), and the derivative-martingale milestone drops non-lattice, as in Appendix A.
• Minima and limits. $M_n$ and $M_n^{\rm kill}$ are extended reals, $+\infty$ on an empty generation, so extinction lies in $\{M_n\ge\frac32\ln n+x\}$. $D_n$ is a real sum over generation $n$, absolutely summable almost surely, and $D_\infty$ is its pointwise limit. The expectation in the goal is a lower integral of $e^{-C^*e^xD_\infty}\in(0,1]$.
• Constants. $C^*$ is chosen before $x$. In Proposition 4.1, $C_1$ and $c_0$ are hypotheses tied to Proposition 1.2 and (2.13), not re-chosen. Corollaries 3.2 and 3.5 assert existence of their constants without Proposition 3.1 and Corollary 3.4.
• Not trivial. A formalization with a real-valued $M_n$ equal to $0$ on extinction, a $D_\infty$ never shown to be the limit, or a $C^*$ depending on $x$ would not be this theorem. The definitions above rule out each of these.

Out of scope: the spine-measure lemmas (Lemmas 2.3, 3.3, 3.8–3.10, 4.3), Propositions 2.1–2.2 cited from Lyons, and Appendices B–C. Contributions are welcome on all milestones. The many-to-one lemma and the renewal statement are independent of the rest and are natural first targets.

Selected references

• E. Aïdékon, Convergence in law of the minimum of a branching random walk, Ann. Probab. 41(3A) (2013) 1362–1426. arXiv:1101.1810, doi:10.1214/12-AOP750
• J. D. Biggins, A. E. Kyprianou, Measure change in multitype branching, Adv. Appl. Probab. 36 (2004) 544–581. Reference [7] of Aïdékon (2013), arXiv:1101.1810, p. 68
• M. Bramson, Convergence of solutions of the Kolmogorov equation to travelling waves, Mem. Amer. Math. Soc. 44, no. 285 (1983). doi:10.1090/memo/0285
• S. P. Lalley, T. Sellke, A conditional limit theorem for the frontier of a branching Brownian motion, Ann. Probab. 15 (1987) 1052–1061. Reference [21] of Aïdékon (2013), arXiv:1101.1810, p. 69
• Y. Hu, Z. Shi, Minimal position and critical martingale convergence in branching random walks, and directed polymers on disordered trees, Ann. Probab. 37 (2009) 742–789. arXiv:math/0702799
• L. Addario-Berry, B. Reed, Minima in branching random walks, Ann. Probab. 37 (2009) 1044–1079. Reference [1] of Aïdékon (2013), arXiv:1101.1810, p. 68
• R. Lyons, A simple path to Biggins' martingale convergence for branching random walk, in Classical and Modern Branching Processes, IMA Vol. Math. Appl. 84 (1997) 217–221. Reference [22] of Aïdékon (2013), arXiv:1101.1810, p. 69

Motivation

Many economic and engineering systems are steered by agents who act at discrete instants rather than continuously: a central bank intervenes on an exchange rate, two energy producers adjust a shared stock, a firm rebalances inventory. Each action has a fixed cost, so continuous control is not realistic. The mathematical model is impulse control: the state follows a diffusion, and a controller may shift it at chosen stopping times by paying a cost. The single-controller theory is classical (Øksendal and Sulem, Applied Stochastic Control of Jump Diffusions, 2007). When two controllers with different objectives act on the same state, the result is a nonzero-sum stochastic differential game with impulse controls.

Before Aïd, Basei, Callegaro, Campi and Vargiolu, the literature on games with impulse controls was almost entirely zero-sum: Cosso (SIAM J. Control Optim., 2013) characterised the value of zero-sum impulse games through a double-obstacle quasi-variational inequality in the viscosity sense. Their paper (Math. Oper. Res. 45(1), 2020; arXiv:1605.00039) gives the first general formulation of the nonzero-sum case together with a verification theorem: a system of quasi-variational inequalities (QVIs) whose sufficiently regular solutions are the equilibrium payoffs. Its Section 4 then computes Nash equilibria in closed form for a one-dimensional game.

Setting

A $k$-dimensional Brownian motion $W$ on a filtered probability space satisfying the usual conditions drives the state equation

$$dY_s=b(Y_s)\,ds+\sigma(Y_s)\,dW_s ,\qquad Y_s\in\mathbb R^d,$$

with globally Lipschitz $b$ and $\sigma$. The game takes place in an open set $S\subseteq\mathbb R^d$ and ends at the exit time $\tau_S$ of the state from $S$. Each of two players $i\in\{1,2\}$ has a nonempty impulse set $Z_i\subseteq\mathbb R^{l_i}$ and a continuous impulse map $\Gamma^i:S\times Z_i\to S$: an intervention with impulse $\delta$ moves the state from $y$ to $\Gamma^i(y,\delta)$.

A strategy of player $i$ is a pair $\varphi_i=(\mathcal C_i,\xi_i)$ with $\mathcal C_i\subseteq S$ open and $\xi_i:S\to Z_i$ continuous. Player $i$ intervenes as soon as the state leaves $\mathcal C_i$, with impulse $\xi_i(y)$ at the current state $y$. Player 1 has priority on ties, and several interventions may happen at the same instant. This defines the controlled process $X$, the intervention times $\tau_{i,n}$ and impulses $\delta_{i,n}$ of each player, and the states $X_{(\tau_{i,n})^-}$ just before each intervention. The payoff of player $i$ is

$$J^i(x;\varphi_1,\varphi_2)=\mathbb E\Big[\int_0^{\tau_S}e^{-\rho_is}f_i(X_s)ds+\sum_{\tau_{i,n}<\tau_S}e^{-\rho_i\tau_{i,n}}\phi_i(X_{(\tau_{i,n})^-},\delta_{i,n})+\sum_{\tau_{j,n}<\tau_S}e^{-\rho_i\tau_{j,n}}\psi_i(X_{(\tau_{j,n})^-},\delta_{j,n})+e^{-\rho_i\tau_S}h_i(X_{\tau_S})\mathbf 1_{\{\tau_S<\infty\}}\Big],$$

where $j\ne i$, $\rho_i>0$, $f_i$ is a running payoff, $\phi_i$ the cost of one's own interventions, $\psi_i$ the gain from the opponent's, and $h_i$ a terminal payoff on $\partial S$. A pair of strategies is $x$-admissible, $(\varphi_1,\varphi_2)\in\Phi_x$, when these four terms are integrable, $\sup_{s\le\tau_S}|X_s|$ has all moments, and the interventions do not accumulate before $\tau_S$. A Nash equilibrium is a pair in $\Phi_x$ from which no player gains by a unilateral admissible deviation.

Given candidate payoff functions $V_1,V_2$ on $\bar S$, let $\delta_i(x)$ be the unique maximiser of $V_i(\Gamma^i(x,\delta))+\phi_i(x,\delta)$ over $Z_i$. Define $\mathcal M_iV_i(x)=V_i(\Gamma^i(x,\delta_i(x)))+\phi_i(x,\delta_i(x))$, $\mathcal H_iV_i(x)=V_i(\Gamma^j(x,\delta_j(x)))+\psi_i(x,\delta_j(x))$, the continuation region $\mathcal D_i=\{\mathcal M_iV_i-V_i<0\}$ and the generator $\mathcal AV=b\cdot\nabla V+\tfrac12\operatorname{tr}(\sigma\sigma^tD^2V)$. The QVI system is

$$V_i=h_i\ \text{on }\partial S,\quad \mathcal M_jV_j-V_j\le0\ \text{on }S,\quad \mathcal H_iV_i-V_i=0\ \text{on }\{\mathcal M_jV_j=V_j\},\quad \max\{\mathcal AV_i-\rho_iV_i+f_i,\ \mathcal M_iV_i-V_i\}=0\ \text{on }\mathcal D_j .$$

Formalization targets

Goal: Theorem 3.3 (verification theorem)

Suppose $V_1,V_2$ solve the QVI system, $V_i\in C^2(\mathcal D_j\setminus\partial\mathcal D_i)\cap C^1(\mathcal D_j)\cap C(\bar S)$ with polynomial growth, $\partial\mathcal D_i$ is a Lipschitz surface near which $V_i$ has locally bounded first and second derivatives, $x\in S$, and the threshold pair $\varphi_i^*=(\mathcal D_i,\delta_i)$ is $x$-admissible. Then

$$(\varphi_1^*,\varphi_2^*)\ \text{is a Nash equilibrium and}\quad V_i(x)=J^i(x;\varphi_1^*,\varphi_2^*),\qquad i=1,2 .$$

Milestones

• Lemma 2.3: the controlled process is the concatenation of diffusion pieces, it jumps only at interventions, and between interventions it stays in $\mathcal C_1\cap\mathcal C_2$.
• Remark 3.6, (3.8b), (3.8d), (3.8f): against $\varphi_2^*$, the state stays in $\mathcal D_2$, and player 2 intervenes only on $\{\mathcal M_2V_2=V_2\}$ with impulse $\delta_2$.
• Step 1 of the proof: $V_1(x)\ge J^1(x;\varphi_1,\varphi_2^*)$ for every admissible deviation $\varphi_1$.
• Step 2 of the proof: $V_1(x)=J^1(x;\varphi_1^*,\varphi_2^*)$.

The goal follows from Steps 1 and 2 and their mirror images for player 2.

Significance

The theorem turns the search for Nash equilibria of nonzero-sum impulse games, an infinite-dimensional fixed-point problem over strategy pairs, into a deterministic problem: find functions satisfying a system of coupled QVIs with prescribed regularity. The regularity conditions become smooth-pasting conditions, hence a system of algebraic equations; Section 4 of the paper solves it explicitly for a one-dimensional game with linear payoffs. A further consequence is structural: equilibrium payoffs need only be $C^2$ on the opponent's continuation region, which is what lets non-smooth, piecewise-defined candidates qualify.

The result is proved in the paper; no machine-checked version exists. A complete formalization would be the first verified verification theorem for impulse control, single-player or game, and would expose every convention of the model: priority on ties, simultaneous interventions, the treatment of exit, and the integrability of the payoff. Several of these conventions need correction on the page, as listed below.

Difficulty

The heuristic argument applies Itô's formula to $e^{-\rho_1t}V_1(X_t)$ and uses the QVIs term by term. This fails on two counts. First, $V_1$ is only $C^1$ across the free boundary $\partial\mathcal D_1$, so Itô's formula does not apply directly. The paper mollifies $V_1$ (following Øksendal's proof of his verification theorem for optimal stopping) and must control the second derivatives near a Lipschitz boundary. Second, the sums over interventions may be infinite and the horizon unbounded, so expectations and limits do not commute. The passage to the limit needs the integrability built into $\Phi_x$ and the polynomial growth of $V_i$. The stochastic-calculus infrastructure itself (Itô's formula for continuous semimartingales stopped at random times, strong solutions of Lipschitz SDEs restarted at stopping times) is largely missing from Mathlib.

Formalization scope

The Lean model is pathwise. A realization is a sequence of diffusion pieces, each solving the state equation from the random restart time with the restart value. The Itô integral is the published relation EthierKurtz.HasBrownianItoIntegral, and the stochastic basis uses the published You2015.Shared.UsualConditions and IsFBrownian. Times take values in $[0,\infty]$ with $e^{-\rho\cdot\infty}=0$, and the state space is EuclideanSpace ℝ (Fin d). $\Phi_x$ asks for one admissible realization, while the Nash inequalities and the payoff identity hold on every admissible realization; strong uniqueness makes these readings equivalent.

The following deviate from the page and are disclosed in the items:

1. $\delta_i$ is assumed continuous, so that $\varphi_i^*$ is a strategy.
2. The fourth QVI is imposed on $\mathcal D_j\setminus\partial\mathcal D_i$, where $\mathcal AV_i$ exists.
3. The exit time is $\alpha^S_{\bar k+1}$, not the printed $\alpha^S_{\bar k}$.
4. The gain term of (2.7) is read with the opponent's interventions.
5. The supremum in (2.8) is taken over $[0,\tau_S]$.
6. Interventions accumulating at a finite $\tau_S$ are excluded from $\Phi_x$, since the page leaves $X_{\tau_S}$ undefined there.
7. Lemma 2.3 is stated in corrected form for simultaneous and boundary interventions.

The payoff is a Bochner expectation only inside $\Phi_x$, which requires the $L^1$ conditions of (2.7) and the integrability of each payoff. A non-integrable deviation therefore never receives the junk payoff $0$, and the Nash inequality cannot hold vacuously.

Contributions are welcome on the stochastic-calculus layer this needs (Itô's formula, strong existence and uniqueness for Lipschitz SDEs, optional stopping for stochastic integrals) and on the mollification lemma for functions that are $C^1$ with piecewise bounded second derivatives across a Lipschitz surface. These are reusable well beyond this mission.

Selected references

• R. Aïd, M. Basei, G. Callegaro, L. Campi, T. Vargiolu, Nonzero-sum stochastic differential games with impulse controls: a verification theorem with applications, Math. Oper. Res. 45(1), 2020 (accepted manuscript, arXiv:1605.00039v4). https://arxiv.org/abs/1605.00039
• A. Cosso, Stochastic differential games involving impulse controls and double-obstacle quasi-variational inequalities, SIAM J. Control Optim. 51(3), 2102–2131, 2013.
• B. Øksendal, Stochastic Differential Equations, 6th ed., Springer, 2003. https://doi.org/10.1007/978-3-642-14394-6
• B. Øksendal, A. Sulem, Applied Stochastic Control of Jump Diffusions, 2nd ed., Springer, 2007. https://doi.org/10.1007/978-3-540-69826-5

Motivation

Stochastic differential equations whose coefficients grow faster than linearly (for instance stochastic volatility models such as the 3/2-model) cannot be simulated with the classical explicit Euler–Maruyama scheme: Hutzenthaler, Jentzen and Kloeden showed that its moments diverge when the drift or diffusion grows superlinearly (Proc. R. Soc. A, 2011). Implicit schemes avoid the divergence but require solving a nonlinear equation at every step. Tamed Euler schemes keep the scheme explicit and damp the coefficients by a factor depending on the step size.

• 2012: Hutzenthaler, Jentzen and Kloeden introduce a tamed Euler scheme for SDEs with superlinearly growing drift (Ann. Appl. Probab. 22, 2012).
• 2013: Sabanis extends the taming analysis for superlinearly growing drift (Electron. Commun. Probab. 18, no. 10, 2013, MR3070913).
• 2015: Hutzenthaler and Jentzen survey explicit schemes for non-globally Lipschitz coefficients (Mem. Amer. Math. Soc. 236, no. 1112, 2015); for the 3/2-model their results give $\mathcal L^p$-convergence without rate only for $p<1/2$, as Sabanis (2016, p. 2) notes.
• 2016: Sabanis (Ann. Appl. Probab. 26(4), 2016, arXiv:1308.1796v4) treats schemes with varying coefficients $b_n,\sigma_n$, covering superlinearly growing diffusion coefficients, and proves $\mathcal L^p$ convergence (Theorem 1), the $\mathcal L^p$ rate 1/2 (Theorem 2) and the uniform $\mathcal L^q$ rate 1/2 (Theorem 3). A motivating example is the $d$-dimensional analogue of the 3/2-model of stochastic volatility, $dX=\lambda X(\mu-|X|)\,dt+\xi|X|^{3/2}\,dW$, used for pricing VIX options.

Theorem 3 is the target here; Theorems 1 and 2 are the targets of companion missions.

Setting

Fix a filtered probability space $(\Omega,\{\mathcal F_t\}_{t\ge0},\mathcal F,P)$ satisfying the usual conditions, a $d_1$-dimensional Wiener martingale $W$, a horizon $T>0$, and exponents $p_0,p_1\ge2$. For $x\in\mathbb R^d$, $|x|$ is the Euclidean norm; for a $d\times d_1$ matrix $A$, $|A|$ is the Hilbert–Schmidt norm; $xy$ is the scalar product. The coefficients are Borel functions $b:[0,\infty)\times\mathbb R^d\to\mathbb R^d$ and $\sigma:[0,\infty)\times\mathbb R^d\to\mathbb R^{d\times d_1}$, and the SDE is

$$dX(t)=b(t,X(t))\,dt+\sigma(t,X(t))\,dW(t),\qquad t\in[0,T],\qquad(2.1)$$

with an $\mathcal F_0$-measurable initial value $X(0)$. With $\kappa_n(t)=\lfloor nt\rfloor/n$, the scheme (2.2) is

$$dX_n(t)=b_n(t,X_n(\kappa_n(t)))\,dt+\sigma_n(t,X_n(\kappa_n(t)))\,dW(t),\qquad X_n(0)=X(0),$$

and in this mission $b_n,\sigma_n$ are the tamed coefficients of Model 2 with $\alpha=1/2$:

$$b_n(t,x)=\frac{b(t,x)}{1+n^{-1/2}|x|^l},\qquad \sigma_n(t,x)=\frac{\sigma(t,x)}{1+n^{-1/2}|x|^l}.$$

The conditions used are: A-2, local boundedness of $b$ on balls; A-4, the coercivity bound $2xb(t,x)+(p_0-1)|\sigma(t,x)|^2\le K(1+|x|^2)$; A-5, $\mathbb E|X(0)|^{p_0}<\infty$; and A-6, the global monotonicity

$$2(x-y)(b(t,x)-b(t,y))+(p_1-1)|\sigma(t,x)-\sigma(t,y)|^2\le L|x-y|^2$$

together with the polynomial Lipschitz bound $|b(t,x)-b(t,y)|\le L(1+|x|^l+|y|^l)|x-y|$, with $l,L>0$. The $\mathfrak p$-condition asks $l\le\frac{p_0-2}{4}$ and a moment exponent $p$ with $0<p<p_1$ and $p\le\frac{p_0}{2l+1}$.

Formalization targets

Goal: Theorem 3 (p. 6)

Under A-2, A-4–A-6 and the $\mathfrak p$-condition, for every $0<q<p$ there is $C$ independent of $n$ with

$$\mathbb E\Big[\sup_{0\le t\le T}|X(t)-X_n(t)|^q\Big]\le Cn^{-q/2},\qquad n\ge1.\qquad(2.14)$$

The supremum is inside the expectation, which distinguishes it from Theorem 2.

Milestones

1. Lemma 2 (p. 8): the moments of $X$ and of $X_n$ up to order $p_0$ are bounded on $[0,T]$ uniformly in $n$ (for general coefficients $b_n,\sigma_n$ under A-1–A-5, B-2, B-3).
2. Lemma 5 (p. 19): the Gyöngy–Krylov maximal inequality. If nonnegative continuous adapted $f,g$ satisfy $\mathbb E[f_\tau\mathbb 1_{\{g_0\le c\}}]\le\mathbb E[g_\tau\mathbb 1_{\{g_0\le c\}}]$ for all $c>0$ and stopping times $\tau\le T$, then

$$\mathbb E\Big[\sup_{t\le\tau}f_t^\gamma\Big]\le\frac{2-\gamma}{1-\gamma}\,\mathbb E\Big[\sup_{t\le\tau}g_t^\gamma\Big],\qquad\gamma\in(0,1).$$

3. Lemma 4 (p. 16): $\sup_{0\le t\le T}\mathbb E|X_n(t)-X_n(\kappa_n(t))|^p\le Cn^{-p/2}$.
4. Lemma 3 (p. 15): the taming errors $\mathbb E\int_0^T|b-b_n|^p(s,X_n(\kappa_n(s)))\,ds$ and the analogue for $\sigma$ are $\le Cn^{-\alpha p}$.

Significance

Theorem 3 gives the optimal strong rate 1/2 for an explicit scheme, uniformly over the time interval, for SDEs whose diffusion coefficient may grow superlinearly. Uniform-in-time error bounds are what pathwise functionals need (running maxima, barrier options, hitting times), and via Borel–Cantelli they give the almost-sure rate of Corollary 1 in the paper. Lemma 5 is a general-purpose tool: a domination inequality of Lenglart type, used throughout stochastic analysis to pass from bounds at stopping times to bounds on running suprema.

The results are proved in the paper; to our knowledge none of them has been formalized. Formalizing them would produce the first machine-checked convergence rate of a numerical scheme for SDEs, and a Lean proof of a Lenglart-type inequality, which Mathlib does not currently contain.

Difficulty

The error $X-X_n$ is controlled by the monotonicity condition A-6, which is one-sided: it bounds $2(x-y)(b(t,x)-b(t,y))$ from above but gives no Lipschitz bound on $b$ or $\sigma$ with a constant independent of $|x|,|y|$. The first idea, estimating $\mathbb E\sup_t|X-X_n|^p$ directly by applying the Burkholder–Davis–Gundy inequality to the martingale part of the error equation, therefore does not close: it produces terms of the same order as the quantity being estimated, weighted by polynomial factors in $|X|$ and $|X_n|$, and the argument that gives Theorem 2 controls $\mathbb E|X(t)-X_n(t)|^p$ only for fixed $t$. Passing from fixed times to the supremum is what forces the loss from $p$ to $q<p$ in Theorem 3, and it is where Lemma 5 enters. On the formal side, the Itô integral against Brownian motion, Itô's formula for functions of multidimensional Itô processes and the Burkholder–Davis–Gundy inequality are not in Mathlib.

Formalization scope

Processes are indexed by $t\in[0,\infty)$ (ℝ≥0) with values in EuclideanSpace ℝ (Fin d); diffusion values live in EuclideanSpace ℝ (Fin d × Fin d₁), whose norm is the Hilbert–Schmidt norm. The stochastic integral is the Ethier–Kurtz platform relation EthierKurtz.HasBrownianItoIntegral, applied coordinatewise, with integrands cut off after $T$. Solutions are hypotheses: the theorems apply to any solution $X$ of (2.1) and any family $(X_n)_{n\ge1}$ of solutions of (2.2) on one probability space with one $W$ and one $X(0)$; existence is not claimed. Processes are required to be adapted to the filtration augmented by null sets (weaker than a complete filtration), the filtration is right-continuous, and nothing is required after $T$. Expectations and suprema are computed in $[0,\infty]$, so no statement holds through an integral defaulting to $0$. Constants $C$ depend on everything except $n$ (and, in Theorem 3, may depend on $q$); only $n\ge1$ is used, and $q>0$, $p>0$ follow the paper's $\mathcal L^p$ convention.

Two hypotheses are added to the printed statements, both because the printed proofs need them:

• $p_1>2$ in Theorem 3. The proof applies Itô's formula for $p\ge2$; an admissible $p<2$ is handled through $p'=2$, which satisfies the $\mathfrak p$-condition exactly when $p_1>2$.
• B-3 in Lemma 4. The proof uses moment bounds uniform in $n$ (Lemma 2), which need B-3. Model 2 satisfies B-3.

Lemma 2 drops the dependence clause $C=C(p,T,K,\mathbb E|X(0)|^p)$ and asserts only finiteness. Lemma 5 assumes neither that $g$ is nondecreasing nor anything beyond the printed hypotheses.

A trivializing formalization is ruled out: the supremum sits inside a Lebesgue integral in $[0,\infty]$, so the goal cannot hold because of a junk value, and the hypotheses are satisfiable (zero coefficients, constant solutions), which a sorry-free check confirms.

Needed infrastructure: Itô's formula for multidimensional Itô processes, the Burkholder–Davis–Gundy inequality (for Lemma 4), Gronwall's inequality in integral form, and stopping-time localisation for continuous adapted processes. Contributions to any of these are welcome, and all are reusable far beyond this mission. Lemma 5 is independent of the SDE part and can be attacked first.

Selected references

• S. Sabanis, Euler approximations with varying coefficients: the case of superlinearly growing diffusion coefficients, Ann. Appl. Probab. 26(4), 2083–2105, 2016. https://doi.org/10.1214/15-AAP1140 — arXiv:1308.1796v4, https://arxiv.org/abs/1308.1796v4
• M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong and weak divergence in finite time of Euler's method for stochastic differential equations with non-globally Lipschitz continuous coefficients, Proc. R. Soc. A 467, 1563–1576, 2011. https://doi.org/10.1098/rspa.2010.0348
• M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong convergence of an explicit numerical method for SDEs with nonglobally Lipschitz continuous coefficients, Ann. Appl. Probab. 22(4), 1611–1641, 2012. https://doi.org/10.1214/11-AAP803
• M. Hutzenthaler, A. Jentzen, Numerical approximations of stochastic differential equations with non-globally Lipschitz continuous coefficients, Mem. Amer. Math. Soc. 236, no. 1112, 2015 (reference [5] of the paper).
• S. Sabanis, A note on tamed Euler approximations, Electron. Commun. Probab. 18, no. 10, 2013. MR3070913
• I. Gyöngy, N. V. Krylov, On the rate of convergence of splitting-up approximations for SPDEs, in Stochastic Inequalities and Applications, Progr. Probab. 56, 301–321, Birkhäuser, 2003 (cited by the paper for Lemma 5). MR2073438
• N. V. Krylov, Introduction to the Theory of Diffusion Processes, Transl. Math. Monographs 142, AMS, 1995 (cited by the paper for Lemma 5). MR1311478

Motivation

Stochastic differential equations with superlinearly growing coefficients appear throughout applied probability: population models with cubic damping, Langevin dynamics with polynomial potentials, and stochastic volatility models such as the 3/2-model used for pricing VIX options, whose diffusion coefficient grows like $|x|^{3/2}$. For such equations the classical explicit Euler–Maruyama method fails: Hutzenthaler, Jentzen and Kloeden (2011) proved that its $p$-th moments diverge whenever a coefficient grows superlinearly, so it cannot converge in $\mathcal L^p$. Implicit methods converge (Higham–Mao–Stuart 2002) but cost a nonlinear solve per step.

The tamed Euler schemes are the explicit response.

• Hutzenthaler, Jentzen and Kloeden (2012) tamed a superlinear drift and proved strong order $1/2$ for globally Lipschitz diffusion coefficients.
• Sabanis (2013) gave a simpler proof for a family of tamed drifts.
• Hutzenthaler and Jentzen (2015) treated superlinear diffusion coefficients, obtaining $\mathcal L^p$-convergence without a rate and only for small $p$.
• Sabanis (2016), the source of this mission, tames drift and diffusion together and proves the optimal strong rate $1/2$ in $\mathcal L^p$ under a one-sided (monotonicity) condition and polynomial growth. For the 3/2-model with $p_1=3.5$, $p_0=6$ this gives $\mathcal L^2$-convergence with order $1/2$, which earlier results did not cover (p. 2).

This mission is the second of three on the paper. Mission I formalizes $\mathcal L^p$-convergence without a rate (Theorem 1), mission III the uniform-in-time rate (Theorem 3).

Setting

Fix a filtered probability space $(\Omega,\{\mathcal F_t\}_{t\ge0},\mathcal F,P)$ with right-continuous filtration, a horizon $T>0$, dimensions $d,d_1$, and a $d_1$-dimensional Wiener martingale $W$: a standard Brownian motion adapted to $\{\mathcal F_t\}$ whose future increments are independent of $\mathcal F_t$. The coefficients are Borel maps $b:[0,\infty)\times\mathbb R^d\to\mathbb R^d$ and $\sigma:[0,\infty)\times\mathbb R^d\to\mathbb R^{d\times d_1}$; $|x|$ is the Euclidean norm, $|A|$ the Hilbert–Schmidt norm, $xy$ the scalar product. The SDE is

$$dX(t)=b(t,X(t))\,dt+\sigma(t,X(t))\,dW(t),\qquad t\in[0,T],\qquad(2.1)$$

with an $\mathcal F_0$-measurable initial value $X(0)=\xi$. For $n\ge1$ let $\kappa_n(t)=\lfloor nt\rfloor/n$ and consider the scheme

$$dX_n(t)=b_n(t,X_n(\kappa_n(t)))\,dt+\sigma_n(t,X_n(\kappa_n(t)))\,dW(t),\qquad X_n(0)=\xi,\qquad(2.2)$$

whose coefficients are frozen at the last grid point, so that $X_n$ is computable step by step. The tamed coefficients of Model 2 are

$$b_n(t,x)=\frac{b(t,x)}{1+n^{-\alpha}|x|^l},\qquad \sigma_n(t,x)=\frac{\sigma(t,x)}{1+n^{-\alpha}|x|^l}.\qquad(2.11)\text{–}(2.12)$$

The hypotheses, with constants $p_0,p_1\ge2$:

• A-2: $b$ is bounded on balls, uniformly in $t\in[0,T]$.
• A-4 (coercivity): $2xb(t,x)+(p_0-1)|\sigma(t,x)|^2\le K(1+|x|^2)$.
• A-5: $\mathbb E|X(0)|^{p_0}<\infty$.
• A-6 (global monotonicity, polynomial growth): for positive $l$ and $L$, $2(x-y)(b(t,x)-b(t,y))+(p_1-1)|\sigma(t,x)-\sigma(t,y)|^2\le L|x-y|^2$ and $|b(t,x)-b(t,y)|\le L(1+|x|^l+|y|^l)|x-y|$.
• The $\mathfrak p$-condition: the scheme uses (2.11)–(2.12) with $\alpha=1/2$, $l\le\frac{p_0-2}{4}$, and $0<p<p_1$, $p\le\frac{p_0}{2l+1}$.
• B-2 and B-3 (for the milestones): $|b_n|\le\min(Cn^\alpha(1+|x|),|b|)$, $|\sigma_n|^2\le\min(Cn^\alpha(1+|x|^2),|\sigma|^2)$, and A-4 for $b_n,\sigma_n$ with a constant uniform in $n$.

Formalization targets

Goal: Theorem 2 (p. 6)

Under A-2, A-4–A-6, the $\mathfrak p$-condition and $p_1>2$, there is a constant $C$ independent of $n$ with

$$\sup_{0\le t\le T}\mathbb E\big[|X(t)-X_n(t)|^p\big]\le Cn^{-p/2}\qquad(n\ge1).\qquad(2.13)$$

The constant is existential and may depend on all data except $n$.

Milestones

1. Lemma 2 (p. 8): $\sup_t\mathbb E|X(t)|^p$ and $\sup_{n\ge1}\sup_t\mathbb E|X_n(t)|^p$ are finite for $0<p\le p_0$, under A-1–A-5, B-2, B-3.
2. Lemma 3 (p. 15): for Model 2, $\mathbb E\int_0^T|b(s,X_n(\kappa_n(s)))-b_n(s,X_n(\kappa_n(s)))|^p\,ds\le Cn^{-\alpha p}$, and the same for $\sigma$.
3. Lemma 4 (p. 16): $\sup_t\mathbb E|X_n(t)-X_n(\kappa_n(t))|^p\le Cn^{-p/2}$.

Significance

Theorem 2 shows that an explicit scheme costing one coefficient evaluation per step attains the same strong order as the classical Euler method under global Lipschitz conditions. It does so for drift and diffusion coefficients that grow polynomially, and for moment orders $p$ that are small relative to $p_0$ and $p_1$. Strong $\mathcal L^p$ rates are what multilevel Monte Carlo needs: the variance of level corrections is controlled by the $\mathcal L^2$ rate. When $l$ could be taken to be $0$ the statement specializes to the classical globally Lipschitz rate (Remark 6).

The result is proved on paper; it has no machine-checked proof. Stochastic integrals are not in Mathlib; this mission uses the Brownian Itô-integral relation published by the Ethier–Kurtz series on the platform. A formal proof would give the first verified strong convergence rate for any Euler-type scheme. Along the way it produces reusable moment bounds for tamed schemes and the $L^p$ control of one-step increments.

Difficulty

The obvious argument applies Itô's formula to $|X-X_n|^p$ and closes a Gronwall inequality. Two steps of it fail without taming. First, the error splits into the monotone part, handled by A-6, and cross terms such as $|X_n(s)-X_n(\kappa_n(s))|^p$ multiplied by $(1+|X_n|^{2l})^{p/2}$; they are controlled only through moments of $X_n$ of order well above $p$ that are uniform in $n$, which the untamed scheme lacks. Second, the taming itself introduces an error $b-b_n$ that must be shown to be $O(n^{-1/2})$ in $\mathcal L^p$ and not merely $o(1)$. The exponents in the $\mathfrak p$-condition are exactly what the Hölder splittings of these two terms require.

Formalization scope

• Processes. Solutions are hypotheses, not constructed: $X$ solves (2.1) and each $X_n$ solves (2.2), on one probability space, with one $W$ and one $\xi$, on $[0,T]$ only. An Itô process is a measurable process adapted to the null-set completion of the filtration, with continuous paths on $[0,T]$, and a.s. for all $t\le T$ simultaneously $X(t)=\xi+\int_0^t B\,ds+\int_0^t S\,dW$. The stochastic integral is the platform relation EthierKurtz_HasBrownianItoIntegral, with the integrand cut off after $T$.
• Expectations and suprema are computed in $[0,\infty]$ (lower Lebesgue integrals), so no junk value of a non-integrable Bochner integral or of an unbounded real supremum enters. Rates are stated as $\le Cn^{-p/2}$ for every $n\ge1$, with $C$ real and quantified after all data.
• Added hypotheses, disclosed. Theorem 2 carries $p_1>2$: the printed proof covers $2\le p<p_1$ and reduces $p<2$ to $p=2$, which the $\mathfrak p$-condition admits exactly when $p_1>2$. Lemma 4 carries B-3, which its proof uses through Lemma 2. Lemma 2 drops the stated dependence of $C$ on $(p,T,K,\mathbb E|X(0)|^p)$ and keeps only its finiteness uniformly in $n$.
• Ruling out trivialization. The hypotheses are satisfiable, e.g. by $b=\sigma=0$ with constant solutions and $p_0=6$, $p_1=3$, $l=1$, $p=2$. The rate is a bound for every $n\ge1$, not an eventual or $o(1)$ statement. A proof that uses a constant depending on $n$, or treats only $X\equiv X_n$, does not prove the goal.
• Infrastructure needed: Itô's formula for $|x|^p$ against the platform's Itô integral, the Burkholder–Davis–Gundy inequality (or its $\mathcal L^p$ moment form), the zero-expectation property of Itô integrals of square-integrable integrands, and Gronwall's lemma in integral form. These are reusable far beyond this mission, and contributions of any of them are welcome.

Selected references

• S. Sabanis, Euler approximations with varying coefficients: the case of superlinearly growing diffusion coefficients, Ann. Appl. Probab. 26(4), 2016. https://arxiv.org/abs/1308.1796 (v4)
• M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong and weak divergence in finite time of Euler's method for stochastic differential equations with non-globally Lipschitz continuous coefficients, Proc. R. Soc. A 467, 2011. https://doi.org/10.1098/rspa.2010.0348
• M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong convergence of an explicit numerical method for SDEs with non-globally Lipschitz continuous coefficients, Ann. Appl. Probab. 22, 2012. https://mathscinet.ams.org/mathscinet-getitem?mr=MR2985171
• M. Hutzenthaler, A. Jentzen, Numerical approximations of stochastic differential equations with non-globally Lipschitz continuous coefficients, Mem. Amer. Math. Soc. 236(1112), 2015. https://doi.org/10.1090/memo/1112
• S. Sabanis, A note on tamed Euler approximations, Electron. Commun. Probab. 18, 2013. https://mathscinet.ams.org/mathscinet-getitem?mr=MR3070913
• D. J. Higham, X. Mao, A. M. Stuart, Strong convergence of Euler-type methods for nonlinear stochastic differential equations, SIAM J. Numer. Anal. 40, 2002. https://mathscinet.ams.org/mathscinet-getitem?mr=MR1949404