disintegrate — Mathlib

English

Let ρ be a measure on α × Ω and ρCond a kernel α → Ω such that ρ is a CondKernel with respect to ρCond. Then ρ can be decomposed as the product of its α-marginal with the conditional kernel: ρ = ρ.fst ⊗ₘ ρCond.

Русский

Пусть ρ — мера на α × Ω, а ρCond — ядро α → Ω так, что ρ является условной (CondKernel) по отношению к ρCond. Тогда ρ распадается как произведение его границы по α с условным ядром: ρ = ρ.fst ⊗ₘ ρCond.

LaTeX

$$$\\rho = \\rho_{\\mathrm{fst}} \\otimes_m \\rho_{\\mathrm{Cond}}.$$$

Lean4

theorem disintegrate : ρ.fst ⊗ₘ ρCond = ρ :=
  IsCondKernel.disintegrate

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