On 1/31/07, sen1 at math.msu.edu <sen1 at math.msu.edu> wrote:
> It should be possible to use maxima to verify (or actually prove) certain standard
> mathematical formulas in calculus.
>
> For instance, one should be able to prove the chain rule for
> derivatives.
>
> diff(f(g(x)),x) = diff(f(g(x)),g(x))*diff(g(x),x)
>
> for arbitrary functions f and g.
>
> So, I tried
>
> (%i36) is ( diff(f(g(x)),x) = diff(f(g(x)),g(x))* diff(g(x),x));
> (%o36) false
There are a couple of problems here.
First of all, Maxima can't apply the chain rule when it doesn't know
the derivative of the outer function; this is fixable, diff(f(g(x)),x)
should presumably be diff(g(x),x)*at(diff(f(%q1),%q1),[%q1=g(x)]), but
of course this is rather messy (the pdiff package has a different
notation). And I bet that once you start working with "at", you'll
find that some trivial simplifications are missing
Secondly, Maxima can't actually differentiate with respect to anything
other than simple variables. It pretends it can, but this is a
syntactic cheap trick which breaks down in all non-trivial cases, e.g.
diff(f(x^2),f(x)) => 0 (!!) I would in fact classify the fact that
Maxima allows f(x) as a variable of differentiation as a bug, since it
has none of the necessary mechanisms to do anything intelligent with
it. It is correctly giving an error message for a variable of
differentiation of x^2.
Third, you should probably use equal(...,...), not ...=.... The "="
comparison is a syntactic comparison, so (x+1)^2 does not "="
x^2+2*x+1, but it does "equal" it.
> But, for some built in functions, it seems to work.
That is because Maxima knows how to differentiate them.
> Can one prove the Chain Rule using maxima?
Well, leaving aside whether depending on a large, not-proven-correct
(and in fact known-to-have-bugs) software system can "prove" anything
at all....
Yes, but you should use the notion of dependent variables instead of
functions of arguments: depends(a,b); depends(b,c); diff(a,c).
-s