Theorems · Theorem · dynamical systems

Ergodic.ae_eq_const_of_ae_eq_comp_ae

∀ {α : Type u_1} {X : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace X]
  [TopologicalSpace.MetrizableSpace X] [Nonempty X] {f : α → α} {g : α → X},
  Ergodic f μ → MeasureTheory.AEStronglyMeasurable g μ → g ∘ f =ᵐ[μ] g → ∃ c, 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.

Defined in

Mathlib.Dynamics.Ergodic.Function

Cited by

0 results in Mathlib

Foundations

Depth 210 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceTopologicalSpaceTopologicalSpace.MetrizableSpaceNonempty