comp_apply' — Mathlib

English

For η: kernel β→γ and κ: kernel α→β, and a ∈ α, and measurable set s ⊆ γ, we have (η ∘ₖ κ) a s = ∫⁻ b η(b, s) dκ(a)(b).

Русский

Для ядер η: β→γ и κ: α→β и a ∈ α и измеримого множества s⊆γ выполняется (η ∘ₖ κ) a s = ∫ η(b, s) dκ(a)(b).

LaTeX

$$$(\\eta \\circ_k \\kappa) a s = \\int^{∞}_{b} \\eta(b, s) \\, d\\kappa(a)(b).$$$

Lean4

theorem comp_apply' (η : Kernel β γ) (κ : Kernel α β) (a : α) {s : Set γ} (hs : MeasurableSet s) :
    (η ∘ₖ κ) a s = ∫⁻ b, η b s ∂κ a := by rw [comp_apply, Measure.bind_apply hs (Kernel.aemeasurable _)]

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