Erdős problem 1048 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

8 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1048.lean

Retained formal statement8 of 8

On the other hand, if $0<r\leq 1$ , then the answer is yes, as also shown by Pommerenke [Po61].

FormalConjectures/ErdosProblems/1048.leanErdos1048.erdos_1048.variants.r_le_one9 linesExact file

1∀ (r : ℝ),2  0 < r →3    r ≤ 1 →4      ∀ (f : Polynomial ℂ),5        f.Monic →6          f.degree ≥ 1 →7            (∀ z ∈ f.roots, ‖z‖ ≤ r) →8              ∃ z ∈ Erdos1048.openLevelSet f,9                ENNReal.ofReal (2 - r) < Metric.ediam (connectedComponentIn (Erdos1048.openLevelSet f) z)

SolvedStatement only, no proof

Sources

Search problems.science