Commit 2026-05-05 10:37 b9ecf8aa

feat(MeasureTheory/VectorMeasure): add integral of a vector-valued function against a vector measure (#28499) add VectorMeasureWithPairing.integral for normed vector spaces E, F, a Banach space G , a continuous linear pairing B : E →L[ℝ] F →L[ℝ] → G and an F-valued vector measure μ, which should be informally written as ∫ B (f x) ∂μ x. motivation: there are natural vector measures such as signed measures and complex measures, and their integrals appear naturally e.g. in a proof of the spectral theorem for general bounded normal operators on a Hilbert space.

• depends on: #26160 for the definition and lemmas about the total variation of a vector measure.