swap_comp

Mathlib.Probability.Kernel.Composition.CompNotation

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

English

The swap operation is an involution on kernels: (swap α β) ∘ₖ (swap β α) = Kernel.id.

Русский

Операция свап является инволюцией на ядрах: (swap α β) ∘ₖ (swap β α) = Kernel.id.

LaTeX

$$$ (\text{swap } α β) \circ_K (\text{swap } β α) = \text{Kernel.id} $$$

Lean4

theorem swap_comp {μ : Measure (α × β)} : (Kernel.swap α β) ∘ₘ μ = μ.map Prod.swap :=
  deterministic_comp_eq_map measurable_swap

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

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

Разделы

Аффилиация

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