α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : MeasureTheory.Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : f ⁻¹' s ≤ᶠ[ae μ] s
h_fin : ↑↑μ s ≠ ⊤
⊢ f ⁻¹' s =ᶠ[ae μ] s
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : MeasureTheory.Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : f ⁻¹' s ≤ᶠ[ae μ] s
h_fin : ↑↑μ s ≠ ⊤
⊢ s =ᶠ[ae μ] ∅ ∨ s =ᶠ[ae μ] univ
refine' hf.quasiErgodic.ae_empty_or_univ' hs _
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : MeasureTheory.Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : f ⁻¹' s ≤ᶠ[ae μ] s
h_fin : ↑↑μ s ≠ ⊤
⊢ MeasurableSet (f ⁻¹' s)
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : MeasureTheory.Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : f ⁻¹' s ≤ᶠ[ae μ] s
h_fin : ↑↑μ s ≠ ⊤
⊢ f ⁻¹' s =ᶠ[ae μ] s
refine' ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).symm.le _ h_fin
no goals
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : MeasureTheory.Measure α
hf : Ergodic f
hs : MeasurableSet s
hs' : f ⁻¹' s ≤ᶠ[ae μ] s
h_fin : ↑↑μ s ≠ ⊤
⊢ MeasurableSet (f ⁻¹' s)
exact measurableSet_preimage hf.measurable hs