Stability of the six-point packing score

This file controls the score when its parameter or the underlying center distances change.

theorem LeanPool.Besicovitch.SixPointPacking.score_eq_add_gain {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) {s β : ℝ} (hs : 0 < s) (hsβ : s < β) : packing.score β = packing.score s + packing.virtualDiameter * (β - s) / (2 * s * β)

Increasing the score parameter adds an explicit virtual-diameter gain.

theorem LeanPool.Besicovitch.SixPointPacking.score_mono {configuration : SixPointConfiguration} (packing : SixPointPacking configuration) {s β : ℝ} (hs : 0 < s) (hsβ : s < β) : packing.score s ≤ packing.score β

The packing score is nondecreasing in its positive parameter.

def LeanPool.Besicovitch.SixPointPacking.transport {configuration configuration' : SixPointConfiguration} (packing : SixPointPacking configuration) (hdistance : ∀ (i j : ↥packing.support), i ≠ j → (↑i).1 = (↑j).1 → dist (configuration (↑i).1 (↑i).2) (configuration (↑j).1 (↑j).2) ≤ dist (configuration' (↑i).1 (↑i).2) (configuration' (↑j).1 (↑j).2)) : SixPointPacking configuration'

Transport a packing when every relevant same-color distance can only increase.

Equations

• packing.transport hdistance = { support := packing.support, meets_color := ⋯, radius := packing.radius, same_color_disjoint := ⋯ }

@[simp]

theorem LeanPool.Besicovitch.SixPointPacking.transport_totalRadius {configuration configuration' : SixPointConfiguration} (packing : SixPointPacking configuration) (hdistance : ∀ (i j : ↥packing.support), i ≠ j → (↑i).1 = (↑j).1 → dist (configuration (↑i).1 (↑i).2) (configuration (↑j).1 (↑j).2) ≤ dist (configuration' (↑i).1 (↑i).2) (configuration' (↑j).1 (↑j).2)) : (packing.transport hdistance).totalRadius = packing.totalRadius

theorem LeanPool.Besicovitch.SixPointPacking.transport_virtualDiameter_le_add {configuration configuration' : SixPointConfiguration} (packing : SixPointPacking configuration) (hdistance : ∀ (i j : ↥packing.support), i ≠ j → (↑i).1 = (↑j).1 → dist (configuration (↑i).1 (↑i).2) (configuration (↑j).1 (↑j).2) ≤ dist (configuration' (↑i).1 (↑i).2) (configuration' (↑j).1 (↑j).2)) {eta : ℝ} (hperturb : ∀ (i j : ↥packing.support), dist (configuration' (↑i).1 (↑i).2) (configuration' (↑j).1 (↑j).2) ≤ dist (configuration (↑i).1 (↑i).2) (configuration (↑j).1 (↑j).2) + eta) : (packing.transport hdistance).virtualDiameter ≤ packing.virtualDiameter + eta

An upper perturbation of all supported distances bounds the transported virtual diameter.

theorem LeanPool.Besicovitch.SixPointPacking.virtualDiameter_le_transport_add {configuration configuration' : SixPointConfiguration} (packing : SixPointPacking configuration) (hdistance : ∀ (i j : ↥packing.support), i ≠ j → (↑i).1 = (↑j).1 → dist (configuration (↑i).1 (↑i).2) (configuration (↑j).1 (↑j).2) ≤ dist (configuration' (↑i).1 (↑i).2) (configuration' (↑j).1 (↑j).2)) {eta : ℝ} (hperturb : ∀ (i j : ↥packing.support), dist (configuration (↑i).1 (↑i).2) (configuration (↑j).1 (↑j).2) ≤ dist (configuration' (↑i).1 (↑i).2) (configuration' (↑j).1 (↑j).2) + eta) : packing.virtualDiameter ≤ (packing.transport hdistance).virtualDiameter + eta

A lower perturbation of all supported distances bounds the original virtual diameter.

theorem LeanPool.Besicovitch.SixPointPacking.abs_transport_virtualDiameter_sub_le {configuration configuration' : SixPointConfiguration} (packing : SixPointPacking configuration) (hdistance : ∀ (i j : ↥packing.support), i ≠ j → (↑i).1 = (↑j).1 → dist (configuration (↑i).1 (↑i).2) (configuration (↑j).1 (↑j).2) ≤ dist (configuration' (↑i).1 (↑i).2) (configuration' (↑j).1 (↑j).2)) {eta : ℝ} (hperturb : ∀ (i j : ↥packing.support), |dist (configuration' (↑i).1 (↑i).2) (configuration' (↑j).1 (↑j).2) - dist (configuration (↑i).1 (↑i).2) (configuration (↑j).1 (↑j).2)| ≤ eta) : |(packing.transport hdistance).virtualDiameter - packing.virtualDiameter| ≤ eta

Pairwise center errors bound the change in virtual diameter by the same error.

theorem LeanPool.Besicovitch.SixPointPacking.score_pos_of_virtualDiameter_error {configuration configuration' : SixPointConfiguration} (packing : SixPointPacking configuration) (packing' : SixPointPacking configuration') {s β lower eta : ℝ} (hs : 0 < s) (hsβ : s < β) (hscore : 0 ≤ packing.score s) (hlower_pos : 0 < lower) (hlower : lower ≤ packing.virtualDiameter) (htotal : packing'.totalRadius = packing.totalRadius) (hvirtual : packing'.virtualDiameter ≤ packing.virtualDiameter + eta) (herror : s * eta < lower * (β - s)) : 0 < packing'.score β

A controlled diameter error preserves strict positivity after increasing the parameter.

theorem LeanPool.Besicovitch.SixPointPacking.transport_score_pos {configuration configuration' : SixPointConfiguration} (packing : SixPointPacking configuration) (hdistance : ∀ (i j : ↥packing.support), i ≠ j → (↑i).1 = (↑j).1 → dist (configuration (↑i).1 (↑i).2) (configuration (↑j).1 (↑j).2) ≤ dist (configuration' (↑i).1 (↑i).2) (configuration' (↑j).1 (↑j).2)) {s β lower eta : ℝ} (hs : 0 < s) (hsβ : s < β) (hscore : 0 ≤ packing.score s) (hlower_pos : 0 < lower) (hlower : lower ≤ packing.virtualDiameter) (herror : s * eta < lower * (β - s)) (hperturb : ∀ (i j : ↥packing.support), |dist (configuration' (↑i).1 (↑i).2) (configuration' (↑j).1 (↑j).2) - dist (configuration (↑i).1 (↑i).2) (configuration (↑j).1 (↑j).2)| ≤ eta) : 0 < (packing.transport hdistance).score β

A transported packing has positive score when its center error is below the score gain.