Derivatives of the quartic with a unique global minimizer

The Hessian is computed from the literal polynomial using MvPolynomial.pderiv. At its minimizing axis point it is a strictly positive diagonal matrix.

theorem PersistentSOS.unique_cubic_first_at_zero (i : Fin 14) : (MvPolynomial.eval 0) ((MvPolynomial.pderiv i) uniqueCubicPoly) = 0

The new cubic has no first - order contribution at the origin.

theorem PersistentSOS.unique_cubic_second_at_zero (i j : Fin 14) : (MvPolynomial.eval 0) ((MvPolynomial.pderiv j) ((MvPolynomial.pderiv i) uniqueCubicPoly)) = 0

The new cubic has no second - order contribution at the origin.

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

The origin remains stationary for every choice of the parameters.

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

The Hessian at the stationary origin remains the negative scalar matrix.

theorem PersistentSOS.cubic_second_axis (r : ℝ) (i j : Fin 14) : (MvPolynomial.eval (axis r)) ((MvPolynomial.pderiv j) ((MvPolynomial.pderiv i) cubicPoly)) = if i = j then if i = 0 then 6 * r else if ↑i ≤ 4 then 3 * r else -6 * r else 0

The second derivatives of the original cubic at an arbitrary axis point.

theorem PersistentSOS.unique_cubic_second_axis (r : ℝ) (i j : Fin 14) : (MvPolynomial.eval (axis r)) ((MvPolynomial.pderiv j) ((MvPolynomial.pderiv i) uniqueCubicPoly)) = if i = j then if i = 0 then 6 * r else if ↑i ≤ 4 then 3002 * r / 1001 else -5998 * r / 1001 else 0

The selected cubic's Hessian on the distinguished axis.

theorem PersistentSOS.unique_hessian_minimizer {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) (i j : Fin 14) : (MvPolynomial.eval (axis (minimizingRadius σ a b))) ((MvPolynomial.pderiv j) ((MvPolynomial.pderiv i) (uniqueQuarticPoly σ a b))) = if i = j then if i = 0 then 2 * a + 3 * b * minimizingRadius σ a b else if ↑i ≤ 4 then b * minimizingRadius σ a b / 1001 else 9001 * b * minimizingRadius σ a b / 1001 else 0

The actual Hessian entries at the explicit minimizing radius.

theorem PersistentSOS.unique_hessian_posDef {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) (hb : 0 < b) : Matrix.PosDef fun (i j : Fin 14) => (MvPolynomial.eval (axis (minimizingRadius σ a b))) ((MvPolynomial.pderiv j) ((MvPolynomial.pderiv i) (uniqueQuarticPoly σ a b)))

The Hessian at the unique global minimizer is positive definite for all positive real regularization, quadratic, and cubic strengths.

theorem PersistentSOS.cubic_first_axis (r : ℝ) (i : Fin 14) : (MvPolynomial.eval (axis r)) ((MvPolynomial.pderiv i) cubicPoly) = if i = 0 then 3 * r ^ 2 else 0

First derivatives of the original cubic on its distinguished axis.

theorem PersistentSOS.unique_cubic_first_axis (r : ℝ) (i : Fin 14) : (MvPolynomial.eval (axis r)) ((MvPolynomial.pderiv i) uniqueCubicPoly) = if i = 0 then 3 * r ^ 2 else 0

The selected cubic has the same axial gradient as the original cubic.

theorem PersistentSOS.unique_stationary_minimizer {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) (i : Fin 14) : (MvPolynomial.eval (axis (minimizingRadius σ a b))) ((MvPolynomial.pderiv i) (uniqueQuarticPoly σ a b)) = 0

The explicitly specified unique minimizer is stationary.