Skip to content

Erdős problem 509

Start work

Let f(z)∈C[z]f(z) ∈ ℂ[z] be a monic non-constant polynomial. Can the set {z∈C:∣f(z)∣≤1}\{z ∈ ℂ : |f(z)| ≤ 1\} be covered by a set of closed discs the sum of whose radii is ≤2≤ 2?

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

509.lean

Retained formal statement5 of 5

Let f(z)∈C[z]f(z) ∈ ℂ[z] be a monic non-constant polynomial. If it is connected, can the set {z∈C:∣f(z)∣≤1}\{z ∈ ℂ : |f(z)| ≤ 1\} be covered by a set of circles the sum of whose radii is ≤2≤ 2? Solution: True. This is due to Pommerenke.

FormalConjectures/ErdosProblems/509.leanErdos509.erdos_509.variants.Pommerenke_connected6 linesExact file
True ↔  ∀ (f : Polynomial ℂ),    f.Monic →      f.natDegree ≠ 0 →        IsConnected {z | ‖Polynomial.eval z f‖ ≤ 1} →          ∃ ι, Nonempty (Erdos509.BoundedDiscCover {z | ‖Polynomial.eval z f‖ ≤ 1} 2 ι)
SolvedStatement only, no proof