Erdős problem 987 · problems.science

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

Sources

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

10 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

987.lean

Retained formal statement2 of 10

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

FormalConjectures/ErdosProblems/987.leanErdos987.erdos_987.parts.ii4 linesExact file

1True ↔2  ∃ x,3    ∃ (_ : ∀ (j : ℕ), x j ∈ Set.Ioo 0 1),4      ∃ 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.

Sources

Search problems.science