Documentation

Mathlib.Dynamics.Ergodic.Function

Functions invariant under (quasi)ergodic map #

In this file we prove that an a.e. strongly measurable function g : α → X that is a.e. invariant under a (quasi)ergodic map is a.e. equal to a constant. We prove several versions of this statement with slightly different measurability assumptions. We also formulate a version for MeasureTheory.AEEqFun functions with all a.e. equalities replaced with equalities in the quotient space.

theorem QuasiErgodic.ae_eq_const_of_ae_eq_comp_of_ae_range₀ {α : Type u_1} {X : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Nonempty X] [MeasurableSpace X] {s : Set X} [MeasurableSpace.CountablySeparated s] {f : αα} {g : αX} (h : QuasiErgodic f μ) (hs : ∀ᵐ (x : α) ∂μ, g x s) (hgm : MeasureTheory.NullMeasurable g μ) (hg_eq : g f =ᵐ[μ] g) :
∃ (c : X), g =ᵐ[μ] Function.const α c

Let f : α → α be a (quasi)ergodic map. Let g : α → X is a null-measurable function from α to a nonempty space with a countable family of measurable sets separating points of a set s such that f x ∈ s for a.e. x. If g that is a.e.-invariant under f, then g is a.e. constant.

theorem PreErgodic.ae_eq_const_of_ae_eq_comp {α : Type u_1} {X : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Nonempty X] [MeasurableSpace X] [MeasurableSpace.CountablySeparated X] {f : αα} {g : αX} (h : PreErgodic f μ) (hgm : Measurable g) (hg_eq : g f = g) :
∃ (c : X), g =ᵐ[μ] Function.const α c

Let f : α → α be a (pre)ergodic map. Let g : α → X be a measurable function from α to a nonempty measurable space with a countable family of measurable sets separating the points of X. If g is invariant under f, then g is a.e. constant.

theorem QuasiErgodic.ae_eq_const_of_ae_eq_comp₀ {α : Type u_1} {X : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Nonempty X] [MeasurableSpace X] [MeasurableSpace.CountablySeparated X] {f : αα} {g : αX} (h : QuasiErgodic f μ) (hgm : MeasureTheory.NullMeasurable g μ) (hg_eq : g f =ᵐ[μ] g) :
∃ (c : X), g =ᵐ[μ] Function.const α c

Let f : α → α be a quasi ergodic map. Let g : α → X be a null-measurable function from α to a nonempty measurable space with a countable family of measurable sets separating the points of X. If g is a.e.-invariant under f, then g is a.e. constant.

theorem Ergodic.ae_eq_const_of_ae_eq_comp₀ {α : Type u_1} {X : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [Nonempty X] [MeasurableSpace X] [MeasurableSpace.CountablySeparated X] {f : αα} {g : αX} (h : Ergodic f μ) (hgm : MeasureTheory.NullMeasurable g μ) (hg_eq : g f =ᵐ[μ] g) :
∃ (c : X), g =ᵐ[μ] Function.const α c

Let f : α → α be an ergodic map. Let g : α → X be a null-measurable function from α to a nonempty measurable space with a countable family of measurable sets separating the points of X. If g is a.e.-invariant under f, then g is a.e. constant.

theorem QuasiErgodic.ae_eq_const_of_ae_eq_comp_ae {α : Type u_1} {X : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] [Nonempty X] {f : αα} {g : αX} (h : QuasiErgodic f μ) (hgm : MeasureTheory.AEStronglyMeasurable g μ) (hg_eq : g f =ᵐ[μ] g) :
∃ (c : X), g =ᵐ[μ] Function.const α c

Let f : α → α be a quasi ergodic map. Let g : α → X be an a.e. strongly measurable function from α to a nonempty metrizable topological space. If g is a.e.-invariant under f, then g is a.e. constant.

theorem QuasiErgodic.eq_const_of_compQuasiMeasurePreserving_eq {α : Type u_1} {X : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] [Nonempty X] {f : αα} (h : QuasiErgodic f μ) {g : α →ₘ[μ] X} (hg_eq : g.compQuasiMeasurePreserving f = g) :
∃ (c : X), g = MeasureTheory.AEEqFun.const α c
theorem Ergodic.ae_eq_const_of_ae_eq_comp_ae {α : Type u_1} {X : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] [Nonempty X] {f : αα} {g : αX} (h : Ergodic f μ) (hgm : MeasureTheory.AEStronglyMeasurable g μ) (hg_eq : g f =ᵐ[μ] g) :
∃ (c : X), g =ᵐ[μ] Function.const α c

Let f : α → α be an ergodic map. Let g : α → X be an a.e. strongly measurable function from α to a nonempty metrizable topological space. If g is a.e.-invariant under f, then g is a.e. constant.

theorem Ergodic.eq_const_of_compMeasurePreserving_eq {α : Type u_1} {X : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [TopologicalSpace X] [TopologicalSpace.MetrizableSpace X] [Nonempty X] {f : αα} (h : Ergodic f μ) {g : α →ₘ[μ] X} (hg_eq : g.compMeasurePreserving f = g) :
∃ (c : X), g = MeasureTheory.AEEqFun.const α c