multivariable chain-rule proof?

[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 fd(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 gotta be a more rigorous proof.

[lurflurf]

yea i thought of that and thought the same thing; that there's gotta 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