/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilErdős Problem 92
open Filteropen scoped EuclideanGeometry
namespace Erdos92
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.
noncomputable def maxEquidistantPointsAt (x : ℝ²) (points : Finset ℝ²) : ℕ :=
letI otherPoints := points.erase x
letI distances := otherPoints.image (dist x)
sSup (distances.image fun d ↦ (otherPoints.filter fun p ↦ dist x p = d).card)
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.
def hasMinEquidistantProperty (k : ℕ) (A : Finset ℝ²) : Prop :=
A.Nonempty ∧ ∀ x ∈ A, k ≤ maxEquidistantPointsAt x A
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.
noncomputable def possible_f_values (n : ℕ) : Set ℕ :=
{k | ∃ (points : Finset ℝ²) (_ : points.card = n), hasMinEquidistantProperty k points}
A sanity check to ensure the set of possible f(n) values is bounded above. A trivial bound is
n, since the points equidistant from any x form a subset of the other n - 1 points.
This ensures sSup is well-defined.
@[category test, AMS 52]
theorem possible_f_values_BddAbove (n : ℕ) : BddAbove (possible_f_values n) := n:ℕ⊢ BddAbove (possible_f_values n)
n:ℕk:ℕhk:k ∈ possible_f_values n⊢ k ≤ n
n:ℕk:ℕpoints:Finset ℝ²hcard:points.card = nhall:∀ x ∈ points, k ≤ maxEquidistantPointsAt x pointsx:ℝ²hx:x ∈ points⊢ k ≤ n
n:ℕk:ℕpoints:Finset ℝ²hcard:points.card = nhall:∀ x ∈ points, k ≤ maxEquidistantPointsAt x pointsx:ℝ²hx:x ∈ points⊢ maxEquidistantPointsAt x points ≤ n
n:ℕk:ℕpoints:Finset ℝ²hcard:points.card = nhall:∀ x ∈ points, k ≤ maxEquidistantPointsAt x pointsx:ℝ²hx:x ∈ points⊢ sSup ↑(Finset.image (fun d => {p ∈ points.erase x | dist x p = d}.card) (Finset.image (dist x) (points.erase x))) ≤ n
n:ℕk:ℕpoints:Finset ℝ²hcard:points.card = nhall:∀ x ∈ points, k ≤ maxEquidistantPointsAt x pointsx:ℝ²hx:x ∈ pointsm:ℕhm:m ∈ ↑(Finset.image (fun d => {p ∈ points.erase x | dist x p = d}.card) (Finset.image (dist x) (points.erase x)))⊢ m ≤ n
n:ℕk:ℕpoints:Finset ℝ²hcard:points.card = nhall:∀ x ∈ points, k ≤ maxEquidistantPointsAt x pointsx:ℝ²hx:x ∈ pointsm:ℕhm:∃ a ∈ Finset.image (dist x) (points.erase x), {p ∈ points.erase x | dist x p = a}.card = m⊢ m ≤ n
n:ℕk:ℕpoints:Finset ℝ²hcard:points.card = nhall:∀ x ∈ points, k ≤ maxEquidistantPointsAt x pointsx:ℝ²hx:x ∈ pointsd:ℝhd:d ∈ Finset.image (dist x) (points.erase x)⊢ {p ∈ points.erase x | dist x p = d}.card ≤ n
calc ((points.erase x).filter fun p => dist x p = d).card
≤ (points.erase x).card := Finset.card_filter_le _ _
_ ≤ points.card := Finset.card_erase_le
_ = n := hcard
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$.
noncomputable def f (n : ℕ) : ℕ := sSup <| possible_f_values n
Is it true that $f(n)\leq n^{o(1)}$?
@[category research open, AMS 52]
theorem erdos_92.variants.weak : answer(sorry) ↔ ∃ o : ℕ → ℝ,
o =o[atTop] (1 : ℕ → ℝ) ∧ ∀ n, (f n : ℝ) ≤ n^(o n) := ⊢ True ↔ ∃ o, o =o[atTop] 1 ∧ ∀ (n : ℕ), ↑(f n) ≤ ↑n ^ o n
All goals completed! 🐙
Or even $f(n) < n^{c/\log\log n}$ for some constant $c > 0$?
@[category research open, AMS 52]
theorem erdos_92.variants.strong : answer(sorry) ↔
∃ c > 0, ∀ᶠ n in atTop, (f n : ℝ) ≤ n^(c / (n : ℝ).log.log) := ⊢ True ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in atTop, ↑(f n) ≤ ↑n ^ (c / Real.log (Real.log ↑n))
All goals completed! 🐙
-- TODO(firsching): formalize the rest of the remarks
end Erdos92