English
For η : Kernel β γ, μ finite, κ finite, the equality (μ.compProd κ).bind (η.prodMkLeft α) equals ((μ.bind κ).bind η).
Русский
Для η: Kernel β γ и конечной μ, κ выполняется равенство (μ.compProd κ).bind (η.prodMkLeft α) = ((μ.bind κ).bind η).
LaTeX
$$$[SFinite(\\mu)] [IsSFiniteKernel(\\kappa)] \\\\Rightarrow ((\\mu.compProd κ).bind (κ.``η.mkLeft α)) = ((\\mu.bind κ).bind η)$$$
Lean4
theorem comp_compProd_comm {η : Kernel (α × β) γ} [SFinite μ] [IsSFiniteKernel η] :
η ∘ₘ (μ ⊗ₘ κ) = ((κ ⊗ₖ η) ∘ₘ μ).snd := by
by_cases hκ : IsSFiniteKernel κ; swap
· simp [compProd_of_not_isSFiniteKernel _ _ hκ, Kernel.compProd_of_not_isSFiniteKernel_left _ _ hκ]
ext s hs
rw [Measure.bind_apply hs η.aemeasurable, Measure.snd_apply hs, Measure.bind_apply _ (Kernel.aemeasurable _),
Measure.lintegral_compProd (η.measurable_coe hs)]
swap; · exact measurable_snd hs
congr with a
rw [Kernel.compProd_apply]
· rfl
· exact measurable_snd hs
