First Proof, Theorem 4

Reference: arxiv/2602.05192v2 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_deg : p.degree = ↑n) (hq_deg : q.degree = ↑n) (hp_monic : p.Monic) (hq_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 : True ↔ ∀ (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)}?$$

arxiv/2602.05192v2 contains a proof.

theorem Arxiv.«2602.05192».four_2 : True ↔ ∀ (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 : True ↔ ∀ (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)}?$$