The Fourier transform of the theta-series Gaussian

On a finite-dimensional real inner product space E of dimension n, the Gaussian x ↦ exp (π i τ ‖x‖²) with 0 < im τ is the case b = -π i τ of the Gaussian x ↦ exp (-b ‖x‖²), 0 < re b, whose Fourier transform Mathlib's fourier_gaussian_innerProductSpace computes, and which is a Schwartz function (SchwartzMap.gaussian). Summed over a lattice, these Gaussians give its theta series. In the shape used for the inversion law of theta series,

𝓕 (x ↦ exp (π i τ ‖x‖²)) y = (τ / i) ^ (-n / 2) * exp (π i (-1 / τ) ‖y‖²),

with the complex power cpow, and for even n = 2k the factor is the integer power ((-i) ^ k * τ ^ k)⁻¹.

Main declarations

• TauCeti.fourier_cexp_pi_mul_I_mul_norm_sq_mul: the Fourier transform of x ↦ exp (π i τ ‖x‖²), with the factor (τ / i) ^ (-n / 2).
• TauCeti.fourier_cexp_pi_mul_I_mul_norm_sq_mul_of_finrank_eq: the same in even rank 2k, with the factor ((-i) ^ k * τ ^ k)⁻¹.

References

• J.-P. Serre, A Course in Arithmetic, Ch. VII §6.

theorem TauCeti.fourier_cexp_pi_mul_I_mul_norm_sq_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {τ : ℂ} (hτ : 0 < τ.im) (y : E) : FourierTransform.fourier (fun (x : E) => Complex.exp (↑Real.pi * Complex.I * ↑(‖x‖ ^ 2) * τ)) y = (τ / Complex.I) ^ (-↑(Module.finrank ℝ E) / 2) * Complex.exp (↑Real.pi * Complex.I * ↑(‖y‖ ^ 2) * (-1 / τ))

The Fourier transform of the Gaussian x ↦ exp (π i τ ‖x‖²): for 0 < im τ and n = finrank ℝ E, 𝓕 (x ↦ exp (π i τ ‖x‖²)) y = (τ / i) ^ (-n / 2) * exp (π i (-1 / τ) ‖y‖²), with the principal branch of the complex power; τ / i lies in the right half-plane.

theorem TauCeti.fourier_cexp_pi_mul_I_mul_norm_sq_mul_of_finrank_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {k : ℕ} (hk : Module.finrank ℝ E = 2 * k) {τ : ℂ} (hτ : 0 < τ.im) (y : E) : FourierTransform.fourier (fun (x : E) => Complex.exp (↑Real.pi * Complex.I * ↑(‖x‖ ^ 2) * τ)) y = ((-Complex.I) ^ k * τ ^ k)⁻¹ * Complex.exp (↑Real.pi * Complex.I * ↑(‖y‖ ^ 2) * (-1 / τ))

The Fourier transform of the Gaussian x ↦ exp (π i τ ‖x‖²) in even rank: if finrank ℝ E = 2 * k and 0 < im τ, then 𝓕 (x ↦ exp (π i τ ‖x‖²)) y = ((-i) ^ k * τ ^ k)⁻¹ * exp (π i (-1 / τ) ‖y‖²).