English
Let f, g be γ → E; let F: E → E' be a map; if f and g are integrable with respect to the composed kernel (η ∘ κ) at a, then the integral of F of the inner sum equals the integral of F of the sum of inner integrals: ∫x F(∫y (f(y)+g(y)) dηx(y)) dκa = ∫x F(∫y f(y) dηx(y) + ∫y g(y) dηx(y)) dκa.
Русский
Пусть f, g : γ → E; F: E → E'; если f и g интегрируемы относительно композиции η∘κ в точке a, то ∫x F(∫y (f(y)+g(y)) dηx(y)) dκa = ∫x F(∫y f(y) dηx(y) + ∫y g(y) dηx(y)) dκa.
LaTeX
$$$$ \\int x\, F\\left(\\int y\\,(f(y)+g(y))\,d\\eta_x(y)\\right)\\,d\\kappa a \n= \\int x\, F\\left(\\int y\\,f(y)\\,d\\eta_x(y) + \\int y\\,g(y)\\,d\\eta_x(y)\\right)\\,d\\kappa a $$$$
Lean4
theorem integral_fn_integral_add_comp ⦃f g : γ → E⦄ (F : E → E') (hf : Integrable f ((η ∘ₖ κ) a))
(hg : Integrable g ((η ∘ₖ κ) a)) :
∫ x, F (∫ y, f y + g y ∂η x) ∂κ a = ∫ x, F (∫ y, f y ∂η x + ∫ y, g y ∂η x) ∂κ a :=
by
refine integral_congr_ae ?_
filter_upwards [hf.ae_of_comp, hg.ae_of_comp] with _ h2f h2g
simp [integral_add h2f h2g]
