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
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/990.leanFalse ↔ ∃ C, ∀ (f : Polynomial ℂ), f.coeff 0 ≠ 0 → ∀ (α β : ℝ), 0 ≤ α → α ≤ β → β ≤ 2 * Real.pi → |↑(Erdos990.rootArgCount f (Set.Icc α β)) - (β - α) / (2 * Real.pi) * ↑f.natDegree| ≤ C * √(↑f.support.card * Real.log (Erdos990.M f))Proof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:990 - PLBY Lean proofs
ErdosProblems.Erdos990 - PLBY Lean proofs
ErdosProblems.Erdos990b
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
Formalization
- Machine
AI standalone
- Machine
construction
- Machine
- People
- Reported outcome