Skip to content

Erdős problem 94

Start work

Suppose nn points in R2\mathbb{R}^2 determine a convex polygon and the set of distances between them is {u1,…,ut}\{u_1,\ldots,u_t\}. Suppose uiu_i appears as the distance between f(ui)f(u_i) many pairs of points. Then ∑if(ui)2≪n3.\sum_i f(u_i)^2 \ll n^3.

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

94.lean

Retained formal statement1 of 4

Suppose nn points in R2\mathbb{R}^2 determine a convex polygon and the set of distances between them is {u1,…,ut}\{u_1,\ldots,u_t\}. Suppose uiu_i appears as the distance between f(ui)f(u_i) many pairs of points. Then ∑if(ui)2≪n3.\sum_i f(u_i)^2 \ll n^3.

In [Er97c] Erdős claims that Fishburn solved this, but gives no reference.

FormalConjectures/ErdosProblems/94.leanErdos94.erdos_944 linesExact file
∃ C > 0,  ∀ (P : Finset (EuclideanSpace ℝ (Fin 2))),    EuclideanGeometry.ConvexIndep ↑P →      ∑ u ∈ EuclideanGeometry.distanceSet P, ↑(EuclideanGeometry.distanceMultiplicity P u) ^ 2 ≤ C * ↑P.card ^ 3
SolvedProof has a holelean4formal statement referenceexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.