Jordan Decomposition of a Symmetric Matrix

This formalizes an auxiliary spectral decomposition for real symmetric matrices.

Let $\iota$ be a finite index type, with decidable equality, and let $B$ be a real matrix indexed by $\iota$. Assume that $B$ is symmetric. Then there exist real matrices $P$ and $N$ such that:

1. $P$ and $N$ are positive semidefinite;
2. $B=P-N$;
3. $PN=0$ and $NP=0$;
4. the squared trace decomposes as

This is the matrix Jordan decomposition used to extend trace-energy estimates from positive semidefinite matrices to arbitrary symmetric matrices.

Formalization Note The matrices are constructed through the real continuous functional calculus cfc; the result includes the empty finite index type.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

theorem symmetric_jordan_decomposition (B : Matrix ι ι ℝ) (hB : B.IsSymm) :
    ∃ P N : Matrix ι ι ℝ,
      P.PosSemidef ∧ N.PosSemidef ∧ B = P - N ∧
      P * N = 0 ∧ N * P = 0 ∧
      (B * B).trace = (P * P).trace + (N * N).trace

Module navigation

Module: Analysis/Matrix/Sign.

Supporting theorems: cfc_eq_mul_diagonal_mul.

Previous: symmetric_matrix_sign_factorization · Next: symmetric_matrix_spectral_geometry.

Source excerpt, lines 261–265 · Frozen source 408915f.