Theorems · Theorem · dynamical systems

MeasureTheory.Conservative.measure_mem_forall_ge_image_notMem_eq_zero

∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ →
    MeasureTheory.NullMeasurableSet s μ → ∀ (n : ℕ), μ {x | x ∈ s ∧ ∀ m ≥ n, f^[m] x ∉ s} = 0

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.

Defined in

Mathlib.Dynamics.Ergodic.Conservative

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace