# Composition-Product of a measure and a kernel #

This operation, denoted by ⊗ₘ, takes μ : Measure α and κ : kernel α β and creates μ ⊗ₘ κ : Measure (α × β). The integral of a function against μ ⊗ₘ κ is ∫⁻ x, f x ∂(μ ⊗ₘ κ) = ∫⁻ a, ∫⁻ b, f (a, b) ∂(κ a) ∂μ.

μ ⊗ₘ κ is defined as ((kernel.const Unit μ) ⊗ₖ (kernel.prodMkLeft Unit κ)) ().

## Main definitions #

• Measure.compProd: from μ : Measure α and κ : kernel α β, get a Measure (α × β).

## Notations #

• μ ⊗ₘ κ = μ.compProd κ
noncomputable def MeasureTheory.Measure.compProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (μ : ) (κ : ()) :

The composition-product of a measure and a kernel.

Equations
• μ.compProd κ =
Instances For

The composition-product of a measure and a kernel.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem MeasureTheory.Measure.compProd_zero_left {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (κ : ()) :
@[simp]
theorem MeasureTheory.Measure.compProd_zero_right {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (μ : ) :
μ.compProd 0 = 0
theorem MeasureTheory.Measure.compProd_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {μ : } {κ : ()} {s : Set (α × β)} (hs : ) :
(μ.compProd κ) s = ∫⁻ (a : α), (κ a) ( ⁻¹' s)μ
theorem MeasureTheory.Measure.compProd_apply_prod {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {μ : } {κ : ()} {s : Set α} {t : Set β} (hs : ) (ht : ) :
(μ.compProd κ) (s ×ˢ t) = ∫⁻ (a : α) in s, (κ a) tμ
theorem MeasureTheory.Measure.compProd_congr {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {μ : } {κ : ()} {η : ()} (h : μ.ae.EventuallyEq κ η) :
μ.compProd κ = μ.compProd η
theorem MeasureTheory.Measure.ae_compProd_of_ae_ae {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {μ : } {κ : ()} {p : α × βProp} (hp : MeasurableSet {x : α × β | p x}) (h : ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b)) :
∀ᵐ (x : α × β) ∂μ.compProd κ, p x
theorem MeasureTheory.Measure.ae_ae_of_ae_compProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {μ : } {κ : ()} {p : α × βProp} (h : ∀ᵐ (x : α × β) ∂μ.compProd κ, p x) :
∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b)
theorem MeasureTheory.Measure.ae_compProd_iff {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {μ : } {κ : ()} {p : α × βProp} (hp : MeasurableSet {x : α × β | p x}) :
(∀ᵐ (x : α × β) ∂μ.compProd κ, p x) ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b)
theorem MeasureTheory.Measure.compProd_add_left {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (μ : ) (ν : ) (κ : ()) :
(μ + ν).compProd κ = μ.compProd κ + ν.compProd κ
theorem MeasureTheory.Measure.compProd_add_right {α : Type u_1} {β : Type u_2} {mα : } {mβ : } (μ : ) (κ : ()) (η : ()) :
μ.compProd (κ + η) = μ.compProd κ + μ.compProd η
theorem MeasureTheory.Measure.lintegral_compProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {μ : } {κ : ()} {f : α × βENNReal} (hf : ) :
∫⁻ (x : α × β), f xμ.compProd κ = ∫⁻ (a : α), ∫⁻ (b : β), f (a, b)κ aμ
theorem MeasureTheory.Measure.set_lintegral_compProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {μ : } {κ : ()} {f : α × βENNReal} (hf : ) {s : Set α} (hs : ) {t : Set β} (ht : ) :
∫⁻ (x : α × β) in s ×ˢ t, f xμ.compProd κ = ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b)κ aμ
theorem MeasureTheory.Measure.integrable_compProd_iff {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {μ : } {κ : ()} {E : Type u_3} {f : α × βE} (hf : MeasureTheory.AEStronglyMeasurable f (μ.compProd κ)) :
MeasureTheory.Integrable f (μ.compProd κ) (∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun (y : β) => f (x, y)) (κ x)) MeasureTheory.Integrable (fun (x : α) => ∫ (y : β), f (x, y)κ x) μ
theorem MeasureTheory.Measure.integral_compProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {μ : } {κ : ()} {E : Type u_3} [] {f : α × βE} (hf : MeasureTheory.Integrable f (μ.compProd κ)) :
∫ (x : α × β), f xμ.compProd κ = ∫ (a : α), ∫ (b : β), f (a, b)κ aμ
theorem MeasureTheory.Measure.setIntegral_compProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {μ : } {κ : ()} {E : Type u_3} [] {s : Set α} (hs : ) {t : Set β} (ht : ) {f : α × βE} (hf : MeasureTheory.IntegrableOn f (s ×ˢ t) (μ.compProd κ)) :
∫ (x : α × β) in s ×ˢ t, f xμ.compProd κ = ∫ (a : α) in s, ∫ (b : β) in t, f (a, b)κ aμ
@[deprecated MeasureTheory.Measure.setIntegral_compProd]
theorem MeasureTheory.Measure.set_integral_compProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {μ : } {κ : ()} {E : Type u_3} [] {s : Set α} (hs : ) {t : Set β} (ht : ) {f : α × βE} (hf : MeasureTheory.IntegrableOn f (s ×ˢ t) (μ.compProd κ)) :
∫ (x : α × β) in s ×ˢ t, f xμ.compProd κ = ∫ (a : α) in s, ∫ (b : β) in t, f (a, b)κ aμ

Alias of MeasureTheory.Measure.setIntegral_compProd.

theorem MeasureTheory.Measure.dirac_compProd_apply {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {κ : ()} {a : α} {s : Set (α × β)} (hs : ) :
(.compProd κ) s = (κ a) ( ⁻¹' s)
theorem MeasureTheory.Measure.dirac_unit_compProd {β : Type u_2} {mβ : } (κ : ) :
.compProd κ =
theorem MeasureTheory.Measure.dirac_unit_compProd_const {β : Type u_2} {mβ : } (μ : ) :
@[simp]
theorem MeasureTheory.Measure.snd_dirac_unit_compProd_const {β : Type u_2} {mβ : } (μ : ) :
(.compProd ).snd = μ
instance MeasureTheory.Measure.instSFiniteProdCompProd {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {μ : } {κ : ()} :
MeasureTheory.SFinite (μ.compProd κ)
Equations
• =
instance MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {μ : } {κ : ()} :
Equations
• =
instance MeasureTheory.Measure.instIsProbabilityMeasureProdCompProdOfIsMarkovKernel {α : Type u_1} {β : Type u_2} {mα : } {mβ : } {μ : } {κ : ()} :
Equations
• =