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.

theorem inner_product_apply_eigenvector {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {μ : 𝕜} {v : E} {T : E →ₗ[𝕜] E} (h : T v = μ • v) : 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 < μ