LSeriesSummable_zetaMul — Mathlib

English

If hs holds with Re(s) > 1 for all χ, then L-series summability of χ.zetaMul at s holds.

Русский

Если для χ с χ^2 = 1 верно Re(s) > 1, тогда LSeriesSummable χ.zetaMul s выполняется.

LaTeX

$$$\forall χ:\mathrm{DirichletCharacter}\;\mathbb{C}\;N,\ {s:\mathbb{C}},\ Real.instLT.lt 1 s.re \Rightarrow LSeriesSummable (ArithmeticFunction.instFunLikeNat.\text{coe } χ.zetaMul) s$$$

Lean4

theorem LSeriesSummable_zetaMul (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) : LSeriesSummable χ.zetaMul s :=
  by
  refine
    ArithmeticFunction.LSeriesSummable_mul (LSeriesSummable_zeta_iff.mpr hs) <|
      LSeriesSummable_of_bounded_of_one_lt_re (m := 1) (fun n hn ↦ ?_) hs
  simpa only [toArithmeticFunction, coe_mk, hn, ↓reduceIte] using norm_le_one χ _

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