Proposition 4.1 — the general method with (25) and the proposed accelerated method generate identical iterates

Proved

AccelPPM.FPR.proposition4_1_methods_coincide

by mikedeng1 · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

monotone-operatorsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1proximal-point-method

Let $\mathcal H$ be a real Hilbert space, $M\in\mathcal M(\mathcal H)$ a maximally monotone operator and $\lambda>0$ . Let $(x'_i)_{i\ge1}$ , $(y'_i)_{i\ge0}$ be generated by the general proximal point method with Kim's step coefficients (25), and let $(x_i)_{i\ge0}$ , $(y_i)_{i\ge0}$ be generated by the proposed accelerated proximal point method, starting from the same initial point: $y'_0=y_0\ (=x_0)$ . Then the two runs coincide:

x'_i=x_i\quad(i\ge1),\qquad y'_i=y_i\quad(i\ge0).

The general method stores all previous updates, whereas the proposed method needs only $x_i$ , $x_{i+1}$ and $y_{i-1}$ per step; this proposition says the cheap recursion computes exactly the iterates of the $O(i)$ -memory method.

Formalization Note The step size $\lambda$ is written lam. Both methods encode the resolvent step $x_{i+1}=J_{\lambda M}(y_i)$ relationally as $\lambda^{-1}(y_i-x_{i+1})\in Mx_{i+1}$ ; since $J_{\lambda M}$ is single-valued for monotone $M$ and $\lambda>0$ , this determines each iterate, and maximality makes it defined everywhere. The general method has no $x'_0$ , so the first conjunct is stated for $i\ge1$ .

Preamble

import Mathlib
import Definitions.Def_AccelPPM_FPR_IsMaximalMonotone
import Definitions.Def_AccelPPM_FPR_IsGeneralPPMSeq
import Definitions.Def_AccelPPM_FPR_IsAccelPPMSeq
import Definitions.Def_AccelPPM_FPR_kimCoeff

Formal statement

namespace AccelPPM.FPR

/-- **Proposition 4.1** (Kim, arXiv:1905.05149v4, p. 9). On a maximally monotone operator `M`
with step size `λ > 0`, a run `(x', y')` of the general proximal point method with Kim's
coefficients (25) and a run `(x, y)` of the proposed accelerated proximal point method starting
from the same initial point (`y'₀ = y₀`) produce identical sequences:
`x'_i = x_i` for all `i ≥ 1` (the general method has no `x'₀`) and `y'_i = y_i` for all `i ≥ 0`. -/
theorem proposition4_1_methods_coincide {H : Type*} [NormedAddCommGroup H]
    [InnerProductSpace ℝ H] [CompleteSpace H]
    (M : H → Set H) (hM : IsMaximalMonotone M) (lam : ℝ) (hlam : 0 < lam)
    (x' y' : ℕ → H) (hgen : IsGeneralPPMSeq M lam kimCoeff x' y')
    (x y : ℕ → H) (hacc : IsAccelPPMSeq M lam x y) (h0 : y' 0 = y 0) :
    (∀ i : ℕ, 1 ≤ i → x' i = x i) ∧ ∀ i : ℕ, y' i = y i := by sorry

end AccelPPM.FPR

Source

Kim, Accelerated proximal point method for maximally monotone operators, arXiv:1905.05149v4, p. 9, Proposition 4.1

Human review

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

View graph