instIsMarkovKernelBoolBoolKernelOfIsProbabilityMeasure

English

If μ and ν are probability measures, then the kernel boolKernel μ ν is a Markov kernel.

Русский

Если μ и ν – вероятностные меры, то ядро boolKernel μ ν является марковским ядром.

LaTeX

$$$\\text{boolKernel } μ ν \\text{ is a Markov Kernel}$$$

Lean4

instance [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] : IsMarkovKernel (boolKernel μ ν) where
  isProbabilityMeasure
    b := by cases b <;> simp only [boolKernel_apply, Bool.false_eq_true, ↓reduceIte] <;> infer_instance

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