Theorems · Inductive type · dynamical systems
ErgodicSMul
(G : Type u_1) → (α : Type u_2) → [SMul G α] → {x : MeasurableSpace α} → MeasureTheory.Measure α → PropA 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
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- SMul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement · cited by 13,106
- MeasureTheory.Measurestatement · cited by 10,939
Cited by17
Results whose statement or proof uses this declaration.
- aeconst_of_dense_setOfPred_preimage_smul_aestatement and proof · cited by 4
- aeconst_of_dense_setOfPred_preimage_smul_eqstatement and proof · cited by 3
- MeasureTheory.aeconst_of_forall_preimage_smul_ae_eqstatement and proof · cited by 2
- ErgodicSMul.aeconst_of_forall_preimage_smul_ae_eqstatement and proof · cited by 1
- ErgodicSMul.casesOnstatement and proof · cited by 1
- MeasureTheory.aeconst_of_forall_smul_ae_eqstatement and proof · cited by 1
- aeconst_of_dense_aestabilizer_smulstatement and proof · cited by 1
- ergodic_smul_of_denseRange_powstatement and proof · cited by 1
- ergodic_smul_of_denseRange_zpowstatement and proof · cited by 1
- MeasureTheory.ergodicSMul_iterateMulActstatement · cited by 0
- ErgodicSMul.of_aestabilizerstatement · cited by 0
- ErgodicSMul.recOnstatement and proof · cited by 0