Erdős Problem #1221

The question

erdos_1221.parts.i. Let $a=(a_1,\dots ,a_n)$ be points, ordered consecutively, around the circle (normalised to have circumference $1$). Let $$M_r(a)=\underset{r}{\max }|a_{i+r}-a_i|$$ and $$m_r(a)=\underset{r}{\min }|a_{i+r}-a_i|,$$ where the indices are interpreted in a cyclic fashion and the distance is around the circle (in other words, the maximum and minimum distance between $r$-consecutive points).

Let $${\Lambda }_r=\underset{a}{\inf }\underset{n}{\mathrm{limsup}}n{M}_r(a_1,\dots ,a_n),$$ $${\lambda }_r=\underset{a}{\sup }\underset{n}{\mathrm{liminf}}n{m}_r(a_1,\dots ,a_n),$$ and $${\mu }_r=\underset{a}{\inf }\underset{n}{\mathrm{limsup}}\frac{M_r(a)}{m_r(a)},$$ where the outer $\inf /\sup$ is over all infinite sequences $a=(a_1,\dots )$.

Is it true that $r({\Lambda }_r-1)$, $r(1-{\lambda }_r)$, and $r({\mu }_r-1)$ tend to infinity as $r\to \infty$?

This is the first part, conjectured by de Bruijn and Erdős [dBEr49, §6]. We read ${\Lambda }_r$ and ${\lambda }_r$ as in bigLambda and smallLambda, that is, as printed. The sequences are required to have pairwise distinct points modulo $1$ (see bigLambda). Then $n{M}_r\ge r$ [dBEr49, §1], so $r({\Lambda }_r-1)\to \infty$ would hold trivially. Also $m_r\ge r{m}_1$, so the sequence $a_k={\log }_2(2k-1)$ of [dBEr49, §2] gives ${\lambda }_r\ge r/\log 4$, which exceeds $1$ for $r\ge 2$, so $r(1-{\lambda }_r)$ would be negative for $r\ge 2$. The intended conjectures are about the quantities normalised by $r$, so $r({\Lambda }_r/r-1)={\Lambda }_r-r$, and the first part asks whether ${\Lambda }_r-r\to \infty$.

erdos_1221.parts.ii. Let $a=(a_1,\dots ,a_n)$ be points, ordered consecutively, around the circle (normalised to have circumference $1$). Let $$M_r(a)=\underset{r}{\max }|a_{i+r}-a_i|$$ and $$m_r(a)=\underset{r}{\min }|a_{i+r}-a_i|,$$ where the indices are interpreted in a cyclic fashion and the distance is around the circle (in other words, the maximum and minimum distance between $r$-consecutive points).

Let $${\Lambda }_r=\underset{a}{\inf }\underset{n}{\mathrm{limsup}}n{M}_r(a_1,\dots ,a_n),$$ $${\lambda }_r=\underset{a}{\sup }\underset{n}{\mathrm{liminf}}n{m}_r(a_1,\dots ,a_n),$$ and $${\mu }_r=\underset{a}{\inf }\underset{n}{\mathrm{limsup}}\frac{M_r(a)}{m_r(a)},$$ where the outer $\inf /\sup$ is over all infinite sequences $a=(a_1,\dots )$.

Is it true that $r({\Lambda }_r-1)$, $r(1-{\lambda }_r)$, and $r({\mu }_r-1)$ tend to infinity as $r\to \infty$?

This is the second part. As in the first part, we normalise ${\lambda }_r$ by $r$, so $r(1-{\lambda }_r/r)=r-{\lambda }_r$, and the second part asks whether $r-{\lambda }_r\to \infty$.

erdos_1221.parts.iii. Let $a=(a_1,\dots ,a_n)$ be points, ordered consecutively, around the circle (normalised to have circumference $1$). Let $$M_r(a)=\underset{r}{\max }|a_{i+r}-a_i|$$ and $$m_r(a)=\underset{r}{\min }|a_{i+r}-a_i|,$$ where the indices are interpreted in a cyclic fashion and the distance is around the circle (in other words, the maximum and minimum distance between $r$-consecutive points).

Let $${\Lambda }_r=\underset{a}{\inf }\underset{n}{\mathrm{limsup}}n{M}_r(a_1,\dots ,a_n),$$ $${\lambda }_r=\underset{a}{\sup }\underset{n}{\mathrm{liminf}}n{m}_r(a_1,\dots ,a_n),$$ and $${\mu }_r=\underset{a}{\inf }\underset{n}{\mathrm{limsup}}\frac{M_r(a)}{m_r(a)},$$ where the outer $\inf /\sup$ is over all infinite sequences $a=(a_1,\dots )$.

Is it true that $r({\Lambda }_r-1)$, $r(1-{\lambda }_r)$, and $r({\mu }_r-1)$ tend to infinity as $r\to \infty$?

This is the third part. The quantity ${\mu }_r$ needs no normalisation, and the third part asks whether $r({\mu }_r-1)\to \infty$, that is, whether ${\mu }_r>1+K/r$ for every $K$ and all large $r$.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.ErdosProblems.«1221» (3 statements).

theorem erdos_1221.parts.i :
    ∀ K : ℝ, ∀ᶠ r : ℕ in atTop, ENNReal.ofReal ((r : ℝ) + K) < bigLambda r

theorem erdos_1221.parts.ii :
    ∀ K : ℝ, ∀ᶠ r : ℕ in atTop, smallLambda r < ENNReal.ofReal ((r : ℝ) - K)

theorem erdos_1221.parts.iii :
    ∀ K : ℝ, ∀ᶠ r : ℕ in atTop, ENNReal.ofReal (1 + K / (r : ℝ)) < mu r

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already — check erdosproblems.com/1221. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• erdosproblems.com/1221
• [dBEr49] de Bruijn, N. G. and Erdős, P., Sequences of points on a circle. Nederl. Akad. Wetensch., Proc. (1949), 14-17 = Indagationes Math. 11 (1949), 46-49. PDF

Source and licence

Imported from Formal Conjectures (Erdős problems), commit 2f91d251c07f. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.