of_aestabilizer — Mathlib

English

If every set invariant under aestabilizer is ae-constant, then the action of G on X is ergodic.

Русский

Если aestabilizer G μ s верен для всех множества s тогда ergodicSMul G X μ.

LaTeX

$$$\forall G\, X\, μ,\ (\forall s, MeasurableSet s \to (Eq (MulAction.aestabilizer G μ s) Top) \to\ EventuallyConst\ s\ (ae\ μ)) \to ErgodicSMul G X μ$$$

Lean4

theorem _root_.ErgodicSMul.of_aestabilizer [Group G] [MulAction G α] [SMulInvariantMeasure G α μ]
    (h : ∀ s, MeasurableSet s → aestabilizer G μ s = ⊤ → EventuallyConst s (ae μ)) : ErgodicSMul G α μ :=
  ⟨fun hm hs ↦ h _ hm <| (Subgroup.eq_top_iff' _).2 fun g ↦ by simpa only [preimage_smul_inv] using hs g⁻¹⟩

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