Erdős Problem 1082

Reference: erdosproblems.com/1082

noncomputable def Erdos1082.distinctDistances (points : Finset (EuclideanSpace ℝ (Fin 2))) : ℕ

Given a finite set of points in the plane, we define the number of distinct distances between pairs of points.

TODO(csonne): Remove this once formal conjectures is bumped.

Equations

• Erdos1082.distinctDistances points = (Finset.image (fun (pair : EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2)) => dist pair.1 pair.2) points.offDiag).card

noncomputable def Erdos1082.distinctDistancesFrom (points : Finset (EuclideanSpace ℝ (Fin 2))) (pt : EuclideanSpace ℝ (Fin 2)) : ℕ

The number of distinct distances from a finite set points to a point pt.

TODO(csonne): Move to ForMathlib.

Equations

• Erdos1082.distinctDistancesFrom points pt = (Finset.image (fun (x : EuclideanSpace ℝ (Fin 2)) => dist x pt) points).card

theorem Erdos1082.erdos_1082a : sorry ↔ ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), EuclideanGeometry.NonTrilinear A.toSet → A.card / 2 ≤ distinctDistances A

Let $A\subset \mathbb{R}^2$ be a set of $n$ points with no three on a line. Does $A$ determine at least $\lfloor n/2\rfloor$ distinct distances?

theorem Erdos1082.erdos_1082b : False ↔ ∀ (A : Finset (EuclideanSpace ℝ (Fin 2))), A.Nonempty → EuclideanGeometry.NonTrilinear A.toSet → ∃ (a : EuclideanSpace ℝ (Fin 2)) (_ : a ∈ A), A.card / 2 ≤ distinctDistancesFrom A a - 1

Let $A\subset \mathbb{R}^2$ be a set of $n$ points with no three on a line. Must there exist a single point from which there are at least $\lfloor n/2\rfloor$ distinct distances?

This question has been answered negatively by Xichuan in the comments, who gave a set of $42$ points in $\mathbb{R}^2$, with no three on a line, such that each point determines only $20$ distinct distances.

A smaller counterexample has been formalised here: it comprised of $8$ points, where each point only determines $3$ distances.