Source indexedtheorem · leanprover/lean4:v4.32.0

intervalIntegrable_sin_div_kernel

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1003 to 1014

Source documentation

The sine-over-argument kernel is interval-integrable on finite intervals; the value at zero is irrelevant by the removable singularity of Real.sinc.

Exact Lean statement

theorem intervalIntegrable_sin_div_kernel (a b : ℝ) :
    IntervalIntegrable
      (fun v : ℝ => if v = 0 then (0 : ℂ) else (Real.sin v / v : ℂ))
      volume a b

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem intervalIntegrable_sin_div_kernel (a b : ℝ) :    IntervalIntegrable      (fun v : ℝ => if v = 0 then (0 : ℂ) else (Real.sin v / v : ℂ))      volume a b := by  let g : ℝ → ℂ := fun v => (Real.sinc v : ℂ)  have hg : IntervalIntegrable g volume a b := by    exact (Complex.continuous_ofReal.comp Real.continuous_sinc).intervalIntegrable a b  refine hg.congr_ae ?_  refine ae_restrict_of_ae ?_  filter_upwards [show ∀ᵐ v : ℝ ∂volume, v ≠ 0 by simp [ae_iff, measure_singleton]]    with v hv  simp [g, Real.sinc_of_ne_zero hv, hv]