integral_integral_swap — Mathlib

English

Let f,g: α×β → E be integrable with respect to μ×ν. Then the double integral of (f − g) equals the double integral of f minus the double integral of g, i.e., the previous rule stated with (f − g) on the left.

Русский

Пусть f,g: α×β → E интегрируемы по μ×ν. Тогда двойной интеграл от (f − g) равен двойному интегралу от f минус двойной интеграл от g.

LaTeX

$$$$\\int\\int (f(x,y) - g(x,y)) \\, dν \\, dμ = \\int\\int f(x,y) \\, dν \\, dμ - \\int\\int g(x,y) \\, dν \\, dμ.$$$$

Lean4

/-- Change the order of Bochner integration. -/
theorem integral_integral_swap ⦃f : α → β → E⦄ (hf : Integrable (uncurry f) (μ.prod ν)) :
    ∫ x, ∫ y, f x y ∂ν ∂μ = ∫ y, ∫ x, f x y ∂μ ∂ν :=
  (integral_integral hf).trans (integral_prod_symm _ hf)

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