lintegral_prod_symm' — Mathlib

English

Tonelli's theorem in symmetric form: the integral of f over μ×ν equals the iterated integral with the order swapped.

Русский

Теорема Тонелли в симметрической форме: интеграл по μ×ν равен итерационному интегралу с измененным порядком.

LaTeX

$$∫ f d(μ×ν) = ∫ ∫ f(x,y) dν dμ$$

Lean4

/-- The symmetric version of Tonelli's Theorem: For `ℝ≥0∞`-valued measurable
functions on `α × β`, the integral of `f` is equal to the iterated integral, in reverse order. -/
theorem lintegral_prod_symm' [SFinite μ] (f : α × β → ℝ≥0∞) (hf : Measurable f) :
    ∫⁻ z, f z ∂μ.prod ν = ∫⁻ y, ∫⁻ x, f (x, y) ∂μ ∂ν :=
  lintegral_prod_symm f hf.aemeasurable

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