Localizing bad convex sets

A selected bad set whose three-diameter enlargement meets a small continuum must itself lie in the doubled ball, provided the centre was chosen outside its seven-diameter enlargement.

def LeanPool.Besicovitch.touchingBadConvexSets (p : ℝ) (chosen : Set (Set (EuclideanSpace ℝ (Fin 2)))) (C : Set (EuclideanSpace ℝ (Fin 2))) : Set (Set (EuclideanSpace ℝ (Fin 2)))

Selected holes whose p-diameter enlargements meet a set.

Equations

• LeanPool.Besicovitch.touchingBadConvexSets p chosen C = {V : Set (EuclideanSpace ℝ (Fin 2)) | V ∈ chosen ∧ (LeanPool.Besicovitch.diameterThickening p V ∩ C).Nonempty}

theorem LeanPool.Besicovitch.subset_ball_two_mul_of_diameterThickening_three_inter {V C : Set (EuclideanSpace ℝ (Fin 2))} (hV : Bornology.IsBounded V) {z : EuclideanSpace ℝ (Fin 2)} {rho : ℝ} (hz : z ∉ diameterThickening 7 V) (hC : C ⊆ Metric.closedBall z rho) (htouch : (diameterThickening 3 V ∩ C).Nonempty) : V ⊆ Metric.ball z (2 * rho)

A hole touching the local continuum is contained in the doubled localization ball.

theorem LeanPool.Besicovitch.mul_tsum_ediam_touchingBadConvexSets_le {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} {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) {C : Set (EuclideanSpace ℝ (Fin 2))} {z : EuclideanSpace ℝ (Fin 2)} {rho : ℝ} (hz : ∀ (V : ↑chosen), z ∉ diameterThickening 7 ↑V) (hC : C ⊆ Metric.closedBall z rho) : ENNReal.ofReal alpha * ∑' (V : ↑(touchingBadConvexSets 3 chosen C)), Metric.ediam ↑V ≤ mu (Metric.ball z (2 * rho) \ F)

The selected holes touching the local continuum charge only the doubled ball.

theorem LeanPool.Besicovitch.tsum_ediam_touchingBadConvexSets_lt_ediam {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} {F : Set (EuclideanSpace ℝ (Fin 2))} (hF : MeasurableSet F) {alpha sigma : ℝ} (halpha : 0 < alpha) (hsigma : 0 < sigma) {chosen : Set (Set (EuclideanSpace ℝ (Fin 2)))} (hchosen : chosen ⊆ badConvexSets mu F alpha) (hcountable : chosen.Countable) (hdisjoint : chosen.PairwiseDisjoint id) {C : Set (EuclideanSpace ℝ (Fin 2))} {z : EuclideanSpace ℝ (Fin 2)} {rho : ℝ} (hrho : 0 < rho) (hz : ∀ (V : ↑chosen), z ∉ diameterThickening 7 ↑V) (hC : C ⊆ Metric.closedBall z rho) (houtside : mu (Metric.ball z (2 * rho) \ F) < ENNReal.ofReal alpha * ENNReal.ofReal (sigma * rho / 14)) (hCdiam : ENNReal.ofReal (sigma * rho / 2) ≤ Metric.ediam C) : ∑' (V : ↑(touchingBadConvexSets 3 chosen C)), Metric.ediam (diameterThickening 3 ↑V) < Metric.ediam C

The three-diameter enlargements touching the local continuum have total diameter smaller than the continuum itself.