compProd_apply_eq_compProd_sectR — Mathlib

English

For kernels κ and η, (κ ⊗ₖ η) a equals (κ a) ⊗ₘ (η.sectR a) for each a.

Русский

Для ядра κ и η выполнено: (κ ⊗ₖ η) a = (κ a) ⊗ₘ (η.sectR a) для каждого a.

LaTeX

$$$(κ ⊗ₖ η) a = (κ a) ⊗_m (η.sectR a)$$$

Lean4

theorem _root_.ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR {γ : Type*} {mγ : MeasurableSpace γ}
    (κ : Kernel α β) (η : Kernel (α × β) γ) [IsSFiniteKernel κ] [IsSFiniteKernel η] (a : α) :
    (κ ⊗ₖ η) a = (κ a) ⊗ₘ (Kernel.sectR η a) := by
  ext s hs
  simp_rw [Kernel.compProd_apply hs, compProd_apply hs, Kernel.sectR_apply]

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