Commit 2026-07-17 20:05 7c77f1a0

View on Github →

feat: the product of vector measures (#41546)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Basic.lean

added theorem MeasureTheory.VectorMeasure.ext_of_generateFrom

added theorem MeasureTheory.VectorMeasure.of_biUnion

modified theorem MeasureTheory.VectorMeasure.of_biUnion_finset

added theorem MeasureTheory.VectorMeasure.of_if

added theorem MeasureTheory.VectorMeasure.restrict_apply_univ

Created Mathlib/MeasureTheory/VectorMeasure/Prod.lean

added theorem MeasureTheory.VectorMeasure.HasProd.flip

added theorem MeasureTheory.VectorMeasure.hasProd_flip_iff

added theorem MeasureTheory.VectorMeasure.integrable_vectorMeasure_prodMk_left

added theorem MeasureTheory.VectorMeasure.prod_apply

added theorem MeasureTheory.VectorMeasure.prod_apply_eq_integral

added theorem MeasureTheory.VectorMeasure.prod_eq_of_forall_apply_prod

added theorem MeasureTheory.VectorMeasure.prod_eq_zero_of_not_hasProd

added theorem MeasureTheory.VectorMeasure.prod_flip_apply_eq_integral

added theorem MeasureTheory.VectorMeasure.stronglyMeasurable_vectorMeasure_prodMk_left

added theorem MeasureTheory.VectorMeasure.variation_prod_le