Broyden’s least-change update

Paper

A Class of Methods for Solving Nonlinear Simultaneous Equations, 1965. Mathematics of Computation 19(92), pp. 577–593. Read the original paper.

The result

For nonzero s, Broyden’s direct update satisfies B′s = y and preserves the old action on directions orthogonal to s. Among all matrices C satisfying Cs = y, it is the unique one with minimum squared Frobenius distance to B.

B′ = B + (y − Bs)sᵀ/(sᵀs) ‖C − B‖²_F = ‖B′ − B‖²_F + ‖C − B′‖²_F when Cs = y

Scope & assumptions

Eight theorems for arbitrary finite rectangular real matrices: the update’s action, secant satisfaction, unchanged orthogonal directions, nonnegative distance and its zero case, a Pythagorean distance identity, minimal change, and uniqueness. Inverse updates, Jacobian approximation quality, and nonlinear solver convergence are not formalized.

sᵀs ≠ 0; over real finite vectors this means s is nonzero. For comparison, C must satisfy the same secant equation. B and C need not be square, symmetric, or invertible. The distance is the explicit sum of squared entry differences, and all arithmetic is exact.

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 · 8 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

/-!
Broyden (1965), DOI 10.1090/S0025-5718-1965-0198670-6.
The direct rank-one secant update and its least-change characterization.
Rectangular real matrices are allowed. No convergence or invertibility claim.
-/
namespace PaperToLean.Broyden
noncomputable section
open scoped BigOperators
variable {m n : ℕ}
abbrev Vec (n : ℕ) := Fin n → ℝ
abbrev Mat (m n : ℕ) := Fin m → Vec n
def dot (x y : Vec n) : ℝ := ∑ i, x i * y i
def distance (C B : Mat m n) : ℝ := ∑ j, ∑ i, (C j i - B j i) ^ 2
def update (B : Mat m n) (s : Vec n) (y : Vec m) : Mat m n :=
  fun j i => B j i + (y j - dot (B j) s) / dot s s * s i

theorem action (B : Mat m n) (s v : Vec n) (y : Vec m) (j : Fin m) :
    dot (update B s y j) v = dot (B j) v +
      (y j - dot (B j) s) / dot s s * dot s v := by
  simp only [dot, update, add_mul, Finset.sum_add_distrib, Finset.mul_sum]
  congr 1
  apply Finset.sum_congr rfl
  intro i _
  ring

theorem secant (B : Mat m n) (s : Vec n) (y : Vec m) (hs : dot s s ≠ 0) :
    ∀ j, dot (update B s y j) s = y j := by
  intro j
  rw [action]
  field_simp
  ring

theorem unchanged_on_orthogonal (B : Mat m n) (s v : Vec n) (y : Vec m)
    (hv : dot s v = 0) : ∀ j, dot (update B s y j) v = dot (B j) v := by
  intro j
  simp [action, hv]

theorem distance_nonneg (C B : Mat m n) : 0 ≤ distance C B := by
  exact Finset.sum_nonneg (fun _ _ => Finset.sum_nonneg (fun _ _ => sq_nonneg _))

theorem distance_zero_iff (C B : Mat m n) : distance C B = 0 ↔ C = B := by
  constructor
  · intro h
    have hj := (Finset.sum_eq_zero_iff_of_nonneg
      (fun j (_ : j ∈ Finset.univ) =>
        Finset.sum_nonneg (fun i (_ : i ∈ Finset.univ) => sq_nonneg (C j i - B j i)))).mp h
    funext j i
    have hi := (Finset.sum_eq_zero_iff_of_nonneg
      (fun i (_ : i ∈ Finset.univ) => sq_nonneg (C j i - B j i))).mp
        (hj j (Finset.mem_univ j))
    exact sub_eq_zero.mp (sq_eq_zero_iff.mp (hi i (Finset.mem_univ i)))
  · rintro rfl
    simp [distance]

/-- The exact gap, stronger than the usual least-change inequality. -/
theorem pythagorean (B C : Mat m n) (s : Vec n) (y : Vec m)
    (hs : dot s s ≠ 0) (hC : ∀ j, dot (C j) s = y j) :
    distance C B = distance (update B s y) B + distance C (update B s y) := by
  have row (b c s : Vec n) (t : ℝ) :
      (∑ i, (c i - b i) ^ 2) = (∑ i, (t * s i) ^ 2) +
      (∑ i, (c i - (b i + t * s i)) ^ 2) +
      2 * t * (dot c s - dot b s - t * dot s s) := by
    simp only [dot, mul_sub, Finset.mul_sum, ← Finset.sum_sub_distrib,
      ← Finset.sum_add_distrib]
    apply Finset.sum_congr rfl
    intro i _
    ring
  unfold distance
  rw [← Finset.sum_add_distrib]
  apply Finset.sum_congr rfl
  intro j _
  have hzero : dot (C j) s - dot (B j) s -
      (y j - dot (B j) s) / dot s s * dot s s = 0 := by
    rw [hC j]
    field_simp
    ring
  have h := row (B j) (C j) s ((y j - dot (B j) s) / dot s s)
  simpa only [hzero, mul_zero, add_zero, update, add_sub_cancel_left] using h

theorem least_change (B C : Mat m n) (s : Vec n) (y : Vec m)
    (hs : dot s s ≠ 0) (hC : ∀ j, dot (C j) s = y j) :
    distance (update B s y) B ≤ distance C B := by
  rw [pythagorean B C s y hs hC]
  exact le_add_of_nonneg_right (distance_nonneg C (update B s y))

theorem unique_minimizer (B C : Mat m n) (s : Vec n) (y : Vec m)
    (hs : dot s s ≠ 0) (hC : ∀ j, dot (C j) s = y j)
    (hmin : distance C B ≤ distance (update B s y) B) : C = update B s y := by
  have hp := pythagorean B C s y hs hC
  have hn := distance_nonneg C (update B s y)
  apply (distance_zero_iff C (update B s y)).mp
  linarith

#print axioms action
#print axioms secant
#print axioms unchanged_on_orthogonal
#print axioms distance_nonneg
#print axioms distance_zero_iff
#print axioms pythagorean
#print axioms least_change
#print axioms unique_minimizer
end
end PaperToLean.Broyden

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

'PaperToLean.Broyden.action' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Broyden.secant' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Broyden.unchanged_on_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Broyden.distance_nonneg' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Broyden.distance_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Broyden.pythagorean' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Broyden.least_change' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Broyden.unique_minimizer' 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 Broyden.lean

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