Finite monomial moment matrices

A complete finite monomial basis spans bounded-degree polynomials over any commutative semiring. For real coefficients, positivity of its moment matrix implies positivity on every quadratic square, for any polynomial variable type.

theorem PersistentSOS.quadratic_eq_sum_monomials {σ : Type u_1} {R : Type u_2} {ι : Type u_3} [CommSemiring R] [Fintype ι] (basis : ι → σ →₀ ℕ) (hcover : ∀ (d : σ →₀ ℕ), (d.sum fun (x : σ) (n : ℕ) => n) ≤ 2 → ∃ (i : ι), basis i = d) (p : MvPolynomial σ R) (hp : p.totalDegree ≤ 2) : ∃ (x : ι → R), p = ∑ i : ι, x i • (MvPolynomial.monomial (basis i)) 1

A complete finite list of monomials of degree at most two spans every quadratic polynomial. Repeated entries in the list are allowed.

theorem PersistentSOS.nonneg_quadratic_square_of_momentMatrix {σ : Type u_1} {ι : Type u_2} [Fintype ι] (basis : ι → σ →₀ ℕ) (hcover : ∀ (d : σ →₀ ℕ), (d.sum fun (x : σ) (n : ℕ) => n) ≤ 2 → ∃ (i : ι), basis i = d) (L : MvPolynomial σ ℝ →ₗ[ℝ] ℝ) (hpsd : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, ∑ j : ι, x i * L ((MvPolynomial.monomial (basis i + basis j)) 1) * x j) (p : MvPolynomial σ ℝ) (hp : p.totalDegree ≤ 2) : 0 ≤ L (p ^ 2)

Positivity of the genuine monomial moment matrix implies positivity on the square of every quadratic polynomial.