ae_mem_imp_frequently_image_mem — Mathlib

English

The measure of s ∩ {x | f^n x ∈ s for infinitely many n} equals μ(s) for a conservative f.

Русский

Мера множества $s$ пересекаемого с множеством частых возвратов равна μ(s).

LaTeX

$$$μ\bigl(s \cap \{x: \exists^{\mathrm{F}} n, f^{n} x \in s\}\bigr) = μ(s).$$$

Lean4

/-- Poincaré recurrence theorem: given a conservative map `f` and a measurable set `s`,
almost every point `x ∈ s` returns back to `s` infinitely many times. -/
theorem ae_mem_imp_frequently_image_mem (hf : Conservative f μ) (hs : NullMeasurableSet s μ) :
    ∀ᵐ x ∂μ, x ∈ s → ∃ᶠ n in atTop, f^[n] x ∈ s :=
  by
  simp only [frequently_atTop, @forall_swap (_ ∈ s), ae_all_iff]
  intro n
  filter_upwards [measure_eq_zero_iff_ae_notMem.1 (hf.measure_mem_forall_ge_image_notMem_eq_zero hs n)]
  simp

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