Commit 2026-06-17 07:42 598d514d

chore: refactor the vector measure integral by changing the reference measure (#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 @ 💬. Everyone seems to agree the refactor is a good idea.