Skip to content

Erdős problem 987

Start work

Clunie [Cl67] proved that there exists an infinite sequence {zν}\{z_\nu\} on the unit circle with Aν≤νA_\nu \le \nu for all ν≥1\nu \ge 1. Translating zν=e(xν)z_\nu = e(x_\nu), the natural domain of xνx_\nu is the half-open unit interval Ico 0 1\mathrm{Ico}\,0\,1, matching the original [Er64b]/[Cl67] statement (any unit complex number is allowed, including z=1z = 1, i.e. x=0x = 0).

Sources

The source's own material, retained exactly.

10 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

987.lean

Retained formal statement3 of 10

Liu [Li69] showed that, for any ϵ>0\epsilon > 0, Ak≫k1−ϵA_k \gg k^{1 - \epsilon} infinitely often under the additional assumption that there are only a finite number of distinct points. Clunie observed in the Mathscinet review of [Li69] that under this assumption in fact Ak=∞A_k = \infty infinitely often (the version stated here).

FormalConjectures/ErdosProblems/987.leanErdos987.erdos_987.variants.finite_distinct_points1 lineExact file
∀ (x : ℕ → ℝ), (∀ (j : ℕ), x j ∈ Set.Ioo 0 1) → (Set.range x).Finite → ∃ᶠ (k : ℕ) in Filter.atTop, Erdos987.A x k = ⊤
SolvedProof has a holelean4external proof

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