Source indexedtheorem · leanprover/lean4:v4.32.0

riemannZeta_eq_mul_tprod_inv_one_add

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:188 to 208

Source documentation

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

Exact Lean statement

theorem riemannZeta_eq_mul_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_eq_mul_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 hs2 : 1 < (2 * s).re := by    simp [s, Complex.mul_re, Complex.ofReal_re]    linarith  have hζ := (riemannZeta_eulerProduct_hasProd hs).multipliable  have hμ := multipliable_complex_inv_one_add r hr  calc    riemannZeta (2 * s)        = ∏' p : Nat.Primes, (1 - ((p : ℕ) : ℂ) ^ (-(2 * s)))⁻¹ :=          (riemannZeta_eulerProduct_tprod hs2).symm    _ = ∏' p : Nat.Primes, (1 - ((p : ℕ) : ℂ) ^ (-s))⁻¹ * (1 + ((p : ℕ) : ℂ) ^ (-s))⁻¹ := by      refine tprod_congr fun p => eulerFactor_two_mul p s hs    _ = (∏' p : Nat.Primes, (1 - ((p : ℕ) : ℂ) ^ (-s))⁻¹) *          ∏' p : Nat.Primes, (1 + ((p : ℕ) : ℂ) ^ (-s))⁻¹ := by      rw [Multipliable.tprod_mul hζ hμ]    _ = riemannZeta s * ∏' p : Nat.Primes, (1 + ((p : ℕ) : ℂ) ^ (-s))⁻¹ := by      rw [← riemannZeta_eulerProduct_tprod hs]