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 statement2 of 4

Lefmann and Theile [LeTh95] prove a stronger version of this question, that $\sum_i f(u_i)^2 \ll n^3$ under the weaker assumption that no three points are on a line.

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

1∃ C > 0,2  ∀ (P : Finset (EuclideanSpace ℝ (Fin 2))),3    EuclideanGeometry.NonTrilinear ↑P →4      ∑ u ∈ EuclideanGeometry.distanceSet P, ↑(EuclideanGeometry.distanceMultiplicity P u) ^ 2 ≤ C * ↑P.card ^ 3

SolvedStatement only, no proofformal statement reference

Sources

Search problems.science