Spectral Sign Factorization

This is an auxiliary spectral factorization for a real symmetric matrix.

Let $\iota$ be a finite index type with decidable equality, and let $M$ be a symmetric real matrix indexed by $\iota$. Define

$$A=\operatorname{CFC.sqrt}(M^2),\qquad S=\operatorname{CFC.sqrt}(A),\qquad \operatorname{Sign}(M)=\operatorname{cfc}(x\mapsto\operatorname{sign}(x))(M).$$

Then

$$S^2=A,$$

and

$$S\,\operatorname{Sign}(M)\,S=M.$$

Moreover, if $M$ is a unit matrix, then

$$\operatorname{Sign}(M)^2=I.$$

The factorization isolates the sign component of a possibly singular or indefinite symmetric matrix and is reusable in arguments involving square-root weights.

Formalization Note The definitions correspond to CFC.sqrt and cfc; the sign-square identity is asserted only under IsUnit M.

Original Lean declaration header

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

theorem symmetric_matrix_sign_factorization
    (M : Matrix ι ι ℝ) (hM : M.IsSymm) :
    let AbsM : Matrix ι ι ℝ := CFC.sqrt (M * M)
    let S : Matrix ι ι ℝ := CFC.sqrt AbsM
    let SignM : Matrix ι ι ℝ := cfc (fun x : ℝ => (SignType.sign x : ℝ)) M
    S * S = AbsM ∧ S * SignM * S = M ∧
      (IsUnit M → SignM * SignM = 1)

Module navigation

Module: Analysis/Matrix/Sign.

Supporting theorems: symmetric_matrix_sqrt_real_cfc_bridge.

Previous: symmetric_matrix_sqrt_real_cfc_bridge · Next: symmetric_jordan_decomposition.

Source excerpt, lines 108–114 · Frozen source 408915f.

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_Sign

open scoped MatrixOrder
variable {ι : Type*}
variable [Fintype ι] [DecidableEq ι]

theorem FunctionalInequalities.Analysis.symmetric_matrix_sign_factorization_readable
    (M : Matrix ι ι ℝ) (hM : M.IsSymm) :
    let AbsM : Matrix ι ι ℝ := CFC.sqrt (M * M)
    let S : Matrix ι ι ℝ := CFC.sqrt AbsM
    let SignM : Matrix ι ι ℝ := cfc (fun x : ℝ => (SignType.sign x : ℝ)) M
    S * S = AbsM ∧ S * SignM * S = M ∧
      (IsUnit M → SignM * SignM = 1) := by sorry