Documentation

LeanPool.Besicovitch.SixPoint.Realization

Physical realization of a six-point packing #

A normalized packing is realized by multiplying its radii by the physical length scale. This file relates its virtual diameter and disjointness constraints to the resulting union of open balls.

source
def LeanPool.Besicovitch.SixPointPacking.ballUnionAt {normalized : SixPointConfiguration} (packing : SixPointPacking normalized) (physical : SixPointConfiguration) (scale : ℝ) :
Set (EuclideanSpace ℝ (Fin 2))

The physical union of balls obtained from a normalized packing at a given scale.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem LeanPool.Besicovitch.SixPointPacking.sum_radiusAt {normalized : SixPointConfiguration} (packing : SixPointPacking normalized) (scale : ℝ) :
    ∑ i ∈ packing.support.attach, scale * ↑(packing.radius i) = scale * packing.totalRadius

    The physical radii sum is the scale times the normalized radii sum.

    source
    theorem LeanPool.Besicovitch.SixPointPacking.isOpen_ballUnionAt {normalized : SixPointConfiguration} (packing : SixPointPacking normalized) (physical : SixPointConfiguration) (scale : ℝ) :
    IsOpen (packing.ballUnionAt physical scale)

    The physical ball union is open.

    source
    theorem LeanPool.Besicovitch.SixPointPacking.ediam_ballUnionAt_le {normalized : SixPointConfiguration} (packing : SixPointPacking normalized) (physical : SixPointConfiguration) {scale : ℝ} (hscale : 0 ≤ scale) (hdistance : ∀ (i j : ↥packing.support), dist (physical (↑i).1 (↑i).2) (physical (↑j).1 (↑j).2) = scale * dist (normalized (↑i).1 (↑i).2) (normalized (↑j).1 (↑j).2)) :
    Metric.ediam (packing.ballUnionAt physical scale) ≤ ENNReal.ofReal (scale * packing.virtualDiameter)

    Exact scaling of center distances bounds the diameter of the physical ball union.

    source
    theorem LeanPool.Besicovitch.SixPointPacking.disjoint_ballAt {normalized : SixPointConfiguration} (packing : SixPointPacking normalized) (physical : SixPointConfiguration) {scale : ℝ} (hscale : 0 ≤ scale) (hdistance : ∀ (i j : ↥packing.support), dist (physical (↑i).1 (↑i).2) (physical (↑j).1 (↑j).2) = scale * dist (normalized (↑i).1 (↑i).2) (normalized (↑j).1 (↑j).2)) (i j : ↥packing.support) (hij : i ≠ j) (hcolor : (↑i).1 = (↑j).1) :
    Disjoint (Metric.ball (physical (↑i).1 (↑i).2) (scale * ↑(packing.radius i))) (Metric.ball (physical (↑j).1 (↑j).2) (scale * ↑(packing.radius j)))

    Same-color physical balls remain disjoint under exact distance scaling.