Commit 2026-06-07 07:23 e37757ed

View on Github →

feat: more API for the integral wrt vector measures (#40285) These are direct adaptations of the API for the Bochner integral. I have gone through the Bochner integral file, copied over all lemmas, and kept all the ones that made sense for vector measures.

Estimated changes

Modified Mathlib/MeasureTheory/VectorMeasure/Integral.lean

added theorem MeasurableEmbedding.integrable_map_vectorMeasure

added theorem MeasurableEmbedding.integral_map_vectorMeasure

added theorem MeasurableEmbedding.variation_transpose_map

added theorem MeasureTheory.VectorMeasure.Integrable.add

added theorem MeasureTheory.VectorMeasure.Integrable.finsetSum

added theorem MeasureTheory.VectorMeasure.Integrable.fun_finsetSum

added theorem MeasureTheory.VectorMeasure.Integrable.map

added theorem MeasureTheory.VectorMeasure.Integrable.neg

added theorem MeasureTheory.VectorMeasure.Integrable.of_integral_ne_zero

added theorem MeasureTheory.VectorMeasure.Integrable.smul

added theorem MeasureTheory.VectorMeasure.Integrable.sub

added theorem MeasureTheory.VectorMeasure.continuousAt_of_dominated

added theorem MeasureTheory.VectorMeasure.continuousOn_of_dominated

added theorem MeasureTheory.VectorMeasure.continuousWithinAt_of_dominated

added theorem MeasureTheory.VectorMeasure.continuous_of_dominated

added theorem MeasureTheory.VectorMeasure.dist_integral_le_lintegral_edist

added theorem MeasureTheory.VectorMeasure.edist_integral_le_lintegral_edist

added theorem MeasureTheory.VectorMeasure.enorm_integral_le_lintegral_enorm

added theorem MeasureTheory.VectorMeasure.enorm_integral_le_of_enorm_le_const

added theorem MeasureTheory.VectorMeasure.exists_ne_zero_of_integral_ne_zero

added theorem MeasureTheory.VectorMeasure.frequently_ae_ne_zero_of_integral_ne_zero

added theorem MeasureTheory.VectorMeasure.hasSum_integral_of_dominated_convergence

added theorem MeasureTheory.VectorMeasure.integral_const

added theorem MeasureTheory.VectorMeasure.integral_dirac'

added theorem MeasureTheory.VectorMeasure.integral_dirac

added theorem MeasureTheory.VectorMeasure.integral_indicator₂

added theorem MeasureTheory.VectorMeasure.integral_map

added theorem MeasureTheory.VectorMeasure.integral_map_equiv

added theorem MeasureTheory.VectorMeasure.integral_non_aestronglyMeasurable

added theorem MeasureTheory.VectorMeasure.integral_smul_nnreal_vectorMeasure

added theorem MeasureTheory.VectorMeasure.integral_toSignedMeasure

added theorem MeasureTheory.VectorMeasure.integral_tsum

added theorem MeasureTheory.VectorMeasure.integral_unique

added theorem MeasureTheory.VectorMeasure.nndist_integral_add_vectorMeasure_le_lintegral

added theorem MeasureTheory.VectorMeasure.norm_integral_le_lintegral_norm

added theorem MeasureTheory.VectorMeasure.norm_integral_le_of_norm_le_const

added theorem MeasureTheory.VectorMeasure.tendsto_integral_filter_of_dominated_convergence

added theorem MeasureTheory.VectorMeasure.tendsto_integral_filter_of_norm_le_const

added theorem MeasureTheory.VectorMeasure.tendsto_integral_of_L1'

added theorem MeasureTheory.VectorMeasure.tendsto_integral_of_L1

added theorem MeasureTheory.VectorMeasure.tendsto_integral_of_dominated_convergence

added theorem MeasureTheory.VectorMeasure.variation_transpose_map_le

added theorem Topology.IsClosedEmbedding.integral_map_vectorMeasure