Conservative systems #

In this file we define f : α → α to be a conservative system w.r.t a measure μ if f is non-singular (measure_theory.quasi_measure_preserving) 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:

measure_theory.conservative.frequently_measure_inter_ne_zero, measure_theory.conservative.exists_gt_measure_inter_ne_zero: if μ s ≠ 0, then for infinitely many n, the measure of s ∩ (f^[n]) ⁻¹' s is positive.
measure_theory.conservative.measure_mem_forall_ge_image_not_mem_eq_zero, measure_theory.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 measure_theory.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

source

structure measure_theory.conservative {α : Type u_2} [measurable_space α] (f : α → α) (μ : measure_theory.measure α . "volume_tac") :

Prop

to_quasi_measure_preserving : measure_theory.measure.quasi_measure_preserving f μ μ
exists_mem_image_mem : ∀ ⦃s : set α⦄, measurable_set s → ⇑μ s ≠ 0 → (∃ (x : α) (H : x ∈ s) (m : ℕ) (H : m ≠ 0), f^[m] x ∈ s)

We say that a non-singular (measure_theory.quasi_measure_preserving) 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.

source

@[protected]

theorem measure_theory.measure_preserving.conservative {α : Type u_2} [measurable_space α] {f : α → α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] (h : measure_theory.measure_preserving f μ μ) :

measure_theory.conservative f μ

A self-map preserving a finite measure is conservative.

source

@[protected]

theorem measure_theory.conservative.id {α : Type u_2} [measurable_space α] (μ : measure_theory.measure α) :

measure_theory.conservative id μ

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

source

theorem measure_theory.conservative.frequently_measure_inter_ne_zero {α : Type u_2} [measurable_space α] {f : α → α} {s : set α} {μ : measure_theory.measure α} (hf : measure_theory.conservative f μ) (hs : measurable_set s) (h0 : ⇑μ s ≠ 0) :

∃ᶠ (m : ℕ) in filter.at_top, ⇑μ (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.

source

theorem measure_theory.conservative.exists_gt_measure_inter_ne_zero {α : Type u_2} [measurable_space α] {f : α → α} {s : set α} {μ : measure_theory.measure α} (hf : measure_theory.conservative f μ) (hs : measurable_set s) (h0 : ⇑μ s ≠ 0) (N : ℕ) :

∃ (m : ℕ) (H : 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.

source

theorem measure_theory.conservative.measure_mem_forall_ge_image_not_mem_eq_zero {α : Type u_2} [measurable_space α] {f : α → α} {s : set α} {μ : measure_theory.measure α} (hf : measure_theory.conservative f μ) (hs : measurable_set s) (n : ℕ) :

⇑μ {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.

source

theorem measure_theory.conservative.ae_mem_imp_frequently_image_mem {α : Type u_2} [measurable_space α] {f : α → α} {s : set α} {μ : measure_theory.measure α} (hf : measure_theory.conservative f μ) (hs : measurable_set s) :

∀ᵐ (x : α) ∂μ, x ∈ s → (∃ᶠ (n : ℕ) in filter.at_top, 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.

source

theorem measure_theory.conservative.inter_frequently_image_mem_ae_eq {α : Type u_2} [measurable_space α] {f : α → α} {s : set α} {μ : measure_theory.measure α} (hf : measure_theory.conservative f μ) (hs : measurable_set s) :

s ∩ {x : α | ∃ᶠ (n : ℕ) in filter.at_top, f^[n] x ∈ s} =ᵐ[μ] s

source

theorem measure_theory.conservative.measure_inter_frequently_image_mem_eq {α : Type u_2} [measurable_space α] {f : α → α} {s : set α} {μ : measure_theory.measure α} (hf : measure_theory.conservative f μ) (hs : measurable_set s) :

⇑μ (s ∩ {x : α | ∃ᶠ (n : ℕ) in filter.at_top, f^[n] x ∈ s}) = ⇑μ s

source

theorem measure_theory.conservative.ae_forall_image_mem_imp_frequently_image_mem {α : Type u_2} [measurable_space α] {f : α → α} {s : set α} {μ : measure_theory.measure α} (hf : measure_theory.conservative f μ) (hs : measurable_set s) :

∀ᵐ (x : α) ∂μ, ∀ (k : ℕ), f^[k] x ∈ s → (∃ᶠ (n : ℕ) in filter.at_top, 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.

source

theorem measure_theory.conservative.frequently_ae_mem_and_frequently_image_mem {α : Type u_2} [measurable_space α] {f : α → α} {s : set α} {μ : measure_theory.measure α} (hf : measure_theory.conservative f μ) (hs : measurable_set s) (h0 : ⇑μ s ≠ 0) :

∃ᵐ (x : α) ∂μ, x ∈ s ∧ ∃ᶠ (n : ℕ) in filter.at_top, 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.

source

theorem measure_theory.conservative.ae_frequently_mem_of_mem_nhds {α : Type u_2} [measurable_space α] [topological_space α] [topological_space.second_countable_topology α] [opens_measurable_space α] {f : α → α} {μ : measure_theory.measure α} (h : measure_theory.conservative f μ) :

∀ᵐ (x : α) ∂μ, ∀ (s : set α), s ∈ nhds x → (∃ᶠ (n : ℕ) in filter.at_top, 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.

source

@[protected]

theorem measure_theory.conservative.iterate {α : Type u_2} [measurable_space α] {f : α → α} {μ : measure_theory.measure α} (hf : measure_theory.conservative f μ) (n : ℕ) :

measure_theory.conservative f^[n] μ

Iteration of a conservative system is a conservative system.