compProd_sum_right — Mathlib

English

Analogous to Left Sum, Kernel.sum η i composed with κ equals Kernel.sum (κ ⊗ η i).

Русский

Аналогично слева: сумма η по i преобразуется в сумму κ ⊗ η_i.

LaTeX

$$$$ \\mathrm{Kernel.sum} κ \\otimes_{\\kern-0.2em} (\\mathrm{Kernel.sum}\\ η) \\ = \\ \\mathrm{Kernel.sum}\\ (i \\mapsto κ \\otimes_{\\kern-0.2em} η_i). $$$$

Lean4

theorem compProd_sum_right {ι : Type*} [Countable ι] {κ : Kernel α β} {η : ι → Kernel (α × β) γ}
    [∀ i, IsSFiniteKernel (η i)] : κ ⊗ₖ Kernel.sum η = Kernel.sum (fun i ↦ κ ⊗ₖ (η i)) :=
  by
  by_cases hκ : IsSFiniteKernel κ
  swap; · simp [hκ]
  ext a s hs
  simp_rw [sum_apply, compProd_apply hs, Measure.sum_apply _ hs, sum_apply, compProd_apply hs]
  rw [← lintegral_tsum]
  · congr with i
    rw [Measure.sum_apply]
    exact measurable_prodMk_left hs
  · exact fun _ ↦ (measurable_kernel_prodMk_left' hs a).aemeasurable

Похожие утверждения