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} [HasCountableSeparatingOn X MeasurableSet s] {f : α → α} {g : α → X} (h : QuasiErgodic f μ) (hs : ∀ᵐ (x : α) ∂μ, g x ∈ s) (hgm : MeasureTheory.NullMeasurable g μ) (hg_eq : g ∘ f =ᶠ[MeasureTheory.Measure.ae μ] g) : ∃ (c : X), g =ᶠ[MeasureTheory.Measure.ae μ] 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] [HasCountableSeparatingOn X MeasurableSet Set.univ] {f : α → α} {g : α → X} (h : PreErgodic f μ) (hgm : Measurable g) (hg_eq : g ∘ f = g) : ∃ (c : X), g =ᶠ[MeasureTheory.Measure.ae μ] 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] [HasCountableSeparatingOn X MeasurableSet Set.univ] {f : α → α} {g : α → X} (h : QuasiErgodic f μ) (hgm : MeasureTheory.NullMeasurable g μ) (hg_eq : g ∘ f =ᶠ[MeasureTheory.Measure.ae μ] g) : ∃ (c : X), g =ᶠ[MeasureTheory.Measure.ae μ] 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] [HasCountableSeparatingOn X MeasurableSet Set.univ] {f : α → α} {g : α → X} (h : Ergodic f μ) (hgm : MeasureTheory.NullMeasurable g μ) (hg_eq : g ∘ f =ᶠ[MeasureTheory.Measure.ae μ] g) : ∃ (c : X), g =ᶠ[MeasureTheory.Measure.ae μ] 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 =ᶠ[MeasureTheory.Measure.ae μ] g) : ∃ (c : X), g =ᶠ[MeasureTheory.Measure.ae μ] 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 : MeasureTheory.AEEqFun.compQuasiMeasurePreserving g 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 =ᶠ[MeasureTheory.Measure.ae μ] g) : ∃ (c : X), g =ᶠ[MeasureTheory.Measure.ae μ] 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 : MeasureTheory.AEEqFun.compMeasurePreserving g f ⋯ = g) : ∃ (c : X), g = MeasureTheory.AEEqFun.const α c