FormalConjectures/Arxiv/2602.05192/FirstProof4.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

9 declarations, 4 contain sorry, 0 declared as axioms

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

Imports (1)
Imported by 1 file
  1. def Arxiv.«2602.05192».finiteAdditiveConvolution Define line 49 source

    Source documentation

    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$.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, Nat, Polynomial

    Proof uses: Finset.sum, Prod, Finset.HasAntidiagonal.antidiagonal, HMul.hMul, HDiv.hDiv, Nat.factorial, HSub.hSub, Prod.fst, Prod.snd, Polynomial.coeff, Finset.range, HAdd.hAdd, OfNat.ofNat, HSMul.hSMul, HPow.hPow, Polynomial.X

    36 instances, coercions and auxiliary constants left out.

    noncomputable def finiteAdditiveConvolution (n : ℕ) (p q : F[X]) : F[X] :=
…
  2. theorem Arxiv.«2602.05192».finiteAdditiveConvolution_comm line 58 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, Nat, Polynomial, Eq, Arxiv.«2602.05192».finiteAdditiveConvolution

    Proof uses: id, Finset.sum_congr, Finset.range, HAdd.hAdd, OfNat.ofNat, HSMul.hSMul, Finset.sum, Prod, Finset.HasAntidiagonal.antidiagonal, HMul.hMul, HDiv.hDiv, Nat.factorial, HSub.hSub, Prod.fst, Prod.snd, Polynomial.coeff, HPow.hPow, Polynomial.X, rfl, Finset and 41 more

    64 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

  3. theorem Arxiv.«2602.05192».finiteAdditiveConvolution_degree sorry line 65 source

    depends on sorry what this means

    Statement uses: Nat, Polynomial, Real, Eq, WithBot, Polynomial.degree, Arxiv.«2602.05192».finiteAdditiveConvolution

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

    17 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  4. theorem Arxiv.«2602.05192».finiteAdditiveConvolution_monic' line 71 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Polynomial, Real, LT.lt, OfNat.ofNat, Eq, WithBot, Polynomial.degree, Polynomial.Monic, Arxiv.«2602.05192».finiteAdditiveConvolution

    Proof uses: Finset.sum, Prod, Finset.HasAntidiagonal.antidiagonal, HMul.hMul, HDiv.hDiv, Nat.factorial, HSub.hSub, Prod.fst, Prod.snd, Polynomial.coeff, Eq.mpr, Singleton.singleton, Finset, Prod.mk, id, congrArg, Finset.Nat.antidiagonal_zero, congrFun', Eq.trans, Finset.sum_congr and 101 more

    146 instances, coercions and auxiliary constants left out.

    Tactic trace: 54 steps

    Open to load the checked before-and-after goal states.

  5. def Arxiv.«2602.05192».Φ For a monic polynomial line 132 source

    Source documentation

    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.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Polynomial, Real, ENNReal

    Proof uses: ite, Multiset.Nodup, Polynomial.roots, Finset, Multiset.toFinset, Real.toNNReal, Finset.sum, HPow.hPow, Nat, Finset.erase, HDiv.hDiv, OfNat.ofNat, HSub.hSub, Top.top

    21 instances, coercions and auxiliary constants left out.

    noncomputable def Φ (p : ℝ[X]) : ℝ≥0∞ :=
…
  6. def Arxiv.«2602.05192».FourProp 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)}?$$ line 144 source

    Source documentation

    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)}?$$

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Polynomial, Real, Nat

    Proof uses: Eq, WithBot, Polynomial.degree, Multiset.card, Polynomial.roots, Polynomial.Monic, LE.le, ENNReal, HAdd.hAdd, HDiv.hDiv, OfNat.ofNat, Arxiv.«2602.05192».Φ, Arxiv.«2602.05192».finiteAdditiveConvolution

    16 instances, coercions and auxiliary constants left out.

    def FourProp (p q : ℝ[X]) (n : ℕ) : Prop :=
…
  7. theorem Arxiv.«2602.05192».four sorry line 157 source

    depends on sorry what this means

    Statement uses: Iff, True, Polynomial, Real, Nat, Arxiv.«2602.05192».FourProp

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat

    3 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  8. theorem Arxiv.«2602.05192».four_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)}?$$ sorry line 166 source

    Source documentation

    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)}?$$

    depends on sorry what this means

    Statement uses: Iff, True, Polynomial, Real, Arxiv.«2602.05192».FourProp, OfNat.ofNat, Nat

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem four_2 : answer(True) ↔ ∀ (p q : ℝ[X]), FourProp p q 2 := by
…

    Mentions: Arxiv.«2602.05192».FourProp

  9. theorem Arxiv.«2602.05192».four_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)}?$$ sorry line 175 source

    Source documentation

    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)}?$$

    depends on sorry what this means

    Statement uses: Iff, True, Polynomial, Real, Arxiv.«2602.05192».FourProp, OfNat.ofNat, Nat

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    4 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem four_3 : answer(True  ) ↔ ∀ (p q : ℝ[X]), FourProp p q 3 := by
…

    Mentions: Arxiv.«2602.05192».FourProp