tsum_exp_neg_mul_int_sq — Mathlib

English

For complex a with Re(a) > 0, the identity holds: sum over Z of exp(-π a n^2) equals a^{-1/2} times sum over Z of exp(-π/a n^2).

Русский

Для a ∈ ℂ с Re(a) > 0 выполняется: сумма по n∈ℤ exp(-π a n^2) = a^{-1/2} сумма exp(-π/a n^2).

LaTeX

$$$$ \\sum_{n\\in \\mathbb{Z}} e^{-\\pi a n^2} = a^{-1/2} \\sum_{n\\in \\mathbb{Z}} e^{-\\pi/a \\; n^2}. $$$$

Lean4

theorem tsum_exp_neg_mul_int_sq {a : ℂ} (ha : 0 < a.re) :
    (∑' n : ℤ, cexp (-π * a * (n : ℂ) ^ 2)) = 1 / a ^ (1 / 2 : ℂ) * ∑' n : ℤ, cexp (-π / a * (n : ℂ) ^ 2) := by
  simpa only [mul_zero, zero_mul, add_zero] using Complex.tsum_exp_neg_quadratic ha 0

Похожие утверждения