English
Let κ be a kernel γ→β, η be a kernel ε→β′, ξ be a kernel (β×ε)→δ, and f: γ→ε be deterministic. If η does not depend on the output of κ, 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 \\times_k \\eta.{\\text{prodMkLeft } \\beta}) \\circ_k (\\kappa \\times_k deterministic f hf) = (\\xi \\circ_k (\\kappa \\times_k deterministic f hf)) \\times_k (\\eta \\circ_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 `η.prodMkLeft β` for a kernel `η`.
If `κ` was deterministic, this would be true even if `η.prodMkLeft β` 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_prodMkLeft_comp_prod_deterministic {β' ε : Type*} {mβ' : MeasurableSpace β'} {mε : MeasurableSpace ε}
(κ : Kernel γ β) [IsSFiniteKernel κ] (η : Kernel ε β') [IsSFiniteKernel η] (ξ : Kernel (β × ε) δ)
[IsSFiniteKernel ξ] {f : γ → ε} (hf : Measurable f) :
(ξ ×ₖ η.prodMkLeft β) ∘ₖ (κ ×ₖ deterministic f hf) =
(ξ ∘ₖ (κ ×ₖ deterministic f hf)) ×ₖ (η ∘ₖ deterministic f hf) :=
by
ext ω s hs
rw [prod_apply' _ _ _ hs, comp_apply' _ _ _ hs, lintegral_prod_deterministic, lintegral_comp,
lintegral_prod_deterministic]
· congr with b
rw [prod_apply' _ _ _ hs, prodMkLeft_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
