aeconst_of_dense_aestabilizer_smul

English

If left multiplication by g is ergodic, then z-powers g^ℤ are dense in G.

Русский

Если левая дифференциация умножения на g эргодична, то z-степени g^ℤ плотны в G.

LaTeX

$$$\text{Ergodic}(g \cdot) μ \Rightarrow DenseRange (g^⋅ : ℤ → G)$$$

Lean4

@[to_additive]
theorem aeconst_of_dense_aestabilizer_smul (hsm : NullMeasurableSet s μ)
    (hd : Dense (MulAction.aestabilizer G μ s : Set G)) : EventuallyConst s (ae μ) :=
  aeconst_of_dense_setOf_preimage_smul_ae hsm <|
    (hd.preimage (isOpenMap_inv _)).mono fun g hg ↦ by simpa only [preimage_smul] using hg

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