Erdős Problem 503

Reference: erdosproblems.com/503

theorem Erdos503.erdos_503 (n : ℕ) : IsGreatest {x : ℕ | ∃ (A : Set (EuclideanSpace ℝ (Fin n))) (_ : A.IsIsosceles), A.ncard = x} sorry

What is the size of the largest $A \subseteq \mathbb{R}^n$ such that every three points from $A$ determine an isosceles triangle? That is, for any three points $x$, $y$, $z$ from $A$, at least two of the distances $|x - y|$, $|y - z|$, $|x - z|$ are equal.

theorem Erdos503.erdos_503.variants.R2 : IsGreatest {x : ℕ | ∃ (A : Set (EuclideanSpace ℝ (Fin 2))) (_ : A.IsIsosceles), A.ncard = x} 6

When $n = 2$, the answer is 6 (due to Kelly [ErKe47] - an alternative proof is given by Kovács [Ko24c]).

[ErKe47] Erdős, Paul and Kelly, L. M., Elementary Problems and Solutions: Solutions: E735. Amer. Math. Monthly (1947), 227-229. [Ko24c] Z. Kovács, A note on Erdős's mysterious remark. arXiv:2412.05190 (2024).

theorem Erdos503.erdos_503.variants.R3 : IsGreatest {x : ℕ | ∃ (A : Set (EuclideanSpace ℝ (Fin 3))) (_ : A.IsIsosceles), A.ncard = x} 8

When $n = 3$, the answer is 8 (due to Croft [Cr62]).

[Cr62] Croft, H. T., $9$-point and $7$-point configurations in $3$-space. Proc. London Math. Soc. (3) (1962), 400-424.

theorem Erdos503.erdos_503.variants.upper_bound (n m : ℕ) : m ∈ {x : ℕ | ∃ (A : Set (EuclideanSpace ℝ (Fin n))) (_ : A.IsIsosceles), A.ncard = x} → m ≤ (n + 2).choose 2

The best upper bound known in general is due to Blokhius [Bl84] who showed that $$ |A| \leq \binom{n + 2}{2} $$

[Bl84] Blokhuis, A., Few-distance sets. (1984), iv+70.

theorem Erdos503.erdos_503.variants.lower_bound (n m : ℕ) : m ∈ {x : ℕ | ∃ (A : Set (EuclideanSpace ℝ (Fin n))) (_ : A.IsIsosceles), A.ncard = x} → (n + 1).choose 2 ≤ m

Alweiss has observed a lower bound of $\binom{n + 1}{2}$ follows from considering the subset of $\mathbb{R}^{n + 1}$ formed of all vectors $e_i + e_j$ where $e_i$, $e_j$ are distinct coordinate vectors. This set can be viewed as a subset of some $\mathbb{R}^n$, and is easily checked to have the required property.