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

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.

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) : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)

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

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.

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

theorem Matrix.IsHermitian.eigenvectorMatrix_mul_inv {𝕜 : Type u_1} [IsROrC 𝕜] [DecidableEq 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.IsHermitian A) : Matrix.IsHermitian.eigenvectorMatrix hA * Matrix.IsHermitian.eigenvectorMatrixInv hA = 1

noncomputable instance Matrix.IsHermitian.instInvertibleMatrixInstMulMatrixToMulToNonUnitalNonAssocRingToNonAssocRingToRingToNormedRingToNormedCommRingToNormedFieldToDenselyNormedFieldToAddCommMonoidToNonUnitalNonAssocSemiringOneToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldToFieldToOneToSemiringToDivisionSemiringEigenvectorMatrixInv {𝕜 : Type u_1} [IsROrC 𝕜] [DecidableEq 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.IsHermitian A) : Invertible (Matrix.IsHermitian.eigenvectorMatrixInv hA)

noncomputable instance Matrix.IsHermitian.instInvertibleMatrixInstMulMatrixToMulToNonUnitalNonAssocRingToNonAssocRingToRingToNormedRingToNormedCommRingToNormedFieldToDenselyNormedFieldToAddCommMonoidToNonUnitalNonAssocSemiringOneToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldToFieldToOneToSemiringToDivisionSemiringEigenvectorMatrix {𝕜 : Type u_1} [IsROrC 𝕜] [DecidableEq 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.IsHermitian A) : Invertible (Matrix.IsHermitian.eigenvectorMatrix hA)

theorem Matrix.IsHermitian.eigenvectorMatrix_apply {𝕜 : Type u_1} [IsROrC 𝕜] [DecidableEq 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.IsHermitian A) (i : n) (j : n) : Matrix.IsHermitian.eigenvectorMatrix hA i j = ↑(Matrix.IsHermitian.eigenvectorBasis hA) j i

theorem Matrix.IsHermitian.transpose_eigenvectorMatrix_apply {𝕜 : Type u_1} [IsROrC 𝕜] [DecidableEq 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.IsHermitian A) (i : n) : Matrix.transpose (Matrix.IsHermitian.eigenvectorMatrix hA) i = ↑(Matrix.IsHermitian.eigenvectorBasis hA) i

The columns of Matrix.IsHermitian.eigenVectorMatrix form the basis

theorem Matrix.IsHermitian.eigenvectorMatrixInv_apply {𝕜 : Type u_1} [IsROrC 𝕜] [DecidableEq 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.IsHermitian A) (i : n) (j : n) : Matrix.IsHermitian.eigenvectorMatrixInv hA i j = star (↑(Matrix.IsHermitian.eigenvectorBasis hA) i j)

theorem Matrix.IsHermitian.conjTranspose_eigenvectorMatrixInv {𝕜 : Type u_1} [IsROrC 𝕜] [DecidableEq 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.IsHermitian A) : Matrix.conjTranspose (Matrix.IsHermitian.eigenvectorMatrixInv hA) = Matrix.IsHermitian.eigenvectorMatrix hA

theorem Matrix.IsHermitian.conjTranspose_eigenvectorMatrix {𝕜 : Type u_1} [IsROrC 𝕜] [DecidableEq 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.IsHermitian A) : Matrix.conjTranspose (Matrix.IsHermitian.eigenvectorMatrix hA) = Matrix.IsHermitian.eigenvectorMatrixInv hA

theorem Matrix.IsHermitian.spectral_theorem {𝕜 : Type u_1} [IsROrC 𝕜] [DecidableEq 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.IsHermitian A) : Matrix.IsHermitian.eigenvectorMatrixInv hA * A = Matrix.diagonal (IsROrC.ofReal ∘ Matrix.IsHermitian.eigenvalues hA) * Matrix.IsHermitian.eigenvectorMatrixInv hA

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} [IsROrC 𝕜] [DecidableEq 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.IsHermitian A) (i : n) : Matrix.IsHermitian.eigenvalues hA i = ↑IsROrC.re (Matrix.dotProduct (star (Matrix.transpose (Matrix.IsHermitian.eigenvectorMatrix hA) i)) (Matrix.mulVec A (Matrix.transpose (Matrix.IsHermitian.eigenvectorMatrix hA) i)))

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.

theorem Matrix.IsHermitian.spectral_theorem' {𝕜 : Type u_1} [IsROrC 𝕜] [DecidableEq 𝕜] {n : Type u_2} [Fintype n] [DecidableEq n] {A : Matrix n n 𝕜} (hA : Matrix.IsHermitian A) : A = Matrix.IsHermitian.eigenvectorMatrix hA * Matrix.diagonal (IsROrC.ofReal ∘ Matrix.IsHermitian.eigenvalues hA) * Matrix.IsHermitian.eigenvectorMatrixInv hA

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⁻¹$

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

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

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

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