Kaczmarz’s row projections

Paper

Angenäherte Auflösung von Systemen linearer Gleichungen, 1937. Bulletin International de l’Académie Polonaise des Sciences et des Lettres, classe A, pp. 355–357. Read the translation and original scan.

The result

A row projection lands exactly on the selected equation. A relaxed step with 0 ≤ ω ≤ 2 cannot increase squared distance to any solution of that row. If 0 < ω < 2 and the row is violated, the distance strictly decreases.

x′ = x + ω(b − a·x)a/(a·a) ‖x′ − z‖² = ‖x − z‖² − ω(2 − ω)(b − a·x)²/(a·a)

Scope & assumptions

Nine theorems in arbitrary finite dimension: positivity and nondegeneracy of the squared row length, residual identity, exact row satisfaction, the squared-distance identity, weak and strict descent, one-row fixed points, and common fixed points for a whole system. Cyclic convergence and convergence rates are not proved.

Vectors are real, the selected row is nonzero, and the comparison point z satisfies that row. The system theorem assumes every row is nonzero and characterizes simultaneous fixed points; it does not assume the system is consistent. Squared distances are explicit sums of squares, not Lean’s default norm on a function space.

Prior work

No matching named formalization was located in the bounded search on 2026-09-09. Mathlib and two optimization repositories were inspected, alongside indexed searches. Generic ingredients and related optimization results already exist. Priority remains unconfirmed; this does not establish a first-ever formalization.

Lean proof

Lean + Mathlib 4.33.1 · 9 checked theorems

import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Ring
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Positivity

/-!
Selected results for Kaczmarz's 1937 row-projection method.
Vectors have arbitrary finite dimension. sqdist is squared Euclidean distance,
not the default supremum norm on a function space. The relaxed step extends
the original unrelaxed update; no convergence rate is assumed or advertised.
-/
namespace PaperToLean.Kaczmarz
noncomputable section
open scoped BigOperators
variable {n : ℕ}
abbrev Vec (n : ℕ) := Fin n → ℝ

def dot (x y : Vec n) : ℝ := ∑ i, x i * y i
def sqdist (x y : Vec n) : ℝ := ∑ i, (x i - y i) ^ 2
def step (a : Vec n) (b ω : ℝ) (x : Vec n) : Vec n :=
  fun i => x i + ω * (b - dot a x) / dot a a * a i

theorem dot_self_nonneg (a : Vec n) : 0 ≤ dot a a := by
  exact Finset.sum_nonneg (fun i _ => mul_self_nonneg (a i))

theorem dot_self_eq_zero (a : Vec n) : dot a a = 0 ↔ a = 0 := by
  constructor
  · intro h
    have hzero := (Finset.sum_eq_zero_iff_of_nonneg
      (fun i (_ : i ∈ Finset.univ) => mul_self_nonneg (a i))).mp h
    funext i
    exact mul_self_eq_zero.mp (hzero i (Finset.mem_univ i))
  · rintro rfl
    simp [dot]

theorem row_residual (a x : Vec n) (b ω : ℝ) (ha : dot a a ≠ 0) :
    dot a (step a b ω x) - b = (1 - ω) * (dot a x - b) := by
  have hs (c : ℝ) : dot a (fun i => x i + c * a i) = dot a x + c * dot a a := by
    simp only [dot, mul_add, Finset.sum_add_distrib, Finset.mul_sum]
    congr 1
    apply Finset.sum_congr rfl
    intro i _
    ring
  unfold step
  rw [hs]
  field_simp
  ring

theorem satisfies_row (a x : Vec n) (b : ℝ) (ha : dot a a ≠ 0) :
    dot a (step a b 1 x) = b := by
  have h := row_residual a x b 1 ha
  linarith

theorem distance_identity (a x z : Vec n) (b ω : ℝ)
    (ha : dot a a ≠ 0) (hz : dot a z = b) :
    sqdist (step a b ω x) z = sqdist x z -
      ω * (2 - ω) * (b - dot a x) ^ 2 / dot a a := by
  have hs (c : ℝ) : sqdist (fun i => x i + c * a i) z =
      sqdist x z + 2 * c * (dot a x - dot a z) + c ^ 2 * dot a a := by
    simp only [sqdist, dot, mul_sub, Finset.mul_sum, ← Finset.sum_sub_distrib,
      ← Finset.sum_add_distrib]
    apply Finset.sum_congr rfl
    intro i _
    ring
  unfold step
  rw [hs, hz]
  field_simp
  ring

theorem relaxed_descent (a x z : Vec n) (b ω : ℝ)
    (ha : a ≠ 0) (hz : dot a z = b) (hω : 0 ≤ ω) (hω' : ω ≤ 2) :
    sqdist (step a b ω x) z ≤ sqdist x z := by
  have hp : 0 < dot a a := lt_of_le_of_ne (dot_self_nonneg a)
    (Ne.symm (fun h => ha ((dot_self_eq_zero a).mp h)))
  rw [distance_identity a x z b ω (ne_of_gt hp) hz]
  have h : 0 ≤ ω * (2 - ω) * (b - dot a x) ^ 2 / dot a a := by positivity
  linarith

theorem strict_descent (a x z : Vec n) (b ω : ℝ)
    (ha : a ≠ 0) (hz : dot a z = b) (hω : 0 < ω) (hω' : ω < 2)
    (hr : dot a x ≠ b) : sqdist (step a b ω x) z < sqdist x z := by
  have hp : 0 < dot a a := lt_of_le_of_ne (dot_self_nonneg a)
    (Ne.symm (fun h => ha ((dot_self_eq_zero a).mp h)))
  rw [distance_identity a x z b ω (ne_of_gt hp) hz]
  have hr' : b - dot a x ≠ 0 := sub_ne_zero.mpr (Ne.symm hr)
  have h : 0 < ω * (2 - ω) * (b - dot a x) ^ 2 / dot a a := by positivity
  linarith

theorem fixed_iff (a x : Vec n) (b : ℝ) (ha : dot a a ≠ 0) :
    step a b 1 x = x ↔ dot a x = b := by
  constructor
  · intro h
    simpa only [h] using satisfies_row a x b ha
  · intro h
    funext i
    simp [step, h]

/-- Common fixed points of all row projections are precisely solutions. -/
theorem system_fixed_iff {m : ℕ} (A : Fin m → Vec n) (b : Fin m → ℝ)
    (x : Vec n) (hA : ∀ j, dot (A j) (A j) ≠ 0) :
    (∀ j, step (A j) (b j) 1 x = x) ↔ (∀ j, dot (A j) x = b j) := by
  exact forall_congr' (fun j => fixed_iff (A j) x (b j) (hA j))

#print axioms dot_self_nonneg
#print axioms dot_self_eq_zero
#print axioms row_residual
#print axioms satisfies_row
#print axioms distance_identity
#print axioms relaxed_descent
#print axioms strict_descent
#print axioms fixed_iff
#print axioms system_fixed_iff
end
end PaperToLean.Kaczmarz

Lean 4.33.1
Dependencies: Mathlib 4.33.1 (see bundled lake-manifest.json)
File: Kaczmarz.lean
SHA-256: a7fbcb369689206655de3a49170c0decac924703d911168a5f9a28ec1f6b7d0f
Result: passed

'PaperToLean.Kaczmarz.dot_self_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kaczmarz.dot_self_eq_zero' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kaczmarz.row_residual' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kaczmarz.satisfies_row' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kaczmarz.distance_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kaczmarz.relaxed_descent' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kaczmarz.strict_descent' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kaczmarz.fixed_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Kaczmarz.system_fixed_iff' depends on axioms: [propext, Classical.choice, Quot.sound]

Run it

Install Lean with elan and Git. Download the project ZIP, extract it, and run these commands in that folder. The first command downloads the pinned Mathlib dependencies.

python3 prepare.py
lake env lean -DwarningAsError=true Kaczmarz.lean

A successful check prints the axiom dependencies and exits without errors.