tendsto_integral_Ioi_exp_neg_mul_sinc_of_tendsto_interval

theorem tendsto_integral_Ioi_exp_neg_mul_sinc_of_tendsto_interval    {L : ℝ}    (hL : Filter.Tendsto      (fun R : ℝ => ∫ x in (0 : ℝ)..R, Real.sinc x)      Filter.atTop (nhds L)) :    Filter.Tendsto      (fun a : ℝ => ∫ x : ℝ in Set.Ioi 0, Real.exp (-a * x) * Real.sinc x)      (𝓝[>] (0 : ℝ)) (nhds L) := by  rw [Metric.tendsto_nhds] at hL ⊢  intro ε hε  let η : ℝ := ε / 4  have hη : 0 < η := by dsimp [η]; positivity  have hL_event : ∀ᶠ R : ℝ in Filter.atTop,      dist (∫ x in (0 : ℝ)..R, Real.sinc x) L < η :=    hL η hη  have htail_lim : Filter.Tendsto (fun R : ℝ => 4 * R⁻¹) Filter.atTop (nhds 0) := by    simpa using (tendsto_const_nhds.mul tendsto_inv_atTop_zero : Filter.Tendsto      (fun R : ℝ => 4 * R⁻¹) Filter.atTop (nhds (4 * 0)))  have htail_event : ∀ᶠ R : ℝ in Filter.atTop, 4 * R⁻¹ < η :=    htail_lim.eventually (gt_mem_nhds hη)  have hlarge : ∀ᶠ R : ℝ in Filter.atTop, 1 ≤ R := Filter.eventually_ge_atTop 1  rcases Filter.eventually_atTop.1 (hL_event.and (htail_event.and hlarge)) with ⟨R, hR⟩  have hFR_dist : dist (∫ x in (0 : ℝ)..R, Real.sinc x) L < η := (hR R le_rfl).1  have htail_small : 4 * R⁻¹ < η := (hR R le_rfl).2.1  have hR_one : 1 ≤ R := (hR R le_rfl).2.2  have hR_pos : 0 < R := zero_lt_one.trans_le hR_one  have hfinite_event :      ∀ᶠ a : ℝ in 𝓝[>] (0 : ℝ),        dist (∫ x in (0 : ℝ)..R, Real.exp (-a * x) * Real.sinc x)          (∫ x in (0 : ℝ)..R, Real.sinc x) < η :=    Metric.tendsto_nhds.mp (tendsto_intervalIntegral_exp_neg_mul_sinc_nhdsGT_zero R) η hη  filter_upwards [hfinite_event, self_mem_nhdsWithin] with a hfinite ha_mem  have ha : 0 < a := ha_mem  let g : ℝ → ℝ := fun x => Real.exp (-a * x) * Real.sinc x  let D : ℝ := ∫ x in (0 : ℝ)..R, g x  let F : ℝ := ∫ x in (0 : ℝ)..R, Real.sinc x  let T : ℝ := ∫ x : ℝ in Set.Ioi R, g x  let G : ℝ := ∫ x : ℝ in Set.Ioi 0, g x  have hg0 : IntegrableOn g (Set.Ioi 0) := by    dsimp [g]    exact integrableOn_exp_neg_mul_sinc a ha  have hgR : IntegrableOn g (Set.Ioi R) := by    exact hg0.mono_set (Set.Ioi_subset_Ioi hR_pos.le)  have hsplit : D + T = G := by    dsimp [D, T, G, g]    exact intervalIntegral.integral_interval_add_Ioi hg0 hgR  have hfinite_norm : ‖D - F‖ < η := by    simpa [D, F, g, Real.dist_eq, Real.norm_eq_abs] using hfinite  have hFR_norm : ‖F - L‖ < η := by    simpa [F, Real.dist_eq, Real.norm_eq_abs] using hFR_dist  have htail_norm : ‖T‖ < η := by    have htail_le : ‖T‖ ≤ 4 * R⁻¹ := by      dsimp [T, g]      exact norm_integral_Ioi_exp_neg_mul_sinc_tail_le ha hR_one    exact lt_of_le_of_lt htail_le htail_small  have htriangle :      ‖G - L‖ ≤ ‖D - F‖ + ‖T‖ + ‖F - L‖ := by    calc      ‖G - L‖ = ‖(D - F) + T + (F - L)‖ := by        rw [← hsplit]        congr 1        ring      _ ≤ ‖(D - F) + T‖ + ‖F - L‖ := norm_add_le _ _      _ ≤ (‖D - F‖ + ‖T‖) + ‖F - L‖ := by        simpa [add_comm, add_left_comm, add_assoc] using          add_le_add_right (norm_add_le (D - F) T) ‖F - L‖      _ = ‖D - F‖ + ‖T‖ + ‖F - L‖ := by ring  have hsum : ‖D - F‖ + ‖T‖ + ‖F - L‖ < ε := by    have hsum_eta : ‖D - F‖ + ‖T‖ + ‖F - L‖ < η + η + η := by      nlinarith [hfinite_norm, htail_norm, hFR_norm]    have heta : η + η + η < ε := by      dsimp [η]      nlinarith [hε]    exact lt_trans hsum_eta heta  have hG : dist G L < ε := by    simpa [Real.dist_eq, Real.norm_eq_abs] using lt_of_le_of_lt htriangle hsum  simpa [G, g] using hG