Chapter 7, Jacobi reduction lemma

Proved

BookSixth.jacobi_reduction

by xiangyazi24 · Sep 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

proofs-from-the-booksixth-edition

If a real symmetric matrix has positive sum of squared off-diagonal entries, an orthogonal conjugation strictly decreases this sum.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.jacobi_reduction {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) (hA : A.IsHermitian) (h : 0 < offDiagonalMass A) :
    ∃ Q : Matrix.unitaryGroup (Fin n) ℝ,
      offDiagonalMass (star (Q : Matrix (Fin n) (Fin n) ℝ) * A * (Q : Matrix (Fin n) (Fin n) ℝ)) < offDiagonalMass A := by sorry

Source

Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), Chapter 7, Jacobi reduction lemma, p. 40. https://doi.org/10.1007/978-3-662-57265-8_7

View graph