Commit 2026-06-04 12:13 c6f1227d

View on Github →

feat: more API for the variation of vector measures (#40188)

Estimated changes

Modified Mathlib/MeasureTheory/Measure/PreVariation.lean

added theorem MeasureTheory.preVariation.exists_Finpartition_sum_ge'

Modified Mathlib/MeasureTheory/VectorMeasure/Basic.lean

modified def MeasureTheory.VectorMeasure.mapGm

modified def MeasureTheory.VectorMeasure.mapRangeHom

modified def MeasureTheory.VectorMeasure.mapRangeₗ

modified def MeasureTheory.VectorMeasure.restrictGm

added theorem MeasureTheory.VectorMeasure.restrict_map

added theorem MeasureTheory.VectorMeasure.restrict_toSignedMeasure

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

added theorem MeasureTheory.VectorMeasure.exists_variation_le_add'

added theorem MeasureTheory.VectorMeasure.exists_variation_le_add

added theorem MeasureTheory.VectorMeasure.variation_toSignedMeasure

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