Source indexedtheorem · leanprover/lean4:v4.32.0

norm_zetaAbelFractKernel_le

PrimeNumberTheoremAnd.Mathlib.NumberTheory.LSeries.RiemannZetaAbelKernel · PrimeNumberTheoremAnd/Mathlib/NumberTheory/LSeries/RiemannZetaAbelKernel.lean:44 to 58

Source documentation

{u} · u^{-s-1} is dominated by u^{- re s - 1} for u ≥ 1.

Exact Lean statement

theorem norm_zetaAbelFractKernel_le (u : ℝ) (hu : 1 ≤ u) (s : ℂ) :
    ‖zetaAbelFractKernel s u‖ ≤ u ^ (-s.re - 1)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem norm_zetaAbelFractKernel_le (u : ℝ) (hu : 1 ≤ u) (s : ℂ) :    ‖zetaAbelFractKernel s u‖ ≤ u ^ (-s.re - 1) := by  have hu0 : 0 < u := one_pos.trans_le hu  have hfract_le1 : ‖((Int.fract u : ℝ) : ℂ)‖ ≤ 1 := by simpa using Int.fract_abs_le_one u  have hle : ‖zetaAbelFractKernel s u‖ ≤ ‖(u : ℂ) ^ (-s - 1)‖ := by    calc      _ = ‖((Int.fract u : ℝ) : ℂ)‖ * ‖(u : ℂ) ^ (-s - 1)‖ := by rw [zetaAbelFractKernel, norm_mul]      _ ≤ 1 * ‖(u : ℂ) ^ (-s - 1)‖ := by        exact mul_le_mul_of_nonneg_right hfract_le1 (norm_nonneg _)      _ = ‖(u : ℂ) ^ (-s - 1)‖ := one_mul _  have hb : ‖(u : ℂ) ^ (-s - 1)‖ = u ^ (-s.re - 1) := by    have hre : (-s - 1).re = -s.re - 1 := by      simp [sub_eq_add_neg]    simpa [hre] using Complex.norm_cpow_eq_rpow_re_of_pos hu0 (-s - 1)  exact hle.trans_eq hb