Theorems · Theorem · dynamical systems

DenseRange.zsmul_of_ergodic_add_left

∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [OpensMeasurableSpace G] {μ : MeasureTheory.Measure G} [μ.IsOpenPosMeasure] {g : G},
  Ergodic (fun x => g + x) μ → DenseRange fun x => x • g

If the left addition of g is ergodic with respect to a measure which is positive on nonempty open sets, then the integer multiples 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

AddGroupTopologicalSpaceIsTopologicalAddGroupMeasurableSpaceOpensMeasurableSpaceMeasureTheory.Measure.IsOpenPosMeasure