Convex Optimization

Motivation

Quadratically constrained quadratic programs (QCQPs) minimize a quadratic function subject to quadratic inequality and equality constraints. They model facility location, pooling, max-cut, trust-region steps and robust optimization problems, and every $\{0,1\}$ integer program can be written as one; in general they are NP-hard. The standard tractable approach is the Shor semidefinite relaxation, which lifts $x$ to the matrix $xx^\top$ and relaxes the rank-one condition to positive semidefiniteness. A recurring question is when this relaxation loses nothing: when its optimal value equals that of the QCQP (SDP tightness), and, more strongly, when its projected epigraph equals the convex hull of the QCQP's epigraph (convex hull exactness). The second property also describes the convex hull of the nonconvex feasible set's epigraph, which is useful in branch-and-bound and cutting-plane methods.

Timeline. The S-lemma (Yakubovich, 1971) gives SDP tightness for one inequality constraint, and Fujie and Kojima (1997) recorded the dual description of the SDP value used below. For the trust-region subproblem and its generalization, convex hull descriptions of the epigraph were given by Ho-Nguyen and Kılınç-Karzan (2017) and by Wang and Kılınç-Karzan (arXiv:1907.08843, 2019). Beck (2007) and Beck, Drori and Teboulle (2012) gave SDP tightness results for quadratic matrix programs. Wang and Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs (arXiv:1911.09195v3, Math. Program. 2021), introduced a general framework based on the faces of a dual set $\Gamma$ and proved convex hull and tightness results for polyhedral $\Gamma$ and for QCQPs with large quadratic eigenvalue multiplicity. This mission formalizes the paper's first convex hull theorem (Theorem 1, p. 13) and the framework it rests on.

Setting

Fix $N$ variables and $m\ge1$ constraints, the first $m_I$ inequalities and the remaining $m_E=m-m_I$ equalities. Each function is

$$q_i(x)=x^\top A_ix+2b_i^\top x+c_i,\qquad A_i\in\mathbb S^N,\ b_i\in\mathbb R^N,\ c_i\in\mathbb R,\quad i=0,\dots,m.$$

The QCQP (1) is $\mathrm{Opt}=\inf\{q_0(x): q_i(x)\le0\ (i\le m_I),\ q_i(x)=0\ (i>m_I)\}$, and its epigraph is $\mathcal D=\{(x,t): x\text{ feasible},\ q_0(x)\le2t\}$.

With $Q_i=\begin{pmatrix}c_i&b_i^\top\\ b_i&A_i\end{pmatrix}$ and $Y=\begin{pmatrix}1&x^\top\\ x&X\end{pmatrix}$, the SDP relaxation (3) minimizes $\langle Q_0,Y\rangle$ over $X\in\mathbb S^N$ with $Y\succeq0$ and the constraints $\langle Q_i,Y\rangle\le0$ or $=0$; its value is $\mathrm{Opt}_{\mathrm{SDP}}$ and its projected epigraph is $\mathcal D_{\mathrm{SDP}}=\{(x,t):\exists X,\ (x,X)\text{ feasible},\ \langle Q_0,Y\rangle\le2t\}$ (4). Always $\mathrm{conv}(\mathcal D)\subseteq\mathcal D_{\mathrm{SDP}}$ and $\mathrm{Opt}\ge\mathrm{Opt}_{\mathrm{SDP}}$.

For $\gamma\in\mathbb R^m$ let $A(\gamma)=A_0+\sum_i\gamma_iA_i$, and similarly $b(\gamma)$, $c(\gamma)$ and the Lagrangian $q(\gamma,x)=q_0(x)+\sum_i\gamma_iq_i(x)$. The dual object is

$$\Gamma=\{\gamma\in\mathbb R^m:\ A(\gamma)\succeq0,\ \gamma_i\ge0\ \text{for } i\le m_I\}.$$

Assumption 1: the QCQP is feasible and some $\gamma^*$ with $\gamma^*_i\ge0$ for $i\le m_I$ has $A(\gamma^*)\succ0$. Assumption 3: $\Gamma$ is polyhedral. For $\hat x\in\mathbb R^N$, $\mathcal F(\hat x)=\arg\max_{\gamma\in\Gamma}q(\gamma,\hat x)$. A face $\mathcal F$ of $\Gamma$ is definite if some $\gamma\in\mathcal F$ has $A(\gamma)\succ0$ and semidefinite otherwise, with shared zero eigenspace $\mathcal V(\mathcal F)=\{v: A(\gamma)v=0\ \forall\gamma\in\mathcal F\}$. Finally $\operatorname{aff\,dim}$ denotes affine dimension.

Formalization targets

Goal: Theorem 1 (p. 13)

Under Assumptions 1 and 3, if every semidefinite face $\mathcal F$ of $\Gamma$ satisfies $\dim\mathcal V(\mathcal F)\ge\operatorname{aff\,dim}\{b(\gamma):\gamma\in\mathcal F\}+1$, then

$$\mathrm{conv}(\mathcal D)=\mathcal D_{\mathrm{SDP}}\qquad\text{and}\qquad\mathrm{Opt}=\mathrm{Opt}_{\mathrm{SDP}}.$$

Milestones

1. Lemma 1 (p. 7): under Assumption 1, $\mathcal D_{\mathrm{SDP}}=\{(x,t):\sup_{\gamma\in\Gamma}q(\gamma,x)\le2t\}$ and $\mathrm{Opt}_{\mathrm{SDP}}=\min_x\sup_{\gamma\in\Gamma}q(\gamma,x)$.
2. Lemma 2 (p. 9): a semidefinite face has a unit vector in $\mathcal V(\mathcal F)$.
3. Lemma 3 (p. 9): under Assumptions 1 and 2, a point of $\mathcal D_{\mathrm{SDP}}$ with definite $\mathcal F(\hat x)$ lies in $\mathcal D$.
4. Observation 1 (p. 10): under Assumption 1, a face of affine dimension $m$ is definite.
5. Lemma 4 (p. 10): under Assumptions 1, 2 and the decomposition condition (7), the two conclusions of Theorem 1 hold.
6. Lemma 8 (p. 13): under Assumption 3, $\Gamma=\Gamma_e+\mathrm{cone}(\Gamma_r)$ with polytopes $\Gamma_e,\Gamma_r$, and $\mathcal F(\hat x)=\mathcal F_e(\hat x)+\mathrm{cone}(\mathcal F_r(\hat x))$ when the supremum is finite.
7. Lemma 7 (p. 13): under the hypotheses of Theorem 1, condition (7) holds.

Companions

Lemma 6 (p. 11: $\dim\mathcal V(\mathcal F)\ge k$ for the quadratic eigenvalue multiplicity $k$), Theorem 2 (p. 15: the hypothesis of Theorem 1 with $k$ in place of $\dim\mathcal V(\mathcal F)$), and Corollaries 1–4 (pp. 16–18: convex quadratic programs, one constraint, $b_i=0$, scalar quadratic forms with $m\le N$).

Significance

The result. Theorem 1 gives a checkable sufficient condition, stated on the faces of a polyhedral dual set, under which the Shor relaxation is exact in the strongest sense: it describes $\mathrm{conv}(\mathcal D)$, so the SDP value equals the QCQP value and, by Remark 7, $\mathrm{conv}(\mathcal D)$ is second-order cone representable. Through Lemma 6 it becomes Theorem 2, the symmetry condition $k\ge\operatorname{aff\,dim}\{b(\gamma)\}+1$; its corollaries recover the convex hull results for the trust-region subproblem and its generalization and give new ones for simultaneously diagonalizable and "Swiss cheese" problems. The sharpness of the bound is shown in §4.3 of the paper.

Formalizing it. The theorem is proved in the paper; nothing in it is machine-checked. A formal proof needs strong conic duality for the SDP in Lemma 1, the Minkowski–Weyl decomposition in Lemma 8, and the face-by-face decomposition argument of Lemma 7. These pieces are shared with the paper's SDP tightness result (Theorem 3), which uses Lemmas 1–3 and 8 again.

Difficulty

The obvious attempt is to take $(\hat x,\hat t)\in\mathcal D_{\mathrm{SDP}}$, recover a rank-one solution of the SDP, and read off a point of $\mathcal D$. This fails because an optimal $Y$ need not have rank one, and a rank-reduction step can leave the feasible set of a nonconvex constraint. The paper instead moves $(\hat x,\hat t)$ along a direction $v$ in the shared zero eigenspace of the face $\mathcal F(\hat x)$, and must show that both endpoints of the move stay in $\mathcal D_{\mathrm{SDP}}$ while the face strictly grows in affine dimension. Controlling the endpoints needs finiteness of the relevant family of quadratic functions, which is where polyhedrality enters; without it (§4.3) the argument and the theorem fail. Lemma 1 also needs a strong duality theorem for semidefinite programs with a minimax step, neither of which is elementary in Lean.

Formalization scope

The Lean development lives in the namespace QCQPTightness.ConvHull. A QCQP is a structure with symmetric $A_0, A_i$, vectors $b_0,b_i$, scalars $c_0,c_i$ and a count $m_I\le m$; constraints are indexed by Fin m, constraint $i$ being an inequality exactly when $i<m_I$. Conventions:

• $\mathrm{Opt}$ and $\mathrm{Opt}_{\mathrm{SDP}}$ are infima in EReal, never real infima; points of $\mathbb R^{N+1}$ are pairs $(x,t)$, and $\mathrm{conv}$ is convexHull ℝ.
• Faces of $\Gamma$ are nonempty convex extreme subsets; the page's convention $\operatorname{aff\,dim}\emptyset=-1$ makes the empty face irrelevant, while Lean's affine dimension of $\emptyset$ would be $0$.
• "$\sup_{\gamma\in\Gamma}q(\gamma,x)\le2t$" is written $\forall\gamma\in\Gamma,\ q(\gamma,x)\le2t$; "a convex combination of points with property $P$" is membership in the convex hull of the set of such points; the unit sphere is $v^\top v=1$.
• The goal carries exactly the paper's hypotheses plus its standing assumption $m\ge1$ (p. 1); Assumption 2 is not assumed because Assumption 3 implies it.
• Lemma 8 is printed with "$\mathcal F_r(\hat x)$ is the face of $\Gamma_e$"; it is formalized with $\Gamma_r$, as the proof and Lemma 7 use it.

A trivializing formalization would assume condition (7), the decomposition of Lemma 8, or any property of $\mathcal F(\hat x)$ in the goal; the goal assumes none of these, and the dimension hypothesis is satisfiable with semidefinite faces present (for $q_0=-x^2$, $q_1=x^2-1$, the face $\{\gamma_1=1\}$ is semidefinite with $\dim\mathcal V=1$).

Infrastructure needed: SDP strong duality (the platform has ConvexOptimization.sdp_strong_duality), the Minkowski–Weyl theorem for polyhedra, faces of convex sets and affine dimension. Proofs of any milestone, of the companions, and reusable lemmas about faces of spectrahedra are welcome.

Selected references

• A. L. Wang, F. Kılınç-Karzan, On the tightness of SDP relaxations of QCQPs, Math. Program. (2021); arXiv:1911.09195v3. https://arxiv.org/abs/1911.09195 , https://doi.org/10.1007/s10107-020-01589-9
• T. Fujie, M. Kojima, Semidefinite programming relaxation for nonconvex quadratic programs, J. Global Optim. 10 (1997) 367–380. https://doi.org/10.1023/A:1008282830093
• A. Beck, Quadratic matrix programming, SIAM J. Optim. 17 (2007) 1224–1238. https://doi.org/10.1137/05064816X
• N. Ho-Nguyen, F. Kılınç-Karzan, A second-order cone based approach for solving the trust-region subproblem and its variants, SIAM J. Optim. 27 (2017) 1485–1512. https://doi.org/10.1137/16M1065197
• A. L. Wang, F. Kılınç-Karzan, The generalized trust region subproblem: solution complexity and convex hull results, arXiv:1907.08843 (2019). https://arxiv.org/abs/1907.08843
• I. Pólik, T. Terlaky, A survey of the S-lemma, SIAM Review 49 (2007) 371–418. https://doi.org/10.1137/S003614450444614X

Motivation

Nesterov's accelerated gradient method for smooth convex functions, called NAG-C in the source paper, minimizes an $L$-smooth convex function $f$ with function values decreasing at the rate $O(L/k^2)$. That rate is optimal among first-order methods (Nesterov, 1983). A line of work starting with Su, Boyd & Candès (2016) studies such methods through ordinary differential equations obtained in the limit of vanishing step size. Their low-resolution ODE $\ddot X+\frac3t\dot X+\nabla f(X)=0$ reproduces the $O(1/t^2)$ function-value rate. The same ODE also models the heavy-ball method, so it cannot explain why Nesterov's method behaves differently from heavy-ball.

Shi, Du, Jordan & Su (arXiv:1810.08907v3) keep the $O(\sqrt s)$ terms of the limit, where $s$ is the step size. The resulting high-resolution ODEs contain a gradient-correction term $\sqrt s\,\nabla^2 f(X)\dot X$, which is absent from the heavy-ball ODE. This mission formalizes the paper's analysis of the high-resolution ODE of NAG-C (Section 4.1, pp. 21–24). Along this ODE the smallest squared gradient norm up to time $t$ decays like $1/t^3$, while the low-resolution ODE gives only $1/t^2$. Small gradients are the natural stopping criterion in practice and the natural target in nonconvex and dual problems, which is why the squared gradient norm is studied separately from function values (Nesterov, 2012).

Setting

Let $f:\mathbb R^n\to\mathbb R$ have gradient $\nabla f$ and Hessian $\nabla^2 f$. For $L>0$, the class $\mathcal F^1_L(\mathbb R^n)$ consists of the differentiable $f$ with

$$f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle,\qquad \|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|\qquad(x,y\in\mathbb R^n).$$

The class $\mathcal F^2_L(\mathbb R^n)$ is its subclass of twice continuously differentiable functions whose Hessian is Lipschitz continuous. A minimizer $x^\star$ of $f$ is fixed.

Given a step size $s>0$, put $t_0=1.5\sqrt s$. The high-resolution ODE of NAG-C (1.12) is

$$\ddot X(t)+\frac3t\dot X(t)+\sqrt s\,\nabla^2 f(X(t))\dot X(t)+\Big(1+\frac{3\sqrt s}{2t}\Big)\nabla f(X(t))=0\qquad(t\ge t_0),$$

with $X(t_0)=x_0$ and $\dot X(t_0)=-\sqrt s\,\nabla f(x_0)$. The analysis uses the Lyapunov function (4.1)

$$\mathcal E(t)=t\Big(t+\frac{\sqrt s}{2}\Big)\big(f(X)-f(x^\star)\big)+\frac12\big\|t\dot X+2(X-x^\star)+t\sqrt s\,\nabla f(X)\big\|^2 .$$

With $s=0$ it reduces to the Lyapunov function of Su, Boyd and Candès.

Formalization targets

Goal: Theorem 5 (p. 21)

For every $f\in\mathcal F^2_L(\mathbb R^n)$, every step size $s>0$, and every solution $X$ of (1.12),

$$\inf_{t_0\le u\le t}\|\nabla f(X(u))\|^2\le\frac{(12+9sL)\,\|x_0-x^\star\|^2}{2\sqrt s\,(t^3-t_0^3)}\qquad\text{for all }t>t_0 .$$

With $s=1/L$ this is $O(\sqrt L/t^3)$. The infimum cannot be dropped, because the gradient norm need not decrease along the trajectory.

Milestones (pp. 22–23)

1. The exact derivative of $\mathcal E$ along (1.12) (first display of the proof of Lemma 4.1, p. 23).
2. Lemma 4.1, (4.2): $\frac{d\mathcal E}{dt}\le-\big[\sqrt s\,t^2+(\frac1L+\frac s2)t+\frac{\sqrt s}{2L}\big]\|\nabla f(X)\|^2$ for $t\ge t_0$.
3. The integrated form: $\int_{t_0}^t\big[\sqrt s\,u^2+(\frac1L+\frac s2)u+\frac{\sqrt s}{2L}\big]\|\nabla f(X(u))\|^2\,du\le\mathcal E(t_0)-\mathcal E(t)\le\mathcal E(t_0)$.
4. (4.3): the infimum is at most $\mathcal E(t_0)$ divided by $\sqrt s(t^3-t_0^3)/3+(\frac1L+\frac s2)(t^2-t_0^2)/2+\frac{\sqrt s}{2L}(t-t_0)$.
5. $\mathcal E(t_0)\le 3s\cdot\frac L2\|x_0-x^\star\|^2+2\|x_0-x^\star\|^2$, from the initial conditions.
6. (4.4): the same bound as (4.3) with numerator $(2+1.5sL)\|x_0-x^\star\|^2$. Keeping only the cubic term of the denominator gives Theorem 5.

A companion item states Corollary 4.2 (p. 24): $f(X(t))-f(x^\star)\le\frac{(4+3sL)\|x_0-x^\star\|^2}{t(2t+\sqrt s)}$ for $t>t_0$.

Significance

Theorem 5 is the continuous-time model of the paper's Theorem 6, which shows that NAG-C itself, without modification, drives $\min_{i\le k}\|\nabla f(x_i)\|^2$ to zero at the rate $O(L^2/k^3)$. Combining the $O(1/t^2)$ function-value rate with $\|\nabla f\|^2\le 2L(f-f^\star)$ gives only $O(L/t^2)$. Previously known $O(L^2/k^3)$ rates required modified methods (Ghadimi & Lan, 2016). The proof attributes the improvement to the gradient-correction term: the factor $\|\nabla f(X)\|^2$ in Lemma 4.1 comes from the term $t\sqrt s\,\nabla f(X)$ in (4.1), which exists only because of the Hessian term in (1.12). The authors conjecture that the low-resolution ODE does not achieve the $1/t^3$ rate (p. 23).

The results of Section 4.1 are proved in the paper; no machine-checked version of them is known. Formalizing them produces a checked Lyapunov analysis of a second-order ODE with Hessian damping and explicit constants. It also gives a template that the discrete analysis of NAG-C (a separate mission in this series) mirrors step by step. Related Hessian-damped systems are analysed in Attouch, Chbani, Fadili & Riahi (2020), with qualitative integrability conclusions instead of an explicit bound on the infimum.

Difficulty

The obvious route goes through the function-value rate and the inequality $\|\nabla f\|^2\le2L(f-f^\star)$. It loses a factor of $t$ and yields only $1/t^2$. The cubic rate needs a Lyapunov function whose derivative contains a term proportional to $t^2\|\nabla f(X)\|^2$. Proving the derivative identity requires differentiating $t\mapsto\nabla f(X(t))$ through the chain rule with the Hessian, and then cancelling that derivative against the gradient-correction term of the ODE. The derivative bound also uses the co-coercivity inequality $f(x^\star)\ge f(X)+\langle\nabla f(X),x^\star-X\rangle+\frac1{2L}\|\nabla f(X)\|^2$ of $L$-smooth convex functions. The remaining steps are measure-theoretic: integrate a one-sided derivative bound on $[t_0,t]$, and compare an infimum with a weighted average.

Formalization scope

• $\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\nabla f$ is Mathlib's gradient, and $\nabla^2 f(x)v$ is the Fréchet derivative of the gradient map applied to $v$.
• The classes $\mathcal F^1_L$ and $\mathcal F^2_L$ are stated in the first-order form printed on p. 8. The Hessian's Lipschitz constant is existential, since the paper fixes none.
• The minimizer $x^\star$ is a hypothesis $f(x^\star)\le f(z)$ for all $z$. The paper presupposes it exists.
• The step size is any $s>0$; there is no condition $s\le1/L$.
• A solution of (1.12) is a pair $(X,V)$ with $X(t_0)=x_0$ and $V(t_0)=-\sqrt s\,\nabla f(x_0)$. For every $t\ge t_0$, $X$ has derivative $V(t)$ and $V$ has the derivative prescribed by (1.12), both relative to $[t_0,\infty)$.
• Every statement quantifies over all solutions. Existence and uniqueness (the paper's Proposition 2.2) are not assumed.
• The infimum $\inf_{t_0\le u\le t}$ ranges over the points of the interval $[t_0,t]$. Statements involving it hold for $t>t_0$, as on the page.
• Derivative bounds assert that the derivative exists.
• The integral bound asserts integrability of its integrand.

Ruled out. A formalization would hold for junk reasons in any of these cases: the infimum is written as a bounded infimum over all reals (in Lean this is $\le 0$); the velocity is not tied to $\dot X$; the goal is stated at $t=t_0$ (where Lean divides by $0$); or derivatives are written with deriv, which is $0$ where a function is not differentiable. The statements here avoid all of these.

Infrastructure. A complete development needs:

• the chain rule for $\nabla f\circ X$ along a path;
• the co-coercivity inequality for $L$-smooth convex functions;
• the fundamental theorem of calculus for one-sided derivatives on $[t_0,t]$;
• the mean-value comparison of an infimum with a weighted average.

The co-coercivity inequality and the interval-integral comparison are reusable beyond this mission. Proofs of the milestones in any order are welcome, as are independent proofs of the goal.

Selected references

• B. Shi, S. S. Du, M. I. Jordan, W. J. Su, Understanding the Acceleration Phenomenon via High-Resolution Differential Equations, arXiv:1810.08907v3, 2018; Math. Program. (2021), DOI 10.1007/s10107-021-01681-8. 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(153), 2016. https://arxiv.org/abs/1503.01243
• Y. Nesterov, A method of solving a convex programming problem with convergence rate O(1/k²), Soviet Math. Dokl. 27, 1983. https://www.mathnet.ru/eng/dan46009
• Y. Nesterov, How to make the gradients small, Optima 88, 2012. http://www.mathopt.org/Optima-Issues/optima88.pdf
• S. Ghadimi, G. Lan, Accelerated gradient methods for nonconvex nonlinear and stochastic programming, Math. Program. 156, 2016. https://arxiv.org/abs/1310.3787
• H. Attouch, Z. Chbani, J. Fadili, H. Riahi, First-order optimization algorithms via inertial systems with Hessian driven damping, Math. Program., 2020. https://arxiv.org/abs/1907.10536

Why a high-resolution ODE for the heavy-ball method

Polyak's heavy-ball method and Nesterov's accelerated gradient method for strongly convex functions (NAG-SC) are the two classical momentum methods of smooth convex optimization. With step size $s$ and momentum $\alpha=(1-\sqrt{\mu s})/(1+\sqrt{\mu s})$ they differ only by a gradient-correction term, yet NAG-SC is accelerated for every $\mu$-strongly convex, $L$-smooth objective while the heavy-ball method can fail to converge outside the quadratic case (Lessard, Recht & Packard 2016). The classical continuous-time limit cannot see this difference: as $s\to0$ both methods converge to the same low-resolution ODE $\ddot X+2\sqrt\mu\,\dot X+\nabla f(X)=0$ (Su, Boyd & Candès 2016 treat the convex analogue).

Shi, Du, Jordan & Su (2018/2021) keep the $O(\sqrt s)$ terms of the limit and obtain high-resolution ODEs, one per method, which do distinguish the two algorithms. This mission formalizes their convergence theorem for the high-resolution ODE of the heavy-ball method (Theorem 2 of arXiv:1810.08907v3). A companion mission in the same series treats the high-resolution ODE of NAG-SC (Theorem 1), whose only difference is a Hessian-driven damping term $\sqrt s\,\nabla^2 f(X)\dot X$.

Setting

Work in $\mathbb R^n$ with the standard inner product $\langle\cdot,\cdot\rangle$ and Euclidean norm $\|\cdot\|$. A function $f:\mathbb R^n\to\mathbb R$ belongs to $\mathcal F^1_L(\mathbb R^n)$ if $L>0$, $f$ is differentiable and convex in the form $f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle$, and $\|\nabla f(x)-\nabla f(y)\|\le L\|x-y\|$ for all $x,y$. It belongs to $\mathcal S^1_{\mu,L}(\mathbb R^n)$ if moreover $0<\mu\le L$ and

$$f(y)\ge f(x)+\langle\nabla f(x),y-x\rangle+\frac\mu2\|y-x\|^2\quad\text{for all }x,y,$$

and to $\mathcal S^2_{\mu,L}(\mathbb R^n)$ if in addition $f$ is twice continuously differentiable with a Lipschitz-continuous Hessian. Write $x^\star$ for the minimizer of $f$.

Given a step size $s>0$ and an initial point $x_0$, the high-resolution ODE of the heavy-ball method is

$$\ddot X(t)+2\sqrt\mu\,\dot X(t)+\bigl(1+\sqrt{\mu s}\bigr)\nabla f(X(t))=0,\qquad X(0)=x_0,\quad \dot X(0)=-\frac{2\sqrt s\,\nabla f(x_0)}{1+\sqrt{\mu s}},\tag{1.10}$$

for $t\ge0$. The initial velocity matches the first step of the discrete method. The paper's Lyapunov function is

$$\mathcal E(t)=\bigl(1+\sqrt{\mu s}\bigr)\bigl(f(X)-f(x^\star)\bigr)+\frac14\|\dot X\|^2+\frac14\bigl\|\dot X+2\sqrt\mu\,(X-x^\star)\bigr\|^2.\tag{3.3}$$

Formalization targets

Goal: Theorem 2 (p. 14)

For $f\in\mathcal S^2_{\mu,L}(\mathbb R^n)$, every step size $0<s\le1/L$, and every $t\ge0$,

$$f(X(t))-f(x^\star)\le\frac{7\,\|x_0-x^\star\|^2}{2s}\,e^{-\sqrt\mu\,t/4}.$$

Milestones

1. The estimate (B.1), p. 50: $\mathcal E\le(1+\sqrt{\mu s})(f(X)-f(x^\star))+\frac34\|\dot X\|^2+2\mu\|X-x^\star\|^2$.
2. The derivative identity of App. B.1, p. 50: along (1.10),

$$\frac{d\mathcal E}{dt}=-\sqrt\mu\Bigl[\|\dot X\|^2+\bigl(1+\sqrt{\mu s}\bigr)\langle\nabla f(X),X-x^\star\rangle\Bigr].$$

3. Lemma 3.2, p. 14: for every $s>0$, $\dfrac{d\mathcal E}{dt}\le-\dfrac{\sqrt\mu}{4}\mathcal E$.
4. The integrated decay, p. 14: $\mathcal E(t)\le e^{-\sqrt\mu t/4}\mathcal E(0)$.
5. The explicit-coefficient bound, p. 14: for $s\le1/L$,

$$f(X)-f(x^\star)\le\left[\frac12+\frac{3}{(1+\sqrt{\mu s})^3}+\frac{2(\mu s)}{1+\sqrt{\mu s}}\right]\frac{\|x_0-x^\star\|^2e^{-\sqrt\mu t/4}}{s}.$$

6. The coefficient inequality, p. 14: for $0<\mu s\le1$, the bracket above is $<7/2$.

Significance

The result. Theorem 2 gives a linear rate $e^{-\sqrt\mu t/4}$ for the heavy-ball ODE with an explicit constant, valid for every $\mathcal S^2_{\mu,L}$ objective and every step size up to $1/L$. Read next to Theorem 1 (rate $e^{-\sqrt\mu t/4}$, constant $2/s$ for the NAG-SC ODE), it shows that at the continuous level both high-resolution ODEs converge at the accelerated rate; the paper locates the difference between the two discrete methods in the discretization, where only the gradient correction of NAG-SC lets the Lyapunov argument survive (its Theorems 3 and 4 and §3.3). The Lyapunov function (3.3) is the NAG-SC function (2.4) with the $\sqrt s\,\nabla f(X)$ term removed, and the two coincide at $s=0$.

Formalizing it. The result is proved in the paper; to our knowledge no machine-checked proof exists. The mission produces a checked chain from the ODE to the rate: a one-sided derivative computation along a trajectory in $\mathbb R^n$, a differential inequality, a Grönwall-type integration, and a closed-form estimate of $\mathcal E(0)$ from the initial conditions and $L$-smoothness. The derivative computation and the Grönwall step reuse directly in the companion missions on the NAG-SC and NAG-C high-resolution ODEs.

Difficulty

The algebra is short; the formal difficulty is analytic. The derivative of $t\mapsto f(X(t))$ must be obtained by the chain rule from a one-sided derivative of $X$ at $t=0$ and $f$'s differentiability, and the derivative of the two squared norms from those of $X$ and $V=\dot X$. Passing from Lemma 3.2 to $\mathcal E(t)\le e^{-\sqrt\mu t/4}\mathcal E(0)$ is a comparison argument for a function known only to have one-sided derivatives on $[0,\infty)$; the naive route through $\frac{d}{dt}\bigl(e^{\sqrt\mu t/4}\mathcal E\bigr)\le0$ requires a monotonicity theorem for functions with derivatives within a half-line. Finally, the estimate of $\mathcal E(0)$ needs $f(x_0)-f(x^\star)\le\frac L2\|x_0-x^\star\|^2$ and $\|\nabla f(x_0)\|\le L\|x_0-x^\star\|$, both consequences of $L$-smoothness and $\nabla f(x^\star)=0$ that must be derived from the class definition, and the constant $7/2$ needs a one-variable inequality in $\sqrt{\mu s}\in(0,1]$.

Formalization scope

$\mathbb R^n$ is EuclideanSpace ℝ (Fin n), $\nabla f$ is Mathlib's gradient, and $\nabla^2f(x)$ is fderiv ℝ (gradient f) x. The classes $\mathcal F^1_L$, $\mathcal S^1_{\mu,L}$, $\mathcal S^2_{\mu,L}$ are structures carrying the paper's first-order inequalities (§1.4, p. 8), with $0<\mu\le L$; the Lipschitz constant of the Hessian is existential, as the paper fixes none. The minimizer is a point $x^\star$ with $f(x^\star)\le f(z)$ for all $z$.

A solution of (1.10) is a pair of curves $X,V:\mathbb R\to\mathbb R^n$ with $X(0)=x_0$, $V(0)=-2\sqrt s\,\nabla f(x_0)/(1+\sqrt{\mu s})$, $V(t)$ the derivative of $X$ and $-2\sqrt\mu V(t)-(1+\sqrt{\mu s})\nabla f(X(t))$ the derivative of $V$ at every $t\ge0$, both taken within $[0,\infty)$; values for $t<0$ play no role. The theorems quantify over every such solution. Existence and uniqueness (the paper's Propositions 2.1–2.2) are not assumed, and no a priori bound on $X$ or $V$ is added. Derivative claims assert that the derivative exists and has the stated value or bound, so a statement cannot hold merely because a derivative is undefined. The goal states the decay of $f(X(t))-f(x^\star)$ with the printed constant $7/(2s)$; it does not assume any decay of $\mathcal E$, and an ODE predicate in which $V$ is not the derivative of $X$ would be a different, trivial statement.

All drafts live in the namespace HighResODE.HeavyBallODE, with one definitions file (classes, ODE, Lyapunov function). Contributions are welcome at every milestone; a general lemma "$\varphi'\le-c\,\varphi$ within $[0,\infty)$ implies $\varphi(t)\le e^{-ct}\varphi(0)$" and the $L$-smoothness estimates around a minimizer are reusable well beyond this mission.

Selected references

• B. Shi, S. S. Du, M. I. Jordan, W. J. Su, Understanding the Acceleration Phenomenon via High-Resolution Differential Equations, Mathematical Programming (2021); cited here in its preprint version arXiv:1810.08907v3. 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, Journal of Machine Learning Research 17 (2016). https://arxiv.org/abs/1503.01243
• L. Lessard, B. Recht, A. Packard, Analysis and Design of Optimization Algorithms via Integral Quadratic Constraints, SIAM Journal on Optimization 26 (2016). https://arxiv.org/abs/1408.3595
• B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Computational Mathematics and Mathematical Physics 4 (1964). https://doi.org/10.1016/0041-5553(64)90137-5

Motivation

Nesterov's accelerated gradient method minimises a smooth convex function $f$ to accuracy $\varepsilon$ in $O(\sqrt{L/\varepsilon})$ gradient evaluations, and a $\mu$-strongly convex one in $O(\sqrt{L/\mu}\,\log(1/\varepsilon))$; both counts match the lower bounds for first-order methods. Nesterov's own analysis (Y. Nesterov, Introductory Lectures on Convex Optimization, 2004, Ch. 2) proceeds by estimate sequences, an algebraic device that certifies the rate but says little about where the method comes from. Since Su, Boyd and Candès (arXiv:1503.01243), accelerated methods have been read as discretisations of ordinary differential equations, with convergence proved by discrete Lyapunov functions.

H. Luo and L. Chen, From differential equation solvers to accelerated first-order methods for convex optimization (arXiv:1909.03145, Math. Program. 2022), introduce the NAG flow, a first-order system in a position $x$, an auxiliary variable $v$ and a scaling parameter $\gamma$ whose Lyapunov function decays exponentially for every $\mu\ge0$. In §6 they show that Nesterov's general scheme of optimal method (Algorithm 1) is itself a corrected semi-implicit discretisation of this flow, and they reprove its rates with one Lyapunov function that covers $\mu=0$ and $\mu>0$ at once. This mission formalises that analysis, Theorem 6.1.

Setting

Let $V$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. A function $f:V\to\mathbb R$ with gradient map $\nabla f$ belongs to $\mathcal S^1_\mu$ ($\mu\ge0$) if it is continuously differentiable and $\mu$-convex,

$$f(x)-f(y)-\langle\nabla f(y),x-y\rangle\ge\tfrac{\mu}{2}\|x-y\|^2\qquad\forall x,y\in V,$$

and to $\mathcal S^{1,1}_{\mu,L}$ if moreover $\nabla f$ is $L$-Lipschitz, with $0\le\mu\le L<\infty$. A point $x^*$ minimises $f$ globally.

Algorithm 1 (Nesterov accelerated gradient method) takes $x_0,v_0\in V$ and $\gamma_0>0$. For $k=0,1,\dots$ it computes the positive root $\alpha_k$ of $L\alpha_k^2=(1-\alpha_k)\gamma_k+\mu\alpha_k$, sets $\gamma_{k+1}=(1-\alpha_k)\gamma_k+\mu\alpha_k$ and

$$y_k=\frac{\alpha_k\gamma_kv_k+\gamma_{k+1}x_k}{\gamma_k+\mu\alpha_k},$$

chooses any $x_{k+1}$ with the sufficient decrease $f(x_{k+1})\le f(y_k)-\frac1{2L}\|\nabla f(y_k)\|^2$ (for instance the gradient step $x_{k+1}=y_k-\frac1L\nabla f(y_k)$), and sets

$$v_{k+1}=\frac{1}{\gamma_{k+1}}\big[(1-\alpha_k)\gamma_kv_k+\alpha_k(\mu y_k-\nabla f(y_k))\big].$$

The Lyapunov function is

$$\mathcal L_k=f(x_k)-f(x^*)+\frac{\gamma_k}{2}\|v_k-x^*\|^2,\tag{74}$$

and $C_{\gamma_0,L}=\frac{L}{\gamma_0}(f(x_0)-f(x^*))+\frac L2\|v_0-x^*\|^2$ (89).

Formalization targets

Goal: Theorem 6.1

For $f\in\mathcal S^{1,1}_{\mu,L}$, every run of Algorithm 1 has $0<\alpha_k\le1$ and

$$\mathcal L_{k+1}\le(1-\alpha_k)\mathcal L_k\quad(k\in\mathbb N),\tag{98}$$ $$\mathcal L_k\le\mathcal L_0\min\left\{\frac{4L}{(\sqrt{\gamma_0}\,k+2\sqrt L)^2},\Big(1-\sqrt{\tfrac{\min\{\gamma_1,\mu\}}{L}}\Big)^{k}\right\}\quad(k\ge0),\tag{99}$$ $$\mathcal L_k\le C_{\gamma_0,L}\min\left\{\frac{4}{k^2},\Big(1-\sqrt{\tfrac{\min\{\gamma_1,\mu\}}{L}}\Big)^{k-1}\right\}\quad(k\ge1).\tag{100}$$

All four conclusions are part of the goal: (98) alone does not carry a rate.

Milestones

1. The equivalent form (96)–(97) (p. 24): Algorithm 1 is the scheme $\frac{\gamma_{k+1}-\gamma_k}{\alpha_k}=\mu-\gamma_k$, $\frac{y_k-x_k}{\alpha_k}=\frac{\gamma_k}{\gamma_{k+1}}(v_k-y_k)$, $\frac{v_{k+1}-v_k}{\alpha_k}=\frac{\mu}{\gamma_{k+1}}(y_k-v_k)-\frac1{\gamma_{k+1}}\nabla f(y_k)$ with the decrease step (97) and $L\alpha_k^2=\gamma_{k+1}$.
2. The formulas for $v_k$ and $v_{k+1}$ in terms of $y_k$, $x_k$, $\nabla f(y_k)$ (p. 24).
3. The direct-computation identity for $\frac{\gamma_{k+1}}2\|v_{k+1}-x^*\|^2-\frac{\gamma_k}2(1-\alpha_k)\|v_k-x^*\|^2$ (p. 24).
4. Its $\mu$-convexity bound (p. 25).
5. The one-step bound $\mathcal L_{k+1}-(1-\alpha_k)\mathcal L_k\le f(x_{k+1})-f(y_k)+\frac{\alpha_k^2}{2\gamma_{k+1}}\|\nabla f(y_k)\|^2$ (p. 25).
6. Lemma B.1 (p. 37): for $L_k\alpha_k^2=\gamma_{k+1}$, $\gamma_{k+1}=(1-\alpha_k)\gamma_k+\mu\alpha_k$, positivity, $\alpha_k\le1$, $\alpha_k\ge\sqrt{\min\{\gamma_1,\mu\}/L}$, and the bounds (129)–(130) on $\prod_{i<k}(1-\alpha_i)$.

A companion item states (103) of Remark 6.3 for Algorithm 1: with $\mu=0$, $\gamma_0=L$, $v_0=x_0$, $f(x_k)-f(x^*)\le\frac{4L}{k^2}\|x_0-x^*\|^2$.

Significance

Theorem 6.1 recovers, by a Lyapunov argument, the optimal rates of Nesterov's method in both regimes: $O(L/(\gamma_0k^2))$ for convex $f$ and $(1-\sqrt{\mu/L})^k$ for strongly convex $f$ once $\gamma_1\ge\mu$, with the parameter $\gamma_k$ moving between them automatically. It covers every sufficient-decrease choice of $x_{k+1}$, not only the gradient step, and it places Nesterov's method in the same family as the predictor–corrector and gradient-corrected schemes of §5, whose analyses share the Lyapunov function (74) and the rate lemmas of Appendix B. Comparing (99) with the rate $(1+\sqrt{\mu/L})^{-k}$ of those schemes shows that Nesterov's method is slightly faster per step, with the same complexity.

The result is proved in the paper; the proof of (100) is omitted as similar to that of (88). Nesterov's rates for related parameterisations have been stated on this platform (Bubeck's monograph, Theorems 3.18–3.19), but not for Algorithm 1 with the adaptive parameter $\gamma_k$, and no machine-checked proof of Theorem 6.1 or Lemma B.1 is known. A formalisation checks the omitted step, pins down where $\alpha_k\le1$ is used, and adds a discrete Lyapunov toolkit for accelerated methods in Hilbert space.

Difficulty

Reading Algorithm 1 directly gives a three-sequence recursion with no visible monotone quantity: $f(x_k)$ itself need not decrease. The contraction (98) holds only for the specific combination (74), and only after the cross terms in $\nabla f(y_k)$ produced by the $v$-update are matched exactly against the sufficient-decrease step; any slack in the step rule $L\alpha_k^2=\gamma_{k+1}$ leaves a positive gradient term. A second difficulty is uniformity in $\mu$: when $\mu=0$ the linear factor $1-\sqrt{\min\{\gamma_1,\mu\}/L}$ equals $1$, so the $O(1/k^2)$ rate must come from a separate estimate of $\prod_{i<k}(1-\alpha_i)$ in terms of the step sizes, which are defined only implicitly by a quadratic equation.

Formalization scope

• $V$ is a real Hilbert space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace); the paper's duality pairing and dual norm are the inner product and the norm (Riesz identification).
• The gradient is an explicit map gradf : V → V with HasGradientAt f (gradf x) x at every point; Mathlib's gradient is not used.
• The classes are structures IsS1 and IsS11; $\mathcal S^{1,1}_{\mu,L}$ includes $0<L$ and $\mu\le L$, and the upper bound (4) is a consequence, not an assumption.
• A run of Algorithm 1 is a structure IsNAGRun of hypotheses on given sequences, one per step. Step 2 records only $\alpha_k>0$ (the page writes $\alpha_k\in(0,1)$, but $\alpha_k=1$ occurs when $\mu=L$, and $\alpha_k\le1$ is a conclusion of the theorem). Step 5 is an inequality, not the gradient step. The step sizes are not replaced by a closed form.
• $x^*$ is a global minimiser of $f$ (the paper's standing assumption, p. 2); $\gamma_1$ is the value produced by the run.
• Indices start at $0$; $(1-s)^k$ and $(1-s)^{k-1}$ are natural powers, with (100) stated for $k\ge1$; (99) is stated for all $k\ge0$.
• Milestones 2 and 3 are stated for one step of (96) with $\alpha_k,\gamma_k,\gamma_{k+1}>0$; milestones 4 and 5 along runs of Algorithm 1 under the hypotheses of Theorem 6.1.
• In Lemma B.1, $L:=\sup_kL_k$ is replaced by an arbitrary real upper bound $L$; the conclusions involving $L$ weaken as $L$ grows, so this is equivalent when the supremum is finite.

A statement that assumes the contraction (98) for arbitrary sequences, or fixes $x_{k+1}$ to the gradient step, or states only (98), would not be Theorem 6.1 and is ruled out: the goal quantifies over all runs of Algorithm 1 and states all four conclusions.

Contributions welcome: proofs of Lemma B.1 (a self-contained statement about real sequences), the algebraic milestones 1–3, and the convexity steps 4–5. The definitions are local to this mission and duplicate those of the other missions of the series, to be merged later.

Selected references

• H. Luo, L. Chen, From differential equation solvers to accelerated first-order methods for convex optimization, Math. Program. 195 (2022); arXiv:1909.03145v4. https://arxiv.org/abs/1909.03145
• Y. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• 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); arXiv:1503.01243. https://arxiv.org/abs/1503.01243
• S. Bubeck, Convex Optimization: Algorithms and Complexity, Found. Trends Mach. Learn. 8 (2015); arXiv:1405.4980. https://arxiv.org/abs/1405.4980

Motivation

Nesterov's accelerated gradient method minimises a smooth convex function $f$ to accuracy $\varepsilon$ in $O(1/\sqrt{\varepsilon})$ gradient evaluations, and a $\mu$-strongly convex one in $O(\sqrt{L/\mu}\log(1/\varepsilon))$, which is optimal for first-order methods. The method's original derivation by estimate sequences gives little insight into why it accelerates. Since Su, Boyd and Candès (arXiv:1503.01243) a large literature reads accelerated methods as discretisations of second-order ordinary differential equations and proves their rates with Lyapunov functions transported from the continuous to the discrete setting.

H. Luo and L. Chen, From differential equation solvers to accelerated first-order methods for convex optimization (arXiv:1909.03145, Math. Program. 2022), introduce the NAG flow, a first-order system in a position variable $x$, a velocity-like variable $v$ and a scaling parameter $\gamma$, whose Lyapunov function decays exponentially for every $\mu\ge0$. They then show that standard ODE-solver constructions applied to this flow (implicit Euler, Gauss–Seidel splitting, predictor–corrector, gradient correction) produce explicit methods with accelerated rates, and that Nesterov's method is one of them. This mission formalises the paper's analysis of the predictor–corrector scheme of §5.2, its first explicit accelerated method.

Setting

Let $V$ be a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. A function $f:V\to\mathbb R$ with gradient map $\nabla f$ belongs to $\mathcal S^1_\mu$ (with $\mu\ge0$) if it is continuously differentiable and $\mu$-convex:

$$f(x)-f(y)-\langle\nabla f(y),x-y\rangle\ge\tfrac{\mu}{2}\|x-y\|^2\qquad\forall x,y\in V.$$

It belongs to $\mathcal S^{1,1}_{\mu,L}$ if moreover $\nabla f$ is $L$-Lipschitz with $0\le\mu\le L<\infty$. The value $\mu=0$ (plain convexity) is allowed throughout. A point $x^*$ minimises $f$ globally.

The method keeps two iterates $x_k,v_k$, a step size $\alpha_k>0$ and a parameter $\gamma_k>0$ that evolves by the implicit parameter equation

$$\frac{\gamma_{k+1}-\gamma_k}{\alpha_k}=\mu-\gamma_{k+1},\qquad\gamma_0>0.\tag{73}$$

The predictor–corrector scheme computes a predictor $y_k$, then $v_{k+1}$, then the corrector $x_{k+1}$:

$$\frac{y_k-x_k}{\alpha_k}=v_k-y_k,\qquad\frac{v_{k+1}-v_k}{\alpha_k}=\frac{\mu}{\gamma_k}(y_k-v_{k+1})-\frac{1}{\gamma_k}\nabla f(y_k),\qquad\frac{x_{k+1}-x_k}{\alpha_k}=v_{k+1}-x_{k+1}.\tag{83}$$

Every line is linear in the unknown, so one step costs one gradient evaluation. The Lyapunov function is

$$\mathcal L_k=f(x_k)-f(x^*)+\frac{\gamma_k}{2}\|v_k-x^*\|^2.\tag{74}$$

The Gauss–Seidel step (80) is the scheme without the predictor: $(x_{k+1}-x_k)/\alpha_k=v_k-x_{k+1}$ and the $v$-update evaluated at $x_{k+1}$.

Formalization targets

Goal: Theorem 5.1

If $f\in\mathcal S^{1,1}_{\mu,L}$ and the step sizes satisfy $L\alpha_k^2=\gamma_k(1+\alpha_k)$, then every run of (83) with (73) satisfies

$$\mathcal L_{k+1}\le\frac{\mathcal L_k}{1+\alpha_k}\quad(k\in\mathbb N),\tag{86}$$ $$\mathcal L_k\le\mathcal L_0\min\left\{\frac{4L}{(\sqrt{\gamma_0}\,k+2\sqrt L)^2},\left(1+\sqrt{\tfrac{\min\{\gamma_0,\mu\}}{L}}\right)^{-k}\right\}\quad(k\ge0),\tag{87}$$ $$\mathcal L_k\le C_{\gamma_0,L}\min\left\{\frac{4}{k^2},\left(1+\sqrt{\tfrac{\min\{\gamma_0,\mu\}}{L}}\right)^{1-k}\right\}\quad(k\ge1),\tag{88}$$

with $C_{\gamma_0,L}=\frac{L}{\gamma_0}(f(x_0)-f(x^*))+\frac L2\|v_0-x^*\|^2$. All three conclusions are part of the goal; (86) alone would not carry the rate.

Milestones

1. Lemma 5.1 (p. 19): for one Gauss–Seidel step (80) with any $\alpha_k>0$ and $f\in\mathcal S^1_\mu$, the estimates (81) and (82) on $\mathcal L_{k+1}-\mathcal L_k$.
2. The bound on $\widehat{\mathcal L}_k$ (p. 20), where $\widehat{\mathcal L}_k=f(y_k)-f(x^*)+\frac{\gamma_{k+1}}2\|v_{k+1}-x^*\|^2$ (84).
3. The corrector relation (p. 20): $x_{k+1}-y_k=\frac{\alpha_k}{1+\alpha_k}(v_{k+1}-v_k)$.
4. Inequality (85) (p. 21): $\mathcal L_{k+1}\le\frac{\mathcal L_k}{1+\alpha_k}+\Bigl(\frac{L\alpha_k^2}{2(1+\alpha_k)^2}-\frac{\gamma_k}{2(1+\alpha_k)}\Bigr)\|v_{k+1}-v_k\|^2$ for any $\alpha_k>0$.
5. Lemma B.2 (pp. 38–39): positivity of $\gamma_k$, the lower bound $\alpha_k\ge\sqrt{\min\{\gamma_0,\mu\}/L}$, and two-sided bounds on $\prod_{i<k}(1+\alpha_i)^{-1}$.
6. The $\alpha_0$ bound (p. 21): $\frac{1}{1+\alpha_0}\le\frac{L}{\gamma_0}$ when $L\alpha_0^2=\gamma_0(1+\alpha_0)$.

Significance

Theorem 5.1 gives a single explicit method, with one gradient call per step and no restart, whose rate is $O(L/(\gamma_0k^2))$ when $\mu=0$ and $O((1+\sqrt{\mu/L})^{-k})$ when $\mu>0$ and $\gamma_0\ge\mu$; the parameter $\gamma_k$ interpolates between the two regimes automatically. Both rates are the optimal ones for first-order methods. The same Lyapunov argument, with Lemma B.2 as its rate engine, is reused in the paper for the gradient-corrected scheme (Theorem 5.2), Nesterov's method (Theorem 6.1) and the composite methods of §7, so the milestones of this mission are the shared core of the series.

The result is proved in the paper, with the proof of Lemma B.2 omitted as similar to that of Lemma B.1. No machine-checked proof of Theorem 5.1, Lemma 5.1 or Lemma B.2 is known. A formalisation checks the omitted proof, fixes the exact hypotheses of each step (which estimate needs only $\mu$-convexity and which needs the Lipschitz gradient), and supplies a reusable discrete Lyapunov toolkit for accelerated methods in Hilbert space.

Difficulty

The obvious approach, imitating the continuous argument with the Gauss–Seidel splitting (80), fails: Lemma 5.1 leaves the cross term $-\alpha_k\langle\nabla f(x_{k+1}),v_{k+1}-v_k\rangle$, which has no sign, and bounding it by Cauchy–Schwarz as in (82) produces a positive gradient term that destroys the contraction. The predictor–corrector scheme is designed so that this cross term cancels exactly against the descent inequality for $f$ between $y_k$ and $x_{k+1}$, and the remaining square vanishes only under the precise step rule $L\alpha_k^2=\gamma_k(1+\alpha_k)$. Turning the contraction into the rates (87)–(88) requires lower bounds on $\alpha_k$ that hold uniformly in $\mu\ge0$, which is the content of Lemma B.2. When $\mu=0$ the linear-rate bound is vacuous, so the $O(1/k^2)$ rate must come from a separate estimate.

Formalization scope

• $V$ is a real Hilbert space (NormedAddCommGroup, InnerProductSpace ℝ, CompleteSpace); the paper's duality pairing and dual norm are the inner product and the norm, by the Riesz identification.
• The gradient is an explicit map gradf : V → V with HasGradientAt f (gradf x) x at every point; Mathlib's gradient, which is $0$ at non-differentiable points, is not used.
• The classes are structures IsS1 and IsS11. The class $\mathcal S^{1,1}_{\mu,L}$ includes $0<L$ and $\mu\le L$; the upper quadratic bound (4) is a consequence, not an assumption.
• The scheme (83), the Gauss–Seidel step (80) and the parameter equation (73) are hypotheses on given sequences, each line in the paper's difference-quotient form. Implicit lines are kept as equations. The step sizes are any positive sequence satisfying $L\alpha_k^2=\gamma_k(1+\alpha_k)$; no closed form is substituted.
• $x^*$ is a global minimiser of $f$ (the paper's standing assumption on p. 2).
• Indices start at $0$; the powers $(1+s)^{-k}$ and $(1+s)^{1-k}$ are integer powers; (88) is stated for $k\ge1$, (87) for all $k\ge0$.
• Lemma 5.1 is stated for a single step with $\gamma_k>0$ given, which is the form in which §5.2 applies it to the predictor $y_k$.
• In Lemma B.2, the paper's $L:=\sup_kL_k$ is replaced by an arbitrary real upper bound $L$ of $(L_k)$; both conclusions involving $L$ weaken as $L$ grows, so this is equivalent when the supremum is finite.

A statement that assumed $\mathcal L_{k+1}\le\mathcal L_k/(1+\alpha_k)$ and derived only the rates, or that quantified over arbitrary sequences rather than runs of (83), would be Lemma B.2's corollary and not Theorem 5.1; the goal quantifies over runs of the scheme.

The development needs elementary Hilbert-space identities, the descent inequality (4) for functions with Lipschitz gradient, and real-sequence estimates for products and square roots. The same definitions and Lemma B.2 recur in the series' missions on Theorems 5.2, 7.2 and 7.3. Proofs of any milestone, and of (4) as an auxiliary lemma, are welcome.

Selected references

• H. Luo and L. Chen, From differential equation solvers to accelerated first-order methods for convex optimization, Mathematical Programming, 2022. Preprint arXiv:1909.03145v4. https://arxiv.org/abs/1909.03145
• W. Su, S. Boyd and E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, Journal of Machine Learning Research 17(153), 2016. https://arxiv.org/abs/1503.01243
• Y. Nesterov, Lectures on Convex Optimization, 2nd ed., Springer Optimization and Its Applications 137, 2018. https://doi.org/10.1007/978-3-319-91578-4