hasSum_zeta_four — Mathlib

English

The value of the zeta function at 4 is ζ(4) = π^4/90.

Русский

Зета-функция в точке 4: ζ(4) = π^4/90.

LaTeX

$$$\displaystyle \sum_{n=1}^{\infty} \frac{1}{n^{4}} = \frac{\pi^{4}}{90}. $$$

Lean4

theorem hasSum_zeta_four : HasSum (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 4) (π ^ 4 / 90) :=
  by
  convert hasSum_zeta_nat two_ne_zero using 1; norm_num
  rw [bernoulli_eq_bernoulli'_of_ne_one, bernoulli'_four]
  · norm_num [Nat.factorial]; field_simp; ring
  · decide

Похожие утверждения