English
If preimages under a dense union of iterations are dense, then a monoid endomorphism is preergodic w.r.t. μ.
Русский
Если предобразования под плотной последовательностью итераций плотны, то моноидный гомоморфизм предэргодичен относительно μ.
LaTeX
$$$\forall f : G \to G, Dense (⋃ n, f^[n] ⁻¹' 1) \to PreErgodic (coe f) μ$$$
Lean4
/-- Let `f : G →* G` be a group endomorphism of a topological group with second countable topology.
If the preimages of `1` under the iterations of `f` are dense,
then it is preergodic with respect to any finite inner regular left invariant measure. -/
@[to_additive /-- 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 preergodic with respect to any finite inner regular left invariant measure. -/
]
theorem preErgodic_of_dense_iUnion_preimage_one {μ : Measure G} [IsFiniteMeasure μ] [μ.InnerRegular]
[μ.IsMulLeftInvariant] (f : G →* G) (hf : Dense (⋃ n, f^[n] ⁻¹' 1)) : PreErgodic f μ :=
by
refine ⟨fun s hsm hs ↦ aeconst_of_dense_setOf_preimage_smul_eq (M := G) hsm.nullMeasurableSet ?_⟩
refine hf.mono <| iUnion_subset fun n x hx ↦ ?_
have hsn : f^[n] ⁻¹' s = s := by rw [preimage_iterate_eq, iterate_fixed hs]
rw [mem_preimage, Set.mem_one] at hx
rw [mem_setOf, ← hsn]
ext y
simp [hx]
