Source indexedtheorem · leanprover/lean4:v4.32.0

riemannZeta_div_riemannZeta_eq_tprod_inv_one_add

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:211 to 222

Source documentation

ζ(2r)/ζ(r) = ∏_p (1 + p^{-r})⁻¹ for real r > 1.

Exact Lean statement

theorem riemannZeta_div_riemannZeta_eq_tprod_inv_one_add (r : ℝ) (hr : 1 < r) :
    riemannZeta (2 * (r : ℂ)) / riemannZeta (r : ℂ) =
      ∏' p : Nat.Primes, (1 + ((p : ℕ) : ℂ) ^ (-((r : ℝ) : ℂ)))⁻¹

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem riemannZeta_div_riemannZeta_eq_tprod_inv_one_add (r : ℝ) (hr : 1 < r) :    riemannZeta (2 * (r : ℂ)) / riemannZeta (r : ℂ) =      ∏' p : Nat.Primes, (1 + ((p : ℕ) : ℂ) ^ (-((r : ℝ) : ℂ)))⁻¹ := by  set s : ℂ := (r : ℂ)  have hs : 1 < s.re := by simpa [s] using hr  have hzeta_ne : riemannZeta s ≠ 0 := riemannZeta_ne_zero_of_one_lt_re hs  calc    riemannZeta (2 * s) / riemannZeta s        = (riemannZeta s * ∏' p : Nat.Primes, (1 + ((p : ℕ) : ℂ) ^ (-s))⁻¹) / riemannZeta s := by          rw [riemannZeta_eq_mul_tprod_inv_one_add r hr]    _ = ∏' p : Nat.Primes, (1 + ((p : ℕ) : ℂ) ^ (-s))⁻¹ := by      rw [mul_div_cancel_left₀ _ hzeta_ne]