feat(MeasureTheory/Integral/IntervalIntegral/Basic): add integral_Ioi_sub_Ioi, ...Ioi', ...Iio, ...Iio'

Author: Deep0Thinking

Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean

@@ -1106,6 +1106,30 @@ theorem integral_interval_add_Ioi' (ha : IntervalIntegrable f μ a b)
       ((intervalIntegrable_iff_integrableOn_Ioc_of_le h).1 ha) hb
   · exact hb.mono_set <| Ioi_subset_Ioi h.le
 
+theorem integral_Ioi_sub_Ioi (hf : IntegrableOn f (Ioi a) μ) (hab : a ≤ b) :
+    ∫ x in Ioi a, f x ∂μ - ∫ x in Ioi b, f x ∂μ = ∫ x in a..b, f x ∂μ :=
+  sub_eq_of_eq_add (integral_interval_add_Ioi hf (hf.mono_set (Ioi_subset_Ioi hab))).symm
+
+theorem integral_Ioi_sub_Ioi' (hf : IntegrableOn f (Ioi a) μ) (hg : IntegrableOn f (Ioi b) μ) :
+    ∫ x in Ioi a, f x ∂μ - ∫ x in Ioi b, f x ∂μ = ∫ x in a..b, f x ∂μ := by
+  wlog! hab : a ≤ b generalizing a b
+  · rw [integral_symm, ← this hg hf hab.le, neg_sub]
+  exact integral_Ioi_sub_Ioi hf hab
+
+theorem integral_Iio_sub_Iio [NoAtoms μ] (hf : IntegrableOn f (Iio b) μ) (hab : a ≤ b) :
+    ∫ x in Iio b, f x ∂μ - ∫ x in Iio a, f x ∂μ = ∫ x in a..b, f x ∂μ := by
+  simp_rw [setIntegral_congr_set Iio_ae_eq_Iic]
+  have hb : IntegrableOn f (Iic b) μ := by rwa [integrableOn_Iic_iff_integrableOn_Iio]
+  have ha : IntegrableOn f (Iic a) μ := hb.mono_set (Iic_subset_Iic.2 hab)
+  exact integral_Iic_sub_Iic ha hb
+
+theorem integral_Iio_sub_Iio' [NoAtoms μ] (hf : IntegrableOn f (Iio b) μ)
+    (hg : IntegrableOn f (Iio a) μ) :
+    ∫ x in Iio b, f x ∂μ - ∫ x in Iio a, f x ∂μ = ∫ x in a..b, f x ∂μ := by
+  wlog! hab : a ≤ b generalizing a b
+  · rw [integral_symm, ← this hg hf hab.le, neg_sub]
+  exact integral_Iio_sub_Iio hf hab
+
 theorem integral_Iic_add_Ioi (h_left : IntegrableOn f (Iic b) μ)
     (h_right : IntegrableOn f (Ioi b) μ) :
     (∫ x in Iic b, f x ∂μ) + (∫ x in Ioi b, f x ∂μ) = ∫ (x : ℝ), f x ∂μ := by