Spectral Geometry of an Invertible Symmetric Matrix

This is an auxiliary finite-dimensional package of spectral facts for an invertible symmetric matrix.

Let $n\in\mathbb N$ and let $M$ be a symmetric real matrix on $\operatorname{Fin}(n)$. Assume that $M$ is a unit matrix. Define

Then:

1. $B$ and $S$ are positive semidefinite;
2. $Q$ is symmetric;
3. $B^2=M^2$, $S^2=B$, and $SQS=M$;
4. $Q^2=I$ and $S$ is a unit matrix;
5. the continuous linear map induced by $Q$ is self-adjoint;
6. there exists a continuous linear equivalence $e$ of $\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin} n)$ whose continuous linear map is the map induced by $S$, and this map is self-adjoint.

This packages the matrix identities and operator-theoretic properties needed when passing from spectral matrices to Euclidean-space maps.

Formalization Note The conclusion is valid for every $n$, including $n=0$; the Euclidean space is specifically EuclideanSpace ℝ (Fin n).

Original Lean declaration header

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

set_option maxHeartbeats 700000 in
theorem symmetric_matrix_spectral_geometry {n : ℕ}
    (M : Matrix (Fin n) (Fin n) ℝ) (hM : M.IsSymm) (hunit : IsUnit M) :
    let B : Matrix (Fin n) (Fin n) ℝ := CFC.sqrt (M*M)
    let S : Matrix (Fin n) (Fin n) ℝ := CFC.sqrt B
    let Q : Matrix (Fin n) (Fin n) ℝ := cfc (fun x : ℝ => (SignType.sign x : ℝ)) M
    B.PosSemidef ∧ S.PosSemidef ∧ Q.IsSymm ∧ B*B=M*M ∧ S*S=B ∧ S*Q*S=M ∧ Q*Q=1 ∧ IsUnit S ∧
    IsSelfAdjoint (Matrix.toEuclideanLin Q).toContinuousLinearMap ∧
    ∃ e : EuclideanSpace ℝ (Fin n) ≃L[ℝ] EuclideanSpace ℝ (Fin n),
      e.toContinuousLinearMap = (Matrix.toEuclideanLin S).toContinuousLinearMap ∧
      IsSelfAdjoint e.toContinuousLinearMap

Module navigation

Module: Analysis/Matrix/Sign.

Supporting theorems: symmetric_matrix_sign_factorization, symmetric_matrix_sqrt_real_cfc_bridge.

Previous: symmetric_jordan_decomposition · Next: exists_symmetric_isUnit_matrix_sequence.

Source excerpt, lines 349–359 · Frozen source 408915f.