Definitions

Part of the explicit persistent quartic SOS counterexample.

@[reducible, inline]

abbrev PersistentSOS.Poly : Type

Ordinary real multivariate polynomials in fourteen variables.

Equations

• PersistentSOS.Poly = MvPolynomial (Fin 14) ℝ

noncomputable def PersistentSOS.qPoly : Poly

The squared Euclidean norm polynomial, the sum of all coordinate squares.

Equations

• PersistentSOS.qPoly = ∑ i : Fin 14, MvPolynomial.X i ^ 2

noncomputable def PersistentSOS.cubicPoly : Poly

The fixed sparse rational cubic, in coordinate order (t, x₁, …, x₄, y₁, …, y₉).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PersistentSOS.Q (z : Fin 14 → ℝ) : ℝ

Evaluation of the squared Euclidean norm polynomial at a real vector.

Equations

• PersistentSOS.Q z = (MvPolynomial.eval z) PersistentSOS.qPoly

noncomputable def PersistentSOS.C (z : Fin 14 → ℝ) : ℝ

Evaluation of the fixed cubic polynomial at a real vector.

Equations

• PersistentSOS.C z = (MvPolynomial.eval z) PersistentSOS.cubicPoly

noncomputable def PersistentSOS.radius (z : Fin 14 → ℝ) : ℝ

Euclidean radius, written as the square root of the sum of coordinate squares.

Equations

• PersistentSOS.radius z = √(PersistentSOS.Q z)

def PersistentSOS.IsSOS (p : Poly) : Prop

Ordinary SOS: a finite sum of squares of arbitrary real polynomials.

Equations

• PersistentSOS.IsSOS p = ∃ (m : ℕ) (f : Fin m → PersistentSOS.Poly), p = ∑ i : Fin m, f i ^ 2

noncomputable def PersistentSOS.quarticPoly (σ a b : ℝ) : Poly

Euclidean quartic regularization with quadratic coefficient -a / 2 and cubic -bC.

Equations

• PersistentSOS.quarticPoly σ a b = MvPolynomial.C (σ / 4) * PersistentSOS.qPoly ^ 2 - MvPolynomial.C (a / 2) * PersistentSOS.qPoly - MvPolynomial.C b * PersistentSOS.cubicPoly

noncomputable def PersistentSOS.objective (σ a b : ℝ) (z : Fin 14 → ℝ) : ℝ

The real - valued function obtained by evaluating the quartic polynomial.

Equations

• PersistentSOS.objective σ a b z = (MvPolynomial.eval z) (PersistentSOS.quarticPoly σ a b)

def PersistentSOS.axis (r : ℝ) : Fin 14 → ℝ

The point on the distinguished coordinate axis with first coordinate r.

Equations

• PersistentSOS.axis r i = if i = 0 then r else 0

noncomputable def PersistentSOS.minimizingRadius (σ a b : ℝ) : ℝ

Positive minimizing radius for quartic regularization with negative quadratic strength a and positive cubic strength b.

Equations

• PersistentSOS.minimizingRadius σ a b = (3 * b + √(9 * b ^ 2 + 4 * a * σ)) / (2 * σ)

noncomputable def PersistentSOS.minimumValue (σ a b : ℝ) : ℝ

Exact minimum, once the cubic has sphere maximum one.

Equations

• PersistentSOS.minimumValue σ a b = -(b * PersistentSOS.minimizingRadius σ a b ^ 3 + a * PersistentSOS.minimizingRadius σ a b ^ 2) / 4

noncomputable def PersistentSOS.uniqueCubicPoly : Poly

A second literal rational cubic selecting the positive first coordinate axis.

Equations

• PersistentSOS.uniqueCubicPoly = MvPolynomial.C (1 / 1001) * (1000 * PersistentSOS.cubicPoly + MvPolynomial.X 0 * PersistentSOS.qPoly)

noncomputable def PersistentSOS.uniqueCubic (z : Fin 14 → ℝ) : ℝ

Evaluation of the cubic with a unique sphere maximizer.

Equations

• PersistentSOS.uniqueCubic z = (MvPolynomial.eval z) PersistentSOS.uniqueCubicPoly

noncomputable def PersistentSOS.uniqueQuarticPoly (σ a b : ℝ) : Poly

Quartic regularization using the cubic with a unique sphere maximizer.

Equations

• PersistentSOS.uniqueQuarticPoly σ a b = MvPolynomial.C (σ / 4) * PersistentSOS.qPoly ^ 2 - MvPolynomial.C (a / 2) * PersistentSOS.qPoly - MvPolynomial.C b * PersistentSOS.uniqueCubicPoly

noncomputable def PersistentSOS.uniqueObjective (σ a b : ℝ) (z : Fin 14 → ℝ) : ℝ

Evaluation of the quartic with a unique global minimizer.

Equations

• PersistentSOS.uniqueObjective σ a b z = (MvPolynomial.eval z) (PersistentSOS.uniqueQuarticPoly σ a b)

noncomputable def PersistentSOS.uniqueSeparation : ℝ

The strict rational moment separation for the selected cubic.

Equations

• PersistentSOS.uniqueSeparation = 132860603 / 143000000000

@[simp]

theorem PersistentSOS.Q_eq_sum (z : Fin 14 → ℝ) : Q z = ∑ i : Fin 14, z i ^ 2

@[simp]

theorem PersistentSOS.objective_eq (σ a b : ℝ) (z : Fin 14 → ℝ) : objective σ a b z = σ / 4 * Q z ^ 2 - a / 2 * Q z - b * C z