English
If aestabilizer set is dense in G, then ae-const holds for s.
Русский
Если aestabilizer плотен в G, то множество s ae-константно.
LaTeX
$$$\text{aeconst\_of\_dense\_aestabilizer\_smul}\ G\ hsm\ hd$$
Lean4
/-- If a monoid `M` continuously acts on an R₁ topological space `X`,
`g` is an element of `M such that its integer 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 integer 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_zpow {g : G} (hg : DenseRange (g ^ · : ℤ → G)) (μ : Measure X) [IsFiniteMeasure μ]
[μ.InnerRegular] [ErgodicSMul G X μ] : Ergodic (g • ·) μ :=
by
borelize G
refine ⟨measurePreserving_smul _ _, ⟨fun s hsm hs ↦ ?_⟩⟩
refine aeconst_of_dense_aestabilizer_smul hsm.nullMeasurableSet (hg.mono ?_)
rw [← Subgroup.coe_zpowers, SetLike.coe_subset_coe, ← Subgroup.zpowers_inv, Subgroup.zpowers_le,
MulAction.mem_aestabilizer, ← preimage_smul, hs]
