instIsMarkovKernelCondKernelReal

Mathlib.Probability.Kernel.Disintegration.StandardBorel

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

← MathLib Explorer

English

If κ is a finite kernel, then condKernelReal κ is a Markov kernel.

Русский

Если κ — конечное ядро, то condKernelReal κ является марковским ядром.

LaTeX

$$IsMarkovKernel( condKernelReal κ )$$

Lean4

instance instIsMarkovKernelCondKernelReal (κ : Kernel α (γ × ℝ)) [IsFiniteKernel κ] :
    IsMarkovKernel (condKernelReal κ) := by
  rw [condKernelReal]
  infer_instance

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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