Examples (5)

　今回は分数不等式についての証明です．
　4変数の3次分数式は，CADによるQEでは難しいようです．

Reduce[ForAll[ {a, b, c, d},
a >= 0 && b >= 0 && c >= 0 && d >= 0 && a + b + c + d == 4,
a/(a^3 + 8) + b/(b^3 + 8) + c/(c^3 + 8) + d/(d^3 + 8) <= 4/9 ] ]
...

　一方

# prove(`&0<=a /\ &0<=b /\ &0<=c /\ &0<=d /\ a+b+c+d= &4 ==> (a / (a pow 3 + &8)
+ b / (b pow 3 + &8)+ c / (c pow 3 + &8) + d / (d pow 3 + &8) <= &4 / &9)` ,
let lemma1,lemma2=IMP_TRANS
(REAL_SOS `&0<=x ==> (&0< x pow 3 + &8 /\ &27*x<=(&2*x+ &1)*(x pow 3 + &8) )`)

(REAL_SOSFIELD`(&0< x pow 3 + &8 /\ &27*x<=(&2*x+ &1)*(x pow 3 + &8) )==>x /
(x pow 3 + &8) <= (&2 * x + &1) / &27`),
REAL_ARITH`x<=(&2*a+ &1)/ &27 /\ y<=(&2*b+ &1)/ &27 /\ z<=(&2*c+ &1)/ &27 /\ w<=(&2*d+ &1)/ &27 /\ a+b+c+d= &4 ==> x+y+z+w<= &4/ &9` in
MESON_TAC[lemma1;lemma2;] );;
1 basis elements and 0 critical pairs
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Searching with depth limit 4
Searching with depth limit 5
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Translating proof certificate to HOL
Searching with depth limit 0
Searching with depth limit 1
Searching with depth limit 2
Searching with depth limit 3
Searching with depth limit 4
csdp warning: Reduced accuracy
Translating proof certificate to HOL
0..0..1..2..3..7..12..18..28..38..48..84..120..160..245..330..solved at 444
val it : thm =
|- &0 <= a /\ &0 <= b /\ &0 <= c /\ &0 <= d /\ a + b + c + d = &4
==> a / (a pow 3 + &8) +
b / (b pow 3 + &8) +
c / (c pow 3 + &8) +
d / (d pow 3 + &8) <=
&4 / &9

のようになり，SOS系を用いないなら

# let lemma01,lemma02=
REAL_FIELD`&0 (&2 * x + &1) / &27 - x / (x pow 3 + &8) = *1`,
MESON[REAL_LE_ADD;REAL_LE_DIV;REAL_LE_MUL;REAL_LE_POW_2;REAL_POW_LE;REAL_LET_A
DD;REAL_ARITH`&0<= &2 /\ &0<= &39/ &8 /\ &0<= &27 /\ &0<= &8 /\ &0< &8`]`&0<=x =
=> ( &0<=*2 /\ &0 (&2 * x + &1) / &27 - x / (x pow 3 + &8) =
*3
val lemma02 : thm =
|- &0 <= x
==> &0 <=
*4 /\
&0 < x pow 3 + &8
# MESON[lemma01;lemma02;REAL_SUB_LE]`&0<=x ==> x / (x pow 3 + &8) <= (&2 * x + &
1) / &27`;;
0..0..1..3..6..13..25..43..72..124..204..solved at 296
val it : thm = |- &0 <= x ==> x / (x pow 3 + &8) <= (&2 * x + &1) / &27

とすれば良いでしょう．

*1:&2* (x + &5 / &4 ) pow 2 + &39 / &8)*(x- &1) pow 2) / (&27*(x pow 3 + &8

*2:&2*(x + &5 / &4 ) pow 2 + &39 / &8)*(x- &1) pow 2) / (&27*(x pow 3 + &8

*3:&2 * (x + &5 / &4) pow 2 + &39 / &8) * (x - &1) pow 2) / (&27 * (x pow 3 + &8

*4:&2 * (x + &5 / &4) pow 2 + &39 / &8) * (x - &1) pow 2) / (&27 * (x pow 3 + &8