parallelComp_sum_right — Mathlib

English

Analogous to the left sum, κ ∥ Kernel.sum η_i equals Kernel.sum (κ ∥ η_i).

Русский

Аналогично, κ ∥ Kernel.sum η_i = Kernel.sum (κ ∥ η_i).

LaTeX

$$$$κ \\parallel Kernel.sum η = Kernel.sum (λ i, κ \\parallel η_i).$$$$

Lean4

theorem parallelComp_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 x
  simp_rw [Kernel.sum_apply, parallelComp_apply, Kernel.sum_apply, Measure.prod_sum_right]

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