Kadiri.sin_div_error_pointwise_bound_of_convex

theorem sin_div_error_pointwise_bound_of_convex    {g : ℝ → ℂ} {s : Set ℝ} (hs : Convex ℝ s) {D x T u : ℝ}    (hD : 0 ≤ D) (hx : x ∈ s) (hxu : x - u ∈ s)    (hgdiff : ∀ y ∈ s, DifferentiableAt ℝ g y)    (hderiv : ∀ y ∈ s, ‖deriv g y‖ ≤ D) :    ‖(if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (Real.pi * u) : ℂ)) •        (g (x - u) - g x)‖ ≤ D / Real.pi := by  by_cases hu : u = 0  · simp [hu, div_nonneg hD Real.pi_pos.le]  · rw [if_neg hu, norm_smul]    have hscalar :        ‖(Real.sin (T * u) / (Real.pi * u) : ℂ)‖ ≤ 1 / (Real.pi * |u|) := by      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 _      exact div_le_div_of_nonneg_right hsin        (mul_nonneg Real.pi_pos.le (abs_nonneg u))    have hdiff : ‖g (x - u) - g x‖ ≤ D * |u| := by      have hmv := hs.norm_image_sub_le_of_norm_deriv_le hgdiff hderiv hx hxu      have hnorm : ‖(x - u) - x‖ = |u| := by        rw [Real.norm_eq_abs]        have hsub : (x - u) - x = -u := by ring        rw [hsub, abs_neg]      simpa [hnorm] using hmv    have hupper_nonneg : 0 ≤ 1 / (Real.pi * |u|) := by positivity    calc      ‖(Real.sin (T * u) / (Real.pi * u) : ℂ)‖ * ‖g (x - u) - g x‖          ≤ (1 / (Real.pi * |u|)) * (D * |u|) := by            exact mul_le_mul hscalar hdiff (norm_nonneg _) hupper_nonneg      _ = D / Real.pi := by            field_simp [Real.pi_ne_zero, abs_pos.mpr hu]