Lemma 1 — Fejér monotone sequences with cluster points in C converge to a point of C

Proved

GoldenRatioVI.Explicit.fejer_convergence

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

convergencefejer-monotonicityp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $\mathcal E$ be a finite-dimensional real inner product space, let $C\subseteq\mathcal E$ be nonempty and let $(z^k)\subset\mathcal E$ . Suppose that $(z^k)$ is Fejér monotone with respect to $C$ ,

\|z^{k+1}-z\|\le\|z^k-z\|\qquad\text{for all } z\in C \text{ and all } k,

and that every cluster point of $(z^k)$ belongs to $C$ . Then $(z^k)$ converges to a point of $C$ .

This is the final step of the convergence proofs of the paper: once the iterates are shown to be Fejér monotone (for a suitable energy) with respect to the solution set and all their cluster points are solutions, the whole sequence converges.

Formalization Note The paper quotes the lemma from Bauschke–Combettes (Theorem 5.5) without the hypothesis $C\neq\emptyset$ , which the cited source has; without it the statement is false (take $C=\emptyset$ and $z^k = k\,e$ for a unit vector $e$ ). The hypothesis is added.

Preamble

import Mathlib
open Filter Topology

Formal statement

namespace GoldenRatioVI.Explicit

/-- Lemma 1 of Malitsky (p. 3), quoting Bauschke–Combettes, Theorem 5.5: in a
finite-dimensional inner product space, let `C` be a nonempty set and `(z^k)` a sequence that is
Fejér monotone w.r.t. `C` (`‖z^{k+1} − c‖ ≤ ‖z^k − c‖` for all `c ∈ C` and all `k`) and whose
cluster points all lie in `C`. Then `(z^k)` converges to a point of `C`. (`C ≠ ∅` is assumed
in Bauschke–Combettes and dropped in the quotation; without it the lemma is false.) -/
theorem fejer_convergence {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] (z : ℕ → E) (C : Set E) (hC : C.Nonempty)
    (hfejer : ∀ c ∈ C, ∀ k : ℕ, ‖z (k + 1) - c‖ ≤ ‖z k - c‖)
    (hclus : ∀ x : E, MapClusterPt x atTop z → x ∈ C) :
    ∃ x ∈ C, Tendsto z atTop (𝓝 x) := by sorry

end GoldenRatioVI.Explicit

Source

Malitsky, Golden Ratio Algorithms for Variational Inequalities, preprint (Optimization Online 6598, 2018), p. 3, Lemma 1 (quoting Bauschke–Combettes, Theorem 5.5)

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