Erdős problem 228
Does there exist, for all large , a polynomial of degree , with coefficients , such that for all , with the implied constants independent of and ?
Sources
FormalConjectures/ErdosProblems/
228.lean
Retained formal statement
Does there exist, for all large , a polynomial of degree , with coefficients , such that for all , with the implied constants independent of and ?
The answer is yes, proved by Balister, Bollobás, Morris, Sahasrabudhe, and Tiba [BBMST19].
[BBMST19] Balister, P. and BollobÁs, B. and Morris, R. and Sahasrabudhe, J. and Tiba, M., _Flat Littlewood Polynomials Exist_. arXiv:1907.09464 (2019).
True ↔ ∃ c₁ c₂, ∀ᶠ (n : ℕ) in Filter.atTop, ∃ p, p.degree = ↑n ∧ (∀ i ≤ n, p.coeff i = 1 ∨ p.coeff i = -1) ∧ ∀ (z : ℂ), ‖z‖ = 1 → √↑n < c₁ * ‖Polynomial.eval z p‖ ∧ ‖Polynomial.eval z p‖ < c₂ * √↑nSolvedStatement only, no proof