[Date Index]
[Thread Index]
[Author Index]
Re: Recursive Proofs...
*To*: mathgroup at smc.vnet.net
*Subject*: [mg29965] Re: Recursive Proofs...
*From*: Ignacio Rodriguez <ignacio at sgirmn.pluri.ucm.es>
*Date*: Fri, 20 Jul 2001 03:28:29 -0400 (EDT)
*Organization*: UCM
*References*: <9j0hdr$fje$1@smc.vnet.net>
*Sender*: owner-wri-mathgroup at wolfram.com
Dear Mr Trichard,
It is possible to use mathematical induction, but please be aware that
Mathematica will not do it by itself.
For example, imagine we define f as
f[0]=0;
f[n_]:=r f[n-1]+a;
and we want to prove that f[n] equals a Sum[r^i,{i,0,n-1}]. We cannot use just
Simplify[f[n]==a Sum[r^i,{i,0,n-1}] as this would lead to an infinite
recursion. However, we can try induction like this
Simplify[(0==a Sum[r^i,{i,0,-1}])&&(r a Sum[r^i,{i,0,n-1}]+a==a
Sum[r^i,{i,0,n}])]
In your case, if you have a 2d recursion it may be a bit more difficult, but
the procedure is esencially the same.
Louis Trichard wrote:
> Dear All,
>
> I have a complicated 2d recursion in which I'd like to prove that the
> r(i,i) = a^i. (i.e. something simple) by induction. I've left out the
> definition of the recursive function, since it is not necessary.
>
> I can use mathematica to show this simple expression for i = 1..100 or
> more, i.e. Simplify[r[10,10]] = a^10, but this is no proof.
>
> I would like some general advice on:
> 1/ How could one use mathematica to help prove such recursive
> expressions by induction (or other methods) for general i, i.e. I know one
> cannot use Simplify[r[i,i]], since this would give an infinite recursion
> depth error.
>
> Thanks for all your help,
>
> Louis Trichard
--
Ignacio Rodriguez Ramirez de Arellano
Unidad de RMN
Universidad Complutense
Paseo Juan XXIII, 1
Madrid 28040, Spain
Tel. 34-91-394-3288
Fax 34-91-394-3245
e-mail: ignacio at sgirmn.pluri.ucm.es
Prev by Date:
**Re: slow integration**
Next by Date:
**Re: notation help: f(x) = (sin x)^(1/3)**
Previous by thread:
**Recursive Proofs...**
Next by thread:
**Nonlinear regression with a complex-valued model function**
| |