English
If f is integrable on I, then the map J ↦ integral J l f vol is box-additive on subboxes of I.
Русский
Если f интегрируема на I, то отображение J ↦ интеграл J по l f vol является аддитивной по подящикам I.
LaTeX
$$$$\\text{toBoxAdditive}(h) : ι \\to^b^a I\\, F,$$$$
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.sum_integral_congr` for an unbundled version. -/
@[simps]
def toBoxAdditive (h : Integrable I l f vol) : ι →ᵇᵃ[I] F
where
toFun J := integral J l f vol
sum_partition_boxes' J hJ π
hπ := by
replace hπ := hπ.iUnion_eq; rw [← Prepartition.iUnion_top] at hπ
rw [(h.to_subbox (WithTop.coe_le_coe.1 hJ)).sum_integral_congr hπ, Prepartition.top_boxes, sum_singleton]
