Erdős Problem 1085

Let f_d(n) be minimal such that, in any set of n points in ℝ^d, there exist at most f_d(n) pairs of points which are distance 1 apart. Estimate f_d(n).

Reference: erdosproblems.com/1085

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

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

Equations

• Erdos1085.f d n = ⨆ (s : Finset (EuclideanSpace ℝ (Fin d))), ⨆ (_ : s.card = n), unitDistNum s

theorem Erdos1085.erdos_1085_lower_d2 : ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑n ^ (1 + c / Real.log (Real.log ↑n)) < ↑(f 2 n)

Erdős showed $f_2(n) > n^{1+c/\log\log n}$ for some $c > 0$.

theorem Erdos1085.erdos_1085_upper_d2 : (fun (n : ℕ) => ↑(f 2 n)) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ (4 / 3)

Spencer, Szemerédi, and Trotter showed $f_2(n) = O(n^{4/3})$.

theorem Erdos1085.erdos_1085_lower_d3 : (fun (n : ℕ) => ↑n ^ (4 / 3) * Real.log (Real.log ↑n)) =O[Filter.atTop] fun (n : ℕ) => ↑(f 3 n)

Erdős showed $f_3(n) = Ω(n^{4/3}\log\log n)$.

theorem Erdos1085.erdos_1085_upper_d3 : sorry ↔ (fun (n : ℕ) => ↑(f 3 n)) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ (4 / 3) * Real.log (Real.log ↑n)

Is the $n^{4/3}\log\log n$ lower bound in 3D also an upper bound?.

theorem Erdos1085.erdos_1085_lower_d4_lenz {d : ℕ} (hd : 4 ≤ d) : ∃ (C : ℝ), ∀ (n : ℕ), ↑(d / 2 - 1) / (2 * ↑(d / 2)) * ↑n ^ 2 - C ≤ ↑(f d n)

Lenz showed that, for $d \ge 4$, $f_d(n) \ge \frac{p - 1}{2p} n^2 - O(1)$ where $p = \lfloor\frac d2\rfloor$.

theorem Erdos1085.erdos_1085_upper_d4_erdos {d : ℕ} (hd : 4 ≤ d) : ∃ (g : ℕ → ℝ), Filter.Tendsto g Filter.atTop (nhds 0) ∧ ∀ (n : ℕ), ↑(f d n) ≤ (↑(d / 2 - 1) / (2 * ↑(d / 2)) + g n) * ↑n ^ 2

Erdős showed that, for $d \ge 4$, $f_d(n) \le \left(\frac{p - 1}{2p} + o(1)\right) n^2$ where $p = \lfloor\frac d2\rfloor$.

theorem Erdos1085.erdos_1085_upper_lower_d5_odd {d : ℕ} (hd : 5 ≤ d) (hd_odd : Odd d) : ∃ c₁ > 0, ∃ (c₂ : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ↑(d / 2 - 1) / (2 * ↑(d / 2)) * ↑n ^ 2 + c₁ * ↑n ^ (4 / 3) ≤ ↑(f d n) ∧ ↑(f d n) ≤ ↑(d / 2 - 1) / ↑(d / 2) * ↑n ^ 2 + c₂ * ↑n ^ (4 / 3)

Erdős and Pach showed that, for $d \ge 5$ odd, there exist constants $c_1(d), c_2(d) > 0$ such that $\frac{p - 1}{2p} n^2 - c_1 n^{4/3} ≤ f_d(n) \le \frac{p - 1}{2p} n^2 + c_2 n^{4/3}$ where $p = \lfloor\frac d2\rfloor$.