Theorems · Theorem · dynamical systems
Ergodic.toMeasurePreserving
∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → α} {μ : autoParam (MeasureTheory.Measure α) Ergodic._auto_1},
Ergodic f μ → MeasureTheory.MeasurePreserving f μ μ- Defined in
- Mathlib.Dynamics.Ergodic.Ergodic
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- MeasureTheory.MeasurePreservingstatement · cited by 259
- Ergodicstatement and proof · cited by 48
Cited by12
Results whose statement or proof uses this declaration.
- Ergodic.quasiErgodicproof · cited by 6
- Ergodic.mem_extremePoints_measure_univ_eqproof · cited by 2
- Ergodic.ae_empty_or_univ_of_ae_le_preimage'proof · cited by 2
- Ergodic.symmproof · cited by 1
- Ergodic.ae_empty_or_univ_of_image_ae_le'proof · cited by 1
- Ergodic.ae_empty_or_univ_of_preimage_ae_le'proof · cited by 1
- Ergodic.eq_smul_of_absolutelyContinuousproof · cited by 1
- MeasureTheory.MeasurePreserving.ergodic_conjugate_iffproof · cited by 1
- Ergodic.smul_measureproof · cited by 0
- MeasureTheory.ergodicSMul_iterateMulActproof · cited by 0
- Ergodic.eq_const_of_compMeasurePreserving_eqstatement and proof · cited by 0
- MeasureTheory.MeasurePreserving.ergodic_of_ergodic_semiconjproof · cited by 0