Source indexedtheorem · leanprover/lean4:v4.32.0

norm_riemannZeta_eulerProduct

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZeta · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZeta.lean:224 to 232

Mathematical statement

Exact Lean statement

theorem norm_riemannZeta_eulerProduct (s : ℂ) (hs : 1 < s.re) :
    ‖riemannZeta s‖ = ∏' p : Nat.Primes, (‖1 - ((p : ℕ) : ℂ) ^ (-s)‖)⁻¹

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem norm_riemannZeta_eulerProduct (s : ℂ) (hs : 1 < s.re) :    ‖riemannZeta s‖ = ∏' p : Nat.Primes, (‖1 - ((p : ℕ) : ℂ) ^ (-s)‖)⁻¹ := by  calc    ‖riemannZeta s‖ = ‖∏' p : Nat.Primes, (1 - ((p : ℕ) : ℂ) ^ (-s))⁻¹‖ := by      rw [riemannZeta_eulerProduct_tprod hs]    _ = ∏' p : Nat.Primes, ‖(1 - ((p : ℕ) : ℂ) ^ (-s))⁻¹‖ := by      exact Multipliable.norm_tprod (riemannZeta_eulerProduct_hasProd hs).multipliable    _ = ∏' p : Nat.Primes, (‖1 - ((p : ℕ) : ℂ) ^ (-s)‖)⁻¹ := by      congr 1; ext p; simp [norm_inv]