Compact cores of measurable exhaustions

An increasing measurable exhaustion which covers a finite-measure set almost everywhere contains a compact core with arbitrarily small discarded mass.

theorem LeanPool.Besicovitch.exists_in_monotone_ae_cover_measure_sdiff_lt {X : Type u_1} [MeasurableSpace X] {mu : MeasureTheory.Measure X} {A : Set X} (hA : MeasurableSet A) (hA_finite : mu A ≠ ⊤) {G : ℕ → Set X} (hG_measurable : ∀ (n : ℕ), MeasurableSet (G n)) (hG_mono : Monotone G) (hcovered : ∀ᵐ (x : X) ∂mu.restrict A, x ∈ ⋃ (n : ℕ), G n) {epsilon : ENNReal} (hepsilon : 0 < epsilon) : ∃ (n : ℕ), mu (A \ G n) < epsilon

A monotone measurable cover has an arbitrarily small exceptional set at a finite stage.

theorem LeanPool.Besicovitch.exists_compact_in_monotone_ae_cover_measure_sdiff_lt {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [T2Space X] {mu : MeasureTheory.Measure X} [mu.InnerRegularCompactLTTop] {A : Set X} (hA : MeasurableSet A) (hA_finite : mu A ≠ ⊤) {G : ℕ → Set X} (hG_measurable : ∀ (n : ℕ), MeasurableSet (G n)) (hG_subset : ∀ (n : ℕ), G n ⊆ A) (hG_mono : Monotone G) (hcovered : ∀ᵐ (x : X) ∂mu.restrict A, x ∈ ⋃ (n : ℕ), G n) {epsilon : ENNReal} (hepsilon : 0 < epsilon) : ∃ (n : ℕ) (F : Set X), IsCompact F ∧ F ⊆ G n ∧ mu (A \ F) < epsilon

An almost-everywhere increasing measurable exhaustion contains a compact core losing less than any prescribed positive mass.

theorem LeanPool.Besicovitch.exists_compact_in_monotone_ae_cover_measure_sdiff_lt_mul {X : Type u_1} [MeasurableSpace X] [TopologicalSpace X] [OpensMeasurableSpace X] [T2Space X] {mu : MeasureTheory.Measure X} [mu.InnerRegularCompactLTTop] {A : Set X} (hA : MeasurableSet A) (hA_pos : 0 < mu A) (hA_finite : mu A ≠ ⊤) {G : ℕ → Set X} (hG_measurable : ∀ (n : ℕ), MeasurableSet (G n)) (hG_subset : ∀ (n : ℕ), G n ⊆ A) (hG_mono : Monotone G) (hcovered : ∀ᵐ (x : X) ∂mu.restrict A, x ∈ ⋃ (n : ℕ), G n) {coefficient : ENNReal} (hcoefficient_pos : 0 < coefficient) (hcoefficient_finite : coefficient ≠ ⊤) : ∃ (n : ℕ) (F : Set X), IsCompact F ∧ F ⊆ G n ∧ mu (A \ F) < coefficient * mu F

The compact core can be chosen so that the discarded mass is a prescribed positive fraction of the retained mass.