A density point outside the enlarged holes

Lebesgue differentiation lets us choose the point outside the seven-diameter enlargements so that the mass missing from the compact core is linearly small in every sufficiently small ball.

theorem LeanPool.Besicovitch.IsStraightMeasure.measure_closedBall_le {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} (hmu : IsStraightMeasure mu) (z : EuclideanSpace ℝ (Fin 2)) (r : ℝ) : mu (Metric.closedBall z r) ≤ ENNReal.ofReal (2 * r)

A straight measure assigns at most 2r mass to a closed ball of radius r.

theorem LeanPool.Besicovitch.annulus_inter_nonempty {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} (hmu : IsStraightMeasure mu) {F : Set (EuclideanSpace ℝ (Fin 2))} {z : EuclideanSpace ℝ (Fin 2)} {sigma alpha rho : ℝ} (hsigma : 0 < sigma) (halpha_pos : 0 < alpha) (halpha : alpha < 28) (hrho : 0 < rho) (hball : ENNReal.ofReal (2 * sigma * rho) < mu (Metric.ball z rho)) (hloss : mu (Metric.ball z rho \ F) < ENNReal.ofReal (sigma * alpha / 28 * rho)) : (Metric.ball z rho \ Metric.ball z (sigma * rho / 2) ∩ F).Nonempty

A lower ball-mass bound and a small loss outside the core leave a core point in the outer annulus.

theorem LeanPool.Besicovitch.exists_scale_measure_ball_sdiff_lt {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} (hmu : IsStraightMeasure mu) {F : Set (EuclideanSpace ℝ (Fin 2))} {z : EuclideanSpace ℝ (Fin 2)} (hdensity : Filter.Tendsto (fun (r : ℝ) => mu (Fᶜ ∩ Metric.closedBall z r) / mu (Metric.closedBall z r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) {k : ℝ} (hk : 0 < k) : ∃ (scale : ℝ), 0 < scale ∧ ∀ (r : ℝ), 0 < r → r < scale → mu (Metric.ball z r \ F) < ENNReal.ofReal (k * r)

At a density point of F, straightness makes the mass outside F smaller than any prescribed positive linear function of the radius.

theorem LeanPool.Besicovitch.exists_densityPoint_not_mem_sevenDiameterThickening {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} [MeasureTheory.IsFiniteMeasure mu] (hmu : IsStraightMeasure mu) {F : Set (EuclideanSpace ℝ (Fin 2))} (hF : MeasurableSet F) {alpha : ℝ} (halpha : 0 < alpha) {chosen : Set (Set (EuclideanSpace ℝ (Fin 2)))} (hchosen : chosen ⊆ badConvexSets mu F alpha) (hcountable : chosen.Countable) (hdisjoint : chosen.PairwiseDisjoint id) (houtside : mu Fᶜ < ENNReal.ofReal (alpha / 15) * mu F) {k : ℝ} (hk : 0 < k) : ∃ z ∈ F, (∀ (V : ↑chosen), z ∉ diameterThickening 7 ↑V) ∧ ∃ (scale : ℝ), 0 < scale ∧ ∀ (r : ℝ), 0 < r → r < scale → mu (Metric.ball z r \ F) < ENNReal.ofReal (k * r)

One may choose the point outside all seven-diameter enlargements to be a density point of the compact core.