English
Let f: α → β → ℝ≥0∞ be AEMeasurable with respect to μ × ν. Then the reversed order of integration holds: ∫⁻ x ∫⁻ y f(x,y) dν dμ = ∫⁻ z f(z.1, z.2) d(μ × ν).
Русский
Пусть f: α → β → ℝ≥0∞ измерима в отношении μ × ν. Тогда обратный порядок интегрирования: ∫⁻_x ∫⁻_y f(x,y) dν dμ = ∫⁻_{(x,y)} f(x,y) d(μ × ν).
LaTeX
$$$$\\int^{\\infty}_{x} \\int^{\\infty}_{y} f(x,y) \\, d\\nu(y) \\, d\\mu(x) = \\int^{\\infty}_{(x,y)\\in α×β} f(x,y) \\, d(\\mu\\times\\nu)$$$$
Lean4
/-- The reversed version of **Tonelli's Theorem**. In this version `f` is in curried form, which
makes it easier for the elaborator to figure out `f` automatically. -/
theorem lintegral_lintegral ⦃f : α → β → ℝ≥0∞⦄ (hf : AEMeasurable (uncurry f) (μ.prod ν)) :
∫⁻ x, ∫⁻ y, f x y ∂ν ∂μ = ∫⁻ z, f z.1 z.2 ∂μ.prod ν :=
(lintegral_prod _ hf).symm
