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

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 : (MeasureTheory.Measure.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`

.

## Instances For

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`

.

A self-map preserving a finite measure is conservative.

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

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

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`

.

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.