Erdős problem 973
Does there exist a constant such that, for every , there exists a sequence with and for all with ?
Sources
FormalConjectures/ErdosProblems/
973.lean
Retained formal statement
Does there exist a constant such that, for every , there exists a sequence with and for all with ?
This is Problem 7.3 in [Ha74], where it is attributed to Erdős.
True ↔ ∃ C > 1, ∀ n ≥ 2, ∃ z, z 1 = 1 ∧ (∀ i ∈ Finset.Icc 1 n, 1 ≤ ‖z i‖) ∧ ∀ k ∈ Finset.Icc 2 (n + 1), ‖∑ i ∈ Finset.Icc 1 n, z i ^ k‖ < C ^ (-↑n)OpenStatement only, no proof