Commit 2023-10-05 17:31 943f6a16

View on Github →

chore: put Measure.withDensity into a new file (#7508) It was in Integral.Lebesgue, which is about the definition of the Lebesgue integral.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

deleted def MeasureTheory.Measure.withDensity

deleted theorem MeasureTheory.ae_withDensity_iff

deleted theorem MeasureTheory.ae_withDensity_iff_ae_restrict

deleted theorem MeasureTheory.aemeasurable_withDensity_ennreal_iff

deleted theorem MeasureTheory.exists_absolutelyContinuous_isFiniteMeasure

deleted theorem MeasureTheory.isFiniteMeasure_withDensity

deleted theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul

deleted theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable

deleted theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable₀

deleted theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀'

deleted theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀

deleted theorem MeasureTheory.lintegral_withDensity_le_lintegral_mul

deleted theorem MeasureTheory.restrict_withDensity

deleted theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul

deleted theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable

deleted theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable₀

deleted theorem MeasureTheory.withDensity_absolutelyContinuous

deleted theorem MeasureTheory.withDensity_add_left

deleted theorem MeasureTheory.withDensity_add_measure

deleted theorem MeasureTheory.withDensity_add_right

deleted theorem MeasureTheory.withDensity_apply

deleted theorem MeasureTheory.withDensity_apply_eq_zero

deleted theorem MeasureTheory.withDensity_congr_ae

deleted theorem MeasureTheory.withDensity_eq_zero

deleted theorem MeasureTheory.withDensity_indicator

deleted theorem MeasureTheory.withDensity_indicator_one

deleted theorem MeasureTheory.withDensity_mul

deleted theorem MeasureTheory.withDensity_ofReal_mutuallySingular

deleted theorem MeasureTheory.withDensity_one

deleted theorem MeasureTheory.withDensity_smul'

deleted theorem MeasureTheory.withDensity_smul

deleted theorem MeasureTheory.withDensity_sum

deleted theorem MeasureTheory.withDensity_tsum

deleted theorem MeasureTheory.withDensity_zero

Modified Mathlib/MeasureTheory/Integral/LebesgueNormedSpace.lean

Created Mathlib/MeasureTheory/Measure/WithDensity.lean

added def MeasureTheory.Measure.withDensity

added theorem MeasureTheory.ae_withDensity_iff

added theorem MeasureTheory.ae_withDensity_iff_ae_restrict

added theorem MeasureTheory.aemeasurable_withDensity_ennreal_iff

added theorem MeasureTheory.exists_absolutelyContinuous_isFiniteMeasure

added theorem MeasureTheory.isFiniteMeasure_withDensity

added theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul

added theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable

added theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable₀

added theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀'

added theorem MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀

added theorem MeasureTheory.lintegral_withDensity_le_lintegral_mul

added theorem MeasureTheory.restrict_withDensity

added theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul

added theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable

added theorem MeasureTheory.set_lintegral_withDensity_eq_set_lintegral_mul_non_measurable₀

added theorem MeasureTheory.withDensity_absolutelyContinuous

added theorem MeasureTheory.withDensity_add_left

added theorem MeasureTheory.withDensity_add_measure

added theorem MeasureTheory.withDensity_add_right

added theorem MeasureTheory.withDensity_apply

added theorem MeasureTheory.withDensity_apply_eq_zero

added theorem MeasureTheory.withDensity_congr_ae

added theorem MeasureTheory.withDensity_eq_zero

added theorem MeasureTheory.withDensity_indicator

added theorem MeasureTheory.withDensity_indicator_one

added theorem MeasureTheory.withDensity_mul

added theorem MeasureTheory.withDensity_ofReal_mutuallySingular

added theorem MeasureTheory.withDensity_one

added theorem MeasureTheory.withDensity_smul'

added theorem MeasureTheory.withDensity_smul

added theorem MeasureTheory.withDensity_sum

added theorem MeasureTheory.withDensity_tsum

added theorem MeasureTheory.withDensity_zero