发表机构
School of Mathematics and Statistics, Xi’an Jiaotong University（西安交通大学数学与统计学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文证明了 Baernstein 关于零点在单位圆上的多项式的拟范数单调性猜想，并推导出多个相关不等式，同时提供了 Lean 4 形式化验证。
AI 中文摘要
设 $m$ 为单位圆周 $\mathbb{T}$ 上的归一化 Haar 测度。对于 $0<r<\infty$，定义 $\lVert f\rVert_{r}:=\left(\int_{\mathbb{T}}|f|^{r}\\,\mathrm{d} m\right)^{1/r}$，其中 $\lVert f\rVert_{0}$ 和 $\lVert f\rVert_{\infty}$ 分别解释为几何平均和上确界范数。设 $Q_n(z)=1+z^n$。我们证明，对于每个次数为 $n$、所有零点都位于 $\mathbb{T}$ 上的非零多项式 $p$，有 $$ \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. $$ 这解决了 Baernstein 的拟范数单调性猜想。作为推论，我们获得了 Visser 系数不等式的 $L^r$ 推广、sharp O'Hara--Rodriguez 不等式及其高次幂类似物、Erdős--Szekeres 乘积界 $ \left\lVert\prod_{j=1}^N(1-z^{s_j})\right\rVert_\infty\ge2\sqrt N $（对所有正整数 $s_1,\ldots,s_N$）以及 Agler--McCarthy 熵猜想。我们还提供了主要结果的 Lean 4 形式化。
英文摘要
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.
Comments23 pages. All comments are welcome!
