Erdős Problem 1150

Reference: erdosproblems.com/1150

theorem Erdos1150.erdos_1150 : sorry ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (P : Polynomial ℂ), (∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1) → P.natDegree = n → ⨆ (z : ↑(Metric.sphere 0 1)), ‖Polynomial.eval (↑z) P‖ > (1 + c) * √↑n

Is there some constant $c > 0$ such that, for all large enough $n$ and all polynomials $P$ of degree $n$ with coefficients in $\{-1, 1\}$, $$\max_{|z|=1} |P(z)| > (1 + c) \sqrt{n}?$$

theorem Erdos1150.erdos_1150.parseval_lower_bound (P : Polynomial ℂ) (n : ℕ) (hcoeff : ∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1) (hdeg : P.natDegree = n) : ⨆ (z : ↑(Metric.sphere 0 1)), ‖Polynomial.eval (↑z) P‖ ≥ √(↑n + 1)

The trivial lower bound from Parseval's identity: for any polynomial $P$ of degree $n$ with coefficients in $\{-1, 1\}$, we have $\max_{|z|=1} |P(z)| \geq \sqrt{n+1}$.

This follows from Parseval's identity: $$\frac{1}{2\pi} \int_0^{2\pi} |P(e^{i\theta})|^2 d\theta = \sum_{k=0}^{n} |a_k|^2 = n+1$$ since each $|a_k|^2 = 1$.