Prove2Me

Theorem 2.5(i) — the inexact forward–backward–forward residuals ∥xn−pn∥\|x_n-p_n\| and ∥yn−qn∥\|y_n-q_n\| are square summable

Proved
MonoSkew.Main.theorem_2_5_i

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

forward-backward-forwardmonotone-operatorsoperator-splittingp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let H\mathcal H be a real Hilbert space, let A:H→2HA:\mathcal H\to2^{\mathcal H} be maximally monotone, and let B:H→HB:\mathcal H\to\mathcal H be monotone. Suppose that zer⁡(A+B)≠∅\operatorname{zer}(A+B)\neq\varnothing and that BB is β\beta-Lipschitzian for some β∈ ]0,+∞[\beta\in\,]0,+\infty[. Let (an)(a_n), (bn)(b_n), (cn)(c_n) be sequences in H\mathcal H with

∑n∥an∥<+∞,∑n∥bn∥<+∞,∑n∥cn∥<+∞,\sum_{n}\|a_n\|<+\infty,\qquad\sum_n\|b_n\|<+\infty,\qquad\sum_n\|c_n\|<+\infty,

let x0∈Hx_0\in\mathcal H, let ε∈ ]0,1/(β+1)[\varepsilon\in\,]0,1/(\beta+1)[, let (γn)(\gamma_n) be a sequence in [ε,(1−ε)/β][\varepsilon,(1-\varepsilon)/\beta], and set, for every n∈Nn\in\mathbb N,

yn=xn−γn(Bxn+an),pn=JγnAyn+bn,qn=pn−γn(Bpn+cn),xn+1=xn−yn+qn,y_n=x_n-\gamma_n(Bx_n+a_n),\quad p_n=J_{\gamma_nA}y_n+b_n,\quad q_n=p_n-\gamma_n(Bp_n+c_n),\quad x_{n+1}=x_n-y_n+q_n,

where JγA=(Id+γA)−1J_{\gamma A}=(\mathrm{Id}+\gamma A)^{-1} is the resolvent. Then

∑n∈N∥xn−pn∥2<+∞and∑n∈N∥yn−qn∥2<+∞.\sum_{n\in\mathbb N}\|x_n-p_n\|^2<+\infty\qquad\text{and}\qquad\sum_{n\in\mathbb N}\|y_n-q_n\|^2<+\infty.

This is the energy estimate of the inexact forward–backward–forward (Tseng) method; the main theorem of the paper applies it on the product space H⊕G\mathcal H\oplus\mathcal G.

Formalization Note The resolvent JγnAJ_{\gamma_nA} is a given map JnJ_n with the resolvent property γn−1(x−Jnx)∈A(Jnx)\gamma_n^{-1}(x-J_nx)\in A(J_nx) for all xx, one map per nn since γn\gamma_n varies; for maximally monotone AA and γn>0\gamma_n>0 this map exists and is unique. Monotonicity of BB is monotonicity of the operator x↦{Bx}x\mapsto\{Bx\}; zer⁡(A+B)={x∣0∈Ax+Bx}\operatorname{zer}(A+B)=\{x\mid 0\in Ax+Bx\}. The space is a generic real Hilbert space (completeness explicit), so the statement applies to H⊕G\mathcal H\oplus\mathcal G. Clause (i) does not involve the point xˉ\bar x of the theorem's lead-in.

Preamble
import Mathlib
import Definitions.Def_ThreeOpSplitting_Convergence_MonotoneOperators
import Definitions.Def_ThreeOpSplitting_Convergence_WeakConvergence
import Definitions.Def_DouglasRachfordPPA_GenDR_Operators
import Definitions.Def_MonoSkew_Main_Basic

open InnerProductSpace Filter Topology
open ThreeOpSplitting.Convergence DouglasRachfordPPA.GenDR
Formal statement
namespace MonoSkew.Main

/-- Theorem 2.5(i) (p. 5): for the inexact forward–backward–forward iteration (2.3) with
absolutely summable errors and step sizes in `[ε, (1 − ε)/β]`,
`Σ ‖x_n − p_n‖² < ∞` and `Σ ‖y_n − q_n‖² < ∞`. -/
theorem theorem_2_5_i {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    (A : E → Set E) (hA : IsMaximalMonotone A)
    (B : E → E) (hB : IsMonotoneOp (fun u => ({B u} : Set E)))
    (hzer : (zer (addSingle A B)).Nonempty)
    (β : ℝ) (hβ : 0 < β) (hBlip : ∀ u w : E, ‖B u - B w‖ ≤ β * ‖u - w‖)
    (a b c : ℕ → E) (ha : Summable (fun n => ‖a n‖)) (hb : Summable (fun n => ‖b n‖))
    (hc : Summable (fun n => ‖c n‖))
    (ε : ℝ) (hε0 : 0 < ε) (hε1 : ε < 1 / (β + 1))
    (γ : ℕ → ℝ) (hγ : ∀ n, ε ≤ γ n ∧ γ n ≤ (1 - ε) / β)
    (J : ℕ → E → E) (hJ : ∀ n, IsResolvent (γ n) A (J n))
    (x y p q : ℕ → E) (hrun : IsFBFRun B γ J a b c x y p q) :
    Summable (fun n => ‖x n - p n‖ ^ 2) ∧ Summable (fun n => ‖y n - q n‖ ^ 2) := by sorry

end MonoSkew.Main
Source
Briceño-Arias and Combettes, A Monotone+Skew Splitting Model for Composite Monotone Inclusions in Duality, arXiv:1011.5517v1, p. 5, Theorem 2.5(i), (2.2), (2.3)
Human review

  • Endorsed by Shuze Chen · Oct 7, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 7, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph