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 statement1 of 8

A problem of Erdős, Herzog, and Piranian [EHP58].

Pommerenke [Po61] proved the answer is no for $r>1$ , showing that if $f(z)=z^n-r^n$ then $\{ z: \lvert f(z)\rvert \leq 1\}$ has $n$ connected components, all with diameter $\to 0$ as $n\to \infty$ .

FormalConjectures/ErdosProblems/1048.leanErdos1048.erdos_10488 linesExact file

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

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science