English
For Dirichlet character χ and 1 < Re(s), the Dirichlet summand is norm-summable: ∑_{n≥1} ||dirichletSummandHom χ(ne_zero_of_one_lt_re hs) n|| < ∞.
Русский
Для симметричного Дирихлета χ и 1 < Re(s) сумма норм Дирихлетового слагаемого сходится: ∑_{n≥1} ||dirichletSummandHom χ(ne_zero_of_one_lt_re hs) n|| < ∞.
LaTeX
$$$\\text{If } 1 < \\Re(s), \\; \\sum_{n=1}^{\\infty} \\big\\|\\operatorname{dirichletSummandHom}(χ)(ne_zero_of_one_lt_re hs)(n)\\big\\| < \\infty.$$$
Lean4
/-- When `s.re > 1`, the map `n ↦ χ(n) * n^(-s)` is norm-summable. -/
theorem summable_dirichletSummand {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re) :
Summable (fun n ↦ ‖dirichletSummandHom χ (ne_zero_of_one_lt_re hs) n‖) :=
by
simp only [dirichletSummandHom, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, norm_mul]
exact
(summable_riemannZetaSummand hs).of_nonneg_of_le (fun _ ↦ by positivity)
(fun n ↦ mul_le_of_le_one_left (norm_nonneg _) <| χ.norm_le_one n)
