comp_assoc

Mathlib.Probability.Kernel.Composition.MeasureComp

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

English

If κ satisfies IsMarkovKernel, then sectR a is Markov for any a.

Русский

Если κ является ядром Маркова, то секR a также является ядром Маркова для любого a.

LaTeX

$$IsMarkovKernel κ ⇒ IsMarkovKernel (κ.sectR a)$$

Lean4

theorem comp_assoc {η : Kernel β γ} : η ∘ₘ (κ ∘ₘ μ) = (η ∘ₖ κ) ∘ₘ μ :=
  Measure.bind_bind κ.aemeasurable η.aemeasurable

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

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

Разделы

Аффилиация

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