使用计算机辅助的平方和方法证明不等式

本文将介绍如何使用计算机辅助平方和方法证明一些复杂不等式. 具体地说, 要证明多项式 $f(x) = f(x_1,\cdots,x_n)$ 在 $\mathbb R^n$ 上是非负的, 一个充分条件是将 $f(x_1,\cdots,x_n)$ 写成一些多项式的平方和 (Sum of Squares, SOS). 或等价地, 构造列向量 $Z(x)$ 和半正定矩阵 $Q$ 使得 $f(x) = Z(x)^\top Q Z(x)$ .

理论基础

平方和方法的理论基础是半定规划 (semidefinite programming, SDP), 相关理论可以在任何一本凸优化的教材中找到.

(施工中)

使用方法

以下是一些能够将多项式写为平方和性质的数学软件.

Macaulay2

Macaulay2 是一个为代数几何和交换代数开发的软件, 语法类似于 Maple. 直接调用软件原生的 SumsOfSquares 功能就可以实现平方和的功能. Macaulay2 不提供原生的 Windows 安装包 (需要在 Windows Linux Subsystem 中使用)，但是可以在 SageMathCell (复制下面的代码, 然后点这个!) 里线上运行.

以下是证明 Vasile Cirtoaje 的著名不等式 $(x^2+y^2+z^2)^2\ge 3(x^3y+y^3z+z^3x)$ 的示例代码:

needsPackage("SumsOfSquares");
R = QQ[x,y,z];
f = (x^2+y^2+z^2)^2-3*(x^3*y+y^3*z+z^3*x);
sosPoly solveSOS f

该代码的输出结果为

      1 2         1      1      1 2 2    9    1 2   2 2               1 2 2
(3)(- -x  + x*y - -x*z - -y*z + -z )  + (-)(- -x  + -y  + x*z - y*z - -z )
      2           2      2      2        4    3     3                 3
SOSPoly

因此平方和的表达式为 $\dfrac14(-x^2+2xy-xz-yz+z^2)^2 + \dfrac14(-x^2+2y^2+3xz-3yz-z^2)^2$ .

Mathematica

作为知名的符号计算软件, Mathematica 也提供了原生的 SOS 功能. 使用下面的代码可以证明 Vasile Cirtoaje 不等式.

p[x_,y_,z_]:=(x^2+y^2+z^2)^2-3*(x^3*y+y^3*z+z^3*x);
PolynomialSumOfSquaresList[p[x,y,z],{x,y,z}]

上述命令将输出两个2次多项式, 并且 $p(x,y,z)$ 恰好是这两个多项式的平方和.

不过, 实际测试中 Mathematica 的计算速度比 Macaulay2 慢不少, 对于较难的问题无法输出正确结果.

MATLAB+Mosek+SOSTOOLS

MATLAB+Mosek+SOSTOOLS 来计算平方和是我测试过的性能较强的 SOS 计算软件, 它将直接给出半正定矩阵 $Q$ 的形式, 因此可以将复杂的不等式证明转化为高阶方阵的特征值问题.

MATLAB (付费) 可以从官方网站下载, 且需安装符号计算工具箱 Symbolic Math Toolbox.
Mosek (教育免费) 可以从官方网站下载, 使用 edu 教育邮箱可以免费获取许可证.
SOSTOOLS 可以从 MATLAB 的官方网站下载.

安装完毕后, 使用下面的 MATLAB 代码可以证明 Vasile Cirtoaje 不等式.

% 1. Construct target polynomial
pvar a b c
p = (a^2+b^2+c^2)^2-3*(a^3*b+b^3*c+c^3*a);
% 2. Find sum of square expression
solver_opt.solver = 'mosek';
[Q,Z] = findsos(p,'rational',solver_opt);

该代码将同时输出向量 $Z$ 和半正定矩阵 $Q$ , 其中 $Q$ 的表达式为

SOSTOOLS 和我的一些示例代码可以从百度网盘下载, 但 MATLAB 和 Mosek 仍需单独下载.

结尾

如果你在安装或使用中遇到任何问题, 可以在下面留下评论.

Xuda Ye