feat(Dynamics/Ergodic): add ergodic_of_ergodic_semiconj (#31793)

Adds the theorem `MeasureTheory.MeasurePreserving.ergodic_of_ergodic_semiconj`, showing that the ergodicity property can be pushed along a semiconjugacy.

Author: lua-vr

Mathlib/Dynamics/Ergodic/Ergodic.lean

@@ -94,17 +94,25 @@ namespace MeasureTheory.MeasurePreserving
 
 variable {β : Type*} {m' : MeasurableSpace β} {μ' : Measure β} {g : α → β}
 
-theorem preErgodic_of_preErgodic_conjugate (hg : MeasurePreserving g μ μ') (hf : PreErgodic f μ)
+theorem preErgodic_of_preErgodic_semiconj (hg : MeasurePreserving g μ μ') (hf : PreErgodic f μ)
     {f' : β → β} (h_comm : Semiconj g f f') : PreErgodic f' μ' where
   aeconst_set s hs₀ hs₁ := by
     rw [← hg.aeconst_preimage hs₀.nullMeasurableSet]
     apply hf.aeconst_set (hg.measurable hs₀)
     rw [← preimage_comp, h_comm.comp_eq, preimage_comp, hs₁]
 
+@[deprecated (since := "2025-11-19")]
+alias preErgodic_of_preErgodic_conjugate := preErgodic_of_preErgodic_semiconj
+
+theorem ergodic_of_ergodic_semiconj (hg : MeasurePreserving g μ μ') (hf : Ergodic f μ)
+    {f' : β → β} (hf' : Measurable f') (h_comm : Semiconj g f f') : Ergodic f' μ' :=
+  ⟨hg.of_semiconj hf.toMeasurePreserving h_comm hf',
+   hg.preErgodic_of_preErgodic_semiconj hf.toPreErgodic h_comm⟩
+
 theorem preErgodic_conjugate_iff {e : α ≃ᵐ β} (h : MeasurePreserving e μ μ') :
     PreErgodic (e ∘ f ∘ e.symm) μ' ↔ PreErgodic f μ := by
-  refine ⟨fun hf => preErgodic_of_preErgodic_conjugate (h.symm e) hf ?_,
-      fun hf => preErgodic_of_preErgodic_conjugate h hf ?_⟩
+  refine ⟨fun hf => preErgodic_of_preErgodic_semiconj (h.symm e) hf ?_,
+      fun hf => preErgodic_of_preErgodic_semiconj h hf ?_⟩
   · simp [Semiconj]
   · simp [Semiconj]
 

Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

@@ -94,6 +94,17 @@ protected theorem comp {g : β → γ} {f : α → β} (hg : MeasurePreserving g
     (hf : MeasurePreserving f μa μb) : MeasurePreserving (g ∘ f) μa μc :=
   ⟨hg.1.comp hf.1, by rw [← map_map hg.1 hf.1, hf.2, hg.2]⟩
 
+protected theorem map_of_comp {f : α → β} {g : β → γ} (hgf : MeasurePreserving (g ∘ f) μa μc)
+    (hg : Measurable g) (hf : Measurable f) :
+    MeasurePreserving g (μa.map f) μc :=
+  ⟨hg, (map_map hg hf).trans hgf.map_eq⟩
+
+protected theorem of_semiconj {f : α → β} {ga : α → α} {gb : β → β}
+    (hfm : MeasurePreserving f μa μb) (hga : MeasurePreserving ga μa μa) (hf : Semiconj f ga gb)
+    (hgb : Measurable gb) : MeasurePreserving gb μb μb := by
+  have := hf.comp_eq ▸ hfm.comp hga |>.map_of_comp hgb hfm.measurable
+  rwa [hfm.map_eq] at this
+
 /-- An alias of `MeasureTheory.MeasurePreserving.comp` with a convenient defeq and argument order
 for `MeasurableEquiv` -/
 protected theorem trans {e : α ≃ᵐ β} {e' : β ≃ᵐ γ}