Composition-product of kernels #
We define the composition-product κ ⊗ₖ η of two s-finite kernels κ : Kernel α β and
η : Kernel (α × β) γ, a kernel from α to β × γ.
A note on names:
The composition-product Kernel α β → Kernel (α × β) γ → Kernel α (β × γ) is named composition in
[Kal21] and product on the wikipedia article on transition kernels.
Most papers studying categories of kernels call composition the map we call composition. We adopt
that convention because it fits better with the use of the name comp elsewhere in mathlib.
Main definitions #
compProd (κ : Kernel α β) (η : Kernel (α × β) γ) : Kernel α (β × γ): composition-product of 2 s-finite kernels. We define a notationκ ⊗ₖ η = compProd κ η.∫⁻ bc, f bc ∂((κ ⊗ₖ η) a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a)
Main statements #
lintegral_compProd: Lebesgue integral of a function against a composition-product of kernels.- Instances stating that
IsMarkovKernel,IsZeroOrMarkovKernel,IsFiniteKernelandIsSFiniteKernelare stable by composition-product.
Notation #
κ ⊗ₖ η = ProbabilityTheory.Kernel.compProd κ η
Composition-Product of kernels #
We define a kernel composition-product
compProd : Kernel α β → Kernel (α × β) γ → Kernel α (β × γ).
Composition-Product of kernels. For s-finite kernels, it satisfies
∫⁻ bc, f bc ∂(compProd κ η a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a)
(see ProbabilityTheory.Kernel.lintegral_compProd).
If either of the kernels is not s-finite, compProd is given the junk value 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Composition-Product of kernels. For s-finite kernels, it satisfies
∫⁻ bc, f bc ∂(compProd κ η a) = ∫⁻ b, ∫⁻ c, f (b, c) ∂(η (a, b)) ∂(κ a)
(see ProbabilityTheory.Kernel.lintegral_compProd).
If either of the kernels is not s-finite, compProd is given the junk value 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
ae filter of the composition-product #
Lebesgue integral #
Lebesgue integral against the composition-product of two kernels.
Lebesgue integral against the composition-product of two kernels.
Lebesgue integral against the composition-product of two kernels.
Kernel.compProd is associative. We have to insert MeasurableEquiv.prodAssoc in two places
because the products of types α × β × γ and (α × β) × γ are different.
If η is a Markov kernel, use instead fst_compProd to get (κ ⊗ₖ η).fst = κ.