tendsto_sin_div_kernel_tail_of_integrable

theorem tendsto_sin_div_kernel_tail_of_integrable    {f : ℝ → E} (hf : Integrable f) {x R : ℝ} (hR : 0 < R) :    Filter.Tendsto      (fun T : ℝ =>        (∫ u : ℝ,          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •            f (x - u)) -          ∫ u in (-R)..R,            (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •              f (x - u))      Filter.atTop (nhds 0) := by  let qTail : ℝ → E := (Set.Ioc (-R) R)ᶜ.indicator    (fun u : ℝ => (if u = 0 then (0 : ℂ) else (1 / (π * u) : ℂ)) •      f (x - u))  have hqTail : Integrable qTail := by    simpa [qTail] using integrable_tail_quotient_of_integrable (E := E) hf x hR  have hlim := tendsto_integral_sin_mul_smul_atTop (E := E) hqTail  refine hlim.congr' ?_  filter_upwards with T  let k : ℝ → E := fun u =>    (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) • f (x - u)  have hk : Integrable k :=    integrable_sin_div_kernel_smul_of_integrable (E := E) hf x T  have hle : -R ≤ R := by linarith  symm  calc    (∫ u : ℝ,        (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •          f (x - u)) -        ∫ u in (-R)..R,          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •            f (x - u)        = ∫ u in (Set.Ioc (-R) R)ᶜ, k u := by          rw [intervalIntegral.integral_of_le hle]          have hdecomp := integral_add_compl (s := Set.Ioc (-R) R) measurableSet_Ioc hk          dsimp [k] at hdecomp          rw [← hdecomp]          abel    _ = ∫ u : ℝ, (Set.Ioc (-R) R)ᶜ.indicator k u := by          rw [integral_indicator measurableSet_Ioc.compl]    _ = ∫ u : ℝ, (Real.sin (T * u) : ℂ) • qTail u := by          apply integral_congr_ae          filter_upwards with u          dsimp [k, qTail]          exact tail_indicator_sin_div_eq_sin_smul_quotient (E := E) f x T hR u