tendsto_intervalIntegral_sin_div_kernel_error_of_intervalIntegrable_quotient

theorem tendsto_intervalIntegral_sin_div_kernel_error_of_intervalIntegrable_quotient    {f : ℝ → E} {x R : ℝ} (hR : 0 < R)    (hq : IntervalIntegrable      (fun u : ℝ =>        if u = 0 then 0 else (1 / (π * u) : ℂ) • (f (x - u) - f x))      volume (-R) R) :    Filter.Tendsto      (fun T : ℝ =>        ∫ u in (-R)..R,          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •            (f (x - u) - f x))      Filter.atTop (nhds 0) := by  let q : ℝ → E := fun u =>    if u = 0 then 0 else (1 / (π * u) : ℂ) • (f (x - u) - f x)  let qWindow : ℝ → E := Set.Ioc (-R) R |>.indicator q  have hle : -R ≤ R := by linarith  have hqIoc : IntegrableOn q (Set.Ioc (-R) R) := by    simpa [q] using (intervalIntegrable_iff_integrableOn_Ioc_of_le hle).1 hq  have hqWindow : Integrable qWindow := by    exact hqIoc.integrable_indicator measurableSet_Ioc  have hlim := tendsto_integral_sin_mul_smul_atTop (E := E) hqWindow  refine hlim.congr' ?_  filter_upwards with T  have hinterval :      (∫ u in (-R)..R,          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •            (f (x - u) - f x)) =        ∫ u in (-R)..R, (Real.sin (T * u) : ℂ) • q u := by    apply intervalIntegral.integral_congr    intro u _hu    dsimp [q]    exact sin_div_kernel_sub_eq_sin_smul_quotient (E := E) f x T u  rw [hinterval, intervalIntegral.integral_of_le hle]  dsimp [qWindow]  rw [← integral_indicator measurableSet_Ioc]  congr with u  by_cases hu : u ∈ Set.Ioc (-R) R  · simp [Set.indicator_of_mem hu]  · simp [Set.indicator_of_notMem hu]