Skip to content

Erdős problem 1041

Start work

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

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1041.lean

Retained formal statement1 of 2

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

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

FormalConjectures/ErdosProblems/1041.leanErdos1041.erdos_10418 linesExact file
∀ (n : ℕ) (f : Polynomial ℂ),  n ≥ 2 →    f.natDegree = n →      f.Monic →        f.rootSet ℂ ⊆ Metric.ball 0 1 →          ∃ z₁ z₂,            ∃ (_ : {z₁, z₂} ≤ f.roots),              ∃ γ, Set.range ⇑γ ⊆ {z | ‖Polynomial.eval z f‖ < 1} ∧ Erdos1041.length (Set.range ⇑γ) < 2
OpenStatement only, no proof