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

Question 1:

Is it true that $\limsup_{k \to \infty} A_k = \infty$ ?

Erdős [Er64b] remarks it is "easy to see" that $\limsup_k \sup_n |\sum_{j \le n} e(k x_j)| = \infty$ . Erdős [Er65b] later found a "very easy" proof that $A_k \gg \log k$ for infinitely many $k$ . Clunie [Cl67] proved that $A_k \gg k^{1/2}$ for infinitely many $k$ , which implies the answer is yes (Tao independently found a proof). This is Problem 7.21 in [Ha74].

FormalConjectures/ErdosProblems/987.leanErdos987.erdos_987.parts.i1 lineExact file

1True ↔ ∀ (x : ℕ → ℝ), (∀ (j : ℕ), x j ∈ Set.Ioo 0 1) → Filter.limsup (fun k => Erdos987.A x k) Filter.atTop = ⊤

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