let x0, y0 be Real; for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,1 holds
partdiff (f,z,1) = diff ((SVF1 (1,f,z)),x0)
let z be Element of REAL 2; for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,1 holds
partdiff (f,z,1) = diff ((SVF1 (1,f,z)),x0)
let f be PartFunc of (REAL 2),REAL; ( z = <*x0,y0*> & f is_partial_differentiable_in z,1 implies partdiff (f,z,1) = diff ((SVF1 (1,f,z)),x0) )
set r = partdiff (f,z,1);
assume that
A1:
z = <*x0,y0*>
and
A2:
f is_partial_differentiable_in z,1
; partdiff (f,z,1) = diff ((SVF1 (1,f,z)),x0)
consider x1, y1 being Real such that
A3:
z = <*x1,y1*>
and
A4:
ex N being Neighbourhood of x1 st
( N c= dom (SVF1 (1,f,z)) & ex L being LinearFunc ex R being RestFunc st
( partdiff (f,z,1) = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x1) = (L . (x - x1)) + (R . (x - x1)) ) ) )
by A1, A2, Th11;
x0 = x1
by A1, A3, FINSEQ_1:77;
then consider N being Neighbourhood of x0 such that
N c= dom (SVF1 (1,f,z))
and
A5:
ex L being LinearFunc ex R being RestFunc st
( partdiff (f,z,1) = L . 1 & ( for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) )
by A4;
consider L being LinearFunc, R being RestFunc such that
A6:
partdiff (f,z,1) = L . 1
and
A7:
for x being Real st x in N holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0))
by A5;
consider r1 being Real such that
A8:
for p being Real holds L . p = r1 * p
by FDIFF_1:def 3;
A9:
partdiff (f,z,1) = r1 * 1
by A6, A8;
consider x2, y2 being Real such that
A10:
z = <*x2,y2*>
and
A11:
SVF1 (1,f,z) is_differentiable_in x2
by A2, Th5;
consider N1 being Neighbourhood of x2 such that
N1 c= dom (SVF1 (1,f,z))
and
A12:
ex L being LinearFunc ex R being RestFunc st
( diff ((SVF1 (1,f,z)),x2) = L . 1 & ( for x being Real st x in N1 holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x2) = (L . (x - x2)) + (R . (x - x2)) ) )
by A11, FDIFF_1:def 5;
consider L1 being LinearFunc, R1 being RestFunc such that
A13:
diff ((SVF1 (1,f,z)),x2) = L1 . 1
and
A14:
for x being Real st x in N1 holds
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x2) = (L1 . (x - x2)) + (R1 . (x - x2))
by A12;
consider p1 being Real such that
A15:
for p being Real holds L1 . p = p1 * p
by FDIFF_1:def 3;
A16:
x0 = x2
by A1, A10, FINSEQ_1:77;
then consider N0 being Neighbourhood of x0 such that
A17:
( N0 c= N & N0 c= N1 )
by RCOMP_1:17;
consider g being Real such that
A18:
0 < g
and
A19:
N0 = ].(x0 - g),(x0 + g).[
by RCOMP_1:def 6;
deffunc H1( Nat) -> set = g / ($1 + 2);
consider s1 being Real_Sequence such that
A20:
for n being Nat holds s1 . n = H1(n)
from SEQ_1:sch 1();
then A21:
s1 is non-zero
by SEQ_1:5;
( s1 is convergent & lim s1 = 0 )
by A20, SEQ_4:31;
then reconsider h = s1 as non-zero 0 -convergent Real_Sequence by A21, FDIFF_1:def 1;
A22:
for n being Element of NAT ex x being Real st
( x in N & x in N1 & h . n = x - x0 )
A24:
diff ((SVF1 (1,f,z)),x2) = p1 * 1
by A13, A15;
A25:
now for x being Real st x in N & x in N1 holds
((partdiff (f,z,1)) * (x - x0)) + (R . (x - x0)) = ((diff ((SVF1 (1,f,z)),x2)) * (x - x0)) + (R1 . (x - x0))let x be
Real;
( x in N & x in N1 implies ((partdiff (f,z,1)) * (x - x0)) + (R . (x - x0)) = ((diff ((SVF1 (1,f,z)),x2)) * (x - x0)) + (R1 . (x - x0)) )assume that A26:
x in N
and A27:
x in N1
;
((partdiff (f,z,1)) * (x - x0)) + (R . (x - x0)) = ((diff ((SVF1 (1,f,z)),x2)) * (x - x0)) + (R1 . (x - x0))
((SVF1 (1,f,z)) . x) - ((SVF1 (1,f,z)) . x0) = (L . (x - x0)) + (R . (x - x0))
by A7, A26;
then
(L . (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0))
by A14, A16, A27;
then
(r1 * (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0))
by A8;
hence
((partdiff (f,z,1)) * (x - x0)) + (R . (x - x0)) = ((diff ((SVF1 (1,f,z)),x2)) * (x - x0)) + (R1 . (x - x0))
by A15, A9, A24;
verum end;
reconsider rd = (partdiff (f,z,1)) - (diff ((SVF1 (1,f,z)),x2)) as Element of REAL by XREAL_0:def 1;
now for n being Nat holds rd = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
R1 is
total
by FDIFF_1:def 2;
then
dom R1 = REAL
by PARTFUN1:def 2;
then A28:
rng h c= dom R1
;
let n be
Nat;
rd = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
R is
total
by FDIFF_1:def 2;
then
dom R = REAL
by PARTFUN1:def 2;
then A29:
rng h c= dom R
;
A30:
n in NAT
by ORDINAL1:def 12;
then
ex
x being
Real st
(
x in N &
x in N1 &
h . n = x - x0 )
by A22;
then
((partdiff (f,z,1)) * (h . n)) + (R . (h . n)) = ((diff ((SVF1 (1,f,z)),x2)) * (h . n)) + (R1 . (h . n))
by A25;
then A31:
(((partdiff (f,z,1)) * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) = (((diff ((SVF1 (1,f,z)),x2)) * (h . n)) + (R1 . (h . n))) / (h . n)
by XCMPLX_1:62;
A32:
(R . (h . n)) / (h . n) =
(R . (h . n)) * ((h . n) ")
by XCMPLX_0:def 9
.=
(R . (h . n)) * ((h ") . n)
by VALUED_1:10
.=
((R /* h) . n) * ((h ") . n)
by A30, A29, FUNCT_2:108
.=
((h ") (#) (R /* h)) . n
by SEQ_1:8
;
A33:
h . n <> 0
by SEQ_1:5;
A34:
(R1 . (h . n)) / (h . n) =
(R1 . (h . n)) * ((h . n) ")
by XCMPLX_0:def 9
.=
(R1 . (h . n)) * ((h ") . n)
by VALUED_1:10
.=
((R1 /* h) . n) * ((h ") . n)
by A30, A28, FUNCT_2:108
.=
((h ") (#) (R1 /* h)) . n
by SEQ_1:8
;
A35:
((diff ((SVF1 (1,f,z)),x2)) * (h . n)) / (h . n) =
(diff ((SVF1 (1,f,z)),x2)) * ((h . n) / (h . n))
by XCMPLX_1:74
.=
(diff ((SVF1 (1,f,z)),x2)) * 1
by A33, XCMPLX_1:60
.=
diff (
(SVF1 (1,f,z)),
x2)
;
((partdiff (f,z,1)) * (h . n)) / (h . n) =
(partdiff (f,z,1)) * ((h . n) / (h . n))
by XCMPLX_1:74
.=
(partdiff (f,z,1)) * 1
by A33, XCMPLX_1:60
.=
partdiff (
f,
z,1)
;
then
(partdiff (f,z,1)) + ((R . (h . n)) / (h . n)) = (diff ((SVF1 (1,f,z)),x2)) + ((R1 . (h . n)) / (h . n))
by A31, A35, XCMPLX_1:62;
then
partdiff (
f,
z,1)
= (diff ((SVF1 (1,f,z)),x2)) + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n))
by A32, A34;
hence
rd = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n
by RFUNCT_2:1;
verum end;
then
( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is constant & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 1 = (partdiff (f,z,1)) - (diff ((SVF1 (1,f,z)),x2)) )
by VALUED_0:def 18;
then A36:
lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = (partdiff (f,z,1)) - (diff ((SVF1 (1,f,z)),x2))
by SEQ_4:25;
A37:
( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 )
by FDIFF_1:def 2;
( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 )
by FDIFF_1:def 2;
then
(partdiff (f,z,1)) - (diff ((SVF1 (1,f,z)),x2)) = 0 - 0
by A36, A37, SEQ_2:12;
hence
partdiff (f,z,1) = diff ((SVF1 (1,f,z)),x0)
by A1, A10, FINSEQ_1:77; verum