English
For a conservative f and null-measurable s, almost every x in s, if f^k x ∈ s then f^n x ∈ s for infinitely many n, for every k.
Русский
Для консервативного f и нулевой измеримости s почти каждое x в s: если f^k x ∈ s, то бесконечно часто встречаются n такие, что f^n x ∈ s, для любого фиксированного k.
LaTeX
$$$\forall x, \text{if } x\in s \text{ and } f^{k}x\in s\text{ then } ∃^{\mathrm{F}} n, f^{n}x\in s$ для любого k, a.e.$$
Lean4
/-- Poincaré recurrence theorem: if `f` is a conservative dynamical system and `s` is a measurable
set, then for `μ`-a.e. `x`, if the orbit of `x` visits `s` at least once, then it visits `s`
infinitely many times. -/
theorem ae_forall_image_mem_imp_frequently_image_mem (hf : Conservative f μ) (hs : NullMeasurableSet s μ) :
∀ᵐ x ∂μ, ∀ k, f^[k] x ∈ s → ∃ᶠ n in atTop, f^[n] x ∈ s :=
by
refine ae_all_iff.2 fun k => ?_
refine
(hf.ae_mem_imp_frequently_image_mem (hs.preimage <| hf.toQuasiMeasurePreserving.iterate k)).mono fun x hx hk => ?_
rw [← map_add_atTop_eq_nat k, frequently_map]
refine (hx hk).mono fun n hn => ?_
rwa [add_comm, iterate_add_apply]
