Theorems · Theorem · dynamical systems

ergodic_smul_of_denseRange_zpow

∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [ContinuousInv G] {X : Type u_2}
  [inst_3 : TopologicalSpace X] [R1Space X] [inst_5 : MeasurableSpace X] [BorelSpace X] [inst_7 : MulAction G X]
  [ContinuousSMul G X] {g : G},
  (DenseRange fun x => g ^ x) →
    ∀ (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul G X μ],
      Ergodic (fun x => g • x) μ

If a monoid M continuously acts on an R₁ topological space X, g is an element of M such that its integer powers are dense in M, and μ is a finite inner regular measure on X which is ergodic with respect to the action of M, then the scalar multiplication by g is an ergodic map.

Defined in

Mathlib.Dynamics.Ergodic.Action.OfMinimal

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupTopologicalSpaceContinuousInvTopologicalSpaceR1SpaceMeasurableSpaceBorelSpaceMulActionContinuousSMulMeasureTheory.IsFiniteMeasureMeasureTheory.Measure.InnerRegularErgodicSMul