integrable_tail_quotient_of_integrable

theorem integrable_tail_quotient_of_integrable    {f : ℝ → E} (hf : Integrable f) (x : ℝ) {R : ℝ} (hR : 0 < R) :    Integrable ((Set.Ioc (-R) R)ᶜ.indicator      (fun u : ℝ => (if u = 0 then (0 : ℂ) else (1 / (π * u) : ℂ)) •        f (x - u))) := by  have hfx : Integrable (fun u : ℝ => f (x - u)) := hf.comp_sub_left x  let C : ℂ := (1 / (π * R) : ℝ)  have hC_nonneg : 0 ≤ 1 / (π * R) :=    div_nonneg zero_le_one (mul_pos Real.pi_pos hR).le  have hboundInt : Integrable (fun u : ℝ => C • f (x - u)) := hfx.smul C  refine hboundInt.mono ?_ ?_  · have hscalar_meas : Measurable        (fun u : ℝ => if u = 0 then (0 : ℂ) else (1 / (π * u) : ℂ)) := by      refine Measurable.ite measurableSet_eq measurable_const ?_      fun_prop    exact (hscalar_meas.aestronglyMeasurable.smul hfx.aestronglyMeasurable).indicator      measurableSet_Ioc.compl  · filter_upwards with u    rw [norm_smul]    have hCnorm : ‖C‖ = 1 / (π * R) := by      rw [show C = ((1 / (π * R) : ℝ) : ℂ) by rfl, Complex.norm_real, Real.norm_eq_abs,        abs_of_nonneg hC_nonneg]    rw [hCnorm]    exact norm_tail_quotient_le (E := E) x hR u