Conservative systems #
In this file we define f : α → α
to be a conservative system w.r.t a measure μ
if f
is
nonsingular (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 manyn
, the measure ofs ∩ f^[n] ⁻¹' s
is positive. 
MeasureTheory.Conservative.measure_mem_forall_ge_image_not_mem_eq_zero
,MeasureTheory.Conservative.ae_mem_imp_frequently_image_mem
: a.e. every point ofs
visitss
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
We say that a nonsingular (MeasureTheory.QuasiMeasurePreserving
) selfmap 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 : MeasureTheory.Measure.AbsolutelyContinuous (MeasureTheory.Measure.map f μ) μ
 exists_mem_iterate_mem : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑↑μ s ≠ 0 → ∃ x ∈ s, ∃ (m : ℕ), m ≠ 0 ∧ f^[m] x ∈ s
If
f
is a conservative selfmap ands
is a measurable set of nonzero measure, then there exists a pointx ∈ s
that returns tos
under a nonzero iteration off
.
Instances For
A selfmap 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 selfmap 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.