Erdős Problem 1043

Reference: erdosproblems.com/1043

def Erdos1043.levelSet (f : Polynomial ℂ) : Set ℂ

The set $\{ z \in \mathbb{C} : \lvert f(z)\rvert\leq 1\}$

Equations

• Erdos1043.levelSet f = {z : ℂ | ‖Polynomial.eval z f‖ ≤ 1}

theorem Erdos1043.erdos_1043 : False ↔ ∀ (f : Polynomial ℂ), f.Monic → f.degree ≥ 1 → ∃ (u : ℂ), ‖u‖ = 1 ∧ MeasureTheory.volume (⇑(Submodule.span ℝ {u}).orthogonalProjection '' levelSet f) ≤ 2

Erdős Problem 1043: Let $f\in \mathbb{C}[x]$ be a monic polynomial. Must there exist a straight line $\ell$ such that the projection of [{ z: \lvert f(z)\rvert\leq 1}] onto $\ell$ has measure at most $2$?

Pommerenke [Po61] proved that the answer is no.

[Po61] Pommerenke, Ch., On metric properties of complex polynomials. Michigan Math. J. (1961), 97-115.

theorem Erdos1043.erdos_1043.variants.weak (f : Polynomial ℂ) : f.Monic → f.degree ≥ 1 → ∃ (u : ℂ), ‖u‖ = 1 ∧ MeasureTheory.volume (⇑(Submodule.span ℝ {u}).orthogonalProjection '' levelSet f) ≤ 3.3

On the other hand, Pommerenke also proved there always exists a line such that the projection has measure at most 3.3.