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.
When both measures have finite variation, we prove stronger results, notably versions of the Fubini theorem. We give general versions for arbitrary pairing functions, and specialized versions for scalar multiplication.
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)
:
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)
Instances
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.
Instances For
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)
:
@[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}
:
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]
:
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}
:
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))
:
@[simp]
theorem
MeasureTheory.VectorMeasure.map_prod_swap
{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}
:
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)
:
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)
:
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]
:
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
theorem
MeasureTheory.Integrable.prod_vectorMeasure
{X : Type u_2}
{Y : Type u_3}
{E : Type u_4}
{F : Type u_5}
{G : Type u_6}
{H : Type u_7}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup H]
{μ : VectorMeasure X E}
{ν : VectorMeasure Y F}
{B : E →L[ℝ] F →L[ℝ] G}
[CompleteSpace G]
[IsFiniteMeasure μ.variation]
[IsFiniteMeasure ν.variation]
{f : X × Y → H}
(hf : Integrable f (μ.variation.prod ν.variation))
:
(μ.prod ν B).Integrable f
theorem
MeasureTheory.VectorMeasure.integral_prod_swap
{X : Type u_2}
{Y : Type u_3}
{E : Type u_4}
{F : Type u_5}
{G : Type u_6}
{H : Type u_7}
{I : Type u_8}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
[NormedAddCommGroup I]
[NormedSpace ℝ I]
{μ : VectorMeasure X E}
{ν : VectorMeasure Y F}
(f : X × Y → H)
{A : E →L[ℝ] F →L[ℝ] G}
{B : H →L[ℝ] G →L[ℝ] I}
:
theorem
MeasureTheory.StronglyMeasurable.integral_vectorMeasure_prod_right
{X : Type u_2}
{Y : Type u_3}
{F : Type u_5}
{G : Type u_6}
{H : Type u_7}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
{ν : VectorMeasure Y F}
{B : G →L[ℝ] F →L[ℝ] H}
[SFinite ν.variation]
⦃f : X → Y → G⦄
(hf : StronglyMeasurable (Function.uncurry f))
:
The vector measure integral is measurable. This shows that the integrand of (the right-hand-side
of) Fubini's theorem is measurable. This version has f in curried form.
theorem
MeasureTheory.StronglyMeasurable.integral_vectorMeasure_prod_right'
{X : Type u_2}
{Y : Type u_3}
{F : Type u_5}
{G : Type u_6}
{H : Type u_7}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
{ν : VectorMeasure Y F}
{B : G →L[ℝ] F →L[ℝ] H}
[SFinite ν.variation]
⦃f : X × Y → G⦄
(hf : StronglyMeasurable f)
:
The vector measure integral is measurable. This shows that the integrand of (the right-hand-side of) Fubini's theorem is measurable.
theorem
MeasureTheory.StronglyMeasurable.integral_vectorMeasure_prod_left
{X : Type u_2}
{Y : Type u_3}
{E : Type u_4}
{G : Type u_6}
{H : Type u_7}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
{μ : VectorMeasure X E}
{B : G →L[ℝ] E →L[ℝ] H}
[SFinite μ.variation]
⦃f : X → Y → G⦄
(hf : StronglyMeasurable (Function.uncurry f))
:
The vector measure integral is measurable. This shows that the integrand of (the right-hand-side
of) the symmetric version of Fubini's theorem is measurable.
This version has f in curried form.
theorem
MeasureTheory.StronglyMeasurable.integral_vectorMeasure_prod_left'
{X : Type u_2}
{Y : Type u_3}
{E : Type u_4}
{G : Type u_6}
{H : Type u_7}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
{μ : VectorMeasure X E}
{B : G →L[ℝ] E →L[ℝ] H}
[SFinite μ.variation]
⦃f : X × Y → G⦄
(hf : StronglyMeasurable f)
:
The vector measure integral is measurable. This shows that the integrand of (the right-hand-side of) the symmetric version of Fubini's theorem is measurable.
theorem
MeasureTheory.AEStronglyMeasurable.integral_vectorMeasure_prod_right'
{X : Type u_2}
{Y : Type u_3}
{F : Type u_5}
{G : Type u_6}
{H : Type u_7}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
{ν : VectorMeasure Y F}
{B : G →L[ℝ] F →L[ℝ] H}
[SFinite ν.variation]
{μ : Measure X}
⦃f : X × Y → G⦄
(hf : AEStronglyMeasurable f (μ.prod ν.variation))
:
The vector measure integral is a.e.-measurable. This shows that the integrand of (the right-hand-side of) Fubini's theorem is a.e.-measurable.
theorem
MeasureTheory.Integrable.integral_vectorMeasure_prod_left
{X : Type u_2}
{Y : Type u_3}
{F : Type u_5}
{G : Type u_6}
{H : Type u_7}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
{ν : VectorMeasure Y F}
{B : G →L[ℝ] F →L[ℝ] H}
[SFinite ν.variation]
{μ : Measure X}
⦃f : X × Y → G⦄
(hf : Integrable f (μ.prod ν.variation))
:
theorem
MeasureTheory.VectorMeasure.lintegral_fn_integral_sub
{X : Type u_2}
{Y : Type u_3}
{F : Type u_5}
{G : Type u_6}
{H : Type u_7}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
{ν : VectorMeasure Y F}
⦃f g : X × Y → G⦄
{μ : Measure X}
{B : G →L[ℝ] F →L[ℝ] H}
[SFinite μ]
[SFinite ν.variation]
(φ : H → ENNReal)
(hf : Integrable f (μ.prod ν.variation))
(hg : Integrable g (μ.prod ν.variation))
:
Vector measure integrals commute with subtraction inside a lower Lebesgue integral.
theorem
MeasureTheory.VectorMeasure.continuous_integral_integral
{X : Type u_2}
{Y : Type u_3}
{E : Type u_4}
{F : Type u_5}
{G : Type u_6}
{H : Type u_7}
{I : Type u_8}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
[NormedAddCommGroup I]
[NormedSpace ℝ I]
{μ : VectorMeasure X E}
{ν : VectorMeasure Y F}
{B : G →L[ℝ] F →L[ℝ] H}
{C : H →L[ℝ] E →L[ℝ] I}
[SFinite ν.variation]
[SFinite μ.variation]
:
The map that sends an L¹-function f : X × Y → G to ∫∫f is continuous.
theorem
MeasureTheory.VectorMeasure.integral_prod
{X : Type u_2}
{Y : Type u_3}
{E : Type u_4}
{F : Type u_5}
{G : Type u_6}
{H : Type u_7}
{I : Type u_8}
{J : Type u_9}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
[NormedAddCommGroup I]
[NormedSpace ℝ I]
[NormedAddCommGroup J]
[NormedSpace ℝ J]
{μ : VectorMeasure X E}
{ν : VectorMeasure Y F}
{B : G →L[ℝ] F →L[ℝ] J}
{C : J →L[ℝ] E →L[ℝ] I}
{A : E →L[ℝ] F →L[ℝ] H}
{D : G →L[ℝ] H →L[ℝ] I}
[CompleteSpace H]
[CompleteSpace J]
[IsFiniteMeasure ν.variation]
[IsFiniteMeasure μ.variation]
{f : X × Y → G}
(hf : Integrable f (μ.variation.prod ν.variation))
(h : ∀ (x : G) (y : E) (z : F), (D x) ((A y) z) = (C ((B x) z)) y)
:
Fubini's Theorem: For integrable functions on X × Y,
the vector measure integral of f for the product vector measure is equal to the iterated vector
measure integral. We express this with respect to general pairing functions, with a compatibility
condition saying that the compositions coincide up to reordering.
theorem
MeasureTheory.VectorMeasure.integral_prod_smul
{X : Type u_2}
{Y : Type u_3}
{E : Type u_4}
{F : Type u_5}
{H : Type u_7}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
{μ : VectorMeasure X E}
{ν : VectorMeasure Y F}
[CompleteSpace F]
{B : E →L[ℝ] F →L[ℝ] H}
[IsFiniteMeasure ν.variation]
[IsFiniteMeasure μ.variation]
{f : X × Y → ℝ}
(hf : Integrable f (μ.variation.prod ν.variation))
:
Fubini's Theorem: For integrable functions on X × Y,
the vector measure integral of f for the product vector measure is equal to the iterated vector
measure integral. Version where f is scalar.
theorem
MeasureTheory.VectorMeasure.integral_prod_symm
{X : Type u_2}
{Y : Type u_3}
{E : Type u_4}
{F : Type u_5}
{G : Type u_6}
{H : Type u_7}
{I : Type u_8}
{J : Type u_9}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
[NormedAddCommGroup I]
[NormedSpace ℝ I]
[NormedAddCommGroup J]
[NormedSpace ℝ J]
{μ : VectorMeasure X E}
{ν : VectorMeasure Y F}
{B : G →L[ℝ] E →L[ℝ] J}
{C : J →L[ℝ] F →L[ℝ] I}
{A : E →L[ℝ] F →L[ℝ] H}
{D : G →L[ℝ] H →L[ℝ] I}
[CompleteSpace H]
[CompleteSpace J]
[IsFiniteMeasure ν.variation]
[IsFiniteMeasure μ.variation]
{f : X × Y → G}
(hf : Integrable f (μ.variation.prod ν.variation))
(h : ∀ (x : G) (y : F) (z : E), (D x) ((A z) y) = (C ((B x) z)) y)
:
Symmetric version of Fubini's Theorem: For integrable functions on X × Y,
the vector measure integral of f for the product vector measure is equal to the iterated vector
measure integral. We express this with respect to general pairing functions, with a compatibility
condition saying that the compositions coincide up to reordering.
This version has the integrals on the right-hand side in the other order.
theorem
MeasureTheory.VectorMeasure.integral_prod_smul_symm
{X : Type u_2}
{Y : Type u_3}
{E : Type u_4}
{F : Type u_5}
{H : Type u_7}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
{μ : VectorMeasure X E}
{ν : VectorMeasure Y F}
[CompleteSpace E]
{B : E →L[ℝ] F →L[ℝ] H}
[IsFiniteMeasure ν.variation]
[IsFiniteMeasure μ.variation]
{f : X × Y → ℝ}
(hf : Integrable f (μ.variation.prod ν.variation))
:
Fubini's Theorem: For integrable functions on X × Y,
the vector measure integral of f for the product vector measure is equal to the iterated vector
measure integral. Version where f is scalar.
This version has the integrals on the right-hand side in the other order.
theorem
MeasureTheory.VectorMeasure.integral_integral
{X : Type u_2}
{Y : Type u_3}
{E : Type u_4}
{F : Type u_5}
{G : Type u_6}
{H : Type u_7}
{I : Type u_8}
{J : Type u_9}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
[NormedAddCommGroup I]
[NormedSpace ℝ I]
[NormedAddCommGroup J]
[NormedSpace ℝ J]
{μ : VectorMeasure X E}
{ν : VectorMeasure Y F}
{B : G →L[ℝ] F →L[ℝ] J}
{C : J →L[ℝ] E →L[ℝ] I}
{A : E →L[ℝ] F →L[ℝ] H}
{D : G →L[ℝ] H →L[ℝ] I}
[CompleteSpace H]
[CompleteSpace J]
[IsFiniteMeasure ν.variation]
[IsFiniteMeasure μ.variation]
{f : X → Y → G}
(hf : Integrable (Function.uncurry f) (μ.variation.prod ν.variation))
(h : ∀ (x : G) (y : E) (z : F), (D x) ((A y) z) = (C ((B x) z)) y)
:
Reversed version of Fubini's Theorem.
theorem
MeasureTheory.VectorMeasure.integral_integral_smul
{X : Type u_2}
{Y : Type u_3}
{E : Type u_4}
{F : Type u_5}
{H : Type u_7}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
{μ : VectorMeasure X E}
{ν : VectorMeasure Y F}
[CompleteSpace F]
{B : E →L[ℝ] F →L[ℝ] H}
[IsFiniteMeasure ν.variation]
[IsFiniteMeasure μ.variation]
{f : X → Y → ℝ}
(hf : Integrable (Function.uncurry f) (μ.variation.prod ν.variation))
:
Reversed version of Fubini's Theorem, version with a scalar function.
theorem
MeasureTheory.VectorMeasure.integral_integral_symm
{X : Type u_2}
{Y : Type u_3}
{E : Type u_4}
{F : Type u_5}
{G : Type u_6}
{H : Type u_7}
{I : Type u_8}
{J : Type u_9}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
[NormedAddCommGroup I]
[NormedSpace ℝ I]
[NormedAddCommGroup J]
[NormedSpace ℝ J]
{μ : VectorMeasure X E}
{ν : VectorMeasure Y F}
{B : G →L[ℝ] E →L[ℝ] J}
{C : J →L[ℝ] F →L[ℝ] I}
{A : E →L[ℝ] F →L[ℝ] H}
{D : G →L[ℝ] H →L[ℝ] I}
[CompleteSpace H]
[CompleteSpace J]
[IsFiniteMeasure ν.variation]
[IsFiniteMeasure μ.variation]
{f : X → Y → G}
(hf : Integrable (Function.uncurry f) (μ.variation.prod ν.variation))
(h : ∀ (x : G) (y : F) (z : E), (D x) ((A z) y) = (C ((B x) z)) y)
:
Reversed version of Fubini's Theorem (symmetric version).
theorem
MeasureTheory.VectorMeasure.integral_integral_smul_symm
{X : Type u_2}
{Y : Type u_3}
{E : Type u_4}
{F : Type u_5}
{H : Type u_7}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
{μ : VectorMeasure X E}
{ν : VectorMeasure Y F}
[CompleteSpace E]
{B : E →L[ℝ] F →L[ℝ] H}
[IsFiniteMeasure ν.variation]
[IsFiniteMeasure μ.variation]
{f : X → Y → ℝ}
(hf : Integrable (Function.uncurry f) (μ.variation.prod ν.variation))
:
Reversed version of Fubini's Theorem (symmetric version), version with a scalar function.
theorem
MeasureTheory.VectorMeasure.integral_integral_swap
{X : Type u_2}
{Y : Type u_3}
{E : Type u_4}
{F : Type u_5}
{G : Type u_6}
{H : Type u_7}
{I : Type u_8}
{J : Type u_9}
{mX : MeasurableSpace X}
{mY : MeasurableSpace Y}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[NormedAddCommGroup F]
[NormedSpace ℝ F]
[NormedAddCommGroup G]
[NormedSpace ℝ G]
[NormedAddCommGroup H]
[NormedSpace ℝ H]
[NormedAddCommGroup I]
[NormedSpace ℝ I]
[NormedAddCommGroup J]
[NormedSpace ℝ J]
{μ : VectorMeasure X E}
{ν : VectorMeasure Y F}
[IsFiniteMeasure ν.variation]
[IsFiniteMeasure μ.variation]
⦃f : X → Y → G⦄
[CompleteSpace H]
[CompleteSpace J]
{B : G →L[ℝ] F →L[ℝ] H}
{C : H →L[ℝ] E →L[ℝ] I}
{A : G →L[ℝ] E →L[ℝ] J}
{D : J →L[ℝ] F →L[ℝ] I}
(hf : Integrable (Function.uncurry f) (μ.variation.prod ν.variation))
(h : ∀ (x : G) (y : F) (z : E), (C ((B x) y)) z = (D ((A x) z)) y)
:
Change the order of integration in integrals wrt vector measures. We express this with respect to general pairing functions, with a compatibility condition saying that the compositions coincide up to reordering.
theorem
MeasureTheory.VectorMeasure.integral_integral_smul_swap
{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 E]
[CompleteSpace F]
[IsFiniteMeasure ν.variation]
[IsFiniteMeasure μ.variation]
⦃f : X → Y → ℝ⦄
{B : E →L[ℝ] F →L[ℝ] G}
(hf : Integrable (Function.uncurry f) (μ.variation.prod ν.variation))
:
Change the order of integration in integrals wrt vector measures.
Case where f is scalar.