The Hopf--Pannwitz diameter bound

Hopf and Pannwitz (1934): a set of n points of the plane realises its diameter at most n times. This file proves the bound in the form the main theorem consumes, and in fact proves slightly more: only maximality of D is used, never that D is attained.

Nothing here is claimed as new. The same bound is already in the pool as LeanPool.Erdos132N14.diameterEdges_card_le, proved by Perles charging over an injective map from a linearly ordered index type into ℂ and stated as a bound on the cardinality of a Finset of unordered pairs. This file reproves it over a Finset (ℝ × ℝ), in squared distances and handshake degree-sum form, because pool projects do not import one another; it is a supporting lemma of this development rather than one of its results.

The classical argument deletes a pendant vertex. If a point v has three points of X at squared distance exactly D, then one of the three — the one lying angularly between the other two, seen from v — has no other such partner, so it can be deleted and induction applies.

The angular step is entirely algebraic here. Write A, B, C for the vectors from v to the three points and let X, Y, Z be the cross products A × B, B × C, A × C. Cramer's rule in the plane is the identity Z • B = Y • A + X • C, and comparing squared lengths turns maximality of D into the strict inequality Z < X + Y. A partner w of the middle point satisfies ⟪B, w - v⟫ = |w - v|² / 2 while ⟪A, w - v⟫ and ⟪C, w - v⟫ are at least that, so pairing Cramer's identity with w - v forces |w - v|² ≤ 0, i.e. w = v.

def Erdos132ThreeChain.DiameterAdj (D : ℝ) (p q : Point) : Prop

Adjacency in the diameter graph: distinct points at squared distance exactly D.

Equations

• Erdos132ThreeChain.DiameterAdj D p q = (p ≠ q ∧ Erdos132ThreeChain.sqDist p q = D)

@[instance_reducible]

noncomputable instance Erdos132ThreeChain.decidableDiameterAdj (D : ℝ) : DecidableRel (DiameterAdj D)

Equations

• Erdos132ThreeChain.decidableDiameterAdj D x✝¹ x✝ = Erdos132ThreeChain.decidableDiameterAdj._aux_1 D x✝¹ x✝

theorem Erdos132ThreeChain.diameterAdj_symm (D : ℝ) (p q : Point) : DiameterAdj D p q → DiameterAdj D q p

theorem Erdos132ThreeChain.diameterAdj_irrefl (D : ℝ) (p : Point) : ¬DiameterAdj D p p

theorem Erdos132ThreeChain.IsSqDiameter.pos {X : Finset Point} {D : ℝ} (h : IsSqDiameter X D) : 0 < D

The plane geometry

theorem Erdos132ThreeChain.sqDist_expand (v a w : Point) : sqDist a w = sqDist v a + sqDist v w - 2 * dotp v a w

The squared distance between two points expanded around a third.

theorem Erdos132ThreeChain.dotp_sq_add_cross_sq (v a b : Point) : dotp v a b ^ 2 + cross v a b ^ 2 = sqDist v a * sqDist v b

Lagrange's identity in the plane.

theorem Erdos132ThreeChain.cross_dotp_identity (v a b c w : Point) : cross v a c * dotp v b w = cross v b c * dotp v a w + cross v a b * dotp v c w

Cramer's rule in the plane, paired with a fourth point.

theorem Erdos132ThreeChain.cross_sq_identity (v a b c : Point) : cross v a c ^ 2 * sqDist v b = cross v b c ^ 2 * sqDist v a + cross v a b ^ 2 * sqDist v c + 2 * (cross v b c * cross v a b) * dotp v a c

Cramer's rule in the plane, in squared-length form.

theorem Erdos132ThreeChain.cross_ne_zero {v a b : Point} {D : ℝ} (hD : 0 < D) (hva : sqDist v a = D) (hvb : sqDist v b = D) (hab : sqDist a b ≤ D) (hne : a ≠ b) : cross v a b ≠ 0

Two distinct points at squared distance D from v, no farther than D from each other, are not collinear with v.

theorem Erdos132ThreeChain.middle_no_other_neighbour {v a b c w : Point} {D : ℝ} (hD : 0 < D) (hva : sqDist v a = D) (hvb : sqDist v b = D) (hvc : sqDist v c = D) (hac : a ≠ c) (hX : 0 < cross v a b) (hY : 0 < cross v b c) (hbw : sqDist b w = D) (haw : sqDist a w ≤ D) (hcw : sqDist c w ≤ D) : w = v

The pendant lemma. Let a, b, c sit at squared distance D from v, with b strictly between a and c as seen from v (both cross products positive). If no squared distance among the points involved exceeds D, then the only point at squared distance D from b is v itself.

theorem Erdos132ThreeChain.exists_middle (v a b c : Point) (hab : cross v a b ≠ 0) (hbc : cross v b c ≠ 0) (hac : cross v a c ≠ 0) : 0 < cross v a b ∧ 0 < cross v b c ∨ 0 < cross v c b ∧ 0 < cross v b a ∨ 0 < cross v b a ∧ 0 < cross v a c ∨ 0 < cross v c a ∧ 0 < cross v a b ∨ 0 < cross v a c ∧ 0 < cross v c b ∨ 0 < cross v b c ∧ 0 < cross v c a

Of three points seen from v with no two collinear with v, one lies strictly between the other two. The six alternatives are the three choices of middle point, each in the two possible orientations.

theorem Erdos132ThreeChain.exists_pendant {X : Finset Point} {D : ℝ} (hD : 0 < D) (hmax : ∀ p ∈ X, ∀ q ∈ X, sqDist p q ≤ D) {v a b c : Point} (haX : a ∈ X) (hbX : b ∈ X) (hcX : c ∈ X) (hva : sqDist v a = D) (hvb : sqDist v b = D) (hvc : sqDist v c = D) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) : (∀ w ∈ X, sqDist a w = D → w = v) ∨ (∀ w ∈ X, sqDist b w = D → w = v) ∨ ∀ w ∈ X, sqDist c w = D → w = v

Three points at squared distance D from v inside a set of diameter D force one of the three to have v as its only partner at squared distance D.

Counting

theorem Erdos132ThreeChain.sum_degree_erase {X : Finset Point} {D : ℝ} {b v : Point} (hbX : b ∈ X) (hvX : v ∈ X) (hbv : b ≠ v) (hstar : Finset.filter (DiameterAdj D b) X = {v}) : ∑ u ∈ X, degree (DiameterAdj D) X u = ∑ u ∈ X.erase b, degree (DiameterAdj D) (X.erase b) u + 2

Deleting a pendant vertex removes exactly one edge, i.e. two from the degree sum.

theorem Erdos132ThreeChain.sum_degree_le_of_pendant {X : Finset Point} {D : ℝ} {b v : Point} (hbX : b ∈ X) (hvX : v ∈ X) (hbv : b ≠ v) (hvb : sqDist v b = D) (hstar : ∀ w ∈ X, sqDist b w = D → w = v) (ih : ∑ u ∈ X.erase b, degree (DiameterAdj D) (X.erase b) u ≤ 2 * (X.erase b).card) : ∑ u ∈ X, degree (DiameterAdj D) X u ≤ 2 * X.card

The induction step packaged: a pendant vertex b whose only partner is v.

theorem Erdos132ThreeChain.sum_degree_le {D : ℝ} (hD : 0 < D) (X : Finset Point) (hmax : ∀ p ∈ X, ∀ q ∈ X, sqDist p q ≤ D) : ∑ v ∈ X, degree (DiameterAdj D) X v ≤ 2 * X.card

Hopf--Pannwitz. If every squared distance inside X is at most D > 0, then the graph joining points of X at squared distance exactly D has degree sum at most 2 * #X, that is, at most #X edges.

theorem Erdos132ThreeChain.hopfPannwitz {X : Finset Point} {D : ℝ} (hD : IsSqDiameter X D) : ∑ v ∈ X, degree (DiameterAdj D) X v ≤ 2 * X.card

Hopf--Pannwitz for a diameter. The diameter graph of a finite planar set has at most as many edges as the set has points.