chore: refactor the vector measure integral by changing the reference measure

[sgouezel]

Given a bilinear form B on E x F to G, a function f with values in E and a vector measure v with values in F, the integral wrt the vector measure is defined when the function is integrable wrt the measure (v.transpose B).variation, which is the minimal condition for the integral to make sense.

I have played a lot recently with integrals for vector measures, and I have realized that assuming this minimal condition creates a lot of complications, for essentially no gain. In this PR, I require the stronger condition that the function is integrable wrt v.variation. So, the integrability condition does not depend on B any more. This makes for smoother statements and smoother proofs (especially in the forthcoming Fubini theorem). In all standard applications, B is an isometry, so (v.transpose B).variation = v.variation, and the theory is unchanged.

Note that the new approach does not lose any generality: in the unlikely event one wants to integrate a function which is only integrable wrt (v.transpose B).variation for some exotic B, then one can integrate with the vector measure v.transpose B (which takes values in E -> G) and the bilinear form which is the function application, i.e., E -> (E -> G) -> G.

---

[github-actions]

PR summary 3c057187cb

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ _root_.MeasureTheory.Measure.variation_toSignedMeasure
+ continuous_integral
+ dominatedFinMeasAdditive_transpose_cbmApplyMeasure
+ enorm_integral_le_lintegral_enorm_transpose
+ integral_eq_setToFun_transpose
+ mk_coe
+ norm_integral_le_integral_norm
- Integrable.add_cbm
- Integrable.finsetSum_cbm
- Integrable.neg_cbm
- Integrable.sub_cbm
- Integrable.zero_cbm
- variation_toSignedMeasure

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

• +7 new declarations
• −6 removed declarations

+MeasureTheory.Measure.variation_toSignedMeasure
-MeasureTheory.VectorMeasure.Integrable.add_cbm
-MeasureTheory.VectorMeasure.Integrable.finsetSum_cbm
-MeasureTheory.VectorMeasure.Integrable.neg_cbm
-MeasureTheory.VectorMeasure.Integrable.sub_cbm
-MeasureTheory.VectorMeasure.Integrable.zero_cbm
+MeasureTheory.VectorMeasure.continuous_integral
+MeasureTheory.VectorMeasure.enorm_integral_le_lintegral_enorm_transpose
+MeasureTheory.VectorMeasure.integral_eq_setToFun_transpose
+MeasureTheory.VectorMeasure.norm_integral_le_integral_norm
-MeasureTheory.VectorMeasure.variation_toSignedMeasure
+MeasureTheory.dominatedFinMeasAdditive_transpose_cbmApplyMeasure
+NNReal.mk_coe

---

Decrease in strong tech debt: (relative, absolute) = (1.00, 0.03)

Current number	Change	Type (strong)
39	-1	disabled simpNF lints

No changes to weak technical debt.

Current commit 3c057187cb
Reference commit 271d273e99

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

[sgouezel]

I can't deprecate these lemmas, because their statements don't even make sense with the new formalism as integrability does not depend on the bilinear form any more.