Documentation

Mathlib.Dynamics.Ergodic.Action.Regular

Regular action of a group on itself is ergodic #

In this file we prove that the left and right actions of a group on itself are ergodic.

source
instance instErgodicSMulOfIsMulLeftInvariant {G : Type u_1} [Group G] [MeasurableSpace G] [MeasurableMul₂ G] [MeasurableInv G] {μ : MeasureTheory.Measure G} [MeasureTheory.SFinite μ] [μ.IsMulLeftInvariant] :
ErgodicSMul G G μ
source
instance instErgodicVAddOfIsAddLeftInvariant {G : Type u_1} [AddGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] :
ErgodicVAdd G G μ
source
instance instErgodicSMulMulOppositeOfIsMulRightInvariant {G : Type u_1} [Group G] [MeasurableSpace G] [MeasurableMul₂ G] [MeasurableInv G] {μ : MeasureTheory.Measure G} [MeasureTheory.SFinite μ] [μ.IsMulRightInvariant] :
ErgodicSMul Gᵐᵒᵖ G μ
source
instance instErgodicVAddAddOppositeOfIsAddRightInvariant {G : Type u_1} [AddGroup G] [MeasurableSpace G] [MeasurableAdd₂ G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant] :
ErgodicVAdd Gᵃᵒᵖ G μ