Source indexedtheorem · leanprover/lean4:v4.32.0

norm_sin_div_kernel_le_abs_height

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:612 to 630

Source documentation

The removable sine kernel is bounded by its height.

Exact Lean statement

theorem norm_sin_div_kernel_le_abs_height (T u : ℝ) :
    ‖(if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ))‖ ≤
      |T| / π

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem norm_sin_div_kernel_le_abs_height (T u : ℝ) :    ‖(if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ))‖ ≤      |T| / π := by  by_cases hu : u = 0  · rw [if_pos hu]    simpa using (div_nonneg (abs_nonneg T) Real.pi_pos.le)  · rw [if_neg hu]    rw [norm_div, norm_mul, Complex.norm_real, Complex.norm_real, Complex.norm_real]    simp only [Real.norm_eq_abs]    have hsin : |Real.sin (T * u)| ≤ |T| * |u| := by      simpa [abs_mul] using (Real.abs_sin_le_abs (x := T * u))    calc      |Real.sin (T * u)| / (|π| * |u|)          ≤ (|T| * |u|) / (|π| * |u|) :=            div_le_div_of_nonneg_right hsin              (mul_nonneg (abs_nonneg _) (abs_nonneg _))      _ = |T| / π := by        rw [abs_of_pos Real.pi_pos]        field_simp [abs_pos.mpr hu, Real.pi_ne_zero]