The quadratic-penalty objective and its critical points

This file defines the objective f_p(u) = ‖σ(u) - p‖² from equation (1.3) of the paper together with the first- and second-order critical point conditions of Definition 3.1. The definitions DotForm, objective, IsFOCP, hessianTerm and IsSOCP are duplicated verbatim in the root module Challenge.lean (the Palomar statement surface); keep the two copies in sync.

@[reducible, inline]

abbrev LowRankUnivariateSOS.DotForm : Type

The development is abstract over an arbitrary real bilinear form on polynomials. In the paper this corresponds to the statement that the argument works for any inner product used to define the penalty f_p. We only use positivity of the associated quadratic map, not any special coefficient model.

Equations

• LowRankUnivariateSOS.DotForm = LinearMap.BilinForm ℝ LowRankUnivariateSOS.Poly

@[simp]

theorem LowRankUnivariateSOS.dot_add_left {B : DotForm} (p q r : Poly) : (B (p + q)) r = (B p) r + (B q) r

The next simp lemmas are the algebraic identities saying that a bilinear form behaves linearly in each argument. They are used repeatedly when expanding the gradient and Hessian expressions from Definition \ref{def:socp}.

@[simp]

theorem LowRankUnivariateSOS.dot_add_right {B : DotForm} (p q r : Poly) : (B p) (q + r) = (B p) q + (B p) r

@[simp]

theorem LowRankUnivariateSOS.dot_smul_left {B : DotForm} (a : ℝ) (p q : Poly) : (B (a • p)) q = a * (B p) q

@[simp]

theorem LowRankUnivariateSOS.dot_smul_right {B : DotForm} (a : ℝ) (p q : Poly) : (B p) (a • q) = a * (B p) q

@[simp]

theorem LowRankUnivariateSOS.dot_zero_left {B : DotForm} (p : Poly) : (B 0) p = 0

@[simp]

theorem LowRankUnivariateSOS.dot_zero_right {B : DotForm} (p : Poly) : (B p) 0 = 0

@[simp]

theorem LowRankUnivariateSOS.dot_neg_left {B : DotForm} (p q : Poly) : (B (-p)) q = -(B p) q

@[simp]

theorem LowRankUnivariateSOS.dot_neg_right {B : DotForm} (p q : Poly) : (B p) (-q) = -(B p) q

noncomputable def LowRankUnivariateSOS.objective (B : DotForm) (p : Poly) (u : UPair) : ℝ

The objective f_p(u) = ⟨σ(u)-p, σ(u)-p⟩ from equation \eqref{eq:nonconvex-obj}.

Equations

• LowRankUnivariateSOS.objective B p u = (B (LowRankUnivariateSOS.residual p u)) (LowRankUnivariateSOS.residual p u)

def LowRankUnivariateSOS.IsFOCP (B : DotForm) (p : Poly) (u : UPair) : Prop

The first-order critical point condition written in the paper's form ⟨A_u(v), σ(u)-p⟩ = 0 for every direction v; see equation \eqref{eq:gradA}.

Equations

• LowRankUnivariateSOS.IsFOCP B p u = ∀ (v : LowRankUnivariateSOS.UPair), (B (LowRankUnivariateSOS.A u v)) (LowRankUnivariateSOS.residual p u) = 0

noncomputable def LowRankUnivariateSOS.hessianTerm (B : DotForm) (p : Poly) (u v : UPair) : ℝ

The quadratic form appearing in the Hessian condition \eqref{eq:hessA}. For a SOCP, this quantity must be nonnegative in every direction v.

Equations

• LowRankUnivariateSOS.hessianTerm B p u v = (B (LowRankUnivariateSOS.sigma2 v)) (LowRankUnivariateSOS.residual p u) + 2 * (B (LowRankUnivariateSOS.A u v)) (LowRankUnivariateSOS.A u v)

def LowRankUnivariateSOS.IsSOCP (B : DotForm) (p : Poly) (u : UPair) : Prop

Second-order criticality in exactly the sense of Definition \ref{def:socp}: the gradient vanishes and the Hessian quadratic form is nonnegative in every direction.

Equations

• LowRankUnivariateSOS.IsSOCP B p u = (LowRankUnivariateSOS.IsFOCP B p u ∧ ∀ (v : LowRankUnivariateSOS.UPair), 0 ≤ LowRankUnivariateSOS.hessianTerm B p u v)

@[simp]

theorem LowRankUnivariateSOS.A_self_eq_sigma2 (u : UPair) : A u u = sigma2 u

Substituting v = u into A_u(v) gives σ(u). This is the elementary identity that lets the FOCP condition immediately say something about the objective itself.

theorem LowRankUnivariateSOS.focp_sigma2_residual_eq_zero {B : DotForm} {p : Poly} {u : UPair} (h : IsFOCP B p u) : (B (sigma2 u)) (residual p u) = 0

Any FOCP satisfies ⟨σ(u), σ(u)-p⟩ = 0. This is equation \eqref{eq:gradA} evaluated at the special direction v = u, and it is used throughout the certificate-style arguments.

theorem LowRankUnivariateSOS.objective_nonneg {B : DotForm} [Fact (LinearMap.BilinMap.toQuadraticMap B).PosDef] (p : Poly) (u : UPair) : 0 ≤ objective B p u

The objective is always nonnegative because it is the quadratic form associated to a positive-definite bilinear form, evaluated at the residual.

theorem LowRankUnivariateSOS.objective_eq_zero_iff_residual_eq_zero {B : DotForm} [Fact (LinearMap.BilinMap.toQuadraticMap B).PosDef] {p : Poly} {u : UPair} : objective B p u = 0 ↔ residual p u = 0

For a positive-definite bilinear form, the objective vanishes exactly when the residual vanishes. This is the formal bridge from the analytic statement f_p(u)=0 to the algebraic statement σ(u)=p.