English
Let f,g: α×β → E be integrable with respect to μ×ν, and let F: E → E' be any function. Then the outer integral of F applied to the inner integral of f+g equals the outer integral of F applied to the sum of the inner integrals of f and g.
Русский
Пусть f,g: α×β → E интегрируемы по мере μ×ν, и пусть F: E → E' — произвольная функция. Тогда внешний интеграл от F применительно к внутреннему интегралу от f+g равен внешнему интегралу от F, применённому к сумме внутренних интегралов 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 addition inside another integral. `F` can be any function. -/
theorem integral_fn_integral_add ⦃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_add h2f h2g]
