Thankyou for replying to my question.
Your two solution lead both to the right answer:
(%i1) input(k) :=
-(k+1)*binomial(n,k+1)/(2*(n-k)*2^n);
(%i2) ratsubst( (n-k)*binomial(n,k),
(k+1)*binomial(n,k+1),
input(k) );
(%o2) -binomial(n,k)/(2*2^n)
(%i3) binomial_id :
'binomial = lambda([n,k], (n-k + 1) *
binomial(n,k-1)/k);
(%o3) binomial=
lambda([n,k],((n-k+1)*binomial(n,k-1))/k)
(%i4) subst(binomial_id, input(k) );
(%o4) ((-k-1)*binomial(n,k))/(2*(k+1)*2^n)
(%i5) ratsimp(%);
(%o5) -binomial(n,k)/(2*2^n)
Actually, I prefer the first one:
with the rewriting of the function "binomial" that
Burton suggested, everytime I have a bin coef it
is rewritten with a "k" at the denominator, so the
rewriting is not true if k=0 (it adds a singularity
for free). In my example it is simplified with
another k at numerator, but sometimes it cannot
happens.
This was the last piece of a little script that make
nusum suitable for my purpose, that is make some
binomial sequence telescopic with Maxima and than
check this with HOLlight: the obstacle was that
while Maxima does syntactic manipulation doesn't
mind of roots of denominators, but when HOL check it,
it cares a lot about that.
I had three example to "unificate":
THEOREM 1
a(k) = binomial(n+1,k)/2^(n+1) - binomial(n,k)/2^n
is telescoped in the variable k by
f(k) = -binomial(n,k)/2^(n+1), in the sense that
a(k) = f(k) - f(k-1)
note that -binomial(n,k)/2^(n+1) and
-(k+1)*binomial(n,k+1)/(2*(n-k)*2^n) are *almost*
the same: what about k=n?
THEOREM 2
binomial(n+1,k)*(n+1)!/((n+1+a)!*k!*(a-k)!) -
binomial(n,k)*(n)!/((n+a)!*k!*(a-k)!)
is telescoped by
-binomial(n,k)*n!/(k!*(n+1+a)!(a-k+1)!)
THEOREM 3
(-1)^k*binomial(n+1,k)*(n+1+a)/(binomial(k+a,k)*a) -
(-1)^k*binomial(n,k)*(n+a)/(binomial(k+a,k)*a)
is telescoped by
-(-1)^(k+1)*binomial(n,k)*
(k+1+a)/((a*binomial(k+1+a,k+1))
thanks to your suggestions, I handled all these in the
same way, hidding the (virtual) singularities under
the carpet, to make HOLlight happy:
input(k) := binomial expression to telescope;
defrule(h,
binomial(n+1,k),
binomial(n,k)*(n+1)/(n+1-k));
(* now I'm adding singularities with this syntactic
rewriting, but I'll "delete" it at the end. I have
to rewrite, otherwise nusum won't recognize the
hypergeometric form of the expression *)
minfactorial( ratsimp( apply1(input(k),h) ) );
nusum(%,k,0,k);
(* now I often have stupid singularities,
but I clean it with the next istruction *)
ratsubst( (n-k)*binomial(n,k),
(k+1)*binomial(n,k+1),
%);
output(k) := ratsimp(%);
Thankyou again.
Giovanni Gherdovich
Chiacchiera con i tuoi amici in tempo reale!
http://it.yahoo.com/mail_it/foot/*http://it.messenger.yahoo.com