Theorem 7.2, p. 31 — Semi-APGM (Algorithm 2) has ℒ_{k+1} ≤ ℒ_k/(1 + α_k), (87) and (88)

Proved

NAGFlow.APGM.theorem_7_2

by mikedeng1 · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

accelerated-gradientconvergence-ratelyapunov-functionp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1proximal-gradient

Let $V$ be a real Hilbert space and consider $\min_{x\in V} f(x)=h(x)+g(x)$ (110), where $h\in\mathcal S^{1,1}_{\mu,L}$ with $0\le\mu\le L<\infty$ and $g:V\to\mathbb R\cup\{+\infty\}$ is proper, closed and convex. Let $x^*\in\operatorname{dom}g$ be a minimiser of $f$ . Let $(\alpha_k,\gamma_k,x_k,y_k,w_k,v_k)$ be generated by Algorithm 2 (Semi-APGM) with $\gamma_0>0$ , $\eta=1/L$ , $v_0\in V$ and $x_0\in\operatorname{dom}g$ , and let

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

Then

\mathcal L_{k+1}\le\frac{\mathcal L_k}{1+\alpha_k}\qquad\forall\,k\in\mathbb N,\qquad(116)

for all $k\ge0$

\mathcal L_k\le\mathcal L_0\times\min\left\{\frac{4L}{(\sqrt{\gamma_0}\,k+2\sqrt L)^2},\ \left(1+\sqrt{\frac{\min\{\gamma_0,\mu\}}{L}}\right)^{-k}\right\},\qquad(87)

and for all $k\ge1$

\mathcal L_k\le C_{\gamma_0,L}\times\min\left\{\frac{4}{k^2},\ \left(1+\sqrt{\frac{\min\{\gamma_0,\mu\}}{L}}\right)^{1-k}\right\},\qquad C_{\gamma_0,L}:=\frac{L}{\gamma_0}\big(f(x_0)-f(x^*)\big)+\frac L2\|v_0-x^*\|^2 .\qquad(88),(89)

The theorem gives an accelerated proximal gradient method with one proximal evaluation per iteration whose rate covers the convex case ( $\mu=0$ , rate $O(L/k^2)$ ) and the strongly convex case ( $\mu>0$ , linear rate $(1+\sqrt{\min\{\gamma_0,\mu\}/L})^{-k}$ ) in one statement, exactly as Theorem 5.1 does for smooth $f$ .

Formalization Note. $g$ is encoded by its domain $D=\operatorname{dom}g$ and its real values on $D$ ; values off $D$ are never used. Hypotheses made explicit: $0<L$ (the page divides by $L$ and takes $\sqrt L$ ), $\gamma_0>0$ and $\alpha_k>0$ (Algorithm 2's input and step 2), $x^*$ a minimiser of $f$ over $\operatorname{dom} g$ (argmin $f\neq\emptyset$ , p. 2), and $x_0\in\operatorname{dom}g$ , which is added: if $x_0\notin\operatorname{dom}g$ then $\mathcal L_0=C_{\gamma_0,L}=+\infty$ and (87)–(88) are void on the page. 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, since $f=h+g$ is nonsmooth. Powers with negative exponent are integer powers of positive reals; $4/k^2$ is stated for $k\ge1$ , as on the page.

Preamble

import Mathlib
import Definitions.Def_NAGFlow_APGM_Setting

Formal statement

namespace NAGFlow.APGM

/-- Theorem 7.2 (Luo & Chen, arXiv:1909.03145v4, p. 31). Let `h ∈ S^{1,1}_{μ,L}` with
`0 ≤ μ ≤ L < ∞`, let `g : V → ℝ ∪ {+∞}` be proper, closed and convex (encoded by `(g, D)`,
`D = dom g`), `f = h + g`, and let `x* ∈ dom g` be a minimiser of `f`. For every run
`(α, γ, x, y, w, v)` of Algorithm 2 (Semi-APGM) started at `x₀ ∈ dom g`, with
`ℒ_k = f(x_k) − f(x*) + (γ_k/2)‖v_k − x*‖²`:
(116) `ℒ_{k+1} ≤ ℒ_k/(1 + α_k)` for every `k ∈ ℕ`;
(87) `ℒ_k ≤ ℒ₀ · min{4L/(√γ₀ k + 2√L)², (1 + √(min{γ₀, μ}/L))^{−k}}` for every `k ≥ 0`;
(88) `ℒ_k ≤ C_{γ₀,L} · min{4/k², (1 + √(min{γ₀, μ}/L))^{1−k}}` for every `k ≥ 1`, where
(89) `C_{γ₀,L} = (L/γ₀)(f(x₀) − f(x*)) + (L/2)‖v₀ − x*‖²`. -/
theorem theorem_7_2 {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
    (h : V → ℝ) (gradh : V → V) (μ L : ℝ) (hh : NAGFlow.PredCorr.IsS11 h gradh μ L)
    (g : V → ℝ) (D : Set V) (hg : IsProperClosedConvex g D)
    (xstar : V) (hxstar : xstar ∈ D) (hmin : ∀ z ∈ D, (h + g) xstar ≤ (h + g) z)
    (α γ : ℕ → ℝ) (x y w v : ℕ → V) (hrun : IsAPGMRun gradh g D μ L α γ x y w v)
    (hx0 : x 0 ∈ D) :
    (∀ k : ℕ, NAGFlow.PredCorr.lyap (h + g) xstar x v γ (k + 1) ≤ NAGFlow.PredCorr.lyap (h + g) xstar x v γ k / (1 + α k)) ∧
      (∀ k : ℕ, NAGFlow.PredCorr.lyap (h + g) xstar x v γ k ≤
        NAGFlow.PredCorr.lyap (h + g) xstar x v γ 0 *
          min (4 * L / (Real.sqrt (γ 0) * k + 2 * Real.sqrt L) ^ 2)
            ((1 + Real.sqrt (min (γ 0) μ / L)) ^ (-(k : ℤ)))) ∧
      (∀ k : ℕ, 1 ≤ k → NAGFlow.PredCorr.lyap (h + g) xstar x v γ k ≤
        (L / γ 0 * ((h + g) (x 0) - (h + g) xstar) + L / 2 * ‖v 0 - xstar‖ ^ 2) *
          min (4 / (k : ℝ) ^ 2) ((1 + Real.sqrt (min (γ 0) μ / L)) ^ (1 - (k : ℤ)))) := by sorry

end NAGFlow.APGM

Source

Luo & Chen, arXiv:1909.03145v4, Theorem 7.2 and (116), p. 31; Algorithm 2, p. 30; (87)–(89), p. 21; (110), p. 28

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph