第5期 杨路，等：常用基本不等式的机器证明 ·385· 所以用2条xprove指令，是因为分别考虑了当n为 xprove((1 +A+a)<B*(1+a), 奇数或偶数时的递推。 [1+A<B]); 例11s1证明文献[30]中7.31与7.32出现 及 的相关不等式： xprove(1/(1+A+a)>C*(1-a), 2引>2 [1/(1+A)>C]); 品 21* n-1' xprove(1 -A-a C*(1-a), [(1-A)>C,a<1]); <,> n-1 (37) 计算机耗时不足1s即能证明式(38)和(39)成立. 之=1 例132】考虑文献[37]中的不等式（文献 式中：xk>0,x2>4x1,n≥2. [23]在给出式(40)时有一个明显的打印错误，将式 显然式(37)在n=2时成立.记 (40)左端x的一个下标k误印为i了)： A=了2-’6三=2下， k 三（月P≤（店）9n≥1.（40) 式中：xk>0,a≥1且a+B≥1.该不等式对于确定的 C=∑，D=∑，E= n+一 a和B是可以机器证明的.下面给出α=2，B=-1 ∑ 情形的证明. 对于式(37)中的第1个不等式，执行B0 TTEMA的 显然式(40)在n=1时成立.记A=∑=，B= xprove指令： ∑t=1（∑1x)-x,执行BOTTEMA的xprove指令： xprove(A C/D (n +1)2/n, xprove(B+/(A+x)<=A+x,[B <=A]) [A>n2/(n-1),n>=2,C>=D]); 计算机耗时不足1s即能证明式(40)成立 对于式(37)中的第2个不等式，执行B0 TTEMA的 例142】考虑文献[30]中5.16的不等式： xprove指令： xprove(B +E (n +1)/n, Ain()≥2in(aw）, [B>n/(n-1),n>=2]); 0≤x≤T,n≥1. (41) 计算机耗时不足1s即能证明式(37)成立.事实上， 式(41)在n确定时就是普通的三角不等式，文 式(37)中的第2个不等式不用机器证明，可直接由 献[30]中验证了n=1,2,3,4的情形.在处理三角 下面显然成立的不等式得到. 不等式时，BOTTEMA具有极高的效率，例如，即使 1>"a≥2 n 取n=90,依然可以执行BOTTEMA的prove指令： 例1223】证明文献[31]中3.2.37所谓的 prove(subs(n =90,sum(sin(*A), k=1.n)>sin(n*A)/2); Weierstrass不等式： 计算机在数秒内即验证了式(41)成立. 对于式(41)在n不确定的情况时，直接在Ma ple下键入： (38) sum(sin(x),k =1..n)sin(nx)/2; 及 可将原不等式化为如下的等价形式： >1-a）>1-a 1+a sin(n)sinc((1) 2 co8(x)-1 (39) 2in(a+10）-号o25a里2+2m(e). 式中：n≥1,0<a<1且∑t.iak<1, 2 cos(x)-1 显然式(38)和式(39)在n=1时成立.记 (42) A=∑4，B=Π(1+a), 注意到0≤x≤T,对式(42)两端同乘2(cos(x)- 1),然后用左端减去右端并运行Maple的simplify c=Π(1-a). 指令，即在Maple下键入： 依次执行如下BOTTEMA的prove指令： simplify(expand((cos(x)-1)*sin(n *x)- xprove(1/(1-A-a)>B*(1+a), (sin(x)*cos((n+1)*x)-8in((n+1)*x)* [1/(1-A)>B,A+a<1]); (cos(x)-1)-sin(x)cos(x)sin(x)*