abscissaOfAbsConv_moebius — Mathlib

English

The abscissa of absolute convergence of the Moebius L-series equals 1.

Русский

Абсцисса абсолютной сходимости L‑серии Моебиуса равна 1.

LaTeX

$$abscissaOfAbsConv ↗μ = 1$$

Lean4

/-- The abscissa of absolute convergence of the L-series of the Möbius function is `1`. -/
theorem abscissaOfAbsConv_moebius : abscissaOfAbsConv ↗μ = 1 := by
  simpa [abscissaOfAbsConv, LSeriesSummable_moebius_iff, Set.Ioi_def, EReal.image_coe_Ioi] using
    csInf_Ioo <| EReal.coe_lt_top 1

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