Theorems · Theorem · dynamical systems

DenseRange.zpow_of_ergodic_mul_left

∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [OpensMeasurableSpace G] {μ : MeasureTheory.Measure G} [μ.IsOpenPosMeasure] {g : G},
  Ergodic (fun x => g * x) μ → DenseRange fun x => g ^ x

If the left multiplication by g is ergodic with respect to a measure which is positive on nonempty open sets, then the integer powers of g are dense in G.

Defined in

Mathlib.Dynamics.Ergodic.Action.OfMinimal

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupTopologicalSpaceIsTopologicalGroupMeasurableSpaceOpensMeasurableSpaceMeasureTheory.Measure.IsOpenPosMeasure