Normalization of six-point configurations

This file translates and rescales a configuration for the finite six-point problem.

noncomputable def LeanPool.Besicovitch.SixPointConfiguration.normalize (configuration : SixPointConfiguration) (origin : EuclideanSpace ℝ (Fin 2)) (scale : ℝ) : SixPointConfiguration

Translate a configuration by origin and divide all coordinates by scale.

Equations

• configuration.normalize origin scale color label = scale⁻¹ • (configuration color label - origin)

theorem LeanPool.Besicovitch.SixPointConfiguration.dist_normalize (configuration : SixPointConfiguration) (origin : EuclideanSpace ℝ (Fin 2)) {scale : ℝ} (hscale : 0 < scale) (color₁ color₂ : SixPointColor) (label₁ label₂ : SixPointLabel) : dist (configuration.normalize origin scale color₁ label₁) (configuration.normalize origin scale color₂ label₂) = dist (configuration color₁ label₁) (configuration color₂ label₂) / scale

Normalization by a positive scale divides every pairwise distance by that scale.

theorem LeanPool.Besicovitch.SixPointConfiguration.dist_eq_scale_mul_dist_normalize (configuration : SixPointConfiguration) (origin : EuclideanSpace ℝ (Fin 2)) {scale : ℝ} (hscale : 0 < scale) (color₁ color₂ : SixPointColor) (label₁ label₂ : SixPointLabel) : dist (configuration color₁ label₁) (configuration color₂ label₂) = scale * dist (configuration.normalize origin scale color₁ label₁) (configuration.normalize origin scale color₂ label₂)

Multiplying normalized distances by the positive scale recovers physical distances.

theorem LeanPool.Besicovitch.SixPointConfiguration.isAdmissibleAt_normalize_of_distances (configuration : SixPointConfiguration) (origin : EuclideanSpace ℝ (Fin 2)) {scale d γ q s : ℝ} (hscale : 0 < scale) (hroot : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.root) = scale) (hchild : ∀ (color : SixPointColor) (label : SixPointLabel), label ≠ SixPointLabel.root → dist (configuration color SixPointLabel.root) (configuration color label) ≤ d) (hsibling : ∀ (color : SixPointColor), 2 * γ * d < dist (configuration color SixPointLabel.left) (configuration color SixPointLabel.right)) (hq : q = d / scale) (hq_le_one : q ≤ 1) (hs_le : s ≤ γ * q) : (configuration.normalize origin scale).IsAdmissibleAt s

Distance bounds at scale scale give an admissible normalized configuration.