Erdős Problem 119

Reference: erdosproblems.com/119

noncomputable def Erdos119.p (z : ℕ → ℂ) (n : ℕ) : ℂ → ℂ

Let $z_i$ be an infinite sequence of complex numbers such that $|z_i| = 1$ for all $i \geq 1$. For $n \geq 1$ let $p_n(z) = \prod_{i \leq n} (z - z_i)$.

Equations

• Erdos119.p z n w = ∏ i ∈ Finset.range n, (w - z i)

noncomputable def Erdos119.M (z : ℕ → ℂ) (n : ℕ) : ℝ

Let $M_n = \max_{|z| = 1} |p_n(z)|$.

Equations

• Erdos119.M z n = sSup {x : ℝ | ∃ (w : ℂ) (_ : ‖w‖ = 1), ‖Erdos119.p z n w‖ = x}

theorem Erdos119.erdos_119_1 : (∀ (z : ℕ → ℂ), (∀ (i : ℕ), ‖z i‖ = 1) → Filter.limsup (fun (n : ℕ) => ↑(M z n)) Filter.atTop = ⊤) ↔ True

Question 1:

Is it true that $\limsup M_n = \infty$?

Wagner [Wa80] proved that there is some $c > 0$ with $M_n > (\log n)^c$ infintely often.

[Wa80] Wagner, Gerold, On a problem of {E}rdős in {D}iophantine approximation. Bull. London Math. Soc. (1980), 81--88.

theorem Erdos119.erdos_119_2 : (∀ (z : ℕ → ℂ), (∀ (i : ℕ), ‖z i‖ = 1) → ∃ (c : ℝ) (_ : c > 0), Infinite ↑{n : ℕ | M z n > ↑n ^ c}) ↔ True

Question 2:

Is it true that there exists $c > 0$ such that for infinitely many $n$ we have $M_n > n^c$?

Beck [Be91] proved that there exists some $c > 0$ such that $\max_{n \leq N} M_n > N^c$.

[Be91] Beck, J., The modulus of polynomials with zeros on the unit circle: A problem of Erdős. Annals of Math. (1991), 609-651.

theorem Erdos119.erdos_119_3 : (∀ (z : ℕ → ℂ), (∀ (i : ℕ), ‖z i‖ = 1) → ∃ (c : ℝ) (_ : c > 0), ∀ᶠ (n : ℕ) in Filter.atTop, ∑ k ∈ Finset.range n, M z k > ↑n ^ (1 + c)) ↔ sorry

Question 3:

Is it true that there exists $c > 0$ such that, for all large $n$, $\sum_{k \leq n} M_k > n^{1 + c}$?