lintegral_comp — Mathlib

English

For kernels η and κ, and a ∈ α, and measurable g, the lintegral over the composition equals the iterated lintegral: ∫ g d(η ∘ κ) a = ∫ ∫ g dη b dκ a.

Русский

Для ядер η и κ, и a ∈ α, и измеримой функции g, линегральная интеграция по композициим равна двойной интеграции: ∫ g d(η ∘ κ) a = ∫ ∫ g dη b dκ a.

LaTeX

$$$\\int^{\\infty} g\\; d(\\eta \\circ_k \\kappa) a = \\int^{\\infty} b \\; \\left(\\int^{\\infty} g c \\, d\\eta b(c)\\right) d\\kappa(a)(b).$$$

Lean4

theorem lintegral_comp (η : Kernel β γ) (κ : Kernel α β) (a : α) {g : γ → ℝ≥0∞} (hg : Measurable g) :
    ∫⁻ c, g c ∂(η ∘ₖ κ) a = ∫⁻ b, ∫⁻ c, g c ∂η b ∂κ a := by
  rw [comp_apply, Measure.lintegral_bind (Kernel.aemeasurable _) hg.aemeasurable]

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