1. Physlib
  2. QuantumMechanics
  3. Operators
  4. SpectralTheory
  5. Symmetric
Imports
/- Copyright (c) 2026 Gregory J. Loges. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Adam Bornemann, Gregory J. Loges -/ module public import Physlib.QuantumMechanics.Operators.SpectralTheory.Basic

Spectral theory for symmetric operators

i. Overview

In this module we develop the spectral theory for symmetric operators.

The numerical range of an operator, Θ T = {⟪x, T x⟫_ℂ | x ∈ T.domain ∧ ‖x‖ = 1}, is a subset of ℂ. For symmetric operators the numerical range consists only of real numbers and it is meaningful to discuss its upper/lower bounds. To facilitate this, we define LinearPMap.realNumericalRange as the projection of LinearPMap.numericalRange onto the real axis. For symmetric operators this simply reinterprets the numerical range as a subset of ℝ.

ii. Key results

    realNumericalRange (Θᵣₑ) : The projection of the numerical range onto the real axis.

    compl_ofReal_subset_regularityDomain : The regularity domain of a symmetric operator contains all complex numbers with non-zero imaginary part.

    regularityDomain_isConnected_iff : The regularity domain of a symmetric operator is connected if and only if it contains a real number.

    IsSymmetric.isEssentiallySelfAdjoint_of_defectNumber_eq_zero : The basic criterion for essential self-adjointness: symmetric + densely defined + vanishing defect numbers at ± i.

iii. Table of contents

    A. Numerical range

    B. Regularity domain

    C. Point spectrum

    D. Essential self-adjointness

iv. References

@[expose] public section

A. Numerical range

The projection of the numerical range onto the real axis.

def realNumericalRange (T : H →ₗ.[ℂ] H) : Set ℝ := re '' (Θ T)
@[inherit_doc realNumericalRange] local notation "Θᵣₑ" => realNumericalRangelemma realNumericalRange_eq (T : H →ₗ.[ℂ] H) : Θᵣₑ T = re '' Θ T := rfl@[simp] lemma realNumericalRange_neg (T : H →ₗ.[ℂ] H) : Θᵣₑ (-T) = -Θᵣₑ T := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] H⊢ Θᵣₑ (-T) = -Θᵣₑ T H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hx✝:ℝ⊢ x✝ ∈ Θᵣₑ (-T) ↔ x✝ ∈ -Θᵣₑ T All goals completed! 🐙include hT

The numerical range of a symmetric operator is contained in the real axis.

lemma im_eq_zero_of_mem_numericalRange {z : ℂ} (hz : z ∈ Θ T) : z.im = 0 := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricz:ℂhz:z ∈ Θ T⊢ z.im = 0 H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricz:ℂx:↥T.domainhx:x ∈ {x | ‖x‖ = 1}hxz:(fun x => ⟪↑x, ↑T x⟫_ℂ) x = z⊢ z.im = 0 H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricz:ℂx:↥T.domainhx:x ∈ {x | ‖x‖ = 1}hxz:⟪↑T x, ↑x⟫_ℂ = z⊢ z.im = 0 All goals completed! 🐙

The numerical range of a symmetric operator is contained in the real axis.

lemma numericalRange_subset : Θ T ⊆ range ofReal := fun z hz ↦ ⟨z.re, Complex.ext rfl (hT.im_eq_zero_of_mem_numericalRange hz).symm⟩

The numerical range of a symmetric operator is equal to its projection onto the real axis.

H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetric⊢ Θ T = ofReal ∘ re '' Θ T All goals completed! 🐙
lemma closure_numericalRange_subset : _root_.closure (Θ T) ⊆ range ofReal := (closure_mono hT.numericalRange_subset).trans Complex.isometry_ofReal.isClosedEmbedding.isClosed_range.closure_subset

B. Regularity domain

The regularity domain of a symmetric operator contains all complex numbers with non-zero imaginary part.

lemma mem_regularityDomain_of_im_ne_zero {z : ℂ} (hz : z.im ≠ 0) : z ∈ T.regularityDomain := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricz:ℂhz:z.im ≠ 0⊢ z ∈ T.regularityDomain H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricz:ℂhz:z.im ≠ 0⊢ z ∈ (_root_.closure (Θ T))ᶜ H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricz:ℂhz:z.im ≠ 0h:z ∈ _root_.closure (Θ T)⊢ z.im = 0 H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricr:ℝhz:(↑r).im ≠ 0h:↑r ∈ _root_.closure (Θ T)⊢ (↑r).im = 0 All goals completed! 🐙

The regularity domain of a symmetric operator contains all complex numbers with non-zero imaginary part.

lemma compl_ofReal_subset_regularityDomain : (range ofReal)ᶜ ⊆ T.regularityDomain := fun z hz ↦ hT.mem_regularityDomain_of_im_ne_zero fun h ↦ hz ⟨z.re, Eq.symm (Complex.ext rfl h)⟩

If m is a lower bound on the numerical range then the regularity domain contains (-∞,m).

All goals completed! 🐙 _ ≤ (s - r) * ‖x‖ ^ 2 := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝh:m ∈ lowerBounds (Θᵣₑ T)z:ℂr:ℝhr:r ∈ Iio mhrz:↑r = zx:↥T.domainhx:NeZero xs:ℝhs':↑s = ↑(‖x‖ ^ 2)⁻¹ * ⟪↑x, ↑T x⟫_ℂhs:m ≤ shsr:r < s⊢ (m - r) * ‖x‖ ^ 2 ≤ (s - r) * ‖x‖ ^ 2 All goals completed! 🐙 _ = ‖s * ‖x‖ ^ 2 - r * ‖x‖ ^ 2‖ := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝh:m ∈ lowerBounds (Θᵣₑ T)z:ℂr:ℝhr:r ∈ Iio mhrz:↑r = zx:↥T.domainhx:NeZero xs:ℝhs':↑s = ↑(‖x‖ ^ 2)⁻¹ * ⟪↑x, ↑T x⟫_ℂhs:m ≤ shsr:r < s⊢ (s - r) * ‖x‖ ^ 2 = ‖s * ‖x‖ ^ 2 - r * ‖x‖ ^ 2‖ All goals completed! 🐙 _ = ‖(s : ℂ) * ‖x‖ ^ 2 - r * ‖x‖ ^ 2‖ := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝh:m ∈ lowerBounds (Θᵣₑ T)z:ℂr:ℝhr:r ∈ Iio mhrz:↑r = zx:↥T.domainhx:NeZero xs:ℝhs':↑s = ↑(‖x‖ ^ 2)⁻¹ * ⟪↑x, ↑T x⟫_ℂhs:m ≤ shsr:r < s⊢ ‖s * ‖x‖ ^ 2 - r * ‖x‖ ^ 2‖ = ‖↑s * ↑‖x‖ ^ 2 - ↑r * ↑‖x‖ ^ 2‖ All goals completed! 🐙 _ = ‖⟪↑x, T x⟫_ℂ - r * ‖x‖ ^ 2‖ := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝh:m ∈ lowerBounds (Θᵣₑ T)z:ℂr:ℝhr:r ∈ Iio mhrz:↑r = zx:↥T.domainhx:NeZero xs:ℝhs':↑s = ↑(‖x‖ ^ 2)⁻¹ * ⟪↑x, ↑T x⟫_ℂhs:m ≤ shsr:r < s⊢ ‖↑s * ↑‖x‖ ^ 2 - ↑r * ↑‖x‖ ^ 2‖ = ‖⟪↑x, ↑T x⟫_ℂ - ↑r * ↑‖x‖ ^ 2‖ All goals completed! 🐙 _ = ‖⟪↑x, T x - z • x⟫_ℂ‖ := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝh:m ∈ lowerBounds (Θᵣₑ T)z:ℂr:ℝhr:r ∈ Iio mhrz:↑r = zx:↥T.domainhx:NeZero xs:ℝhs':↑s = ↑(‖x‖ ^ 2)⁻¹ * ⟪↑x, ↑T x⟫_ℂhs:m ≤ shsr:r < s⊢ ‖⟪↑x, ↑T x⟫_ℂ - ↑r * ↑‖x‖ ^ 2‖ = ‖⟪↑x, ↑T x - z • ↑x⟫_ℂ‖ All goals completed! 🐙 _ ≤ ‖T x - z • x‖ * ‖x‖ := mul_comm _ ‖x‖ ▸ norm_inner_le_norm _ _

If m is an upper bound on the numerical range then the regularity domain contains (m,∞).

H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝh:m ∈ upperBounds (Θᵣₑ T)z:ℂr:ℝhr:r ∈ Ioi mhrz:↑r = z⊢ -z ∈ (-T).regularityDomain H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝh:m ∈ upperBounds (Θᵣₑ T)z:ℂr:ℝhr:r ∈ Ioi mhrz:↑r = z⊢ -m ∈ lowerBounds (Θᵣₑ (-T))H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝh:m ∈ upperBounds (Θᵣₑ T)z:ℂr:ℝhr:r ∈ Ioi mhrz:↑r = z⊢ -z ∈ ofReal '' Iio (-m) H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝh:m ∈ upperBounds (Θᵣₑ T)z:ℂr:ℝhr:r ∈ Ioi mhrz:↑r = z⊢ -m ∈ lowerBounds (Θᵣₑ (-T)) exact fun _ _ ↦ H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝh:m ∈ upperBounds (Θᵣₑ T)z:ℂr:ℝhr:r ∈ Ioi mhrz:↑r = zx✝¹:ℝx✝:x✝¹ ∈ Θᵣₑ (-T)⊢ -m ≤ x✝¹ All goals completed! 🐙 H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝh:m ∈ upperBounds (Θᵣₑ T)z:ℂr:ℝhr:r ∈ Ioi mhrz:↑r = z⊢ -z ∈ ofReal '' Iio (-m) exact ⟨-r, H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝh:m ∈ upperBounds (Θᵣₑ T)z:ℂr:ℝhr:r ∈ Ioi mhrz:↑r = z⊢ -r ∈ Iio (-m) All goals completed! 🐙, H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝh:m ∈ upperBounds (Θᵣₑ T)z:ℂr:ℝhr:r ∈ Ioi mhrz:↑r = z⊢ ↑(-r) = -z All goals completed! 🐙⟩

The regularity domain of a symmetric operator is connected iff it contains a real number.

H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricr:ℝhr:↑r ∈ T.regularityDomainz₁:ℂhz₁:z₁ ∈ T.regularityDomainz₂:ℂhz₂:z₂ ∈ T.regularityDomainh:∀ z ∈ T.regularityDomain, JoinedIn T.regularityDomain z ↑r⊢ JoinedIn T.regularityDomain z₁ z₂ All goals completed! 🐙

The regularity domain of a lower semibounded symmetric operator is connected.

lemma regularityDomain_isConnected_of_bddBelow (h : BddBelow (Θᵣₑ T)) : IsConnected T.regularityDomain := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetrich:BddBelow (Θᵣₑ T)⊢ IsConnected T.regularityDomain H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝhm:m ∈ lowerBounds (Θᵣₑ T)⊢ IsConnected T.regularityDomain H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝhm:m ∈ lowerBounds (Θᵣₑ T)⊢ (ofReal ⁻¹' T.regularityDomain).Nonempty exact ⟨m - 1, hT.Iio_subset_regularityDomain hm ⟨m - 1, H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝhm:m ∈ lowerBounds (Θᵣₑ T)⊢ m - 1 ∈ Iio m ∧ ↑(m - 1) = ↑(m - 1) All goals completed! 🐙⟩⟩

The regularity domain of an upper semibounded symmetric operator is connected.

lemma regularityDomain_isConnected_of_bddAbove (h : BddAbove (Θᵣₑ T)) : IsConnected T.regularityDomain := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetrich:BddAbove (Θᵣₑ T)⊢ IsConnected T.regularityDomain H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝhm:m ∈ upperBounds (Θᵣₑ T)⊢ IsConnected T.regularityDomain H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝhm:m ∈ upperBounds (Θᵣₑ T)⊢ (ofReal ⁻¹' T.regularityDomain).Nonempty exact ⟨m + 1, hT.Ioi_subset_regularityDomain hm ⟨m + 1, H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricm:ℝhm:m ∈ upperBounds (Θᵣₑ T)⊢ m + 1 ∈ Ioi m ∧ ↑(m + 1) = ↑(m + 1) All goals completed! 🐙⟩⟩

C. Point spectrum

Eigenvalues of a symmetric unbounded operator are real.

H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricz:ℂhz:z ∈ σᵖ Tx:↥(T - z • 1).domainhx:x ∈ (T - z • 1).toFun.kerhx₀:x ≠ 0⊢ z = (↑(‖x‖ ^ 2))⁻¹ * ⟪↑x, ↑T ⟨↑x, ⋯⟩⟫_ℂ refine (eq_inv_mul_iff_mul_eq₀ (H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricz:ℂhz:z ∈ σᵖ Tx:↥(T - z • 1).domainhx:x ∈ (T - z • 1).toFun.kerhx₀:x ≠ 0⊢ ↑(‖x‖ ^ 2) ≠ 0 All goals completed! 🐙)).mpr (Eq.symm ?_) calc _ = ⟪↑x, (T - z • 1) x + z • x⟫_ℂ := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricz:ℂhz:z ∈ σᵖ Tx:↥(T - z • 1).domainhx:x ∈ (T - z • 1).toFun.kerhx₀:x ≠ 0⊢ ⟪↑x, ↑T ⟨↑x, ⋯⟩⟫_ℂ = ⟪↑x, ↑(T - z • 1) x + z • ↑x⟫_ℂ All goals completed! 🐙 _ = ⟪x, z • x⟫_ℂ := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricz:ℂhz:z ∈ σᵖ Tx:↥(T - z • 1).domainhx:x ∈ (T - z • 1).toFun.kerhx₀:x ≠ 0⊢ ⟪↑x, ↑(T - z • 1) x + z • ↑x⟫_ℂ = ⟪x, z • x⟫_ℂ All goals completed! 🐙 _ = ↑(‖x‖ ^ 2) * z := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricz:ℂhz:z ∈ σᵖ Tx:↥(T - z • 1).domainhx:x ∈ (T - z • 1).toFun.kerhx₀:x ≠ 0⊢ ⟪x, z • x⟫_ℂ = ↑(‖x‖ ^ 2) * z All goals completed! 🐙

D. Essential self-adjointness

The basic criterion for essential self-adjointness: a symmetric, densely-defined operator whose defect numbers at I and -I both vanish is essentially self-adjoint.

H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricinst✝:CompleteSpace Hhdense:T.HasDenseDomainhpos:T.defectNumber I = 0hneg:T.defectNumber (-I) = 0hrange:∀ {z : ℂ}, z.im ≠ 0 → T.defectNumber z = 0 → (T.closure - z • 1).toFun.range = ⊤hI:T.closure + I • 1 = T.closure - -I • 1⊢ (T.closure - -I • 1).toFun.range = ⊤ exact hrange (H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricinst✝:CompleteSpace Hhdense:T.HasDenseDomainhpos:T.defectNumber I = 0hneg:T.defectNumber (-I) = 0hrange:∀ {z : ℂ}, z.im ≠ 0 → T.defectNumber z = 0 → (T.closure - z • 1).toFun.range = ⊤hI:T.closure + I • 1 = T.closure - -I • 1⊢ (-I).im ≠ 0 All goals completed! 🐙) hneg H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricinst✝:CompleteSpace Hhdense:T.HasDenseDomainhpos:T.defectNumber I = 0hneg:T.defectNumber (-I) = 0hrange:∀ {z : ℂ}, z.im ≠ 0 → T.defectNumber z = 0 → (T.closure - z • 1).toFun.range = ⊤⊢ (T.closure - I • 1).toFun.range = ⊤ exact hrange (H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] HhT:T.IsSymmetricinst✝:CompleteSpace Hhdense:T.HasDenseDomainhpos:T.defectNumber I = 0hneg:T.defectNumber (-I) = 0hrange:∀ {z : ℂ}, z.im ≠ 0 → T.defectNumber z = 0 → (T.closure - z • 1).toFun.range = ⊤⊢ I.im ≠ 0 All goals completed! 🐙) hpos