Skip to content

Erdős problem 990

Let f=a0++adxdC[x]f=a_0+\cdots+a_dx^d\in \mathbb{C}[x] be a polynomial. Is it true that, if ff has roots z1,,zdz_1,\ldots,z_d with corresponding arguments θ1,,θd[0,2π]\theta_1,\ldots,\theta_d\in [0,2\pi], then for all intervals I[0,2π]I\subseteq [0,2\pi] (#θiI)I2πd(nlogM)1/2, \left\lvert (\# \theta_i \in I) - \frac{\lvert I\rvert}{2\pi}d\right\rvert \ll \left(n\log M\right)^{1/2}, where nn is the number of non-zero coefficients of ff and M=a0++ad(a0ad)1/2. M=\frac{\lvert a_0\rvert+\cdots +\lvert a_d\rvert}{(\lvert a_0\rvert\lvert a_d\rvert)^{1/2}}.

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

990.lean

Retained formal statement4 of 4

Hayman [Ha72b] proved (#θiI)I2πdn1, \left\lvert (\# \theta_i \in I) - \frac{\lvert I\rvert}{2\pi}d\right\rvert \leq n-1, and noted this is essentially sharp since f(x)=(xp1)n1f(x)=(x^{p}-1)^{n-1} has nn non-zero coefficients and has 11 as a positive real zero of multiplicity n1n-1 (although for this ff the parameter MM becomes very large).

FormalConjectures/ErdosProblems/990.leanErdos990.erdos_990.variants.hayman7 linesExact file
∀ (f : Polynomial ℂ),  f.coeff 0 ≠ 0 →    ∀ (α β : ℝ),      0 ≤ α →        α ≤ β →          β ≤ 2 * Real.pi            |↑(Erdos990.rootArgCount f (Set.Icc α β)) - (β - α) / (2 * Real.pi) * ↑f.natDegree| ≤ ↑f.support.card - 1
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page