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 the Ergodic and QuasiErgodic definitions.
• 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✝) : Prop

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 =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ

theorem PreErgodic.ae_empty_or_univ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : autoParam (MeasureTheory.Measure α) _auto✝} (self : PreErgodic f μ) ⦃s : Set α⦄ : MeasurableSet s → f ⁻¹' s = s → s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ

structure Ergodic {α : Type u_1} {m : MeasurableSpace α} (f : α → α) (μ : autoParam (MeasureTheory.Measure α) _auto✝) extends MeasureTheory.MeasurePreserving , PreErgodic : Prop

A map f : α → α is said to be ergodic with respect to a measure μ if it is measure preserving and pre-ergodic.

structure QuasiErgodic {α : Type u_1} {m : MeasurableSpace α} (f : α → α) (μ : autoParam (MeasureTheory.Measure α) _auto✝) extends MeasureTheory.Measure.QuasiMeasurePreserving , PreErgodic : Prop

A map f : α → α is said to be quasi ergodic with respect to a measure μ if it is quasi measure preserving and pre-ergodic.

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) : μ s = 0 ∨ μ sᶜ = 0

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) : (∀ᵐ (x : α) ∂μ, x ∈ s) ∨ ∀ᵐ (x : α) ∂μ, x ∉ 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) : μ s = 0 ∨ μ s = 1

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 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) μ μ') : Ergodic (⇑e ∘ f ∘ ⇑e.symm) μ' ↔ Ergodic f μ

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 =ᵐ[μ] s) : s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] 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 =ᵐ[μ] s) : s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] 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 =ᵐ[μ] s) : (∀ᵐ (x : α) ∂μ, x ∈ s) ∨ ∀ᵐ (x : α) ∂μ, x ∉ 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 μ) : QuasiErgodic 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 ≤ᵐ[μ] s) (h_fin : μ s ≠ ⊤) : s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ

See also Ergodic.ae_empty_or_univ_of_preimage_ae_le.

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 ≤ᵐ[μ] f ⁻¹' s) (h_fin : μ s ≠ ⊤) : s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ

See also Ergodic.ae_empty_or_univ_of_ae_le_preimage.

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 ≤ᵐ[μ] s) (h_fin : μ s ≠ ⊤) : s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] 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 ≤ᵐ[μ] s) : s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] 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 ≤ᵐ[μ] f ⁻¹' s) : s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] 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 ≤ᵐ[μ] s) : s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] Set.univ