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 rexp_neg_quadratic_isLittleO_rpow_atTop {a : ℝ} (ha : a < 0) (b s : ℝ) : (fun (x : ℝ) => Real.exp (a * x ^ 2 + b * x)) =o[Filter.atTop] fun (x : ℝ) => x ^ s

theorem cexp_neg_quadratic_isLittleO_rpow_atTop {a : ℂ} (ha : a.re < 0) (b : ℂ) (s : ℝ) : (fun (x : ℝ) => Complex.exp (a * ↑x ^ 2 + b * ↑x)) =o[Filter.atTop] fun (x : ℝ) => x ^ s

theorem cexp_neg_quadratic_isLittleO_abs_rpow_cocompact {a : ℂ} (ha : a.re < 0) (b : ℂ) (s : ℝ) : (fun (x : ℝ) => Complex.exp (a * ↑x ^ 2 + b * ↑x)) =o[Filter.cocompact ℝ] fun (x : ℝ) => |x| ^ s

theorem tendsto_rpow_abs_mul_exp_neg_mul_sq_cocompact {a : ℝ} (ha : 0 < a) (s : ℝ) : Filter.Tendsto (fun (x : ℝ) => |x| ^ s * Real.exp (-a * x ^ 2)) (Filter.cocompact ℝ) (nhds 0)

theorem isLittleO_exp_neg_mul_sq_cocompact {a : ℂ} (ha : 0 < a.re) (s : ℝ) : (fun (x : ℝ) => Complex.exp (-a * ↑x ^ 2)) =o[Filter.cocompact ℝ] fun (x : ℝ) => |x| ^ s

theorem Complex.tsum_exp_neg_quadratic {a : ℂ} (ha : 0 < a.re) (b : ℂ) : ∑' (n : ℤ), Complex.exp (-↑Real.pi * a * ↑n ^ 2 + 2 * ↑Real.pi * b * ↑n) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), Complex.exp (-↑Real.pi / a * (↑n + Complex.I * b) ^ 2)

Jacobi's theta-function transformation formula for the sum of exp -Q(x), where Q is a negative definite quadratic form.

theorem Complex.tsum_exp_neg_mul_int_sq {a : ℂ} (ha : 0 < a.re) : ∑' (n : ℤ), Complex.exp (-↑Real.pi * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), Complex.exp (-↑Real.pi / a * ↑n ^ 2)

theorem Real.tsum_exp_neg_mul_int_sq {a : ℝ} (ha : 0 < a) : ∑' (n : ℤ), Real.exp (-Real.pi * a * ↑n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ℤ), Real.exp (-Real.pi / a * ↑n ^ 2)