lintegral_prod_le — Mathlib

English

For any f: α×β → ENNReal, the product integral is bounded above by the iterated integral of f.

Русский

Для любой f: α×β → ENNReal интеграл по произведению не превосходит итерационного интеграла от f.

LaTeX

$$MeasureTheory.lintegral_prod_le (f) : ∫ f d(μ × ν) ≤ ∫ ∫ f dν dμ$$

Lean4

theorem lintegral_prod_le (f : α × β → ℝ≥0∞) : ∫⁻ z, f z ∂μ.prod ν ≤ ∫⁻ x, ∫⁻ y, f (x, y) ∂ν ∂μ :=
  by
  rw [Measure.prod]
  exact (lintegral_bind_le _ _ _).trans <| lintegral_mono fun a ↦ lintegral_map_le _ _

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