Simultaneous diagonalization by congruence

TheoremPositive-definite matrices are congruent to the identity#✓fully proved

Let \(P\) be a real square matrix with rows and columns indexed by a finite set, and suppose \(P\) is positive definite: \(P\) is symmetric and \(x^{\mathsf{T}} P x > 0\) for every nonzero real vector \(x\). Then there is an invertible real matrix \(Q\) of the same size such that \(Q^{\mathsf{T}} P Q = I\), where \(I\) is the identity matrix.

theorem _root_.Matrix.PosDef.exists_isUnit_transpose_mul_mul_eq_one
    {P : Matrix n n ℝ} (hP : P.PosDef) :
    ∃ Q : Matrix n n ℝ, IsUnit Q ∧ Matrix.transpose Q * P * Q = 1

Used by 1

Used bySimultaneous diagonalization by congruence

TheoremSimultaneous diagonalization by congruence#✓fully proved

Let \(S\) and \(P\) be real square matrices with rows and columns indexed by a finite set \(n\), where \(S\) is symmetric and \(P\) is positive definite. Then there is an invertible real matrix \(C\), indexed by \(n\), such that \(C^{\mathsf T} S C\) is diagonal and \(C^{\mathsf T} P C\) is the identity matrix.

Proof: Normalize \(P\) to the identity by a congruence built from its orthonormal eigenbasis, scaled by the inverse square roots of its eigenvalues, then orthogonally diagonalize the transformed symmetric matrix. This is the argument of Wikipedia's "Definite matrix", section "Simultaneous diagonalization", with the eigenbasis scaling in place of a Cholesky factor.

theorem simultaneous_diagonalization_posDef
    (S P : Matrix n n ℝ) (hS : S.IsSymm) (hP : P.PosDef) :
    ∃ C : Matrix n n ℝ,
      IsUnit C ∧ (Matrix.transpose C * S * C).IsDiag ∧ Matrix.transpose C * P * C = 1

Sources

• R. A. Horn and C. R. Johnson, Matrix Analysis, 2nd ed., Cambridge University Press (2013), Theorem 4.5.15.

Uses 1

Proof usesPositive-definite matrices are congruent to the identity

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.