:: Second-order Partial Differentiation of Real Binary Functions
:: by Bing Xie , Xiquan Liang and Xiuzhuan Shen
::
:: Received December 16, 2008
:: Copyright (c) 2008 Association of Mizar Users
environ
vocabularies FUNCT_1, ARYTM, ARYTM_1, FINSEQ_1, RELAT_1, ORDINAL2, SEQ_1,
SEQ_2, RCOMP_1, PARTFUN1, FDIFF_1, PDIFF_1, BORSUK_1, PDIFF_2, ARYTM_3,
SEQM_3, FCONT_1, ANPROJ_1, PDIFF_3, OPPCAT_1;
notations TARSKI, SUBSET_1, FUNCT_1, FUNCT_2, RELSET_1, PARTFUN1, RFUNCT_2,
XXREAL_0, XCMPLX_0, XREAL_0, NAT_1, ORDINAL1, NUMBERS, REAL_1, VALUED_0,
VALUED_1, SEQ_1, SEQ_2, FINSEQ_1, RCOMP_1, EUCLID, FDIFF_1, FCONT_1,
PDIFF_1, PDIFF_2, PARTFUN2;
constructors REAL_1, SEQ_2, PARTFUN1, RFUNCT_2, RCOMP_1, FDIFF_1, SEQ_1,
NAT_1, FCONT_1, PDIFF_1, PARTFUN2, PDIFF_2, SEQM_3, FUNCT_2, COMPLEX1;
registrations RELSET_1, XREAL_0, MEMBERED, FDIFF_1, FUNCT_2, NAT_1, NUMBERS,
XBOOLE_0, XXREAL_0, VALUED_0, VALUED_1, ORDINAL1, SEQ_4;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions EUCLID, RCOMP_1;
theorems TARSKI, XBOOLE_0, XBOOLE_1, XREAL_1, RCOMP_1, SEQ_4, SEQ_1, SEQ_2,
FINSEQ_1, FINSEQ_2, RFUNCT_2, PARTFUN1, FDIFF_1, PDIFF_2, VALUED_1,
XCMPLX_0, XCMPLX_1, FUNCT_2, VALUED_0, ORDINAL1;
schemes SEQ_1, FUNCT_2;
begin :: Second-order Partial Derivatives
reserve Z for set;
reserve X,Y for Subset of REAL;
reserve x,x0,x1,x2,y,y0,y1,y2,g,g1,g2,r,r1,s,p,p1,p2 for Real;
reserve z,z0 for Element of REAL 2;
reserve n,m,k for Element of NAT;
reserve Z,Z1 for Subset of REAL 2;
reserve s1,s3 for Real_Sequence;
reserve f,f1,f2,g for PartFunc of REAL 2,REAL;
reserve R,R1,R2 for REST;
reserve L,L1,L2 for LINEAR;
registration
cluster -> total REST;
coherence by FDIFF_1:def 3;
end;
definition
let f be PartFunc of REAL 2,REAL;
let z be Element of REAL 2;
func pdiff1(f,z) -> Function of REAL 2, REAL means
for z st z in REAL 2 holds it.z = partdiff1(f,z);
existence
proof
deffunc F(Element of REAL 2) = partdiff1(f,$1);
consider g being Function of REAL 2,REAL such that
A1: for z being Element of REAL 2 holds g.z = F(z) from FUNCT_2:sch 4;
take g;
thus for z st z in REAL 2 holds g.z = partdiff1(f,z) by A1;
end;
uniqueness
proof
let F,G be Function of REAL 2,REAL;
assume that
A2: for z st z in REAL 2 holds F.z = partdiff1(f,z) and
A3: for z st z in REAL 2 holds G.z = partdiff1(f,z);
now
let z be Element of REAL 2;
F.z = partdiff1(f,z) by A2;
hence F.z = G.z by A3;
end;
hence thesis by FUNCT_2:113;
end;
func pdiff2(f,z) -> Function of REAL 2, REAL means
for z st z in REAL 2 holds it.z = partdiff2(f,z);
existence
proof
deffunc F(Element of REAL 2) = partdiff2(f,$1);
consider g being Function of REAL 2,REAL such that
A1: for z being Element of REAL 2 holds g.z = F(z) from FUNCT_2:sch 4;
take g;
thus for z st z in REAL 2 holds g.z = partdiff2(f,z) by A1;
end;
uniqueness
proof
let F,G be Function of REAL 2,REAL;
assume that
A2: for z st z in REAL 2 holds F.z = partdiff2(f,z) and
A3: for z st z in REAL 2 holds G.z = partdiff2(f,z);
now
let z be Element of REAL 2;
F.z = partdiff2(f,z) by A2;
hence F.z = G.z by A3;
end;
hence thesis by FUNCT_2:113;
end;
end;
definition
let f be PartFunc of REAL 2,REAL;
let z be Element of REAL 2;
pred f is_hpartial_differentiable`11_in z means :Def3:
ex x0,y0 being Real st z = <*x0,y0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(pdiff1(f,z),z) &
ex L,R st for x st x in N holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x0 = L.(x-x0) + R.(x-x0);
pred f is_hpartial_differentiable`12_in z means :Def4:
ex x0,y0 being Real st z = <*x0,y0*> &
ex N being Neighbourhood of y0 st N c= dom SVF2(pdiff1(f,z),z) &
ex L,R st for y st y in N holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y0 = L.(y-y0) + R.(y-y0);
pred f is_hpartial_differentiable`21_in z means :Def5:
ex x0,y0 being Real st z = <*x0,y0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(pdiff2(f,z),z) &
ex L,R st for x st x in N holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x0 = L.(x-x0) + R.(x-x0);
pred f is_hpartial_differentiable`22_in z means :Def6:
ex x0,y0 being Real st z = <*x0,y0*> &
ex N being Neighbourhood of y0 st N c= dom SVF2(pdiff2(f,z),z) &
ex L,R st for y st y in N holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y0 = L.(y-y0) + R.(y-y0);
end;
definition
let f be PartFunc of REAL 2,REAL;
let z be Element of REAL 2;
assume A1: f is_hpartial_differentiable`11_in z;
func hpartdiff11(f,z) -> Real means :Def7:
ex x0,y0 being Real st z = <*x0,y0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(pdiff1(f,z),z) &
ex L,R st it = L.1 & for x st x in N holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x0 = L.(x-x0) + R.(x-x0);
existence
proof
consider x0,y0 being Real such that
A2: z = <*x0,y0*> & ex N being Neighbourhood of x0 st
N c= dom SVF1(pdiff1(f,z),z) & ex L,R st for x st x in N holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x0 = L.(x-x0) + R.(x-x0)
by A1,Def3;
consider N being Neighbourhood of x0 such that
A3: N c= dom SVF1(pdiff1(f,z),z) & ex L,R st for x st x in N holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x0 = L.(x-x0) + R.(x-x0)
by A2;
consider L,R such that
A4: for x st x in N holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x0 = L.(x-x0) + R.(x-x0)
by A3;
consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 4;
take r;
L.1 = r*1 by A5
.= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s;
assume that
A6: ex x0,y0 being Real st z = <*x0,y0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(pdiff1(f,z),z) &
ex L,R st r = L.1 & for x st x in N holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x0
= L.(x-x0) + R.(x-x0) and
A7: ex x0,y0 being Real st z = <*x0,y0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(pdiff1(f,z),z) &
ex L,R st s = L.1 & for x st x in N holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x0 = L.(x-x0) + R.(x-x0);
consider x0,y0 being Real such that
A8: z = <*x0,y0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(pdiff1(f,z),z) &
ex L,R st r = L.1 & for x st x in N holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x0 = L.(x-x0) + R.(x-x0)
by A6;
consider N being Neighbourhood of x0 such that
A9: N c= dom SVF1(pdiff1(f,z),z) & ex L,R st r = L.1 & for x st x in N holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x0
= L.(x-x0) + R.(x-x0) by A8;
consider L,R such that
A10: r = L.1 & for x st x in N holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x0
= L.(x-x0) + R.(x-x0) by A9;
consider x1,y1 being Real such that
A11: z = <*x1,y1*> &
ex N being Neighbourhood of x1 st N c= dom SVF1(pdiff1(f,z),z) &
ex L,R st s = L.1 & for x st x in N holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x1
= L.(x-x1) + R.(x-x1) by A7;
consider N1 being Neighbourhood of x1 such that
A12: N1 c= dom SVF1(pdiff1(f,z),z) &
ex L,R st s = L.1 & for x st x in N1 holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x1
= L.(x-x1) + R.(x-x1) by A11;
consider L1,R1 such that
A13: s = L1.1 & for x st x in N1 holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x1 = L1.(x-x1) + R1.(x-x1)
by A12;
consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 4;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 4;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 by A8,A11,FINSEQ_1:98;
A19: now let x;
assume
A20: x in N & x in N1;
then SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x0
= L.(x-x0) + R.(x-x0) by A10;
then L.(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A13,A18,A20;
then r1*(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A14;
hence r*(x-x0) + R.(x-x0) = s*(x-x0) + R1.(x-x0) by A15,A16,A17;
end;
consider N0 be Neighbourhood of x0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:38;
consider g be real number such that
A22: 0 < g & N0 = ].x0-g,x0+g.[ by RCOMP_1:def 7;
deffunc F(Element of NAT) = g/($1+2);
consider s1 such that
A23: for n holds s1.n = F(n) from SEQ_1:sch 1;
now let n;
g/(n+2) <> 0 by A22,XREAL_1:141;
hence s1.n <> 0 by A23;
end;
then
A24: s1 is non-zero by SEQ_1:7;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:46;
then reconsider h = s1 as convergent_to_0 Real_Sequence
by A24,FDIFF_1:def 1;
A25: for n ex x st x in N & x in N1 & h.n = x-x0
proof
let n;
A26: g/(n+2) > 0 by A22,XREAL_1:141;
0+1 < n+1+1 by XREAL_1:8;
then g/(n+2) < g/1 by A22,XREAL_1:78;then
A27: x0+g/(n+2) < x0+g by XREAL_1:8;
AA: x0+-g < x0+g/(n+2) by A22,A26,XREAL_1:8;
A28: x0+g/(n+2) in ].x0-g,x0+g.[ by A27,AA;
take x = x0+g/(n+2);
thus thesis by A21,A22,A23,A28;
end;
A29: for n being Nat holds r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n
proof let n be Nat;
X: n in NAT by ORDINAL1:def 13; then
ex x st x in N & x in N1 & h.n = x-x0 by A25;then
A30: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
h is non-zero by FDIFF_1:def 1;then
A31: h.n <> 0 by SEQ_1:7,X;
A32: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A30,XCMPLX_1:63;
A33: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:75
.= r*1 by A31,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:75
.= s*1 by A31,XCMPLX_1:60
.= s;then
A34: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A32,A33,XCMPLX_1:63;
dom R = REAL by PARTFUN1:def 4;then
A35: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 4;then
A36: rng h c= dom R1;
A37: (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 A35,FUNCT_2:185,X
.= ((h")(#)(R/*h)).n by VALUED_1:5;
(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 A36,FUNCT_2:185,X
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A34,A37;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by X,RFUNCT_2:6;
end; then
A38: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A29;then
A39: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A38,SEQ_4:40;
A40: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 3;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 3;
then r-s = 0-0 by A39,A40,SEQ_2:26;
hence thesis;
end;
end;
definition
let f be PartFunc of REAL 2,REAL;
let z be Element of REAL 2;
assume A1: f is_hpartial_differentiable`12_in z;
func hpartdiff12(f,z) -> Real means :Def8:
ex x0,y0 being Real st z = <*x0,y0*> &
ex N being Neighbourhood of y0 st N c= dom SVF2(pdiff1(f,z),z) &
ex L,R st it = L.1 & for y st y in N holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y0 = L.(y-y0) + R.(y-y0);
existence
proof
consider x0,y0 being Real such that
A2: z = <*x0,y0*> & ex N being Neighbourhood of y0 st
N c= dom SVF2(pdiff1(f,z),z) & ex L,R st for y st y in N holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y0 = L.(y-y0) + R.(y-y0)
by A1,Def4;
consider N being Neighbourhood of y0 such that
A3: N c= dom SVF2(pdiff1(f,z),z) & ex L,R st for y st y in N holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y0 = L.(y-y0) + R.(y-y0)
by A2;
consider L,R such that
A4: for y st y in N holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y0 = L.(y-y0) + R.(y-y0)
by A3;
consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 4;
take r;
L.1 = r*1 by A5
.= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s;
assume that
A6: ex x0,y0 being Real st z = <*x0,y0*> &
ex N being Neighbourhood of y0 st N c= dom SVF2(pdiff1(f,z),z) &
ex L,R st r = L.1 & for y st y in N holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y0
= L.(y-y0) + R.(y-y0) and
A7: ex x0,y0 being Real st z = <*x0,y0*> &
ex N being Neighbourhood of y0 st N c= dom SVF2(pdiff1(f,z),z) &
ex L,R st s = L.1 & for y st y in N holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y0 = L.(y-y0) + R.(y-y0);
consider x0,y0 being Real such that
A8: z = <*x0,y0*> &
ex N being Neighbourhood of y0 st N c= dom SVF2(pdiff1(f,z),z) &
ex L,R st r = L.1 & for y st y in N holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y0 = L.(y-y0) + R.(y-y0)
by A6;
consider N being Neighbourhood of y0 such that
A9: N c= dom SVF2(pdiff1(f,z),z) & ex L,R st r = L.1 & for y st y in N holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y0
= L.(y-y0) + R.(y-y0) by A8;
consider L,R such that
A10: r = L.1 & for y st y in N holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y0
= L.(y-y0) + R.(y-y0) by A9;
consider x1,y1 being Real such that
A11: z = <*x1,y1*> &
ex N being Neighbourhood of y1 st N c= dom SVF2(pdiff1(f,z),z) &
ex L,R st s = L.1 & for y st y in N holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y1
= L.(y-y1) + R.(y-y1) by A7;
consider N1 being Neighbourhood of y1 such that
A12: N1 c= dom SVF2(pdiff1(f,z),z) &
ex L,R st s = L.1 & for y st y in N1 holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y1
= L.(y-y1) + R.(y-y1) by A11;
consider L1,R1 such that
A13: s = L1.1 & for y st y in N1 holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y1
= L1.(y-y1) + R1.(y-y1) by A12;
consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 4;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 4;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 by A8,A11,FINSEQ_1:98;
A19: now let y;
assume
A20: y in N & y in N1;
then SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y0
= L.(y-y0) + R.(y-y0) by A10;
then L.(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A13,A18,A20;
then r1*(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A14;
hence r*(y-y0) + R.(y-y0) = s*(y-y0) + R1.(y-y0) by A15,A16,A17;
end;
consider N0 be Neighbourhood of y0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:38;
consider g be real number such that
A22: 0 < g & N0 = ].y0-g,y0+g.[ by RCOMP_1:def 7;
deffunc F(Element of NAT) = g/($1+2);
consider s1 such that
A23: for n holds s1.n = F(n) from SEQ_1:sch 1;
now let n;
g/(n+2) <> 0 by A22,XREAL_1:141;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:7;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:46;
then reconsider h = s1 as convergent_to_0 Real_Sequence
by A24,FDIFF_1:def 1;
A25: for n ex y st y in N & y in N1 & h.n = y-y0
proof
let n;
A26: g/(n+2) > 0 by A22,XREAL_1:141;
0+1 < n+1+1 by XREAL_1:8;
then g/(n+2) < g/1 by A22,XREAL_1:78;then
A27: y0+g/(n+2) < y0+g by XREAL_1:8;
AA: y0+-g < y0+g/(n+2) by A22,A26,XREAL_1:8;
A28: y0+g/(n+2) in ].y0-g,y0+g.[ by A27,AA;
take y = y0+g/(n+2);
thus thesis by A21,A22,A23,A28;
end;
A29: now let n be Nat;
X: n in NAT by ORDINAL1:def 13; then
ex y st y in N & y in N1 & h.n = y-y0 by A25;then
A30: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
h is non-zero by FDIFF_1:def 1;then
A31: h.n <> 0 by X,SEQ_1:7;
A32: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A30,XCMPLX_1:63;
A33: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:75
.= r*1 by A31,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:75
.= s*1 by A31,XCMPLX_1:60
.= s;then
A34: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A32,A33,XCMPLX_1:63;
dom R = REAL by PARTFUN1:def 4;then
A35: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 4;then
A36: rng h c= dom R1;
A37: (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 A35,FUNCT_2:185,X
.= ((h")(#)(R/*h)).n by VALUED_1:5;
(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 A36,FUNCT_2:185,X
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A34,A37;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by X,RFUNCT_2:6;
end; then
A38: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A29;then
A39: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A38,SEQ_4:40;
A40: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 3;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 3;
then r-s = 0-0 by A39,A40,SEQ_2:26;
hence thesis;
end;
end;
definition
let f be PartFunc of REAL 2,REAL;
let z be Element of REAL 2;
assume A1: f is_hpartial_differentiable`21_in z;
func hpartdiff21(f,z) -> Real means :Def9:
ex x0,y0 being Real st z = <*x0,y0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(pdiff2(f,z),z) &
ex L,R st it = L.1 & for x st x in N holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x0 = L.(x-x0) + R.(x-x0);
existence
proof
consider x0,y0 being Real such that
A2: z = <*x0,y0*> & ex N being Neighbourhood of x0 st
N c= dom SVF1(pdiff2(f,z),z) & ex L,R st for x st x in N holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x0 = L.(x-x0) + R.(x-x0)
by A1,Def5;
consider N being Neighbourhood of x0 such that
A3: N c= dom SVF1(pdiff2(f,z),z) & ex L,R st for x st x in N holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x0 = L.(x-x0) + R.(x-x0)
by A2;
consider L,R such that
A4: for x st x in N holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x0 = L.(x-x0) + R.(x-x0)
by A3;
consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 4;
take r;
L.1 = r*1 by A5
.= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s;
assume that
A6: ex x0,y0 being Real st z = <*x0,y0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(pdiff2(f,z),z) &
ex L,R st r = L.1 & for x st x in N holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x0
= L.(x-x0) + R.(x-x0) and
A7: ex x0,y0 being Real st z = <*x0,y0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(pdiff2(f,z),z) &
ex L,R st s = L.1 & for x st x in N holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x0 = L.(x-x0) + R.(x-x0);
consider x0,y0 being Real such that
A8: z = <*x0,y0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(pdiff2(f,z),z) &
ex L,R st r = L.1 & for x st x in N holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x0 = L.(x-x0) + R.(x-x0)
by A6;
consider N being Neighbourhood of x0 such that
A9: N c= dom SVF1(pdiff2(f,z),z) & ex L,R st r = L.1 & for x st x in N holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x0
= L.(x-x0) + R.(x-x0) by A8;
consider L,R such that
A10: r = L.1 & for x st x in N holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x0
= L.(x-x0) + R.(x-x0) by A9;
consider x1,y1 being Real such that
A11: z = <*x1,y1*> &
ex N being Neighbourhood of x1 st N c= dom SVF1(pdiff2(f,z),z) &
ex L,R st s = L.1 & for x st x in N holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x1
= L.(x-x1) + R.(x-x1) by A7;
consider N1 being Neighbourhood of x1 such that
A12: N1 c= dom SVF1(pdiff2(f,z),z) &
ex L,R st s = L.1 & for x st x in N1 holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x1
= L.(x-x1) + R.(x-x1) by A11;
consider L1,R1 such that
A13: s = L1.1 & for x st x in N1 holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x1
= L1.(x-x1) + R1.(x-x1) by A12;
consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 4;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 4;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 by A8,A11,FINSEQ_1:98;
A19: now let x;
assume
A20: x in N & x in N1;
then SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x0
= L.(x-x0) + R.(x-x0) by A10;
then L.(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A13,A18,A20;
then r1*(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A14;
hence r*(x-x0) + R.(x-x0) = s*(x-x0) + R1.(x-x0) by A15,A16,A17;
end;
consider N0 be Neighbourhood of x0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:38;
consider g be real number such that
A22: 0 < g & N0 = ].x0-g,x0+g.[ by RCOMP_1:def 7;
deffunc F(Element of NAT) = g/($1+2);
consider s1 such that
A23: for n holds s1.n = F(n) from SEQ_1:sch 1;
now let n;
g/(n+2) <> 0 by A22,XREAL_1:141;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:7;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:46;
then reconsider h = s1 as convergent_to_0 Real_Sequence
by A24,FDIFF_1:def 1;
A25: for n ex x st x in N & x in N1 & h.n = x-x0
proof
let n;
A26: g/(n+2) > 0 by A22,XREAL_1:141;
0+1 < n+1+1 by XREAL_1:8;
then g/(n+2) < g/1 by A22,XREAL_1:78;then
A27: x0+g/(n+2) < x0+g by XREAL_1:8;
AA: x0+-g < x0+g/(n+2) by A22,A26,XREAL_1:8;
A28: x0+g/(n+2) in ].x0-g,x0+g.[ by A27,AA;
take x = x0+g/(n+2);
thus thesis by A21,A22,A23,A28;
end;
A29: now let n be Nat;
X: n in NAT by ORDINAL1:def 13; then
ex x st x in N & x in N1 & h.n = x-x0 by A25;then
A30: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
h is non-zero by FDIFF_1:def 1;then
A31: h.n <> 0 by X,SEQ_1:7;
A32: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A30,XCMPLX_1:63;
A33: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:75
.= r*1 by A31,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:75
.= s*1 by A31,XCMPLX_1:60
.= s;then
A34: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A32,A33,XCMPLX_1:63;
dom R = REAL by PARTFUN1:def 4;then
A35: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 4;then
A36: rng h c= dom R1;
A37: (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 A35,FUNCT_2:185,X
.= ((h")(#)(R/*h)).n by VALUED_1:5;
(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 A36,FUNCT_2:185,X
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A34,A37;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by VALUED_1:15,X;
end; then
A38: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A29;then
A39: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A38,SEQ_4:40;
A40: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 3;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 3;
then r-s = 0-0 by A39,A40,SEQ_2:26;
hence thesis;
end;
end;
definition
let f be PartFunc of REAL 2,REAL;
let z be Element of REAL 2;
assume A1: f is_hpartial_differentiable`22_in z;
func hpartdiff22(f,z) -> Real means :Def10:
ex x0,y0 being Real st z = <*x0,y0*> &
ex N being Neighbourhood of y0 st N c= dom SVF2(pdiff2(f,z),z) &
ex L,R st it = L.1 & for y st y in N holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y0 = L.(y-y0) + R.(y-y0);
existence
proof
consider x0,y0 being Real such that
A2: z = <*x0,y0*> & ex N being Neighbourhood of y0 st
N c= dom SVF2(pdiff2(f,z),z) & ex L,R st for y st y in N holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y0 = L.(y-y0) + R.(y-y0)
by A1,Def6;
consider N being Neighbourhood of y0 such that
A3: N c= dom SVF2(pdiff2(f,z),z) & ex L,R st for y st y in N holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y0 = L.(y-y0) + R.(y-y0)
by A2;
consider L,R such that
A4: for y st y in N holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y0 = L.(y-y0) + R.(y-y0)
by A3;
consider r such that
A5: for p holds L.p = r*p by FDIFF_1:def 4;
take r;
L.1 = r*1 by A5
.= r;
hence thesis by A2,A3,A4;
end;
uniqueness
proof
let r,s;
assume that
A6: ex x0,y0 being Real st z = <*x0,y0*> &
ex N being Neighbourhood of y0 st N c= dom SVF2(pdiff2(f,z),z) &
ex L,R st r = L.1 & for y st y in N holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y0
= L.(y-y0) + R.(y-y0) and
A7: ex x0,y0 being Real st z = <*x0,y0*> &
ex N being Neighbourhood of y0 st N c= dom SVF2(pdiff2(f,z),z) &
ex L,R st s = L.1 & for y st y in N holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y0 = L.(y-y0) + R.(y-y0);
consider x0,y0 being Real such that
A8: z = <*x0,y0*> &
ex N being Neighbourhood of y0 st N c= dom SVF2(pdiff2(f,z),z) &
ex L,R st r = L.1 & for y st y in N holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y0 = L.(y-y0) + R.(y-y0)
by A6;
consider N being Neighbourhood of y0 such that
A9: N c= dom SVF2(pdiff2(f,z),z) & ex L,R st r = L.1 & for y st y in N holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y0
= L.(y-y0) + R.(y-y0) by A8;
consider L,R such that
A10: r = L.1 & for y st y in N holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y0
= L.(y-y0) + R.(y-y0) by A9;
consider x1,y1 being Real such that
A11: z = <*x1,y1*> &
ex N being Neighbourhood of y1 st N c= dom SVF2(pdiff2(f,z),z) &
ex L,R st s = L.1 & for y st y in N holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y1
= L.(y-y1) + R.(y-y1) by A7;
consider N1 being Neighbourhood of y1 such that
A12: N1 c= dom SVF2(pdiff2(f,z),z) & ex L,R st s = L.1 & for y st y in N1 holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y1
= L.(y-y1) + R.(y-y1) by A11;
consider L1,R1 such that
A13: s = L1.1 & for y st y in N1 holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y1
= L1.(y-y1) + R1.(y-y1) by A12;
consider r1 such that
A14: for p holds L.p = r1*p by FDIFF_1:def 4;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 4;
A16: r = r1*1 by A10,A14;
A17: s = p1*1 by A13,A15;
A18: x0 = x1 & y0 = y1 by A8,A11,FINSEQ_1:98;
A19: now let y;
assume
A20: y in N & y in N1;
then SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y0
= L.(y-y0) + R.(y-y0) by A10;
then L.(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A13,A18,A20;
then r1*(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A14;
hence r*(y-y0) + R.(y-y0) = s*(y-y0) + R1.(y-y0) by A15,A16,A17;
end;
consider N0 be Neighbourhood of y0 such that
A21: N0 c= N & N0 c= N1 by A18,RCOMP_1:38;
consider g be real number such that
A22: 0 < g & N0 = ].y0-g,y0+g.[ by RCOMP_1:def 7;
deffunc F(Element of NAT) = g/($1+2);
consider s1 such that
A23: for n holds s1.n = F(n) from SEQ_1:sch 1;
now let n;
g/(n+2) <> 0 by A22,XREAL_1:141;
hence s1.n <> 0 by A23;
end; then
A24: s1 is non-zero by SEQ_1:7;
s1 is convergent & lim s1 = 0 by A23,SEQ_4:46;
then reconsider h = s1 as convergent_to_0 Real_Sequence
by A24,FDIFF_1:def 1;
A25: for n ex y st y in N & y in N1 & h.n = y-y0
proof
let n;
A26: g/(n+2) > 0 by A22,XREAL_1:141;
0+1 < n+1+1 by XREAL_1:8;
then g/(n+2) < g/1 by A22,XREAL_1:78;then
A27: y0+g/(n+2) < y0+g by XREAL_1:8;
AA: y0+-g < y0+g/(n+2) by A22,A26,XREAL_1:8;
A28: y0+g/(n+2) in ].y0-g,y0+g.[ by A27,AA;
take y = y0+g/(n+2);
thus thesis by A21,A22,A23,A28;
end;
A29: now let n be Nat;
X: n in NAT by ORDINAL1:def 13; then
ex y st y in N & y in N1 & h.n = y-y0 by A25;then
A30: r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A19;
h is non-zero by FDIFF_1:def 1;then
A31: h.n <> 0 by SEQ_1:7,X;
A32: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n)
by A30,XCMPLX_1:63;
A33: (r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:75
.= r*1 by A31,XCMPLX_1:60
.= r;
(s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:75
.= s*1 by A31,XCMPLX_1:60
.= s;then
A34: r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A32,A33,XCMPLX_1:63;
dom R = REAL by PARTFUN1:def 4;then
A35: rng h c= dom R;
dom R1 = REAL by PARTFUN1:def 4;then
A36: rng h c= dom R1;
A37: (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 A35,FUNCT_2:185,X
.= ((h")(#)(R/*h)).n by VALUED_1:5;
(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 A36,FUNCT_2:185,X
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A34,A37;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:6,X;
end; then
A38: ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant by VALUED_0:def 18;
(((h")(#)(R1/*h))-((h")(#)(R/*h))).1 = r-s by A29;then
A39: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by A38,SEQ_4:40;
A40: (h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 3;
(h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 3;
then r-s = 0-0 by A39,A40,SEQ_2:26;
hence thesis;
end;
end;
theorem
z = <*x0,y0*> & f is_hpartial_differentiable`11_in z implies
SVF1(pdiff1(f,z),z) is_differentiable_in x0
proof
assume that
A1: z = <*x0,y0*> and
A2: f is_hpartial_differentiable`11_in z;
consider x1,y1 such that
A4: z = <*x1,y1*> & ex N being Neighbourhood of x1 st
N c= dom SVF1(pdiff1(f,z),z) & ex L,R st for x st x in N holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x1 = L.(x-x1) + R.(x-x1)
by A2,Def3;
x0 = x1 by A1,A4,FINSEQ_1:98;
hence thesis by A4,FDIFF_1:def 5;
end;
theorem
z = <*x0,y0*> & f is_hpartial_differentiable`12_in z implies
SVF2(pdiff1(f,z),z) is_differentiable_in y0
proof
assume that
A1: z = <*x0,y0*> and
A2: f is_hpartial_differentiable`12_in z;
consider x1,y1 such that
A4: z = <*x1,y1*> & ex N being Neighbourhood of y1 st
N c= dom SVF2(pdiff1(f,z),z) & ex L,R st for y st y in N holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y1 = L.(y-y1) + R.(y-y1)
by A2,Def4;
y0 = y1 by A1,A4,FINSEQ_1:98;
hence thesis by A4,FDIFF_1:def 5;
end;
theorem
z = <*x0,y0*> & f is_hpartial_differentiable`21_in z implies
SVF1(pdiff2(f,z),z) is_differentiable_in x0
proof
assume that
A1: z = <*x0,y0*> and
A2: f is_hpartial_differentiable`21_in z;
consider x1,y1 such that
A4: z = <*x1,y1*> & ex N being Neighbourhood of x1 st
N c= dom SVF1(pdiff2(f,z),z) & ex L,R st for x st x in N holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x1 = L.(x-x1) + R.(x-x1)
by A2,Def5;
x0 = x1 by A1,A4,FINSEQ_1:98;
hence thesis by A4,FDIFF_1:def 5;
end;
theorem
z = <*x0,y0*> & f is_hpartial_differentiable`22_in z implies
SVF2(pdiff2(f,z),z) is_differentiable_in y0
proof
assume that
A1: z = <*x0,y0*> and
A2: f is_hpartial_differentiable`22_in z;
consider x1,y1 such that
A4: z = <*x1,y1*> & ex N being Neighbourhood of y1 st
N c= dom SVF2(pdiff2(f,z),z) & ex L,R st for y st y in N holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y1 = L.(y-y1) + R.(y-y1)
by A2,Def6;
y0 = y1 by A1,A4,FINSEQ_1:98;
hence thesis by A4,FDIFF_1:def 5;
end;
theorem Th5:
z = <*x0,y0*> & f is_hpartial_differentiable`11_in z implies
hpartdiff11(f,z) = diff(SVF1(pdiff1(f,z),z),x0)
proof
set r = hpartdiff11(f,z);
assume that
A1: z = <*x0,y0*> and
A2: f is_hpartial_differentiable`11_in z;
consider x1,y1 being Real such that
A3: z = <*x1,y1*> & ex N being Neighbourhood of x1 st
N c= dom SVF1(pdiff1(f,z),z) & ex L,R st for x st x in N holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x1 = L.(x-x1) + R.(x-x1)
by A2,Def3;
consider N being Neighbourhood of x1 such that
A4: N c= dom SVF1(pdiff1(f,z),z) & ex L,R st for x st x in N holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x1 = L.(x-x1) + R.(x-x1)
by A3;
consider L,R such that
A5: for x st x in N holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x1 = L.(x-x1) + R.(x-x1)
by A4;
A6: x0 = x1 & y0 = y1 by A1,A3,FINSEQ_1:98;
A7: r = L.1 by A2,A3,A4,A5,Def7;
A8: SVF1(pdiff1(f,z),z) is_differentiable_in x0 by A4,A6,FDIFF_1:def 5;
thus hpartdiff11(f,z) = diff(SVF1(pdiff1(f,z),z),x0)
by A4,A5,A6,A7,A8,FDIFF_1:def 6;
end;
theorem Th6:
z = <*x0,y0*> & f is_hpartial_differentiable`12_in z implies
hpartdiff12(f,z) = diff(SVF2(pdiff1(f,z),z),y0)
proof
set r = hpartdiff12(f,z);
assume that
A1: z = <*x0,y0*> and
A2: f is_hpartial_differentiable`12_in z;
consider x1,y1 being Real such that
A3: z = <*x1,y1*> & ex N being Neighbourhood of y1 st
N c= dom SVF2(pdiff1(f,z),z) & ex L,R st for y st y in N holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y1 = L.(y-y1) + R.(y-y1)
by A2,Def4;
consider N being Neighbourhood of y1 such that
A4: N c= dom SVF2(pdiff1(f,z),z) & ex L,R st for y st y in N holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y1 = L.(y-y1) + R.(y-y1)
by A3;
consider L,R such that
A5: for y st y in N holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y1 = L.(y-y1) + R.(y-y1)
by A4;
A6: x0 = x1 & y0 = y1 by A1,A3,FINSEQ_1:98;
A7: r = L.1 by A2,A3,A4,A5,Def8;
A8: SVF2(pdiff1(f,z),z) is_differentiable_in y0 by A4,A6,FDIFF_1:def 5;
thus hpartdiff12(f,z) = diff(SVF2(pdiff1(f,z),z),y0)
by A4,A5,A6,A7,A8,FDIFF_1:def 6;
end;
theorem Th7:
z = <*x0,y0*> & f is_hpartial_differentiable`21_in z implies
hpartdiff21(f,z) = diff(SVF1(pdiff2(f,z),z),x0)
proof
set r = hpartdiff21(f,z);
assume that
A1: z = <*x0,y0*> and
A2: f is_hpartial_differentiable`21_in z;
consider x1,y1 being Real such that
A3: z = <*x1,y1*> & ex N being Neighbourhood of x1 st
N c= dom SVF1(pdiff2(f,z),z) & ex L,R st for x st x in N holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x1 = L.(x-x1) + R.(x-x1)
by A2,Def5;
consider N being Neighbourhood of x1 such that
A4: N c= dom SVF1(pdiff2(f,z),z) & ex L,R st for x st x in N holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x1 = L.(x-x1) + R.(x-x1)
by A3;
consider L,R such that
A5: for x st x in N holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x1 = L.(x-x1) + R.(x-x1)
by A4;
A6: x0 = x1 & y0 = y1 by A1,A3,FINSEQ_1:98;
A7: r = L.1 by A2,A3,A4,A5,Def9;
A8: SVF1(pdiff2(f,z),z) is_differentiable_in x0 by A4,A6,FDIFF_1:def 5;
thus hpartdiff21(f,z) = diff(SVF1(pdiff2(f,z),z),x0)
by A4,A5,A6,A7,A8,FDIFF_1:def 6;
end;
theorem Th8:
z = <*x0,y0*> & f is_hpartial_differentiable`22_in z implies
hpartdiff22(f,z) = diff(SVF2(pdiff2(f,z),z),y0)
proof
set r = hpartdiff22(f,z);
assume that
A1: z = <*x0,y0*> and
A2: f is_hpartial_differentiable`22_in z;
consider x1,y1 being Real such that
A3: z = <*x1,y1*> & ex N being Neighbourhood of y1 st
N c= dom SVF2(pdiff2(f,z),z) & ex L,R st for y st y in N holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y1 = L.(y-y1) + R.(y-y1)
by A2,Def6;
consider N being Neighbourhood of y1 such that
A4: N c= dom SVF2(pdiff2(f,z),z) & ex L,R st for y st y in N holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y1 = L.(y-y1) + R.(y-y1)
by A3;
consider L,R such that
A5: for y st y in N holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y1 = L.(y-y1) + R.(y-y1)
by A4;
A6: x0 = x1 & y0 = y1 by A1,A3,FINSEQ_1:98;
A7: r = L.1 by A2,A3,A4,A5,Def10;
A8: SVF2(pdiff2(f,z),z) is_differentiable_in y0 by A4,A6,FDIFF_1:def 5;
thus hpartdiff22(f,z) = diff(SVF2(pdiff2(f,z),z),y0)
by A4,A5,A6,A7,A8,FDIFF_1:def 6;
end;
definition
let f be PartFunc of REAL 2,REAL;
let Z be set;
pred f is_hpartial_differentiable`11_on Z means :Def11:
Z c= dom f & for z be Element of REAL 2 st z in Z holds
f|Z is_hpartial_differentiable`11_in z;
pred f is_hpartial_differentiable`12_on Z means :Def12:
Z c= dom f & for z be Element of REAL 2 st z in Z holds
f|Z is_hpartial_differentiable`12_in z;
pred f is_hpartial_differentiable`21_on Z means :Def13:
Z c= dom f & for z be Element of REAL 2 st z in Z holds
f|Z is_hpartial_differentiable`21_in z;
pred f is_hpartial_differentiable`22_on Z means :Def14:
Z c= dom f & for z be Element of REAL 2 st z in Z holds
f|Z is_hpartial_differentiable`22_in z;
end;
definition
let f be PartFunc of REAL 2,REAL;
let Z be set;
assume A1: f is_hpartial_differentiable`11_on Z;
func f`hpartial11|Z -> PartFunc of REAL 2,REAL means
dom it = Z & for z be Element of REAL 2 st z in Z holds
it.z = hpartdiff11(f,z);
existence
proof
defpred P[Element of REAL 2] means $1 in Z;
deffunc F(Element of REAL 2) = hpartdiff11(f,$1);
consider F being PartFunc of REAL 2,REAL such that
A2: (for z be Element of REAL 2 holds z in dom F iff P[z]) &
for z be Element of REAL 2 st z in dom F holds F.z = F(z)
from SEQ_1:sch 3;
take F;
for y be set st y in dom F holds y in Z by A2;then
A3: dom F c= Z by TARSKI:def 3;
now
let y be set such that
A4: y in Z;
Z c= dom f by A1,Def11;
then Z is Subset of REAL 2 by XBOOLE_1:1;
hence y in dom F by A2,A4;
end;
then Z c= dom F by TARSKI:def 3;
hence dom F = Z by A3,XBOOLE_0:def 10;
hereby
let z be Element of REAL 2;
assume z in Z;then
z in dom F by A2;
hence F.z = hpartdiff11(f,z) by A2;
end;
end;
uniqueness
proof
let F,G be PartFunc of REAL 2,REAL;
assume that
A6: dom F = Z & for z be Element of REAL 2 st z in Z holds
F.z = hpartdiff11(f,z) and
A7: dom G = Z & for z be Element of REAL 2 st z in Z holds
G.z = hpartdiff11(f,z);
now
let z be Element of REAL 2;
assume
A8: z in dom F;
then F.z = hpartdiff11(f,z) by A6;
hence F.z = G.z by A6,A7,A8;
end;
hence thesis by A6,A7,PARTFUN1:34;
end;
end;
definition
let f be PartFunc of REAL 2,REAL;
let Z be set;
assume A1: f is_hpartial_differentiable`12_on Z;
func f`hpartial12|Z -> PartFunc of REAL 2,REAL means
dom it = Z & for z be Element of REAL 2 st z in Z holds
it.z = hpartdiff12(f,z);
existence
proof
defpred P[Element of REAL 2] means $1 in Z;
deffunc F(Element of REAL 2) = hpartdiff12(f,$1);
consider F being PartFunc of REAL 2,REAL such that
A2: (for z be Element of REAL 2 holds z in dom F iff P[z]) &
for z be Element of REAL 2 st z in dom F holds F.z = F(z)
from SEQ_1:sch 3;
take F;
for y be set st y in dom F holds y in Z by A2;then
A3: dom F c= Z by TARSKI:def 3;
now
let y be set such that
A4: y in Z;
Z c= dom f by A1,Def12;
then Z is Subset of REAL 2 by XBOOLE_1:1;
hence y in dom F by A2,A4;
end;
then Z c= dom F by TARSKI:def 3;
hence dom F = Z by A3,XBOOLE_0:def 10;
hereby
let z be Element of REAL 2;
assume z in Z;then
z in dom F by A2;
hence F.z = hpartdiff12(f,z) by A2;
end;
end;
uniqueness
proof
let F,G be PartFunc of REAL 2,REAL;
assume that
A6: dom F = Z & for z be Element of REAL 2 st z in Z holds
F.z = hpartdiff12(f,z) and
A7: dom G = Z & for z be Element of REAL 2 st z in Z holds
G.z = hpartdiff12(f,z);
now
let z be Element of REAL 2;
assume
A8: z in dom F;
then F.z = hpartdiff12(f,z) by A6;
hence F.z = G.z by A6,A7,A8;
end;
hence thesis by A6,A7,PARTFUN1:34;
end;
end;
definition
let f be PartFunc of REAL 2,REAL;
let Z be set;
assume A1: f is_hpartial_differentiable`21_on Z;
func f`hpartial21|Z -> PartFunc of REAL 2,REAL means
dom it = Z & for z be Element of REAL 2 st z in Z holds
it.z = hpartdiff21(f,z);
existence
proof
defpred P[Element of REAL 2] means $1 in Z;
deffunc F(Element of REAL 2) = hpartdiff21(f,$1);
consider F being PartFunc of REAL 2,REAL such that
A2: (for z be Element of REAL 2 holds z in dom F iff P[z]) &
for z be Element of REAL 2 st z in dom F holds F.z = F(z)
from SEQ_1:sch 3;
take F;
for y be set st y in dom F holds y in Z by A2;then
A3: dom F c= Z by TARSKI:def 3;
now
let y be set such that
A4: y in Z;
Z c= dom f by A1,Def13;
then Z is Subset of REAL 2 by XBOOLE_1:1;
hence y in dom F by A2,A4;
end;
then Z c= dom F by TARSKI:def 3;
hence dom F = Z by A3,XBOOLE_0:def 10;
hereby
let z be Element of REAL 2;
assume z in Z;then
z in dom F by A2;
hence F.z = hpartdiff21(f,z) by A2;
end;
end;
uniqueness
proof
let F,G be PartFunc of REAL 2,REAL;
assume that
A6: dom F = Z & for z be Element of REAL 2 st z in Z holds
F.z = hpartdiff21(f,z) and
A7: dom G = Z & for z be Element of REAL 2 st z in Z holds
G.z = hpartdiff21(f,z);
now
let z be Element of REAL 2;
assume
A8: z in dom F;
then F.z = hpartdiff21(f,z) by A6;
hence F.z = G.z by A6,A7,A8;
end;
hence thesis by A6,A7,PARTFUN1:34;
end;
end;
definition
let f be PartFunc of REAL 2,REAL;
let Z be set;
assume A1: f is_hpartial_differentiable`22_on Z;
func f`hpartial22|Z -> PartFunc of REAL 2,REAL means
dom it = Z & for z be Element of REAL 2 st z in Z holds
it.z = hpartdiff22(f,z);
existence
proof
defpred P[Element of REAL 2] means $1 in Z;
deffunc F(Element of REAL 2) = hpartdiff22(f,$1);
consider F being PartFunc of REAL 2,REAL such that
A2: (for z be Element of REAL 2 holds z in dom F iff P[z]) &
for z be Element of REAL 2 st z in dom F holds F.z = F(z)
from SEQ_1:sch 3;
take F;
for y be set st y in dom F holds y in Z by A2;then
A3: dom F c= Z by TARSKI:def 3;
now
let y be set such that
A4: y in Z;
Z c= dom f by A1,Def14;
then Z is Subset of REAL 2 by XBOOLE_1:1;
hence y in dom F by A2,A4;
end;
then Z c= dom F by TARSKI:def 3;
hence dom F = Z by A3,XBOOLE_0:def 10;
hereby
let z be Element of REAL 2;
assume z in Z;then
z in dom F by A2;
hence F.z = hpartdiff22(f,z) by A2;
end;
end;
uniqueness
proof
let F,G be PartFunc of REAL 2,REAL;
assume that
A6: dom F = Z & for z be Element of REAL 2 st z in Z holds
F.z = hpartdiff22(f,z) and
A7: dom G = Z & for z be Element of REAL 2 st z in Z holds
G.z = hpartdiff22(f,z);
now
let z be Element of REAL 2;
assume
A8: z in dom F;
then F.z = hpartdiff22(f,z) by A6;
hence F.z = G.z by A6,A7,A8;
end;
hence thesis by A6,A7,PARTFUN1:34;
end;
end;
begin :: Main Properties of Second-order Partial Derivatives
theorem Th9:
f is_hpartial_differentiable`11_in z iff
pdiff1(f,z) is_partial_differentiable`1_in z
proof
thus f is_hpartial_differentiable`11_in z implies
pdiff1(f,z) is_partial_differentiable`1_in z
proof
assume
A0: f is_hpartial_differentiable`11_in z;
consider x0,y0 being Real such that
A1: z = <*x0,y0*> & ex N being Neighbourhood of x0
st N c= dom SVF1(pdiff1(f,z),z) & ex L,R st for x st x in N holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x0 = L.(x-x0) + R.(x-x0)
by A0,Def3;
thus thesis by A1,PDIFF_2:def 5;
end;
assume
A3: pdiff1(f,z) is_partial_differentiable`1_in z;
consider x0,y0 being Real such that
A4: z = <*x0,y0*> & ex N being Neighbourhood of x0
st N c= dom SVF1(pdiff1(f,z),z) & ex L,R st for x st x in N holds
SVF1(pdiff1(f,z),z).x - SVF1(pdiff1(f,z),z).x0 = L.(x-x0) + R.(x-x0)
by A3,PDIFF_2:def 5;
thus thesis by A4,Def3;
end;
theorem Th10:
f is_hpartial_differentiable`12_in z iff
pdiff1(f,z) is_partial_differentiable`2_in z
proof
thus f is_hpartial_differentiable`12_in z implies
pdiff1(f,z) is_partial_differentiable`2_in z
proof
assume
A0: f is_hpartial_differentiable`12_in z;
consider x0,y0 being Real such that
A1: z = <*x0,y0*> & ex N being Neighbourhood of y0
st N c= dom SVF2(pdiff1(f,z),z) & ex L,R st for y st y in N holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y0 = L.(y-y0) + R.(y-y0)
by A0,Def4;
thus thesis by A1,PDIFF_2:def 6;
end;
assume
A3: pdiff1(f,z) is_partial_differentiable`2_in z;
consider x0,y0 being Real such that
A4: z = <*x0,y0*> & ex N being Neighbourhood of y0
st N c= dom SVF2(pdiff1(f,z),z) & ex L,R st for y st y in N holds
SVF2(pdiff1(f,z),z).y - SVF2(pdiff1(f,z),z).y0 = L.(y-y0) + R.(y-y0)
by A3,PDIFF_2:def 6;
thus thesis by A4,Def4;
end;
theorem Th11:
f is_hpartial_differentiable`21_in z iff
pdiff2(f,z) is_partial_differentiable`1_in z
proof
thus f is_hpartial_differentiable`21_in z implies
pdiff2(f,z) is_partial_differentiable`1_in z
proof
assume
A0: f is_hpartial_differentiable`21_in z;
consider x0,y0 being Real such that
A1: z = <*x0,y0*> & ex N being Neighbourhood of x0
st N c= dom SVF1(pdiff2(f,z),z) & ex L,R st for x st x in N holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x0 = L.(x-x0) + R.(x-x0)
by A0,Def5;
thus thesis by A1,PDIFF_2:def 5;
end;
assume
A3: pdiff2(f,z) is_partial_differentiable`1_in z;
consider x0,y0 being Real such that
A4: z = <*x0,y0*> & ex N being Neighbourhood of x0
st N c= dom SVF1(pdiff2(f,z),z) & ex L,R st for x st x in N holds
SVF1(pdiff2(f,z),z).x - SVF1(pdiff2(f,z),z).x0 = L.(x-x0) + R.(x-x0)
by A3,PDIFF_2:def 5;
thus thesis by A4,Def5;
end;
theorem Th12:
f is_hpartial_differentiable`22_in z iff
pdiff2(f,z) is_partial_differentiable`2_in z
proof
thus f is_hpartial_differentiable`22_in z implies
pdiff2(f,z) is_partial_differentiable`2_in z
proof
assume
A0: f is_hpartial_differentiable`22_in z;
consider x0,y0 being Real such that
A1: z = <*x0,y0*> & ex N being Neighbourhood of y0
st N c= dom SVF2(pdiff2(f,z),z) & ex L,R st for y st y in N holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y0 = L.(y-y0) + R.(y-y0)
by A0,Def6;
thus thesis by A1,PDIFF_2:def 6;
end;
assume
A3: pdiff2(f,z) is_partial_differentiable`2_in z;
consider x0,y0 being Real such that
A4: z = <*x0,y0*> & ex N being Neighbourhood of y0
st N c= dom SVF2(pdiff2(f,z),z) & ex L,R st for y st y in N holds
SVF2(pdiff2(f,z),z).y - SVF2(pdiff2(f,z),z).y0 = L.(y-y0) + R.(y-y0)
by A3,PDIFF_2:def 6;
thus thesis by A4,Def6;
end;
theorem
f is_hpartial_differentiable`11_in z iff
pdiff1(f,z) is_partial_differentiable_in z,1
proof
thus f is_hpartial_differentiable`11_in z implies
pdiff1(f,z) is_partial_differentiable_in z,1
proof
assume f is_hpartial_differentiable`11_in z;
then pdiff1(f,z) is_partial_differentiable`1_in z by Th9;
hence thesis by PDIFF_2:7;
end;
assume pdiff1(f,z) is_partial_differentiable_in z,1;
then pdiff1(f,z) is_partial_differentiable`1_in z by PDIFF_2:7;
hence thesis by Th9;
end;
theorem
f is_hpartial_differentiable`12_in z iff
pdiff1(f,z) is_partial_differentiable_in z,2
proof
thus f is_hpartial_differentiable`12_in z implies
pdiff1(f,z) is_partial_differentiable_in z,2
proof
assume f is_hpartial_differentiable`12_in z;
then pdiff1(f,z) is_partial_differentiable`2_in z by Th10;
hence thesis by PDIFF_2:8;
end;
assume pdiff1(f,z) is_partial_differentiable_in z,2;
then pdiff1(f,z) is_partial_differentiable`2_in z by PDIFF_2:8;
hence thesis by Th10;
end;
theorem
f is_hpartial_differentiable`21_in z iff
pdiff2(f,z) is_partial_differentiable_in z,1
proof
thus f is_hpartial_differentiable`21_in z implies
pdiff2(f,z) is_partial_differentiable_in z,1
proof
assume f is_hpartial_differentiable`21_in z;
then pdiff2(f,z) is_partial_differentiable`1_in z by Th11;
hence thesis by PDIFF_2:7;
end;
assume pdiff2(f,z) is_partial_differentiable_in z,1;
then pdiff2(f,z) is_partial_differentiable`1_in z by PDIFF_2:7;
hence thesis by Th11;
end;
theorem
f is_hpartial_differentiable`22_in z iff
pdiff2(f,z) is_partial_differentiable_in z,2
proof
thus f is_hpartial_differentiable`22_in z implies
pdiff2(f,z) is_partial_differentiable_in z,2
proof
assume f is_hpartial_differentiable`22_in z;
then pdiff2(f,z) is_partial_differentiable`2_in z by Th12;
hence thesis by PDIFF_2:8;
end;
assume pdiff2(f,z) is_partial_differentiable_in z,2;
then pdiff2(f,z) is_partial_differentiable`2_in z by PDIFF_2:8;
hence thesis by Th12;
end;
theorem Th17:
f is_hpartial_differentiable`11_in z implies
hpartdiff11(f,z) = partdiff1(pdiff1(f,z),z)
proof
assume
A1: f is_hpartial_differentiable`11_in z;
consider x0,y0 being Real such that
A2: z = <*x0,y0*> by FINSEQ_2:120;
A3: pdiff1(f,z) is_partial_differentiable`1_in z by A1,Th9;
hpartdiff11(f,z) = diff(SVF1(pdiff1(f,z),z),x0) by A1,A2,Th5
.= partdiff1(pdiff1(f,z),z) by A2,A3,PDIFF_2:11;
hence thesis;
end;
theorem Th18:
f is_hpartial_differentiable`12_in z implies
hpartdiff12(f,z) = partdiff2(pdiff1(f,z),z)
proof
assume
A1: f is_hpartial_differentiable`12_in z;
consider x0,y0 being Real such that
A2: z = <*x0,y0*> by FINSEQ_2:120;
A3: pdiff1(f,z) is_partial_differentiable`2_in z by A1,Th10;
hpartdiff12(f,z) = diff(SVF2(pdiff1(f,z),z),y0) by A1,A2,Th6
.= partdiff2(pdiff1(f,z),z) by A2,A3,PDIFF_2:12;
hence thesis;
end;
theorem Th19:
f is_hpartial_differentiable`21_in z implies
hpartdiff21(f,z) = partdiff1(pdiff2(f,z),z)
proof
assume
A1: f is_hpartial_differentiable`21_in z;
consider x0,y0 being Real such that
A2: z = <*x0,y0*> by FINSEQ_2:120;
A3: pdiff2(f,z) is_partial_differentiable`1_in z by A1,Th11;
hpartdiff21(f,z) = diff(SVF1(pdiff2(f,z),z),x0) by A1,A2,Th7
.= partdiff1(pdiff2(f,z),z) by A2,A3,PDIFF_2:11;
hence thesis;
end;
theorem Th20:
f is_hpartial_differentiable`22_in z implies
hpartdiff22(f,z) = partdiff2(pdiff2(f,z),z)
proof
assume
A1: f is_hpartial_differentiable`22_in z;
consider x0,y0 being Real such that
A2: z = <*x0,y0*> by FINSEQ_2:120;
A3: pdiff2(f,z) is_partial_differentiable`2_in z by A1,Th12;
hpartdiff22(f,z) = diff(SVF2(pdiff2(f,z),z),y0) by A1,A2,Th8
.= partdiff2(pdiff2(f,z),z) by A2,A3,PDIFF_2:12;
hence thesis;
end;
theorem
for z0 being Element of REAL 2
for N being Neighbourhood of proj(1,2).z0 st
f is_hpartial_differentiable`11_in z0 & N c= dom SVF1(pdiff1(f,z0),z0) holds
for h be convergent_to_0 Real_Sequence, c be constant Real_Sequence
st rng c = {proj(1,2).z0} & rng (h+c) c= N holds
h"(#)(SVF1(pdiff1(f,z0),z0)/*(h+c) - SVF1(pdiff1(f,z0),z0)/*c)
is convergent &
hpartdiff11(f,z0)
= lim (h"(#)(SVF1(pdiff1(f,z0),z0)/*(h+c) - SVF1(pdiff1(f,z0),z0)/*c))
proof
let z0 be Element of REAL 2;
let N be Neighbourhood of proj(1,2).z0;
assume
A1: f is_hpartial_differentiable`11_in z0 & N c= dom SVF1(pdiff1(f,z0),z0);
let h be convergent_to_0 Real_Sequence,
c be constant Real_Sequence such that
A2: rng c = {proj(1,2).z0} & rng (h+c) c= N;
A3: pdiff1(f,z0) is_partial_differentiable`1_in z0 by A1,Th9;
consider x0,y0 being Real such that
A4: z0 = <*x0,y0*> by FINSEQ_2:120;
partdiff1(pdiff1(f,z0),z0)
= diff(SVF1(pdiff1(f,z0),z0),x0) by A3,A4,PDIFF_2:11
.= hpartdiff11(f,z0) by A1,A4,Th5;
hence thesis by A1,A2,A3,PDIFF_2:15;
end;
theorem
for z0 being Element of REAL 2
for N being Neighbourhood of proj(2,2).z0 st
f is_hpartial_differentiable`12_in z0 & N c= dom SVF2(pdiff1(f,z0),z0) holds
for h be convergent_to_0 Real_Sequence, c be constant Real_Sequence
st rng c = {proj(2,2).z0} & rng (h+c) c= N holds
h"(#)(SVF2(pdiff1(f,z0),z0)/*(h+c) - SVF2(pdiff1(f,z0),z0)/*c)
is convergent &
hpartdiff12(f,z0)
= lim (h"(#)(SVF2(pdiff1(f,z0),z0)/*(h+c) - SVF2(pdiff1(f,z0),z0)/*c))
proof
let z0 be Element of REAL 2;
let N be Neighbourhood of proj(2,2).z0;
assume
A1: f is_hpartial_differentiable`12_in z0 & N c= dom SVF2(pdiff1(f,z0),z0);
let h be convergent_to_0 Real_Sequence,
c be constant Real_Sequence such that
A2: rng c = {proj(2,2).z0} & rng (h+c) c= N;
A3: pdiff1(f,z0) is_partial_differentiable`2_in z0 by A1,Th10;
consider x0,y0 being Real such that
A4: z0 = <*x0,y0*> by FINSEQ_2:120;
partdiff2(pdiff1(f,z0),z0)
= diff(SVF2(pdiff1(f,z0),z0),y0) by A3,A4,PDIFF_2:12
.= hpartdiff12(f,z0) by A1,A4,Th6;
hence thesis by A1,A2,A3,PDIFF_2:16;
end;
theorem
for z0 being Element of REAL 2
for N being Neighbourhood of proj(1,2).z0 st
f is_hpartial_differentiable`21_in z0 & N c= dom SVF1(pdiff2(f,z0),z0) holds
for h be convergent_to_0 Real_Sequence, c be constant Real_Sequence
st rng c = {proj(1,2).z0} & rng (h+c) c= N holds
h"(#)(SVF1(pdiff2(f,z0),z0)/*(h+c) - SVF1(pdiff2(f,z0),z0)/*c)
is convergent &
hpartdiff21(f,z0)
= lim (h"(#)(SVF1(pdiff2(f,z0),z0)/*(h+c) - SVF1(pdiff2(f,z0),z0)/*c))
proof
let z0 be Element of REAL 2;
let N be Neighbourhood of proj(1,2).z0;
assume
A1: f is_hpartial_differentiable`21_in z0 & N c= dom SVF1(pdiff2(f,z0),z0);
let h be convergent_to_0 Real_Sequence,
c be constant Real_Sequence such that
A2: rng c = {proj(1,2).z0} & rng (h+c) c= N;
A3: pdiff2(f,z0) is_partial_differentiable`1_in z0 by A1,Th11;
consider x0,y0 being Real such that
A4: z0 = <*x0,y0*> by FINSEQ_2:120;
partdiff1(pdiff2(f,z0),z0)
= diff(SVF1(pdiff2(f,z0),z0),x0) by A3,A4,PDIFF_2:11
.= hpartdiff21(f,z0) by A1,A4,Th7;
hence thesis by A1,A2,A3,PDIFF_2:15;
end;
theorem
for z0 being Element of REAL 2
for N being Neighbourhood of proj(2,2).z0 st
f is_hpartial_differentiable`22_in z0 & N c= dom SVF2(pdiff2(f,z0),z0) holds
for h be convergent_to_0 Real_Sequence, c be constant Real_Sequence
st rng c = {proj(2,2).z0} & rng (h+c) c= N holds
h"(#)(SVF2(pdiff2(f,z0),z0)/*(h+c) - SVF2(pdiff2(f,z0),z0)/*c)
is convergent &
hpartdiff22(f,z0)
= lim (h"(#)(SVF2(pdiff2(f,z0),z0)/*(h+c) - SVF2(pdiff2(f,z0),z0)/*c))
proof
let z0 be Element of REAL 2;
let N be Neighbourhood of proj(2,2).z0;
assume
A1: f is_hpartial_differentiable`22_in z0 & N c= dom SVF2(pdiff2(f,z0),z0);
let h be convergent_to_0 Real_Sequence,
c be constant Real_Sequence such that
A2: rng c = {proj(2,2).z0} & rng (h+c) c= N;
A3: pdiff2(f,z0) is_partial_differentiable`2_in z0 by A1,Th12;
consider x0,y0 being Real such that
A4: z0 = <*x0,y0*> by FINSEQ_2:120;
partdiff2(pdiff2(f,z0),z0)
= diff(SVF2(pdiff2(f,z0),z0),y0) by A3,A4,PDIFF_2:12
.= hpartdiff22(f,z0) by A1,A4,Th8;
hence thesis by A1,A2,A3,PDIFF_2:16;
end;
theorem
f1 is_hpartial_differentiable`11_in z0 &
f2 is_hpartial_differentiable`11_in z0 implies
pdiff1(f1,z0)+pdiff1(f2,z0) is_partial_differentiable`1_in z0 &
partdiff1(pdiff1(f1,z0)+pdiff1(f2,z0),z0)
= hpartdiff11(f1,z0) + hpartdiff11(f2,z0)
proof
assume that
A1: f1 is_hpartial_differentiable`11_in z0 and
A2: f2 is_hpartial_differentiable`11_in z0;
A3: pdiff1(f1,z0) is_partial_differentiable`1_in z0 by A1,Th9;
AA: pdiff1(f2,z0) is_partial_differentiable`1_in z0 by A2,Th9;then
A4: pdiff1(f1,z0)+pdiff1(f2,z0) is_partial_differentiable`1_in z0 &
partdiff1(pdiff1(f1,z0)+pdiff1(f2,z0),z0)
= partdiff1(pdiff1(f1,z0),z0) + partdiff1(pdiff1(f2,z0),z0)
by A3,PDIFF_2:17;
partdiff1(pdiff1(f1,z0)+pdiff1(f2,z0),z0)
= hpartdiff11(f1,z0) + partdiff1(pdiff1(f2,z0),z0) by A1,A4,Th17
.= hpartdiff11(f1,z0) + hpartdiff11(f2,z0) by A2,Th17;
hence thesis by A3,AA,PDIFF_2:17;
end;
theorem
f1 is_hpartial_differentiable`12_in z0 &
f2 is_hpartial_differentiable`12_in z0 implies
pdiff1(f1,z0)+pdiff1(f2,z0) is_partial_differentiable`2_in z0 &
partdiff2(pdiff1(f1,z0)+pdiff1(f2,z0),z0)
= hpartdiff12(f1,z0) + hpartdiff12(f2,z0)
proof
assume that
A1: f1 is_hpartial_differentiable`12_in z0 and
A2: f2 is_hpartial_differentiable`12_in z0;
A3: pdiff1(f1,z0) is_partial_differentiable`2_in z0 by A1,Th10;
AA: pdiff1(f2,z0) is_partial_differentiable`2_in z0 by A2,Th10;then
A4: pdiff1(f1,z0)+pdiff1(f2,z0) is_partial_differentiable`2_in z0 &
partdiff2(pdiff1(f1,z0)+pdiff1(f2,z0),z0)
= partdiff2(pdiff1(f1,z0),z0) + partdiff2(pdiff1(f2,z0),z0)
by A3,PDIFF_2:18;
partdiff2(pdiff1(f1,z0)+pdiff1(f2,z0),z0)
= hpartdiff12(f1,z0) + partdiff2(pdiff1(f2,z0),z0) by A1,A4,Th18
.= hpartdiff12(f1,z0) + hpartdiff12(f2,z0) by A2,Th18;
hence thesis by A3,AA,PDIFF_2:18;
end;
theorem
f1 is_hpartial_differentiable`21_in z0 &
f2 is_hpartial_differentiable`21_in z0 implies
pdiff2(f1,z0)+pdiff2(f2,z0) is_partial_differentiable`1_in z0 &
partdiff1(pdiff2(f1,z0)+pdiff2(f2,z0),z0)
= hpartdiff21(f1,z0) + hpartdiff21(f2,z0)
proof
assume that
A1: f1 is_hpartial_differentiable`21_in z0 and
A2: f2 is_hpartial_differentiable`21_in z0;
A3: pdiff2(f1,z0) is_partial_differentiable`1_in z0 by A1,Th11;
AA: pdiff2(f2,z0) is_partial_differentiable`1_in z0 by A2,Th11;then
A4: pdiff2(f1,z0)+pdiff2(f2,z0) is_partial_differentiable`1_in z0 &
partdiff1(pdiff2(f1,z0)+pdiff2(f2,z0),z0)
= partdiff1(pdiff2(f1,z0),z0) + partdiff1(pdiff2(f2,z0),z0)
by A3,PDIFF_2:17;
partdiff1(pdiff2(f1,z0)+pdiff2(f2,z0),z0)
= hpartdiff21(f1,z0) + partdiff1(pdiff2(f2,z0),z0) by A1,A4,Th19
.= hpartdiff21(f1,z0) + hpartdiff21(f2,z0) by A2,Th19;
hence thesis by A3,AA,PDIFF_2:17;
end;
theorem
f1 is_hpartial_differentiable`22_in z0 &
f2 is_hpartial_differentiable`22_in z0 implies
pdiff2(f1,z0)+pdiff2(f2,z0) is_partial_differentiable`2_in z0 &
partdiff2(pdiff2(f1,z0)+pdiff2(f2,z0),z0)
= hpartdiff22(f1,z0) + hpartdiff22(f2,z0)
proof
assume that
A1: f1 is_hpartial_differentiable`22_in z0 and
A2: f2 is_hpartial_differentiable`22_in z0;
A3: pdiff2(f1,z0) is_partial_differentiable`2_in z0 by A1,Th12;
AA: pdiff2(f2,z0) is_partial_differentiable`2_in z0 by A2,Th12;then
A4: pdiff2(f1,z0)+pdiff2(f2,z0) is_partial_differentiable`2_in z0 &
partdiff2(pdiff2(f1,z0)+pdiff2(f2,z0),z0)
= partdiff2(pdiff2(f1,z0),z0) + partdiff2(pdiff2(f2,z0),z0)
by A3,PDIFF_2:18;
partdiff2(pdiff2(f1,z0)+pdiff2(f2,z0),z0)
= hpartdiff22(f1,z0) + partdiff2(pdiff2(f2,z0),z0) by A1,A4,Th20
.= hpartdiff22(f1,z0) + hpartdiff22(f2,z0) by A2,Th20;
hence thesis by A3,AA,PDIFF_2:18;
end;
theorem
f1 is_hpartial_differentiable`11_in z0 &
f2 is_hpartial_differentiable`11_in z0 implies
pdiff1(f1,z0)-pdiff1(f2,z0) is_partial_differentiable`1_in z0 &
partdiff1(pdiff1(f1,z0)-pdiff1(f2,z0),z0)
= hpartdiff11(f1,z0) - hpartdiff11(f2,z0)
proof
assume that
A1: f1 is_hpartial_differentiable`11_in z0 and
A2: f2 is_hpartial_differentiable`11_in z0;
A3: pdiff1(f1,z0) is_partial_differentiable`1_in z0 by A1,Th9;
AA: pdiff1(f2,z0) is_partial_differentiable`1_in z0 by A2,Th9;then
A4: pdiff1(f1,z0)-pdiff1(f2,z0) is_partial_differentiable`1_in z0 &
partdiff1(pdiff1(f1,z0)-pdiff1(f2,z0),z0)
= partdiff1(pdiff1(f1,z0),z0) - partdiff1(pdiff1(f2,z0),z0)
by A3,PDIFF_2:19;
partdiff1(pdiff1(f1,z0)-pdiff1(f2,z0),z0)
= hpartdiff11(f1,z0) - partdiff1(pdiff1(f2,z0),z0) by A1,A4,Th17
.= hpartdiff11(f1,z0) - hpartdiff11(f2,z0) by A2,Th17;
hence thesis by A3,AA,PDIFF_2:19;
end;
theorem
f1 is_hpartial_differentiable`12_in z0 &
f2 is_hpartial_differentiable`12_in z0 implies
pdiff1(f1,z0)-pdiff1(f2,z0) is_partial_differentiable`2_in z0 &
partdiff2(pdiff1(f1,z0)-pdiff1(f2,z0),z0)
= hpartdiff12(f1,z0) - hpartdiff12(f2,z0)
proof
assume that
A1: f1 is_hpartial_differentiable`12_in z0 and
A2: f2 is_hpartial_differentiable`12_in z0;
A3: pdiff1(f1,z0) is_partial_differentiable`2_in z0 by A1,Th10;
AA: pdiff1(f2,z0) is_partial_differentiable`2_in z0 by A2,Th10;then
A4: pdiff1(f1,z0)-pdiff1(f2,z0) is_partial_differentiable`2_in z0 &
partdiff2(pdiff1(f1,z0)-pdiff1(f2,z0),z0)
= partdiff2(pdiff1(f1,z0),z0) - partdiff2(pdiff1(f2,z0),z0)
by A3,PDIFF_2:20;
partdiff2(pdiff1(f1,z0)-pdiff1(f2,z0),z0)
= hpartdiff12(f1,z0) - partdiff2(pdiff1(f2,z0),z0) by A1,A4,Th18
.= hpartdiff12(f1,z0) - hpartdiff12(f2,z0) by A2,Th18;
hence thesis by A3,AA,PDIFF_2:20;
end;
theorem
f1 is_hpartial_differentiable`21_in z0 &
f2 is_hpartial_differentiable`21_in z0 implies
pdiff2(f1,z0)-pdiff2(f2,z0) is_partial_differentiable`1_in z0 &
partdiff1(pdiff2(f1,z0)-pdiff2(f2,z0),z0)
= hpartdiff21(f1,z0) - hpartdiff21(f2,z0)
proof
assume that
A1: f1 is_hpartial_differentiable`21_in z0 and
A2: f2 is_hpartial_differentiable`21_in z0;
A3: pdiff2(f1,z0) is_partial_differentiable`1_in z0 by A1,Th11;
AA: pdiff2(f2,z0) is_partial_differentiable`1_in z0 by A2,Th11;then
A4: pdiff2(f1,z0)-pdiff2(f2,z0) is_partial_differentiable`1_in z0 &
partdiff1(pdiff2(f1,z0)-pdiff2(f2,z0),z0)
= partdiff1(pdiff2(f1,z0),z0) - partdiff1(pdiff2(f2,z0),z0)
by A3,PDIFF_2:19;
partdiff1(pdiff2(f1,z0)-pdiff2(f2,z0),z0)
= hpartdiff21(f1,z0) - partdiff1(pdiff2(f2,z0),z0) by A1,A4,Th19
.= hpartdiff21(f1,z0) - hpartdiff21(f2,z0) by A2,Th19;
hence thesis by A3,AA,PDIFF_2:19;
end;
theorem
f1 is_hpartial_differentiable`22_in z0 &
f2 is_hpartial_differentiable`22_in z0 implies
pdiff2(f1,z0)-pdiff2(f2,z0) is_partial_differentiable`2_in z0 &
partdiff2(pdiff2(f1,z0)-pdiff2(f2,z0),z0)
= hpartdiff22(f1,z0) - hpartdiff22(f2,z0)
proof
assume that
A1: f1 is_hpartial_differentiable`22_in z0 and
A2: f2 is_hpartial_differentiable`22_in z0;
A3: pdiff2(f1,z0) is_partial_differentiable`2_in z0 by A1,Th12;
AA: pdiff2(f2,z0) is_partial_differentiable`2_in z0 by A2,Th12;then
A4: pdiff2(f1,z0)-pdiff2(f2,z0) is_partial_differentiable`2_in z0 &
partdiff2(pdiff2(f1,z0)-pdiff2(f2,z0),z0)
= partdiff2(pdiff2(f1,z0),z0) - partdiff2(pdiff2(f2,z0),z0)
by A3,PDIFF_2:20;
partdiff2(pdiff2(f1,z0)-pdiff2(f2,z0),z0)
= hpartdiff22(f1,z0) - partdiff2(pdiff2(f2,z0),z0) by A1,A4,Th20
.= hpartdiff22(f1,z0) - hpartdiff22(f2,z0) by A2,Th20;
hence thesis by A3,AA,PDIFF_2:20;
end;
theorem
f is_hpartial_differentiable`11_in z0 implies
r(#)pdiff1(f,z0) is_partial_differentiable`1_in z0 &
partdiff1((r(#)pdiff1(f,z0)),z0) = r*hpartdiff11(f,z0)
proof
assume
A1: f is_hpartial_differentiable`11_in z0;
then pdiff1(f,z0) is_partial_differentiable`1_in z0 by Th9;then
r(#)pdiff1(f,z0) is_partial_differentiable`1_in z0 &
partdiff1((r(#)pdiff1(f,z0)),z0) = r*partdiff1(pdiff1(f,z0),z0)
by PDIFF_2:21;
hence thesis by A1,Th17;
end;
theorem
f is_hpartial_differentiable`12_in z0 implies
r(#)pdiff1(f,z0) is_partial_differentiable`2_in z0 &
partdiff2((r(#)pdiff1(f,z0)),z0) = r*hpartdiff12(f,z0)
proof
assume
A1: f is_hpartial_differentiable`12_in z0;
then pdiff1(f,z0) is_partial_differentiable`2_in z0 by Th10;then
r(#)pdiff1(f,z0) is_partial_differentiable`2_in z0 &
partdiff2((r(#)pdiff1(f,z0)),z0) = r*partdiff2(pdiff1(f,z0),z0)
by PDIFF_2:22;
hence thesis by A1,Th18;
end;
theorem
f is_hpartial_differentiable`21_in z0 implies
r(#)pdiff2(f,z0) is_partial_differentiable`1_in z0 &
partdiff1((r(#)pdiff2(f,z0)),z0) = r*hpartdiff21(f,z0)
proof
assume
A1: f is_hpartial_differentiable`21_in z0;
then pdiff2(f,z0) is_partial_differentiable`1_in z0 by Th11;then
r(#)pdiff2(f,z0) is_partial_differentiable`1_in z0 &
partdiff1((r(#)pdiff2(f,z0)),z0) = r*partdiff1(pdiff2(f,z0),z0)
by PDIFF_2:21;
hence thesis by A1,Th19;
end;
theorem
f is_hpartial_differentiable`22_in z0 implies
r(#)pdiff2(f,z0) is_partial_differentiable`2_in z0 &
partdiff2((r(#)pdiff2(f,z0)),z0) = r*hpartdiff22(f,z0)
proof
assume
A1: f is_hpartial_differentiable`22_in z0;
then pdiff2(f,z0) is_partial_differentiable`2_in z0 by Th12;then
r(#)pdiff2(f,z0) is_partial_differentiable`2_in z0 &
partdiff2((r(#)pdiff2(f,z0)),z0) = r*partdiff2(pdiff2(f,z0),z0)
by PDIFF_2:22;
hence thesis by A1,Th20;
end;
theorem
f1 is_hpartial_differentiable`11_in z0 &
f2 is_hpartial_differentiable`11_in z0 implies
pdiff1(f1,z0)(#)pdiff1(f2,z0) is_partial_differentiable`1_in z0
proof
assume f1 is_hpartial_differentiable`11_in z0 &
f2 is_hpartial_differentiable`11_in z0;
then pdiff1(f1,z0) is_partial_differentiable`1_in z0 &
pdiff1(f2,z0) is_partial_differentiable`1_in z0 by Th9;
hence thesis by PDIFF_2:23;
end;
theorem
f1 is_hpartial_differentiable`12_in z0 &
f2 is_hpartial_differentiable`12_in z0 implies
pdiff1(f1,z0)(#)pdiff1(f2,z0) is_partial_differentiable`2_in z0
proof
assume f1 is_hpartial_differentiable`12_in z0 &
f2 is_hpartial_differentiable`12_in z0;
then pdiff1(f1,z0) is_partial_differentiable`2_in z0 &
pdiff1(f2,z0) is_partial_differentiable`2_in z0 by Th10;
hence thesis by PDIFF_2:24;
end;
theorem
f1 is_hpartial_differentiable`21_in z0 &
f2 is_hpartial_differentiable`21_in z0 implies
pdiff2(f1,z0)(#)pdiff2(f2,z0) is_partial_differentiable`1_in z0
proof
assume f1 is_hpartial_differentiable`21_in z0 &
f2 is_hpartial_differentiable`21_in z0;
then pdiff2(f1,z0) is_partial_differentiable`1_in z0 &
pdiff2(f2,z0) is_partial_differentiable`1_in z0 by Th11;
hence thesis by PDIFF_2:23;
end;
theorem
f1 is_hpartial_differentiable`22_in z0 &
f2 is_hpartial_differentiable`22_in z0 implies
pdiff2(f1,z0)(#)pdiff2(f2,z0) is_partial_differentiable`2_in z0
proof
assume f1 is_hpartial_differentiable`22_in z0 &
f2 is_hpartial_differentiable`22_in z0;
then pdiff2(f1,z0) is_partial_differentiable`2_in z0 &
pdiff2(f2,z0) is_partial_differentiable`2_in z0 by Th12;
hence thesis by PDIFF_2:24;
end;
theorem
for z0 being Element of REAL 2 holds
f is_hpartial_differentiable`11_in z0
implies SVF1(pdiff1(f,z0),z0) is_continuous_in proj(1,2).z0
proof
let z0 be Element of REAL 2;
assume f is_hpartial_differentiable`11_in z0;
then pdiff1(f,z0) is_partial_differentiable`1_in z0 by Th9;
hence thesis by PDIFF_2:25;
end;
theorem
for z0 being Element of REAL 2 holds
f is_hpartial_differentiable`12_in z0
implies SVF2(pdiff1(f,z0),z0) is_continuous_in proj(2,2).z0
proof
let z0 be Element of REAL 2;
assume f is_hpartial_differentiable`12_in z0;
then pdiff1(f,z0) is_partial_differentiable`2_in z0 by Th10;
hence thesis by PDIFF_2:26;
end;
theorem
for z0 being Element of REAL 2 holds
f is_hpartial_differentiable`21_in z0
implies SVF1(pdiff2(f,z0),z0) is_continuous_in proj(1,2).z0
proof
let z0 be Element of REAL 2;
assume f is_hpartial_differentiable`21_in z0;
then pdiff2(f,z0) is_partial_differentiable`1_in z0 by Th11;
hence thesis by PDIFF_2:25;
end;
theorem
for z0 being Element of REAL 2 holds
f is_hpartial_differentiable`22_in z0
implies SVF2(pdiff2(f,z0),z0) is_continuous_in proj(2,2).z0
proof
let z0 be Element of REAL 2;
assume f is_hpartial_differentiable`22_in z0;
then pdiff2(f,z0) is_partial_differentiable`2_in z0 by Th12;
hence thesis by PDIFF_2:26;
end;
theorem
f is_hpartial_differentiable`11_in z0 implies
ex R st R.0 = 0 & R is_continuous_in 0
proof
assume f is_hpartial_differentiable`11_in z0;
then pdiff1(f,z0) is_partial_differentiable`1_in z0 by Th9;
hence thesis by PDIFF_2:27;
end;
theorem
f is_hpartial_differentiable`12_in z0 implies
ex R st R.0 = 0 & R is_continuous_in 0
proof
assume f is_hpartial_differentiable`12_in z0;
then pdiff1(f,z0) is_partial_differentiable`2_in z0 by Th10;
hence thesis by PDIFF_2:28;
end;
theorem
f is_hpartial_differentiable`21_in z0 implies
ex R st R.0 = 0 & R is_continuous_in 0
proof
assume f is_hpartial_differentiable`21_in z0;
then pdiff2(f,z0) is_partial_differentiable`1_in z0 by Th11;
hence thesis by PDIFF_2:27;
end;
theorem
f is_hpartial_differentiable`22_in z0 implies
ex R st R.0 = 0 & R is_continuous_in 0
proof
assume f is_hpartial_differentiable`22_in z0;
then pdiff2(f,z0) is_partial_differentiable`2_in z0 by Th12;
hence thesis by PDIFF_2:28;
end;