English
For k ≥ 1, the sum ∑_{n≥1} 1/n^{2k} equals (-1)^{k+1} (2π)^{2k} B_{2k} /(2 (2k)!).
Русский
Для k ≥ 1 сумма ∑_{n≥1} 1/n^{2k} равна (-1)^{k+1} (2π)^{2k} B_{2k} /(2 (2k)!).
LaTeX
$$$\displaystyle \sum_{n=1}^{\infty} \frac{1}{n^{2k}} = (-1)^{k+1} \frac{(2\pi)^{2k}}{2\,(2k)!} \; B_{2k}. $$$
Lean4
theorem hasSum_zeta_nat {k : ℕ} (hk : k ≠ 0) :
HasSum (fun n : ℕ => 1 / (n : ℝ) ^ (2 * k))
((-1 : ℝ) ^ (k + 1) * (2 : ℝ) ^ (2 * k - 1) * π ^ (2 * k) * bernoulli (2 * k) / (2 * k)!) :=
by
convert hasSum_one_div_nat_pow_mul_cos hk (left_mem_Icc.mpr zero_le_one) using 1
· ext1 n; rw [mul_zero, Real.cos_zero, mul_one]
rw [Polynomial.eval_zero_map, Polynomial.bernoulli_eval_zero, eq_ratCast]
have : (2 : ℝ) ^ (2 * k - 1) = (2 : ℝ) ^ (2 * k) / 2 :=
by
rw [eq_div_iff (two_ne_zero' ℝ)]
conv_lhs =>
congr
· skip
· rw [← pow_one (2 : ℝ)]
rw [← pow_add, Nat.sub_add_cancel]
omega
rw [this, mul_pow]
ring
