compProd_add_right — Mathlib

English

If κ and η are kernels, then μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η, under finiteness assumptions.

Русский

Если κ, η — ядра, то μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η при соответствующих предпосылках.

LaTeX

$$$μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η$$$

Lean4

theorem compProd_add_right (μ : Measure α) (κ η : Kernel α β) [IsSFiniteKernel κ] [IsSFiniteKernel η] :
    μ ⊗ₘ (κ + η) = μ ⊗ₘ κ + μ ⊗ₘ η := by
  by_cases hμ : SFinite μ
  · simp_rw [Measure.compProd, Kernel.prodMkLeft_add, Kernel.compProd_add_right, Kernel.add_apply]
  · simp [hμ]

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