English
Difference of two integral sums equals a sum over the intersection partition of their tags, of the difference of the corresponding partial integrals.
Русский
Разность двух сумм интеграла равна сумме по пересеченному разбиению разниц частичных интегралов.
LaTeX
$$$\forall π_1,π_2:\; π_1.IsPartition \land π_2.IsPartition \Rightarrow \mathrm{integralSum}(f,vol,π_1) - \mathrm{integralSum}(f,vol,π_2) = \sum_{J \in (π_1.toPrepartition \cap π_2.toPrepartition).boxes} (vol J (f (π_1.infPrepartition π_2.toPrepartition).tag J) - vol J (f (π_2.infPrepartition π_1.toPrepartition).tag J))$$$
Lean4
theorem integralSum_fiberwise {α} (g : Box ι → α) (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) (π : TaggedPrepartition I) :
(∑ y ∈ π.boxes.image g, integralSum f vol (π.filter (g · = y))) = integralSum f vol π :=
π.sum_fiberwise g fun J => vol J (f <| π.tag J)
