mathlib documentation

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:

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 #

theorem linear_map.is_symmetric.orthogonal_supr_eigenspaces_eq_bot {๐•œ : 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) [finite_dimensional ๐•œ E] :
(โจ† (ฮผ : ๐•œ), module.End.eigenspace T ฮผ)แ—ฎ = โŠฅ

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

@[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} [normed_add_comm_group E] [inner_product_space ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} [finite_dimensional ๐•œ 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} [normed_add_comm_group E] [inner_product_space ๐•œ E] {T : E โ†’โ‚—[๐•œ] E} [finite_dimensional ๐•œ E] [hT : fact T.is_symmetric] (x : E) (ฮผ : module.End.eigenvalues T) :
theorem linear_map.is_symmetric.direct_sum_is_internal {๐•œ : 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] :

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) :
orthonormal_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
@[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) :

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 < ฮผ