Source indexedtheorem · leanprover/lean4:v4.32.0

integrable_sin_div_kernel_smul_of_integrable

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:633 to 657

Source documentation

The sine kernel times an integrable source remains integrable.

Exact Lean statement

theorem integrable_sin_div_kernel_smul_of_integrable
    {f : ℝ → E} (hf : Integrable f) (x T : ℝ) :
    Integrable
      (fun u : ℝ =>
        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •
          f (x - u))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem integrable_sin_div_kernel_smul_of_integrable    {f : ℝ → E} (hf : Integrable f) (x T : ℝ) :    Integrable      (fun u : ℝ =>        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •          f (x - u)) := by  have hfx : Integrable (fun u : ℝ => f (x - u)) := hf.comp_sub_left x  let C : ℂ := (|T| / π : ℝ)  have hC_nonneg : 0 ≤ |T| / π := div_nonneg (abs_nonneg T) Real.pi_pos.le  have hboundInt : Integrable (fun u : ℝ => C • f (x - u)) := hfx.smul C  refine hboundInt.mono ?_ ?_  · have hscalar_meas : Measurable        (fun u : ℝ =>          if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) := by      refine Measurable.ite measurableSet_eq measurable_const ?_      fun_prop    exact hscalar_meas.aestronglyMeasurable.smul hfx.aestronglyMeasurable  · filter_upwards with u    rw [norm_smul, norm_smul]    have hCnorm : ‖C‖ = |T| / π := by      rw [show C = ((|T| / π : ℝ) : ℂ) by rfl, Complex.norm_real, Real.norm_eq_abs,        abs_of_nonneg hC_nonneg]    rw [hCnorm]    exact mul_le_mul (norm_sin_div_kernel_le_abs_height T u) le_rfl      (norm_nonneg _) hC_nonneg