English
For any additive target M, the sum of f over the boxes of split I i x equals the sum of f evaluated on the lower and upper pieces (with empty parts contributing zero).
Русский
Для любой целевой абелевой группы M сумма f по коробкам разбиения split I i x равна сумме f на нижнем и верхнем кусках (пустые части дают ноль).
LaTeX
$$$\\sum_{J \\in (\\mathrm{split}\\ I\\ i\\ x).\\mathrm{boxes}} f(J) = (I.\\mathrm{splitLower}\\ i\\ x).\\mathrm{elim}'\\ 0\\ f + (I.\\mathrm{splitUpper}\\ i\\ x).\\mathrm{elim}'\\ 0\\ f$$$
Lean4
theorem sum_split_boxes {M : Type*} [AddCommMonoid M] (I : Box ι) (i : ι) (x : ℝ) (f : Box ι → M) :
(∑ J ∈ (split I i x).boxes, f J) = (I.splitLower i x).elim' 0 f + (I.splitUpper i x).elim' 0 f := by
classical rw [split, sum_ofWithBot, Finset.sum_pair (I.splitLower_ne_splitUpper i x)]
