LSeriesSummable_of_one_lt_re — Mathlib

English

If Φ is a periodic function modulo N, then the L-series converges for 1 < Re(s).

Русский

Если Φ периодична по модулю N, то L-функция сходится при 1 < Re(s).

LaTeX

$$$\\\\text{LSeries}_{\\\\mathbb{Z}/N\\\\mathbb{Z}}(\\\\Phi, s) \\text{ converges for } 1 < \\Re(s)$$$

Lean4

/-- If `Φ` is a periodic function, then the L-series of `Φ` converges for `1 < re s`. -/
theorem LSeriesSummable_of_one_lt_re (Φ : ZMod N → ℂ) {s : ℂ} (hs : 1 < re s) : LSeriesSummable (Φ ·) s :=
  by
  let c := max' _ <| univ_nonempty.image (norm ∘ Φ)
  refine LSeriesSummable_of_bounded_of_one_lt_re (fun n _ ↦ le_max' _ _ ?_) (m := c) hs
  exact mem_image_of_mem _ (mem_univ _)

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