instIsMarkovKernelCondDistrib

Mathlib.Probability.Kernel.CondDistrib

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.instIsMarkovKernelCondDistrib

English

The conditional distribution condDistrib Y X μ is a Markov kernel.

Русский

Условное распределение condDistrib Y X μ является марковским ядром.

LaTeX

$$$$\\mathrm{condDistrib}(Y,X,\\mu) \\text{ является марковским ядром}.$$$$

Lean4

instance [MeasurableSpace β] : IsMarkovKernel (condDistrib Y X μ) := by rw [condDistrib]; infer_instance

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

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

Разделы

Аффилиация

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