English
For any natural k, real a, and t > 0, the sequence n ↦ f_nat(k, a, t, n) is summable over n ∈ ℕ, i.e., the infinite series ∑ f_nat(k, a, t, n) converges.
Русский
Для любого натурального k, вещественного a и t>0 ряд ∑_{n≥0} f_nat(k,a,t,n) сходится.
LaTeX
$$$\sum_{n=0}^{\infty} f_{nat}(k,a,t,n) \quad \text{Сходится.}$$$
Lean4
theorem summable_f_nat (k : ℕ) (a : ℝ) {t : ℝ} (ht : 0 < t) : Summable (f_nat k a t) :=
by
have : Summable fun n : ℕ ↦ n ^ k * exp (-π * (n + a) ^ 2 * t) :=
by
refine
(((summable_pow_mul_jacobiTheta₂_term_bound (|a| * t) ht k).mul_right (rexp (-π * a ^ 2 * t))).comp_injective
Nat.cast_injective).of_norm_bounded
(fun n ↦ ?_)
simp_rw [mul_assoc, Function.comp_apply, ← Real.exp_add, norm_mul, norm_pow, Int.cast_abs, Int.cast_natCast,
norm_eq_abs, Nat.abs_cast, abs_exp]
gcongr
rw [← sub_nonneg]
rw [show
-π * (t * n ^ 2 - 2 * (|a| * (t * n))) + -π * (a ^ 2 * t) - -π * ((n + a) ^ 2 * t) = π * t * n * (|a| + a) * 2
by ring]
refine mul_nonneg (mul_nonneg (by positivity) ?_) two_pos.le
rw [← neg_le_iff_add_nonneg]
apply neg_le_abs
apply (this.mul_left (2 ^ k)).of_norm_bounded_eventually_nat
simp_rw [← mul_assoc, f_nat, norm_mul, norm_eq_abs, abs_exp, mul_le_mul_iff_of_pos_right (exp_pos _), ← mul_pow,
abs_pow, two_mul]
filter_upwards [eventually_ge_atTop (Nat.ceil |a|)] with n hn
gcongr
exact (abs_add_le ..).trans (add_le_add (Nat.abs_cast _).le (Nat.ceil_le.mp hn))
