instIsCondKernel

Mathlib.Probability.Kernel.Disintegration.StandardBorel

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

← MathLib Explorer

English

If κ is finite, then κ.condKernelBorel is a CondKernel.

Русский

Если κ конечное, то κ.condKernelBorel является CondKernel.

LaTeX

$$$κ.\\mathrm{IsCondKernel}\\,κ.condKernelBorel$$$

Lean4

instance instIsCondKernel (κ : Kernel α (γ × Ω)) [IsFiniteKernel κ] : κ.IsCondKernel κ.condKernelBorel where
  disintegrate := by rw [condKernelBorel, compProd_fst_borelMarkovFromReal _ _ (compProd_fst_condKernelReal _)]

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

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

Разделы

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

Аффилиация

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