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