Erdős problem 115

If $p(z)$ is a polynomial of degree $n$ such that $\{z : \lvert p(z)\rvert\leq 1\}$ is connected then is it true that $\max_{\substack{z\in\mathbb{C}\\ \lvert p(z)\rvert\leq 1}} \lvert p'(z)\rvert \leq (\tfrac{1}{2}+o(1))n^2?$

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

FormalConjectures/ErdosProblems/

115.lean

Retained formal statement1 of 1

If $p(z)$ is a polynomial of degree $n$ such that $\{z : \lvert p(z)\rvert\leq 1\}$ is connected then is it true that $\max_{\substack{z\in\mathbb{C}\\ \lvert p(z)\rvert\leq 1}} \lvert p'(z)\rvert \leq (\tfrac{1}{2}+o(1))n^2?$

Eremenko and Lempert [ErLe94] have shown this is true, and in fact Chebyshev polynomials are the extreme examples.

FormalConjectures/ErdosProblems/115.leanErdos115.erdos_1159 linesExact file

1True ↔2  ∀ ε > 0,3    ∀ᶠ (n : ℕ) in Filter.atTop,4      ∀ (p : Polynomial ℂ),5        p.Monic →6          p.natDegree = n →7            IsConnected {z | ‖Polynomial.eval z p‖ ≤ 1} →8              ∀ (z : ℂ),9                ‖Polynomial.eval z p‖ ≤ 1 → ‖Polynomial.eval z (Polynomial.derivative p)‖ ≤ (1 / 2 + ε) * ↑n ^ 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.