Enlarging bad convex sets #
The seven-diameter enlargements of a disjoint family of bad convex sets still leave a point of
the compact core uncovered. The number 15 = 2 * 7 + 1 is exactly the diameter expansion
factor.
theorem
LeanPool.Besicovitch.measure_iUnion_diameterThickening_le
{mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))}
(hmu : IsStraightMeasure mu)
{alpha p : ℝ}
(halpha : 0 < alpha)
(hp : 0 ≤ p)
{F : Set (EuclideanSpace ℝ (Fin 2))}
{chosen : Set (Set (EuclideanSpace ℝ (Fin 2)))}
(hchosen : chosen ⊆ badConvexSets mu F alpha)
(hcountable : chosen.Countable)
:
mu (⋃ (V : ↑chosen), diameterThickening p ↑V) ≤ ENNReal.ofReal (2 * p + 1) * ∑' (V : ↑chosen), Metric.ediam ↑V
Straightness bounds the mass of all diameter thickenings by their total expanded diameter.
theorem
LeanPool.Besicovitch.measure_iUnion_sevenDiameterThickening_lt
{mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))}
(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)
:
The seven-diameter enlargements have less mass than the retained core.
theorem
LeanPool.Besicovitch.exists_mem_not_mem_sevenDiameterThickening
{mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))}
(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)
:
∃ z ∈ F, ∀ (V : ↑chosen), z ∉ diameterThickening 7 ↑V
Consequently, some point of the retained core lies outside every seven-diameter enlargement.