integral_integral_sub' — Mathlib

English

For integrable f: α×β → E with respect to μ×ν, the Bochner integral over μ×ν equals the iterated integral ∫x ∫y f(x,y).

Русский

Пусть f: α×β → E интегрируема по μ×ν. Тогда интеграл по μ×ν равен итерационному интегралу ∫x ∫y f(x,y).

LaTeX

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

Lean4

/-- Double integrals commute with subtraction. This is the version with `(f - g) (x, y)`
  (instead of `f (x, y) - g (x, y)`) in the LHS. -/
theorem integral_integral_sub' ⦃f g : α × β → E⦄ (hf : Integrable f (μ.prod ν)) (hg : Integrable g (μ.prod ν)) :
    (∫ x, ∫ y, (f - g) (x, y) ∂ν ∂μ) = (∫ x, ∫ y, f (x, y) ∂ν ∂μ) - ∫ x, ∫ y, g (x, y) ∂ν ∂μ :=
  integral_integral_sub hf hg

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