本日のC.A.D.
t が実数，a, b, c がある 3 角形の 3 辺の長さならば
$(a^2+b^2+c^2) (a^{t-2} b^{t-2}+b^{t-2} c^{t-2}+c^{t-2} a^{t-2})<2 (a^t+b^t+c^t)(a^{t-2}+b^{t-2}+c^{t-2})$
1.22 Bottema, et. al. "GEOMETRIC INEQUALITIES"
今回も指数に変数が含まれるので（比の値の範囲ではなく）大小関係の特定に十分な不等式を導入し，（過剰ですが）その辺々の比の値の範囲を求めます．具体的には，a^{t-2}，b^{t-2}，c^{t-2} をそれぞれ x，y，z と一般化して
$(a^2+b^2+c^2) (xy+yz+zx)<2(a^2x+b^2y+c^2z)(x+y+z)$
また，不等式制約は，対称性により，a, b, c の広義増加性と 3 角不等式，一方，t が任意なので，x, y, z については正値広義単調性までとします．
? tst12([ex,ex,ex,ex,ex,ex],[d,x,y,z,a,b,c],andx,"0<a,a<=b,b<=c,c<a+b,0<x,x<=y,y<=z,0<d,(a^2+b^2+c^2)*(x*y+y*z+z*x)==d*(a^2*x+b^2*y+c^2*z)*(x+y+z)");Ans(); *** using Lazard's method (MPP17). [c,3] [b,4] [a,1] [z,12] [y,43] [x,1] [d,377] time = 8,841 ms. 1031 1031(0,0) 29204(78,1598) 320854(4336,29828) 320854(0,0) 983448(38288,145366) 566(47168,1130) *** combined adjacent 565 cells. 1[[d,1] < d <= [d-1,1],true,true,true,true,true,true] time = 13min, 19,415 ms. ? tst12([ex,ex,ex,ex,ex,ex],[d,x,y,z,a,b,c],andx,"0<a,a<=b,b<=c,c<a+b,0<z,z<=y,y<=x,0<d,(a^2+b^2+c^2)*(x*y+y*z+z*x)==d*(a^2*x+b^2*y+c^2*z)*(x+y+z)");Ans(); *** using Lazard's method (MPP17). [c,3] [b,4] [a,1] [z,13] [y,43] [x,1] [d,377] time = 8,559 ms. 1031 3093(0,0) 117166(61974,47520) 201216(40502,139587) 201216(0,0) 690484(41426,95670) 795(0,1590) *** combined adjacent 794 cells. 1[[d,1] < d < [d-2,1],true,true,true,true,true,true] time = 11min, 30,179 ms. ? tst12([ex,ex,ex,ex,ex,ex],[d,x,y,z,a,b,c],andx,"0<a,a<=b,b<=c,c<a+b,0<x,0<z,(y-x)*(y-z)<=0,0<d,(a^2+b^2+c^2)*(x*y+y*z+z*x)==d*(a^2*x+b^2*y+c^2*z)*(x+y+z)");Ans(); *** using Lazard's method (MPP17). [c,3] [b,4] [a,1] [z,13] [y,43] [x,1] [d,377] time = 8,570 ms. 1031 1031(0,0) 114073(78,1598) 521039(26034,109955) 521039(0,0) 1671870(79714,241034) 795(0,1590) *** combined adjacent 794 cells. 1[[d,1] < d < [d-2,1],true,true,true,true,true,true] time = 26min, 57,177 ms.
更に a=1 とすると，x=1 なので 5 変数となり
? tst12([ex,ex,ex,ex],[d,z,y,b,c],andx,"1<=b,b<=c,c<1+b,1<=y,y<=z,0<d,(1+b^2+c^2)*(y+y*z+z)==d*(1+b^2*y+c^2*z)*(1+y+z)");Ans(); *** using Lazard's method (MPP17). [c,3] [b,4] [y,13] [z,40] [d,237] time = 2,281 ms. 625 67211(68,1376) 104558(15730,64574) 337786(12140,29078) 342(11048,682) *** combined adjacent 341 cells. 1[[d,1] < d <= [d-1,1],true,true,true,true] time = 4min, 25,670 ms. ? tst12([ex,ex,ex,ex],[d,z,y,b,c],andx,"1<=b,b<=c,c<1+b,1>=y,y>=z,z>0,0<d,(1+b^2+c^2)*(y+y*z+z)==d*(1+b^2*y+c^2*z)*(1+y+z)");Ans(); *** using Lazard's method (MPP17). [c,3] [b,4] [y,13] [z,40] [d,237] time = 2,266 ms. 625 29875(68,1376) 104556(4584,33736) 342718(20434,39140) 473(0,946) *** combined adjacent 472 cells. 1[[d,1] < d < [d-2,1],true,true,true,true] time = 3min, 14,980 ms. ? tst12([ex,ex,ex,ex],[d,z,y,b,c],andx,"1<=b,b<=c,c<1+b,0<z,(y-1)*(y-z)<=0,0<d,(1+b^2+c^2)*(y+y*z+z)==d*(1+b^2*y+c^2*z)*(1+y+z)",7);Ans(); *** using the sum of squares projection. [c,3] [b,4] [y,13] [z,40] [d,237] time = 8,947 ms. 625 27975(66,1227) 181357(4586,30227) 580316(32238,67214) 473(0,946) *** combined adjacent 472 cells. 1[[d,1] < d < [d-2,1],true,true,true,true] time = 5min, 38,770 ms.
のように高速化されます．
なお，一般化の大小関係の特定（∀X[P→Q] が True，つまり，∃X[P/\¬Q] が False であること）のみなら
? tst12([ex,ex,ex,ex,ex,ex],[z,y,x,b,c,a],andx,"0<a,a<=b,b<=c,c<a+b,0<x,0<z,(y-x)*(y-z)<=0,(a^2+b^2+c^2)*(x*y+y*z+z*x)>=2*(a^2*x+b^2*y+c^2*z)*(x+y+z)");Ans(); *** using Lazard's method (MPP17). [a,4] [c,5] [b,1] [x,11] [y,23] [z,1] time = 241 ms. 1 25(0,0) 27(8,23) 81(0,0) 320(154,147) 0(110,436) 1[false] time = 328 ms. ? tst12([ex,ex,ex,ex],[z,y,b,c],andx,"1<=b,b<=c,c<1+b,0<z,(y-1)*(y-z)<=0,(1+b^2+c^2)*(y+y*z+z)>=2*(1+b^2*y+c^2*z)*(1+y+z)");Ans(); *** using Lazard's method (MPP17). [c,3] [b,4] [y,10] [z,8] time = 148 ms. 7 23(0,6) 46(8,4) 0(0,0) 1[false] time = 38 ms.
のように容易です．
