English
For every k ≥ 2, the sequence a_n = -k!/(2π i n)^k (n ∈ ℤ) is absolutely summable (the series converges).
Русский
Для каждого k ≥ 2 последовательность a_n = -k!/(2π i n)^k (n ∈ ℤ) абсолютно сходится (ряд сходится).
LaTeX
$$$\sum_{n \in \mathbb{Z}} \left| \dfrac{-k!}{(2\pi i n)^k} \right| < \infty.$$$
Lean4
theorem summable_bernoulli_fourier {k : ℕ} (hk : 2 ≤ k) : Summable (fun n => -k ! / (2 * π * I * n) ^ k : ℤ → ℂ) :=
by
have : ∀ n : ℤ, -(k ! : ℂ) / (2 * π * I * n) ^ k = -k ! / (2 * π * I) ^ k * (1 / (n : ℂ) ^ k) := by intro n;
rw [mul_one_div, div_div, ← mul_pow]
simp_rw [this]
refine Summable.mul_left _ <| .of_norm ?_
have : (fun x : ℤ => ‖1 / (x : ℂ) ^ k‖) = fun x : ℤ => |1 / (x : ℝ) ^ k| :=
by
ext1 x
simp only [one_div, norm_inv, norm_pow, norm_intCast, pow_abs, abs_inv]
simp_rw [this]
rwa [summable_abs_iff, Real.summable_one_div_int_pow]
