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


Am 10.03.2013 20:27, schrieb Nasser M. Abbasi: > On 3/10/2013 11:57 AM, clicliclic@freenet.de wrote: > >> >> Since the Mathematica variables are complex by default, they must here >> perhaps be explicitly restricted to real. > > Sure. > >  > FindInstance[ > Min[r[a, b, c, d], r[a, c, b, d], r[a, d, c, b]] > 0, {a, b, c, > d}, Reals] > > FindInstance[ > Min[r[a, b, c, d], r[a, c, b, d], r[a, d, c, b]] > 0, {a, b, c, > > d}, Reals] > FindInstance[ > Min[t[a, b, c, d], t[a, c, b, d], t[a, d, c, b]] > 0, {a, b, c, > d}, Reals] >  > > {} > {} > {} >  > >> Judging form the "Notes On >> Internal Implementation" it looks like Mathematica's Reduce[] might be >> able to do reduce such inequalities: among other techniques, it fields >> cylindrical algebraic decomposition (CAD). >> >> Martin. >> > > yes: > >  > Reduce[Min[r[a, b, c, d], r[a, c, b, d], r[a, d, c, b]] > 0, {a, b, c, > d}, Reals] > > Reduce[Min[r[a, b, c, d], r[a, c, b, d], r[a, d, c, b]] > 0, {a, b, c, > d}, Reals] > > Reduce[Min[t[a, b, c, d], t[a, c, b, d], t[a, d, c, b]] > 0, {a, b, c, > d}, Reals] >  > False > False > False >  > > Nasser
Hi,
without doubt this is a possibility. The original task has been:
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}
Cheers, Peter

