
Re: can your CAS help proving inequalities?
Posted:
Mar 11, 2013 12:00 PM


Am 11.03.2013 16:46, schrieb clicliclic@freenet.de: > > 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. > No, it succeeds  but it is by two orders of magnitude faster :)
In[1]:= 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] ] // AbsoluteTiming
Out[1]= {0.187011, True}
Peter

