Theorems · Theorem · dynamical systems

ergodic_add_left_iff_denseRange_zsmul

∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [SecondCountableTopology G] [BorelSpace G] {g : G} (μ : MeasureTheory.Measure G)
  [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [μ.IsAddLeftInvariant] [NeZero μ],
  Ergodic (fun x => g + x) μ ↔ DenseRange fun x => x • g

Defined in

Mathlib.Dynamics.Ergodic.Action.OfMinimal

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddGroupTopologicalSpaceIsTopologicalAddGroupMeasurableSpaceSecondCountableTopologyBorelSpaceMeasureTheory.IsFiniteMeasureMeasureTheory.Measure.InnerRegularMeasureTheory.Measure.IsAddLeftInvariantNeZero