Numerical Analysis

Motivation

The r-algorithm of N. Z. Shor is a variable-metric method for minimizing functions that are not differentiable everywhere, such as maxima of smooth functions, penalty functions and Lagrangian dual functions of integer and decomposition problems. It combines a subgradient step with a space dilation along the difference of two successive almost-gradients, and the book reports it competitive with the best variable-metric and conjugate-gradient methods on "gully"-shaped test problems (Shor 1985, §3.6, pp. 68–77). Its convergence theory is limited. Section 3.7 of Shor's book gives a convergence proof only for an idealized version with exact directional minimization, on a class of piecewise smooth functions, and the book itself calls a weakening of the assumptions and rate estimates desirable (p. 85). This mission formalizes that section.

Timeline. Shor and Zhurbenko introduced the r-algorithm in 1971 (Kibernetika, no. 3, 51–59). Shor analysed the convergence of its exact-line-search version in 1975 (Kibernetika, no. 4, 48–53). Section 3.7 of the 1979 Russian monograph, translated in 1985, gives that analysis for piecewise smooth functions. The book states on p. 85 that weaker assumptions and rate estimates would be desirable.

Setting

Let $E_n$ be $n$-dimensional Euclidean space with inner product $(x, y)$, $n \ge 1$. For a unit vector $\xi$ and $\alpha > 0$ the operator of space dilation is $R_\alpha(\xi)x = x + (\alpha - 1)(x, \xi)\xi$.

Widths. For a compact convex set $W$ and a unit vector $\eta$, the width in direction $\eta$ is $d_\eta(W) = \max_{x \in W}(\eta, x) - \min_{x \in W}(\eta, x)$. The width is $d(W) = \min_{\|\eta\| = 1} d_\eta(W)$ and the diameter is $D(W) = \max_{\|\eta\| = 1} d_\eta(W)$. With $e_\rho(W) = \inf_{z \in W}|(\rho, z)|$ put $K_\rho(W) = d_\rho(W)/e_\rho(W)$ (or $+\infty$ when $e_\rho(W) = 0$) and $p(W) = \inf_{\|\rho\| = 1} K_\rho(W)$.

The class $K$. $E_n$ is partitioned into closed sets $\bar D_1, \dots, \bar D_m$, each the closure of its interior, whose interiors are disjoint and homeomorphic to an open ball or open halfspace; $f_i$ is continuously differentiable on an open set containing $\bar D_i$; and $f = f_i$ on $\bar D_i$. At a point $x$, the set of almost-gradients $G_f(x)$ is the set of gradients $\nabla f_i(x)$ of the pieces with $x \in \bar D_i$. For $\delta, \varepsilon > 0$, $\bar P_{\delta,\varepsilon}(x)$ is the closed convex hull of all $G_f(y)$, $\|y - x\| < \delta$, together with the $\varepsilon$-balls around the elements of $G_f(x)$.

The $r(\alpha)$-algorithm. Fix $\alpha > 1$, $\beta = 1/\alpha$. Start from $x_0$, $\tilde g_0 = 0$ and a nonsingular $B_0$. At iteration $k + 1$ choose $g_f(x_k) \in G_f(x_k)$ with $(B_k^* g_f(x_k), \tilde g_k) \le 0$; set $g_k^* = B_k^* g_f(x_k)$, $r_k = g_k^* - \tilde g_k$, $\xi_{k+1} = r_k/\|r_k\|$, $B_{k+1} = B_k R_\beta(\xi_{k+1})$, $\tilde g_{k+1} = R_\beta(\xi_{k+1}) g_k^*$, and $x_{k+1} = x_k - h_{k+1}B_{k+1}\tilde g_{k+1}$ with $h_{k+1} \ge 0$ such that $f$ does not increase along the step and some almost-gradient at $x_{k+1}$ makes a non-acute angle with $\tilde g_{k+1}$ in the transformed metric. The standing assumption is $f(x) \to +\infty$ as $\|x\| \to \infty$ (3.50).

Formalization targets

Goal: convergence to an isolated local minimum (Theorem 3.13)

Assume (3.50) and $\|x_{k+1} - x_k\| \to 0$ (3.52). If $x^*$ is an isolated local minimum, the component of $\{x : f(x^*) \le f(x) \le f(x_0)\}$ containing $x_0$ also contains $x^*$, and no other point $z$ of that component has linearly dependent $G_f(z)$, then

$$\lim_{k \to \infty} x_k = x^* .$$

Milestones

• Lemma 3.2 (p. 80): for $B = SO$ with minimum eigenvalue $\lambda(B)$ of $S$, $\lambda(B)d(W) \le d(BW) \le \lambda(B)D(W)$.
• Lemma 3.3 (p. 80): for $z_1, z_2 \in W$, $0 < \beta \le 1$ and $\gamma = \|z_1 - z_2\|/d(W) \ge 1$,

$$d\Big(R_\beta\big(\tfrac{z_1 - z_2}{\|z_1 - z_2\|}\big)W\Big) \ge \frac{d(W)}{\sqrt{1 + (1-\beta^2)/(\beta^2\gamma^2)}} .$$

• Theorem 3.11 (p. 82): for every $\sqrt[n]{\beta} < v < 1$, $\varepsilon, \delta > 0$ and $r \ge 1$ there is $\bar k > r$ with

$$p\big(\bar P_{\delta,\varepsilon}(x_{\bar k})\big) \ge \sqrt{\frac{v^2\sqrt[n]{\alpha^2} - 1}{\alpha^2 - 1}} .$$

• Theorem 3.12 (p. 84): the level set $\{f = f_\infty\}$, $f_\infty = \lim_k f(x_k)$, contains a point $x^*$ with $G_f(x^*)$ linearly dependent.

Significance

Theorem 3.13 is the only convergence theorem the book gives for the r-algorithm. Theorems 3.11 and 3.12 hold for any function of the class $K$, convex or not, and say that iterates of the exact version cannot stall at a point where the local almost-gradients are linearly independent: linear dependence of $G_f(x)$ is a generalized stationarity condition that includes $0 \in \operatorname{conv} G_f(x)$. Lemmas 3.2 and 3.3 are statements about widths of convex bodies under linear maps and single dilations, and apply to any analysis of space-dilation methods, including the ellipsoid method.

All four results and the goal are proved in the book, the goal as a corollary without a written proof. None of them is formalized. The formalization adds a machine-checked definition of the class $K$ and of the algorithm as a relation on sequences covering every admissible choice of almost-gradients and stepsizes, a verified proof of the book's argument, and a check of the corollary step, which the book leaves to the reader.

Difficulty

The obvious argument for descent methods is that the function value drops by a fixed amount at every step unless the gradient is small. That argument fails here. The r-algorithm can make null steps, with $x_{k+1} = x_k$ while $B_k$ and $\tilde g_k$ change, and its steps are measured in a metric that degenerates as the dilations accumulate ($\det B_k = \beta^k \det B_0$). A small step does not certify near-stationarity, and a large accumulated dilation does not certify progress.

The difficulty is to relate the geometry of the transformed almost-gradient sets $B_k^*\bar P_{\delta,\varepsilon}(x_k)$ to the decay forced on $B_k$. This needs width estimates for convex bodies under linear maps and single dilations, which Mathlib does not have. Theorem 3.12 also needs a uniform lower bound, near a compact level set, on the Gram determinants of the piece gradients, and the book's proof of it is only sketched. Theorem 3.13 is stated as a corollary with no proof at all. Deriving it requires showing that the iterates cannot leave the prescribed component of $\{f(x^*) \le f \le f(x_0)\}$, and that their accumulation points reduce to $x^*$.

Formalization scope

• $E_n$ is EuclideanSpace ℝ (Fin n) with $n \ge 1$; operators are continuous linear maps; $B_k^*$ is the adjoint. $K_\rho$ and $p$ are valued in $[0, +\infty]$, so $K_\rho(W) = +\infty$ is represented exactly. Widths are sInf/sSup of support values, equal to the book's minima and maxima on nonempty compact sets.
• A function of class $K$ is given with its representation (pieces, open domains, smooth $f_i$), and $G_f(x)$ is the set of gradients of the incident pieces, as on p. 79. Linear dependence of $G_f(x)$ is the negation of linear independence of that set.
• A run of the algorithm is a predicate on sequences $x_k, \tilde g_k, B_k, g_f(x_k), h_{k+1}$; every theorem holds for every run. Step (3) divides by $\|r_k\|$, so $r_k \ne 0$ is part of the run: a run that reaches a point where no admissible choice gives $r_k \ne 0$ has no continuation, as in the book. The stepsize $h_{k+1} = \operatorname{argmin}$ is one admissible choice, not the definition.
• The standing assumption (3.50) is a hypothesis of Theorem 3.11 as well as of 3.12 and 3.13, because the book imposes it for the rest of the section on p. 79.
• In Lemma 3.3, $\beta > 0$ is added (the bound divides by $\beta^2$). "Body" means nonempty interior. An isolated local minimum is a local minimum with a neighbourhood containing no other local minimum.
• Runs exist, so the hypotheses are not vacuous. For $f(t) = |t_1| + 2|t_2|$ (four quadrant pieces), started at the minimizer $x_0 = 0$ with null steps, one can choose $g_f(x_{k+1}) = -g_f(x_k)$ at every step, and $0 \notin G_f$ keeps $r_k \neq 0$. A formalization under which no infinite run exists would make every theorem vacuous. The run predicate also forbids the degenerate reading $h_{k+1} < 0$, under which the monotonicity condition (a) would hold vacuously on an empty segment.
• Needed infrastructure: widths of compact convex sets under linear maps (via the singular values of $B$), the effect of a rank-one dilation on widths, determinant bounds for products of dilations, and Gram-determinant continuity. The first three apply to any space-dilation method and are welcome as independent lemmas.

Selected references

• N. Z. Shor, Minimization Methods for Non-Differentiable Functions, Springer Series in Computational Mathematics 3, Springer 1985, §3.7, pp. 77–85. doi:10.1007/978-3-642-82118-9
• N. Z. Shor, N. G. Zhurbenko, A minimization method using the operation of space dilation in the direction of the difference of two successive gradients, Kibernetika (Kiev), no. 3, 51–59, 1971 (listed in the bibliography of Shor 1985; no online copy known).
• N. Z. Shor, The analysis of convergence of a gradient type method with space dilation in the direction of the difference of two successive gradients, Kibernetika (Kiev), no. 4, 48–53, 1975 (listed in the bibliography of Shor 1985; no online copy known).

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