Section 3, (D) — every feasible point of (D) bounds the fixed-point residual of the general proximal point method

Proved

AccelPPM.FPR.weak_duality_D

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

monotone-operatorsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1performance-estimationsemidefinite-programming

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 step coefficients $h=\{h_{i,k}\}$ . Let $x_*\in X_*(M)$ and $R>0$ with $\|y_0-x_*\|\le R$ . Fix $N\ge1$ . If $(a_2,\dots,a_N,b_N,c)$ is feasible for the dual problem (D), i.e. $a_2,\dots,a_N,b_N,c\ge0$ and

\sum_{i=2}^{N}a_iA_{i-1,i}(h)+b_NB_N(h)+cC-u_Nu_N^\top\succeq0,

then

\frac1{R^2}\,\|x_N-y_{N-1}\|^2\ \le\ c .

In words: the optimal value $\mathcal B_D(h)$ of (D) is an upper bound on the worst-case fixed-point residual (17) of the general proximal point method after $N$ steps, which is how the paper computes worst-case rates for a given $h$ by solving an SDP.

Formalization Note The step size $\lambda$ is written lam. The resolvent step $x_{i+1}=J_{\lambda M}(y_i)$ is encoded relationally as $\lambda^{-1}(y_i-x_{i+1})\in Mx_{i+1}$ ; for monotone $M$ and $\lambda>0$ this determines $x_{i+1}$ , and maximality makes the resolvent defined everywhere (Minty). The general method has no $x_0$ , so the initial-distance condition is on $y_0$ , as in the last constraint of (17). $N$ is a natural number with $N\ge1$ and y (N - 1) is $y_{N-1}$ . The statement holds in every real Hilbert space; no dimension hypothesis is imposed.

Preamble

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

Formal statement

namespace AccelPPM.FPR

/-- **Section 3, (D)** (Kim, arXiv:1905.05149v4, pp. 5–7): every feasible point of the dual
problem (D) bounds the worst-case fixed-point residual (17) of the general proximal point method.
For every `N ≥ 1`, every step-coefficient array `h`, every feasible `(a_2, …, a_N, b_N, c)` of (D),
every maximally monotone `M` on a real Hilbert space `H`, every step size `λ > 0`, every run
`(x, y)` of the general proximal point method with coefficients `h`, and every zero `x_*` of `M`
with `‖y₀ − x_*‖ ≤ R` (`R > 0`):
`‖x_N − y_{N−1}‖² / R² ≤ c`. -/
theorem weak_duality_D {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H]
    [CompleteSpace H] (N : ℕ) (hN : 1 ≤ N) (h : ℕ → ℕ → ℝ) (a : ℕ → ℝ) (b c : ℝ)
    (hfeas : IsDualFeasible N h a b c)
    (M : H → Set H) (hM : IsMaximalMonotone M) (lam : ℝ) (hlam : 0 < lam)
    (x y : ℕ → H) (hseq : IsGeneralPPMSeq M lam h 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 ≤ c := by sorry

end AccelPPM.FPR

Source

Kim, Accelerated proximal point method for maximally monotone operators, arXiv:1905.05149v4, pp. 5–7, Section 3, problem (17) and its Lagrangian dual (D) ("for any given h ... one can compute its (upper bound of) worst-case fixed-point residual by numerically solving (D)")

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