Integrals over finite covers

The integral over a set covered by finitely many measurable pieces is bounded by the sum of the piece integrals for nonnegative functions.

theorem ESS.uc_integral_le_sum_of_finite_cover (f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hf : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), 0 ≤ f z) (S : Set CKN.Foundation.Parabolic.ParabolicPoint) (G : Finset CKN.Foundation.Parabolic.Vec3) (T : CKN.Foundation.Parabolic.Vec3 → Set CKN.Foundation.Parabolic.ParabolicPoint) (hcover : S ⊆ ⋃ c ∈ G, T c) (hSInt : MeasureTheory.IntegrableOn f S MeasureTheory.volume) (hTInt : ∀ c ∈ G, MeasureTheory.IntegrableOn f (T c) MeasureTheory.volume) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, f z ≤ ∑ c ∈ G, ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in T c, f z

A finite cover bounds a nonnegative real integral by the sum of its covering integrals.