Erdős Problem 90: The unit distance problem

Reference: erdosproblems.com/90

noncomputable def Erdos90.unitDistancePairsCount (points : Finset (EuclideanSpace ℝ (Fin 2))) : ℕ

Given a finite set of points, this function counts the number of unordered pairs of distinct points that are at a distance of exactly 1 from each other.

Equations

• Erdos90.unitDistancePairsCount points = (Finset.filter (fun (p : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2)) => dist p.1 p.2 = 1) points.offDiag).card / 2

noncomputable def Erdos90.unitDistanceCounts (n : ℕ) : Set ℕ

The set of all possible numbers of unit distances for a configuration of $n$ points.

Equations

• Erdos90.unitDistanceCounts n = {x : ℕ | ∃ (points : Finset (EuclideanSpace ℝ (Fin 2))) (_ : points.card = n), Erdos90.unitDistancePairsCount points = x}

theorem Erdos90.unitDistanceCounts_BddAbove (n : ℕ) : BddAbove (unitDistanceCounts 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 Erdos90.maxUnitDistances (n : ℕ) : ℕ

The maximum number of unit distances determined by any set of $n$ points in the plane. This function is often denoted as $u(n)$ in combinatorics.

Equations

• Erdos90.maxUnitDistances n = sSup (Erdos90.unitDistanceCounts n)

theorem Erdos90.erdos_90 : (∃ (O : ℕ → ℝ) (_ : O =O[Filter.atTop] fun (n : ℕ) => 1 / Real.log (Real.log ↑n)), (fun (n : ℕ) => ↑(maxUnitDistances n)) = fun (n : ℕ) => ↑n ^ (1 + O n)) ↔ sorry

Does every set of $n$ distinct points in $\mathbb{R}^2$ contain at most $n^{1+O(\frac{1}{\log\log n})}$ many pairs which are distance $1$ apart?