English
If powers g^n with integer n are dense in G, then the action by g is ergodic.
Русский
Если целочисленные степени g^n плотно образуют G, то действие g эргодично.
LaTeX
$$$\text{ergodic\_smul}\ (g)\ μ \Rightarrow Ergodic (g\cdot) μ$$$
Lean4
/-- If `N` acts continuously and ergodically on `X` and `M` acts minimally on `N`,
then the corresponding action of `M` on `X` is ergodic. -/
@[to_additive /-- If `N` acts additively continuously and ergodically on `X` and `M` acts minimally on `N`,
then the corresponding action of `M` on `X` is ergodic. -/
]
theorem trans_isMinimal (N : Type*) [MulAction M N] [Monoid N] [TopologicalSpace N] [MulAction.IsMinimal M N]
[MulAction N X] [IsScalarTower M N X] [ContinuousSMul N X] [ErgodicSMul N X μ] : ErgodicSMul M X μ
where
measure_preimage_smul c s
hsm := by simpa only [smul_one_smul] using SMulInvariantMeasure.measure_preimage_smul (c • 1 : N) hsm
aeconst_of_forall_preimage_smul_ae_eq {s} hsm
hs := by
refine aeconst_of_dense_setOf_preimage_smul_ae (M := N) hsm.nullMeasurableSet ?_
refine (MulAction.dense_orbit M 1).mono ?_
rintro _ ⟨g, rfl⟩
simpa using hs g
