Source indexedtheorem · leanprover/lean4:v4.32.0

norm_riemannZeta_shift_le

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaConvexity · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaConvexity.lean:156 to 171

Source documentation

If ‖s‖ ≤ 1 and 2 < |t|, then ‖ζ (s + 3/2 + it)‖ < 10 + 2|t|.

Exact Lean statement

theorem norm_riemannZeta_shift_le (t : ℝ) (s : ℂ) (hs : ‖s‖ ≤ 1) (ht : 2 < |t|) :
    ‖riemannZeta (s + (3 / 2 : ℝ) + Complex.I * t)‖ < 10 + 2 * |t|

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem norm_riemannZeta_shift_le (t : ℝ) (s : ℂ) (hs : ‖s‖ ≤ 1) (ht : 2 < |t|) :    ‖riemannZeta (s + (3 / 2 : ℝ) + Complex.I * t)‖ < 10 + 2 * |t| := by  set z := verticalLine (s.re + (3 / 2 : ℝ)) (s.im + t)  have hz : s + (3 / 2 : ℝ) + Complex.I * t = z := by    simp only [z]    conv_lhs => rw [mul_comm Complex.I t]    exact verticalLine_add_const s (3 / 2) t  have ⟨hz_re, hz_im⟩ := shift_mem_strip s t hs ht  have hz_im_le : |z.im| ≤ 1 + |t| := by    simp only [z, verticalLine_im]    linarith [abs_add_le s.im t, (Complex.abs_im_le_norm s).trans hs]  calc    ‖riemannZeta (s + (3 / 2 : ℝ) + Complex.I * t)‖ = ‖riemannZeta z‖ := by rw [hz]    _ < (8 : ℝ) + 2 * |z.im| := norm_riemannZeta_lt_linear_im_on_strip z hz_re hz_im    _ ≤ (8 : ℝ) + 2 * (1 + |t|) := by gcongr    _ = (10 : ℝ) + 2 * |t| := by ring