Conservative systems

In this file we define f : α → α to be a conservative system w.r.t a measure μ if f is non-singular (MeasureTheory.QuasiMeasurePreserving) and for every measurable set s of positive measure at least one point x ∈ s returns back to s after some number of iterations of f. There are several properties that look like they are stronger than this one but actually follow from it:

• MeasureTheory.Conservative.frequently_measure_inter_ne_zero, MeasureTheory.Conservative.exists_gt_measure_inter_ne_zero: if μ s ≠ 0, then for infinitely many n, the measure of s ∩ f^[n] ⁻¹' s is positive.

• MeasureTheory.Conservative.measure_mem_forall_ge_image_notMem_eq_zero, MeasureTheory.Conservative.ae_mem_imp_frequently_image_mem: a.e. every point of s visits s infinitely many times (Poincaré recurrence theorem).

We also prove the topological Poincaré recurrence theorem MeasureTheory.Conservative.ae_frequently_mem_of_mem_nhds. Let f : α → α be a conservative dynamical system on a topological space with second countable topology and measurable open sets. Then almost every point x : α is recurrent: it visits every neighborhood s ∈ 𝓝 x infinitely many times.

Tags

conservative dynamical system, Poincare recurrence theorem

structure MeasureTheory.Conservative {α : Type u_1} [MeasurableSpace α] (f : α → α) (μ : Measure α) extends MeasureTheory.Measure.QuasiMeasurePreserving f μ μ : Prop

We say that a non-singular (MeasureTheory.QuasiMeasurePreserving) self-map is conservative if for any measurable set s of positive measure there exists x ∈ s such that x returns back to s under some iteration of f.

• measurable : Measurable f
• absolutelyContinuous : (map f μ).AbsolutelyContinuous μ
• exists_mem_iterate_mem' ⦃s : Set α⦄ : MeasurableSet s → μ s ≠ 0 → ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s

  If f is a conservative self-map and s is a measurable set of nonzero measure, then there exists a point x ∈ s that returns to s under a non-zero iteration of f.

theorem MeasureTheory.MeasurePreserving.conservative {α : Type u_1} [MeasurableSpace α] {f : α → α} {μ : Measure α} [IsFiniteMeasure μ] (h : MeasurePreserving f μ μ) : Conservative f μ

A self-map preserving a finite measure is conservative.

theorem MeasureTheory.Conservative.id {α : Type u_1} [MeasurableSpace α] (μ : Measure α) : Conservative id μ

The identity map is conservative w.r.t. any measure.

theorem MeasureTheory.Conservative.of_absolutelyContinuous {α : Type u_1} [MeasurableSpace α] {f : α → α} {μ ν : Measure α} (h : Conservative f μ) (hν : ν.AbsolutelyContinuous μ) (h' : Measure.QuasiMeasurePreserving f ν ν) : Conservative f ν

theorem MeasureTheory.Conservative.measureRestrict {α : Type u_1} [MeasurableSpace α] {f : α → α} {s : Set α} {μ : Measure α} (h : Conservative f μ) (hs : Set.MapsTo f s s) : Conservative f (μ.restrict s)

Restriction of a conservative system to an invariant set is a conservative system, formulated in terms of the restriction of the measure.

theorem MeasureTheory.Conservative.congr_ae {α : Type u_1} [MeasurableSpace α] {f : α → α} {μ ν : Measure α} (hf : Conservative f μ) (h : ae μ = ae ν) : Conservative f ν

theorem MeasureTheory.conservative_congr {α : Type u_1} [MeasurableSpace α] {f : α → α} {μ ν : Measure α} (h : ae μ = ae ν) : Conservative f μ ↔ Conservative f ν

theorem MeasureTheory.Conservative.exists_mem_iterate_mem {α : Type u_1} [MeasurableSpace α] {f : α → α} {s : Set α} {μ : Measure α} (hf : Conservative f μ) (hsm : NullMeasurableSet s μ) (hs₀ : μ s ≠ 0) : ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s

If f is a conservative self-map and s is a null measurable set of nonzero measure, then there exists a point x ∈ s that returns to s under a non-zero iteration of f.

theorem MeasureTheory.Conservative.frequently_measure_inter_ne_zero {α : Type u_1} [MeasurableSpace α] {f : α → α} {s : Set α} {μ : Measure α} (hf : Conservative f μ) (hs : NullMeasurableSet s μ) (h0 : μ 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.

theorem MeasureTheory.Conservative.exists_gt_measure_inter_ne_zero {α : Type u_1} [MeasurableSpace α] {f : α → α} {s : Set α} {μ : Measure α} (hf : Conservative f μ) (hs : NullMeasurableSet s μ) (h0 : μ s ≠ 0) (N : ℕ) : ∃ m > N, μ (s ∩ f^[m] ⁻¹' s) ≠ 0

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

theorem MeasureTheory.Conservative.measure_mem_forall_ge_image_notMem_eq_zero {α : Type u_1} [MeasurableSpace α] {f : α → α} {s : Set α} {μ : Measure α} (hf : Conservative f μ) (hs : 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.

@[deprecated MeasureTheory.Conservative.measure_mem_forall_ge_image_notMem_eq_zero (since := "2025-05-23")]

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

Alias of MeasureTheory.Conservative.measure_mem_forall_ge_image_notMem_eq_zero.

---

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.

theorem MeasureTheory.Conservative.ae_mem_imp_frequently_image_mem {α : Type u_1} [MeasurableSpace α] {f : α → α} {s : Set α} {μ : Measure α} (hf : Conservative f μ) (hs : 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.

theorem MeasureTheory.Conservative.inter_frequently_image_mem_ae_eq {α : Type u_1} [MeasurableSpace α] {f : α → α} {s : Set α} {μ : Measure α} (hf : Conservative f μ) (hs : NullMeasurableSet s μ) : s ∩ {x : α | ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s} =ᶠ[ae μ] s

theorem MeasureTheory.Conservative.measure_inter_frequently_image_mem_eq {α : Type u_1} [MeasurableSpace α] {f : α → α} {s : Set α} {μ : Measure α} (hf : Conservative f μ) (hs : NullMeasurableSet s μ) : μ (s ∩ {x : α | ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s}) = μ s

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

Poincaré recurrence theorem: if f is a conservative dynamical system and s is a measurable set, then for μ-a.e. x, if the orbit of x visits s at least once, then it visits s infinitely many times.

theorem MeasureTheory.Conservative.frequently_ae_mem_and_frequently_image_mem {α : Type u_1} [MeasurableSpace α] {f : α → α} {s : Set α} {μ : Measure α} (hf : Conservative f μ) (hs : NullMeasurableSet s μ) (h0 : μ 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.

theorem MeasureTheory.Conservative.ae_frequently_mem_of_mem_nhds {α : Type u_1} [MeasurableSpace α] [TopologicalSpace α] [SecondCountableTopology α] [OpensMeasurableSpace α] {f : α → α} {μ : Measure α} (h : Conservative f μ) : ∀ᵐ (x : α) ∂μ, ∀ s ∈ nhds x, ∃ᶠ (n : ℕ) in Filter.atTop, f^[n] x ∈ s

Poincaré recurrence theorem. Let f : α → α be a conservative dynamical system on a topological space with second countable topology and measurable open sets. Then almost every point x : α is recurrent: it visits every neighborhood s ∈ 𝓝 x infinitely many times.

theorem MeasureTheory.Conservative.iterate {α : Type u_1} [MeasurableSpace α] {f : α → α} {μ : Measure α} (hf : Conservative f μ) (n : ℕ) : Conservative f^[n] μ

Iteration of a conservative system is a conservative system.