Maximum-modulus points on concentric circles
Yunpeng Li
math.CV
Oct 10, 2026 · v2
TL;DR
Corollary 2 (the cofinal bound answering Erdős Problem #1117 negatively) has a cited Lean 4 formalization.
Abstract
We give a negative answer to the second question of Erdős Problem #1117: can the number $ν_f(r)$ of maximum-modulus points of a nonzero, non-monomial entire function on $|z|=r$ tend to infinity as $r\to\infty$? Write $f(z)=z^m g(z)$ with $g(0)\ne0$, and let $k$ be the first positive exponent with a nonzero coefficient in the Taylor expansion of $g$. We prove that $\{r>0:ν_f(r)>2k\}$ is locally finite in $(0,\infty)$, and that the constant $2k$ is sharp. In particular, $\liminf_{r\to\infty}ν_f(r)\le2k<\infty$, without a growth assumption. The proof combines finite local parametrizations of a logarithmic-derivative correspondence with analytic continuation and a local description of stationary points.
Problem
Erdős Problem #1117(b) asks whether the number ν_f(r) of maximum-modulus points on |z|=r of a non-monomial entire function f can tend to infinity as r→∞.
Approach
Writing f=z^m g with g(z)=a_0+a_k z^k+…, the proof studies a correspondence pairing points z,w with zw=s and equal logarithmic derivatives A(z)=B(w). It combines finite local holomorphic parametrizations of this correspondence, analytic continuation across the excluded value m, and an open-closed projection argument. These steps bound the fiber sizes by 2k. The resulting cofinal bound (Corollary 2) is formalized in Lean 4.
Results
The set of radii with ν_f(r)>2k is locally finite in (0,∞), and the constant 2k is sharp. Hence liminf ν_f(r) ≤ 2k, which answers question (b) negatively without any growth assumption.
