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
If then the component which contains must have diameter , which shows is best possible.
∀ (r : ℝ), 0 ≤ r → r ≤ 1 / 2 → ∀ (f : Polynomial ℂ), f.Monic → f.degree ≥ 1 → (∀ z ∈ f.roots, ‖z‖ ≤ r) → 2 ≤ Metric.ediam (connectedComponentIn (Erdos1043.levelSet f) 0)SolvedStatement only, no proof