Documentation

LeanPool.Besicovitch.Geometry.ConvexEnlargement

Convex enlargements #

This file records the two elementary enlargements used in the continuum argument: thickening a set by a multiple of its diameter, and replacing an open set by its open convex hull.

source
def LeanPool.Besicovitch.diameterThickening (p : ℝ) (s : Set (EuclideanSpace ℝ (Fin 2))) :
Set (EuclideanSpace ℝ (Fin 2))

The p-diameter thickening of a set.

Equations
Instances For
    source
    theorem LeanPool.Besicovitch.isOpen_diameterThickening (p : ℝ) (s : Set (EuclideanSpace ℝ (Fin 2))) :
    IsOpen (diameterThickening p s)

    Diameter thickenings are open.

    source
    theorem LeanPool.Besicovitch.diam_diameterThickening_le {p : ℝ} (hp : 0 ≤ p) (s : Set (EuclideanSpace ℝ (Fin 2))) :
    Metric.diam (diameterThickening p s) ≤ (2 * p + 1) * Metric.diam s

    A nonnegative p-diameter thickening has diameter at most (2p + 1) times the original.

    source
    theorem LeanPool.Besicovitch.ediam_diameterThickening_le {p : ℝ} (hp : 0 ≤ p) {s : Set (EuclideanSpace ℝ (Fin 2))} (hs : Bornology.IsBounded s) :
    Metric.ediam (diameterThickening p s) ≤ ENNReal.ofReal (2 * p + 1) * Metric.ediam s

    The extended diameter of a nonnegative diameter thickening obeys the same linear bound.

    source
    theorem LeanPool.Besicovitch.subset_diameterThickening {p : ℝ} {s : Set (EuclideanSpace ℝ (Fin 2))} (hpositive : 0 < p * Metric.diam s) :
    s ⊆ diameterThickening p s

    A set is contained in every positive-radius diameter thickening.

    source
    theorem LeanPool.Besicovitch.subset_diameterThickening_of_inter_nonempty {u s : Set (EuclideanSpace ℝ (Fin 2))} {p : ℝ} (hu : Bornology.IsBounded u) (hus : (u ∩ s).Nonempty) (hdiam : Metric.diam u < p * Metric.diam s) :
    u ⊆ diameterThickening p s

    A bounded set meeting s lies in the p-diameter thickening of s when its diameter is smaller than the thickening radius.

    source
    def LeanPool.Besicovitch.openConvexHull (s : Set (EuclideanSpace ℝ (Fin 2))) :
    Set (EuclideanSpace ℝ (Fin 2))

    The interior of the convex hull of a set.

    Equations
    Instances For
      source
      theorem LeanPool.Besicovitch.isOpen_openConvexHull (s : Set (EuclideanSpace ℝ (Fin 2))) :
      IsOpen (openConvexHull s)

      The open convex hull is open.

      source
      theorem LeanPool.Besicovitch.convex_openConvexHull (s : Set (EuclideanSpace ℝ (Fin 2))) :
      Convex ℝ (openConvexHull s)

      The open convex hull is convex.

      source
      theorem LeanPool.Besicovitch.subset_openConvexHull {s : Set (EuclideanSpace ℝ (Fin 2))} (hs : IsOpen s) :
      s ⊆ openConvexHull s

      An open set is contained in its open convex hull.

      source
      theorem LeanPool.Besicovitch.ediam_openConvexHull {s : Set (EuclideanSpace ℝ (Fin 2))} (hs : IsOpen s) :
      Metric.ediam (openConvexHull s) = Metric.ediam s

      Passing from an open set to its open convex hull does not change its extended diameter.

      source
      theorem LeanPool.Besicovitch.diam_openConvexHull {s : Set (EuclideanSpace ℝ (Fin 2))} (hs : IsOpen s) :
      Metric.diam (openConvexHull s) = Metric.diam s

      Passing from an open set to its open convex hull does not change its diameter.