Integrals over countable covers

For nonnegative integrands, a summable family of covering integrals controls the integral on the covered set.

theorem ESS.uc_integral_le_tsum_of_cover (f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hf : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), 0 ≤ f z) (S : Set CKN.Foundation.Parabolic.ParabolicPoint) (Sₙ : ℕ → Set CKN.Foundation.Parabolic.ParabolicPoint) (hcover : S ⊆ ⋃ (n : ℕ), Sₙ n) (hSInt : MeasureTheory.IntegrableOn f S MeasureTheory.volume) (hSnInt : ∀ (n : ℕ), MeasureTheory.IntegrableOn f (Sₙ n) MeasureTheory.volume) (hsum : Summable fun (n : ℕ) => ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in Sₙ n, f z) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, f z ≤ ∑' (n : ℕ), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in Sₙ n, f z

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