instIsMarkovKernelCondKernelBorel

English

If η is a Markov kernel, then the constructed borelMarkovFromReal Ω η is Markov.

Русский

Если η является ядром Маркова, то построенное borelMarkovFromReal Ω η является ядром Маркова.

LaTeX

$$$IsMarkovKernel(\\mathrm{borelMarkovFromReal}\\,Ω\\,η)$$$

Lean4

instance instIsMarkovKernelCondKernelBorel (κ : Kernel α (γ × Ω)) [IsFiniteKernel κ] :
    IsMarkovKernel (condKernelBorel κ) := by
  rw [condKernelBorel]
  infer_instance

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