# Documentation

Mathlib.Dynamics.Ergodic.Conservative

# 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:

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_2} [] (f : αα) (μ : ) extends :
• measurable :
• absolutelyContinuous :
• exists_mem_image_mem : ∀ ⦃s : Set α⦄, μ s 0x, x s m x_1, f^[m] x s

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.

Instances For
theorem MeasureTheory.MeasurePreserving.conservative {α : Type u_2} [] {f : αα} {μ : } :

A self-map preserving a finite measure is conservative.

theorem MeasureTheory.Conservative.id {α : Type u_2} [] (μ : ) :

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

theorem MeasureTheory.Conservative.frequently_measure_inter_ne_zero {α : Type u_2} [] {f : αα} {s : Set α} {μ : } (hf : ) (hs : ) (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_2} [] {f : αα} {s : Set α} {μ : } (hf : ) (hs : ) (h0 : μ s 0) (N : ) :
m, 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_not_mem_eq_zero {α : Type u_2} [] {f : αα} {s : Set α} {μ : } (hf : ) (hs : ) (n : ) :
μ {x | x s ∀ (m : ), 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.

theorem MeasureTheory.Conservative.ae_mem_imp_frequently_image_mem {α : Type u_2} [] {f : αα} {s : Set α} {μ : } (hf : ) (hs : ) :
∀ᵐ (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_2} [] {f : αα} {s : Set α} {μ : } (hf : ) (hs : ) :
s {x | ∃ᶠ (n : ) in Filter.atTop, f^[n] x s} =ᶠ[] s
theorem MeasureTheory.Conservative.measure_inter_frequently_image_mem_eq {α : Type u_2} [] {f : αα} {s : Set α} {μ : } (hf : ) (hs : ) :
μ (s {x | ∃ᶠ (n : ) in Filter.atTop, f^[n] x s}) = μ s
theorem MeasureTheory.Conservative.ae_forall_image_mem_imp_frequently_image_mem {α : Type u_2} [] {f : αα} {s : Set α} {μ : } (hf : ) (hs : ) :
∀ᵐ (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_2} [] {f : αα} {s : Set α} {μ : } (hf : ) (hs : ) (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_2} [] [] {f : αα} {μ : } (h : ) :
∀ᵐ (x : α) ∂μ, ∀ (s : Set α), 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_2} [] {f : αα} {μ : } (hf : ) (n : ) :

Iteration of a conservative system is a conservative system.