zeta_eq_tsum_one_div_nat_add_one_cpow

English

Equivalently, for Re(s) > 1, ζ(s) = ∑_{n≥0} (n+1)^{−s}.

Русский

Эквивалентно: для Re(s) > 1 ζ(s) = ∑_{n≥0} (n+1)^{−s}.

LaTeX

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

Lean4

/-- Alternate formulation of `zeta_eq_tsum_one_div_nat_cpow` with a `+ 1` (to avoid relying
on mathlib's conventions for `0 ^ s`). -/
theorem zeta_eq_tsum_one_div_nat_add_one_cpow {s : ℂ} (hs : 1 < re s) : riemannZeta s = ∑' n : ℕ, 1 / (n + 1 : ℂ) ^ s :=
  by
  have := zeta_eq_tsum_one_div_nat_cpow hs
  rw [Summable.tsum_eq_zero_add] at this
  · simpa [zero_cpow (Complex.ne_zero_of_one_lt_re hs)]
  · rwa [Complex.summable_one_div_nat_cpow]

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