# mathlib3documentation

analysis.inner_product_space.spectrum

# Spectral theory of self-adjoint operators #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

• is_self_adjoint.conj_eigenvalue_eq_self: the eigenvalues are real
• is_self_adjoint.orthogonal_family_eigenspaces: the eigenspaces are orthogonal
• is_self_adjoint.orthogonal_supr_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 is_self_adjoint.diagonalization provides a linear isometry equivalence E to the direct sum of the eigenspaces of T. The theorem is_self_adjoint.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 is_self_adjoint.eigenvector_basis provides an orthonormal basis for E consisting of eigenvectors of T, with is_self_adjoint.eigenvalues giving the corresponding list of eigenvalues, as real numbers. The definition is_self_adjoint.diagonalization_basis gives the associated linear isometry equivalence from E to Euclidean space, and the theorem is_self_adjoint.diagonalization_basis_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.

## TODO #

Spectral theory for compact self-adjoint operators, bounded self-adjoint operators.

## Tags #

self-adjoint operator, spectral theorem, diagonalization theorem

theorem linear_map.is_symmetric.invariant_orthogonal_eigenspace {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) (μ : 𝕜) (v : E) (hv : v ) :

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

theorem linear_map.is_symmetric.conj_eigenvalue_eq_self {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) {μ : 𝕜} (hμ : μ) :
μ = μ

The eigenvalues of a self-adjoint operator are real.

theorem linear_map.is_symmetric.orthogonal_family_eigenspaces {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) :
(λ (μ : 𝕜), μ)) (λ (μ : 𝕜), .subtypeₗᵢ)

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

theorem linear_map.is_symmetric.orthogonal_family_eigenspaces' {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) :
(λ (μ : , μ)) (λ (μ : , .subtypeₗᵢ)
theorem linear_map.is_symmetric.orthogonal_supr_eigenspaces_invariant {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) ⦃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 linear_map.is_symmetric.orthogonal_supr_eigenspaces {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) (μ : 𝕜) :
μ =

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

### Finite-dimensional theory #

theorem linear_map.is_symmetric.orthogonal_supr_eigenspaces_eq_bot {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [ E] :
( (μ : 𝕜), =

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

theorem linear_map.is_symmetric.orthogonal_supr_eigenspaces_eq_bot' {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [ E] :
( (μ : , =
@[protected, instance]
noncomputable def linear_map.is_symmetric.direct_sum_decomposition {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} [ E] [hT : fact T.is_symmetric] :

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
theorem linear_map.is_symmetric.direct_sum_decompose_apply {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} [ E] [hT : fact T.is_symmetric] (x : E) (μ : module.End.eigenvalues T) :
((direct_sum.decompose (λ (μ : , x) μ =
theorem linear_map.is_symmetric.direct_sum_is_internal {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [ E] :

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 linear_map.is_symmetric.diagonalization {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [ E] :
E ≃ₗᵢ[𝕜] (λ (μ : , μ))

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

Equations
@[simp]
theorem linear_map.is_symmetric.diagonalization_symm_apply {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [ E] (w : (λ (μ : , μ))) :
(hT.diagonalization.symm) w = finset.univ.sum (λ (μ : , (w μ))
theorem linear_map.is_symmetric.diagonalization_apply_self_apply {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [ E] (v : E) (μ : module.End.eigenvalues 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.

@[irreducible]
noncomputable def linear_map.is_symmetric.eigenvector_basis {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [ E] {n : } (hn : = 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
@[irreducible]
noncomputable def linear_map.is_symmetric.eigenvalues {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [ 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
theorem linear_map.is_symmetric.has_eigenvector_eigenvector_basis {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [ E] {n : } (hn : = n) (i : fin n) :
(hT.eigenvalues hn i) ((hT.eigenvector_basis hn) i)
theorem linear_map.is_symmetric.has_eigenvalue_eigenvalues {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [ E] {n : } (hn : = n) (i : fin n) :
(hT.eigenvalues hn i)
@[simp]
theorem linear_map.is_symmetric.apply_eigenvector_basis {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [ E] {n : } (hn : = n) (i : fin n) :
theorem linear_map.is_symmetric.diagonalization_basis_apply_self_apply {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [ E] {n : } (hn : = n) (v : E) (i : fin n) :
((hT.eigenvector_basis hn).repr) (T v) i = (hT.eigenvalues hn i) * ((hT.eigenvector_basis hn).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} [is_R_or_C 𝕜] {E : Type u_2} [ E] {μ : 𝕜} {v : E} {T : E →ₗ[𝕜] E} (h : v ) :
(T v) = μ * v ^ 2
theorem eigenvalue_nonneg_of_nonneg {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] {μ : } {T : E →ₗ[𝕜] E} (hμ : μ) (hnn : (x : E), 0 is_R_or_C.re (T x))) :
0 μ
theorem eigenvalue_pos_of_pos {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] {μ : } {T : E →ₗ[𝕜] E} (hμ : μ) (hnn : (x : E), 0 < is_R_or_C.re (T x))) :
0 < μ