instIsProbabilityMeasureBindCoeKernelOfIsMarkovKernel

English

If μ is a probability measure on α and κ is a Markov kernel α → β, then the composition μ ∘ₘ κ is a probability measure on α × β.

Русский

Если μ — распределение вероятности на α, а κ — марковское ядро α → β, тогда композиция μ ∘ₘ κ является распределением вероятности на α × β.

LaTeX

$$$[ \\text{IsProbabilityMeasure } \\mu] \\land [ \\text{IsMarkovKernel } \\kappa] \\\\Rightarrow \\text{IsProbabilityMeasure}( \\mu \\bind (\\kappa) )$$$

Lean4

instance [IsProbabilityMeasure μ] [IsMarkovKernel κ] : IsProbabilityMeasure (κ ∘ₘ μ) := by rw [← snd_compProd];
  infer_instance

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