Complex Gaussians as Schwartz functions

For b : ℂ with 0 < b.re, the Gaussian x ↦ exp (-b ‖x‖²) on a real inner product space is a Schwartz function, SchwartzMap.gaussian. The parameter is complex, so this covers both the real heat-kernel Gaussians and the oscillating Gaussians x ↦ exp (π i τ ‖x‖²), 0 < τ.im, whose lattice sums are theta series. The normalisation -b * ‖x‖ ^ 2 is the one of Mathlib's fourier_gaussian_innerProductSpace, which computes the Fourier transform of this function; SchwartzMap.fourierInv_gaussian restates it for the inverse Fourier transform of the Schwartz Gaussian. Translates of the Gaussian are Schwartz functions through Mathlib's SchwartzMap.compSubConstCLM.

The decay estimate writes the Gaussian as Complex.exp composed with x ↦ -b * ‖x‖ ^ 2. Every real iterated derivative of Complex.exp at z has norm ‖exp z‖, and the inner function has temperate growth (Mathlib's Function.hasTemperateGrowth_norm_sq), so the Faà di Bruno bound norm_iteratedFDeriv_comp_le bounds the n-th derivative by a polynomial in ‖x‖ times exp (-b.re * ‖x‖ ^ 2). The two scalar inputs, TauCeti.norm_iteratedFDeriv_real_cexp and TauCeti.one_add_pow_mul_exp_neg_mul_sq_le, live in TauCeti.Analysis.SpecialFunctions.Exp.Deriv and TauCeti.Analysis.SpecialFunctions.Gaussian.Basic.

Main declarations

• SchwartzMap.gaussian: the Gaussian x ↦ exp (-b ‖x‖²), 0 < b.re, as a Schwartz function.
• SchwartzMap.gaussian_apply, SchwartzMap.coe_gaussian: its values.
• SchwartzMap.fourierInv_gaussian: its inverse Fourier transform (π / b)^(n/2) exp (-π² ‖x‖² / b), where n is the dimension.

noncomputable def SchwartzMap.gaussian {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {b : ℂ} (hb : 0 < b.re) : SchwartzMap V ℂ

The Gaussian x ↦ exp (-b ‖x‖²) on a real inner product space, for 0 < b.re, as a Schwartz function. Its Fourier transform is computed by Mathlib's fourier_gaussian_innerProductSpace.

@[simp]

theorem SchwartzMap.gaussian_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {b : ℂ} (hb : 0 < b.re) (x : V) : (gaussian hb) x = Complex.exp (-b * ↑‖x‖ ^ 2)

The value of the Schwartz Gaussian at x is exp (-b ‖x‖²).

theorem SchwartzMap.coe_gaussian {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {b : ℂ} (hb : 0 < b.re) : ⇑(gaussian hb) = fun (x : V) => Complex.exp (-b * ↑‖x‖ ^ 2)

The Schwartz Gaussian, as a function, is x ↦ exp (-b ‖x‖²).

theorem SchwartzMap.fourierInv_gaussian {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {b : ℂ} (hb : 0 < b.re) (x : V) : (FourierTransformInv.fourierInv (gaussian hb)) x = (↑Real.pi / b) ^ (↑(Module.finrank ℝ V) / 2) * Complex.exp (-↑Real.pi ^ 2 * ↑‖x‖ ^ 2 / b)

The inverse Fourier transform of the Schwartz Gaussian exp (-b ‖ξ‖²), 0 < b.re, on a real inner product space of dimension n is the Gaussian (π / b)^(n/2) exp (-π² ‖x‖² / b).