ergodic_mul_left_of_denseRange_pow

English

If powers of g are dense in G, left-multiplication by g is ergodic.

Русский

Если степени g образуют плотное множество в G, левая сумма g эргодична.

LaTeX

$$$\text{DenseRange\_pow}\ (g)\Rightarrow Ergodic (g * ·) μ$$$

Lean4

@[to_additive]
theorem ergodic_mul_left_of_denseRange_pow (hg : DenseRange (g ^ · : ℕ → G)) (μ : Measure G) [IsFiniteMeasure μ]
    [μ.InnerRegular] [μ.IsMulLeftInvariant] : Ergodic (g * ·) μ :=
  ergodic_smul_of_denseRange_pow hg μ

Похожие утверждения