English
For any k ∈ ℕ and a ∈ ℝ, with t > 0, the family n ↦ f_int(k, a, t, n) is summable over n ∈ ℤ.
Русский
Для любых k ∈ ℕ, a ∈ ℝ и t > 0 функция n ↦ f_int(k,a,t,n) суммируема по n ∈ ℤ.
LaTeX
$$$\text{Summable}(f_{int}(k,a,t))\quad (t>0).$$$
Lean4
theorem summable_f_int (k : ℕ) (a : ℝ) {t : ℝ} (ht : 0 < t) : Summable (f_int k a t) :=
by
apply Summable.of_norm
suffices ∀ n, ‖f_int k a t n‖ = ‖(Int.rec (f_nat k a t) (f_nat k (1 - a) t) : ℤ → ℝ) n‖ from
funext this ▸ (HasSum.int_rec (summable_f_nat k a ht).hasSum (summable_f_nat k (1 - a) ht).hasSum).summable.norm
intro n
rcases n with - | m
· simp only [f_int, f_nat, Int.ofNat_eq_coe, Int.cast_natCast, norm_mul, norm_eq_abs, abs_pow, abs_abs]
·
simp only [f_int, f_nat, Int.cast_negSucc, norm_mul, norm_eq_abs, abs_pow, abs_abs,
(by { push_cast; ring
} : -↑(m + 1) + a = -(m + (1 - a))),
abs_neg, neg_sq]
