Sphere

Part of the explicit persistent quartic SOS counterexample.

theorem PersistentSOS.Q_nonneg (z : Fin 14 → ℝ) : 0 ≤ Q z

theorem PersistentSOS.radius_nonneg (z : Fin 14 → ℝ) : 0 ≤ radius z

theorem PersistentSOS.radius_sq (z : Fin 14 → ℝ) : radius z ^ 2 = Q z

theorem PersistentSOS.Q_eq_norm_sq (z : Fin 14 → ℝ) : Q z = ‖WithLp.toLp 2 z‖ ^ 2

theorem PersistentSOS.radius_eq_norm (z : Fin 14 → ℝ) : radius z = ‖WithLp.toLp 2 z‖

noncomputable def PersistentSOS.xSq (z : Fin 14 → ℝ) : ℝ

Squared norm of the four coordinates used by the quadratic map.

Equations

• PersistentSOS.xSq z = z 1 ^ 2 + z 2 ^ 2 + z 3 ^ 2 + z 4 ^ 2

noncomputable def PersistentSOS.ySq (z : Fin 14 → ℝ) : ℝ

Squared norm of the nine coordinates paired with the quadratic map.

Equations

• PersistentSOS.ySq z = z 5 ^ 2 + z 6 ^ 2 + z 7 ^ 2 + z 8 ^ 2 + z 9 ^ 2 + z 10 ^ 2 + z 11 ^ 2 + z 12 ^ 2 + z 13 ^ 2

noncomputable def PersistentSOS.quadMap (z : Fin 14 → ℝ) : Fin 9 → ℝ

The nine-component rational quadratic map appearing in the cubic.

Equations

• PersistentSOS.quadMap z = ![z 1 ^ 2, z 2 ^ 2, z 3 ^ 2, z 1 * z 2 + z 3 * z 4, z 1 * z 3 + z 2 * z 4, z 2 * z 3, 7 / 5 * z 1 * z 4, z 2 * z 4, z 3 * z 4]

noncomputable def PersistentSOS.yVec (z : Fin 14 → ℝ) : Fin 9 → ℝ

The nine coordinates paired with the quadratic map.

Equations

• PersistentSOS.yVec z = ![z 5, z 6, z 7, z 8, z 9, z 10, z 11, z 12, z 13]

noncomputable def PersistentSOS.dotTerm (z : Fin 14 → ℝ) : ℝ

Pairing of the nine-coordinate vector with the quadratic map.

Equations

• PersistentSOS.dotTerm z = ∑ i : Fin 9, PersistentSOS.yVec z i * PersistentSOS.quadMap z i

theorem PersistentSOS.xSq_nonneg (z : Fin 14 → ℝ) : 0 ≤ xSq z

theorem PersistentSOS.ySq_nonneg (z : Fin 14 → ℝ) : 0 ≤ ySq z

theorem PersistentSOS.Q_decomp (z : Fin 14 → ℝ) : Q z = z 0 ^ 2 + xSq z + ySq z

theorem PersistentSOS.C_decomp (z : Fin 14 → ℝ) : C z = z 0 ^ 3 - 3 * z 0 * ySq z + 3 / 2 * z 0 * xSq z + 259 / 100 * dotTerm z

theorem PersistentSOS.choiLam_nonneg (a b c d : ℝ) : 0 ≤ a ^ 2 * b ^ 2 + a ^ 2 * c ^ 2 + b ^ 2 * c ^ 2 + d ^ 4 - 4 * a * b * c * d

theorem PersistentSOS.quadMap_contraction (z : Fin 14 → ℝ) : ∑ i : Fin 9, quadMap z i ^ 2 ≤ xSq z ^ 2

theorem PersistentSOS.dotTerm_bound (z : Fin 14 → ℝ) : dotTerm z ≤ √(ySq z) * xSq z

theorem PersistentSOS.cubic_unit_refined_upper (z : Fin 14 → ℝ) (hQ : Q z = 1) : C z + (3 / 2 * √3 - 259 / 100) * (√(ySq z) * xSq z) ≤ 1

theorem PersistentSOS.coefficient_strict : 259 / 100 < 3 / 2 * √3

theorem PersistentSOS.cubic_unit_upper (z : Fin 14 → ℝ) (hQ : Q z = 1) : C z ≤ 1

theorem PersistentSOS.C_scale (z : Fin 14 → ℝ) (r : ℝ) : (C fun (i : Fin 14) => r * z i) = r ^ 3 * C z

theorem PersistentSOS.Q_scale (z : Fin 14 → ℝ) (r : ℝ) : (Q fun (i : Fin 14) => r * z i) = r ^ 2 * Q z

theorem PersistentSOS.C_neg (z : Fin 14 → ℝ) : (C fun (i : Fin 14) => -z i) = -C z

theorem PersistentSOS.cubic_unit_abs (z : Fin 14 → ℝ) (hQ : Q z = 1) : |C z| ≤ 1

theorem PersistentSOS.Q_eq_zero_iff (z : Fin 14 → ℝ) : Q z = 0 ↔ z = 0

theorem PersistentSOS.cubic_abs_le (z : Fin 14 → ℝ) : |C z| ≤ radius z ^ 3

theorem PersistentSOS.Q_axis (r : ℝ) : Q (axis r) = r ^ 2

@[simp]

theorem PersistentSOS.C_axis (r : ℝ) : C (axis r) = r ^ 3

theorem PersistentSOS.unit_sphere_attainment : Q (axis 1) = 1 ∧ C (axis 1) = 1

theorem PersistentSOS.dotTerm_sq_le (z : Fin 14 → ℝ) : dotTerm z ^ 2 ≤ ySq z * xSq z ^ 2

theorem PersistentSOS.dotTerm_zero_of_xSq_zero (z : Fin 14 → ℝ) (h : xSq z = 0) : dotTerm z = 0

theorem PersistentSOS.dotTerm_zero_of_ySq_zero (z : Fin 14 → ℝ) (h : ySq z = 0) : dotTerm z = 0

theorem PersistentSOS.cubic_unit_maximizers (z : Fin 14 → ℝ) (hQ : Q z = 1) : C z = 1 ↔ xSq z = 0 ∧ (z 0 = 1 ∨ z 0 = -1 / 2)

Exact equality classification on the unit sphere. The four x coordinates vanish; the first coordinate is either 1 or -1 / 2. The sphere equation then determines the squared length of the nine y coordinates as 0 or 3 / 4, respectively.

theorem PersistentSOS.xSq_zero_iff (z : Fin 14 → ℝ) : xSq z = 0 ↔ z 1 = 0 ∧ z 2 = 0 ∧ z 3 = 0 ∧ z 4 = 0

theorem PersistentSOS.cubic_unit_maximizers_coordinates (z : Fin 14 → ℝ) (hQ : Q z = 1) : C z = 1 ↔ (z 1 = 0 ∧ z 2 = 0 ∧ z 3 = 0 ∧ z 4 = 0) ∧ (z 0 = 1 ∨ z 0 = -1 / 2)

theorem PersistentSOS.xSq_scale (z : Fin 14 → ℝ) (r : ℝ) : (xSq fun (i : Fin 14) => r * z i) = r ^ 2 * xSq z

theorem PersistentSOS.cubic_upper_equality (z : Fin 14 → ℝ) : C z = radius z ^ 3 ↔ xSq z = 0 ∧ (z 0 = radius z ∨ z 0 = -radius z / 2)

Global equality classification for the sharp homogeneous cubic bound.

theorem PersistentSOS.cubic_upper_equality_coordinates (z : Fin 14 → ℝ) : C z = radius z ^ 3 ↔ (z 1 = 0 ∧ z 2 = 0 ∧ z 3 = 0 ∧ z 4 = 0) ∧ (z 0 = radius z ∨ z 0 = -radius z / 2)