Compact uniform-density pieces

An almost-everywhere strict lower-density bound can be made uniform on a compact subset, while losing arbitrarily little Hausdorff measure.

theorem LeanPool.Besicovitch.monotone_uniformDensitySet (mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))) (A : Set (EuclideanSpace ℝ (Fin 2))) (gamma : ℝ) : Monotone fun (m : ℕ) => uniformDensitySet mu A gamma m

Increasing the scale index only weakens the defining radius restriction.

theorem LeanPool.Besicovitch.uniformDensitySet_mono_level {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} {A : Set (EuclideanSpace ℝ (Fin 2))} {beta gamma : ℝ} {m : ℕ} (hbeta_gamma : beta ≤ gamma) : uniformDensitySet mu A gamma m ⊆ uniformDensitySet mu A beta m

Lowering the density level enlarges a uniform density set.

theorem LeanPool.Besicovitch.exists_mem_diagonal_uniformDensitySet_of_lt_lowerOneDensity {A : Set (EuclideanSpace ℝ (Fin 2))} {x : EuclideanSpace ℝ (Fin 2)} {sigma : ℝ} (hx : x ∈ A) (hsigma : 0 ≤ sigma) (hdensity : ENNReal.ofReal sigma < lowerOneDensity A x) : ∃ (n : ℕ), x ∈ uniformDensitySet ((MeasureTheory.Measure.hausdorffMeasure 1).restrict A) A (sigma + 1 / (↑n + 1)) n

A point strictly above level sigma belongs to the diagonal uniform-density exhaustion.

theorem LeanPool.Besicovitch.ae_mem_iUnion_uniformDensitySet {A : Set (EuclideanSpace ℝ (Fin 2))} (hA : MeasurableSet A) {gamma : ℝ} (hgamma : 0 ≤ gamma) (hdensity : ∀ᵐ (x : EuclideanSpace ℝ (Fin 2)) ∂(MeasureTheory.Measure.hausdorffMeasure 1).restrict A, ENNReal.ofReal gamma < lowerOneDensity A x) : ∀ᵐ (x : EuclideanSpace ℝ (Fin 2)) ∂(MeasureTheory.Measure.hausdorffMeasure 1).restrict A, x ∈ ⋃ (m : ℕ), uniformDensitySet ((MeasureTheory.Measure.hausdorffMeasure 1).restrict A) A gamma m

Almost every point lies in a uniform-density set when its lower density exceeds the level.

theorem LeanPool.Besicovitch.exists_uniformDensitySet_measure_sdiff_lt {A : Set (EuclideanSpace ℝ (Fin 2))} (hA : MeasurableSet A) {gamma : ℝ} (hgamma : 0 ≤ gamma) (hdensity : ∀ᵐ (x : EuclideanSpace ℝ (Fin 2)) ∂(MeasureTheory.Measure.hausdorffMeasure 1).restrict A, ENNReal.ofReal gamma < lowerOneDensity A x) (hfinite : (MeasureTheory.Measure.hausdorffMeasure 1) A ≠ ⊤) {epsilon : ENNReal} (hepsilon : 0 < epsilon) : ∃ (m : ℕ), (MeasureTheory.Measure.hausdorffMeasure 1) (A \ uniformDensitySet ((MeasureTheory.Measure.hausdorffMeasure 1).restrict A) A gamma m) < epsilon

Almost-everywhere density gives an arbitrarily small exceptional set at one uniform scale.

theorem LeanPool.Besicovitch.exists_compact_uniformDensitySet_measure_sdiff_lt {A : Set (EuclideanSpace ℝ (Fin 2))} (hA : MeasurableSet A) {gamma : ℝ} (hgamma : 0 ≤ gamma) (hdensity : ∀ᵐ (x : EuclideanSpace ℝ (Fin 2)) ∂(MeasureTheory.Measure.hausdorffMeasure 1).restrict A, ENNReal.ofReal gamma < lowerOneDensity A x) (hfinite : (MeasureTheory.Measure.hausdorffMeasure 1) A ≠ ⊤) {epsilon : ENNReal} (hepsilon : 0 < epsilon) : ∃ (m : ℕ) (F : Set (EuclideanSpace ℝ (Fin 2))), IsCompact F ∧ F ⊆ uniformDensitySet ((MeasureTheory.Measure.hausdorffMeasure 1).restrict A) A gamma m ∧ (MeasureTheory.Measure.hausdorffMeasure 1) (A \ F) < epsilon

A compact uniform-density piece can retain all but any prescribed positive mass.

theorem LeanPool.Besicovitch.exists_compact_uniformDensitySet_measure_sdiff_lt_mul {A : Set (EuclideanSpace ℝ (Fin 2))} (hA : MeasurableSet A) (hA_pos : 0 < (MeasureTheory.Measure.hausdorffMeasure 1) A) (hA_finite : (MeasureTheory.Measure.hausdorffMeasure 1) A ≠ ⊤) {gamma alpha : ℝ} (hgamma : 0 ≤ gamma) (halpha : 0 < alpha) (hdensity : ∀ᵐ (x : EuclideanSpace ℝ (Fin 2)) ∂(MeasureTheory.Measure.hausdorffMeasure 1).restrict A, ENNReal.ofReal gamma < lowerOneDensity A x) : ∃ (m : ℕ) (F : Set (EuclideanSpace ℝ (Fin 2))), IsCompact F ∧ F ⊆ uniformDensitySet ((MeasureTheory.Measure.hausdorffMeasure 1).restrict A) A gamma m ∧ (MeasureTheory.Measure.hausdorffMeasure 1) (A \ F) < ENNReal.ofReal alpha * (MeasureTheory.Measure.hausdorffMeasure 1) F

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

theorem LeanPool.Besicovitch.exists_compact_uniformDensitySet_above {A : Set (EuclideanSpace ℝ (Fin 2))} (hA : MeasurableSet A) (hA_pos : 0 < (MeasureTheory.Measure.hausdorffMeasure 1) A) (hA_finite : (MeasureTheory.Measure.hausdorffMeasure 1) A ≠ ⊤) {sigma alpha : ℝ} (hsigma : 0 ≤ sigma) (halpha : 0 < alpha) (hdensity : ∀ᵐ (x : EuclideanSpace ℝ (Fin 2)) ∂(MeasureTheory.Measure.hausdorffMeasure 1).restrict A, ENNReal.ofReal sigma < lowerOneDensity A x) : ∃ (gamma : ℝ) (m : ℕ) (F : Set (EuclideanSpace ℝ (Fin 2))), sigma < gamma ∧ IsCompact F ∧ F ⊆ uniformDensitySet ((MeasureTheory.Measure.hausdorffMeasure 1).restrict A) A gamma m ∧ (MeasureTheory.Measure.hausdorffMeasure 1) (A \ F) < ENNReal.ofReal alpha * (MeasureTheory.Measure.hausdorffMeasure 1) F

An almost-everywhere density bound strictly above sigma is uniform at a common higher level on a compact core whose discarded mass is a prescribed fraction of the retained mass.