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