English
Let f,g: α×β → E be integrable with respect to μ×ν, and F: E → ℝ≥0∞ any function. Then the lower integral of F applied to ∫(f−g) equals the lower integral of F applied to (∫ f) − (∫ g).
Русский
Пусть f,g: α×β → E интегрируемы по μ×ν, и F: E → ℝ≥0∞ произвольная функция. Тогда линеграл от F применительно к ∫(f−g) равен линегралу от F применительно к (∫ f) − (∫ g).
LaTeX
$$$$\\int\\!\\!\\int_{α}^{-} F\\left(\\int_{β} (f(x,y) - g(x,y)) \\; dν(y)\\right) dμ(x) \\\\;=\\\\ \\int_{α}^{-} F\\left(\\left(\\int_{β} f(x,y)\\; dν(y)\\right) - \\left(\\int_{β} g(x,y)\\; dν(y)\\right)\\right) dμ(x).$$$$
Lean4
/-- Integrals commute with subtraction inside a lower Lebesgue integral.
`F` can be any function. -/
theorem lintegral_fn_integral_sub ⦃f g : α × β → E⦄ (F : E → ℝ≥0∞) (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 lintegral_congr_ae ?_
filter_upwards [hf.prod_right_ae, hg.prod_right_ae] with _ h2f h2g
simp [integral_sub h2f h2g]
