Degree bounds for ordinary sums of squares

A finite sum of squares of real polynomials cannot cancel its highest terms. Consequently, every summand of an SOS polynomial of degree at most 2 * d has degree at most d. The SOS representations in this result are unrestricted ordinary polynomial representations.

theorem PersistentSOS.totalDegree_sq_le_sum_sq {σ : Type u_1} {ι : Type u_2} [LinearOrder σ] [WellFoundedGT σ] (s : Finset ι) (f : ι → MvPolynomial σ ℝ) {i : ι} (hi : i ∈ s) : (f i ^ 2).totalDegree ≤ (∑ j ∈ s, f j ^ 2).totalDegree

Each square in an ordinary finite sum of squares has total degree no larger than the sum. This includes representations with arbitrary - degree polynomial summands.

theorem PersistentSOS.totalDegree_le_of_sum_sq {σ : Type u_1} {ι : Type u_2} [LinearOrder σ] [WellFoundedGT σ] (s : Finset ι) (f : ι → MvPolynomial σ ℝ) (d : ℕ) (h : (∑ j ∈ s, f j ^ 2).totalDegree ≤ 2 * d) {i : ι} (hi : i ∈ s) : (f i).totalDegree ≤ d

Ordinary SOS degree bridge, valid for every even total - degree bound.

theorem PersistentSOS.quartic_sos_summand_degree {σ : Type u_1} [LinearOrder σ] [WellFoundedGT σ] {p : MvPolynomial σ ℝ} (hp : p.totalDegree ≤ 4) {m : ℕ} {f : Fin m → MvPolynomial σ ℝ} (h : p = ∑ i : Fin m, f i ^ 2) (i : Fin m) : (f i).totalDegree ≤ 2

In particular, every summand in any ordinary quartic SOS representation is a polynomial of total degree at most two.