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 null-measurable sets s that
are almost invariant (i.e. 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.PreErgodic.of_preimage_eq: to prove pre-ergodicity of a quasi-measure-preserving map, it suffices to check the ergodicity condition on strictly invariant measurable sets.
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
null-measurable almost invariant set is either almost empty or full.
- aeconst_set ⦃s : Set α⦄ : MeasureTheory.NullMeasurableSet s μ → f ⁻¹' s =ᵐ[μ] s → Filter.EventuallyEmptyOrUniv 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 α⦄ : MeasureTheory.NullMeasurableSet s μ → f ⁻¹' s =ᵐ[μ] s → Filter.EventuallyEmptyOrUniv 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 α⦄ : MeasureTheory.NullMeasurableSet s μ → f ⁻¹' s =ᵐ[μ] s → Filter.EventuallyEmptyOrUniv s (MeasureTheory.ae μ)
Instances For
theorem
PreErgodic.of_preimage_eq
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{μ : MeasureTheory.Measure α}
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ)
(h : ∀ ⦃s : Set α⦄, MeasurableSet s → f ⁻¹' s = s → Filter.EventuallyEmptyOrUniv s (MeasureTheory.ae μ))
:
PreErgodic f μ
To prove that a quasi-measure-preserving f is pre-ergodic, it suffices to check the ergodicity
condition on strictly invariant measurable sets.
theorem
Ergodic.of_preimage_eq
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{μ : MeasureTheory.Measure α}
(hf : MeasureTheory.MeasurePreserving f μ μ)
(h : ∀ ⦃s : Set α⦄, MeasurableSet s → f ⁻¹' s = s → Filter.EventuallyEmptyOrUniv s (MeasureTheory.ae μ))
:
Ergodic f μ
To prove that a quasi-measure-preserving f is ergodic, it suffices to check the ergodicity
condition on strictly invariant measurable sets.
theorem
QuasiErgodic.of_preimage_eq
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{μ : MeasureTheory.Measure α}
(hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ)
(h : ∀ ⦃s : Set α⦄, MeasurableSet s → f ⁻¹' s = s → Filter.EventuallyEmptyOrUniv s (MeasureTheory.ae μ))
:
QuasiErgodic f μ
To prove that a quasi-measure-preserving f is quasi-ergodic, it suffices to check the
ergodicity condition on strictly invariant measurable sets.
theorem
PreErgodic.ae_empty_or_univ
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{f : α → α}
{μ : MeasureTheory.Measure α}
(hf : PreErgodic f μ)
(hs : MeasureTheory.NullMeasurableSet 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 : MeasureTheory.NullMeasurableSet 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 : MeasureTheory.NullMeasurableSet s μ)
(hs : f ⁻¹' s =ᵐ[μ] s)
:
theorem
PreErgodic.prob_eq_zero_or_one
{α : Type u_1}
{m : MeasurableSpace α}
{s : Set α}
{f : α → α}
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsProbabilityMeasure μ]
(hf : PreErgodic f μ)
(hs : MeasureTheory.NullMeasurableSet 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 : ℕ)
(hqmp : MeasureTheory.Measure.QuasiMeasurePreserving f μ μ)
(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_semiconj
{α : 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.ergodic_of_ergodic_semiconj
{α : Type u_1}
{m : MeasurableSpace α}
{f : α → α}
{μ : Measure α}
{β : Type u_2}
{m' : MeasurableSpace β}
{μ' : Measure β}
{g : α → β}
(hg : MeasurePreserving g μ μ')
(hf : Ergodic f μ)
{f' : β → β}
(hf' : Measurable f')
(h_comm : Function.Semiconj g f f')
:
Ergodic 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) μ μ')
:
@[deprecated PreErgodic.aeconst_set (since := "2026-09-06")]
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)
:
@[deprecated PreErgodic.ae_empty_or_univ (since := "2026-09-06")]
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.
@[deprecated PreErgodic.ae_mem_or_ae_notMem (since := "2026-09-06")]
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.
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)
: