English
For measurable sets s ⊆ β × γ, κ ⊗ₖ η evaluated at a on s equals the integral ∫ η(a,b)(Prod.mk b⁻¹' s) dκ(a)(b).
Русский
Для измеримого множества s ⊆ β × γ имеет место (κ ⊗ₖ η) a (s) = ∫ η(a,b) (Prod.mk b⁻¹' s) dκ(a)(b).
LaTeX
$$$$ (\kappa \otimes_k \eta)(a)(s) = \int_{\beta} \eta(a,b)(\,Prod.mk b^{-1}' s\,) \, d\kappa(a)(b) $$$$
Lean4
theorem compProd_apply (hs : MeasurableSet s) (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ)
[IsSFiniteKernel η] (a : α) : (κ ⊗ₖ η) a s = ∫⁻ b, η (a, b) (Prod.mk b ⁻¹' s) ∂κ a :=
by
rw [compProd, comp_apply, copy_apply, Measure.dirac_bind (by fun_prop), comp_apply, parallelComp_apply,
Kernel.id_apply, Measure.bind_apply hs (by fun_prop), lintegral_prod _ (Kernel.measurable_coe _ hs).aemeasurable,
lintegral_dirac']
swap
· suffices
Measurable fun p : α × β ↦
(swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic MeasurableEquiv.prodAssoc.symm (MeasurableEquiv.measurable _) ∘ₖ
(Kernel.id ∥ₖ copy β))
p s
by fun_prop
exact Kernel.measurable_coe _ hs
congr with b
rw [comp_apply, parallelComp_apply, Kernel.id_apply, copy_apply, Measure.dirac_prod_dirac,
Measure.dirac_bind (by fun_prop), comp_apply, deterministic_apply (by fun_prop), Measure.dirac_bind (by fun_prop),
comp_apply]
simp only [MeasurableEquiv.prodAssoc, MeasurableEquiv.symm_mk, MeasurableEquiv.coe_mk, Equiv.prodAssoc_symm_apply]
rw [parallelComp_apply, Kernel.id_apply, Measure.bind_apply hs (by fun_prop),
lintegral_prod _ (Kernel.measurable_coe _ hs).aemeasurable]
classical
have h_int x : ∫⁻ y, swap γ β (x, y) s ∂Measure.dirac b = (Prod.mk b ⁻¹' s).indicator 1 x :=
by
rw [lintegral_dirac']
· simp [swap_apply' _ hs, Set.indicator_apply]
· simpa [swap_apply' _ hs, Prod.swap_prod_mk] using measurable_const.indicator (measurable_prodMk_right hs)
simp_rw [h_int]
rw [lintegral_indicator_one]
exact measurable_prodMk_left hs
