Erdős Problem 1084

Reference: erdosproblems.com/1084

Let f_2(n) be the maximum number of pairs of points at distance exactly 1 among any set of n points in ℝ², under the condition that all pairwise distances are at least 1.

Estimate the growth of f_2(n).

Status: open.

noncomputable def Erdos1084.f (d n : ℕ) : ℕ

The maximal number of pairs of points which are distance 1 apart that a set of n 1-separated points in ℝ^d make.

Equations

• Erdos1084.f d n = ⨆ (s : Finset (EuclideanSpace ℝ (Fin d))), ⨆ (_ : s.card = n), ⨆ (_ : Metric.IsSeparated' 1 ↑s), unitDistNum s

theorem Erdos1084.erdos_1084.variants.upper_d1 {n : ℕ} : f 1 n = n - 1

It is easy to check that $f_1(n) = n - 1$.

theorem Erdos1084.erdos_1084.variants.easy_upper_d2 {n : ℕ} (hn : n ≠ 0) : f 2 n < 3 * n

It is easy to check that $f_2(n) < 3n$.

theorem Erdos1084.erdos_1084.variants.upper_d2 : ∃ c > 0, ∀ n > 0, ↑(f 2 n) < 3 * ↑n - c * √↑n

Erdős showed that there is some constant $c > 0$ such that $f_2(n) < 3n - c n^{1/2}$.

theorem Erdos1084.erdos_1084.variants.triangular_optimal_d2 {n : ℕ} : f 2 (3 * n ^ 2 + 3 * n + 1) = 9 * n ^ 2 + 3 * n

Erdős conjectured that the triangular lattice is best possible in 2D, in particular that $f_2(3n^2 + 3n + 1) < 9n^2 + 3n$.

Note: in [Er75f] is read $9n^2 + 6n$, but this seems to be a typo.

theorem Erdos1084.erdos_1084.variants.upper_lower_d3 : ∃ (c₁ : ℝ), ∃ c₂ > 0, ∀ᶠ (n : ℕ) in Filter.atTop, 6 * ↑n - c₁ * ↑n ^ (2 / 3) ≤ ↑(f 3 n) ∧ ↑(f 3 n) ≤ 6 * ↑n - c₂ * ↑n ^ (2 / 3)

Erdős claims the existence of two constants $c_1, c_2 > 0$ such that $6n - c_1 n^{2/3} ≤ f_3(n) \le 6n - c_2 n^{2/3}$.