norm_tail_quotient_le

lemma norm_tail_quotient_le    {f : ℝ → E} (x : ℝ) {R : ℝ} (hR : 0 < R) (u : ℝ) :    ‖(Set.Ioc (-R) R)ᶜ.indicator        (fun u : ℝ => (if u = 0 then (0 : ℂ) else (1 / (π * u) : ℂ)) •          f (x - u)) u‖ ≤      (1 / (π * R)) * ‖f (x - u)‖ := by  by_cases huSet : u ∈ (Set.Ioc (-R) R)ᶜ  · rw [Set.indicator_of_mem huSet]    have hu_not : u ∉ Set.Ioc (-R) R := by simpa using huSet    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        exact ⟨by linarith, hR.le⟩      simpa [h0] using hzmem    rw [if_neg hu_ne, norm_smul]    have hscalar : ‖(1 / (π * u) : ℂ)‖ ≤ 1 / (π * R) := by      rw [norm_div, norm_one, norm_mul, Complex.norm_real, Complex.norm_real]      simp only [Real.norm_eq_abs, one_div]      rw [abs_of_pos Real.pi_pos]      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      simpa [mul_comm, mul_left_comm, mul_assoc] using inv_anti₀ hden_pos hden    exact mul_le_mul hscalar le_rfl (norm_nonneg _)      (div_nonneg zero_le_one (mul_pos Real.pi_pos hR).le)  · rw [Set.indicator_of_notMem huSet]    simpa using mul_nonneg (div_nonneg zero_le_one (mul_pos Real.pi_pos hR).le)      (norm_nonneg (f (x - u)))