Theorems · Definition · measure theory

MeasureTheory.VectorMeasure.integral

{X : Type u_2} →
  {E : Type u_4} →
    {F : Type u_5} →
      {G : Type u_6} →
        {mX : MeasurableSpace X} →
          [inst : NormedAddCommGroup E] →
            [inst_1 : NormedSpace ℝ E] →
              [inst_2 : NormedAddCommGroup F] →
                [inst_3 : NormedSpace ℝ F] →
                  [inst_4 : NormedAddCommGroup G] →
                    [inst_5 : NormedSpace ℝ G] → MeasureTheory.VectorMeasure X F → (X → E) → (E →L[ℝ] F →L[ℝ] G) → G

The G-valued integral of E-valued function and the F-valued vector measure μ with linear paring B : E →L[ℝ] F →L[ℝ] G . This is set to be 0 if G is not complete or if f is not integrable with respect to (μ.transpose B).variation. Notation ∫ᵛ x, f x ∂[B; μ]. When μ is G-valued, to get the integral in G of a real-valued function, take B = ContinousLinearMap.lsmul ℝ ℝ. Notation ∫ᵛ x, f x ∂•μ. When μ is a signed measure, to get the integral in G of a G-valued function, take B = (ContinousLinearMap.lsmul ℝ ℝ).flip. Notation ∫ᵛ x, f x ∂<•μ.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Integral

Cited by

126 results in Mathlib

Foundations

Depth 241 from the axioms, rests on 6,488 definitions · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace