Integral with respect to a complex measure

Stream: maths

[Oliver Butterley]

Having defined total variation for complex measures (PR in queue: #25442) one could write a complex measure as the combination of angular part and total variation measure. In such a way we can write the integral with respect to a complex measure. On the other hand, what is the mathlib way to do this? Maybe there is instead an elegant way to define the integral with respect to a large class of VectorMeasure?

import Mathlib
open MeasureTheory ENNReal
variable {X : Type*} [MeasurableSpace X]

def MeasureTheory.VectorMeasure.variation
    {V : Type*} [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V]  [T2Space V]
    (μ : VectorMeasure X V) : VectorMeasure X ℝ≥0∞ := by
  -- This is the definition from PR #25442.
  sorry

/-- The variation measure part in the polar decomposition of a complex measure. -/
noncomputable def MeasureTheory.VectorMeasure.var
     (μ : ComplexMeasure X) := μ.variation.ennrealToMeasure

/-- The angular part (density function) in the polar decomposition of a complex measure. -/
noncomputable def MeasureTheory.VectorMeasure.ang
     (μ : ComplexMeasure X) := μ.rnDeriv μ.var

noncomputable def ComplexMeasure.integral (μ : ComplexMeasure X) (f : X → ℂ) :=
  ∫ x, f x * μ.ang x ∂(μ.var)

[Oliver Butterley]

Or, define integration with respect to a signed measure using the Hahn-Jordan decomposition and then integration with respect to a complex measure but integrating separately the real and imaginary parts.
In summary, three approaches come to mind for integration with respect to a complex measure:

• Use variation and polar rep of complex measure
• Separately integrate real and imaginary parts and use Hahn-Jordan decomposition to integrate with respect to signed measure
• Directly define the integral via simple functions, etc. This could work for a larger class of VectorMeasure.

[Etienne Marion]

Can’t you define total variation for a larger class of vector measures?

[Oliver Butterley]

Etienne Marion said:

Can’t you define total variation for a larger class of vector measures?

We did for all (μ : VectorMeasure X V) where [TopologicalSpace V] [ENormedAddCommMonoid V] [T2Space V] .
Do you mean that some of these assumptions on V could be dropped?

[Etienne Marion]

Oh sorry you wrote complex measures so I assumed that you only did it for C

[Oliver Butterley]

Ah! I see what you mean. Yes, my comment gave a certain impression that was inaccurate.

For the project at hand we needed variation and integration for complex measures. We defined variation for all VectorMeasure since that was natural. Now turning our attention to the integral and wondering how best to proceed.

[Yoh Tanimoto]

I think it would be nice to define the integral of vector measure, perhaps Banach space-valued ones. We will need it to define the resolution of the identity (the spectral measure) of self-adjoint operators.

Does anyone has a suggestion for literature?