Derivatives

Part of the explicit persistent quartic SOS counterexample.

theorem PersistentSOS.cubic_first_at_zero (i : Fin 14) : (MvPolynomial.eval 0) ((MvPolynomial.pderiv i) cubicPoly) = 0

theorem PersistentSOS.cubic_second_at_zero (i j : Fin 14) : (MvPolynomial.eval 0) ((MvPolynomial.pderiv j) ((MvPolynomial.pderiv i) cubicPoly)) = 0

theorem PersistentSOS.q_first (i : Fin 14) : (MvPolynomial.pderiv i) qPoly = 2 * MvPolynomial.X i

theorem PersistentSOS.stationary_origin (σ a b : ℝ) (i : Fin 14) : (MvPolynomial.eval 0) ((MvPolynomial.pderiv i) (quarticPoly σ a b)) = 0

theorem PersistentSOS.hessian_origin (σ a b : ℝ) (i j : Fin 14) : (MvPolynomial.eval 0) ((MvPolynomial.pderiv j) ((MvPolynomial.pderiv i) (quarticPoly σ a b))) = if i = j then -a else 0