Theorems · Theorem · dynamical systems

AddMonoidHom.preErgodic_of_dense_iUnion_preimage_zero

∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [SecondCountableTopology G]
  [inst_4 : MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [MeasureTheory.IsFiniteMeasure μ]
  [μ.InnerRegular] [μ.IsAddLeftInvariant] (f : G →+ G), Dense (⋃ n, (⇑f)^[n] ⁻¹' 0) → PreErgodic (⇑f) μ

Let f : G →+ G be an additive group endomorphism of a topological additive group with second countable topology. If the preimages of 0 under the iterations of f are dense, then it is pre-ergodic with respect to any finite inner regular left invariant measure.

Defined in

Mathlib.Dynamics.Ergodic.Action.OfMinimal

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddGroupTopologicalSpaceIsTopologicalAddGroupSecondCountableTopologyMeasurableSpaceBorelSpaceMeasureTheory.IsFiniteMeasureMeasureTheory.Measure.InnerRegularMeasureTheory.Measure.IsAddLeftInvariant