Prove2Me

Lemma 2.2 — quasi-Fejér sequences whose sequential weak cluster points lie in CC converge weakly to a point of CC

Proved
MonoSkew.Main.lemma_2_2

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

fejer-monotonicitymonotone-operatorsp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1weak-convergence

Let H\mathcal H be a real Hilbert space, let CC be a nonempty subset of H\mathcal H, and let (xn)n∈N(x_n)_{n\in\mathbb N} be a sequence in H\mathcal H. Suppose that, for every x∈Cx\in C, there exists a summable sequence (εn)n∈N(\varepsilon_n)_{n\in\mathbb N} in [0,+∞[[0,+\infty[ such that

(∀n∈N)∥xn+1−x∥2≤∥xn−x∥2+εn,(\forall n\in\mathbb N)\qquad \|x_{n+1}-x\|^2\le\|x_n-x\|^2+\varepsilon_n,

and that every sequential weak cluster point of (xn)n∈N(x_n)_{n\in\mathbb N} lies in CC. Then (xn)n∈N(x_n)_{n\in\mathbb N} converges weakly to a point of CC.

This is the quasi-Fejér version of Opial's lemma. It is the device that turns the energy estimates of the forward–backward–forward method into weak convergence of its iterates.

Formalization Note The sequence (εn)(\varepsilon_n) may depend on x∈Cx\in C. A sequential weak cluster point is the weak limit of a subsequence (xφ(k))(x_{\varphi(k)}) with φ\varphi strictly increasing; weak convergence uk⇀uu_k\rightharpoonup u means ⟨uk,y⟩→⟨u,y⟩\langle u_k,y\rangle\to\langle u,y\rangle for every yy. Completeness of H\mathcal H is an explicit hypothesis (the paper's "Hilbert space").

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

/-- Lemma 2.2 (p. 4): let `C` be a nonempty subset of a real Hilbert space `E` and `(x_n)` a
sequence in `E`. If for every `c ∈ C` there is a summable sequence `ε_n ≥ 0` with
`‖x_{n+1} − c‖² ≤ ‖x_n − c‖² + ε_n` for all `n`, and every sequential weak cluster point of
`(x_n)` lies in `C`, then `(x_n)` converges weakly to a point of `C`. -/
theorem lemma_2_2 {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    (C : Set E) (hC : C.Nonempty) (x : ℕ → E)
    (hfej : ∀ c ∈ C, ∃ ε : ℕ → ℝ, (∀ n, 0 ≤ ε n) ∧ Summable ε ∧
      ∀ n, ‖x (n + 1) - c‖ ^ 2 ≤ ‖x n - c‖ ^ 2 + ε n)
    (hclus : ∀ w, IsSeqWeakClusterPt x w → w ∈ C) :
    ∃ c ∈ C, WeakTendsto x c := 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. 4, Lemma 2.2, (2.1)
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