English
For any real S, any T>0, and any k ∈ ℕ, the sum over n ∈ ℤ of |n|^k exp(-π (T n^2 - 2 S |n|)) converges.
Русский
Для любых S ∈ ℝ, T>0 и любого k ∈ ℕ сумма по n∈ℤ из |n|^k exp(-π (T n^2 - 2 S |n|)) сходится.
LaTeX
$$$\sum_{n\in\mathbb{Z}} \bigl|n\bigr|^{k} \exp\bigl(-\pi (T n^{2} - 2 S |n|)\bigr) < \infty$$$
Lean4
/-- The uniform bound we have given is summable, and remains so after multiplying by any fixed
power of `|n|` (we shall need this for `k = 0, 1, 2`). -/
theorem summable_pow_mul_jacobiTheta₂_term_bound (S : ℝ) {T : ℝ} (hT : 0 < T) (k : ℕ) :
Summable (fun n : ℤ ↦ (|n| ^ k : ℝ) * Real.exp (-π * (T * n ^ 2 - 2 * S * |n|))) :=
by
suffices Summable (fun n : ℕ ↦ (n ^ k : ℝ) * Real.exp (-π * (T * n ^ 2 - 2 * S * n))) by
apply Summable.of_nat_of_neg <;> simpa only [Int.cast_neg, neg_sq, abs_neg, Int.cast_natCast, Nat.abs_cast]
apply summable_of_isBigO_nat (summable_pow_mul_exp_neg_nat_mul k zero_lt_one)
apply IsBigO.mul (isBigO_refl _ _)
refine Real.isBigO_exp_comp_exp_comp.mpr (Tendsto.isBoundedUnder_le_atBot ?_)
simp_rw [← tendsto_neg_atTop_iff, Pi.sub_apply]
conv =>
enter [1, n]
rw [show -(-π * (T * n ^ 2 - 2 * S * n) - -1 * n) = n * (π * T * n - (2 * π * S + 1)) by ring]
refine tendsto_natCast_atTop_atTop.atTop_mul_atTop₀ (tendsto_atTop_add_const_right _ _ ?_)
exact tendsto_natCast_atTop_atTop.const_mul_atTop (mul_pos pi_pos hT)
