Theorems · Theorem · dynamical systems

MeasureTheory.Conservative.frequently_measure_inter_ne_zero

∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ →
    MeasureTheory.NullMeasurableSet s μ → μ s ≠ 0 → ∃ᶠ (m : ℕ) in Filter.atTop, μ (s ∩ f^[m] ⁻¹' s) ≠ 0

If f is a conservative map and s is a measurable set of nonzero measure, then for infinitely many values of m a positive measure of points x ∈ s returns back to s after m iterations of f.

Defined in

Mathlib.Dynamics.Ergodic.Conservative

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpace