Erdős problem 1041 · problems.science

Erdős–Herzog–Piranian Component Lemma (Metric Properties of Polynomials, 1958): If $f$ is a monic degree $n$ polynomial with all roots in the unit disk, then some connected component of $\{z \mid |f(z)| < 1\}$ contains at least two roots with multiplicity.

Sources

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

2 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1041.lean

Retained formal statement1 of 2

Let $f(z) = \prod_{i=1}^{n} (z - z_i) \in \mathbb{C}[x]$ with $|z_i| < 1$ for all $i$ .

Conjecture: Must there always exist a path of length less than 2 in $\{ z \in \mathbb{C} \mid |f(z)| < 1 \}$ which connects two of the roots of $f$ ?

FormalConjectures/ErdosProblems/1041.leanErdos1041.erdos_10418 linesExact file

1∀ (n : ℕ) (f : Polynomial ℂ),2  n ≥ 2 →3    f.natDegree = n →4      f.Monic →5        f.rootSet ℂ ⊆ Metric.ball 0 1 →6          ∃ z₁ z₂,7            ∃ (_ : {z₁, z₂} ≤ f.roots),8              ∃ γ, Set.range ⇑γ ⊆ {z | ‖Polynomial.eval z f‖ < 1} ∧ Erdos1041.length (Set.range ⇑γ) < 2

OpenStatement only, no proof

Sources

Search problems.science