tsum_riemannZetaSummand — Mathlib

English

For Re(s) > 1, the Dirichlet zeta summand matches the zeta function: ∑_{n≥1} riemannZetaSummandHom(ne_zero_of_one_lt_re hs) n = ζ(s).

Русский

При Re(s) > 1 сумма ζ-суммирования равна ζ(s).

LaTeX

$$$\text{If } \Re(s) > 1, \quad \sum_{n=1}^{\infty} \riemannZetaSummandHom(ne_zero_of_one_lt_re hs)\, n = \zeta(s).$$$

Lean4

theorem tsum_riemannZetaSummand (hs : 1 < s.re) :
    ∑' (n : ℕ), riemannZetaSummandHom (ne_zero_of_one_lt_re hs) n = riemannZeta s :=
  by
  have hsum := summable_riemannZetaSummand hs
  rw [zeta_eq_tsum_one_div_nat_add_one_cpow hs, hsum.of_norm.tsum_eq_zero_add, map_zero, zero_add]
  simp only [riemannZetaSummandHom, cpow_neg, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, Nat.cast_add, Nat.cast_one,
    one_div]

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