Local constancy of the Hermitian signature

The signature of a nonsingular Hermitian matrix is unchanged by sufficiently small Hermitian perturbations. More precisely, nearby Hermitian matrices are congruent to the original matrix by an invertible matrix. This gives local constancy for continuous Hermitian families, without choosing or ordering their eigenvalues continuously.

The congruence uses the square root near the identity from TauCeti.Analysis.Normed.Algebra.SquareRoot. For a fixed nonsingular Hermitian matrix A, the comparison A⁻¹ * B is self-adjoint for the pairing defined by A. Uniqueness of the square root near the identity makes its square root self-adjoint for that pairing too, and hence gives Rᴴ * A * R = B. This is the matrix version of the square-root argument in TauCeti.exists_congruence_of_symmetric_family.

This stability result applies in particular to signature functions of Seifert matrices away from their singular parameters. Through Gram matrices, it also gives local constancy of the negative index of a continuous family of symmetric bilinear forms on a finite-dimensional real space at a nondegenerate member, and hence constancy along a preconnected set of nondegenerate members. At a degenerate member the negative index can jump, but only upwards: a negative-definite subspace stays negative-definite under small perturbations, so the negative index of any continuous family of bilinear forms is lower semicontinuous.

References

• R. S. Palais, Morse theory on Hilbert manifolds, Topology 2 (1963), 299–340, Section 2 (congruences from operator square roots).

theorem Matrix.IsHermitian.eventually_exists_conjTranspose_mul_mul_eq {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A : Matrix ι ι 𝕜} (hA : A.IsHermitian) (hdet : IsUnit A.det) : ∀ᶠ (B : Matrix ι ι 𝕜) in nhds A, B.IsHermitian → ∃ (R : Matrix ι ι 𝕜), IsUnit R.det ∧ R.conjTranspose * A * R = B

Every Hermitian matrix sufficiently close to a nonsingular Hermitian matrix is congruent to it by an invertible matrix.

theorem Matrix.IsHermitian.eventually_signature_eq {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A : Matrix ι ι 𝕜} (hA : A.IsHermitian) (hdet : IsUnit A.det) : ∀ᶠ (B : Matrix ι ι 𝕜) in nhds A, ∀ (hB : B.IsHermitian), hB.signature = hA.signature

The Hermitian signature is constant near every nonsingular Hermitian matrix, when restricted to Hermitian perturbations.

theorem Matrix.IsHermitian.eventually_signature_eq_of_continuousAt {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {X : Type u_3} [TopologicalSpace X] {B : X → Matrix ι ι 𝕜} (hB : ∀ (x : X), (B x).IsHermitian) {x : X} (hc : ContinuousAt B x) (hdet : IsUnit (B x).det) : ∀ᶠ (y : X) in nhds x, ⋯.signature = ⋯.signature

A continuous Hermitian family has locally constant signature at every parameter where its matrix is nonsingular. The parameter space is arbitrary.

theorem Matrix.IsHermitian.eventually_sigNeg_toQuadraticForm'_eq_of_continuousAt {ι : Type u_2} [Fintype ι] [DecidableEq ι] {X : Type u_3} [TopologicalSpace X] {B : X → Matrix ι ι ℝ} {x : X} (hB : ∀ᶠ (y : X) in nhds x, (B y).IsHermitian) (hc : ContinuousAt B x) (hdet : IsUnit (B x).det) : ∀ᶠ (y : X) in nhds x, sigNeg (B y).toQuadraticForm' = sigNeg (B x).toQuadraticForm'

The negative index of the quadratic form of a continuous real symmetric matrix family is locally constant at a nonsingular member. Only local symmetry of the family is required.

theorem ContinuousLinearMap.eventually_sigNeg_toBilinForm_eq_of_continuousAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {X : Type u_2} [TopologicalSpace X] {V : X → E →L[ℝ] E →L[ℝ] ℝ} {x : X} (hsymm : ∀ᶠ (y : X) in nhds x, (V y).toBilinForm.IsSymm) (hc : ContinuousAt V x) (hnd : (V x).toBilinForm.Nondegenerate) : ∀ᶠ (y : X) in nhds x, sigNeg (LinearMap.BilinMap.toQuadraticMap (V y).toBilinForm) = sigNeg (LinearMap.BilinMap.toQuadraticMap (V x).toBilinForm)

The negative index of a continuous family of symmetric bilinear forms on a finite-dimensional real space is locally constant at a nondegenerate member. Only local symmetry of the family is required.

theorem ContinuousLinearMap.eventually_sigNeg_toBilinForm_le_of_continuousAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {X : Type u_2} [TopologicalSpace X] {V : X → E →L[ℝ] E →L[ℝ] ℝ} {x : X} (hc : ContinuousAt V x) : ∀ᶠ (y : X) in nhds x, sigNeg (LinearMap.BilinMap.toQuadraticMap (V x).toBilinForm) ≤ sigNeg (LinearMap.BilinMap.toQuadraticMap (V y).toBilinForm)

The negative index is lower semicontinuous. Along a family of continuous bilinear forms on a finite-dimensional real space, continuous at x, the negative index at nearby parameters is at least the negative index at x. Neither symmetry nor nondegeneracy is required.

theorem ContinuousLinearMap.sigNeg_toBilinForm_eq_of_isPreconnected {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {X : Type u_2} [TopologicalSpace X] {V : X → E →L[ℝ] E →L[ℝ] ℝ} {s : Set X} (hs : IsPreconnected s) (hc : ContinuousOn V s) (hsymm : ∀ t ∈ s, (V t).toBilinForm.IsSymm) (hnd : ∀ t ∈ s, (V t).toBilinForm.Nondegenerate) {x y : X} (hx : x ∈ s) (hy : y ∈ s) : sigNeg (LinearMap.BilinMap.toQuadraticMap (V x).toBilinForm) = sigNeg (LinearMap.BilinMap.toQuadraticMap (V y).toBilinForm)

The negative index is constant between crossings. Along a family of symmetric continuous bilinear forms, continuous and nondegenerate on a preconnected set s, the negative index takes the same value at any two points of s.