Lemma 1, Case 1 — a Fejér-monotone sequence converges when $A$ spans $E_n$

Proved

RelaxationMethod.FullDim.lemma1_case1

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

convergencefejer-monotonep2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $A$ be a set of points of $E_n$ that is not contained in any hyperplane, i.e. whose affine span is all of $E_n$ (dimension $r = n$ ). If the sequence $q_0, q_1, \dots$ is Fejér-monotone with respect to $A$ (it lies outside $A$ , consecutive terms differ, and $|q_{i+1} - a| \le |q_i - a|$ for every $a \in A$ ), then it converges: there is a point $l \in E_n$ with

\lim_{\nu\to\infty} q_\nu = l .

This is the convergence engine of the paper: applied to relaxation sequences it gives Agmon's convergence theorem (Theorem 1, Case 1) and is the first step of the finite-termination proof for the reflexion method (Theorem 1, Case 2).

Formalization Note The paper states the lemma for the polytope $A$ of (1.4); we state it for an arbitrary set $A$ whose affine span is the whole space, which contains the paper's case (a nonempty polytope of dimension $n$ ). "Not contained in any hyperplane" is affineSpan ℝ A = ⊤; this also forces $A$ to be nonempty.

Preamble

import Mathlib
import Definitions.Def_RelaxationMethod_FullDim_RelaxStep
import Definitions.Def_RelaxationMethod_FullDim_FejerMonotone
open Filter Topology

Formal statement

namespace RelaxationMethod.FullDim

/-- Lemma 1, Case 1, p. 397: a sequence that is Fejér-monotone with respect to a set `A` of
dimension `n` (not contained in any hyperplane, `affineSpan ℝ A = ⊤`) converges to a point.
Stated for an arbitrary set `A`, which contains the paper's case of the polytope (1.4). -/
theorem lemma1_case1 {n : ℕ} (A : Set (EuclideanSpace ℝ (Fin n)))
    (hr : affineSpan ℝ A = ⊤) (q : ℕ → EuclideanSpace ℝ (Fin n))
    (hq : IsFejerMonotone A q) :
    ∃ l : EuclideanSpace ℝ (Fin n), Tendsto q atTop (𝓝 l) := by sorry

end RelaxationMethod.FullDim

Source

Motzkin and Schoenberg, The relaxation method for linear inequalities, Canad. J. Math. 6 (1954), p. 397, Lemma 1, Case 1

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Let $n$ be a natural number and let $A\subseteq\mathbb{R}^n$ be an arbitrary set. No convexity, closedness or boundedness is assumed.

Hypotheses:

The affine hull of $A$ is all of $\mathbb{R}^n$ .
$q_0,q_1,\dots$ $q_{0}, q_{1}, \dots$ is a sequence in $\mathbb{R}^n$ $R^{n}$ that is Fejér monotone with respect to $A$ $A$ . That is:
- $q_\nu\notin A$ for all $\nu$ ;
- $q_\nu\ne q_{\nu+1}$ for all $\nu$ ;
- $|q_{\nu+1}-x|\le|q_\nu-x|$ for every $x\in A$ and every $\nu$ .

Conclusion. There is a point $l\in\mathbb{R}^n$ with $q_\nu\to l$ as $\nu\to\infty$ , in the Euclidean topology. Nothing is asserted about where $l$ lies relative to $A$ .

Degenerate cases:

$A$ empty: The affine hull of the empty set is empty, not $\mathbb{R}^n$ , so $A$ cannot be empty.
$A=\mathbb{R}^n$ : The condition $q_\nu\notin A$ cannot hold, so the statement is vacuous.
$n=0$ : The space is a single point, so consecutive distinct terms are impossible and the statement is vacuous.

Human review

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

View graph

Lemma 1, Case 1 — a Fejér-monotone sequence converges when AAA spans EnE_nEn​

Lemma 1, Case 1 — a Fejér-monotone sequence converges when $A$ spans $E_n$