condKernel

Mathlib.Probability.Kernel.Disintegration.StandardBorel

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.condKernel

Lean4

/-- Conditional kernel of a measure on a product space: a Markov kernel such that
`ρ = ρ.fst ⊗ₘ ρ.condKernel` (see `MeasureTheory.Measure.compProd_fst_condKernel`). -/
noncomputable def _root_.MeasureTheory.Measure.condKernel :=
  val_proj @wrapped✝.{}

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

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

Разделы

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

Аффилиация

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