Assumptions and inequalities

Hello all.

I have some expressions like sums of ratios of real polynomials in a variable t. Mathematically, by assuming t real in a specific interval, each such expression is either always positive, or always non-negative.

For Sage, this is sometimes the case, sometimes not: as you can see, the first one is correct, the second one not


var('t')
expr1 = -1 + (t^2 - 1)/t^2 + 1/t^2
expr2 = (t^2 - 1)/(t^2 - 3)
with assuming(t > 0, t  < 1/2):
print(bool(expr1 <= 0), bool(expr1 > 0))
print(bool(expr2 <= 0), bool(expr2 > 0))


Output: (True, False) \n (False, False)

Questions: Why? How can I avoid this problem?

(An answer to the second question would be enough for me)

edit retag close merge delete

It seems that Sage uses Maxima and Pynac for the assumptions framework. The same problem is present in Maxima 5.39.0:

(%i1) declare(x, real);
(%o1)                                done
(%i2) assume(x > 0, x < 1/2);
1
(%o2)                           [x > 0, x < -]
2
(%i3) is(x^2 - 1 < 0);
(%o3)                                true
(%i4) is(x^2 - 3 < 0);
(%o4)                               unknown
(%i5) is((x^2 - 1)/(x^2 - 3) > 0);
(%o5)                               unknown


I guess that Sage converts Maxima's unknown to False. I tried to track down what Pynac does, but found the code hard to follow.

( 2018-07-05 07:53:47 -0600 )edit
1

Thanks. About my first question: Could the reason be that sqrt(3) is not rational? (I have no idea).

About my second question: I also tried without assumptions in other ways, like by using solve or solve_ineq. But I have similar problems.

Anyway, an alternative procedure that works (that is, an answer to the second question), for me would be considered as a full answer (and very appreciated).

( 2018-07-05 09:17:08 -0600 )edit

The bug or "missing feature" in Maxima (first reported in 2011) is indeed because of irrational roots. To work around your problem I would first treat the numerator and denominator separately (or multiply them, as suggested in the answer below, though this gives a polynomial with larger degree) so the problem is reduced to polynomials. Then it depends on what you want to do: to determine the sign in one interval, or to determine all the intervals on which the sign is constant (the latter can be used to answer the former).

( 2018-07-06 04:11:19 -0600 )edit

Sort by » oldest newest most voted

One possible approach could be to use qepcad optional package. You can install it by typing from a terminal:

sage -i qepcad


Then, you can do something:

sage: var('t')
t
sage: f = qf.forall(t,qf.implies(qf.and_([t>0, t<1/2]), expr2 > 0))
sage: f
(A t)[[t > 0 /\ t < 1/2] ==> (t^2 - 1)/(t^2 - 3) > 0]


But apparently, it takes too much time (unless qepcad is only able do deal with polynomials but the interface does not catch the error, to be investigated). So, if only the sign matters, you can notice that the sign of a/b is the same than the one of a*b, so, up to taking care of the possible cases when b=0, you can do:

sage: f = qf.forall(t,qf.implies(qf.and_([t>0, t<1/2]), expr2.denominator()*expr2.numerator() > 0))
TRUE


Which is correct.

If you want to get a Python boolean, just do:

sage: qepcad(f) == 'TRUE'
True

sage: f = qf.forall(t,qf.implies(qf.and_([t>0, t<1/2]), expr2.denominator()*expr2.numerator() <= 0))
False

more