English
For k ≥ 1 and x ∈ [0,1], the sum ∑_{n≥1} sin(2π n x)/n^{2k+1} equals (-1)^{k+1} (2π)^{2k+1} / (2 (2k+1)!) · B_{2k+1}(x).
Русский
Для k ≥ 1 и x ∈ [0,1] сумма ∑_{n≥1} sin(2π n x)/n^{2k+1} равна (-1)^{k+1} (2π)^{2k+1} / (2 (2k+1)!) · B_{2k+1}(x).
LaTeX
$$$\displaystyle \sum_{n=1}^{\infty} \frac{\sin(2\pi n x)}{n^{2k+1}} = (-1)^{k+1} \frac{(2\pi)^{2k+1}}{2\,(2k+1)!} \; B_{2k+1}(x).$$$
Lean4
theorem hasSum_one_div_nat_pow_mul_sin {k : ℕ} (hk : k ≠ 0) {x : ℝ} (hx : x ∈ Icc (0 : ℝ) 1) :
HasSum (fun n : ℕ => 1 / (n : ℝ) ^ (2 * k + 1) * Real.sin (2 * π * n * x))
((-1 : ℝ) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / (2 * k + 1)! *
(Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))).eval x) :=
by
have :
HasSum (fun n : ℕ => 1 / (n : ℂ) ^ (2 * k + 1) * (fourier n (x : 𝕌) - fourier (-n) (x : 𝕌)))
((-1 : ℂ) ^ (k + 1) * I * (2 * π : ℂ) ^ (2 * k + 1) / (2 * k + 1)! * bernoulliFun (2 * k + 1) x) :=
by
convert hasSum_one_div_nat_pow_mul_fourier (by cutsat : 2 ≤ 2 * k + 1) hx using 1
· ext1 n
rw [pow_add (-1 : ℂ), pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul, pow_one, ← neg_eq_neg_one_mul, ←
sub_eq_add_neg]
· congr
rw [pow_add, pow_one]
conv_rhs =>
rw [mul_pow]
congr
congr
· skip
· rw [pow_add, pow_one, pow_mul, I_sq]
ring
have ofReal_two : ((2 : ℝ) : ℂ) = 2 := by norm_cast
convert ((hasSum_iff _ _).mp (this.div_const (2 * I))).1
· convert (ofReal_re _).symm
rw [ofReal_mul]; rw [← mul_div]; congr
· rw [ofReal_div, ofReal_one, ofReal_pow]; rfl
· rw [ofReal_sin, ofReal_mul, fourier_coe_apply, fourier_coe_apply, sin, ofReal_one, div_one, div_one, ofReal_mul,
ofReal_mul, ofReal_two, Int.cast_neg, Int.cast_natCast, ofReal_natCast, ← div_div, div_I, div_mul_eq_mul_div₀, ←
neg_div, ← neg_mul, neg_sub]
congr 4
· 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, ← div_div, div_I, div_mul_eq_mul_div₀]
have : ∀ α β γ δ : ℂ, α * I * β / γ * δ * I = I ^ 2 * α * β / γ * δ := by intros; ring
rw [this, I_sq]
rw [bernoulliFun]
ring
