Prove2Me

Theorem 4.3, p. 13 — the relaxed inertial forward-reflected-backward iterates converge weakly to a zero of A + B

Proved
FRBSplitting.Inertial.theorem_4_3

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

inertial-methodmonotone-inclusionoperator-splittingp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1weak-convergence

Let HH be a real Hilbert space, A:H⇉HA:H\rightrightarrows H maximally monotone, and B:H→HB:H\to H monotone with (A+B)−1(0)≠∅(A+B)^{-1}(0)\ne\varnothing. Suppose α∈[0,1)\alpha\in[0,1), β∈(0,1]\beta\in(0,1], λ>0\lambda>0 and either

  1. BB is LL-Lipschitz and
λ<min⁡{2−β−αβ−2α2L,1−α−αββL},(41)\lambda<\min\Big\{\frac{2-\beta-\alpha\beta-2\alpha}{2L},\frac{1-\alpha-\alpha\beta}{\beta L}\Big\},\qquad(41)
  1. or BB is 1L\tfrac1L-cocoercive, α<2−β2+β\alpha<\frac{2-\beta}{2+\beta} and
λ<min⁡{2−β−αβ+2α2L,1−α+αββL}.(42)\lambda<\min\Big\{\frac{2-\beta-\alpha\beta+2\alpha}{2L},\frac{1-\alpha+\alpha\beta}{\beta L}\Big\}.\qquad(42)

Given x0,x−1∈Hx_0,x_{-1}\in H, define (xk)(x_k) and (zk)(z_k) by the relaxed inertial scheme

zk+1=JλA(xk−λB(xk)−λβ(B(xk)−B(xk−1))+αβ(xk−xk−1)),xk+1=(1−β)xk+βzk+1.z_{k+1}=J_{\lambda A}\Big(x_k-\lambda B(x_k)-\frac\lambda\beta\big(B(x_k)-B(x_{k-1})\big)+\frac\alpha\beta(x_k-x_{k-1})\Big),\qquad x_{k+1}=(1-\beta)x_k+\beta z_{k+1}.

Then (xk)(x_k) converges weakly to a point of (A+B)−1(0)(A+B)^{-1}(0).

Inertia (α>0\alpha>0) and relaxation (β<1\beta<1) extend the forward-reflected-backward method of §2, which is the case α=0\alpha=0, β=1\beta=1; the theorem describes exactly which parameter combinations keep weak convergence, without cocoercivity in case 1.

Formalization Note. The resolvent is supplied as a family J with the hypothesis that each J γ, γ>0\gamma>0, is the resolvent of γA\gamma A (it exists and is unique for maximally monotone AA). Indices are shifted by one (x j is xj−1x_{j-1}), which does not affect a limit. Weak convergence is ⟨xk,v⟩→⟨xˉ,v⟩\langle x_k,v\rangle\to\langle\bar x,v\rangle for all vv. "1L\tfrac1L-cocoercive" is 1L∥Bx−By∥2≤⟨Bx−By,x−y⟩\tfrac1L\|Bx-By\|^2\le\langle Bx-By,x-y\rangle. L>0L>0 is assumed in both cases because (41) and (42) divide by LL. BB is assumed monotone in both cases, as printed.

Preamble
import Mathlib
import Definitions.Def_ThreeOpSplitting_Accel_MonotoneOperators
import Definitions.Def_FRBSplitting_Inertial_Setting
open InnerProductSpace ThreeOpSplitting.Accel
Formal statement
namespace FRBSplitting.Inertial

theorem theorem_4_3 {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
    (A : H → Set H) (B : H → H) (J : ℝ → H → H) (L α β lam : ℝ)
    (hA : IsMaximalMonotone A)
    (hJ : IsResolventFamily A J)
    (hBm : IsMonotoneFun B)
    (hzer : (FRBSplitting.Weak.zeroSet A B).Nonempty)
    (hα0 : 0 ≤ α) (hα1 : α < 1) (hβ0 : 0 < β) (hβ1 : β ≤ 1) (hlam : 0 < lam) (hL : 0 < L)
    (hcase : (IsLipschitzOp L B ∧
        lam < min ((2 - β - α * β - 2 * α) / (2 * L)) ((1 - α - α * β) / (β * L))) ∨
      (IsCocoercive L⁻¹ B ∧ α < (2 - β) / (2 + β) ∧
        lam < min ((2 - β - α * β + 2 * α) / (2 * L)) ((1 - α + α * β) / (β * L))))
    (x z : ℕ → H) (hrun : IsRelaxedInertialRun J B α β lam x z) :
    ∃ xs ∈ FRBSplitting.Weak.zeroSet A B, FRBSplitting.Weak.IsWeakLimit x xs := by sorry

end FRBSplitting.Inertial
Source
Malitsky & Tam, A Forward-Backward Splitting Method for Monotone Inclusions Without Cocoercivity, arXiv:1808.04162v4, p. 13, Theorem 4.3, (41)–(42), with (34) on p. 11
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