tsum_exp_neg_mul_int_sq — Mathlib

English

For real a > 0, the Jacobi-type relation holds for sums of exp(-π a n^2).

Русский

Для действительного a > 0 верно то же преобразование Джакоби для сумм exp(-π a n^2).

LaTeX

$$$$ \\sum_{n\\in \\mathbb{Z}} e^{-\\pi a n^2} = (1/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) :
    (∑' n : ℤ, exp (-π * a * (n : ℝ) ^ 2)) = (1 : ℝ) / a ^ (1 / 2 : ℝ) * (∑' n : ℤ, exp (-π / a * (n : ℝ) ^ 2)) := by
  simpa only [← ofReal_inj, ofReal_tsum, ofReal_exp, ofReal_mul, ofReal_neg, ofReal_pow, ofReal_intCast, ofReal_div,
    ofReal_one, ofReal_cpow ha.le, ofReal_ofNat, mul_zero, zero_mul, add_zero] using
    Complex.tsum_exp_neg_quadratic (by rwa [ofReal_re] : 0 < (a : ℂ).re) 0

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