Erdős problem 94 · problems.science

Suppose $n$ points in $\mathbb{R}^2$ determine a convex polygon and the set of distances between them is $\{u_1,\ldots,u_t\}$ . Suppose $u_i$ appears as the distance between $f(u_i)$ many pairs of points. Then $\sum_i f(u_i)^2 \ll n^3.$

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

94.lean

Retained formal statement3 of 4

Erdős and Fishburn also make the stronger conjecture that $\sum f(u_i)^2$ is maximal for the regular $n$ -gon (for large enough $n$ ).

FormalConjectures/ErdosProblems/94.leanErdos94.erdos_94.variants.regular_ngon7 linesExact file

1∀ᶠ (n : ℕ) in Filter.atTop,2  ∀ (P : Finset (EuclideanSpace ℝ (Fin 2))),3    P.card = n →4      EuclideanGeometry.ConvexIndep ↑P →5        ∑ u ∈ EuclideanGeometry.distanceSet P, ↑(EuclideanGeometry.distanceMultiplicity P u) ^ 2 ≤6          ∑ u ∈ EuclideanGeometry.distanceSet (Erdos94.regularNGon n),7            ↑(EuclideanGeometry.distanceMultiplicity (Erdos94.regularNGon n) u) ^ 2

OpenStatement only, no proofformal statement reference

Sources

Search problems.science