let m be non zero Nat; for f being PartFunc of (REAL-NS m),(REAL-NS 1)
for X being Subset of (REAL-NS m)
for x being Point of (REAL-NS m) st X is open & x in X & ( for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) holds
( f is_differentiable_in x & ( for h being Point of (REAL-NS m) ex w being FinSequence of REAL 1 st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> ) & (diff (f,x)) . h = Sum w ) ) )
let f be PartFunc of (REAL-NS m),(REAL-NS 1); for X being Subset of (REAL-NS m)
for x being Point of (REAL-NS m) st X is open & x in X & ( for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) holds
( f is_differentiable_in x & ( for h being Point of (REAL-NS m) ex w being FinSequence of REAL 1 st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> ) & (diff (f,x)) . h = Sum w ) ) )
let X be Subset of (REAL-NS m); for x being Point of (REAL-NS m) st X is open & x in X & ( for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) holds
( f is_differentiable_in x & ( for h being Point of (REAL-NS m) ex w being FinSequence of REAL 1 st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> ) & (diff (f,x)) . h = Sum w ) ) )
let x be Point of (REAL-NS m); ( X is open & x in X & ( for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) implies ( f is_differentiable_in x & ( for h being Point of (REAL-NS m) ex w being FinSequence of REAL 1 st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> ) & (diff (f,x)) . h = Sum w ) ) ) )
assume A1:
( X is open & x in X & ( for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) )
; ( f is_differentiable_in x & ( for h being Point of (REAL-NS m) ex w being FinSequence of REAL 1 st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> ) & (diff (f,x)) . h = Sum w ) ) )
A2:
( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS 1) = REAL 1 )
by REAL_NS1:def 4;
reconsider One0 = <*jj*> as Element of REAL 1 by FINSEQ_2:98;
reconsider One = One0 as Point of (REAL-NS 1) by REAL_NS1:def 4;
reconsider f0 = f as PartFunc of (REAL m),(REAL 1) by A2;
reconsider X0 = X as Subset of (REAL m) by REAL_NS1:def 4;
reconsider x0 = x as Element of REAL m by REAL_NS1:def 4;
A3:
X0 is open
by A1;
A4:
now for i being Nat st 1 <= i & i <= m holds
( f0 is_partial_differentiable_on X0,i & f0 `partial| (X0,i) is_continuous_on X0 )let i be
Nat;
( 1 <= i & i <= m implies ( f0 is_partial_differentiable_on X0,i & f0 `partial| (X0,i) is_continuous_on X0 ) )assume A5:
( 1
<= i &
i <= m )
;
( f0 is_partial_differentiable_on X0,i & f0 `partial| (X0,i) is_continuous_on X0 )then A6:
f is_partial_differentiable_on X,
i
by A1;
hence A7:
f0 is_partial_differentiable_on X0,
i
by Th33;
f0 `partial| (X0,i) is_continuous_on X0A8:
f `partial| (
X,
i)
is_continuous_on X
by A1, A5;
A9:
(
dom (f0 `partial| (X0,i)) = X0 & ( for
x0 being
Element of
REAL m st
x0 in X0 holds
(f0 `partial| (X0,i)) /. x0 = partdiff (
f0,
x0,
i) ) )
by Def5, A7;
A10:
for
z being
Element of
REAL m st
z in X0 holds
ex
y being
Point of
(REAL-NS m) st
(
z = y &
(f0 `partial| (X0,i)) /. z = (partdiff (f,y,i)) . One )
proof
let z be
Element of
REAL m;
( z in X0 implies ex y being Point of (REAL-NS m) st
( z = y & (f0 `partial| (X0,i)) /. z = (partdiff (f,y,i)) . One ) )
assume A11:
z in X0
;
ex y being Point of (REAL-NS m) st
( z = y & (f0 `partial| (X0,i)) /. z = (partdiff (f,y,i)) . One )
then
f0 is_partial_differentiable_in z,
i
by A7, A5, A3, Th34;
then consider g being
PartFunc of
(REAL-NS m),
(REAL-NS 1),
y being
Point of
(REAL-NS m) such that A12:
(
f0 = g &
z = y &
partdiff (
f0,
z,
i)
= (partdiff (g,y,i)) . <*1*> )
by PDIFF_1:def 14;
take
y
;
( z = y & (f0 `partial| (X0,i)) /. z = (partdiff (f,y,i)) . One )
thus
z = y
by A12;
(f0 `partial| (X0,i)) /. z = (partdiff (f,y,i)) . One
thus
(f0 `partial| (X0,i)) /. z = (partdiff (f,y,i)) . One
by A12, A11, Def5, A7;
verum
end;
for
z0 being
Element of
REAL m for
r being
Real st
z0 in X0 &
0 < r holds
ex
s being
Real st
(
0 < s & ( for
z1 being
Element of
REAL m st
z1 in X &
|.(z1 - z0).| < s holds
|.(((f0 `partial| (X0,i)) /. z1) - ((f0 `partial| (X0,i)) /. z0)).| < r ) )
proof
let z0 be
Element of
REAL m;
for r being Real st z0 in X0 & 0 < r holds
ex s being Real st
( 0 < s & ( for z1 being Element of REAL m st z1 in X & |.(z1 - z0).| < s holds
|.(((f0 `partial| (X0,i)) /. z1) - ((f0 `partial| (X0,i)) /. z0)).| < r ) )let r be
Real;
( z0 in X0 & 0 < r implies ex s being Real st
( 0 < s & ( for z1 being Element of REAL m st z1 in X & |.(z1 - z0).| < s holds
|.(((f0 `partial| (X0,i)) /. z1) - ((f0 `partial| (X0,i)) /. z0)).| < r ) ) )
assume A13:
(
z0 in X0 &
0 < r )
;
ex s being Real st
( 0 < s & ( for z1 being Element of REAL m st z1 in X & |.(z1 - z0).| < s holds
|.(((f0 `partial| (X0,i)) /. z1) - ((f0 `partial| (X0,i)) /. z0)).| < r ) )
reconsider y0 =
z0 as
Point of
(REAL-NS m) by REAL_NS1:def 4;
consider s being
Real such that A14:
(
0 < s & ( for
y1 being
Point of
(REAL-NS m) st
y1 in X &
||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) )
by A8, A13, NFCONT_1:19;
reconsider s =
s as
Real ;
take
s
;
( 0 < s & ( for z1 being Element of REAL m st z1 in X & |.(z1 - z0).| < s holds
|.(((f0 `partial| (X0,i)) /. z1) - ((f0 `partial| (X0,i)) /. z0)).| < r ) )
thus
0 < s
by A14;
for z1 being Element of REAL m st z1 in X & |.(z1 - z0).| < s holds
|.(((f0 `partial| (X0,i)) /. z1) - ((f0 `partial| (X0,i)) /. z0)).| < r
thus
for
z1 being
Element of
REAL m st
z1 in X &
|.(z1 - z0).| < s holds
|.(((f0 `partial| (X0,i)) /. z1) - ((f0 `partial| (X0,i)) /. z0)).| < r
verumproof
let z1 be
Element of
REAL m;
( z1 in X & |.(z1 - z0).| < s implies |.(((f0 `partial| (X0,i)) /. z1) - ((f0 `partial| (X0,i)) /. z0)).| < r )
assume A15:
(
z1 in X &
|.(z1 - z0).| < s )
;
|.(((f0 `partial| (X0,i)) /. z1) - ((f0 `partial| (X0,i)) /. z0)).| < r
reconsider y1 =
z1 as
Point of
(REAL-NS m) by REAL_NS1:def 4;
|.(z1 - z0).| = ||.(y1 - y0).||
by REAL_NS1:1, REAL_NS1:5;
then A16:
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r
by A15, A14;
(f `partial| (X,i)) /. y1 = partdiff (
f,
y1,
i)
by A6, A15, PDIFF_1:def 20;
then A17:
||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| < r
by A16, A6, A13, PDIFF_1:def 20;
A18:
ex
y1 being
Point of
(REAL-NS m) st
(
z1 = y1 &
(f0 `partial| (X0,i)) /. z1 = (partdiff (f,y1,i)) . One )
by A10, A15;
A19:
ex
y0 being
Point of
(REAL-NS m) st
(
z0 = y0 &
(f0 `partial| (X0,i)) /. z0 = (partdiff (f,y0,i)) . One )
by A10, A13;
reconsider PDP =
(partdiff (f,y1,i)) - (partdiff (f,y0,i)) as
Lipschitzian LinearOperator of
(REAL-NS 1),
(REAL-NS 1) by LOPBAN_1:def 9;
((partdiff (f,y1,i)) . One) - ((partdiff (f,y0,i)) . One) = PDP . One
by LOPBAN_1:40;
then A20:
||.(((partdiff (f,y1,i)) . One) - ((partdiff (f,y0,i)) . One)).|| <= ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| * ||.One.||
by LOPBAN_1:32;
||.One.|| =
|.One0.|
by REAL_NS1:1
.=
|.1.|
by TOPREALC:18
.=
1
by ABSVALUE:def 1
;
then
||.(((partdiff (f,y1,i)) . One) - ((partdiff (f,y0,i)) . One)).|| < r
by A20, A17, XXREAL_0:2;
hence
|.(((f0 `partial| (X0,i)) /. z1) - ((f0 `partial| (X0,i)) /. z0)).| < r
by A18, A19, REAL_NS1:1, REAL_NS1:5;
verum
end;
end; hence
f0 `partial| (
X0,
i)
is_continuous_on X0
by A9, Th38;
verum end;
then A21:
( f0 is_differentiable_in x0 & ( for h0 being Element of REAL m ex w being FinSequence of REAL 1 st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = ((proj (i,m)) . h0) * (partdiff (f0,x0,i)) ) & (diff (f0,x0)) . h0 = Sum w ) ) )
by Th47, A3, A1;
then
ex g being PartFunc of (REAL-NS m),(REAL-NS 1) ex y being Point of (REAL-NS m) st
( f0 = g & x0 = y & g is_differentiable_in y )
;
hence
f is_differentiable_in x
; for h being Point of (REAL-NS m) ex w being FinSequence of REAL 1 st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> ) & (diff (f,x)) . h = Sum w )
A22:
ex g being PartFunc of (REAL-NS m),(REAL-NS 1) ex y being Point of (REAL-NS m) st
( f0 = g & x0 = y & diff (f0,x0) = diff (g,y) )
by A21, PDIFF_1:def 8;
now for h being Point of (REAL-NS m) ex w being FinSequence of REAL 1 st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> ) & (diff (f,x)) . h = Sum w )let h be
Point of
(REAL-NS m);
ex w being FinSequence of REAL 1 st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> ) & (diff (f,x)) . h = Sum w )reconsider h0 =
h as
Element of
REAL m by REAL_NS1:def 4;
consider w being
FinSequence of
REAL 1
such that A23:
(
dom w = Seg m & ( for
i being
Nat st
i in Seg m holds
w . i = ((proj (i,m)) . h0) * (partdiff (f0,x0,i)) ) &
(diff (f0,x0)) . h0 = Sum w )
by Th47, A3, A1, A4;
take w =
w;
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> ) & (diff (f,x)) . h = Sum w )thus
dom w = Seg m
by A23;
( ( for i being Nat st i in Seg m holds
w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> ) & (diff (f,x)) . h = Sum w )thus
for
i being
Nat st
i in Seg m holds
w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*>
(diff (f,x)) . h = Sum wproof
let i be
Nat;
( i in Seg m implies w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> )
assume A24:
i in Seg m
;
w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*>
then A25:
( 1
<= i &
i <= m )
by FINSEQ_1:1;
then
f0 is_partial_differentiable_on X0,
i
by A4;
then
f0 is_partial_differentiable_in x0,
i
by A1, A3, A25, Th34;
then A26:
ex
g being
PartFunc of
(REAL-NS m),
(REAL-NS 1) ex
y being
Point of
(REAL-NS m) st
(
f0 = g &
x0 = y &
partdiff (
f0,
x0,
i)
= (partdiff (g,y,i)) . <*1*> )
by PDIFF_1:def 14;
A27:
((proj (i,m)) . h) * One =
((proj (i,m)) . h0) * One0
by REAL_NS1:3
.=
<*(((proj (i,m)) . h0) * 1)*>
by RVSUM_1:47
.=
<*((proj (i,m)) . h)*>
;
reconsider PDP =
partdiff (
f,
x,
i) as
Lipschitzian LinearOperator of
(REAL-NS 1),
(REAL-NS 1) by LOPBAN_1:def 9;
((proj (i,m)) . h0) * (partdiff (f0,x0,i)) =
((proj (i,m)) . h0) * (PDP . One)
by A26, REAL_NS1:3
.=
(partdiff (f,x,i)) . <*((proj (i,m)) . h)*>
by A27, LOPBAN_1:def 5
;
hence
w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*>
by A24, A23;
verum
end; thus
(diff (f,x)) . h = Sum w
by A23, A22;
verum end;
hence
for h being Point of (REAL-NS m) ex w being FinSequence of REAL 1 st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> ) & (diff (f,x)) . h = Sum w )
; verum