Theorems · Definition · measure theory

MeasureTheory.VectorMeasure.prod

{X : Type u_2} →
  {Y : Type u_3} →
    {E : Type u_4} →
      {F : Type u_5} →
        {G : Type u_6} →
          {mX : MeasurableSpace X} →
            {mY : MeasurableSpace Y} →
              [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 E →
                            MeasureTheory.VectorMeasure Y F →
                              (E →L[ℝ] F →L[ℝ] G) → MeasureTheory.VectorMeasure (X × Y) G

The product of two vector measures μ and ν with respect to a continuous bilinear map B, giving mass B (μ s) (ν t) to any measurable product set s × t. If such a measure does not exist, we use the junk value 0.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Prod

Cited by

7 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace