English
Let κ and η be s-finite kernels on their respective spaces. For x = (a, c) and any measurable set s ⊆ β × δ, the value of the parallel composition (κ ∥ₖ η) at x on s is given by the integral over b in β of the δ-measure η at x₂ applied to the fiber {d ∈ δ : (b, d) ∈ s}, with respect to κ at x₁.
Русский
Пусть κ и η — s конечные ядра на соответствующих пространствах. Для x = (a, c) и любого измеримого множества s ⊆ β × δ значение параллельной композиции (κ ∥ₖ η) в точке x на s задаётся интегралом по b ∈ β от меры η на δ, применённой к ответвению {d ∈ δ : (b, d) ∈ s}, взвешенным мерой κ в x₁.
LaTeX
$$$$(κ ∥ₖ η) x s = \\int^{-}_{b} η x.2 (Prod.mk b ⁻¹' s) \\; dκ x.1,$$$$
Lean4
theorem parallelComp_apply' [IsSFiniteKernel κ] [IsSFiniteKernel η] {s : Set (β × δ)} (hs : MeasurableSet s) :
(κ ∥ₖ η) x s = ∫⁻ b, η x.2 (Prod.mk b ⁻¹' s) ∂κ x.1 := by rw [parallelComp_apply, Measure.prod_apply hs]
