comp_apply_univ — Mathlib

English

Composition-Product of kernels: for s-finite kernels κ: α → β and η: β → γ, compProd κ η describes the joint distribution of a pair (b,c) with κ(a,db) and η(a,b,dc). If either kernel is not s-finite, the value is 0.

Русский

compProd κ η задаёт совместное распределение пары (b,c) при условии a: κ(a,db) и η(a,b,dc); если одно из ядер не s-конечное, значение равно 0.

LaTeX

$$$ \text{compProd}(\kappa, \eta) : α \to (β × γ) $ with the defining relation $(\text{compProd } κ η)(a, S) = \int_{β} \int_{γ} 1_S(b,c) \, dη(a,b)(c) \, dκ(a,b)$ (when s-finite).$$

Lean4

@[simp]
theorem comp_apply_univ [IsMarkovKernel κ] : (κ ∘ₘ μ) Set.univ = μ Set.univ := by simp [bind_apply .univ κ.aemeasurable]

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