Erdős problem 1048

If $f\in \mathbb{C}[x]$ is a monic polynomial with all roots satisfying $\lvert z\rvert \leq r$ for some $r<2$ , then must $\{ z: \lvert f(z)\rvert <1\}$ have a connected component with diameter $>2-r$ ?

Sources

The source's own material, retained exactly.

8 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1048.lean

Retained formal statement3 of 8

If $0\leq r\leq 1/2$ then the component which contains $0$ must have diameter $\geq 2$ , which $f(z)=z^n$ shows is best possible.

FormalConjectures/ErdosProblems/1048.leanErdos1048.erdos_1048.variants.diam_ge_two_is_best1 lineExact file

1∀ (n : ℕ), 1 ≤ n → Metric.ediam (connectedComponentIn (Erdos1043.levelSet (Polynomial.X ^ n)) 0) = 2

SolvedStatement only, no proof