Papers With

← All papers
First page of From $\log 2$ to $π/2$: the sharp asymptotic inradius of polynomial lemniscates

From $\log 2$ to $π/2$: the sharp asymptotic inradius of polynomial lemniscates

YuJian Geng, Dong Qiu

math.CV Sep 6, 2026 · v1
formalization analysis
Read PDF arXiv abstract Code
TL;DR
Accompanies a complex-analysis proof of the sharp asymptotic inradius of polynomial lemniscates with a Lean 4 formalization and step-by-step source index.
Abstract
Let $R_n$ be the infimum of the inradii of $\{z:|p(z)|<1\}$ over monic degree-$n$ polynomials whose zeros lie in the closed unit disk. We prove $nR_n\toπ/2$, matching the asymptotic obstruction supplied by $z^n-1$. We first establish the exact universal radius $2^{1/n}-1$ for disks centered at zeros, which recovers the $(\log2)/n$ bound. Small inradius then forces radial concentration of the zeros and decay of their low reciprocal moments. These estimates give an entire limit with a modulus reflection identity; a second rescaling produces an exponential tangent and strict sublevel disks of every radius below $π/2$. The proof is accompanied by a Lean 4 formalization and a step-by-step source index.
Problem

Let R_n be the infimum of inradii of {|p(z)|<1} over monic degree-n polynomials with zeros in the closed unit disk. The goal is to determine the sharp asymptotic constant for nR_n, matching the obstruction from z^n-1.

Approach

An exact universal radius 2^{1/n}-1 is established for disks centered at zeros, recovering the (log2)/n bound. Small inradius forces radial concentration of zeros and decay of low reciprocal moments, yielding an entire limit with a modulus reflection identity. A second rescaling produces an exponential tangent and strict sublevel disks below π/2. The arguments are accompanied by a Lean 4 formalization with a step-by-step source index mapping mathematical steps to Lean file locations.

Results

The authors prove nR_n → π/2, with a uniform lower bound ρ(p) ≥ (π/2−ε)/n for large n and matching upper obstruction from z^n−1. The final statement is formalized as main_positive_radius_stepwise in PaperStepDetails.lean.