Theorems · Theorem · dynamical systems

MeasureTheory.Conservative.ae_mem_imp_frequently_image_mem

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

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.

Defined in

Mathlib.Dynamics.Ergodic.Conservative

Cited by

4 results in Mathlib

Foundations

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

Assumes

MeasurableSpace