Theorems · Theorem · dynamical systems

PreErgodic.ae_eq_const_of_ae_eq_comp

∀ {α : Type u_1} {X : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [Nonempty X]
  [inst_2 : MeasurableSpace X] [MeasurableSpace.CountablySeparated X] {f : α → α} {g : α → X},
  PreErgodic f μ → Measurable g → g ∘ f = g → ∃ c, 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.

Defined in

Mathlib.Dynamics.Ergodic.Function

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceNonemptyMeasurableSpaceMeasurableSpace.CountablySeparated