Erdős Problem 1043

References:

• erdosproblems.com/1043
• [EHP58] Erdős, P. and Herzog, F. and Piranian, G., Metric properties of polynomials. J. Analyse Math. (1958), 125-148.
• [Po59] Pommerenke, Ch., On some problems by Erdős, Herzog and Piranian. Michigan Math. J. (1959), 221-225.
• [Po61] Pommerenke, Ch., On metric properties of complex polynomials. Michigan Math. J. (1961), 97-115.

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 (⇑(ℝ ∙ 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.

This was formalized in Lean by Alexeev using Aristotle.

theorem Erdos1043.erdos_1043.variants.weak (f : Polynomial ℂ) : f.Monic → f.degree ≥ 1 → ∃ (u : ℂ), ‖u‖ = 1 ∧ MeasureTheory.volume (⇑(ℝ ∙ 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.