Theorem
Lean target:
theorem RealStable.liebSokal_multiaffine
{F G : MvPolynomial σ ℂ}
(hF : RealStable F) (hG : RealStable G)
(hFma : Multiaffine F) (hGma : Multiaffine G) :
applyNegDifferential F G = 0 ∨ RealStable (applyNegDifferential F G)applyNegDifferential F G denotes the operator F(-∂) {G}. The final signature should use the real-stability/multivariate API chosen in #87.
Reference
Gribinski--Marcus, A rectangular additive convolution for polynomials, Theorem 2.4, cited there as the Lieb-Sokal theorem.
Dependencies
Notes
This theorem is the second main stability input for Gribinski--Marcus Theorem 2.3. It should be proved or imported in a general enough form to apply to the polarized p and q polynomials in the proof of the rectangular additive convolution theorem.
Theorem
Lean target:
applyNegDifferential F Gdenotes the operatorF(-∂) {G}. The final signature should use the real-stability/multivariate API chosen in #87.Reference
Gribinski--Marcus, A rectangular additive convolution for polynomials, Theorem 2.4, cited there as the Lieb-Sokal theorem.
Dependencies
Notes
This theorem is the second main stability input for Gribinski--Marcus Theorem 2.3. It should be proved or imported in a general enough form to apply to the polarized
pandqpolynomials in the proof of the rectangular additive convolution theorem.