lintegral_prod_of_measurable — Mathlib

English

If f: α×β → ENNReal is measurable, then the product integral equals the iterated integral.

Русский

Если f измеримо, то интеграл по произведению равен итерационному интегралу.

LaTeX

$$$\int f \, d(\mu \times \nu) = \int \! \! \! \int f(x,y) \, d\nu \, d\mu$$$

Lean4

/-- **Tonelli's Theorem**: For `ℝ≥0∞`-valued measurable functions on `α × β`,
  the integral of `f` is equal to the iterated integral. -/
@[deprecated lintegral_prod (since := "2025-04-06")]
theorem lintegral_prod_of_measurable (f : α × β → ℝ≥0∞) (hf : Measurable f) :
    ∫⁻ z, f z ∂μ.prod ν = ∫⁻ x, ∫⁻ y, f (x, y) ∂ν ∂μ :=
  lintegral_prod f hf.aemeasurable

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