feat: more API for integrals wrt vector measures

[sgouezel]

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.

---

[github-actions]

PR summary b38591ffde

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.MeasureTheory.VectorMeasure.Integral	2276	2279	+3 (+0.13%)

Import changes for all files

Files	Import difference
Mathlib.MeasureTheory.VectorMeasure.Integral	3

---

Declarations diff (regex)

+ Integrable.add_cbm
+ Integrable.add_vectorMeasure
+ Integrable.finsetSum_cbm
+ Integrable.finsetSum_vectorMeasure
+ Integrable.neg_cbm
+ Integrable.neg_vectorMeasure
+ Integrable.restrict
+ Integrable.smul_vectorMeasure
+ Integrable.sub_cbm
+ Integrable.sub_vectorMeasure
+ Integrable.zero_cbm
+ Integrable.zero_vectorMeasure
+ IntegrableOn
+ absolutelyContinuous_variation_transpose
+ instance [IsFiniteMeasure μ.variation] :
+ integral_eq_setToFun
+ integral_of_not_completeSpace
+ integral_smul_vectorMeasure
+ transpose_add
+ transpose_dirac
+ transpose_map
+ transpose_restrict
+ transpose_smul
+ transpose_zero
+ variation_transpose_eq
+ variation_transpose_eq_smul
+ variation_transpose_le
+ variation_transpose_lsmul
+ variation_transpose_lsmul_flip
- transpose_zero_vectorMeasure

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 b38591f).

• +31 new declarations
• −1 removed declarations

+MeasureTheory.VectorMeasure.Integrable.add_cbm
+MeasureTheory.VectorMeasure.Integrable.add_vectorMeasure
+MeasureTheory.VectorMeasure.Integrable.finsetSum_cbm
+MeasureTheory.VectorMeasure.Integrable.finsetSum_vectorMeasure
+MeasureTheory.VectorMeasure.Integrable.neg_cbm
+MeasureTheory.VectorMeasure.Integrable.neg_vectorMeasure
+MeasureTheory.VectorMeasure.Integrable.restrict
+MeasureTheory.VectorMeasure.Integrable.smul_vectorMeasure
+MeasureTheory.VectorMeasure.Integrable.sub_cbm
+MeasureTheory.VectorMeasure.Integrable.sub_vectorMeasure
+MeasureTheory.VectorMeasure.Integrable.zero_cbm
+MeasureTheory.VectorMeasure.Integrable.zero_vectorMeasure
+MeasureTheory.VectorMeasure.IntegrableOn
+MeasureTheory.VectorMeasure.absolutelyContinuous_variation_transpose
+MeasureTheory.VectorMeasure.instIsFiniteMeasureVariationContinuousLinearMapRealIdTranspose
+MeasureTheory.VectorMeasure.integral_eq_setToFun
+MeasureTheory.VectorMeasure.integral_of_not_completeSpace
+MeasureTheory.VectorMeasure.integral_smul_vectorMeasure
+MeasureTheory.VectorMeasure.transpose_add
+MeasureTheory.VectorMeasure.transpose_dirac
+MeasureTheory.VectorMeasure.transpose_map
+MeasureTheory.VectorMeasure.transpose_restrict
+MeasureTheory.VectorMeasure.transpose_smul
+MeasureTheory.VectorMeasure.transpose_zero
-MeasureTheory.VectorMeasure.transpose_zero_vectorMeasure
+MeasureTheory.VectorMeasure.variation_transpose_eq
+MeasureTheory.VectorMeasure.variation_transpose_eq_smul
+MeasureTheory.VectorMeasure.variation_transpose_le
+MeasureTheory.VectorMeasure.variation_transpose_lsmul
+MeasureTheory.VectorMeasure.variation_transpose_lsmul_flip
+MeasureTheory.VectorMeasure.«term∫ᵛ_In_,_∂[_;_]»
+MeasureTheory.VectorMeasure.«term∫ᵛ_In_,_∂•_»

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit b38591ffde
Reference commit 01e91cd1ce

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).

[EtienneC30]

Thanks!

[EtienneC30]

Do you think it's worth having a notation for this case?

[sgouezel]

Sure, why not! Any idea?

[EtienneC30]

I think these would be better in the Integrable namespace. Can you also add a neg a sub and a smul versions please? Same remarks for the cbm section. Also it would be nice to have the same for the sum etc. of functions.

[sgouezel]

I've tried to copy exactly the names of the Bochner integral API. The lemmas are named integrable_add_measure there.

[sgouezel]

Still I agree with you that dot notation is better, so I've changed, and added the lemmas. The ones for the sum etc. of functions are ready for the next PR.