Theorems · Inductive type · measure theory

MeasureTheory.VectorMeasure.HasProd

{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) → Prop

Two vector measures μ and ν have a product with respect to B if there exists a measure giving mass B (μ s) (ν t) to any measurable product set s × t. This is satisfied whenever μ or ν has finite variation.

Defined in

Mathlib.MeasureTheory.VectorMeasure.Prod

Cited by

6 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace