English
If f is ergodic and s is null-measurable with f[s] ≤ᵐ s, and μ(s) finite, then s is almost empty or almost universal.
Русский
Если f эргодичен и s нулево измеримо, а f[s] ≤ᵐ s и μ(s) конечна, то s почти пусто или почти все пространство.
LaTeX
$$$\mathrm{Ergodic}(f, \mu) \to \mathrm{NullMeasurableSet}(s, \mu) \to (f(s) \leq^\mathrm{ae} s) \to s =^\mu \emptyset \lor s =^\mu \mathrm{univ}$$$
Lean4
/-- See also `Ergodic.ae_empty_or_univ_of_image_ae_le`. -/
theorem ae_empty_or_univ_of_image_ae_le' (hf : Ergodic f μ) (hs : NullMeasurableSet s μ) (hs' : f '' s ≤ᵐ[μ] s)
(h_fin : μ s ≠ ∞) : s =ᵐ[μ] (∅ : Set α) ∨ s =ᵐ[μ] univ :=
by
replace hs' : s ≤ᵐ[μ] f ⁻¹' s :=
(HasSubset.Subset.eventuallyLE (subset_preimage_image f s)).trans (hf.quasiMeasurePreserving.preimage_mono_ae hs')
exact ae_empty_or_univ_of_ae_le_preimage' hf hs hs' h_fin
