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

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 $ζ_1,\ldots,ζ_{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-ζ_j|^2}\ge n-1. $$ Moreover, equality holds if and only if $p(z)=c(z^n-ω)$ for some $c\in\mathbb C\setminus\{0\}$ and $|ω|=1$. We also provide a Lean 4 formalization of the main results.