Complex.tsum_exp_neg_quadratic

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

The theorem `Complex.tsum_exp_neg_quadratic` states Jacobi's theta-function transformation formula for the sum of exponential functions whose exponent is a negative definite quadratic form. Specifically, for any complex number `a` with positive real part, and for any complex number `b`, the infinite sum over all integers `n` of the exponential of the expression `(-π*a*n² + 2π*b*n)` is equal to `(1 / a ^ (1 / 2))` times the infinite sum over all integers `n` of the exponential of `(-π/a * (n + Complex.I * b) ^ 2)`. Here, `π` is the mathematical constant Pi, `Complex.I` denotes the imaginary unit, and `^` denotes exponentiation.

More concisely: For any complex number `a` with positive real part and `b` in the complex plane, the sum of exponentials of the negative definite quadratic forms `-π*a*n² + 2π*b*n` over all integers `n` equals `(1 / (a ^ (1 / 2))` times the sum of exponentials of `-π/a * (n + I*b)²` over all integers `n`, where `I` is the imaginary unit.