intervalIntegral_sinc_tail_eq_ibp

theorem intervalIntegral_sinc_tail_eq_ibp {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) :    ∫ x in a..b, Real.sinc x =      (-Real.cos b / b + Real.cos a / a) -        ∫ x in a..b, Real.cos x / x ^ 2 := by  have hpos_uIcc : ∀ x ∈ Set.uIcc a b, 0 < x := by    intro x hx    rw [Set.uIcc_of_le hab] at hx    exact ha.trans_le hx.1  have hsinc :      (∫ x in a..b, Real.sinc x) = ∫ x in a..b, x⁻¹ * Real.sin x := by    refine intervalIntegral.integral_congr ?_    intro x hx    have hx0 : x ≠ 0 := (hpos_uIcc x hx).ne'    rw [Real.sinc_of_ne_zero hx0]    ring  have hu : ∀ x ∈ Set.uIcc a b,      HasDerivAt (fun y : ℝ => y⁻¹) (-(x ^ 2)⁻¹) x := by    intro x hx    exact hasDerivAt_inv (hpos_uIcc x hx).ne'  have hv : ∀ x ∈ Set.uIcc a b,      HasDerivAt (fun y : ℝ => -Real.cos y) (Real.sin x) x := by    intro x _hx    have h : HasDerivAt (fun y : ℝ => -Real.cos y) (-(-Real.sin x)) x :=      (Real.hasDerivAt_cos x).neg    rwa [neg_neg] at h  have hu' : 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 (by simpa [Set.uIcc_of_le hab] using hx)).ne').neg  have hv' : IntervalIntegrable (fun x : ℝ => Real.sin x) volume a b :=    Real.continuous_sin.intervalIntegrable a b  have hIBP := intervalIntegral.integral_mul_deriv_eq_deriv_mul    (u := fun x : ℝ => x⁻¹) (v := fun x : ℝ => -Real.cos x)    (u' := fun x : ℝ => -(x ^ 2)⁻¹) (v' := fun x : ℝ => Real.sin x)    hu hv hu' hv'  have hint :      (∫ x in a..b, (-(x ^ 2)⁻¹) * -Real.cos x) =        ∫ x in a..b, Real.cos x / x ^ 2 := by    apply intervalIntegral.integral_congr    intro x _hx    field_simp [sq]  rw [hsinc, hIBP, hint]  ring_nf