Lemma 1, Case 2 — a Fejér-monotone sequence converges or its limit points lie on a sphere with axis $L_r$

Proved

RelaxationMethod.LowDim.lemma1_case2

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

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

Let $A \subseteq E_n$ be nonempty, let $L_r$ be the affine span of $A$ , and assume $L_r \neq E_n$ (that is, $r < n$ ). Let $\{q_\nu\}$ be Fejér-monotone with respect to $A$ . Then either $\{q_\nu\}$ converges to a point, or there is a point $c \notin L_r$ such that every limit point of $\{q_\nu\}$ lies on the spherical surface having $L_r$ as its axis and passing through $c$ :

\text{every limit point } x \text{ satisfies } |x - a| = |c - a| \text{ for all } a \in L_r.

Together with Case 1 ( $r = n$ : convergence), this is the paper's Lemma 1. Case 2 is what makes a non-convergent run accumulate on a sphere around the axis $L_r$ , the starting point of both cases of Theorem 2.

Formalization Note The paper states the lemma for the polytope $A$ ; it is stated here for an arbitrary nonempty set $A$ , which is stronger (the proof on p. 398 uses only that $A$ spans $L_r$ , and §10 applies it to a convex set). "Limit point of the sequence" is a cluster point (MapClusterPt x atTop q), not a point of the closure of the range. The condition $c \notin L_r$ excludes the degenerate one-point locus.

Preamble

import Mathlib
import Definitions.Def_RelaxationMethod_Shared_FejerMonotone
import Definitions.Def_RelaxationMethod_LowDim_AxisSphere

open Filter Topology

Formal statement

namespace RelaxationMethod.LowDim

/-- Lemma 1, Case 2, p. 397: if `A` is nonempty and its affine span `L_r` is not the whole space
(`r < n`), a Fejér-monotone sequence with respect to `A` either converges or all its limit
points lie on one spherical surface having `L_r` as its axis. Stated for an arbitrary nonempty
set `A` (the paper states it for the polytope `A`). -/
theorem lemma1_case2 {n : ℕ} (A : Set (EuclideanSpace ℝ (Fin n))) (hA : A.Nonempty)
    (hr : affineSpan ℝ A ≠ ⊤) (q : ℕ → EuclideanSpace ℝ (Fin n))
    (hq : RelaxationMethod.Shared.IsFejerMonotone A q) :
    (∃ l, Tendsto q atTop (𝓝 l)) ∨
      ∃ c ∉ affineSpan ℝ A,
        ∀ x, MapClusterPt x atTop q → x ∈ axisSphere (affineSpan ℝ A) c := by sorry

end RelaxationMethod.LowDim

Source

Motzkin and Schoenberg, The relaxation method for linear inequalities, Canad. J. Math. 6 (1954), DOI 10.4153/CJM-1954-038-x, p. 397, §4, Lemma 1, Case 2 (proof p. 398)

Read-back

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

Setting. Work in $\mathbb{R}^n$ with Euclidean distance.

$A\subseteq\mathbb{R}^n$ is an arbitrary nonempty set. It need not be a polytope, convex, or closed.
$\operatorname{aff}(A)$ , the affine span of $A$ , is assumed not to be all of $\mathbb{R}^n$ .
$(q_\nu)_{\nu\ge 0}$ is a sequence satisfying the predicate "Fejér-monotone with respect to $A$ ". That predicate comes from the imported definition RelaxationMethod.Shared.IsFejerMonotone, whose text is not included in the code provided, so the hypothesis cannot be unfolded here.
For an affine subspace $L$ and a point $c$ , write

S(L,c)=\{x: |x-a|=|c-a|\ \forall a\in L\}.

Claim. At least one of the following holds.

$(q_\nu)$ converges to some point $l\in\mathbb{R}^n$ .
There is a point $c\notin\operatorname{aff}(A)$ such that every cluster point of $(q_\nu)$ lies in $S(\operatorname{aff}(A),c)$ . A cluster point is a point $x$ such that every neighbourhood of $x$ contains $q_\nu$ for infinitely many $\nu$ . Membership in $S(\operatorname{aff}(A),c)$ means

|x-a|=|c-a| \quad\text{for all } a\in\operatorname{aff}(A).

The point $c$ is not required to be related to the sequence in any other way.

Degenerate cases:

No cluster points. If $(q_\nu)$ has no cluster points (for example, if $|q_\nu|\to\infty$ ), the second alternative holds automatically. A point $c\notin\operatorname{aff}(A)$ always exists because $\operatorname{aff}(A)\ne\mathbb{R}^n$ .
One cluster point. If there is exactly one cluster point $x$ , the second alternative holds with $c=x$ whenever $x\notin\operatorname{aff}(A)$ .
$n=0$ . The affine span of a nonempty set is the whole space, so the hypothesis on $\operatorname{aff}(A)$ fails 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 2 — a Fejér-monotone sequence converges or its limit points lie on a sphere with axis LrL_rLr​

Lemma 1, Case 2 — a Fejér-monotone sequence converges or its limit points lie on a sphere with axis $L_r$