Theorems · Theorem · dynamical systems

QuasiErgodic.eq_const_of_compQuasiMeasurePreserving_eq

∀ {α : Type u_1} {X : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace X]
  [TopologicalSpace.MetrizableSpace X] [Nonempty X] {f : α → α} (h : QuasiErgodic f μ) {g : α →ₘ[μ] X},
  g.compQuasiMeasurePreserving f ⋯ = g → ∃ c, g = MeasureTheory.AEEqFun.const α c

Defined in

Mathlib.Dynamics.Ergodic.Function

Cited by

1 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceTopologicalSpace.MetrizableSpaceNonempty