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_monic : f.Monic) (h : f.rootSet ℂ ⊆ Metric.ball 0 1) : ∃ C ⊆ {z : ℂ | ‖Polynomial.eval z f‖ < 1}, IsConnected C ∧ 2 ≤ (Multiset.filter (fun (x : ℂ) => x ∈ C) f.roots).card

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.

See p. 139, above Problem 5: [EHP58] Erdős, P. and Herzog, F. and Piranian, G., Metric properties of polynomials. J. Analyse Math. (1958), 125-148.

theorem Erdos1041.erdos_1041 (n : ℕ) (f : Polynomial ℂ) (hn : n ≥ 2) (hnum : f.natDegree = n) (h_monic : f.Monic) (h : f.rootSet ℂ ⊆ Metric.ball 0 1) : ∃ (z₁ : ℂ) (z₂ : ℂ) (_ : {z₁, z₂} ≤ f.roots) (γ : 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$?