[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : PreErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s = s
⊢ ↑↑μ s = 0 ∨ ↑↑μ sᶜ = 0
[PROOFSTEP]
simpa using hf.ae_empty_or_univ hs hs'
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
hf : PreErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s = s
⊢ ↑↑μ s = 0 ∨ ↑↑μ s = 1
[PROOFSTEP]
simpa [hs] using hf.measure_self_or_compl_eq_zero hs hs'
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
hg : MeasurePreserving g
hf : PreErgodic f
f' : β → β
h_comm : g ∘ f = f' ∘ g
⊢ ∀ ⦃s : Set β⦄, MeasurableSet s → f' ⁻¹' s = s → s =ᶠ[ae μ'] ∅ ∨ s =ᶠ[ae μ'] univ
[PROOFSTEP]
intro s hs₀ hs₁
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
hg : MeasurePreserving g
hf : PreErgodic f
f' : β → β
h_comm : g ∘ f = f' ∘ g
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
⊢ s =ᶠ[ae μ'] ∅ ∨ s =ᶠ[ae μ'] univ
[PROOFSTEP]
replace hs₁ : f ⁻¹' (g ⁻¹' s) = g ⁻¹' s
[GOAL]
case hs₁
α : Type u_1
m : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
hg : MeasurePreserving g
hf : PreErgodic f
f' : β → β
h_comm : g ∘ f = f' ∘ g
s : Set β
hs₀ : MeasurableSet s
hs₁ : f' ⁻¹' s = s
⊢ f ⁻¹' (g ⁻¹' s) = g ⁻¹' s
[PROOFSTEP]
rw [← preimage_comp, h_comm, preimage_comp, hs₁]
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
hg : MeasurePreserving g
hf : PreErgodic f
f' : β → β
h_comm : g ∘ f = f' ∘ g
s : Set β
hs₀ : MeasurableSet s
hs₁ : f ⁻¹' (g ⁻¹' s) = g ⁻¹' s
⊢ s =ᶠ[ae μ'] ∅ ∨ s =ᶠ[ae μ'] univ
[PROOFSTEP]
cases' hf.ae_empty_or_univ (hg.measurable hs₀) hs₁ with hs₂ hs₂ <;> [left; right]
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
hg : MeasurePreserving g
hf : PreErgodic f
f' : β → β
h_comm : g ∘ f = f' ∘ g
s : Set β
hs₀ : MeasurableSet s
hs₁ : f ⁻¹' (g ⁻¹' s) = g ⁻¹' s
⊢ s =ᶠ[ae μ'] ∅ ∨ s =ᶠ[ae μ'] univ
[PROOFSTEP]
cases' hf.ae_empty_or_univ (hg.measurable hs₀) hs₁ with hs₂ hs₂
[GOAL]
case inl
α : Type u_1
m : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
hg : MeasurePreserving g
hf : PreErgodic f
f' : β → β
h_comm : g ∘ f = f' ∘ g
s : Set β
hs₀ : MeasurableSet s
hs₁ : f ⁻¹' (g ⁻¹' s) = g ⁻¹' s
hs₂ : g ⁻¹' s =ᶠ[ae μ] ∅
⊢ s =ᶠ[ae μ'] ∅ ∨ s =ᶠ[ae μ'] univ
[PROOFSTEP]
left
[GOAL]
case inr
α : Type u_1
m : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
hg : MeasurePreserving g
hf : PreErgodic f
f' : β → β
h_comm : g ∘ f = f' ∘ g
s : Set β
hs₀ : MeasurableSet s
hs₁ : f ⁻¹' (g ⁻¹' s) = g ⁻¹' s
hs₂ : g ⁻¹' s =ᶠ[ae μ] univ
⊢ s =ᶠ[ae μ'] ∅ ∨ s =ᶠ[ae μ'] univ
[PROOFSTEP]
right
[GOAL]
case inl.h
α : Type u_1
m : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
hg : MeasurePreserving g
hf : PreErgodic f
f' : β → β
h_comm : g ∘ f = f' ∘ g
s : Set β
hs₀ : MeasurableSet s
hs₁ : f ⁻¹' (g ⁻¹' s) = g ⁻¹' s
hs₂ : g ⁻¹' s =ᶠ[ae μ] ∅
⊢ s =ᶠ[ae μ'] ∅
[PROOFSTEP]
simpa only [ae_eq_empty, hg.measure_preimage hs₀] using hs₂
[GOAL]
case inr.h
α : Type u_1
m : MeasurableSpace α
f : α → α
s✝ : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
hg : MeasurePreserving g
hf : PreErgodic f
f' : β → β
h_comm : g ∘ f = f' ∘ g
s : Set β
hs₀ : MeasurableSet s
hs₁ : f ⁻¹' (g ⁻¹' s) = g ⁻¹' s
hs₂ : g ⁻¹' s =ᶠ[ae μ] univ
⊢ s =ᶠ[ae μ'] univ
[PROOFSTEP]
simpa only [ae_eq_univ, ← preimage_compl, hg.measure_preimage hs₀.compl] using hs₂
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
⊢ PreErgodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ PreErgodic f
[PROOFSTEP]
refine'
  ⟨fun hf => preErgodic_of_preErgodic_conjugate (h.symm e) hf _, fun hf => preErgodic_of_preErgodic_conjugate h hf _⟩
[GOAL]
case refine'_1
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
hf : PreErgodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e))
⊢ ↑(MeasurableEquiv.symm e) ∘ ↑e ∘ f ∘ ↑(MeasurableEquiv.symm e) = f ∘ ↑(MeasurableEquiv.symm e)
[PROOFSTEP]
change (e.symm ∘ e) ∘ f ∘ e.symm = f ∘ e.symm
[GOAL]
case refine'_1
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
hf : PreErgodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e))
⊢ (↑(MeasurableEquiv.symm e) ∘ ↑e) ∘ f ∘ ↑(MeasurableEquiv.symm e) = f ∘ ↑(MeasurableEquiv.symm e)
[PROOFSTEP]
rw [MeasurableEquiv.symm_comp_self, comp.left_id]
[GOAL]
case refine'_2
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
hf : PreErgodic f
⊢ ↑e ∘ f = (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ∘ ↑e
[PROOFSTEP]
change e ∘ f = e ∘ f ∘ e.symm ∘ e
[GOAL]
case refine'_2
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
hf : PreErgodic f
⊢ ↑e ∘ f = ↑e ∘ f ∘ ↑(MeasurableEquiv.symm e) ∘ ↑e
[PROOFSTEP]
rw [MeasurableEquiv.symm_comp_self, comp.right_id]
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
⊢ Ergodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ Ergodic f
[PROOFSTEP]
have : MeasurePreserving (e ∘ f ∘ e.symm) μ' μ' ↔ MeasurePreserving f μ μ := by
  rw [h.comp_left_iff, (MeasurePreserving.symm e h).comp_right_iff]
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
⊢ MeasurePreserving (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ MeasurePreserving f
[PROOFSTEP]
rw [h.comp_left_iff, (MeasurePreserving.symm e h).comp_right_iff]
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
this : MeasurePreserving (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ MeasurePreserving f
⊢ Ergodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ Ergodic f
[PROOFSTEP]
replace h : PreErgodic (e ∘ f ∘ e.symm) μ' ↔ PreErgodic f μ := h.preErgodic_conjugate_iff
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
this : MeasurePreserving (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ MeasurePreserving f
h : PreErgodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ PreErgodic f
⊢ Ergodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ Ergodic f
[PROOFSTEP]
exact
  ⟨fun hf => { this.mp hf.toMeasurePreserving, h.mp hf.toPreErgodic with }, fun hf =>
    { this.mpr hf.toMeasurePreserving, h.mpr hf.toPreErgodic with }⟩
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : QuasiErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s =ᶠ[ae μ] s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
obtain ⟨t, h₀, h₁, h₂⟩ := hf.toQuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae hs hs'
[GOAL]
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : QuasiErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s =ᶠ[ae μ] s
t : Set α
h₀ : MeasurableSet t
h₁ : t =ᶠ[ae μ] s
h₂ : f ⁻¹' t = t
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
rcases hf.ae_empty_or_univ h₀ h₂ with (h₃ | h₃) <;> [left; right]
[GOAL]
case intro.intro.intro
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : QuasiErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s =ᶠ[ae μ] s
t : Set α
h₀ : MeasurableSet t
h₁ : t =ᶠ[ae μ] s
h₂ : f ⁻¹' t = t
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
rcases hf.ae_empty_or_univ h₀ h₂ with (h₃ | h₃)
[GOAL]
case intro.intro.intro.inl
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : QuasiErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s =ᶠ[ae μ] s
t : Set α
h₀ : MeasurableSet t
h₁ : t =ᶠ[ae μ] s
h₂ : f ⁻¹' t = t
h₃ : t =ᶠ[ae μ] ∅
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
left
[GOAL]
case intro.intro.intro.inr
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : QuasiErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s =ᶠ[ae μ] s
t : Set α
h₀ : MeasurableSet t
h₁ : t =ᶠ[ae μ] s
h₂ : f ⁻¹' t = t
h₃ : t =ᶠ[ae μ] univ
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
right
[GOAL]
case intro.intro.intro.inl.h
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : QuasiErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s =ᶠ[ae μ] s
t : Set α
h₀ : MeasurableSet t
h₁ : t =ᶠ[ae μ] s
h₂ : f ⁻¹' t = t
h₃ : t =ᶠ[ae μ] ∅
⊢ s =ᶠ[ae μ] ∅
[PROOFSTEP]
exact ae_eq_trans h₁.symm h₃
[GOAL]
case intro.intro.intro.inr.h
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : QuasiErgodic f
hs : MeasurableSet s
hs' : f ⁻¹' s =ᶠ[ae μ] s
t : Set α
h₀ : MeasurableSet t
h₁ : t =ᶠ[ae μ] s
h₂ : f ⁻¹' t = t
h₃ : t =ᶠ[ae μ] univ
⊢ s =ᶠ[ae μ] univ
[PROOFSTEP]
exact ae_eq_trans h₁.symm h₃
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : QuasiErgodic f
hsm : NullMeasurableSet s
hs : f ⁻¹' s =ᶠ[ae μ] s
⊢ s =ᶠ[ae μ] univ → ∀ᵐ (x : α) ∂μ, x ∈ s
[PROOFSTEP]
simp [mem_ae_iff]
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : QuasiErgodic f
hsm : NullMeasurableSet s
hs : f ⁻¹' s =ᶠ[ae μ] s
⊢ s =ᶠ[ae μ] ∅ → ∀ᵐ (x : α) ∂μ, ¬x ∈ s
[PROOFSTEP]
simp [ae_iff]
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : f ⁻¹' s ≤ᶠ[ae μ] s
h_fin : ↑↑μ s ≠ ⊤
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
refine' hf.quasiErgodic.ae_empty_or_univ' hs _
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : f ⁻¹' s ≤ᶠ[ae μ] s
h_fin : ↑↑μ s ≠ ⊤
⊢ f ⁻¹' s =ᶠ[ae μ] s
[PROOFSTEP]
refine' ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).symm.le _ h_fin
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : f ⁻¹' s ≤ᶠ[ae μ] s
h_fin : ↑↑μ s ≠ ⊤
⊢ MeasurableSet (f ⁻¹' s)
[PROOFSTEP]
exact measurableSet_preimage hf.measurable hs
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : ↑↑μ s ≠ ⊤
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
replace h_fin : μ (f ⁻¹' s) ≠ ∞
[GOAL]
case h_fin
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : ↑↑μ s ≠ ⊤
⊢ ↑↑μ (f ⁻¹' s) ≠ ⊤
[PROOFSTEP]
rwa [hf.measure_preimage hs]
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : ↑↑μ (f ⁻¹' s) ≠ ⊤
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
refine' hf.quasiErgodic.ae_empty_or_univ' hs _
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
h_fin : ↑↑μ (f ⁻¹' s) ≠ ⊤
⊢ f ⁻¹' s =ᶠ[ae μ] s
[PROOFSTEP]
exact (ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).le hs h_fin).symm
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : f '' s ≤ᶠ[ae μ] s
h_fin : ↑↑μ s ≠ ⊤
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
replace hs' : s ≤ᵐ[μ] f ⁻¹' s :=
  (HasSubset.Subset.eventuallyLE (subset_preimage_image f s)).trans (hf.quasiMeasurePreserving.preimage_mono_ae hs')
[GOAL]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Ergodic f
hs : MeasurableSet s
h_fin : ↑↑μ s ≠ ⊤
hs' : s ≤ᶠ[ae μ] f ⁻¹' s
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
[PROOFSTEP]
exact ae_empty_or_univ_of_ae_le_preimage' hf hs hs' h_fin
