chore: refactor the vector measure integral by changing the reference measure (leanprover-community#40603)

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

Zulip discussion at [#mathlib4 > Refactoring vector measure integral @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Refactoring.20vector.20measure.20integral/near/603283077). Everyone seems to agree the refactor is a good idea.

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/Data/NNReal/Defs.lean

@@ -127,6 +127,8 @@ noncomputable instance : LinearOrderedCommGroupWithZero ℝ≥0 where
 example {p q : ℝ≥0} (h1p : 0 < p) (h2p : p ≤ q) : q⁻¹ ≤ p⁻¹ := by
   with_reducible_and_instances exact inv_anti₀ h1p h2p
 
+@[simp] lemma mk_coe (a : ℝ≥0) (ha : 0 ≤ (a : ℝ)) : NNReal.mk (a : ℝ) ha = a := rfl
+
 -- Simp lemma to put back `n.val` into the normal form given by the coercion.
 @[simp]
 theorem val_eq_coe (n : ℝ≥0) : n.val = n :=