
Re: can your CAS help proving inequalities?
Posted:
Mar 11, 2013 11:46 AM


Peter Pein schrieb: > > [...] > > Show that for all real a,b,c,d three inequalities hold. Direct > transation into Mathematica code yields (in version 9): > > (* def. of r,s,t omitted *) > In[4]:= InputForm[ > tests=ForAll[{a,b,c,d},Element[{a,b,c,d},Reals],And@@ > (#1[#2[#3@@@{{a,b,c,d},{a,c,b,d},{a,d,c,b}}],0]&@@@{ > {LessEqual,Min,r},{GreaterEqual,Max,s},{LessEqual,Min,t}})] > ] > Out[4]//InputForm= > ForAll[{a, b, c, d}, Element[a  b  c  d, Reals], > Min[(a  c)*(b  c)*(a  d)*(b  d), (a  b)*(b + c)*(a  d)*(c  d), > (a  b)*(a  c)*(b + d)*(c + d)] <= 0 && > Max[(b + c)*(a + d)  2*(b*c + a*d)  Abs[(b + c)*(a  d)], > (a + c)*(b + d)  2*(a*c + b*d)  Abs[(a  c)*(b  d)], > (a + b)*(c + d)  2*(a*b + c*d)  Abs[(a  b)*(c  d)]] >= 0 && > Min[(b + c)*(a + d)  2*(b*c + a*d) + Abs[(b + c)*(a  d)], > (a + c)*(b + d)  2*(a*c + b*d) + Abs[(a  c)*(b  d)], > (a + b)*(c + d)  2*(a*b + c*d) + Abs[(a  b)*(c  d)]] <= 0] > > and on my not too fast box it lasts ~22 seconds to get: > > In[5]:= AbsoluteTiming[FullSimplify[tests]] > Out[5]= {21.934255,True} >
You are posing this as a quantifier elimination problem. Does the simpler
FullSimplify[Max[ (b + c)*(a + d)  2*(b*c + a*d)  Abs[(b + c)*(a  d)], (a + c)*(b + d)  2*(a*c + b*d)  Abs[(a  c)*(b  d)], (a + b)*(c + d)  2*(a*b + c*d)  Abs[(a  b)*(c  d)]] >= 0] /; Element[{a,b,c,d},Reals]
fail? In any event, the problem is presumably again addressed by CAD.
Martin.

