riemannZeta_eulerProduct_exp_log — Mathlib

English

A variant of the Euler product for the Riemann zeta function: exp(∑' p: Nat.Primes, −log(1 − p^{−s})) = ζ(s).

Русский

Вариант Эйлерова произведения для ζ-функции: exp(∑' p: Nat.Primes, −log(1 − p^{−s})) = ζ(s).

LaTeX

$$$\exp\Big(\sum_{p \text{ prime}} -\log(1 - p^{-s})\Big) = \zeta(s).$$$

Lean4

/-- A variant of the Euler product for the Riemann zeta function. -/
theorem riemannZeta_eulerProduct_exp_log {s : ℂ} (hs : 1 < s.re) :
    exp (∑' p : Nat.Primes, -Complex.log (1 - p ^ (-s))) = riemannZeta s :=
  LSeries_one_eq_riemannZeta hs ▸ ArithmeticFunction.LSeries_zeta_eulerProduct_exp_log hs

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