Finite-cover loss estimates using subadditivity, allowing overlapping local patches.
theorem
KamProject.Arnold1963.measure_complement_finite_union_lt
{E : Type u_1}
{ι : Type u_2}
[MeasurableSpace E]
[Fintype ι]
(μ : MeasureTheory.Measure E)
(F : Set E)
(P K : ι → Set E)
{ε η κ : ℝ}
(hε : 0 ≤ ε)
(hη : 0 ≤ η)
(hfin : μ F ≠ ⊤)
(hcover : μ (F \ ⋃ (i : ι), P i) < ENNReal.ofReal ε * μ F)
(hloss : ∀ (i : ι), μ (P i \ K i) ≤ ENNReal.ofReal η * μ F)
(hbudget : ε + ↑(Fintype.card ι) * η ≤ κ)
: