Baernstein's quasi-norm monotonicity conjecture for polynomials with unimodular zero

Let $m$ denote the normalized Haar measure on the unit circle $\mathbb{T}$. For $0<r<\mathrm{\infty }$, define $\parallel f{\parallel }_r:={\left({\int }_{\mathbb{T}}\mathrm{\mid }f{\mathrm{\mid }}^r\mathrm{d}m\right)}^{1\mathrm{/}r}$, with $\parallel f{\parallel }_0$ and $\parallel f{\parallel }_{\mathrm{\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{\parallel p{\parallel }_s}{\parallel Q_n{\parallel }_s}\le \frac{\parallel p{\parallel }_t}{\parallel Q_n{\parallel }_t},0\le s\le t\le \mathrm{\infty }\mathrm{.}$$ 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 ${\parallel {\prod }_{j=1}^N(1-z^{s_j})\parallel }_{\mathrm{\infty }}\ge 2\sqrt{N}$ for all positive integers $s_1,\dots ,s_N$ and Agler–McCarthy’s entropy conjecture. We also provide a Lean 4 formalization of the main results.