Source indexedtheorem · leanprover/lean4:v4.32.0

tendsto_intervalIntegral_exp_neg_mul_sinc_nhdsGT_zero

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1784 to 1802

Source documentation

On a fixed finite window, damping tends back to the undamped sinc integral.

Exact Lean statement

theorem tendsto_intervalIntegral_exp_neg_mul_sinc_nhdsGT_zero (R : ℝ) :
    Filter.Tendsto
      (fun a : ℝ => ∫ x in (0 : ℝ)..R, Real.exp (-a * x) * Real.sinc x)
      (𝓝[>] (0 : ℝ))
      (nhds (∫ x in (0 : ℝ)..R, Real.sinc x))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem tendsto_intervalIntegral_exp_neg_mul_sinc_nhdsGT_zero (R : ℝ) :    Filter.Tendsto      (fun a : ℝ => ∫ x in (0 : ℝ)..R, Real.exp (-a * x) * Real.sinc x)      (𝓝[>] (0 : ℝ))      (nhds (∫ x in (0 : ℝ)..R, Real.sinc x)) := by  let f : ℝ → ℝ → ℝ := fun a x => Real.exp (-a * x) * Real.sinc x  have hf : Continuous f.uncurry := by    dsimp [f, Function.uncurry]    fun_prop  have hcont : Continuous fun a : ℝ => ∫ x in (0 : ℝ)..R, f a x :=    intervalIntegral.continuous_parametric_intervalIntegral_of_continuous'      (μ := volume) (f := f) hf (0 : ℝ) R  have ht : Filter.Tendsto (fun a : ℝ => ∫ x in (0 : ℝ)..R, f a x)      (𝓝 (0 : ℝ)) (nhds (∫ x in (0 : ℝ)..R, f 0 x)) :=    hcont.tendsto (0 : ℝ)  have ht' : Filter.Tendsto (fun a : ℝ => ∫ x in (0 : ℝ)..R, f a x)      (𝓝[>] (0 : ℝ)) (nhds (∫ x in (0 : ℝ)..R, f 0 x)) :=    ht.mono_left nhdsWithin_le_nhds  simpa [f] using ht'