# Documentation

Mathlib.Analysis.InnerProductSpace.Spectrum

# Spectral theory of self-adjoint operators #

This file covers the spectral theory of self-adjoint operators on an inner product space.

The first part of the file covers general properties, true without any condition on boundedness or compactness of the operator or finite-dimensionality of the underlying space, notably:

• LinearMap.IsSymmetric.conj_eigenvalue_eq_self: the eigenvalues are real
• LinearMap.IsSymmetric.orthogonalFamily_eigenspaces: the eigenspaces are orthogonal
• LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces: the restriction of the operator to the mutual orthogonal complement of the eigenspaces has, itself, no eigenvectors

The second part of the file covers properties of self-adjoint operators in finite dimension. Letting T be a self-adjoint operator on a finite-dimensional inner product space T,

• The definition LinearMap.IsSymmetric.diagonalization provides a linear isometry equivalence E to the direct sum of the eigenspaces of T. The theorem LinearMap.IsSymmetric.diagonalization_apply_self_apply states that, when T is transferred via this equivalence to an operator on the direct sum, it acts diagonally.
• The definition LinearMap.IsSymmetric.eigenvectorBasis provides an orthonormal basis for E consisting of eigenvectors of T, with LinearMap.IsSymmetric.eigenvalues giving the corresponding list of eigenvalues, as real numbers. The definition LinearMap.IsSymmetric.eigenvectorBasis gives the associated linear isometry equivalence from E to Euclidean space, and the theorem LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply states that, when T is transferred via this equivalence to an operator on Euclidean space, it acts diagonally.

These are forms of the diagonalization theorem for self-adjoint operators on finite-dimensional inner product spaces.

## Tags #

self-adjoint operator, spectral theorem, diagonalization theorem

theorem LinearMap.IsSymmetric.invariant_orthogonalComplement_eigenspace {𝕜 : Type u_1} [] {E : Type u_2} [] {T : E →ₗ[𝕜] E} (hT : ) (μ : 𝕜) (v : E) (hv : v ()) :
T v ()

A self-adjoint operator preserves orthogonal complements of its eigenspaces.

theorem LinearMap.IsSymmetric.conj_eigenvalue_eq_self {𝕜 : Type u_1} [] {E : Type u_2} [] {T : E →ₗ[𝕜] E} (hT : ) {μ : 𝕜} (hμ : ) :
↑() μ = μ

The eigenvalues of a self-adjoint operator are real.

theorem LinearMap.IsSymmetric.orthogonalFamily_eigenspaces {𝕜 : Type u_1} [] {E : Type u_2} [] {T : E →ₗ[𝕜] E} (hT : ) :
OrthogonalFamily 𝕜 (fun μ => { x // }) fun μ =>

The eigenspaces of a self-adjoint operator are mutually orthogonal.

theorem LinearMap.IsSymmetric.orthogonalFamily_eigenspaces' {𝕜 : Type u_1} [] {E : Type u_2} [] {T : E →ₗ[𝕜] E} (hT : ) :
OrthogonalFamily 𝕜 (fun μ => { x // x Module.End.eigenspace T (T μ) }) fun μ => Submodule.subtypeₗᵢ (Module.End.eigenspace T (T μ))
theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_invariant {𝕜 : Type u_1} [] {E : Type u_2} [] {T : E →ₗ[𝕜] E} (hT : ) ⦃v : E (hv : v (⨆ (μ : 𝕜), )) :
T v (⨆ (μ : 𝕜), )

The mutual orthogonal complement of the eigenspaces of a self-adjoint operator on an inner product space is an invariant subspace of the operator.

theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces {𝕜 : Type u_1} [] {E : Type u_2} [] {T : E →ₗ[𝕜] E} (hT : ) (μ : 𝕜) :
Module.End.eigenspace (LinearMap.restrict T (_ : ∀ ⦃v : E⦄, v (⨆ (μ : 𝕜), )T v (⨆ (μ : 𝕜), ))) μ =

The mutual orthogonal complement of the eigenspaces of a self-adjoint operator on an inner product space has no eigenvalues.

### Finite-dimensional theory #

theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot {𝕜 : Type u_1} [] {E : Type u_2} [] {T : E →ₗ[𝕜] E} (hT : ) [] :
(⨆ (μ : 𝕜), ) =

The mutual orthogonal complement of the eigenspaces of a self-adjoint operator on a finite-dimensional inner product space is trivial.

theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot' {𝕜 : Type u_1} [] {E : Type u_2} [] {T : E →ₗ[𝕜] E} (hT : ) [] :
(⨆ (μ : ), Module.End.eigenspace T (T μ)) =
noncomputable instance LinearMap.IsSymmetric.directSumDecomposition {𝕜 : Type u_1} [] [dec_𝕜 : ] {E : Type u_2} [] {T : E →ₗ[𝕜] E} [] [hT : ] :

The eigenspaces of a self-adjoint operator on a finite-dimensional inner product space E gives an internal direct sum decomposition of E.

Note this takes hT as a Fact to allow it to be an instance.

theorem LinearMap.IsSymmetric.directSum_decompose_apply {𝕜 : Type u_1} [] [dec_𝕜 : ] {E : Type u_2} [] {T : E →ₗ[𝕜] E} [] [_hT : ] (x : E) (μ : ) :
↑(↑(DirectSum.decompose fun μ => Module.End.eigenspace T (T μ)) x) μ = ↑(orthogonalProjection (Module.End.eigenspace T (T μ))) x
theorem LinearMap.IsSymmetric.direct_sum_isInternal {𝕜 : Type u_1} [] [dec_𝕜 : ] {E : Type u_2} [] {T : E →ₗ[𝕜] E} (hT : ) [] :

The eigenspaces of a self-adjoint operator on a finite-dimensional inner product space E gives an internal direct sum decomposition of E.

noncomputable def LinearMap.IsSymmetric.diagonalization {𝕜 : Type u_1} [] [dec_𝕜 : ] {E : Type u_2} [] {T : E →ₗ[𝕜] E} (hT : ) [] :
E ≃ₗᵢ[𝕜] PiLp 2 fun μ => { x // x Module.End.eigenspace T (T μ) }

Isometry from an inner product space E to the direct sum of the eigenspaces of some self-adjoint operator T on E.

Instances For
@[simp]
theorem LinearMap.IsSymmetric.diagonalization_symm_apply {𝕜 : Type u_1} [] [dec_𝕜 : ] {E : Type u_2} [] {T : E →ₗ[𝕜] E} (hT : ) [] (w : PiLp 2 fun μ => { x // x Module.End.eigenspace T (T μ) }) :
= Finset.sum Finset.univ fun μ => ↑(w μ)
theorem LinearMap.IsSymmetric.diagonalization_apply_self_apply {𝕜 : Type u_1} [] [dec_𝕜 : ] {E : Type u_2} [] {T : E →ₗ[𝕜] E} (hT : ) [] (v : E) (μ : ) :
↑() (T v) μ = T μ

Diagonalization theorem, spectral theorem; version 1: A self-adjoint operator T on a finite-dimensional inner product space E acts diagonally on the decomposition of E into the direct sum of the eigenspaces of T.

theorem LinearMap.IsSymmetric.eigenvectorBasis_def {𝕜 : Type u_3} [] [dec_𝕜 : ] {E : Type u_4} [] {T : E →ₗ[𝕜] E} (hT : ) [] {n : } (hn : ) :
@[irreducible]
noncomputable def LinearMap.IsSymmetric.eigenvectorBasis {𝕜 : Type u_3} [] [dec_𝕜 : ] {E : Type u_4} [] {T : E →ₗ[𝕜] E} (hT : ) [] {n : } (hn : ) :

A choice of orthonormal basis of eigenvectors for self-adjoint operator T on a finite-dimensional inner product space E.

TODO Postcompose with a permutation so that these eigenvectors are listed in increasing order of eigenvalue.

Instances For
theorem LinearMap.IsSymmetric.eigenvalues_def {𝕜 : Type u_3} [] [dec_𝕜 : ] {E : Type u_4} [] {T : E →ₗ[𝕜] E} (hT : ) [] {n : } (hn : ) (i : Fin n) :
= IsROrC.re (T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => Module.End.eigenspace T (T μ)) i (_ : OrthogonalFamily 𝕜 (fun μ => { x // x Module.End.eigenspace T (T μ) }) fun μ => Submodule.subtypeₗᵢ (Module.End.eigenspace T (T μ)))))
@[irreducible]
noncomputable def LinearMap.IsSymmetric.eigenvalues {𝕜 : Type u_3} [] [dec_𝕜 : ] {E : Type u_4} [] {T : E →ₗ[𝕜] E} (hT : ) [] {n : } (hn : ) (i : Fin n) :

The sequence of real eigenvalues associated to the standard orthonormal basis of eigenvectors for a self-adjoint operator T on E.

TODO Postcompose with a permutation so that these eigenvalues are listed in increasing order.

Instances For
theorem LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasis {𝕜 : Type u_1} [] [dec_𝕜 : ] {E : Type u_2} [] {T : E →ₗ[𝕜] E} (hT : ) [] {n : } (hn : ) (i : Fin n) :
Module.End.HasEigenvector T (↑()) (↑() i)
theorem LinearMap.IsSymmetric.hasEigenvalue_eigenvalues {𝕜 : Type u_1} [] [dec_𝕜 : ] {E : Type u_2} [] {T : E →ₗ[𝕜] E} (hT : ) [] {n : } (hn : ) (i : Fin n) :
@[simp]
theorem LinearMap.IsSymmetric.apply_eigenvectorBasis {𝕜 : Type u_1} [] [dec_𝕜 : ] {E : Type u_2} [] {T : E →ₗ[𝕜] E} (hT : ) [] {n : } (hn : ) (i : Fin n) :
T (↑() i) = ↑() ↑() i
theorem LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply {𝕜 : Type u_1} [] [dec_𝕜 : ] {E : Type u_2} [] {T : E →ₗ[𝕜] E} (hT : ) [] {n : } (hn : ) (v : E) (i : Fin n) :
().repr (T v) i = ↑() * ().repr v i

Diagonalization theorem, spectral theorem; version 2: A self-adjoint operator T on a finite-dimensional inner product space E acts diagonally on the identification of E with Euclidean space induced by an orthonormal basis of eigenvectors of T.

@[simp]
theorem inner_product_apply_eigenvector {𝕜 : Type u_1} [] {E : Type u_2} [] {μ : 𝕜} {v : E} {T : E →ₗ[𝕜] E} (h : ) :
inner v (T v) = μ * v ^ 2
theorem eigenvalue_nonneg_of_nonneg {𝕜 : Type u_1} [] {E : Type u_2} [] {μ : } {T : E →ₗ[𝕜] E} (hμ : ) (hnn : ∀ (x : E), 0 IsROrC.re (inner x (T x))) :
0 μ
theorem eigenvalue_pos_of_pos {𝕜 : Type u_1} [] {E : Type u_2} [] {μ : } {T : E →ₗ[𝕜] E} (hμ : ) (hnn : ∀ (x : E), 0 < IsROrC.re (inner x (T x))) :
0 < μ