The free Gaussian packet

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

Analysis/Semigroup/SchrodingerSchwartz.lean puts the free Schrödinger group U₀(t) = e^{−itH₀}, H₀ = −½ d²/dx², on Schwartz space. This module (BACKLOG #48, FC-5‴) lets the reader see it act, on the one initial state whose evolution is explicit — the Gaussian:

• the Gaussian is a Schwartz function: gaussianS a ha : 𝓢(ℝ, ℂ) is x ↦ e^{−π a x²} for Re a > 0 (the pin has no Gaussian bundled as a SchwartzMap). Its n-th derivative is P_n(x) e^{−π a x²} with P_{n+1} = P_n' − 2πa X P_n (iteratedDeriv_gaussFun, gaussPoly), and |x|^m e^{−c x²} ≤ 1 + m!/cᵐ (pow_mul_exp_neg_le, from x^m/m! ≤ eˣ) gives the decay;
• its Fourier transform is the Gaussian a^{−1/2} e^{−πξ²/a} (fourier_gaussianS, Mathlib's fourier_gaussian_pi read as a Schwartz identity), and the free phase e^{−2π²itξ²} turns it into the Gaussian of the complex parameter a⁻¹ + 2πit (smulLeft_phase_fourier_gaussianS); the inverse transform of an even function is its transform (fourierInv_gaussianS);
• ★★ freeSchrodingerS_gaussianS — the packet spreads: U₀(t) g_a = packetAmp a t • g_{a(t)} with a(t) = (a⁻¹ + 2πit)⁻¹ = a / (1 + 2πiat) (packetParam_eq) and amplitude (1 + 2πiat)^{−1/2} (packetAmp_eq, after ★ mul_cpow_of_re_pos: the principal square root is multiplicative on the right half-plane); ★ freeSchrodinger_gaussianS_toLp is the same in L², through freeSchrodinger_toLp;
• ★ re_packetParam_ofReal — for a real width parameter σ > 0 the density is |U₀(t) g_σ|² = |amp|² e^{−2π σ(t) x²} with σ(t) = σ / (1 + (2πσt)²) decreasing in |t| (norm_freeSchrodingerS_gaussianS): the Gaussian widens as √(1 + (2πσt)²), the textbook spreading of a free wave packet (units ℏ = m = 1, Mathlib's Fourier convention).

Honest scope

⚠️ One dimension only (E = ℝ); the d-dimensional Gaussian e^{−πa‖x‖²} follows the same route through Mathlib's fourier_gaussian_innerProductSpace and is not done. The packet is centred at the origin with zero mean momentum; the moving packet e^{2πipx} g_a(x − q) (Mathlib's fourier_gaussian_pi' carries the shift) is not stated. No uncertainty product is computed.

References: M. Reed, B. Simon, Methods of Modern Mathematical Physics II §IX.7; A. Messiah, Quantum Mechanics I ch. II §3 (the spreading of a free Gaussian packet); Analysis/Semigroup/SchrodingerSchwartz.lean (FC-5″); specs/feynman-continuum-scoping.md §5; specs/BACKLOG.md #48; specs/future-work.md FP-1.

The Gaussian and its derivatives

noncomputable def SchrodingerGroup.gaussFun (a : ℂ) (x : ℝ) : ℂ

The Gaussian x ↦ e^{−π a x²} on ℝ, as a plain function.

Equations

• SchrodingerGroup.gaussFun a x = Complex.exp (-↑Real.pi * a * ↑x ^ 2)

noncomputable def SchrodingerGroup.gaussPoly (a : ℂ) : ℕ → Polynomial ℂ

The polynomial factor of the n-th derivative of the Gaussian: P_0 = 1, P_{n+1} = P_n' − 2πa X P_n.

Equations

• SchrodingerGroup.gaussPoly a 0 = 1
• SchrodingerGroup.gaussPoly a n.succ = Polynomial.derivative (SchrodingerGroup.gaussPoly a n) - (2 * ↑Real.pi * a) • (Polynomial.X * SchrodingerGroup.gaussPoly a n)

theorem SchrodingerGroup.norm_gaussFun (a : ℂ) (x : ℝ) : ‖gaussFun a x‖ = Real.exp (-(Real.pi * a.re * x ^ 2))

theorem SchrodingerGroup.contDiff_gaussFun (a : ℂ) : ContDiff ℝ (↑⊤) (gaussFun a)

theorem SchrodingerGroup.hasDerivAt_eval_mul_gaussFun (a : ℂ) (p : Polynomial ℂ) (x : ℝ) : HasDerivAt (fun (x : ℝ) => Polynomial.eval (↑x) p * gaussFun a x) (Polynomial.eval (↑x) (Polynomial.derivative p - (2 * ↑Real.pi * a) • (Polynomial.X * p)) * gaussFun a x) x

The derivative of P(x) e^{−π a x²} is (P' − 2πa X P)(x) e^{−π a x²}.

theorem SchrodingerGroup.iteratedDeriv_gaussFun (a : ℂ) (n : ℕ) : iteratedDeriv n (gaussFun a) = fun (x : ℝ) => Polynomial.eval (↑x) (gaussPoly a n) * gaussFun a x

The n-th derivative of the Gaussian is P_n(x) e^{−π a x²}.

theorem SchrodingerGroup.norm_eval_le_sum (p : Polynomial ℂ) (z : ℂ) : ‖Polynomial.eval z p‖ ≤ ∑ i ∈ Finset.range (p.natDegree + 1), ‖p.coeff i‖ * ‖z‖ ^ i

A polynomial is bounded by the sum of its coefficients' norms times the powers.

theorem SchrodingerGroup.pow_mul_exp_neg_le {c : ℝ} (hc : 0 < c) (m : ℕ) (x : ℝ) : |x| ^ m * Real.exp (-(c * x ^ 2)) ≤ 1 + ↑m.factorial / c ^ m

|x|^m e^{−c x²} ≤ 1 + m!/cᵐ for c > 0: from y^m/m! ≤ e^y at y = c x².

theorem SchrodingerGroup.decay_gaussFun {a : ℂ} (ha : 0 < a.re) (k n : ℕ) : ∃ (C : ℝ), ∀ (x : ℝ), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (gaussFun a) x‖ ≤ C

The Schwartz decay of the Gaussian: every |x|^k |∂ⁿ g| is bounded.

noncomputable def SchrodingerGroup.gaussianS (a : ℂ) (ha : 0 < a.re) : SchwartzMap ℝ ℂ

The Gaussian x ↦ e^{−π a x²}, Re a > 0, as a Schwartz function on ℝ.

Equations

• SchrodingerGroup.gaussianS a ha = { toFun := SchrodingerGroup.gaussFun a, smooth' := ⋯, decay' := ⋯ }

theorem SchrodingerGroup.coe_gaussianS (a : ℂ) (ha : 0 < a.re) : ⇑(gaussianS a ha) = gaussFun a

@[simp]

theorem SchrodingerGroup.gaussianS_apply (a : ℂ) (ha : 0 < a.re) (x : ℝ) : (gaussianS a ha) x = Complex.exp (-↑Real.pi * a * ↑x ^ 2)

theorem SchrodingerGroup.norm_gaussianS_apply (a : ℂ) (ha : 0 < a.re) (x : ℝ) : ‖(gaussianS a ha) x‖ = Real.exp (-(Real.pi * a.re * x ^ 2))

The Fourier transform and the free phase

theorem SchrodingerGroup.fourier_gaussianS (a : ℂ) (ha : 0 < a.re) : ⇑(FourierTransform.fourier (gaussianS a ha)) = fun (ξ : ℝ) => 1 / a ^ (1 / 2) * Complex.exp (-↑Real.pi / a * ↑ξ ^ 2)

The Fourier transform of the Gaussian is the Gaussian a^{−1/2} e^{−πξ²/a}.

theorem SchrodingerGroup.re_inv_pos {b : ℂ} (hb : 0 < b.re) : 0 < b⁻¹.re

theorem SchrodingerGroup.fourierInv_gaussianS (b : ℂ) (hb : 0 < b.re) : FourierTransformInv.fourierInv (gaussianS b hb) = (1 / b ^ (1 / 2)) • gaussianS b⁻¹ ⋯

The inverse Fourier transform of the (even) Gaussian is its Fourier transform.

theorem SchrodingerGroup.re_inv_add_pos {a : ℂ} (ha : 0 < a.re) (t : ℝ) : 0 < (a⁻¹ + 2 * ↑Real.pi * Complex.I * ↑t).re

The inverse width parameter a⁻¹ + 2πit of the packet at time t has positive real part.

theorem SchrodingerGroup.smulLeft_phase_fourier_gaussianS (a : ℂ) (ha : 0 < a.re) (t : ℝ) : (SchwartzMap.smulLeftCLM ℂ (phaseFun freeSymbol t)) (FourierTransform.fourier (gaussianS a ha)) = (1 / a ^ (1 / 2)) • gaussianS (a⁻¹ + 2 * ↑Real.pi * Complex.I * ↑t) ⋯

The free phase e^{−2π²itξ²} times the transform of g_a is the transform of the Gaussian of parameter a⁻¹ + 2πit, up to the constant a^{−1/2}.

The spreading packet

noncomputable def SchrodingerGroup.packetParam (a : ℂ) (t : ℝ) : ℂ

The width parameter of the packet at time t: a(t) = (a⁻¹ + 2πit)⁻¹ = a / (1 + 2πiat).

Equations

• SchrodingerGroup.packetParam a t = (a⁻¹ + 2 * ↑Real.pi * Complex.I * ↑t)⁻¹

noncomputable def SchrodingerGroup.packetAmp (a : ℂ) (t : ℝ) : ℂ

The amplitude of the packet at time t: a^{−1/2} (a⁻¹ + 2πit)^{−1/2} = (1 + 2πiat)^{−1/2}.

Equations

• SchrodingerGroup.packetAmp a t = 1 / a ^ (1 / 2) * (1 / (a⁻¹ + 2 * ↑Real.pi * Complex.I * ↑t) ^ (1 / 2))

theorem SchrodingerGroup.re_packetParam_pos {a : ℂ} (ha : 0 < a.re) (t : ℝ) : 0 < (packetParam a t).re

theorem SchrodingerGroup.one_add_mul_eq {a : ℂ} (ha : a ≠ 0) (t : ℝ) : 1 + 2 * ↑Real.pi * Complex.I * a * ↑t = a * (a⁻¹ + 2 * ↑Real.pi * Complex.I * ↑t)

theorem SchrodingerGroup.packetParam_eq {a : ℂ} (ha : 0 < a.re) (t : ℝ) : packetParam a t = a / (1 + 2 * ↑Real.pi * Complex.I * a * ↑t)

theorem SchrodingerGroup.mul_cpow_of_re_pos {x y : ℂ} (hx : 0 < x.re) (hy : 0 < y.re) (r : ℂ) : (x * y) ^ r = x ^ r * y ^ r

★ The principal power is multiplicative on the right half-plane.

theorem SchrodingerGroup.packetAmp_eq {a : ℂ} (ha : 0 < a.re) (t : ℝ) : packetAmp a t = 1 / (1 + 2 * ↑Real.pi * Complex.I * a * ↑t) ^ (1 / 2)

The amplitude in closed form: (1 + 2πiat)^{−1/2}.

theorem SchrodingerGroup.freeSchrodingerS_gaussianS (a : ℂ) (ha : 0 < a.re) (t : ℝ) : (freeSchrodingerS t) (gaussianS a ha) = packetAmp a t • gaussianS (packetParam a t) ⋯

★★ The free Gaussian packet spreads: U₀(t) g_a = packetAmp a t • g_{a(t)} with a(t) = (a⁻¹ + 2πit)⁻¹. The Fourier transform of g_a is a Gaussian, the free phase multiplies its exponent by 2πit, and the inverse transform is a Gaussian again.

theorem SchrodingerGroup.freeSchrodinger_gaussianS_toLp (a : ℂ) (ha : 0 < a.re) (t : ℝ) : (freeSchrodinger t) ((gaussianS a ha).toLp 2 MeasureTheory.volume) = (packetAmp a t • gaussianS (packetParam a t) ⋯).toLp 2 MeasureTheory.volume

★ The same in L²: the free Schrödinger group of SchrodingerGroup.lean sends the Gaussian to the spread Gaussian.

theorem SchrodingerGroup.norm_freeSchrodingerS_gaussianS (a : ℂ) (ha : 0 < a.re) (t x : ℝ) : ‖((freeSchrodingerS t) (gaussianS a ha)) x‖ = ‖packetAmp a t‖ * Real.exp (-(Real.pi * (packetParam a t).re * x ^ 2))

The modulus of the spread packet is a real Gaussian of parameter Re a(t).

theorem SchrodingerGroup.re_packetParam_ofReal {σ : ℝ} (hσ : 0 < σ) (t : ℝ) : (packetParam (↑σ) t).re = σ / (1 + (2 * Real.pi * σ * t) ^ 2)

★ For a real width parameter σ > 0, Re a(t) = σ / (1 + (2πσt)²): the density e^{−2π Re a(t) x²} widens with |t|.