Commit 2023-12-07 17:41 cd73b841
View on Github →feat: define the composition-product of a measure and a kernel (#8852)
The composition-product of a measure and a kernel, 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) ∂μ.
This PR also modifies the Disintegration file to use the new definition.
From the PFR project.