Structures · Other
ErgodicSMul
A group action of G on a space α with measure μ is called ergodic,
if for any (null) measurable set s,
if it is a.e.-invariant under each scalar multiplication (g • ·), g : G,
then it is either null or conull.
- Defined in
- Mathlib.Dynamics.Ergodic.Action.Basic
- Shape
- 3 explicit arguments · adds aeconst_of_forall_preimage_smul_ae_eq
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- aeconst_of_dense_setOfPred_preimage_smul_ae
- aeconst_of_dense_setOfPred_preimage_smul_eq
- MeasureTheory.aeconst_of_forall_preimage_smul_ae_eq
- ErgodicSMul.aeconst_of_forall_preimage_smul_ae_eq
- ergodic_smul_of_denseRange_pow
- ergodic_smul_of_denseRange_zpow
- MeasureTheory.aeconst_of_forall_smul_ae_eq
- aeconst_of_dense_aestabilizer_smul
- aeconst_of_dense_setOf_preimage_smul_eq
- aeconst_of_dense_setOf_preimage_smul_ae
- ErgodicSMul.toSMulInvariantMeasure
- ErgodicSMul.trans_isMinimal
- MulAction.aeconst_of_aestabilizer_eq_top