compProd — Mathlib

English

If κ is a Markov kernel and η is a Markov kernel, then their product κ ⊗ η is also a Markov kernel.

Русский

Если κ и η — марковские ядра, то их произведение κ ⊗ η тоже является марковским ядром.

LaTeX

$$$$ \\text{IsMarkovKernel}(κ) \\land \\text{IsMarkovKernel}(η) \\implies \\text{IsMarkovKernel}(κ \\otimes_{\\kern-0.2em} η). $$$$

Lean4

instance compProd (κ : Kernel α β) [IsMarkovKernel κ] (η : Kernel (α × β) γ) [IsMarkovKernel η] :
    IsMarkovKernel (κ ⊗ₖ η) where isProbabilityMeasure a := ⟨by simp [compProd_apply]⟩

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