Poisson summation applied to the Gaussian #
In Real.tsum_exp_neg_mul_int_sq
and Complex.tsum_exp_neg_mul_int_sq
, we use Poisson summation
to prove the identity
∑' (n : ℤ), exp (-π * a * n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), exp (-π / a * n ^ 2)
for positive real a
, or complex a
with positive real part. (See also
NumberTheory.ModularForms.JacobiTheta
.)
First we show that Gaussian-type functions have rapid decay along cocompact ℝ
.
theorem
tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact
{a : ℝ}
(ha : 0 < a)
(s : ℝ)
:
Filter.Tendsto (fun (x : ℝ) => |x| ^ s * (-a * x ^ 2).exp) (Filter.cocompact ℝ) (nhds 0)
Jacobi's theta-function transformation formula for the sum of exp -Q(x)
, where Q
is a
negative definite quadratic form.