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

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

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

Equations
  • hA.eigenvalues₀ = .eigenvalues
Instances For
    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
      noncomputable def Matrix.IsHermitian.eigenvectorBasis {𝕜 : Type u_1} [RCLike 𝕜] {n : Type u_2} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :

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

      Equations
      Instances For
        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.equiv 2 ((i : n) → (fun (x : n) => 𝕜) i)) (hA.eigenvectorBasis j)) = hA.eigenvalues j (WithLp.equiv 2 ((i : n) → (fun (x : n) => 𝕜) i)) (hA.eigenvectorBasis j)
        noncomputable def Matrix.IsHermitian.eigenvectorUnitary {𝕜 : Type u_3} [RCLike 𝕜] {n : Type u_4} [Fintype n] {A : Matrix n n 𝕜} [DecidableEq n] (hA : A.IsHermitian) :

        Unitary matrix whose columns are Matrix.IsHermitian.eigenvectorBasis.

        Equations
        Instances For
          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
          @[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 : n) (j : n) :
          hA.eigenvectorUnitary i j = (WithLp.equiv 2 ((i : n) → (fun (x : n) => 𝕜) i)) (hA.eigenvectorBasis j) i
          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.equiv 2 ((i : n) → (fun (x : n) => 𝕜) i)) (hA.eigenvectorBasis j)
          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.equiv 2 ((i : n) → (fun (x : n) => 𝕜) i)) (hA.eigenvectorBasis j)) = Pi.single j 1
          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 = Matrix.diagonal (RCLike.ofReal hA.eigenvalues)

          Unitary diagonalization of a Hermitian matrix.

          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 * Matrix.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.

          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 (Matrix.dotProduct (star ((WithLp.equiv 2 ((i : n) → (fun (x : n) => 𝕜) i)) (hA.eigenvectorBasis i))) (A.mulVec ((WithLp.equiv 2 ((i : n) → (fun (x : n) => 𝕜) i)) (hA.eigenvectorBasis i))))
          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.

          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 = (Matrix.diagonal hA.eigenvalues).rank

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

          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

          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.