Stochastic Systems

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

Motivation

Stochastic differential equations (SDEs) whose coefficients grow faster than linearly appear throughout applied probability: population and epidemic models with cubic damping, Langevin dynamics with non-quadratic potentials, and stochastic volatility models such as the 3/2-model used for pricing VIX options (Goard–Mazur 2013). Their solutions are almost never available in closed form, so they are simulated, and the method of choice is the explicit Euler–Maruyama scheme, because it is cheap and easy to implement.

For superlinearly growing coefficients the classical explicit scheme fails: its moments can diverge even when those of the true solution are finite, so it does not converge in $\mathcal L^p$. Implicit schemes repair this at a higher computational cost (Higham–Mao–Stuart 2002). A second repair is to keep the scheme explicit but modify ("tame") its coefficients by an amount that vanishes as the step size goes to zero.

Timeline.

• 2002: Higham, Mao and Stuart prove strong convergence of implicit Euler-type methods under a one-sided Lipschitz condition (MR1949404).
• 2012: Hutzenthaler, Jentzen and Kloeden introduce the tamed Euler scheme for superlinearly growing drift and globally Lipschitz diffusion (Ann. Appl. Probab. 22, MR2985171).
• 2013: Sabanis gives a short proof of convergence of tamed schemes with rate, again for superlinear drift (Electron. Commun. Probab. 18, MR3070913); Gyöngy and Sabanis prove convergence in probability of Euler approximations under local monotonicity conditions (Appl. Math. Optim. 68, MR3131501).
• 2015: Hutzenthaler and Jentzen obtain $\mathcal L^p$-convergence of explicit schemes with superlinear diffusion coefficients, in the 3/2-model only for $p<1/2$ (Mem. Amer. Math. Soc. 236, no. 1112).
• 2016: Sabanis treats superlinearly growing drift and diffusion coefficients under a local monotonicity condition, with $\mathcal L^p$-convergence for every $p<p_0$ (Ann. Appl. Probab. 26, arXiv:1308.1796). This mission formalizes that $\mathcal L^p$-convergence theorem.

Setting

Fix a filtered probability space $(\Omega,\{\mathcal F_t\}_{t\ge0},\mathcal F,P)$ satisfying the usual conditions, a Wiener martingale $W$ in $\mathbb R^{d_1}$ (a standard Brownian motion adapted to $\mathcal F_t$ whose future increments are independent of $\mathcal F_t$), and a horizon $T>0$. For $x\in\mathbb R^d$, $|x|$ is the Euclidean norm and $xy$ the scalar product; for a $d\times d_1$ matrix, $|A|$ is the Hilbert–Schmidt norm.

The SDE is

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

with Borel coefficients $b(t,x)\in\mathbb R^d$, $\sigma(t,x)\in\mathbb R^{d\times d_1}$ and an $\mathcal F_0$-measurable initial value $X(0)$.

For $n\ge1$ let $\kappa_n(t)=\lfloor nt\rfloor/n$, the last grid point of mesh $1/n$ before $t$. The scheme is

$$dX_n(t)=b_n(t,X_n(\kappa_n(t)))\,dt+\sigma_n(t,X_n(\kappa_n(t)))\,dW(t),\qquad t\in[0,T],\tag{2.2}$$

with the same initial value $X(0)$ and Borel coefficient sequences $b_n,\sigma_n$ ("varying coefficients"). Between grid points the coefficients are frozen at $X_n(\kappa_n(t))$, so the scheme is explicit.

The hypotheses, with $p_0,p_1\in[2,\infty)$: A-1 continuity of $b$ in $x$; A-2 local boundedness of $b$; A-3 local monotonicity $2(x-y)(b(t,x)-b(t,y))+(p_1-1)|\sigma(t,x)-\sigma(t,y)|^2\le L_R|x-y|^2$ on $|x|,|y|\le R$; 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$. For the scheme: B-1 $\int_0^T\sup_{|x|\le R}[|b_n-b|^{p_0}+|\sigma_n-\sigma|^{p_0}]\,dt\to0$ for every $R$; B-2 $|b_n|\le\min(Cn^\alpha(1+|x|),|b|)$ and $|\sigma_n|^2\le\min(Cn^\alpha(1+|x|^2),|\sigma|^2)$ for some $\alpha\in(0,1/2]$; B-3 the coercivity bound of A-4 for $b_n,\sigma_n$, uniformly in $n$.

Formalization targets

Goal: Theorem 1 (p. 5)

Under A-1–A-5 and B-1–B-3 with $\alpha\in(0,1/2]$, for every $0<p<p_0$,

$$\lim_{n\to\infty}\sup_{0\le t\le T}\mathbb E\big[|X(t)-X_n(t)|^p\big]=0.$$

No rate is claimed; the statement holds for every coefficient sequence satisfying B-1–B-3, not only for the paper's tamed Models 1 and 2.

Milestones

• Lemma 1 (p. 7): under A-5, B-2, B-3, $\sup_{n\ge1}\sup_{0\le u\le T}\mathbb E|X_n(u)|^2<\infty$.
• Lemma 2 (p. 8): under A-1–A-5, B-2, B-3, for every $p\le p_0$,

$$\sup_{0\le t\le T}\mathbb E|X(t)|^p\ \vee\ \sup_{n\ge1}\sup_{0\le t\le T}\mathbb E|X_n(t)|^p<\infty.$$

• Theorem 4 (p. 6): under A-1–A-4 and B-1, $\sup_{0\le t\le T}|X_n(t)-X(t)|\to0$ in probability.

Significance

Theorem 1 gives $\mathcal L^p$-convergence of a whole class of explicit schemes, with no global Lipschitz condition on either coefficient, for every $p$ below the coercivity order $p_0$. In the 3/2-model of the introduction ($p_1=3.5$, $p_0=6$), earlier explicit results gave $\mathcal L^p$-convergence only for $p<1/2$ (Hutzenthaler–Jentzen 2015, §4.10.3); Theorem 1 gives it for all $p<6$. The theorem is also the qualitative base on which the paper's rate results (Theorems 2 and 3, separate missions of this series) are built, and it justifies Monte Carlo estimates of moments computed with such schemes.

The result is proved in the paper. It has, to our knowledge, no machine-checked proof anywhere; Mathlib has Brownian motion but no stochastic integral, and the Itô integral used here is the relational definition published by the Ethier–Kurtz series on this platform. A formal proof needs Itô's formula for $|x|^p$, Gronwall's lemma for moment functions, the convergence in probability of Theorem 4 (which the paper cites from Gyöngy–Sabanis rather than proving), and a uniform-integrability argument. Each of these is reusable well beyond this paper.

Difficulty

The natural first idea, estimating $\mathbb E|X(t)-X_n(t)|^p$ directly by Itô's formula and Gronwall, fails: under only local monotonicity the difference of drifts cannot be bounded by $|X-X_n|$ with a constant uniform in the state, so the Gronwall constant blows up. The route through convergence in probability and uniform moment bounds is forced, and the hard step is Lemma 2: bounding $\mathbb E|X_n(t)|^{p_0}$ uniformly in $n$. The coefficients of the scheme may grow like $n^\alpha$, and the frozen argument $X_n(\kappa_n(s))$ produces a correction term $\mathbb E\int|X_n(s)|^{p_0-2}(X_n(s)-X_n(\kappa_n(s)))b_n\,ds$ whose control is exactly where the restriction $\alpha\le1/2$ enters. For fixed $n$ finiteness of moments is easy (linear growth); uniformity in $n$ is the content.

Formalization scope

States are EuclideanSpace ℝ (Fin d); diffusion values are EuclideanSpace ℝ (Fin d × Fin d₁), whose norm is the Hilbert–Schmidt norm. Time is ℝ≥0; coefficients are uncurried maps on ℝ≥0 × ℝ^d, assumed Borel measurable. An Itô process on $[0,T]$ is a measurable process, adapted to the filtration augmented by all $P$-null sets, with continuous paths on $[0,T]$, satisfying the integral equation almost surely simultaneously for all $t\le T$; the stochastic integral is the platform relation EthierKurtz.HasBrownianItoIntegral, applied coordinatewise with the integrand cut off after $T$. Nothing is required of the processes after $T$, so no existence beyond the horizon is assumed. Right-continuity of the filtration is a hypothesis; completeness is replaced by adaptedness to the augmented filtration, which is weaker, so the formal theorems are at least as strong as the paper's.

The solutions $X$ and $(X_n)_{n\ge1}$ are hypotheses, all on one probability space with one Wiener process and one initial value; the theorems do not construct them. Expectations are lower Lebesgue integrals in $[0,\infty]$ and suprema over $t$ are taken in $[0,\infty]$, so no statement can hold because an expectation or a supremum takes a default value. B-1's integrand, a supremum over an uncountable ball, is required to be a.e. measurable in $t$, as the paper's Lebesgue integral presupposes. The exponent in Theorem 1 and Lemma 2 is restricted to $p>0$, the paper's convention for $\mathcal L^p$. The dependence clauses "$C:=C(T,K,\mathbb E|X(0)|^2)$" (Lemma 1) and "$C:=C(p,T,K,\mathbb E|X(0)|^p)$" (Lemma 2) are not formalized: only finiteness, i.e. a bound independent of $n$, is stated, which is what the proofs establish. Theorem 4 is stated with exactly its printed hypotheses.

A trivializing formalization, in which the moment bounds or the limit hold because the expectation or the supremum defaults to $0$, or because the hypotheses on the solutions cannot be met, is ruled out: all quantities live in $[0,\infty]$, and a sorry-free check shows every hypothesis is satisfiable (zero coefficients, constant solutions).

Contributions welcome: Itô's formula for the platform's integral relation, Burkholder–Davis–Gundy or Doob inequalities for it, a Gronwall lemma for measurable moment functions, and the Gyöngy–Sabanis convergence-in-probability theorem.

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)
• I. Gyöngy, S. Sabanis, A note on Euler approximations for stochastic differential equations with delay, Appl. Math. Optim. 68, 2013. https://mathscinet.ams.org/mathscinet-getitem?mr=MR3131501
• 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

Motivation

Servers in manufacturing lines, communication links and service systems break down, are taken offline for maintenance, or go on vacation. When the interruptions are rare but long, they dominate congestion. A single down period can build a backlog that takes a long time to clear, and in a network that backlog propagates downstream. Standard heavy-traffic diffusion approximations, which describe queue lengths by reflected Brownian motion, do not capture this effect.

Chen and Whitt (Queueing Systems 13, 1993) identify a regime in which the effect survives in the limit. Up times are of order $n$ and down times of order $\sqrt n$, while the load is within $1/\sqrt n$ of capacity. Under the diffusion scaling each down period then becomes a jump, and the limit of the queue-length process is a reflected jump-diffusion. The paper generalises the single-station result of Kella and Whitt (Adv. Appl. Probab. 22, 1990; reference [22] of the paper) to open networks.

Timeline:

• 1981: Harrison and Reiman define the multidimensional reflection map on continuous paths (Ann. Probab. 9). Reiman (Math. Oper. Res. 9, 1984) extends it to paths with jumps.
• 1990: Kella and Whitt prove the one-station jump-diffusion limit for long up and down times.
• 1991: Chen and Mandelbaum give fluid and diffusion limits of open networks without interruptions (Math. Oper. Res. 16 and Ann. Probab. 19; references [5], [6] of the paper).
• 1993: Chen and Whitt prove the network case with interruptions (this mission), in Skorohod's $M_1$ topology.

Setting

A network has $J$ single-server stations. Customers arrive from outside station $j$ according to a counting process $A_j$. Station $j$ completes $S_j(t)$ services in its first $t$ units of busy time. The $l$th departure from station $k$ is routed to station $j$ when the indicator $\chi_{kj}(l)=1$, and $R_{kj}(m)=\sum_{l\le m}\chi_{kj}(l)$ counts such departures. Station $j$ alternates up periods $u^j_1,u^j_2,\dots$ and down periods $d^j_1,d^j_2,\dots$, starting up, and $D_j(t)$ is its cumulative down time in $[0,t]$. With a work-conserving discipline, the queue length $Z$ and the busy time $B$ satisfy

$$Z_j(t)=Z_j(0)+A_j(t)+\sum_{k}R_{kj}\big(S_k(B_k(t))\big)-S_j(B_j(t)),\qquad B_j(t)=\int_0^t 1[Z_j(s)>0,\ j\text{ up at }s]\,ds ,$$

and the idle time is $Y_j(t)=t-D_j(t)-B_j(t)$.

The reflection map $(\psi,\phi)$ associated with a matrix $Q$ takes a path $x$ to the pair $(y,z)$ with $z=x+(I-Q)y\ge 0$, $y$ nondecreasing, and $y_j$ increasing only when $z_j=0$.

A sequence of networks is indexed by $n$. The arrival, service and routing processes satisfy functional central limit theorems with rates $\lambda^n\to\lambda$ and $\mu^n\to\mu$ at speed $1/\sqrt n$. Up and down times scale as $(u^{j,n}_k/n,\ d^{j,n}_k/\sqrt n)\Rightarrow(u^j_k,d^j_k)$. The network is balanced, $\lambda=[I-P^{\mathsf t}]\mu$, with $P$ the routing matrix. The limit down time $\hat D_j(t)$ is the sum of $d^j_k$ over the up periods completed by time $t$, which is a pure-jump process.

The $M_1$ topology on paths with jumps compares completed graphs, in which each jump is filled in by the straight segment from $x(t-)$ to $x(t)$, through their monotone parametrisations.

Formalization targets

Goal: Theorem 4.1, case $J=1$

For a single station with feedback probability $p\in[0,1)$, with $\hat Z^n(t)=n^{-1/2}Z^n(nt)$, $\hat B^n(t)=n^{-1/2}[B^n(nt)-nt]$, $\hat Y^n(t)=n^{-1/2}Y^n(nt)$ and $\hat D^n(t)=n^{-1/2}D^n(nt)$,

$$(\hat Z^n,\hat B^n,\hat Y^n,\hat D^n)\Rightarrow(\hat Z,\hat B,\hat Y,\hat D)\quad\text{in }D((0,\infty),\mathbb R^{4},M_1).$$

Here $\hat Z=\phi(\hat X)$, $\hat Y=\mu^{-1}\psi(\hat X)$ and $\hat B=-\hat D-\hat Y$, with $Q=p$ and

$$\hat X(t)=\hat Z(0)+\hat\xi(t)+\big(c_\lambda-(1-p)c_\mu\big)t+(1-p)\mu\hat D(t).$$

The paper states Theorem 4.1 for $J$ stations, with the analogous formulas and $Q=P^{\mathsf t}$. The mission's goal is its case $J=1$ (see Formalization scope).

Milestones

1. Lemma 4.1: $\hat D^n\Rightarrow\hat D$ in $D((0,\infty),\mathbb R^J,M_1)$.
2. Lemma 4.2: $n^{-1}B^n_j(nt)\to t$ u.o.c.
3. Eq. (4.24): $n^{-1/2}\xi^n(nt)\to\hat\xi(t)$ u.o.c.
4. Eqs. (4.28)–(4.29): $\big(n^{-1/2}X^n(nt),\,n^{-1/2}D^n(nt)\big)\to(\hat X,\hat D)$ jointly in $M_1$.
5. The almost-sure form of Theorem 4.1 on a Skorohod representation space, case $J=1$.

Significance

The theorem yields a tractable approximation for networks with rare long interruptions: a reflected Lévy-type process driven by a Brownian part and a compound jump part. Its distribution can be studied through the reflection map. The jump directions $[I-P^{\mathsf t}]\operatorname{diag}(\mu)e_j$ make explicit how an outage at one station drains its downstream stations while its own queue builds up. Remark (4.3) of the paper derives a diffusion analogue of Little's law from the same limit.

The theorem is proved in the paper, and no part of it has been formalized. A formalization would produce the first machine-checked $M_1$ topology on paths with jumps, a heavy-traffic limit theorem for a queueing network, and the random-time-change argument for counting processes.

Difficulty

The obvious argument chains three facts: the primitive processes converge, hence so does the scaled free process $X$, and the reflection map is continuous. Two steps break. First, subtraction is not continuous in $M_1$ when the two paths jump at the same time in opposite directions, so the joint convergence of $\hat D^n$ across stations needs (4.11) and one common parametrisation. Second, the reflection map is Lipschitz in the uniform topology, but the uniform topology cannot see jumps that occur at nearby times. Carrying the convergence through the reflection map in the $M_1$ topology requires controlling how the regulator and the regulated process move along each jump segment of $\hat X$, jointly for all coordinates.

Formalization scope

Stations are Fin J; the network index is n : ℕ, and only $n\to\infty$ enters. Durations are indexed from $0$ in Lean. The queue length is integer valued, (3.2) is computed in $\mathbb Z$, and a solution satisfies $Z\ge 0$.

• Solutions, not constructions. Every statement quantifies over all solutions $(Z^n,B^n)$ of (3.2)–(3.3) and all reflection pairs of $\hat X$. Existence and uniqueness are asserted in the paper by citation and are not assumed or proved here.
• $M_1$. Parametric representations are monotone in the order of the completed graph, which is the standard definition. The page states only that the time component is nondecreasing. Convergence on $(0,\infty)$ means convergence on every $[a,b]$ with $0<a<b$ continuity points of the limit. Jump segments are segments in $\mathbb R^d$ (strong $M_1$). Convergence in $D((0,\infty),\cdot,M_1)$ includes the requirement that every path be càdlàg on $(0,\infty)$, so a copy of the limit that is continuous nowhere cannot satisfy the continuity-point condition vacuously.
• Weak convergence is in coupling form: one probability space carries copies with the right laws that converge almost surely. The limits in (4.1)–(4.4) are continuous, so there the mode is u.o.c.
• Corrected printed errors. Lemma 4.2 is stated with $n^{-1}$ in place of the printed $n^{-1/2}$, as in its proof. The map on p. 346 is read as $\phi(X)=Z$, $\psi(X)=\operatorname{diag}(\mu)Y$, following (4.13). The reflection map allows $y(0)\ge 0$, because $\hat X(0)$ may leave the orthant when $\hat D(0)>0$; when $x(0)\ge 0$ this agrees with (2.2).
• Added hypotheses. The processes $Z^n,B^n,\hat Z,\hat Y$ are assumed to be stochastic processes (measurable at each time). All networks share one probability space, so that the routing is literally common. No independence is assumed.
• The goal is the case $J=1$ of Theorem 4.1. The printed theorem claims strong $M_1$ convergence, with one parametric representation for all $4J$ coordinates, for every $J$. For $J\ge 2$ that claim fails: during an upstream outage, a downstream queue that empties part-way through the jump bends the prelimit graph of $(\hat D_j,\hat Y_k)$, while the limit's completed graph is a straight segment. For $J=1$ every coordinate moves linearly through each jump. The milestones Lemma 4.1, Lemma 4.2, (4.24) and (4.28)–(4.29) are stated for general $J$, and the almost-sure core of the proof for $J=1$.

A trivializing formalization is excluded. The hypotheses are satisfiable (for example by deterministic arrival and service processes), $\hat N$ is used only when $\sum_ku^j_k=\infty$, and laws are compared only for measurable path maps.

Needed infrastructure: the Skorohod space with the $M_1$ topology and its characterization on $(0,\infty)$, continuity of addition and of composition with continuous time changes, the multidimensional reflection map on paths with jumps, and a Skorohod representation argument. Proofs of Lemma 4.1 and Lemma 4.2 are welcome independently.

Selected references

• H. Chen, W. Whitt, Diffusion approximations for open queueing networks with service interruptions, Queueing Systems 13 (1993) 335–359. https://doi.org/10.1007/BF01149260
• O. Kella, W. Whitt, Diffusion approximations for queues with server vacations, Adv. Appl. Probab. 22 (1990) 706–729 (reference [22] of the paper).
• J. M. Harrison, M. I. Reiman, Reflected Brownian motion on an orthant, Ann. Probab. 9 (1981) 302–308. https://doi.org/10.1214/aop/1176994472
• H. Chen, A. Mandelbaum, Discrete flow networks: diffusion approximations and bottlenecks, Ann. Probab. 19 (1991) 1463–1519 (reference [6] of the paper).
• M. I. Reiman, Open queueing networks in heavy traffic, Math. Oper. Res. 9 (1984) 441–458 (reference [25] of the paper).
• W. Whitt, Some useful functions for functional limit theorems, Math. Oper. Res. 5 (1980) 67–85. https://doi.org/10.1287/moor.5.1.67
• A. V. Skorohod, Limit theorems for stochastic processes, Theory Probab. Appl. 1 (1956) 261–290. https://doi.org/10.1137/1101022

Motivation

Many engineered systems switch between a finite number of operating modes at random times: a power grid after a line failure, a networked controller whose links drop, a manufacturing plant whose machines break down and are repaired. A standard model for such systems is a hybrid stochastic differential equation, also called an SDE with Markovian switching: the state follows an Itô equation whose coefficients depend on a mode that evolves as a continuous-time Markov chain. The monograph of Mao and Yuan (Stochastic Differential Equations with Markovian Switching, 2006) develops the stability theory of these equations.

A controller that stabilizes such a system usually needs the current state. In practice the state is sampled: it is observed at times $0,\tau,2\tau,\dots$ and the control is held between observations. Mao (Automatica 49, 2013) showed that, under a global Lipschitz condition on the drift and diffusion, a feedback control based on discrete-time observations makes a hybrid SDE mean-square exponentially stable when $\tau$ is small enough. You, Liu, Lu, Mao and Qiu (SIAM J. Control Optim. 53(2), 2015) replaced that condition by local Lipschitz continuity plus linear growth, gave an explicit bound (3.5) on the admissible observation interval, and proved $H_\infty$-stability, asymptotic stability, and, in Section 4, exponential stability in mean square and almost surely with an explicit rate. This mission formalizes that exponential stability result, Theorem 4.2, and the steps of its proof.

Setting

Let $(\Omega,\mathcal F,\{\mathcal F_t\}_{t\ge0},\mathbb P)$ be a probability space with a filtration satisfying the usual conditions (increasing, right-continuous, $\mathcal F_0$ contains the null sets). On it live an $m$-dimensional $\{\mathcal F_t\}$-Brownian motion $w$ and a right-continuous $\{\mathcal F_t\}$-Markov chain $r$ on $S=\{1,\dots,N\}$ with generator $\Gamma=(\gamma_{ij})$ ($\gamma_{ij}\ge0$ for $i\ne j$, zero row sums), independent of $w$. Fix $\tau>0$ and the sampling time $\delta_t=[t/\tau]\tau$. The controlled system is

$$dx(t)=\big(f(x(t),r(t),t)+u(x(\delta_t),r(t),t)\big)dt+g(x(t),r(t),t)\,dw(t),\qquad x(0)=x_0,\ r(0)=r_0,\tag{2.1}$$

with $f,u:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^n$ and $g:\mathbb R^n\times S\times\mathbb R_+\to\mathbb R^{n\times m}$.

The hypotheses are:

• Assumption 2.1: $f,g$ locally Lipschitz in $x$, and $|f(x,i,t)|\le K_1|x|$, $|g(x,i,t)|\le K_2|x|$ ($|g|$ the trace norm).
• Assumption 2.2: $|u(x,i,t)-u(y,i,t)|\le K_3|x-y|$ and $u(0,i,t)=0$.
• Assumption 3.1: there are $U\in C^{2,1}(\mathbb R^n\times S\times\mathbb R_+;\mathbb R_+)$ and $\lambda_1,\lambda_2>0$ with $\mathcal LU(x,i,t)+\lambda_1|U_x(x,i,t)|^2\le-\lambda_2|x|^2$, where

$$\mathcal LU=U_t+U_x[f+u]+\tfrac12\operatorname{trace}[g^TU_{xx}g]+\sum_j\gamma_{ij}U(x,j,t).$$

• Assumption 4.1: $c_1|x|^2\le U(x,i,t)\le c_2|x|^2$ with $c_1,c_2>0$.
• Condition (3.5): $\lambda_2>\frac{\tau K_3^2}{\lambda_1}\big[2\tau(K_1^2+2K_3^2)+K_2^2\big]$ and $\tau\le\frac1{4K_3}$.

Put $\theta=K_3^2/\lambda_1$, $\lambda=\lambda_2-\theta\tau[2\tau(K_1^2+2K_3^2)+K_2^2]$ (positive by (3.5)), and

$$H_1=\theta\tau\big(2\tau(K_1^2+2K_3^2)+K_2^2\big)+\frac{24\theta\tau^4K_3^4}{1-6\tau^2K_3^2},\qquad H_2=\frac{12\theta\tau^2K_3^2(\tau K_1^2+K_2^2)}{1-6\tau^2K_3^2}.$$

In Lean these are Assumption21, Assumption22, C21, LU, Assumption31, Assumption41, Condition35, theta, lam, H1, H2, rateEquationLHS; the basis is HybridSetup, the Itô integral IsItoIntegral, the sampling time delta, solutions SolvesSampledHybridSDE, and the functional (4.7) Vbar, all in the namespace You2015.Expo.

Formalization targets

Goal: Theorem 4.2 (exponential stability)

Under the hypotheses above, the equation

$$2\tau\gamma e^{2\tau\gamma}(H_1+\tau H_2)+\gamma c_2=\lambda\tag{4.4}$$

has a unique root $\gamma>0$, and every solution of (2.1) satisfies

$$\limsup_{t\to\infty}\frac1t\log\big(\mathbb E|x(t)|^2\big)\le-\gamma,\qquad\limsup_{t\to\infty}\frac1t\log|x(t)|\le-\frac\gamma2\quad\text{a.s.}$$

for all $x_0\in\mathbb R^n$, $r_0\in S$.

Milestones, in the order the proof uses them

1. (3.15) $\mathbb E|x(t)-x(\delta_t)|^2\le2\mathbb E\int_{\delta_t}^t[\tau|f+u(x(\delta_s),\cdot)|^2+|g|^2]ds$.
2. Theorem 3.2 ($H_\infty$-stability): $\int_0^\infty\mathbb E|x(s)|^2ds<\infty$.
3. (3.21) $\mathbb E|x(s)-x(\delta_s)|^2\le\frac{3(\tau K_1^2+K_2^2)}{1-6\tau^2K_3^2}\int_{\delta_s}^s\mathbb E|x(z)|^2dz+\frac{6\tau^2K_3^2}{1-6\tau^2K_3^2}\mathbb E|x(s)|^2$.
4. (4.11) $\mathbb E\bar V(\hat x_z,\hat r_z,z)\le(H_1+\tau H_2)\int_{z-2\tau}^z\mathbb E|x(y)|^2dy$ for $z\ge2\tau$.
5. (4.14) $c_1e^{\gamma t}\mathbb E|x(t)|^2\le C$ for $t\ge2\tau$.
6. (4.14) $\Rightarrow$ (4.3), the mean-square-to-almost-sure transfer cited from Mao–Yuan [23, Theorem 8.8].

Significance

The result. Theorem 4.2 gives a quantitative guarantee: a controller that samples the state every $\tau$ units makes the switching system decay exponentially, with a rate $\gamma$ computable from the constants of the assumptions. Asymptotic stability (Section 3 of the paper) says nothing about how fast trajectories settle; the rate is what a designer trades against the sampling cost when choosing $\tau$. The almost sure statement concerns individual trajectories, which is what an operator observes.

Formalizing it. The results are proved in the paper; none of them is machine-checked. Mathlib has real Brownian motion but no Itô integral, no stochastic differential equations and no continuous-time Markov chains. The mission therefore also produces a definition layer: a filtration under the usual conditions, a multidimensional $\{\mathcal F_t\}$-Brownian motion, an $\{\mathcal F_t\}$-Markov chain with a given generator, the $L^2$ Itô integral of vector-valued integrands, and the solution notion of an SDE with Markovian switching and a sampled-state delay. A related but different layer exists on Prove2Me for Ethier–Kurtz (EthierKurtz_IsStandardBrownian, EthierKurtz_HasBrownianItoIntegral, EthierKurtz_SolvesBrownianSDE); it has no mode switching and no sampled state, so it cannot express (2.1). Formalization also checks the constants: it found that the printed $H_1$ in (4.5) disagrees with the paper's own derivation (see below).

Difficulty

Equation (2.1) is a stochastic differential delay equation whose delay $t-\delta_t$ is bounded but jumps at every observation time, so the delay-equation stability theorems that require a differentiable delay with derivative below one (Mao–Yuan, p. 285) do not apply. A Lyapunov function of the current state alone leaves the term $U_x[u(x(t))-u(x(\delta_t))]$, which has no sign and depends on the path over a whole observation interval. An exponential rate requires controlling this delay term with an exponential weight, and the weight inflates the delay contribution by a factor $e^{2\tau\gamma}$; the rate equation (4.4) records exactly this balance. The almost sure part does not follow from the mean-square part by Chebyshev's inequality at fixed times alone: a pathwise bound needs control of the supremum of $|x|$ over each unit interval, which involves the martingale part of the solution.

Formalization scope

Conventions committed to in Lean:

• The state space is EuclideanSpace ℝ (Fin n), so $|x|$ is the Euclidean norm; the explicit constants in (3.5), (3.21), (4.5) depend on it. The diffusion $g$ is given by its $m$ columns and $|g|^2=\sum_k|g_k|^2$ (trace norm). Modes are Fin N (0-based). Time is ℝ≥0; time integrals are over subsets of $\mathbb R$ at s.toNNReal.
• Every expectation of a nonnegative quantity ($\mathbb E|x|^2$, $\mathbb E\bar V$) and every time integral of one is a lower Lebesgue integral in $[0,\infty]$, so a non-integrable process cannot produce a junk value $0$.
• Logarithms. The paper's $\log$ takes the value $-\infty$ at $0$. For a finite $a(t)\ge0$, $\limsup_{t\to\infty}\frac1t\log a(t)\le-\gamma$ is stated in the equivalent form "for every $\gamma'<\gamma$, eventually $a(t)\le e^{-\gamma't}$". Lean's Real.log 0 = 0 never enters. In (4.3) the almost-sure quantifier is outside the quantifier over $\gamma'$.
• Correction of (4.5). The page prints the last term of $H_1$ as $24\tau^3K_3^4/(1-6\tau^2K_3^2)$. Substituting (3.21) into (4.9), as the proof does, gives $24\theta\tau^4K_3^4/(1-6\tau^2K_3^2)$ (the same computation reproduces the printed $H_2$). The mission uses the corrected $H_1$ in the goal, (4.11) and (4.14). With the printed value the claimed rate could exceed what the proof yields whenever $\theta\tau>1$.
• "The unique root" is a conjunct of the goal ($\exists!\,\gamma>0$); the stability conclusions are stated for every positive root. "(so $\lambda>0$)" is a consequence of (3.5), not a hypothesis. (4.4) is kept as an equality.
• "The solution of (2.1)" is read as every process satisfying the solution definition: progressively measurable, almost surely continuous paths, $\mathbb E|x(t)|^2<\infty$ for each $t$, and for each $t$, almost surely, the integral equation with Itô integrals in the $L^2$ sense. Existence and uniqueness (cited from Mao–Yuan on p. 908) are not asserted.
• "An $m$-dimensional Brownian motion" and "a Markov chain with generator $\Gamma$" are read in the Mao–Yuan framework the paper cites: an $\{\mathcal F_t\}$-Brownian motion with independent coordinates and increments independent of the past, and an $\{\mathcal F_t\}$-Markov chain with transition matrix $e^{t\Gamma}$. The usual conditions are kept as hypotheses.
• "Locally Lipschitz" is uniform in the mode and time on each ball. $C^{2,1}$ carries its derivatives $U_t,U_x,U_{xx}$ as witnesses tied to $U$ by derivative relations and joint continuity.
• "$\tau>0$ sufficiently small for (3.5)" means every $\tau>0$ satisfying both inequalities of (3.5). $U,\lambda_1,\lambda_2,c_1,c_2,\tau$ are data. The constant $C$ of (4.14) is chosen after $x_0$, $r_0$, the solution and $\gamma$, and before $t$.
• (3.15), (3.21) and the transfer (4.14) $\Rightarrow$ (4.3) are stated under fewer hypotheses than the surrounding proof has (Assumptions 2.1, 2.2, $\tau>0$, and for (3.21) $\tau\le1/(4K_3)$), because their derivations use no more. $\bar V$ of (4.7) is used only for $z\ge2\tau$, where no extension of the solution to negative times is needed. Other misprints on the page ($g(x,i,s)=f(x,i,0)$ on p. 909, $V(\hat x_0,\hat r_0,t)$ for $V(\hat x_0,\hat r_0,0)$ on p. 918, the swapped $\vee,\wedge$ on p. 907) are not formalized.

A trivializing formalization is ruled out: the expectations are not Bochner integrals, $\log 0$ is never evaluated, the goal asserts that the rate equation has exactly one positive root (so the stability clauses are not vacuous), the solution notion admits the true solution and requires path continuity, and the derivative witnesses of $U$ are tied to $U$. A sorry-free local check confirms that Assumptions 2.1, 2.2, 4.1, condition (3.5) and $\lambda>0$ hold for $n=m=N=1$, $f=g=0$, $u(x)=-x$, $U=|x|^2$, $K_1=K_2=K_3=1$, $\lambda_1=1/4$, $\lambda_2=1$, $c_1=c_2=1$, $\tau=1/10$; for these data $\mathcal LU+\lambda_1|U_x|^2=-|x|^2$ by hand.

Welcome contributions: the Itô isometry and Itô's formula for the $L^2$ integral defined here, a generalized Itô formula for functions of a Markov-modulated Itô process, the Burkholder–Davis–Gundy inequality, and the Borel–Cantelli argument that turns mean-square exponential decay into almost sure decay. These are reusable far beyond this mission. Section 3 of the paper (asymptotic stability) is a separate mission of the same series.

Selected references

• S. You, W. Liu, J. Lu, X. Mao, Q. Qiu, Stabilization of Hybrid Systems by Feedback Control Based on Discrete-Time State Observations, SIAM J. Control Optim. 53(2), 905–925, 2015. https://doi.org/10.1137/140985779
• X. Mao, C. Yuan, Stochastic Differential Equations with Markovian Switching, Imperial College Press, 2006. https://doi.org/10.1142/p473
• X. Mao, Stabilization of continuous-time hybrid stochastic differential equations by discrete-time feedback control, Automatica 49(12), 3677–3681, 2013. https://doi.org/10.1016/j.automatica.2013.09.005