compProd_sum_left — Mathlib

English

If ι is countable and κ: ι → Kernel α β with each κ_i S-finite, then Kernel.sum κ ⊗ η = Kernel.sum (i ↦ κ_i ⊗ η).

Русский

Если ι — счетное множество и κ_i — ядра, то сумма κ_i ⊗ η эквивалентна сумме по i.

LaTeX

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

Lean4

theorem compProd_sum_left {ι : Type*} [Countable ι] {κ : ι → Kernel α β} {η : Kernel (α × β) γ}
    [∀ i, IsSFiniteKernel (κ i)] : Kernel.sum κ ⊗ₖ η = Kernel.sum (fun i ↦ (κ i) ⊗ₖ η) :=
  by
  by_cases hη : IsSFiniteKernel η
  · ext a s hs
    simp_rw [sum_apply, compProd_apply hs, sum_apply, lintegral_sum_measure, Measure.sum_apply _ hs, compProd_apply hs]
  · simp [hη]

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