Theorem
Lean target: introduce the multivariate real-stability bridge used in Gribinski--Marcus:
theorem hasOnlyNonnegRoots_iff_realStable_XY
{d : ℕ} {p : ℝ[X]}
(hpdeg : p.natDegree = d) (hlead : 0 < p.leadingCoeff) :
HasOnlyNonnegRoots p ↔ RealStable (xyLift p)Here xyLift p should be the bivariate polynomial corresponding to p(x * y) in whatever multivariate polynomial API we choose. The statement may be better phrased through a local PPlus d p predicate if that makes the exact-degree convention cleaner.
Reference
Gribinski--Marcus, A rectangular additive convolution for polynomials, Lemma 2.5. Mao--Wang use this theorem indirectly through Gribinski--Marcus Lemma 2.3.
Dependencies
- Choose or introduce a multivariate polynomial/real-stability API.
- Reuse
HasOnlyNonnegRoots from RealRooted/NarayanaTransformation.lean or move it to a more general file if needed.
- Basic facts about upper-half-plane substitution and real roots.
Notes
This is the entry point for replacing the current rectangularAdditiveConvolutionPreservesNonnegRoots_degreeAtLeastThree sorry with the actual Gribinski--Marcus proof route.
Theorem
Lean target: introduce the multivariate real-stability bridge used in Gribinski--Marcus:
Here
xyLift pshould be the bivariate polynomial corresponding top(x * y)in whatever multivariate polynomial API we choose. The statement may be better phrased through a localPPlus d ppredicate if that makes the exact-degree convention cleaner.Reference
Gribinski--Marcus, A rectangular additive convolution for polynomials, Lemma 2.5. Mao--Wang use this theorem indirectly through Gribinski--Marcus Lemma 2.3.
Dependencies
HasOnlyNonnegRootsfromRealRooted/NarayanaTransformation.leanor move it to a more general file if needed.Notes
This is the entry point for replacing the current
rectangularAdditiveConvolutionPreservesNonnegRoots_degreeAtLeastThreesorry with the actual Gribinski--Marcus proof route.