第5期 杨路,等:常用基本不等式的机器证明 ·379· 正实数,则 对于算术与几何平均不等式(1)的机器证明, a“T. 还可以采取多种其他不同的策略,例如,容易知道, n n 日 算术与几何平均不等式(1)等价于如下的Jacobsthal 不等式[]: 显然,仅需对n个正实数a1,a2,…,an,证明如 (Ha>0,b>0,n≥1)(n-1)a"+b"≥ 下的算术与几何平均不等式: na"-1b. (8) “Ta, (1) 事实上,只需在式(5)中令¥=片,即可得到式(5) 与式(8)的等价性.式(8)对于n=1的情形是显然 即可直接证明几何与调和平均不等式,因为1,1 a1'a2 成立的,用数学归纳法完成式(8)的证明,只需引进 …,1皆为正实数,利用式(1)有 新变元s、t,执行BOTTEMA的xprove指令: an xprove(n*s*a+tb>= (n+1)*s*a*b,[(n-1)*s*a+t>=n*s*b]); ≥ (2) 屏幕几乎立即提示“The inequalitity holds'”. n 对于几何与调和平均不等式(3),也可仿照上 将式(2)取倒数即得 述过程给出其机器证明方法,当然,直接利用算术与 VΠ4≥ n (3) 几何平均不等式(1)证明几何与调和平均不等式 (3)的过程也是非常简单的 如果考虑如下的算术与调和平均不等式: 下面给出式(1)的证明.容易验证式(1)在n= 1时成立.按照数学归纳法,假设式(1)成立,则需要 ≥n ∑”1 (9) 证明 n N+I 2k=1 dx T 类似上面的讨论,引进新变元A、B,执行BOTTEMA 的prove指令: 亦成立.由于式(1)成立,只需证 xprove((A +a)/(n +1)>= n3VT4+a≥(n+1)Va 4中 (n+1)/(B+1/a),[A/n>n/B]); 上式可以改写成: 即完成了式(9)的机器证明. I +1 l.2 Cauchy不等式的机器证明 n· a +1≥(n+1) (4) Cauchy不等式(Cauchy inequality)设x1,2, …,xn及y1,y2,…,y为2组实数数列,则 方便起见,作代换 正=心,式4)变为 +1 (∑)2≤∑∑元 an+l nx+1+1≥(n+1)x”. 该不等式的机器证明实现参见文献[1,23],文献 (5) [23]基于QEPCAD,而文献[1]是基于BOTTEMA 现在,仅需证明式(5)对任意正数x和任意正整数n 成立即可.仍用数学归纳法,记式(5)为中,显然1 的.下面采用文献[1]的方法,记中n是如下公式: 成立.为证 (∑tw)-∑a∑ti≤0, 中n→中n+1, (6) 容易验证中1和中2成立.按照数学归纳法,需要证明 这时引进新的变元「,考虑命题: 中→0n+1: (10) (Vr>0,x>0,n≥1)nrx+1≥(n+1)r→ 这时引进新的变元r、s、t、xy,考虑命题: (n+1)rx2+1≥(n+2)rx. (7) (HT,s,t,x,y)r2≤st→ 如果式(7)为真,那么式(6)当然就为真,因为可以 (r+y)2≤(s+x2)(t+y2). (11) 令T代表x”,由于r、x、n全都是非负,因此可以执行 如果式(11)为真,那么式(10)当然就为真,因为可 BOTTEMA的xprove指令: 以令T、s、t、xy分别代表∑t=xy、∑t=1x、∑=1yi、 xprove((n +1)**1>= x+1y+…但式(11)和式(10)显然并不等价,事实 (n+2)*r*x,[n*T*x+1>=(n+1)*r]); 上,如果对实变量T、s、、x、y不附加任何其他条件的 屏幕几乎立即提示“The inequalitity holds”.这即完 话,命题式(11)是不成立的. 成了算术几何平均不等式的证明. 注意,式(11)是一个实量词消去问题,因而