Erdős problem 1047
Let be a monic polynomial with distinct roots, and let be a constant small enough such that has distinct connected components.
Sources
FormalConjectures/ErdosProblems/
1047.lean
Retained formal statement
Let be a monic polynomial with distinct roots, and let be a constant small enough such that has distinct connected components.
Must all these components be convex?
A question of Grunsky, which was reported by Erdős, Herzog, and Piranian [EHP58].
The answer is no, as shown by Pommerenke [Po61], who showed that, if is sufficiently large, and where is sufficiently close to , then has two components, and the component which contains is not convex.
False ↔ ∀ (f : Polynomial ℂ) (m : ℕ) (c : ℝ), f.Monic → (f.rootSet ℂ).ncard = m → 0 < c → (Erdos1047.componentsIn (Erdos1047.sublevelSet f c)).ncard = m → ∀ t ∈ Erdos1047.componentsIn (Erdos1047.sublevelSet f c), Convex ℝ tSolvedStatement only, no proof