comp_sum_left — Mathlib

English

Let κ: Kernel α β and η i: ι → Kernel β γ with ι countable. Then (Kernel.sum η) ∘ₖ κ = Kernel.sum (i ↦ (η i) ∘ₖ κ).

Русский

Пусть κ: α → β и η_i: β → γ для i в ι, где ι счётно. Тогда (Kernel.sum η) ∘ₖ κ = Kernel.sum (i ↦ (η i) ∘ₖ κ).

LaTeX

$$$ (Kernel.sum \eta) \circ_K \kappa = Kernel.sum (\lambda i. (\eta i) \circ_K \kappa) $$$

Lean4

theorem comp_sum_left {ι : Type*} [Countable ι] (κ : Kernel α β) (η : ι → Kernel β γ) :
    (Kernel.sum η) ∘ₖ κ = Kernel.sum (fun i ↦ (η i) ∘ₖ κ) :=
  by
  ext _ _ hs
  simp_rw [sum_apply, comp_apply' _ _ _ hs, sum_apply, Measure.sum_apply _ hs, comp_apply' _ _ _ hs]
  rw [lintegral_tsum]
  exact fun _ ↦ (Kernel.measurable_coe _ hs).aemeasurable

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