English
If an element g has its powers dense in a monoid M, then the action by g on X is ergodic.
Русский
Если степень элемента g порождает плотное множество в M, то действие g на X эргодично.
LaTeX
$$$\text{ergodic\_smul\_pow}\ (g\, \text{dense range})\ μ\Rightarrow Ergodic (g\cdot) μ$$$
Lean4
/-- If a monoid `M` continuously acts on an R₁ topological space `X`,
`g` is an element of `M such that its natural powers are dense in `M`,
and `μ` is a finite inner regular measure on `X` which is ergodic with respect to the action of `M`,
then the scalar multiplication by `g` is an ergodic map. -/
@[to_additive /-- If an additive monoid `M` continuously acts on an R₁ topological space `X`,
`g` is an element of `M such that its natural multiples are dense in `M`,
and `μ` is a finite inner regular measure on `X` which is ergodic with respect to the action of `M`,
then the vector addition of `g` is an ergodic map. -/
]
theorem ergodic_smul_of_denseRange_pow {M : Type*} [Monoid M] [TopologicalSpace M] [MulAction M X] [ContinuousSMul M X]
{g : M} (hg : DenseRange (g ^ · : ℕ → M)) (μ : Measure X) [IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul M X μ] :
Ergodic (g • ·) μ := by
borelize M
refine ⟨measurePreserving_smul _ _, ⟨fun s hsm hs ↦ ?_⟩⟩
refine aeconst_of_dense_setOf_preimage_smul_eq hsm.nullMeasurableSet (hg.mono ?_)
refine range_subset_iff.2 fun n ↦ ?_
rw [mem_setOf, ← smul_iterate, preimage_iterate_eq, iterate_fixed hs]
