# 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} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) (ฮผ : ๐) (v : E) (hv : v โ ()แฎ) :

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

theorem LinearMap.IsSymmetric.conj_eigenvalue_eq_self {๐ : Type u_1} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) {ฮผ : ๐} (hฮผ : ) :
(starRingEnd ๐) ฮผ = ฮผ

The eigenvalues of a self-adjoint operator are real.

theorem LinearMap.IsSymmetric.orthogonalFamily_eigenspaces {๐ : Type u_1} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) :
OrthogonalFamily ๐ (fun (ฮผ : ๐) => โฅ()) fun (ฮผ : ๐) =>

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

theorem LinearMap.IsSymmetric.orthogonalFamily_eigenspaces' {๐ : Type u_1} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) :
OrthogonalFamily ๐ (fun (ฮผ : ) => โฅ(Module.End.eigenspace T (โT ฮผ))) fun (ฮผ : ) => Submodule.subtypeโแตข (Module.End.eigenspace T (โT ฮผ))
theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_invariant {๐ : Type u_1} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {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} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) (ฮผ : ๐) :

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} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) [FiniteDimensional ๐ E] :
(โจ (ฮผ : ๐), )แฎ = โฅ

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} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) [FiniteDimensional ๐ E] :
(โจ (ฮผ : ), Module.End.eigenspace T (โT ฮผ))แฎ = โฅ
noncomputable instance LinearMap.IsSymmetric.directSumDecomposition {๐ : Type u_1} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {T : E โโ[๐] E} [FiniteDimensional ๐ E] [hT : ] :
DirectSum.Decomposition fun (ฮผ : ) => Module.End.eigenspace T (โT ฮผ)

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.

Equations
• LinearMap.IsSymmetric.directSumDecomposition =
theorem LinearMap.IsSymmetric.directSum_decompose_apply {๐ : Type u_1} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {T : E โโ[๐] E} [FiniteDimensional ๐ 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} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) [FiniteDimensional ๐ E] :
DirectSum.IsInternal fun (ฮผ : ) => Module.End.eigenspace T (โT ฮผ)

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} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) [FiniteDimensional ๐ E] :
E โโแตข[๐] PiLp 2 fun (ฮผ : ) => โฅ(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.

Equations
Instances For
@[simp]
theorem LinearMap.IsSymmetric.diagonalization_symm_apply {๐ : Type u_1} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) [FiniteDimensional ๐ E] (w : PiLp 2 fun (ฮผ : ) => โฅ(Module.End.eigenspace T (โT ฮผ))) :
= Finset.sum Finset.univ fun (ฮผ : ) => โ(w ฮผ)
theorem LinearMap.IsSymmetric.diagonalization_apply_self_apply {๐ : Type u_1} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) [FiniteDimensional ๐ E] (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} [RCLike ๐] {E : Type u_4} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) [FiniteDimensional ๐ E] {n : โ} (hn : = n) :
@[irreducible]
noncomputable def LinearMap.IsSymmetric.eigenvectorBasis {๐ : Type u_3} [RCLike ๐] {E : Type u_4} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) [FiniteDimensional ๐ E] {n : โ} (hn : = n) :
OrthonormalBasis (Fin n) ๐ E

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.

Equations
Instances For
theorem LinearMap.IsSymmetric.eigenvalues_def {๐ : Type u_3} [RCLike ๐] {E : Type u_4} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) [FiniteDimensional ๐ E] {n : โ} (hn : = n) (i : Fin n) :
= RCLike.re (โT ())
@[irreducible]
noncomputable def LinearMap.IsSymmetric.eigenvalues {๐ : Type u_3} [RCLike ๐] {E : Type u_4} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) [FiniteDimensional ๐ E] {n : โ} (hn : = n) (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.

Equations
Instances For
theorem LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasis {๐ : Type u_1} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) [FiniteDimensional ๐ E] {n : โ} (hn : = n) (i : Fin n) :
Module.End.HasEigenvector T (โ()) ()
theorem LinearMap.IsSymmetric.hasEigenvalue_eigenvalues {๐ : Type u_1} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) [FiniteDimensional ๐ E] {n : โ} (hn : = n) (i : Fin n) :
@[simp]
theorem LinearMap.IsSymmetric.apply_eigenvectorBasis {๐ : Type u_1} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) [FiniteDimensional ๐ E] {n : โ} (hn : = n) (i : Fin n) :
T () = โ() โข
theorem LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply {๐ : Type u_1} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {T : E โโ[๐] E} (hT : ) [FiniteDimensional ๐ E] {n : โ} (hn : = n) (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} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {ฮผ : ๐} {v : E} {T : E โโ[๐] E} (h : v โ ) :
โชv, T vโซ_๐ = ฮผ * โ ^ 2
theorem eigenvalue_nonneg_of_nonneg {๐ : Type u_1} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {ฮผ : โ} {T : E โโ[๐] E} (hฮผ : Module.End.HasEigenvalue T โฮผ) (hnn : โ (x : E), 0 โค RCLike.re โชx, T xโซ_๐) :
0 โค ฮผ
theorem eigenvalue_pos_of_pos {๐ : Type u_1} [RCLike ๐] {E : Type u_2} [InnerProductSpace ๐ E] {ฮผ : โ} {T : E โโ[๐] E} (hฮผ : Module.End.HasEigenvalue T โฮผ) (hnn : โ (x : E), 0 < RCLike.re โชx, T xโซ_๐) :
0 < ฮผ