English
The fiberwise version expresses that the fiberwise sums equal the global sum when grouping by a function g.
Русский
Фиберной версией выражается равенство сумм, получаемых фиберизацией, с суммой по всему множеству.
LaTeX
$$$\forall g,f,π:\; (π.image g).sum (\lambda y, integralSum f vol (π.filter (g = y))) = integralSum f vol π$$$
Lean4
theorem integralSum_sub_partitions (f : ℝⁿ → E) (vol : ι →ᵇᵃ E →L[ℝ] F) {π₁ π₂ : TaggedPrepartition I}
(h₁ : π₁.IsPartition) (h₂ : π₂.IsPartition) :
integralSum f vol π₁ - integralSum f vol π₂ =
∑ J ∈ (π₁.toPrepartition ⊓ π₂.toPrepartition).boxes,
(vol J (f <| (π₁.infPrepartition π₂.toPrepartition).tag J) -
vol J (f <| (π₂.infPrepartition π₁.toPrepartition).tag J)) :=
by
rw [← integralSum_inf_partition f vol π₁ h₂, ← integralSum_inf_partition f vol π₂ h₁, integralSum, integralSum,
Finset.sum_sub_distrib]
simp only [infPrepartition_toPrepartition, inf_comm]
