English
Let (κ_i)_{i∈ι} be a countable family of kernels α → β. Then the kernel obtained by summing the kernels prodMkRight γ (κ_i) across i equals the productMkRight γ of the sum kernel, i.e. Kernel.sum (λ i, Kernel.prodMkRight γ (κ i)) = Kernel.prodMkRight γ (Kernel.sum κ).
Русский
Пусть {κ_i}_{i∈ι} есть счетная семейство ядер α→β. Тогда ядро, получаемое суммированием ядер через prodMkRight γ по всем i, равно prodMkRight γ от суммы ядер: Kernel.sum (λ i, Kernel.prodMkRight γ (κ i)) = Kernel.prodMkRight γ (Kernel.sum κ).
LaTeX
$$$\displaystyle \operatorname{Kernel.sum} \bigl( \lambda i \mapsto \operatorname{Kernel.prodMkRight} \gamma (\kappa i) \bigr) = \operatorname{Kernel.prodMkRight} \gamma (\operatorname{Kernel.sum} \kappa)$$$
Lean4
theorem sum_prodMkRight {ι : Type*} [Countable ι] {κ : ι → Kernel α β} :
Kernel.sum (fun i ↦ Kernel.prodMkRight γ (κ i)) = Kernel.prodMkRight γ (Kernel.sum κ) :=
by
ext
simp_rw [sum_apply, prodMkRight_apply, sum_apply]
