Theorems · Inductive type · dynamical systems
ErgodicVAdd
(G : Type u_1) → (α : Type u_2) → [VAdd G α] → {x : MeasurableSpace α} → MeasureTheory.Measure α → PropAn 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
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- VAdd
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- VAddstatement · cited by 616
Cited by15
Results whose statement or proof uses this declaration.
- aeconst_of_dense_setOfPred_preimage_vadd_aestatement and proof · cited by 4
- aeconst_of_dense_setOfPred_preimage_vadd_eqstatement and proof · cited by 3
- MeasureTheory.aeconst_of_forall_preimage_vadd_ae_eqstatement and proof · cited by 2
- ErgodicVAdd.aeconst_of_forall_preimage_vadd_ae_eqstatement and proof · cited by 1
- ErgodicVAdd.casesOnstatement and proof · cited by 1
- MeasureTheory.aeconst_of_forall_vadd_ae_eqstatement and proof · cited by 1
- aeconst_of_dense_aestabilizer_vaddstatement and proof · cited by 1
- ergodic_vadd_of_denseRange_nsmulstatement and proof · cited by 1
- ergodic_vadd_of_denseRange_zsmulstatement and proof · cited by 1
- AddAction.aeconst_of_aestabilizer_eq_topstatement and proof · cited by 0
- ErgodicVAdd.recOnstatement and proof · cited by 0
- ErgodicVAdd.trans_isMinimalstatement and proof · cited by 0