Compact convex attachments

For each selected hole, the continuum construction attaches the closed convex hull of the core points in its two-diameter enlargement.

def LeanPool.Besicovitch.convexAttachment (F V : Set (EuclideanSpace ℝ (Fin 2))) : Set (EuclideanSpace ℝ (Fin 2))

The compact convex piece attached to the core near a selected hole.

Equations

• LeanPool.Besicovitch.convexAttachment F V = closure ((convexHull ℝ) (F ∩ LeanPool.Besicovitch.diameterThickening 2 V))

theorem LeanPool.Besicovitch.isClosed_convexAttachment (F V : Set (EuclideanSpace ℝ (Fin 2))) : IsClosed (convexAttachment F V)

A convex attachment is closed and convex.

theorem LeanPool.Besicovitch.convex_convexAttachment (F V : Set (EuclideanSpace ℝ (Fin 2))) : Convex ℝ (convexAttachment F V)

theorem LeanPool.Besicovitch.isCompact_convexAttachment {F V : Set (EuclideanSpace ℝ (Fin 2))} (hF : IsCompact F) : IsCompact (convexAttachment F V)

Attachments to a compact core are compact.

theorem LeanPool.Besicovitch.inter_subset_convexAttachment {F V : Set (EuclideanSpace ℝ (Fin 2))} (hdiam : 0 < Metric.diam V) : F ∩ V ⊆ convexAttachment F V

Every core point already in a hole belongs to its attachment.

theorem LeanPool.Besicovitch.diam_convexAttachment_le {F V : Set (EuclideanSpace ℝ (Fin 2))} (hV : Bornology.IsBounded V) : Metric.diam (convexAttachment F V) ≤ 5 * Metric.diam V

An attachment has diameter at most five times the diameter of its hole.

theorem LeanPool.Besicovitch.ediam_convexAttachment_le {F V : Set (EuclideanSpace ℝ (Fin 2))} (hV : Bornology.IsBounded V) : Metric.ediam (convexAttachment F V) ≤ ENNReal.ofReal 5 * Metric.ediam V

The same five-fold bound holds for extended diameter.

theorem LeanPool.Besicovitch.convexAttachment_subset_diameterThickening_three {F V : Set (EuclideanSpace ℝ (Fin 2))} (hV_convex : Convex ℝ V) (hdiam : 0 < Metric.diam V) : convexAttachment F V ⊆ diameterThickening 3 V

For a positive-diameter convex hole, its attachment lies in the three-diameter enlargement.

theorem LeanPool.Besicovitch.convexAttachment_isCompact_isConnected {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} {F V : Set (EuclideanSpace ℝ (Fin 2))} {alpha : ℝ} (hF : IsCompact F) (halpha : 0 < alpha) (hV : V ∈ badConvexSets mu F alpha) : IsCompact (convexAttachment F V) ∧ IsConnected (convexAttachment F V)

A bad hole has a nonempty compact connected attachment.