Dynamical Systems

Motivation

A forward–backward stochastic differential equation (FBSDE) couples a forward diffusion $X$ with a backward equation for a pair $(Y,Z)$ whose terminal value depends on $X_T$. FBSDEs are the probabilistic form of quasilinear parabolic PDEs and appear in stochastic control (the stochastic maximum principle), in mathematical finance (hedging with large investors, stochastic differential utility) and in mean-field games. Their solvability over an arbitrary horizon is delicate: the coupling can make a solution exist only on short time intervals.

Ma, Wu, Zhang and Zhang (arXiv:1110.4658v2, Ann. Appl. Probab. 25 (2015)) reduce well-posedness of a general one-dimensional FBSDE to the behaviour of two scalar dominating ODEs: when these have solutions that stay bounded on $[0,T]$, the FBSDE has a regular decoupling field and a unique solution. Section 5.1 of the paper tests this programme on the simplest class, the linear FBSDE with constant coefficients, and obtains necessary and sufficient conditions. The authors describe these as setting the "limits" for the solvability of general FBSDEs.

Earlier approaches each covered part of the picture: the method of contraction mappings for small time (Antonelli 1993, MR1233625), the four-step scheme for Markovian FBSDEs with regular coefficients (Ma, Protter, Yong 1994, MR1262970), and the method of continuation under monotonicity conditions (Hu, Peng 1995, MR1355060; Peng, Wu 1999, MR1675098; later Yong 1997, MR1440146). The unified approach of the paper contains these as special cases.

Setting

Let $b_1,b_2,b_3,\sigma_1,\sigma_2,f_1,f_2,f_3,h$ be real numbers and consider the linear FBSDE (4.1)

$$\mathcal X_t=1+\int_0^t(b_1\mathcal X+b_2\mathcal Y+b_3\mathcal Z)\,ds+\int_0^t(\sigma_1\mathcal X+\sigma_2\mathcal Y+\sigma_3\mathcal Z)\,dB,\qquad \mathcal Y_t=h\mathcal X_T+\int_t^T(f_1\mathcal X+f_2\mathcal Y+f_3\mathcal Z)\,ds-\int_t^T\mathcal Z\,dB,$$

in Case 1, $\sigma_3=0$. Then the two dominating ODEs coincide and become the scalar backward equation

$$y_t=h+\int_t^T F(y_s)\,ds,\qquad t\in[0,T], \tag{5.3}$$

with the cubic

$$F(y)=f_1+[f_2+b_1+\sigma_1f_3]\,y+[b_2+f_3\sigma_2+b_3\sigma_1]\,y^2+\sigma_2b_3\,y^3 . \tag{5.4}$$

In the Appendix's notation (A.3), $F(y)=f_1+a_1y+a_2y^2+a_3y^3$ with $a_1=f_2+b_1+\sigma_1f_3$, $a_2=b_2+f_3\sigma_2+b_3\sigma_1$, $a_3=\sigma_2b_3$.

A solution on $[0,T]$ of $y_t=h+\int_t^TG(s,y_s)\,ds$ is a function $y$ such that, for every $t\in[0,T]$, $s\mapsto G(s,y_s)$ is integrable on $[t,T]$ and the equation holds at $t$. A bounded solution additionally has $\sup_{[0,T]}|y|<\infty$. In Lean the coefficients form the structure UnifiedFBSDE.Cubic.Coeffs, $F$ is Coeffs.F, and the predicates are IsSolution and IsBoundedSolution.

Formalization targets

Goal: Theorem 5.3

$$\Big(\forall T>0,\ \exists\,y \text{ bounded solution of (5.3) on }[0,T]\Big)\iff \begin{cases} \text{(i) } F(h)\ge0 \text{ and } F(\lambda)=0 \text{ for some }\lambda\ge h,\ \text{or}\\ \text{(ii) } F(h)\le0 \text{ and } F(\lambda)=0 \text{ for some }\lambda\le h,\ \text{or}\\ \text{(iii) } \sigma_2b_3=0 \text{ and } b_2+f_3\sigma_2+b_3\sigma_1=0. \end{cases}$$

Milestones

1. Lemma 5.1: comparison for backward ODEs. Between a bounded sub-solution and a bounded super-solution, (5.1) has a unique solution.
2. Remark 5.2: a checkable sufficient condition for hypothesis (iv) of Lemma 5.1.
3. Sufficiency of (i), (ii): the solution stays in $[h,\lambda]$ (resp. $[\lambda,h]$).
4. (5.5): under (iii), (5.3) is linear and has a bounded solution.
5. (A.4): if $a_3>0$ and $F$ has no zero in $[h,\infty)$, then $F(y)\ge\varepsilon(y-y_1)^3$ on $[h,\infty)$ for some $\varepsilon>0$, $y_1<h$.
6. (A.6): the explicit comparison solution $\tilde y_t-y_1=(2\varepsilon(t-T)+(h-y_1)^{-2})^{-1/2}$ and its blow-up time $T-1/(2\varepsilon(h-y_1)^2)$.
7. Blow-up by comparison: a continuous $G\ge\varepsilon(y-y_1)^3$ on $[h,\infty)$ admits no solution on $[0,T]$ when $T>1/(2\varepsilon(h-y_1)^2)$.
8. Case 2: if $a_3=0$, $a_2>0$, $F(h)>0$ and $F$ has no zero above $h$, then $F(y)\ge\varepsilon(y-y_1)^2$ on $[h,\infty)$ and (5.3) has no solution for $T$ large.

Companion: Theorem 5.4

For a fixed horizon $T$: (i) $\sigma_2b_3<0$ or $F(h)=0$; (ii) $F(h)>0$, $\sigma_2b_3\le\varepsilon$, $a_2\le\varepsilon$; (iii) $F(h)<0$, $\sigma_2b_3\le\varepsilon$, $a_2\ge-\varepsilon$, with $\varepsilon=\varepsilon(T)$ small. Each guarantees a bounded solution on $[0,T]$.

Significance

Theorem 5.3 turns the existence of a global bounded solution of the dominating ODE into a finite check on a cubic polynomial: the sign of $F(h)$, the location of a real root, and two coefficient identities. Through the paper's main construction, a bounded solution yields a uniformly Lipschitz decoupling field, and hence well-posedness of the linear FBSDE on any horizon. When none of (i)–(iii) holds, the dominating ODE explodes in finite time. This is the sense in which the paper says the constant-coefficient results "more or less set the 'limits'" for the solvability of general FBSDEs: the conditions it later imposes on random coefficients (§5.2, §7) are modelled on the cases (i)–(iii).

The result is proved in the paper: sufficiency on p. 21, necessity in the Appendix (pp. 46–47). To our knowledge none of it is machine-checked. A formalization produces a reusable comparison theorem for scalar backward integral equations with Lipschitz-on-a-band nonlinearities (Lemma 5.1), explicit finite-time blow-up criteria for polynomial ODEs, and a complete, checked classification of global solvability for the cubic Riccati-type equation (5.3).

Difficulty

Sufficiency rests on Lemma 5.1, which requires Carathéodory existence and uniqueness for an equation that is only Lipschitz on a time-dependent band, followed by an integrating-factor comparison argument. Mathlib's Picard–Lindelöf and Gronwall tools are stated for forward equations with continuous right-hand sides, so they need adaptation.

Necessity is a case analysis whose obvious version fails at two points. First, one cannot simply bound $F$ below by $a_3(y-y_1)^3$ using the smallest real root: the intermediate inequality (A.5) as printed points the wrong way for some root orderings, and the correct bound uses the largest root or an infimum over $[h,\infty)$. Second, the blow-up step compares a solution of (5.3) with an explicit exploding solution. This needs the solution to stay above $h$ for the whole interval, which in turn needs continuity of the right-hand side. For a discontinuous right-hand side the comparison fails.

Formalization scope

Time is real, with $0<T$ and $t\in[0,T]$. Solutions are functions $\mathbb R\to\mathbb R$ whose values outside $[0,T]$ are irrelevant. The integral $\int_t^T$ is Mathlib's interval integral. "For arbitrary $T$" is $\forall T>0,\ \exists y$, with the universal quantifier outside. "A zero point in $[h,\infty)$" is $\exists\lambda\ge h,\ F(\lambda)=0$.

Pinned readings, all disclosed in the items:

• Lemma 5.1 adds $y^1\le y^2$ on $[0,T]$ (the lemma is false without it), $L\ge0$, and integrability of $c^1,c^2$. Its $\alpha$ ranges over measurable functions with $|\alpha|\le L$, and $F^i$ is measurable on $\mathbb R\times\mathbb R$.
• The blow-up milestone assumes $G$ continuous.
• In Theorem 5.4(ii)–(iii), $\varepsilon$ is chosen after $T$, $h$, $f_1$ and $a_1$, the data its proof uses.
• (A.5) is not stated.

Trivializing formalizations are ruled out. The solution predicate carries integrability of the integrand, so Lean's junk value $0$ for a non-integrable integral cannot make an arbitrary $y$ with $y_t=h$ a solution. The goal assumes neither a zero of $F$ nor a blow-up: both are proved in the milestones. Lemma 5.1's uniqueness is over solutions in the band.

The needed infrastructure is scalar ODE theory on Mathlib: existence for Lipschitz Carathéodory equations, differentiation of $t\mapsto\int_t^T g$, comparison of sub- and super-solutions, and elementary real-root facts for cubics. The comparison lemma and the blow-up lemma are reusable beyond this mission. Contributions of either the sufficiency or the necessity chain are welcome independently.

Selected references

• J. Ma, Z. Wu, D. Zhang, J. Zhang, On well-posedness of forward–backward SDEs—a unified approach, Ann. Appl. Probab. 25(4):2168–2214, 2015. https://arxiv.org/abs/1110.4658 , https://doi.org/10.1214/14-AAP1046
• F. Antonelli, Backward–forward stochastic differential equations, Ann. Appl. Probab. 3(3):777–793, 1993. MR1233625, https://mathscinet.ams.org/mathscinet-getitem?mr=1233625
• J. Ma, P. Protter, J. Yong, Solving forward–backward stochastic differential equations explicitly—a four step scheme, Probab. Theory Related Fields 98:339–359, 1994. MR1262970, https://mathscinet.ams.org/mathscinet-getitem?mr=1262970
• Y. Hu, S. Peng, Solution of forward–backward stochastic differential equations, Probab. Theory Related Fields 103:273–283, 1995. MR1355060, https://mathscinet.ams.org/mathscinet-getitem?mr=1355060
• S. Peng, Z. Wu, Fully coupled forward–backward stochastic differential equations and applications to optimal control, SIAM J. Control Optim. 37(3):825–843, 1999. MR1675098, https://mathscinet.ams.org/mathscinet-getitem?mr=1675098
• J. Yong, Finding adapted solutions of forward–backward stochastic differential equations: method of continuation, Probab. Theory Related Fields 107:537–572, 1997. MR1440146, https://mathscinet.ams.org/mathscinet-getitem?mr=1440146

Motivation

Nesterov's accelerated gradient method minimizes a convex function $f$ with $L$-Lipschitz gradient at the rate $O(1/k^2)$, which is optimal among first-order methods. For a $\mu$-strongly convex $f$ the method with the generic momentum coefficient $(k-1)/(k+2)$ does not exploit the strong convexity: Su, Boyd and Candès show in §4.2 of arXiv:1503.01243 that its rate stays polynomial. Linear convergence $O((1-\sqrt{\mu/L})^k)$ is available with the momentum $(\sqrt L-\sqrt\mu)/(\sqrt L+\sqrt\mu)$, but this requires knowing $\mu$, which is rarely available in practice.

Restarting is the practical remedy. O'Donoghue and Candès (2013) proposed gradient restarting: reset the momentum whenever the objective increases. It is observed to recover linear convergence, but no rate was proved for it. Section 5 of Su, Boyd and Candès proposes a variant, speed restarting, which resets the momentum when the speed of the iterates stops increasing, and proves a linear rate for its continuous-time limit. This mission formalizes that result, Theorem 10 of the paper, and the lemmas it rests on.

Setting

Write $\mathbb R^n$ with the Euclidean norm. A function $f:\mathbb R^n\to\mathbb R$ is in $\mathcal F_L$ if it is convex and continuously differentiable with $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$. It is in $\mathcal S_\mu$ if it is continuously differentiable and $f(x)-\mu\|x\|^2/2$ is convex. The class $\mathcal S_{\mu,L}=\mathcal F_L\cap\mathcal S_\mu$ with $0<\mu\le L$ is the standing assumption of the whole mission. A minimizer is written $x^\star$ and $f^\star=f(x^\star)$; the ratio $L/\mu$ is the condition number.

The Nesterov ODE is

$$\ddot X(t)+\frac3t\dot X(t)+\nabla f(X(t))=0,\qquad X(0)=x_0,\ \dot X(0)=0, \tag{3}$$

the continuous-time limit of Nesterov's scheme with step size tending to zero. The paper's Theorem 1 shows it has a unique solution in $C^2((0,\infty))\cap C^1([0,\infty))$. In Lean a solution is a pair $(X,V)$ with $V=\dot X$ (IsSolution f 3 x₀ X V).

The speed restarting time of the solution from $x_0$ is

$$T=T(x_0;f)=\sup\Bigl\{t>0:\ \forall u\in(0,t),\ \frac{\mathrm d\|\dot X(u)\|^2}{\mathrm du}>0\Bigr\},$$

the first time at which the speed $\|\dot X\|$ decreases (restartTime; the set is restartSet).

The speed restarted ODE (29) replaces $3/t$ by $3/t_{\mathrm{sr}}$, where $t_{\mathrm{sr}}=t-\tau$ is the time since the latest restart $\tau$. Its solution $X^{\mathrm{sr}}$ starts at $x_0$, follows (3) from $x_0$ for time $T_1=T(x_0;f)$, then follows (3) from $X^{\mathrm{sr}}(T_1)$ for time $T_2=T(X^{\mathrm{sr}}(T_1);f)$, and so on. If a restart point is a minimizer the trajectory stays there. In Lean this is the predicate IsSpeedRestarted f x₀ Xsr.

Formalization targets

Goal: Theorem 10

There are positive constants $c_1,c_2$, depending only on $L/\mu$, such that for every $f\in\mathcal S_{\mu,L}$, every $x_0$ and every $t\ge0$,

$$f(X^{\mathrm{sr}}(t))-f^\star\le\frac{c_1L\|x_0-x^\star\|^2}2\,e^{-c_2t\sqrt L}.$$

The constants are left unspecified, so the goal survives improvements of them.

Milestones

For one unrestarted solution $X$ of (3), with $M(t)=\sup_{u\in(0,t]}\|\dot X(u)\|/u$:

• Lemma 11. For $t<\sqrt{12/L}$: $M(t)\le\|\nabla f(x_0)\|/(4(1-Lt^2/12))$.
• (30). For $0<t<\sqrt{12/L}$: $\bigl|\,\|\dot X(t)\|-\tfrac t4\|\nabla f(x_0)\|\,\bigr|\le L\|\nabla f(x_0)\|t^3/(48(1-Lt^2/12))$.
• Lemma 25. If $x_0\ne x^\star$: $T(x_0,f)\ge 4/(5\sqrt L)$.
• Descent display. $\dfrac{\mathrm df(X(t))}{\mathrm dt}=-\dfrac3t\|\dot X\|^2-\dfrac12\dfrac{\mathrm d\|\dot X\|^2}{\mathrm dt}\le0$ for $t\le T$.
• Lemma 12. For a universal $C>0$: $f(X(T))-f^\star\le(1-C\mu/L)(f(x_0)-f^\star)$.
• Lemma 13. For a universal $\tilde C$: $T\le 4\exp(\tilde CL/\mu)/(5\sqrt L)$.

Significance

Theorem 10 is a linear convergence guarantee for a momentum method that does not need $\mu$: the restart rule only watches the speed. The paper presents it as a new result; gradient restarting has no comparable theorem. It also gives a framework for analyzing restart rules: each restart decreases the gap by a factor depending on $L/\mu$ (Lemma 12), and restarts happen at a rate bounded below (Lemmas 13 and 25). Section 5.3 of the paper reports that the discrete analogue of the scheme (Algorithm 1) converges linearly in experiments.

The results are proved in the paper, but not formalized anywhere to our knowledge; the platform has no statement about restarting the Nesterov ODE. The formal work is the full proof, in particular the analysis of (3) near its singular point $t=0$. Sharper constants are of interest: the paper conjectures that $T=O(\sqrt L/\mu)$ for a large class of $f$, which would improve $c_2$, and the generalization to friction $r/t$ with $r>3$ mentioned after Theorem 10 is a natural further target.

Difficulty

The ODE (3) is singular at $t=0$, so the standard Picard–Lindelöf theory does not apply there, and the small-time estimates (Lemma 11, (30), Lemma 25) must control the solution uniformly up to $t=0$, where the friction coefficient $3/t$ is unbounded. Lemma 11 bounds a supremum by a quantity that involves the same supremum; this argument needs a separate proof that the supremum is finite.

The speed restarting time is defined as a supremum, and neither $T>0$ nor $T<\infty$ follows from the definition. The restarted trajectory is assembled from infinitely many segments, and the number of restarts before time $t$ needs a lower bound. The obvious route through the $O(1/t^2)$ rate of the unrestarted ODE gives only a polynomial rate, because it does not use strong convexity in a way that survives the restarts.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\nabla f$ is Mathlib's gradient, $L$ is an NNReal, and $\mathcal S_\mu$ is the paper's literal definition. The classes $\mathcal F_L$, $\mathcal S_{\mu,L}$ and the solution predicate of (3) come from the series' shared definitions (NesterovODE.WellPosed.Setting, NesterovODE.StrongCvx.Setting); the speed restarting time and the restarted trajectory sit in this mission's Setting definition, namespace NesterovODE.Restart.

Conventions the formalization commits to:

• Solutions of (3) are pairs $(X,V)$, quantified over: every solution in the regularity class of Theorem 1 is covered. Values at negative times are unconstrained.
• $\tfrac12\mathrm d\|\dot X\|^2/\mathrm du$ is written as $\langle V(u),-\tfrac3uV(u)-\nabla f(X(u))\rangle$, its value along a solution.
• $M(t)$ is not defined; Lemma 11 is stated as a bound on every $\|\dot X(u)\|/u$, $u\in(0,t]$.
• Lean's sSup is $0$ on an empty or unbounded set. Lemma 25 is stated as membership of $4/(5\sqrt L)$ in the set defining $T$, and Lemma 13 as a bound on every element of that set, so neither can hold through this junk value.
• The constants of Lemmas 12 and 13 are chosen before the dimension, $f$, $\mu$, $L$, $x_0$ and the trajectory; those of Theorem 10 are functions of $L/\mu$ chosen in the same position. Choosing them after $f$ would trivialize the statements and is ruled out.
• Lemmas 11, 12, 13, 25, (30) and the descent display carry the standing assumption $f\in\mathcal S_{\mu,L}$; Lemmas 12, 13, 25 also carry $x_0\ne x^\star$, the paper's convention in §5. Theorem 10 holds for every $x_0$.
• The leftmost "$0\le$" of (30) is stated for $0<t\le\sqrt{6/L}$, the range on which it is true; the page writes it for all $t<\sqrt{12/L}$.
• The restarted trajectory stays at a minimizer once it reaches one. Restart times tending to infinity is not assumed: it follows from Lemmas 25 and 13.

A complete development needs the analysis of (3) at $t=0$ (also the subject of mission I of this series), monotonicity arguments from derivative signs, and properties of strongly convex functions with Lipschitz gradient. The last two are reusable beyond this mission. Proofs of any milestone, and statements with explicit constants, are welcome.

Selected references

• W. Su, S. Boyd, E. J. Candès, A Differential Equation for Modeling Nesterov's Accelerated Gradient Method: Theory and Insights, arXiv:1503.01243v2, 2015; J. Mach. Learn. Res. 17(153):1–43, 2016. https://arxiv.org/abs/1503.01243
• B. O'Donoghue, E. J. Candès, Adaptive Restart for Accelerated Gradient Schemes, Foundations of Computational Mathematics 15:715–732, 2015. https://doi.org/10.1007/s10208-013-9150-3
• Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Mathematics Doklady 27:372–376, 1983.
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9

Motivation

Accelerated gradient methods minimize smooth convex functions with a characteristic momentum term. Su, Boyd, and Candès identified a continuous-time differential equation whose trajectories model that acceleration. The equation replaces an iteration index by continuous time and makes the effects of damping visible. This mission concerns the paper's strongly convex regime: the function has curvature everywhere, yet the ODE with damping proportional to $1/t$ is not simply a linear-rate method. Theorem 8 quantifies the faster polynomial rate that the authors establish when the damping parameter is large enough.

The paper first treats the coefficient $3/t$, obtaining an inverse-square objective bound. In §4 it replaces $3$ by $r$, and in §4.3 it combines larger damping with strong convexity. The result gives a family of exponents $\alpha$ rather than a single preferred exponent. The rate reaches $t^{-2r/3}$ at the end of the allowed range. The paper also explains that simply raising $r$ does not automatically improve every finite-time bound, because its constant can grow with $r$.

Setting

The state space is Euclidean $\mathbb R^n$. A function belongs to $\mathcal F_L$ when it is convex, continuously differentiable, and its gradient is $L$-Lipschitz for some $L>0$. It belongs to $\mathcal S_\mu$ when it is continuously differentiable and $x\mapsto f(x)-\mu\|x\|^2/2$ is convex. The class $\mathcal S_{\mu,L}$ is their intersection. For this mission $\mu>0$. A point $x^\star$ is any global minimizer, and $f^\star=f(x^\star)$.

Given an initial point $x_0$, a damping parameter $r$, and time $t>0$, the ODE trajectory satisfies

$$\ddot X(t)+\frac r t\dot X(t)+\nabla f(X(t))=0, \qquad X(0)=x_0,\quad \dot X(0)=0.$$

The velocity $V$ records $\dot X$. The regularity asserted is $X\in C^2((0,\infty))\cap C^1([0,\infty))$. The paper writes “the solution” and says an earlier existence argument applies to general $r$; the formal statements quantify over every trajectory satisfying the ODE and initial conditions. This captures the rate claim without identifying functions at irrelevant negative times.

Two energy functions organize the chapter. The first, $E_5(t)$, weights the objective gap by $2t^2/(r-1)$ and adds $(r-1)\|X(t)+tV(t)/(r-1)-x^\star\|^2$. The second, $E_8(t;\alpha)$, weights the gap by $t^\alpha$ and adds $((2r-\alpha)^2t^{\alpha-2}/8)\|X(t)+2tV(t)/(2r-\alpha)-x^\star\|^2$. The threshold $t_\alpha$ is $\sqrt{(\alpha-2)(2r-\alpha)/(2\mu)}$ for $\alpha>2$. These are the paper's objects in §4.1 and §4.3, not alternate energies chosen for ease of formalization.

Formalization targets

Theorem 5: high-friction baseline

For $r>3$, the paper proves both a pointwise inverse-square estimate and a bound on accumulated weighted error:

$$f(X(t))-f^\star\leq\frac{(r-1)^2\|x_0-x^\star\|^2}{2t^2}, \qquad \int_0^\infty t(f(X(t))-f^\star)\,dt \leq\frac{(r-1)^2\|x_0-x^\star\|^2}{2(r-3)}.$$

Its energy derivative inequality (18) is an earlier milestone. Equation (24) gives the integrated bound for $E_8$ at and after $t_\alpha$, and equation (26) bounds the energy at that threshold. Those two displays are additional milestones. Their full statements, including the intermediate inequalities, are retained in Lean.

Theorem 8: strongly convex rate

For every $r,\alpha$ with $2\leq\alpha\leq2r/3$, there is a constant $C=C(r,\alpha)$ such that

$$f(X(t))-f^\star\leq \frac{C\|x_0-x^\star\|^2}{\mu^{(\alpha-2)/2}t^\alpha} \qquad(t>0).$$

The constant does not depend on $n$, $L$, $\mu$, $f$, the minimizer, initial point, chosen solution, or time. At $\alpha=2$ the claim includes $r=3$; the threshold arguments used for $\alpha>2$ are not imposed on that boundary case.

Significance

The theorem says how curvature and damping change the continuous-time objective rate. It separates the exponent, which is set by $r$ and $\alpha$, from the explicit dependence on strong convexity, $\mu^{-(\alpha-2)/2}$. The baseline Theorem 5 is also useful independently: its weighted integral estimate records more than an $O(t^{-2})$ pointwise statement. The paper uses these continuous-time estimates to motivate comparisons with generalized discrete Nesterov schemes Su, Boyd, and Candès, §4.

This result is proved in the cited paper. The work here is to state its hypotheses, energy identities, and rate in Lean so that the established argument can be checked. The definitions of smooth and strongly convex classes, the singular-time solution predicate, and the calculus of real-power energies are reusable in other continuous-time optimization results. No machine-checked proof of these newly drafted statements is claimed by this proposal.

Difficulty

At $t=0$ the damping coefficient $r/t$ is singular, so a statement that applies ordinary second-order ODE calculus across zero would miss the actual boundary condition. Away from zero, the ordinary inverse-square energy does not by itself deliver the stronger exponents of Theorem 8. The stronger energy has real powers of $t$ and its derivative contains terms with different signs. Strong convexity controls some terms only after the threshold $t_\alpha$; the early-time and late-time regimes therefore have different estimates. The argument must also cover real exponents throughout $[2,2r/3]$, including the endpoint $\alpha=2$.

Formalization scope

Lean uses EuclideanSpace ℝ (Fin n) for $\mathbb R^n$, with any natural number $n$. The function classes follow the literal definitions on page 5: convexity, continuous differentiability, a Lipschitz gradient with positive constant $L$, and convexity of $f-\mu\|\cdot\|^2/2$. The rate assumes $\mu>0$, implicit in the paper's denominator and in $t_\alpha$. A minimizer is supplied as a point satisfying $f(x^\star)\leq f(y)$ for every $y$; it is not assumed to be a special optimizer returned by a choice function.

The ODE predicate includes the initial data, a right derivative for $X$ at zero, right continuity of $V$ at zero, and derivatives of both functions for positive time. It says nothing about negative time. Theorem 5 explicitly asserts integrability on $(0,\infty)$ before bounding its integral, preventing the default value of a nonintegrable Bochner integral from satisfying the statement. Real powers are used only with positive bases. Every appearance of $E_5$ is under $r>1$, and every use of $E_8$ in a milestone is under $\alpha>2$ and $\alpha\leq2r/3$, so its denominators are nonzero.

In the goal, $C$ is existentially quantified before the dimension, function, curvature and smoothness constants, trajectory, and time. A constant selected separately for each function or time would weaken Theorem 8 and is excluded. Contributions establishing the energy derivatives, the improper integral, the threshold estimates, and the real-exponent induction are all within scope. The statement of Theorem 8 keeps the paper's full exponent range even if some parts demand substantial new calculus support.

Selected references

• Weijie Su, Stephen Boyd, and Emmanuel J. Candès, A Differential Equation for Modeling Nesterov's Accelerated Gradient Method: Theory and Insights, Journal of Machine Learning Research 17(153), 2016; arXiv:1503.01243v2, cited here by preprint pages 5, 12–13, and 17–19.

Motivation

Nesterov's accelerated gradient method (Nesterov, 1983) minimizes a smooth convex function $f$ with the update

$$x_k=y_{k-1}-s\nabla f(y_{k-1}),\qquad y_k=x_k+\frac{k-1}{k+2}(x_k-x_{k-1}),$$

and, for step size $s\le 1/L$, attains $f(x_k)-f^\star\le 2\|x_0-x^\star\|^2/(s(k+1)^2)$. The rate $O(1/k^2)$ is optimal among first-order methods, yet the classical proof proceeds by an "estimate sequence" argument that offers little insight into why the momentum coefficient $(k-1)/(k+2)$ works.

Su, Boyd and Candès (arXiv:1503.01243, J. Mach. Learn. Res. 17, 2016) showed that, as $s\to0$, the iterates track the solution of the second-order ordinary differential equation

$$\ddot X+\frac3t\dot X+\nabla f(X)=0,\qquad X(0)=x_0,\ \dot X(0)=0,$$

under the time identification $t\approx k\sqrt s$. Their Theorem 3 is the continuous-time counterpart of Nesterov's rate. Its short proof by an energy (Lyapunov) function became the template for a large literature on continuous-time models of accelerated methods, including Wibisono, Wilson and Jordan's variational perspective (PNAS 2016) and Attouch, Chbani, Peypouquet and Redont's analysis of the damped system $\ddot x+\frac\alpha t\dot x+\nabla\Phi(x)=0$ (Math. Program. 2018).

This mission formalizes Theorem 3 and the three steps of its proof.

Setting

Let $n\ge0$ and let $\mathbb R^n$ carry the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. For $f:\mathbb R^n\to\mathbb R$ differentiable, $\nabla f$ is its gradient.

• For $L>0$, the class $\mathcal F_L$ consists of the convex, continuously differentiable $f$ with $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ for all $x,y$. The class $\mathcal F_\infty$ is $\bigcup_{L>0}\mathcal F_L$.
• A minimizer $x^\star$ is any point with $f(x^\star)\le f(y)$ for all $y$, and $f^\star=f(x^\star)$.
• A solution of the ODE (3) with initial point $x_0$ is a curve $X$ on $[0,\infty)$, twice continuously differentiable on $(0,\infty)$ and continuously differentiable on $[0,\infty)$, with $X(0)=x_0$, $\dot X(0)=0$, and $\ddot X(t)+\frac3t\dot X(t)+\nabla f(X(t))=0$ for every $t>0$. The damping coefficient $3/t$ is singular at $t=0$; the paper's Theorem 1 shows that a unique such solution exists for every $f\in\mathcal F_\infty$.
• The energy along a solution is

$$\mathcal E(t)=t^2\big(f(X(t))-f^\star\big)+2\Big\|X(t)+\frac t2\dot X(t)-x^\star\Big\|^2 .$$

In the Lean development these are IsFL, IsFinfty, IsSolution f 3 x₀ X V and energy f xstar X V t, in the namespace NesterovODE.Rate, where V is the velocity $\dot X$.

Formalization targets

Goal: Theorem 3 (p. 7)

For every $f\in\mathcal F_\infty$, every minimizer $x^\star$, every $x_0$ and every solution $X$ of (3),

$$f(X(t))-f^\star\le\frac{2\|x_0-x^\star\|^2}{t^2}\qquad\text{for all }t>0.$$

Milestones (proof of Theorem 3, pp. 7–8)

1. Derivative of the energy. For $t>0$,

$$\dot{\mathcal E}=2t(f(X)-f^\star)+t^2\langle\nabla f(X),\dot X\rangle+4\Big\langle X+\frac t2\dot X-x^\star,\frac32\dot X+\frac t2\ddot X\Big\rangle .$$

2. The energy is nonincreasing. Using the ODE,

$$\dot{\mathcal E}=2t(f(X)-f^\star)+4\Big\langle X-x^\star,-\frac t2\nabla f(X)\Big\rangle=2t(f(X)-f^\star)-2t\langle X-x^\star,\nabla f(X)\rangle\le0 .$$

3. The bound chain. $\mathcal E$ is nonincreasing on $[0,\infty)$ and, for $t>0$,

$$f(X(t))-f^\star\le\frac{\mathcal E(t)}{t^2}\le\frac{\mathcal E(0)}{t^2}=\frac{2\|x_0-x^\star\|^2}{t^2}.$$

Significance

Theorem 3 is the statement that makes the ODE a faithful model of Nesterov's scheme at the level of rates: under $t\approx k\sqrt s$, the bound (7) reproduces the discrete bound (6) with the same constant 2. The paper also shows that the constant cannot be improved (p. 8). The energy $\mathcal E$ is the continuous analogue of the potential used in discrete proofs, and the same template, with other weights, gives the paper's later results on the generalized damping $r/t$ and on strongly convex objectives.

The result is proved in the paper. As far as the platform and Mathlib are concerned it is not formalized: Mathlib has the calculus (derivatives of inner products and norms along curves, the first-order characterization of convexity, monotonicity from a sign of the derivative) but no statement about this ODE. A machine-checked proof establishes the Lyapunov argument for the singular-at-zero system, including the endpoint $t=0$ where only one-sided regularity is available, and supplies reusable lemmas for the other missions of this series and for formalizations of inertial dynamics with vanishing damping.

Difficulty

The algebra is short; the care lies in the analytic bookkeeping that the paper leaves implicit.

• The energy is defined through $f\circ X$ and $\|X+\frac t2\dot X-x^\star\|^2$, so its derivative needs the chain rule for a $C^1$ function along a differentiable curve and the derivative of a squared norm of a curve.
• The ODE holds only for $t>0$ and the coefficient $3/t$ blows up at $0$. Monotonicity of $\mathcal E$ on the closed half-line therefore needs right-continuity of $\mathcal E$ at $0$, which follows from right-continuity of $X$ and $\dot X$ there, together with $t\dot X(t)\to0$; the derivative argument alone gives monotonicity only on $(0,\infty)$.
• The sign of $\dot{\mathcal E}$ needs the first-order inequality $f(x^\star)\ge f(X)+\langle\nabla f(X),x^\star-X\rangle$ for a differentiable convex function.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\nabla f$ is Mathlib's gradient f. $f\in\mathcal F_L$ is 0 < L ∧ ConvexOn ℝ Set.univ f ∧ ContDiff ℝ 1 f ∧ LipschitzWith L (gradient f) with L : NNReal.
• A solution is encoded as a pair of curves $(X,V)$: $X(0)=x_0$, $V(0)=0$, $X$ has right derivative $V(0)$ at $0$, $V$ is right-continuous at $0$, and for every $t>0$, $X$ has derivative $V(t)$ and $V$ has derivative $-\frac3tV(t)-\nabla f(X(t))$. For continuous $\nabla f$ this is exactly the paper's regularity class $C^2((0,\infty))\cap C^1([0,\infty))$ with the ODE and the initial conditions. Values of $X$ for $t<0$ are unconstrained and never used.
• The paper states Theorem 3 for "the unique global solution". The Lean statements quantify over every solution and every minimizer, which by Theorem 1 is the same statement and does not depend on Theorem 1 (formalized in a separate mission of this series).
• No hypothesis beyond the paper's is added. The Lipschitz constant is part of $\mathcal F_\infty$ and is kept although the proof of Theorem 3 does not use it quantitatively.
• The bound is stated for $t>0$ only. At $t=0$ the right-hand side $2\|x_0-x^\star\|^2/0$ is $0$ in Lean, and the inequality would be false.
• The derivative statements use HasDerivAt rather than deriv, so no derivative silently takes the default value $0$; the solution predicate is satisfiable (for $f(x)=\|x\|^2/2$, $x_0=0$, the zero curve is a solution), so the goal is not vacuous.

Contributions welcome: proofs of the three milestones and of the goal; general lemmas on the derivative of $t\mapsto f(X(t))$ and $t\mapsto\|X(t)+\frac t2V(t)-x^\star\|^2$; and the first-order convexity inequality in gradient form, which the strongly convex and generalized-damping missions of this series also need.

Selected references

• 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(153):1–43, 2016; cited from arXiv:1503.01243v2, 2015. https://arxiv.org/abs/1503.01243
• Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Mathematics Doklady 27(2):372–376, 1983.
• A. Wibisono, A. C. Wilson, M. I. Jordan, A variational perspective on accelerated methods in optimization, Proc. Natl. Acad. Sci. 113(47):E7351–E7358, 2016. https://doi.org/10.1073/pnas.1614734113
• H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing viscosity, Math. Program. 168:123–175, 2018. https://doi.org/10.1007/s10107-016-1065-5

Motivation

Balanced truncation is the standard method for reducing the state dimension of a linear control system while keeping its input–output behaviour: states that are both hard to reach and hard to observe are discarded. Its justification rests on two Gramians, the solutions $P$ and $Q$ of a pair of Lyapunov equations, whose quadratic forms measure how much input energy a state costs to reach and how much output energy it produces. For linear systems the facts are classical: the image of the controllability Gramian is the reachable subspace, and the kernel of the observability Gramian is the unobservable subspace.

Bilinear systems, in which the input multiplies the state, are the simplest nonlinear extension of linear control systems. Their generalized Lyapunov equations have the same form as the Lyapunov equations of linear stochastic systems with multiplicative noise, which is why Benner and Damm treat the two classes together. Balanced truncation was extended to them using the solutions of generalized Lyapunov equations (Al-Baiyat and Bettayeb, 1993; Gray and Mesko, 1998, both as cited by Benner and Damm). Benner and Damm, in Lyapunov Equations, Energy Functionals, and Model Order Reduction of Bilinear and Stochastic Systems (SIAM J. Control Optim. 49(2), 2011, doi:10.1137/09075041X), examine which of the linear-system energy interpretations survive for bilinear systems. Their Theorem 3.1 is the structural result that does survive: the kernels of the Gramians still identify states that are unreachable from the origin and states that produce no output, so these states can be eliminated without changing the transfer behaviour.

Setting

Fix $n, m, p \ge 0$ and real matrices $A, N_1,\dots,N_m\in\mathbb R^{n\times n}$, $B\in\mathbb R^{n\times m}$, $C\in\mathbb R^{p\times n}$. The bilinear control system (3.1)–(3.2) is

$$\dot x = Ax + \sum_{j=1}^m N_j x\,u_j + Bu,\qquad y = Cx,$$

with state $x(t)\in\mathbb R^n$, input $u(t) = [u_1(t),\dots,u_m(t)]^T\in\mathbb R^m$ and output $y(t)\in\mathbb R^p$. The homogeneous system (3.5) drops the term $Bu$: $\dot x = Ax + \sum_j N_j x\,u_j$, $y = Cx$. The same $m$ indexes the bilinear terms and the columns of $B$. Write $x(t, x_0, u)$ for a solution with input $u$ and initial state $x(0) = x_0$, and $y(t,x_0,u) = Cx(t,x_0,u)$.

An admissible input is a function $u:[0,\infty)\to\mathbb R^m$ that is integrable on every interval $[0,T]$. A solution with $x(0) = x_0$ is a continuous $x:[0,\infty)\to\mathbb R^n$ satisfying

$$x(t) = x_0 + \int_0^t \Big(Ax(s) + \sum_{j=1}^m u_j(s)N_jx(s) + Bu(s)\Big)\,ds\qquad (t\ge 0).$$

The generalized Lyapunov equations (3.6) are

$$AP + PA^T + \sum_{j=1}^m N_jPN_j^T = -BB^T,\qquad A^TQ + QA + \sum_{j=1}^m N_j^TQN_j = -C^TC .$$

A solution $P$ of the first is a controllability Gramian and a solution $Q$ of the second an observability Gramian. "$P\ge 0$" means $P$ is symmetric nonnegative definite; $\mathrm{Im}\,P$ and $\mathrm{Ker}\,P$ are its image and kernel.

Formalization targets

Goal: Theorem 3.1 (p. 695)

(a) If $P\ge 0$ solves the first equation of (3.6), then for every admissible input $u$

$$x(t,0,u)\in\mathrm{Im}\,P\qquad\text{for all } t\ge 0 .$$

(b) If $Q\ge 0$ solves the second equation of (3.6) and $x_0\in\mathrm{Ker}\,Q$, then for the homogeneous system (3.5) and every admissible input $u$

$$y(t,x_0,u) = Cx(t,x_0,u) = 0\qquad\text{for all } t\ge 0 .$$

Milestones (the steps of the paper's proof, pp. 695–696)

1. $N_j^T\,\mathrm{Ker}\,P\subset\mathrm{Ker}\,P\subset\mathrm{Ker}\,B^T$.
2. $A^T\,\mathrm{Ker}\,P\subset\mathrm{Ker}\,P$.
3. $\mathrm{Im}\,P$ is invariant under the vector field of (3.1): $z\in\mathrm{Im}\,P$ implies $Az + \sum_j w_jN_jz + Bw\in\mathrm{Im}\,P$ for every $w\in\mathbb R^m$.
4. $N_j\,\mathrm{Ker}\,Q\subset\mathrm{Ker}\,Q\subset\mathrm{Ker}\,C$ and $A\,\mathrm{Ker}\,Q\subset\mathrm{Ker}\,Q$.
5. $\mathrm{Ker}\,Q$ is invariant under the vector field of (3.5).

Significance

The result. Part (a) says that a state outside $\mathrm{Im}\,P$ cannot be reached from the origin by any input, so its controllability energy $E_c$ is infinite; part (b) says that a state in $\mathrm{Ker}\,Q$ is indistinguishable from the origin at the output, so its observability energy $E_o$ is zero. Together they justify the first step of balanced truncation for bilinear systems (Remark 3.2 of the paper): the system can be restricted to $\mathrm{Im}\,P$ and projected along $\mathrm{Ker}\,Q$ without changing its input–output map, after which the Gramians are nonsingular and can be balanced. The theorem needs neither stability of $A$ nor uniqueness of the Gramians, so it applies to every nonnegative definite solution of (3.6). The rest of §3 of the paper shows that the finer, quantitative energy estimates of the linear case fail for bilinear systems; this qualitative statement is what remains exact.

Formalizing it. The theorem is proved in the paper; no machine-checked version is known. A formal proof yields a reusable invariance principle: a subspace that is invariant under every vector field $z\mapsto Az + \sum_j w_jN_jz + Bw$ is invariant under the flow of the input-driven system, for merely integrable inputs. It also yields the linear-algebra lemmas relating kernels of nonnegative definite solutions of generalized Lyapunov equations to the system matrices, which are used throughout model reduction and stochastic stability theory.

Difficulty

The algebraic part (milestones 1, 2, 4) rests on the fact that for a nonnegative definite matrix $M$, $v^TMv = 0$ forces $Mv = 0$, applied to the terms of the Lyapunov equation tested against a kernel vector. The passage from the vector field to trajectories is where care is needed. The paper's sentence "$\dot x(t)\in\mathrm{Im}\,P$ whenever $x(t)\in\mathrm{Im}\,P$, so $\mathrm{Im}\,P$ is invariant" is not by itself an argument: tangency of a vector field to a subspace implies invariance only together with a uniqueness or Gronwall-type estimate, and here the field depends on time through an input that is only integrable, so $x$ is merely absolutely continuous and $\dot x$ exists only almost everywhere. A pointwise "the derivative points into the subspace" argument therefore does not apply as stated, and the step needs an estimate on the component of $x(t)$ orthogonal to the subspace.

Formalization scope

The Lean development uses states Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, the matrix–vector product *ᵥ, and indices $j = 1,\dots,m$ as Fin m. $\mathrm{Im}\,P$ and $\mathrm{Ker}\,P$ are LinearMap.range and LinearMap.ker of Matrix.toLin' P; "$P\ge 0$" is Matrix.PosSemidef, which includes symmetry. Admissible inputs are integrable on every $[0,T]$ (this contains $L^2[0,\infty[$, the input space of the paper's energy functionals). A solution is a function continuous on $[0,\infty)$ whose integrand is integrable on every $[0,t]$ and which satisfies the integral equation for all $t\ge 0$; no uniqueness of solutions is presupposed, and the theorem is asserted for every such solution.

Two reading decisions are fixed. First, part (b) is stated for every admissible input $u$, not only for $u = 0$ as printed in the theorem: the paper's proof concludes "$x(t,x_0,u)\in\mathrm{Ker}\,Q$ for all $t\ge0$, implying $y(t,x_0,u) = 0$", and the theorem's clause "i.e., $E_o(x_0) = 0$" (with $E_o$ a maximum over inputs) needs this form. The $\forall u$ statement contains the printed one. Second, the clauses "i.e., $E_c(x_0) = \infty$" and "i.e., $E_o(x_0) = 0$", which restate the conclusions through the energy functionals (3.3)–(3.4), are not formalized.

The statements must not be trivialized: assuming $P$ positive definite makes (a) empty ($\mathrm{Im}\,P = \mathbb R^n$), assuming $A$ stable or the Gramians unique adds hypotheses the paper does not have, and a solution notion requiring $C^1$ trajectories for integrable inputs would make the solution set empty. None of these is used. A local check confirms the hypotheses have content: for $A = -I_2$, $N_1 = 0$, $B = e_1$, the matrix $P = \mathrm{diag}(1/2, 0)$ is a nonnegative definite solution of (3.6) with $e_2\notin\mathrm{Im}\,P$.

A complete development needs Mathlib's facts on nonnegative definite matrices, interval integrals of vector-valued functions, and a Gronwall inequality with an integrable coefficient. The flow-invariance lemma for input-driven linear-in-state systems is reusable beyond this mission. Contributions welcome: proofs of the five milestones, and the passage from vector-field invariance to trajectory invariance.

Selected references

• P. Benner, T. Damm, Lyapunov Equations, Energy Functionals, and Model Order Reduction of Bilinear and Stochastic Systems, SIAM J. Control Optim. 49(2), 686–711, 2011. https://doi.org/10.1137/09075041X
• S. A. Al-Baiyat, M. Bettayeb, A new model reduction scheme for k-power bilinear systems, Proceedings of the 32nd IEEE Conference on Decision and Control, San Antonio, 1993, pp. 22–27 (reference [1] of Benner–Damm).
• W. S. Gray, J. Mesko, Energy functions and algebraic Gramians for bilinear systems, Preprints of the 4th IFAC Nonlinear Control Systems Design Symposium, Enschede, 1998, pp. 103–108 (reference [25] of Benner–Damm).
• B. C. Moore, Principal component analysis in linear systems: Controllability, observability, and model reduction, IEEE Trans. Automat. Control 26(1), 17–32, 1981. https://doi.org/10.1109/TAC.1981.1102568

Motivation

Nesterov's accelerated gradient method and its proximal variant FISTA minimize a smooth convex function with a value gap of order $O(1/k^2)$ after $k$ iterations, against $O(1/k)$ for plain gradient descent. They are among the most widely used first-order methods in large-scale optimization, signal processing and machine learning. Su, Boyd and Candès (JMLR 2016) observed that, for $\alpha = 3$, the second-order differential equation

$$\ddot x(t) + \frac{\alpha}{t}\,\dot x(t) + \nabla\Phi(x(t)) = 0 \tag{1}$$

is a continuous-time limit of Nesterov's scheme, and proved $\Phi(x(t)) - \min\Phi = O(1/t^2)$ for $\alpha \ge 3$. A rate on the values says nothing about the trajectory itself: whether $x(t)$ (or the iterates $x_k$) converges at all was a long-standing question. The paper of Attouch, Chbani, Peypouquet and Redont answers it for $\alpha > 3$: every trajectory of (1) converges weakly to a minimizer of $\Phi$.

Timeline:

• 1983 — Nesterov introduces the accelerated gradient method with an $O(1/k^2)$ rate on the values.
• 2000 — Alvarez proves weak convergence of the trajectories of the heavy ball with friction, $\ddot x + \gamma\dot x + \nabla\Phi(x) = 0$, whose damping is constant (SIAM J. Control Optim. 38).
• 2009 — Beck and Teboulle extend it to composite problems (FISTA), still with a rate on the values only.
• 2014–2016 — Su, Boyd, Candès identify (1) as the continuous model of Nesterov's method and prove the $O(1/t^2)$ rate for $\alpha\ge3$.
• 2015 — Attouch, Chbani, Peypouquet, Redont prove weak convergence of the trajectories of (1) for $\alpha > 3$ (this mission), and of the iterates of the corresponding algorithms; Chambolle and Dossal obtain the discrete result independently. The case $\alpha = 3$ remains open.

Setting

Let $\mathcal H$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$, and let $\Phi:\mathcal H\to\mathbb R$ be a continuously differentiable convex function with gradient $\nabla\Phi$. Fix a damping parameter $\alpha>0$ and an initial time $t_0>0$. A solution of (1) on $[t_0,+\infty[$ is a pair of maps $x, v$ from the time axis to $\mathcal H$ such that, at every $t\ge t_0$, $x$ has derivative $v(t)$ and $v$ has derivative $-\frac{\alpha}{t}v(t) - \nabla\Phi(x(t))$. So $v=\dot x$, and $\ddot x$ satisfies (1). The damping coefficient $\alpha/t$ is singular at $0$ and vanishes as $t\to+\infty$; this is why the time origin is positive.

Three functions of time measure the progress of a solution:

• the global energy $W(t) = \frac12\|\dot x(t)\|^2 + \Phi(x(t))$;
• the anchored distance $h_z(t) = \frac12\|x(t)-z\|^2$ to a point $z\in\mathcal H$;
• when $\Phi$ has a minimizer $x^*$, the anchored energies, for $\lambda,\xi\ge0$,

$$\mathcal E_{\lambda,\xi}(t) = t^2\big(\Phi(x(t))-\min\Phi\big) + \tfrac12\|\lambda(x(t)-x^*) + t\dot x(t)\|^2 + \tfrac{\xi}{2}\|x(t)-x^*\|^2 .$$

$x(t)$ converges weakly to $\bar x$ as $t\to+\infty$ if $\langle x(t),y\rangle\to\langle\bar x,y\rangle$ for every $y\in\mathcal H$. A weak limit point of $x(t)$ is the weak limit of a sequence $x(s_n)$ with $s_n\to+\infty$. $\operatorname{argmin}\Phi$ is the set of minimizers of $\Phi$.

Formalization targets

Goal: Theorem 2.16

If $\operatorname{argmin}\Phi\ne\emptyset$ and $\alpha>3$, then for every solution $x$ of (1) there is $\bar x\in\operatorname{argmin}\Phi$ with

$$x(t)\rightharpoonup\bar x\qquad(t\to+\infty).$$

The goal asserts only the qualitative conclusion; no rate or constant enters it.

Milestones

1. Lemma 2.1 (energy dissipation): $\dot W(t) = -\frac{\alpha}{t}\|\dot x(t)\|^2$ for $t>t_0$; $W$ is nonincreasing with a limit in $\mathbb R\cup\{-\infty\}$, finite when $\Phi$ is bounded below.
2. (7): $\ddot h_z(t) + \frac{\alpha}{t}\dot h_z(t) + \Phi(x(t)) - \Phi(z) \le \|\dot x(t)\|^2$.
3. Lemma 2.2: $\int_{t_0}^t \frac1s(W(s)-\Phi(z))\,ds \le C - \frac1t\dot h_z(t) - \frac{3}{2\alpha}W(t)$ with an explicit constant $C$.
4. Theorem 2.3 i), ii) (minimizing property, every $\alpha>0$): $\lim W(t) = \lim \Phi(x(t)) = \inf\Phi\in\mathbb R\cup\{-\infty\}$, and every weak limit point of $x(t)$ is a minimizer.
5. Remark 2.6: the Lyapunov inequality for $\frac{d}{dt}\mathcal E_{\lambda,\xi}$, and monotonicity of $\mathcal E_{\lambda,\lambda(\alpha-\lambda-1)}$ for $\alpha\ge3$, $2\le\lambda\le\alpha-1$.
6. Theorem 2.14 ii) with (13), (15): for $\alpha>3$, $\|x(t)-x^*\|^2 \le \mathcal E_{2,2(\alpha-3)}(t_0)/(\alpha-3)$ and $\int_{t_0}^{\infty} t\|\dot x(t)\|^2\,dt \le \mathcal E_{2,2(\alpha-3)}(t_0)/(\alpha-3)$.
7. Lemma A.4: if $t\ddot w + \alpha\dot w \le g$ a.e. with $\alpha>1$, $g\ge0$ integrable and $w$ bounded below, then $[\dot w]_+$ is integrable and $\lim w(t)$ exists.
8. Lemma A.2 (Opial's lemma, continuous form).

Significance

The result. Theorem 2.16 is the first proof that the trajectories of the continuous Nesterov model converge, not only their values. The paper's discrete analysis parallels the continuous one and yields weak convergence of the iterates of Nesterov-type forward–backward algorithms for $\alpha>3$ (Theorem 5.3, a companion mission). The minimizing property (Theorem 2.3) holds for every $\alpha>0$, with no minimizer assumed, and shows that a bounded trajectory exists only if $\Phi$ has a minimizer. Strong convergence results under further geometric assumptions (Theorems 3.1–3.3) build directly on Theorem 2.16.

Formalizing it. All statements are proved on paper. None of them, nor the differential equation (1), is formalized on Prove2Me or in Mathlib; the discrete analogue (weak convergence of the unperturbed accelerated forward–backward iterates) exists on the platform as a separate result. A formal development provides: a reusable encoding of solutions of a non-autonomous second-order ODE in a Hilbert space; Lyapunov arguments with one-sided derivatives on a half-line; a continuous-time Opial lemma, which is the standard tool for weak convergence of evolution equations and of semigroups; and the scalar differential-inequality lemma A.4.

Difficulty

Lyapunov functions such as $W$ or $\mathcal E_{\alpha-1,0}$ give rates on the values but not convergence of $x(t)$: a decreasing energy says nothing about where the trajectory goes, and the minimizer set may be a continuum. The natural first idea, showing that $\|x(t)-x^*\|$ is eventually monotone as for the gradient flow, fails: the inertial term makes $h_{x^*}$ oscillate, and (7) controls only $t\ddot h + \alpha\dot h$, a second-order quantity. Making it usable requires integrability of $t\|\dot x(t)\|^2$ on $[t_0,+\infty[$, which is not available from the Su–Boyd–Candès energy and holds only for $\alpha>3$; the borderline $\alpha=3$ is open. In infinite dimension, convergence is genuinely weak: bounded sets are not compact, so the argument must identify weak limit points through weak lower semicontinuity of $\Phi$ and conclude through Opial's lemma.

Formalization scope

• Space. $\mathcal H$ is a real inner product space that is complete (InnerProductSpace ℝ H, CompleteSpace H); no finite dimension is assumed, since in finite dimension weak and norm convergence coincide.
• Potential. $\Phi:\mathcal H\to\mathbb R$ with ConvexOn ℝ Set.univ Φ and ContDiff ℝ 1 Φ; $\nabla\Phi$ is Mathlib's gradient. Minimizers are points $z$ with $\Phi(z)\le\Phi(y)$ for all $y$; $\min\Phi$ is written $\Phi(x^*)$ for such a point.
• Solutions. (1) is the first-order system $\dot x=v$, $\dot v=-\frac{\alpha}{t}v-\nabla\Phi(x)$, with derivatives within $[t_0,+\infty[$ at every $t\ge t_0$ and $t_0>0$. Existence of solutions is not assumed or proved: every statement concerns a given solution, as in the paper.
• Limits and integrals. Limits in $\mathbb R\cup\{-\infty\}$ are taken in EReal, $\inf\Phi$ as an EReal infimum. Improper integrals $\int_{t_0}^{+\infty}$ carry an explicit integrability conjunct; integrals over $[t_0,t]$ are interval integrals of continuous functions.
• Explicit constants. The constant $C$ of Lemma 2.2 and the bounds $\mathcal E_{2,2(\alpha-3)}(t_0)/(\alpha-3)$ of (13), (15) are stated exactly as the paper computes them.
• Trivializations ruled out. Weak convergence is not replaced by norm convergence, the derivative relations between $x$, $v$ and their energies are part of the hypotheses or conclusions (never a free deriv), and the solution predicate is non-vacuous: the constant trajectory for $\Phi=0$ and the explicit solution $x(t)=t^2$ of Example 2.5 satisfy it.
• Citation. Theorem numbers and pages refer to the Optimization Online preprint 5179 (October 2015), titled "…asymptotic vanishing damping", not to the Mathematical Programming typesetting.

Contributions of reusable infrastructure are welcome, in particular a continuous-time Opial lemma, weak lower semicontinuity of continuous convex functions on a Hilbert space along weakly convergent sequences, and integration-by-parts lemmas for one-sided derivatives on a half-line.

Selected references

• H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing damping, Optimization Online preprint 5179, 2015; published as …vanishing viscosity, Mathematical Programming 168 (2018) 123–175. https://optimization-online.org/wp-content/uploads/2015/10/5179.pdf, https://doi.org/10.1007/s10107-016-0992-8
• W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, Journal of Machine Learning Research 17 (2016) 1–43. https://jmlr.org/papers/v17/15-084.html
• F. Alvarez, On the minimizing property of a second order dissipative system in Hilbert spaces, SIAM Journal on Control and Optimization 38 (2000) 1102–1119. https://doi.org/10.1137/S0363012998335802
• Z. Opial, Weak convergence of the sequence of successive approximations for nonexpansive mappings, Bulletin of the AMS 73 (1967) 591–597. https://doi.org/10.1090/S0002-9904-1967-11761-0
• A. Beck, M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM Journal on Imaging Sciences 2 (2009) 183–202. https://doi.org/10.1137/080716542
• A. Chambolle, Ch. Dossal, On the convergence of the iterates of the "fast iterative shrinkage/thresholding algorithm", Journal of Optimization Theory and Applications 166 (2015) 968–982. https://doi.org/10.1007/s10957-015-0746-4