Numerical Analysis

Motivation

The ℓ1-regularized least squares problem (the Lasso, or basis pursuit denoising) is the model problem of compressed sensing and sparse inverse problems: given a matrix $A\in\mathbb R^{m\times n}$, data $d\in\mathbb R^m$ and a weight $\mu>0$, one seeks a vector $x$ that fits $Ax\approx d$ while having few nonzero entries. The standard first-order method for it is the iterative shrinkage thresholding algorithm (ISTA), a forward-backward splitting scheme whose backward step is componentwise soft thresholding. Each iteration costs two matrix–vector products, which is why ISTA and its variants are used on problems far too large for interior-point methods.

The classical complexity guarantee for ISTA is $f(x_k)-\min f=O(1/k)$, the rate of the proximal gradient method on any convex composite problem (Beck–Teboulle 2009). ISTA itself goes back to Daubechies–Defrise–De Mol 2004, and its link with forward-backward splitting to Combettes–Wajs 2005. An asymptotic linear rate was known, with an explanation through partial smoothness (Liang–Fadili–Peyré), but there was no global, explicit, non-asymptotic bound. Bolte, Nguyen, Peypouquet and Suter (arXiv:1510.08234v3, Math. Program. 2017) derive such a bound from two ingredients: an error bound for the Lasso objective on $\ell_1$ balls, with a constant written through a Hoffman constant, and their general theory turning a Kurdyka–Łojasiewicz (KL) inequality into complexity bounds for descent methods.

Setting

Write $\mathbb R^n$ with the Euclidean norm $\|\cdot\|$, and $\|x\|_1=\sum_i|x_i|$. For a matrix $M$, $\|M\|$ is its spectral norm, the operator norm from $\mathbb R^n$ to $\mathbb R^m$ with Euclidean norms. The objective is

$$f(x)=\mu\|x\|_1+\tfrac12\|Ax-d\|^2,\qquad \mu>0,$$

with $\min f=\inf_x f(x)$ and $S=\operatorname{argmin} f$. Put $g=\mu\|\cdot\|_1$ and $h=\tfrac12\|A\cdot-d\|^2$. Then $h$ is convex with gradient $A^T(Ax-d)$, Lipschitz with constant $L=\|A^TA\|$.

Given stepsizes $0<\lambda^-\le\lambda_k\le\lambda^+$ with $\lambda^+L<2$ and any $x_0$, ISTA is

$$x_{k+1}=\operatorname{prox}_{\lambda_k\mu\|\cdot\|_1}\big(x_k-\lambda_k(A^TAx_k-A^Td)\big),\qquad k\ge0,$$

where $\operatorname{prox}_\varphi(v)$ is the minimizer of $\varphi(y)+\tfrac12\|y-v\|^2$. More generally, in a real Hilbert space $H$ with $g$ proper, lower semicontinuous and convex and $h$ convex with $L$-Lipschitz gradient, the forward-backward method takes $x_{k+1}$ to be a minimizer of $g(z)+\langle\nabla h(x_k),z-x_k\rangle+\frac1{2\lambda_k}\|z-x_k\|^2$.

A sequence is a subgradient descent sequence for a convex $f$ with constants $a,b>0$ if $x_0\in\operatorname{dom} f$ and, for every $k\ge1$,

• (H1) $f(x_k)+a\|x_k-x_{k-1}\|^2\le f(x_{k-1})$;
• (H2) some $\omega_k\in\partial f(x_k)$ has $\|\omega_k\|\le b\|x_k-x_{k-1}\|$.

With $\min f=0$, $f$ has the KL property on a set $X\cap[0<f<\bar r]$ with desingularizing function $\varphi$ if $\varphi'(f(x))\|v\|\ge1$ for every such $x$ and every $v\in\partial f(x)$.

A number $\nu\ge0$ is a Hoffman constant for a pair of matrices $(A',E)$ if, for every right-hand side with $X=\{A'x\le a'\}$ and $Y=\{Ex=e\}$ intersecting, $\operatorname{dist}(x,X\cap Y)\le\nu\|Ex-e\|$ for all $x\in X$.

Formalization targets

Goal: Theorem 25

Put $a=\frac1{\lambda^+}-\frac L2$ and $b=\frac1{\lambda^-}+L$, and $R=\max\big(\frac{f(x_0)}\mu,1+\frac{\|d\|^2}{2\mu}\big)$. Let $\gamma_R>0$ be such that $f(x)-\min f\ge2\gamma_R\operatorname{dist}^2(x,S)$ whenever $\|x\|_1\le R$. Then ISTA converges to some $x^*\in S$ and

$$f(x_k)-\min f\le\frac{f(x_0)-\min f}{q^k}\quad(k\ge0),\qquad \|x_k-x^*\|\le C\,\frac{\sqrt{f(x_0)-\min f}}{q^{(k-1)/2}}\quad(k\ge1),$$ $$q=1+\frac{2a\gamma_R}{b^2},\qquad C=\frac1{\sqrt a}\Bigg(1+\frac1{ab^{-2}\gamma_R\sqrt{1+\frac1{2ab^{-2}\gamma_R}}}\Bigg).$$

Milestones

1. Lemma 10, (9)–(10): for $R>\|d\|^2/(2\mu)$ the error bound holds with $\gamma_R=1/\big(4\nu^2(1+\mu R+(R\|A\|+\|d\|)(4R\|A\|+\|d\|))\big)$. Here $\nu$ is a Hoffman constant of an explicit pair of matrices built from $A$ and $\mu$.
2. Lemma 10, KL consequence: under the error bound, $f-\min f$ has the KL property on the $\ell_1$ ball with $\varphi(s)=\sqrt{2s/\gamma_R}$.
3. Proposition 13: the forward-backward method satisfies (H1) and (H2) with the constants $a,b$ above.
4. §5.3: every ISTA iterate satisfies $\|x_k\|_1\le R$.
5. Corollary 20 in the stable-set form of Corollary 19: a subgradient descent sequence that stays in a set $X$, on which the KL inequality holds with $\psi(s)=\frac\ell2s^2$, satisfies $f(x_k)\le f(x_0)/(1+2a\sigma)^k$ and the companion bound on $\|x_k-x^*\|$, $\sigma=\ell b^{-2}$.

Significance

The result. The theorem replaces the sublinear $O(1/k)$ guarantee of ISTA by a global linear rate with explicit constants depending only on $\mu$, $A$, $d$, the stepsizes, $x_0$ and a Hoffman constant. It also bounds the distance of the iterates to the limit, not only the objective gap, and needs no uniqueness of the minimizer. Through $\gamma_R$, it shows that conditioning of the objective near its minimizers, rather than strong convexity, governs the complexity of the method. The general machinery behind it (Theorem 16 of the paper, a separate mission of this series) applies to any method producing subgradient descent sequences.

Formalizing it. The result is proved on paper, and no machine-checked proof of it or of its ingredients is known. A formalization would give a verified linear-rate certificate for a widely deployed algorithm. It would also yield reusable lemmas: the descent and relative-error properties of the forward-backward method in a Hilbert space, and quadratic growth for the Lasso on $\ell_1$ balls. Lemma 10 rests on an external result (Beck–Shtern, Lemma 2.5) that a complete development must also formalize.

Difficulty

The Lasso objective is not strongly convex when $A$ has a nontrivial kernel, and its minimizer need not be unique. The textbook argument for linear convergence of proximal gradient methods, which uses strong convexity, therefore does not apply. Quadratic growth $f-\min f\ge2\gamma\operatorname{dist}^2(\cdot,S)$ is the substitute, but it holds only on bounded sets, with a constant degrading in the radius. The analysis must therefore show that the iterates stay in a fixed $\ell_1$ ball and keep track of how the growth constant enters the rate. Deriving the explicit $\gamma_R$ requires recasting the problem as a quadratic program over a polyhedron with $2^n+1$ facets and invoking a Hoffman-type error bound for it.

Formalization scope

Citations refer to the arXiv preprint arXiv:1510.08234v3 (20 July 2016), with its numbering and pages; the journal version is not used. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) and matrices act through Matrix.toEuclideanLin. Spectral norms are operator norms of the associated continuous linear maps, never Mathlib's default entrywise matrix norm. The data vector, called $b$ in §3.2.1 of the paper and $d$ in §5.3, is $d$ throughout; $b$ is the constant of (H2).

Functions with values in $(-\infty,+\infty]$ are EReal-valued. The convex subdifferential, Γ₀, $\|\cdot\|_1$, the prox predicate and the class $\mathcal K(0,\bar r)$ of desingularizing functions are reused from published platform definitions. The stepsize condition $\lambda^+<2/L$ is written $\lambda^+L<2$, so that $A=0$ (where $L=0$) is covered. $\min f$ is the infimum of $f$, and $q^{(k-1)/2}$ is a real power.

In the goal, $\gamma_R$ is any positive constant satisfying the error bound on the ball of radius $R$; it is not fixed to the value (10) and not existentially quantified. The constants $a,b,q,C,R$ are fixed formulas, never existentials. A statement with an unspecified constant, with $\gamma_R$ chosen after the sequence, or with the stepsize hypothesis written as $\lambda^+<2/L$ (unsatisfiable or vacuous at $L=0$) would trivialize the goal and is ruled out.

The subgradient-descent and KL notions duplicate, in the sub-namespace ErrBoundCplx.ISTA, those of the series' first mission, because draft items cannot import each other. Proofs of any milestone are welcome, in particular Proposition 13 and the KL consequence of Lemma 10, which are self-contained. A formalization of Hoffman's error bound and of Beck–Shtern's Lemma 2.5 is the main infrastructure Lemma 10 needs.

Selected references

• J. Bolte, T. P. Nguyen, J. Peypouquet, B. W. Suter, From error bounds to the complexity of first-order descent methods for convex functions, Math. Program. 165 (2017) 471–507; arXiv:1510.08234v3. https://arxiv.org/abs/1510.08234v3
• A. Beck, S. Shtern, Linearly convergent away-step conditional gradient for non-strongly convex functions, preprint (cited as [10], Lemma 2.5). https://arxiv.org/abs/1504.05002
• A. Beck, M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM J. Imaging Sci. 2 (2009) 183–202. https://doi.org/10.1137/080716542
• A. J. Hoffman, On approximate solutions of systems of linear inequalities, J. Res. Natl. Bur. Stand. 49 (1952) 263–265. https://doi.org/10.6028/jres.049.027
• I. Daubechies, M. Defrise, C. De Mol, An iterative thresholding algorithm for linear inverse problems with a sparsity constraint, Comm. Pure Appl. Math. 57 (2004) 1413–1457. https://doi.org/10.1002/cpa.20042
• J. Liang, J. Fadili, G. Peyré, Local linear convergence of forward-backward under partial smoothness, preprint. https://arxiv.org/abs/1407.5611
• P. L. Combettes, V. R. Wajs, Signal recovery by proximal forward-backward splitting, Multiscale Model. Simul. 4 (2005) 1168–1200. https://doi.org/10.1137/050626090
• H. Attouch, J. Bolte, B. F. Svaiter, Convergence of descent methods for semi-algebraic and tame problems, Math. Program. 137 (2013) 91–129. https://doi.org/10.1007/s10107-011-0484-9

Motivation

Accelerated first-order methods, such as Nesterov's method and FISTA, reach a convergence rate of $\mathcal O(1/k^2)$ on the objective values of a smooth convex function, against $\mathcal O(1/k)$ for plain gradient descent. Since the work of Su, Boyd and Candès (arXiv:1503.01243), these methods are studied through their continuous-time limits, second-order differential equations with a vanishing viscous damping $\frac{\alpha}{t}\dot x$. The trajectories of these equations, and the iterates of the corresponding algorithms, oscillate strongly around the minimizers.

Adding a Hessian-driven damping term $\beta(t)\nabla^2 f(x(t))\dot x(t)$ to the dynamic damps these oscillations while keeping the fast rate. The idea goes back to Alvarez, Attouch, Bolte and Redont (2002) and was developed for fast convex minimization by Attouch, Peypouquet and Redont (arXiv:1601.07113, J. Differential Equations 2016). Shi, Du, Jordan and Su (arXiv:1810.08907) showed that the gradient-correction term of Nesterov's method is exactly such a Hessian damping, observed in a high-resolution limit. Because $\nabla^2 f(x(t))\dot x(t)$ is the time derivative of $\nabla f(x(t))$, the Hessian never has to be evaluated after discretization, and the resulting algorithms are genuinely first-order.

Attouch, Chbani, Fadili and Riahi (arXiv:1907.10536, Math. Program. 2020) study the system (DIN-AVD)$_{\alpha,\beta,b}$, $\ddot x+\frac{\alpha}{t}\dot x+\beta(t)\nabla^2f(x)\dot x+b(t)\nabla f(x)=0$, with general time-dependent coefficients, and derive algorithms from it. This mission formalizes their first discrete result: the convergence rate of the implicit (proximal) discretization.

Setting

Let $\mathcal H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$, and let $f:\mathcal H\to\mathbb R$ be a convex function of class $\mathcal C^1$ with gradient $\nabla f$, attaining its minimum at some point $x^\star$. Fix $\alpha\ge1$, a step size $h>0$ with $s=h^2$, and two non-negative sequences $(\beta_k)_{k\in\mathbb N}$ (the Hessian damping) and $(b_k)_{k\in\mathbb N}$ (the time scaling of the gradient).

For $\mu\ge0$ and $y\in\mathcal H$, the proximal point $\mathrm{prox}_{\mu f}(y)$ is the minimizer of $z\mapsto\mu f(z)+\tfrac12\|z-y\|^2$.

The Inertial Proximal Algorithm with Hessian Damping (IPAHD) generates a sequence $(x_k)_{k\in\mathbb N}$ by, for $k\ge1$,

$$\mu_k=\frac{k}{k+\alpha}\big(\beta_k\sqrt s+sb_k\big),\qquad y_k=x_k+\Big(1-\frac{\alpha}{k+\alpha}\Big)(x_k-x_{k-1})+\beta_k\sqrt s\Big(1-\frac{\alpha}{k+\alpha}\Big)\nabla f(x_k),$$ $$x_{k+1}=\mathrm{prox}_{\mu_kf}(y_k).$$

It is the implicit time discretization, with step $h$, of (DIN-AVD)$_{\alpha,\beta,b}$:

$$k(x_{k+1}-2x_k+x_{k-1})+\alpha(x_{k+1}-x_k)+\beta_khk\big(\nabla f(x_{k+1})-\nabla f(x_k)\big)+b_kh^2k\nabla f(x_{k+1})=0. \tag{8}$$

The rate is measured by the sequence

$$\delta_k:=h\big(b_khk-\beta_{k+1}-k(\beta_{k+1}-\beta_k)\big)(k+1), \tag{9}$$

under two growth conditions: $(\mathcal G_2^{\rm dis})$ $b_khk-\beta_{k+1}-k(\beta_{k+1}-\beta_k)>0$ and $(\mathcal G_3^{\rm dis})$ $\delta_{k+1}-\delta_k\le(\alpha-1)\frac{\delta_k}{k+1}$. They are the discrete counterparts of the conditions $(\mathcal G_2)$, $(\mathcal G_3)$ of the continuous analysis.

Formalization targets

Goal: Theorem 4 (p. 11)

If $(\mathcal G_2^{\rm dis})$ and $(\mathcal G_3^{\rm dis})$ hold for every $k\ge k_0$, for some $k_0\ge1$, then every sequence generated by (IPAHD) satisfies: $\delta_k>0$ for $k\ge k_0$, and

$$f(x_k)-\min_{\mathcal H}f=\mathcal O\Big(\frac1{\delta_k}\Big),\qquad \sum_k\delta_k\beta_{k+1}\|\nabla f(x_{k+1})\|^2<+\infty.$$

The rate is stated in terms of $\delta_k$, with no constant fixed in advance, so it covers every admissible choice of $(\beta_k)$ and $(b_k)$ at once.

Milestones (the steps of the proof, pp. 10–13)

1. Every run of (IPAHD) satisfies (8).
2. Under (8), $v_{k+1}-v_k=h C_k\nabla f(x_{k+1})$, where $v_k:=(\alpha-1)(x_k-x^\star)+k(x_k-x_{k-1}+\beta_kh\nabla f(x_k))$ and $C_k=\beta_{k+1}+k(\beta_{k+1}-\beta_k)-b_khk$.
3. $\tfrac12\|v_{k+1}\|^2-\tfrac12\|v_k\|^2\le-(\alpha-1)hC_k(f(x^\star)-f(x_{k+1}))-hC_k(k+1)(f(x_k)-f(x_{k+1}))$.
4. For the energy $E_k:=\delta_k(f(x_k)-f(x^\star))+\tfrac12\|v_k\|^2$: $E_{k+1}-E_k\le\big(\delta_{k+1}-\delta_k-(\alpha-1)\frac{\delta_k}{k+1}\big)(f(x_{k+1})-f(x^\star))$.
5. $f(x_k)-\min f\le E_{k_0}/\delta_k$ for $k\ge k_0$.
6. $E_{k+1}-E_k+h\big(\tfrac h2C_k^2+\delta_k\beta_{k+1}\big)\|\nabla f(x_{k+1})\|^2\le0$.

Significance

With $\beta_k\equiv\beta>0$ and $b_k=1+\beta/(hk)$ one gets $\delta_k=h^2k(k+1)$, so Theorem 4 gives the accelerated rate $\mathcal O(1/k^2)$ for a proximal algorithm with Hessian damping, together with the summability of $k^2\|\nabla f(x_{k+1})\|^2$, a fast decay of the gradients that the plain inertial proximal algorithm does not provide. The time-dependent coefficients let the user trade damping against speed, and Remark 2 of the paper gives $\mathcal O(1/(k(k+1)))$ under a uniform version of $(\mathcal G_2^{\rm dis})$. The proximal scheme only needs $f$ of class $\mathcal C^1$; the non-smooth case (Theorem 5) is obtained from it through the Moreau envelope.

The result is proved in the paper. As far as the platform's catalog shows, neither the algorithm nor any Lyapunov analysis of an inertial algorithm with Hessian-driven damping has been machine-checked. A formal proof would certify a discrete energy argument whose printed version contains an index slip (a dropped factor $k+1$ in an intermediate display on p. 12), and the definitions are reused by the other missions of this series.

Difficulty

The proof is a discrete Lyapunov argument, and the difficulty is bookkeeping rather than a single deep step. The coefficient $\delta_k$ is not chosen in advance: it is forced by the requirement that the terms $f(x_k)-f(x_{k+1})$ cancel in $E_{k+1}-E_k$, and the inequality for $\tfrac12\|v_{k+1}\|^2-\tfrac12\|v_k\|^2$ only closes after the signs of $C_k$, $\beta_{k+1}$ and $\alpha-1$ are used in the right places. The convexity of $f$ enters twice, at different points ($x^\star$ and $x_k$). Reading the proximal step as the first-order optimality condition $x_{k+1}+\mu_k\nabla f(x_{k+1})=y_k$ and converting it into (8) requires matching $\sqrt s$ with $h$ and the coefficient $1-\frac{\alpha}{k+\alpha}$ with $\frac{k}{k+\alpha}$. A naive direct estimate of $f(x_k)-\min f$ from the proximal inequality alone gives only the unaccelerated rate.

Formalization scope

The space is {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H], $\nabla f$ is Mathlib's gradient f, convexity is ConvexOn ℝ Set.univ f and $\mathcal C^1$ is ContDiff ℝ 1 f. The minimizer is a point $x^\star$ with $f(x^\star)\le f(y)$ for all $y$, the concrete form of the paper's standing hypothesis $\mathrm{argmin}f\neq\emptyset$. The proximal step is the published predicate GoldenRatioVI.Shared.IsProxPoint: $x_{k+1}$ minimizes $\mu_kf(z)+\tfrac12\|z-y_k\|^2$. No proximal function with a junk value is defined. Sequences are indexed by $\mathbb N$, the recursion is required for $k\ge1$, and $x_0$, $x_1$ are free. $\mathcal O$ is =O[Filter.atTop] and the series is Summable in $\mathbb R$.

Hypotheses added relative to the printed theorem, all disclosed in the statements:

• $h>0$, $s=h^2$;
• $\beta_k,b_k\ge0$ for every $k$, the discrete analogue of the standing hypothesis (H), needed for $\mu_k\ge0$ and used in the proof;
• the growth conditions are assumed for $k\ge k_0$, with $k_0\ge1$.

At $k=0$, $(\mathcal G_2^{\rm dis})$ reads $-\beta_1>0$, so reading the conditions "for all $k$" would make every hypothesis set unsatisfiable and the theorem empty. A sorry-free check shows the hypotheses hold for $\beta\equiv0$, $b\equiv1$, $h=1$, $\alpha=4$, $k_0=2$. The goal statement mentions only $f$, the run and $\delta_k$; it does not refer to $v_k$, $E_k$ or $C_k$, and a formalization that assumes an energy inequality would not prove Theorem 4.

The definitions $\mu_k$, $y_k$, the run predicate, $\delta_k$, $C_k$, $v_k$ and $E_k$ live in one definition file. Proofs of the milestones are welcome individually; the identities (milestones 1–2) are algebra plus the first-order condition of the proximal step, and the inequalities (3–6) need the gradient inequality of a differentiable convex function. Theorem 5 (the non-smooth case) is not part of this mission.

Selected references

• H. Attouch, Z. Chbani, J. Fadili, H. Riahi, First-order optimization algorithms via inertial systems with Hessian driven damping, Math. Program., 2020; arXiv:1907.10536v2. https://arxiv.org/abs/1907.10536
• H. Attouch, J. Peypouquet, P. Redont, Fast convex minimization via inertial dynamics with Hessian driven damping, J. Differential Equations 261 (2016), 5734–5783. https://arxiv.org/abs/1601.07113
• B. Shi, S. S. Du, M. I. Jordan, W. J. Su, Understanding the acceleration phenomenon via high-resolution differential equations, Math. Program., 2021. https://arxiv.org/abs/1810.08907
• W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, J. Mach. Learn. Res. 17 (2016). https://arxiv.org/abs/1503.01243

Motivation

Accelerated gradient methods use information from earlier iterates to reduce the objective gap of a smooth convex optimization problem faster than ordinary gradient descent. Their behavior depends on the precise momentum rule. Attouch, Chbani, Fadili, and Riahi study a discrete rule with an additional difference of consecutive gradients, motivated by an inertial differential equation with Hessian driven damping. This mission concerns their inertial gradient algorithm with Hessian damping, called IGAHD, and the rates proved for it in Theorem 6 of the source paper. The result matters when one wants a rate for objective values together with control of the gradients seen during the run.

The paper appeared as a 2020 preprint and subsequently in Mathematical Programming. The mission follows the pinned arXiv version, whose theorem and equation numbers supply all citations here. The proximal and strongly convex algorithms elsewhere in the paper have separate missions; their dynamics and rate statements differ from IGAHD.

Setting

Let $H$ be a real Hilbert space and let $f:H\to\mathbb R$ be convex and differentiable. Assume that its gradient $\nabla f$ is $L$-Lipschitz: $\|\nabla f(u)-\nabla f(v)\|\le L\|u-v\|$ for every $u,v\in H$, where $L>0$. Choose a minimizer $x^*$, so $f(x^*)=\min_H f$. The positive step size $s$ satisfies $s\le1/L$. The momentum parameter $\alpha$ is at least $3$, and the damping parameter $\beta$ lies in $[0,2\sqrt{s})$.

Given $x_0,x_1\in H$, the algorithm takes the following two steps for every integer $k\ge1$:

$$\begin{aligned} y_k={}&x_k+\left(1-\frac{\alpha}{k}\right)(x_k-x_{k-1}) -\beta\sqrt{s}\bigl(\nabla f(x_k)-\nabla f(x_{k-1})\bigr) -\frac{\beta\sqrt{s}}{k}\nabla f(x_{k-1}),\\ x_{k+1}={}&y_k-s\nabla f(y_k). \end{aligned}$$

The paper sets $t_{k+1}=k/(\alpha-1)$ and $v_k=x_{k-1}-x^*+t_k(x_k-x_{k-1}+\beta\sqrt{s}\nabla f(x_{k-1}))$. Its Lyapunov quantity is $E_k=t_k^2(f(x_k)-f(x^*))+(2s)^{-1}\|v_k\|^2$ for $k\ge1$. These expressions are fixed by the source formulas (14)–(15), p. 15, not chosen to simplify a later proof.

Formalization targets

The central target is the full rate statement of Theorem 6. In the range where the paper's monotonicity argument applies, $E_k$ is eventually nonincreasing. For every IGAHD run,

$$f(x_k)-\min_H f=O(k^{-2})\quad(k\to\infty).$$

When $\beta>0$, the theorem also gives both weighted gradient summability claims:

$$\sum_{k\ge0} k^2\|\nabla f(y_k)\|^2<\infty, \qquad \sum_{k\ge0} k^2\|\nabla f(x_k)\|^2<\infty.$$

The milestone list follows claims the authors state while proving that target. It begins with the extended descent inequality (Lemma 1, (28)), records the identities for $t_k$ and $v_k$, and then captures the displayed energy and $\varepsilon$ inequalities. Remark 4 asks for the $O(k^{-3})$ bound on the smallest squared gradient norm among the first $k$ iterates; Remark 5 asks for the $O(k^{-2})$ objective gap at $y_k$. Those are companion statements and are not substituted for the main theorem.

Significance

The rate bounds give three kinds of information about one trajectory. The objective gap controls the values attained at the iterates. The two summable series imply that the gradients at both the extrapolated points and the iterates become small in a weighted aggregate sense when damping is positive. The paper then uses this series estimate to derive the best-iterate estimate of Remark 4 and the extrapolated-value estimate of Remark 5, all on p. 18.

The result is proved in the cited paper; the open work here is its Lean proof and the supporting smooth convex analysis. The development makes the precise discrete algorithm, the Lyapunov quantity, and the descent inequality reusable as mathematical interfaces. A complete formal proof would also make explicit where the author's finite-index monotonicity wording needs correction.

Difficulty

The usual smooth descent estimate alone gives a decrease after one gradient step, but the extrapolated point $y_k$ also carries a momentum term and a gradient difference. Its objective value is therefore not the same quantity as $f(x_k)$, and a direct comparison of successive objective values does not give the claimed summability. The source uses a stronger descent inequality with a squared difference of gradients. The energy change then contains a quadratic expression in $\nabla f(y_k)$ and $\nabla f(x_k)$ whose sign depends on $\beta<2\sqrt{s}$ and, at first, on how large $k$ is. Establishing that sign uniformly over the relevant tail of the run is the central obstruction.

Formalization scope

The Lean space is a complete real inner product space. Convexity is ConvexOn ℝ Set.univ f; differentiability is explicit because the phrase “whose gradient is $L$-Lipschitz” presupposes a gradient. The existence of a minimizer is represented by a selected $x^*$ with $f(x^*)\le f(z)$ for every $z$. Positive $L$ and positive $s$ make $s\le1/L$ meaningful. The algorithm is a predicate on sequences $x,y:\mathbb N\to H$, imposed from $k=1$ so no coefficient is divided by zero. The first two $x$ terms are free, and $y_0$ is unused. The $O$ statements use the filter at infinity, so finite initial terms do not affect them; summability uses the ordinary series over natural indices.

The printed claim that $(E_k)$ is nonincreasing from its first term is false for the paper's own definitions. On $H=\mathbb R$ with $f(u)=u^2/2$, $L=s=1$, $\alpha=3$, $\beta=0$, $x_0=0$, and $x_1=1$, one gets $E_1=0$ and $E_2=1/8$. The formal goal keeps eventual monotonicity, as supported by the proof on pp. 16–18. This correction is disclosed rather than treated as a new hypothesis. No energy decrease, gradient bound, or conclusion is assumed in the run predicate. The milestone definitions also specify $B_k$ exactly as on p. 17. Contributions to the goal, to the extended descent lemma, or to the explicit energy estimates are all useful; the definition layer and smooth convex lemmas can serve later optimization formalizations.

Selected references

• H. Attouch, Z. Chbani, J. Fadili, and H. Riahi, First-order optimization algorithms via inertial systems with Hessian driven damping, Mathematical Programming, 2020; arXiv:1907.10536v2, especially §3.2, pp. 15–18, and Appendix A.1, p. 34.

Motivation

Many problems in statistics and signal processing ask for an orthonormal frame $X\in\mathbb R^{n\times r}$ that is both a good fit to the data and sparse or otherwise structured. Sparse principal component analysis, compressed modes in physics, unsupervised feature selection and sparse blind deconvolution all take the form

$$\min_{X}\ F(X)=f(X)+h(X)\quad\text{s.t.}\quad X^\top X=I_r,$$

with $f$ smooth and $h$ convex but nonsmooth, typically an $\ell_1$ penalty. Before the work of Chen, Ma, So and Zhang, algorithms for this class fell into three groups: subgradient-oriented methods, which solve a quadratic program over sampled subgradients in every step; proximal point algorithms, whose subproblems are as hard as the original problem; and operator-splitting methods such as SOC and MADMM. The manifold proximal gradient method (ManPG) carries the Euclidean proximal gradient method over to the Stiefel manifold. The paper shows that ManPG keeps the global convergence and the $O(\varepsilon^{-2})$ iteration complexity that Riemannian gradient descent has for smooth objectives (Boumal, Absil and Cartis, 2019).

Setting

The feasible set is the Stiefel manifold

$$\mathcal M=\mathrm{St}(n,r)=\{X\in\mathbb R^{n\times r}: X^\top X=I_r\},\qquad r\le n.$$

The ambient space $\mathbb R^{n\times r}$ carries the Frobenius inner product $\langle A,B\rangle=\operatorname{Tr}(A^\top B)$ and norm $\|A\|_F$. The tangent space at $X\in\mathcal M$ is $T_X\mathcal M=\{V: V^\top X+X^\top V=0\}$. The orthogonal projection onto it is $\operatorname{Proj}_{T_X\mathcal M}(Y)=(I_n-XX^\top)Y+\tfrac12X(X^\top Y-Y^\top X)$.

The standing assumptions on $F=f+h$ are imposed on all of $\mathbb R^{n\times r}$:

• (i) $f$ is differentiable, and its gradient $\nabla f$ is $L$-Lipschitz;
• (ii) $h$ is convex and $L_h$-Lipschitz.

A point $X\in\mathcal M$ is stationary (Definition 3.3) if

$$0\in\operatorname{grad}f(X)+\operatorname{Proj}_{T_X\mathcal M}\partial h(X),\qquad \operatorname{grad}f(X)=\operatorname{Proj}_{T_X\mathcal M}\nabla f(X),$$

where $\partial h$ is the convex subdifferential.

A retraction $\mathrm{Retr}_X(\xi)$ maps tangent vectors at $X$ back to $\mathcal M$, with $\mathrm{Retr}_X(0)=X$. On the compact manifold $\mathcal M$ every retraction satisfies, for some $M_1,M_2>0$ and all $X\in\mathcal M$, $\xi\in T_X\mathcal M$ (Fact 3.6),

$$\|\mathrm{Retr}_X(\xi)-X\|_F\le M_1\|\xi\|_F,\qquad \|\mathrm{Retr}_X(\xi)-(X+\xi)\|_F\le M_2\|\xi\|_F^2.$$

ManPG (Algorithm 1) takes $X_0\in\mathcal M$, $\gamma\in(0,1)$ and $t>0$. In iteration $k$ it solves the convex subproblem

$$V_k=\operatorname*{argmin}_{V\in T_{X_k}\mathcal M}\ \langle\nabla f(X_k),V\rangle+\frac1{2t}\|V\|_F^2+h(X_k+V).\tag{4.3}$$

It then backtracks $\alpha=1,\gamma,\gamma^2,\dots$ until $F(\mathrm{Retr}_{X_k}(\alpha V_k))\le F(X_k)-\alpha\|V_k\|_F^2/(2t)$, and sets $X_{k+1}=\mathrm{Retr}_{X_k}(\alpha_kV_k)$.

A point $X\in\mathcal M$ is $\varepsilon$-stationary (Definition 5.4) if the solution of (4.3) at $X$ with $t=1/L$ has $\|V\|_F\le\varepsilon/L$. The proof of Lemma 5.2 uses a bound $G$ on $\|\nabla f\|_F$ over $\mathcal M$ and the constants

$$c_0=M_2G+\frac{LM_1^2}{2},\qquad \bar\alpha=\frac{1}{2(c_0+L_hM_2)t}.$$

Formalization targets

Goal: Theorem 5.5

For every run of ManPG:

1. every limit point $\bar X$ of $\{X_k\}$ is stationary;
2. with $t=1/L$, for every $\varepsilon>0$ some

$$k\le\left\lceil\frac{2L\,(F(X_0)-F^*)}{\gamma\bar\alpha\varepsilon^2}\right\rceil$$

has $\|V_k\|_F\le\varepsilon/L$ and $X_k$ is $\varepsilon$-stationary.

Here $F^*$ is the optimal value of (1.1). The constant is the paper's, kept exactly.

Milestones, in the order the proof uses them

• Lemma 5.1: $g(\alpha V_k)-g(0)\le\frac{(\alpha-2)\alpha}{2t}\|V_k\|_F^2$ for $\alpha\in[0,1]$, where $g$ is the objective of (4.3).
• (5.5): $f(\mathrm{Retr}_{X}(\alpha V))-f(X)\le\alpha\langle\nabla f(X),V\rangle+c_0\alpha^2\|V\|_F^2$.
• Lemma 5.2, split into three parts:
  • sufficient decrease for every $0<\alpha\le\min\{1,\bar\alpha\}$;
  • well-definedness of the line search: a run exists from every $X_0$;
  • the run form $\gamma\min\{1,\bar\alpha\}\le\alpha_k\le1$, with $F(X_{k+1})-F(X_k)\le-\frac{\alpha_k}{2t}\|V_k\|_F^2$.
• Lemma 5.3: $V_k=0$ implies $X_k$ is stationary.
• Two displays of the proof of Theorem 5.5:
  • $\|V_k\|_F^2\to0$;
  • the telescoped chain $F(X_0)-F^*>\frac{tK\varepsilon^2}{2}\gamma\bar\alpha$ when $\|V_k\|_F>\varepsilon/L$ for all $k<K$.

Significance

Theorem 5.5 is the paper's main result. It certifies ManPG as a first-order method for nonsmooth problems on the Stiefel manifold with the same $O(\varepsilon^{-2})$ complexity as Riemannian gradient descent in the smooth case. When $h=0$ the bound reduces to the Boumal–Absil–Cartis rate (Remark 5.6). Later proximal methods on matrix manifolds build on this analysis. Lemmas 5.1–5.3 are the reusable steps: descent of the subproblem, sufficient decrease after retraction, and the stopping test as a stationarity certificate.

The result is proved in the paper; it is not formalized anywhere. No proof assistant library contains the convergence theory of a proximal method on a matrix manifold. The mission produces a machine-checked version of the full chain from the subproblem to the iteration bound. Along the way it builds infrastructure that Mathlib lacks: the Frobenius geometry of $\mathbb R^{n\times r}$ as a trace formula, the tangent space and projection of the Stiefel manifold, and optimality conditions for convex problems restricted to a subspace.

Difficulty

The bookkeeping inequalities (Lemma 5.1, (5.5), the decrease estimate, the telescoping) are short computations once the right facts are available. The difficulty lies elsewhere.

• Lemma 5.3 and the limit-point claim need the optimality condition of the subproblem (4.3): a subdifferential sum rule for a convex function restricted to the linear subspace $T_X\mathcal M$, followed by the projection formula. The paper cites this condition rather than proving it.
• The limit-point claim also needs a closedness argument. Subgradients of the Lipschitz function $h$ are bounded by $L_h$, so along a convergent subsequence they have a limit point that is again a subgradient. The projection $X\mapsto\operatorname{Proj}_{T_X\mathcal M}$ must be shown continuous. The paper's proof leaves both steps implicit.
• The well-definedness of the line search requires existence of a minimizer of (4.3), by strong convexity and coercivity on a subspace.
• The descent lemma for $f$ has to be derived from the derivative along lines and the Lipschitz gradient.

A natural first idea is to restate everything for the Riemannian gradient and reuse smooth Riemannian results. That route does not work: $h$ is nonsmooth, and the argument runs in the ambient space through the Euclidean subdifferential.

Formalization scope

• Representation.
  • Matrices are Matrix (Fin n) (Fin r) ℝ.
  • The inner product is trace (Aᵀ * B) and the norm is its square root. No Mathlib matrix norm instance is used.
  • $\mathrm{St}(n,r)$ is the published definition ProjLikeRetr.Stiefel.stiefel.
• Assumptions.
  • $f$ comes with a gradient map gradf, tied to it by derivatives along every line.
  • $\nabla f$ is $L$-Lipschitz in the Frobenius norm, with $L>0$.
  • $h$ is convex and $L_h$-Lipschitz on the whole ambient space.
  • $r\le n$.
• Retraction. The retraction is any map sending tangent vectors at points of $\mathcal M$ into $\mathcal M$, with $\mathrm{Retr}_X(0)=X$ and the bounds (3.1)–(3.2). By Fact 3.6 this covers every retraction; smoothness is never used.
• Constants.
  • $G$, $M_1$, $M_2$, $L$, $L_h$ are parameters, each with its defining hypothesis.
  • $c_0$ and $\bar\alpha$ are the explicit formulas above.
  • $F^*$ is an attained lower bound of $F$ on $\mathcal M$.
• The run. A run of Algorithm 1 is a predicate on sequences $(X_k,V_k,\alpha_k)$. Each $V_k$ minimizes (4.3), $\alpha_k=\gamma^j$ for the least passing $j$, and $X_{k+1}=\mathrm{Retr}_{X_k}(\alpha_kV_k)$.
• The goal's conventions.
  • A limit point is a cluster point of the sequence.
  • "Returns an $\varepsilon$-stationary point within $N$ iterations" means some $k\le N$ passes the stopping test $\|V_k\|_F\le\varepsilon/L$, with $N=\lceil\cdot\rceil$ as Nat.ceil.

Two encodings would trivialize the theorem, and the mission excludes both.

• An unsatisfiable run predicate would make the goal vacuous. The well-definedness milestone asserts that a run exists from every $X_0\in\mathcal M$.
• A projection or stationarity condition that holds trivially would make the first claim empty. Stationarity uses the explicit projection formula and the convex subdifferential on all of $\mathbb R^{n\times r}$.

Lemma 5.2 as printed fixes $\alpha\le\min\{1,\bar\alpha\}$ and asserts the decrease for the accepted iterate. What its proof establishes is three separate facts: decrease at every trial stepsize $\alpha\le\min\{1,\bar\alpha\}$, termination of the line search, and $\alpha_k\ge\gamma\min\{1,\bar\alpha\}$ along a run. The mission states these three facts.

Contributions are welcome at every level: proofs of the milestones, and general lemmas such as the descent lemma for $C^{1,1}$ functions on $\mathbb R^{n\times r}$, the optimality condition of a strongly convex problem on a subspace, and properties of the Stiefel tangent projection. Theorem numbers and pages refer to arXiv:1811.00980v2, the version read for this mission.

Selected references

• S. Chen, S. Ma, A. M.-C. So, T. Zhang, Proximal gradient method for nonsmooth optimization over the Stiefel manifold, SIAM Journal on Optimization 30(1), 2020. https://doi.org/10.1137/18m122457x (arXiv:1811.00980v2: https://arxiv.org/abs/1811.00980)
• N. Boumal, P.-A. Absil, C. Cartis, Global rates of convergence for nonconvex optimization on manifolds, IMA Journal of Numerical Analysis 39(1), 2019. https://doi.org/10.1093/imanum/drx080
• P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244

Motivation

Many stochastic differential equations used in physics, biology and Bayesian sampling are ergodic: their law converges to an invariant measure $\pi$, and quantities of interest are averages $\pi(\varphi)=\int\varphi\,\mathrm d\pi=\lim_{t\to\infty}\mathbb E[\varphi(X_t)]$. Estimating such averages by simulation requires a numerical method whose accuracy does not deteriorate as the simulated time grows. Two obstacles meet here. First, the drifts of interest (the FENE polymer model, Langevin dynamics with polynomial potentials) are not globally Lipschitz, and for such drifts the explicit Euler–Maruyama method with a uniform timestep has moments that blow up as the step tends to zero (Hutzenthaler, Jentzen, Kloeden 2011). Second, standard strong error bounds grow exponentially with the time horizon, which makes them useless for long-time averages.

W. Fang and M. B. Giles (Ann. Appl. Probab. 30 (2020) 526–560) answer both with an adaptive timestep: the step is chosen from the current state, small where the drift is large. On a finite interval they prove strong convergence of order $\tfrac12$; for a class of contractive ergodic SDEs they prove that the moments of the numerical solution and its strong error are bounded uniformly in time. The second result is the subject of this mission. It underlies the paper's multilevel Monte Carlo estimator for invariant measures.

Earlier work on the same problem used tamed schemes, which modify the drift instead of the step: Hutzenthaler, Jentzen, Kloeden 2012 on finite intervals and Sabanis 2016 with a time-uniform rate. An adaptive Euler–Maruyama scheme of a different form, with error control, was shown to converge and to be stable by Lamba, Mattingly, Stuart 2007.

Setting

Let $(\Omega,\mathcal F,\mathbb P)$ carry a filtration $(\mathcal F_t)_{t\ge0}$ and a $d$-dimensional standard Brownian motion $W$ with respect to it. On $\mathbb R^m$ (Euclidean norm $\|\cdot\|$, inner product $\langle\cdot,\cdot\rangle$) consider

$$\mathrm dX_t=f(X_t)\,\mathrm dt+g(X_t)\,\mathrm dW_t,\qquad X_0=x_0,$$

with drift $f:\mathbb R^m\to\mathbb R^m$ and diffusion $g:\mathbb R^m\to\mathbb R^{m\times d}$; matrices carry the Frobenius norm $\|A\|=(\sum_{i,j}A_{ij}^2)^{1/2}$.

Given a timestep function $h:\mathbb R^m\to(0,\infty)$, the adaptive Euler–Maruyama scheme is

$$t_0=0,\ \widehat X_0=x_0,\qquad t_{n+1}=t_n+h(\widehat X_{t_n}),\qquad \widehat X_{t_{n+1}}=\widehat X_{t_n}+f(\widehat X_{t_n})h(\widehat X_{t_n})+g(\widehat X_{t_n})(W_{t_{n+1}}-W_{t_n}).$$

For $t\ge0$ let $\underline t$ be the last grid time not after $t$. The piecewise-constant interpolant is $\overline X_t=\widehat X_{\underline t}$ and the continuous interpolant is $\widehat X_t=\widehat X_{\underline t}+f(\widehat X_{\underline t})(t-\underline t)+g(\widehat X_{\underline t})(W_t-W_{\underline t})$.

The hypotheses are:

• Assumption 7 (dissipative). $f,g$ are locally Lipschitz, and for constants $\alpha,\beta>0$: $\langle x,f(x)\rangle\le-\alpha\|x\|^2+\beta$ and $\|g(x)\|^2\le\beta$.
• Assumption 8 (timestep). $h$ is continuous with values in $(0,h_{\max}]$, and $\langle x,f(x)\rangle+\tfrac12h(x)\|f(x)\|^2\le-\alpha\|x\|^2+\beta$.
• Assumption 9 (contractive). For some $p^*>2$ and $\lambda,\eta>0$: $\langle x-y,f(x)-f(y)\rangle+\tfrac{p^*-1}2\|g(x)-g(y)\|^2\le-\lambda\|x-y\|^2$, $\|g(x)-g(y)\|^2\le\eta\|x-y\|^2$, and $\|f(x)-f(y)\|\le(\gamma(\|x\|^q+\|y\|^q)+\mu)\|x-y\|$ with $\gamma,\mu,q>0$.
• Assumption 3 (refinement). For $\delta\in(0,1]$ and a fixed $T>0$, the refined timestep $h^\delta$ satisfies $\delta\min(T,h(x))\le h^\delta(x)\le\min(\delta T,h(x))$.

Formalization targets

Goal: Theorem 6 (p. 534)

Under Assumption 9, with $g$ bounded, $h$ satisfying Assumption 8 and $h^\delta$ satisfying Assumption 3, for every $p\in(0,p^*]$ there is $C_p$ such that, with $\widehat X$ computed with timestep $h^\delta$,

$$\mathbb E\big[\|\widehat X_t-X_t\|^p\big]\le C_p\,\delta^{p/2}\qquad\text{for all }\delta\in(0,1],\ t\ge0.$$

The constant is fixed before $\delta$ and $t$; uniformity in $t$ is the content of the theorem.

Milestones, in the order the proof uses them

1. Lemma 3 (p. 532): under Assumption 7, $\sup_{t\ge0}\mathbb E\|X_t\|^p<\infty$ for every $p>0$.
2. (45) (p. 554): the weighted one-step inequality bounding $e^{2\alpha t_{n+1}}\|\widehat X_{t_{n+1}}\|^2$ by $e^{2\alpha t_n}\|\widehat X_{t_n}\|^2$ plus explicit drift, noise and martingale terms.
3. (47) (p. 554): its partial-step analogue from $\underline t$ to $t$.
4. §6.3, Step 2 (p. 556): $\mathbb E[\sup_{0\le s\le t}e^{\alpha ps}\|\widehat X_s\|^p]\le2C^4_p\|x_0\|^p+2C^5_pe^{\alpha pt}$ for $p\ge4$, with $C^4_p,C^5_p$ independent of $x_0$ and uniform over the coefficients $f,g$ (given the constants of Assumption 7) and over timestep functions.
5. Theorem 5 (p. 533): under Assumptions 7 and 8, $\mathbb E\|\widehat X_t\|^p<C_p$ and $\mathbb E\|\overline X_t\|^p<C_p$ for all $t\ge0$, with $C_p$ independent of $f$, $g$ (given the constants of Assumption 7) and of $h$.
6. (52) (p. 558): for $p\in(2,p^*]$, with $e_t=\widehat X_t-X_t$ and an explicit function $\widehat L$,

$$\mathbb E\big[e^{\lambda pt/2}\|e_t\|^p\big]\le2\Big(\tfrac{8(p-2)}{p\lambda}\Big)^{p/2-1}\int_0^t\mathbb E\big[\widehat L(\widehat X_s,\overline X_s)^{p/2}\|\widehat X_s-\overline X_s\|^p\big]e^{\lambda ps/2}\,\mathrm ds.$$

The remaining step from (52) to Theorem 6 is a time-uniform bound $\mathbb E\|\widehat X_s-\overline X_s\|^{2p}\le C\delta^p$, obtained as in the finite-time analysis of §6.2.

Significance

Theorem 6 says that the adaptive scheme tracks the true solution with error of order $\delta^{1/2}$ forever, not merely on a fixed window. Combined with ergodicity, it bounds the bias of long-time averages of the scheme uniformly in the averaging horizon, which is what the paper's adaptive multilevel Monte Carlo method for invariant measures (§3) needs. Theorem 5 is of independent use: it shows that the adaptive scheme preserves the time-uniform moment bounds of a dissipative SDE, a property the uniform-step Euler scheme lacks for superlinear drift.

All results here are proved in the source; none is open. To our knowledge none has a machine-checked proof. A complete formalization would give the first verified strong convergence result for an adaptive-step SDE scheme, and the infinite-horizon energy estimates (45)–(47) and the error inequality (52) would be the first verified time-uniform estimates of this kind.

Difficulty

The timestep is random and depends on the state, so the grid times $t_n$ are stopping times rather than fixed numbers, and the number of steps up to time $t$ is random. Standard discrete Grönwall arguments, which iterate over a deterministic grid, do not apply directly; neither does the usual argument that the scheme is an Itô process with adapted, piecewise-constant coefficients, which must be rebuilt for random grids.

The obvious route to a time-uniform bound — a finite-time bound with constant $C_T$ followed by $T\to\infty$ — fails because $C_T$ grows exponentially. Uniformity has to come from an exponential weight ($e^{2\alpha t}$ in (45)–(47), $e^{\lambda pt/2}$ in (52)) that converts dissipation or contractivity into a bound that survives division by the weight, with every constant independent of $t$ and of the timestep function.

Formalization scope

The state space is EuclideanSpace ℝ (Fin m); diffusion values are EuclideanSpace ℝ (Fin m × Fin d), whose norm is the Frobenius norm. Times are in ℝ≥0, grid indices start at $0$, and $x_0$ is deterministic. The grid is defined by recursion; the index $n_t$ is the least $n$ with $t<t_{n+1}$ and equals the junk value $0$ on the event that the grid never passes $t$ (a null event under the hypotheses). Moments are lower Lebesgue integrals ∫⁻ … ‖·‖ₑ ^ p in $[0,\infty]$ with real exponents, never Bochner integrals. A solution on $[0,\infty)$ is a process that solves the SDE on every horizon $[0,T]$, in the sense of the published definition SabanisEuler.Shared.IsSolution. Existential constants are placed before every quantifier they must not depend on: before $t$ in Lemma 3, before $f$, $g$, $h$ and $t$ in Theorem 5, before $f$, $g$, $x_0$, $h$ and $t$ in Step 2, before $\delta$ and $t$ in Theorem 6. A constant chosen after $t$, or a moment that is a Bochner integral of a possibly non-integrable function, would make these statements trivial; both are ruled out. Pages are the journal's printed pages (PDF page + 525).

Two deviations from the printed text are deliberate. Theorem 6 additionally assumes $\|g(x)\|^2\le\beta_g$: its proof invokes Theorem 5, whose Assumption 7 contains this bound, which Assumption 9 does not imply, and the introduction (p. 527) assumes "a bounded and non-degenerate diffusion coefficient". Each $h^\delta$ is assumed measurable. Separately, the printed (47) has $\phi(\widehat X_{\underline t})=\widehat X_{\underline t}+h(\widehat X_{\underline t})f(\widehat X_{\underline t})$ in its last term; the formalized inequality uses $\widehat X_{\underline t}+(t-\underline t)f(\widehat X_{\underline t})$, as the expansion and the source's (48) require. The undefined word "nondegenerate" in Assumption 7 is not encoded.

A full development needs the Itô formula for $e^{ct}\|Y_t\|^p$ applied to Itô processes with random-grid coefficients, the Burkholder–Davis–Gundy inequality, and moment bounds for Brownian increments over stopping-time intervals. These are reusable well beyond this mission. Contributions of any of them, or of proofs of the deterministic inequalities (45) and (47), are welcome.

Selected references

• W. Fang, M. B. Giles, Adaptive Euler–Maruyama method for SDEs with nonglobally Lipschitz drift, Ann. Appl. Probab. 30(2) (2020) 526–560. https://doi.org/10.1214/19-AAP1507
• M. Hutzenthaler, A. Jentzen, P. E. Kloeden, Strong and weak divergence in finite time of Euler's method for SDEs with non-globally Lipschitz coefficients, Proc. R. Soc. A 467 (2011) 1563–1576. 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) (2012) 1611–1641. https://doi.org/10.1214/11-AAP803
• S. Sabanis, Euler approximations with varying coefficients: the case of superlinearly growing diffusion coefficients, Ann. Appl. Probab. 26(4) (2016) 2083–2105. https://doi.org/10.1214/15-AAP1140
• H. Lamba, J. C. Mattingly, A. M. Stuart, An adaptive Euler–Maruyama scheme for SDEs: convergence and stability, IMA J. Numer. Anal. 27(3) (2007) 479–506. https://doi.org/10.1093/imanum/drl032
• D. J. Higham, X. Mao, A. M. Stuart, Strong convergence of Euler-type methods for nonlinear stochastic differential equations, SIAM J. Numer. Anal. 40(3) (2002) 1041–1063. https://doi.org/10.1137/S0036142901389530