Erdős problem 1043

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$ ?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1043.lean

Retained formal statement2 of 2

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

FormalConjectures/ErdosProblems/1043.leanErdos1043.erdos_1043.variants.weak3 linesExact file

1∀ (f : Polynomial ℂ),2  f.Monic →3    f.degree ≥ 1 → ∃ u, ‖u‖ = 1 ∧ MeasureTheory.volume (⇑(ℝ ∙ u).orthogonalProjection '' Erdos1043.levelSet f) ≤ 3.3

SolvedStatement only, no proof