Commit 2026-05-30 11:56 e647009b

View on Github →

feat: more API for the variation of vector measures (#39616) Prompted by the extension of the API around integrals wrt vector measures in #39113

Estimated changes

Modified Mathlib/Data/ENNReal/Action.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Basic.lean

added theorem MeasureTheory.VectorMeasure.dirac_zero

added theorem MeasureTheory.VectorMeasure.mapRange_smul

modified def MeasureTheory.VectorMeasure.restrict

added theorem MeasureTheory.VectorMeasure.restrict_dirac

added theorem MeasureTheory.VectorMeasure.restrict_dirac_of_mem

added theorem MeasureTheory.VectorMeasure.restrict_dirac_of_notMem

added theorem MeasureTheory.VectorMeasure.restrict_inter_add_diff

added theorem MeasureTheory.VectorMeasure.restrict_restrict

added theorem MeasureTheory.VectorMeasure.restrict_singleton

added theorem MeasureTheory.VectorMeasure.restrict_union

added theorem MeasureTheory.VectorMeasure.restrict_union_add_inter

Modified Mathlib/MeasureTheory/VectorMeasure/Decomposition/JordanSub.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Variation/Basic.lean

added theorem MeasurableEmbedding.variation_map

added theorem MeasureTheory.VectorMeasure.variation_apply_eq_zero

added theorem MeasureTheory.VectorMeasure.variation_apply_le_of_forall_enorm_le

added theorem MeasureTheory.VectorMeasure.variation_dirac

added theorem MeasureTheory.VectorMeasure.variation_eq_zero

added theorem MeasureTheory.VectorMeasure.variation_map_le

added theorem MeasureTheory.VectorMeasure.variation_restrict

added theorem MeasureTheory.VectorMeasure.variation_restrict_le

added theorem MeasureTheory.VectorMeasure.variation_smul