LSeriesSummable_moebius_iff — Mathlib

English

For s ∈ ℂ, LSeriesSummable (↗μ) s iff 1 < s.re.

Русский

Для s ∈ ℂ LSeriesSummable (↗μ) s эквивалентно 1 < s.re.

LaTeX

$$LSeriesSummable (↗μ) s \leftrightarrow 1 < s.re$$

Lean4

/-- The L-series of the Möbius function converges absolutely at `s` if and only if `re s > 1`. -/
theorem LSeriesSummable_moebius_iff {s : ℂ} : LSeriesSummable (↗μ) s ↔ 1 < s.re :=
  by
  refine ⟨fun H ↦ ?_, LSeriesSummable_of_bounded_of_one_lt_re (m := 1) fun n _ ↦ ?_⟩
  · by_contra! h
    exact not_LSeriesSummable_moebius_at_one <| LSeriesSummable.of_re_le_re (by simpa) H
  · norm_cast
    exact abs_moebius_le_one

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