instIsMarkovKernelCondKernelUnitBorel

Mathlib.Probability.Kernel.Disintegration.StandardBorel

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Kernel.instIsMarkovKernelCondKernelUnitBorel

English

For κ : Kernel Unit (Prod α Ω) finite, the conditional kernel condKernelUnitBorel is Markov.

Русский

Для κ: Kernel Unit (Prod α Ω) конечного типа условное ядро condKernelUnitBorel является ядром Маркова.

LaTeX

$$$IsMarkovKernel(κ.condKernelUnitBorel)$$$

Lean4

instance instIsMarkovKernelCondKernelUnitBorel : IsMarkovKernel κ.condKernelUnitBorel :=
  by
  rw [condKernelUnitBorel]
  infer_instance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru