Erdős problem 973
Does there exist a constant such that, for every , there exists a sequence with and for all with ?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/973.leanTrue ↔ ∃ 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