Packing bad convex sets

For a disjoint countable family of bad convex sets, the sum of their diameters is controlled by the mass outside the compact core.

theorem LeanPool.Besicovitch.mul_tsum_ediam_badConvexSets_le_measure {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} {F ambient : Set (EuclideanSpace ℝ (Fin 2))} (hF : MeasurableSet F) {alpha : ℝ} {chosen : Set (Set (EuclideanSpace ℝ (Fin 2)))} (hchosen : chosen ⊆ badConvexSets mu F alpha) (hcountable : chosen.Countable) (hdisjoint : chosen.PairwiseDisjoint id) (hcontained : ∀ V ∈ chosen, V ⊆ ambient) : ENNReal.ofReal alpha * ∑' (V : ↑chosen), Metric.ediam ↑V ≤ mu (ambient \ F)

Disjoint bad convex sets contained in an ambient set charge only its mass outside the core.

theorem LeanPool.Besicovitch.mul_tsum_ediam_badConvexSets_le {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} {F : Set (EuclideanSpace ℝ (Fin 2))} (hF : MeasurableSet F) {alpha : ℝ} {chosen : Set (Set (EuclideanSpace ℝ (Fin 2)))} (hchosen : chosen ⊆ badConvexSets mu F alpha) (hcountable : chosen.Countable) (hdisjoint : chosen.PairwiseDisjoint id) : ENNReal.ofReal alpha * ∑' (V : ↑chosen), Metric.ediam ↑V ≤ mu Fᶜ

Disjoint bad convex sets have total extended diameter controlled by the mass outside the compact core.

theorem LeanPool.Besicovitch.tsum_ediam_badConvexSets_lt {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} {F : Set (EuclideanSpace ℝ (Fin 2))} (hF : MeasurableSet F) {alpha enlargement : ℝ} (halpha : 0 < alpha) (henlargement : 0 < enlargement) {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 / enlargement) * mu F) : ∑' (V : ↑chosen), Metric.ediam ↑V < ENNReal.ofReal (1 / enlargement) * mu F

If the outside mass is less than alpha / enlargement times the retained mass, then the diameter sum is less than 1 / enlargement times the retained mass.