Commit 2023-06-06 06:00 c340d963

View on Github →

feat: port MeasureTheory.Measure.WithDensityVectorMeasure (#4715)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Measure/VectorMeasure.lean

added def MeasureTheory.Measure.toENNRealVectorMeasure

added theorem MeasureTheory.Measure.toENNRealVectorMeasure_add

added theorem MeasureTheory.Measure.toENNRealVectorMeasure_apply_measurable

added theorem MeasureTheory.Measure.toENNRealVectorMeasure_zero

deleted def MeasureTheory.Measure.toEnnrealVectorMeasure

deleted theorem MeasureTheory.Measure.toEnnrealVectorMeasure_add

deleted theorem MeasureTheory.Measure.toEnnrealVectorMeasure_apply_measurable

deleted theorem MeasureTheory.Measure.toEnnrealVectorMeasure_zero

Created Mathlib/MeasureTheory/Measure/WithDensityVectorMeasure.lean

added theorem MeasureTheory.Integrable.ae_eq_of_withDensityᵥ_eq

added theorem MeasureTheory.Integrable.withDensityᵥ_eq_iff

added theorem MeasureTheory.Integrable.withDensityᵥ_trim_absolutelyContinuous

added theorem MeasureTheory.Integrable.withDensityᵥ_trim_eq_integral

added def MeasureTheory.Measure.withDensityᵥ

added theorem MeasureTheory.Measure.withDensityᵥ_absolutelyContinuous

added theorem MeasureTheory.WithDensityᵥEq.congr_ae

added theorem MeasureTheory.withDensityᵥ_add'

added theorem MeasureTheory.withDensityᵥ_add

added theorem MeasureTheory.withDensityᵥ_apply

added theorem MeasureTheory.withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part

added theorem MeasureTheory.withDensityᵥ_neg'

added theorem MeasureTheory.withDensityᵥ_neg

added theorem MeasureTheory.withDensityᵥ_smul'

added theorem MeasureTheory.withDensityᵥ_smul

added theorem MeasureTheory.withDensityᵥ_sub'

added theorem MeasureTheory.withDensityᵥ_sub

added theorem MeasureTheory.withDensityᵥ_toReal

added theorem MeasureTheory.withDensityᵥ_zero