lintegral_bind_le — Mathlib

English

The lintegral over the bind operation is bounded above by the iterated lintegral: ∫ f d(bind m μ) ≤ ∫ a ∫ f dμ(a) dm(a).

Русский

Линтеграл по оператору bind не превышает итеративный линтеиграл: ∫ f d(bind m μ) ≤ ∫ a ∫ f dμ(a) dm(a).

LaTeX

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

Lean4

theorem lintegral_bind_le (f : β → ℝ≥0∞) (m : Measure α) (μ : α → Measure β) :
    ∫⁻ x, f x ∂bind m μ ≤ ∫⁻ a, ∫⁻ x, f x ∂μ a ∂m :=
  (lintegral_join_le _ _).trans (lintegral_map_le _ _)

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