English
The integral sum over a biUnion of tagged partitions is the sum of the integral sums over each tag.
Русский
Сумма интеграла по би-объединению тегированных разбиений равна сумме интегралов по каждому тегу.
LaTeX
$$$\forall f\; (π: I) (πi: \forall J, TaggedPrepartition J)\Rightarrow \mathrm{integralSum} f vol (π.biUnionTagged πi) = \sum_{J \in π.boxes} \mathrm{integralSum} f vol (πi J)$$$
Lean4
theorem integralSum_biUnion_partition (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) (π : TaggedPrepartition I)
(πi : ∀ J, Prepartition J) (hπi : ∀ J ∈ π, (πi J).IsPartition) :
integralSum f vol (π.biUnionPrepartition πi) = integralSum f vol π :=
by
refine (π.sum_biUnion_boxes _ _).trans (sum_congr rfl fun J hJ => ?_)
calc
(∑ J' ∈ (πi J).boxes, vol J' (f (π.tag <| π.toPrepartition.biUnionIndex πi J'))) =
∑ J' ∈ (πi J).boxes, vol J' (f (π.tag J)) :=
sum_congr rfl fun J' hJ' => by rw [Prepartition.biUnionIndex_of_mem _ hJ hJ']
_ = vol J (f (π.tag J)) :=
(vol.map ⟨⟨fun g : E →L[ℝ] F => g (f (π.tag J)), rfl⟩, fun _ _ => rfl⟩).sum_partition_boxes le_top (hπi J hJ)
