The fixed points of the Jacobi sweep are the solutions of $Ax=b$

Proved

MetodosNumericos.jacobi_fixed_point_equiv

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

linear-algebranumerical-analysis

If all diagonal entries of $A$ are nonzero, then a vector $x$ satisfies $Ax = b$ if and only if it is unchanged by the Jacobi sweep. This is the equivalence $Ax = b \\iff x = Bx + d$ of Proposição 5.5.2, stated for the Jacobi splitting.

Preamble

import Mathlib
import Definitions.Def_MetodosNumericos_sistemasDefs

Formal statement

namespace MetodosNumericos

theorem jacobi_fixed_point_equiv {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (b : Fin n → ℝ)
    (hdiag : ∀ i, A i i ≠ 0) (x : Fin n → ℝ) :
    A.mulVec x = b ↔ jacobiSweep A b x = x := by sorry

end MetodosNumericos

Source

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

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 $A$ , a vector $b$ and a vector $x$ , under the hypothesis that $a_{ii} \\neq 0$ for every index $i$ , the statement is an if-and-only-if between:

the vector equality $Ax = b$ , where $Ax$ is the usual matrix-vector product; and
the vector equality $J(x) = x$ , where $J(x)$ is the Jacobi sweep, whose $i$ -th coordinate is $\\dfrac{b_i - \\sum_{j \\neq i} a_{ij}x_j}{a_{ii}}$ .

Both sides are equalities of functions on the index type, i.e. hold coordinatewise for every $i$ . For $n = 0$ both sides are 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

The fixed points of the Jacobi sweep are the solutions of Ax=bAx=bAx=b

The fixed points of the Jacobi sweep are the solutions of $Ax=b$