LSeriesSummable_of_one_lt_re — Mathlib

English

If Re(s) > 1, then the L-series L(χ) converges absolutely for any Dirichlet character χ modulo N.

Русский

Если Re(s) > 1, то L-ряд χ сходится абсолютно для любого Dirichlet-символа χ модуля N.

LaTeX

$$$1 < \operatorname{Re}(s) \Rightarrow L(\uparrow χ)(s) \text{ converges absolutely.}$$$

Lean4

/-- The L-series of a Dirichlet character converges absolutely at `s` if `re s > 1`. -/
theorem LSeriesSummable_of_one_lt_re {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :
    LSeriesSummable (↗χ) s :=
  LSeriesSummable_of_bounded_of_one_lt_re (fun _ _ ↦ χ.norm_le_one _) hs

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