Documentation

LeanPool.Besicovitch.SixPoint.ChildSwapPacking

Relabelling a packing by the simultaneous child swap #

The sibling failure tree can select either diagonal endpoint. This file transports a packing across the simultaneous swap of both colors, preserving its total radius, virtual diameter, and score.

source
def LeanPool.Besicovitch.swapChildrenIndexEquiv :
SixPointIndex ≃ SixPointIndex

The involution on six-point indices that swaps both pairs of children.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem LeanPool.Besicovitch.swapChildrenIndexEquiv_color (index : SixPointIndex) :
    (swapChildrenIndexEquiv index).1 = index.1

    Child relabelling preserves the color of each index.

    source
    @[simp]
    theorem LeanPool.Besicovitch.swapConfigurationChildren_eq_swapIndex (configuration : SixPointConfiguration) (index : SixPointIndex) :
    swapConfigurationChildren configuration index.1 index.2 = configuration (swapChildrenIndexEquiv index).1 (swapChildrenIndexEquiv index).2

    The permuted configuration agrees with the relabelled original centers.

    source
    theorem LeanPool.Besicovitch.SixPointPacking.swapChildrenIndex_mem_of_mem_map {support : Finset SixPointIndex} {index : SixPointIndex} (hindex : index ∈ Finset.map swapChildrenIndexEquiv.toEmbedding support) :
    swapChildrenIndexEquiv index ∈ support

    Membership in a swapped support pulls back along the child-swap involution.

    source
    def LeanPool.Besicovitch.SixPointPacking.unswapChildren {configuration : SixPointConfiguration} (packing : SixPointPacking (swapConfigurationChildren configuration)) :
    SixPointPacking configuration

    Transport a packing through the child permutation.

    Equations
    Instances For
      source
      theorem LeanPool.Besicovitch.SixPointPacking.unswapChildren_totalRadius {configuration : SixPointConfiguration} (packing : SixPointPacking (swapConfigurationChildren configuration)) :
      packing.unswapChildren.totalRadius = packing.totalRadius

      Child relabelling preserves the total radius.

      source
      theorem LeanPool.Besicovitch.SixPointPacking.unswapChildren_virtualDiameter {configuration : SixPointConfiguration} (packing : SixPointPacking (swapConfigurationChildren configuration)) :
      packing.unswapChildren.virtualDiameter = packing.virtualDiameter

      Child relabelling preserves the virtual diameter.

      source
      theorem LeanPool.Besicovitch.SixPointPacking.unswapChildren_score {configuration : SixPointConfiguration} (packing : SixPointPacking (swapConfigurationChildren configuration)) (s : ℝ) :
      packing.unswapChildren.score s = packing.score s

      Child relabelling preserves the packing score.