lintegral_bind — Mathlib

English

If μ is AEMeasurable with respect to m and f is AEMeasurable with respect to bind m μ, then the lintegral with respect to bind m μ of f equals the iterated lintegral.

Русский

Если μ измеримо почти наверняка относительно m, а f измеримо относительно bind m μ, то линтеграль равен итеративному интегралу.

LaTeX

$$$\\int\\!^{-} x\, f(x) \\partial(\\operatorname{bind} m \\mu) = \\int^{a}\\!\\int^{x}\\! f(x) \\partial \\mu(a) \\partial m$$$

Lean4

theorem lintegral_bind {m : Measure α} {μ : α → Measure β} {f : β → ℝ≥0∞} (hμ : AEMeasurable μ m)
    (hf : AEMeasurable f (bind m μ)) : ∫⁻ x, f x ∂bind m μ = ∫⁻ a, ∫⁻ x, f x ∂μ a ∂m :=
  (lintegral_join hf).trans (lintegral_map' (aemeasurable_lintegral hf) hμ)

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