Erdős Problem 100

References:

• erdosproblems.com/100
• [Kanold](No references found)
• [GuKa15](Guth, Larry and Katz, Nets Hawk, On the Erd\H{o}s distinct distances problem in the plane. Ann. of Math. (2) (2015), 155-190.)
• [Piepmeyer](No references found)

def Erdos100.DistancesSeparated (A : Finset (EuclideanSpace ℝ (Fin 2))) : Prop

If two distances in A differ, they differ by at least 1.

Equations

• Erdos100.DistancesSeparated A = ∀ (p₁ q₁ p₂ q₂ : EuclideanSpace ℝ (Fin 2)), p₁ ∈ A → q₁ ∈ A → p₂ ∈ A → q₂ ∈ A → dist p₁ q₁ ≠ dist p₂ q₂ → |dist p₁ q₁ - dist p₂ q₂| ≥ 1

theorem Erdos100.erdos_100 : sorry ↔ ∃ C > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → DistancesSeparated A → Metric.diam ↑A > C * ↑n

Is the diameter of $A$ at least $Cn$ for some constant $C > 0$?

theorem Erdos100.erdos_100_strong : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → DistancesSeparated A → Metric.diam ↑A ≥ ↑n - 1

Stronger conjecture: diameter $\geq n - 1$ for sufficiently large $n$.

theorem Erdos100.erdos_100_kanold : ∃ C > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → DistancesSeparated A → Metric.diam ↑A ≥ ↑n ^ (3 / 4)

From [Kanold]: diameter $\geq n^{3/4}$. TODO: find reference

theorem Erdos100.erdos_100_guth_katz : ∃ C > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = n → DistancesSeparated A → Metric.diam ↑A ≥ C * ↑n / Real.log ↑n

From [GuKa15]: diameter $\gg n / \log n$.

theorem Erdos100.erdos_100_piepmeyer : ∃ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.card = 9 ∧ DistancesSeparated A ∧ Metric.diam ↑A < 5

From [Piepmeyer]: 9 points with diameter $< 5$. TODO: find reference