zeta_eq_tsum_one_div_nat_cpow — Mathlib

English

For Re(s) > 1, the Riemann zeta function equals the Dirichlet series ∑_{n≥1} n^{−s}.

Русский

При Re(s) > 1 дзета Римана равна ряд Римана: ζ(s) = ∑_{n≥1} n^{−s}.

LaTeX

$$$\\\\riemannZeta(s) = \\\\sum_{n=1}^{∞} n^{-s}$, 1 < Re(s)$$

Lean4

/-- The Riemann zeta function agrees with the naive Dirichlet-series definition when the latter
converges. (Note that this is false without the assumption: when `re s ≤ 1` the sum is divergent,
and we use a different definition to obtain the analytic continuation to all `s`.) -/
theorem zeta_eq_tsum_one_div_nat_cpow {s : ℂ} (hs : 1 < re s) : riemannZeta s = ∑' n : ℕ, 1 / (n : ℂ) ^ s := by
  simpa only [QuotientAddGroup.mk_zero, cosZeta_zero, mul_zero, zero_mul, Real.cos_zero, ofReal_one] using
    (hasSum_nat_cosZeta 0 hs).tsum_eq.symm

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