feat(dynamics/ergodic/ergodic): expand ergodic map API for finite mea…

…sures (#17864)

src/dynamics/ergodic/ergodic.lean

@@ -29,6 +29,7 @@ preserving condition is relaxed to quasi measure preserving.
 -/
 
 open set function filter measure_theory measure_theory.measure
+open_locale ennreal
 
 variables {α : Type*} {m : measurable_space α} (f : α → α) {s : set α}
 include m
@@ -107,15 +108,6 @@ end
 
 end measure_theory.measure_preserving
 
-namespace ergodic
-
-/-- An ergodic map is quasi ergodic. -/
-lemma quasi_ergodic (hf : ergodic f μ) : quasi_ergodic f μ :=
-{ .. hf.to_pre_ergodic,
-  .. hf.to_measure_preserving.quasi_measure_preserving, }
-
-end ergodic
-
 namespace quasi_ergodic
 
 /-- For a quasi ergodic map, sets that are almost invariant (rather than strictly invariant) are
@@ -131,3 +123,64 @@ begin
 end
 
 end quasi_ergodic
+
+namespace ergodic
+
+/-- An ergodic map is quasi ergodic. -/
+lemma quasi_ergodic (hf : ergodic f μ) : quasi_ergodic f μ :=
+{ .. hf.to_pre_ergodic,
+  .. hf.to_measure_preserving.quasi_measure_preserving, }
+
+/-- See also `ergodic.ae_empty_or_univ_of_preimage_ae_le`. -/
+lemma ae_empty_or_univ_of_preimage_ae_le'
+  (hf : ergodic f μ) (hs : measurable_set s) (hs' : f⁻¹' s ≤ᵐ[μ] s) (h_fin : μ s ≠ ∞) :
+  s =ᵐ[μ] (∅ : set α) ∨ s =ᵐ[μ] univ :=
+begin
+  refine hf.quasi_ergodic.ae_empty_or_univ' hs _,
+  refine ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).symm.le _ h_fin,
+  exact measurable_set_preimage hf.measurable hs,
+end
+
+/-- See also `ergodic.ae_empty_or_univ_of_ae_le_preimage`. -/
+lemma ae_empty_or_univ_of_ae_le_preimage'
+  (hf : ergodic f μ) (hs : measurable_set s) (hs' : s ≤ᵐ[μ] f⁻¹' s) (h_fin : μ s ≠ ∞) :
+  s =ᵐ[μ] (∅ : set α) ∨ s =ᵐ[μ] univ :=
+begin
+  replace h_fin : μ (f⁻¹' s) ≠ ∞, { rwa hf.measure_preimage hs, },
+  refine hf.quasi_ergodic.ae_empty_or_univ' hs _,
+  exact (ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).le hs h_fin).symm,
+end
+
+/-- See also `ergodic.ae_empty_or_univ_of_image_ae_le`. -/
+lemma ae_empty_or_univ_of_image_ae_le'
+  (hf : ergodic f μ) (hs : measurable_set s) (hs' : f '' s ≤ᵐ[μ] s) (h_fin : μ s ≠ ∞) :
+  s =ᵐ[μ] (∅ : set α) ∨ s =ᵐ[μ] univ :=
+begin
+  replace hs' : s ≤ᵐ[μ] f ⁻¹' s :=
+    (has_subset.subset.eventually_le (subset_preimage_image f s)).trans
+    (hf.quasi_measure_preserving.preimage_mono_ae hs'),
+  exact ae_empty_or_univ_of_ae_le_preimage' hf hs hs' h_fin,
+end
+
+section is_finite_measure
+
+variables [is_finite_measure μ]
+
+lemma ae_empty_or_univ_of_preimage_ae_le
+  (hf : ergodic f μ) (hs : measurable_set s) (hs' : f⁻¹' s ≤ᵐ[μ] s) :
+  s =ᵐ[μ] (∅ : set α) ∨ s =ᵐ[μ] univ :=
+ae_empty_or_univ_of_preimage_ae_le' hf hs hs' $ measure_ne_top μ s
+
+lemma ae_empty_or_univ_of_ae_le_preimage
+  (hf : ergodic f μ) (hs : measurable_set s) (hs' : s ≤ᵐ[μ] f⁻¹' s) :
+  s =ᵐ[μ] (∅ : set α) ∨ s =ᵐ[μ] univ :=
+ae_empty_or_univ_of_ae_le_preimage' hf hs hs' $ measure_ne_top μ s
+
+lemma ae_empty_or_univ_of_image_ae_le
+  (hf : ergodic f μ) (hs : measurable_set s) (hs' : f '' s ≤ᵐ[μ] s) :
+  s =ᵐ[μ] (∅ : set α) ∨ s =ᵐ[μ] univ :=
+ae_empty_or_univ_of_image_ae_le' hf hs hs' $ measure_ne_top μ s
+
+end is_finite_measure
+
+end ergodic

src/measure_theory/measure/measure_space.lean

@@ -267,12 +267,30 @@ lemma measure_eq_measure_larger_of_between_null_diff {s₁ s₂ s₃ : set α}
 lemma measure_compl (h₁ : measurable_set s) (h_fin : μ s ≠ ∞) : μ (sᶜ) = μ univ - μ s :=
 by { rw compl_eq_univ_diff, exact measure_diff (subset_univ s) h₁ h_fin }
 
+@[simp] lemma union_ae_eq_left_iff_ae_subset : (s ∪ t : set α) =ᵐ[μ] s ↔ t ≤ᵐ[μ] s :=
+begin
+  rw ae_le_set,
+  refine ⟨λ h, by simpa only [union_diff_left] using (ae_eq_set.mp h).1,
+    λ h, eventually_le_antisymm_iff.mpr
+    ⟨by rwa [ae_le_set, union_diff_left], has_subset.subset.eventually_le $ subset_union_left s t⟩⟩,
+end
+
+@[simp] lemma union_ae_eq_right_iff_ae_subset : (s ∪ t : set α) =ᵐ[μ] t ↔ s ≤ᵐ[μ] t :=
+by rw [union_comm, union_ae_eq_left_iff_ae_subset]
+
+lemma ae_eq_of_ae_subset_of_measure_ge (h₁ : s ≤ᵐ[μ] t) (h₂ : μ t ≤ μ s) (hsm : measurable_set s)
+  (ht : μ t ≠ ∞) : s =ᵐ[μ] t :=
+begin
+  refine eventually_le_antisymm_iff.mpr ⟨h₁, ae_le_set.mpr _⟩,
+  replace h₂ : μ t = μ s, from h₂.antisymm (measure_mono_ae h₁),
+  replace ht : μ s ≠ ∞, from h₂ ▸ ht,
+  rw [measure_diff' t hsm ht, measure_congr (union_ae_eq_left_iff_ae_subset.mpr h₁), h₂, tsub_self],
+end
+
 /-- If `s ⊆ t`, `μ t ≤ μ s`, `μ t ≠ ∞`, and `s` is measurable, then `s =ᵐ[μ] t`. -/
 lemma ae_eq_of_subset_of_measure_ge (h₁ : s ⊆ t) (h₂ : μ t ≤ μ s) (hsm : measurable_set s)
   (ht : μ t ≠ ∞) : s =ᵐ[μ] t :=
-have A : μ t = μ s, from h₂.antisymm (measure_mono h₁),
-have B : μ s ≠ ∞, from A ▸ ht,
-h₁.eventually_le.antisymm $ ae_le_set.2 $ by rw [measure_diff h₁ hsm B, A, tsub_self]
+ae_eq_of_ae_subset_of_measure_ge (has_subset.subset.eventually_le h₁) h₂ hsm ht
 
 lemma measure_Union_congr_of_subset [countable β] {s : β → set α} {t : β → set α}
   (hsub : ∀ b, s b ⊆ t b) (h_le : ∀ b, μ (t b) ≤ μ (s b)) :

src/measure_theory/measure/measure_space_def.lean

@@ -367,7 +367,11 @@ lemma ae_le_set_inter {s' t' : set α} (h : s ≤ᵐ[μ] t) (h' : s' ≤ᵐ[μ]
   (s ∩ s' : set α) ≤ᵐ[μ] (t ∩ t' : set α) :=
 h.inter h'
 
-@[simp] lemma union_ae_eq_right : (s ∪ t : set α) =ᵐ[μ] t ↔ μ (s \ t) = 0 :=
+lemma ae_le_set_union {s' t' : set α} (h : s ≤ᵐ[μ] t) (h' : s' ≤ᵐ[μ] t') :
+  (s ∪ s' : set α) ≤ᵐ[μ] (t ∪ t' : set α) :=
+h.union h'
+
+lemma union_ae_eq_right : (s ∪ t : set α) =ᵐ[μ] t ↔ μ (s \ t) = 0 :=
 by simp [eventually_le_antisymm_iff, ae_le_set, union_diff_right,
   diff_eq_empty.2 (set.subset_union_right _ _)]