Erdős Problem 1041

Reference: erdosproblems.com/1041

noncomputable def Erdos1041.length (s : Set ℂ) : ENNReal

The length of a subset $s$ of $\mathbb{C}$ is defined to be its 1-dimensional Hausdorff measure $\mathcal{H}^1(s)$.

Equations

• Erdos1041.length s = (MeasureTheory.Measure.hausdorffMeasure 1) s

theorem Erdos1041.exists_connected_component_contains_two_roots (n : ℕ) (f : Polynomial ℂ) (hn : n ≥ 2) (hnum : f.natDegree = n) (h : f.rootSet ℂ ⊆ Metric.ball 0 1) : ∃ (z₁ : ℂ) (z₂ : ℂ), connectedComponentIn {z : ℂ | ‖Polynomial.eval z f‖ < 1} z₁ = connectedComponentIn {z : ℂ | ‖Polynomial.eval z f‖ < 1} z₂ ∧ z₁ ≠ z₂ ∧ z₁ ∈ f.rootSet ℂ ∧ z₂ ∈ f.rootSet ℂ

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

theorem Erdos1041.erdos_1041 (n : ℕ) (f : Polynomial ℂ) (hn : n ≥ 2) (hnum : f.natDegree = n) (h : f.rootSet ℂ ⊆ Metric.ball 0 1) : ∃ (z₁ : ℂ) (z₂ : ℂ) (_ : z₁ ≠ z₂) (_ : z₁ ∈ f.rootSet ℂ) (_ : z₂ ∈ f.rootSet ℂ) (γ : Path z₁ z₂), Set.range ⇑γ ⊆ {z : ℂ | ‖Polynomial.eval z f‖ < 1} ∧ length (Set.range ⇑γ) < 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$?