English
If a monoid endomorphism has dense preimages under its iterates, then it is ergodic w.r.t. Haar measure on G.
Русский
Если предобразования под итерациями моноидного гомоморфизма плотны, то он эргодичен относительно Haar-меры на G.
LaTeX
$$$\forall f : G \to G, Dense (⋃ n, f^[n] ⁻¹' 1) \to Continuous f \to Surjective f \to Ergodic f μ$$$
Lean4
/-- Let `f : G →* G` be a continuous surjective group endomorphism
of a compact topological group with second countable topology.
If the preimages of `1` under the iterations of `f` are dense,
then `f` is ergodic with respect to any finite inner regular left invariant measure. -/
@[to_additive /-- 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. -/
]
theorem ergodic_of_dense_iUnion_preimage_one [CompactSpace G] {μ : Measure G} [μ.IsHaarMeasure] (f : G →* G)
(hf : Dense (⋃ n, f^[n] ⁻¹' 1)) (hcont : Continuous f) (hsurj : Surjective f) : Ergodic f μ :=
⟨f.measurePreserving hcont hsurj rfl, f.preErgodic_of_dense_iUnion_preimage_one hf⟩
