compProd_posterior_eq_swap_comp

Mathlib.Probability.Kernel.Posterior

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

English

A balanced equality expresses how swap interacts with compProd and posterior.

Русский

Балансированное равенство выражает взаимодействие swap с compProd и posterior.

LaTeX

$$$(κ ∘ μ) ⊗ κ†μ = μ ⊗ κ$$$

Lean4

theorem compProd_posterior_eq_swap_comp : (κ ∘ₘ μ) ⊗ₘ κ†μ = Kernel.swap Ω 𝓧 ∘ₘ μ ⊗ₘ κ := by
  rw [compProd_posterior_eq_map_swap, Measure.swap_comp]

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

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

Разделы

Аффилиация

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