Relabelling supported packings

A color-preserving permutation transports a packing and preserves its radius sum and score.

def LeanPool.Besicovitch.SixPointPacking.relabelSupportEquiv (support : Finset SixPointIndex) (permutation : SixPointIndex ≃ SixPointIndex) : ↥(Finset.map permutation.toEmbedding support) ≃ ↥support

Pull the support back along the relabelling permutation.

Equations

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

def LeanPool.Besicovitch.SixPointPacking.relabel {source target : SixPointConfiguration} (packing : SixPointPacking source) (permutation : SixPointIndex ≃ SixPointIndex) (hcolor : ∀ (index : SixPointIndex), (permutation index).1 = index.1) (hconfiguration : ∀ (index : SixPointIndex), source index.1 index.2 = target (permutation index).1 (permutation index).2) : SixPointPacking target

Transport a packing along a color-preserving permutation of its centers.

Equations

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

theorem LeanPool.Besicovitch.SixPointPacking.relabel_totalRadius {source target : SixPointConfiguration} (packing : SixPointPacking source) (permutation : SixPointIndex ≃ SixPointIndex) (hcolor : ∀ (index : SixPointIndex), (permutation index).1 = index.1) (hconfiguration : ∀ (index : SixPointIndex), source index.1 index.2 = target (permutation index).1 (permutation index).2) : (packing.relabel permutation hcolor hconfiguration).totalRadius = packing.totalRadius

Relabelling preserves the sum of the supported radii.

theorem LeanPool.Besicovitch.SixPointPacking.relabel_virtualDiameter {source target : SixPointConfiguration} (packing : SixPointPacking source) (permutation : SixPointIndex ≃ SixPointIndex) (hcolor : ∀ (index : SixPointIndex), (permutation index).1 = index.1) (hconfiguration : ∀ (index : SixPointIndex), source index.1 index.2 = target (permutation index).1 (permutation index).2) : (packing.relabel permutation hcolor hconfiguration).virtualDiameter = packing.virtualDiameter

Relabelling preserves every contribution to the virtual diameter.

theorem LeanPool.Besicovitch.SixPointPacking.relabel_score {source target : SixPointConfiguration} (packing : SixPointPacking source) (permutation : SixPointIndex ≃ SixPointIndex) (hcolor : ∀ (index : SixPointIndex), (permutation index).1 = index.1) (hconfiguration : ∀ (index : SixPointIndex), source index.1 index.2 = target (permutation index).1 (permutation index).2) (s : ℝ) : (packing.relabel permutation hcolor hconfiguration).score s = packing.score s

Relabelling preserves the score at every threshold.