English
If μ is either the zero measure or a probability measure and κ is a Markov kernel, then the composition κ ∘ₘ μ is either the zero measure or a probability measure.
Русский
Если μ равномерно нулевой мерой или вероятностной мерой, а κ — марковское ядро, то композиция κ ∘ₘ μ либо нулевая мера, либо вероятность.
LaTeX
$$$[ \\text{IsZeroOrProbabilityMeasure } \\mu] \\land [ \\text{IsZeroOrMarkovKernel } \\kappa] \\\\Rightarrow \\text{IsZeroOrProbabilityMeasure}( \\mu \\bind (\\kappa) )$$$
Lean4
instance [IsZeroOrProbabilityMeasure μ] [IsZeroOrMarkovKernel κ] : IsZeroOrProbabilityMeasure (κ ∘ₘ μ) := by
rw [← snd_compProd]; infer_instance
