instIsProbabilityMeasureProdCompProdOfIsMarkovKernel

English

μ ⊗ₘ κ is a probability measure if μ is a probability measure and κ is a Markov kernel.

Русский

μ ⊗ₘ κ является вероятностной мерой, если μ — вероятностная мера и κ — марковское ядро.

LaTeX

$$$\\text{IsProbabilityMeasure}(\\mu \\otimes_{\\mathrm{m}} \\kappa)$$$

Lean4

instance [IsProbabilityMeasure μ] [IsMarkovKernel κ] : IsProbabilityMeasure (μ ⊗ₘ κ) := by rw [compProd]; infer_instance

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