math.CV — Complex Variables
Smale's mean value constant (1981) equals 4, and other miscellanea
For a complex polynomial p of degree d ≥ 2 with p(0) = 0 and p′(0) ≠ 0, let S(p) be the minimum of |p(c)/(c p′(0))| over the critical points c of p, and let K(d) be the supremum of S(p) over all such p of degree d. In 1981 Smale proved that K(d) ≤ 4 for every d, and asked whether 4 can be replaced by 1. We prove that Smale's mean value constant sup_d K(d) equals 4 and that K(d) → 4 as d → ∞, combining a reduction due to Jatar and Ng with an explicit construction. Each K(d) is known to be below 4, so the supremum is not attained. The main result has also been formalized in the Lean 4 proof assistant. We give three further proofs: by a variant of the main construction in which part of the boundary of an auxiliary domain is a level curve of an entire function; by a Riemann map onto a domain with thin hairs; and by a Riemann surface whose conformal radius at its base point is near 1. We also include a complete proof of the known fact that K(d) does not decrease.