Source indexedtheorem · leanprover/lean4:v4.32.0

intervalIntegrable_scaled_sin_div_kernel

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1018 to 1035

Source documentation

The scaled sine kernel is interval-integrable on finite intervals; its value at zero is again irrelevant.

Exact Lean statement

theorem intervalIntegrable_scaled_sin_div_kernel (T a b : ℝ) :
    IntervalIntegrable
      (fun u : ℝ => if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ))
      volume a b

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem intervalIntegrable_scaled_sin_div_kernel (T a b : ℝ) :    IntervalIntegrable      (fun u : ℝ => if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ))      volume a b := by  let g : ℝ → ℂ := fun u => (((T / π : ℝ) * Real.sinc (T * u) : ℝ) : ℂ)  have hg : IntervalIntegrable g volume a b := by    apply Continuous.intervalIntegrable    dsimp [g]    fun_prop  refine hg.congr_ae ?_  refine ae_restrict_of_ae ?_  filter_upwards [show ∀ᵐ u : ℝ ∂volume, u ≠ 0 by simp [ae_iff, measure_singleton]]    with u hu  by_cases hT : T = 0  · simp [g, hT, hu]  · have hTu : T * u ≠ 0 := mul_ne_zero hT hu    simp [g, hu, Real.sinc_of_ne_zero hTu]    field_simp [Real.pi_ne_zero, hT, hu]