instIsSFiniteKernelBoolBoolKernelOfSFinite

English

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

Русский

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

LaTeX

$$$\\text{IsMarkovKernel}(\\text{boolKernel}(\\mu, \\nu))$$$

Lean4

instance [SFinite μ] [SFinite ν] : IsSFiniteKernel (boolKernel μ ν) where
  tsum_finite :=
    by
    refine ⟨fun n ↦ boolKernel (sfiniteSeq μ n) (sfiniteSeq ν n), fun n ↦ inferInstance, ?_⟩
    ext b
    rw [Kernel.sum_apply]
    cases b <;> simp [sum_sfiniteSeq]

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