# 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[] 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)) (nhds 0)
theorem isLittleO_exp_neg_mul_sq_cocompact {a : } (ha : 0 < a.re) (s : ) :
(fun (x : ) => Complex.exp (-a * x ^ 2)) =o[] fun (x : ) => |x| ^ s
theorem Complex.tsum_exp_neg_quadratic {a : } (ha : 0 < a.re) (b : ) :
∑' (n : ), Complex.exp ( * n ^ 2 + 2 * * b * n) = 1 / a ^ (1 / 2) * ∑' (n : ), Complex.exp ( * (n + ) ^ 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 ( * n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ), Complex.exp ( * n ^ 2)
theorem Real.tsum_exp_neg_mul_int_sq {a : } (ha : 0 < a) :
∑' (n : ), Real.exp ( * n ^ 2) = 1 / a ^ (1 / 2) * ∑' (n : ), Real.exp ( * n ^ 2)