Beyond Sendov's conjecture: the quadratic Tang--Zhang inequality

RESUMO

Very recently, Lech Mazur proved the celebrated Sendov conjecture, and Terence Tao subsequently distilled the main ideas of the proof in a blog post. In this paper, we establish a quantitative strengthening of Sendov's conjecture, namely the quadratic Tang--Zhang inequality. Let $p$ be a polynomial of degree $n\ge2$ whose zeros lie in the closed unit disk, and let $\zeta_1,\ldots,\zeta_{n-1}$ denote its critical points, counted with multiplicity. We prove that, for every zero $a$ of $p$, $$ \sum_{j=1}^{n-1}\frac{1}{|a-\zeta_j|^2}\ge n-1. $$ Moreover, equality holds if and only if $p(z)=c(z^n-\omega)$ for some $c\in\mathbb C\setminus\{0\}$ and $|\omega|=1$. We also provide a Lean 4 formalization of the main results.