Documentation

Mathlib.LinearAlgebra.Matrix.Spectrum

Spectral theory of Hermitian matrices #

This file proves the spectral theorem for matrices. The proof of the spectral theorem is based on the spectral theorem for linear maps (LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply).

Tags #

spectral theorem, diagonalization theorem

source
theorem Matrix.finite_real_spectrum {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] :
(spectrum ℝ A).Finite
source
instance Matrix.instFiniteElemRealSpectrum {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] :
Finite ↑(spectrum ℝ A)
source
theorem Matrix.spectrum_toEuclideanLin {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] :
spectrum 𝕜 (toEuclideanLin A) = spectrum 𝕜 A

The spectrum of a matrix A coincides with the spectrum of toEuclideanLin A.

source
@[deprecated Matrix.spectrum_toEuclideanLin (since := "13-08-2025")]
theorem Matrix.IsHermitian.spectrum_toEuclideanLin {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] :
spectrum 𝕜 (toEuclideanLin A) = spectrum 𝕜 A

Alias of Matrix.spectrum_toEuclideanLin.

The spectrum of a matrix A coincides with the spectrum of toEuclideanLin A.

source
noncomputable def Matrix.IsHermitian.eigenvalues₀ {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
Fin (Fintype.card n) → ℝ

The eigenvalues of a Hermitian matrix, indexed by Fin (Fintype.card n) where n is the index type of the matrix.

Equations
Instances For
    source
    theorem Matrix.IsHermitian.eigenvalues₀_antitone {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
    Antitone hA.eigenvalues₀
    source
    noncomputable def Matrix.IsHermitian.eigenvalues {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
    n → ℝ

    The eigenvalues of a Hermitian matrix, reusing the index n of the matrix entries.

    Equations
    Instances For
      source
      noncomputable def Matrix.IsHermitian.eigenvectorBasis {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
      OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)

      A choice of an orthonormal basis of eigenvectors of a Hermitian matrix.

      Equations
      Instances For
        source
        theorem Matrix.IsHermitian.mulVec_eigenvectorBasis {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (j : n) :
        A.mulVec (WithLp.ofLp (hA.eigenvectorBasis j)) = hA.eigenvalues j • WithLp.ofLp (hA.eigenvectorBasis j)
        source
        theorem Matrix.IsHermitian.eigenvalues_mem_spectrum_real {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (i : n) :
        hA.eigenvalues i ∈ spectrum ℝ A

        Eigenvalues of a Hermitian matrix A are in the ℝ spectrum of A.

        source
        noncomputable def Matrix.IsHermitian.eigenvectorUnitary {𝕜 : Type u_3} [RCLike 𝕜] {n : Type u_4} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
        ↥(unitaryGroup n 𝕜)

        Unitary matrix whose columns are Matrix.IsHermitian.eigenvectorBasis.

        Equations
        Instances For
          source
          theorem Matrix.IsHermitian.eigenvectorUnitary_coe {𝕜 : Type u_3} [RCLike 𝕜] {n : Type u_4} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
          ↑hA.eigenvectorUnitary = (EuclideanSpace.basisFun n 𝕜).toBasis.toMatrix ⇑hA.eigenvectorBasis.toBasis
          source
          @[simp]
          theorem Matrix.IsHermitian.eigenvectorUnitary_transpose_apply {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (j : n) :
          (↑hA.eigenvectorUnitary).transpose j = WithLp.ofLp (hA.eigenvectorBasis j)
          source
          @[simp]
          theorem Matrix.IsHermitian.eigenvectorUnitary_col_eq {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (j : n) :
          (↑hA.eigenvectorUnitary).col j = WithLp.ofLp (hA.eigenvectorBasis j)
          source
          @[simp]
          theorem Matrix.IsHermitian.eigenvectorUnitary_apply {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (i j : n) :
          ↑hA.eigenvectorUnitary i j = WithLp.ofLp (hA.eigenvectorBasis j) i
          source
          theorem Matrix.IsHermitian.eigenvectorUnitary_mulVec {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (j : n) :
          (↑hA.eigenvectorUnitary).mulVec (Pi.single j 1) = WithLp.ofLp (hA.eigenvectorBasis j)
          source
          theorem Matrix.IsHermitian.star_eigenvectorUnitary_mulVec {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (j : n) :
          (star ↑hA.eigenvectorUnitary).mulVec (WithLp.ofLp (hA.eigenvectorBasis j)) = Pi.single j 1
          source
          theorem Matrix.IsHermitian.star_mul_self_mul_eq_diagonal {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
          star ↑hA.eigenvectorUnitary * A * ↑hA.eigenvectorUnitary = diagonal (RCLike.ofReal ∘ hA.eigenvalues)

          Unitary diagonalization of a Hermitian matrix.

          source
          theorem Matrix.IsHermitian.spectral_theorem {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
          A = ↑hA.eigenvectorUnitary * diagonal (RCLike.ofReal ∘ hA.eigenvalues) * star ↑hA.eigenvectorUnitary

          Diagonalization theorem, spectral theorem for matrices; A Hermitian matrix can be diagonalized by a change of basis. For the spectral theorem on linear maps, see LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply.

          source
          theorem Matrix.IsHermitian.eigenvalues_eq {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (i : n) :
          hA.eigenvalues i = RCLike.re (star (WithLp.ofLp (hA.eigenvectorBasis i)) ⬝ᵥ A.mulVec (WithLp.ofLp (hA.eigenvectorBasis i)))
          source
          theorem Matrix.IsHermitian.charpoly_eq {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
          A.charpoly = ∏ i : n, (Polynomial.X - Polynomial.C ↑(hA.eigenvalues i))
          source
          theorem Matrix.IsHermitian.roots_charpoly_eq_eigenvalues {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
          A.charpoly.roots = Multiset.map (RCLike.ofReal ∘ hA.eigenvalues) Finset.univ.val
          source
          theorem Matrix.IsHermitian.roots_charpoly_eq_eigenvalues₀ {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
          A.charpoly.roots = Multiset.map (RCLike.ofReal ∘ hA.eigenvalues₀) Finset.univ.val
          source
          theorem Matrix.IsHermitian.sort_roots_charpoly_eq_eigenvalues₀ {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
          Multiset.sort (fun (x1 x2 : ℝ) => x1 ≥ x2) (Multiset.map (⇑RCLike.re) A.charpoly.roots) = List.ofFn hA.eigenvalues₀
          source
          theorem Matrix.IsHermitian.eigenvalues_eq_eigenvalues_iff {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A B : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) (hB : B.IsHermitian) :
          hA.eigenvalues = hB.eigenvalues ↔ A.charpoly = B.charpoly
          source
          theorem Matrix.IsHermitian.splits_charpoly {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
          Polynomial.Splits (RingHom.id 𝕜) A.charpoly
          source
          theorem Matrix.IsHermitian.det_eq_prod_eigenvalues {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
          A.det = ∏ i : n, ↑(hA.eigenvalues i)

          The determinant of a Hermitian matrix is the product of its eigenvalues.

          source
          theorem Matrix.IsHermitian.rank_eq_rank_diagonal {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
          A.rank = (diagonal hA.eigenvalues).rank

          rank of a Hermitian matrix is the rank of after diagonalization by the eigenvector unitary

          source
          theorem Matrix.IsHermitian.rank_eq_card_non_zero_eigs {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
          A.rank = Fintype.card { i : n // hA.eigenvalues i ≠ 0 }

          rank of a Hermitian matrix is the number of nonzero eigenvalues of the Hermitian matrix

          source
          theorem Matrix.IsHermitian.spectrum_eq_image_range {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
          spectrum 𝕜 A = RCLike.ofReal '' Set.range hA.eigenvalues

          The spectrum of a Hermitian matrix is the range of its eigenvalues under RCLike.ofReal.

          source
          theorem Matrix.IsHermitian.spectrum_real_eq_range_eigenvalues {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
          spectrum ℝ A = Set.range hA.eigenvalues

          The ℝ-spectrum of a Hermitian matrix over RCLike field is the range of the eigenvalue function.

          source
          @[deprecated Matrix.IsHermitian.spectrum_real_eq_range_eigenvalues (since := "2025-08-14")]
          theorem Matrix.IsHermitian.eigenvalues_eq_spectrum_real {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
          spectrum ℝ A = Set.range hA.eigenvalues

          Alias of Matrix.IsHermitian.spectrum_real_eq_range_eigenvalues.

          The ℝ-spectrum of a Hermitian matrix over RCLike field is the range of the eigenvalue function.

          source
          theorem Matrix.IsHermitian.eigenvalues_eq_zero_iff {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
          hA.eigenvalues = 0 ↔ A = 0

          The eigenvalues of a Hermitian matrix A are all zero iff A = 0.

          source
          theorem Matrix.IsHermitian.exists_eigenvector_of_ne_zero {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} (hA : A.IsHermitian) (h_ne : A ≠ 0) :
          ∃ (v : n → 𝕜) (t : ℝ), t ≠ 0 ∧ v ≠ 0 ∧ A.mulVec v = t • v

          A nonzero Hermitian matrix has an eigenvector with nonzero eigenvalue.

          source
          theorem Matrix.IsHermitian.trace_eq_sum_eigenvalues {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :
          A.trace = ∑ i : n, ↑(hA.eigenvalues i)