norm_intervalIntegral_sinc_tail_le

theorem norm_intervalIntegral_sinc_tail_le {a b : ℝ} (ha : 1 ≤ a) (hab : a ≤ b) :    ‖∫ x in a..b, Real.sinc x‖ ≤ 3 * a⁻¹ := by  have ha_pos : 0 < a := zero_lt_one.trans_le ha  have hb_pos : 0 < b := ha_pos.trans_le hab  have hpos_uIcc : ∀ x ∈ Set.Icc a b, 0 < x := by    intro x hx    exact ha_pos.trans_le hx.1  have hboundary : ‖-Real.cos b / b + Real.cos a / a‖ ≤ 2 * a⁻¹ := by    calc      ‖-Real.cos b / b + Real.cos a / a‖          = |(-Real.cos b / b) + (Real.cos a / a)| := by rw [Real.norm_eq_abs]      _ ≤ |-Real.cos b / b| + |Real.cos a / a| := abs_add_le _ _      _ ≤ b⁻¹ + a⁻¹ := by            refine add_le_add ?_ ?_            · calc                |-Real.cos b / b| = |Real.cos b| / b := by                  rw [abs_div, abs_neg, abs_of_pos hb_pos]                _ ≤ 1 / b := div_le_div_of_nonneg_right (Real.abs_cos_le_one b) hb_pos.le                _ = b⁻¹ := by rw [one_div]            · calc                |Real.cos a / a| = |Real.cos a| / a := by                  rw [abs_div, abs_of_pos ha_pos]                _ ≤ 1 / a := div_le_div_of_nonneg_right (Real.abs_cos_le_one a) ha_pos.le                _ = a⁻¹ := by rw [one_div]      _ ≤ a⁻¹ + a⁻¹ := by            exact add_le_add (by              simpa [one_div] using one_div_le_one_div_of_le ha_pos hab) le_rfl      _ = 2 * a⁻¹ := by ring  have hnormInt : IntervalIntegrable (fun x : ℝ => ‖Real.cos x / x ^ 2‖) volume a b := by    apply ContinuousOn.intervalIntegrable_of_Icc hab    exact ((Real.continuous_cos.continuousOn).div (continuousOn_pow 2) fun x hx => by      exact pow_ne_zero 2 (hpos_uIcc x hx).ne').norm  have hinvInt : IntervalIntegrable (fun x : ℝ => (x ^ 2)⁻¹) volume a b := by    apply ContinuousOn.intervalIntegrable_of_Icc hab    exact (continuousOn_pow 2).inv₀ fun x hx => by      exact pow_ne_zero 2 (hpos_uIcc x hx).ne'  have hJ : ‖∫ x in a..b, Real.cos x / x ^ 2‖ ≤ a⁻¹ := by    calc      ‖∫ x in a..b, Real.cos x / x ^ 2‖          ≤ ∫ x in a..b, ‖Real.cos x / x ^ 2‖ :=            intervalIntegral.norm_integral_le_integral_norm hab      _ ≤ ∫ x in a..b, (x ^ 2)⁻¹ := by            refine intervalIntegral.integral_mono_on hab hnormInt hinvInt ?_            intro x hx            have hx_pos : 0 < x := hpos_uIcc x hx            calc              ‖Real.cos x / x ^ 2‖ = |Real.cos x| / x ^ 2 := by                rw [Real.norm_eq_abs, abs_div, abs_of_pos (pow_pos hx_pos 2)]              _ ≤ 1 / x ^ 2 :=                div_le_div_of_nonneg_right (Real.abs_cos_le_one x) (sq_nonneg x)              _ = (x ^ 2)⁻¹ := by rw [one_div]      _ = a⁻¹ - b⁻¹ := intervalIntegral_inv_sq_of_pos ha_pos hab      _ ≤ a⁻¹ := sub_le_self _ (inv_nonneg.mpr hb_pos.le)  rw [intervalIntegral_sinc_tail_eq_ibp ha_pos hab]  calc    ‖(-Real.cos b / b + Real.cos a / a) - ∫ x in a..b, Real.cos x / x ^ 2‖        ≤ ‖-Real.cos b / b + Real.cos a / a‖ +            ‖∫ x in a..b, Real.cos x / x ^ 2‖ := norm_sub_le _ _    _ ≤ 2 * a⁻¹ + a⁻¹ := add_le_add hboundary hJ    _ = 3 * a⁻¹ := by ring