Commit 2026-05-26 15:32 ef854083

View on Github →

feat(MeasureTheory): the integral of a vector-valued function against a vector measure is additive (#30230) Add some basic lemmas about the integral of a vector measure. This PR specifically focuses on the additivity of the integral. Created with the help of Codex.

Estimated changes

Modified Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean

added theorem MeasureTheory.DominatedFinMeasAdditive.add_measure

added theorem MeasureTheory.DominatedFinMeasAdditive.finsetSum_measure

added theorem MeasureTheory.DominatedFinMeasAdditive.neg

added theorem MeasureTheory.DominatedFinMeasAdditive.of_le

added theorem MeasureTheory.DominatedFinMeasAdditive.sub_measure

added theorem MeasureTheory.FinMeasAdditive.add_left_measure

added theorem MeasureTheory.FinMeasAdditive.add_measure

added theorem MeasureTheory.FinMeasAdditive.add_right_measure

added theorem MeasureTheory.FinMeasAdditive.neg

added theorem MeasureTheory.FinMeasAdditive.sub

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean

added theorem MeasureTheory.setToFun_add_measure

added theorem MeasureTheory.setToFun_finsetSum_measure

added theorem MeasureTheory.setToFun_neg'

added theorem MeasureTheory.setToFun_sub_measure

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Basic.lean

added theorem MeasureTheory.VectorMeasure.apply_eq_zero_of_isEmpty

added theorem MeasureTheory.VectorMeasure.coe_finsetSum

added theorem MeasureTheory.VectorMeasure.eq_zero_of_isEmpty

Modified Mathlib/MeasureTheory/VectorMeasure/Integral.lean

modified theorem MeasureTheory.VectorMeasure.integral_add

added theorem MeasureTheory.VectorMeasure.integral_add_cbm

added theorem MeasureTheory.VectorMeasure.integral_add_vectorMeasure

added theorem MeasureTheory.VectorMeasure.integral_congr_ae

added theorem MeasureTheory.VectorMeasure.integral_eq_zero_of_ae

added theorem MeasureTheory.VectorMeasure.integral_finsetSum

added theorem MeasureTheory.VectorMeasure.integral_finsetSum_cbm

added theorem MeasureTheory.VectorMeasure.integral_finsetSum_vectorMeasure

modified theorem MeasureTheory.VectorMeasure.integral_fun_add

modified theorem MeasureTheory.VectorMeasure.integral_fun_neg

modified theorem MeasureTheory.VectorMeasure.integral_fun_smul

modified theorem MeasureTheory.VectorMeasure.integral_fun_sub

modified theorem MeasureTheory.VectorMeasure.integral_neg

added theorem MeasureTheory.VectorMeasure.integral_neg_cbm

added theorem MeasureTheory.VectorMeasure.integral_neg_vectorMeasure

added theorem MeasureTheory.VectorMeasure.integral_of_isEmpty

modified theorem MeasureTheory.VectorMeasure.integral_smul

modified theorem MeasureTheory.VectorMeasure.integral_sub

added theorem MeasureTheory.VectorMeasure.integral_sub_cbm

added theorem MeasureTheory.VectorMeasure.integral_sub_vectorMeasure

added theorem MeasureTheory.VectorMeasure.integral_undef

added theorem MeasureTheory.VectorMeasure.integral_zero

added theorem MeasureTheory.VectorMeasure.integral_zero_cbm

added theorem MeasureTheory.VectorMeasure.integral_zero_vectorMeasure

added theorem MeasureTheory.VectorMeasure.transpose_add_cbm

added theorem MeasureTheory.VectorMeasure.transpose_add_vectorMeasure

added theorem MeasureTheory.VectorMeasure.transpose_finsetSum_cbm

added theorem MeasureTheory.VectorMeasure.transpose_finsetSum_vectorMeasure

added theorem MeasureTheory.VectorMeasure.transpose_neg_cbm

added theorem MeasureTheory.VectorMeasure.transpose_neg_vectorMeasure

added theorem MeasureTheory.VectorMeasure.transpose_sub_cbm

added theorem MeasureTheory.VectorMeasure.transpose_sub_vectorMeasure

added theorem MeasureTheory.VectorMeasure.transpose_zero_cbm

added theorem MeasureTheory.VectorMeasure.transpose_zero_vectorMeasure