Theorems · Theorem · dynamical systems

ergodic_vadd_of_denseRange_nsmul

∀ {X : Type u_2} [inst : TopologicalSpace X] [R1Space X] [inst_2 : MeasurableSpace X] [BorelSpace X] {M : Type u_3}
  [inst_4 : AddMonoid M] [inst_5 : TopologicalSpace M] [inst_6 : AddAction M X] [ContinuousVAdd M X] {g : M},
  (DenseRange fun x => x • g) →
    ∀ (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd M X μ],
      Ergodic (fun x => g +ᵥ x) μ

If an additive monoid M continuously acts on an R₁ topological space X, g is an element of M such that its natural multiples 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 vector addition of 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

TopologicalSpaceR1SpaceMeasurableSpaceBorelSpaceAddMonoidTopologicalSpaceAddActionContinuousVAddMeasureTheory.IsFiniteMeasureMeasureTheory.Measure.InnerRegularErgodicVAdd