lintegral_swapLeft

Mathlib.Probability.Kernel.Composition.MapComap

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

← MathLib Explorer

English

If κ is a Markov kernel, then swapLeft κ is Markov.

Русский

Если κ — ядро Маркова, то swapLeft κ — ядро Маркова.

LaTeX

$$$\text{If } \kappa \text{ is Markov, then } \mathrm{swapLeft}(\kappa) \text{ is Markov.}$$$

Lean4

theorem lintegral_swapLeft (κ : Kernel (α × β) γ) (a : β × α) (g : γ → ℝ≥0∞) :
    ∫⁻ c, g c ∂swapLeft κ a = ∫⁻ c, g c ∂κ a.swap := by rw [swapLeft_apply]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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