Erdős problem 1048
If is a monic polynomial with all roots satisfying for some , then must have a connected component with diameter ?
Sources
FormalConjectures/ErdosProblems/
1048.lean
Retained formal statement
Pommerenke [Po61] proved the answer is no for , showing that if then has connected components, all with diameter as .
∀ (r : ℝ), 1 < r → ∀ (n : ℕ), 1 ≤ n → ∀ (f : Polynomial ℂ), f = Polynomial.X ^ n - Polynomial.C (↑r ^ n) → {C | ∃ z ∈ Erdos1043.levelSet f, C = connectedComponentIn (Erdos1043.levelSet f) z}.ncard = nSolvedStatement only, no proof