Eq. (28) — with $h$ from (25), $\frac1{R^2}\|x_N-y_{N-1}\|^2\le\mathcal B_D(h)\le\frac1{N^2}$

Proved

AccelPPM.FPR.eq28_general_method_bound

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

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

Let $\mathcal H$ be a real Hilbert space, $M\in\mathcal M(\mathcal H)$ a maximally monotone operator, $\lambda>0$ , and let $(x_i)_{i\ge1}$ , $(y_i)_{i\ge0}$ be generated by the general proximal point method with Kim's step coefficients $h$ of (25). Let $x_*\in X_*(M)$ and $R>0$ with $\|y_0-x_*\|\le R$ . Then for every $N\ge1$ ,

\frac1{R^2}\,\|x_N-y_{N-1}\|^2\ \le\ \mathcal B_D(h)\ \le\ \frac1{N^2},

where $\mathcal B_D(h)$ is the optimal value of the dual problem (D) at horizon $N$ .

This is the accelerated rate of the general proximal point method with coefficients (25); via Proposition 4.1 it transfers to the proposed accelerated method and gives Theorem 4.1.

Formalization Note The step size $\lambda$ is written lam; the resolvent step is encoded relationally as $\lambda^{-1}(y_i-x_{i+1})\in Mx_{i+1}$ (equivalent to $x_{i+1}=J_{\lambda M}(y_i)$ for maximally monotone $M$ and $\lambda>0$ ). The coefficients (25) are kimCoeff for every $i$ : their values do not depend on $N$ , so one run of the method serves every horizon $N$ . $\mathcal B_D(h)$ is boundBD N kimCoeff : EReal, the infimum of the feasible $c$ of (D) ( $+\infty$ if (D) were infeasible); the two real quantities $\|x_N-y_{N-1}\|^2/R^2$ and $1/N^2$ are cast to EReal for the comparison. The initial-distance condition is on $y_0$ , as in (17): the general method has no $x_0$ .

Preamble

import Mathlib
import Definitions.Def_AccelPPM_FPR_IsMaximalMonotone
import Definitions.Def_AccelPPM_FPR_IsGeneralPPMSeq
import Definitions.Def_AccelPPM_FPR_kimCoeff
import Definitions.Def_AccelPPM_FPR_boundBD

Formal statement

namespace AccelPPM.FPR

/-- **Eq. (28)** (Kim, arXiv:1905.05149v4, p. 10, proof of Theorem 4.1). For every `N ≥ 1`, the
general proximal point method with Kim's coefficients `h = (25)`, run on a maximally monotone
operator `M` with step size `λ > 0` from `y₀` with `‖y₀ − x_*‖ ≤ R` for a zero `x_*` of `M`
(`R > 0`), satisfies
`(1/R²) ‖x_N − y_{N−1}‖² ≤ B_D(h) ≤ 1/N²`, where `B_D(h)` is valued in `EReal`
(`+∞` for an infeasible `h`) and the two real bounds are cast to `EReal`. -/
theorem eq28_general_method_bound {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    [CompleteSpace H] (N : ℕ) (hN : 1 ≤ N)
    (M : H → Set H) (hM : IsMaximalMonotone M) (lam : ℝ) (hlam : 0 < lam)
    (x y : ℕ → H) (hseq : IsGeneralPPMSeq M lam kimCoeff x y)
    (xstar : H) (hxstar : xstar ∈ zeroSet M) (R : ℝ) (hR : 0 < R)
    (hy0 : ‖y 0 - xstar‖ ≤ R) :
    ((‖x N - y (N - 1)‖ ^ 2 / R ^ 2 : ℝ) : EReal) ≤ boundBD N kimCoeff ∧
      boundBD N kimCoeff ≤ ((1 / (N : ℝ) ^ 2 : ℝ) : EReal) := by sorry

end AccelPPM.FPR

Source

Kim, Accelerated proximal point method for maximally monotone operators, arXiv:1905.05149v4, p. 10, proof of Theorem 4.1, Eq. (28)

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

Eq. (28) — with hhh from (25), 1R2∥xN−yN−1∥2≤BD(h)≤1N2\frac1{R^2}\|x_N-y_{N-1}\|^2\le\mathcal B_D(h)\le\frac1{N^2}R21​∥xN​−yN−1​∥2≤BD​(h)≤N21​

Eq. (28) — with $h$ from (25), $\frac1{R^2}\|x_N-y_{N-1}\|^2\le\mathcal B_D(h)\le\frac1{N^2}$