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.

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 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)`

.

> 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 ﬁ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:

> 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 speciﬁc 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.