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.

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

The eigenvalues of a self-adjoint operator are real.

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

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

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

theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_invariant {𝕜 : Type u_1} [IsROrC 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : LinearMap.IsSymmetric T) ⦃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} [IsROrC 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : LinearMap.IsSymmetric T) (μ : 𝕜) : Module.End.eigenspace (LinearMap.restrict T (_ : ∀ ⦃v : E⦄, 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 has no eigenvalues.

Finite-dimensional theory

theorem LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot {𝕜 : Type u_1} [IsROrC 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : LinearMap.IsSymmetric T) [FiniteDimensional 𝕜 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.

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

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

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

• One or more equations did not get rendered due to their size.

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

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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

theorem LinearMap.IsSymmetric.diagonalization_apply_self_apply {𝕜 : Type u_1} [IsROrC 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : LinearMap.IsSymmetric T) [FiniteDimensional 𝕜 E] (v : E) (μ : Module.End.Eigenvalues T) : (LinearMap.IsSymmetric.diagonalization hT) (T v) μ = ↑T μ • (LinearMap.IsSymmetric.diagonalization hT) 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.eigenvectorBasis_def {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : LinearMap.IsSymmetric T) [FiniteDimensional 𝕜 E] {n : ℕ} (hn : FiniteDimensional.finrank 𝕜 E = n) : LinearMap.IsSymmetric.eigenvectorBasis hT hn = DirectSum.IsInternal.subordinateOrthonormalBasis hn (_ : DirectSum.IsInternal fun (μ : Module.End.Eigenvalues T) => Module.End.eigenspace T (↑T μ)) (_ : OrthogonalFamily 𝕜 (fun (μ : Module.End.Eigenvalues T) => ↥(Module.End.eigenspace T (↑T μ))) fun (μ : Module.End.Eigenvalues T) => Submodule.subtypeₗᵢ (Module.End.eigenspace T (↑T μ)))

@[irreducible]

noncomputable def LinearMap.IsSymmetric.eigenvectorBasis {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : LinearMap.IsSymmetric T) [FiniteDimensional 𝕜 E] {n : ℕ} (hn : FiniteDimensional.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.

TODO Postcompose with a permutation so that these eigenvectors are listed in increasing order of eigenvalue.

Equations

• @LinearMap.IsSymmetric.eigenvectorBasis = LinearMap.IsSymmetric.wrapped✝.1

theorem LinearMap.IsSymmetric.eigenvalues_def {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : LinearMap.IsSymmetric T) [FiniteDimensional 𝕜 E] {n : ℕ} (hn : FiniteDimensional.finrank 𝕜 E = n) (i : Fin n) : LinearMap.IsSymmetric.eigenvalues hT hn i = IsROrC.re (↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun (μ : Module.End.Eigenvalues T) => Module.End.eigenspace T (↑T μ)) i (_ : OrthogonalFamily 𝕜 (fun (μ : Module.End.Eigenvalues T) => ↥(Module.End.eigenspace T (↑T μ))) fun (μ : Module.End.Eigenvalues T) => Submodule.subtypeₗᵢ (Module.End.eigenspace T (↑T μ)))))

@[irreducible]

noncomputable def LinearMap.IsSymmetric.eigenvalues {𝕜 : Type u_3} [IsROrC 𝕜] {E : Type u_4} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E} (hT : LinearMap.IsSymmetric T) [FiniteDimensional 𝕜 E] {n : ℕ} (hn : FiniteDimensional.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

• @LinearMap.IsSymmetric.eigenvalues = LinearMap.IsSymmetric.wrapped✝.1

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

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

@[simp]

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

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

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

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