Commit 2026-10-04 13:42 700eb6b6

View on Github →

chore: move QuasiMeasurePreserving to the namespace of MeasurePreserving (#44142) Moves QuasiMeasurePreserving to the MeasureTheory namespace, so that it matches the namespace of MeasurePreserving.

Estimated changes

Modified Mathlib/Dynamics/BirkhoffSum/QuasiMeasurePreserving.lean

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.birkhoffAverage_ae_eq_of_ae_eq

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.birkhoffSum_ae_eq_of_ae_eq

added theorem MeasureTheory.QuasiMeasurePreserving.birkhoffAverage_ae_eq_of_ae_eq

added theorem MeasureTheory.QuasiMeasurePreserving.birkhoffSum_ae_eq_of_ae_eq

Modified Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean

Modified Mathlib/MeasureTheory/Function/AEEqFun.lean

Modified Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.ae

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq_comp

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.ae_map_le

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.image_zpow_ae_eq

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.liminf_preimage_iterate_ae_eq

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.limsup_preimage_iterate_ae_eq

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.mono

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.mono_left

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.mono_right

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.preimage_ae_eq

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.preimage_iterate_ae_eq

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.preimage_mono_ae

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.smul_ae_eq_of_ae_eq

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.smul_measure

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.tendsto_ae

deleted structure MeasureTheory.Measure.QuasiMeasurePreserving

deleted theorem MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_one

added theorem MeasureTheory.QuasiMeasurePreserving.ae

added theorem MeasureTheory.QuasiMeasurePreserving.ae_eq_comp

added theorem MeasureTheory.QuasiMeasurePreserving.ae_map_le

added theorem MeasureTheory.QuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae

added theorem MeasureTheory.QuasiMeasurePreserving.image_zpow_ae_eq

added theorem MeasureTheory.QuasiMeasurePreserving.liminf_preimage_iterate_ae_eq

added theorem MeasureTheory.QuasiMeasurePreserving.limsup_preimage_iterate_ae_eq

added theorem MeasureTheory.QuasiMeasurePreserving.mono

added theorem MeasureTheory.QuasiMeasurePreserving.mono_left

added theorem MeasureTheory.QuasiMeasurePreserving.mono_right

added theorem MeasureTheory.QuasiMeasurePreserving.preimage_ae_eq

added theorem MeasureTheory.QuasiMeasurePreserving.preimage_iterate_ae_eq

added theorem MeasureTheory.QuasiMeasurePreserving.preimage_mono_ae

added theorem MeasureTheory.QuasiMeasurePreserving.preimage_null

added theorem MeasureTheory.QuasiMeasurePreserving.smul_ae_eq_of_ae_eq

added theorem MeasureTheory.QuasiMeasurePreserving.smul_measure

added theorem MeasureTheory.QuasiMeasurePreserving.tendsto_ae

added structure MeasureTheory.QuasiMeasurePreserving

added theorem MeasureTheory.pairwise_aedisjoint_of_aedisjoint_forall_ne_one

Modified Mathlib/NumberTheory/WellApproximable.lean

Modified Mathlib/Probability/Kernel/CondDistrib.lean