English
Let f be a nonnegative measurable function on s × t with respect to μ × ν. Then the integral over s × t equals the iterated integral with the order swapped: ∫_{s×t} f d(μ×ν) = ∫_{t} [∫_{s} f(x,y) dμ(x) ] dν(y).
Русский
Пусть f≥0 измерима на s × t относительно μ × ν. Тогда интеграл по s × t равен поочередному интегралу: ∫_{s×t} f d(μ×ν) = ∫_{t} [∫_{s} f(x,y) dμ(x) ] dν(y).
LaTeX
$$$\\displaystyle \\iint_{s\\times t} f(x,y) \\, d(\\mu\\times\\nu) \\\\quad=\\\\\\int_{t} \\left( \\int_{s} f(x,y) \\, d\\mu(x) \\right) d\\nu(y)$$$
Lean4
/-- The symmetric version of Tonelli's Theorem for set integrals: For `ℝ≥0∞`-valued almost
everywhere measurable functions on `s ×ˢ t`, the integral of `f` on `s ×ˢ t` is equal to the
iterated integral on `t` and `s` respectively. -/
theorem setLIntegral_prod_symm [SFinite μ] {s : Set α} {t : Set β} (f : α × β → ℝ≥0∞)
(hf : AEMeasurable f ((μ.prod ν).restrict (s ×ˢ t))) :
∫⁻ z in s ×ˢ t, f z ∂μ.prod ν = ∫⁻ y in t, ∫⁻ x in s, f (x, y) ∂μ ∂ν :=
by
rw [← Measure.prod_restrict, ← lintegral_prod_swap, Measure.prod_restrict, setLIntegral_prod]
· rfl
· refine AEMeasurable.comp_measurable ?_ measurable_swap
convert hf
rw [← Measure.prod_restrict, Measure.prod_swap, Measure.prod_restrict]
