The free Schrödinger group on Schwartz functions, and the Schrödinger equation

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

Analysis/Semigroup/SchrodingerGroup.lean defines the unitary group U_κ(t) = 𝓕⁻¹ e^{−itκ} 𝓕 on L²(E) and never writes a generator. This module (BACKLOG #43, FC-5″) writes it, on Schwartz functions, where Mathlib's Fourier calculus is available:

• the phase e^{−itκ} of a symbol of temperate growth has temperate growth (hasTemperateGrowth_phaseFun; s ↦ e^{is} has all its derivatives unimodular), so the multiplier is Mathlib's SchwartzMap.fourierMultiplierCLM and U_κ(t) preserves Schwartz space: ★ fourierGroup_toLp, U_κ(t) (f.toLp 2) = (𝓕⁻¹ (e^{−itκ} · 𝓕 f)).toLp 2;
• the kinetic energy operator kineticOp = fourierMultiplierCLM (2π²ξ²) is −½ Δ (★ kineticOp_eq_laplacian, from Mathlib's laplacian_eq_fourierMultiplierCLM) — the identification of freeSchrodinger with the differential operator −½ d²/dx²;
• ★★ hasDerivAt_freeSchrodinger — the free Schrödinger equation i ∂_t ψ = −½ Δ ψ holds in L² for ψ(t) = e^{−itH₀} f, f Schwartz: ∂_t (U₀(t) f) = −i H₀ (U₀(t) f) at every t. The derivative at 0 is a dominated convergence for the difference quotient of the phase (|(e^{−itκ} − 1)/t| ≤ |κ|), lifted through the Fourier isometry; the group law moves it to every t. hasDerivAt_fourierGroup_toLp is the same for any dispersion relation κ of temperate growth: ∂_t U_κ(t) f = −i κ(D) (U_κ(t) f).

Honest scope

⚠️ The derivative is taken in L² (the strong derivative of the orbit), for Schwartz initial data; the statement in the Schwartz topology is not made. The action on a Gaussian packet — the packet spreading into a Gaussian of complex variance — is Analysis/Semigroup/GaussianPacket.lean (FC-5‴, BACKLOG #48). The space E is any finite-dimensional real inner product space (H₀ = −½ Δ on ℝᵈ).

References: M. Reed, B. Simon, Methods of Modern Mathematical Physics II §IX.7; Analysis/Semigroup/SchrodingerGroup.lean (FC-5); specs/feynman-continuum-scoping.md §5; specs/BACKLOG.md #43; specs/future-work.md FP-1.

Temperate growth of a real phase

theorem SchrodingerGroup.hasDerivAt_exp_mul_I (s : ℝ) : HasDerivAt (fun (s : ℝ) => Complex.exp (↑s * Complex.I)) (Complex.exp (↑s * Complex.I) * Complex.I) s

theorem SchrodingerGroup.iteratedDeriv_exp_mul_I (n : ℕ) : (iteratedDeriv n fun (s : ℝ) => Complex.exp (↑s * Complex.I)) = fun (s : ℝ) => Complex.I ^ n * Complex.exp (↑s * Complex.I)

theorem SchrodingerGroup.hasTemperateGrowth_exp_mul_I : Function.HasTemperateGrowth fun (s : ℝ) => Complex.exp (↑s * Complex.I)

s ↦ e^{is} has temperate growth: all its derivatives are unimodular.

theorem SchrodingerGroup.hasTemperateGrowth_phaseFun {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {κ : E → ℝ} (hκ : Function.HasTemperateGrowth κ) (t : ℝ) : Function.HasTemperateGrowth (phaseFun κ t)

★ The phase e^{−itκ} of a symbol of temperate growth has temperate growth.

theorem SchrodingerGroup.hasTemperateGrowth_freeSymbol {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : Function.HasTemperateGrowth freeSymbol

The group on Schwartz space

noncomputable def SchrodingerGroup.fourierGroupS {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (κ : E → ℝ) (t : ℝ) : SchwartzMap E ℂ →L[ℂ] SchwartzMap E ℂ

The unitary group U_κ on Schwartz space: Mathlib's Fourier multiplier with symbol e^{−itκ}.

Equations

• SchrodingerGroup.fourierGroupS κ t = SchwartzMap.fourierMultiplierCLM ℂ (SchrodingerGroup.phaseFun κ t)

noncomputable def SchrodingerGroup.freeSchrodingerS {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (t : ℝ) : SchwartzMap E ℂ →L[ℂ] SchwartzMap E ℂ

The free Schrödinger group on Schwartz space.

Equations

• SchrodingerGroup.freeSchrodingerS t = SchrodingerGroup.fourierGroupS SchrodingerGroup.freeSymbol t

theorem SchrodingerGroup.phaseGroup_toLp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {κ : E → ℝ} (hκm : Measurable κ) (hκ : Function.HasTemperateGrowth κ) (t : ℝ) (ψ : SchwartzMap E ℂ) : (phaseGroup hκm t) (ψ.toLp 2 MeasureTheory.volume) = ((SchwartzMap.smulLeftCLM ℂ (phaseFun κ t)) ψ).toLp 2 MeasureTheory.volume

On Schwartz functions the L² phase group is multiplication by the phase.

theorem SchrodingerGroup.fourierGroup_toLp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {κ : E → ℝ} (hκm : Measurable κ) (hκ : Function.HasTemperateGrowth κ) (t : ℝ) (f : SchwartzMap E ℂ) : (fourierGroup hκm t) (f.toLp 2 MeasureTheory.volume) = ((fourierGroupS κ t) f).toLp 2 MeasureTheory.volume

★ The unitary group preserves Schwartz space: U_κ(t) (f.toLp 2) = (𝓕⁻¹ (e^{−itκ} · 𝓕 f)).toLp 2.

theorem SchrodingerGroup.freeSchrodinger_toLp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (t : ℝ) (f : SchwartzMap E ℂ) : (freeSchrodinger t) (f.toLp 2 MeasureTheory.volume) = ((freeSchrodingerS t) f).toLp 2 MeasureTheory.volume

The generator

noncomputable def SchrodingerGroup.kineticOp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] : SchwartzMap E ℂ →L[ℝ] SchwartzMap E ℂ

The kinetic energy operator H₀ = −½ d²/dx² on Schwartz functions, as the Fourier multiplier of the free symbol 2π²ξ².

Equations

• SchrodingerGroup.kineticOp = SchwartzMap.fourierMultiplierCLM ℂ SchrodingerGroup.freeSymbol

theorem SchrodingerGroup.kineticOp_eq_laplacian {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : SchwartzMap E ℂ) : kineticOp f = -(1 / 2) • Laplacian.laplacian f

★ H₀ = −½ Δ on Schwartz functions, from Mathlib's laplacian_eq_fourierMultiplierCLM.

The Schrödinger equation

theorem SchrodingerGroup.norm_phaseQuot_le {E : Type u_1} {κ : E → ℝ} (t : ℝ) (x : E) : ‖↑t⁻¹ * (phaseFun κ t x - 1) + Complex.I * ↑(κ x)‖ ≤ 2 * |κ x|

The difference quotient of the phase is bounded by 2|κ|.

theorem SchrodingerGroup.tendsto_phaseQuot {E : Type u_1} {κ : E → ℝ} (x : E) : Filter.Tendsto (fun (t : ℝ) => ↑t⁻¹ * (phaseFun κ t x - 1) + Complex.I * ↑(κ x)) (nhdsWithin 0 {0}ᶜ) (nhds 0)

The difference quotient of the phase tends to −iκ.

theorem SchrodingerGroup.hasDerivAt_phaseGroup_toLp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {κ : E → ℝ} (hκm : Measurable κ) (hκ : Function.HasTemperateGrowth κ) (ψ : SchwartzMap E ℂ) : HasDerivAt (fun (t : ℝ) => (phaseGroup hκm t) (ψ.toLp 2 MeasureTheory.volume)) (-Complex.I • ((SchwartzMap.smulLeftCLM ℂ κ) ψ).toLp 2 MeasureTheory.volume) 0

★ The strong derivative of the phase group at t = 0, on Schwartz functions: ∂_t (e^{−itκ} ψ)|₀ = −iκψ in L², by dominated convergence with dominator 4κ²|ψ|².

theorem SchrodingerGroup.hasDerivAt_fourierGroup_toLp_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {κ : E → ℝ} (hκm : Measurable κ) (hκ : Function.HasTemperateGrowth κ) (f : SchwartzMap E ℂ) : HasDerivAt (fun (t : ℝ) => (fourierGroup hκm t) (f.toLp 2 MeasureTheory.volume)) (-Complex.I • ((SchwartzMap.fourierMultiplierCLM ℂ κ) f).toLp 2 MeasureTheory.volume) 0

★ The strong derivative of U_κ at t = 0 on Schwartz functions: ∂_t (U_κ(t) f)|₀ = −i κ(D) f in L².

theorem SchrodingerGroup.hasDerivAt_fourierGroup_toLp {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {κ : E → ℝ} (hκm : Measurable κ) (hκ : Function.HasTemperateGrowth κ) (f : SchwartzMap E ℂ) (t₀ : ℝ) : HasDerivAt (fun (t : ℝ) => (fourierGroup hκm t) (f.toLp 2 MeasureTheory.volume)) (-Complex.I • ((SchwartzMap.fourierMultiplierCLM ℂ κ) ((fourierGroupS κ t₀) f)).toLp 2 MeasureTheory.volume) t₀

★★ The Schrödinger equation for U_κ, in L², for Schwartz initial data: at every t, ∂_t (U_κ(t) f) = −i κ(D) (U_κ(t) f).

theorem SchrodingerGroup.hasDerivAt_freeSchrodinger {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (f : SchwartzMap E ℂ) (t₀ : ℝ) : HasDerivAt (fun (t : ℝ) => (freeSchrodinger t) (f.toLp 2 MeasureTheory.volume)) (-Complex.I • (kineticOp ((freeSchrodingerS t₀) f)).toLp 2 MeasureTheory.volume) t₀

★★ The free Schrödinger equation i ∂_t ψ = H₀ ψ, H₀ = −½ d²/dx², in L² for Schwartz initial data: ψ(t) = e^{−itH₀} f satisfies ∂_t ψ(t) = −i H₀ ψ(t) at every t.