The following program gives an erroneous answer to the "is" test half-way through, but a
correct one at the end. The only difference 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.
y:=n->v*(1-q^n); m:=n->y(n)-y(n-1); t:=n->(m(n)-m(n+1))/(1+m(n)*m(n+1)); P:=2/3; q:=1-P; t(n); expand(%); assume(n>=0,v<=1/(P*q^n)); about(v); is(t(n)>=t(n+1)); restart; y:=n->v*(1-q^n); m:=n->y(n)-y(n-1); t:=n->(m(n)-m(n+1))/(1+m(n)*m(n+1)); P:=2/3; q:=1-P; t(n); expand(%); assume(n>=0,v=1/(P*q^n)); about(v); is(t(n)>=t(n+1));
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).
For example:
> 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 difficult problem to decide when an expression is nonnegative for all values of the variables in some region defined by inequalities. In this particular case, I think I can trace some of Maple’s difficulties to some rather simple deficiencies.
> 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 specific number. So I’ll change q to exp(lnq), where
lnq < 0 (which implies 0 < q < 1).
> restart; y:=n->v*(1-exp(n*lnq)); > m:=n->y(n)-y(n-1); > t:=n->(m(n)-m(n+1))/(1+m(n)*m(n+1)); > assume(n>=0, v<= 1/((1-exp(lnq))*exp(n*lnq)), v>=0, lnq<0); > is(t(n)>=t(n+1));
true
>The answer should be "true" regardless.
I disagree. In the first 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:
> restart; > y:=n->v*(1-q^n): > m:=n->y(n)-y(n-1): > t:=n->(m(n)-m(n+1))/(1+m(n)*m(n+1)): > p:=2/3: q:=1-p: > assume(n>=0,v<=1/(p*q^n)); > is(t(n)>=t(n+1)); false > simplify(subs({n=1,v=-1},t(n)-t(n+1))); -1848 ----- 7657 > is(%>=0); false
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:
> restart; > y:=n->v*(1-q^n): > m:=n->y(n)-y(n-1): > t:=n->(m(n)-m(n+1))/(1+m(n)*m(n+1)): > p:=2/3: q:=1-p: > assume(n>=0,v=1/(p*q^n)); > is(t(n)>=t(n+1)); true > simplify(subs({v=1/(p*q^n)},t(n)-t(n+1))); 0 > is(%>=0); true
If you make more specific assumptions about n and v then Maple fails even if _EnvTry is set
to ’hard’:
> restart; > y:=n->v*(1-q^n): > m:=n->y(n)-y(n-1): > t:=n->(m(n)-m(n+1))/(1+m(n)*m(n+1)): > p:=2/3: q:=1-p: > e:=simplify(t(n)-t(n+1)); n (n + 1) 2 3 v (9 - 4 v ) e := 8 ---------------------------- n 2 n 2 (3 9 + 4 v ) (27 9 + 4 v ) > assume(n,nonnegint); > assume(v,positive); > additionally(v<=1/(p*q^n)); > _EnvTry:=hard: > is(e,nonneg); FAIL
The reason is that Maple cannot determine whether 3^n (or 9^n) is greater than or equal
to zero:
> [op(e)]; n~ (n~ + 1) 2 1 1 [8, 3 , v~, 9 - 4 v~ , -------------, --------------] n~ 2 n~ 2 3 9 + 4 v~ 27 9 + 4 v~ > map(is,%,nonneg); [true, FAIL, true, FAIL, FAIL, FAIL] > is(3^n,nonneg); FAIL
This is a weak point of the assume facility, of course.