§5 — an infinite relaxation sequence is Fejér-monotone with respect to $A$

Proved

RelaxationMethod.FullDim.run_fejerMonotone

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

fejer-monotonep2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1relaxation-method

Let $A$ be the nonempty solution polytope of a system of linear inequalities in $E_n$ and let $0 < \lambda \le 2$ . If $p_0, p_1, p_2, \dots$ is a run of the relaxation process with parameter $\lambda$ that never terminates, i.e. $p_\nu \notin A$ for every $\nu$ , then the sequence $\{p_\nu\}$ is Fejér-monotone with respect to $A$ :

p_\nu \ne p_{\nu+1}, \qquad |p_{\nu+1} - a| \le |p_\nu - a| \quad \text{for all } a \in A,\ \nu \ge 0 .

This is the link between the relaxation process and Lemma 1, which is a statement about Fejér-monotone sequences.

Formalization Note The paper states this in §5 ("As already mentioned in § 1") for the case $r = n$ , $0 < \lambda < 2$ , and uses it again in §6 for $\lambda = 2$ ; we state it for $0 < \lambda \le 2$ and without the dimension hypothesis, which the claim does not use. The parameter $\lambda$ is named lam.

Preamble

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

Formal statement

namespace RelaxationMethod.FullDim

/-- §5, p. 398 (from §1): an infinite run of the relaxation process with `0 < lam ≤ 2`,
i.e. one that never enters the nonempty polytope `A`, is Fejér-monotone with respect to `A`. -/
theorem run_fejerMonotone {n m : ℕ} (a : Fin m → EuclideanSpace ℝ (Fin n)) (b : Fin m → ℝ)
    (hA : (polytope a b).Nonempty) (lam : ℝ) (hlam0 : 0 < lam) (hlam2 : lam ≤ 2)
    (p : ℕ → EuclideanSpace ℝ (Fin n)) (hrun : IsRelaxRun a b lam p)
    (hinf : ∀ ν : ℕ, p ν ∉ polytope a b) :
    IsFejerMonotone (polytope a b) p := by sorry

end RelaxationMethod.FullDim

Source

Motzkin and Schoenberg, The relaxation method for linear inequalities, Canad. J. Math. 6 (1954), p. 398, §5 (and §1, pp. 393–394)

Read-back

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

Fix natural numbers $n$ and $m$ . Take vectors $a_0,\dots,a_{m-1}\in\mathbb{R}^n$ and reals $b_0,\dots,b_{m-1}$ . Let $H_i=\{x:\langle a_i,x\rangle+b_i\ge 0\}$ and $A=\bigcap_{i<m}H_i$ .

Hypotheses:

$A$ is nonempty.
$\lambda$ is a real number with $0<\lambda\le 2$ .
$p_0,p_1,\dots$ is a sequence in $\mathbb{R}^n$ that is a relaxation run with parameter $\lambda$ . That is, whenever $p_\nu\notin A$ , there is an index $j$ with $d(p_\nu,H_i)\le d(p_\nu,H_j)$ for all $i$ , and a point $q\in H_j$ with $|p_\nu-q|=d(p_\nu,H_j)$ , such that $p_{\nu+1}=p_\nu+\lambda(q-p_\nu)$ . Here $d$ is the infimum distance, taken as $0$ to an empty set.
$p_\nu\notin A$ for every $\nu\ge 0$ .

Conclusion. The sequence is Fejér monotone with respect to $A$ . That is, all three of the following hold:

$p_\nu\notin A$ for all $\nu$ .
$p_\nu\ne p_{\nu+1}$ for all $\nu$ .
For every $x\in A$ and every $\nu$ ,

|p_{\nu+1}-x|\le|p_\nu-x| .

Degenerate cases:

$m=0$ : $A=\mathbb{R}^n$ , so the hypothesis that every $p_\nu\notin A$ cannot hold and the statement is vacuous.
$n=0$ : A nonempty $A$ is the whole one-point space, so again 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

§5 — an infinite relaxation sequence is Fejér-monotone with respect to AAA

§5 — an infinite relaxation sequence is Fejér-monotone with respect to $A$