English
If f is ergodic and s is null-measurable with f⁻¹' s ≤ᵐ s, and μ(s) finite, then s is almost empty or almost full.
Русский
Пусть f эргодичен; s нулевой измеримости; f⁻¹' s ≤ᵐ s и μ(s) конечна; тогда s почти пусто или почти полно.
LaTeX
$$$\mathrm{Ergodic}(f, \mu) \Rightarrow \mathrm{NullMeasurableSet}(s, \mu) \Rightarrow (f^{-1}(s) \leq^\mathrm{ae} s) \Rightarrow s =^\mu \emptyset \lor s =^\mu \mathrm{univ}$$$
Lean4
/-- See also `Ergodic.ae_empty_or_univ_of_preimage_ae_le`. -/
theorem ae_empty_or_univ_of_preimage_ae_le' (hf : Ergodic f μ) (hs : NullMeasurableSet s μ) (hs' : f ⁻¹' s ≤ᵐ[μ] s)
(h_fin : μ s ≠ ∞) : s =ᵐ[μ] (∅ : Set α) ∨ s =ᵐ[μ] univ :=
by
refine hf.quasiErgodic.ae_empty_or_univ₀ hs ?_
refine ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).ge ?_ h_fin
exact hs.preimage hf.quasiMeasurePreserving
