Source indexedtheorem · leanprover/lean4:v4.32.0

norm_riemannZeta_div_riemannZeta

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:234 to 244

Mathematical statement

Exact Lean statement

theorem norm_riemannZeta_div_riemannZeta (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 norm_riemannZeta_div_riemannZeta (r : ℝ) (hr : 1 < r) :    ‖riemannZeta (2 * (r : ℂ)) / riemannZeta (r : ℂ)‖ =      ∏' p : Nat.Primes, (1 + ((p : ℕ) : ℝ) ^ (-r))⁻¹ := by  set s : ℂ := (r : ℂ)  have hw := multipliable_complex_inv_one_add r hr  calc    ‖riemannZeta (2 * s) / riemannZeta s‖ = ‖∏' p : Nat.Primes, (1 + ((p : ℕ) : ℂ) ^ (-s))⁻¹‖ := by      simpa [s] using congrArg norm (riemannZeta_div_riemannZeta_eq_tprod_inv_one_add r hr)    _ = ∏' p : Nat.Primes, ‖(1 + ((p : ℕ) : ℂ) ^ (-s))⁻¹‖ := Multipliable.norm_tprod hw    _ = ∏' p : Nat.Primes, (1 + ((p : ℕ) : ℝ) ^ (-r))⁻¹ := by      refine tprod_congr fun p => norm_cast_inv_one_add p r