Erdős problem 987
Clunie [Cl67] proved that there exists an infinite sequence on the unit circle with for all . Translating , the natural domain of is the half-open unit interval , matching the original [Er64b]/[Cl67] statement (any unit complex number is allowed, including , i.e. ).
Sources
FormalConjectures/ErdosProblems/
987.lean
Clunie [Cl67] proved that there exists an infinite sequence on the unit circle with for all . Translating , the natural domain of is the half-open unit interval , matching the original [Er64b]/[Cl67] statement (any unit complex number is allowed, including , i.e. ).
Note: erdosproblems.com/987 phrases the problem with the *open* interval , which excludes and is strictly stronger than what [Er64b]/[Cl67] state; we align with the original papers here. The shifted-vdc variant under the open interval is preserved as linear_upper_bound_clunie.
∃ x, ∃ (_ : ∀ (j : ℕ), x j ∈ Set.Ico 0 1), ∀ (k : ℕ), 1 ≤ k → Erdos987.A x k ≤ ↑↑k