Documentation

LeanPool.Besicovitch.SixPoint.EndpointGeometry

Coordinate-free endpoint geometry #

After translating the red root to the origin, the blue children are pulled back toward their own root. The resulting vectors are the e, p, and w variables in the nine-packing proof.

source
def LeanPool.Besicovitch.SixPointConfiguration.rootDisplacement (configuration : SixPointConfiguration) :
EuclideanSpace ℝ (Fin 2)

The displacement from the red root to the blue root.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def LeanPool.Besicovitch.SixPointConfiguration.redDisplacement (configuration : SixPointConfiguration) (label : SixPointLabel) :
    EuclideanSpace ℝ (Fin 2)

    A red point, translated relative to the red root.

    Equations
    Instances For
      source
      def LeanPool.Besicovitch.SixPointConfiguration.bluePullback (configuration : SixPointConfiguration) (label : SixPointLabel) :
      EuclideanSpace ℝ (Fin 2)

      A blue point pulled back from the blue root into the red child disk.

      Equations
      Instances For
        source
        theorem LeanPool.Besicovitch.SixPointConfiguration.norm_rootDisplacement {configuration : SixPointConfiguration} {s : ℝ} (h : configuration.IsAdmissibleAt s) :
        ‖configuration.rootDisplacement‖ = 1

        The root displacement of an admissible configuration has unit norm.

        source
        theorem LeanPool.Besicovitch.SixPointConfiguration.norm_redDisplacement_le_one {configuration : SixPointConfiguration} {s : ℝ} (h : configuration.IsAdmissibleAt s) {label : SixPointLabel} (hlabel : label ≠ SixPointLabel.root) :
        ‖configuration.redDisplacement label‖ ≤ 1

        Red child displacements have norm at most one.

        source
        theorem LeanPool.Besicovitch.SixPointConfiguration.norm_bluePullback_le_one {configuration : SixPointConfiguration} {s : ℝ} (h : configuration.IsAdmissibleAt s) {label : SixPointLabel} (hlabel : label ≠ SixPointLabel.root) :
        ‖configuration.bluePullback label‖ ≤ 1

        Pulled-back blue child displacements have norm at most one.

        source
        theorem LeanPool.Besicovitch.SixPointConfiguration.dist_redDisplacement (configuration : SixPointConfiguration) (label₁ label₂ : SixPointLabel) :
        dist (configuration.redDisplacement label₁) (configuration.redDisplacement label₂) = dist (configuration SixPointColor.red label₁) (configuration SixPointColor.red label₂)

        The distance between red children is their displacement-vector distance.

        source
        theorem LeanPool.Besicovitch.SixPointConfiguration.dist_bluePullback (configuration : SixPointConfiguration) (label₁ label₂ : SixPointLabel) :
        dist (configuration.bluePullback label₁) (configuration.bluePullback label₂) = dist (configuration SixPointColor.blue label₁) (configuration SixPointColor.blue label₂)

        Pulling back both blue children preserves their distance.

        source
        theorem LeanPool.Besicovitch.SixPointConfiguration.two_mul_le_dist_redDisplacement {configuration : SixPointConfiguration} {s : ℝ} (h : configuration.IsAdmissibleAt s) :
        2 * s ≤ dist (configuration.redDisplacement SixPointLabel.left) (configuration.redDisplacement SixPointLabel.right)

        Admissibility gives the endpoint lower bound for the red displacement pair.

        source
        theorem LeanPool.Besicovitch.SixPointConfiguration.two_mul_le_dist_bluePullback {configuration : SixPointConfiguration} {s : ℝ} (h : configuration.IsAdmissibleAt s) :
        2 * s ≤ dist (configuration.bluePullback SixPointLabel.left) (configuration.bluePullback SixPointLabel.right)

        Admissibility gives the endpoint lower bound for the pulled-back blue pair.

        source
        theorem LeanPool.Besicovitch.SixPointConfiguration.dist_red_blue_eq_norm (configuration : SixPointConfiguration) (redLabel blueLabel : SixPointLabel) :
        dist (configuration SixPointColor.red redLabel) (configuration SixPointColor.blue blueLabel) = ‖configuration.rootDisplacement - configuration.redDisplacement redLabel - configuration.bluePullback blueLabel‖

        A red-blue child distance is the norm of e - p - w.