Erdős Problem 96

Reference: erdosproblems.com/96

noncomputable def Erdos96.convexUnitDistanceCounts (n : ℕ) : Set ℕ

The set of all possible numbers of unit distances determined by the vertices of a convex $n$-gon.

Equations

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

theorem Erdos96.convexUnitDistanceCounts_bddAbove (n : ℕ) : BddAbove (convexUnitDistanceCounts n)

This lemma confirms that the set of possible unit-distance counts is bounded above, which ensures that taking the supremum (sSup) is a well-defined operation. The trivial upper bound is the total number of pairs of points, $\binom{n}{2}$.

noncomputable def Erdos96.maxConvexUnitDistances (n : ℕ) : ℕ

The maximum number of unit distances determined by the vertices of a convex $n$-gon. This function is often denoted as $U_c(n)$ in combinatorics.

Equations

• Erdos96.maxConvexUnitDistances n = sSup (Erdos96.convexUnitDistanceCounts n)

theorem Erdos96.erdos_96 : True ↔ (fun (n : ℕ) => ↑(maxConvexUnitDistances n)) =O[Filter.atTop] fun (n : ℕ) => ↑n

If $n$ points in $\mathbb{R}^2$ form a convex polygon then there are $O(n)$ many pairs which are distance $1$ apart.