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

FormalConjectures/ErdosProblems/

1043.lean

Retained formal statement1 of 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.

This was formalized in Lean by Alexeev using Aristotle.

FormalConjectures/ErdosProblems/1043.leanErdos1043.erdos_10434 linesExact file

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

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.