English
Let κ γ→β, η ε→β′, ξ (ε×β)→δ, f γ→ε be deterministic. Then (ξ ×ₖ η.prodMkRight β) ∘ₖ (deterministic f hf ×ₖ κ) = (ξ ∘ₖ (deterministic f hf ×ₖ κ)) ×ₖ (η ∘ₖ deterministic f hf).
Русский
Пусть κ: γ→β, η: ε→β′, ξ: (ε×β)→δ, и f детерминирован. Тогда (ξ ×ₖ η.prodMkRight β) ∘ₖ (deterministic f hf ×ₖ κ) = (ξ ∘ₖ (deterministic f hf ×ₖ κ)) ×ₖ (η ∘ₖ deterministic f hf).
LaTeX
$$$$(\\xi ×_k η.{\\text{prodMkRight } β}) ∘_k (deterministic f hf ×_k κ) = (\\xi ∘_k (deterministic f hf ×_k κ)) ×_k (η ∘_k deterministic f hf).$$$$
Lean4
/-- The composition of two product kernels `(ξ ×ₖ η') ∘ₖ (ζ ×ₖ κ)` is the product of the
compositions, `(ξ ∘ₖ (ζ ×ₖ κ)) ×ₖ (η' ∘ₖ (ζ ×ₖ κ))`, if `ζ` is deterministic (of the form
`.deterministic f hf`) and `η'` does not depend on the output of `κ`.
That is, `η'` has the form `η.prodMkRight β` for a kernel `η`.
If `κ` was deterministic, this would be true even if `η.prodMkRight β` was a more general
kernel since `Kernel.deterministic f hf ×ₖ κ` would be deterministic and commute with copying.
Here `κ` is not deterministic, but it is discarded in one branch of the copy. -/
theorem prod_prodMkRight_comp_deterministic_prod {β' ε : Type*} {mβ' : MeasurableSpace β'} {mε : MeasurableSpace ε}
(κ : Kernel γ β) [IsSFiniteKernel κ] (η : Kernel ε β') [IsSFiniteKernel η] (ξ : Kernel (ε × β) δ)
[IsSFiniteKernel ξ] {f : γ → ε} (hf : Measurable f) :
(ξ ×ₖ η.prodMkRight β) ∘ₖ (deterministic f hf ×ₖ κ) =
(ξ ∘ₖ (deterministic f hf ×ₖ κ)) ×ₖ (η ∘ₖ deterministic f hf) :=
by
ext ω s hs
rw [prod_apply' _ _ _ hs, comp_apply' _ _ _ hs, lintegral_deterministic_prod, lintegral_comp,
lintegral_deterministic_prod]
· congr with b
rw [prod_apply' _ _ _ hs, prodMkRight_apply, comp_deterministic_eq_comap, comap_apply]
· exact (measurable_measure_prodMk_left hs).lintegral_kernel
· exact measurable_measure_prodMk_left hs
· exact Kernel.measurable_coe _ hs
