English
If f is integrable on I, and π₁, π₂ are prepartitions with the same iUnion, then the sums of integrals over their boxes are equal.
Русский
Если f интегрируема на I, и π₁, π₂ — предразбиения с одинаковым iUnion, то суммы интегралов по их коробкам совпадают.
LaTeX
$$$$\\sum_{J\\in π_1.boxes} \\operatorname{integral} J l f vol = \\sum_{J\\in π_2.boxes} \\operatorname{integral} J l f vol,$$$$
Lean4
/-- If `f` is integrable on `I`, then `fun J ↦ integral J l f vol` is box-additive on subboxes of
`I`: if `π₁`, `π₂` are two prepartitions of `I` covering the same part of `I`, the sum of integrals
of `f` over the boxes of `π₁` is equal to the sum of integrals of `f` over the boxes of `π₂`.
See also `BoxIntegral.Integrable.toBoxAdditive` for a bundled version. -/
theorem sum_integral_congr (h : Integrable I l f vol) {π₁ π₂ : Prepartition I} (hU : π₁.iUnion = π₂.iUnion) :
∑ J ∈ π₁.boxes, integral J l f vol = ∑ J ∈ π₂.boxes, integral J l f vol :=
by
refine tendsto_nhds_unique (h.tendsto_integralSum_sum_integral π₁) ?_
rw [l.toFilteriUnion_congr _ hU]
exact h.tendsto_integralSum_sum_integral π₂
