theorem MathlibNt.Analysis.IntegralExcessCover.majorized_of_excess_cover {α : Type u_1} {ι : Type u_2} [Fintype ι] (G S A : Set α) (E : ι → Set α) (g f : α → ℝ) (e M : ℝ) (he : 0 ≤ e) (hM : 0 ≤ M) (hf0 : ∀ x ∈ S, 0 ≤ f x) (hzero : ∀ x ∉ G, g x = 0) (hinside : G ∩ S ⊆ A) (hlocal : ∀ x ∈ G ∩ S, g x ≤ f x + e) (hcover : ∀ x ∈ G \ S, ∃ (i : ι), x ∈ E i) (hcap : ∀ x ∈ G \ S, g x ≤ M) (x : α) : g x ≤ S.indicator f x + A.indicator (fun (x : α) => e) x + ∑ i : ι, (E i).indicator (fun (x : α) => M) x

Pointwise payment for a finite, possibly overlapping cover of the excess.

theorem MathlibNt.Analysis.IntegralExcessCover.integral_sub_setIntegral_le_of_excess_cover {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] (μ : MeasureTheory.Measure α) (G S A : Set α) (E : ι → Set α) (g f : α → ℝ) (e M : ℝ) (hg : MeasureTheory.Integrable g μ) (hf : MeasureTheory.IntegrableOn f S μ) (hS : MeasurableSet S) (hA : MeasurableSet A) (hAfin : μ A ≠ ⊤) (hE : ∀ (i : ι), MeasurableSet (E i)) (hEfin : ∀ (i : ι), μ (E i) ≠ ⊤) (he : 0 ≤ e) (hM : 0 ≤ M) (hf0 : ∀ x ∈ S, 0 ≤ f x) (hzero : ∀ x ∉ G, g x = 0) (hinside : G ∩ S ⊆ A) (hlocal : ∀ x ∈ G ∩ S, g x ≤ f x + e) (hcover : ∀ x ∈ G \ S, ∃ (i : ι), x ∈ E i) (hcap : ∀ x ∈ G \ S, g x ≤ M) : ∫ (x : α), g x ∂μ - ∫ (x : α) in S, f x ∂μ ≤ μ.real A * e + ∑ i : ι, μ.real (E i) * M

Local error on the common region plus a finite cover of the excess. The cover sets may overlap; neither S ⊆ G nor measurability of G is required. All integrability hypotheses refer to the actual functions being integrated.