Theorems · Definition · measure theory

MeasureTheory.cbmApplyMeasure

{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 → (E →L[ℝ] F →L[ℝ] G) → Set X → E →L[ℝ] G

Given a set s, return the continuous linear map fun x : E ↦ B x (μ s) (actually defined using transpose through mapRange), where the B is a G-valued bilinear form on E × F and μ is an F-valued vector measure. The extension of that set function through setToFun gives the pairing integral of E-valued integrable functions.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Integral

Cited by

4 results in Mathlib

Foundations

Depth 181 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace