feat (measure_theory/integral): lemmas integral_Ioi_eq_integral_Ici…

… etc (#18899)

We already have some lemmas relating integrals over open vs. closed intervals, but some were missing (notably half-infinite integrals). This should now be a full set.



Co-authored-by: sgouezel <[email protected]>

src/measure_theory/integral/integrable_on.lean

@@ -563,3 +563,100 @@ lemma continuous_on.strongly_measurable_at_filter_nhds_within {α β : Type*} [m
   (hf : continuous_on f s) (hs : measurable_set s) (x : α) :
   strongly_measurable_at_filter f (𝓝[s] x) μ :=
 ⟨s, self_mem_nhds_within, hf.ae_strongly_measurable hs⟩
+
+/-! ### Lemmas about adding and removing interval boundaries
+
+The primed lemmas take explicit arguments about the measure being finite at the endpoint, while
+the unprimed ones use `[has_no_atoms μ]`.
+-/
+
+section partial_order
+
+variables [partial_order α] [measurable_singleton_class α]
+  {f : α → E} {μ : measure α} {a b : α}
+
+lemma integrable_on_Icc_iff_integrable_on_Ioc' (ha : μ {a} ≠ ∞) :
+  integrable_on f (Icc a b) μ ↔ integrable_on f (Ioc a b) μ :=
+begin
+  by_cases hab : a ≤ b,
+  { rw [←Ioc_union_left hab, integrable_on_union, eq_true_intro
+      (integrable_on_singleton_iff.mpr $ or.inr ha.lt_top), and_true] },
+  { rw [Icc_eq_empty hab, Ioc_eq_empty],
+    contrapose! hab,
+    exact hab.le }
+end
+
+lemma integrable_on_Icc_iff_integrable_on_Ico' (hb : μ {b} ≠ ∞) :
+  integrable_on f (Icc a b) μ ↔ integrable_on f (Ico a b) μ :=
+begin
+  by_cases hab : a ≤ b,
+  { rw [←Ico_union_right hab, integrable_on_union, eq_true_intro
+      (integrable_on_singleton_iff.mpr $ or.inr hb.lt_top), and_true] },
+  { rw [Icc_eq_empty hab, Ico_eq_empty],
+    contrapose! hab,
+    exact hab.le }
+end
+
+lemma integrable_on_Ico_iff_integrable_on_Ioo' (ha : μ {a} ≠ ∞) :
+  integrable_on f (Ico a b) μ ↔ integrable_on f (Ioo a b) μ :=
+begin
+  by_cases hab : a < b,
+  { rw [←Ioo_union_left hab, integrable_on_union, eq_true_intro
+      (integrable_on_singleton_iff.mpr $ or.inr ha.lt_top), and_true] },
+  { rw [Ioo_eq_empty hab, Ico_eq_empty hab] }
+end
+
+lemma integrable_on_Ioc_iff_integrable_on_Ioo' (hb : μ {b} ≠ ∞) :
+  integrable_on f (Ioc a b) μ ↔ integrable_on f (Ioo a b) μ :=
+begin
+  by_cases hab : a < b,
+  { rw [←Ioo_union_right hab, integrable_on_union, eq_true_intro
+      (integrable_on_singleton_iff.mpr $ or.inr hb.lt_top), and_true] },
+  { rw [Ioo_eq_empty hab, Ioc_eq_empty hab] }
+end
+
+lemma integrable_on_Icc_iff_integrable_on_Ioo' (ha : μ {a} ≠ ∞) (hb : μ {b} ≠ ∞) :
+  integrable_on f (Icc a b) μ ↔ integrable_on f (Ioo a b) μ :=
+by rw [integrable_on_Icc_iff_integrable_on_Ioc' ha, integrable_on_Ioc_iff_integrable_on_Ioo' hb]
+
+lemma integrable_on_Ici_iff_integrable_on_Ioi' (hb : μ {b} ≠ ∞) :
+  integrable_on f (Ici b) μ ↔ integrable_on f (Ioi b) μ :=
+by rw [←Ioi_union_left, integrable_on_union,
+  eq_true_intro (integrable_on_singleton_iff.mpr $ or.inr hb.lt_top), and_true]
+
+lemma integrable_on_Iic_iff_integrable_on_Iio' (hb : μ {b} ≠ ∞) :
+  integrable_on f (Iic b) μ ↔ integrable_on f (Iio b) μ :=
+by rw [←Iio_union_right, integrable_on_union,
+  eq_true_intro (integrable_on_singleton_iff.mpr $ or.inr hb.lt_top), and_true]
+
+variables [has_no_atoms μ]
+
+lemma integrable_on_Icc_iff_integrable_on_Ioc :
+  integrable_on f (Icc a b) μ ↔ integrable_on f (Ioc a b) μ :=
+integrable_on_Icc_iff_integrable_on_Ioc' (by { rw measure_singleton, exact ennreal.zero_ne_top })
+
+lemma integrable_on_Icc_iff_integrable_on_Ico :
+  integrable_on f (Icc a b) μ ↔ integrable_on f (Ico a b) μ :=
+integrable_on_Icc_iff_integrable_on_Ico' (by { rw measure_singleton, exact ennreal.zero_ne_top })
+
+lemma integrable_on_Ico_iff_integrable_on_Ioo :
+  integrable_on f (Ico a b) μ ↔ integrable_on f (Ioo a b) μ :=
+integrable_on_Ico_iff_integrable_on_Ioo' (by { rw measure_singleton, exact ennreal.zero_ne_top })
+
+lemma integrable_on_Ioc_iff_integrable_on_Ioo :
+  integrable_on f (Ioc a b) μ ↔ integrable_on f (Ioo a b) μ :=
+integrable_on_Ioc_iff_integrable_on_Ioo' (by { rw measure_singleton, exact ennreal.zero_ne_top })
+
+lemma integrable_on_Icc_iff_integrable_on_Ioo :
+  integrable_on f (Icc a b) μ ↔ integrable_on f (Ioo a b) μ :=
+by rw [integrable_on_Icc_iff_integrable_on_Ioc, integrable_on_Ioc_iff_integrable_on_Ioo]
+
+lemma integrable_on_Ici_iff_integrable_on_Ioi :
+  integrable_on f (Ici b) μ ↔ integrable_on f (Ioi b) μ :=
+integrable_on_Ici_iff_integrable_on_Ioi' (by { rw measure_singleton, exact ennreal.zero_ne_top })
+
+lemma integrable_on_Iic_iff_integrable_on_Iio :
+  integrable_on f (Iic b) μ ↔ integrable_on f (Iio b) μ :=
+integrable_on_Iic_iff_integrable_on_Iio' (by { rw measure_singleton, exact ennreal.zero_ne_top })
+
+end partial_order

src/measure_theory/integral/interval_integral.lean

@@ -83,39 +83,6 @@ lemma interval_integrable_iff_integrable_Ioc_of_le (hab : a ≤ b) :
   interval_integrable f μ a b ↔ integrable_on f (Ioc a b) μ :=
 by rw [interval_integrable_iff, uIoc_of_le hab]
 
-lemma integrable_on_Icc_iff_integrable_on_Ioc' {f : ℝ → E} (ha : μ {a} ≠ ∞) :
-  integrable_on f (Icc a b) μ ↔ integrable_on f (Ioc a b) μ :=
-begin
-  cases le_or_lt a b with hab hab,
-  { have : Icc a b = Icc a a ∪ Ioc a b := (Icc_union_Ioc_eq_Icc le_rfl hab).symm,
-    rw [this, integrable_on_union],
-    simp [ha.lt_top] },
-  { simp [hab, hab.le] },
-end
-
-lemma integrable_on_Icc_iff_integrable_on_Ioc [has_no_atoms μ] {f : ℝ → E} {a b : ℝ} :
-  integrable_on f (Icc a b) μ ↔ integrable_on f (Ioc a b) μ :=
-integrable_on_Icc_iff_integrable_on_Ioc' (by simp)
-
-lemma integrable_on_Ioc_iff_integrable_on_Ioo'
-  {f : ℝ → E} {a b : ℝ} (hb : μ {b} ≠ ∞) :
-  integrable_on f (Ioc a b) μ ↔ integrable_on f (Ioo a b) μ :=
-begin
-  cases lt_or_le a b with hab hab,
-  { have : Ioc a b = Ioo a b ∪ Icc b b := (Ioo_union_Icc_eq_Ioc hab le_rfl).symm,
-    rw [this, integrable_on_union],
-    simp [hb.lt_top] },
-  { simp [hab] },
-end
-
-lemma integrable_on_Ioc_iff_integrable_on_Ioo [has_no_atoms μ] {f : ℝ → E} {a b : ℝ} :
-  integrable_on f (Ioc a b) μ ↔ integrable_on f (Ioo a b) μ :=
-integrable_on_Ioc_iff_integrable_on_Ioo' (by simp)
-
-lemma integrable_on_Icc_iff_integrable_on_Ioo [has_no_atoms μ] {f : ℝ → E} {a b : ℝ} :
-  integrable_on f (Icc a b) μ ↔ integrable_on f (Ioo a b) μ :=
-by rw [integrable_on_Icc_iff_integrable_on_Ioc, integrable_on_Ioc_iff_integrable_on_Ioo]
-
 lemma interval_integrable_iff' [has_no_atoms μ] :
   interval_integrable f μ a b ↔ integrable_on f (uIcc a b) μ :=
 by rw [interval_integrable_iff, ←Icc_min_max, uIoc, integrable_on_Icc_iff_integrable_on_Ioc]
@@ -125,18 +92,6 @@ lemma interval_integrable_iff_integrable_Icc_of_le
   interval_integrable f μ a b ↔ integrable_on f (Icc a b) μ :=
 by rw [interval_integrable_iff_integrable_Ioc_of_le hab, integrable_on_Icc_iff_integrable_on_Ioc]
 
-lemma integrable_on_Ici_iff_integrable_on_Ioi' {f : ℝ → E} (ha : μ {a} ≠ ∞) :
-  integrable_on f (Ici a) μ ↔ integrable_on f (Ioi a) μ :=
-begin
-  have : Ici a = Icc a a ∪ Ioi a := (Icc_union_Ioi_eq_Ici le_rfl).symm,
-  rw [this, integrable_on_union],
-  simp [ha.lt_top]
-end
-
-lemma integrable_on_Ici_iff_integrable_on_Ioi [has_no_atoms μ] {f : ℝ → E} :
-  integrable_on f (Ici a) μ ↔ integrable_on f (Ioi a) μ :=
-integrable_on_Ici_iff_integrable_on_Ioi' (by simp)
-
 /-- If a function is integrable with respect to a given measure `μ` then it is interval integrable
   with respect to `μ` on `uIcc a b`. -/
 lemma measure_theory.integrable.interval_integrable (hf : integrable f μ) :

src/measure_theory/integral/set_integral.lean

@@ -593,22 +593,69 @@ lemma set_integral_trim {α} {m m0 : measurable_space α} {μ : measure α} (hm
   ∫ x in s, f x ∂μ = ∫ x in s, f x ∂(μ.trim hm) :=
 by rwa [integral_trim hm hf_meas, restrict_trim hm μ]
 
-lemma integral_Icc_eq_integral_Ioc' [partial_order α] {f : α → E} {a b : α} (ha : μ {a} = 0) :
+/-! ### Lemmas about adding and removing interval boundaries
+
+The primed lemmas take explicit arguments about the endpoint having zero measure, while the
+unprimed ones use `[has_no_atoms μ]`.
+-/
+
+section partial_order
+
+variables [partial_order α] {a b : α}
+
+lemma integral_Icc_eq_integral_Ioc' (ha : μ {a} = 0) :
   ∫ t in Icc a b, f t ∂μ = ∫ t in Ioc a b, f t ∂μ :=
 set_integral_congr_set_ae (Ioc_ae_eq_Icc' ha).symm
 
-lemma integral_Ioc_eq_integral_Ioo' [partial_order α] {f : α → E} {a b : α} (hb : μ {b} = 0) :
+lemma integral_Icc_eq_integral_Ico' (hb : μ {b} = 0) :
+  ∫ t in Icc a b, f t ∂μ = ∫ t in Ico a b, f t ∂μ :=
+set_integral_congr_set_ae (Ico_ae_eq_Icc' hb).symm
+
+lemma integral_Ioc_eq_integral_Ioo' (hb : μ {b} = 0) :
   ∫ t in Ioc a b, f t ∂μ = ∫ t in Ioo a b, f t ∂μ :=
 set_integral_congr_set_ae (Ioo_ae_eq_Ioc' hb).symm
 
-lemma integral_Icc_eq_integral_Ioc [partial_order α] {f : α → E} {a b : α} [has_no_atoms μ] :
-  ∫ t in Icc a b, f t ∂μ = ∫ t in Ioc a b, f t ∂μ :=
+lemma integral_Ico_eq_integral_Ioo' (ha : μ {a} = 0) :
+  ∫ t in Ico a b, f t ∂μ = ∫ t in Ioo a b, f t ∂μ :=
+set_integral_congr_set_ae (Ioo_ae_eq_Ico' ha).symm
+
+lemma integral_Icc_eq_integral_Ioo' (ha : μ {a} = 0) (hb : μ {b} = 0) :
+  ∫ t in Icc a b, f t ∂μ = ∫ t in Ioo a b, f t ∂μ :=
+set_integral_congr_set_ae (Ioo_ae_eq_Icc' ha hb).symm
+
+lemma integral_Iic_eq_integral_Iio' (ha : μ {a} = 0) :
+  ∫ t in Iic a, f t ∂μ = ∫ t in Iio a, f t ∂μ :=
+set_integral_congr_set_ae (Iio_ae_eq_Iic' ha).symm
+
+lemma integral_Ici_eq_integral_Ioi' (ha : μ {a} = 0) :
+  ∫ t in Ici a, f t ∂μ = ∫ t in Ioi a, f t ∂μ :=
+set_integral_congr_set_ae (Ioi_ae_eq_Ici' ha).symm
+
+variable [has_no_atoms μ]
+
+lemma integral_Icc_eq_integral_Ioc : ∫ t in Icc a b, f t ∂μ = ∫ t in Ioc a b, f t ∂μ :=
 integral_Icc_eq_integral_Ioc' $ measure_singleton a
 
-lemma integral_Ioc_eq_integral_Ioo [partial_order α] {f : α → E} {a b : α} [has_no_atoms μ] :
-  ∫ t in Ioc a b, f t ∂μ = ∫ t in Ioo a b, f t ∂μ :=
+lemma integral_Icc_eq_integral_Ico : ∫ t in Icc a b, f t ∂μ = ∫ t in Ico a b, f t ∂μ :=
+integral_Icc_eq_integral_Ico' $ measure_singleton b
+
+lemma integral_Ioc_eq_integral_Ioo : ∫ t in Ioc a b, f t ∂μ = ∫ t in Ioo a b, f t ∂μ :=
 integral_Ioc_eq_integral_Ioo' $ measure_singleton b
 
+lemma integral_Ico_eq_integral_Ioo : ∫ t in Ico a b, f t ∂μ = ∫ t in Ioo a b, f t ∂μ :=
+integral_Ico_eq_integral_Ioo' $ measure_singleton a
+
+lemma integral_Icc_eq_integral_Ioo : ∫ t in Icc a b, f t ∂μ = ∫ t in Ico a b, f t ∂μ :=
+by rw [integral_Icc_eq_integral_Ico, integral_Ico_eq_integral_Ioo]
+
+lemma integral_Iic_eq_integral_Iio : ∫ t in Iic a, f t ∂μ = ∫ t in Iio a, f t ∂μ :=
+integral_Iic_eq_integral_Iio' $ measure_singleton a
+
+lemma integral_Ici_eq_integral_Ioi : ∫ t in Ici a, f t ∂μ = ∫ t in Ioi a, f t ∂μ :=
+integral_Ici_eq_integral_Ioi' $ measure_singleton a
+
+end partial_order
+
 end normed_add_comm_group
 
 section mono