Erdős Problem 89

Reference: erdosproblems.com/89

noncomputable def Erdos89.minimalDistinctDistances (n : ℕ) : ℕ

The minimum number of distinct distances guaranteed for any set of $n$ points.

Equations

• Erdos89.minimalDistinctDistances n = sInf {x : ℕ | ∃ (points : Finset (EuclideanSpace ℝ (Fin 2))) (_ : points.card = n), ↑(EuclideanGeometry.distinctDistances points) = ↑x}

theorem Erdos89.erdos_89 : (fun (n : ℕ) => ↑n / √(Real.log ↑n)) ≪ fun (n : ℕ) => ↑(minimalDistinctDistances n)

Does every set of $n$ distinct points in $\mathbb{R}^2$ determine $\gg \frac{n}{\sqrt{\log n}}$ many distinct distances?

theorem Erdos89.erdos_89.variants.n_dvd_log_n : (fun (n : ℕ) => ↑n / Real.log ↑n) ≪ fun (n : ℕ) => ↑(minimalDistinctDistances n)

Guth and Katz [GuKa15] proved that there are always $\gg \frac{n}{\log n}$ many distinct distances.

[GuKa15] Guth, Larry and Katz, Nets Hawk, On the Erdős distinct distances problem in the plane. Ann. of Math. (2) (2015), 155-190.

theorem Erdos89.erdos_89.variants.implies_n_dvd_log_n (h : (fun (n : ℕ) => ↑n / √(Real.log ↑n)) ≪ fun (n : ℕ) => ↑(minimalDistinctDistances n)) : (fun (n : ℕ) => ↑n / Real.log ↑n) ≪ fun (n : ℕ) => ↑(minimalDistinctDistances n)

This theorem provides a sanity check, showing that the main conjecture (erdos_89) is strictly stronger than the solved Guth and Katz result. It proves that, trivially, if the lower bound $\frac{n}{\sqrt{\log n}}$ holds, then the weaker lower bound $\frac{n}{\log n}$ must also hold.