The free Hamiltonian in position space is −½ d²/dx², on Schwartz functions

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #128 (out of #64(i)).

FreeHamiltonian.lean built the free Hamiltonian in the position representation, freePositionOp, as the Fourier conjugate of multiplication by the symbol 2π²ξ², and proved it self-adjoint with spectrum [0, ∞). The name says −½Δ; the construction says "conjugate of a multiplier". This file makes the name honest on the Schwartz core: for every Schwartz function φ, its L² class lies in the domain of freePositionOp, and the operator sends it to the L² class of −½ φ''.

• fourier_kineticOp: the transform of the Schwartz kinetic operator kineticOp φ (SchrodingerSchwartz.lean, already identified with −½Δφ there) is the symbol times the transform of φ, pointwise 𝓕(H₀φ)(ξ) = 2π²ξ² · 𝓕φ(ξ) (fourier_kineticOp_apply);
• toLp_fourier_mem_freeSymbolOp_domain, ★ freeSymbolOp_toLp_fourier: in the momentum representation the multiplier acts on (𝓕φ).toLp exactly as the transform of H₀φ;
• toLp_mem_freePositionOp_domain: Schwartz functions lie in the position-space domain;
• ★★ freePositionOp_toLp: freePositionOp (φ.toLp) = (kineticOp φ).toLp, hence ★★★ freePositionOp_toLp_eq_laplacian: = ((−½) • Δφ).toLp, and pointwise almost everywhere ★★★ freePositionOp_toLp_ae: = −½ · φ'' (iteratedDeriv 2 φ, i.e. deriv (deriv φ), freePositionOp_toLp_ae_deriv).
• freeSymbol_eq_neg_half_mul_sq records the convention the row flagged: with Mathlib's 𝓕 f (ξ) = ∫ e^{−2πixξ} f(x) dx, the symbol 2π²ξ² is −½ (2πiξ)², which is why −½ d²/dx² has this symbol and not ½ξ².

Every step moves across the transform by Mathlib's own bridges — SchwartzMap.toLp_fourier_eq, toLp_fourierInv_eq (the L² Fourier transform agrees with the Schwartz one on Schwartz classes) and the Schwartz Fourier inversion — so nothing about L² limits is re-proved here.

Honest scope

• The Schwartz core only. The row asked for two things: (a) the Fourier–derivative identity on the whole domain 𝓕⁻¹{(1 + ξ²) f ∈ L²}, and (b) the identification of that domain with the Sobolev space H²(ℝ). This file proves (a) on Schwartz functions and does not prove that Schwartz functions are a core for freePositionOp (that its closure from the Schwartz restriction is the whole operator), nor (b): Mathlib has no H^s scale on Lp at this pin, and H² is a definition before it is a theorem. What is proved is that the self-adjoint operator of #64(i) restricts to −½ d²/dx² on every Schwartz function, which is the sense in which an analyst reads the name.
• One dimension, as in FreeHamiltonian.lean; the Laplacian form freePositionOp_toLp_eq_laplacian is the one that would survive to ℝⁿ, and the second-derivative form is its reading on ℝ (laplacian_eq_iteratedDeriv_real).
• Nothing here is a dynamics statement: PhaseGenerator.lean already has the Schrödinger equation with freePositionOp as generator; this file says what that generator is on smooth data.

References: Reed–Simon I §IX.7 (the free Hamiltonian on H²); FreeHamiltonian.lean (freeSymbolOp, freePositionOp, freePositionOp_apply), SchrodingerSchwartz.lean (kineticOp, kineticOp_eq_laplacian), PhaseGenerator.lean (hasDerivAt_fourierGroup_freePositionOp); Mathlib SchwartzMap.toLp_fourier_eq, SchwartzMap.laplacian_apply, InnerProductSpace.laplacian_eq_iteratedDeriv_real; specs/BACKLOG.md #128, #64.

The convention

theorem SchrodingerGroup.freeSymbol_eq_neg_half_mul_sq (ξ : ℝ) : ↑(freeSymbol ξ) = -(1 / 2) * (2 * ↑Real.pi * Complex.I * ↑ξ) ^ 2

The convention, as an identity. With 𝓕 carrying e^{−2πixξ}, the free symbol 2π²ξ² is −½ (2πiξ)²: the symbol of −½ d²/dx².

The transform of the kinetic operator

theorem SchrodingerGroup.fourier_kineticOp (φ : SchwartzMap ℝ ℂ) : FourierTransform.fourier (kineticOp φ) = (SchwartzMap.smulLeftCLM ℂ freeSymbol) (FourierTransform.fourier φ)

The transform of the Schwartz kinetic operator is the symbol times the transform.

theorem SchrodingerGroup.fourier_kineticOp_apply (φ : SchwartzMap ℝ ℂ) (ξ : ℝ) : (FourierTransform.fourier (kineticOp φ)) ξ = ↑(freeSymbol ξ) * (FourierTransform.fourier φ) ξ

Pointwise: 𝓕(H₀φ)(ξ) = 2π²ξ² · 𝓕φ(ξ).

The momentum representation on Schwartz classes

theorem SchrodingerGroup.toLp_fourier_mem_freeSymbolOp_domain (φ : SchwartzMap ℝ ℂ) : (FourierTransform.fourier φ).toLp 2 MeasureTheory.volume ∈ freeSymbolOp.domain

The transform of a Schwartz function lies in the domain of the momentum-space operator.

theorem SchrodingerGroup.coeFn_freeSymbolOp (f : ↥freeSymbolOp.domain) : ↑↑(↑freeSymbolOp f) =ᵐ[MeasureTheory.volume] fun (ξ : ℝ) => ↑(freeSymbol ξ) * ↑↑↑f ξ

The momentum-space operator, pointwise almost everywhere: multiplication by the symbol. Stated for a variable of the domain so that its instances at concrete elements need no unfolding.

theorem SchrodingerGroup.freeSymbolOp_eq_of_coe_eq (φ : SchwartzMap ℝ ℂ) (f : ↥freeSymbolOp.domain) (hf : ↑f = (FourierTransform.fourier φ).toLp 2 MeasureTheory.volume) : ↑freeSymbolOp f = (FourierTransform.fourier (kineticOp φ)).toLp 2 MeasureTheory.volume

★ The multiplier acts on a Schwartz transform as the transform of the kinetic operator, stated for any element of the domain whose coordinate is the transform's class.

theorem SchrodingerGroup.freeSymbolOp_toLp_fourier (φ : SchwartzMap ℝ ℂ) : ↑freeSymbolOp ⟨(FourierTransform.fourier φ).toLp 2 MeasureTheory.volume, ⋯⟩ = (FourierTransform.fourier (kineticOp φ)).toLp 2 MeasureTheory.volume

★ The same at the canonical element.

The position representation on Schwartz classes

theorem SchrodingerGroup.fourierL2_symm_toLp_fourier (ψ : SchwartzMap ℝ ℂ) : (MeasureTheory.Lp.fourierTransformₗᵢ ℝ ℂ).symm ((FourierTransform.fourier ψ).toLp 2 MeasureTheory.volume) = ψ.toLp 2 MeasureTheory.volume

The L² inverse transform of a Schwartz transform is the Schwartz class itself.

theorem SchrodingerGroup.toLp_mem_freePositionOp_domain (φ : SchwartzMap ℝ ℂ) : φ.toLp 2 MeasureTheory.volume ∈ freePositionOp.domain

Schwartz functions lie in the position-space domain of the free Hamiltonian.

theorem SchrodingerGroup.freePositionOp_toLp (φ : SchwartzMap ℝ ℂ) : ↑freePositionOp ⟨φ.toLp 2 MeasureTheory.volume, ⋯⟩ = (kineticOp φ).toLp 2 MeasureTheory.volume

★★ On a Schwartz class the position-space free Hamiltonian is the kinetic operator.

theorem SchrodingerGroup.freePositionOp_toLp_eq_laplacian (φ : SchwartzMap ℝ ℂ) : ↑freePositionOp ⟨φ.toLp 2 MeasureTheory.volume, ⋯⟩ = (-(1 / 2) • Laplacian.laplacian φ).toLp 2 MeasureTheory.volume

★★★ The free Hamiltonian in position space is −½Δ on Schwartz functions.

theorem SchrodingerGroup.freePositionOp_toLp_ae (φ : SchwartzMap ℝ ℂ) : ↑↑(↑freePositionOp ⟨φ.toLp 2 MeasureTheory.volume, ⋯⟩) =ᵐ[MeasureTheory.volume] fun (x : ℝ) => -(1 / 2) * iteratedDeriv 2 (⇑φ) x

★★★ Pointwise, almost everywhere: (H₀ φ)(x) = −½ φ''(x).

theorem SchrodingerGroup.freePositionOp_toLp_ae_deriv (φ : SchwartzMap ℝ ℂ) : ↑↑(↑freePositionOp ⟨φ.toLp 2 MeasureTheory.volume, ⋯⟩) =ᵐ[MeasureTheory.volume] fun (x : ℝ) => -(1 / 2) * deriv (deriv ⇑φ) x

The same, written with two derivatives: (H₀ φ)(x) = −½ (φ')'(x).