:: Partial Differentiation of Real Binary Functions
:: by Bing Xie , Xiquan Liang , Hongwei Li and Yanping Zhuang
::
:: Received August 5, 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, RELAT_1,
CARD_3, FUNCT_1, FINSEQ_1, FINSEQ_2, PDIFF_1, RCOMP_1, TARSKI, ARYTM_1,
ARYTM_3, CARD_1, XXREAL_1, VALUED_0, SEQ_2, ORDINAL2, XXREAL_0, NAT_1,
FUNCT_2, VALUED_1, XBOOLE_0, COMPLEX1, FCONT_1, PDIFF_2, FUNCT_7;
notations TARSKI, SUBSET_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, XCMPLX_0,
XREAL_0, COMPLEX1, ORDINAL1, NUMBERS, REAL_1, NAT_1, VALUED_0, VALUED_1,
SEQ_1, SEQ_2, FINSEQ_1, FINSEQ_2, RCOMP_1, EUCLID, FDIFF_1, XXREAL_0,
FCONT_1, PDIFF_1;
constructors REAL_1, SEQ_2, COMPLEX1, RCOMP_1, FDIFF_1, FCONT_1, PDIFF_1,
RELSET_1, BINOP_2, RVSUM_1, COMSEQ_2;
registrations RELSET_1, XREAL_0, MEMBERED, FDIFF_1, FUNCT_2, NAT_1, NUMBERS,
XBOOLE_0, FINSEQ_1, VALUED_0, VALUED_1, ORDINAL1, EUCLID, SEQ_2;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI;
equalities EUCLID, RCOMP_1, PDIFF_1;
expansions TARSKI, PDIFF_1;
theorems TARSKI, XBOOLE_0, XBOOLE_1, XREAL_1, RCOMP_1, SEQ_4, SEQ_1, SEQ_2,
FINSEQ_1, FINSEQ_2, RFUNCT_2, RELAT_1, FUNCT_1, FUNCT_2, PARTFUN1,
FDIFF_1, VALUED_1, SEQM_3, RFUNCT_1, XCMPLX_0, XCMPLX_1, PDIFF_1, NAT_1,
VALUED_0, ORDINAL1, XREAL_0;
schemes SEQ_1;
begin :: Preliminaries
reserve x,x0,x1,x2,y,y0,y1,y2,r,r1,s,p,p1 for Real;
reserve z,z0 for Element of REAL 2;
reserve n,m,k for Element of NAT;
reserve Z for Subset of REAL 2;
reserve s1 for Real_Sequence;
reserve f,f1,f2 for PartFunc of REAL 2,REAL;
reserve R,R1,R2 for RestFunc;
reserve L,L1,L2 for LinearFunc;
theorem Th1:
dom proj(1,2) = REAL 2 & rng proj(1,2) = REAL & for x,y be
Real holds proj(1,2).<*x,y*> = x
proof
set f = proj(1,2);
for x be object st x in REAL ex z be object st z in REAL 2 & x = f.z
proof
set y = the Element of REAL;
let x be object;
assume x in REAL;
then reconsider x1 = x as Element of REAL;
reconsider z = <*x1,y*> as Element of REAL 2 by FINSEQ_2:101;
f.z = z.1 by PDIFF_1:def 1;
then f.z = x;
hence thesis;
end;
hence dom proj(1,2) = REAL 2 & rng proj(1,2) = REAL by FUNCT_2:10,def 1;
let x,y be Real;
reconsider x,y as Element of REAL by XREAL_0:def 1;
now
let x,y be Element of REAL;
<*x,y*> is Element of 2-tuples_on REAL by FINSEQ_2:101;
then proj(1,2).<*x,y*> = <*x,y*>.1 by PDIFF_1:def 1;
hence proj(1,2).<*x,y*> = x;
end;
then proj(1,2).<*x,y*> = x;
hence thesis;
end;
theorem Th2:
dom proj(2,2) = REAL 2 & rng proj(2,2) = REAL & for x,y be
Real holds proj(2,2).<*x,y*> = y
proof
set f = proj(2,2);
for y be object st y in REAL ex z be object st z in REAL 2 & y = f.z
proof
set x = the Element of REAL;
let y be object;
assume y in REAL;
then reconsider y1 = y as Element of REAL;
reconsider z = <*x,y1*> as Element of REAL 2 by FINSEQ_2:101;
f.z = z.2 by PDIFF_1:def 1;
then f.z = y;
hence thesis;
end;
hence dom proj(2,2) = REAL 2 & rng proj(2,2) = REAL by FUNCT_2:10,def 1;
let x,y be Real;
reconsider x,y as Element of REAL by XREAL_0:def 1;
now
let x,y be Element of REAL;
<*x,y*> is Element of 2-tuples_on REAL by FINSEQ_2:101;
then proj(2,2).<*x,y*> = <*x,y*>.2 by PDIFF_1:def 1;
hence proj(2,2).<*x,y*> = y;
end;
then proj(2,2).<*x,y*> = y;
hence thesis;
end;
begin :: Partial Differentiation of Real Binary Functions
definition
let n,i be Element of NAT;
let f be PartFunc of REAL n,REAL;
let z be Element of REAL n;
func SVF1(i,f,z) -> PartFunc of REAL,REAL equals
f*reproj(i,z);
coherence;
end;
theorem Th3:
z = <*x,y*> & f is_partial_differentiable_in z,1 implies SVF1(1,f
,z) is_differentiable_in x
by Th1;
theorem Th4:
z = <*x,y*> & f is_partial_differentiable_in z,2 implies SVF1(2,f
,z) is_differentiable_in y
by Th2;
theorem Th5:
for f be PartFunc of REAL 2,REAL for z be Element of REAL 2 holds
(ex x0,y0 being Real
st z = <*x0,y0*> & SVF1(1,f,z) is_differentiable_in x0)
iff f is_partial_differentiable_in z,1
proof
let f be PartFunc of REAL 2,REAL;
let z be Element of REAL 2;
consider x0,y0 being Element of REAL such that
A1: z = <*x0,y0*> by FINSEQ_2:100;
thus (ex x0,y0 being Real st z = <*x0,y0*> &
SVF1(1,f,z) is_differentiable_in x0) implies
f is_partial_differentiable_in z,1 by Th1;
assume
A2: f is_partial_differentiable_in z,1;
proj(1,2).z = x0 by A1,Th1;
then SVF1(1,f,z) is_differentiable_in x0 by A2;
hence thesis by A1;
end;
theorem Th6:
for f be PartFunc of REAL 2,REAL for z be Element of REAL 2 holds
(ex x0,y0 being Real
st z = <*x0,y0*> & SVF1(2,f,z) is_differentiable_in y0)
iff f is_partial_differentiable_in z,2
proof
let f be PartFunc of REAL 2,REAL;
let z be Element of REAL 2;
consider x0,y0 being Element of REAL such that
A1: z = <*x0,y0*> by FINSEQ_2:100;
thus (ex x0,y0 being Real st z = <*x0,y0*> &
SVF1(2,f,z) is_differentiable_in y0) implies
f is_partial_differentiable_in z,2 by Th2;
assume
A2: f is_partial_differentiable_in z,2;
proj(2,2).z = y0 by A1,Th2;
then SVF1(2,f,z) is_differentiable_in y0 by A2;
hence thesis by A1;
end;
theorem
z = <*x0,y0*> & f is_partial_differentiable_in z,1 implies ex N being
Neighbourhood of x0 st N c= dom SVF1(1,f,z) & ex L,R st for x st x in N holds
SVF1(1,f,z).x - SVF1(1,f,z).x0 = L.(x-x0) + R.(x-x0)
proof
assume that
A1: z = <*x0,y0*> and
A2: f is_partial_differentiable_in z,1;
ex x1,y1 st z = <*x1,y1*> & SVF1(1,f,z) is_differentiable_in x1 by A2,Th5;
then SVF1(1,f,z) is_differentiable_in x0 by A1,FINSEQ_1:77;
hence thesis by FDIFF_1:def 4;
end;
theorem
z = <*x0,y0*> & f is_partial_differentiable_in z,2 implies ex N being
Neighbourhood of y0 st N c= dom SVF1(2,f,z) & ex L,R st for y st y in N holds
SVF1(2,f,z).y - SVF1(2,f,z).y0 = L.(y-y0) + R.(y-y0)
proof
assume that
A1: z = <*x0,y0*> and
A2: f is_partial_differentiable_in z,2;
ex x1,y1 st z = <*x1,y1*> & SVF1(2,f,z) is_differentiable_in y1 by A2,Th6;
then SVF1(2,f,z) is_differentiable_in y0 by A1,FINSEQ_1:77;
hence thesis by FDIFF_1:def 4;
end;
theorem Th9:
for f be PartFunc of REAL 2,REAL for z be Element of REAL 2 holds
f is_partial_differentiable_in z,1 iff
ex x0,y0 being Real st z = <*x0,y0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(1,f,z) & ex L,R st for x st x
in N holds SVF1(1,f,z).x - SVF1(1,f,z).x0 = L.(x-x0) + R.(x-x0)
proof
let f be PartFunc of REAL 2,REAL;
let z be Element of REAL 2;
hereby
assume
A1: f is_partial_differentiable_in z,1;
thus ex x0,y0 being Real
st z = <*x0,y0*> & ex N being Neighbourhood of x0
st N c= dom SVF1(1,f,z) & ex L,R st for x st x in N holds SVF1(1,f,z).x - SVF1(
1,f,z).x0 = L.(x-x0) + R.(x-x0)
proof
consider x0,y0 such that
A2: z = <*x0,y0*> and
A3: SVF1(1,f,z) is_differentiable_in x0 by A1,Th5;
ex N being Neighbourhood of x0 st N c= dom SVF1(1,f,z) & ex L,R st
for x st x in N holds SVF1(1,f,z).x - SVF1(1,f,z).x0 = L.(x-x0) + R.(x-x0) by
A3,FDIFF_1:def 4;
hence thesis by A2;
end;
end;
given x0,y0 being Real such that
A4: z = <*x0,y0*> and
A5: ex N being Neighbourhood of
x0 st N c= dom SVF1(1,f,z) & ex L,R st for x st x in N holds SVF1(1,f,z).x -
SVF1(1,f,z).x0 = L.(x-x0) + R.(x-x0);
:: consider x0,y0 such that
:: A4: z = <*x0,y0*> and
:: A5: ex N being Neighbourhood of x0 st N c= dom SVF1(1,f,z) & ex L,R st
:: for x st x in N holds SVF1(1,f,z).x - SVF1(1,f,z).x0 = L.(x-x0) + R.(x-x0);
SVF1(1,f,z) is_differentiable_in x0 by A5,FDIFF_1:def 4;
hence thesis by A4,Th5;
end;
theorem Th10:
for f be PartFunc of REAL 2,REAL for z be Element of REAL 2
holds f is_partial_differentiable_in z,2 iff
ex x0,y0 being Real st z = <*x0,y0
*> & ex N being Neighbourhood of y0 st N c= dom SVF1(2,f,z) & ex L,R st for y
st y in N holds SVF1(2,f,z).y - SVF1(2,f,z).y0 = L.(y-y0) + R.(y-y0)
proof
let f be PartFunc of REAL 2,REAL;
let z be Element of REAL 2;
hereby
assume
A1: f is_partial_differentiable_in z,2;
thus ex x0,y0 being Real
st z = <*x0,y0*> & ex N being Neighbourhood of y0
st N c= dom SVF1(2,f,z) & ex L,R st for y st y in N holds SVF1(2,f,z).y - SVF1(
2,f,z).y0 = L.(y-y0) + R.(y-y0)
proof
consider x0,y0 such that
A2: z = <*x0,y0*> and
A3: SVF1(2,f,z) is_differentiable_in y0 by A1,Th6;
ex N being Neighbourhood of y0 st N c= dom SVF1(2,f,z) & ex L,R st
for y st y in N holds SVF1(2,f,z).y - SVF1(2,f,z).y0 = L.(y-y0) + R.(y-y0) by
A3,FDIFF_1:def 4;
hence thesis by A2;
end;
end;
:: assume ex x0,y0 being Real st z = <*x0,y0*> & ex N being Neighbourhood of
:: y0 st N c= dom SVF1(2,f,z) & ex L,R st for y st y in N holds SVF1(2,f,z).y -
:: SVF1(2,f,z).y0 = L.(y-y0) + R.(y-y0);
:: then
given x0,y0 such that
A4: z = <*x0,y0*> and
A5: ex N being Neighbourhood of y0 st N c= dom SVF1(2,f,z) & ex L,R st
for y st y in N holds SVF1(2,f,z).y - SVF1(2,f,z).y0 = L.(y-y0) + R.(y-y0);
SVF1(2,f,z) is_differentiable_in y0 by A5,FDIFF_1:def 4;
hence thesis by A4,Th6;
end;
Lm1: z = <*x0,y0*> & f is_partial_differentiable_in z,1 implies (r = diff(SVF1
(1,f,z),x0) iff
ex x0,y0 being Real
st z = <*x0,y0*> & ex N being Neighbourhood
of x0 st N c= dom SVF1(1,f,z) & ex L,R st r = L.1 & for x st x in N holds SVF1(
1,f,z).x - SVF1(1,f,z).x0 = L.(x-x0) + R.(x-x0))
proof
set F1 = SVF1(1,f,z);
assume that
A1: z = <*x0,y0*> and
A2: f is_partial_differentiable_in z,1;
A3: F1 is_differentiable_in x0 by A1,A2,Th3;
hereby
assume
A4: r = diff(F1,x0);
F1 is_differentiable_in x0 by A1,A2,Th3;
then
ex N being Neighbourhood of x0 st N c= dom F1 & ex L,R st r=L.1 & for x
st x in N holds F1.x-F1.x0 = L.(x-x0) + R.(x -x0) by A4,FDIFF_1:def 5;
hence
ex x0,y0 being Real
st z = <*x0,y0*> & ex N being Neighbourhood of x0
st N c= dom SVF1(1,f,z) & ex L,R st r = L.1 & for x st x in N holds SVF1(1,f,z)
.x - SVF1(1,f,z).x0 = L.(x-x0) + R.(x-x0) by A1;
end;
given x1,y1 being Real such that
A5: z = <*x1,y1*> and
A6: ex N being Neighbourhood of x1 st N c= dom SVF1(1,f,z) & ex L,R st r
= L.1 & for x st x in N holds SVF1(1,f,z).x - SVF1(1,f,z).x1 = L.(x-x1) + R.(x-
x1);
x1 = x0 by A1,A5,FINSEQ_1:77;
hence thesis by A6,A3,FDIFF_1:def 5;
end;
Lm2: z = <*x0,y0*> & f is_partial_differentiable_in z,2 implies (r = diff(SVF1
(2,f,z),y0) iff
ex x0,y0 being Real st z = <*x0,y0*> & ex N being Neighbourhood
of y0 st N c= dom SVF1(2,f,z) & ex L,R st r = L.1 & for y st y in N holds SVF1(
2,f,z).y - SVF1(2,f,z).y0 = L.(y-y0) + R.(y-y0))
proof
set F1 = SVF1(2,f,z);
assume that
A1: z = <*x0,y0*> and
A2: f is_partial_differentiable_in z,2;
A3: F1 is_differentiable_in y0 by A1,A2,Th4;
hereby
assume
A4: r = diff(F1,y0);
F1 is_differentiable_in y0 by A1,A2,Th4;
then
ex N being Neighbourhood of y0 st N c= dom F1 & ex L,R st r=L.1 & for y
st y in N holds F1.y-F1.y0 = L.(y-y0) + R.(y -y0) by A4,FDIFF_1:def 5;
hence
ex x0,y0 being Real
st z = <*x0,y0*> & ex N being Neighbourhood of y0
st N c= dom F1 & ex L,R st r = L.1 & for y st y in N holds SVF1(2,f,z).y - SVF1
(2,f,z).y0 = L.(y-y0) + R.(y-y0) by A1;
end;
given x1,y1 being Real such that
A5: z = <*x1,y1*> and
A6: ex N being Neighbourhood of y1 st N c= dom F1 & ex L,R st r = L.1 &
for y st y in N holds F1.y - F1.y1 = L.(y-y1) + R.(y-y1);
y1 = y0 by A1,A5,FINSEQ_1:77;
hence thesis by A6,A3,FDIFF_1:def 5;
end;
theorem Th11:
z = <*x0,y0*> & f is_partial_differentiable_in z,1 implies (r =
partdiff(f,z,1) iff
ex x0,y0 being Real st z = <*x0,y0*> & ex N being
Neighbourhood of x0 st N c= dom SVF1(1,f,z) & ex L,R st r = L.1 & for x st x in
N holds SVF1(1,f,z).x - SVF1(1,f,z).x0 = L.(x-x0) + R.(x-x0))
proof
assume that
A1: z = <*x0,y0*> and
A2: f is_partial_differentiable_in z,1;
hereby
assume r = partdiff(f,z,1);
then r = diff(SVF1(1,f,z),x0) by A1,Th1;
hence
ex x0,y0 being Real st z = <*x0,y0*> &
ex N being Neighbourhood of x0
st N c= dom SVF1(1,f,z) & ex L,R st r = L.1 & for x st x in N holds SVF1(1,f,z)
.x - SVF1(1,f,z).x0 = L.(x-x0) + R.(x-x0) by A1,A2,Lm1;
end;
given x1,y1 being Real such that
A3: z = <*x1,y1*> & ex N being Neighbourhood of x1 st N c= dom SVF1(1,f,
z) & ex L,R st r = L.1 & for x st x in N holds SVF1(1,f,z).x - SVF1(1,f,z).x1 =
L.(x-x1 ) + R.(x- x1);
r = diff(SVF1(1,f,z),x0) by A1,A2,A3,Lm1;
hence thesis by A1,Th1;
end;
theorem Th12:
z = <*x0,y0*> & f is_partial_differentiable_in z,2 implies (r =
partdiff(f,z,2) iff
ex x0,y0 being Real st z = <*x0,y0*> & ex N being
Neighbourhood of y0 st N c= dom SVF1(2,f,z) & ex L,R st r = L.1 & for y st y in
N holds SVF1(2,f,z).y - SVF1(2,f,z).y0 = L.(y-y0) + R.(y-y0))
proof
assume that
A1: z = <*x0,y0*> and
A2: f is_partial_differentiable_in z,2;
hereby
assume r = partdiff(f,z,2);
then r = diff(SVF1(2,f,z),y0) by A1,Th2;
hence
ex x0,y0 being Real
st z = <*x0,y0*> & ex N being Neighbourhood of y0
st N c= dom SVF1(2,f,z) & ex L,R st r = L.1 & for y st y in N holds SVF1(2,f,z)
.y - SVF1(2,f,z).y0 = L.(y-y0) + R.(y-y0) by A1,A2,Lm2;
end;
given x1,y1 being Real such that
A3: z = <*x1,y1*> & ex N being Neighbourhood of y1 st N c= dom SVF1(2,f,
z) & ex L,R st r = L.1 & for y st y in N holds SVF1(2,f,z).y - SVF1(2,f,z).y1 =
L.(y-y1 ) + R.(y- y1);
r = diff(SVF1(2,f,z),y0) by A1,A2,A3,Lm2;
hence thesis by A1,Th2;
end;
theorem
z = <*x0,y0*> & f is_partial_differentiable_in z,1 implies partdiff(f,
z,1) = diff(SVF1(1,f,z),x0)
proof
set r = partdiff(f,z,1);
assume that
A1: z = <*x0,y0*> and
A2: f is_partial_differentiable_in z,1;
consider x1,y1 being Real such that
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of x1 st N c= dom SVF1(1,f,z) & ex L,R st r
= L.1 & for x st x in N holds SVF1(1,f,z).x - SVF1(1,f,z).x1 = L.(x-x1) + R.(x-
x1) by A1,A2,Th11;
x0 = x1 by A1,A3,FINSEQ_1:77;
then consider N being Neighbourhood of x0 such that
N c= dom SVF1(1,f,z) and
A5: ex L,R st r = L.1 & for x st x in N holds SVF1(1,f,z).x - SVF1(1,f,z
).x0 = L.(x-x0) + R.(x-x0) by A4;
consider L,R such that
A6: r = L.1 and
A7: for x st x in N holds SVF1(1,f,z).x - SVF1(1,f,z).x0 = L.(x-x0) + R.
(x-x0) by A5;
consider r1 such that
A8: for p holds L.p = r1*p by FDIFF_1:def 3;
A9: r = r1*1 by A6,A8;
consider x2,y2 such that
A10: z = <*x2,y2*> and
A11: SVF1(1,f,z) is_differentiable_in x2 by A2,Th5;
consider N1 being Neighbourhood of x2 such that
N1 c= dom SVF1(1,f,z) and
A12: ex L,R st diff(SVF1(1,f,z),x2) = L.1 & for x st x in N1 holds SVF1(
1 ,f,z).x - SVF1(1,f,z).x2 = L.(x-x2) + R.(x-x2) by A11,FDIFF_1:def 5;
consider L1,R1 such that
A13: diff(SVF1(1,f,z),x2) = L1.1 and
A14: for x st x in N1 holds SVF1(1,f,z).x - SVF1(1,f,z).x2 = L1.(x-x2) +
R1.(x-x2) by A12;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
A16: x0 = x2 by A1,A10,FINSEQ_1:77;
then consider N0 be Neighbourhood of x0 such that
A17: N0 c= N & N0 c= N1 by RCOMP_1:17;
consider g be Real such that
A18: 0 < g and
A19: N0 = ].x0-g,x0+g.[ by RCOMP_1:def 6;
deffunc F(Nat) = g/($1+2);
consider s1 such that
A20: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
now
let n be Nat;
g/(n+2) <> 0 by A18,XREAL_1:139;
hence s1.n <> 0 by A20;
end;
then
A21: s1 is non-zero by SEQ_1:5;
s1 is convergent & lim s1 = 0 by A20,SEQ_4:31;
then reconsider h = s1 as 0-convergent non-zero Real_Sequence
by A21,FDIFF_1:def 1;
A22: 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 A18,XREAL_1:76;
then
A23: x0+g/(n+2) < x0+g by XREAL_1:6;
g/(n+2) > 0 by A18,XREAL_1:139;
then x0+-g < x0+g/(n+2) by A18,XREAL_1:6;
then x0+g/(n+2) in ].x0-g,x0+g.[ by A23;
hence thesis by A17,A19,A20;
end;
A24: diff(SVF1(1,f,z),x2) = p1*1 by A13,A15;
A25: now
let x;
assume that
A26: x in N and
A27: x in N1;
SVF1(1,f,z).x - SVF1(1,f,z).x0 = L.(x-x0) + R.(x-x0) by A7,A26;
then L.(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A14,A16,A27;
then r1*(x-x0) + R.(x-x0) = L1.(x-x0) + R1.(x-x0) by A8;
hence
r*(x-x0) + R.(x-x0) = diff(SVF1(1,f,z),x2)*(x-x0) + R1.(x-x0) by A15,A9,A24
;
end;
reconsider rd = r - diff(SVF1(1,f,z),x2) as Element of REAL by XREAL_0:def 1;
now
R1 is total by FDIFF_1:def 2;
then dom R1 = REAL by PARTFUN1:def 2;
then
A28: rng h c= dom R1;
let n be Nat;
R is total by FDIFF_1:def 2;
then dom R = REAL by PARTFUN1:def 2;
then
A29: rng h c= dom R;
A30: n in NAT by ORDINAL1:def 12;
then ex x st x in N & x in N1 & h.n = x-x0 by A22;
then r*(h.n) + R.(h.n) = diff(SVF1(1,f,z),x2)*(h.n) + R1.(h.n) by A25;
then
A31: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (diff(SVF1(1,f,z),x2)*(h.n) + R1.
(h.n))/(h.n) by XCMPLX_1:62;
A32: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R.(h.n))*(h".n) by VALUED_1:10
.= ((R/*h).n)*(h".n) by A30,A29,FUNCT_2:108
.= ((h")(#)(R/*h)).n by SEQ_1:8;
A33: h.n <> 0 by SEQ_1:5;
A34: (R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R1.(h.n))*(h".n) by VALUED_1:10
.= ((R1/*h).n)*(h".n) by A30,A28,FUNCT_2:108
.= ((h")(#)(R1/*h)).n by SEQ_1:8;
A35: (diff(SVF1(1,f,z),x2)*(h.n))/(h.n) = diff(SVF1(1,f,z),x2)*((h.n)/(h.n
)) by XCMPLX_1:74
.= diff(SVF1(1,f,z),x2)*1 by A33,XCMPLX_1:60
.= diff(SVF1(1,f,z),x2);
(r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
.= r*1 by A33,XCMPLX_1:60
.= r;
then
r + (R.(h.n))/(h.n) = diff(SVF1(1,f,z),x2) + (R1.(h.n))/(h.n) by A31,A35,
XCMPLX_1:62;
then r = diff(SVF1(1,f,z),x2) + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n)
by A32,A34;
hence rd = (((h")(#)(R1/*h))-((h")(#)(R/*h))).n by
RFUNCT_2:1;
end;
then ((h")(#)(R1/*h))-((h")(#)(R/*h)) is constant & (((h")(#)(R1/*h))-((h")
(#)(R /*h))).1 = r-diff(SVF1(1,f,z),x2) by VALUED_0:def 18;
then
A36: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-diff(SVF1(1,f,z),x2) by
SEQ_4:25;
A37: (h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
(h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
then r-diff(SVF1(1,f,z),x2) = 0-0 by A36,A37,SEQ_2:12;
hence thesis by A1,A10,FINSEQ_1:77;
end;
theorem
z = <*x0,y0*> & f is_partial_differentiable_in z,2 implies partdiff(f,
z,2) = diff(SVF1(2,f,z),y0)
proof
set r = partdiff(f,z,2);
assume that
A1: z = <*x0,y0*> and
A2: f is_partial_differentiable_in z,2;
consider x1,y1 being Real such that
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of y1 st N c= dom SVF1(2,f,z) & ex L,R st r
= L.1 & for y st y in N holds SVF1(2,f,z).y - SVF1(2,f,z).y1 = L.(y-y1) + R.(y-
y1) by A1,A2,Th12;
y0 = y1 by A1,A3,FINSEQ_1:77;
then consider N being Neighbourhood of y0 such that
N c= dom SVF1(2,f,z) and
A5: ex L,R st r = L.1 & for y st y in N holds SVF1(2,f,z).y - SVF1(2,f,z
).y0 = L.(y-y0) + R.(y-y0) by A4;
consider L,R such that
A6: r = L.1 and
A7: for y st y in N holds SVF1(2,f,z).y - SVF1(2,f,z).y0 = L.(y-y0) + R.
(y-y0) by A5;
consider r1 such that
A8: for p holds L.p = r1*p by FDIFF_1:def 3;
A9: r = r1*1 by A6,A8;
consider x2,y2 such that
A10: z = <*x2,y2*> and
A11: SVF1(2,f,z) is_differentiable_in y2 by A2,Th6;
consider N1 being Neighbourhood of y2 such that
N1 c= dom SVF1(2,f,z) and
A12: ex L,R st diff(SVF1(2,f,z),y2) = L.1 & for y st y in N1 holds SVF1(
2 ,f,z).y - SVF1(2,f,z).y2 = L.(y-y2) + R.(y-y2) by A11,FDIFF_1:def 5;
consider L1,R1 such that
A13: diff(SVF1(2,f,z),y2) = L1.1 and
A14: for y st y in N1 holds SVF1(2,f,z).y - SVF1(2,f,z).y2 = L1.(y-y2) +
R1.(y-y2) by A12;
consider p1 such that
A15: for p holds L1.p = p1*p by FDIFF_1:def 3;
A16: y0 = y2 by A1,A10,FINSEQ_1:77;
then consider N0 be Neighbourhood of y0 such that
A17: N0 c= N & N0 c= N1 by RCOMP_1:17;
consider g be Real such that
A18: 0 < g and
A19: N0 = ].y0-g,y0+g.[ by RCOMP_1:def 6;
deffunc F(Nat) = g/($1+2);
consider s1 such that
A20: for n being Nat holds s1.n = F(n) from SEQ_1:sch 1;
now
let n be Nat;
g/(n+2) <> 0 by A18,XREAL_1:139;
hence s1.n <> 0 by A20;
end;
then
A21: s1 is non-zero by SEQ_1:5;
s1 is convergent & lim s1 = 0 by A20,SEQ_4:31;
then reconsider h = s1 as 0-convergent non-zero Real_Sequence
by A21,FDIFF_1:def 1;
A22: 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 A18,XREAL_1:76;
then
A23: y0+g/(n+2) < y0+g by XREAL_1:6;
g/(n+2) > 0 by A18,XREAL_1:139;
then y0+-g < y0+g/(n+2) by A18,XREAL_1:6;
then y0+g/(n+2) in ].y0-g,y0+g.[ by A23;
hence thesis by A17,A19,A20;
end;
A24: diff(SVF1(2,f,z),y2) = p1*1 by A13,A15;
A25: now
let y;
assume that
A26: y in N and
A27: y in N1;
SVF1(2,f,z).y - SVF1(2,f,z).y0 = L.(y-y0) + R.(y-y0) by A7,A26;
then L.(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A14,A16,A27;
then r1*(y-y0) + R.(y-y0) = L1.(y-y0) + R1.(y-y0) by A8;
hence
r*(y-y0) + R.(y-y0) = diff(SVF1(2,f,z),y2)*(y-y0) + R1.(y-y0) by A15,A9,A24
;
end;
reconsider rd = r - diff(SVF1(2,f,z),y2) as Element of REAL by XREAL_0:def 1;
now
R1 is total by FDIFF_1:def 2;
then dom R1 = REAL by PARTFUN1:def 2;
then
A28: rng h c= dom R1;
let n be Nat;
R is total by FDIFF_1:def 2;
then dom R = REAL by PARTFUN1:def 2;
then
A29: rng h c= dom R;
A30: n in NAT by ORDINAL1:def 12;
then ex y st y in N & y in N1 & h.n = y-y0 by A22;
then r*(h.n) + R.(h.n) = diff(SVF1(2,f,z),y2)*(h.n) + R1.(h.n) by A25;
then
A31: (r*(h.n))/(h.n) + (R.(h.n))/(h.n) = (diff(SVF1(2,f,z),y2)*(h.n) + R1.
(h.n))/(h.n) by XCMPLX_1:62;
A32: (R.(h.n))/(h.n) = (R.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R.(h.n))*(h".n) by VALUED_1:10
.= ((R/*h).n)*(h".n) by A30,A29,FUNCT_2:108
.= ((h")(#)(R/*h)).n by SEQ_1:8;
A33: h.n <> 0 by SEQ_1:5;
A34: (R1.(h.n))/(h.n) = (R1.(h.n))*(h.n)" by XCMPLX_0:def 9
.= (R1.(h.n))*(h".n) by VALUED_1:10
.= ((R1/*h).n)*(h".n) by A30,A28,FUNCT_2:108
.= ((h")(#)(R1/*h)).n by SEQ_1:8;
A35: (diff(SVF1(2,f,z),y2)*(h.n))/(h.n) = diff(SVF1(2,f,z),y2)*((h.n)/(h.n
)) by XCMPLX_1:74
.= diff(SVF1(2,f,z),y2)*1 by A33,XCMPLX_1:60
.= diff(SVF1(2,f,z),y2);
(r*(h.n))/(h.n) = r*((h.n)/(h.n)) by XCMPLX_1:74
.= r*1 by A33,XCMPLX_1:60
.= r;
then
r + (R.(h.n))/(h.n) = diff(SVF1(2,f,z),y2) + (R1.(h.n))/(h.n) by A31,A35,
XCMPLX_1:62;
then r = diff(SVF1(2,f,z),y2) + (((h")(#)(R1/*h)).n - ((h")(#)(R/*h)).n)
by A32,A34;
hence rd = (((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-diff(SVF1(2,f,z),y2) by VALUED_0:def 18;
then
A36: lim (((h")(#)(R1/*h))-((h")(#)(R/*h))) = r-diff(SVF1(2,f,z),y2) by
SEQ_4:25;
A37: (h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by FDIFF_1:def 2;
(h")(#)(R/*h) is convergent & lim ((h")(#)(R/*h)) = 0 by FDIFF_1:def 2;
then r-diff(SVF1(2,f,z),y2) = 0-0 by A36,A37,SEQ_2:12;
hence thesis by A1,A10,FINSEQ_1:77;
end;
definition
let f be PartFunc of REAL 2,REAL;
let Z be set;
pred f is_partial_differentiable`1_on Z means
Z c= dom f & for z be
Element of REAL 2 st z in Z holds f|Z is_partial_differentiable_in z,1;
pred f is_partial_differentiable`2_on Z means
Z c= dom f & for z be
Element of REAL 2 st z in Z holds f|Z is_partial_differentiable_in z,2;
end;
theorem
f is_partial_differentiable`1_on Z implies Z c= dom f & for z st z in
Z holds f is_partial_differentiable_in z,1
proof
set g = f|Z;
assume
A1: f is_partial_differentiable`1_on Z;
hence Z c= dom f;
let z0 be Element of REAL 2;
assume z0 in Z;
then g is_partial_differentiable_in z0,1 by A1;
then consider x0,y0 being Real such that
A2: z0 = <*x0,y0*> and
A3: ex N being Neighbourhood of x0 st N c= dom SVF1(1,g,z0) & ex L,R st
for x st x in N holds SVF1(1,g,z0).x - SVF1(1,g,z0).x0 = L.(x-x0) + R.(x-x0)
by Th9;
consider N being Neighbourhood of x0 such that
A4: N c= dom SVF1(1,g,z0) and
A5: ex L,R st for x st x in N holds SVF1(1,g,z0).x - SVF1(1,g,z0).x0 = L
.(x-x0) + R.(x-x0) by A3;
consider L,R such that
A6: for x st x in N holds SVF1(1,g,z0).x - SVF1(1,g,z0).x0 = L.(x-x0) +
R.(x-x0) by A5;
A7: for x st x in N holds SVF1(1,f,z0).x - SVF1(1,f,z0).x0 = L.(x-x0) + R.(
x-x0)
proof
let x;
A8: for x st x in dom (SVF1(1,g,z0)) holds SVF1(1,g,z0).x = SVF1(1,f,z0). x
proof
let x;
assume
A9: x in dom (SVF1(1,g,z0));
then
A10: x in dom reproj(1,z0) by FUNCT_1:11;
A11: reproj(1,z0).x in dom (f|Z) by A9,FUNCT_1:11;
SVF1(1,g,z0).x = (f|Z).(reproj(1,z0).x) by A9,FUNCT_1:12
.= f.(reproj(1,z0).x) by A11,FUNCT_1:47
.= SVF1(1,f,z0).x by A10,FUNCT_1:13;
hence thesis;
end;
A12: x0 in N by RCOMP_1:16;
assume
A13: x in N;
then L.(x-x0) + R.(x-x0) = SVF1(1,g,z0).x - SVF1(1,g,z0).x0 by A6
.= SVF1(1,f,z0).x - SVF1(1,g,z0).x0 by A4,A13,A8
.= SVF1(1,f,z0).x - SVF1(1,f,z0).x0 by A4,A8,A12;
hence thesis;
end;
for x st x in dom SVF1(1,g,z0) holds x in dom SVF1(1,f,z0)
proof
let x;
dom (f|Z) = dom f /\ Z by RELAT_1:61;
then
A14: dom (f|Z) c= dom f by XBOOLE_1:17;
assume x in dom SVF1(1,g,z0);
then x in dom reproj(1,z0) & reproj(1,z0).x in dom (f|Z) by FUNCT_1:11;
hence thesis by A14,FUNCT_1:11;
end;
then for x be object st x in dom SVF1(1,g,z0) holds x in dom SVF1(1,f,z0);
then dom SVF1(1,g,z0) c= dom SVF1(1,f,z0);
then N c= dom SVF1(1,f,z0) by A4;
hence thesis by A2,A7,Th9;
end;
theorem
f is_partial_differentiable`2_on Z implies Z c= dom f & for z st z in
Z holds f is_partial_differentiable_in z,2
proof
set g = f|Z;
assume
A1: f is_partial_differentiable`2_on Z;
hence Z c= dom f;
let z0 be Element of REAL 2;
assume z0 in Z;
then g is_partial_differentiable_in z0,2 by A1;
then consider x0,y0 being Real such that
A2: z0 = <*x0,y0*> and
A3: ex N being Neighbourhood of y0 st N c= dom SVF1(2,g,z0) & ex L,R st
for y st y in N holds SVF1(2,g,z0).y - SVF1(2,g,z0).y0 = L.(y-y0) + R.(y-y0)
by Th10;
consider N being Neighbourhood of y0 such that
A4: N c= dom SVF1(2,g,z0) and
A5: ex L,R st for y st y in N holds SVF1(2,g,z0).y - SVF1(2,g,z0).y0 = L
.(y-y0) + R.(y-y0) by A3;
consider L,R such that
A6: for y st y in N holds SVF1(2,g,z0).y - SVF1(2,g,z0).y0 = L.(y-y0) +
R.(y-y0) by A5;
A7: for y st y in N holds SVF1(2,f,z0).y - SVF1(2,f,z0).y0 = L.(y-y0) + R.(
y-y0)
proof
let y;
A8: for y st y in dom SVF1(2,g,z0) holds SVF1(2,g,z0).y = SVF1(2,f,z0).y
proof
let y;
assume
A9: y in dom (SVF1(2,g,z0));
then
A10: y in dom reproj(2,z0) by FUNCT_1:11;
A11: reproj(2,z0).y in dom (f|Z) by A9,FUNCT_1:11;
SVF1(2,g,z0).y = (f|Z).(reproj(2,z0).y) by A9,FUNCT_1:12
.= f.(reproj(2,z0).y) by A11,FUNCT_1:47
.= SVF1(2,f,z0).y by A10,FUNCT_1:13;
hence thesis;
end;
A12: y0 in N by RCOMP_1:16;
assume
A13: y in N;
then L.(y-y0) + R.(y-y0) = SVF1(2,g,z0).y - SVF1(2,g,z0).y0 by A6
.= SVF1(2,f,z0).y - SVF1(2,g,z0).y0 by A4,A13,A8
.= SVF1(2,f,z0).y - SVF1(2,f,z0).y0 by A4,A8,A12;
hence thesis;
end;
for y st y in dom (SVF1(2,g,z0)) holds y in dom (SVF1(2,f,z0))
proof
let y;
dom (f|Z) = dom f /\ Z by RELAT_1:61;
then
A14: dom (f|Z) c= dom f by XBOOLE_1:17;
assume y in dom (SVF1(2,g,z0));
then y in dom reproj(2,z0) & reproj(2,z0).y in dom (f|Z) by FUNCT_1:11;
hence thesis by A14,FUNCT_1:11;
end;
then for y be object st y in dom (SVF1(2,g,z0))
holds y in dom (SVF1(2,f,z0));
then dom (SVF1(2,g,z0)) c= dom (SVF1(2,f,z0));
then N c= dom (SVF1(2,f,z0)) by A4;
hence thesis by A2,A7,Th10;
end;
definition
let f be PartFunc of REAL 2,REAL;
let Z be set;
assume
A1: f is_partial_differentiable`1_on Z;
func f`partial1|Z -> PartFunc of REAL 2,REAL means
dom it = Z & for z be
Element of REAL 2 st z in Z holds it.z = partdiff(f,z,1);
existence
proof
deffunc F(Element of REAL 2) = In(partdiff(f,$1,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;
for y be object st y in dom F holds y in Z by A2;
then dom F c= Z;
hence dom F = Z by A4,XBOOLE_0:def 10;
let z be Element of REAL 2;
assume z in Z;
then z in dom F by A2;
then F.z = F(z) by A2;
hence thesis;
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 = partdiff(f,z,1) and
A7: dom G = Z and
A8: for z be Element of REAL 2 st z in Z holds G.z = partdiff(f,z,1);
now
let z be Element of REAL 2;
assume
A9: z in dom F;
then F.z = partdiff(f,z,1) 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_partial_differentiable`2_on Z;
func f`partial2|Z -> PartFunc of REAL 2,REAL means
dom it = Z & for z be
Element of REAL 2 st z in Z holds it.z = partdiff(f,z,2);
existence
proof
deffunc F(Element of REAL 2) = In(partdiff(f,$1,2),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;
for y be object st y in dom F holds y in Z by A2;
then dom F c= Z;
hence dom F = Z by A4,XBOOLE_0:def 10;
let z be Element of REAL 2;
assume z in Z;
then z in dom F by A2;
then F.z = F(z) by A2;
hence thesis;
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 = partdiff(f,z,2) and
A7: dom G = Z and
A8: for z be Element of REAL 2 st z in Z holds G.z = partdiff(f,z,2);
now
let z be Element of REAL 2;
assume
A9: z in dom F;
then F.z = partdiff(f,z,2) 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 Partial Differentiation of Real Binary Functions
theorem
for z0 being Element of REAL 2 for N being Neighbourhood of proj(1,2).
z0 st f is_partial_differentiable_in z0,1 & N c= dom SVF1(1,f,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,f,z0)/*(h+c) - SVF1(1,f,z0)/*c) is
convergent & partdiff(f,z0,1) = lim (h"(#)(SVF1(1,f,z0)/*(h+c) - SVF1(1,f,z0)/*
c))
proof
let z0 be Element of REAL 2;
let N be Neighbourhood of proj(1,2).z0;
assume that
A1: f is_partial_differentiable_in z0,1 and
A2: N c= dom SVF1(1,f,z0);
consider x0,y0 being Real such that
A3: z0 = <*x0,y0*> and
A4: ex N1 being Neighbourhood of x0 st N1 c= dom SVF1(1,f,z0) & ex L,R
st for x st x in N1 holds SVF1(1,f,z0).x - SVF1(1,f,z0).x0 = L.(x-x0) + R.(x-x0
) by A1,Th9;
consider N1 be Neighbourhood of x0 such that
N1 c= dom SVF1(1,f,z0) and
A5: ex L,R st for x st x in N1 holds SVF1(1,f,z0).x - SVF1(1,f,z0).x0 =
L.(x-x0) + R.(x-x0) by A4;
A6: proj(1,2).z0 = x0 by A3,Th1;
then consider N2 be Neighbourhood of x0 such that
A7: N2 c= N and
A8: N2 c= N1 by RCOMP_1:17;
A9: N2 c= dom SVF1(1,f,z0) by A2,A7;
let h be 0-convergent non-zero Real_Sequence,
c be constant Real_Sequence such
that
A10: rng c = {proj(1,2).z0} and
A11: rng (h+c) c= N;
consider g be Real such that
A12: 0 < g and
A13: N2 = ].x0-g,x0+g.[ by RCOMP_1:def 6;
x0 + 0 < x0 + g & x0 - g < x0 - 0 by A12,XREAL_1:8,44;
then
A14: x0 in N2 by A13;
A15: rng c c= dom SVF1(1,f,z0)
proof
let y be object;
assume y in rng c;
then y = x0 by A10,A6,TARSKI:def 1;
then y in N by A7,A14;
hence thesis by A2;
end;
ex n st rng (c^\n) c= N2 & rng ((h+c)^\n) c= N2
proof
x0 in rng c by A10,A6,TARSKI:def 1;
then
A16: lim c = x0 by SEQ_4:25;
lim h = 0;
then lim (h+c) = 0+x0 by A16,SEQ_2:6
.= x0;
then consider n being Nat such that
A17: for m being Nat st n <= m holds |.(h+c).m-x0.| < g by A12,
SEQ_2:def 7;
reconsider n as Element of NAT by ORDINAL1:def 12;
take n;
A18: rng (c^\n) = {x0} by A10,A6,VALUED_0:26;
thus rng (c^\n) c= N2
by A14,A18,TARSKI:def 1;
let y be object;
assume y in rng ((h+c)^\n);
then consider m such that
A19: y = ((h+c)^\n).m by FUNCT_2:113;
n + 0 <= n+m by XREAL_1:7;
then
A20: |.(h+c).(n+m)-x0.|<g by A17;
then (h+c).(m+n) - x0 < g by SEQ_2:1;
then ((h+c)^\n).m - x0 < g by NAT_1:def 3;
then
A21: ((h+c)^\n).m < x0 + g by XREAL_1:19;
-g < (h+c).(m+n) - x0 by A20,SEQ_2:1;
then -g < ((h+c)^\n).m - x0 by NAT_1:def 3;
then x0 +-g < ((h+c)^\n).m by XREAL_1:20;
hence thesis by A13,A19,A21;
end;
then consider n such that
rng (c^\n) c= N2 and
A22: rng ((h+c)^\n) c= N2;
consider L,R such that
A23: for x st x in N1 holds SVF1(1,f,z0).x - SVF1(1,f,z0).x0 = L.(x-x0) +
R.(x-x0) by A5;
A24: rng (c^\n) c= dom SVF1(1,f,z0)
proof
let y be object;
assume
A25: y in rng (c^\n);
rng (c^\n) = rng c by VALUED_0:26;
then y = x0 by A10,A6,A25,TARSKI:def 1;
then y in N by A7,A14;
hence thesis by A2;
end;
A26: L is total by FDIFF_1:def 3;
A27: (L/*(h^\n) + R/*(h^\n))(#)(h^\n)" is convergent & lim ((L/*(h^\n) + R/*
(h^\n))(#)(h^\n)") = L.1
proof
deffunc F(Nat) = L.1 + ((R/*(h^\n))(#)(h^\n)").$1;
consider s1 such that
A28: for k being Nat holds s1.k = F(k) from SEQ_1:sch 1;
A29: now
A30: ((h^\n)")(#)(R/*(h^\n)) is convergent & lim (((h^\n)")(#)(R/*(h^\n)
)) = 0 by FDIFF_1:def 2;
let r be Real;
assume 0 < r;
then consider m being Nat such that
A31: for k being Nat st m <= k holds |.(((h^\n)")(#)(R/*(h^\n))).k-0.| < r
by A30,
SEQ_2:def 7;
take n1 = m;
let k be Nat such that
A32: n1 <= k;
|.s1.k-L.1.| = |.L.1+((R/*(h^\n))(#)(h^\n)").k-L.1 .| by A28
.= |.(((h^\n)")(#)(R/*(h^\n))).k-0 .|;
hence |.s1.k-L.1.| < r by A31,A32;
end;
consider s such that
A33: for p1 holds L.p1 = s*p1 by FDIFF_1:def 3;
A34: L.1 = s*1 by A33
.= s;
now
let m;
A35: (h^\n).m <> 0 by SEQ_1:5;
thus ((L/*(h^\n) + R/*(h^\n))(#)(h^\n)").m = ((L/*(h^\n) + R/*(h^\n)).m)
*((h^\n)").m by SEQ_1:8
.= ((L/*(h^\n)).m + (R/*(h^\n)).m) * ((h^\n)").m by SEQ_1:7
.= ((L/*(h^\n)).m)*((h^\n)").m + ((R/*(h^\n)).m)*((h^\n)").m
.= ((L/*(h^\n)).m)*((h^\n)").m + ((R/*(h^\n))(#)(h^\n)").m by SEQ_1:8
.= ((L/*(h^\n)).m)*((h^\n).m)" + ((R/*(h^\n))(#)(h^\n)").m by
VALUED_1:10
.= (L.((h^\n).m))*((h^\n).m)" + ((R/*(h^\n))(#)(h^\n)").m by A26,
FUNCT_2:115
.= (s*((h^\n).m))*((h^\n).m)" + ((R/*(h^\n))(#)(h^\n)").m by A33
.= s*(((h^\n).m)*((h^\n).m)") + ((R/*(h^\n))(#)(h^\n)").m
.= s*1 + ((R/*(h^\n))(#)(h^\n)").m by A35,XCMPLX_0:def 7
.= s1.m by A28,A34;
end;
then
A36: (L/*(h^\n) + R/*(h^\n))(#)(h^\n)" = s1 by FUNCT_2:63;
hence (L/*(h^\n)+R/*(h^\n))(#)(h^\n)" is convergent by A29,SEQ_2:def 6;
hence thesis by A36,A29,SEQ_2:def 7;
end;
A37: rng ((h+c)^\n) c= dom SVF1(1,f,z0)
by A22,A7,A2;
A38: rng (h+c) c= dom SVF1(1,f,z0)
by A11,A2;
A39: for k holds SVF1(1,f,z0).(((h+c)^\n).k) - SVF1(1,f,z0).((c^\n).k) = L.(
(h^\n).k) + R.((h^\n).k)
proof
let k;
((h+c)^\n).k in rng ((h+c)^\n) by VALUED_0:28;
then
A40: ((h+c)^\n).k in N2 by A22;
(c^\n).k in rng (c^\n) & rng (c^\n) = rng c by VALUED_0:26,28;
then
A41: (c^\n).k = x0 by A10,A6,TARSKI:def 1;
((h+c)^\n).k - (c^\n).k = (h^\n + c^\n).k - (c^\n).k by SEQM_3:15
.= (h^\n).k + (c^\n).k - (c^\n).k by SEQ_1:7
.= (h^\n).k;
hence thesis by A23,A8,A40,A41;
end;
A42: R is total by FDIFF_1:def 2;
now
let k;
thus (SVF1(1,f,z0)/*((h+c)^\n) - SVF1(1,f,z0)/*(c^\n)).k = (SVF1(1,f,z0)/*
((h+c)^\n)).k - (SVF1(1,f,z0)/*(c^\n)).k by RFUNCT_2:1
.= SVF1(1,f,z0).(((h+c)^\n).k) - (SVF1(1,f,z0)/*(c^\n)).k by A37,
FUNCT_2:108
.= SVF1(1,f,z0).(((h+c)^\n).k) - SVF1(1,f,z0).((c^\n).k) by A24,
FUNCT_2:108
.= L.((h^\n).k) + R.((h^\n).k) by A39
.= (L/*(h^\n)).k + R.((h^\n).k) by A26,FUNCT_2:115
.= (L/*(h^\n)).k + (R/*(h^\n)).k by A42,FUNCT_2:115
.= (L/*(h^\n) + R/*(h^\n)).k by SEQ_1:7;
end;
then
SVF1(1,f,z0)/*((h+c)^\n) - SVF1(1,f,z0)/*(c^\n) = L/*(h^\n) + R/*(h^\n)
by FUNCT_2:63;
then
A43: ((L/*(h^\n)+R/*(h^\n))(#)(h^\n)") = ((((SVF1(1,f,z0)/*(h+c))^\n)-SVF1(1
,f,z0)/*(c^\n))(#)(h^\n)") by A38,VALUED_0:27
.= ((((SVF1(1,f,z0)/*(h+c))^\n)-((SVF1(1,f,z0)/*c)^\n))(#)(h^\n)") by A15,
VALUED_0:27
.= ((((SVF1(1,f,z0)/*(h+c))-(SVF1(1,f,z0)/*c))^\n)(#)(h^\n)") by SEQM_3:17
.= ((((SVF1(1,f,z0)/*(h+c))-(SVF1(1,f,z0)/*c))^\n)(#)((h")^\n)) by
SEQM_3:18
.= ((((SVF1(1,f,z0)/*(h+c))-(SVF1(1,f,z0)/*c))(#) h")^\n) by SEQM_3:19;
then
A44: L
.1 = lim ((h")(#)((SVF1(1,f,z0)/*(h+c))-(SVF1(1,f,z0)/*c))) by A27,SEQ_4:22;
thus h"(#)(SVF1(1,f,z0)/*(h+c)-SVF1(1,f,z0)/*c) is convergent by A27,A43,
SEQ_4:21;
for x st x in N2 holds SVF1(1,f,z0).x - SVF1(1,f,z0).x0 = L.(x-x0) + R.
(x-x0) by A23,A8;
hence thesis by A1,A3,A9,A44,Th11;
end;
theorem
for z0 being Element of REAL 2 for N being Neighbourhood of proj(2,2).
z0 st f is_partial_differentiable_in z0,2 & N c= dom SVF1(2,f,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,f,z0)/*(h+c) - SVF1(2,f,z0)/*c) is
convergent & partdiff(f,z0,2) = lim (h"(#)(SVF1(2,f,z0)/*(h+c) - SVF1(2,f,z0)/*
c))
proof
let z0 be Element of REAL 2;
let N be Neighbourhood of proj(2,2).z0;
assume that
A1: f is_partial_differentiable_in z0,2 and
A2: N c= dom SVF1(2,f,z0);
consider x0,y0 being Real such that
A3: z0 = <*x0,y0*> and
A4: ex N1 being Neighbourhood of y0 st N1 c= dom SVF1(2,f,z0) & ex L,R
st for y st y in N1 holds SVF1(2,f,z0).y - SVF1(2,f,z0).y0 = L.(y-y0) + R.(y-y0
) by A1,Th10;
consider N1 be Neighbourhood of y0 such that
N1 c= dom SVF1(2,f,z0) and
A5: ex L,R st for y st y in N1 holds SVF1(2,f,z0).y - SVF1(2,f,z0).y0 =
L.(y-y0) + R.(y-y0) by A4;
A6: proj(2,2).z0 = y0 by A3,Th2;
then consider N2 be Neighbourhood of y0 such that
A7: N2 c= N and
A8: N2 c= N1 by RCOMP_1:17;
A9: N2 c= dom SVF1(2,f,z0) by A2,A7;
let h be 0-convergent non-zero Real_Sequence,
c be constant Real_Sequence such
that
A10: rng c = {proj(2,2).z0} and
A11: rng (h+c) c= N;
consider g be Real such that
A12: 0 < g and
A13: N2 = ].y0-g,y0+g.[ by RCOMP_1:def 6;
y0 + 0 < y0 + g & y0 - g < y0 - 0 by A12,XREAL_1:8,44;
then
A14: y0 in N2 by A13;
A15: rng c c= dom SVF1(2,f,z0)
proof
let y be object;
assume y in rng c;
then y = y0 by A10,A6,TARSKI:def 1;
then y in N by A7,A14;
hence thesis by A2;
end;
ex n st rng (c^\n) c= N2 & rng ((h+c)^\n) c= N2
proof
y0 in rng c by A10,A6,TARSKI:def 1;
then
A16: lim c = y0 by SEQ_4:25;
lim h = 0;
then lim (h+c) = 0+y0 by A16,SEQ_2:6
.= y0;
then consider n being Nat such that
A17: for m being Nat st n <= m holds |.(h+c).m-y0.| < g by A12,
SEQ_2:def 7;
reconsider n as Element of NAT by ORDINAL1:def 12;
take n;
A18: rng (c^\n) = {y0} by A10,A6,VALUED_0:26;
thus rng (c^\n) c= N2
by A14,A18,TARSKI:def 1;
let y be object;
assume y in rng ((h+c)^\n);
then consider m such that
A19: y = ((h+c)^\n).m by FUNCT_2:113;
n + 0 <= n+m by XREAL_1:7;
then
A20: |.(h+c).(n+m)-y0.|<g by A17;
then (h+c).(m+n) - y0 < g by SEQ_2:1;
then ((h+c)^\n).m - y0 < g by NAT_1:def 3;
then
A21: ((h+c)^\n).m < y0 + g by XREAL_1:19;
-g < (h+c).(m+n) - y0 by A20,SEQ_2:1;
then -g < ((h+c)^\n).m - y0 by NAT_1:def 3;
then y0 +-g < ((h+c)^\n).m by XREAL_1:20;
hence thesis by A13,A19,A21;
end;
then consider n such that
rng (c^\n) c= N2 and
A22: rng ((h+c)^\n) c= N2;
consider L,R such that
A23: for y st y in N1 holds SVF1(2,f,z0).y - SVF1(2,f,z0).y0 = L.(y-y0) +
R.(y-y0) by A5;
A24: rng (c^\n) c= dom SVF1(2,f,z0)
proof
let y be object;
assume
A25: y in rng (c^\n);
rng (c^\n) = rng c by VALUED_0:26;
then y = y0 by A10,A6,A25,TARSKI:def 1;
then y in N by A7,A14;
hence thesis by A2;
end;
A26: L is total by FDIFF_1:def 3;
A27: (L/*(h^\n) + R/*(h^\n))(#)(h^\n)" is convergent & lim ((L/*(h^\n) + R/*
(h^\n))(#)(h^\n)") = L.1
proof
deffunc F(Nat) = L.1 + ((R/*(h^\n))(#)(h^\n)").$1;
consider s1 such that
A28: for k being Nat holds s1.k = F(k) from SEQ_1:sch 1;
A29: now
A30: ((h^\n)")(#)(R/*(h^\n)) is convergent & lim (((h^\n)")(#)(R/*(h^\n)
)) = 0 by FDIFF_1:def 2;
let r be Real;
assume 0 < r;
then consider m being Nat such that
A31: for k being Nat st m <= k holds |.(((h^\n)")(#)(R/*(h^\n))).k-0.| < r
by A30,
SEQ_2:def 7;
take n1 = m;
let k be Nat such that
A32: n1 <= k;
|.s1.k-L.1.| = |.L.1+((R/*(h^\n))(#)(h^\n)").k-L.1 .| by A28
.= |.(((h^\n)")(#)(R/*(h^\n))).k-0 .|;
hence |.s1.k-L.1.| < r by A31,A32;
end;
consider s such that
A33: for p1 holds L.p1 = s*p1 by FDIFF_1:def 3;
A34: L.1 = s*1 by A33
.= s;
now
let m;
A35: (h^\n).m <> 0 by SEQ_1:5;
thus ((L/*(h^\n) + R/*(h^\n))(#)(h^\n)").m = ((L/*(h^\n) + R/*(h^\n)).m)
*((h^\n)").m by SEQ_1:8
.= ((L/*(h^\n)).m + (R/*(h^\n)).m) * ((h^\n)").m by SEQ_1:7
.= ((L/*(h^\n)).m)*((h^\n)").m + ((R/*(h^\n)).m)*((h^\n)").m
.= ((L/*(h^\n)).m)*((h^\n)").m + ((R/*(h^\n))(#)(h^\n)").m by SEQ_1:8
.= ((L/*(h^\n)).m)*((h^\n).m)" + ((R/*(h^\n))(#)(h^\n)").m by
VALUED_1:10
.= (L.((h^\n).m))*((h^\n).m)" + ((R/*(h^\n))(#)(h^\n)").m by A26,
FUNCT_2:115
.= (s*((h^\n).m))*((h^\n).m)" + ((R/*(h^\n))(#)(h^\n)").m by A33
.= s*(((h^\n).m)*((h^\n).m)") + ((R/*(h^\n))(#)(h^\n)").m
.= s*1 + ((R/*(h^\n))(#)(h^\n)").m by A35,XCMPLX_0:def 7
.= s1.m by A28,A34;
end;
then
A36: (L/*(h^\n) + R/*(h^\n))(#)(h^\n)" = s1 by FUNCT_2:63;
hence (L/*(h^\n)+R/*(h^\n))(#)(h^\n)" is convergent by A29,SEQ_2:def 6;
hence thesis by A36,A29,SEQ_2:def 7;
end;
A37: rng ((h+c)^\n) c= dom SVF1(2,f,z0)
by A22,A7,A2;
A38: rng (h+c) c= dom SVF1(2,f,z0)
by A11,A2;
A39: for k holds SVF1(2,f,z0).(((h+c)^\n).k) - SVF1(2,f,z0).((c^\n).k) = L.(
(h^\n).k) + R.((h^\n).k)
proof
let k;
((h+c)^\n).k in rng ((h+c)^\n) by VALUED_0:28;
then
A40: ((h+c)^\n).k in N2 by A22;
(c^\n).k in rng (c^\n) & rng (c^\n) = rng c by VALUED_0:26,28;
then
A41: (c^\n).k = y0 by A10,A6,TARSKI:def 1;
((h+c)^\n).k - (c^\n).k = (h^\n + c^\n).k - (c^\n).k by SEQM_3:15
.= (h^\n).k + (c^\n).k - (c^\n).k by SEQ_1:7
.= (h^\n).k;
hence thesis by A23,A8,A40,A41;
end;
A42: R is total by FDIFF_1:def 2;
now
let k;
thus (SVF1(2,f,z0)/*((h+c)^\n) - SVF1(2,f,z0)/*(c^\n)).k = (SVF1(2,f,z0)/*
((h+c)^\n)).k - (SVF1(2,f,z0)/*(c^\n)).k by RFUNCT_2:1
.= SVF1(2,f,z0).(((h+c)^\n).k) - (SVF1(2,f,z0)/*(c^\n)).k by A37,
FUNCT_2:108
.= SVF1(2,f,z0).(((h+c)^\n).k) - SVF1(2,f,z0).((c^\n).k) by A24,
FUNCT_2:108
.= L.((h^\n).k) + R.((h^\n).k) by A39
.= (L/*(h^\n)).k + R.((h^\n).k) by A26,FUNCT_2:115
.= (L/*(h^\n)).k + (R/*(h^\n)).k by A42,FUNCT_2:115
.= (L/*(h^\n) + R/*(h^\n)).k by SEQ_1:7;
end;
then
SVF1(2,f,z0)/*((h+c)^\n) - SVF1(2,f,z0)/*(c^\n) = L/*(h^\n) + R/*(h^\n)
by FUNCT_2:63;
then
A43: ((L/*(h^\n)+R/*(h^\n))(#)(h^\n)") = ((((SVF1(2,f,z0)/*(h+c))^\n)-SVF1(2
,f,z0)/*(c^\n))(#)(h^\n)") by A38,VALUED_0:27
.= ((((SVF1(2,f,z0)/*(h+c))^\n)-((SVF1(2,f,z0)/*c)^\n))(#)(h^\n)") by A15,
VALUED_0:27
.= ((((SVF1(2,f,z0)/*(h+c))-(SVF1(2,f,z0)/*c))^\n)(#)(h^\n)") by SEQM_3:17
.= ((((SVF1(2,f,z0)/*(h+c))-(SVF1(2,f,z0)/*c))^\n)(#)((h")^\n)) by
SEQM_3:18
.= ((((SVF1(2,f,z0)/*(h+c))-(SVF1(2,f,z0)/*c))(#) h")^\n) by SEQM_3:19;
then
A44: L
.1 = lim ((h")(#)((SVF1(2,f,z0)/*(h+c))-(SVF1(2,f,z0)/*c))) by A27,SEQ_4:22;
thus h"(#)(SVF1(2,f,z0)/*(h+c)-SVF1(2,f,z0)/*c) is convergent by A27,A43,
SEQ_4:21;
for y st y in N2 holds SVF1(2,f,z0).y - SVF1(2,f,z0).y0 = L.(y-y0) + R.
(y-y0) by A23,A8;
hence thesis by A1,A3,A9,A44,Th12;
end;
theorem
f1 is_partial_differentiable_in z0,1 & f2 is_partial_differentiable_in
z0,1 implies f1(#)f2 is_partial_differentiable_in z0,1
proof
assume that
A1: f1 is_partial_differentiable_in z0,1 and
A2: f2 is_partial_differentiable_in z0,1;
consider x0,y0 being Real such that
A3: z0 = <*x0,y0*> and
A4: ex N being Neighbourhood of x0 st N c= dom SVF1(1,f1,z0) & ex L,R st
for x st x in N holds SVF1(1,f1,z0).x - SVF1(1,f1,z0).x0 = L.(x-x0) + R.(x-x0)
by A1,Th9;
reconsider x0,y0 as Element of REAL by XREAL_0:def 1;
consider N1 be Neighbourhood of x0 such that
A5: N1 c= dom SVF1(1,f1,z0) and
A6: ex L,R st for x st x in N1 holds SVF1(1,f1,z0).x - SVF1(1,f1,z0).x0
= L.(x-x0) + R.(x-x0) by A4;
consider L1,R1 such that
A7: for x st x in N1 holds SVF1(1,f1,z0).x - SVF1(1,f1,z0).x0 = L1.(x-x0
) + R1.(x-x0) by A6;
consider x1,y1 being Real such that
A8: z0 = <*x1,y1*> and
A9: ex N being Neighbourhood of x1 st N c= dom SVF1(1,f2,z0) & ex L,R st
for x st x in N holds SVF1(1,f2,z0).x - SVF1(1,f2,z0).x1 = L.(x-x1) + R.(x-x1)
by A2,Th9;
x0 = x1 by A3,A8,FINSEQ_1:77;
then consider N2 be Neighbourhood of x0 such that
A10: N2 c= dom SVF1(1,f2,z0) and
A11: ex L,R st for x st x in N2 holds SVF1(1,f2,z0).x - SVF1(1,f2,z0).x0
= L.(x-x0) + R.(x-x0) by A9;
consider L2,R2 such that
A12: for x st x in N2 holds SVF1(1,f2,z0).x - SVF1(1,f2,z0).x0 = L2.(x-
x0) + R2.(x-x0) by A11;
consider N be Neighbourhood of x0 such that
A13: N c= N1 and
A14: N c= N2 by RCOMP_1:17;
A15: N c= dom SVF1(1,f2,z0) by A10,A14;
A16: N c= dom SVF1(1,f1,z0) by A5,A13;
A17: for y st y in N holds y in dom SVF1(1,f1(#)f2,z0)
proof
let y;
assume
A18: y in N;
then reproj(1,z0).y in dom f1 & reproj(1,z0).y in dom f2 by A16,A15,
FUNCT_1:11;
then reproj(1,z0).y in dom f1 /\ dom f2 by XBOOLE_0:def 4;
then
A19: reproj(1,z0).y in dom (f1(#)f2) by VALUED_1:def 4;
y in dom reproj(1,z0) by A15,A18,FUNCT_1:11;
hence thesis by A19,FUNCT_1:11;
end;
then for y be object st y in N holds y in dom SVF1(1,f1(#)f2,z0);
then
A20: N c= dom SVF1(1,f1(#)f2,z0);
reconsider R12=(SVF1(1,f1,z0).x0)(#)R2 as RestFunc by FDIFF_1:5;
A21: L2 is total by FDIFF_1:def 3;
reconsider R11=(SVF1(1,f2,z0).x0)(#)R1 as RestFunc by FDIFF_1:5;
A22: L1 is total by FDIFF_1:def 3;
A23: R1 is total by FDIFF_1:def 2;
reconsider R17=R1(#)R2 as RestFunc by FDIFF_1:4;
reconsider R16=R1(#)L2, R18=R2(#)L1 as RestFunc by FDIFF_1:7;
reconsider R14=L1(#)L2 as RestFunc by FDIFF_1:6;
reconsider R19=R16+R17 as RestFunc by FDIFF_1:4;
reconsider R20=R19+R18 as RestFunc by FDIFF_1:4;
A24: R14 is total by FDIFF_1:def 2;
A25: R18 is total by FDIFF_1:def 2;
A26: R2 is total by FDIFF_1:def 2;
reconsider R13=R11+R12 as RestFunc by FDIFF_1:4;
reconsider L11=(SVF1(1,f2,z0).x0)(#)L1, L12=(SVF1(1,f1,z0).x0)(#)L2 as
LinearFunc by FDIFF_1:3;
reconsider L=L11+L12 as LinearFunc by FDIFF_1:2;
reconsider R15=R13+R14 as RestFunc by FDIFF_1:4;
reconsider R=R15+R20 as RestFunc by FDIFF_1:4;
A27: R16 is total by FDIFF_1:def 2;
A28: L11 is total & L12 is total by FDIFF_1:def 3;
now
A29: x0 in dom ((f1(#)f2)*reproj(1,z0)) by A17,RCOMP_1:16;
then
A30: x0 in dom reproj(1,z0) by FUNCT_1:11;
reproj(1,z0).x0 in dom (f1(#)f2) by A29,FUNCT_1:11;
then
A31: reproj(1,z0).x0 in dom f1 /\ dom f2 by VALUED_1:def 4;
then reproj(1,z0).x0 in dom f1 by XBOOLE_0:def 4;
then
A32: x0 in dom (f1*reproj(1,z0)) by A30,FUNCT_1:11;
reproj(1,z0).x0 in dom f2 by A31,XBOOLE_0:def 4;
then
A33: x0 in dom (f2*reproj(1,z0)) by A30,FUNCT_1:11;
let x;
A34: x0 in N by RCOMP_1:16;
assume
A35: x in N;
then
A36: SVF1(1,f1,z0).x - SVF1(1,f1,z0).x0 + SVF1(1,f1,z0).x0 = L1.(x-x0) +
R1.(x-x0) + SVF1(1,f1,z0).x0 by A7,A13;
A37: x in dom ((f1(#)f2)*reproj(1,z0)) by A17,A35;
then
A38: x in dom reproj(1,z0) by FUNCT_1:11;
reproj(1,z0).x in dom (f1(#)f2) by A37,FUNCT_1:11;
then
A39: reproj(1,z0).x in dom f1 /\ dom f2 by VALUED_1:def 4;
then reproj(1,z0).x in dom f1 by XBOOLE_0:def 4;
then
A40: x in dom (f1*reproj(1,z0)) by A38,FUNCT_1:11;
reconsider xx0 =x-x0 as Element of REAL by XREAL_0:def 1;
reproj(1,z0).x in dom f2 by A39,XBOOLE_0:def 4;
then
A41: x in dom (f2*reproj(1,z0)) by A38,FUNCT_1:11;
thus SVF1(1,f1(#)f2,z0).x - SVF1(1,f1(#)f2,z0).x0 = (f1(#)f2).(reproj(1,z0
).x) - SVF1(1,f1(#)f2,z0).x0 by A20,A35,FUNCT_1:12
.= (f1.(reproj(1,z0).x))*(f2.(reproj(1,z0).x)) - SVF1(1,f1(#)f2,z0).x0
by VALUED_1:5
.= (SVF1(1,f1,z0).x)*(f2.(reproj(1,z0).x)) - SVF1(1,f1(#)f2,z0).x0 by A40
,FUNCT_1:12
.= (SVF1(1,f1,z0).x)*(SVF1(1,f2,z0).x) - ((f1(#)f2)*reproj(1,z0)).x0
by A41,FUNCT_1:12
.= (SVF1(1,f1,z0).x)*(SVF1(1,f2,z0).x) - (f1(#)f2).(reproj(1,z0).x0)
by A20,A34,FUNCT_1:12
.= (SVF1(1,f1,z0).x)*(SVF1(1,f2,z0).x) - (f1.(reproj(1,z0).x0))*(f2.(
reproj(1,z0).x0)) by VALUED_1:5
.= (SVF1(1,f1,z0).x)*(SVF1(1,f2,z0).x) - (SVF1(1,f1,z0).x0)*(f2.(
reproj(1,z0).x0)) by A32,FUNCT_1:12
.= (SVF1(1,f1,z0).x)*(SVF1(1,f2,z0).x)+-(SVF1(1,f1,z0).x)* (SVF1(1,f2,
z0).x0)+ (SVF1(1,f1,z0).x)*(SVF1(1,f2,z0).x0)-(SVF1(1,f1,z0).x0)* (SVF1(1,f2,z0
).x0) by A33,FUNCT_1:12
.= (SVF1(1,f1,z0).x)*(SVF1(1,f2,z0).x-SVF1(1,f2,z0).x0)+ (SVF1(1,f1,z0
).x-SVF1(1,f1,z0).x0)*(SVF1(1,f2,z0).x0)
.= (SVF1(1,f1,z0).x)*(SVF1(1,f2,z0).x-SVF1(1,f2,z0).x0)+ (L1.(x-x0)+R1
.(x-x0))*(SVF1(1,f2,z0).x0) by A7,A13,A35
.= (SVF1(1,f1,z0).x)*(SVF1(1,f2,z0).x-SVF1(1,f2,z0).x0)+ ((SVF1(1,f2,
z0).x0)*L1.(x-x0)+(SVF1(1,f2,z0).x0)*R1.(x-x0))
.= (SVF1(1,f1,z0).x)*(SVF1(1,f2,z0).x-SVF1(1,f2,z0).x0)+ (L11.(x-x0)+(
SVF1(1,f2,z0).x0)*R1.(xx0)) by A22,RFUNCT_1:57
.= (L1.(x-x0)+R1.(xx0)+SVF1(1,f1,z0).x0)* (SVF1(1,f2,z0).x-SVF1(1,f2,
z0).x0)+ (L11.(x-x0)+R11.(x-x0)) by A23,A36,RFUNCT_1:57
.= (L1.(x-x0)+R1.(x-x0)+SVF1(1,f1,z0).x0)*(L2.(x-x0)+R2.(x-x0))+ (L11.
(x-x0)+R11.(x-x0)) by A12,A14,A35
.= (L1.(x-x0)+R1.(x-x0))*(L2.(x-x0)+R2.(x-x0))+ ((SVF1(1,f1,z0).x0)*L2
.(x-x0)+(SVF1(1,f1,z0).x0)*R2.(x-x0))+ (L11.(x-x0)+R11.(x-x0))
.= (L1.(x-x0)+R1.(x-x0))*(L2.(x-x0)+R2.(x-x0))+ (L12.(x-x0)+(SVF1(1,f1
,z0).x0)*R2.(x-x0))+(L11.(x-x0)+R11.(xx0)) by A21,RFUNCT_1:57
.= (L1.(x-x0)+R1.(xx0))*(L2.(x-x0)+R2.(x-x0))+ (L12.(x-x0)+R12.(x-x0)
)+(L11.(x-x0)+R11.(x-x0)) by A26,RFUNCT_1:57
.= (L1.(x-x0)+R1.(x-x0))*(L2.(x-x0)+R2.(x-x0))+ (L12.(x-x0)+(L11.(x-x0
)+(R11.(x-x0)+R12.(x-x0))))
.= (L1.(x-x0)+R1.(xx0))*(L2.(x-x0)+R2.(x-x0))+ (L12.(x-x0)+(L11.(x-x0
)+R13.(x-x0))) by A23,A26,RFUNCT_1:56
.= (L1.(x-x0)+R1.(x-x0))*(L2.(x-x0)+R2.(x-x0))+ (L11.(x-x0)+L12.(x-x0)
+R13.(x-x0))
.= (L1.(x-x0)*L2.(x-x0)+L1.(xx0)*R2.(x-x0))+ R1.(x-x0)*(L2.(x-x0)+R2.
(x-x0))+(L.(x-x0)+R13.(x-x0)) by A28,RFUNCT_1:56
.= R14.(x-x0)+R2.(xx0)*L1.(x-x0)+R1.(x-x0)*(L2.(x-x0)+R2.(x-x0))+ (L.
(x-x0)+R13.(x-x0)) by A22,A21,RFUNCT_1:56
.= R14.(x-x0)+R18.(xx0)+(R1.(x-x0)*L2.(x-x0)+R1.(x-x0)*R2.(x-x0))+ (L
.(x-x0)+R13.(x-x0)) by A22,A26,RFUNCT_1:56
.= R14.(x-x0)+R18.(xx0)+(R16.(x-x0)+R1.(x-x0)*R2.(x-x0))+ (L.(x-x0)+
R13.(x-x0)) by A21,A23,RFUNCT_1:56
.= R14.(x-x0)+R18.(xx0)+(R16.(x-x0)+R17.(x-x0))+(L.(x-x0)+R13.(x-x0))
by A23,A26,RFUNCT_1:56
.= R14.(x-x0)+R18.(xx0)+R19.(x-x0)+(L.(x-x0)+R13.(x-x0)) by A23,A26,A27,
RFUNCT_1:56
.= R14.(x-x0)+(R19.(x-x0)+R18.(x-x0))+(L.(x-x0)+R13.(x-x0))
.= L.(x-x0)+R13.(xx0)+(R14.(x-x0)+R20.(x-x0)) by A23,A26,A27,A25,
RFUNCT_1:56
.= L.(x-x0)+(R13.(x-x0)+R14.(x-x0)+R20.(x-x0))
.= L.(x-x0)+(R15.(xx0)+R20.(x-x0)) by A23,A26,A24,RFUNCT_1:56
.= L.(x-x0)+R.(x-x0) by A23,A26,A24,A27,A25,RFUNCT_1:56;
end;
hence thesis by A3,A20,Th9;
end;
theorem
f1 is_partial_differentiable_in z0,2 & f2 is_partial_differentiable_in
z0,2 implies f1(#)f2 is_partial_differentiable_in z0,2
proof
assume that
A1: f1 is_partial_differentiable_in z0,2 and
A2: f2 is_partial_differentiable_in z0,2;
consider x0,y0 being Real such that
A3: z0 = <*x0,y0*> and
A4: ex N being Neighbourhood of y0 st N c= dom SVF1(2,f1,z0) & ex L,R st
for y st y in N holds SVF1(2,f1,z0).y - SVF1(2,f1,z0).y0 = L.(y-y0) + R.(y-y0)
by A1,Th10;
reconsider x0,y0 as Real;
consider N1 be Neighbourhood of y0 such that
A5: N1 c= dom SVF1(2,f1,z0) and
A6: ex L,R st for y st y in N1 holds SVF1(2,f1,z0).y - SVF1(2,f1,z0).y0
= L.(y-y0) + R.(y-y0) by A4;
consider L1,R1 such that
A7: for y st y in N1 holds SVF1(2,f1,z0).y - SVF1(2,f1,z0).y0 = L1.(y-y0
) + R1.(y-y0) by A6;
consider x1,y1 being Real such that
A8: z0 = <*x1,y1*> and
A9: ex N being Neighbourhood of y1 st N c= dom SVF1(2,f2,z0) & ex L,R st
for y st y in N holds SVF1(2,f2,z0).y - SVF1(2,f2,z0).y1 = L.(y-y1) + R.(y-y1)
by A2,Th10;
y0 = y1 by A3,A8,FINSEQ_1:77;
then consider N2 be Neighbourhood of y0 such that
A10: N2 c= dom SVF1(2,f2,z0) and
A11: ex L,R st for y st y in N2 holds SVF1(2,f2,z0).y - SVF1(2,f2,z0).y0
= L.(y-y0) + R.(y-y0) by A9;
consider L2,R2 such that
A12: for y st y in N2 holds SVF1(2,f2,z0).y - SVF1(2,f2,z0).y0 = L2.(y-
y0) + R2.(y-y0) by A11;
consider N be Neighbourhood of y0 such that
A13: N c= N1 and
A14: N c= N2 by RCOMP_1:17;
A15: N c= dom SVF1(2,f2,z0) by A10,A14;
A16: N c= dom SVF1(2,f1,z0) by A5,A13;
A17: for y st y in N holds y in dom SVF1(2,f1(#)f2,z0)
proof
let y;
assume
A18: y in N;
then reproj(2,z0).y in dom f1 & reproj(2,z0).y in dom f2 by A16,A15,
FUNCT_1:11;
then reproj(2,z0).y in dom f1 /\ dom f2 by XBOOLE_0:def 4;
then
A19: reproj(2,z0).y in dom (f1(#)f2) by VALUED_1:def 4;
y in dom reproj(2,z0) by A15,A18,FUNCT_1:11;
hence thesis by A19,FUNCT_1:11;
end;
then for y be object st y in N holds y in dom SVF1(2,f1(#)f2,z0);
then
A20: N c= dom SVF1(2,f1(#)f2,z0);
reconsider L12=(SVF1(2,f1,z0).y0)(#)L2 as LinearFunc by FDIFF_1:3;
A21: L2 is total by FDIFF_1:def 3;
reconsider L11=(SVF1(2,f2,z0).y0)(#)L1 as LinearFunc by FDIFF_1:3;
A22: L1 is total by FDIFF_1:def 3;
reconsider L=L11+L12 as LinearFunc by FDIFF_1:2;
A23: R1 is total by FDIFF_1:def 2;
reconsider R16=R1(#)L2, R18=R2(#)L1 as RestFunc by FDIFF_1:7;
reconsider R14=L1(#)L2 as RestFunc by FDIFF_1:6;
reconsider R11=(SVF1(2,f2,z0).y0)(#)R1, R12=(SVF1(2,f1,z0).y0)(#)R2
as RestFunc by FDIFF_1:5;
reconsider R13=R11+R12 as RestFunc by FDIFF_1:4;
reconsider R15=R13+R14, R17=R1(#)R2 as RestFunc by FDIFF_1:4;
reconsider R19=R16+R17 as RestFunc by FDIFF_1:4;
reconsider R20=R19+R18 as RestFunc by FDIFF_1:4;
reconsider R=R15+R20 as RestFunc by FDIFF_1:4;
A24: R14 is total by FDIFF_1:def 2;
A25: R16 is total by FDIFF_1:def 2;
A26: R18 is total by FDIFF_1:def 2;
A27: R2 is total by FDIFF_1:def 2;
A28: L11 is total & L12 is total by FDIFF_1:def 3;
now
A29: y0 in dom ((f1(#)f2)*reproj(2,z0)) by A17,RCOMP_1:16;
then
A30: y0 in dom reproj(2,z0) by FUNCT_1:11;
reproj(2,z0).y0 in dom (f1(#)f2) by A29,FUNCT_1:11;
then
A31: reproj(2,z0).y0 in dom f1 /\ dom f2 by VALUED_1:def 4;
then reproj(2,z0).y0 in dom f1 by XBOOLE_0:def 4;
then
A32: y0 in dom (f1*reproj(2,z0)) by A30,FUNCT_1:11;
reproj(2,z0).y0 in dom f2 by A31,XBOOLE_0:def 4;
then
A33: y0 in dom (f2*reproj(2,z0)) by A30,FUNCT_1:11;
let y;
A34: y0 in N by RCOMP_1:16;
reconsider yy0 = y-y0 as Element of REAL by XREAL_0:def 1;
assume
A35: y in N;
then
A36: SVF1(2,f1,z0).y - SVF1(2,f1,z0).y0 + SVF1(2,f1,z0).y0 = L1.(y-y0) +
R1.(y-y0) + SVF1(2,f1,z0).y0 by A7,A13;
A37: y in dom ((f1(#)f2)*reproj(2,z0)) by A17,A35;
then
A38: y in dom reproj(2,z0) by FUNCT_1:11;
reproj(2,z0).y in dom (f1(#)f2) by A37,FUNCT_1:11;
then
A39: reproj(2,z0).y in dom f1 /\ dom f2 by VALUED_1:def 4;
then reproj(2,z0).y in dom f1 by XBOOLE_0:def 4;
then
A40: y in dom (f1*reproj(2,z0)) by A38,FUNCT_1:11;
reproj(2,z0).y in dom f2 by A39,XBOOLE_0:def 4;
then
A41: y in dom (f2*reproj(2,z0)) by A38,FUNCT_1:11;
thus SVF1(2,f1(#)f2,z0).y - SVF1(2,f1(#)f2,z0).y0 = (f1(#)f2).(reproj(2,z0
).y) - SVF1(2,f1(#)f2,z0).y0 by A20,A35,FUNCT_1:12
.= (f1.(reproj(2,z0).y))*(f2.(reproj(2,z0).y)) - SVF1(2,f1(#)f2,z0).y0
by VALUED_1:5
.= (SVF1(2,f1,z0).y)*(f2.(reproj(2,z0).y)) - SVF1(2,f1(#)f2,z0).y0 by A40
,FUNCT_1:12
.= (SVF1(2,f1,z0).y)*(SVF1(2,f2,z0).y) - ((f1(#)f2)*reproj(2,z0)).y0
by A41,FUNCT_1:12
.= (SVF1(2,f1,z0).y)*(SVF1(2,f2,z0).y) - (f1(#)f2).(reproj(2,z0).y0)
by A20,A34,FUNCT_1:12
.= (SVF1(2,f1,z0).y)*(SVF1(2,f2,z0).y) - (f1.(reproj(2,z0).y0))*(f2.(
reproj(2,z0).y0)) by VALUED_1:5
.= (SVF1(2,f1,z0).y)*(SVF1(2,f2,z0).y) - (SVF1(2,f1,z0).y0)*(f2.(
reproj(2,z0).y0)) by A32,FUNCT_1:12
.= (SVF1(2,f1,z0).y)*(SVF1(2,f2,z0).y)+ -(SVF1(2,f1,z0).y)*(SVF1(2,f2,
z0).y0)+ (SVF1(2,f1,z0).y)*(SVF1(2,f2,z0).y0)- (SVF1(2,f1,z0).y0)*(SVF1(2,f2,z0
).y0) by A33,FUNCT_1:12
.= (SVF1(2,f1,z0).y)*(SVF1(2,f2,z0).y-SVF1(2,f2,z0).y0)+ (SVF1(2,f1,z0
).y-SVF1(2,f1,z0).y0)*(SVF1(2,f2,z0).y0)
.= (SVF1(2,f1,z0).y)*(SVF1(2,f2,z0).y-SVF1(2,f2,z0).y0)+ (L1.(y-y0)+R1
.(y-y0))*(SVF1(2,f2,z0).y0) by A7,A13,A35
.= (SVF1(2,f1,z0).y)*(SVF1(2,f2,z0).y-SVF1(2,f2,z0).y0)+ ((SVF1(2,f2,
z0).y0)*L1.(y-y0)+(SVF1(2,f2,z0).y0)*R1.(y-y0))
.= (SVF1(2,f1,z0).y)*(SVF1(2,f2,z0).y-SVF1(2,f2,z0).y0)+ (L11.(y-y0)+(
SVF1(2,f2,z0).y0)*R1.(yy0)) by A22,RFUNCT_1:57
.= (L1.(y-y0)+R1.(y-y0)+SVF1(2,f1,z0).y0)* (SVF1(2,f2,z0).y-SVF1(2,f2,
z0).y0)+ (L11.(y-y0)+R11.(yy0)) by A23,A36,RFUNCT_1:57
.= (L1.(y-y0)+R1.(y-y0)+SVF1(2,f1,z0).y0)*(L2.(y-y0)+R2.(y-y0))+ (L11.
(y-y0)+R11.(y-y0)) by A12,A14,A35
.= (L1.(y-y0)+R1.(y-y0))*(L2.(y-y0)+R2.(y-y0))+ ((SVF1(2,f1,z0).y0)*L2
.(y-y0)+(SVF1(2,f1,z0).y0)*R2.(y-y0))+ (L11.(y-y0)+R11.(y-y0))
.= (L1.(y-y0)+R1.(y-y0))*(L2.(y-y0)+R2.(y-y0))+ (L12.(y-y0)+(SVF1(2,f1
,z0).y0)*R2.(y-y0))+(L11.(yy0)+R11.(y-y0)) by A21,RFUNCT_1:57
.= (L1.(y-y0)+R1.(y-y0))*(L2.(y-y0)+R2.(y-y0))+ (L12.(y-y0)+R12.(y-y0)
)+(L11.(y-y0)+R11.(yy0)) by A27,RFUNCT_1:57
.= (L1.(y-y0)+R1.(y-y0))*(L2.(y-y0)+R2.(y-y0))+ (L12.(y-y0)+(L11.(y-y0
)+(R11.(y-y0)+R12.(y-y0))))
.= (L1.(y-y0)+R1.(yy0))*(L2.(y-y0)+R2.(y-y0))+ (L12.(y-y0)+(L11.(y-y0
)+R13.(y-y0))) by A23,A27,RFUNCT_1:56
.= (L1.(y-y0)+R1.(y-y0))*(L2.(y-y0)+R2.(y-y0))+ (L11.(y-y0)+L12.(y-y0)
+R13.(y-y0))
.= (L1.(y-y0)*L2.(y-y0)+L1.(y-y0)*R2.(y-y0))+ R1.(y-y0)*(L2.(y-y0)+R2.
(y-y0))+(L.(y-y0)+R13.(yy0)) by A28,RFUNCT_1:56
.= R14.(y-y0)+R2.(y-y0)*L1.(y-y0)+R1.(y-y0)*(L2.(y-y0)+R2.(y-y0))+ (L.
(y-y0)+R13.(yy0)) by A22,A21,RFUNCT_1:56
.= R14.(y-y0)+R18.(y-y0)+(R1.(y-y0)*L2.(y-y0)+R1.(y-y0)*R2.(y-y0))+ (L
.(y-y0)+R13.(yy0)) by A22,A27,RFUNCT_1:56
.= R14.(y-y0)+R18.(y-y0)+(R16.(y-y0)+R1.(y-y0)*R2.(y-y0))+ (L.(y-y0)+
R13.(yy0)) by A21,A23,RFUNCT_1:56
.= R14.(yy0)+R18.(y-y0)+(R16.(y-y0)+R17.(y-y0))+(L.(y-y0)+R13.(y-y0))
by A23,A27,RFUNCT_1:56
.= R14.(yy0)+R18.(y-y0)+R19.(y-y0)+(L.(y-y0)+R13.(y-y0)) by A23,A27,A25,
RFUNCT_1:56
.= R14.(y-y0)+(R19.(y-y0)+R18.(y-y0))+(L.(y-y0)+R13.(y-y0))
.= L.(yy0)+R13.(y-y0)+(R14.(y-y0)+R20.(y-y0)) by A23,A27,A25,A26,
RFUNCT_1:56
.= L.(yy0)+(R13.(y-y0)+R14.(y-y0)+R20.(y-y0))
.= L.(yy0)+(R15.(y-y0)+R20.(y-y0)) by A23,A27,A24,RFUNCT_1:56
.= L.(y-y0)+R.(y-y0) by A23,A27,A24,A25,A26,RFUNCT_1:56;
end;
hence thesis by A3,A20,Th10;
end;
theorem
for z0 being Element of REAL 2 holds f is_partial_differentiable_in z0
,1 implies SVF1(1,f,z0) is_continuous_in proj(1,2).z0
by FDIFF_1:24;
theorem
for z0 being Element of REAL 2 holds f is_partial_differentiable_in z0
,2 implies SVF1(2,f,z0) is_continuous_in proj(2,2).z0
by FDIFF_1:24;