liminf_preimage_iterate_ae_eq — Mathlib

English

Similarly, the liminf of the sequence of iterated preimages of s equals s almost everywhere for a quasi-measure-preserving self-map.

Русский

Аналогично, лиминф последовательности предобразов итераций множества s равен почти-s для квазисохранения меры.

LaTeX

$$liminf (n→∞) (preimage f)^[n] s =_{ae}^{\mu} s$$

Lean4

theorem liminf_preimage_iterate_ae_eq {f : α → α} (hf : QuasiMeasurePreserving f μ μ) (hs : f ⁻¹' s =ᵐ[μ] s) :
    liminf (α := Set α) (fun n => (preimage f)^[n] s) atTop =ᵐ[μ] s :=
  liminf_ae_eq_of_forall_ae_eq (fun n => (preimage f)^[n] s) fun n ↦ by
    simpa only [Set.preimage_iterate_eq] using hf.preimage_iterate_ae_eq n hs

Похожие утверждения