English
For 1 < Re(s), the Dirichlet summand sums to the Dirichlet L-series: ∑_{n≥1} dirichletSummandHom χ(ne_zero_of_one_lt_re hs) n = L(χ, s).
Русский
Для 1 < Re(s) ζ-суммирование Дирихлетова: сумма слагаемых равна L(χ, s).
LaTeX
$$$\sum_{n=1}^{\infty} \operatorname{dirichletSummandHom}(χ)(ne_zero_of_one_lt_re hs)(n) = L(χ, s).$$$
Lean4
theorem tsum_dirichletSummand {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re) :
∑' (n : ℕ), dirichletSummandHom χ (ne_zero_of_one_lt_re hs) n = L (↗χ) s := by
simp only [dirichletSummandHom, cpow_neg, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, LSeries,
LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs), div_eq_mul_inv]