# 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} [] {μ : } [] [] {s : Set X} [HasCountableSeparatingOn X MeasurableSet s] {f : αα} {g : αX} (h : ) (hs : ∀ᵐ (x : α) ∂μ, g x s) (hgm : ) (hg_eq : ) :
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} [] {μ : } [] [] [HasCountableSeparatingOn X MeasurableSet Set.univ] {f : αα} {g : αX} (h : ) (hgm : ) (hg_eq : g f = g) :
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} [] {μ : } [] [] [HasCountableSeparatingOn X MeasurableSet Set.univ] {f : αα} {g : αX} (h : ) (hgm : ) (hg_eq : ) :
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} [] {μ : } [] [] [HasCountableSeparatingOn X MeasurableSet Set.univ] {f : αα} {g : αX} (h : ) (hgm : ) (hg_eq : ) :
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} [] {μ : } [] [] {f : αα} {g : αX} (h : ) (hgm : ) (hg_eq : ) :
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} [] {μ : } [] [] {f : αα} (h : ) {g : α →ₘ[μ] X} (hg_eq : ) :
c,
theorem Ergodic.ae_eq_const_of_ae_eq_comp_ae {α : Type u_1} {X : Type u_2} [] {μ : } [] [] {f : αα} {g : αX} (h : ) (hgm : ) (hg_eq : ) :
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} [] {μ : } [] [] {f : αα} (h : ) {g : α →ₘ[μ] X} (hg_eq : ) :
c,