A positive sphere moment functional with strict cubic separation

The rational moment table is interpreted on ordinary multivariate polynomials. Positivity follows from the exact finite block certificates and complete coverage of all monomials of total degree at most two.

@[reducible, inline]

abbrev PersistentSOS.MomentIndex : Type

Indices of the complete quadratic monomial basis across all eight blocks.

Equations

• PersistentSOS.MomentIndex = ((c : Fin 8) × Fin (PersistentSOS.blockSize c))

noncomputable def PersistentSOS.sphereFunctional : Poly →ₗ[ℝ] ℝ

The normalized exact moment functional separating the cubic from its sphere bound.

Equations

• PersistentSOS.sphereFunctional = PersistentSOS.momentLinearMap PersistentSOS.momentNumerator

@[simp]

theorem PersistentSOS.sphereFunctional_monomial (d : Exponent) (c : ℝ) : sphereFunctional ((MvPolynomial.monomial d) c) = c * ↑(momentNumerator (exponentKey d)) / 1000000000

theorem PersistentSOS.basisPair_covers (i j : Fin 15) : ∃ (b : MomentIndex), basisPair b.fst b.snd = (i, j) ∨ basisPair b.fst b.snd = (j, i)

@[simp]

theorem PersistentSOS.variableExponent_zero : variableExponent 0 = 0

@[simp]

theorem PersistentSOS.variableExponent_succ (i : Fin 14) : variableExponent i.succ = Finsupp.single i 1

theorem PersistentSOS.momentBasis_zero : ∃ (b : MomentIndex), momentBasis b = 0

theorem PersistentSOS.momentBasis_single (i : Fin 14) : ∃ (b : MomentIndex), momentBasis b = Finsupp.single i 1

theorem PersistentSOS.momentBasis_pair (i j : Fin 14) : ∃ (b : MomentIndex), momentBasis b = Finsupp.single i 1 + Finsupp.single j 1

theorem PersistentSOS.momentBasis_covers (d : Exponent) (hd : (Finsupp.sum d fun (x : Fin 14) (n : ℕ) => n) ≤ 2) : ∃ (b : MomentIndex), momentBasis b = d

theorem PersistentSOS.moment_inner_sum (x : MomentIndex → ℝ) (c : Fin 8) (i : Fin (blockSize c)) : ∑ d : Fin 8, ∑ j : Fin (blockSize d), x ⟨c, i⟩ * ↑(momentNumerator (basisKey c i + basisKey d j)) * x ⟨d, j⟩ = ∑ j : Fin (blockSize c), x ⟨c, i⟩ * ↑(blockNumerator c i j) * x ⟨c, j⟩

theorem PersistentSOS.moment_gram_nonneg (x : MomentIndex → ℝ) : 0 ≤ ∑ i : MomentIndex, ∑ j : (c : Fin 8) × Fin (blockSize c), x i * sphereFunctional ((MvPolynomial.monomial (momentBasis i + momentBasis j)) 1) * x j

theorem PersistentSOS.moment_square_nonneg (h : Poly) (hd : MvPolynomial.totalDegree h ≤ 2) : 0 ≤ sphereFunctional (h ^ 2)

theorem PersistentSOS.moment_one : sphereFunctional 1 = 1

theorem PersistentSOS.moment_q : sphereFunctional qPoly = 1

theorem PersistentSOS.moment_q_sq : sphereFunctional (qPoly ^ 2) = 1

theorem PersistentSOS.moment_cubic : sphereFunctional cubicPoly = 500753357629 / 500000000000