Packings on six-point configurations

A support remembers selected zero-radius labels, so its virtual diameter has no degenerate cases.

structure LeanPool.Besicovitch.SixPointPacking (configuration : SixPointConfiguration) : Type

A supported radius assignment with disjoint same-color balls.

• support : Finset SixPointIndex

  The centers retained by the packing.

• meets_color (color : SixPointColor) : ∃ (label : SixPointLabel), (color, label) ∈ self.support
• radius : ↥self.support → ↑(Set.Icc 0 1)

  The radius at each retained center.

• same_color_disjoint (i j : ↥self.support) : i ≠ j → (↑i).1 = (↑j).1 → ↑(self.radius i) + ↑(self.radius j) ≤ dist (configuration (↑i).1 (↑i).2) (configuration (↑j).1 (↑j).2)

theorem LeanPool.Besicovitch.SixPointPacking.support_nonempty {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) : packing.support.Nonempty

The support of a six-point packing is nonempty.

def LeanPool.Besicovitch.SixPointPacking.totalRadius {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) : ℝ

The sum of all supported radii.

Equations

• packing.totalRadius = ∑ i ∈ packing.support.attach, ↑(packing.radius i)

noncomputable def LeanPool.Besicovitch.SixPointPacking.virtualDiameter {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) : ℝ

The maximum pairwise center distance plus the two radii on the explicit support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.Besicovitch.SixPointPacking.score {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) (s : ℝ) : ℝ

The packing score at parameter s.

Equations

• packing.score s = packing.totalRadius - packing.virtualDiameter / (2 * s)

theorem LeanPool.Besicovitch.SixPointPacking.pair_le_virtualDiameter {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) (i j : ↥packing.support) : dist (configuration (↑i).1 (↑i).2) (configuration (↑j).1 (↑j).2) + ↑(packing.radius i) + ↑(packing.radius j) ≤ packing.virtualDiameter

Every supported pair contributes at most the virtual diameter.

theorem LeanPool.Besicovitch.SixPointPacking.virtualDiameter_nonneg {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) : 0 ≤ packing.virtualDiameter

The virtual diameter is nonnegative.

theorem LeanPool.Besicovitch.SixPointPacking.dist_le_virtualDiameter {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) (i j : ↥packing.support) : dist (configuration (↑i).1 (↑i).2) (configuration (↑j).1 (↑j).2) ≤ packing.virtualDiameter

Every supported center distance is at most the virtual diameter.

theorem LeanPool.Besicovitch.SixPointPacking.crossColor_le_virtualDiameter {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) {lower : ℝ} (hcross : ∀ (redLabel blueLabel : SixPointLabel), (SixPointColor.red, redLabel) ∈ packing.support → (SixPointColor.blue, blueLabel) ∈ packing.support → lower ≤ dist (configuration SixPointColor.red redLabel) (configuration SixPointColor.blue blueLabel)) : lower ≤ packing.virtualDiameter

A lower bound between the two colors is inherited by the virtual diameter.

theorem LeanPool.Besicovitch.SixPointPacking.two_mul_radius_le_virtualDiameter {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) (i : ↥packing.support) : 2 * ↑(packing.radius i) ≤ packing.virtualDiameter

Twice any supported radius is at most the virtual diameter.

theorem LeanPool.Besicovitch.SixPointPacking.totalRadius_nonneg {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) : 0 ≤ packing.totalRadius

The total radius is nonnegative.