English
If ι is a countable index set and κ: ι → Kernel α β, η: Kernel β γ, then composing η with Kernel.sum κ equals Kernel.sum of the compositions: η ∘ₖ Kernel.sum κ = Kernel.sum (i ↦ η ∘ₖ (κ i)).
Русский
Если индексное множество ι счётно и κ: ι → Kernel α β, η: Kernel β γ, то композиция η с суммой Kernel.sum κ равна сумме композиций: η ∘ₖ Kernel.sum κ = Kernel.sum (i ↦ η ∘ₖ κ i).
LaTeX
$$$ \eta \circ_K \Kernel.sum \kappa = \Kernel.sum (\lambda i. \eta \circ_K (\kappa i))$$$
Lean4
theorem comp_sum_right {ι : Type*} [Countable ι] (κ : ι → Kernel α β) (η : Kernel β γ) :
η ∘ₖ Kernel.sum κ = Kernel.sum fun i ↦ η ∘ₖ (κ i) :=
by
ext _ _ hs
simp_rw [sum_apply, comp_apply' _ _ _ hs, Measure.sum_apply _ hs, sum_apply, lintegral_sum_measure,
comp_apply' _ _ _ hs]