Integral against vector measures

Stream: Brownian motion

[Etienne Marion]

Browsing the internet I found vector_integral.pdf about Dobrakov integral which seems to be quite general.

[Yoh Tanimoto]

yes, the monograph by Dinculeanu cited therein appears standard, although I'm no expert at all

[Yoh Tanimoto]

I copied some files containing basic facts about integral against a (usual, ENNReal-valued) measure and am adapting them to VectorMeasure
https://github.com/oliver-butterley/SpectralThm/pull/21/files

I translated most of APIs about simple functions and integrals of simple functions. The next will be L1 functions.

Is this a right approach?

[Etienne Marion]

It seems to go smoothly, I don't know if everything works that well when we turn to integrable functions, but maybe! However I thought that we may want to develop not only an integral of a scalar function against a vector measure, but more generally of a vector-valued function against an operator-valued measure (that would be given for instance by Dinculeanu's work), and then deduce the former from the latter.

[Sébastien Gouëzel]

Vector valued function and operator valued measure looks symmetry breaking to me: why not also operator valued function and vector measure? If you want to be really general, Id' say you want function taking value in E, vector measure taking value in F, and a bilinear map from E x F to G? Unless there is something specific to the case you're referring to, where things work better than in the general situation?

[Etienne Marion]

No you're right it's with a bilinear map! I got confused because the first thing I looked at was only about operator-valued measures but then I looked at Dinculenau's work which indeed takes this more symmetrical approach.

[Yoh Tanimoto]

I see, so I guess the most general assumptions and basic definition will be the following?

import Mathlib

open MeasureTheory VectorMeasure ContinuousLinearMap

noncomputable section

variable {α E F G R S K: Type*}

variable [m : MeasurableSpace α] [NormedAddCommGroup E] [NontriviallyNormedField R]
  [NormedSpace R E]
  [NormedAddCommGroup F] [NontriviallyNormedField S]
  [NormedSpace S F] (μ : VectorMeasure α F)
  [NormedAddCommGroup G] [NontriviallyNormedField K] [NormedSpace K G]
  {σ : R →+* K} {ρ : S →+* K} (B : E →SL[σ] F →SL[ρ] G)
  (μ : VectorMeasure α F)

namespace MeasureTheory

local infixr:25 " →ₛ " => SimpleFunc

def setToVectorSimpleFunc (T : Set α → E →SL[σ] G) (f : α →ₛ E) : G :=
  ∑ x ∈ f.range, T (f ⁻¹' {x}) x

def weightedVectorSMul (s : Set α) : E →SL[σ] G where
  toFun c := B c (μ s)
  map_add' _ _ := map_add₂ B _ _ (μ s)
  map_smul' _ _ := map_smulₛₗ₂ B _ _ (μ s)

variable (f : α →ₛ E)

#check setToVectorSimpleFunc (weightedVectorSMul B μ) f

end MeasureTheory

end

[Etienne Marion]

Yes that looks good!

[Sébastien Gouëzel]

Does it really make sense to have a field K which is not the reals?

[Yoh Tanimoto]

well, at least I would like also the complex numbers and I had in mind the case where σ is the conjugate. Should we use RCLike instead?

Of course, when we define L1 funtions and prove that continuous functions are L1 etc., K and G will have to be complete spaces.

[Sébastien Gouëzel]

Complex-linear maps are also real-linear, and in particular the conjugation is also real-linear, so I'm not sure you would lose in generality by considering only real-linear maps.

[Yoh Tanimoto]

wouldn't it be inconvenient when we want to prove that integral is complex-linear?

[Sébastien Gouëzel]

I don't think so. For instance, we already know that the usual integral for complex-valued functions is complex-linear, although it is first built as a purely real theory (see e.g. docs#integral_smul_const)

[Yoh Tanimoto]

ah ok, I was thinking more about multiplication by a scalar to the function but that is just the linearity of the bilinear form.

I can switch to reals or RCLike K (I haven't even started), but I'm just wondering whether it wasn't the philosophy that we should make things as general as possible. Should I specialize to reals/RCLike K from the beginning or when I need it?

[Yoh Tanimoto]

sorry, which is the natural way to consider a conjugate linear map as a Real-linear map?

import Mathlib

variable  {E : Type*} [AddCommGroup E] [Module ℂ E]
  (f : E →ₗ⋆[ℂ] E) (g : E →ₗ[ℂ] E)

#check (f : E →ₗ⋆[ℂ] E)
-- fails #check (f : E →ₗ[ℝ] E)
#check (g : E →ₗ[ℂ] E)
#check (g : E →ₗ[ℝ] E)

[Sébastien Gouëzel]

I don't know if we have a way in the library to do it transparently now, what I'm saying is that, mathematically, it's true that a complex conjugate linear map is a real linear map.

[Sébastien Gouëzel]

For the practical implementation of vector measure integrals using bilinear maps, as sketched above, using current Mathlib, I think you don't need to redo everything: the setToL1 mechanism should also apply to this situation (it was designed to be very general).

Let me be a little bit more precise. Suppose you have a vector-valued measure mu (with values in a space E), and a bilinear map B : E ->L[R] F ->L[R] G. Then you get a function T : Set alpha -> F ->L[R] G, mapping s and x to B (mu s) x. If you check the property hT : DominatedFinMeasAdditive μ.totalVariation T C (where mu.totalVariation is the positive measure given by the total variation of mu), then setToL1 hT associates to an integrable function f for mu.totalVariation an element of G; this is the desired integral of f with respect to the vector measure mu and the bilinear form B.

[Yoh Tanimoto]

Ah that was the intention of setToL1, I see! I will try then.

[Yoh Tanimoto]

Of course I agree that mathematically a conjugate linear map is real linear. I will see how this can be automated

[Yoh Tanimoto]

ok vectorIntegral defined.
https://github.com/oliver-butterley/SpectralThm/pull/21

[Yoh Tanimoto]

I opened #28499

I'm not sure how to proceed from here. There are a huge amount of theorems about Bochner integral. Should we dulicate them all for vector measures? Or is there a better way?

[Sébastien Gouëzel]

I think we will have to duplicate, because the assumptions have to be different (in one case, it's for functions integrable wrt mu, in the other one wrt the total variation measure associated to mu). However, normally the statement should have been stated cleanly for SetToL1, which means that there shouldn't be much proof duplication, just applying straight away the SetToL1 results to the specific situation at hand.

(And this should be done in another PR, because this one is already large enough :-)

[Sébastien Gouëzel]

(Note also that your PR is stuck on #26156, which is awaiting-author)

[Yoh Tanimoto]

Ah, do you mean that 'f' can be integrable with respect to a vector measure 'mu' and a bilinear pairing 'B' even though it is not integrable with respect to 'mu.variation' (e.g. when 'B = 0')?

Yes, we should first get total variation merged.

[Yongxi Lin (Aaron)]

I created a draft PR #30230 that depends on #28499. The goal of this PR is to create an analogue file of Mathlib.MeasureTheory.Integral.Bochner.Basic.lean for integrals against a vector measure with pairing. I mainly proved some results about linearity. That is, the integral is a linear operator on functions, bilinear forms, and vector measures, respectively. I need some help and advices from the community before making this PR open.

1. As suggest in #28499, given a vector measure μ, a function f, and a pairing B, the notation for the integral of f against μ and B is ∫ x, B (f x) ∂μ. I am not sure how I should create this notation because I am not familiar with the notation3 function and I don't know how to determine the correct precedence level in the notation.
2. Similarly, if we haveBμ: VectorMeasureWithPairing α E F G (where α is the underlying measure space and E,F,G are normed vector spaces over $\mathbb{R}$, this type is also defined in #28499), which is the bundled version of (B : E →L[ℝ] F →L[ℝ] → G) (μ : VectorMeasure α F), I want to create a notation to represent the integral of f against Bμ. Here are some possible candidates: ∫ x, ∂ Bμ f x and ∫ x, f x ∂Bμ. Temporarily I am using the second one in my draft PR. This create troubles because it is the same notation for integrals against a scalar measure, which is also why I want a different notation. Also the notation I suggested may not be the most natural/suitable one, so feel free to share your thoughts here.
3. I want to prove that for a real number r and an E-valued vector measureμ, (r• μ).variation=|r| • (μ.variation). However, |r| • (μ.variation) cannot be defined. I think this is because MeasureTheory.VectorMeasure.instSMul requires ContinuousConstSMul, and we are missing the instance ContinuousConstSMul ℝ≥0 ℝ≥0∞. I want to make a PR to add this instance into Mathlib.
4. I also realized that the above lemma should work in a more general case. That is, if I have an action f : R -> E -> F, an element r : R and an E-valued vector measure μ, I should be able to define an F-valued vector measure (r• μ). For instance, I can multiply a NNReal-valued measure with a complex number to obtain a complex measure. However, I am not sure what type classes I need in order to define this.