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 : α → α)
(μ : MeasureTheory.Measure α := by volume_tac)
:
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.
- aeconst_set ⦃s : Set α⦄ : MeasurableSet s → f ⁻¹' s = s → Filter.EventuallyConst s (MeasureTheory.ae μ)
Instances For
structure
Ergodic
{α : Type u_1}
{m : MeasurableSpace α}
(f : α → α)
(μ : MeasureTheory.Measure α := by volume_tac)
extends MeasureTheory.MeasurePreserving f μ μ, PreErgodic f μ :
A map f : α → α is said to be ergodic with respect to a measure μ if it is measure
preserving and pre-ergodic.
- measurable : Measurable f
- aeconst_set ⦃s : Set α⦄ : MeasurableSet s → f ⁻¹' s = s → Filter.EventuallyConst s (MeasureTheory.ae μ)
Instances For
structure
QuasiErgodic
{α : Type u_1}
{m : MeasurableSpace α}
(f : α → α)
(μ : MeasureTheory.Measure α := by volume_tac)
extends MeasureTheory.Measure.QuasiMeasurePreserving f μ μ, PreErgodic f μ :
A map f : α → α is said to be quasi ergodic with respect to a measure μ if it is quasi
measure preserving and pre-ergodic.
- measurable : Measurable f
- absolutelyContinuous : (map f μ).AbsolutelyContinuous μ
- aeconst_set ⦃s : Set α⦄ : MeasurableSet s → f ⁻¹' s = s → Filter.EventuallyConst s (MeasureTheory.ae μ)
Instances For
theorem
PreErgodic.ae_empty_or_univ
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{f : α → α}
{μ : MeasureTheory.Measure α}
(hf : PreErgodic f μ)
(hs : MeasurableSet s)
(hfs : f ⁻¹' s = s)
:
theorem
PreErgodic.measure_self_or_compl_eq_zero
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{f : α → α}
{μ : MeasureTheory.Measure α}
(hf : PreErgodic f μ)
(hs : MeasurableSet s)
(hs' : f ⁻¹' s = s)
:
theorem
PreErgodic.ae_mem_or_ae_notMem
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{f : α → α}
{μ : MeasureTheory.Measure α}
(hf : PreErgodic f μ)
(hsm : MeasurableSet s)
(hs : f ⁻¹' s = s)
:
@[deprecated PreErgodic.ae_mem_or_ae_notMem (since := "2025-05-24")]
theorem
PreErgodic.ae_mem_or_ae_nmem
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{f : α → α}
{μ : MeasureTheory.Measure α}
(hf : PreErgodic f μ)
(hsm : MeasurableSet s)
(hs : f ⁻¹' s = s)
:
Alias of PreErgodic.ae_mem_or_ae_notMem.
theorem
PreErgodic.prob_eq_zero_or_one
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{f : α → α}
{μ : 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] μ)
:
PreErgodic f μ
theorem
PreErgodic.smul_measure
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{μ : MeasureTheory.Measure α}
{R : Type u_2}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
(hf : PreErgodic f μ)
(c : R)
:
PreErgodic f (c • μ)
theorem
MeasureTheory.MeasurePreserving.preErgodic_of_preErgodic_conjugate
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{μ : Measure α}
{β : Type u_2}
{m' : MeasurableSpace β}
{μ' : Measure β}
{g : α → β}
(hg : MeasurePreserving g μ μ')
(hf : PreErgodic f μ)
{f' : β → β}
(h_comm : Function.Semiconj g f f')
:
PreErgodic f' μ'
theorem
MeasureTheory.MeasurePreserving.preErgodic_conjugate_iff
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{μ : Measure α}
{β : Type u_2}
{m' : MeasurableSpace β}
{μ' : Measure β}
{e : α ≃ᵐ β}
(h : MeasurePreserving (⇑e) μ μ')
:
theorem
MeasureTheory.MeasurePreserving.ergodic_conjugate_iff
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{μ : Measure α}
{β : Type u_2}
{m' : MeasurableSpace β}
{μ' : Measure β}
{e : α ≃ᵐ β}
(h : MeasurePreserving (⇑e) μ μ')
:
theorem
QuasiErgodic.aeconst_set₀
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{f : α → α}
{μ : MeasureTheory.Measure α}
(hf : QuasiErgodic f μ)
(hsm : MeasureTheory.NullMeasurableSet s μ)
(hs : f ⁻¹' s =ᵐ[μ] s)
:
theorem
QuasiErgodic.ae_empty_or_univ₀
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{f : α → α}
{μ : MeasureTheory.Measure α}
(hf : QuasiErgodic f μ)
(hsm : MeasureTheory.NullMeasurableSet s μ)
(hs : f ⁻¹' s =ᵐ[μ] s)
:
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_notMem₀
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{f : α → α}
{μ : MeasureTheory.Measure α}
(hf : QuasiErgodic f μ)
(hsm : MeasureTheory.NullMeasurableSet s μ)
(hs : f ⁻¹' s =ᵐ[μ] s)
:
For a quasi ergodic map, sets that are almost invariant (rather than strictly invariant) are still either almost empty or full.
@[deprecated QuasiErgodic.ae_mem_or_ae_notMem₀ (since := "2025-05-24")]
theorem
QuasiErgodic.ae_mem_or_ae_nmem₀
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{f : α → α}
{μ : MeasureTheory.Measure α}
(hf : QuasiErgodic f μ)
(hsm : MeasureTheory.NullMeasurableSet s μ)
(hs : f ⁻¹' s =ᵐ[μ] s)
:
Alias of QuasiErgodic.ae_mem_or_ae_notMem₀.
For a quasi ergodic map, sets that are almost invariant (rather than strictly invariant) are still either almost empty or full.
theorem
QuasiErgodic.smul_measure
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{μ : MeasureTheory.Measure α}
{R : Type u_2}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
(hf : QuasiErgodic f μ)
(c : R)
:
QuasiErgodic f (c • μ)
theorem
QuasiErgodic.zero_measure
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
(hf : Measurable f)
:
QuasiErgodic f 0
theorem
Ergodic.quasiErgodic
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{μ : MeasureTheory.Measure α}
(hf : Ergodic f μ)
:
QuasiErgodic f μ
An ergodic map is quasi ergodic.
theorem
Ergodic.ae_empty_or_univ_of_preimage_ae_le'
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{f : α → α}
{μ : MeasureTheory.Measure α}
(hf : Ergodic f μ)
(hs : MeasureTheory.NullMeasurableSet s μ)
(hs' : f ⁻¹' s ≤ᵐ[μ] s)
(h_fin : μ s ≠ ⊤)
:
theorem
Ergodic.ae_empty_or_univ_of_ae_le_preimage'
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{f : α → α}
{μ : MeasureTheory.Measure α}
(hf : Ergodic f μ)
(hs : MeasureTheory.NullMeasurableSet s μ)
(hs' : s ≤ᵐ[μ] f ⁻¹' s)
(h_fin : μ s ≠ ⊤)
:
theorem
Ergodic.ae_empty_or_univ_of_image_ae_le'
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{f : α → α}
{μ : MeasureTheory.Measure α}
(hf : Ergodic f μ)
(hs : MeasureTheory.NullMeasurableSet s μ)
(hs' : f '' s ≤ᵐ[μ] s)
(h_fin : μ s ≠ ⊤)
:
See also Ergodic.ae_empty_or_univ_of_image_ae_le.
theorem
Ergodic.symm
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{e : α ≃ᵐ α}
(he : Ergodic (⇑e) μ)
:
If a measurable equivalence is ergodic, then so is the inverse map.
@[simp]
theorem
Ergodic.symm_iff
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{e : α ≃ᵐ α}
:
theorem
Ergodic.smul_measure
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{μ : MeasureTheory.Measure α}
{R : Type u_2}
[SMul R ENNReal]
[IsScalarTower R ENNReal ENNReal]
(hf : Ergodic f μ)
(c : R)
:
theorem
Ergodic.zero_measure
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
(hf : Measurable f)
:
Ergodic f 0
theorem
Ergodic.ae_empty_or_univ_of_preimage_ae_le
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{f : α → α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
(hf : Ergodic f μ)
(hs : MeasureTheory.NullMeasurableSet s μ)
(hs' : f ⁻¹' s ≤ᵐ[μ] s)
:
theorem
Ergodic.ae_empty_or_univ_of_ae_le_preimage
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{f : α → α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
(hf : Ergodic f μ)
(hs : MeasureTheory.NullMeasurableSet s μ)
(hs' : s ≤ᵐ[μ] f ⁻¹' s)
:
theorem
Ergodic.ae_empty_or_univ_of_image_ae_le
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{f : α → α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
(hf : Ergodic f μ)
(hs : MeasureTheory.NullMeasurableSet s μ)
(hs' : f '' s ≤ᵐ[μ] s)
: