Skip to content

Erdős problem 959

How large can the difference between the largest and second-largest distance multiplicities be among nn planar points?

Sources

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

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

959.lean

Retained formal statement1 of 2

Let AR2A\subseteq \mathbb{R}^2 be a set of size nn and let {d1,,dk}\{d_1,\ldots,d_k\} be the set of distinct distances determined by AA. Let f(d)f(d) be the number of times the distance dd is determined, ordered so that f(d1)f(d2)f(dk)f(d_1)\geq f(d_2)\geq \cdots \geq f(d_k). Estimate max(f(d1)f(d2)),\max (f(d_1)-f(d_2)), where the maximum is taken over all AA of size nn (this is extremalGap n).

The asymptotic order of extremalGap is not known; a natural formalization of "estimate" asks whether it has a well-defined polynomial growth exponent.

FormalConjectures/ErdosProblems/959.leanErdos959.erdos_9591 lineExact file
True ↔ ∃ γ, Filter.Tendsto (fun n => Real.log ↑(Erdos959.extremalGap n) / Real.logn) Filter.atTop (nhds γ)
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page