Source indexedtheorem · leanprover/lean4:v4.32.0

integrableOn_exp_neg_mul_sinc

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1744 to 1757

Source documentation

The exponentially damped sinc function is integrable on the positive half-line.

Exact Lean statement

theorem integrableOn_exp_neg_mul_sinc (a : ℝ) (ha : 0 < a) :
    IntegrableOn (fun x : ℝ => Real.exp (-a * x) * Real.sinc x) (Set.Ioi 0)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem integrableOn_exp_neg_mul_sinc (a : ℝ) (ha : 0 < a) :    IntegrableOn (fun x : ℝ => Real.exp (-a * x) * Real.sinc x) (Set.Ioi 0) := by  change Integrable (fun x : ℝ => Real.exp (-a * x) * Real.sinc x)    (volume.restrict (Set.Ioi 0))  have h_exp : Integrable (fun x : ℝ => Real.exp (-a * x))      (volume.restrict (Set.Ioi 0)) := by    change IntegrableOn (fun x : ℝ => Real.exp (-a * x)) (Set.Ioi 0)    simpa [mul_comm] using exp_neg_integrableOn_Ioi (0 : ℝ) (b := a) ha  refine h_exp.mono ?_ ?_  · exact (by fun_prop : AEStronglyMeasurable      (fun x : ℝ => Real.exp (-a * x) * Real.sinc x) (volume.restrict (Set.Ioi 0)))  · filter_upwards with x    rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_mul]    exact mul_le_of_le_one_right (abs_nonneg _) (Real.abs_sinc_le_one x)