Theorem 4

Reference: arxiv/2602.05192 First Proof by Mohammed Abouzaid, Andrew J. Blumberg, Martin Hairer, Joe Kileel, Tamara G. Kolda, Paul D. Nelson, Daniel Spielman, Nikhil Srivastava, Rachel Ward, Shmuel Weinberger, Lauren Williams

noncomputable def Arxiv.«2602.05192».finiteAdditiveConvolution {F : Type} [Field F] (n : ℕ) (p q : Polynomial F) : Polynomial F

Define $p \boxplus_n q(x)$ to be the polynomial $$ (p \boxplus_n q)(x) = \sum_{k=0}^n c_k x^{n-k} $$ where the coefficients $c_k$ are given by the formula: $$ c_k = \sum_{i+j=k} \frac{(n-i)! (n-j)!}{n! (n-k)!} a_i b_j $$ for $k = 0, 1, \dots, n$.

Equations

• One or more equations did not get rendered due to their size.

theorem Arxiv.«2602.05192».finiteAdditiveConvolution_comm {F : Type} [Field F] (n : ℕ) (p q : Polynomial F) : finiteAdditiveConvolution n p q = finiteAdditiveConvolution n q p

theorem Arxiv.«2602.05192».finiteAdditiveConvolution_degree (n : ℕ) (p q : Polynomial ℝ) (hp : p.degree = ↑n) (hq : q.degree = ↑n) : (finiteAdditiveConvolution n p q).degree = ↑n

theorem Arxiv.«2602.05192».finiteAdditiveConvolution_monic' (n : ℕ) (p q : Polynomial ℝ) (hn : 0 < n) (hp : p.degree = ↑n) (hq : q.degree = ↑n) : p.Monic → q.Monic → (finiteAdditiveConvolution n p q).Monic

noncomputable def Arxiv.«2602.05192».Φ (p : Polynomial ℝ) : ENNReal

For a monic polynomial $p(x)=\prod_{i\le n}(x- \lambda_i)$, define $$\Phi_n(p):=\sum_{i\le n}(\sum_{j\neq i} \frac1{\lambda_i-\lambda_j})^2$$ and $\Phi_n(p):=\infty$ if $p$ has a multiple root.

Equations

• Arxiv.«2602.05192».Φ p = if p.roots.Nodup then have roots := p.roots.toFinset; ↑(∑ i ∈ roots, (∑ j ∈ roots.erase i, 1 / (i - j)) ^ 2).toNNReal else ⊤

def Arxiv.«2602.05192».FourProp (p q : Polynomial ℝ) (n : ℕ) : Prop

A predicate that holds if $p(x)$ and $q(x)$ are monic real-rooted polynomials of degree $n$, then $$\frac{1}{\Phi_n(p\boxplus_n q)} \ge \frac{1}{\Phi_n(p)}+\frac{1}{\Phi_n(q)}?$$

Equations

• One or more equations did not get rendered due to their size.

theorem Arxiv.«2602.05192».four : sorry ↔ ∀ (p q : Polynomial ℝ) (n : ℕ), FourProp p q n

Is it true that if $p(x)$ and $q(x)$ are monic real-rooted polynomials of degree $n$, then $$\frac{1}{\Phi_n(p\boxplus_n q)} \ge \frac{1}{\Phi_n(p)}+\frac{1}{\Phi_n(q)}?$$

Note: while no proof of this is published yet, the authors of arxiv/2602.05192 announced that a proof will be released on 2026-02-13

TODO(firsching): update category and remove Note when proof is published.

theorem Arxiv.«2602.05192».four_2 : sorry ↔ ∀ (p q : Polynomial ℝ), FourProp p q 2

Is it true that if $p(x)$ and $q(x)$ are monic real-rooted polynomials of degree $2$, then $$\frac{1}{\Phi_2(p\boxplus_n q)} \ge \frac{1}{\Phi_2(p)}+\frac{1}{\Phi_2(q)}?$$

theorem Arxiv.«2602.05192».four_3 : sorry ↔ ∀ (p q : Polynomial ℝ), FourProp p q 3

Is it true that if $p(x)$ and $q(x)$ are monic real-rooted polynomials of degree $3$, then $$\frac{1}{\Phi_3(p\boxplus_n q)} \ge \frac{1}{\Phi_3(p)}+\frac{1}{\Phi_3(q)}?$$