feat: more API for set integrals wrt vector measures

[sgouezel]

This is essentially an adapted copy of the API we already have for the Bochner integral

---

[github-actions]

PR summary 70c65d93b1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ Integrable.tendsto_setIntegral_nhds_zero
+ _root_.MeasurableEmbedding.setIntegral_map_vectorMeasure
+ _root_.Topology.IsClosedEmbedding.setIntegral_map_vectorMeasure
+ continuousLinearMap_apply_integral
+ enorm_setIntegral_le_lintegral_enorm
+ enorm_setIntegral_le_lintegral_enorm_transpose
+ enorm_setIntegral_le_of_enorm_le_const
+ enorm_setIntegral_le_of_enorm_le_const_ae
+ hasSum_setIntegral_iUnion
+ hasSum_setIntegral_iUnion_nat
+ integral_continuousLinearMap_comp
+ integral_iUnion
+ integral_indicator_const
+ norm_setIntegral_le_of_norm_le_const
+ norm_setIntegral_le_of_norm_le_const_ae
+ setIntegral_const
+ setIntegral_eq_integral_of_ae_compl_eq_zero
+ setIntegral_eq_integral_of_forall_compl_eq_zero
+ setIntegral_eq_of_subset_of_ae_sdiff_eq_zero
+ setIntegral_eq_of_subset_of_forall_sdiff_eq_zero
+ setIntegral_map
+ setIntegral_map_equiv
+ setIntegral_toSignedMeasure
+ setIntegral_union_eq_left_of_ae
+ setIntegral_union_eq_left_of_forall
+ tendsto_setIntegral_of_L1
+ tendsto_setIntegral_of_L1'

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 70c65d9).

• +26 new declarations
• −0 removed declarations

+MeasurableEmbedding.setIntegral_map_vectorMeasure
+MeasureTheory.VectorMeasure.Integrable.tendsto_setIntegral_nhds_zero
+MeasureTheory.VectorMeasure.continuousLinearMap_apply_integral
+MeasureTheory.VectorMeasure.enorm_setIntegral_le_lintegral_enorm
+MeasureTheory.VectorMeasure.enorm_setIntegral_le_lintegral_enorm_transpose
+MeasureTheory.VectorMeasure.enorm_setIntegral_le_of_enorm_le_const
+MeasureTheory.VectorMeasure.enorm_setIntegral_le_of_enorm_le_const_ae
+MeasureTheory.VectorMeasure.hasSum_setIntegral_iUnion
+MeasureTheory.VectorMeasure.integral_continuousLinearMap_comp
+MeasureTheory.VectorMeasure.integral_iUnion
+MeasureTheory.VectorMeasure.integral_indicator_const
+MeasureTheory.VectorMeasure.norm_setIntegral_le_of_norm_le_const
+MeasureTheory.VectorMeasure.norm_setIntegral_le_of_norm_le_const_ae
+MeasureTheory.VectorMeasure.setIntegral_const
+MeasureTheory.VectorMeasure.setIntegral_eq_integral_of_ae_compl_eq_zero
+MeasureTheory.VectorMeasure.setIntegral_eq_integral_of_forall_compl_eq_zero
+MeasureTheory.VectorMeasure.setIntegral_eq_of_subset_of_ae_sdiff_eq_zero
+MeasureTheory.VectorMeasure.setIntegral_eq_of_subset_of_forall_sdiff_eq_zero
+MeasureTheory.VectorMeasure.setIntegral_map
+MeasureTheory.VectorMeasure.setIntegral_map_equiv
+MeasureTheory.VectorMeasure.setIntegral_toSignedMeasure
+MeasureTheory.VectorMeasure.setIntegral_union_eq_left_of_ae
+MeasureTheory.VectorMeasure.setIntegral_union_eq_left_of_forall
+MeasureTheory.VectorMeasure.tendsto_setIntegral_of_L1
+MeasureTheory.VectorMeasure.tendsto_setIntegral_of_L1'
+Topology.IsClosedEmbedding.setIntegral_map_vectorMeasure

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 70c65d93b1
Reference commit 555b02bc95

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).