theorem integrableOn_g_Ioc (f : ℝ → ℝ) (hf_mono : Monotone f) (a b : ℝ) (ha : 0 < a) (hab : a ≤ b) : MeasureTheory.IntegrableOn (fun (t : ℝ) => (f t - t) / t ^ 2) (Set.Ioc a b) MeasureTheory.volume

theorem setIntegral_Ioc_split (g : ℝ → ℝ) (a b c : ℝ) (hab : a ≤ b) (hbc : b ≤ c) (hg1 : MeasureTheory.IntegrableOn g (Set.Ioc a b) MeasureTheory.volume) (hg2 : MeasureTheory.IntegrableOn g (Set.Ioc b c) MeasureTheory.volume) : ∫ (t : ℝ) in Set.Ioc a c, g t = (∫ (t : ℝ) in Set.Ioc a b, g t) + ∫ (t : ℝ) in Set.Ioc b c, g t