mathlib3 documentation

dynamics.ergodic.ergodic

Ergodic maps and measures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

pre_ergodic: the ergodicity condition without the measure preserving condition. This exists to share code between the ergodic and quasi_ergodic definitions.
ergodic: the definition of ergodic maps / measures.
quasi_ergodic: the definition of quasi ergodic maps / measures.
ergodic.quasi_ergodic: an ergodic map / measure is quasi ergodic.
quasi_ergodic.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 pre_ergodic {α : Type u_1} {m : measurable_space α} (f : α → α) (μ : measure_theory.measure α . "volume_tac") :

Prop

ae_empty_or_univ : ∀ ⦃s : set α⦄, measurable_set s → f ⁻¹' s = s → s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] set.univ

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.

@[nolint]

structure ergodic {α : Type u_1} {m : measurable_space α} (f : α → α) (μ : measure_theory.measure α . "volume_tac") :

Prop

to_measure_preserving : measure_theory.measure_preserving f μ μ
to_pre_ergodic : pre_ergodic f μ

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

@[nolint]

structure quasi_ergodic {α : Type u_1} {m : measurable_space α} (f : α → α) (μ : measure_theory.measure α . "volume_tac") :

Prop

to_quasi_measure_preserving : measure_theory.measure.quasi_measure_preserving f μ μ
to_pre_ergodic : pre_ergodic f μ

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

theorem pre_ergodic.measure_self_or_compl_eq_zero {α : Type u_1} {m : measurable_space α} {f : α → α} {s : set α} {μ : measure_theory.measure α} (hf : pre_ergodic f μ) (hs : measurable_set s) (hs' : f ⁻¹' s = s) :

⇑μ s = 0 ∨ ⇑μ sᶜ = 0

theorem pre_ergodic.prob_eq_zero_or_one {α : Type u_1} {m : measurable_space α} {f : α → α} {s : set α} {μ : measure_theory.measure α} [measure_theory.is_probability_measure μ] (hf : pre_ergodic f μ) (hs : measurable_set s) (hs' : f ⁻¹' s = s) :

⇑μ s = 0 ∨ ⇑μ s = 1

On a probability space, the (pre)ergodicity condition is a zero one law.

theorem pre_ergodic.of_iterate {α : Type u_1} {m : measurable_space α} {f : α → α} {μ : measure_theory.measure α} (n : ℕ) (hf : pre_ergodic f^[n] μ) :

pre_ergodic f μ

theorem measure_theory.measure_preserving.pre_ergodic_of_pre_ergodic_conjugate {α : Type u_1} {m : measurable_space α} {f : α → α} {μ : measure_theory.measure α} {β : Type u_2} {m' : measurable_space β} {μ' : measure_theory.measure β} {g : α → β} (hg : measure_theory.measure_preserving g μ μ') (hf : pre_ergodic f μ) {f' : β → β} (h_comm : g ∘ f = f' ∘ g) :

pre_ergodic f' μ'

theorem measure_theory.measure_preserving.pre_ergodic_conjugate_iff {α : Type u_1} {m : measurable_space α} {f : α → α} {μ : measure_theory.measure α} {β : Type u_2} {m' : measurable_space β} {μ' : measure_theory.measure β} {e : α ≃ᵐ β} (h : measure_theory.measure_preserving ⇑e μ μ') :

pre_ergodic (⇑e ∘ f ∘ ⇑(e.symm)) μ' ↔ pre_ergodic f μ

theorem measure_theory.measure_preserving.ergodic_conjugate_iff {α : Type u_1} {m : measurable_space α} {f : α → α} {μ : measure_theory.measure α} {β : Type u_2} {m' : measurable_space β} {μ' : measure_theory.measure β} {e : α ≃ᵐ β} (h : measure_theory.measure_preserving ⇑e μ μ') :

ergodic (⇑e ∘ f ∘ ⇑(e.symm)) μ' ↔ ergodic f μ

theorem quasi_ergodic.ae_empty_or_univ' {α : Type u_1} {m : measurable_space α} {f : α → α} {s : set α} {μ : measure_theory.measure α} (hf : quasi_ergodic f μ) (hs : measurable_set 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 ergodic.quasi_ergodic {α : Type u_1} {m : measurable_space α} {f : α → α} {μ : measure_theory.measure α} (hf : ergodic f μ) :

quasi_ergodic f μ

An ergodic map is quasi ergodic.

theorem ergodic.ae_empty_or_univ_of_preimage_ae_le' {α : Type u_1} {m : measurable_space α} {f : α → α} {s : set α} {μ : measure_theory.measure α} (hf : ergodic f μ) (hs : measurable_set 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 : measurable_space α} {f : α → α} {s : set α} {μ : measure_theory.measure α} (hf : ergodic f μ) (hs : measurable_set 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 : measurable_space α} {f : α → α} {s : set α} {μ : measure_theory.measure α} (hf : ergodic f μ) (hs : measurable_set 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 : measurable_space α} {f : α → α} {s : set α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] (hf : ergodic f μ) (hs : measurable_set s) (hs' : f ⁻¹' s ≤ᵐ[μ] s) :

s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] set.univ

theorem ergodic.ae_empty_or_univ_of_ae_le_preimage {α : Type u_1} {m : measurable_space α} {f : α → α} {s : set α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] (hf : ergodic f μ) (hs : measurable_set s) (hs' : s ≤ᵐ[μ] f ⁻¹' s) :

s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] set.univ

theorem ergodic.ae_empty_or_univ_of_image_ae_le {α : Type u_1} {m : measurable_space α} {f : α → α} {s : set α} {μ : measure_theory.measure α} [measure_theory.is_finite_measure μ] (hf : ergodic f μ) (hs : measurable_set s) (hs' : f '' s ≤ᵐ[μ] s) :

s =ᵐ[μ] ∅ ∨ s =ᵐ[μ] set.univ