disintegrate

Mathlib.Probability.Kernel.Disintegration.Basic

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

English

For κ with CondKernel κCond, κ is retrieved as κ = κ.fst ⊗ κCond.

Русский

Для κ с CondKernel κCond ядро восстанавливается как κ = κ.fst ⊗ κCond.

LaTeX

$$$\\kappa = \\kappa_{\\mathrm{fst}} \\otimes_k \\kappa_{\\mathrm{Cond}}$$$

Lean4

theorem disintegrate [κ.IsCondKernel κCond] : κ.fst ⊗ₖ κCond = κ :=
  IsCondKernel.disintegrate

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

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

Разделы

Аффилиация

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