Erdős problem 94

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

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

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

Source providers

Erdős Problems1
locator only
Formal Conjectures4
statement retained
VibeMathed0
not observed here
PLBY Lean proofs1
no statement retained
Jayyhk Erdős Lean1
no statement retained
William Blair Lean proofs0
not observed here
Erdős AI contributions wiki1
no statement retained
GPT-Erdős0
not observed here

Referenced paths

FormalConjectures/
- ErdosProblems/
  - 94.lean4