English
For a conservative f and s with μ(s) > 0, the set of x ∈ s that are recurrent to s has full measure in s.
Русский
Для консервативной $f$ и множества $s$ с положительной мерой, множество возвращающихся к $s$ имеет полную меру внутри $s$.
LaTeX
$$$μ\bigl(s ∩ {x: ∃ᶠ n, f^{n} x ∈ s}\bigr) = μ(s).$$$
Lean4
/-- Poincaré recurrence theorem: given a conservative map `f` and a measurable set `s`, the set
of points `x ∈ s` such that `x` does not return to `s` after `≥ n` iterations has measure zero. -/
theorem measure_mem_forall_ge_image_notMem_eq_zero (hf : Conservative f μ) (hs : NullMeasurableSet s μ) (n : ℕ) :
μ ({x ∈ s | ∀ m ≥ n, f^[m] x ∉ s}) = 0 := by
by_contra H
have : NullMeasurableSet (s ∩ {x | ∀ m ≥ n, f^[m] x ∉ s}) μ :=
by
simp only [setOf_forall, ← compl_setOf]
exact hs.inter <| .biInter (to_countable _) fun m _ ↦ (hs.preimage <| hf.toQuasiMeasurePreserving.iterate m).compl
rcases (hf.exists_gt_measure_inter_ne_zero this H) n with ⟨m, hmn, hm⟩
rcases nonempty_of_measure_ne_zero hm with ⟨x, ⟨_, hxn⟩, hxm, -⟩
exact hxn m hmn.lt.le hxm
