chore(measure_theory): move and rename some lemmas (#12699)

* move `ae_interval_oc_iff`, `ae_measurable_interval_oc_iff`, and `ae_interval_oc_iff'` to `measure_theory.measure.measure_space`, rename `ae_interval_oc_iff'` to `ae_restrict_interval_oc_iff`;
* add lemmas about `ae` and union of sets.

src/data/set/intervals/unordered_interval.lean

@@ -145,9 +145,12 @@ by simp [interval_oc, h]
 lemma interval_oc_of_lt (h : b < a) : Ι a b = Ioc b a :=
 by simp [interval_oc, le_of_lt h]
 
+lemma interval_oc_eq_union : Ι a b = Ioc a b ∪ Ioc b a :=
+by cases le_total a b; simp [interval_oc, *]
+
 lemma forall_interval_oc_iff  {P : α → Prop} :
   (∀ x ∈ Ι a b, P x) ↔ (∀ x ∈ Ioc a b, P x) ∧ (∀ x ∈ Ioc b a, P x) :=
-by { dsimp [interval_oc], cases le_total a b with hab hab ; simp [hab] }
+by simp only [interval_oc_eq_union, mem_union_eq, or_imp_distrib, forall_and_distrib]
 
 lemma interval_oc_subset_interval_oc_of_interval_subset_interval {a b c d : α}
   (h : [a, b] ⊆ [c, d]) : Ι a b ⊆ Ι c d :=

src/measure_theory/integral/interval_integral.lean

@@ -171,34 +171,6 @@ open_locale classical topological_space filter ennreal big_operators interval
 variables {α β 𝕜 E F : Type*} [linear_order α] [measurable_space α]
   [measurable_space E] [normed_group E]
 
-/-!
-### Almost everywhere on an interval
--/
-
-section
-variables {μ : measure α} {a b : α} {P : α → Prop}
-
-lemma ae_interval_oc_iff :
-  (∀ᵐ x ∂μ, x ∈ Ι a b → P x) ↔ (∀ᵐ x ∂μ, x ∈ Ioc a b → P x) ∧ (∀ᵐ x ∂μ, x ∈ Ioc b a → P x) :=
-by { dsimp [interval_oc], cases le_total a b with hab hab ; simp [hab] }
-
-lemma ae_measurable_interval_oc_iff {μ : measure α} {β : Type*} [measurable_space β] {f : α → β} :
-  (ae_measurable f $ μ.restrict $ Ι a b) ↔
-  (ae_measurable f $ μ.restrict $ Ioc a b) ∧ (ae_measurable f $ μ.restrict $ Ioc b a) :=
-by { dsimp [interval_oc], cases le_total a b with hab hab ; simp [hab] }
-
-variables [topological_space α] [opens_measurable_space α] [order_closed_topology α]
-
-lemma ae_interval_oc_iff' : (∀ᵐ x ∂μ, x ∈ Ι a b → P x) ↔
-  (∀ᵐ x ∂ (μ.restrict $ Ioc a b), P x) ∧ (∀ᵐ x ∂ (μ.restrict $ Ioc b a), P x) :=
-begin
-  simp_rw ae_interval_oc_iff,
-  rw [ae_restrict_eq, eventually_inf_principal, ae_restrict_eq, eventually_inf_principal] ;
-  exact measurable_set_Ioc
-end
-
-end
-
 /-!
 ### Integrability at an interval
 -/

src/measure_theory/measure/measure_space.lean

@@ -89,7 +89,7 @@ measure, almost everywhere, measure space, completion, null set, null measurable
 noncomputable theory
 
 open set filter (hiding map) function measurable_space topological_space (second_countable_topology)
-open_locale classical topological_space big_operators filter ennreal nnreal
+open_locale classical topological_space big_operators filter ennreal nnreal interval
 
 variables {α β γ δ ι R R' : Type*}
 
@@ -103,6 +103,11 @@ instance ae_is_measurably_generated : is_measurably_generated μ.ae :=
 ⟨λ s hs, let ⟨t, hst, htm, htμ⟩ := exists_measurable_superset_of_null hs in
   ⟨tᶜ, compl_mem_ae_iff.2 htμ, htm.compl, compl_subset_comm.1 hst⟩⟩
 
+/-- See also `measure_theory.ae_restrict_interval_oc_iff`. -/
+lemma ae_interval_oc_iff [linear_order α] {a b : α} {P : α → Prop} :
+  (∀ᵐ x ∂μ, x ∈ Ι a b → P x) ↔ (∀ᵐ x ∂μ, x ∈ Ioc a b → P x) ∧ (∀ᵐ x ∂μ, x ∈ Ioc b a → P x) :=
+by simp only [interval_oc_eq_union, mem_union_eq, or_imp_distrib, eventually_and]
+
 lemma measure_union (hd : disjoint s₁ s₂) (h : measurable_set s₂) :
   μ (s₁ ∪ s₂) = μ s₁ + μ s₂ :=
 measure_union₀ h.null_measurable_set hd.ae_disjoint
@@ -1773,6 +1778,25 @@ begin
   { simp [map_of_not_measurable h] }
 end
 
+@[simp] lemma ae_restrict_Union_eq [encodable ι] (s : ι → set α) :
+  (μ.restrict (⋃ i, s i)).ae = ⨆ i, (μ.restrict (s i)).ae :=
+le_antisymm (ae_sum_eq (λ i, μ.restrict (s i)) ▸ ae_mono restrict_Union_le) $
+  supr_le $ λ i, ae_mono $ restrict_mono (subset_Union s i) le_rfl
+
+@[simp] lemma ae_restrict_union_eq (s t : set α) :
+  (μ.restrict (s ∪ t)).ae = (μ.restrict s).ae ⊔ (μ.restrict t).ae :=
+by simp [union_eq_Union, supr_bool_eq]
+
+lemma ae_restrict_interval_oc_eq [linear_order α] (a b : α) :
+  (μ.restrict (Ι a b)).ae = (μ.restrict (Ioc a b)).ae ⊔ (μ.restrict (Ioc b a)).ae :=
+by simp only [interval_oc_eq_union, ae_restrict_union_eq]
+
+/-- See also `measure_theory.ae_interval_oc_iff`. -/
+lemma ae_restrict_interval_oc_iff [linear_order α] {a b : α} {P : α → Prop} :
+  (∀ᵐ x ∂μ.restrict (Ι a b), P x) ↔
+    (∀ᵐ x ∂μ.restrict (Ioc a b), P x) ∧ (∀ᵐ x ∂μ.restrict (Ioc b a), P x) :=
+by rw [ae_restrict_interval_oc_eq, eventually_sup]
+
 lemma ae_restrict_iff {p : α → Prop} (hp : measurable_set {x | p x}) :
   (∀ᵐ x ∂(μ.restrict s), p x) ↔ ∀ᵐ x ∂μ, x ∈ s → p x :=
 begin
@@ -3224,6 +3248,11 @@ protected lemma Union [encodable ι] {s : ι → set α} (h : ∀ i, ae_measurab
   ae_measurable f (μ.restrict (⋃ i, s i)) ↔ ∀ i, ae_measurable f (μ.restrict (s i)) :=
 ⟨λ h i, h.mono_measure $ restrict_mono (subset_Union _ _) le_rfl, ae_measurable.Union⟩
 
+@[simp] lemma _root_.ae_measurable_union_iff {s t : set α} :
+  ae_measurable f (μ.restrict (s ∪ t)) ↔
+    ae_measurable f (μ.restrict s) ∧ ae_measurable f (μ.restrict t) :=
+by simp only [union_eq_Union, ae_measurable_Union_iff, bool.forall_bool, cond, and.comm]
+
 @[measurability]
 lemma smul_measure [monoid R] [distrib_mul_action R ℝ≥0∞] [is_scalar_tower R ℝ≥0∞ ℝ≥0∞]
   (h : ae_measurable f μ) (c : R) :
@@ -3259,6 +3288,11 @@ let ⟨g, hgm, hg⟩ := h in hgm.null_measurable.congr hg.symm
 
 end ae_measurable
 
+lemma ae_measurable_interval_oc_iff [linear_order α] {f : α → β} {a b : α} :
+  (ae_measurable f $ μ.restrict $ Ι a b) ↔
+    (ae_measurable f $ μ.restrict $ Ioc a b) ∧ (ae_measurable f $ μ.restrict $ Ioc b a) :=
+by rw [interval_oc_eq_union, ae_measurable_union_iff]
+
 lemma ae_measurable_iff_measurable [μ.is_complete] :
   ae_measurable f μ ↔ measurable f :=
 ⟨λ h, h.null_measurable.measurable_of_complete, λ h, h.ae_measurable⟩