Conservative systems #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 manyn, the measure ofs ∩ (f^[n]) ⁻¹' sis 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 ofsvisitssinfinitely 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
- 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.
A self-map preserving a finite measure is conservative.
The identity map is conservative w.r.t. any measure.
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.
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.
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.
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.
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.
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.
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.
Iteration of a conservative system is a conservative system.