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