All missions

Motivation

Accelerated first-order methods, the heavy-ball method of Polyak and Nesterov's accelerated gradient (NAG) method, reach an error $\varepsilon$ on a $\mu$-strongly convex, $L$-smooth problem in $O(\sqrt{\kappa}\log(1/\varepsilon))$ gradient steps, $\kappa=L/\mu$, against $O(\kappa\log(1/\varepsilon))$ for plain gradient descent. A long line of work has tried to explain where this square root comes from by reading the methods as discretizations of ordinary differential equations: Su, Boyd and Candès (arXiv:1503.01243), Wibisono, Wilson and Jordan (arXiv:1603.04245), and others.

Luo and Chen (arXiv:1909.03145, Math. Program. 2022) take the view from numerical analysis. Section 2 of their paper treats the quadratic case: the gradient flow $x'=-Ax$ is stiff, and an explicit scheme for it needs step size $O(1/\kappa(A))$. They embed $A$ in a $2\times2$ block matrix $G$ whose spectrum lies in the left half-plane with condition number $\sqrt{\kappa(A)}$, and they show that an explicit Gauss–Seidel splitting scheme for $y'=Gy$ is stable with step size of order $1/\sqrt{\kappa(A)}$. This is the linear-algebra core of the paper's argument. The later sections build the nonlinear schemes (missions 2–8 of this series) on it.

Setting

Let $A$ be a real symmetric $d\times d$ matrix. Its eigenvalues are real, and we assume

$$0<\mu=\lambda_{\min}(A)\le\lambda\le\lambda_{\max}(A)=L\qquad\text{for all }\lambda\in\sigma(A),$$

with condition number $\kappa(A)=L/\mu$. For any real square matrix $M$, the spectrum $\sigma(M)$ is the set of its eigenvalues, which are complex in general, and the spectral radius is $\rho(M)=\max_{\lambda\in\sigma(M)}|\lambda|$.

The two transformations (39) of the paper are the $2d\times2d$ block matrices

$$G_{\mathrm{HB}}=\begin{pmatrix}0 & I\\ -A/\mu & -2I\end{pmatrix},\qquad G_{\mathrm{NAG}}=\begin{pmatrix}-I & I\\ I-A/\mu & -I\end{pmatrix}.$$

For the linear system $y'=Gy$, write $G=M+N$, where $M$ is the block lower triangular part of $G$ (the two diagonal blocks and the lower-left block) and $N=G-M$. The Gauss–Seidel splitting scheme (41) with step size $\alpha>0$ is

$$\frac{y_{k+1}-y_k}{\alpha}=My_{k+1}+Ny_k,\qquad\text{i.e.}\qquad y_{k+1}=E(\alpha,G)\,y_k,\quad E(\alpha,G)=(I-\alpha M)^{-1}(I+\alpha N).$$

The matrix $I-\alpha M$ is block lower triangular with diagonal blocks that are multiples of $I$, so the scheme is explicit and never inverts $A$. A one-step scheme is A-stable if $\rho(E(\alpha,G))<1$.

Appendix A works with the scalar model $R=\begin{pmatrix}-a&c\\-b&-d\end{pmatrix}$, where $a,b,c,d\ge0$ and $\operatorname{tr}R<0<\det R$, and with its Gauss–Seidel matrix $E(\alpha,R)$, defined in the same way from the lower triangular part of $R$.

Formalization targets

Goal: Theorem 2.1 (p. 10)

For $G=G_{\mathrm{HB}}$ or $G=G_{\mathrm{NAG}}$, if $0<\alpha\le2/\sqrt{\kappa(A)}$, then the scheme is A-stable and

$$\rho(E(\alpha,G))\le\frac{1}{\sqrt{1+2\alpha}}.$$

Milestones (Appendix A, pp. 35–36)

1. (124): the closed form of $E(\alpha,R)$, and $0<\det E(\alpha,R)=1/(1+|\operatorname{tr}R|\alpha+ad\alpha^2)<1$.
2. Lemma A.1: if $|\operatorname{tr}R|-2\sqrt{\det R}\le bc\,\alpha\le|\operatorname{tr}R|+2\sqrt{\det R}$, then $\rho(E(\alpha,R))=1/\sqrt{1+|\operatorname{tr}R|\alpha+ad\alpha^2}<1$.
3. The heavy-ball reduction: a closed block form of $E(\alpha,G_{\mathrm{HB}})$, and $\sigma(E(\alpha,G_{\mathrm{HB}}))=\bigcup_{\lambda\in\sigma(A)}\sigma(E(\alpha,R(\lambda)))$ with $R(\lambda)=\begin{pmatrix}0&1\\-\lambda/\mu&-2\end{pmatrix}$.
4. Heavy-ball spectral radius: under (127), $\rho(E(\alpha,G_{\mathrm{HB}}))=1/\sqrt{1+2\alpha}$.
5. NAG spectral radius: under (127), $\rho(E(\alpha,G_{\mathrm{NAG}}))=1/\sqrt{1+2\alpha+\alpha^2}\le1/\sqrt{1+2\alpha}$.

Companion statements

• Proposition 2.1 (p. 9): $\operatorname{Re}\lambda<0$ on $\sigma(G)$ and $\kappa(G_{\mathrm{HB}})=\kappa(G_{\mathrm{NAG}})=\sqrt{\kappa(A)}$.
• The choice $\alpha=2/\sqrt{\kappa(A)}$ (p. 36): $\rho(E(\alpha,G))\le1/\sqrt{1+4/\sqrt{\kappa(A)}}\le1/(1+1/\sqrt{\kappa(A)})$.

The goal is the weakest of these statements. Milestones 4 and 5 show that it is attained for heavy ball and strict for NAG.

Significance

The result. Theorem 2.1 gives a contraction factor $1/(1+1/\sqrt{\kappa(A)})$ per step for an explicit, matrix-free scheme. Applied to $f(x)=\tfrac12x^\top Ax$, that is the accelerated linear rate. Eliminating $v$ from $y=(x,v)$ shows that both transformations discretize the same second-order ODE $\mu x''+2\mu x'+\nabla f(x)=0$. The theorem therefore explains acceleration as a stability property of an ODE solver, not as an algebraic trick. The paper's nonlinear schemes (predictor–corrector, gradient correction, Nesterov's method, the proximal variants) are built from this splitting. Their Lyapunov analyses generalize the spectral computation formalized here.

Formalizing it. The result is proved in the paper; to our knowledge no machine-checked proof exists. A formalization has to make the paper's "it is clear that" spectral reduction rigorous: the block diagonalisation through $A=U\Lambda U^\top$ and the identification of the spectrum of a structured $2d\times2d$ non-symmetric matrix with a union of $2\times2$ spectra. It also has to treat spectra of real matrices over $\mathbb C$. Both are reusable well beyond this paper, since every spectral analysis of a momentum method (heavy ball, NAG, their discretizations) runs through the same reduction.

Difficulty

The obvious route bounds a norm of $E(\alpha,G)$. It fails: $E(\alpha,G)$ is not normal, and the paper stresses that $\|E\|_2$ is not controlled by $\rho(E)$. The bound concerns eigenvalues only, and the eigenvalues are complex.

A second naive route applies a Gershgorin or field-of-values estimate to $G$ directly. It loses the square root, because the off-diagonal blocks $A/\mu$ have norm $\kappa(A)$. The real content is that for each eigenvalue $\lambda$ of $A$, the $2\times2$ Gauss–Seidel matrix has a negative discriminant exactly when the step-size condition holds. Its eigenvalues are then a conjugate pair on the circle of radius $\sqrt{\det E}$, and $\det E$ does not depend on $\lambda$. Reaching this needs three things: the reduction of the block spectrum to scalar spectra, the explicit inverse of $I-\alpha M$, and a careful equivalence of the discriminant condition with (126).

Formalization scope

Matrices are Matrix (Fin d) (Fin d) ℝ, and the block matrices live on Fin d ⊕ Fin d, built with Matrix.fromBlocks.

• The splitting. It is blockwise: $M$ takes the two diagonal blocks and the lower-left block of $G$. That is how the paper's own formula for $E(\alpha,G_{\mathrm{HB}})$ reads it; the entrywise lower triangle would split $A$ itself.
• Spectra. The spectrum of a real matrix is spectrum ℂ of its complexification. "$\rho(M)=r$" is IsGreatest of the set of eigenvalue moduli. "$\rho(M)\le r$" and "$\rho(M)<1$" are stated eigenvalue by eigenvalue, so no junk supremum over an empty set can make a bound vacuous.
• The model matrix. $\mu=\lambda_{\min}(A)$ and $L=\lambda_{\max}(A)$ are encoded as hypotheses: both are eigenvalues of $A$ and bound every eigenvalue. $\kappa(A)$ is the number $L/\mu$. Every statement assumes $\mu>0$, the case of §2.3 where $G_{\mathrm{HB}}$ and $G_{\mathrm{NAG}}$ are defined.
• Step size and inverse. The step size satisfies $\alpha>0$, which the paper leaves implicit in (124). The matrix inverse in $E$ is Mathlib's. It is genuine here, because $I-\alpha M$ is invertible for $\alpha>0$.

Two trivializations are ruled out explicitly. A spectral radius defined as sSup over a possibly empty spectrum would make every bound hold vacuously at $d=0$. A spectrum taken over $\mathbb R$ would miss the complex eigenvalues, which are all of them here.

A complete development needs:

• block-diagonalisation of the structured block matrices by $\operatorname{diag}(U,U)$ and a permutation;
• the spectrum of a block-diagonal matrix of $2\times2$ blocks;
• the eigenvalues of a real $2\times2$ matrix with negative discriminant;
• explicit $2\times2$ and block-triangular inverses.

Lemmas of this kind, stated for general symmetric $A$, are welcome as separate theorems.

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
• W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, JMLR 17 (2016). https://arxiv.org/abs/1503.01243
• A. Wibisono, A. C. Wilson, M. I. Jordan, A variational perspective on accelerated methods in optimization, PNAS 113 (2016). https://arxiv.org/abs/1603.04245
• B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Comput. Math. Math. Phys. 4 (1964). https://doi.org/10.1016/0041-5553(64)90137-5
• E. Hairer, G. Wanner, Solving Ordinary Differential Equations II: Stiff and Differential-Algebraic Problems, Springer, 1996 (A-stability). https://doi.org/10.1007/978-3-642-05221-7

Motivation

Many problems in optimization reduce to a linear complementarity problem over a cone: convex quadratic programs, linear and second-order cone programs, and more generally the KKT systems of convex quadratic cone programs (QCPs). First-order solvers for these problems, such as SCS (O'Donoghue–Chu–Parikh–Boyd 2016), must return either a solution or a certificate that none exists, and must do so reliably at scale; in branch-and-bound methods for mixed-integer quadratic programs, for example, fast and robust infeasibility certificates decide which branches are pruned. O'Donoghue (arXiv:2004.02177v4) embeds a monotone linear complementarity problem into a single homogeneous problem that always has a solution, from which either an answer or a certificate of infeasibility can be read off, and solves the embedded problem by Douglas–Rachford (DR) splitting. This is the algorithm behind SCS 3.0.

DR splitting converges for the sum of two maximal monotone operators. The mission formalizes the result that makes the method applicable: the paper's embedding operator is maximal monotone.

Setting

Write $\mathbb R^{d+1}=\mathbb R^d\times\mathbb R$ with points $u=(z,\tau)$ and inner product $(z,\tau)^\top(w,\kappa)=z^\top w+\tau\kappa$. An operator on $\mathbb R^d\times\mathbb R$ is identified with its graph, a set of pairs (point, value). It is monotone if $(u-v)^\top(x-y)\ge 0$ for all pairs $(x,u),(y,v)$ in it, and maximal monotone if it is monotone and not strictly contained in another monotone operator.

Fix $M\in\mathbb R^{d\times d}$ and $q\in\mathbb R^d$. The matrix $M$ is monotone if $M+M^\top\succeq 0$ (3.4); $M$ need not be symmetric. For a nonempty closed convex cone $\mathcal C\subseteq\mathbb R^d$ with dual cone $\mathcal C^*$, the problem $\mathrm{LCP}(M,q,\mathcal C)$ asks for $z$ with

$$\mathcal C\ni z\perp(Mz+q)\in\mathcal C^* .$$

The paper introduces three operators on $\mathbb R^d\times\mathbb R$:

• the Andersen–Ye feasibility embedding (4.1), defined for $\tau>0$ only:

$$\mathcal F(z,\tau)=\bigl(Mz+q\tau,\ -z^\top Mz/\tau-z^\top q\bigr);$$

• the infeasibility embedding (4.7), defined on $\{(z,0)\mid z^\top Mz=0\}$:

$$\mathcal I(z,0)=\{(Mz,\kappa)\mid \kappa\le -z^\top q\};$$

• their union $\mathcal Q=\mathcal F\cup\mathcal I$.

The embedded problem is $0\in\mathcal Q(u)+N_{\mathcal C\times\mathbb R_+}(u)$. Its solutions with $\tau>0$ give solutions $z/\tau$ of the LCP, and its solutions with $\kappa>0$ give certificates of infeasibility.

Formalization targets

Goal: Lemma 4.4

For every monotone $M$ and every $q$,

$$\mathcal Q=\mathcal F\cup\mathcal I\ \text{ is maximal monotone on } \mathbb R^d\times\mathbb R .$$

Milestones

In the order the proof of Lemma 4.4 uses them:

1. (3.6): for monotone $M$, $z^\top Mz=0\iff(M+M^\top)z=0$.
2. Lemma 4.1: $\mathcal F$ is monotone.
3. Lemma 4.3: $\mathcal I$ is monotone.
4. $\mathcal Q$ is monotone (first paragraph of the proof of Lemma 4.4).
5. If $p_\tau>0$ and $(p,r)$ is monotonically related to every pair of $\mathcal F$, then $r=\mathcal F(p)$.
6. (4.11)–(4.13): if $p_\tau=0$ and $(p,r)$ is monotonically related to every pair of $\mathcal F$, then $p_z^\top Mp_z=0$, $Mp_z=r_z$ and $r_\tau\le -p_z^\top q$, that is, $(p,r)\in\mathcal I$.

Companion results

The mission also states the following results of the same construction:

• $\mathcal F$ alone is not maximal monotone (p. 7).
• Lemma 4.2 in certificate form: $\lambda$ satisfies (4.4) iff $\lambda^\top q<0$ and $\mathcal C\ni\lambda\perp M\lambda\in\mathcal C^*$ (p. 8).
• The weak alternatives between $\mathrm{LCP}(M,q,\mathcal C)$ and its certificate system (p. 8).
• The decoding of solutions of the embedded problem, Table 1 (p. 10).
• The closed-form resolvent of $\mathcal Q$, (5.3)–(5.5) (pp. 12–13).
• Lemma 5.1: DR iterates do not collapse to the trivial solution (p. 14).

Significance

Lemma 4.4 is the hinge of the paper. $N_{\mathcal C\times\mathbb R_+}$ is maximal monotone, so once $\mathcal Q$ is too, DR splitting applied to the embedded inclusion converges for every LCP with monotone $M$, feasible or not. This holds whether the problem has a solution or a certificate, without the strict feasibility or strong duality an interior-point homogeneous model relies on. The closed-form resolvent and Lemma 5.1 then turn this into Algorithm 5.1: one cached linear solve with $I+M$ and one scalar quadratic per iteration.

The result is proved in the paper. The DR convergence theorem itself and the extension theorem used for maximality are cited from Bauschke–Combettes. To our knowledge none of the results here has been machine-checked. A formal proof supplies two pieces of value. First, an argument for maximality that does not rest on the Zorn-based extension theorem the paper invokes. Second, a checked statement of the operator underlying a widely used solver, with its exact domains.

Difficulty

Monotonicity of $\mathcal F$, of $\mathcal I$ and of their union is matrix algebra plus (3.6). The difficulty is maximality: given a pair $(p,r)$ that is monotonically related to every pair of $\mathcal Q$, one must show it already lies in $\mathcal Q$. There are three regimes, according to the sign of $p_\tau$.

• $p_\tau>0$. The pair lies in the open domain of a continuous operator.
• $p_\tau=0$. The paper's limit argument as $\tau\to0$ yields (4.11)–(4.13).
• $p_\tau<0$. The paper rules this case out through a general theorem on maximal monotone extensions with domain in the closed convex hull of the original domain [Bauschke–Combettes, Thm 21.9]. That theorem is not available in Mathlib.

The naive route, "$\mathcal F$ is continuous and monotone, so it is maximal", fails because $\operatorname{dom}\mathcal F$ is open and not the whole space. Indeed $\mathcal F$ alone is not maximal. The boundary behaviour is carried entirely by $\mathcal I$, whose domain condition $z^\top Mz=0$ is exactly what monotonicity forces in the limit.

Formalization scope

Points of $\mathbb R^{d+1}$ are pairs in (Fin d → ℝ) × ℝ, and the inner product is $z^\top w+\tau\kappa$ written with dotProduct. Operators are Sets of (point, value) pairs. Maximal monotonicity is the containment form over all monotone operators on this space.

The standing assumption "M is monotone" is the explicit hypothesis (M + Mᵀ).PosSemidef in every theorem that involves $M$ (all but Lemma 5.1). It is not $M\succeq 0$ (which would force symmetry), and the lemmas' sentences do not repeat it. The cone $\mathcal C$ does not enter $\mathcal Q$ and is not a hypothesis of the goal. Where a companion uses it, it is a nonempty, closed, convex cone, as on p. 4. The supremum in (4.4) is written pointwise. The dimension $d=0$ is allowed; the goal is true there.

The domain conditions are part of the graphs: $\tau>0$ in $\mathcal F$, and $\tau=0$ together with $z^\top Mz=0$ in $\mathcal I$. Each of the following trivializing or falsifying formalizations is ruled out:

• $\mathcal F$ without $\tau>0$: Lean's $x/0=0$ would add spurious pairs and make Lemma 4.4 false.
• $\mathcal I$ without $z^\top Mz=0$: this breaks the monotonicity of $\mathcal Q$.
• A "maximality" that is only monotonicity, or maximality among single-valued operators only.
• A pairing of points with values in place of differences.

Lemma 4.2 is stated in the certificate form its proof establishes. The distance-based notion of strong infeasibility is not formalized.

The development needs only finite-dimensional linear algebra from Mathlib: Matrix.mulVec, dotProduct, Matrix.PosSemidef, matrix inverse, and EuclideanSpace for Lemma 5.1. The definitions of monotone and maximal monotone graphs on $\mathbb R^d\times\mathbb R$ are reusable. Welcome contributions include:

• a direct proof of the case $p_\tau<0$ that avoids the cited extension theorem [7, Thm 21.9];
• a general lemma that a continuous monotone map on an open set admits no extension pair inside it;
• proofs of the companion results.

Selected references

• B. O'Donoghue, Operator splitting for a homogeneous embedding of the linear complementarity problem, SIAM J. Optim. 31(3), 2021, https://doi.org/10.1137/20M1366307; the mission cites the preprint arXiv:2004.02177v4, https://arxiv.org/abs/2004.02177v4
• H. H. Bauschke and P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, 2nd ed., Springer, 2017. https://doi.org/10.1007/978-3-319-48311-5
• E. D. Andersen and Y. Ye, On a homogeneous algorithm for the monotone complementarity problem, Math. Program. 84, 1999 (reference [2] of https://arxiv.org/abs/2004.02177).
• B. O'Donoghue, E. Chu, N. Parikh, S. Boyd, Conic optimization via operator splitting and homogeneous self-dual embedding, J. Optim. Theory Appl. 169, 2016. https://doi.org/10.1007/s10957-016-0892-3
• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173

Motivation

Many convex problems in signal processing, statistics and control have the composite form "smooth loss plus nonsmooth regulariser, subject to a simple constraint": a least-squares or entropy term $h$, a sparsity or total-variation penalty $g$, and a feasible set $Q$ such as a box, a simplex or a cone. Accelerated proximal gradient methods (FISTA, Beck and Teboulle 2009; Nesterov's composite gradient methods) reach the optimal $O(1/k^2)$ rate for such problems when $Q = V$. When a constraint is present, the standard schemes evaluate $\nabla h$ at extrapolated points that may leave $Q$; for an $h$ such as the entropy on $Q=[0,\infty)$, that gradient does not exist.

Luo and Chen (arXiv:1909.03145v4, Math. Program. 2022) derive accelerated first-order methods as discretisations of a single ODE, the NAG flow, and analyse every scheme with one discrete Lyapunov function. Their Section 7.3 turns the predictor–corrector discretisation into a forward–backward splitting, the semi-implicit accelerated forward–backward method (Semi-AFB), whose iterates stay in $Q$ by construction, and proves for it the same rate as for the unconstrained smooth case.

Timeline. Tseng (2008) gave an accelerated proximal gradient method with rate $O(L/k^2)$ for this problem with $\mu = 0$. Nesterov (Math. Program. 2013, "Gradient methods for minimizing composite functions") treated the same problem with $h$ $L$-smooth on $Q$ and $g$ $\mu$-strongly convex, $\mu\ge0$, and obtained the rate $O(\min\{L/k^2,(1+\sqrt{\mu/L})^{-k}\})$ with estimate sequences, at the cost of two proximal computations over $Q$ per iteration. Luo and Chen's Theorem 7.3 (2019, revised 2022) gives the same type of rate with one proximal computation per iteration and a Lyapunov proof.

Setting

$V$ is a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. For a set $\Omega\subseteq V$, a function $h$ is in $\mathcal S^1_\mu(\Omega)$ if it is continuously differentiable on $\Omega$, with gradient map $\nabla h$, and

$$h(x)-h(y)-\langle\nabla h(y),x-y\rangle\ \ge\ \frac{\mu}{2}\|x-y\|^2\qquad\forall\,x,y\in\Omega,\quad \mu\ge0 .$$

It is in $\mathcal S^{1,1}_{\mu,L}(\Omega)$ if moreover $\nabla h$ is $L$-Lipschitz on $\Omega$, $0<L<\infty$.

The problem (104) is

$$\min_{x\in Q}\ f(x),\qquad f=h+g,$$

with $Q$ closed and convex, $h\in\mathcal S^{1,1}_{\mu,L}(Q)$, $0\le\mu\le L$, and $g:V\to\mathbb R\cup\{+\infty\}$ proper, closed and convex, with $Q\cap\operatorname{dom}g\ne\emptyset$. Let $x^*$ be a minimiser.

Algorithm 4 (Semi-AFB). Given $x_0,v_0\in Q$ and $\gamma_0>0$, for $k=0,1,\dots$: choose $\alpha_k>0$ with $L\alpha_k^2=\gamma_k(1+\alpha_k)$; set $\gamma_{k+1}=(\gamma_k+\mu\alpha_k)/(1+\alpha_k)$, $y_k=(x_k+\alpha_kv_k)/(1+\alpha_k)$ and $w_k=(\gamma_kv_k+\mu\alpha_ky_k)/(\gamma_k+\mu\alpha_k)$; let

$$v_{k+1}\in\operatorname*{argmin}_{v\in Q}\Bigl\{g(v)+\langle\nabla h(y_k),v\rangle+\frac{\gamma_k+\mu\alpha_k}{2\alpha_k}\|v-w_k\|^2\Bigr\};$$

and set $x_{k+1}=(x_k+\alpha_kv_{k+1})/(1+\alpha_k)$. The Lyapunov function is

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

Formalization targets

Goal: Theorem 7.3 (p. 33)

For every run of Algorithm 4,

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

with $C_{\gamma_0,L}=\frac{L}{\gamma_0}(f(x_0)-f(x^*))+\frac L2\|v_0-x^*\|^2$ (89). The contraction (121) is the core; (87) and (88) are its consequences through Lemma B.2.

Milestones

1. (120): under the optimality variational inequality for $v_{k+1}$, the inner-product bound for $\gamma_k\langle v_{k+1}-v_k,v_{k+1}-x\rangle$.
2. The difference identity for $\mathcal L_{k+1}-\mathcal L_k$ (p. 33).
3. The one-step estimate (123) (p. 34).
4. The $h$-term bound: $x_{k+1}-y_k=\frac{\alpha_k}{1+\alpha_k}(v_{k+1}-v_k)$ and the $h$-terms of (123) are $\le0$ (pp. 34–35).
5. The $g$-term bound: the $g$-terms of (123) are $\le0$ (p. 35).
6. The bound $1/(1+\alpha_0)\le L/\gamma_0$ (p. 21).
7. Lemma B.2: positivity of $\gamma_k$, the lower bound on $\alpha_k$, and the decay of $\prod_{i<k}(1+\alpha_i)^{-1}$ (pp. 38–39).

Significance

The result. Theorem 7.3 shows that one explicit gradient step on $h$ and one proximal step on $g$ restricted to $Q$ per iteration suffice for acceleration, uniformly in $\mu\ge0$: it gives the rate $O(L/k^2)$ for convex $h$ and the linear rate $(1+\sqrt{\min\{\gamma_0,\mu\}/L})^{-k}$ for strongly convex $h$ in one statement, and $\gamma_0$ need not know $\mu$. All iterates $x_k,y_k,v_k$ remain in $Q$, so the method applies when $\nabla h$ exists only on $Q$.

Formalizing it. The theorem is proved on paper, with a short Lyapunov argument; no machine-checked version is known to exist. A formal proof checks the bookkeeping of the argument, including the role of the domain of $g$, and makes the Lyapunov inequality available as a reusable step for other accelerated splitting schemes. The scalar Lemma B.2 is shared with the paper's other schemes (Theorems 5.1, 5.2 and 7.2).

Difficulty

The first-order condition that the paper uses for $v_{k+1}$, a variational inequality with some $p_{k+1}\in\partial g(v_{k+1})$, needs the subdifferential sum rule $\partial(g+i_Q)=\partial g+N_Q$, which requires a constraint qualification that (104) does not impose. It fails, for example, when $Q$ and $\operatorname{dom}g$ meet in a single boundary point. A proof of the goal therefore cannot simply take such a $p_{k+1}$ for granted. The second difficulty is bookkeeping: (2) and (4) hold for $h$ on $Q$ only, so each of the points $x_k,y_k,v_{k+1},x_{k+1},x^*$ at which they are applied must be shown to lie in $Q$, and the convexity of $g$ is used at points that must lie in $\operatorname{dom}g$. Finally, (87) and (88) require the scalar recursion of Lemma B.2 for the product $\prod_{i<k}(1+\alpha_i)^{-1}$, whose square-root estimates are not routine.

Formalization scope

$V$ is a real Hilbert space (InnerProductSpace ℝ V, CompleteSpace V); $V^*$ is identified with $V$ by Riesz. The gradient of $h$ is an explicit map gradh with a gradient of $h$ within $Q$ at every point of $Q$ (HasGradientWithinAt). Nothing is assumed about $h$ off $Q$, and (4) is not assumed. The extended-valued $g$ is encoded by its effective domain D and its real values g : V → ℝ on D. Convexity is ConvexOn ℝ D g, closedness is a closed epigraph, and step 5's argmin over $Q$ is a minimiser over $Q\cap D$. The scheme is a hypothesis on sequences (IsAFBRun), with $\alpha_k$ any positive solution of the step relation. Integer powers are used for $(\cdot)^{-k}$ and $(\cdot)^{1-k}$. Lemma B.2's $L:=\sup_kL_k$ is encoded as any real upper bound of $(L_k)$.

Standing and added hypotheses: $x^*$ minimises $f$ over $Q\cap\operatorname{dom}g$ (the paper assumes argmin $f\ne\emptyset$). $\gamma_0>0$, $\alpha_k>0$ and $L>0$ are inputs of Algorithm 4. The hypothesis $x_0\in\operatorname{dom}g$ is added to the page's $x_0\in Q$, because otherwise $\mathcal L_0=C_{\gamma_0,L}=+\infty$. The goal makes no subgradient or variational-inequality assumption. Milestone (120) carries the variational inequality as an explicit premise. A trivializing formalization would quantify over sequences assumed to satisfy (121), or replace the argmin of step 5 by an arbitrary point of $Q$; the goal quantifies over genuine runs of Algorithm 4, with a genuine minimisation predicate.

A complete development needs elementary Hilbert-space identities, the minimiser inequality for a strongly convex function over a convex set, the descent inequality (4) on a convex set from (3), and the scalar recursion of Lemma B.2. The last two are reusable across the whole series. Contributions to any milestone are welcome.

Selected references

• H. Luo and L. Chen, From differential equation solvers to accelerated first-order methods for convex optimization, Math. Program. (2022); arXiv:1909.03145v4. https://arxiv.org/abs/1909.03145
• Yu. Nesterov, Gradient methods for minimizing composite functions, Math. Program. 140 (2013) 125–161. https://doi.org/10.1007/s10107-012-0629-5
• A. Beck and M. Teboulle, A fast iterative shrinkage-thresholding algorithm for linear inverse problems, SIAM J. Imaging Sci. 2 (2009) 183–202. https://doi.org/10.1137/080716542
• P. Tseng, On accelerated proximal gradient methods for convex-concave optimization, technical report, University of Washington, 2008.
• Yu. Nesterov, Lectures on Convex Optimization, Springer, 2018. https://doi.org/10.1007/978-3-319-91578-4

Motivation

The projected gradient method is the basic algorithm for minimising a smooth convex function over a closed convex set. For an objective with an $L_f$-Lipschitz gradient it converges at the sublinear rate $f(x^k)-f^*\le L_f\|x^0-x^*\|^2/(2k)$, and the classical way to obtain a linear (geometric) rate is to assume strong convexity. Many objectives that arise in practice are not strongly convex: least squares with a rank-deficient matrix, the dual of a linearly constrained problem, or $g(Ax)$ with $g$ strongly convex and $A$ singular. Such problems have a whole set of minimisers rather than a single one, yet the projected gradient method is observed to converge linearly on them.

Necoara, Nesterov and Glineur (arXiv:1504.06298, v4 2016; Math. Program. 175 (2019)) introduce a hierarchy of relaxations of strong convexity, measured relative to the optimal set instead of between arbitrary pairs of points, and prove linear convergence of several first order methods under each of them. This mission formalizes the first such result: linear convergence of the projected gradient method on quasi-strongly convex objectives (Theorem 11 of the preprint).

Related conditions have a longer history: the error bounds of Luo and Tseng (1993) for feasible descent methods and the Polyak–Łojasiewicz inequality (Polyak 1963). Karimi, Nutini and Schmidt (2016) compare several of these in the unconstrained case.

Setting

Let $X\subseteq\mathbb R^n$ be a closed convex set, with the Euclidean inner product $\langle u,v\rangle=u^\top v$ and norm $\|\cdot\|$. Let $f$ be a convex function on $X$, differentiable at every point of $X$, whose gradient is Lipschitz on $X$:

$$\|\nabla f(x)-\nabla f(y)\|\le L_f\|x-y\|\qquad\forall x,y\in X,\quad L_f>0 .$$

Problem (P) is $f^*=\min_{x\in X}f(x)$, with optimal set $X^*=\arg\min_{x\in X}f(x)$, assumed nonempty.

The projection of $u$ onto a closed convex set $S$ is $[u]_S=\arg\min_{z\in S}\|z-u\|$. For $x\in X$ write $\bar x=[x]_{X^*}$ for the point of $X^*$ nearest to $x$; then $\|x-\bar x\|$ is the distance from $x$ to the optimal set.

$f$ is quasi-strongly convex with constant $\kappa_f>0$ if, for every $x\in X$,

$$f^*\ \ge\ f(x)+\langle\nabla f(x),\bar x-x\rangle+\frac{\kappa_f}{2}\|x-\bar x\|^2 .\tag{10}$$

This is the strong convexity inequality with the second point fixed to $\bar x$. It does not force a unique minimiser. The class of convex functions with $L_f$-Lipschitz gradient satisfying (10) is denoted $q\mathcal S_{L_f,\kappa_f}(X)$, and $\mu_f=\kappa_f/L_f$ is the condition number.

The projected gradient method (GM) starts from $x^0\in X$ and iterates

$$x^{k+1}=\big[x^k-\alpha_k\nabla f(x^k)\big]_X,\qquad k\ge0,$$

with step sizes $\alpha_k\le 1/L_f$.

Formalization targets

Goal: Theorem 11

For $f\in q\mathcal S_{L_f,\kappa_f}(X)$ and (GM) with $\alpha_k=1/L_f$, for every $k\ge0$,

$$\|x^k-\bar x^k\|^2\ \le\ \Big(\frac{1-\mu_f}{1+\mu_f}\Big)^k\,\|x^0-\bar x^0\|^2 ,\qquad \mu_f=\frac{\kappa_f}{L_f}. \tag{45}$$

Milestones (proof of Theorem 11, p. 20)

1. The optimality condition of the projection step, (47): $\langle x^{k+1}-x^k+\alpha_k\nabla f(x^k),x-x^{k+1}\rangle\ge0$ for all $x\in X$.
2. Sufficient decrease: $f(x^{k+1})\le f(x^k)-\frac{L_f}{2}\|x^{k+1}-x^k\|^2$ for $\alpha_k\le1/L_f$.
3. Quasi-strong convexity (10) implies quadratic functional growth $f(x)-f^*\ge\frac{\kappa_f}{2}\|x-\bar x\|^2$ (Theorem 4).
4. The one-step inequality $\|x^{k+1}-\bar x^k\|^2\le(1-\alpha_k\kappa_f)\|x^k-\bar x^k\|^2-2\alpha_k(f(x^{k+1})-f^*)$.
5. The contraction (48): $\|x^{k+1}-\bar x^{k+1}\|^2\le\frac{1-\alpha_k\kappa_f}{1+\alpha_k\kappa_f}\|x^k-\bar x^k\|^2$ for $0<\alpha_k\le1/L_f$.

Companions: function values (p. 21)

$$f(x^k)-f^*\le\frac{L_f\|x^0-\bar x^0\|^2}{2}\Big(\frac{1-\mu_f}{1+\mu_f}\Big)^{k-1}\ (k\ge1),\tag{49}$$ $$f(x^k)-f^*\le\frac{L_f\|x^0-\bar x^0\|^2}{2}\cdot\frac{\mu_f}{(1-\mu_f)^{-k}-1}\ (k\ge1,\ \mu_f<1).\tag{50}$$

Significance

Theorem 11 gives a geometric rate for the distance to the optimal set on a class strictly larger than the strongly convex functions. The rate $(1-\mu_f)/(1+\mu_f)$ depends only on the ratio $\kappa_f/L_f$, exactly as in the strongly convex case with $\kappa_f$ in place of the strong convexity constant. Through (49) the rate passes to function values, and (50) interpolates between the linear rate and the classical $O(1/k)$ rate as $\mu_f\to0$. The paper's later sections show that the class contains, for example, $g(Ax)$ over a polyhedron with $g$ strongly convex, which covers dual and least-squares problems with singular data.

The result is proved in the paper; it is not known to be formalized. The mission produces a machine-checked statement of the class (10), the projected gradient iteration with a non-unique optimal set, and the rate (45), together with the intermediate inequalities of the proof. The definitions of the optimal set, the nearest-point projection and the (GM) run are reusable for the companion missions of this series (fast gradient, feasible descent methods) and for other projection-based methods.

Difficulty

The standard proof for strongly convex $f$ compares $x^{k+1}$ with the unique minimiser $x^*$ and uses strong convexity between $x^k$ and $x^*$. Here the minimiser is not unique, and the comparison point $\bar x^k$ changes with $k$: the inequality at step $k$ is written relative to $\bar x^k$, and the bound at step $k+1$ must be relative to $\bar x^{k+1}$. The two are linked only through the nearest-point property $\|x^{k+1}-\bar x^{k+1}\|\le\|x^{k+1}-\bar x^k\|$. In addition, (10) controls only the direction toward $\bar x$, so to absorb the term $f(x^{k+1})-f^*$ the proof needs quadratic functional growth at $x^{k+1}$, which is not part of the hypothesis and requires the separate implication (10) ⇒ (22). That implication uses convexity of $f$ essentially; (10) alone does not imply it with the same constant by a one-line argument.

In Lean, the work includes the descent lemma on a convex set from a gradient that is Lipschitz only on $X$, the variational inequality of the Euclidean projection, and the implication (10) ⇒ (22) with the same constant.

Formalization scope

• The space is EuclideanSpace ℝ (Fin n). $f$ is a function on the whole space, convex on $X$ (ConvexOn ℝ X f) and differentiable at every point of $X$, with $\nabla f$ = gradient f; the Lipschitz bound (1) is required on $X$ with $L_f>0$.
• $X$ is closed and convex; "simple" (cheap projection) is not a mathematical hypothesis and is dropped. $X^*$ is nonempty through a named minimiser; $f^*$ is $f(\bar x)$ for $\bar x\in X^*$, never an infimum.
• The projection is the predicate "$p\in S$ and $\|u-p\|\le\|u-z\|$ for all $z\in S$", not a choice function. A (GM) run is any sequence whose steps are nearest points, starting at $k=0$ (the page's "for $k\ge1$" is a slip). Statements hold for every nearest point $\bar x^k$; on a nonempty closed convex set it is unique.
• The class hypothesis is (10) with constant $\kappa_f>0$, kept separate from convexity and (1). No hypothesis $\kappa_f\le L_f$ is added: if $\kappa_f>L_f$ then (10) and the descent inequality force $X\subseteq X^*$ and the claims hold with both sides zero.
• Companion (50) adds $\kappa_f<L_f$, since at $\mu_f=1$ its right-hand side divides by zero.
• Trivializing formalizations are ruled out: the projection is not a choice that could be junk, $X^*$ cannot be empty, the gradient is only queried at points of $X$ where $f$ is differentiable, and $f^*$ is attained.
• Contributions welcome: proofs of the milestones, in particular the descent lemma on a convex set and the variational inequality for nearest points, which are reusable beyond this mission.

Selected references

• I. Necoara, Yu. Nesterov, F. Glineur, Linear convergence of first order methods for non-strongly convex optimization, arXiv:1504.06298v4, 2016; Math. Program. 175 (2019) 69–107. https://arxiv.org/abs/1504.06298
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Annals of Operations Research 46 (1993) 157–178. https://doi.org/10.1007/BF02096261
• H. Karimi, J. Nutini, M. Schmidt, Linear convergence of gradient and proximal-gradient methods under the Polyak–Łojasiewicz condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636

Motivation

Every fast integer-multiplication algorithm in the literature is stated for the multitape Turing machine. The algorithms are built from a small set of standard subroutines whose costs are usually quoted as "well known":

• linear-time addition;
• sorting by merging on tapes;
• fast matrix transposition;
• a crude $O(n^{1+\delta})$ multiplier, used for the small multiplications inside fixed-point arithmetic.

Harvey–van der Hoeven (2021) use all of these in §2.1, §2.3 and §4–§5 of their $O(n\log n)$ paper. They cite Brent–Zimmermann for the arithmetic, Knuth vol. 3 for merge sort, and Bostan–Gaudry–Schost for transposition.

This mission formalizes that toolkit in the shared machine model IntMul_MultitapeModel. Its goal is the classical Schönhage–Strassen bound $\mathsf M(n)=O(n\log n\log\log n)$. The toolkit is exactly what is missing before the recursive step of the companion mission, Harvey–van der Hoeven Proposition 5.4, can be decomposed. Proposition 5.4 is the last open link on that mission's main line.

Timeline (multitape Turing model).

• Folklore: schoolbook multiplication in $O(n^2)$; addition in $O(n)$.
• 1962: Karatsuba–Ofman, $O(n^{\log_2 3})$.
• 1963–1966: Toom and Cook, $O(n^{1+\epsilon})$ for every $\epsilon>0$.
• 1971: Schönhage–Strassen, $O(n\log n\log\log n)$.
• 1973 (2nd ed. 1998): Knuth, TAOCP vol. 3 §5.4, merge sorting on tapes.
• 2007: Bostan–Gaudry–Schost, Appendix: transposing an $m\times k$ matrix with $N$ bits in total in $O(N\log\min(m,k))$ on a multitape machine.
• 2019/2021: Harvey–van der Hoeven, $O(n\log n)$, using all of the above.

Setting

The machine model, input and output conventions, and the time-bound predicate $\mathrm{MulTimeBound}$ are those of IntMul_MultitapeModel. That model follows Montanaro's lecture notes:

• $k\ge2$ one-way tapes, with a read-only input tape and a separate output tape;
• $\triangleright$ appears only in cell $0$ of each tape;
• $\mathrm{START}\ne\mathrm{HALT}$, and the halting state freezes the configuration.

For subroutines whose input is not of the form $x\#y$, the new definitions file IntMul_MultitapeWords starts the machine on an arbitrary word over $\{0,1,\#\}$. It also provides the encodings

• $\mathrm{bits}(x)$, a bit string written as a word;
• $u_1\#u_2\#\cdots\#u_m$, a list of words joined by separators.

Formalization targets

Goal: Schönhage–Strassen

$\mathrm{MulTimeBound}(n\mapsto n\ln n\ln\ln n)$: a single multitape machine multiplies $n$-bit integers for every $n\ge1$ in worst-case time $O(n\log n\log\log n)$.

Milestones

1. Schoolbook multiplication: $\mathrm{MulTimeBound}(n^2)$.
2. Karatsuba–Ofman: $\mathrm{MulTimeBound}(n^{\log_2 3})$.
3. Linear-time addition: on input $x\#y$ with $|x|=|y|=n$, output $\operatorname{bin}_{n+1}(\operatorname{val}x+\operatorname{val}y)$ within $c(n+1)$ steps.
4. Merge sort on tapes:
   • Input: $m$ records, each a key of $\ell$ bits and a payload of $q$ bits, written as $k_1\#p_1\#k_2\#p_2\#\cdots$.
   • Output: the records stably sorted by key value, in the same format.
   • Time: $c\,(N+1)(\lceil\log_2 m\rceil+1)$, where $N$ is the input length.
5. Matrix transposition:
   • Input: an $m\times k$ matrix ($m,k\ge1$) with entries of $\ell\ge1$ bits, in row-major order. Entries are separated by $\#$ and rows by $\#\#$.
   • Output: the transpose, in the same format.
   • Time: $c\,(N+1)(\lceil\log_2\min(m,k)\rceil+1)$.

Formalization scope

Constants may depend only on the machine. All time bounds count exact steps of one fixed machine in the shared model. Building machines by composing smaller ones (subroutine calls, scratch tapes, recursion) is the solvers' business; any reusable infrastructure for it is welcome as published lemmas.

Selected references

• A. Schönhage, V. Strassen, Schnelle Multiplikation großer Zahlen, Computing 7 (1971), 281–292.
• A. Karatsuba, Yu. Ofman, Multiplication of multidigit numbers on automata, Soviet Physics Doklady 7 (1963), 595–596.
• D. E. Knuth, The Art of Computer Programming, Vol. 3: Sorting and Searching, 2nd ed., Addison-Wesley, 1998, §5.4.
• A. Bostan, P. Gaudry, É. Schost, Linear recurrences with polynomial coefficients and application to integer factorization and Cartier–Manin operator, SIAM J. Comput. 36 (2007), 1777–1806, Appendix.
• R. P. Brent, P. Zimmermann, Modern Computer Arithmetic, Cambridge University Press, 2011, Ch. 1.
• D. Harvey, J. van der Hoeven, Integer multiplication in time $O(n\log n)$, Ann. of Math. 193 (2021), §2.1.
• A. Montanaro, Computational Complexity, lecture notes, §3–§4.

Motivation

Linear convergence of first order methods is classically tied to strong convexity. Many problems in data fitting, machine learning and control are not strongly convex, yet gradient methods are observed to converge linearly on them: least squares with a rank-deficient matrix, the dual of a linearly constrained quadratic program, $f(x) = g(Ax)$ with $g$ strongly convex and $A$ singular. Their optimal sets are not single points, so strong convexity fails, and some weaker property of $f$ has to explain the observed rates.

I. Necoara, Yu. Nesterov and F. Glineur (arXiv:1504.06298v4, 2016; Math. Program. 175 (2019)) introduce a chain of relaxations of strong convexity — quasi-strong convexity, quadratic under-approximation, quadratic gradient growth, quadratic functional growth — and prove linear rates for several first order methods under each. Among these results, Theorem 13 singles out one condition: for the projected gradient method with constant step size, linear convergence (in the sense made precise below) holds if and only if $f$ has quadratic functional growth. This mission formalizes that equivalence and the two results it rests on, Theorem 5 and Theorem 12.

Related conditions appear in Łojasiewicz's gradient inequality, in Luo and Tseng's error bounds (1993), in the Polyak–Łojasiewicz condition studied by Karimi, Nutini and Schmidt (2016), and in Drusvyatskiy and Lewis's equivalence of quadratic growth and error bounds (2018).

Setting

Work in $\mathbb{R}^n$ with the Euclidean inner product $\langle u, v\rangle = u^\top v$ and norm $\|\cdot\|$. Problem (P) is

$$f^* = \min_{x \in X} f(x),$$

with $X \subseteq \mathbb{R}^n$ closed and convex and $f$ convex, with gradient Lipschitz on $X$ with constant $L_f > 0$:

$$\|\nabla f(x) - \nabla f(y)\| \le L_f \|x - y\| \qquad \forall x, y \in X. \tag{1}$$

The optimal set $X^* = \{x \in X : f(x) \le f(y)\ \forall y \in X\}$ is assumed nonempty. The projection $[u]_S$ of $u$ onto a nonempty closed convex set $S$ is the nearest point of $S$ to $u$. For $x \in X$ write $\bar x = [x]_{X^*}$.

The projected gradient step from $x$ is $x^+ = [x - \tfrac{1}{L_f}\nabla f(x)]_X$, and $\bar x^+ = [x^+]_{X^*}$. The projected gradient method (GM) starts at $x^0 \in X$ and iterates $x^{k+1} = [x^k - \alpha_k \nabla f(x^k)]_X$ for $k \ge 0$.

$f$ has quadratic functional growth with constant $\kappa_f > 0$, written $f \in \mathcal F_{L_f,\kappa_f}$, when

$$f(x) - f^* \ge \frac{\kappa_f}{2}\,\|x - \bar x\|^2 \qquad \forall x \in X. \tag{22}$$

The condition number is $\mu_f = \kappa_f / L_f$.

Formalization targets

Goal: Theorem 13 (p. 23)

Under the standing assumptions of (P):

1. if $f$ satisfies (22) with constant $\kappa_f > 0$, then for every $x \in X$

$$\|x^+ - \bar x^+\|^2 \le \frac{1}{1 + \mu_f}\,\|x - \bar x\|^2 ;$$

2. if for some $0 < \beta < 1$ the step contracts the distance to the optimal set,

$$\|x^+ - \bar x^+\| \le \beta\,\|x - \bar x\| \qquad \forall x \in X,$$

then $f$ satisfies (22) with constant $L_f(1-\beta)^2$.

Together these say that a uniform one-step contraction of $\operatorname{dist}(\cdot, X^*)$ by the gradient step with step size $1/L_f$ is equivalent to quadratic functional growth.

Milestones

• (28): $f(x^+) \le f(x) - \tfrac{L_f}{2}\|x^+ - x\|^2$;
• (26): under the contraction hypothesis, $(1-\beta)\|x - \bar x\| \le \|x - x^+\|$;
• Theorem 5: contraction implies (22) with $\kappa_f = L_f(1-\beta)^2$;
• the one-step inequality $\|x^{k+1} - x\|^2 \le \|x^k - x\|^2 - 2\alpha_k(f(x^{k+1}) - f(x))$ for $0 < \alpha_k \le 1/L_f$ and all $x \in X$;
• (52): under (22), $\|x^{k+1} - \bar x^{k+1}\|^2 \le \tfrac{1}{1+\kappa_f\alpha_k}\|x^k - \bar x^k\|^2$;
• Theorem 12: along (GM) with $\alpha_k = 1/L_f$, $\|x^k - \bar x^k\|^2 \le (1+\mu_f)^{-k}\|x^0 - \bar x^0\|^2$.

A companion item states the function-value rate (53), $f(x^k) - f^* \le \tfrac{L_f\|x^0 - \bar x^0\|^2}{2}(1+\mu_f)^{-(k-1)}$ for $k \ge 1$.

Significance

The result. Theorem 13 identifies quadratic functional growth as the exact condition, in the paper's hierarchy, for linear convergence of projected gradient: every stronger class (strong, quasi-strong convexity, quadratic gradient growth, quadratic under-approximation) gives linear convergence through it, and no condition weaker than (22) can. It also gives explicit constants in both directions: rate $(1+\mu_f)^{-1}$ per step from growth, and growth constant $L_f(1-\beta)^2$ from contraction factor $\beta$.

Formalizing it. The results are proved in the paper; to the knowledge of this mission none of them has a machine-checked proof. The work is to formalize the known proofs: the descent inequality (28) and the variational inequality of the projection onto a closed convex set, the one-step inequality of the projected gradient method, and the two directions of Theorem 13. The projection lemmas and the one-step inequality are reusable for any analysis of projected gradient on convex sets.

Difficulty

The ⇒ direction is a contraction argument along one step; its difficulty is the projection calculus: the variational inequality characterizing $[u]_X$, applied with $u = x^k - \alpha_k\nabla f(x^k)$, and the descent lemma (2), which must be derived from (1) on the convex set $X$ only, since $f$ need not be smooth off $X$. The nearest point $\bar x^{k+1}$ of $x^{k+1}$ differs from $\bar x^k$; the argument must compare distances to two different optimal points.

The ⇐ direction is not a statement about one run of the method: it needs the contraction hypothesis at every feasible point. A version with a multi-step rate along runs ($\operatorname{dist}(x^k, X^*) \le C q^k$) is not what the paper proves, and the one-step hypothesis cannot be recovered from it without extra work.

Formalization scope

Lean represents $\mathbb{R}^n$ as EuclideanSpace ℝ (Fin n) and $\nabla f$ as gradient f. $f$ is a function on all of $\mathbb{R}^n$ that is differentiable at every point of $X$; only its values and gradients on $X$ enter. The standing assumptions of p. 3 are explicit hypotheses of every theorem: $X$ closed and convex, $f$ convex on $X$, (1) with $L_f > 0$, and a named minimiser $x^\star \in X^*$; the paper's "simple" (cheap projection) is not a mathematical hypothesis and is dropped, and "closed" for $f$ is implied by continuity on $X$. The optimal value is $f(x^\star)$, or $f(\bar x)$, never an infimum. Projections are predicates (IsNearest), never chosen points, and every statement quantifies over all nearest points; they exist and are unique on nonempty closed convex sets. Iterates are indexed from $k = 0$. The page prints "for $k \ge 1$" in (GM); this slip is not copied. Theorem 12's "converges linearly to some optimal point" is formalized as the rate (51) only, since convergence of the iterates themselves is not proved on the page. In the goal, part 1 is stated in the squared form of (52).

The formalization does not define the projection by a choice function, does not allow an empty optimal set (which would make every growth inequality vacuous), and does not read the gradient off the set where $f$ is assumed differentiable.

Needed infrastructure: the variational characterization of the Euclidean projection onto a closed convex set, the descent lemma on a convex set, closedness and convexity of $X^*$, and existence of nearest points. Contributions of these lemmas, of the milestones in any order, and of the goal are welcome.

Selected references

• I. Necoara, Yu. Nesterov, F. Glineur, Linear convergence of first order methods for non-strongly convex optimization, arXiv:1504.06298v4, 2016; Math. Program. 175 (2019) 69–107. https://arxiv.org/abs/1504.06298
• Yu. Nesterov, Introductory Lectures on Convex Optimization: A Basic Course, Kluwer, 2004. https://doi.org/10.1007/978-1-4419-8853-9
• Z.-Q. Luo, P. Tseng, Error bounds and convergence analysis of feasible descent methods: a general approach, Ann. Oper. Res. 46 (1993) 157–178. https://doi.org/10.1007/BF02096261
• H. Karimi, J. Nutini, M. Schmidt, Linear convergence of gradient and proximal-gradient methods under the Polyak–Łojasiewicz condition, ECML PKDD 2016. https://arxiv.org/abs/1608.04636
• D. Drusvyatskiy, A. S. Lewis, Error bounds, quadratic growth, and linear convergence of proximal methods, Math. Oper. Res. 43 (2018) 919–948. https://arxiv.org/abs/1602.06661