Erdős problem 1041

Erdős–Herzog–Piranian Component Lemma (Metric Properties of Polynomials, 1958): If $f$ is a monic degree $n$ polynomial with all roots in the unit disk, then some connected component of $\{z \mid |f(z)| < 1\}$ contains at least two roots with multiplicity.

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1041.lean

Retained formal statement2 of 2

Erdős–Herzog–Piranian Component Lemma (Metric Properties of Polynomials, 1958): If $f$ is a monic degree $n$ polynomial with all roots in the unit disk, then some connected component of $\{z \mid |f(z)| < 1\}$ 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.

FormalConjectures/ErdosProblems/1041.leanErdos1041.exists_connected_component_contains_two_roots6 linesExact file

1∀ (n : ℕ) (f : Polynomial ℂ),2  n ≥ 2 →3    f.natDegree = n →4      f.Monic →5        f.rootSet ℂ ⊆ Metric.ball 0 1 →6          ∃ C ⊆ {z | ‖Polynomial.eval z f‖ < 1}, IsConnected C ∧ 2 ≤ (Multiset.filter (fun x => x ∈ C) f.roots).card

SolvedStatement only, no proof