lintegral_lintegral_swap — Mathlib

English

Change the order of Lebesgue integration for nonnegative functions: ∫⁻ x ∫⁻ y f(x,y) dν dμ = ∫⁻ y ∫⁻ x f(x,y) dμ dν.

Русский

Поменять порядок лебесгового интегрирования для неотрицательных функций: ∫⁻_x ∫⁻_y f(x,y) dν dμ = ∫⁻_y ∫⁻_x f(x,y) dμ dν.

LaTeX

$$$$\\int^{\\infty}_x \\int^{\\infty}_y f(x,y) \\, d\\nu(y) \\, d\\mu(x) = \\int^{\\infty}_y \\int^{\\infty}_x f(x,y) \\, d\\mu(x) \\, d\\nu(y)$$$$

Lean4

/-- Change the order of Lebesgue integration. -/
theorem lintegral_lintegral_swap [SFinite μ] ⦃f : α → β → ℝ≥0∞⦄ (hf : AEMeasurable (uncurry f) (μ.prod ν)) :
    ∫⁻ x, ∫⁻ y, f x y ∂ν ∂μ = ∫⁻ y, ∫⁻ x, f x y ∂μ ∂ν :=
  (lintegral_lintegral hf).trans (lintegral_prod_symm _ hf)

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