Linear moment functionals and finite Gram forms

A single exponent-indexed function supplies every occurrence of a monomial.

@[reducible, inline]

abbrev PersistentSOS.Exponent : Type

Exponent vectors of ordinary polynomials in fourteen variables.

Equations

• PersistentSOS.Exponent = (Fin 14 →₀ ℕ)

def PersistentSOS.exponentKey (d : Exponent) : ℕ

A base - five key used only to index the explicit finite moment table.

Equations

• PersistentSOS.exponentKey d = ∑ i : Fin 14, d i * 5 ^ ↑i

@[simp]

theorem PersistentSOS.exponentKey_zero : exponentKey 0 = 0

@[simp]

theorem PersistentSOS.exponentKey_add (d e : Exponent) : exponentKey (d + e) = exponentKey d + exponentKey e

@[simp]

theorem PersistentSOS.exponentKey_single (i : Fin 14) (n : ℕ) : exponentKey (Finsupp.single i n) = n * 5 ^ ↑i

noncomputable def PersistentSOS.momentLinearMap (m : ℕ → ℤ) : Poly →ₗ[ℝ] ℝ

Extend any moment table linearly to ordinary real multivariate polynomials.

Equations

• PersistentSOS.momentLinearMap m = (Finsupp.linearCombination ℝ fun (d : PersistentSOS.Exponent) => ↑(m (PersistentSOS.exponentKey d)) / 1000000000) ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv ℝ)

@[simp]

theorem PersistentSOS.momentLinearMap_monomial (m : ℕ → ℤ) (d : Exponent) (c : ℝ) : (momentLinearMap m) ((MvPolynomial.monomial d) c) = c * ↑(m (exponentKey d)) / 1000000000

theorem PersistentSOS.block_nonneg {κ : Type u_1} [Fintype κ] (size : κ → ℕ) (A : (k : κ) → Fin (size k) → Fin (size k) → ℝ) (hA : ∀ (k : κ), IsPSD (A k)) (x : (k : κ) × Fin (size k) → ℝ) : 0 ≤ ∑ k : κ, quadraticForm (A k) fun (i : Fin (size k)) => x ⟨k, i⟩

A block - diagonal collection of nonnegative quadratic forms is nonnegative.