Documentation

TauCeti.Analysis.Matrix.HermitianSignature

The signature of a Hermitian matrix #

The signature of a Hermitian matrix is the number of its positive eigenvalues minus the number of its negative ones, the difference of the two indices of inertia of the Hermitian form x ↦ xᴴ A x. Mathlib's eigenvalues of a Hermitian matrix are real over any RCLike field, so Matrix.IsHermitian.signature is defined at that generality.

The theory is developed over an RCLike field. A Hermitian form there is related to a real quadratic form through Matrix.realify, which turns it into a real quadratic form of twice the rank (Matrix.IsHermitian.signature_realify).

That identity is what makes the real theory available here. In particular Sylvester's law of inertia over an RCLike field (Matrix.IsHermitian.signature_congr: the signature is unchanged by A ↦ P * A * Pᴴ for invertible P) follows from its real counterpart Matrix.signature_congr, and the signature of a real symmetric matrix read as a Hermitian complex matrix is its real signature (Matrix.IsHermitian.signature_map_ofReal).

Main definitions #

Main results #

References #

source
noncomputable def Matrix.IsHermitian.signature {ι : Type u_1} [Fintype ι] {𝕜 : Type u_3} [RCLike 𝕜] {A : Matrix ι ι 𝕜} (hA : A.IsHermitian) :
ℤ

The signature of a Hermitian matrix: its positive eigenvalues counted against its negative ones.

The eigenvalues do not depend on the decidability of equality on the index type, so the local decider here is invisible: Matrix.IsHermitian.signature_def identifies the definition with the one read off any DecidableEq ι instance.

Equations
Instances For
    source
    theorem Matrix.IsHermitian.signature_def {ι : Type u_1} [Fintype ι] {𝕜 : Type u_3} [RCLike 𝕜] {A : Matrix ι ι 𝕜} [DecidableEq ι] (hA : A.IsHermitian) :
    hA.signature = ∑ i : ι, if 0 < hA.eigenvalues i then 1 else if hA.eigenvalues i < 0 then -1 else 0

    The signature read off the eigenvalues for any DecidableEq ι instance.

    source
    @[simp]
    theorem Matrix.IsHermitian.signature_submatrix_equiv_self {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {𝕜 : Type u_3} [RCLike 𝕜] {A : Matrix ι ι 𝕜} (e : ι ≃ κ) (hA : A.IsHermitian) :
    ⋯.signature = hA.signature

    Reindexing both coordinates of a Hermitian matrix along an equivalence does not change its signature.

    source
    theorem Matrix.IsHermitian.signature_realify {ι : Type u_1} [Fintype ι] {𝕜 : Type u_3} [RCLike 𝕜] {A : Matrix ι ι 𝕜} (hA : A.IsHermitian) :
    A.realify.signature = 2 * hA.signature

    The realification of a Hermitian matrix has twice its signature. Each eigenvalue of a Hermitian matrix occurs twice in the realified form.

    source
    theorem Matrix.IsHermitian.signature_congr {ι : Type u_1} [Fintype ι] {𝕜 : Type u_3} [RCLike 𝕜] {A : Matrix ι ι 𝕜} [DecidableEq ι] {P : Matrix ι ι 𝕜} (hP : IsUnit P.det) (hA : A.IsHermitian) :
    ⋯.signature = hA.signature

    Sylvester's law of inertia for Hermitian matrices. The signature is unchanged by *-congruence A ↦ P * A * Pᴴ with P invertible.

    source
    @[simp]
    theorem Matrix.IsHermitian.signature_map_ofReal {ι : Type u_1} [Fintype ι] {𝕜 : Type u_3} [RCLike 𝕜] {M : Matrix ι ι ℝ} (hM : (M.map RCLike.ofReal).IsHermitian) :
    hM.signature = M.signature

    A real matrix, read as a Hermitian matrix over an RCLike field, keeps its real signature.

    source
    @[simp]
    theorem Matrix.IsHermitian.signature_zero {ι : Type u_1} [Fintype ι] {𝕜 : Type u_3} [RCLike 𝕜] :
    ⋯.signature = 0

    The zero matrix has signature zero.

    source
    @[simp]
    theorem Matrix.IsHermitian.signature_diagonal {ι : Type u_1} [Fintype ι] {𝕜 : Type u_3} [RCLike 𝕜] [DecidableEq ι] {d : ι → ℝ} :
    ⋯.signature = ∑ i : ι, if 0 < d i then 1 else if d i < 0 then -1 else 0

    The signature of a real diagonal matrix counts its positive entries against its negative ones.

    source
    theorem Matrix.IsHermitian.signature_eq_of_congr_diagonal {ι : Type u_1} [Fintype ι] {𝕜 : Type u_3} [RCLike 𝕜] {A : Matrix ι ι 𝕜} [DecidableEq ι] {P : Matrix ι ι 𝕜} (hP : IsUnit P.det) (hA : A.IsHermitian) {d : ι → ℝ} (h : P * A * P.conjTranspose = (diagonal d).map RCLike.ofReal) :
    hA.signature = ∑ i : ι, if 0 < d i then 1 else if d i < 0 then -1 else 0

    The signature from an explicit diagonalising *-congruence.

    source
    @[simp]
    theorem Matrix.IsHermitian.signature_fromBlocks_zero {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {𝕜 : Type u_3} [RCLike 𝕜] {A : Matrix ι ι 𝕜} {B : Matrix κ κ 𝕜} (hA : A.IsHermitian) (hB : B.IsHermitian) :
    ⋯.signature = hA.signature + hB.signature

    Additivity of the signature along a block diagonal. The realification of a block-diagonal matrix is, after reindexing, the block diagonal of the two realifications.

    source
    @[simp]
    theorem Matrix.IsHermitian.signature_neg {ι : Type u_1} [Fintype ι] {𝕜 : Type u_3} [RCLike 𝕜] {A : Matrix ι ι 𝕜} (hA : A.IsHermitian) :
    ⋯.signature = -hA.signature

    Negating a Hermitian matrix negates its signature.

    source
    theorem Matrix.IsHermitian.signature_eq_zero_of_congr_neg {ι : Type u_1} [Fintype ι] {𝕜 : Type u_3} [RCLike 𝕜] {A : Matrix ι ι 𝕜} [DecidableEq ι] {P : Matrix ι ι 𝕜} (hP : IsUnit P.det) (hA : A.IsHermitian) (hneg : P * A * P.conjTranspose = -A) :
    hA.signature = 0

    A Hermitian matrix congruent to its negation by an invertible matrix has signature zero.

    source
    theorem Matrix.IsHermitian.signature_eq_zero_of_fin_two_diagonal_eq_zero {𝕜 : Type u_3} [RCLike 𝕜] {A : Matrix (Fin 2) (Fin 2) 𝕜} (hA : A.IsHermitian) (h₀ : A 0 0 = 0) (h₁ : A 1 1 = 0) :
    hA.signature = 0

    A two-dimensional Hermitian form with zero diagonal has signature zero, including when its off-diagonal entry vanishes.

    source
    @[simp]
    theorem Matrix.IsHermitian.signature_map_starRingEnd {ι : Type u_1} [Fintype ι] {𝕜 : Type u_3} [RCLike 𝕜] {A : Matrix ι ι 𝕜} (hA : A.IsHermitian) :
    ⋯.signature = hA.signature

    Conjugating every entry of a Hermitian matrix preserves its signature: it is the congruence by the reflection negating the imaginary coordinates.