English
The Riemann zeta function at 2 equals π^2/6: ζ(2) = π^2/6.
Русский
Зета-функция Римана в точке 2 равна π^2/6: ζ(2) = π^2/6.
LaTeX
$$$$ \operatorname{riemannZeta}(2) = \frac{\pi^2}{6}. $$$$
Lean4
/-- Explicit formula for `ζ (2 * k)`, for `k ∈ ℕ` with `k ≠ 0`, in terms of the Bernoulli number
`bernoulli (2 * k)`.
Compare `hasSum_zeta_nat` for a version formulated in terms of a sum over `1 / n ^ (2 * k)`, and
`riemannZeta_neg_nat_eq_bernoulli` for values at negative integers (equivalent to the above via
the functional equation). -/
theorem riemannZeta_two_mul_nat {k : ℕ} (hk : k ≠ 0) :
riemannZeta (2 * k) = (-1) ^ (k + 1) * (2 : ℂ) ^ (2 * k - 1) * (π : ℂ) ^ (2 * k) * bernoulli (2 * k) / (2 * k)! :=
by
convert congr_arg ((↑) : ℝ → ℂ) (hasSum_zeta_nat hk).tsum_eq
· rw [← Nat.cast_two, ← Nat.cast_mul, zeta_nat_eq_tsum_of_gt_one (by cutsat)]
simp [push_cast]
· norm_cast
