Erdős problem 1041
Erdős–Herzog–Piranian Component Lemma (Metric Properties of Polynomials, 1958): If is a monic degree polynomial with all roots in the unit disk, then some connected component of contains at least two roots with multiplicity.
Sources
FormalConjectures/ErdosProblems/
1041.lean
Retained formal statement
Erdős–Herzog–Piranian Component Lemma (Metric Properties of Polynomials, 1958): If is a monic degree polynomial with all roots in the unit disk, then some connected component of contains at least two roots with multiplicity.
See p. 139, above Problem 5: [EHP58] Erdős, P. and Herzog, F. and Piranian, G., _Metric properties of polynomials_. J. Analyse Math. (1958), 125-148.
∀ (n : ℕ) (f : Polynomial ℂ), n ≥ 2 → f.natDegree = n → f.Monic → f.rootSet ℂ ⊆ Metric.ball 0 1 → ∃ C ⊆ {z | ‖Polynomial.eval z f‖ < 1}, IsConnected C ∧ 2 ≤ (Multiset.filter (fun x => x ∈ C) f.roots).cardSolvedStatement only, no proof