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 → ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (f : Polynomial ℂ), f = Polynomial.X ^ n - Polynomial.C (↑r ^ n) → ∀ z ∈ Erdos1043.levelSet f, Metric.ediam (connectedComponentIn (Erdos1043.levelSet f) z) < ENNReal.ofReal εSolvedStatement only, no proof