Is There a Formal Proof of the Multivariable Chain Rule?

[ice109]

can someone link/show me a formal proof of the multivariable chain rule?

 

[slider142]

There's a cute proof of this in Spivak's "Calculus on Manifolds". If you want to try it yourself, try defining the function f_d(x) = f(x + h) - f(x) - df(h) and similarly for g, pretty much the numerator in the definition of the derivative, then evaluating the limit in the definition of the derivative for $g\circ f$, where you let the linear function in the limit be dg(f(x))df(x).

 

[ice109]

what? how is this multavariable?

 

[lurflurf]

what? how is this multavariable?

let x be a vector x=(x1,x2,...,xn)

 

[ObsessiveMathsFreak]

There must be a better proof of the chain rule that that.

 

[ice109]

There must be a better proof of the chain rule than that.

yea i thought of that and thought the same thing; that there's got to be a more rigorous proof.

 

[lurflurf]

yea i thought of that and thought the same thing; that there's got to be a more rigorous proof.

more rigorous than very rigorous
interesting
maybe you mean more detailed
that I can provide

Chain rule
let
f:E->F
g:F->G
with E (or a subset) open in F
F (or a subset) open in G
and f differentiable at x
g differentiable at f(x)
then
(g◦f)' exist with
(g◦f)'=[g'◦f][f']
or in more full notation
[g(f(x))]'=[g'(f(x)][f'(x)]
notes on mappings
f:E->F
g:F->G
f':E->L(E,F)
g':F->L(F,G)
(g◦f):E->G
(g◦f)':E->L(E,G)
g'◦f:E->(F,G)
[g'◦f][f']:E->L(E,G)
where L(E,F) is a space of linear mappings from E to F
so all is as it should be
thus derivatives are linear mappings
Δx=dx
Δf:=f(x+dx)-f(x)
df:=f'(x)dx
Δf=df+o(dx) (f differentiable)
informal derivation
dg(f(x))=g'(f(x))df(x)+o(df(x))=g'(f(x))f'(x)dx+o(dx)+f'(x)o(dx)
more formal
let
Δf=df+|dx|rf
rf=(Δf-df)/|dx|
so lim rf=0
now
lim rf=lim rg=0 (f,g differentiable)
Δ[g(f(x))]=g'(f(x))Δf(x)+|Δf|rg(f(x))
=g'(f(x))f'(x)dx+|dx|r(f)+|dx||f'(x)dx/|dx|+rf|rg)
=g'(f(x))f'(x)dx+|dx|{rf+|f'(x)dx/|dx|+rf|rg}
we now need only
lim {r(f)+|f'(x)dx/|dx|+rf(x)|rg(f(x))}=0
which is clear from
rf(x)->0
rg(f(x))->0
and
|f'(x)dx/|dx|+rf|<|f'(x)|+|rf|<∞
ie bounded near x
where |f'(x)| is the norm induced on linear maps by the norm on vectors