Source indexedtheorem · leanprover/lean4:v4.32.0

norm_riemannZeta_ratio_le_on_verticalLine

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaConvexity · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaConvexity.lean:38 to 48

Source documentation

For σ > 1, the Euler product at re s = 2σ controls ‖ζ(2σ) / ζ σ‖ on the line σ + it.

Exact Lean statement

theorem norm_riemannZeta_ratio_le_on_verticalLine (σ t : ℝ) (hσ : 1 < σ) :
    ‖riemannZeta (2 * (σ : ℂ)) / riemannZeta (σ : ℂ)‖ ≤ ‖riemannZeta (verticalLine σ t)‖

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem norm_riemannZeta_ratio_le_on_verticalLine (σ t : ℝ) (hσ : 1 < σ) :    ‖riemannZeta (2 * (σ : ℂ)) / riemannZeta (σ : ℂ)‖ ≤ ‖riemannZeta (verticalLine σ t)‖ := by  have hs : 1 < (verticalLine σ t).re := by rw [verticalLine_re]; exact hσ  calc    ‖riemannZeta (2 * (σ : ℂ)) / riemannZeta (σ : ℂ)‖        = ∏' p : Nat.Primes, (1 + ((p : ℕ) : ℝ) ^ (-σ))⁻¹ :=          norm_riemannZeta_div_riemannZeta σ hσ    _ ≤ ∏' p : Nat.Primes, (‖1 - ((p : ℕ) : ℂ) ^ (-verticalLine σ t)‖)⁻¹ :=        tprod_inv_one_add_real_le_riemannZeta_norm_on_verticalLine σ t hσ    _ = ‖riemannZeta (verticalLine σ t)‖ := by      simpa [verticalLine] using (norm_riemannZeta_eulerProduct (verticalLine σ t) hs).symm