Baernstein's quasi-norm monotonicity conjecture for polynomials with unimodular zero
Teng Zhang
math.CV
Oct 1, 2026 · v1
TL;DR
Provides a Lean 4 formalization of the main theorem, including arbitrary root multiplicities and the endpoint exponents 0 and infinity.
Abstract
Let $m$ denote the normalized Haar measure on the unit circle $\mathbb{T}$. For $0<r<\infty$, define $\lVert f\rVert_{r}:=\left(\int_{\mathbb{T}}|f|^{r}\,\mathrm{d} m\right)^{1/r}$, with $\lVert f\rVert_{0}$ and $\lVert f\rVert_{\infty}$ interpreted as the geometric mean and the supremum norm, respectively. Set $Q_n(z)=1+z^n$. We prove that, for every nonzero polynomial $p$ of degree $n$ whose zeros all lie on $\mathbb{T}$, $$ \frac{\lVert p\rVert_s}{\lVert Q_n\rVert_s} \le \frac{\lVert p\rVert_t}{\lVert Q_n\rVert_t}, \qquad 0\le s\le t\le\infty. $$ This settles Baernstein's quasi-norm monotonicity conjecture. As corollaries, we obtain an $L^r$ extension of Visser's coefficient inequality, the sharp O'Hara–Rodriguez inequality and its higher-power analogues, the Erdős–Szekeres product bound $ \left\lVert\prod_{j=1}^N(1-z^{s_j})\right\rVert_\infty\ge2\sqrt N $ for all positive integers $s_1,\ldots,s_N$ and Agler–McCarthy's entropy conjecture. We also provide a Lean 4 formalization of the main results.
Problem
Baernstein's 2008 conjecture asserts that for polynomials of degree n with all zeros on the unit circle, the ratio of the L^r quasi-norm to that of Q_n(z)=1+z^n is nondecreasing in r on [0,∞].
Approach
The polynomial is normalized to self-inversive form with a polar factorization. Differentiating L^r means reduces monotonicity to an entropy comparison. A boundary-to-area identity turns this into a weighted Dirichlet integral governed by a kernel. Kernel positivity is proved separately for 0<a≤1 by coefficient estimates and for a≥1 by beta-function and principal-value analysis. Repeated roots are handled by approximation, and the main results are formalized in Lean 4.
Results
The conjecture is proved in full. Corollaries include an L^r extension of Visser's coefficient inequality, the sharp O'Hara–Rodriguez inequality and its higher-power analogues, the Erdős–Szekeres bound ||∏(1-z^{s_j})||_∞ ≥ 2√N, and the Agler–McCarthy entropy conjecture.
