Erdős Problem 92

Reference: erdosproblems.com/92

noncomputable def Erdos92.maxEquidistantPointsAt (x : EuclideanSpace ℝ (Fin 2)) (points : Finset (EuclideanSpace ℝ (Fin 2))) : ℕ

For a given point x and a set of other points, this function finds the maximum number of points that lie on a single circle centered at x. It does this by grouping the other points by their distance to x and finding the size of the largest group.

Equations

• Erdos92.maxEquidistantPointsAt x points = sSup ↑(Finset.image (fun (d : ℝ) => {p ∈ points.erase x | dist x p = d}.card) (Finset.image (dist x) (points.erase x)))

def Erdos92.hasMinEquidistantProperty (k : ℕ) (A : Finset (EuclideanSpace ℝ (Fin 2))) : Prop

This property holds for a set of points A if every point x in A has at least k other points from A that are equidistant from x.

Equations

• Erdos92.hasMinEquidistantProperty k A = (A.Nonempty ∧ ∀ x ∈ A, k ≤ Erdos92.maxEquidistantPointsAt x A)

noncomputable def Erdos92.possible_f_values (n : ℕ) : Set ℕ

The set of all possible values k for which there exists a set of n points satisfying the hasMinEquidistantProperty k. The function f(n) will be the supremum of this set.

Equations

• Erdos92.possible_f_values n = {k : ℕ | ∃ (points : Finset (EuclideanSpace ℝ (Fin 2))) (_ : points.card = n), Erdos92.hasMinEquidistantProperty k points}

theorem Erdos92.possible_f_values_BddAbove (n : ℕ) : BddAbove (possible_f_values n)

A sanity check to ensure the set of possible f(n) values is bounded above. A trivial bound is n-1, since any point can have at most n-1 other points equidistant from it. This ensures sSup is well-defined.

noncomputable def Erdos92.f (n : ℕ) : ℕ

Let $f(n)$ be maximal such that there exists a set $A$ of $n$ points in $\mathbb^2$ in which every $x \in A$ has at least $f(n)$ points in $A$ equidistant from $x$.

Equations

• Erdos92.f n = sSup (Erdos92.possible_f_values n)

theorem Erdos92.erdos_92.variants.weak : (∃ (o : ℕ → ℝ), o =o[Filter.atTop] 1 ∧ ∀ (n : ℕ), ↑(f n) ≤ ↑n ^ o n) ↔ sorry

Is it true that $f(n)\leq n^{o(1)}$?

theorem Erdos92.erdos_92.variants.strong : (∃ c > 0, ∀ (n : ℕ), ↑(f n) ≤ ↑n ^ (c / Real.log (Real.log ↑n))) ↔ sorry

Or even $f(n) < n^{c/\log\log n}$ for some constant $c > 0$?