This project formalizes in Lean 4 a low-rank sum-of-squares result for univariate polynomials. Its main theorem shows that for the rank-2 quadratic-penalty objective, every second-order critical point is globally optimal.
Useful links:
This project formalizes in Lean 4 a low-rank sum-of-squares result for univariate polynomials. Its main theorem shows that for the rank-2 quadratic-penalty objective, every second-order critical point is globally optimal.
Useful links: