Erdős Problem 519

References:

• erdosproblems.com/519
• [Er61] Erdős, Paul, Some unsolved problems. Magyar Tud. Akad. Mat. Kutató Int. Közl. (1961), 221-254.
• [Er65b] Erdős, Paul, Some recent advances and current problems in number theory. Lectures on Modern Mathematics, Vol. III (1965), 196-244.
• [Bi94] Biró, A., On a problem of Turán concerning sums of powers of complex numbers. Acta Math. Hungar. (1994), 209-216.
• [Bi00] Biró, András, An improved estimate in a power sum problem of Turán. Indag. Math. (N.S.) (2000), 343-358.
• [Bi00b] Biró, A., An upper estimate in Turán's pure power sum problem. Indag. Math. (N.S.) (2000), 499--508.
• [At61b] Atkinson, F. V., On sums of powers of complex numbers. Acta Math. Acad. Sci. Hungar. (1961), 185-188.

noncomputable def Erdos519.powerSum {n : ℕ} (z : Fin n → ℂ) (k : ℕ) : ℂ

The $k$th power sum of a finite sequence of complex numbers.

Equations

• Erdos519.powerSum z k = ∑ i : Fin n, z i ^ k

theorem Erdos519.erdos_519 : True ↔ ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ) (hn : 0 < n) (z : Fin n → ℂ), z ⟨0, hn⟩ = 1 → ∃ (k : Fin n), c < ‖powerSum z (↑k + 1)‖

Let $z_1,\ldots,z_n\in \mathbb{C}$ with $z_1=1$. Must there exist an absolute constant $c>0$ such that [ \max_{1\leq k\leq n}\left\lvert \sum_{i}z_i^k\right\rvert>c? ]

Atkinson proved that $c=1/6$ suffices.