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

Note it is trivial that $\sum f(u_i)=\binom{n}{2}$ .

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

1∀ (P : Finset (EuclideanSpace ℝ (Fin 2))),2  ∑ u ∈ EuclideanGeometry.distanceSet P, EuclideanGeometry.distanceMultiplicity P u = P.card.choose 2

TestStatement only, no proofformal statement reference

Sources

Search problems.science