LSeriesHasSum_zeta — Mathlib

English

Let s be a complex number with Re(s) > 1. The Dirichlet series associated to the constant arithmetic function 1 equals the Riemann zeta function: L((↗ζ), s) = ζ(s).

Русский

Пусть s — комплексное число с Re(s) > 1. Дирихлеева серия, соответствующая константной функции 1, равна дзета-функции Римана: L((↗ζ), s) = ζ(s).

LaTeX

$$$1 < \\operatorname{Re}(s) \\;\\Rightarrow\\; L(1,s) = \\zeta(s)$$$

Lean4

/-- The L-series of the arithmetic function `ζ` equals the Riemann Zeta Function on its
domain of convergence `1 < re s`. -/
theorem LSeriesHasSum_zeta {s : ℂ} (hs : 1 < s.re) : LSeriesHasSum (↗ζ) s (riemannZeta s) :=
  LSeries_zeta_eq_riemannZeta hs ▸ (LSeriesSummable_zeta_iff.mpr hs).LSeriesHasSum

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