Commit 2023-05-10 07:35 fc66e256

View on Github →

feat: port Dynamics.Ergodic.Ergodic (#3879)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Dynamics/Ergodic/Ergodic.lean

added theorem Ergodic.ae_empty_or_univ_of_ae_le_preimage'

added theorem Ergodic.ae_empty_or_univ_of_ae_le_preimage

added theorem Ergodic.ae_empty_or_univ_of_image_ae_le'

added theorem Ergodic.ae_empty_or_univ_of_image_ae_le

added theorem Ergodic.ae_empty_or_univ_of_preimage_ae_le'

added theorem Ergodic.ae_empty_or_univ_of_preimage_ae_le

added theorem Ergodic.quasiErgodic

added structure Ergodic

added theorem MeasureTheory.MeasurePreserving.ergodic_conjugate_iff

added theorem MeasureTheory.MeasurePreserving.preErgodic_conjugate_iff

added theorem MeasureTheory.MeasurePreserving.preErgodic_of_preErgodic_conjugate

added theorem PreErgodic.measure_self_or_compl_eq_zero

added theorem PreErgodic.of_iterate

added theorem PreErgodic.prob_eq_zero_or_one

added structure PreErgodic

added theorem QuasiErgodic.ae_empty_or_univ'

added structure QuasiErgodic