parallelComp_sum_left — Mathlib

English

If κ is a countable family of kernels κ_i, then the sum κ ∥ η equals the sum of the parallel compositions κ_i ∥ η, provided η is s-finite.

Русский

Если имеется счетное семейство ядер κ_i, сумма κ ∥ η равна сумма κ_i ∥ η, при условии, что η удовлетворяет условию s-конечности.

LaTeX

$$$$\\mathrm{Kernel.sum}\\, κ \\parallel η = \\mathrm{Kernel.sum}\\, (i \\mapsto κ_i \\parallel η).$$$$

Lean4

theorem parallelComp_sum_left {ι : Type*} [Countable ι] (κ : ι → Kernel α β) [∀ i, IsSFiniteKernel (κ i)]
    (η : Kernel γ δ) : 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_left]

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