Prove2Me

Free Schrödinger operator: self-adjoint, σess(H0)=[0,∞)\sigma_{ess}(H_0)=[0,\infty), Cc∞C_c^\infty is a core

Proved
TeschlQM.OneParticle.freeHamiltonian_selfAdjoint_core

by Gabewhigham · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsschrodinger-operatorsspectral-theory

Let n≥1n\ge 1 and let H0=−ΔH_0=-\Delta be the free Schrödinger operator on L2(Rn)L^2(\mathbb R^n) with domain H2(Rn)H^2(\mathbb R^n), defined via the Fourier transform as multiplication by (2π∣ξ∣)2(2\pi|\xi|)^2. Then

  1. H0H_0 is self-adjoint;
  2. its essential spectrum is σess(H0)=[0,∞)\sigma_{ess}(H_0)=[0,\infty) (since σ(H0)=[0,∞)\sigma(H_0)=[0,\infty) and H0H_0 has no eigenvalues, the discrete spectrum is empty);
  3. Cc∞(Rn)C_c^\infty(\mathbb R^n) is a core for H0H_0.

This collects the facts about H0H_0 used in the proof of Theorem 10.2.

Preamble
import Mathlib
import Definitions.Def_TeschlQM_OneParticle_multiplicationOperator
import Definitions.Def_TeschlQM_OneParticle_freeHamiltonian
import Definitions.Def_TeschlQM_Shared_resolventSet
import Definitions.Def_TeschlQM_OneParticle_essentialSpectrum
import Definitions.Def_TeschlQM_OneParticle_testFunctions
Formal statement
namespace TeschlQM.OneParticle

/-- Teschl, Theorem 7.8 and Lemma 7.9 (pp. 167–168): for `n ≥ 1` the free Schrödinger operator
`H₀` is self-adjoint, its essential spectrum is `[0, ∞)`, and `C_c^∞(ℝⁿ)` is a core for `H₀`. -/
theorem freeHamiltonian_selfAdjoint_core (n : ℕ) (hn : 1 ≤ n) :
    IsSelfAdjoint (freeHamiltonian n) ∧
      essentialSpectrum (freeHamiltonian n) = (fun t : ℝ => (t : ℂ)) '' Set.Ici 0 ∧
      (freeHamiltonian n).HasCore (testFunctions n) := by sorry

end TeschlQM.OneParticle
Source
Teschl, Mathematical Methods in Quantum Mechanics, AMS GSM 99, 2009, Theorem 7.8 (p. 168) and Lemma 7.9 (p. 168); used in the proof of Theorem 10.2, p. 222

View graph