§1 — an infinite relaxation sequence with $0 < \lambda \leqslant 2$ is Fejér-monotone

Proved

RelaxationMethod.LowDim.run_isFejerMonotone

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

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

Let $A = \bigcap_i H_i$ be the solution polytope of a system of linear inequalities, assumed nonempty, and let $0 < \lambda \leqslant 2$ . Let $p_0, p_1, \dots$ be an infinite sequence produced by the relaxation process: every $p_\nu$ lies outside $A$ , and $p_{\nu+1}$ is obtained from $p_\nu$ by a relaxation step with parameter $\lambda$ . Then $\{p_\nu\}$ is Fejér-monotone with respect to $A$ :

p_\nu \neq p_{\nu+1}, \qquad |p_\nu - a| \geqslant |p_{\nu+1} - a| \quad (a \in A,\ \nu = 0, 1, \dots).

This observation from §1 is the link between the process and Lemma 1, and is used in the proofs of Theorems 1 and 2.

Formalization Note The paper argues for $0 < \lambda < 2$ (strict inequality for $a$ in $H_j$ ) and notes that for $\lambda = 2$ (1.1) holds with equality allowed; the statement covers the whole range $0 < \lambda \leqslant 2$ with the non-strict inequality (2.2), as §5 and §8 use it. The run is a sequence $p$ with a relaxation step after every point outside $A$ , together with the hypothesis that no point lies in $A$ .

Preamble

import Mathlib
import Definitions.Def_RelaxationMethod_LowDim_RelaxStep
import Definitions.Def_RelaxationMethod_Shared_FejerMonotone

Formal statement

namespace RelaxationMethod.LowDim

/-- §1, pp. 393–394 (restated in §5, p. 398): an infinite sequence produced by the relaxation
process with `0 < λ ⩽ 2` is Fejér-monotone with respect to the (nonempty) polytope `A`. -/
theorem run_isFejerMonotone {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 : ∀ ν, p ν ∉ polytope a b → IsRelaxStep a b lam (p ν) (p (ν + 1)))
    (hinf : ∀ ν, p ν ∉ polytope a b) :
    RelaxationMethod.Shared.IsFejerMonotone (polytope a b) p := 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, pp. 393–394, §1 (restated p. 398, §5)

Read-back

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

Setting. Work in $\mathbb{R}^n$ with the standard inner product.

There are $m$ vectors $a_1,\dots,a_m\in\mathbb{R}^n$ and $m$ reals $b_1,\dots,b_m$ .
Each $i$ gives a half-space $H_i=\{x:\langle a_i,x\rangle+b_i\ge 0\}$ .
The polytope is $A=\bigcap_i H_i$ . It is assumed nonempty.
$d(p,S)$ is the distance from a point to a set, with $d(p,\emptyset)=0$ .
$\lambda$ is a real number with $0<\lambda\le 2$ .
$(p_\nu)_{\nu\ge 0}$ is a sequence in $\mathbb{R}^n$ .

Hypotheses on the sequence.

$p_\nu\notin A$ for every $\nu\ge 0$ .
Whenever $p_\nu\notin A$ $p_{ν} \in / A$ (so, by the previous point, for every $\nu$ $ν$ ), $p_{\nu+1}$ $p_{ν + 1}$ comes from $p_\nu$ $p_{ν}$ by a relaxation step with parameter $\lambda$ $λ$ . This means there is an index $j$ $j$ (it may depend on $\nu$ $ν$ , with no fixed tie-breaking rule) such that:
- $d(p_\nu,H_i)\le d(p_\nu,H_j)$ for all $i$ ;
- there is a $q\in H_j$ with $|p_\nu-q|=d(p_\nu,H_j)$ and $p_{\nu+1}=p_\nu+\lambda(q-p_\nu)$ .

The initial point $p_0$ is arbitrary apart from lying outside $A$ .

Claim. The sequence $(p_\nu)$ satisfies the predicate "Fejér-monotone with respect to $A$ ". This predicate comes from an imported definition, RelaxationMethod.Shared.IsFejerMonotone, whose text is not included in the code provided. What exactly is asserted therefore depends on that definition and cannot be unfolded here.

Degenerate cases:

$m=0$ . Then $A=\mathbb{R}^n$ , so the hypothesis $p_\nu\notin A$ cannot hold and the statement is vacuously true.
$n=0$ . A nonempty $A$ is the whole one-point space, so again the statement is vacuous.
$\lambda=0$ is excluded, and so is $\lambda>2$ .

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

§1 — an infinite relaxation sequence with 0<λ⩽20 < \lambda \leqslant 20<λ⩽2 is Fejér-monotone

§1 — an infinite relaxation sequence with $0 < \lambda \leqslant 2$ is Fejér-monotone