Two-color six-point configurations

This file records exactly the metric assumptions in the finite six-point problem.

inductive LeanPool.Besicovitch.SixPointColor : Type

The two colors in a six-point configuration.

• red : SixPointColor
• blue : SixPointColor

@[instance_reducible]

instance LeanPool.Besicovitch.instDecidableEqSixPointColor : DecidableEq SixPointColor

Equations

• LeanPool.Besicovitch.instDecidableEqSixPointColor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LeanPool.Besicovitch.instFintypeSixPointColor : Fintype SixPointColor

Equations

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

inductive LeanPool.Besicovitch.SixPointLabel : Type

The root and two child labels belonging to each color.

• root : SixPointLabel
• left : SixPointLabel
• right : SixPointLabel

@[instance_reducible]

instance LeanPool.Besicovitch.instDecidableEqSixPointLabel : DecidableEq SixPointLabel

Equations

• LeanPool.Besicovitch.instDecidableEqSixPointLabel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LeanPool.Besicovitch.instFintypeSixPointLabel : Fintype SixPointLabel

Equations

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

@[reducible, inline]

abbrev LeanPool.Besicovitch.SixPointIndex : Type

A label for one of the six points.

Equations

• LeanPool.Besicovitch.SixPointIndex = (LeanPool.Besicovitch.SixPointColor × LeanPool.Besicovitch.SixPointLabel)

@[reducible, inline]

abbrev LeanPool.Besicovitch.SixPointConfiguration : Type

A two-color six-point configuration in the Euclidean plane.

Equations

• LeanPool.Besicovitch.SixPointConfiguration = (LeanPool.Besicovitch.SixPointColor → LeanPool.Besicovitch.SixPointLabel → EuclideanSpace ℝ (Fin 2))

def LeanPool.Besicovitch.SixPointConfiguration.ofPoints (redRoot redLeft redRight blueRoot blueLeft blueRight : EuclideanSpace ℝ (Fin 2)) : SixPointConfiguration

The labelled configuration determined by two roots and two children of each color.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.Besicovitch.SixPointConfiguration.ofPoints redRoot redLeft redRight blueRoot blueLeft blueRight LeanPool.Besicovitch.SixPointColor.red LeanPool.Besicovitch.SixPointLabel.root = redRoot
• LeanPool.Besicovitch.SixPointConfiguration.ofPoints redRoot redLeft redRight blueRoot blueLeft blueRight LeanPool.Besicovitch.SixPointColor.red LeanPool.Besicovitch.SixPointLabel.left = redLeft

structure LeanPool.Besicovitch.SixPointConfiguration.IsAdmissibleAt (configuration : SixPointConfiguration) (s : ℝ) : Prop

A normalized configuration at separation parameter s.

• root_distance : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.root) = 1
• child_distance (color : SixPointColor) (label : SixPointLabel) : label ≠ SixPointLabel.root → dist (configuration color SixPointLabel.root) (configuration color label) ≤ 1
• sibling_distance (color : SixPointColor) : 2 * s ≤ dist (configuration color SixPointLabel.left) (configuration color SixPointLabel.right)

theorem LeanPool.Besicovitch.SixPointConfiguration.IsAdmissibleAt.mono {configuration : SixPointConfiguration} {s t : ℝ} (hst : s ≤ t) (h : configuration.IsAdmissibleAt t) : configuration.IsAdmissibleAt s

Raising the separation parameter only shrinks the admissible configuration class.