mathlibdocumentation

analysis.inner_product_space.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:

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

Tags #

self-adjoint operator, spectral theorem, diagonalization theorem

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

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

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

The eigenvalues of a self-adjoint operator are real.

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

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

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

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

Finite-dimensional theory #

theorem inner_product_space.is_self_adjoint.orthogonal_supr_eigenspaces_eq_bot {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} [ E] :
(⨆ (μ : 𝕜), =

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

theorem inner_product_space.is_self_adjoint.orthogonal_supr_eigenspaces_eq_bot' {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} [ E] :
(⨆ (μ : , =
theorem inner_product_space.is_self_adjoint.direct_sum_submodule_is_internal {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} [ E] :

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

noncomputable def inner_product_space.is_self_adjoint.diagonalization {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} [ 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 inner_product_space.is_self_adjoint.diagonalization_symm_apply {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} [ E] (w : (λ (μ : , μ))) :
(hT.diagonalization.symm) w = ∑ (μ : , (w μ)
theorem inner_product_space.is_self_adjoint.diagonalization_apply_self_apply {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} [ 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.

noncomputable def inner_product_space.is_self_adjoint.eigenvector_basis {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} [ E] {n : } (hn : = n) :
basis (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
theorem inner_product_space.is_self_adjoint.eigenvector_basis_orthonormal {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} [ E] {n : } (hn : = n) :
noncomputable def inner_product_space.is_self_adjoint.eigenvalues {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} [ 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 inner_product_space.is_self_adjoint.has_eigenvector_eigenvector_basis {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} [ E] {n : } (hn : = n) (i : fin n) :
(hT.eigenvalues hn i) ((hT.eigenvector_basis hn) i)
@[simp]
theorem inner_product_space.is_self_adjoint.apply_eigenvector_basis {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} [ E] {n : } (hn : = n) (i : fin n) :
noncomputable def inner_product_space.is_self_adjoint.diagonalization_basis {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} [ E] {n : } (hn : = n) :
E ≃ₗᵢ[𝕜] (fin n)

An isometry from an inner product space E to Euclidean space, induced by a choice of orthonormal basis of eigenvectors for a self-adjoint operator T on E.

Equations
@[simp]
theorem inner_product_space.is_self_adjoint.diagonalization_basis_symm_apply {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} [ E] {n : } (hn : = n) (w : (fin n)) :
((hT.diagonalization_basis hn).symm) w = ∑ (i : fin n), w i (hT.eigenvector_basis hn) i
theorem inner_product_space.is_self_adjoint.diagonalization_basis_apply_self_apply {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [ E] {T : E →ₗ[𝕜] E} [ E] {n : } (hn : = n) (v : E) (i : fin n) :

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.