Skip to content

Erdős problem 1150

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

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1150.lean

Retained formal statement1 of 2

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

FormalConjectures/ErdosProblems/1150.leanErdos1150.erdos_11506 linesExact file
True ↔  ∃ c > 0,    ∀ᶠ (n : ℕ) in Filter.atTop,      ∀ (P : Polynomial ℂ),        (∀ i ≤ P.natDegree, P.coeff i = -1 ∨ P.coeff i = 1) →          P.natDegree = n → ⨆ z, ‖Polynomial.eval (↑z) P‖ > (1 + c) * √↑n
OpenStatement only, no proof