:: Second-order Partial Differentiation of Real Binary Functions
:: by Bing Xie , Xiquan Liang and Xiuzhuan Shen
::
:: Received December 16, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, REAL_1, SEQ_1, PARTFUN1, FDIFF_1, FUNCT_1,
PDIFF_1, FINSEQ_1, RCOMP_1, TARSKI, RELAT_1, PDIFF_2, ARYTM_1, ARYTM_3,
CARD_1, XXREAL_1, VALUED_0, SEQ_2, ORDINAL2, XXREAL_0, NAT_1, VALUED_1,
FUNCT_2, CARD_3, FCONT_1, PDIFF_3, FUNCT_7, XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, RELSET_1, PARTFUN1,
XXREAL_0, XCMPLX_0, XREAL_0, ORDINAL1, NUMBERS, REAL_1, VALUED_0,
VALUED_1, SEQ_1, SEQ_2, FINSEQ_1, FINSEQ_2, RCOMP_1, EUCLID, FDIFF_1,
FCONT_1, PDIFF_1, PDIFF_2;
constructors REAL_1, SEQ_2, RCOMP_1, FDIFF_1, FCONT_1, PDIFF_1, PDIFF_2,
RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2, COMPLEX1;
registrations RELSET_1, XREAL_0, MEMBERED, FDIFF_1, FUNCT_2, NAT_1, NUMBERS,
XBOOLE_0, VALUED_0, VALUED_1, EUCLID, ORDINAL1;
requirements SUBSET, REAL, NUMERALS, ARITHM;
equalities 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, PDIFF_1, XREAL_0;
schemes SEQ_1, FUNCT_2;
begin :: Second-order Partial Derivatives
reserve x,x0,x1,y,y0,y1,r,r1,s,p,p1 for Real;
reserve z,z0 for Element of REAL 2;
reserve n for Element of NAT;
reserve s1 for Real_Sequence;
reserve f,f1,f2 for PartFunc of REAL 2,REAL;
reserve R,R1 for RestFunc;
reserve L,L1 for LinearFunc;
registration
cluster -> total for RestFunc;
coherence by FDIFF_1:def 2;
end;
definition
let i be Element of NAT;
let n be non zero Element of NAT;
let f be PartFunc of REAL n,REAL;
func pdiff1(f,i) -> Function of REAL n, REAL means
for z being Element of REAL n holds it.z = partdiff(f,z,i);
existence
proof
deffunc F(Element of REAL n) = In(partdiff(f,$1,i),REAL);
consider g being Function of REAL n,REAL such that
A1: for z being Element of REAL n holds g.z = F(z) from FUNCT_2:sch 4;
take g;
let z be Element of REAL n;
g.z = F(z) by A1;
hence thesis;
end;
uniqueness
proof
let F,G be Function of REAL n,REAL;
assume that
A2: for z being Element of REAL n holds F.z = partdiff(f,z,i) and
A3: for z being Element of REAL n holds G.z = partdiff(f,z,i);
now
let z be Element of REAL n;
F.z = partdiff(f,z,i) by A2;
hence F.z = G.z by A3;
end;
hence thesis by FUNCT_2:63;
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
ex x0,y0
st z = <*x0,y0*> & ex N being Neighbourhood of x0 st N c= dom SVF1(1,pdiff1(f,1
),z) & ex L,R st for x st x in N holds SVF1(1,pdiff1(f,1),z).x - SVF1(1,pdiff1(
f,1),z).x0 = L.(x-x0) + R.(x-x0);
pred f is_hpartial_differentiable`12_in z means
ex x0,y0
st z = <*x0,y0*> & ex N being Neighbourhood of y0 st N c= dom SVF1(2,pdiff1(f,1
),z) & ex L,R st for y st y in N holds SVF1(2,pdiff1(f,1),z).y - SVF1(2,pdiff1(
f,1),z).y0 = L.(y-y0) + R.(y-y0);
pred f is_hpartial_differentiable`21_in z means
ex x0,y0
st z = <*x0,y0*> & ex N being Neighbourhood of x0 st N c= dom SVF1(1,pdiff1(f,2
),z) & ex L,R st for x st x in N holds SVF1(1,pdiff1(f,2),z).x - SVF1(1,pdiff1(
f,2),z).x0 = L.(x-x0) + R.(x-x0);
pred f is_hpartial_differentiable`22_in z means
ex x0,y0
st z = <*x0,y0*> & ex N being Neighbourhood of y0 st N c= dom SVF1(2,pdiff1(f,2
),z) & ex L,R st for y st y in N holds SVF1(2,pdiff1(f,2),z).y - SVF1(2,pdiff1(
f,2),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
:Def6:
ex x0,y0 st z = <*x0,
y0*> & ex N being Neighbourhood of x0 st N c= dom SVF1(1,pdiff1(f,1),z) & ex L,
R st it = L.1 & for x st x in N holds SVF1(1,pdiff1(f,1),z).x - SVF1(1,pdiff1(f
,1),z).x0 = L.(x-x0) + R.(x-x0);
existence
proof
consider x0,y0 such that
A2: z = <*x0,y0*> and
A3: ex N being Neighbourhood of x0 st N c= dom SVF1(1,pdiff1(f,1),z) &
ex L,R st for x st x in N holds SVF1(1,pdiff1(f,1),z).x - SVF1(1,pdiff1(f,1),z)
.x0 = L.(x-x0) + R.(x-x0) by A1;
consider N being Neighbourhood of x0 such that
A4: N c= dom SVF1(1,pdiff1(f,1),z) and
A5: ex L,R st for x st x in N holds SVF1(1,pdiff1(f,1),z).x - SVF1(1,
pdiff1(f,1),z).x0 = L.(x-x0) + R.(x-x0) by A3;
consider L,R such that
A6: for x st x in N holds SVF1(1,pdiff1(f,1),z).x - SVF1(1,pdiff1(f,1)
,z).x0 = L.(x-x0) + R.(x-x0) by A5;
consider r such that
A7: for p holds L.p = r*p by FDIFF_1:def 3;
take r;
L.1 = r*1 by A7
.= r;
hence thesis by A2,A4,A6;
end;
uniqueness
proof
let r,s be Real;
assume that
A8: ex x0,y0 st z = <*x0,y0*> & ex N being Neighbourhood of
x0 st N c= dom SVF1(1,pdiff1(f,1),z) & ex L,R st r = L.1 & for x st x in N
holds SVF1(1,pdiff1(f,1),z).x - SVF1(1,pdiff1(f,1),z).x0 = L.(x-x0) + R.(x-x0)
and
A9: ex x0,y0 st z = <*x0,y0*> & ex N being Neighbourhood
of x0 st N c= dom SVF1(1,pdiff1(f,1),z) & ex L,R st s = L.1 & for x st x in N
holds SVF1(1,pdiff1(f,1),z).x - SVF1(1,pdiff1(f,1),z).x0 = L.(x-x0) + R.(x-x0);
consider x1,y1 such that
A10: z = <*x1,y1*> and
A11: ex N being Neighbourhood of x1 st N c= dom SVF1(1,pdiff1(f,1),z)
& ex L,R st s = L.1 & for x st x in N holds SVF1(1,pdiff1(f,1),z).x - SVF1(1,
pdiff1(f,1),z).x1 = L.(x-x1) + R.(x-x1) by A9;
consider N1 being Neighbourhood of x1 such that
N1 c= dom SVF1(1,pdiff1(f,1),z) and
A12: ex L,R st s = L.1 & for x st x in N1 holds SVF1(1,pdiff1(f,1),z).
x - SVF1(1,pdiff1(f,1),z).x1 = L.(x-x1) + R.(x-x1) by A11;
consider L1,R1 such that
A13: s = L1.1 and
A14: for x st x in N1 holds SVF1(1,pdiff1(f,1),z).x - SVF1(1,pdiff1(f,
1) ,z).x1 = L1.(x-x1) + R1.(x-x1) by A12;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
A16: s = p1*1 by A13,A15;
consider x0,y0 such that
A17: z = <*x0,y0*> and
A18: ex N being Neighbourhood of x0 st N c= dom SVF1(1,pdiff1(f,1),z)
& ex L,R st r = L.1 & for x st x in N holds SVF1(1,pdiff1(f,1),z).x - SVF1(1,
pdiff1(f,1),z).x0 = L.(x-x0) + R.(x-x0) by A8;
consider N being Neighbourhood of x0 such that
N c= dom SVF1(1,pdiff1(f,1),z) and
A19: ex L,R st r = L.1 & for x st x in N holds SVF1(1,pdiff1(f,1),z).x
- SVF1(1,pdiff1(f,1),z).x0 = L.(x-x0) + R.(x-x0) by A18;
consider L,R such that
A20: r = L.1 and
A21: for x st x in N holds SVF1(1,pdiff1(f,1),z).x - SVF1(1,pdiff1(f,1
), z).x0 = L.(x-x0) + R.(x-x0) by A19;
consider r1 such that
A22: for p holds L.p = r1*p by FDIFF_1:def 3;
A23: x0 = x1 by A17,A10,FINSEQ_1:77;
then consider N0 be Neighbourhood of x0 such that
A24: N0 c= N & N0 c= N1 by RCOMP_1:17;
consider g be Real such that
A25: 0 < g and
A26: N0 = ].x0-g,x0+g.[ by RCOMP_1:def 6;
deffunc F(Nat) = g/($1+2);
consider s1 such that
A27: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
now
let n be Nat;
g/(n+2) <> 0 by A25,XREAL_1:139;
hence s1.n <> 0 by A27;
end;
then
A28: s1 is non-zero by SEQ_1:5;
s1 is convergent & lim s1 = 0 by A27,SEQ_4:31;
then reconsider h = s1 as 0-convergent non-zero Real_Sequence by A28,
FDIFF_1:def 1;
A29: for n ex x st x in N & x in N1 & h.n = x-x0
proof
let n;
take x0+g/(n+2);
0+1 < n+1+1 by XREAL_1:6;
then g/(n+2) < g/1 by A25,XREAL_1:76;
then
A30: x0+g/(n+2) < x0+g by XREAL_1:6;
g/(n+2) > 0 by A25,XREAL_1:139;
then x0+-g < x0+g/(n+2) by A25,XREAL_1:6;
then x0+g/(n+2) in ].x0-g,x0+g.[ by A30;
hence thesis by A24,A26,A27;
end;
A31: r = r1*1 by A20,A22;
A32: now
let x;
assume that
A33: x in N and
A34: x in N1;
SVF1(1,pdiff1(f,1),z).x - SVF1(1,pdiff1(f,1),z).x0 = L.(x-x0) + R.(
x-x0) by A21,A33;
then L.(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A14,A23,A34;
then r1*(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A22;
hence r*(x-x0) + R.(x-x0) = s*(x-x0) + R1.(x-x0) by A15,A31,A16;
end;
A35: r - s in REAL by XREAL_0:def 1;
for n being Nat holds r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n
proof
dom R1 = REAL by PARTFUN1:def 2;
then
A36: rng h c= dom R1;
let n be Nat;
dom R = REAL by PARTFUN1:def 2;
then
A37: rng h c= dom R;
A38: n in NAT by ORDINAL1:def 12;
then ex x st x in N & x in N1 & h.n = x-x0 by A29;
then r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A32;
then
A39: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n) by
XCMPLX_1:62;
A40: (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 A38,A37,FUNCT_2:108
.= ((h")(#)(R/*h)).n by VALUED_1:5;
A41: h.n <> 0 by SEQ_1:5;
A42: (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 A38,A36,FUNCT_2:108
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
A43: (s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
.= s*1 by A41,XCMPLX_1:60
.= s;
(r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
.= r*1 by A41,XCMPLX_1:60
.= r;
then r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A39,A43,XCMPLX_1:62;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A40,A42;
hence thesis by RFUNCT_2:1;
end;
then
((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant & (((h")(#)(R1/*h))-((h"
)(#)(R /*h))).1 = r-s by VALUED_0:def 18,A35;
then
A44: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by SEQ_4:25;
A45: (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 r-s = 0-0 by A44,A45,SEQ_2:12;
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
:Def7:
ex x0,y0 st z = <*x0,
y0*> & ex N being Neighbourhood of y0 st N c= dom SVF1(2,pdiff1(f,1),z) & ex L,
R st it = L.1 & for y st y in N holds SVF1(2,pdiff1(f,1),z).y - SVF1(2,pdiff1(f
,1),z).y0 = L.(y-y0) + R.(y-y0);
existence
proof
consider x0,y0 such that
A2: z = <*x0,y0*> and
A3: ex N being Neighbourhood of y0 st N c= dom SVF1(2,pdiff1(f,1),z) &
ex L,R st for y st y in N holds SVF1(2,pdiff1(f,1),z).y - SVF1(2,pdiff1(f,1),z)
.y0 = L.(y-y0) + R.(y-y0) by A1;
consider N being Neighbourhood of y0 such that
A4: N c= dom SVF1(2,pdiff1(f,1),z) and
A5: ex L,R st for y st y in N holds SVF1(2,pdiff1(f,1),z).y - SVF1(2,
pdiff1(f,1),z).y0 = L.(y-y0) + R.(y-y0) by A3;
consider L,R such that
A6: for y st y in N holds SVF1(2,pdiff1(f,1),z).y - SVF1(2,pdiff1(f,1)
,z).y0 = L.(y-y0) + R.(y-y0) by A5;
consider r such that
A7: for p holds L.p = r*p by FDIFF_1:def 3;
take r;
L.1 = r*1 by A7
.= r;
hence thesis by A2,A4,A6;
end;
uniqueness
proof
let r,s be Real;
assume that
A8: ex x0,y0 st z = <*x0,y0*> & ex N being Neighbourhood of
y0 st N c= dom SVF1(2,pdiff1(f,1),z) & ex L,R st r = L.1 & for y st y in N
holds SVF1(2,pdiff1(f,1),z).y - SVF1(2,pdiff1(f,1),z).y0 = L.(y-y0) + R.(y-y0)
and
A9: ex x0,y0 st z = <*x0,y0*> & ex N being Neighbourhood
of y0 st N c= dom SVF1(2,pdiff1(f,1),z) & ex L,R st s = L.1 & for y st y in N
holds SVF1(2,pdiff1(f,1),z).y - SVF1(2,pdiff1(f,1),z).y0 = L.(y-y0) + R.(y-y0);
consider x1,y1 such that
A10: z = <*x1,y1*> and
A11: ex N being Neighbourhood of y1 st N c= dom SVF1(2,pdiff1(f,1),z)
& ex L,R st s = L.1 & for y st y in N holds SVF1(2,pdiff1(f,1),z).y - SVF1(2,
pdiff1(f,1),z).y1 = L.(y-y1) + R.(y-y1) by A9;
consider N1 being Neighbourhood of y1 such that
N1 c= dom SVF1(2,pdiff1(f,1),z) and
A12: ex L,R st s = L.1 & for y st y in N1 holds SVF1(2,pdiff1(f,1),z).
y - SVF1(2,pdiff1(f,1),z).y1 = L.(y-y1) + R.(y-y1) by A11;
consider L1,R1 such that
A13: s = L1.1 and
A14: for y st y in N1 holds SVF1(2,pdiff1(f,1),z).y - SVF1(2,pdiff1(f,
1) ,z).y1 = L1.(y-y1) + R1.(y-y1) by A12;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
A16: s = p1*1 by A13,A15;
consider x0,y0 such that
A17: z = <*x0,y0*> and
A18: ex N being Neighbourhood of y0 st N c= dom SVF1(2,pdiff1(f,1),z)
& ex L,R st r = L.1 & for y st y in N holds SVF1(2,pdiff1(f,1),z).y - SVF1(2,
pdiff1(f,1),z).y0 = L.(y-y0) + R.(y-y0) by A8;
consider N being Neighbourhood of y0 such that
N c= dom SVF1(2,pdiff1(f,1),z) and
A19: ex L,R st r = L.1 & for y st y in N holds SVF1(2,pdiff1(f,1),z).y
- SVF1(2,pdiff1(f,1),z).y0 = L.(y-y0) + R.(y-y0) by A18;
consider L,R such that
A20: r = L.1 and
A21: for y st y in N holds SVF1(2,pdiff1(f,1),z).y - SVF1(2,pdiff1(f,1
), z).y0 = L.(y-y0) + R.(y-y0) by A19;
consider r1 such that
A22: for p holds L.p = r1*p by FDIFF_1:def 3;
A23: y0 = y1 by A17,A10,FINSEQ_1:77;
then consider N0 be Neighbourhood of y0 such that
A24: N0 c= N & N0 c= N1 by RCOMP_1:17;
consider g be Real such that
A25: 0 < g and
A26: N0 = ].y0-g,y0+g.[ by RCOMP_1:def 6;
deffunc F(Nat) = g/($1+2);
consider s1 such that
A27: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
now
let n be Nat ;
g/(n+2) <> 0 by A25,XREAL_1:139;
hence s1.n <> 0 by A27;
end;
then
A28: s1 is non-zero by SEQ_1:5;
s1 is convergent & lim s1 = 0 by A27,SEQ_4:31;
then reconsider h = s1 as 0-convergent non-zero Real_Sequence by A28,
FDIFF_1:def 1;
A29: for n ex y st y in N & y in N1 & h.n = y-y0
proof
let n;
take y0+g/(n+2);
0+1 < n+1+1 by XREAL_1:6;
then g/(n+2) < g/1 by A25,XREAL_1:76;
then
A30: y0+g/(n+2) < y0+g by XREAL_1:6;
g/(n+2) > 0 by A25,XREAL_1:139;
then y0+-g < y0+g/(n+2) by A25,XREAL_1:6;
then y0+g/(n+2) in ].y0-g,y0+g.[ by A30;
hence thesis by A24,A26,A27;
end;
A31: r = r1*1 by A20,A22;
A32: now
let y;
assume that
A33: y in N and
A34: y in N1;
SVF1(2,pdiff1(f,1),z).y - SVF1(2,pdiff1(f,1),z).y0 = L.(y-y0) + R.(
y-y0) by A21,A33;
then L.(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A14,A23,A34;
then r1*(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A22;
hence r*(y-y0) + R.(y-y0) = s*(y-y0) + R1.(y-y0) by A15,A31,A16;
end;
A35: r - s in REAL by XREAL_0:def 1;
now
dom R1 = REAL by PARTFUN1:def 2;
then
A36: rng h c= dom R1;
let n be Nat;
dom R = REAL by PARTFUN1:def 2;
then
A37: rng h c= dom R;
A38: n in NAT by ORDINAL1:def 12;
then ex y st y in N & y in N1 & h.n = y-y0 by A29;
then r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A32;
then
A39: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n) by
XCMPLX_1:62;
A40: (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 A38,A37,FUNCT_2:108
.= ((h")(#)(R/*h)).n by VALUED_1:5;
A41: h.n <> 0 by SEQ_1:5;
A42: (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 A38,A36,FUNCT_2:108
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
A43: (s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
.= s*1 by A41,XCMPLX_1:60
.= s;
(r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
.= r*1 by A41,XCMPLX_1:60
.= r;
then r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A39,A43,XCMPLX_1:62;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A40,A42;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:1;
end;
then
((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant & (((h")(#)(R1/*h))-((h"
)(#)(R /*h))).1 = r-s by VALUED_0:def 18,A35;
then
A44: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by SEQ_4:25;
A45: (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 r-s = 0-0 by A44,A45,SEQ_2:12;
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
:Def8:
ex x0,y0 st z = <*x0,
y0*> & ex N being Neighbourhood of x0 st N c= dom SVF1(1,pdiff1(f,2),z) & ex L,
R st it = L.1 & for x st x in N holds SVF1(1,pdiff1(f,2),z).x - SVF1(1,pdiff1(f
,2),z).x0 = L.(x-x0) + R.(x-x0);
existence
proof
consider x0,y0 such that
A2: z = <*x0,y0*> and
A3: ex N being Neighbourhood of x0 st N c= dom SVF1(1,pdiff1(f,2),z) &
ex L,R st for x st x in N holds SVF1(1,pdiff1(f,2),z).x - SVF1(1,pdiff1(f,2),z)
.x0 = L.(x-x0) + R.(x-x0) by A1;
consider N being Neighbourhood of x0 such that
A4: N c= dom SVF1(1,pdiff1(f,2),z) and
A5: ex L,R st for x st x in N holds SVF1(1,pdiff1(f,2),z).x - SVF1(1,
pdiff1(f,2),z).x0 = L.(x-x0) + R.(x-x0) by A3;
consider L,R such that
A6: for x st x in N holds SVF1(1,pdiff1(f,2),z).x - SVF1(1,pdiff1(f,2)
,z).x0 = L.(x-x0) + R.(x-x0) by A5;
consider r such that
A7: for p holds L.p = r*p by FDIFF_1:def 3;
take r;
L.1 = r*1 by A7
.= r;
hence thesis by A2,A4,A6;
end;
uniqueness
proof
let r,s be Real;
assume that
A8: ex x0,y0 st z = <*x0,y0*> & ex N being Neighbourhood of
x0 st N c= dom SVF1(1,pdiff1(f,2),z) & ex L,R st r = L.1 & for x st x in N
holds SVF1(1,pdiff1(f,2),z).x - SVF1(1,pdiff1(f,2),z).x0 = L.(x-x0) + R.(x-x0)
and
A9: ex x0,y0 st z = <*x0,y0*> & ex N being Neighbourhood
of x0 st N c= dom SVF1(1,pdiff1(f,2),z) & ex L,R st s = L.1 & for x st x in N
holds SVF1(1,pdiff1(f,2),z).x - SVF1(1,pdiff1(f,2),z).x0 = L.(x-x0) + R.(x-x0);
consider x1,y1 such that
A10: z = <*x1,y1*> and
A11: ex N being Neighbourhood of x1 st N c= dom SVF1(1,pdiff1(f,2),z)
& ex L,R st s = L.1 & for x st x in N holds SVF1(1,pdiff1(f,2),z).x - SVF1(1,
pdiff1(f,2),z).x1 = L.(x-x1) + R.(x-x1) by A9;
consider N1 being Neighbourhood of x1 such that
N1 c= dom SVF1(1,pdiff1(f,2),z) and
A12: ex L,R st s = L.1 & for x st x in N1 holds SVF1(1,pdiff1(f,2),z).
x - SVF1(1,pdiff1(f,2),z).x1 = L.(x-x1) + R.(x-x1) by A11;
consider L1,R1 such that
A13: s = L1.1 and
A14: for x st x in N1 holds SVF1(1,pdiff1(f,2),z).x - SVF1(1,pdiff1(f,
2) ,z).x1 = L1.(x-x1) + R1.(x-x1) by A12;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
A16: s = p1*1 by A13,A15;
consider x0,y0 such that
A17: z = <*x0,y0*> and
A18: ex N being Neighbourhood of x0 st N c= dom SVF1(1,pdiff1(f,2),z)
& ex L,R st r = L.1 & for x st x in N holds SVF1(1,pdiff1(f,2),z).x - SVF1(1,
pdiff1(f,2),z).x0 = L.(x-x0) + R.(x-x0) by A8;
consider N being Neighbourhood of x0 such that
N c= dom SVF1(1,pdiff1(f,2),z) and
A19: ex L,R st r = L.1 & for x st x in N holds SVF1(1,pdiff1(f,2),z).x
- SVF1(1,pdiff1(f,2),z).x0 = L.(x-x0) + R.(x-x0) by A18;
consider L,R such that
A20: r = L.1 and
A21: for x st x in N holds SVF1(1,pdiff1(f,2),z).x - SVF1(1,pdiff1(f,2
), z).x0 = L.(x-x0) + R.(x-x0) by A19;
consider r1 such that
A22: for p holds L.p = r1*p by FDIFF_1:def 3;
A23: x0 = x1 by A17,A10,FINSEQ_1:77;
then consider N0 be Neighbourhood of x0 such that
A24: N0 c= N & N0 c= N1 by RCOMP_1:17;
consider g be Real such that
A25: 0 < g and
A26: N0 = ].x0-g,x0+g.[ by RCOMP_1:def 6;
deffunc F(Nat) = g/($1+2);
consider s1 such that
A27: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
now
let n be Nat;
g/(n+2) <> 0 by A25,XREAL_1:139;
hence s1.n <> 0 by A27;
end;
then
A28: s1 is non-zero by SEQ_1:5;
s1 is convergent & lim s1 = 0 by A27,SEQ_4:31;
then reconsider h = s1 as 0-convergent non-zero Real_Sequence by A28,
FDIFF_1:def 1;
A29: for n ex x st x in N & x in N1 & h.n = x-x0
proof
let n;
take x0+g/(n+2);
0+1 < n+1+1 by XREAL_1:6;
then g/(n+2) < g/1 by A25,XREAL_1:76;
then
A30: x0+g/(n+2) < x0+g by XREAL_1:6;
g/(n+2) > 0 by A25,XREAL_1:139;
then x0+-g < x0+g/(n+2) by A25,XREAL_1:6;
then x0+g/(n+2) in ].x0-g,x0+g.[ by A30;
hence thesis by A24,A26,A27;
end;
A31: r = r1*1 by A20,A22;
A32: now
let x;
assume that
A33: x in N and
A34: x in N1;
SVF1(1,pdiff1(f,2),z).x - SVF1(1,pdiff1(f,2),z).x0 = L.(x-x0) + R.(
x-x0) by A21,A33;
then L.(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A14,A23,A34;
then r1*(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A22;
hence r*(x-x0) + R.(x-x0) = s*(x-x0) + R1.(x-x0) by A15,A31,A16;
end;
A35: r - s in REAL by XREAL_0:def 1;
now
dom R1 = REAL by PARTFUN1:def 2;
then
A36: rng h c= dom R1;
let n be Nat;
dom R = REAL by PARTFUN1:def 2;
then
A37: rng h c= dom R;
A38: n in NAT by ORDINAL1:def 12;
then ex x st x in N & x in N1 & h.n = x-x0 by A29;
then r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A32;
then
A39: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n) by
XCMPLX_1:62;
A40: (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 A38,A37,FUNCT_2:108
.= ((h")(#)(R/*h)).n by VALUED_1:5;
A41: h.n <> 0 by SEQ_1:5;
A42: (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 A38,A36,FUNCT_2:108
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
A43: (s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
.= s*1 by A41,XCMPLX_1:60
.= s;
(r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
.= r*1 by A41,XCMPLX_1:60
.= r;
then r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A39,A43,XCMPLX_1:62;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A40,A42;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by A38,VALUED_1:15;
end;
then
((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant & (((h")(#)(R1/*h))-((h"
)(#)(R /*h))).1 = r-s by VALUED_0:def 18,A35;
then
A44: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by SEQ_4:25;
A45: (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 r-s = 0-0 by A44,A45,SEQ_2:12;
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
:Def9:
ex x0,y0 st z = <*x0,
y0*> & ex N being Neighbourhood of y0 st N c= dom SVF1(2,pdiff1(f,2),z) & ex L,
R st it = L.1 & for y st y in N holds SVF1(2,pdiff1(f,2),z).y - SVF1(2,pdiff1(f
,2),z).y0 = L.(y-y0) + R.(y-y0);
existence
proof
consider x0,y0 such that
A2: z = <*x0,y0*> and
A3: ex N being Neighbourhood of y0 st N c= dom SVF1(2,pdiff1(f,2),z) &
ex L,R st for y st y in N holds SVF1(2,pdiff1(f,2),z).y - SVF1(2,pdiff1(f,2),z)
.y0 = L.(y-y0) + R.(y-y0) by A1;
consider N being Neighbourhood of y0 such that
A4: N c= dom SVF1(2,pdiff1(f,2),z) and
A5: ex L,R st for y st y in N holds SVF1(2,pdiff1(f,2),z).y - SVF1(2,
pdiff1(f,2),z).y0 = L.(y-y0) + R.(y-y0) by A3;
consider L,R such that
A6: for y st y in N holds SVF1(2,pdiff1(f,2),z).y - SVF1(2,pdiff1(f,2)
,z).y0 = L.(y-y0) + R.(y-y0) by A5;
consider r such that
A7: for p holds L.p = r*p by FDIFF_1:def 3;
take r;
L.1 = r*1 by A7
.= r;
hence thesis by A2,A4,A6;
end;
uniqueness
proof
let r,s be Real;
assume that
A8: ex x0,y0 st z = <*x0,y0*> & ex N being Neighbourhood of
y0 st N c= dom SVF1(2,pdiff1(f,2),z) & ex L,R st r = L.1 & for y st y in N
holds SVF1(2,pdiff1(f,2),z).y - SVF1(2,pdiff1(f,2),z).y0 = L.(y-y0) + R.(y-y0)
and
A9: ex x0,y0 st z = <*x0,y0*> & ex N being Neighbourhood
of y0 st N c= dom SVF1(2,pdiff1(f,2),z) & ex L,R st s = L.1 & for y st y in N
holds SVF1(2,pdiff1(f,2),z).y - SVF1(2,pdiff1(f,2),z).y0 = L.(y-y0) + R.(y-y0);
consider x1,y1 such that
A10: z = <*x1,y1*> and
A11: ex N being Neighbourhood of y1 st N c= dom SVF1(2,pdiff1(f,2),z)
& ex L,R st s = L.1 & for y st y in N holds SVF1(2,pdiff1(f,2),z).y - SVF1(2,
pdiff1(f,2),z).y1 = L.(y-y1) + R.(y-y1) by A9;
consider N1 being Neighbourhood of y1 such that
N1 c= dom SVF1(2,pdiff1(f,2),z) and
A12: ex L,R st s = L.1 & for y st y in N1 holds SVF1(2,pdiff1(f,2),z).
y - SVF1(2,pdiff1(f,2),z).y1 = L.(y-y1) + R.(y-y1) by A11;
consider L1,R1 such that
A13: s = L1.1 and
A14: for y st y in N1 holds SVF1(2,pdiff1(f,2),z).y - SVF1(2,pdiff1(f,
2) ,z).y1 = L1.(y-y1) + R1.(y-y1) by A12;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
A16: s = p1*1 by A13,A15;
consider x0,y0 such that
A17: z = <*x0,y0*> and
A18: ex N being Neighbourhood of y0 st N c= dom SVF1(2,pdiff1(f,2),z)
& ex L,R st r = L.1 & for y st y in N holds SVF1(2,pdiff1(f,2),z).y - SVF1(2,
pdiff1(f,2),z).y0 = L.(y-y0) + R.(y-y0) by A8;
consider N being Neighbourhood of y0 such that
N c= dom SVF1(2,pdiff1(f,2),z) and
A19: ex L,R st r = L.1 & for y st y in N holds SVF1(2,pdiff1(f,2),z).y
- SVF1(2,pdiff1(f,2),z).y0 = L.(y-y0) + R.(y-y0) by A18;
consider L,R such that
A20: r = L.1 and
A21: for y st y in N holds SVF1(2,pdiff1(f,2),z).y - SVF1(2,pdiff1(f,2
), z).y0 = L.(y-y0) + R.(y-y0) by A19;
consider r1 such that
A22: for p holds L.p = r1*p by FDIFF_1:def 3;
A23: y0 = y1 by A17,A10,FINSEQ_1:77;
then consider N0 be Neighbourhood of y0 such that
A24: N0 c= N & N0 c= N1 by RCOMP_1:17;
consider g be Real such that
A25: 0 < g and
A26: N0 = ].y0-g,y0+g.[ by RCOMP_1:def 6;
deffunc F(Nat) = g/($1+2);
consider s1 such that
A27: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
now
let n be Nat;
g/(n+2) <> 0 by A25,XREAL_1:139;
hence s1.n <> 0 by A27;
end;
then
A28: s1 is non-zero by SEQ_1:5;
s1 is convergent & lim s1 = 0 by A27,SEQ_4:31;
then reconsider h = s1 as 0-convergent non-zero Real_Sequence by A28,
FDIFF_1:def 1;
A29: for n ex y st y in N & y in N1 & h.n = y-y0
proof
let n;
take y0+g/(n+2);
0+1 < n+1+1 by XREAL_1:6;
then g/(n+2) < g/1 by A25,XREAL_1:76;
then
A30: y0+g/(n+2) < y0+g by XREAL_1:6;
g/(n+2) > 0 by A25,XREAL_1:139;
then y0+-g < y0+g/(n+2) by A25,XREAL_1:6;
then y0+g/(n+2) in ].y0-g,y0+g.[ by A30;
hence thesis by A24,A26,A27;
end;
A31: r = r1*1 by A20,A22;
A32: now
let y;
assume that
A33: y in N and
A34: y in N1;
SVF1(2,pdiff1(f,2),z).y - SVF1(2,pdiff1(f,2),z).y0 = L.(y-y0) + R.(
y-y0) by A21,A33;
then L.(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A14,A23,A34;
then r1*(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A22;
hence r*(y-y0) + R.(y-y0) = s*(y-y0) + R1.(y-y0) by A15,A31,A16;
end;
A35: r -s in REAL by XREAL_0:def 1;
now
dom R1 = REAL by PARTFUN1:def 2;
then
A36: rng h c= dom R1;
let n be Nat;
dom R = REAL by PARTFUN1:def 2;
then
A37: rng h c= dom R;
A38: n in NAT by ORDINAL1:def 12;
then ex y st y in N & y in N1 & h.n = y-y0 by A29;
then r*(h.n) + R.(h.n) = s*(h.n) + R1.(h.n) by A32;
then
A39: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (s*(h.n) + R1.(h.n))/(h.n) by
XCMPLX_1:62;
A40: (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 A38,A37,FUNCT_2:108
.= ((h")(#)(R/*h)).n by VALUED_1:5;
A41: h.n <> 0 by SEQ_1:5;
A42: (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 A38,A36,FUNCT_2:108
.= ((h")(#)(R1/*h)).n by VALUED_1:5;
A43: (s*(h.n))/(h.n) = s*((h.n)/(h.n)) by XCMPLX_1:74
.= s*1 by A41,XCMPLX_1:60
.= s;
(r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
.= r*1 by A41,XCMPLX_1:60
.= r;
then r + (R.(h.n))/(h.n) = s + (R1.(h.n))/(h.n) by A39,A43,XCMPLX_1:62;
then r = s + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n) by A40,A42;
hence r - s = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by RFUNCT_2:1;
end;
then
((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant & (((h")(#)(R1/*h))-((h"
)(#)(R /*h))).1 = r-s by VALUED_0:def 18,A35;
then
A44: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-s by SEQ_4:25;
A45: (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 r-s = 0-0 by A44,A45,SEQ_2:12;
hence thesis;
end;
end;
theorem
z = <*x0,y0*> & f is_hpartial_differentiable`11_in z implies SVF1(1,
pdiff1(f,1),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
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of x1 st N c= dom SVF1(1,pdiff1(f,1),z) &
ex L,R st for x st x in N holds SVF1(1,pdiff1(f,1),z).x - SVF1(1,pdiff1(f,1),z)
.x1 = L.(x-x1) + R.(x-x1) by A2;
x0 = x1 by A1,A3,FINSEQ_1:77;
hence thesis by A4,FDIFF_1:def 4;
end;
theorem
z = <*x0,y0*> & f is_hpartial_differentiable`12_in z implies SVF1(2,
pdiff1(f,1),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
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of y1 st N c= dom SVF1(2,pdiff1(f,1),z) &
ex L,R st for y st y in N holds SVF1(2,pdiff1(f,1),z).y - SVF1(2,pdiff1(f,1),z)
.y1 = L.(y-y1) + R.(y-y1) by A2;
y0 = y1 by A1,A3,FINSEQ_1:77;
hence thesis by A4,FDIFF_1:def 4;
end;
theorem
z = <*x0,y0*> & f is_hpartial_differentiable`21_in z implies SVF1(1,
pdiff1(f,2),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
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of x1 st N c= dom SVF1(1,pdiff1(f,2),z) &
ex L,R st for x st x in N holds SVF1(1,pdiff1(f,2),z).x - SVF1(1,pdiff1(f,2),z)
.x1 = L.(x-x1) + R.(x-x1) by A2;
x0 = x1 by A1,A3,FINSEQ_1:77;
hence thesis by A4,FDIFF_1:def 4;
end;
theorem
z = <*x0,y0*> & f is_hpartial_differentiable`22_in z implies SVF1(2,
pdiff1(f,2),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
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of y1 st N c= dom SVF1(2,pdiff1(f,2),z) &
ex L,R st for y st y in N holds SVF1(2,pdiff1(f,2),z).y - SVF1(2,pdiff1(f,2),z)
.y1 = L.(y-y1) + R.(y-y1) by A2;
y0 = y1 by A1,A3,FINSEQ_1:77;
hence thesis by A4,FDIFF_1:def 4;
end;
theorem Th5:
z = <*x0,y0*> & f is_hpartial_differentiable`11_in z implies
hpartdiff11(f,z) = diff(SVF1(1,pdiff1(f,1),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 such that
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of x1 st N c= dom SVF1(1,pdiff1(f,1),z) &
ex L,R st for x st x in N holds SVF1(1,pdiff1(f,1),z).x - SVF1(1,pdiff1(f,1),z)
.x1 = L.(x-x1) + R.(x-x1) by A2;
consider N being Neighbourhood of x1 such that
A5: N c= dom SVF1(1,pdiff1(f,1),z) and
A6: ex L,R st for x st x in N holds SVF1(1,pdiff1(f,1),z).x - SVF1(1,
pdiff1(f,1),z).x1 = L.(x-x1) + R.(x-x1) by A4;
A7: x0 = x1 by A1,A3,FINSEQ_1:77;
then
A8: SVF1(1,pdiff1(f,1),z) is_differentiable_in x0 by A5,A6,FDIFF_1:def 4;
consider L,R such that
A9: for x st x in N holds SVF1(1,pdiff1(f,1),z).x - SVF1(1,pdiff1(f,1),z
).x1 = L.(x-x1) + R.(x-x1) by A6;
r = L.1 by A2,A3,A5,A9,Def6;
hence thesis by A5,A9,A7,A8,FDIFF_1:def 5;
end;
theorem Th6:
z = <*x0,y0*> & f is_hpartial_differentiable`12_in z implies
hpartdiff12(f,z) = diff(SVF1(2,pdiff1(f,1),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 such that
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of y1 st N c= dom SVF1(2,pdiff1(f,1),z) &
ex L,R st for y st y in N holds SVF1(2,pdiff1(f,1),z).y - SVF1(2,pdiff1(f,1),z)
.y1 = L.(y-y1) + R.(y-y1) by A2;
consider N being Neighbourhood of y1 such that
A5: N c= dom SVF1(2,pdiff1(f,1),z) and
A6: ex L,R st for y st y in N holds SVF1(2,pdiff1(f,1),z).y - SVF1(2,
pdiff1(f,1),z).y1 = L.(y-y1) + R.(y-y1) by A4;
A7: y0 = y1 by A1,A3,FINSEQ_1:77;
then
A8: SVF1(2,pdiff1(f,1),z) is_differentiable_in y0 by A5,A6,FDIFF_1:def 4;
consider L,R such that
A9: for y st y in N holds SVF1(2,pdiff1(f,1),z).y - SVF1(2,pdiff1(f,1),z
).y1 = L.(y-y1) + R.(y-y1) by A6;
r = L.1 by A2,A3,A5,A9,Def7;
hence thesis by A5,A9,A7,A8,FDIFF_1:def 5;
end;
theorem Th7:
z = <*x0,y0*> & f is_hpartial_differentiable`21_in z implies
hpartdiff21(f,z) = diff(SVF1(1,pdiff1(f,2),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 such that
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of x1 st N c= dom SVF1(1,pdiff1(f,2),z) &
ex L,R st for x st x in N holds SVF1(1,pdiff1(f,2),z).x - SVF1(1,pdiff1(f,2),z)
.x1 = L.(x-x1) + R.(x-x1) by A2;
consider N being Neighbourhood of x1 such that
A5: N c= dom SVF1(1,pdiff1(f,2),z) and
A6: ex L,R st for x st x in N holds SVF1(1,pdiff1(f,2),z).x - SVF1(1,
pdiff1(f,2),z).x1 = L.(x-x1) + R.(x-x1) by A4;
A7: x0 = x1 by A1,A3,FINSEQ_1:77;
then
A8: SVF1(1,pdiff1(f,2),z) is_differentiable_in x0 by A5,A6,FDIFF_1:def 4;
consider L,R such that
A9: for x st x in N holds SVF1(1,pdiff1(f,2),z).x - SVF1(1,pdiff1(f,2),z
).x1 = L.(x-x1) + R.(x-x1) by A6;
r = L.1 by A2,A3,A5,A9,Def8;
hence thesis by A5,A9,A7,A8,FDIFF_1:def 5;
end;
theorem Th8:
z = <*x0,y0*> & f is_hpartial_differentiable`22_in z implies
hpartdiff22(f,z) = diff(SVF1(2,pdiff1(f,2),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 such that
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of y1 st N c= dom SVF1(2,pdiff1(f,2),z) &
ex L,R st for y st y in N holds SVF1(2,pdiff1(f,2),z).y - SVF1(2,pdiff1(f,2),z)
.y1 = L.(y-y1) + R.(y-y1) by A2;
consider N being Neighbourhood of y1 such that
A5: N c= dom SVF1(2,pdiff1(f,2),z) and
A6: ex L,R st for y st y in N holds SVF1(2,pdiff1(f,2),z).y - SVF1(2,
pdiff1(f,2),z).y1 = L.(y-y1) + R.(y-y1) by A4;
A7: y0 = y1 by A1,A3,FINSEQ_1:77;
then
A8: SVF1(2,pdiff1(f,2),z) is_differentiable_in y0 by A5,A6,FDIFF_1:def 4;
consider L,R such that
A9: for y st y in N holds SVF1(2,pdiff1(f,2),z).y - SVF1(2,pdiff1(f,2),z
).y1 = L.(y-y1) + R.(y-y1) by A6;
r = L.1 by A2,A3,A5,A9,Def9;
hence thesis by A5,A9,A7,A8,FDIFF_1:def 5;
end;
definition
let f be PartFunc of REAL 2,REAL;
let Z be set;
pred f is_hpartial_differentiable`11_on Z means
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
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
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
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
deffunc F(Element of REAL 2) = In(hpartdiff11(f,$1),REAL);
defpred P[Element of REAL 2] means $1 in Z;
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;
now
Z c= dom f by A1;
then
A3: Z is Subset of REAL 2 by XBOOLE_1:1;
let y be object;
assume y in Z;
hence y in dom F by A2,A3;
end;
then
A4: Z c= dom F by TARSKI:def 3;
for y be object st y in dom F holds y in Z by A2;
then dom F c= Z by TARSKI:def 3;
hence dom F = Z by A4,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 = F(z) by A2
.= hpartdiff11(f,z);
end;
end;
uniqueness
proof
let F,G be PartFunc of REAL 2,REAL;
assume that
A5: dom F = Z and
A6: for z be Element of REAL 2 st z in Z holds F.z = hpartdiff11(f,z) and
A7: dom G = Z and
A8: 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
A9: z in dom F;
then F.z = hpartdiff11(f,z) by A5,A6;
hence F.z = G.z by A5,A8,A9;
end;
hence thesis by A5,A7,PARTFUN1:5;
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
deffunc F(Element of REAL 2) = In(hpartdiff12(f,$1),REAL);
defpred P[Element of REAL 2] means $1 in Z;
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;
now
Z c= dom f by A1;
then
A3: Z is Subset of REAL 2 by XBOOLE_1:1;
let y be object;
assume y in Z;
hence y in dom F by A2,A3;
end;
then
A4: Z c= dom F by TARSKI:def 3;
for y be object st y in dom F holds y in Z by A2;
then dom F c= Z by TARSKI:def 3;
hence dom F = Z by A4,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 = F(z) by A2
.= hpartdiff12(f,z);
end;
end;
uniqueness
proof
let F,G be PartFunc of REAL 2,REAL;
assume that
A5: dom F = Z and
A6: for z be Element of REAL 2 st z in Z holds F.z = hpartdiff12(f,z) and
A7: dom G = Z and
A8: 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
A9: z in dom F;
then F.z = hpartdiff12(f,z) by A5,A6;
hence F.z = G.z by A5,A8,A9;
end;
hence thesis by A5,A7,PARTFUN1:5;
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
deffunc F(Element of REAL 2) = In(hpartdiff21(f,$1),REAL);
defpred P[Element of REAL 2] means $1 in Z;
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;
now
Z c= dom f by A1;
then
A3: Z is Subset of REAL 2 by XBOOLE_1:1;
let y be object;
assume y in Z;
hence y in dom F by A2,A3;
end;
then
A4: Z c= dom F by TARSKI:def 3;
for y be object st y in dom F holds y in Z by A2;
then dom F c= Z by TARSKI:def 3;
hence dom F = Z by A4,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 = F(z) by A2
.= hpartdiff21(f,z);
end;
end;
uniqueness
proof
let F,G be PartFunc of REAL 2,REAL;
assume that
A5: dom F = Z and
A6: for z be Element of REAL 2 st z in Z holds F.z = hpartdiff21(f,z) and
A7: dom G = Z and
A8: 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
A9: z in dom F;
then F.z = hpartdiff21(f,z) by A5,A6;
hence F.z = G.z by A5,A8,A9;
end;
hence thesis by A5,A7,PARTFUN1:5;
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
deffunc F(Element of REAL 2) = In(hpartdiff22(f,$1),REAL);
defpred P[Element of REAL 2] means $1 in Z;
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;
now
Z c= dom f by A1;
then
A3: Z is Subset of REAL 2 by XBOOLE_1:1;
let y be object;
assume y in Z;
hence y in dom F by A2,A3;
end;
then
A4: Z c= dom F by TARSKI:def 3;
for y be object st y in dom F holds y in Z by A2;
then dom F c= Z by TARSKI:def 3;
hence dom F = Z by A4,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 = F(z) by A2
.= hpartdiff22(f,z);
end;
end;
uniqueness
proof
let F,G be PartFunc of REAL 2,REAL;
assume that
A5: dom F = Z and
A6: for z be Element of REAL 2 st z in Z holds F.z = hpartdiff22(f,z) and
A7: dom G = Z and
A8: 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
A9: z in dom F;
then F.z = hpartdiff22(f,z) by A5,A6;
hence F.z = G.z by A5,A8,A9;
end;
hence thesis by A5,A7,PARTFUN1:5;
end;
end;
begin :: Main Properties of Second-order Partial Derivatives
theorem Th9:
f is_hpartial_differentiable`11_in z iff pdiff1(f,1)
is_partial_differentiable_in z,1
by PDIFF_2:9;
theorem Th10:
f is_hpartial_differentiable`12_in z iff pdiff1(f,1)
is_partial_differentiable_in z,2
by PDIFF_2:10;
theorem Th11:
f is_hpartial_differentiable`21_in z iff pdiff1(f,2)
is_partial_differentiable_in z,1
by PDIFF_2:9;
theorem Th12:
f is_hpartial_differentiable`22_in z iff pdiff1(f,2)
is_partial_differentiable_in z,2
by PDIFF_2:10;
theorem Th13:
f is_hpartial_differentiable`11_in z implies hpartdiff11(f,z) =
partdiff(pdiff1(f,1),z,1)
proof
consider x0,y0 being Element of REAL such that
A1: z = <*x0,y0*> by FINSEQ_2:100;
assume
A2: f is_hpartial_differentiable`11_in z;
then
A3: pdiff1(f,1) is_partial_differentiable_in z,1 by Th9;
hpartdiff11(f,z) = diff(SVF1(1,pdiff1(f,1),z),x0) by A2,A1,Th5
.= partdiff(pdiff1(f,1),z,1) by A1,A3,PDIFF_2:13;
hence thesis;
end;
theorem Th14:
f is_hpartial_differentiable`12_in z implies hpartdiff12(f,z) =
partdiff(pdiff1(f,1),z,2)
proof
consider x0,y0 being Element of REAL such that
A1: z = <*x0,y0*> by FINSEQ_2:100;
assume
A2: f is_hpartial_differentiable`12_in z;
then
A3: pdiff1(f,1) is_partial_differentiable_in z,2 by Th10;
hpartdiff12(f,z) = diff(SVF1(2,pdiff1(f,1),z),y0) by A2,A1,Th6
.= partdiff(pdiff1(f,1),z,2) by A1,A3,PDIFF_2:14;
hence thesis;
end;
theorem Th15:
f is_hpartial_differentiable`21_in z implies hpartdiff21(f,z) =
partdiff(pdiff1(f,2),z,1)
proof
consider x0,y0 being Element of REAL such that
A1: z = <*x0,y0*> by FINSEQ_2:100;
assume
A2: f is_hpartial_differentiable`21_in z;
then
A3: pdiff1(f,2) is_partial_differentiable_in z,1 by Th11;
hpartdiff21(f,z) = diff(SVF1(1,pdiff1(f,2),z),x0) by A2,A1,Th7
.= partdiff(pdiff1(f,2),z,1) by A1,A3,PDIFF_2:13;
hence thesis;
end;
theorem Th16:
f is_hpartial_differentiable`22_in z implies hpartdiff22(f,z) =
partdiff(pdiff1(f,2),z,2)
proof
consider x0,y0 being Element of REAL such that
A1: z = <*x0,y0*> by FINSEQ_2:100;
assume
A2: f is_hpartial_differentiable`22_in z;
then
A3: pdiff1(f,2) is_partial_differentiable_in z,2 by Th12;
hpartdiff22(f,z) = diff(SVF1(2,pdiff1(f,2),z),y0) by A2,A1,Th8
.= partdiff(pdiff1(f,2),z,2) by A1,A3,PDIFF_2:14;
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(1,pdiff1(f,1),z0)
holds for h be 0-convergent non-zero Real_Sequence,
c be constant Real_Sequence st
rng c = {proj(1,2).z0} & rng (h+c) c= N holds h"(#)(SVF1(1,pdiff1(f,1),z0)/*(h+
c) - SVF1(1,pdiff1(f,1),z0)/*c) is convergent & hpartdiff11(f,z0) = lim (h"(#)(
SVF1(1,pdiff1(f,1),z0)/*(h+c) - SVF1(1,pdiff1(f,1),z0)/*c))
proof
let z0 be Element of REAL 2;
let N be Neighbourhood of proj(1,2).z0;
assume that
A1: f is_hpartial_differentiable`11_in z0 and
A2: N c= dom SVF1(1,pdiff1(f,1),z0);
let h be 0-convergent non-zero Real_Sequence,
c be constant Real_Sequence such that
A3: rng c = {proj(1,2).z0} & rng (h+c) c= N;
consider x0,y0 being Element of REAL such that
A4: z0 = <*x0,y0*> by FINSEQ_2:100;
A5: pdiff1(f,1) is_partial_differentiable_in z0,1 by A1,Th9;
then partdiff(pdiff1(f,1),z0,1) = diff(SVF1(1,pdiff1(f,1),z0),x0) by A4,
PDIFF_2:13
.= hpartdiff11(f,z0) by A1,A4,Th5;
hence thesis by A2,A3,A5,PDIFF_2:17;
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 SVF1(2,pdiff1(f,1),z0)
holds for h be 0-convergent non-zero Real_Sequence,
c be constant Real_Sequence st
rng c = {proj(2,2).z0} & rng (h+c) c= N holds h"(#)(SVF1(2,pdiff1(f,1),z0)/*(h+
c) - SVF1(2,pdiff1(f,1),z0)/*c) is convergent & hpartdiff12(f,z0) = lim (h"(#)(
SVF1(2,pdiff1(f,1),z0)/*(h+c) - SVF1(2,pdiff1(f,1),z0)/*c))
proof
let z0 be Element of REAL 2;
let N be Neighbourhood of proj(2,2).z0;
assume that
A1: f is_hpartial_differentiable`12_in z0 and
A2: N c= dom SVF1(2,pdiff1(f,1),z0);
let h be 0-convergent non-zero Real_Sequence,
c be constant Real_Sequence such
that
A3: rng c = {proj(2,2).z0} & rng (h+c) c= N;
consider x0,y0 being Element of REAL such that
A4: z0 = <*x0,y0*> by FINSEQ_2:100;
A5: pdiff1(f,1) is_partial_differentiable_in z0,2 by A1,Th10;
then partdiff(pdiff1(f,1),z0,2) = diff(SVF1(2,pdiff1(f,1),z0),y0) by A4,
PDIFF_2:14
.= hpartdiff12(f,z0) by A1,A4,Th6;
hence thesis by A2,A3,A5,PDIFF_2:18;
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(1,pdiff1(f,2),z0)
holds for h be 0-convergent non-zero Real_Sequence,
c be constant Real_Sequence st
rng c = {proj(1,2).z0} & rng (h+c) c= N holds h"(#)(SVF1(1,pdiff1(f,2),z0)/*(h+
c) - SVF1(1,pdiff1(f,2),z0)/*c) is convergent & hpartdiff21(f,z0) = lim (h"(#)(
SVF1(1,pdiff1(f,2),z0)/*(h+c) - SVF1(1,pdiff1(f,2),z0)/*c))
proof
let z0 be Element of REAL 2;
let N be Neighbourhood of proj(1,2).z0;
assume that
A1: f is_hpartial_differentiable`21_in z0 and
A2: N c= dom SVF1(1,pdiff1(f,2),z0);
let h be 0-convergent non-zero Real_Sequence,
c be constant Real_Sequence such
that
A3: rng c = {proj(1,2).z0} & rng (h+c) c= N;
consider x0,y0 being Element of REAL such that
A4: z0 = <*x0,y0*> by FINSEQ_2:100;
A5: pdiff1(f,2) is_partial_differentiable_in z0,1 by A1,Th11;
then partdiff(pdiff1(f,2),z0,1) = diff(SVF1(1,pdiff1(f,2),z0),x0) by A4,
PDIFF_2:13
.= hpartdiff21(f,z0) by A1,A4,Th7;
hence thesis by A2,A3,A5,PDIFF_2:17;
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 SVF1(2,pdiff1(f,2),z0)
holds for h be 0-convergent non-zero Real_Sequence,
c be constant Real_Sequence st
rng c = {proj(2,2).z0} & rng (h+c) c= N holds h"(#)(SVF1(2,pdiff1(f,2),z0)/*(h+
c) - SVF1(2,pdiff1(f,2),z0)/*c) is convergent & hpartdiff22(f,z0) = lim (h"(#)(
SVF1(2,pdiff1(f,2),z0)/*(h+c) - SVF1(2,pdiff1(f,2),z0)/*c))
proof
let z0 be Element of REAL 2;
let N be Neighbourhood of proj(2,2).z0;
assume that
A1: f is_hpartial_differentiable`22_in z0 and
A2: N c= dom SVF1(2,pdiff1(f,2),z0);
let h be 0-convergent non-zero Real_Sequence,
c be constant Real_Sequence such that
A3: rng c = {proj(2,2).z0} & rng (h+c) c= N;
consider x0,y0 being Element of REAL such that
A4: z0 = <*x0,y0*> by FINSEQ_2:100;
A5: pdiff1(f,2) is_partial_differentiable_in z0,2 by A1,Th12;
then partdiff(pdiff1(f,2),z0,2) = diff(SVF1(2,pdiff1(f,2),z0),y0) by A4,
PDIFF_2:14
.= hpartdiff22(f,z0) by A1,A4,Th8;
hence thesis by A2,A3,A5,PDIFF_2:18;
end;
theorem
f1 is_hpartial_differentiable`11_in z0 & f2
is_hpartial_differentiable`11_in z0 implies pdiff1(f1,1)+pdiff1(f2,1)
is_partial_differentiable_in z0,1 & partdiff(pdiff1(f1,1)+pdiff1(f2,1),z0,1) =
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,1) is_partial_differentiable_in z0,1 & pdiff1(f2,1)
is_partial_differentiable_in z0,1 by A1,A2,Th9;
then
partdiff(pdiff1(f1,1)+pdiff1(f2,1),z0,1) = partdiff(pdiff1(f1,1),z0,1) +
partdiff(pdiff1(f2,1),z0,1) by PDIFF_1:29;
then
partdiff(pdiff1(f1,1)+pdiff1(f2,1),z0,1) = hpartdiff11(f1,z0) + partdiff
(pdiff1(f2,1),z0,1) by A1,Th13
.= hpartdiff11(f1,z0) + hpartdiff11(f2,z0) by A2,Th13;
hence thesis by A3,PDIFF_1:29;
end;
theorem
f1 is_hpartial_differentiable`12_in z0 & f2
is_hpartial_differentiable`12_in z0 implies pdiff1(f1,1)+pdiff1(f2,1)
is_partial_differentiable_in z0,2 & partdiff(pdiff1(f1,1)+pdiff1(f2,1),z0,2) =
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,1) is_partial_differentiable_in z0,2 & pdiff1(f2,1)
is_partial_differentiable_in z0,2 by A1,A2,Th10;
then
partdiff(pdiff1(f1,1)+pdiff1(f2,1),z0,2) = partdiff(pdiff1(f1,1),z0,2) +
partdiff(pdiff1(f2,1),z0,2) by PDIFF_1:29;
then
partdiff(pdiff1(f1,1)+pdiff1(f2,1),z0,2) = hpartdiff12(f1,z0) + partdiff
(pdiff1(f2,1),z0,2) by A1,Th14
.= hpartdiff12(f1,z0) + hpartdiff12(f2,z0) by A2,Th14;
hence thesis by A3,PDIFF_1:29;
end;
theorem
f1 is_hpartial_differentiable`21_in z0 & f2
is_hpartial_differentiable`21_in z0 implies pdiff1(f1,2)+pdiff1(f2,2)
is_partial_differentiable_in z0,1 & partdiff(pdiff1(f1,2)+pdiff1(f2,2),z0,1) =
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: pdiff1(f1,2) is_partial_differentiable_in z0,1 & pdiff1(f2,2)
is_partial_differentiable_in z0,1 by A1,A2,Th11;
then
partdiff(pdiff1(f1,2)+pdiff1(f2,2),z0,1) = partdiff(pdiff1(f1,2),z0,1) +
partdiff(pdiff1(f2,2),z0,1) by PDIFF_1:29;
then
partdiff(pdiff1(f1,2)+pdiff1(f2,2),z0,1) = hpartdiff21(f1,z0) + partdiff
(pdiff1(f2,2),z0,1) by A1,Th15
.= hpartdiff21(f1,z0) + hpartdiff21(f2,z0) by A2,Th15;
hence thesis by A3,PDIFF_1:29;
end;
theorem
f1 is_hpartial_differentiable`22_in z0 & f2
is_hpartial_differentiable`22_in z0 implies pdiff1(f1,2)+pdiff1(f2,2)
is_partial_differentiable_in z0,2 & partdiff(pdiff1(f1,2)+pdiff1(f2,2),z0,2) =
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: pdiff1(f1,2) is_partial_differentiable_in z0,2 & pdiff1(f2,2)
is_partial_differentiable_in z0,2 by A1,A2,Th12;
then
partdiff(pdiff1(f1,2)+pdiff1(f2,2),z0,2) = partdiff(pdiff1(f1,2),z0,2) +
partdiff(pdiff1(f2,2),z0,2) by PDIFF_1:29;
then
partdiff(pdiff1(f1,2)+pdiff1(f2,2),z0,2) = hpartdiff22(f1,z0) + partdiff
(pdiff1(f2,2),z0,2) by A1,Th16
.= hpartdiff22(f1,z0) + hpartdiff22(f2,z0) by A2,Th16;
hence thesis by A3,PDIFF_1:29;
end;
theorem
f1 is_hpartial_differentiable`11_in z0 & f2
is_hpartial_differentiable`11_in z0 implies pdiff1(f1,1)-pdiff1(f2,1)
is_partial_differentiable_in z0,1 & partdiff(pdiff1(f1,1)-pdiff1(f2,1),z0,1) =
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,1) is_partial_differentiable_in z0,1 & pdiff1(f2,1)
is_partial_differentiable_in z0,1 by A1,A2,Th9;
then
partdiff(pdiff1(f1,1)-pdiff1(f2,1),z0,1) = partdiff(pdiff1(f1,1),z0,1) -
partdiff(pdiff1(f2,1),z0,1) by PDIFF_1:31;
then
partdiff(pdiff1(f1,1)-pdiff1(f2,1),z0,1) = hpartdiff11(f1,z0) - partdiff
(pdiff1(f2,1),z0,1) by A1,Th13
.= hpartdiff11(f1,z0) - hpartdiff11(f2,z0) by A2,Th13;
hence thesis by A3,PDIFF_1:31;
end;
theorem
f1 is_hpartial_differentiable`12_in z0 & f2
is_hpartial_differentiable`12_in z0 implies pdiff1(f1,1)-pdiff1(f2,1)
is_partial_differentiable_in z0,2 & partdiff(pdiff1(f1,1)-pdiff1(f2,1),z0,2) =
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,1) is_partial_differentiable_in z0,2 & pdiff1(f2,1)
is_partial_differentiable_in z0,2 by A1,A2,Th10;
then
partdiff(pdiff1(f1,1)-pdiff1(f2,1),z0,2) = partdiff(pdiff1(f1,1),z0,2) -
partdiff(pdiff1(f2,1),z0,2) by PDIFF_1:31;
then
partdiff(pdiff1(f1,1)-pdiff1(f2,1),z0,2) = hpartdiff12(f1,z0) - partdiff
(pdiff1(f2,1),z0,2) by A1,Th14
.= hpartdiff12(f1,z0) - hpartdiff12(f2,z0) by A2,Th14;
hence thesis by A3,PDIFF_1:31;
end;
theorem
f1 is_hpartial_differentiable`21_in z0 & f2
is_hpartial_differentiable`21_in z0 implies pdiff1(f1,2)-pdiff1(f2,2)
is_partial_differentiable_in z0,1 & partdiff(pdiff1(f1,2)-pdiff1(f2,2),z0,1) =
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: pdiff1(f1,2) is_partial_differentiable_in z0,1 & pdiff1(f2,2)
is_partial_differentiable_in z0,1 by A1,A2,Th11;
then
partdiff(pdiff1(f1,2)-pdiff1(f2,2),z0,1) = partdiff(pdiff1(f1,2),z0,1) -
partdiff(pdiff1(f2,2),z0,1) by PDIFF_1:31;
then
partdiff(pdiff1(f1,2)-pdiff1(f2,2),z0,1) = hpartdiff21(f1,z0) - partdiff
(pdiff1(f2,2),z0,1) by A1,Th15
.= hpartdiff21(f1,z0) - hpartdiff21(f2,z0) by A2,Th15;
hence thesis by A3,PDIFF_1:31;
end;
theorem
f1 is_hpartial_differentiable`22_in z0 & f2
is_hpartial_differentiable`22_in z0 implies pdiff1(f1,2)-pdiff1(f2,2)
is_partial_differentiable_in z0,2 & partdiff(pdiff1(f1,2)-pdiff1(f2,2),z0,2) =
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: pdiff1(f1,2) is_partial_differentiable_in z0,2 & pdiff1(f2,2)
is_partial_differentiable_in z0,2 by A1,A2,Th12;
then
partdiff(pdiff1(f1,2)-pdiff1(f2,2),z0,2) = partdiff(pdiff1(f1,2),z0,2) -
partdiff(pdiff1(f2,2),z0,2) by PDIFF_1:31;
then
partdiff(pdiff1(f1,2)-pdiff1(f2,2),z0,2) = hpartdiff22(f1,z0) - partdiff
(pdiff1(f2,2),z0,2) by A1,Th16
.= hpartdiff22(f1,z0) - hpartdiff22(f2,z0) by A2,Th16;
hence thesis by A3,PDIFF_1:31;
end;
theorem
f is_hpartial_differentiable`11_in z0 implies r(#)pdiff1(f,1)
is_partial_differentiable_in z0,1 & partdiff((r(#)pdiff1(f,1)),z0,1) = r*
hpartdiff11(f,z0)
proof
assume
A1: f is_hpartial_differentiable`11_in z0;
reconsider r as Real;
A2: pdiff1(f,1) is_partial_differentiable_in z0,1 by Th9,A1;
then partdiff((r(#)pdiff1(f,1)),z0,1) = r*partdiff(pdiff1(f,1),z0,1) by
PDIFF_1:33;
hence thesis by A1,A2,Th13,PDIFF_1:33;
end;
theorem
f is_hpartial_differentiable`12_in z0 implies r(#)pdiff1(f,1)
is_partial_differentiable_in z0,2 & partdiff((r(#)pdiff1(f,1)),z0,2) = r*
hpartdiff12(f,z0)
proof
assume
A1: f is_hpartial_differentiable`12_in z0;
reconsider r as Real;
A2: pdiff1(f,1) is_partial_differentiable_in z0,2 by Th10,A1;
partdiff((r(#)pdiff1(f,1)),z0,2) = r*partdiff(pdiff1(f,1),z0,2) by
PDIFF_1:33,A2;
hence thesis by A1,A2,Th14,PDIFF_1:33;
end;
theorem
f is_hpartial_differentiable`21_in z0 implies r(#)pdiff1(f,2)
is_partial_differentiable_in z0,1 & partdiff((r(#)pdiff1(f,2)),z0,1) = r*
hpartdiff21(f,z0)
proof
assume
A1: f is_hpartial_differentiable`21_in z0;
reconsider r as Real;
A2: pdiff1(f,2) is_partial_differentiable_in z0,1 by Th11,A1;
partdiff((r(#)pdiff1(f,2)),z0,1) = r*partdiff(pdiff1(f,2),z0,1) by
PDIFF_1:33,A2;
hence thesis by A1,A2,Th15,PDIFF_1:33;
end;
theorem
f is_hpartial_differentiable`22_in z0 implies r(#)pdiff1(f,2)
is_partial_differentiable_in z0,2 & partdiff((r(#)pdiff1(f,2)),z0,2) = r*
hpartdiff22(f,z0)
proof
assume
A1: f is_hpartial_differentiable`22_in z0;
then
A2: pdiff1(f,2) is_partial_differentiable_in z0,2 by Th12;
reconsider r as Real;
partdiff((r(#)pdiff1(f,2)),z0,2) = r*partdiff(pdiff1(f,2),z0,2) by
PDIFF_1:33,A2;
hence thesis by A1,A2,Th16,PDIFF_1:33;
end;
theorem
f1 is_hpartial_differentiable`11_in z0 & f2
is_hpartial_differentiable`11_in z0 implies pdiff1(f1,1)(#)pdiff1(f2,1)
is_partial_differentiable_in z0,1
proof
assume f1 is_hpartial_differentiable`11_in z0 & f2
is_hpartial_differentiable`11_in z0;
then pdiff1(f1,1) is_partial_differentiable_in z0,1 & pdiff1(f2,1)
is_partial_differentiable_in z0,1 by Th9;
hence thesis by PDIFF_2:19;
end;
theorem
f1 is_hpartial_differentiable`12_in z0 & f2
is_hpartial_differentiable`12_in z0 implies pdiff1(f1,1)(#)pdiff1(f2,1)
is_partial_differentiable_in z0,2
proof
assume f1 is_hpartial_differentiable`12_in z0 & f2
is_hpartial_differentiable`12_in z0;
then pdiff1(f1,1) is_partial_differentiable_in z0,2 & pdiff1(f2,1)
is_partial_differentiable_in z0,2 by Th10;
hence thesis by PDIFF_2:20;
end;
theorem
f1 is_hpartial_differentiable`21_in z0 & f2
is_hpartial_differentiable`21_in z0 implies pdiff1(f1,2)(#)pdiff1(f2,2)
is_partial_differentiable_in z0,1
proof
assume f1 is_hpartial_differentiable`21_in z0 & f2
is_hpartial_differentiable`21_in z0;
then pdiff1(f1,2) is_partial_differentiable_in z0,1 & pdiff1(f2,2)
is_partial_differentiable_in z0,1 by Th11;
hence thesis by PDIFF_2:19;
end;
theorem
f1 is_hpartial_differentiable`22_in z0 & f2
is_hpartial_differentiable`22_in z0 implies pdiff1(f1,2)(#)pdiff1(f2,2)
is_partial_differentiable_in z0,2
proof
assume f1 is_hpartial_differentiable`22_in z0 & f2
is_hpartial_differentiable`22_in z0;
then pdiff1(f1,2) is_partial_differentiable_in z0,2 & pdiff1(f2,2)
is_partial_differentiable_in z0,2 by Th12;
hence thesis by PDIFF_2:20;
end;
theorem
for z0 being Element of REAL 2 holds f
is_hpartial_differentiable`11_in z0 implies SVF1(1,pdiff1(f,1),z0)
is_continuous_in proj(1,2).z0
by Th9,PDIFF_2:21;
theorem
for z0 being Element of REAL 2 holds f
is_hpartial_differentiable`12_in z0 implies SVF1(2,pdiff1(f,1),z0)
is_continuous_in proj(2,2).z0
by Th10,PDIFF_2:22;
theorem
for z0 being Element of REAL 2 holds f
is_hpartial_differentiable`21_in z0 implies SVF1(1,pdiff1(f,2),z0)
is_continuous_in proj(1,2).z0
by Th11,PDIFF_2:21;
theorem
for z0 being Element of REAL 2 holds f
is_hpartial_differentiable`22_in z0 implies SVF1(2,pdiff1(f,2),z0)
is_continuous_in proj(2,2).z0
by Th12,PDIFF_2:22;