Theorems · Theorem · dynamical systems

AddMonoidHom.ergodic_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] [CompactSpace G] {μ : MeasureTheory.Measure G} [μ.IsAddHaarMeasure]
  (f : G →+ G), Dense (⋃ n, (⇑f)^[n] ⁻¹' 0) → Continuous ⇑f → Function.Surjective ⇑f → Ergodic (⇑f) μ

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

Defined in

Mathlib.Dynamics.Ergodic.Action.OfMinimal

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddGroupTopologicalSpaceIsTopologicalAddGroupSecondCountableTopologyMeasurableSpaceBorelSpaceCompactSpaceMeasureTheory.Measure.IsAddHaarMeasure