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 statement2 of 10

Question 2 (parts.ii): Is it possible for Ak=o(k)A_k = o(k)? Yes — there exists a sequence (xn)∈(0,1)(x_n) \in (0, 1) and a bound b(k)=o(k)b(k) = o(k) with Axk≤bkA x k \le b k eventually. A corollary of sqrt_log_upper_bound (which gives a klog⁡k\sqrt{k \log k} bound) plus the asymptotic klog⁡k=o(k)\sqrt{k \log k} = o(k).

FormalConjectures/ErdosProblems/987.leanErdos987.erdos_987.parts.ii4 linesExact file
True ↔  ∃ x,    ∃ (_ : ∀ (j : ℕ), x j ∈ Set.Ioo 0 1),      ∃ b, (b =o[Filter.atTop] fun k => ↑k) ∧ ∀ᶠ (k : ℕ) in Filter.atTop, Erdos987.A x k ≤ ↑(b 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.