Erdős problem 509
Let be a monic non-constant polynomial. Can the set be covered by a set of closed discs the sum of whose radii is ?
Sources
FormalConjectures/ErdosProblems/
509.lean
Retained formal statement
Let f(z) ∈ ℂ[z] be a monic non-constant polynomial. Can the set \{z ∈ ℂ : |f(z)| ≤ 1\} be covered by a set of closed discs the sum of whose radii is ≤ 2.59? Solution: True. This is due to Pommerenke.
True ↔ ∀ (f : Polynomial ℂ), f.Monic → f.natDegree ≠ 0 → ∃ ι, Nonempty (Erdos509.BoundedDiscCover {z | ‖Polynomial.eval z f‖ ≤ 1} 2.59 ι)SolvedStatement only, no proof