Source indexedtheorem · leanprover/lean4:v4.32.0

norm_integral_Ioi_exp_neg_mul_sinc_tail_le

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1760 to 1781

Source documentation

Uniform half-line tail control for the damped one-sided sinc integral.

Exact Lean statement

theorem norm_integral_Ioi_exp_neg_mul_sinc_tail_le
    {a R : ℝ} (ha : 0 < a) (hR : 1 ≤ R) :
    ‖∫ x : ℝ in Set.Ioi R, Real.exp (-a * x) * Real.sinc x‖ ≤ 4 * R⁻¹

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem norm_integral_Ioi_exp_neg_mul_sinc_tail_le    {a R : ℝ} (ha : 0 < a) (hR : 1 ≤ R) :    ‖∫ x : ℝ in Set.Ioi R, Real.exp (-a * x) * Real.sinc x‖ ≤ 4 * R⁻¹ := by  have hR_pos : 0 < R := zero_lt_one.trans_le hR  have hint : IntegrableOn (fun x : ℝ => Real.exp (-a * x) * Real.sinc x) (Set.Ioi R) := by    exact (integrableOn_exp_neg_mul_sinc a ha).mono_set (Set.Ioi_subset_Ioi hR_pos.le)  have htend :=    intervalIntegral_tendsto_integral_Ioi      (f := fun x : ℝ => Real.exp (-a * x) * Real.sinc x)      (a := R) (b := fun B : ℝ => B) hint Filter.tendsto_id  have hnorm :      Filter.Tendsto        (fun B : ℝ => ‖∫ x in R..B, Real.exp (-a * x) * Real.sinc x‖)        Filter.atTop        (nhds ‖∫ x : ℝ in Set.Ioi R, Real.exp (-a * x) * Real.sinc x‖) :=    continuous_norm.tendsto      (∫ x : ℝ in Set.Ioi R, Real.exp (-a * x) * Real.sinc x) |>.comp htend  have hbound : ∀ᶠ B : ℝ in Filter.atTop,      ‖∫ x in R..B, Real.exp (-a * x) * Real.sinc x‖ ≤ 4 * R⁻¹ := by    filter_upwards [Filter.eventually_ge_atTop R] with B hRB    exact norm_intervalIntegral_exp_neg_mul_sinc_tail_le ha hR hRB  exact le_of_tendsto hnorm hbound