mathlib3 documentation

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:

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,

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} [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) (μ : 𝕜) (v : E) (hv : v (module.End.eigenspace T μ)) :

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} [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) {μ : 𝕜} (hμ : module.End.has_eigenvalue T μ) :
(star_ring_end 𝕜) μ = μ

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} [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) :
orthogonal_family 𝕜 (λ (μ : 𝕜), (module.End.eigenspace T μ)) (λ (μ : 𝕜), (module.End.eigenspace T μ).subtypeₗᵢ)

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

theorem linear_map.is_symmetric.orthogonal_supr_eigenspaces_invariant {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) ⦃v : E⦄ (hv : v ( (μ : 𝕜), module.End.eigenspace T μ)) :
T v ( (μ : 𝕜), module.End.eigenspace T μ)

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} [normed_add_comm_group E] [inner_product_space 𝕜 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 #

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

@[protected, instance]

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

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} [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [finite_dimensional 𝕜 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} [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [finite_dimensional 𝕜 E] (w : pi_Lp 2 (λ (μ : module.End.eigenvalues T), (module.End.eigenspace T μ))) :
theorem linear_map.is_symmetric.diagonalization_apply_self_apply {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [finite_dimensional 𝕜 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} [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [finite_dimensional 𝕜 E] {n : } (hn : finite_dimensional.finrank 𝕜 E = n) :

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} [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [finite_dimensional 𝕜 E] {n : } (hn : finite_dimensional.finrank 𝕜 E = 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} [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [finite_dimensional 𝕜 E] {n : } (hn : finite_dimensional.finrank 𝕜 E = n) (i : fin n) :
theorem linear_map.is_symmetric.has_eigenvalue_eigenvalues {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [finite_dimensional 𝕜 E] {n : } (hn : finite_dimensional.finrank 𝕜 E = n) (i : fin n) :
@[simp]
theorem linear_map.is_symmetric.apply_eigenvector_basis {𝕜 : Type u_1} [is_R_or_C 𝕜] [dec_𝕜 : decidable_eq 𝕜] {E : Type u_2} [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [finite_dimensional 𝕜 E] {n : } (hn : finite_dimensional.finrank 𝕜 E = 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} [normed_add_comm_group E] [inner_product_space 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.is_symmetric) [finite_dimensional 𝕜 E] {n : } (hn : finite_dimensional.finrank 𝕜 E = 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} [normed_add_comm_group E] [inner_product_space 𝕜 E] {μ : 𝕜} {v : E} {T : E →ₗ[𝕜] E} (h : v module.End.eigenspace T μ) :
theorem eigenvalue_nonneg_of_nonneg {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [normed_add_comm_group E] [inner_product_space 𝕜 E] {μ : } {T : E →ₗ[𝕜] E} (hμ : module.End.has_eigenvalue T μ) (hnn : (x : E), 0 is_R_or_C.re (has_inner.inner x (T x))) :
0 μ
theorem eigenvalue_pos_of_pos {𝕜 : Type u_1} [is_R_or_C 𝕜] {E : Type u_2} [normed_add_comm_group E] [inner_product_space 𝕜 E] {μ : } {T : E →ₗ[𝕜] E} (hμ : module.End.has_eigenvalue T μ) (hnn : (x : E), 0 < is_R_or_C.re (has_inner.inner x (T x))) :
0 < μ