English
Let f and g be real-valued vector-valued functions on the index set; for any partition π of the box I and any volume map vol, the integral sum is linear in the integrand: integralSum(f + g) = integralSum(f) + integralSum(g).
Русский
Пусть f и g — векторнозначные функции; для любой разбиения π коробки I и объёма vol сумма интеграла линейна по интегранту: integralSum(f + g) = integralSum(f) + integralSum(g).
LaTeX
$$$\mathrm{integralSum}(f+g)\;\mathrm{vol}\;\pi = \mathrm{integralSum}(f)\;\mathrm{vol}\;\pi + \mathrm{integralSum}(g)\;\mathrm{vol}\;\pi$$$
Lean4
@[simp]
theorem integralSum_add (f g : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) (π : TaggedPrepartition I) :
integralSum (f + g) vol π = integralSum f vol π + integralSum g vol π := by
simp only [integralSum, Pi.add_apply, (vol _).map_add, Finset.sum_add_distrib]
