The limit of a convergent affine iteration is a fixed point

Proved

MetodosNumericos.affine_iteration_limit_is_solution

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

linear-algebranumerical-analysis

If the iterates $x^{(k+1)} = Bx^{(k)} + d$ converge to $\\alpha$ , then $\\alpha = B\\alpha + d$ . This is Proposição 5.5.1: the limit of the successive approximations solves the fixed-point form of the system, hence the system itself.

Preamble

import Mathlib

open Filter Topology

Formal statement

namespace MetodosNumericos

theorem affine_iteration_limit_is_solution {n : ℕ} (B : Matrix (Fin n) (Fin n) ℝ)
    (d : Fin n → ℝ) (x : ℕ → (Fin n → ℝ)) (alpha : Fin n → ℝ)
    (hrec : ∀ k, x (k + 1) = B.mulVec (x k) + d)
    (hconv : Tendsto x atTop (𝓝 alpha)) :
    alpha = B.mulVec alpha + d := by sorry

end MetodosNumericos

Source

S. R. Freitas, Métodos Numéricos (UFMS, 2000), Cap. 5, Proposição 5.5.1, p. 106.

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$ , a vector $d \\in \\mathbb{R}^n$ , a sequence of vectors $x^{(0)}, x^{(1)}, \\dots \\in \\mathbb{R}^n$ and a vector $\\alpha \\in \\mathbb{R}^n$ , the hypotheses are:

for every natural number $k$ , $x^{(k+1)} = Bx^{(k)} + d$ (matrix-vector product plus vector, componentwise);
the sequence $k \\mapsto x^{(k)}$ converges to $\\alpha$ in $\\mathbb{R}^n$ (equivalently, coordinatewise).

The conclusion is the vector equality $\\alpha = B\\alpha + d$ . Nothing is assumed about $B$ or $d$ , and the initial vector $x^{(0)}$ is unconstrained. For $n = 0$ the statement is trivially true.

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