Documentation

LeanPool.Besicovitch.SixPoint.BlueChildSwap

Swapping the two blue children #

The four-child minimax has two matching branches. Swapping only the blue children identifies the anti-diagonal branch with the diagonal one and preserves admissibility and every packing score.

source
def LeanPool.Besicovitch.swapBlueIndexEquiv :
SixPointIndex ≃ SixPointIndex

The index permutation that interchanges the two blue children.

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

    Child relabelling preserves the color of each index.

    source
    def LeanPool.Besicovitch.swapBlueChildren (configuration : SixPointConfiguration) :
    SixPointConfiguration

    The configuration obtained by interchanging the two blue children.

    Equations
    Instances For
      source
      @[simp]
      theorem LeanPool.Besicovitch.swapBlueChildren_eq_swapBlueIndex (configuration : SixPointConfiguration) (index : SixPointIndex) :
      swapBlueChildren configuration index.1 index.2 = configuration (swapBlueIndexEquiv index).1 (swapBlueIndexEquiv index).2

      The permuted configuration agrees with the relabelled original centers.

      source
      theorem LeanPool.Besicovitch.IsAdmissibleAt.swapBlueChildren {configuration : SixPointConfiguration} {s : ℝ} (h : configuration.IsAdmissibleAt s) :
      (Besicovitch.swapBlueChildren configuration).IsAdmissibleAt s

      Swapping the blue children preserves endpoint admissibility.

      source
      theorem LeanPool.Besicovitch.selectedDiagonalMatchingFails_swapBlueChildren (configuration : SixPointConfiguration) :
      SelectedDiagonalMatchingFails (swapBlueChildren configuration) ↔ (2 * barC - 1) * (dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right) + dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right)) ≤ dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right) + dist (configuration SixPointColor.red SixPointLabel.right) (configuration SixPointColor.blue SixPointLabel.left)

      After swapping the blue children, the selected diagonal is the original anti-diagonal.

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

      Membership in a swapped support pulls back along the involution.

      source
      def LeanPool.Besicovitch.SixPointPacking.unswapBlue {configuration : SixPointConfiguration} (packing : SixPointPacking (swapBlueChildren configuration)) :
      SixPointPacking configuration

      Transport a packing through the child permutation.

      Equations
      Instances For
        source
        theorem LeanPool.Besicovitch.SixPointPacking.unswapBlue_totalRadius {configuration : SixPointConfiguration} (packing : SixPointPacking (swapBlueChildren configuration)) :
        packing.unswapBlue.totalRadius = packing.totalRadius

        Child relabelling preserves the total radius.

        source
        theorem LeanPool.Besicovitch.SixPointPacking.unswapBlue_virtualDiameter {configuration : SixPointConfiguration} (packing : SixPointPacking (swapBlueChildren configuration)) :
        packing.unswapBlue.virtualDiameter = packing.virtualDiameter

        Child relabelling preserves the virtual diameter.

        source
        theorem LeanPool.Besicovitch.SixPointPacking.unswapBlue_score {configuration : SixPointConfiguration} (packing : SixPointPacking (swapBlueChildren configuration)) (s : ℝ) :
        packing.unswapBlue.score s = packing.score s

        Child relabelling preserves the packing score.