feat(MeasureTheory/VectorMeasure): add integral of a vector-valued function against a vector measure

[yoh-tanimoto]

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: [Merged by Bors] - feat(MeasureTheory.VectorMeasure): add several lemmas which characterize variation #26160 for the definition and lemmas about the total variation of a vector measure.

[yoh-tanimoto]

I noticed that μ.variation is not the correct reference measure. I switched it to (μ.comp B.flip).variation.

[EtienneC30]

Thanks! I am thinking it would be worth introducing VectorMeasureWithPairing.Integrable which would correspond to being integrable with respect to the variation of the transpose.

[EtienneC30]

It is still a bit unclear to me whether we want this or not, compared to just define the integral with B and µ as arguments. On the one hand I feel like in concrete settings we may have B and µ in an unbundled way, which would mean writing ⟨B, μ⟩ often, which is not that bad but still a bit less nice. On the other hand I guess we might just define a VectorMeasureWithPairing on the fly, or even have a file compiling many different VectorMeasureWithPairings. What do you think?

[yoh-tanimoto]

do you mean that we keep VectorMeasureWithPairing just as a namespace? I introduced the structure because in this way you can use the dot notation, but maybe not so useful?

[EtienneC30]

If it is just about namespace we can simply use VectorMeasure. The question is whether we want to bundle the measure and the pairing or not (and also what is the notation if we do not bundle).

[yoh-tanimoto]

Ah right, I could define integral without bundling. Now the bundling started to look redundant...

noncomputable def integral (μ : VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) (f : X → E) : G :=
  if _ : CompleteSpace G then
  setToFun (μ.mapRange B.flip.toAddMonoidHom B.flip.continuous).variation
    (μ.mapRange B.flip.toAddMonoidHom B.flip.continuous)
    (dominatedFinMeasAdditive_cbmApplyMeasure B μ) f
  else 0

I would like a notation like ∫ᵛ x, B (f x) ∂μ, but not sure how to define:

notation3 " ∫ᵛ "(...)", "B:50" "r:60:(scoped f => f)" ∂"μ:70 =>
  integral (MeasureTheory.VectorMeasureWithPairing.mk B μ) r

variable (B : E →L[ℝ] F →L[ℝ] G) (μ : VectorMeasure X F) (f : X → E)
#check ∫ᵖ x, B (f x) ∂μ

gives "unexpected token '∂'; expected term". Could you help?

[yoh-tanimoto]

I removed VectorMeasureWithPairing. I think this is better indeed.