Source indexedtheorem · leanprover/lean4:v4.32.0

tendsto_integral_Ioi_exp_neg_mul_sinc_nhdsGT_zero

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:2041 to 2052

Source documentation

Abel limit of the Laplace-regularized sinc integral as the damping tends to zero from the right.

Exact Lean statement

theorem tendsto_integral_Ioi_exp_neg_mul_sinc_nhdsGT_zero :
    Filter.Tendsto
      (fun a : ℝ => ∫ x : ℝ in Set.Ioi 0, Real.exp (-a * x) * Real.sinc x)
      (𝓝[>] (0 : ℝ)) (𝓝 (π / 2 : ℝ))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem tendsto_integral_Ioi_exp_neg_mul_sinc_nhdsGT_zero :    Filter.Tendsto      (fun a : ℝ => ∫ x : ℝ in Set.Ioi 0, Real.exp (-a * x) * Real.sinc x)      (𝓝[>] (0 : ℝ)) (𝓝 (π / 2 : ℝ)) := by  have hinv : Filter.Tendsto (fun a : ℝ => a⁻¹) (𝓝[>] (0 : ℝ)) Filter.atTop :=    tendsto_inv_nhdsGT_zero  have harctan : Filter.Tendsto (fun a : ℝ => Real.arctan a⁻¹)      (𝓝[>] (0 : ℝ)) (𝓝 (π / 2 : ℝ)) :=    (Real.tendsto_arctan_atTop.comp hinv).mono_right nhdsWithin_le_nhds  refine harctan.congr' ?_  filter_upwards [self_mem_nhdsWithin] with a ha  exact (integral_Ioi_exp_neg_mul_sinc_eq_arctan_inv a ha).symm