LSeriesSummable_zeta_iff — Mathlib

English

The L-series of 1 is summable at s if and only if Re(s) > 1.

Русский

L-ряд единицы суммируется при s тогда и только тогда, когда Re(s) > 1.

LaTeX

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

Lean4

/-- The `LSeries` associated to the arithmetic function `ζ` converges at `s` if and only if
`re s > 1`. -/
theorem LSeriesSummable_zeta_iff {s : ℂ} : LSeriesSummable (ζ ·) s ↔ 1 < s.re :=
  (LSeriesSummable_congr s const_one_eq_zeta).symm.trans <| LSeriesSummable_one_iff

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