English
Let f,g: α×β → E be integrable with respect to μ×ν, and F: E → E' any function. Then the outer integral of F applied to the inner integral of f−g equals the outer integral of F applied to (∫ f) − (∫ g).
Русский
Пусть f,g: α×β → E интегрируемы по μ×ν, и F: E → E' произвольная функция. Тогда внешний интеграл от F applied to inner integral of f−g равен внешнему интегралу от F applied к (∫ f) − (∫ g).
LaTeX
$$$$\\int_\\alpha F\\left(\\int_\\beta (f(x,y) - g(x,y))\\, d\\nu(y)\\right) \\, d\\mu(x) \\\\;=\\\\ \\int_\\alpha F\\left(\\left(\\int_\\beta f(x,y)\\, d\\nu(y)\\right) - \\left(\\int_\\beta g(x,y)\\, d\\nu(y)\\right)\\right) \\, d\\mu(x).$$$$
Lean4
/-- Integrals commute with subtraction inside another integral.
`F` can be any measurable function. -/
theorem integral_fn_integral_sub ⦃f g : α × β → E⦄ (F : E → E') (hf : Integrable f (μ.prod ν))
(hg : Integrable g (μ.prod ν)) :
(∫ x, F (∫ y, f (x, y) - g (x, y) ∂ν) ∂μ) = ∫ x, F ((∫ y, f (x, y) ∂ν) - ∫ y, g (x, y) ∂ν) ∂μ :=
by
refine integral_congr_ae ?_
filter_upwards [hf.prod_right_ae, hg.prod_right_ae] with _ h2f h2g
simp [integral_sub h2f h2g]
