Scaling six-point packing radii

This file shrinks every radius while retaining the same centers and support. Shrinking creates the strict score gain used when the density parameter is larger than the finite endpoint.

def LeanPool.Besicovitch.SixPointPacking.scaleRadii {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) (q : ℝ) (hq0 : 0 ≤ q) (hq1 : q ≤ 1) : SixPointPacking configuration

Shrink every packing radius by a factor in [0, 1].

Equations

• packing.scaleRadii q hq0 hq1 = { support := packing.support, meets_color := ⋯, radius := fun (i : ↥packing.support) => ⟨q * ↑(packing.radius i), ⋯⟩, same_color_disjoint := ⋯ }

@[simp]

theorem LeanPool.Besicovitch.SixPointPacking.scaleRadii_totalRadius {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) (q : ℝ) (hq0 : 0 ≤ q) (hq1 : q ≤ 1) : (packing.scaleRadii q hq0 hq1).totalRadius = q * packing.totalRadius

theorem LeanPool.Besicovitch.SixPointPacking.scaleRadii_virtualDiameter_le {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) (q : ℝ) (hq0 : 0 ≤ q) (hq1 : q ≤ 1) : (packing.scaleRadii q hq0 hq1).virtualDiameter ≤ packing.virtualDiameter

Shrinking radii cannot increase the virtual diameter.

theorem LeanPool.Besicovitch.SixPointPacking.scaleRadii_score_ge {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) {s β q lower : ℝ} (hs : 0 < s) (hβ : 0 < β) (hq : 0 ≤ q) (hq1 : q ≤ 1) (hgain : s ≤ β * q) (hscore : 0 ≤ packing.score s) (hlower : lower ≤ packing.virtualDiameter) : lower * (β * q - s) / (2 * s * β) ≤ (packing.scaleRadii q hq hq1).score β

The score after shrinking has an explicit lower bound from the original diameter.

theorem LeanPool.Besicovitch.SixPointPacking.scaleRadii_score_pos {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) {s β q lower : ℝ} (hs : 0 < s) (hβ : 0 < β) (hq : 0 < q) (hq1 : q ≤ 1) (hgain : s < β * q) (hscore : 0 ≤ packing.score s) (hlower : lower ≤ packing.virtualDiameter) (hlower_pos : 0 < lower) : 0 < (packing.scaleRadii q ⋯ hq1).score β

Shrinking by q gives positive score at β when s < βq.