Structures · Other
ErgodicVAdd
An additive 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 addition (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_vadd_ae_eq
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- AddOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- aeconst_of_dense_setOfPred_preimage_vadd_ae
- aeconst_of_dense_setOfPred_preimage_vadd_eq
- MeasureTheory.aeconst_of_forall_preimage_vadd_ae_eq
- MeasureTheory.aeconst_of_forall_vadd_ae_eq
- ergodic_vadd_of_denseRange_zsmul
- ergodic_vadd_of_denseRange_nsmul
- aeconst_of_dense_aestabilizer_vadd
- ErgodicVAdd.aeconst_of_forall_preimage_vadd_ae_eq
- aeconst_of_dense_setOf_preimage_vadd_eq
- AddAction.aeconst_of_aestabilizer_eq_top
- aeconst_of_dense_setOf_preimage_vadd_ae
- ErgodicVAdd.trans_isMinimal
- ErgodicVAdd.toVAddInvariantMeasure