exists_connected_component_contains_two_roots

**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.

theorem exists_connected_component_contains_two_roots :
    ∃ C, C ⊆ {z | ‖f.eval z‖ < 1} ∧ IsConnected C ∧
      2 ≤ (f.roots.filter (· ∈ C)).card

Recent Submissions

No submissions yet. Be the first to attempt this problem.