The free Hamiltonian as a self-adjoint operator, and its spectrum

Category: 1-Mathlib (CSD-free; staged for upstream).

Everything the corpus proves about continuum dynamics is proved with bounded objects: the unitary group U₀(t) = 𝓕⁻¹ e^{−2π²itξ²} 𝓕 (SchrodingerGroup.lean), the Fourier multiplier, the kernel. The Hamiltonian itself is unbounded and was never written as an operator. This module writes it, in the momentum representation, on top of ../InnerProductSpace/MultiplicationOperator.lean:

• freeSymbolOp — the free Hamiltonian in the momentum representation: multiplication by the corpus's own freeSymbol, m(ξ) = 2π²ξ², on L²(ℝ) with its natural domain, dense (dense_domain_freeSymbolOp);
• ★★★ isSelfAdjoint_freeSymbolOp — it is self-adjoint: the first unbounded self-adjoint operator of the continuum in this corpus (the circle's twisted Laplacian, ../Fourier/CircleSobolev.lean, is the discrete-spectrum case);
• ★★★ spectrum_freeSymbolOp — its spectrum is the nonnegative real axis, both inclusions: ⊆ because the symbol's values are the nonnegative reals and the resolvent exists off their closure (★ range_freeSymbol, isClosed_nonnegAxis), and ⊇ because every ball around a nonnegative real has preimage of positive measure (it is a nonempty open set) and finite measure (it is bounded, preimage_ball_subset_Icc), so ★★ mem_spectrum_freeSymbolOp applies. The spectrum is purely continuous in the sense that matters here: it is an uncountable set reached by approximate eigenvectors, not by eigenvectors — no eigenvalue is claimed anywhere;
• coeFn_phaseGroup_freeSymbol — the group and the generator are built from one function: in the momentum representation U₀(t) is multiplication by e^{−itm} for the same m.

Honest scope

⚠️ The momentum representation. freeSymbolOp is −½Δ conjugated by the Fourier transform. The position-space operator is its Fourier conjugate, and conjugating a LinearPMap by a unitary is not built here, so "−½Δ is self-adjoint with spectrum [0, ∞)" is not stated in position space. The Fourier transform is a unitary of L²(ℝ) (SchrodingerGroup.fourierL2), so the two operators are unitarily equivalent in the ordinary mathematical sense; that equivalence is what is missing in Lean (MATHLIB-ABSENT(LinearPMap.conjIsometry)).

⚠️ No H₀ + V. Adding a bounded real potential needs two things this module does not have: the conjugation above (in momentum space a potential is a convolution, not a multiplier) and the lemma that a bounded symmetric perturbation of a self-adjoint LinearPMap is self-adjoint on the same domain. Both are recorded in specs/BACKLOG.md #64 as what the interacting Wigner equation still waits on.

⚠️ No Stone's theorem, so U₀(t) = e^{−itH₀} is not an identity here: the two objects are built from the same symbol, which is all coeFn_phaseGroup_freeSymbol says. One dimension.

References: M. Reed, B. Simon, Methods of Modern Mathematical Physics I §VIII.3, II §IX.7; MultiplicationOperator.lean, SchrodingerGroup.lean, CircleSobolev.lean; specs/BACKLOG.md #64, #93; specs/future-work.md.

The range of the free symbol

theorem SchrodingerGroup.freeSymbol_real (ξ : ℝ) : freeSymbol ξ = 2 * Real.pi ^ 2 * ξ ^ 2

theorem SchrodingerGroup.freeSymbol_nonneg (ξ : ℝ) : 0 ≤ freeSymbol ξ

theorem SchrodingerGroup.continuous_freeSymbol : Continuous freeSymbol

theorem SchrodingerGroup.freeSymbol_sqrt {r : ℝ} (hr : 0 ≤ r) : freeSymbol √(r / (2 * Real.pi ^ 2)) = r

Every nonnegative real is a value of the free symbol: 2π²ξ² = r at ξ = √(r/2π²).

theorem SchrodingerGroup.range_freeSymbol : Set.range freeSymbol = Set.Ici 0

★ The free symbol's range is [0, ∞).

The nonnegative real axis in ℂ

def SchrodingerGroup.nonnegAxis : Set ℂ

The nonnegative real axis, as the set the spectrum will turn out to be.

Equations

• SchrodingerGroup.nonnegAxis = {z : ℂ | z.im = 0 ∧ 0 ≤ z.re}

theorem SchrodingerGroup.ofReal_image_Ici : (fun (r : ℝ) => ↑r) '' Set.Ici 0 = nonnegAxis

theorem SchrodingerGroup.isClosed_nonnegAxis : IsClosed nonnegAxis

theorem SchrodingerGroup.range_ofReal_freeSymbol : (Set.range fun (ξ : ℝ) => ↑(freeSymbol ξ)) = nonnegAxis

The free Hamiltonian in the momentum representation

noncomputable def SchrodingerGroup.freeSymbolOp : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →ₗ.[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The free Hamiltonian in the momentum representation: multiplication by the free symbol 2π²ξ² on L²(ℝ), on its natural domain {f : (1 + ξ²) f ∈ L²}.

Equations

• SchrodingerGroup.freeSymbolOp = MeasureTheory.L2.mulOp SchrodingerGroup.freeSymbol

theorem SchrodingerGroup.dense_domain_freeSymbolOp : Dense ↑freeSymbolOp.domain

theorem SchrodingerGroup.isSelfAdjoint_freeSymbolOp : IsSelfAdjoint freeSymbolOp

★★★ The free Hamiltonian is self-adjoint on its natural domain: the first unbounded self-adjoint operator of the continuum in this corpus.

Its spectrum is the nonnegative real axis

theorem SchrodingerGroup.spectrum_freeSymbolOp_subset : freeSymbolOp.spectrum ⊆ nonnegAxis

theorem SchrodingerGroup.isOpen_preimage_ball (lam ε : ℝ) : IsOpen (freeSymbol ⁻¹' Metric.ball lam ε)

theorem SchrodingerGroup.preimage_ball_subset_Icc (lam ε : ℝ) : freeSymbol ⁻¹' Metric.ball lam ε ⊆ Set.Icc (-√((|lam| + ε) / (2 * Real.pi ^ 2))) √((|lam| + ε) / (2 * Real.pi ^ 2))

theorem SchrodingerGroup.mem_spectrum_freeSymbolOp {r : ℝ} (hr : 0 ≤ r) : ↑r ∈ freeSymbolOp.spectrum

★★ Every nonnegative real is in the spectrum: the preimage of each ball around it is a nonempty open set, hence of positive measure, and bounded, hence of finite measure — so the essential-value criterion applies.

theorem SchrodingerGroup.spectrum_freeSymbolOp : freeSymbolOp.spectrum = nonnegAxis

★★★ The spectrum of the free Hamiltonian is the nonnegative real axis [0, ∞): the continuum spectrum of −½Δ, with no eigenvalues anywhere in it.

The link with the propagator

theorem SchrodingerGroup.coeFn_phaseGroup_freeSymbol (t : ℝ) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↑↑((phaseGroup ⋯ t) f) =ᵐ[MeasureTheory.volume] fun (ξ : ℝ) => Complex.exp (↑(-(t * freeSymbol ξ)) * Complex.I) * ↑↑f ξ

The free group, in the momentum representation, is multiplication by e^{−it m} for the same symbol m whose multiplication operator is the free Hamiltonian: the group and the generator are built from one function. Turning this into U₀(t) = e^{−itH₀} as operators is Stone's theorem, which the pin does not have.

The position representation

#64(i)'s point: with LinearPMap.conjIsometry the momentum-space operator moves across the Fourier transform, which is a unitary of L²(ℝ) at this pin (MeasureTheory.Lp.fourierTransformₗᵢ). What comes out is the free Hamiltonian in the position representation — self-adjoint, with the same spectrum, and defined on the image of the momentum domain.

noncomputable def SchrodingerGroup.freePositionOp : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →ₗ.[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The free Hamiltonian in the position representation: the momentum-space multiplication operator conjugated by the Fourier transform.

Equations

• SchrodingerGroup.freePositionOp = LinearPMap.conjIsometry (MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ).symm SchrodingerGroup.freeSymbolOp

theorem SchrodingerGroup.freePositionOp_domain : freePositionOp.domain = Submodule.map (↑(MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ).symm.toLinearEquiv) freeSymbolOp.domain

theorem SchrodingerGroup.freePositionOp_apply (f : ↥freeSymbolOp.domain) : ↑freePositionOp ⟨(MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ).symm ↑f, ⋯⟩ = (MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ).symm (↑freeSymbolOp f)

★★ The two representations are unitarily equivalent by construction: applying the position operator to the inverse transform of a momentum-domain state is the inverse transform of the momentum operator's value. This is the statement that makes the name honest.

theorem SchrodingerGroup.isSelfAdjoint_freePositionOp : IsSelfAdjoint freePositionOp

★★★ The free Hamiltonian is self-adjoint in the position representation too. Self-adjointness is a property of the operator, not of the representation, and this is that sentence as a theorem.

theorem SchrodingerGroup.dense_domain_freePositionOp : Dense ↑freePositionOp.domain

The position-space domain is dense, which it has to be for the operator to be self-adjoint.

theorem SchrodingerGroup.spectrum_freePositionOp : freePositionOp.spectrum = nonnegAxis

★★★ The spectrum is the same nonnegative real axis. The spectrum is representation- independent, so the continuum spectrum of the free Hamiltonian is [0, ∞) in position space as well — and the proof is the conjugation lemma, not a second computation.

The Schrödinger operator with a bounded potential

#64(ii)'s payoff, and the reason (i) and (ii) belong together: the free Hamiltonian lives in the momentum representation, a potential multiplies in the position representation, so H₀ + V is only a statement once both are in the same place. (i) moved H₀ across the Fourier transform and (ii) adds the potential there.

noncomputable def SchrodingerGroup.schrodingerOp (V : ℝ → ℝ) (hV : MeasureTheory.AEStronglyMeasurable (fun (x : ℝ) => ↑(V x)) MeasureTheory.volume) {C : ℝ} (hb : ∀ᵐ (x : ℝ), ‖↑(V x)‖ ≤ C) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →ₗ.[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The Schrödinger operator H₀ + V for a bounded real potential, in the position representation, on the same domain as the free Hamiltonian.

Equations

• SchrodingerGroup.schrodingerOp V hV hb = SchrodingerGroup.freePositionOp.addCLM (MeasureTheory.L2.mulCLM (fun (x : ℝ) => ↑(V x)) hV hb)

theorem SchrodingerGroup.schrodingerOp_domain (V : ℝ → ℝ) (hV : MeasureTheory.AEStronglyMeasurable (fun (x : ℝ) => ↑(V x)) MeasureTheory.volume) {C : ℝ} (hb : ∀ᵐ (x : ℝ), ‖↑(V x)‖ ≤ C) : (schrodingerOp V hV hb).domain = freePositionOp.domain

theorem SchrodingerGroup.isSelfAdjoint_schrodingerOp (V : ℝ → ℝ) (hV : MeasureTheory.AEStronglyMeasurable (fun (x : ℝ) => ↑(V x)) MeasureTheory.volume) {C : ℝ} (hb : ∀ᵐ (x : ℝ), ‖↑(V x)‖ ≤ C) : IsSelfAdjoint (schrodingerOp V hV hb)

★★★ The Schrödinger operator is self-adjoint for every bounded real potential, on the free Hamiltonian's own domain. This is what #64's interacting half needed from (i) and (ii) together: the generator of the interacting dynamics exists as a self-adjoint operator, and what is still missing is Stone's theorem to turn it into the unitary group the equation differentiates.

theorem SchrodingerGroup.dense_domain_schrodingerOp (V : ℝ → ℝ) (hV : MeasureTheory.AEStronglyMeasurable (fun (x : ℝ) => ↑(V x)) MeasureTheory.volume) {C : ℝ} (hb : ∀ᵐ (x : ℝ), ‖↑(V x)‖ ≤ C) : Dense ↑(schrodingerOp V hV hb).domain

The domain is dense, as it must be.