LSeries_one_eq_riemannZeta — Mathlib

English

For Re(s) > 1, the L-series of the constant sequence 1 equals 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 LSeries_one_eq_riemannZeta {s : ℂ} (hs : 1 < s.re) : L 1 s = riemannZeta s :=
  LSeries_zeta_eq ▸ LSeries_zeta_eq_riemannZeta hs

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