Commit 2026-06-06 06:16 d46bd453

View on Github →

feat: more API for integrals wrt vector measures (#40198) We port part of the API of Bochner integrals to integrals wrt vector measures (more to come, this was split to keep the PR at a reasonable size). Also shorten several proofs using directly setToFun versions of the lemmas instead of repeating the proofs.

Estimated changes

Modified Mathlib/MeasureTheory/VectorMeasure/Integral.lean

added theorem MeasureTheory.VectorMeasure.Integrable.add_cbm

added theorem MeasureTheory.VectorMeasure.Integrable.add_vectorMeasure

added theorem MeasureTheory.VectorMeasure.Integrable.finsetSum_cbm

added theorem MeasureTheory.VectorMeasure.Integrable.finsetSum_vectorMeasure

added theorem MeasureTheory.VectorMeasure.Integrable.neg_cbm

added theorem MeasureTheory.VectorMeasure.Integrable.neg_vectorMeasure

added theorem MeasureTheory.VectorMeasure.Integrable.restrict

added theorem MeasureTheory.VectorMeasure.Integrable.smul_vectorMeasure

added theorem MeasureTheory.VectorMeasure.Integrable.sub_cbm

added theorem MeasureTheory.VectorMeasure.Integrable.sub_vectorMeasure

added theorem MeasureTheory.VectorMeasure.Integrable.zero_cbm

added theorem MeasureTheory.VectorMeasure.Integrable.zero_vectorMeasure

added theorem MeasureTheory.VectorMeasure.absolutelyContinuous_variation_transpose

added theorem MeasureTheory.VectorMeasure.integral_eq_setToFun

modified theorem MeasureTheory.VectorMeasure.integral_fun_neg

modified theorem MeasureTheory.VectorMeasure.integral_fun_smul

added theorem MeasureTheory.VectorMeasure.integral_of_not_completeSpace

added theorem MeasureTheory.VectorMeasure.integral_smul_vectorMeasure

modified theorem MeasureTheory.VectorMeasure.integral_zero

added theorem MeasureTheory.VectorMeasure.transpose_add

added theorem MeasureTheory.VectorMeasure.transpose_dirac

added theorem MeasureTheory.VectorMeasure.transpose_map

added theorem MeasureTheory.VectorMeasure.transpose_restrict

added theorem MeasureTheory.VectorMeasure.transpose_smul

added theorem MeasureTheory.VectorMeasure.transpose_zero

deleted theorem MeasureTheory.VectorMeasure.transpose_zero_vectorMeasure

added theorem MeasureTheory.VectorMeasure.variation_transpose_eq

added theorem MeasureTheory.VectorMeasure.variation_transpose_eq_smul

added theorem MeasureTheory.VectorMeasure.variation_transpose_le

added theorem MeasureTheory.VectorMeasure.variation_transpose_lsmul

added theorem MeasureTheory.VectorMeasure.variation_transpose_lsmul_flip