integral_integral — Mathlib

English

If f: α×β → E is integrable with respect to μ×ν, then the integral over μ×ν equals the iterated integral with the variables swapped.

Русский

Если f: α×β → E интегрируема по μ×ν, то интеграл по μ×ν равен итерационному интегралу после перестановки переменных.

LaTeX

$$$$\\int_{α×β} f(x,y) \\, dμ×ν = \\int_{β} \\int_{α} f(x,y) \\, dμ(x) \\, dν(y).$$$$

Lean4

/-- Reversed version of **Fubini's Theorem**. -/
theorem integral_integral {f : α → β → E} (hf : Integrable (uncurry f) (μ.prod ν)) :
    ∫ x, ∫ y, f x y ∂ν ∂μ = ∫ z, f z.1 z.2 ∂μ.prod ν :=
  (integral_prod _ hf).symm

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