Transfer

Part of the explicit persistent quartic SOS counterexample.

noncomputable def PersistentSOS.separation : ℝ

The strict rational separation of the fixed cubic from its sphere bound.

Equations

• PersistentSOS.separation = 753357629 / 500000000000

theorem PersistentSOS.separation_pos : 0 < separation

theorem PersistentSOS.functional_separation (L : Poly →ₗ[ℝ] ℝ) (h1 : L 1 = 1) (hQ : L qPoly = 1) (hQQ : L (qPoly ^ 2) = 1) (hC : L cubicPoly = 1 + separation) (σ a b r γ : ℝ) : L (MvPolynomial.C (σ / 4 * r ^ 4) * qPoly ^ 2 - MvPolynomial.C (a / 2 * r ^ 2) * qPoly - MvPolynomial.C (b * r ^ 3) * cubicPoly - MvPolynomial.C γ) = radialValue σ a b r - b * separation * r ^ 3 - γ

An abstract linear - separation calculation, used with a separately verified ordinary moment functional. The public explicit theorem supplies that witness.

theorem PersistentSOS.scaled_sos_nonneg (L : Poly →ₗ[ℝ] ℝ) (hL : ∀ (h : Poly), MvPolynomial.totalDegree h ≤ 2 → 0 ≤ L (h ^ 2)) {p : Poly} (hp : MvPolynomial.totalDegree p ≤ 4) (hsos : IsSOS p) (r : ℝ) : 0 ≤ L ((scalePoly r) p)

Positivity for an ordinary quartic SOS, after any common coordinate scaling.

theorem PersistentSOS.objective_global_lower_bound {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) (hb : 0 < b) (z : Fin 14 → ℝ) : minimumValue σ a b ≤ objective σ a b z

Exact global lower bound for every positive parameter.

theorem PersistentSOS.objective_axis_attainment {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) : objective σ a b (axis (minimizingRadius σ a b)) = minimumValue σ a b

The distinguished axis point attains the exact global minimum.

theorem PersistentSOS.moment_quantitative_transfer (L : Poly →ₗ[ℝ] ℝ) (h1 : L 1 = 1) (hQ : L qPoly = 1) (hQQ : L (qPoly ^ 2) = 1) (hC : L cubicPoly = 1 + separation) (hL : ∀ (h : Poly), MvPolynomial.totalDegree h ≤ 2 → 0 ≤ L (h ^ 2)) {σ a b γ : ℝ} (hσ : 0 < σ) (ha : 0 < a) (hsos : IsSOS (quarticPoly σ a b - MvPolynomial.C γ)) : γ ≤ minimumValue σ a b - b * separation * minimizingRadius σ a b ^ 3

The abstract moment - to - SOS transfer. The explicit theorem below instantiates all witness hypotheses by exact certificate proofs.