Contraction implies convergence of the affine iteration

Proved

MetodosNumericos.affine_iteration_converges_of_contraction

by Lucas · Sep 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebranumerical-analysis

If $\\lVert Bv\\rVert \\le c\\lVert v\\rVert$ for all $v$ with $c < 1$ , and $y$ satisfies $y = By + d$ , then every sequence with $x^{(k+1)} = Bx^{(k)} + d$ converges to $y$ , whatever the starting vector. This is Proposição 5.5.3, with the consistency of the vector and matrix norms expressed directly by the hypothesis on $B$ .

Preamble

import Mathlib

open Filter Topology

Formal statement

namespace MetodosNumericos

theorem affine_iteration_converges_of_contraction {n : ℕ} (B : Matrix (Fin n) (Fin n) ℝ)
    (d : Fin n → ℝ) (c : ℝ) (hc : c < 1)
    (hB : ∀ v : Fin n → ℝ, ‖B.mulVec v‖ ≤ c * ‖v‖)
    (y : Fin n → ℝ) (hy : y = B.mulVec y + d)
    (x : ℕ → (Fin n → ℝ)) (hrec : ∀ k, x (k + 1) = B.mulVec (x k) + d) :
    Tendsto x atTop (𝓝 y) := by sorry

end MetodosNumericos

Source

S. R. Freitas, Métodos Numéricos (UFMS, 2000), Cap. 5, Proposição 5.5.3, pp. 108–109.

Read-back

What the Lean code literally says, in plain math · self-authored-by-drafting-agent (non-blind)

Disclosure: this read-back is not blind. It was written by the same agent that drafted the Lean statement, at the explicit instruction of the mission's human owner, and not by an independent auditor with fresh context.

For a natural number $n$ , a real $n \\times n$ matrix $B$ , vectors $d, y \\in \\mathbb{R}^n$ , a real number $c$ and a sequence of vectors $x^{(k)}$ , the hypotheses are:

$c < 1$ ;
for every vector $v \\in \\mathbb{R}^n$ , $\\lVert Bv\\rVert \\le c\\,\\lVert v\\rVert$ , where $\\lVert \\cdot \\rVert$ is the supremum norm on the finite product space (the maximum of the absolute values of the coordinates);
$y = By + d$ ;
for every $k$ , $x^{(k+1)} = Bx^{(k)} + d$ .

The conclusion is that $x^{(k)} \\to y$ as $k \\to \\infty$ .

The starting vector $x^{(0)}$ is arbitrary. Taking $v = 0$ shows the hypothesis is consistent for any $c \\ge 0$ ; for $n \\ge 1$ it forces $c \\ge 0$ unless $B = 0$ . The vector $y$ is given as a hypothesis, not asserted to exist or to be unique.

Human review

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

View graph