ergodic_mul_left_of_denseRange_zpow

English

Equivalence: ergodicity of left multiplication by g is equivalent to density of g^ℤ in G.

Русский

Эквивалентность: эргодичность левого умножения на g равна плотности g^ℤ в G.

LaTeX

$$$\text{Ergodic}(g * ·) μ \iff DenseRange (g^⋅ : ℤ → G)$$$

Lean4

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

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