English
If 1 < Re(s), then the norm of the zeta summand decays sufficiently to ensure summability: ∑_{n≥1} ||riemannZetaSummandHom (ne_zero_of_one_lt_re hs) n|| converges.
Русский
При 1 < Re(s) нормa слагаемого ζ-суммы достаточно мала, чтобы обеспечить суммируемость: ∑_{n≥1} ||riemannZetaSummandHom (не 0) n|| сходится.
LaTeX
$$$\\text{If } 1 < \\Re(s)\\text{, then } \\sum_{n=1}^{\\infty} \\big\\|\\operatorname{riemannZetaSummandHom}(ne\\;0\\;\\of{\\Re(s)})\\, n\\big\\| < \\infty.$$$
Lean4
/-- When `s.re > 1`, the map `n ↦ n^(-s)` is norm-summable. -/
theorem summable_riemannZetaSummand (hs : 1 < s.re) :
Summable (fun n ↦ ‖riemannZetaSummandHom (ne_zero_of_one_lt_re hs) n‖) :=
by
simp only [riemannZetaSummandHom, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]
convert Real.summable_nat_rpow_inv.mpr hs with n
rw [← ofReal_natCast, norm_cpow_eq_rpow_re_of_nonneg (Nat.cast_nonneg n) <| re_neg_ne_zero_of_one_lt_re hs, neg_re,
Real.rpow_neg <| Nat.cast_nonneg n]
