Erdős problem 990
Let be a polynomial. Is it true that, if has roots with corresponding arguments , then for all intervals where is the number of non-zero coefficients of and
Sources
FormalConjectures/ErdosProblems/
990.lean
Retained formal statement
Erdős and Turán [ErTu50] proved such an upper bound with replaced by .
∃ C, ∀ (f : Polynomial ℂ), f.coeff 0 ≠ 0 → ∀ (α β : ℝ), 0 ≤ α → α ≤ β → β ≤ 2 * Real.pi → |↑(Erdos990.rootArgCount f (Set.Icc α β)) - (β - α) / (2 * Real.pi) * ↑f.natDegree| ≤ C * √(↑f.natDegree * Real.log (Erdos990.M f))SolvedStatement only, no proof