Theorems · Inductive type · dynamical systems
PreErgodic
{α : Type u_1} → {m : MeasurableSpace α} → (α → α) → autoParam (MeasureTheory.Measure α) PreErgodic._auto_1 → PropA map f : α → α is said to be pre-ergodic with respect to a measure μ if any measurable
strictly invariant set is either almost empty or full.
- Defined in
- Mathlib.Dynamics.Ergodic.Ergodic
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 9 from the axioms · uses no axioms
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 by25
Results whose statement or proof uses this declaration.
- PreErgodic.aeconst_setstatement and proof · cited by 7
- Ergodic.toPreErgodicstatement · cited by 7
- Ergodic.quasiErgodicproof · cited by 6
- PreErgodic.measure_self_or_compl_eq_zerostatement and proof · cited by 3
- PreErgodic.smul_measurestatement and proof · cited by 2
- PreErgodic.zero_measurestatement · cited by 2
- QuasiErgodic.toPreErgodicstatement · cited by 2
- MeasureTheory.MeasurePreserving.preErgodic_of_preErgodic_semiconjstatement and proof · cited by 2
- PreErgodic.ae_empty_or_univstatement and proof · cited by 1
- PreErgodic.ae_mem_or_ae_notMemstatement and proof · cited by 1
- Ergodic.zero_measureproof · cited by 1
- MonoidHom.preErgodic_of_dense_iUnion_preimage_onestatement · cited by 1