Theorems

Cauchy interlacing

The eigenvalues of a Hermitian principal submatrix interlace those of the original matrix. The corresponding characteristic polynomials also interlace.

References

C. D. Godsil, Algebraic Combinatorics, Routledge, 2017; and S. Fisk, “A very short proof of Cauchy’s interlace theorem for eigenvalues of Hermitian matrices,” American Mathematical Monthly 112 (2005), 118. See also the Cauchy interlacing entry on symmetricfunctions.com.

Theorems

  • Eigenvalues of a principal submatrix interlace

    RealRooted.Challenges.CauchyInterlacing.principalSubmatrix_eigenvalues_interlacesource
    theorem principalSubmatrix_eigenvalues_interlace
    {𝕜 : Type*} [RCLike 𝕜] {n : ℕ}
    (A : Matrix (Fin (n + 1)) (Fin (n + 1)) 𝕜)
    (hA : A.IsHermitian) (i : Fin (n + 1)) :
    RealRooted.Interlace
      (RealRooted.sortedEigenvalues
        (A.submatrix i.succAbove i.succAbove) (hA.submatrix i.succAbove))
      (RealRooted.sortedEigenvalues A hA)

  • Characteristic polynomials of a principal submatrix interlace

    RealRooted.Challenges.CauchyInterlacing.principalSubmatrix_charpoly_interlacessource
    theorem principalSubmatrix_charpoly_interlaces {n : ℕ}
    (A : Matrix (Fin (n + 1)) (Fin (n + 1)) ℝ)
    (hA : A.IsHermitian) (i : Fin (n + 1)) :
    Interlaces (A.submatrix i.succAbove i.succAbove).charpoly A.charpoly

Lean source RealRooted/Challenges/CauchyInterlacing.lean at revision 5827550b.