Theorem 2.10 — iterates of a continuous $M$ -Fejér map converge to a point of $M$

Proved

ShorNonsmooth.Fejer.fejer_map_iterates_converge

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

fejer-mapfixed-point-iterationp2o-batch-b23ap2o-gran-per-chapterp2o-plan-bookp2o-v1

Let $M \subseteq E_n$ be nonempty and let $\varphi : E_n \to E_n$ be an $M$ -Fejér map: $\varphi(y) = y$ and $\|\varphi(x) - y\| < \|x - y\|$ for all $y \in M$ and $x \notin M$ . If $\varphi$ is continuous, then for every starting point $x_0 \in E_n$ the sequence

x_{k+1} = \varphi(x_k), \qquad k = 0, 1, \dots,

converges to an element of $M$ : there is $\bar x \in M$ with $x_k \to \bar x$ .

This is the basic convergence principle of Fejér-type approximations (Eremin). Polyak's method is built on the same inequality, but its map need not be continuous, so the principle does not apply to it directly.

Formalization Note $M$ is any nonempty subset of $E_n$ (no closedness is assumed, as in the book). The sequence is any $x : \mathbb{N} \to E_n$ satisfying the recursion; its first term is arbitrary.

Preamble

import Mathlib
import Definitions.Def_ShorNonsmooth_Fejer_PolyakMethod

open Filter Topology

Formal statement

namespace ShorNonsmooth.Fejer

/-- Shor (1985), p. 37, Theorem 2.10 (after Eremin [23]). If an `M`-Fejér map `φ` is
continuous, then for any starting point `x₀` the sequence generated by `x_{k+1} = φ(x_k)`,
`k = 0, 1, …`, converges to an element of `M`. -/
theorem fejer_map_iterates_converge {n : ℕ} (M : Set (EuclideanSpace ℝ (Fin n)))
    (φ : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n))
    (hφ : IsMFejer M φ) (hcont : Continuous φ)
    (x : ℕ → EuclideanSpace ℝ (Fin n)) (hx : ∀ k, x (k + 1) = φ (x k)) :
    ∃ xbar ∈ M, Tendsto x atTop (𝓝 xbar) := by sorry

end ShorNonsmooth.Fejer

Source

Shor, Minimization Methods for Non-Differentiable Functions, Springer 1985, p. 37, Theorem 2.10 (with Definition (2.31), p. 36)

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 2.10 — iterates of a continuous MMM-Fejér map converge to a point of MMM

Theorem 2.10 — iterates of a continuous $M$ -Fejér map converge to a point of $M$