English
For a quasi-measure-preserving self-map f, if a null-measurable set s is almost invariant (f^{-1} s =ᵐ s), there exists a measurable invariant set t which is almost equal to s and satisfies f^{-1} t = t.
Русский
Для самоперемещающегося по мере отображения f существует измеримое инвариантное множество t, почти эквивалентное s, такое что f^{-1}(t) = t.
LaTeX
$$$\exists t\ (MeasurableSet\ t) \wedge t =_{ae}^{\mu} s \wedge f^{-1}(t) = t$$$
Lean4
/-- For a quasi-measure-preserving self-map `f`, if a null measurable set `s` is a.e. invariant,
then it is a.e. equal to a measurable invariant set.
-/
theorem exists_preimage_eq_of_preimage_ae {f : α → α} (h : QuasiMeasurePreserving f μ μ) (hs : NullMeasurableSet s μ)
(hs' : f ⁻¹' s =ᵐ[μ] s) : ∃ t : Set α, MeasurableSet t ∧ t =ᵐ[μ] s ∧ f ⁻¹' t = t :=
by
obtain ⟨t, htm, ht⟩ := hs
refine ⟨limsup (f^[·] ⁻¹' t) atTop, ?_, ?_, ?_⟩
· exact .measurableSet_limsup fun n ↦ h.measurable.iterate n htm
· have : f ⁻¹' t =ᵐ[μ] t := (h.preimage_ae_eq ht.symm).trans (hs'.trans ht)
exact limsup_ae_eq_of_forall_ae_eq _ fun n ↦ .trans (h.preimage_iterate_ae_eq _ this) ht.symm
· simp only [Set.preimage_iterate_eq]
exact CompleteLatticeHom.apply_limsup_iterate (CompleteLatticeHom.setPreimage f) t
