The planar diameter bound

This module formalizes the classical Perles charging proof that a finite planar set has at most as many diameter pairs as points. Every diameter edge is assigned to a clockwise-extreme endpoint, and the signed-area lemmas show that no endpoint can receive two different edges.

def LeanPool.Erdos132N14.EdgeIncident {ι : Type u_1} (v : ι) (e : ι × ι) : Prop

Whether v is an endpoint of the increasing representative e.

Equations

• LeanPool.Erdos132N14.EdgeIncident v e = (v = e.1 ∨ v = e.2)

def LeanPool.Erdos132N14.otherEndpoint {ι : Type u_1} [LinearOrder ι] (e : ι × ι) (v : ι) : ι

The endpoint of e opposite an incident vertex v.

Equations

• LeanPool.Erdos132N14.otherEndpoint e v = if e.1 = v then e.2 else e.1

theorem LeanPool.Erdos132N14.pairWith_endpoint_other {ι : Type u_1} [LinearOrder ι] {S : Finset ι} {e : ι × ι} {v : ι} (he : e ∈ pairs S) (hv : EdgeIncident v e) : pairWith v (otherEndpoint e v) = e

theorem LeanPool.Erdos132N14.endpoint_mem {ι : Type u_1} [LinearOrder ι] {S : Finset ι} {e : ι × ι} {v : ι} (he : e ∈ pairs S) (hv : EdgeIncident v e) : v ∈ S

theorem LeanPool.Erdos132N14.otherEndpoint_mem {ι : Type u_1} [LinearOrder ι] {S : Finset ι} {e : ι × ι} {v : ι} (he : e ∈ pairs S) (hv : EdgeIncident v e) : otherEndpoint e v ∈ S

theorem LeanPool.Erdos132N14.otherEndpoint_ne {ι : Type u_1} [LinearOrder ι] {S : Finset ι} {e : ι × ι} {v : ι} (he : e ∈ pairs S) (hv : EdgeIncident v e) : otherEndpoint e v ≠ v

theorem LeanPool.Erdos132N14.dist_endpoint_other_eq_pairDistance {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) {S : Finset ι} {e : ι × ι} {v : ι} (he : e ∈ pairs S) (hv : EdgeIncident v e) : dist (P.point v) (P.point (otherEndpoint e v)) = P.pairDistance e

noncomputable def LeanPool.Erdos132N14.diameterEdges {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) (S : Finset ι) (d : ℝ) : Finset (ι × ι)

The pairs in S that realize a specified distance.

Equations

• LeanPool.Erdos132N14.diameterEdges P S d = {e ∈ LeanPool.Erdos132N14.pairs S | P.pairDistance e = d}

def LeanPool.Erdos132N14.ClockwiseExtremeAt {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) (E : Finset (ι × ι)) (e : ι × ι) (v : ι) : Prop

Edge e is clockwise-extreme at v among the edges E.

Equations

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

theorem LeanPool.Erdos132N14.diameter_edge_extreme_at_endpoint {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) (S : Finset ι) {d : ℝ} (hd : 0 < d) (hmax : ∀ f ∈ pairs S, P.pairDistance f ≤ d) {e : ι × ι} (he : e ∈ diameterEdges P S d) : ClockwiseExtremeAt P (diameterEdges P S d) e e.1 ∨ ClockwiseExtremeAt P (diameterEdges P S d) e e.2

Every maximal-distance edge is clockwise-extreme at one endpoint.

theorem LeanPool.Erdos132N14.clockwiseExtremeAt_unique {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) (S : Finset ι) {d : ℝ} (hd : 0 < d) (hmax : ∀ g ∈ pairs S, P.pairDistance g ≤ d) {e f : ι × ι} {v : ι} (he : e ∈ diameterEdges P S d) (hf : f ∈ diameterEdges P S d) (heIncident : EdgeIncident v e) (hfIncident : EdgeIncident v f) (heExtreme : ClockwiseExtremeAt P (diameterEdges P S d) e v) (hfExtreme : ClockwiseExtremeAt P (diameterEdges P S d) f v) : e = f

A vertex cannot be clockwise-extreme for two different diameter edges.

noncomputable def LeanPool.Erdos132N14.diameterOwner {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) (S : Finset ι) (d : ℝ) (e : ι × ι) : ι

The endpoint to which the Perles argument charges a diameter edge.

Equations

• LeanPool.Erdos132N14.diameterOwner P S d e = if LeanPool.Erdos132N14.ClockwiseExtremeAt P (LeanPool.Erdos132N14.diameterEdges P S d) e e.1 then e.1 else e.2

theorem LeanPool.Erdos132N14.diameterOwner_incident {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) (S : Finset ι) (d : ℝ) (e : ι × ι) : EdgeIncident (diameterOwner P S d e) e

theorem LeanPool.Erdos132N14.diameterOwner_extreme {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) (S : Finset ι) {d : ℝ} (hd : 0 < d) (hmax : ∀ f ∈ pairs S, P.pairDistance f ≤ d) {e : ι × ι} (he : e ∈ diameterEdges P S d) : ClockwiseExtremeAt P (diameterEdges P S d) e (diameterOwner P S d e)

theorem LeanPool.Erdos132N14.diameterOwner_injectiveOn {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) (S : Finset ι) {d : ℝ} (hd : 0 < d) (hmax : ∀ f ∈ pairs S, P.pairDistance f ≤ d) : Set.InjOn (diameterOwner P S d) ↑(diameterEdges P S d)

The diameter owner map is injective on maximal-distance edges.

theorem LeanPool.Erdos132N14.diameterEdges_card_le {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) (S : Finset ι) {d : ℝ} (hd : 0 < d) (hmax : ∀ f ∈ pairs S, P.pairDistance f ≤ d) : (diameterEdges P S d).card ≤ S.card

The number of pairs realizing a positive maximal distance is at most the number of points.

def LeanPool.Erdos132N14.HopfPannwitzLowMultiplicityDistance14 : Prop

Every fourteen-point planar configuration has a realized distance represented by at most fourteen unordered pairs.

Equations

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

theorem LeanPool.Erdos132N14.hopfPannwitzLowMultiplicityDistance14 : HopfPannwitzLowMultiplicityDistance14

The Hopf--Pannwitz low-multiplicity input used by the fourteen-point descent, proved by charging each diameter pair to a unique endpoint.