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 aMeasure (α × β)
.
Notation #
μ ⊗ₘ κ = μ.compProd κ
The composition-product of a measure and a kernel.
Equations
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
The composition product of a measure and a constant kernel is the product between the two measures.
Measure.compProd
is associative. We have to insert MeasurableEquiv.prodAssoc
because the products of types α × β × γ
and (α × β) × γ
are different.
Measure.compProd
is associative. We have to insert MeasurableEquiv.prodAssoc
because the products of types α × β × γ
and (α × β) × γ
are different.