Commit 2025-01-07 20:33 1e7c41df

View on Github →

chore: extract 3 new files out of MeasureSpace (#20509) The MeasureSpace file contains many definitions about measures and is 2000 lines long. This PR splits 3 files by taking material from the bottom of MeasureSpace:

Map: map of a measure by a function
AbsolutelyContinuous: absolute continuity of measures
QuasiMeasurePreserving: quasi measure preserving functions

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Covering/VitaliFamily.lean

Modified Mathlib/MeasureTheory/Group/Defs.lean

Created Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean

added theorem MeasurableEmbedding.absolutelyContinuous_map

added theorem MeasureTheory.Measure.AbsolutelyContinuous.add_left

added theorem MeasureTheory.Measure.AbsolutelyContinuous.add_left_iff

added theorem MeasureTheory.Measure.AbsolutelyContinuous.add_right

added theorem MeasureTheory.Measure.AbsolutelyContinuous.ae_eq

added theorem MeasureTheory.Measure.AbsolutelyContinuous.mk

added def MeasureTheory.Measure.AbsolutelyContinuous

added theorem MeasureTheory.Measure.absolutelyContinuous_of_eq

added theorem MeasureTheory.Measure.absolutelyContinuous_of_le

added theorem MeasureTheory.Measure.absolutelyContinuous_of_le_smul

added theorem MeasureTheory.Measure.absolutelyContinuous_smul

added theorem MeasureTheory.Measure.absolutelyContinuous_sum_left

added theorem MeasureTheory.Measure.absolutelyContinuous_sum_right

added theorem MeasureTheory.Measure.absolutelyContinuous_zero_iff

added theorem MeasureTheory.Measure.ae_le_iff_absolutelyContinuous

added theorem MeasureTheory.Measure.smul_absolutelyContinuous

added theorem MeasureTheory.ae_mono

Modified Mathlib/MeasureTheory/Measure/Comap.lean

Created Mathlib/MeasureTheory/Measure/Map.lean

added theorem AEMeasurable.of_map_ne_zero

added theorem MeasurableEquiv.map_ae

added theorem MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq

added theorem MeasurableEquiv.map_map_symm

added theorem MeasurableEquiv.map_measurableEquiv_injective

added theorem MeasurableEquiv.map_symm_map

added theorem MeasureTheory.Measure.le_liftLinear_apply

added theorem MeasureTheory.Measure.le_map_apply

added theorem MeasureTheory.Measure.le_map_apply_image

added def MeasureTheory.Measure.liftLinear

added theorem MeasureTheory.Measure.liftLinear_apply

added theorem MeasureTheory.Measure.liftLinear_apply₀

added theorem MeasureTheory.Measure.map_add

added theorem MeasureTheory.Measure.map_apply

added theorem MeasureTheory.Measure.map_apply_of_aemeasurable

added theorem MeasureTheory.Measure.map_apply₀

added theorem MeasureTheory.Measure.map_congr

added theorem MeasureTheory.Measure.map_eq_zero_iff

added theorem MeasureTheory.Measure.map_id'

added theorem MeasureTheory.Measure.map_id

added theorem MeasureTheory.Measure.map_map

added theorem MeasureTheory.Measure.map_mono

added theorem MeasureTheory.Measure.map_ne_zero_iff

added theorem MeasureTheory.Measure.map_of_not_aemeasurable

added theorem MeasureTheory.Measure.map_toOuterMeasure

added theorem MeasureTheory.Measure.map_zero

added def MeasureTheory.Measure.mapₗ

added theorem MeasureTheory.Measure.mapₗ_apply_of_measurable

added theorem MeasureTheory.Measure.mapₗ_congr

added theorem MeasureTheory.Measure.mapₗ_eq_zero_iff

added theorem MeasureTheory.Measure.mapₗ_mk_apply_of_aemeasurable

added theorem MeasureTheory.Measure.mapₗ_ne_zero_iff

added theorem MeasureTheory.Measure.measure_preimage_of_map_eq_self

added theorem MeasureTheory.Measure.preimage_null_of_map_null

added theorem MeasureTheory.Measure.tendsto_ae_map

added theorem MeasureTheory.ae_map_iff

added theorem MeasureTheory.ae_map_mem_range

added theorem MeasureTheory.ae_of_ae_map

added theorem MeasureTheory.mem_ae_map_iff

added theorem MeasureTheory.mem_ae_of_mem_ae_map

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

deleted theorem AEMeasurable.of_map_ne_zero

deleted theorem MeasurableEmbedding.absolutelyContinuous_map

deleted theorem MeasurableEquiv.map_ae

deleted theorem MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq

deleted theorem MeasurableEquiv.map_map_symm

deleted theorem MeasurableEquiv.map_measurableEquiv_injective

deleted theorem MeasurableEquiv.map_symm_map

deleted theorem MeasurableEquiv.quasiMeasurePreserving_symm

deleted theorem MeasureTheory.AEDisjoint.preimage

deleted theorem MeasureTheory.Measure.AbsolutelyContinuous.add_left

deleted theorem MeasureTheory.Measure.AbsolutelyContinuous.add_left_iff

deleted theorem MeasureTheory.Measure.AbsolutelyContinuous.add_right

deleted theorem MeasureTheory.Measure.AbsolutelyContinuous.ae_eq

deleted theorem MeasureTheory.Measure.AbsolutelyContinuous.mk

deleted def MeasureTheory.Measure.AbsolutelyContinuous

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.ae

deleted theorem MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq

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.absolutelyContinuous_of_eq

deleted theorem MeasureTheory.Measure.absolutelyContinuous_of_le

deleted theorem MeasureTheory.Measure.absolutelyContinuous_of_le_smul

deleted theorem MeasureTheory.Measure.absolutelyContinuous_smul

deleted theorem MeasureTheory.Measure.absolutelyContinuous_sum_left

deleted theorem MeasureTheory.Measure.absolutelyContinuous_sum_right

deleted theorem MeasureTheory.Measure.absolutelyContinuous_zero_iff

deleted theorem MeasureTheory.Measure.ae_le_iff_absolutelyContinuous

deleted theorem MeasureTheory.Measure.le_liftLinear_apply

deleted theorem MeasureTheory.Measure.le_map_apply

deleted theorem MeasureTheory.Measure.le_map_apply_image

deleted def MeasureTheory.Measure.liftLinear

deleted theorem MeasureTheory.Measure.liftLinear_apply

deleted theorem MeasureTheory.Measure.liftLinear_apply₀

deleted theorem MeasureTheory.Measure.map_add

deleted theorem MeasureTheory.Measure.map_apply

deleted theorem MeasureTheory.Measure.map_apply_of_aemeasurable

deleted theorem MeasureTheory.Measure.map_apply₀

deleted theorem MeasureTheory.Measure.map_congr

deleted theorem MeasureTheory.Measure.map_eq_zero_iff

deleted theorem MeasureTheory.Measure.map_id'

deleted theorem MeasureTheory.Measure.map_id

deleted theorem MeasureTheory.Measure.map_map

deleted theorem MeasureTheory.Measure.map_mono

deleted theorem MeasureTheory.Measure.map_ne_zero_iff

deleted theorem MeasureTheory.Measure.map_of_not_aemeasurable

deleted theorem MeasureTheory.Measure.map_toOuterMeasure

deleted theorem MeasureTheory.Measure.map_zero

deleted def MeasureTheory.Measure.mapₗ

deleted theorem MeasureTheory.Measure.mapₗ_apply_of_measurable

deleted theorem MeasureTheory.Measure.mapₗ_congr

deleted theorem MeasureTheory.Measure.mapₗ_eq_zero_iff

deleted theorem MeasureTheory.Measure.mapₗ_mk_apply_of_aemeasurable

deleted theorem MeasureTheory.Measure.mapₗ_ne_zero_iff

deleted theorem MeasureTheory.Measure.measure_preimage_of_map_eq_self

deleted theorem MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_one

deleted theorem MeasureTheory.Measure.preimage_null_of_map_null

deleted theorem MeasureTheory.Measure.smul_absolutelyContinuous

deleted theorem MeasureTheory.Measure.tendsto_ae_map

deleted theorem MeasureTheory.NullMeasurableSet.mono

deleted theorem MeasureTheory.NullMeasurableSet.mono_ac

deleted theorem MeasureTheory.NullMeasurableSet.preimage

deleted theorem MeasureTheory.ae_map_iff

deleted theorem MeasureTheory.ae_map_mem_range

deleted theorem MeasureTheory.ae_mono

deleted theorem MeasureTheory.ae_of_ae_map

deleted theorem MeasureTheory.mem_ae_map_iff

deleted theorem MeasureTheory.mem_ae_of_mem_ae_map

Created Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean

added theorem MeasurableEquiv.quasiMeasurePreserving_symm

added theorem MeasureTheory.AEDisjoint.preimage

added theorem MeasureTheory.Measure.QuasiMeasurePreserving.ae

added theorem MeasureTheory.Measure.QuasiMeasurePreserving.ae_eq

added theorem MeasureTheory.Measure.QuasiMeasurePreserving.ae_map_le

added theorem MeasureTheory.Measure.QuasiMeasurePreserving.exists_preimage_eq_of_preimage_ae

added theorem MeasureTheory.Measure.QuasiMeasurePreserving.image_zpow_ae_eq

added theorem MeasureTheory.Measure.QuasiMeasurePreserving.liminf_preimage_iterate_ae_eq

added theorem MeasureTheory.Measure.QuasiMeasurePreserving.limsup_preimage_iterate_ae_eq

added theorem MeasureTheory.Measure.QuasiMeasurePreserving.mono

added theorem MeasureTheory.Measure.QuasiMeasurePreserving.mono_left

added theorem MeasureTheory.Measure.QuasiMeasurePreserving.mono_right

added theorem MeasureTheory.Measure.QuasiMeasurePreserving.preimage_ae_eq

added theorem MeasureTheory.Measure.QuasiMeasurePreserving.preimage_iterate_ae_eq

added theorem MeasureTheory.Measure.QuasiMeasurePreserving.preimage_mono_ae

added theorem MeasureTheory.Measure.QuasiMeasurePreserving.preimage_null

added theorem MeasureTheory.Measure.QuasiMeasurePreserving.smul_ae_eq_of_ae_eq

added theorem MeasureTheory.Measure.QuasiMeasurePreserving.smul_measure

added theorem MeasureTheory.Measure.QuasiMeasurePreserving.tendsto_ae

added structure MeasureTheory.Measure.QuasiMeasurePreserving

added theorem MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_one

added theorem MeasureTheory.NullMeasurableSet.mono

added theorem MeasureTheory.NullMeasurableSet.mono_ac

added theorem MeasureTheory.NullMeasurableSet.preimage

Modified Mathlib/MeasureTheory/Measure/Restrict.lean