English
Let κ: α → β and η: β → γ be s-finite, μ a finite measure on δ. Then (η ×K (const β μ)) ∘K κ = (η ∘K κ) ×K (const α μ).
Русский
Пусть κ: α → β и η: β → γ — s-finite, μ — конечная мера на δ. Тогда (η ×K (const β μ)) ∘K κ = (η ∘K κ) ×K (const α μ).
LaTeX
$$$\\displaystyle (\\eta \\times_K (\\mathrm{const }\\; \\beta \\; \\mu)) \\circ_K \\kappa = (\\eta \\circ_K \\kappa) \\times_K (\\mathrm{const }\\; \\alpha \\; \\mu)$$$
Lean4
theorem prod_const_comp {δ} {mδ : MeasurableSpace δ} (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel β γ)
[IsSFiniteKernel η] (μ : Measure δ) [SFinite μ] : (η ×ₖ (const β μ)) ∘ₖ κ = (η ∘ₖ κ) ×ₖ (const α μ) :=
by
ext x s ms
simp_rw [comp_apply' _ _ _ ms, prod_apply' _ _ _ ms, const_apply,
lintegral_comp _ _ _ (measurable_measure_prodMk_left ms)]