compProd_add_left — Mathlib

English

If κ is a kernel and μ, ν are measures with finite mass, then (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ.

Русский

Если κ — ядро, а μ, ν имеют конечную массу, то (μ + ν) ⊗ₘ κ = μ ⊗ₘ κ + ν ⊗ₘ κ.

LaTeX

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

Lean4

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

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