Erdős Problem 973

References:

• erdosproblems.com/973
• [Er92f] Erdős, L., On some problems of {P}. Turán concerning power sums of complex numbers. Acta Math. Hungar. (1992), 11--24.
• [Ha74] Hayman, W. K., Research problems in function theory: new problems. (1974), 155--180.
• [Tu84b] Turán, Paul, On a new method of analysis and its applications. (1984), xvi+584.

theorem Erdos973.erdos_973 : sorry ↔ ∃ 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)

Does there exist a constant $C>1$ such that, for every $n\geq 2$, there exists a sequence $z_i\in \mathbb{C}$ with $z_1=1$ and $\lvert z_i\rvert \geq 1$ for all $1\leq i\leq n$ with $\max_{2\leq k\leq n+1}\left\lvert \sum_{1\leq i\leq n}z_i^k\right\rvert < C^{-n}$?

This is Problem 7.3 in [Ha74], where it is attributed to Erdős.

theorem Erdos973.erdos_973.variants.le_one : ∃ C > 1, ∀ n ≥ 2, ∃ (z : ℕ → ℂ), z 1 = 1 ∧ (∀ i ∈ Finset.Icc 1 n, ‖z i‖ ≤ 1) ∧ ∀ k ∈ Finset.Icc 2 (n + 1), ‖∑ i ∈ Finset.Icc 1 n, z i ^ k‖ < C ^ (-↑n)

Erdős proved (as described on p.35 of [Tu84b]) that such a sequence does exist with $\lvert z_i\rvert\leq 1$. Indeed, Erdős' construction gives a value of $C\approx 1.32$.

theorem Erdos973.erdos_973.variants.m2_bounds (n : ℕ) : n ≥ 2 → ∀ (M_2 : ℝ), IsGLB {M : ℝ | ∃ (z : ℕ → ℂ), (∀ j ∈ Finset.Icc 1 n, ‖z j‖ ≤ 1) ∧ (∃ j ∈ Finset.Icc 1 n, ‖z j‖ = 1) ∧ ∃ k ∈ Finset.Icc 2 (n + 1), M = ‖∑ j ∈ Finset.Icc 1 n, z j ^ k‖ ∧ ∀ m ∈ Finset.Icc 2 (n + 1), ‖∑ j ∈ Finset.Icc 1 n, z j ^ m‖ ≤ M} M_2 → 1.746 ^ (-↑n) < M_2 ∧ M_2 < 1.745 ^ (-↑n)

In [Er92f] (a different) Erdős refines this analysis, proving that if $M_2=\min_{z_j} \max_{2\leq k\leq n+1} \left\lvert \sum_{1\leq j\leq n}z_j^k\right\rvert$ where the minimum is taken over all $z_j\in \mathbb{C}$ with $\max \lvert z_j\rvert=1$, then $(1.746)^{-n} < M_2 < (1.745)^{-n}$.

theorem Erdos973.erdos_973.variants.tang : ∃ (f : ℕ → ℝ), (f =o[Filter.atTop] fun (x : ℕ) => 1) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (z : ℕ → ℂ), (∀ i ∈ Finset.Icc 1 n, 1 ≤ ‖z i‖) → ∃ k ∈ Finset.Icc 2 (n + 1), ‖∑ i ∈ Finset.Icc 1 n, z i ^ k‖ ≥ (2 * Real.exp 1) ^ (-(1 + f n) * ↑n)

Tang notes in the comments that Theorem 6.1 of [Tu84b] implies that, if $\lvert z_i\rvert \geq 1$ for all $i$, then $\max_{2\leq k\leq n+1}\left\lvert \sum_{1\leq i\leq n}z_i^k\right\rvert \geq (2e)^{-(1+o(1))n}$.