riemannZeta_eulerProduct — Mathlib

English

For complex s with Re(s) > 1, the Euler product over primes converges to the Riemann zeta function ζ(s).

Русский

Пусть s комплексно, Re(s) > 1. Тогда Эйлеров продукт по всем простым числам сходится к дзета-функции: ζ(s).

LaTeX

$$$\Re(s) > 1 \;\Rightarrow\; \displaystyle \lim_{n \to \infty} \prod_{p \in \text{primesBelow}(n)} (1 - p^{-s})^{-1} = \zeta(s)$$$

Lean4

/-- The Euler product for the Riemann ζ function, valid for `s.re > 1`.
This version is stated in the form of convergence of finite partial products. -/
theorem riemannZeta_eulerProduct (hs : 1 < s.re) :
    Tendsto (fun n : ℕ ↦ ∏ p ∈ primesBelow n, (1 - (p : ℂ) ^ (-s))⁻¹) atTop (𝓝 (riemannZeta s)) :=
  by
  rw [← tsum_riemannZetaSummand hs]
  apply eulerProduct_completely_multiplicative <| summable_riemannZetaSummand hs

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