Ergodic maps and measures #
Let f : α → α be measure preserving with respect to a measure μ. We say f is ergodic with
respect to μ (or μ is ergodic with respect to f) if the only measurable sets s such that
f⁻¹' s = s are either almost empty or full.
In this file we define ergodic maps / measures together with quasi-ergodic maps / measures and provide some basic API. Quasi-ergodicity is a weaker condition than ergodicity for which the measure preserving condition is relaxed to quasi measure preserving.
Main definitions: #
PreErgodic: the ergodicity condition without the measure preserving condition. This exists to share code between theErgodicandQuasiErgodicdefinitions.Ergodic: the definition of ergodic maps / measures.QuasiErgodic: the definition of quasi ergodic maps / measures.Ergodic.quasiErgodic: an ergodic map / measure is quasi ergodic.QuasiErgodic.ae_empty_or_univ': when the map is quasi measure preserving, one may relax the strict invariance condition to almost invariance in the ergodicity condition.
structure
PreErgodic
{α : Type u_1}
{m : MeasurableSpace α}
(f : α → α)
(μ : autoParam (MeasureTheory.Measure α) _auto✝)
:
A map f : α → α is said to be pre-ergodic with respect to a measure μ if any measurable
strictly invariant set is either almost empty or full.
- ae_empty_or_univ : ∀ ⦃s : Set α⦄, MeasurableSet s → f ⁻¹' s = s → s =ᶠ[MeasureTheory.Measure.ae μ] ∅ ∨ s =ᶠ[MeasureTheory.Measure.ae μ] Set.univ
Instances For
structure
Ergodic
{α : Type u_1}
{m : MeasurableSpace α}
(f : α → α)
(μ : autoParam (MeasureTheory.Measure α) _auto✝)
extends
MeasureTheory.MeasurePreserving
,
PreErgodic
:
A map f : α → α is said to be ergodic with respect to a measure μ if it is measure
preserving and pre-ergodic.
Instances For
structure
QuasiErgodic
{α : Type u_1}
{m : MeasurableSpace α}
(f : α → α)
(μ : autoParam (MeasureTheory.Measure α) _auto✝)
extends
MeasureTheory.Measure.QuasiMeasurePreserving
,
PreErgodic
:
A map f : α → α is said to be quasi ergodic with respect to a measure μ if it is quasi
measure preserving and pre-ergodic.
Instances For
theorem
PreErgodic.measure_self_or_compl_eq_zero
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : PreErgodic f)
(hs : MeasurableSet s)
(hs' : f ⁻¹' s = s)
:
theorem
PreErgodic.ae_mem_or_ae_nmem
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : PreErgodic f)
(hsm : MeasurableSet s)
(hs : f ⁻¹' s = s)
:
theorem
PreErgodic.prob_eq_zero_or_one
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{s : Set α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsProbabilityMeasure μ]
(hf : PreErgodic f)
(hs : MeasurableSet s)
(hs' : f ⁻¹' s = s)
:
On a probability space, the (pre)ergodicity condition is a zero one law.
theorem
PreErgodic.of_iterate
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{μ : MeasureTheory.Measure α}
(n : ℕ)
(hf : PreErgodic f^[n])
:
theorem
MeasureTheory.MeasurePreserving.preErgodic_of_preErgodic_conjugate
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{m' : MeasurableSpace β}
{μ' : MeasureTheory.Measure β}
{g : α → β}
(hg : MeasureTheory.MeasurePreserving g)
(hf : PreErgodic f)
{f' : β → β}
(h_comm : g ∘ f = f' ∘ g)
:
PreErgodic f'
theorem
MeasureTheory.MeasurePreserving.preErgodic_conjugate_iff
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{m' : MeasurableSpace β}
{μ' : MeasureTheory.Measure β}
{e : α ≃ᵐ β}
(h : MeasureTheory.MeasurePreserving ⇑e)
:
PreErgodic (⇑e ∘ f ∘ ⇑e.symm) ↔ PreErgodic f
theorem
MeasureTheory.MeasurePreserving.ergodic_conjugate_iff
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{μ : MeasureTheory.Measure α}
{β : Type u_2}
{m' : MeasurableSpace β}
{μ' : MeasureTheory.Measure β}
{e : α ≃ᵐ β}
(h : MeasureTheory.MeasurePreserving ⇑e)
:
theorem
QuasiErgodic.ae_empty_or_univ'
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : QuasiErgodic f)
(hs : MeasurableSet s)
(hs' : f ⁻¹' s =ᶠ[MeasureTheory.Measure.ae μ] s)
:
s =ᶠ[MeasureTheory.Measure.ae μ] ∅ ∨ s =ᶠ[MeasureTheory.Measure.ae μ] Set.univ
For a quasi ergodic map, sets that are almost invariant (rather than strictly invariant) are still either almost empty or full.
theorem
QuasiErgodic.ae_empty_or_univ₀
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : QuasiErgodic f)
(hsm : MeasureTheory.NullMeasurableSet s)
(hs : f ⁻¹' s =ᶠ[MeasureTheory.Measure.ae μ] s)
:
s =ᶠ[MeasureTheory.Measure.ae μ] ∅ ∨ s =ᶠ[MeasureTheory.Measure.ae μ] Set.univ
For a quasi ergodic map, sets that are almost invariant (rather than strictly invariant) are still either almost empty or full.
theorem
QuasiErgodic.ae_mem_or_ae_nmem₀
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : QuasiErgodic f)
(hsm : MeasureTheory.NullMeasurableSet s)
(hs : f ⁻¹' s =ᶠ[MeasureTheory.Measure.ae μ] s)
:
For a quasi ergodic map, sets that are almost invariant (rather than strictly invariant) are still either almost empty or full.
theorem
Ergodic.quasiErgodic
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{μ : MeasureTheory.Measure α}
(hf : Ergodic f)
:
An ergodic map is quasi ergodic.
theorem
Ergodic.ae_empty_or_univ_of_preimage_ae_le'
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : Ergodic f)
(hs : MeasurableSet s)
(hs' : f ⁻¹' s ≤ᶠ[MeasureTheory.Measure.ae μ] s)
(h_fin : ↑↑μ s ≠ ⊤)
:
s =ᶠ[MeasureTheory.Measure.ae μ] ∅ ∨ s =ᶠ[MeasureTheory.Measure.ae μ] Set.univ
theorem
Ergodic.ae_empty_or_univ_of_ae_le_preimage'
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : Ergodic f)
(hs : MeasurableSet s)
(hs' : s ≤ᶠ[MeasureTheory.Measure.ae μ] f ⁻¹' s)
(h_fin : ↑↑μ s ≠ ⊤)
:
s =ᶠ[MeasureTheory.Measure.ae μ] ∅ ∨ s =ᶠ[MeasureTheory.Measure.ae μ] Set.univ
theorem
Ergodic.ae_empty_or_univ_of_image_ae_le'
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{s : Set α}
{μ : MeasureTheory.Measure α}
(hf : Ergodic f)
(hs : MeasurableSet s)
(hs' : f '' s ≤ᶠ[MeasureTheory.Measure.ae μ] s)
(h_fin : ↑↑μ s ≠ ⊤)
:
s =ᶠ[MeasureTheory.Measure.ae μ] ∅ ∨ s =ᶠ[MeasureTheory.Measure.ae μ] Set.univ
See also Ergodic.ae_empty_or_univ_of_image_ae_le.
theorem
Ergodic.ae_empty_or_univ_of_preimage_ae_le
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{s : Set α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
(hf : Ergodic f)
(hs : MeasurableSet s)
(hs' : f ⁻¹' s ≤ᶠ[MeasureTheory.Measure.ae μ] s)
:
s =ᶠ[MeasureTheory.Measure.ae μ] ∅ ∨ s =ᶠ[MeasureTheory.Measure.ae μ] Set.univ
theorem
Ergodic.ae_empty_or_univ_of_ae_le_preimage
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{s : Set α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
(hf : Ergodic f)
(hs : MeasurableSet s)
(hs' : s ≤ᶠ[MeasureTheory.Measure.ae μ] f ⁻¹' s)
:
s =ᶠ[MeasureTheory.Measure.ae μ] ∅ ∨ s =ᶠ[MeasureTheory.Measure.ae μ] Set.univ
theorem
Ergodic.ae_empty_or_univ_of_image_ae_le
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{s : Set α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
(hf : Ergodic f)
(hs : MeasurableSet s)
(hs' : f '' s ≤ᶠ[MeasureTheory.Measure.ae μ] s)
:
s =ᶠ[MeasureTheory.Measure.ae μ] ∅ ∨ s =ᶠ[MeasureTheory.Measure.ae μ] Set.univ