Theorem MeasureTheory.Measure.QuasiMeasurePreserving.birkhoffAverage_ae_eq_of_ae_eq

Modification history

2026-10-04 13:42
Mathlib/Dynamics/BirkhoffSum/QuasiMeasurePreserving.lean
chore: move `QuasiMeasurePreserving` to the namespace of `MeasurePreserving` (#44142) …
Deleted MeasureTheory.Measure.QuasiMeasurePreserving.birkhoffAverage_ae_eq_of_ae_eqView on Github →
2025-08-18 01:29
Mathlib/Dynamics/BirkhoffSum/QuasiMeasurePreserving.lean
feat(Dynamics/BirkhoffSum): add 2 lemmas for `birkhoffSum`/`birkhoffAverage` concerning `ae_eq` observables (#26074) …
Added MeasureTheory.Measure.QuasiMeasurePreserving.birkhoffAverage_ae_eq_of_ae_eqView on Github →