Documentation

LeanPool.Besicovitch.Rectifiability.BadConvexSets

Bad convex sets #

A bad convex set meets the compact density core but contains disproportionately much measure outside it. These are the holes used in the continuum construction.

source
def LeanPool.Besicovitch.badConvexSets (mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))) (F : Set (EuclideanSpace ℝ (Fin 2))) (alpha : ℝ) :
Set (Set (EuclideanSpace ℝ (Fin 2)))

Open convex sets meeting F whose mass outside F exceeds alpha times their diameter.

Equations
Instances For
    source
    @[simp]
    theorem LeanPool.Besicovitch.mem_badConvexSets {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} {F V : Set (EuclideanSpace ℝ (Fin 2))} {alpha : ℝ} :
    V ∈ badConvexSets mu F alpha ↔ IsOpen V ∧ Convex ℝ V ∧ (V ∩ F).Nonempty ∧ ENNReal.ofReal alpha * Metric.ediam V < mu (V \ F)
    source
    theorem LeanPool.Besicovitch.isBounded_of_mem_badConvexSets {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} {F V : Set (EuclideanSpace ℝ (Fin 2))} {alpha : ℝ} (halpha : 0 < alpha) (hV : V ∈ badConvexSets mu F alpha) :
    Bornology.IsBounded V

    A bad convex set with positive leakage coefficient is bounded.

    source
    theorem LeanPool.Besicovitch.diam_pos_of_mem_badConvexSets {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} {F V : Set (EuclideanSpace ℝ (Fin 2))} {alpha : ℝ} (halpha : 0 < alpha) (hV : V ∈ badConvexSets mu F alpha) :
    0 < Metric.diam V

    A nonempty open bad convex set has positive diameter.

    source
    theorem LeanPool.Besicovitch.diam_lt_measure_univ_div_of_mem_badConvexSets {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} [MeasureTheory.IsFiniteMeasure mu] {F V : Set (EuclideanSpace ℝ (Fin 2))} {alpha : ℝ} (halpha : 0 < alpha) (hV : V ∈ badConvexSets mu F alpha) :
    Metric.diam V < (mu Set.univ).toReal / alpha

    The total mass supplies a uniform real diameter bound for all bad convex sets.

    source
    theorem LeanPool.Besicovitch.openConvexHull_mem_badConvexSets {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} {F U : Set (EuclideanSpace ℝ (Fin 2))} {alpha tau : ℝ} (halpha_tau : alpha ≤ tau) (hU_open : IsOpen U) (hUF : (U ∩ F).Nonempty) (hleakage : ENNReal.ofReal tau * Metric.ediam U < mu (U \ F)) :
    openConvexHull U ∈ badConvexSets mu F alpha

    A BPC witness becomes bad after replacing it by its open convex hull and lowering the coefficient.

    source
    theorem LeanPool.Besicovitch.exists_countable_disjoint_badConvexSets {mu : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))} [MeasureTheory.IsFiniteMeasure mu] (F : Set (EuclideanSpace ℝ (Fin 2))) {alpha : ℝ} (halpha : 0 < alpha) :
    ∃ chosen ⊆ badConvexSets mu F alpha, chosen.PairwiseDisjoint id ∧ chosen.Countable ∧ ∀ V ∈ badConvexSets mu F alpha, ∃ W ∈ chosen, (V ∩ W).Nonempty ∧ Metric.diam V < 2 * Metric.diam W

    The bad convex sets have a countable disjoint scale-dominating subfamily.