Documentation

LeanPool.PersistentSOS.Polynomial

Polynomial #

Part of the explicit persistent quartic SOS counterexample.

source
noncomputable def PersistentSOS.scalePoly (r : ℝ) :
Poly →ₐ[ℝ] Poly

Substitution of a common real scale in every polynomial variable.

Equations
Instances For
    source
    theorem PersistentSOS.scalePoly_C (r c : ℝ) :
    (scalePoly r) (MvPolynomial.C c) = MvPolynomial.C c
    source
    @[simp]
    theorem PersistentSOS.scalePoly_X (r : ℝ) (i : Fin 14) :
    (scalePoly r) (MvPolynomial.X i) = MvPolynomial.C r * MvPolynomial.X i
    source
    theorem PersistentSOS.totalDegree_scalePoly_le (r : ℝ) (p : Poly) :
    MvPolynomial.totalDegree ((scalePoly r) p) ≤ MvPolynomial.totalDegree p

    Common scaling cannot increase total degree.

    source
    @[simp]
    theorem PersistentSOS.scalePoly_qPoly (r : ℝ) :
    (scalePoly r) qPoly = MvPolynomial.C (r ^ 2) * qPoly
    source
    @[simp]
    theorem PersistentSOS.scalePoly_cubicPoly (r : ℝ) :
    (scalePoly r) cubicPoly = MvPolynomial.C (r ^ 3) * cubicPoly
    source
    theorem PersistentSOS.scalePoly_quarticPoly (r σ a b : ℝ) :
    (scalePoly r) (quarticPoly σ a b) = MvPolynomial.C (σ / 4 * r ^ 4) * qPoly ^ 2 - MvPolynomial.C (a / 2 * r ^ 2) * qPoly - MvPolynomial.C (b * r ^ 3) * cubicPoly

    The quartic, quadratic, and cubic terms scale with their literal degrees.

    source
    theorem PersistentSOS.totalDegree_qPoly_le :
    MvPolynomial.totalDegree qPoly ≤ 2

    Degree of the squared Euclidean norm polynomial.

    source
    theorem PersistentSOS.totalDegree_cubicPoly_le :
    MvPolynomial.totalDegree cubicPoly ≤ 3

    The cubic has degree at most three, using separately checked sparse components.

    source
    theorem PersistentSOS.totalDegree_quarticPoly_le (σ a b : ℝ) :
    MvPolynomial.totalDegree (quarticPoly σ a b) ≤ 4

    The objective is a quartic polynomial for all parameter values.

    source
    theorem PersistentSOS.totalDegree_shiftedQuartic_le (σ a b γ : ℝ) :
    MvPolynomial.totalDegree (quarticPoly σ a b - MvPolynomial.C γ) ≤ 4

    Subtracting a real lower bound preserves the quartic degree bound.