English
Let κ: γ→β, η: ε→β′, ξ: (β×ε)→δ, f γ→ε deterministic. Then (ξ ×ₖ η.prodMkLeft β) ∘ₖ (κ ×ₖ deterministic f hf) equals (ξ ∘ₖ (κ ×ₖ deterministic f hf)) ×ₖ (η ∘ₖ deterministic f hf).
Русский
Пусть κ: γ→β, η: ε→β′, ξ: (β×ε)→δ, f: γ→ε детерминирован. Тогда (ξ ×ₖ η.prodMkLeft β) ∘ₖ (κ ×ₖ deterministic f hf) равно (ξ ∘ₖ (κ ×ₖ deterministic f hf)) ×ₖ (η ∘ₖ deterministic f hf).
LaTeX
$$$$(\\xi ×_k \\eta.{\\text{prodMkLeft } β}) ∘_k (\\kappa ×_k deterministic f hf) = (\\xi ∘_k (\\kappa ×_k deterministic f hf)) ×_k (\\eta ∘_k deterministic f hf).$$$$
Lean4
theorem prod_comp_right [SFinite ν] {κ : Kernel β γ} [IsSFiniteKernel κ] :
μ.prod (κ ∘ₘ ν) = (Kernel.id ∥ₖ κ) ∘ₘ (μ.prod ν) :=
by
ext s hs
rw [Measure.prod_apply hs, Measure.bind_apply hs (Kernel.aemeasurable _)]
simp_rw [Measure.bind_apply (measurable_prodMk_left hs) (Kernel.aemeasurable _)]
rw [MeasureTheory.lintegral_prod]
swap; · exact (Kernel.measurable_coe _ hs).aemeasurable
congr with a
congr with b
rw [Kernel.parallelComp_apply, Kernel.id_apply, Measure.prod_apply hs, lintegral_dirac']
exact measurable_measure_prodMk_left hs
