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.
• LinearMap.IsSymmetric.eigenvalues gives the eigenvalues in decreasing order. This is done for several reasons: (i) This agrees with the standard convention of listing singular values in decreasing order, with the operator norm as the first singular value (ii) For positive compact operators on an infinite dimensional space, one can list the nonzero eigenvalues in decreasing (but not increasing) order since they converge to zero. (iii) This simplifies several theorem statements. For example the Schur-Horn theorem states that the diagonal of the matrix representation of a selfadjoint linear map is majorized by the eigenvalue sequence listed in decreasing order.

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 LinearMap.IsSymmetric.invariant_orthogonalComplement_eigenspace {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (μ : 𝕜) (v : E) (hv : v ∈ (Module.End.eigenspace T μ)ᗮ) : T v ∈ (Module.End.eigenspace T μ)ᗮ

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} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) {μ : 𝕜} (hμ : Module.End.HasEigenvalue T μ) : (starRingEnd 𝕜) μ = μ

The eigenvalues of a self-adjoint operator are real.

theorem LinearMap.IsSymmetric.orthogonalFamily_eigenspaces {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) : OrthogonalFamily 𝕜 (fun (μ : 𝕜) => ↥(Module.End.eigenspace T μ)) fun (μ : 𝕜) => (Module.End.eigenspace T μ).subtypeₗᵢ

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

theorem LinearMap.IsSymmetric.orthogonalFamily_eigenspaces' {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) : OrthogonalFamily 𝕜 (fun (μ : Module.End.Eigenvalues T) => ↥(Module.End.eigenspace T (↑T 1 μ))) fun (μ : Module.End.Eigenvalues T) => (Module.End.eigenspace T (↑T 1 μ)).subtypeₗᵢ

theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_invariant {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) ⦃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 LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (μ : 𝕜) : Module.End.eigenspace (T.restrict ⋯) μ = ⊥

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} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] (hT : T.IsSymmetric) : (⨆ (μ : 𝕜), 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.

theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot' {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] (hT : T.IsSymmetric) : (⨆ (μ : Module.End.Eigenvalues T), Module.End.eigenspace T (↑T 1 μ))ᗮ = ⊥

noncomputable instance LinearMap.IsSymmetric.directSumDecomposition {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] [hT : Fact T.IsSymmetric] : DirectSum.Decomposition fun (μ : Module.End.Eigenvalues T) => Module.End.eigenspace T (↑T 1 μ)

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 = ⋯.decomposition ⋯

theorem LinearMap.IsSymmetric.directSum_decompose_apply {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] [_hT : Fact T.IsSymmetric] (x : E) (μ : Module.End.Eigenvalues T) : ((DirectSum.decompose fun (μ : Module.End.Eigenvalues T) => Module.End.eigenspace T (↑T 1 μ)) x) μ = (Module.End.eigenspace T (↑T 1 μ)).orthogonalProjection x

theorem LinearMap.IsSymmetric.direct_sum_isInternal {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] (hT : T.IsSymmetric) : DirectSum.IsInternal fun (μ : Module.End.Eigenvalues T) => Module.End.eigenspace T (↑T 1 μ)

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} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] (hT : T.IsSymmetric) : E ≃ₗᵢ[𝕜] PiLp 2 fun (μ : Module.End.Eigenvalues T) => ↥(Module.End.eigenspace T (↑T 1 μ))

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

Equations

• hT.diagonalization = ⋯.isometryL2OfOrthogonalFamily ⋯

@[simp]

theorem LinearMap.IsSymmetric.diagonalization_symm_apply {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] (hT : T.IsSymmetric) (w : PiLp 2 fun (μ : Module.End.Eigenvalues T) => ↥(Module.End.eigenspace T (↑T 1 μ))) : hT.diagonalization.symm w = ∑ μ : Module.End.Eigenvalues T, ↑(w μ)

theorem LinearMap.IsSymmetric.diagonalization_apply_self_apply {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] (hT : T.IsSymmetric) (v : E) (μ : Module.End.Eigenvalues T) : hT.diagonalization (T v) μ = ↑T 1 μ • hT.diagonalization v μ

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.eigenvalues_def {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) : hT.eigenvalues hn = LinearMap.IsSymmetric.unsortedEigenvalues✝ hT hn ∘ ⇑(Tuple.sort (LinearMap.IsSymmetric.unsortedEigenvalues✝ hT hn)) ∘ ⇑Fin.revPerm

@[irreducible]

noncomputable def LinearMap.IsSymmetric.eigenvalues {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) : Fin n → ℝ

The eigenvalues for a self-adjoint operator T on a finite-dimensional inner product space E, sorted in decreasing order

Equations

• hT.eigenvalues hn = LinearMap.IsSymmetric.unsortedEigenvalues✝ hT hn ∘ ⇑(Tuple.sort (LinearMap.IsSymmetric.unsortedEigenvalues✝ hT hn)) ∘ ⇑Fin.revPerm

theorem LinearMap.IsSymmetric.eigenvectorBasis_def {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) : hT.eigenvectorBasis hn = (DirectSum.IsInternal.subordinateOrthonormalBasis hn ⋯ ⋯).reindex (Equiv.symm (Tuple.sort (LinearMap.IsSymmetric.unsortedEigenvalues✝ hT hn) * Fin.revPerm))

@[irreducible]

noncomputable def LinearMap.IsSymmetric.eigenvectorBasis {𝕜 : Type u_3} [RCLike 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = 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. Eigenvectors are sorted in decreasing order of their eigenvalues.

Equations

• hT.eigenvectorBasis hn = (DirectSum.IsInternal.subordinateOrthonormalBasis hn ⋯ ⋯).reindex (Equiv.symm (Tuple.sort (LinearMap.IsSymmetric.unsortedEigenvalues✝ hT hn) * Fin.revPerm))

theorem LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasis {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (i : Fin n) : Module.End.HasEigenvector T (↑(hT.eigenvalues hn i)) ((hT.eigenvectorBasis hn) i)

theorem LinearMap.IsSymmetric.eigenvalues_antitone {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) : Antitone (hT.eigenvalues hn)

Eigenvalues are sorted in decreasing order.

theorem LinearMap.IsSymmetric.hasEigenvalue_eigenvalues {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (i : Fin n) : Module.End.HasEigenvalue T ↑(hT.eigenvalues hn i)

@[simp]

theorem LinearMap.IsSymmetric.apply_eigenvectorBasis {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (i : Fin n) : T ((hT.eigenvectorBasis hn) i) = ↑(hT.eigenvalues hn i) • (hT.eigenvectorBasis hn) i

theorem LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (v : E) (i : Fin n) : (hT.eigenvectorBasis hn).repr (T v) i = ↑(hT.eigenvalues hn i) * (hT.eigenvectorBasis 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} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {μ : 𝕜} {v : E} {T : E →ₗ[𝕜] E} (h : v ∈ Module.End.eigenspace T μ) : inner 𝕜 v (T v) = μ * ↑‖v‖ ^ 2

theorem eigenvalue_nonneg_of_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {μ : ℝ} {T : E →ₗ[𝕜] E} (hμ : Module.End.HasEigenvalue T ↑μ) (hnn : ∀ (x : E), 0 ≤ RCLike.re (inner 𝕜 x (T x))) : 0 ≤ μ

theorem eigenvalue_pos_of_pos {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {μ : ℝ} {T : E →ₗ[𝕜] E} (hμ : Module.End.HasEigenvalue T ↑μ) (hnn : ∀ (x : E), 0 < RCLike.re (inner 𝕜 x (T x))) : 0 < μ