Optimization

Motivation

The alternating direction method of multipliers (ADMM) solves linearly constrained problems

$$\underset{(x,z)\in\mathbb R^m\times\mathbb R^n}{\text{minimize}}\ f(x)+g(z)\quad\text{subject to}\quad Ax+Bz=b,\tag{1.2}$$

by alternating a minimization in $x$, a minimization in $z$ and a multiplier update. It is one of the standard methods for distributed optimization, statistical learning and signal processing, and in practice it is often applied to nonconvex $f$ or $g$ (see Boyd et al., Distributed optimization and statistical learning via the alternating direction method of multipliers, 2011, doi:10.1561/2200000016).

For convex problems, ADMM with $\lambda=1$ is classically Douglas–Rachford splitting (DRS) applied to the Fenchel dual of (1.2) (Gabay 1983). The dual reading needs convexity. Themelis and Patrinos (arXiv:1709.05747v4, §5; SIAM J. Optim. 30(1), 2020, doi:10.1137/18M1163993) prove a primal equivalence instead: for arbitrary $f,g$ and for every relaxation parameter $\lambda$, one ADMM update is one DRS step on a reformulation of (1.2) built from image functions. A primal equivalence for $\lambda=1$ was noted earlier by Bauschke and Koch (2015, Rem. 3.14) for $A=-B=I$, and Yan and Yin (2016, Thm. 1) showed that this case loses no generality. This mission formalizes the general statement and the convergence theorem for nonconvex ADMM that the paper derives from it.

Setting

All spaces are Euclidean, $\overline{\mathbb R}=\mathbb R\cup\{+\infty\}$, $A\in\mathbb R^{p\times m}$, $B\in\mathbb R^{p\times n}$, $b\in\mathbb R^p$. A function is proper if it never takes the value $-\infty$ and is finite somewhere. The proximal mapping of $h$ with stepsize $\gamma>0$ is the set

$$\operatorname{prox}_{\gamma h}(s)=\operatorname*{arg\,min}_{w}\Big\{h(w)+\tfrac1{2\gamma}\|w-s\|^2\Big\}.$$

For $h:\mathbb R^n\to\overline{\mathbb R}$ and a linear map $C$, the image function is

$$(Ch)(s)=\inf_{x}\{h(x)\mid Cx=s\}\in[-\infty,+\infty].$$

The $\beta$-augmented Lagrangian of (1.2) is $\mathcal L_\beta(x,z,y)=f(x)+g(z)+\langle y,Ax+Bz-b\rangle+\frac\beta2\|Ax+Bz-b\|^2$. One ADMM update with penalty $\beta>0$ and relaxation $\lambda>0$ maps $(x,y,z)$ to $(x^+,y^+,z^+)$:

$$y^{+/2}=y-\beta(1-\lambda)(Ax+Bz-b),\quad x^+\in\operatorname*{arg\,min}\mathcal L_\beta(\cdot,z,y^{+/2}),\quad y^+=y^{+/2}+\beta(Ax^++Bz-b),\quad z^+\in\operatorname*{arg\,min}\mathcal L_\beta(x^+,\cdot,y^+).$$

One DRS step with stepsize $\gamma$ and relaxation $\lambda$ on $\varphi_1+\varphi_2$ maps $s$ to $s^+=s+\lambda(v-u)$, where $u\in\operatorname{prox}_{\gamma\varphi_1}(s)$ and $v\in\operatorname{prox}_{\gamma\varphi_2}(2u-s)$. The reformulation of (1.2) is

$$\underset{s\in\mathbb R^p}{\text{minimize}}\ (Af)(s)+(Bg)(b-s),\tag{5.1}$$

that is, $\varphi_1=(Af)$ and $\varphi_2=(Bg)(b-\cdot)$. The regular subdifferential is $\hat\partial$, the limiting one $\partial$.

Formalization targets

Goal: primal equivalence (Theorem 5.5)

Let $f,g$ be proper, $\beta>0$ large enough that every ADMM subproblem has a solution, and $\lambda>0$. With $s=Ax-y/\beta$, $u=Ax$, $v=b-Bz$ and $s^+,u^+,v^+$ the same expressions at $(x^+,y^+,z^+)$, and $\gamma=1/\beta$,

$$s^+=s+\lambda(v-u),\qquad u^+\in\operatorname{prox}_{\gamma\varphi_1}(s^+),\qquad v^+\in\operatorname{prox}_{\gamma\varphi_2}(2u^+-s^+),$$

together with $\varphi_1(u^+)=f(x^+)$, $\varphi_2(v^+)=g(z^+)$, $-y^+\in\hat\partial\varphi_1(u^+)$, $-A^\top y^+\in\hat\partial f(x^+)$ and $\operatorname{dist}(-B^\top y^+,\hat\partial g(z^+))\le\beta\|B\|\|Ax^++Bz^+-b\|$.

Milestones

Proposition 5.2(i)–(iii) (properness of $(Ch)$, $(Ch)(Cx_\beta)=h(x_\beta)$, $\operatorname{prox}_{(Ch)/\beta}\supseteq CX_\beta$), Proposition 5.3 ($C^\top\hat\partial(Ch)(\bar s)\subseteq\hat\partial h(\bar x)$), the inclusions (5.3a) and (5.3b), and the identity $s+\lambda(v-u)=s^+$.

Companions

Theorem 5.5(vi): if $A$ is surjective, $(Af)$ is $L$-smooth and $\beta>L$, then $\varphi^{\mathrm{DR}}_\gamma(s^+)=\mathcal L_\beta(x^+,z^+,y^+)$. Theorem 5.6: under Assumption II and $(\gamma,\lambda)$ in the ranges of Theorem 4.1 with $\beta=1/\gamma$, $\mathcal L_\beta$ decreases by $\frac{c\lambda^2}{(1+\gamma L)^2}\|Ax^k+Bz^k-b\|^2$ per step, $\min_{i\le k}\|Ax^i+Bz^i-b\|=o(1/\sqrt k)$, cluster points are KKT points with common cost, and the iterates are bounded when $\Phi$ is level bounded.

Significance

Theorem 5.5 reduces nonconvex ADMM to nonconvex DRS: any descent, convergence or rate statement for DRS on $\varphi_1+\varphi_2$ becomes one for ADMM, with the Douglas–Rachford envelope becoming the augmented Lagrangian (5.5(vi)). This is how the paper obtains Theorem 5.6, with explicit penalty bounds for every $\lambda\in(0,4)$ permitted by Theorem 4.1, under assumptions weaker than earlier nonconvex ADMM analyses (Li and Pong, 2015, doi:10.1137/140998135, require $A=I$ and coercivity).

The results are proved in the paper. No machine-checked proof of a primal ADMM–DRS equivalence is known; the platform holds formalizations of proximal ADMM variants and of convex DRS for monotone operators, but not of image functions. The mission produces a reusable library of image functions and their proximal and subdifferential calculus, and a precise statement of relaxed ADMM in the nonconvex, extended-real setting.

Difficulty

The individual steps are short, but the objects are extended-real and set-valued. An image function may equal $-\infty$, and its infimum need not be attained; that $(Af)$ is proper and that the infimum is attained at $x^+$ must be derived from the solvability of the ADMM subproblems, not assumed. The proximal mappings are multivalued, so the equivalence is an inclusion between argmin sets, and the algebra relating $y^{+/2}$, $y^+$ and $s^+$ has to be matched to the relaxation exactly. The subgradient claims require regular subdifferentials of extended-real functions, and (v) requires the optimality condition of the $z$-subproblem, whose quadratic term couples $z^+$ with the residual. Theorem 5.6 additionally rests on the whole DRS convergence analysis of §4.

Formalization scope

Points are EuclideanSpace ℝ (Fin _), matrices are continuous linear maps, $A^\top$ is ContinuousLinearMap.adjoint, and $\|B\|$ is the operator norm. Extended-real functions are EReal-valued; the image function imageFn is the EReal infimum over $\{x\mid Cx=s\}$, so it is $+\infty$ off the range and may be $-\infty$. Proximal mappings and $X_\beta$ are sets, and an ADMM update (IsADMMStep) is any selection of minimizers in the order $y^{+/2},x^+,y^+,z^+$. The two subproblems minimize the terms of $\mathcal L_\beta$ that depend on the minimized variable, because the dropped constant $g(z)$ may be $+\infty$ at a starting point and would make every $x$ a minimizer. "Large enough penalty" is SubproblemsSolvable. The regular and limiting subdifferentials are the published IsRegularSubgrad and LimitingSubdiff.

Added hypotheses: $f$ and $g$ proper in Theorem 5.5 and 5.5(vi), and $h$ proper in Proposition 5.2(i). The page omits them, and they are necessary: for $h\equiv+\infty$ every $X_\beta(s)$ is the whole space while $(Ch)\equiv+\infty$ is not proper. Claim (v) is stated as the existence of $w\in\hat\partial g(z^+)$ with $\|-B^\top y^+-w\|\le\beta\|B\|\|Ax^++Bz^+-b\|$, which is stronger than the distance bound and avoids the distance to an empty set. Theorem 5.6 uses the constants $c$ of Theorem 4.1 as derived in its proof ((4.8), (4.10)); the printed (4.3) has the sign of one entry of a max reversed and the printed (4.5) an extra factor $1/\lambda$, and both are then false (counterexamples in the companion mission on DRS convergence). Theorem 5.6 adds $L>0$; its run is indexed so that the paper's $(x^k,y^k,z^k)$ is the term $k+1$, with the starting triple at index $0$.

The goal does not assume the DRS relations or (5.3a)–(5.3b), and $s^+,u^+,v^+$ are defined from the ADMM iterates by (5.2), not chosen independently; a formalization that quantifies over an arbitrary prox selection, or that hard-codes $\lambda=1$, is a different statement.

Needed infrastructure: image functions and their proximal calculus, regular subgradients of extended-real functions under linear maps, and, for Theorem 5.6, the DRS convergence theory of §4 (formalized in the companion mission I of this series). Proofs of individual milestones are welcome independently.

Selected references

• A. Themelis, P. Patrinos, Douglas–Rachford splitting and ADMM for nonconvex optimization: tight convergence results, SIAM J. Optim. 30(1):149–181, 2020. arXiv:1709.05747v4, doi:10.1137/18M1163993
• H. H. Bauschke, V. R. Koch, Projection methods: Swiss army knives for solving feasibility and best approximation problems with halfspaces, in Infinite Products of Operators and Their Applications, Contemp. Math. 636, pp. 1–40, AMS, 2015.
• M. Yan, W. Yin, Self equivalence of the alternating direction method of multipliers, in Splitting Methods in Communication, Imaging, Science, and Engineering, pp. 165–194, Springer, 2016.
• G. Li, T. K. Pong, Global convergence of splitting methods for nonconvex composite optimization, SIAM J. Optim. 25(4):2434–2460, 2015. doi:10.1137/140998135
• S. Boyd, N. Parikh, E. Chu, B. Peleato, J. Eckstein, Distributed optimization and statistical learning via the alternating direction method of multipliers, Found. Trends Mach. Learn. 3(1), 2011. doi:10.1561/2200000016
• D. Gabay, Applications of the method of multipliers to variational inequalities, in Augmented Lagrangian Methods, Studies in Mathematics and Its Applications 15, pp. 299–331, Elsevier, 1983.

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

Motivation

Accelerated first-order methods, beginning with Nesterov's 1983 scheme, reach the optimal iteration complexity among gradient methods for smooth convex minimization, but their classical derivations ("estimate sequences") give little insight into why acceleration works. A line of work started by Su, Boyd and Candès (arXiv:1503.01243) reads accelerated methods as discretizations of second-order ordinary differential equations and proves their rates with Lyapunov functions: a quantity that decreases along the continuous trajectory and, after discretization, along the iterates.

Luo and Chen (arXiv:1909.03145, Math. Program. 2022) introduce the NAG flow, a first-order system in two variables $(x, v)$ with a time-varying parameter $\gamma$, and derive several accelerated methods from it as numerical ODE solvers. Their §4 treats the simplest discretization, the fully implicit (backward Euler) scheme. It is not a practical method by itself, since each step solves a nonlinear equation, but it is the case in which the continuous Lyapunov argument transfers to the discrete level almost word for word, and it is the benchmark for the semi-implicit and explicit schemes of §§5–7. This mission formalizes its convergence theorem, Theorem 4.1.

Setting

Let $V$ be a real Hilbert space with inner product $(\cdot,\cdot)$ and norm $\|\cdot\|$; the duality pairing $\langle\cdot,\cdot\rangle$ is identified with the inner product. Let $f:V\to\mathbb R$ and $\mu\ge 0$. The function $f$ belongs to the class $\mathcal S^1_\mu$ if it is continuously differentiable with gradient $\nabla f$ and satisfies the $\mu$-convexity inequality

$$f(x)-f(y)-\langle\nabla f(y),x-y\rangle\ \ge\ \frac\mu2\|x-y\|^2\qquad\forall x,y\in V .$$

For $\mu=0$ this is convexity, for $\mu>0$ strong convexity. A global minimiser $x^*$ of $f$ is fixed throughout.

Given positive step sizes $\alpha_k>0$ and $\gamma_0>0$, the implicit scheme (72)–(73) relates consecutive iterates $(x_k,v_k,\gamma_k)$ and $(x_{k+1},v_{k+1},\gamma_{k+1})$ by

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

All right-hand sides are evaluated at the new iterate, which is what makes the scheme implicit. The Lyapunov function (74) is

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

Formalization targets

Goal: Theorem 4.1 (p. 17)

For $f\in\mathcal S^1_\mu$ with $\mu\ge0$ and every run of (72)–(73) with $\gamma_0>0$ and $\alpha_k>0$,

$$\mathcal L_{k+1}\ \le\ \frac{\mathcal L_k}{1+\alpha_k},\qquad k\in\mathbb N .$$

No condition links $\alpha_k$ to $\gamma_k$ or to any smoothness constant, and $f$ need not have a Lipschitz gradient.

Milestones (proof of Theorem 4.1, p. 17)

1. The difference identity: under (73),

$$\mathcal L_{k+1}-\mathcal L_k=f(x_{k+1})-f(x_k)+\tfrac{\alpha_k}2(\mu-\gamma_{k+1})\|v_{k+1}-x^*\|^2+\gamma_k\big(v_{k+1}-v_k,\tfrac{v_{k+1}+v_k}2-x^*\big).$$

2. The last-term identity $\gamma_k\big(v_{k+1}-v_k,\tfrac{v_{k+1}+v_k}2-x^*\big)=\gamma_k(v_{k+1}-v_k,v_{k+1}-x^*)-\tfrac{\gamma_k}2\|v_{k+1}-v_k\|^2$.
3. The substitution of the second line of (72) into $\gamma_k(v_{k+1}-v_k,v_{k+1}-x^*)$.
4. The split of the gradient term by the first line of (72).
5. The one-step inequality (75): $\mathcal L_{k+1}-\mathcal L_k\le-\alpha_k\mathcal L_{k+1}$.

A companion item states (76): each step of (72) is a proximal point step $x_{k+1}=\mathbf{prox}_{\eta_kf}(y_k)$ with explicit $\eta_k$, $y_k$ and $\gamma_{k+1}=(\gamma_k+\mu\alpha_k)/(1+\alpha_k)$.

Significance

Theorem 4.1 gives a linear rate $\mathcal L_k\le\mathcal L_0\prod_{i<k}(1+\alpha_i)^{-1}$ for every convex $f$, not only strongly convex ones, as long as $\alpha_k\ge\alpha>0$; larger steps give faster decay. It is the exact discrete counterpart of the exponential decay $\mathcal L(t)\le e^{-t}\mathcal L(0)$ of the NAG flow (Lemma 3.2 of the paper), and the semi-implicit and explicit schemes of §§5–7 are analysed by comparison with it: their proofs follow the same difference computation and must control the extra terms that the implicit scheme does not produce. Through (76), the implicit scheme is an extrapolated proximal point method, close to Güler's accelerated proximal point algorithm when $\mu=0$.

The result is proved on paper. To the knowledge of this mission it has no machine-checked proof. Formalizing it fixes the exact hypotheses of the discrete Lyapunov argument (in particular that $\gamma_k>0$ and $\mu\ge0$ are what make the dropped squares nonpositive) and provides the algebraic identities reused by the later schemes of the paper.

Difficulty

The argument is algebraic, but the bookkeeping is where it can fail. The difference $\mathcal L_{k+1}-\mathcal L_k$ produces terms in $\|v_{k+1}-x^*\|^2$, $\|x_{k+1}-x^*\|^2$, $\|x_{k+1}-v_{k+1}\|^2$, $\|v_{k+1}-v_k\|^2$ and $\|x_{k+1}-x_k\|^2$, which must cancel or carry the right sign exactly. The naive attempt, to bound $\mathcal L_{k+1}-\mathcal L_k$ by $-\alpha_k\mathcal L_k$ as in an explicit Euler analysis, fails: the implicit scheme controls the decrease by the new value $\mathcal L_{k+1}$, and the contraction factor $1/(1+\alpha_k)$ comes from solving for it. The $\gamma$-terms close only because (73) is also discretized implicitly, so that $\gamma_{k+1}$, not $\gamma_k$, multiplies $\|v_{k+1}-x^*\|^2$.

Formalization scope

$V$ is a type with NormedAddCommGroup, InnerProductSpace ℝ V and CompleteSpace V. The gradient is an explicit map gradf : V → V with HasGradientAt f (gradf x) x at every point, and continuity of gradf encodes "continuously differentiable". The class $\mathcal S^1_\mu$, the Lyapunov function, one step of (72)–(73), and a run are definitions; the scheme's equations are kept in the page's difference-quotient form, as hypotheses on given sequences. Nothing asserts that the implicit system has a solution, and iterates are not defined by choice. Sequences are indexed from $0$.

Conventions committed to: $x^*$ is a global minimiser (the paper's standing assumption that $\operatorname{argmin}f$ is nonempty); $\gamma_0>0$ and $\alpha_k>0$ as on p. 16; the one-step milestones that divide by $\gamma_k$ assume $\gamma_k>0$, which along a run follows from (73). The prox in (76) is stated as membership in the argmin through the published predicate GoldenRatioVI.Shared.IsProxPoint.

A trivializing formalization is ruled out: the goal is stated for sequences satisfying the scheme (72)–(73) itself, never for sequences assumed to satisfy (75), and no Lipschitz-gradient class or step-size rule from later sections is imported.

The definitions of $\mathcal S^1_\mu$ and $\mathcal L_k$ are shared with the other missions of this series and will be consolidated. Contributions welcome: proofs of the identities, of (75), of the goal, and of (76).

Selected references

• H. Luo, 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
• W. Su, S. Boyd, E. J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, J. Mach. Learn. Res. 17, 2016. https://arxiv.org/abs/1503.01243
• O. Güler, New proximal point algorithms for convex minimization, SIAM J. Optim. 2(4), 649–664, 1992. https://doi.org/10.1137/0802032
• R. T. Rockafellar, Monotone operators and the proximal point algorithm, SIAM J. Control Optim. 14(5), 877–898, 1976. https://doi.org/10.1137/0314056
• Y. Nesterov, A method for solving the convex programming problem with convergence rate O(1/k²), Soviet Math. Dokl. 27, 372–376, 1983.

Motivation

Nesterov's accelerated gradient method minimises a smooth convex function $f$ to accuracy $\varepsilon$ in $O(1/\sqrt{\varepsilon})$ gradient evaluations, against $O(1/\varepsilon)$ for plain gradient descent, and this rate is optimal for first-order methods (Nesterov 2018). The method is usually presented through estimate sequences, which certify the rate but say little about where the iteration comes from. A line of work starting with Su, Boyd and Candès (2016) and Wibisono, Wilson and Jordan (2016) reads accelerated methods as discretisations of ordinary differential equations, with a Lyapunov function carrying the convergence proof from continuous to discrete time.

Luo and Chen introduce the NAG flow, a first-order system in a position variable $x$, a velocity-like variable $v$ and a damping parameter $\gamma$, which covers the convex case ($\mu=0$) and the strongly convex case ($\mu>0$) in one equation. They then examine which numerical schemes for this flow keep its exponential Lyapunov decay. The implicit scheme does (Theorem 4.1), but needs a proximal step. The explicit Gauss–Seidel splitting (80) does not: its one-step estimate leaves a positive term $\frac{\alpha_k^2}{2\gamma_k}\|\nabla f(x_{k+1})\|^2$ (Lemma 5.1). Section 5 repairs it in two ways. This mission formalises the second one, from §5.3: a gradient correction step appended to the splitting.

Setting

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

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

and $\nabla f$ is continuous. It belongs to $\mathcal S^{1,1}_{\mu,L}$ if moreover $\nabla f$ is $L$-Lipschitz with $0<L<\infty$, and $0\le\mu\le L$. A global minimiser $x^*$ of $f$ is assumed to exist.

The scheme carries a step size $\alpha_k>0$ and a damping parameter $\gamma_k$ governed by the implicit recursion

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

Given $(x_k,v_k)$, the gradient-corrected scheme (91) computes

$$\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 x_{k+1}=y_k-\frac1L\nabla f(y_k).$$

The first two lines are the Gauss–Seidel splitting (80) with output $y_k$. Both can be solved explicitly, so one step costs one gradient evaluation, at $y_k$. The third line is a gradient descent step from $y_k$.

The discrete Lyapunov function is

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

and the proof also uses the intermediate value $\widehat{\mathcal L}_k=f(y_k)-f(x^*)+\frac{\gamma_{k+1}}{2}\|v_{k+1}-x^*\|^2$ (84).

Formalization targets

Goal: Theorem 5.2

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 (91) together with (73) satisfies

$$\mathcal L_{k+1}\le\frac{\mathcal L_k}{1+\alpha_k}\quad(k\in\mathbb N),\qquad(92)$$ $$\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{L}{2}\|v_0-x^*\|^2$ (89). The paper states (87) and (88) by reference to Theorem 5.1; the goal writes them out.

Milestones

1. Lemma 5.1 (p. 19): the one-step estimates (81) and (82) for one Gauss–Seidel step and $f\in\mathcal S^1_\mu$.
2. (93) (p. 22): (82) applied to the first two lines of (91), $\widehat{\mathcal L}_k-\mathcal L_k\le-\alpha_k\widehat{\mathcal L}_k+\frac{\alpha_k^2}{2\gamma_k}\|\nabla f(y_k)\|^2$.
3. (94) (p. 22): the descent inequality $f(x_{k+1})-f(y_k)\le-\frac{1}{2L}\|\nabla f(y_k)\|^2$.
4. $\mathcal L_{k+1}\le\widehat{\mathcal L}_k-\frac1{2L}\|\nabla f(y_k)\|^2$ (p. 22).
5. The combined estimate (p. 22): $\mathcal L_{k+1}-\mathcal L_k\le-\alpha_k\mathcal L_{k+1}+\frac{1}{2L\gamma_k}(L\alpha_k^2-\gamma_k(1+\alpha_k))\|\nabla f(y_k)\|^2$ for arbitrary $\alpha_k>0$.
6. 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}$.
7. The bound on $1/(1+\alpha_0)$ (proof of Theorem 5.1, p. 21): $\frac{1}{1+\alpha_0}\le\frac{L}{\gamma_0}$, which yields the constant (89).

Significance

Theorem 5.2 gives an explicit, one-gradient-per-step method with the accelerated rate $O(1/k^2)$ for convex $f$ and the accelerated linear rate $(1+\sqrt{\min\{\gamma_0,\mu\}/L})^{-k}$ for strongly convex $f$. The convex and strongly convex cases are covered by a single Lyapunov argument, with no restart and no prior knowledge of whether $\mu>0$ beyond its value in (73). The analysis is modular: (92) holds for any correction step with the decay property (94). Section 7 of the paper reuses it for composite problems, replacing the gradient step by a proximal gradient step.

This result is proved in the paper; nothing here is open. To our knowledge none of these statements has been machine-checked. A completed mission gives a checked Lyapunov proof of an accelerated method on a general Hilbert space, with the step sizes left as arbitrary roots of $L\alpha_k^2=\gamma_k(1+\alpha_k)$ rather than fixed by a closed formula. The paper omits the proof of Lemma B.2 ("Similarly, …"), so formalising it supplies a missing argument.

Difficulty

The naive analysis of the Gauss–Seidel splitting fails. The term $\frac{\alpha_k^2}{2\gamma_k}\|\nabla f\|^2$ in (82) is positive, so this estimate yields no contraction of $\mathcal L_k$ for any step size; the paper notes that the splitting (80) "does not lead to the contraction property" (p. 19). The correction works only because $\mathcal L_{k+1}$ and $\widehat{\mathcal L}_k$ share $v_{k+1}$ and $\gamma_{k+1}$, and differ only in the $f$-value at $x_{k+1}$ against $y_k$. The step-size rule then has to cancel the two gradient-norm terms exactly. The rates (87)–(88) need a second, independent argument: a discrete comparison for the product $\prod_{i<k}(1+\alpha_i)^{-1}$ under the coupled recursions for $\alpha_k$ and $\gamma_k$ (Lemma B.2). The descent inequality (94) requires the quadratic upper bound (4), which the formalization does not assume. It must be derived from the Lipschitz continuity of $\nabla f$ on a Hilbert space.

Formalization scope

All statements live in the namespace NAGFlow.GradCorr, with one definitions file NAGFlow.GradCorr.Setting. The conventions are as follows.

• $V$ is a real Hilbert space: [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]. The paper's duality pairing and dual norm $\|\cdot\|_*$ are the inner product and the norm (Riesz).
• $\nabla f$ is an explicit map gradf : V → V with HasGradientAt f (gradf x) x at every point, never Mathlib's gradient. The classes are the structures IsS1 and IsS11. IsS11 contains $0<L$ and $\mu\le L$; inequality (4) is not assumed.
• $x^*$ is any point with $f(x^*)\le f(y)$ for all $y$.
• The scheme (91) and the recursion (73) are hypotheses on given sequences (IsGCRun, IsGammaRun), indexed from $0$. The two implicit lines are kept as equations. $\gamma_0>0$ and $\alpha_k>0$ are part of IsGammaRun.
• The step sizes are any positive sequence with $L\alpha_k^2=\gamma_k(1+\alpha_k)$, not a closed formula.
• $\mu=0$ is allowed throughout, so $\min\{\gamma_0,\mu\}$ may be $0$.
• Negative powers are integer powers (zpow), and (88) is stated for $k\ge1$.
• In Lemma B.2, $L:=\sup_kL_k$ is encoded as an arbitrary real upper bound of $(L_k)$. The conclusions involving $L$ weaken as $L$ grows.

The goal quantifies over runs of the scheme (91) itself. A version that assumes the contraction (92), or that fixes $\alpha_k$ by a formula that makes (91) degenerate, would not be this theorem.

The development needs the quadratic upper bound for $L$-smooth functions on a Hilbert space, a one-step Lyapunov estimate for the splitting, and the scalar sequence analysis of Lemma B.2. The last two are shared with the predictor–corrector and composite missions of this series. Lemma B.2 and the $\alpha_0$ bound are statements about real sequences only and can be reused independently. 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, 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
• A. Wibisono, A. C. Wilson and M. I. Jordan, A variational perspective on accelerated methods in optimization, Proceedings of the National Academy of Sciences 113(47), 2016. https://arxiv.org/abs/1603.04245
• 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

Motivation

Many problems in signal processing, statistics and control are posed as composite convex minimisation: minimise $f = h + g$, where $h$ is smooth and $g$ is convex but possibly nonsmooth or extended-valued (an $\ell^1$ penalty, a nuclear norm, the indicator of a constraint set). Proximal gradient methods handle $g$ through its proximal operator and $h$ through its gradient. Their accelerated versions, Nesterov's composite method (Nesterov 2013) and FISTA (Beck–Teboulle 2009), reach the optimal $O(L/k^2)$ rate for convex problems, and separate variants exist for the strongly convex case.

Luo and Chen (arXiv:1909.03145, Math. Program. 2022) derive accelerated methods as discretisations of a single ODE, the NAG flow, and analyse every scheme with one discrete Lyapunov function. Section 7.2 extends their corrected semi-implicit scheme from smooth $f$ to $f = h + g$ by replacing $\nabla f$ with the composite gradient mapping. The result is Algorithm 2 (Semi-APGM). It calls the proximal operator once per iteration, and Theorem 7.2 shows that it has the same rate as the smooth methods, in the convex and the strongly convex case at once.

Setting

$V$ is a real Hilbert space with inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$. The smooth part $h : V \to \mathbb R$ has gradient $\nabla h$ and lies in the class $\mathcal S^{1,1}_{\mu,L}$, with $0 \le \mu \le L < \infty$ and $L > 0$. That is, $h$ is $\mu$-convex,

$$h(x) - h(y) - \langle \nabla h(y), x - y\rangle \ge \tfrac{\mu}{2}\|x - y\|^2,$$

and $\nabla h$ is $L$-Lipschitz. The nonsmooth part $g : V \to \mathbb R \cup \{+\infty\}$ is proper, closed and convex, with effective domain $D = \operatorname{dom} g$. The subdifferential is $\partial g(x) = \{p : g(y) \ge g(x) + \langle p, y - x\rangle\ \forall y\}$. The proximal operator is

$$\operatorname{prox}_{\eta g}(z) = \operatorname{argmin}_{y \in V}\Big\{ g(y) + \tfrac{1}{2\eta}\|y - z\|^2 \Big\}.$$

With step $\eta = 1/L$, set $S_f(x) = \operatorname{prox}_{g/L}(x - \nabla h(x)/L)$ and $\mathcal G_f(x) = L(x - S_f(x))$, the composite gradient mapping. Fix a minimiser $x^*$ of $f$.

Algorithm 2 starts from $x_0, v_0 \in V$ and $\gamma_0 > 0$. For $k = 0, 1, \dots$ it chooses $\alpha_k > 0$ with $L\alpha_k^2 = \gamma_k(1 + \alpha_k)$ and sets

$$\gamma_{k+1} = \frac{\gamma_k + \mu\alpha_k}{1 + \alpha_k}, \quad y_k = \frac{x_k + \alpha_k v_k}{1 + \alpha_k}, \quad w_k = \frac{\gamma_k v_k + \mu\alpha_k y_k}{\gamma_k + \mu\alpha_k},$$ $$x_{k+1} = S_f(y_k), \qquad v_{k+1} = w_k + \frac{\gamma_k}{\gamma_{k+1}}\frac{x_{k+1} - y_k}{\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.2

For every run of Algorithm 2 with $x_0 \in \operatorname{dom} g$,

$$\mathcal L_{k+1} \le \frac{\mathcal L_k}{1 + \alpha_k} \quad \forall k, \qquad \mathcal L_k \le \mathcal L_0 \min\Big\{\frac{4L}{(\sqrt{\gamma_0}k + 2\sqrt L)^2}, \Big(1 + \sqrt{\tfrac{\min\{\gamma_0,\mu\}}{L}}\Big)^{-k}\Big\},$$

and, for $k \ge 1$,

$$\mathcal L_k \le C_{\gamma_0,L}\min\Big\{\frac{4}{k^2}, \Big(1 + \sqrt{\tfrac{\min\{\gamma_0,\mu\}}{L}}\Big)^{1-k}\Big\}, \qquad C_{\gamma_0,L} = \frac{L}{\gamma_0}\big(f(x_0) - f(x^*)\big) + \frac{L}{2}\|v_0 - x^*\|^2 .$$

Milestones

In attack order:

1. Algorithm 2 is a run of the semi-implicit scheme (115).
2. The proximal optimality condition (112).
3. The inclusion $\mathcal G_f(x) - \nabla h(x) \in \partial g(S_f(x))$ (113).
4. Lemma 7.1, the quadratic lower bound (114) for $f$ built from $\mathcal G_f$.
5. The one-step estimate (117) for (115) with arbitrary $\alpha_k > 0$.
6. The bound $1/(1 + \alpha_0) \le L/\gamma_0$.
7. Lemma B.2, which turns the contraction factors $\prod 1/(1 + \alpha_i)$ into explicit rates.

Significance

The theorem gives a single accelerated proximal gradient method whose rate interpolates between $O(L/k^2)$ for $\mu = 0$ and the linear rate $(1 + \sqrt{\mu/L})^{-k}$ for $\mu > 0$ (when $\gamma_0 \ge \mu$). Neither the method nor its parameters change between the two regimes. Lemma 7.1 is the only property of $g$ that the proof uses, so the same analysis covers constraints (an indicator $g$), sparsity penalties and any other proximable term.

The result is proved on paper; this mission formalizes it. The paper's argument is short because it reuses the smooth case: "proceed as the proof of Lemma 5.1 and use Lemma 7.1". A machine-checked version has to carry out that reuse explicitly. It also has to supply the proximal facts the paper cites as well known ((112)) and the proof of Lemma B.2, which the paper omits. None of these statements is known to be formalized in Lean.

Difficulty

There is no single hard step. The work is in three places.

• Algebra on the run. Equation (117) needs the difference identity for $\frac{\gamma}{2}\|v - x^*\|^2$, the $v$-update of (115) and two applications of Lemma 7.1, at $y = x^*$ and at $y = x_k$. The cross terms must cancel exactly.
• The extended-valued function. The predictor $y_k$ may lie outside $\operatorname{dom} g$, where the page's $f(y_k)$ is $+\infty$. An argument that evaluates $f$ at $y_k$ is invalid unless the terms involving $f(y_k)$ cancel.
• Lemma B.2. The product bound for $\prod 1/(1 + \alpha_i)$ requires a telescoping estimate on $1/\sqrt{\rho_k}$ whose proof the paper does not give.

Reading Algorithm 2 as a gradient method on $f$ does not work, because $f$ is not differentiable. All smoothness has to come from $h$ through Lemma 7.1.

Formalization scope

• Space. $V$ is a real Hilbert space, and the paper's duality pairing and dual norm are the inner product and the norm (Riesz).
• Gradient. $\nabla h$ is an explicit map with a gradient at every point.
• Encoding of $g$. The extended-valued $g$ is a pair: its domain $D$ and a real-valued function whose values off $D$ are never used.
  • "Proper" means $D \ne \emptyset$.
  • "Convex" means convex on the convex set $D$.
  • "Closed" means the epigraph $\{(x,t) : x \in D,\ g(x) \le t\}$ is closed. This does not force $D$ to be closed.
  • $x^*$ minimises $h + g$ over $D$.
• Named outputs. The proximal operator and $S_f$ are predicates on a named output (a minimiser over $D$). Existence and uniqueness are theorems, not assumptions.
• Added hypotheses.
  • $L > 0$, $\gamma_0 > 0$ and $\alpha_k > 0$, from the paper's class and algorithm.
  • $x_0 \in \operatorname{dom} g$. Without it the page's $\mathcal L_0$ is $+\infty$ and the theorem is void.
• Corrected slip. The page's "(110) $f \in \mathcal S^{1,1}_{\mu,L}$" is read as $h \in \mathcal S^{1,1}_{\mu,L}$, as in (104) and Lemma 7.1.
• Lemma B.2. $L := \sup_k L_k$ is replaced by any real upper bound of $(L_k)$.
• Ruled out. A finite-valued $g$ on all of $V$, without a domain, would drop the constrained and indicator cases and is not a faithful formalization. So is a statement with hypotheses that force $\mathcal L_k$ to be trivially controlled.

All objects are defined locally under NAGFlow.APGM. A complete development needs elementary convex analysis in Hilbert space (prox optimality, the descent lemma (4) from the Lipschitz gradient) and the scalar recursion of Lemma B.2. The proximal facts and Lemma B.2 can be reused by the other missions of this series (Theorems 5.1, 5.2 and 7.3) and by any accelerated-method formalization. Contributions are welcome on any milestone, in any order.

Selected references

• H. Luo, L. Chen, From differential equation solvers to accelerated first-order methods for convex optimization, Math. Program. 195 (2022) 735–781. 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, 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
• Yu. Nesterov, Lectures on Convex Optimization, 2nd ed., Springer, 2018. https://doi.org/10.1007/978-3-319-91578-4