English
For k ≥ 1 and x ∈ [0,1], the sum ∑_{n≥1} cos(2π n x)/n^{2k} equals (-1)^{k+1} (2π)^{2k} / (2 (2k)!) · B_{2k}(x).
Русский
Для k ≥ 1 и x ∈ [0,1] сумма ∑_{n≥1} cos(2π n x)/n^{2k} равна (-1)^{k+1} (2π)^{2k} / (2 (2k)!) · B_{2k}(x).
LaTeX
$$$\displaystyle \sum_{n=1}^{\infty} \frac{\cos(2\pi n x)}{n^{2k}} = (-1)^{k+1} \frac{(2\pi)^{2k}}{2\,(2k)!} \; B_{2k}(x).$$$
Lean4
theorem hasSum_one_div_nat_pow_mul_cos {k : ℕ} (hk : k ≠ 0) {x : ℝ} (hx : x ∈ Icc (0 : ℝ) 1) :
HasSum (fun n : ℕ => 1 / (n : ℝ) ^ (2 * k) * Real.cos (2 * π * n * x))
((-1 : ℝ) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / (2 * k)! *
(Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))).eval x) :=
by
have :
HasSum (fun n : ℕ => 1 / (n : ℂ) ^ (2 * k) * (fourier n (x : 𝕌) + fourier (-n) (x : 𝕌)))
((-1 : ℂ) ^ (k + 1) * (2 * (π : ℂ)) ^ (2 * k) / (2 * k)! * bernoulliFun (2 * k) x) :=
by
convert hasSum_one_div_nat_pow_mul_fourier (by cutsat : 2 ≤ 2 * k) hx using 3
· rw [pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul]
· rw [pow_add, pow_one]
conv_rhs =>
rw [mul_pow]
congr
congr
· skip
· rw [pow_mul, I_sq]
ring
have ofReal_two : ((2 : ℝ) : ℂ) = 2 := by norm_cast
convert ((hasSum_iff _ _).mp (this.div_const 2)).1 with n
· convert (ofReal_re _).symm
rw [ofReal_mul]; rw [← mul_div]; congr
· rw [ofReal_div, ofReal_one, ofReal_pow]; rfl
· rw [ofReal_cos, ofReal_mul, fourier_coe_apply, fourier_coe_apply, cos, ofReal_one, div_one, div_one, ofReal_mul,
ofReal_mul, ofReal_two, Int.cast_neg, Int.cast_natCast, ofReal_natCast]
congr 3
· ring
· ring
· convert (ofReal_re _).symm
rw [ofReal_mul, ofReal_div, ofReal_div, ofReal_mul, ofReal_pow, ofReal_pow, ofReal_neg, ofReal_natCast, ofReal_mul,
ofReal_two, ofReal_one]
rw [bernoulliFun]
ring
