tsum_dirichletSummand — Mathlib

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]

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