absicssaOfAbsConv_eq_one — Mathlib

English

For a Dirichlet character χ with N > 0, the abscissa of absolute convergence of its L-series is 1.

Русский

Для χ с N > 0 абсцисса абсолютной конвергенции L-рядов χ равна 1.

LaTeX

$$$\operatorname{abscissaOfAbsConv}(\uparrow χ) = 1.$$$

Lean4

/-- The abscissa of absolute convergence of the L-series of a Dirichlet character mod `N > 0`
is `1`. -/
theorem absicssaOfAbsConv_eq_one {N : ℕ} (hn : N ≠ 0) (χ : DirichletCharacter ℂ N) : abscissaOfAbsConv ↗χ = 1 := by
  simpa [abscissaOfAbsConv, LSeriesSummable_iff hn χ, Set.Ioi_def, EReal.image_coe_Ioi] using
    csInf_Ioo <| EReal.coe_lt_top 1

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