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
Hayman [Ha72b] proved and noted this is essentially sharp since has non-zero coefficients and has as a positive real zero of multiplicity (although for this the parameter becomes very large).
∀ (f : Polynomial ℂ), f.coeff 0 ≠ 0 → ∀ (α β : ℝ), 0 ≤ α → α ≤ β → β ≤ 2 * Real.pi → |↑(Erdos990.rootArgCount f (Set.Icc α β)) - (β - α) / (2 * Real.pi) * ↑f.natDegree| ≤ ↑f.support.card - 1SolvedStatement only, no proof