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} [IsROrC 𝕜] [DecidableEq 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.IsHermitian A) :

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

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

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

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

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

      Instances For
        noncomputable def Matrix.IsHermitian.eigenvectorMatrix {𝕜 : Type u_1} [IsROrC 𝕜] [DecidableEq 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.IsHermitian A) :
        Matrix n n 𝕜

        A matrix whose columns are an orthonormal basis of eigenvectors of a hermitian matrix.

        Instances For
          noncomputable def Matrix.IsHermitian.eigenvectorMatrixInv {𝕜 : Type u_1} [IsROrC 𝕜] [DecidableEq 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.IsHermitian A) :
          Matrix n n 𝕜

          The inverse of eigenvectorMatrix

          Instances For

            The columns of Matrix.IsHermitian.eigenVectorMatrix form the basis

            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.det_eq_prod_eigenvalues {𝕜 : Type u_1} [IsROrC 𝕜] [DecidableEq 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.IsHermitian A) :
            Matrix.det A = Finset.prod Finset.univ fun i => ↑(Matrix.IsHermitian.eigenvalues hA i)

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

            spectral theorem (Alternate form for convenience) A hermitian matrix can be can be replaced by a diagonal matrix sandwiched between the eigenvector matrices. This alternate form allows direct rewriting of A since: $ A = V D V⁻¹$

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

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