English
Jacobi-type transformation for the sum over Z of exp(-π a n^2 + 2π b n).
Русский
Тип Тета-Функции Джакоби: преобразование суммы по Z от exp(-π a n^2 + 2π b n).
LaTeX
$$$$ \\sum_{n\\in \\mathbb{Z}} e^{-\\pi a n^2 + 2\\pi b n} = a^{-1/2} \\sum_{n\\in \\mathbb{Z}} e^{-\\pi/a (n + i b)^2}. $$$$
Lean4
/-- Jacobi's theta-function transformation formula for the sum of `exp -Q(x)`, where `Q` is a
negative definite quadratic form. -/
theorem tsum_exp_neg_quadratic {a : ℂ} (ha : 0 < a.re) (b : ℂ) :
(∑' n : ℤ, cexp (-π * a * n ^ 2 + 2 * π * b * n)) =
1 / a ^ (1 / 2 : ℂ) * ∑' n : ℤ, cexp (-π / a * (n + I * b) ^ 2) :=
by
let f : ℝ → ℂ := fun x ↦ cexp (-π * a * x ^ 2 + 2 * π * b * x)
have hCf : Continuous f := by
refine Complex.continuous_exp.comp (Continuous.add ?_ ?_)
· exact continuous_const.mul (Complex.continuous_ofReal.pow 2)
· exact continuous_const.mul Complex.continuous_ofReal
have hFf : 𝓕 f = fun x : ℝ ↦ 1 / a ^ (1 / 2 : ℂ) * cexp (-π / a * (x + I * b) ^ 2) :=
fourierIntegral_gaussian_pi' ha b
have h1 : 0 < (↑π * a).re := by
rw [re_ofReal_mul]
exact mul_pos pi_pos ha
have h2 : 0 < (↑π / a).re := by
rw [div_eq_mul_inv, re_ofReal_mul, inv_re]
refine mul_pos pi_pos (div_pos ha <| normSq_pos.mpr ?_)
contrapose! ha
rw [ha, zero_re]
have f_bd : f =O[cocompact ℝ] (fun x => |x| ^ (-2 : ℝ)) :=
by
convert (cexp_neg_quadratic_isLittleO_abs_rpow_cocompact ?_ _ (-2)).isBigO
rwa [neg_mul, neg_re, neg_lt_zero]
have Ff_bd : (𝓕 f) =O[cocompact ℝ] (fun x => |x| ^ (-2 : ℝ)) :=
by
rw [hFf]
have : ∀ (x : ℝ), -↑π / a * (↑x + I * b) ^ 2 = -↑π / a * x ^ 2 + (-2 * π * I * b) / a * x + π * b ^ 2 / a := by
intro x; ring_nf; rw [I_sq]; ring
simp_rw [this]
conv => enter [2, x]; rw [Complex.exp_add, ← mul_assoc _ _ (Complex.exp _), mul_comm]
refine
((cexp_neg_quadratic_isLittleO_abs_rpow_cocompact (?_) (-2 * ↑π * I * b / a) (-2)).isBigO.const_mul_left
_).const_mul_left
_
rwa [neg_div, neg_re, neg_lt_zero]
convert Real.tsum_eq_tsum_fourierIntegral_of_rpow_decay hCf one_lt_two f_bd Ff_bd 0 using 1
· simp only [f, zero_add, ofReal_intCast]
· rw [← tsum_mul_left]
simp only [QuotientAddGroup.mk_zero, fourier_eval_zero, mul_one, hFf, ofReal_intCast]
