norm_sin_div_kernel_tail_le_integral_norm

theorem norm_sin_div_kernel_tail_le_integral_norm    {f : ℝ → E} (hf : Integrable f) (x T : ℝ) {R : ℝ} (hR : 0 < R) :    ‖(∫ 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)‖ ≤      (1 / (π * R)) * ∫ u : ℝ, ‖f u‖ := by  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  have htail_eq :      (∫ 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  rw [htail_eq]  let C : ℝ := 1 / (π * R)  have hC_nonneg : 0 ≤ C := by    dsimp [C]    positivity  have hfx : Integrable (fun u : ℝ => f (x - u)) := hf.comp_sub_left x  have hbound_int : Integrable (fun u : ℝ => C * ‖f (x - u)‖) :=    hfx.norm.const_mul C  have hmono : ∀ᵐ u ∂(volume.restrict (Set.Ioc (-R) R)ᶜ),      ‖k u‖ ≤ C * ‖f (x - u)‖ := by    filter_upwards [MeasureTheory.self_mem_ae_restrict measurableSet_Ioc.compl] with u hucomp    dsimp [k, C]    have hu_not : u ∉ Set.Ioc (-R) R := by simpa using hucomp    have hR_abs : R ≤ |u| := le_abs_of_notMem_Ioc_neg_pos hR hu_not    have hu_ne : u ≠ 0 := by      intro h0      apply hu_not      have hzmem : (0 : ℝ) ∈ Set.Ioc (-R) R := ⟨by linarith, hR.le⟩      simpa [h0] using hzmem    rw [if_neg hu_ne, norm_smul]    have hscalar : ‖(Real.sin (T * u) / (π * u) : ℂ)‖ ≤ C := by      dsimp [C]      rw [norm_div, norm_mul, Complex.norm_real, Complex.norm_real, Complex.norm_real]      simp only [Real.norm_eq_abs]      rw [abs_of_pos Real.pi_pos]      have hsin : |Real.sin (T * u)| ≤ 1 := Real.abs_sin_le_one (T * u)      have hden : π * R ≤ π * |u| :=        mul_le_mul_of_nonneg_left hR_abs Real.pi_pos.le      have hden_pos : 0 < π * R := mul_pos Real.pi_pos hR      calc        |Real.sin (T * u)| / (π * |u|) ≤ 1 / (π * |u|) := by          exact div_le_div_of_nonneg_right hsin            (mul_nonneg Real.pi_pos.le (abs_nonneg u))        _ ≤ 1 / (π * R) := by          simpa [one_div] using inv_anti₀ hden_pos hden    exact mul_le_mul hscalar le_rfl (norm_nonneg _) hC_nonneg  have hnorm_le : ‖∫ u in (Set.Ioc (-R) R)ᶜ, k u‖ ≤      ∫ u in (Set.Ioc (-R) R)ᶜ, C * ‖f (x - u)‖ := by    calc      ‖∫ u in (Set.Ioc (-R) R)ᶜ, k u‖          ≤ ∫ u in (Set.Ioc (-R) R)ᶜ, ‖k u‖ := norm_integral_le_integral_norm _      _ ≤ ∫ u in (Set.Ioc (-R) R)ᶜ, C * ‖f (x - u)‖ := by        exact integral_mono_ae (hk.norm.mono_measure Measure.restrict_le_self)          (hbound_int.mono_measure Measure.restrict_le_self) hmono  have hset_le : (∫ u in (Set.Ioc (-R) R)ᶜ, C * ‖f (x - u)‖) ≤      ∫ u : ℝ, C * ‖f (x - u)‖ := by    exact integral_mono_measure Measure.restrict_le_self      (Filter.Eventually.of_forall fun _u => mul_nonneg hC_nonneg (norm_nonneg _)) hbound_int  have htranslate : (∫ u : ℝ, C * ‖f (x - u)‖) = C * ∫ u : ℝ, ‖f u‖ := by    rw [integral_const_mul]    congr 1    calc      (∫ u : ℝ, ‖f (x - u)‖) = ∫ u : ℝ, ‖f (x + u)‖ := by        simpa [sub_eq_add_neg] using          integral_neg_eq_self (f := fun u : ℝ => ‖f (x + u)‖) (μ := volume)      _ = ∫ u : ℝ, ‖f u‖ := by        simpa using integral_add_left_eq_self (μ := volume) (fun u : ℝ => ‖f u‖) x  exact hnorm_le.trans (hset_le.trans_eq htranslate)