English
Let f: α → ℝ≥0∞ and g: β → ℝ≥0∞ be AEMeasurable. Then the product integral equals product of separate integrals: ∫⁻ z f(z.1) g(z.2) d(μ×ν) = (∫⁻ x f(x) dμ) (∫⁻ y g(y) dν).
Русский
Пусть f: α → ℝ≥0∞ и g: β → ℝ≥0∞ измеримы. Тогда интеграл от произведения функций по произведению меры равен произведению отдельных интегралов: ∫⁻ f(x)g(y) dμ×ν = (∫⁻ f dμ)(∫⁻ g dν).
LaTeX
$$$$\\iint f(x) g(y) \\, d(\\mu\\times\\nu) = \\left(\\iint f(x) \\, d\\mu\\right) \\left(\\iint g(y) \\, d\\nu\\right)$$$$
Lean4
theorem lintegral_prod_mul {f : α → ℝ≥0∞} {g : β → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g ν) :
∫⁻ z, f z.1 * g z.2 ∂μ.prod ν = (∫⁻ x, f x ∂μ) * ∫⁻ y, g y ∂ν :=
by
rw [lintegral_prod _ (by fun_prop)]
simp [lintegral_lintegral_mul hf hg]
