Radial

Part of the explicit persistent quartic SOS counterexample.

noncomputable def PersistentSOS.radialValue (σ a b r : ℝ) : ℝ

The one - variable radial lower envelope.

Equations

• PersistentSOS.radialValue σ a b r = σ / 4 * r ^ 4 - b * r ^ 3 - a / 2 * r ^ 2

theorem PersistentSOS.minimizingRadius_pos {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) (hb : 0 < b) : 0 < minimizingRadius σ a b

theorem PersistentSOS.minimizingRadius_equation {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) : σ * minimizingRadius σ a b ^ 2 = 3 * b * minimizingRadius σ a b + a

theorem PersistentSOS.radial_at_minimizingRadius {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) : radialValue σ a b (minimizingRadius σ a b) = minimumValue σ a b

theorem PersistentSOS.radial_factorization {σ a b r s : ℝ} (he : σ * r ^ 2 = 3 * b * r + a) : radialValue σ a b s + (b * r ^ 3 + a * r ^ 2) / 4 = (s - r) ^ 2 * (σ * s ^ 2 + (2 * σ * r - 4 * b) * s + b * r + a) / 4

theorem PersistentSOS.radial_global_minimum {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) (hb : 0 < b) {s : ℝ} (hs : 0 ≤ s) : minimumValue σ a b ≤ radialValue σ a b s

theorem PersistentSOS.radial_minimum_eq_iff {σ a b : ℝ} (hσ : 0 < σ) (ha : 0 < a) (hb : 0 < b) {s : ℝ} (hs : 0 ≤ s) : radialValue σ a b s = minimumValue σ a b ↔ s = minimizingRadius σ a b

The radial minimizer is unique among nonnegative radii.