Product of vector measures

Given two vector measures, we define their product μ.prod ν B as the vector measure assigning to a measurable product s × t the mass B (μ s) (ν t), if such a vector measure exists. We show that it exists when either μ or ν has finite variation.

The API is modelled on the one for the product of positive measures.

class 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} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X E) (ν : VectorMeasure Y F) (B : 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.

• exists_prod : ∃ (ρ : VectorMeasure (X × Y) G), ∀ (s : Set X) (t : Set Y), MeasurableSet s → MeasurableSet t → ρ (s ×ˢ t) = (B (μ s)) (ν t)

noncomputable def 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} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (μ : VectorMeasure X E) (ν : VectorMeasure Y F) (B : E →L[ℝ] F →L[ℝ] G) : 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.

Equations

• μ.prod ν B = if h : μ.HasProd ν B then ⋯.choose else 0

theorem MeasureTheory.VectorMeasure.prod_eq_zero_of_not_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} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X E} {ν : VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G} (h : ¬μ.HasProd ν B) : μ.prod ν B = 0

@[simp]

theorem MeasureTheory.VectorMeasure.prod_apply {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} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X E} {ν : VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G} [h : μ.HasProd ν B] {s : Set X} {t : Set Y} : (μ.prod ν B) (s ×ˢ t) = (B (μ s)) (ν t)

theorem MeasureTheory.VectorMeasure.HasProd.flip {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} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X E} {ν : VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G} [μ.HasProd ν B] : ν.HasProd μ B.flip

theorem MeasureTheory.VectorMeasure.hasProd_flip_iff {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} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X E} {ν : VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G} : ν.HasProd μ B.flip ↔ μ.HasProd ν B

theorem MeasureTheory.VectorMeasure.stronglyMeasurable_vectorMeasure_prodMk_left {X : Type u_2} {Y : Type u_3} {F : Type u_5} {mX : MeasurableSpace X} {mY : MeasurableSpace Y} [NormedAddCommGroup F] {ν : VectorMeasure Y F} {s : Set (X × Y)} (hs : MeasurableSet s) : StronglyMeasurable fun (x : X) => ν (Prod.mk x ⁻¹' s)

If ν is a vector measure, and s ⊆ X × Y is measurable, then x ↦ ν { y | (x, y) ∈ s } is a strongly measurable function.

theorem MeasureTheory.VectorMeasure.integrable_vectorMeasure_prodMk_left {X : Type u_2} {Y : Type u_3} {E : Type u_4} {F : Type u_5} {mX : MeasurableSpace X} {mY : MeasurableSpace Y} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : VectorMeasure X E} {ν : VectorMeasure Y F} [IsFiniteMeasure μ.variation] {s : Set (X × Y)} (hs : MeasurableSet s) : μ.Integrable fun (x : X) => ν (Prod.mk x ⁻¹' s)

instance MeasureTheory.VectorMeasure.instHasProdOfCompleteSpaceOfIsFiniteMeasureVariation {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} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X E} {ν : VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace G] [IsFiniteMeasure μ.variation] : μ.HasProd ν B

instance MeasureTheory.VectorMeasure.instHasProdOfCompleteSpaceOfIsFiniteMeasureVariation_1 {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} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X E} {ν : VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace G] [h : IsFiniteMeasure ν.variation] : μ.HasProd ν B

theorem MeasureTheory.VectorMeasure.prod_eq_of_forall_apply_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} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X E} {ν : VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G} {ρ : VectorMeasure (X × Y) G} (hρ : ∀ (s : Set X) (t : Set Y), MeasurableSet s → MeasurableSet t → ρ (s ×ˢ t) = (B (μ s)) (ν t)) : μ.prod ν B = ρ

theorem MeasureTheory.VectorMeasure.prod_apply_eq_integral {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} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X E} {ν : VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace G] [IsFiniteMeasure μ.variation] {s : Set (X × Y)} (hs : MeasurableSet s) : (μ.prod ν B) s = ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' s) ∂[B.flip; μ]

theorem MeasureTheory.VectorMeasure.prod_flip_apply_eq_integral {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} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X E} {ν : VectorMeasure Y F} [CompleteSpace G] [IsFiniteMeasure μ.variation] {B : F →L[ℝ] E →L[ℝ] G} {s : Set (X × Y)} (hs : MeasurableSet s) : (μ.prod ν B.flip) s = ∫ᵛ (x : X), ν (Prod.mk x ⁻¹' s) ∂[B; μ]

theorem MeasureTheory.VectorMeasure.variation_prod_le {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} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X E} {ν : VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace G] [IsFiniteMeasure μ.variation] [SFinite ν.variation] : (μ.prod ν B).variation ≤ ‖B‖ₑ • μ.variation.prod ν.variation

instance MeasureTheory.VectorMeasure.instIsFiniteMeasureProdVariationProdOfCompleteSpace {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} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {μ : VectorMeasure X E} {ν : VectorMeasure Y F} {B : E →L[ℝ] F →L[ℝ] G} [CompleteSpace G] [IsFiniteMeasure μ.variation] [IsFiniteMeasure ν.variation] : IsFiniteMeasure (μ.prod ν B).variation