LSeriesHasSum_one — Mathlib

English

For Re(s) > 1, the L-series of the constant sequence 1 has sum equal to the Riemann zeta function: L(1,s) = ζ(s).

Русский

Для Re(s) > 1 сумма L-серии константы 1 равна дзета-функции Римана: L(1,s) = ζ(s).

LaTeX

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

Lean4

/-- The L-series of the constant sequence `1` equals the Riemann zeta function on its
domain of convergence `1 < re s`. -/
theorem LSeriesHasSum_one {s : ℂ} (hs : 1 < s.re) : LSeriesHasSum 1 s (riemannZeta s) :=
  LSeries_one_eq_riemannZeta hs ▸ (LSeriesSummable_one_iff.mpr hs).LSeriesHasSum

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