The following program gives an erroneous answer to the ”is” test half-way through, but a correct one at the end. The only diﬀerence is in the ”assume” statement just ahead of the test: whether to assume v = or <= 1/(P*q^n).
The answer should be ”true” regardless. What gives? I am using Maple V 5.1 on a PC.
Actually Maple’s answer is quite correct in this case: it is not true in general that t(n) >= t(n+1) under the assumptions n>=0,v<=1/(P*q^n).
> normal(t(1) - t(2)); 2 v~ (-81 + 4 v~ ) -24 -------------------------- 2 2 (27 + 4 v~ ) (243 + 4 v~ )
The sign depends on the sign of v. But you didn’t tell Maple anything that determines that sign. You probably meant to assume in addition that v >= 0.
> additionally(v >= 0); > is(t(n) >= t(n+1)); FAIL
The ”assume” facility is rather limited in capabilities, so it’s not really all that surprising when a result is ”FAIL”. In general it’s a very diﬃcult problem to decide when an expression is nonnegative for all values of the variables in some region deﬁned by inequalities. In this particular case, I think I can trace some of Maple’s diﬃculties to some rather simple deﬁciencies.
> is(3^n > 0); FAIL
It seems that Maple doesn’t know that a positive power of 3 is positive. In fact it doesn’t even know that this is real. Well, we can tell Maple this:
> additionally(3^n > 0);
Unfortunately, this still doesn’t help. Even though Maple now ”knows” that 3^n > 0, it doesn’t seem able to use that information in other expressions.
> is ((3^n)^2 > 0); FAIL > assume(x > 0); is(x + 3^n > 0); FAIL
It may actually be better to use ”exp”, which Maple seems to know more about, rather than powers of a speciﬁc number. So I’ll change q to exp(lnq), where lnq < 0 (which implies 0 < q < 1).
>The answer should be "true" regardless.
I disagree. In the ﬁrst case n=1 and v=-1 do not contradict your assumptions. If you substitute them into t(n) and t(n+1) then you get:
In the second case assuming v=1/(p*q^n) is virtually the same as substituting it into t(n)-t(n+1). The latter is zero for all n and thus greater than or equal to zero, anyway:
If you make more speciﬁc assumptions about n and v then Maple fails even if _EnvTry is set to ’hard’:
The reason is that Maple cannot determine whether 3^n (or 9^n) is greater than or equal to zero:
This is a weak point of the assume facility, of course.