riemannZeta_eulerProduct_hasProd — Mathlib

English

For Re(s) > 1, the Euler product holds: HasProd over primes of (1 − p^{−s})^{−1} equals ζ(s).

Русский

Для Re(s) > 1 Эйлерово произведение: произведение по p простым числам (1 − p^{−s})^{−1} сходится к ζ(s).

LaTeX

$$$\forall s \text{ с } \Re(s)>1:\; \prod_{p \text{ prime}} (1 - p^{-s})^{-1} = \zeta(s).$$$

Lean4

/-- The Euler product for the Riemann ζ function, valid for `s.re > 1`.
This version is stated in terms of `HasProd`. -/
theorem riemannZeta_eulerProduct_hasProd (hs : 1 < s.re) :
    HasProd (fun p : Primes ↦ (1 - (p : ℂ) ^ (-s))⁻¹) (riemannZeta s) :=
  by
  rw [← tsum_riemannZetaSummand hs]
  apply eulerProduct_completely_multiplicative_hasProd <| summable_riemannZetaSummand hs

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