Theorems · Theorem · dynamical systems

MeasureTheory.Conservative.frequently_ae_mem_and_frequently_image_mem

∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ →
    MeasureTheory.NullMeasurableSet s μ → μ s ≠ 0 → ∃ᵐ (x : α) ∂μ, x ∈ s ∧ ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s

If f is a conservative self-map and s is a measurable set of positive measure, then ae μ-frequently we have x ∈ s and s returns to s under infinitely many iterations of f.

Defined in

Mathlib.Dynamics.Ergodic.Conservative

Cited by

1 results in Mathlib

Foundations

Depth 209 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpace