LSeriesSummable_iff — Mathlib

English

For N > 0 and χ, L(χ) is summable at s if and only if 1 < Re(s).

Русский

Для N > 0 и χ L(χ) суммируем при s тогда и только тогда, когда 1 < Re(s).

LaTeX

$$$LSeriesSummable(\uparrow χ)(s) \iff 1 < \Re(s).$$$

Lean4

/-- The L-series of a Dirichlet character mod `N > 0` converges absolutely at `s` if and only if
`re s > 1`. -/
theorem LSeriesSummable_iff {N : ℕ} (hN : N ≠ 0) (χ : DirichletCharacter ℂ N) {s : ℂ} :
    LSeriesSummable (↗χ) s ↔ 1 < s.re :=
  by
  refine ⟨fun H ↦ ?_, LSeriesSummable_of_one_lt_re χ⟩
  by_contra! h
  exact not_LSeriesSummable_at_one hN χ <| LSeriesSummable.of_re_le_re (by simp [h]) H

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