zeta_nat_eq_tsum_of_gt_one — Mathlib

English

For integers k > 1, the zeta value ζ(k) equals the Dirichlet series ∑_{n≥1} n^{−k}.

Русский

Для целых k > 1 дзета-значение ζ(k) равно ∑_{n≥1} n^{−k}.

LaTeX

$$$\\\\riemannZeta(k) = \\\\sum_{n=1}^{∞} n^{-k}$, for k > 1$$

Lean4

/-- Special case of `zeta_eq_tsum_one_div_nat_cpow` when the argument is in `ℕ`, so the power
function can be expressed using naïve `pow` rather than `cpow`. -/
theorem zeta_nat_eq_tsum_of_gt_one {k : ℕ} (hk : 1 < k) : riemannZeta k = ∑' n : ℕ, 1 / (n : ℂ) ^ k := by
  simp only [zeta_eq_tsum_one_div_nat_cpow
        (by rwa [← ofReal_natCast, ofReal_re, ← Nat.cast_one, Nat.cast_lt] : 1 < re k),
    cpow_natCast]

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