Prove2Me

Theorem 5.1, p. 21 — with Lα_k² = γ_k(1 + α_k), the predictor–corrector scheme (83) has ℒ_{k+1} ≤ ℒ_k/(1 + α_k), (87) and (88)

Proved
NAGFlow.PredCorr.theorem_5_1

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

accelerated-gradientconvergence-ratelyapunov-functionode-discretizationp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let VV be a real Hilbert space and f∈Sμ,L1,1f\in\mathcal S^{1,1}_{\mu,L} with 0≤μ≤L<∞0\le\mu\le L<\infty, and let x∗x^* be a global minimiser of ff. Let (αk,γk)(\alpha_k,\gamma_k) satisfy the parameter equation (73),

γk+1−γkαk=μ−γk+1,γ0>0, αk>0,\frac{\gamma_{k+1}-\gamma_k}{\alpha_k}=\mu-\gamma_{k+1},\qquad\gamma_0>0,\ \alpha_k>0,

with the step sizes chosen by Lαk2=γk(1+αk)L\alpha_k^2=\gamma_k(1+\alpha_k), and let (xk,yk,vk)(x_k,y_k,v_k) be a run of the predictor–corrector scheme (83),

yk−xkαk=vk−yk,vk+1−vkαk=μγk(yk−vk+1)−1γk∇f(yk),xk+1−xkαk=vk+1−xk+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}.

Let Lk=f(xk)−f(x∗)+γk2∥vk−x∗∥2\mathcal L_k=f(x_k)-f(x^*)+\frac{\gamma_k}{2}\|v_k-x^*\|^2 (74). Then

  1. for every k∈Nk\in\mathbb N,
Lk+1≤Lk1+αk;(86)\mathcal L_{k+1}\le\frac{\mathcal L_k}{1+\alpha_k};\qquad(86)
  1. for every k≥0k\ge0,
Lk≤L0×min⁡{4L(γ0 k+2L)2, (1+min⁡{γ0,μ}L)−k};(87)\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)
  1. for every k≥1k\ge1,
Lk≤Cγ0,L×min⁡{4k2, (1+min⁡{γ0,μ}L)1−k},(88)\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(88)

where

Cγ0,L=Lγ0(f(x0)−f(x∗))+L2∥v0−x∗∥2.(89)C_{\gamma_0,L}=\frac{L}{\gamma_0}\bigl(f(x_0)-f(x^*)\bigr)+\frac{L}{2}\|v_0-x^*\|^2.\qquad(89)

The predictor–corrector scheme is an explicit method (one gradient evaluation per step) that attains the accelerated rate O(1/k2)O(1/k^2) for convex ff and the accelerated linear rate (1+min⁡{γ0,μ}/L)−k(1+\sqrt{\min\{\gamma_0,\mu\}/L})^{-k} for strongly convex ff, within one statement that covers μ=0\mu=0 and μ>0\mu>0.

Formalization Note. VV is a real Hilbert space, and the dual norm is its norm (Riesz). The gradient is an explicit map with HasGradientAt at every point. The scheme and (73) are hypotheses on given sequences, in difference-quotient form; αk\alpha_k is any positive sequence satisfying Lαk2=γk(1+αk)L\alpha_k^2=\gamma_k(1+\alpha_k), not a formula. The positivity γ0>0\gamma_0>0 and αk>0\alpha_k>0 are those of (73) and of the scheme; 0<L0<L is part of the class. The negative and 1−k1-k powers are integer powers of a number ≥1\ge1. When μ=0\mu=0 the second entry of each minimum equals 11.

Preamble
import Mathlib
import Definitions.Def_NAGFlow_PredCorr_Setting
Formal statement
namespace NAGFlow.PredCorr

/-- Theorem 5.1 (Luo & Chen, arXiv:1909.03145v4, p. 21). Let `f ∈ S^{1,1}_{μ,L}` with
`0 ≤ μ ≤ L < ∞`, let `x*` be a global minimiser of `f`, and let `(x, y, v)` be a run of the
predictor–corrector scheme (83) together with (73) (`γ₀ > 0`, `α_k > 0`), with step sizes chosen by
`Lα_k² = γ_k(1 + α_k)`. Then, with `ℒ_k` the Lyapunov function (74):
(86) `ℒ_{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_5_1 {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
    (f : V → ℝ) (gradf : V → V) (μ L : ℝ) (hf : IsS11 f gradf μ L)
    (xstar : V) (hxstar : ∀ y, f xstar ≤ f y)
    (α γ : ℕ → ℝ) (hγ : IsGammaRun μ α γ)
    (hstep : ∀ k, L * α k ^ 2 = γ k * (1 + α k))
    (x y v : ℕ → V) (hrun : IsPCRun gradf μ α γ x y v) :
    (∀ k : ℕ, lyap f xstar x v γ (k + 1) ≤ lyap f xstar x v γ k / (1 + α k)) ∧
      (∀ k : ℕ, lyap f xstar x v γ k ≤
        lyap f 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 → lyap f xstar x v γ k ≤
        (L / γ 0 * (f (x 0) - f xstar) + L / 2 * ‖v 0 - xstar‖ ^ 2) *
          min (4 / (k : ℝ) ^ 2) ((1 + Real.sqrt (min (γ 0) μ / L)) ^ (1 - (k : ℤ)))) := by sorry

end NAGFlow.PredCorr
Source
Luo & Chen, arXiv:1909.03145v4, Theorem 5.1 and Eqs. (86)–(89), p. 21; scheme (83) p. 20; (73)–(74) p. 16
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