English
In a conservative system on a second-countable topological space with measurable open sets, almost every x is recurrent in the sense that every neighborhood of x is hit infinitely often by the orbit.
Русский
В консервативной системе на пространствах с счётной базой и измеримыми открытыми множествами почти всякая точка повторяется: каждый окрестности x встречается бесконечно часто вдоль орбиты.
LaTeX
$$$\mathrm{ae}(\mu)$-a.e. x, \text{∀ } s ∈ 𝓝 x, ∃^{\mathrm{F}} n, f^{n} x ∈ s.$$
Lean4
/-- Poincaré recurrence theorem. Let `f : α → α` be a conservative dynamical system on a topological
space with second countable topology and measurable open sets. Then almost every point `x : α`
is recurrent: it visits every neighborhood `s ∈ 𝓝 x` infinitely many times. -/
theorem ae_frequently_mem_of_mem_nhds [TopologicalSpace α] [SecondCountableTopology α] [OpensMeasurableSpace α]
{f : α → α} {μ : Measure α} (h : Conservative f μ) : ∀ᵐ x ∂μ, ∀ s ∈ 𝓝 x, ∃ᶠ n in atTop, f^[n] x ∈ s :=
by
have : ∀ s ∈ countableBasis α, ∀ᵐ x ∂μ, x ∈ s → ∃ᶠ n in atTop, f^[n] x ∈ s := fun s hs =>
h.ae_mem_imp_frequently_image_mem (isOpen_of_mem_countableBasis hs).nullMeasurableSet
refine ((ae_ball_iff <| countable_countableBasis α).2 this).mono fun x hx s hs => ?_
rcases (isBasis_countableBasis α).mem_nhds_iff.1 hs with ⟨o, hoS, hxo, hos⟩
exact (hx o hoS hxo).mono fun n hn => hos hn
