:: Partial Differentiation of Real Ternary Functions
:: by Takao Inou\'e , Bing Xie and Xiquan Liang
::
:: Received November 7, 2009
:: Copyright (c) 2009-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 SUBSET_1, NUMBERS, FINSEQ_1, FINSEQ_2, PARTFUN1, REAL_1, EUCLID,
FUNCT_1, RELAT_1, ARYTM_3, ARYTM_1, RVSUM_1, CARD_3, CARD_1, SQUARE_1,
COMPLEX1, XXREAL_0, FDIFF_1, VALUED_1, XXREAL_1, TARSKI, EUCLID_8,
FUNCT_2, XBOOLE_0, NAT_1, VALUED_0, ORDINAL2, SEQ_1, SEQ_2, RCOMP_1,
PDIFF_1, PDIFF_2, FCONT_1, PDIFF_4, 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, SQUARE_1,
RVSUM_1, VALUED_1, SEQ_1, SEQ_2, FINSEQ_1, FINSEQ_2, RCOMP_1, EUCLID,
FDIFF_1, XXREAL_0, FCONT_1, PDIFF_1, PDIFF_2, EUCLID_8;
constructors REAL_1, SEQ_2, COMPLEX1, RCOMP_1, FDIFF_1, FCONT_1, PDIFF_1,
RELSET_1, PDIFF_2, EUCLID_8, SQUARE_1, BINOP_2, FINSEQOP, FINSEQ_4,
MONOID_0, COMSEQ_2;
registrations RELSET_1, XREAL_0, MEMBERED, FDIFF_1, FUNCT_2, NAT_1, NUMBERS,
FINSEQ_1, VALUED_0, VALUED_1, ORDINAL1, EUCLID, RVSUM_1, RCOMP_1,
FUNCOP_1, FCONT_3, SQUARE_1, SEQ_2;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI;
equalities EUCLID, RCOMP_1, PDIFF_1, PDIFF_2, EUCLID_8, VALUED_1, RVSUM_1,
XBOOLE_0, SUBSET_1;
expansions TARSKI, PDIFF_1, XBOOLE_0;
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, XCMPLX_0, XCMPLX_1, PDIFF_1, NAT_1, VALUED_0,
RFUNCT_1, RVSUM_1, EUCLID_5, PARTFUN2, EUCLID_8, XREAL_0, ORDINAL1;
schemes SEQ_1;
begin :: Preliminaries
reserve D for set;
reserve x,x0,x1,x2,y,y0,y1,y2,z,z0,z1,z2,r,s,t for Real;
reserve p,a,u,u0 for Element of REAL 3;
reserve n,m,k for Element of NAT;
reserve f,f1,f2,f3,g for PartFunc of REAL 3,REAL;
reserve R,R1,R2 for RestFunc;
reserve L,L1,L2 for LinearFunc;
theorem Th1:
dom proj(1,3) = REAL 3 & rng proj(1,3) = REAL &
for x,y,z be Real holds proj(1,3).<*x,y,z*> = x
proof
set f = proj(1,3);
A1: for x be object st x in REAL ex u be object st u in REAL 3 & x = f.u
proof
let x be object;
assume x in REAL;
then reconsider x1 = x as Element of REAL;
set y = the Element of REAL;
reconsider u = <*x1,y,y*> as Element of REAL 3 by FINSEQ_2:104;
f.u = u.1 by PDIFF_1:def 1;
then f.u = x;
hence thesis;
end;
now let x,y,z;
reconsider xx=x, yy=y, zz=z as Element of REAL by XREAL_0:def 1;
<*xx,yy,zz*> is Element of 3-tuples_on REAL by FINSEQ_2:104;
then proj(1,3).<*x,y,z*> = <*x,y,z*>.1 by PDIFF_1:def 1;
hence proj(1,3).<*x,y,z*> = x;
end;
hence thesis by A1,FUNCT_2:10,def 1;
end;
theorem Th2:
dom proj(2,3) = REAL 3 & rng proj(2,3) = REAL &
for x,y,z be Real holds proj(2,3).<*x,y,z*> = y
proof
set f = proj(2,3);
A1: for y be object st y in REAL ex u be object st u in REAL 3 & y = f.u
proof
let y be object;
assume y in REAL;
then reconsider y1 = y as Element of REAL;
set x = the Element of REAL;
reconsider u = <*x,y1,x*> as Element of REAL 3 by FINSEQ_2:104;
f.u = u.2 by PDIFF_1:def 1;
then f.u = y;
hence thesis;
end;
now let x,y,z;
reconsider xx=x, yy=y, zz=z as Element of REAL by XREAL_0:def 1;
<*xx,yy,zz*> is Element of 3-tuples_on REAL by FINSEQ_2:104;
then proj(2,3).<*x,y,z*> = <*x,y,z*>.2 by PDIFF_1:def 1;
hence proj(2,3).<*x,y,z*> = y;
end;
hence thesis by A1,FUNCT_2:10,def 1;
end;
theorem Th3:
dom proj(3,3) = REAL 3 & rng proj(3,3) = REAL &
for x,y,z be Real holds proj(3,3).<*x,y,z*> = z
proof
set f = proj(3,3);
A1: for z be object st z in REAL ex u be object st u in REAL 3 & z = f.u
proof
let z be object;
assume z in REAL;
then reconsider z1 = z as Element of REAL;
set x = the Element of REAL;
reconsider u = <*x,x,z1*> as Element of REAL 3 by FINSEQ_2:104;
f.u = u.3 by PDIFF_1:def 1;
then f.u = z;
hence thesis;
end;
now let x,y,z be Real;
reconsider xx=x, yy=y, zz=z as Element of REAL by XREAL_0:def 1;
<*xx,yy,zz*> is Element of 3-tuples_on REAL by FINSEQ_2:104;
then proj(3,3).<*x,y,z*> = <*x,y,z*>.3 by PDIFF_1:def 1;
hence proj(3,3).<*x,y,z*> = z;
end;
hence thesis by A1,FUNCT_2:10,def 1;
end;
begin :: Partial Differentiation of Real Ternary Functions
theorem Th4:
u = <*x,y,z*> & f is_partial_differentiable_in u,1 implies
SVF1(1,f,u) is_differentiable_in x
by Th1;
theorem Th5:
u = <*x,y,z*> & f is_partial_differentiable_in u,2 implies
SVF1(2,f,u) is_differentiable_in y
by Th2;
theorem Th6:
u = <*x,y,z*> & f is_partial_differentiable_in u,3 implies
SVF1(3,f,u) is_differentiable_in z
by Th3;
theorem Th7:
for f be PartFunc of REAL 3,REAL for u be Element of REAL 3 holds
(ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
SVF1(1,f,u) is_differentiable_in x0) iff
f is_partial_differentiable_in u,1
proof
let f be PartFunc of REAL 3,REAL;
let u be Element of REAL 3;
thus (ex x0,y0,z0 being Real st
u = <*x0,y0,z0*> & SVF1(1,f,u) is_differentiable_in x0) implies
f is_partial_differentiable_in u,1 by Th1;
assume
A1: f is_partial_differentiable_in u,1;
consider x0,y0,z0 being Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
proj(1,3).u = x0 by A2,Th1;
then SVF1(1,f,u) is_differentiable_in x0 by A1;
hence (ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
SVF1(1,f,u) is_differentiable_in x0) by A2;
end;
theorem Th8:
for f be PartFunc of REAL 3,REAL for u be Element of REAL 3 holds
(ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
SVF1(2,f,u) is_differentiable_in y0) iff
f is_partial_differentiable_in u,2
proof
let f be PartFunc of REAL 3,REAL;
let u be Element of REAL 3;
thus (ex x0,y0,z0 being Real st
u = <*x0,y0,z0*> & SVF1(2,f,u) is_differentiable_in y0) implies
f is_partial_differentiable_in u,2 by Th2;
assume
A1: f is_partial_differentiable_in u,2;
consider x0,y0,z0 being Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
proj(2,3).u = y0 by A2,Th2;
then SVF1(2,f,u) is_differentiable_in y0 by A1;
hence (ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
SVF1(2,f,u) is_differentiable_in y0) by A2;
end;
theorem Th9:
for f be PartFunc of REAL 3,REAL for u be Element of REAL 3 holds
(ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
SVF1(3,f,u) is_differentiable_in z0) iff
f is_partial_differentiable_in u,3
proof
let f be PartFunc of REAL 3,REAL;
let u be Element of REAL 3;
thus (ex x0,y0,z0 being Real st
u = <*x0,y0,z0*> & SVF1(3,f,u) is_differentiable_in z0) implies
f is_partial_differentiable_in u,3 by Th3;
assume
A1: f is_partial_differentiable_in u,3;
consider x0,y0,z0 being Element of REAL such that
A2: u = <*x0,y0,z0*> by FINSEQ_2:103;
proj(3,3).u = z0 by A2,Th3;
then SVF1(3,f,u) is_differentiable_in z0 by A1;
hence (ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
SVF1(3,f,u) is_differentiable_in z0) by A2;
end;
theorem
u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 implies
ex N being Neighbourhood of x0 st N c= dom SVF1(1,f,u) &
ex L,R st for x st x in N holds
SVF1(1,f,u).x - SVF1(1,f,u).x0 = L.(x-x0) + R.(x-x0)
proof
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_partial_differentiable_in u,1;
consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & SVF1(1,f,u) is_differentiable_in x1 by A2,Th7;
SVF1(1,f,u) is_differentiable_in x0 by A1,A3,FINSEQ_1:78;
hence thesis by FDIFF_1:def 4;
end;
theorem
u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 implies
ex N being Neighbourhood of y0 st N c= dom SVF1(2,f,u) &
ex L,R st for y st y in N holds
SVF1(2,f,u).y - SVF1(2,f,u).y0 = L.(y-y0) + R.(y-y0)
proof
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_partial_differentiable_in u,2;
consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> & SVF1(2,f,u) is_differentiable_in y1 by A2,Th8;
SVF1(2,f,u) is_differentiable_in y0 by A1,A3,FINSEQ_1:78;
hence thesis by FDIFF_1:def 4;
end;
theorem
u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 implies
ex N being Neighbourhood of z0 st N c= dom SVF1(3,f,u) &
ex L,R st for z st z in N holds
SVF1(3,f,u).z - SVF1(3,f,u).z0 = L.(z-z0) + R.(z-z0)
proof
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_partial_differentiable_in u,3;
consider x1,y1,z1 such that
A3: u = <*x1,y1,z1*> &
SVF1(3,f,u) is_differentiable_in z1 by A2,Th9;
SVF1(3,f,u) is_differentiable_in z0 by A1,A3,FINSEQ_1:78;
hence thesis by FDIFF_1:def 4;
end;
theorem Th13:
for f be PartFunc of REAL 3,REAL for u be Element of REAL 3 holds
f is_partial_differentiable_in u,1 iff
ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(1,f,u) &
ex L,R st for x st x in N holds
SVF1(1,f,u).x - SVF1(1,f,u).x0 = L.(x-x0) + R.(x-x0)
proof
let f be PartFunc of REAL 3,REAL;
let u be Element of REAL 3;
hereby assume A1: f is_partial_differentiable_in u,1;
thus (ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(1,f,u) &
ex L,R st for x st x in N holds
SVF1(1,f,u).x - SVF1(1,f,u).x0 = L.(x-x0) + R.(x-x0))
proof
consider x0,y0,z0 such that
A2: u = <*x0,y0,z0*> & SVF1(1,f,u) is_differentiable_in x0 by A1,Th7;
ex N being Neighbourhood of x0 st N c= dom SVF1(1,f,u) &
ex L,R st for x st x in N holds
SVF1(1,f,u).x - SVF1(1,f,u).x0 = L.(x-x0) + R.(x-x0) by A2,FDIFF_1:def 4;
hence thesis by A2;
end;
end;
assume (ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(1,f,u) &
ex L,R st for x st x in N holds
SVF1(1,f,u).x - SVF1(1,f,u).x0 = L.(x-x0) + R.(x-x0));
then consider x0,y0,z0 such that
A3: u = <*x0,y0,z0*> & ex N being Neighbourhood of x0
st N c= dom SVF1(1,f,u) & ex L,R st for x st x in N holds
SVF1(1,f,u).x - SVF1(1,f,u).x0 = L.(x-x0) + R.(x-x0);
consider N being Neighbourhood of x0 such that
A4: N c= dom SVF1(1,f,u) & ex L,R st for x st x in N holds
SVF1(1,f,u).x - SVF1(1,f,u).x0 = L.(x-x0) + R.(x-x0) by A3;
SVF1(1,f,u) is_differentiable_in x0 by A4,FDIFF_1:def 4;
hence thesis by A3,Th7;
end;
theorem Th14:
for f be PartFunc of REAL 3,REAL for u be Element of REAL 3 holds
f is_partial_differentiable_in u,2 iff
ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of y0 st N c= dom SVF1(2,f,u) &
ex L,R st for y st y in N holds
SVF1(2,f,u).y - SVF1(2,f,u).y0 = L.(y-y0) + R.(y-y0)
proof
let f be PartFunc of REAL 3,REAL;
let u be Element of REAL 3;
hereby assume A1: f is_partial_differentiable_in u,2;
thus (ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of y0 st N c= dom SVF1(2,f,u) &
ex L,R st for y st y in N holds
SVF1(2,f,u).y - SVF1(2,f,u).y0 = L.(y-y0) + R.(y-y0))
proof
consider x0,y0,z0 such that
A2: u = <*x0,y0,z0*> & SVF1(2,f,u) is_differentiable_in y0 by A1,Th8;
ex N being Neighbourhood of y0 st N c= dom SVF1(2,f,u) &
ex L,R st for y st y in N holds
SVF1(2,f,u).y - SVF1(2,f,u).y0 = L.(y-y0) + R.(y-y0) by A2,FDIFF_1:def 4;
hence thesis by A2;
end;
end;
assume (ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of y0 st N c= dom SVF1(2,f,u) &
ex L,R st for y st y in N holds
SVF1(2,f,u).y - SVF1(2,f,u).y0 = L.(y-y0) + R.(y-y0));
then consider x0,y0,z0 such that
A3: u = <*x0,y0,z0*> & ex N being Neighbourhood of y0
st N c= dom SVF1(2,f,u) & ex L,R st for y st y in N holds
SVF1(2,f,u).y - SVF1(2,f,u).y0 = L.(y-y0) + R.(y-y0);
consider N being Neighbourhood of y0 such that
A4: N c= dom SVF1(2,f,u) & ex L,R st for y st y in N holds
SVF1(2,f,u).y - SVF1(2,f,u).y0 = L.(y-y0) + R.(y-y0) by A3;
SVF1(2,f,u) is_differentiable_in y0 by A4,FDIFF_1:def 4;
hence thesis by A3,Th8;
end;
theorem Th15:
for f be PartFunc of REAL 3,REAL for u be Element of REAL 3 holds
f is_partial_differentiable_in u,3 iff
ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of z0 st N c= dom SVF1(3,f,u) &
ex L,R st for z st z in N holds
SVF1(3,f,u).z - SVF1(3,f,u).z0 = L.(z-z0) + R.(z-z0)
proof
let f be PartFunc of REAL 3,REAL;
let u be Element of REAL 3;
hereby assume A1: f is_partial_differentiable_in u,3;
thus (ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of z0 st N c= dom SVF1(3,f,u) &
ex L,R st for z st z in N holds
SVF1(3,f,u).z - SVF1(3,f,u).z0 = L.(z-z0) + R.(z-z0))
proof
consider x0,y0,z0 such that
A2: u = <*x0,y0,z0*> &
SVF1(3,f,u) is_differentiable_in z0 by A1,Th9;
ex N being Neighbourhood of z0 st N c= dom SVF1(3,f,u) &
ex L,R st for z st z in N holds
SVF1(3,f,u).z - SVF1(3,f,u).z0 = L.(z-z0) + R.(z-z0) by A2,FDIFF_1:def 4;
hence thesis by A2;
end;
end;
assume (ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of z0 st N c= dom SVF1(3,f,u) &
ex L,R st for z st z in N holds
SVF1(3,f,u).z - SVF1(3,f,u).z0 = L.(z-z0) + R.(z-z0));
then consider x0,y0,z0 such that
A3: u = <*x0,y0,z0*> & ex N being Neighbourhood of z0
st N c= dom SVF1(3,f,u) & ex L,R st for z st z in N holds
SVF1(3,f,u).z - SVF1(3,f,u).z0 = L.(z-z0) + R.(z-z0);
consider N being Neighbourhood of z0 such that
A4: N c= dom SVF1(3,f,u) & ex L,R st for z st z in N holds
SVF1(3,f,u).z - SVF1(3,f,u).z0 = L.(z-z0) + R.(z-z0) by A3;
SVF1(3,f,u) is_differentiable_in z0 by A4,FDIFF_1:def 4;
hence thesis by A3,Th9;
end;
Lm1:
u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 implies
(r = diff(SVF1(1,f,u),x0) iff
ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(1,f,u) &
ex L,R st r = L.1 & for x st x in N holds
SVF1(1,f,u).x - SVF1(1,f,u).x0 = L.(x-x0) + R.(x-x0))
proof
set F1 = SVF1(1,f,u);
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_partial_differentiable_in u,1;
hereby assume A3: r = diff(F1,x0);
F1 is_differentiable_in x0 by A1,A2,Th4; then
consider N being Neighbourhood of x0 such that
A4: 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 A3,FDIFF_1:def 5;
thus ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(1,f,u) &
ex L,R st r = L.1 & for x st x in N holds
SVF1(1,f,u).x - SVF1(1,f,u).x0 = L.(x-x0) + R.(x-x0) by A1,A4;
end;
given x1,y1,z1 being Real such that
A5: u = <*x1,y1,z1*> &
ex N being Neighbourhood of x1 st N c= dom SVF1(1,f,u) &
ex L,R st r = L.1 & for x st x in N holds
SVF1(1,f,u).x - SVF1(1,f,u).x1 = L.(x-x1) + R.(x-x1);
A6:x1 = x0 by A5,A1,FINSEQ_1:78;
F1 is_differentiable_in x0 by A1,A2,Th4;
hence thesis by A6,A5,FDIFF_1:def 5;
end;
Lm2:
u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 implies
(r = diff(SVF1(2,f,u),y0) iff
ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of y0 st N c= dom SVF1(2,f,u) &
ex L,R st r = L.1 & for y st y in N holds
SVF1(2,f,u).y - SVF1(2,f,u).y0 = L.(y-y0) + R.(y-y0))
proof
set F1 = SVF1(2,f,u);
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_partial_differentiable_in u,2;
hereby assume A3: r = diff(F1,y0);
F1 is_differentiable_in y0 by A1,A2,Th5; then
consider N being Neighbourhood of y0 such that
A4: 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 A3,FDIFF_1:def 5;
thus ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
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,u).y - SVF1(2,f,u).y0 = L.(y-y0) + R.(y-y0) by A1,A4;
end;
given x1,y1,z1 being Real such that
A5: u = <*x1,y1,z1*> & 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);
A6:y1 = y0 by A5,A1,FINSEQ_1:78;
F1 is_differentiable_in y0 by A1,A2,Th5;
hence thesis by A6,A5,FDIFF_1:def 5;
end;
Lm3:
u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 implies
(r = diff(SVF1(3,f,u),z0) iff
ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of z0 st N c= dom SVF1(3,f,u) &
ex L,R st r = L.1 & for z st z in N holds
SVF1(3,f,u).z - SVF1(3,f,u).z0 = L.(z-z0) + R.(z-z0))
proof
set F1 = SVF1(3,f,u);
assume that
A1: u = <*x0,y0,z0*> and
A2: f is_partial_differentiable_in u,3;
hereby assume A3: r = diff(F1,z0);
F1 is_differentiable_in z0 by A1,A2,Th6; then
consider N being Neighbourhood of z0 such that
A4: N c= dom F1 &
ex L,R st r=L.1 & for z st z in N holds F1.z-F1.z0 = L.(z-z0) + R.(z-z0)
by A3,FDIFF_1:def 5;
thus ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of z0 st N c= dom F1 &
ex L,R st r = L.1 & for z st z in N holds
SVF1(3,f,u).z - SVF1(3,f,u).z0 = L.(z-z0) + R.(z-z0) by A1,A4;
end;
given x1,y1,z1 being Real such that
A5: u = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st N c= dom F1 &
ex L,R st r = L.1 & for z st z in N holds
F1.z - F1.z1 = L.(z-z1) + R.(z-z1);
A6:z1 = z0 by A5,A1,FINSEQ_1:78;
F1 is_differentiable_in z0 by A1,A2,Th6;
hence thesis by A6,A5,FDIFF_1:def 5;
end;
theorem Th16:
u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1 implies
(r = partdiff(f,u,1) iff
ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(1,f,u) &
ex L,R st r = L.1 & for x st x in N holds
SVF1(1,f,u).x - SVF1(1,f,u).x0 = L.(x-x0) + R.(x-x0))
proof
assume A1:u = <*x0,y0,z0*> & f is_partial_differentiable_in u,1;
hereby assume r = partdiff(f,u,1); then
r = diff(SVF1(1,f,u),x0) by Th1,A1;
hence ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of x0 st N c= dom SVF1(1,f,u) &
ex L,R st r = L.1 & for x st x in N holds
SVF1(1,f,u).x - SVF1(1,f,u).x0 = L.(x-x0) + R.(x-x0) by Lm1,A1;
end;
given x1,y1,z1 being Real such that
A2: u = <*x1,y1,z1*> & ex N being Neighbourhood of x1 st N c= dom SVF1(1,f,u) &
ex L,R st r = L.1 & for x st x in N holds
SVF1(1,f,u).x - SVF1(1,f,u).x1 = L.(x-x1) + R.(x-x1);
r = diff(SVF1(1,f,u),x0) by A2,A1,Lm1;
hence thesis by Th1,A1;
end;
theorem Th17:
u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2 implies
(r = partdiff(f,u,2) iff
ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of y0 st N c= dom SVF1(2,f,u) &
ex L,R st r = L.1 & for y st y in N holds
SVF1(2,f,u).y - SVF1(2,f,u).y0 = L.(y-y0) + R.(y-y0))
proof
assume A1:u = <*x0,y0,z0*> & f is_partial_differentiable_in u,2;
hereby assume r = partdiff(f,u,2); then
r = diff(SVF1(2,f,u),y0) by Th2,A1;
hence ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of y0 st N c= dom SVF1(2,f,u) &
ex L,R st r = L.1 & for y st y in N holds
SVF1(2,f,u).y - SVF1(2,f,u).y0 = L.(y-y0) + R.(y-y0) by Lm2,A1;
end;
given x1,y1,z1 being Real such that
A2: u = <*x1,y1,z1*> & ex N being Neighbourhood of y1 st N c= dom SVF1(2,f,u) &
ex L,R st r = L.1 & for y st y in N holds
SVF1(2,f,u).y - SVF1(2,f,u).y1 = L.(y-y1) + R.(y-y1);
r = diff(SVF1(2,f,u),y0) by A2,A1,Lm2;
hence thesis by Th2,A1;
end;
theorem Th18:
u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3 implies
(r = partdiff(f,u,3) iff
ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of z0 st N c= dom SVF1(3,f,u) &
ex L,R st r = L.1 & for z st z in N holds
SVF1(3,f,u).z - SVF1(3,f,u).z0 = L.(z-z0) + R.(z-z0))
proof
assume A1:u = <*x0,y0,z0*> & f is_partial_differentiable_in u,3;
hereby assume r = partdiff(f,u,3); then
r = diff(SVF1(3,f,u),z0) by Th3,A1;
hence ex x0,y0,z0 being Real st u = <*x0,y0,z0*> &
ex N being Neighbourhood of z0 st N c= dom SVF1(3,f,u) &
ex L,R st r = L.1 & for z st z in N holds
SVF1(3,f,u).z - SVF1(3,f,u).z0 = L.(z-z0) + R.(z-z0) by Lm3,A1;
end;
given x1,y1,z1 being Real such that
A2: u = <*x1,y1,z1*> & ex N being Neighbourhood of z1 st N c= dom SVF1(3,f,u) &
ex L,R st r = L.1 & for z st z in N holds
SVF1(3,f,u).z - SVF1(3,f,u).z1 = L.(z-z1) + R.(z-z1);
r = diff(SVF1(3,f,u),z0) by A2,A1,Lm3;
hence thesis by Th3,A1;
end;
theorem
u = <*x0,y0,z0*> implies partdiff(f,u,1) = diff(SVF1(1,f,u),x0) by Th1;
theorem
u = <*x0,y0,z0*> implies partdiff(f,u,2) = diff(SVF1(2,f,u),y0) by Th2;
theorem
u = <*x0,y0,z0*> implies partdiff(f,u,3) = diff(SVF1(3,f,u),z0) by Th3;
definition
let f be PartFunc of REAL 3,REAL;
let D be set;
pred f is_partial_differentiable`1_on D means
D c= dom f & for u be Element of REAL 3 st u in D holds
f|D is_partial_differentiable_in u,1;
pred f is_partial_differentiable`2_on D means
D c= dom f & for u be Element of REAL 3 st u in D holds
f|D is_partial_differentiable_in u,2;
pred f is_partial_differentiable`3_on D means
D c= dom f & for u be Element of REAL 3 st u in D holds
f|D is_partial_differentiable_in u,3;
end;
theorem
f is_partial_differentiable`1_on D implies
D c= dom f & for u st u in D holds f is_partial_differentiable_in u,1
proof
assume
A1: f is_partial_differentiable`1_on D;
hence D c= dom f;
set g = f|D;
let u0 be Element of REAL 3;
assume u0 in D;then
g is_partial_differentiable_in u0,1 by A1;
then consider x0,y0,z0 being Real such that
A2: u0 = <*x0,y0,z0*> & ex N being Neighbourhood of x0
st N c= dom SVF1(1,g,u0) & ex L,R st for x st x in N holds
SVF1(1,g,u0).x - SVF1(1,g,u0).x0 = L.(x-x0) + R.(x-x0) by Th13;
consider N being Neighbourhood of x0 such that
A3: N c= dom SVF1(1,g,u0) & ex L,R st for x st x in N holds
SVF1(1,g,u0).x - SVF1(1,g,u0).x0 = L.(x-x0) + R.(x-x0) by A2;
for x st x in dom SVF1(1,g,u0) holds x in dom SVF1(1,f,u0)
proof
let x;
assume x in dom SVF1(1,g,u0);
then
A4: x in dom reproj(1,u0) & reproj(1,u0).x in dom (f|D) by FUNCT_1:11;
dom (f|D) = dom f /\ D by RELAT_1:61;then
dom (f|D) c= dom f by XBOOLE_1:17;
hence thesis by A4,FUNCT_1:11;
end;
then for x be object st x in dom SVF1(1,g,u0) holds x in dom SVF1(1,f,u0);
then dom SVF1(1,g,u0) c= dom SVF1(1,f,u0);then
A5: N c= dom SVF1(1,f,u0) by A3;
consider L,R such that
A6: for x st x in N holds SVF1(1,g,u0).x - SVF1(1,g,u0).x0 =
L.(x-x0) + R.(x-x0) by A3;
for x st x in N holds SVF1(1,f,u0).x - SVF1(1,f,u0).x0 =
L.(x-x0) + R.(x-x0)
proof
let x;
assume
A7: x in N;
A8: for x st x in dom (SVF1(1,g,u0)) holds SVF1(1,g,u0).x = SVF1(1,f,u0).x
proof
let x;
assume
A9: x in dom (SVF1(1,g,u0));
then
A10: x in dom reproj(1,u0) & reproj(1,u0).x in dom (f|D) by FUNCT_1:11;
SVF1(1,g,u0).x = (f|D).(reproj(1,u0).x) by A9,FUNCT_1:12
.= f.(reproj(1,u0).x) by A10,FUNCT_1:47
.= SVF1(1,f,u0).x by A10,FUNCT_1:13;
hence thesis;
end;
A11: x0 in N by RCOMP_1:16;
L.(x-x0) + R.(x-x0) = SVF1(1,g,u0).x - SVF1(1,g,u0).x0 by A6,A7
.= SVF1(1,f,u0).x - SVF1(1,g,u0).x0 by A3,A7,A8
.= SVF1(1,f,u0).x - SVF1(1,f,u0).x0 by A3,A8,A11;
hence thesis;
end;
hence thesis by A2,A5,Th13;
end;
theorem
f is_partial_differentiable`2_on D implies
D c= dom f & for u st u in D holds f is_partial_differentiable_in u,2
proof
assume
A1: f is_partial_differentiable`2_on D;
hence D c= dom f;
set g = f|D;
let u0 be Element of REAL 3;
assume u0 in D;then
g is_partial_differentiable_in u0,2 by A1;
then consider x0,y0,z0 being Real such that
A2: u0 = <*x0,y0,z0*> & ex N being Neighbourhood of y0
st N c= dom SVF1(2,g,u0) & ex L,R st for y st y in N holds
SVF1(2,g,u0).y - SVF1(2,g,u0).y0 = L.(y-y0) + R.(y-y0) by Th14;
consider N being Neighbourhood of y0 such that
A3: N c= dom SVF1(2,g,u0) & ex L,R st for y st y in N holds
SVF1(2,g,u0).y - SVF1(2,g,u0).y0 = L.(y-y0) + R.(y-y0) by A2;
for y st y in dom (SVF1(2,g,u0)) holds y in dom (SVF1(2,f,u0))
proof
let y;
assume y in dom (SVF1(2,g,u0));
then
A4: y in dom reproj(2,u0) & reproj(2,u0).y in dom (f|D) by FUNCT_1:11;
dom (f|D) = dom f /\ D by RELAT_1:61;then
dom (f|D) c= dom f by XBOOLE_1:17;
hence thesis by A4,FUNCT_1:11;
end;
then for y be object st y in dom (SVF1(2,g,u0))
holds y in dom (SVF1(2,f,u0));
then dom (SVF1(2,g,u0)) c= dom (SVF1(2,f,u0));then
A5: N c= dom (SVF1(2,f,u0)) by A3;
consider L,R such that
A6: for y st y in N holds SVF1(2,g,u0).y - SVF1(2,g,u0).y0 =
L.(y-y0) + R.(y-y0) by A3;
for y st y in N holds SVF1(2,f,u0).y - SVF1(2,f,u0).y0 =
L.(y-y0) + R.(y-y0)
proof
let y;
assume
A7: y in N;
A8: for y st y in dom SVF1(2,g,u0) holds SVF1(2,g,u0).y = SVF1(2,f,u0).y
proof
let y;
assume
A9: y in dom (SVF1(2,g,u0));
then
A10: y in dom reproj(2,u0) & reproj(2,u0).y in dom (f|D) by FUNCT_1:11;
SVF1(2,g,u0).y = (f|D).(reproj(2,u0).y) by A9,FUNCT_1:12
.= f.(reproj(2,u0).y) by A10,FUNCT_1:47
.= SVF1(2,f,u0).y by A10,FUNCT_1:13;
hence thesis;
end;
A11: y0 in N by RCOMP_1:16;
L.(y-y0) + R.(y-y0) = SVF1(2,g,u0).y - SVF1(2,g,u0).y0 by A6,A7
.= SVF1(2,f,u0).y - SVF1(2,g,u0).y0 by A3,A7,A8
.= SVF1(2,f,u0).y - SVF1(2,f,u0).y0 by A3,A8,A11;
hence thesis;
end;
hence thesis by A2,A5,Th14;
end;
theorem
f is_partial_differentiable`3_on D implies
D c= dom f & for u st u in D holds f is_partial_differentiable_in u,3
proof
assume
A1: f is_partial_differentiable`3_on D;
hence D c= dom f;
set g = f|D;
let u0 be Element of REAL 3;
assume u0 in D;then
g is_partial_differentiable_in u0,3 by A1;
then consider x0,y0,z0 being Real such that
A2: u0 = <*x0,y0,z0*> & ex N being Neighbourhood of z0
st N c= dom SVF1(3,g,u0) & ex L,R st for z st z in N holds
SVF1(3,g,u0).z - SVF1(3,g,u0).z0 = L.(z-z0) + R.(z-z0)
by Th15;
consider N being Neighbourhood of z0 such that
A3: N c= dom SVF1(3,g,u0) & ex L,R st for z st z in N holds
SVF1(3,g,u0).z - SVF1(3,g,u0).z0 = L.(z-z0) + R.(z-z0) by A2;
for z st z in dom (SVF1(3,g,u0)) holds z in dom (SVF1(3,f,u0))
proof
let z;
assume z in dom (SVF1(3,g,u0));
then
A4: z in dom reproj(3,u0) & reproj(3,u0).z in dom (f|D) by FUNCT_1:11;
dom (f|D) = dom f /\ D by RELAT_1:61;then
dom (f|D) c= dom f by XBOOLE_1:17;
hence thesis by A4,FUNCT_1:11;
end;
then for z be object st z in dom (SVF1(3,g,u0))
holds z in dom (SVF1(3,f,u0));
then dom (SVF1(3,g,u0)) c= dom (SVF1(3,f,u0));then
A5: N c= dom (SVF1(3,f,u0)) by A3;
consider L,R such that
A6: for z st z in N holds SVF1(3,g,u0).z - SVF1(3,g,u0).z0 =
L.(z-z0) + R.(z-z0) by A3;
for z st z in N holds SVF1(3,f,u0).z - SVF1(3,f,u0).z0 =
L.(z-z0) + R.(z-z0)
proof
let z;
assume
A7: z in N;
A8: for z st z in dom SVF1(3,g,u0) holds SVF1(3,g,u0).z = SVF1(3,f,u0).z
proof
let z;
assume
A9: z in dom (SVF1(3,g,u0));
then
A10: z in dom reproj(3,u0) & reproj(3,u0).z in dom (f|D) by FUNCT_1:11;
SVF1(3,g,u0).z = (f|D).(reproj(3,u0).z) by A9,FUNCT_1:12
.= f.(reproj(3,u0).z) by A10,FUNCT_1:47
.= SVF1(3,f,u0).z by A10,FUNCT_1:13;
hence thesis;
end;
A11: z0 in N by RCOMP_1:16;
L.(z-z0) + R.(z-z0) = SVF1(3,g,u0).z - SVF1(3,g,u0).z0 by A6,A7
.= SVF1(3,f,u0).z - SVF1(3,g,u0).z0 by A3,A7,A8
.= SVF1(3,f,u0).z - SVF1(3,f,u0).z0 by A3,A8,A11;
hence thesis;
end;
hence thesis by A2,A5,Th15;
end;
definition
let f be PartFunc of REAL 3,REAL;
let D be set;
assume A1: f is_partial_differentiable`1_on D;
func f`partial1|D -> PartFunc of REAL 3,REAL means
dom it = D & for u be Element of REAL 3 st u in D holds
it.u = partdiff(f,u,1);
existence
proof
defpred P[Element of REAL 3] means $1 in D;
deffunc F(Element of REAL 3) = In(partdiff(f,$1,1),REAL);
consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
for u be Element of REAL 3 st u in dom F holds F.u = F(u)
from SEQ_1:sch 3;
take F;
for y be object st y in dom F holds y in D by A2;then
A3: dom F c= D;
now
let y be object such that
A4: y in D;
D c= dom f by A1;
then D is Subset of REAL 3 by XBOOLE_1:1;
hence y in dom F by A2,A4;
end;
then D c= dom F;
hence dom F = D by A3;
let u be Element of REAL 3;
assume u in D;
then u in dom F by A2;
then F.u = F(u) by A2;
hence thesis;
end;
uniqueness
proof
let F,G be PartFunc of REAL 3,REAL;
assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
F.u = partdiff(f,u,1) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
G.u = partdiff(f,u,1);
now
let u be Element of REAL 3;
assume
A7: u in dom F;
then F.u = partdiff(f,u,1) by A5;
hence F.u = G.u by A5,A6,A7;
end;
hence thesis by A5,A6,PARTFUN1:5;
end;
end;
definition
let f be PartFunc of REAL 3,REAL;
let D be set;
assume A1: f is_partial_differentiable`2_on D;
func f`partial2|D -> PartFunc of REAL 3,REAL means
dom it = D & for u be Element of REAL 3 st u in D holds
it.u = partdiff(f,u,2);
existence
proof
defpred P[Element of REAL 3] means $1 in D;
deffunc F(Element of REAL 3) = In(partdiff(f,$1,2),REAL);
consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
for u be Element of REAL 3 st u in dom F holds F.u = F(u)
from SEQ_1:sch 3;
take F;
for y be object st y in dom F holds y in D by A2;then
A3: dom F c= D;
now
let y be object such that
A4: y in D;
D c= dom f by A1;
then D is Subset of REAL 3 by XBOOLE_1:1;
hence y in dom F by A2,A4;
end;
then D c= dom F;
hence dom F = D by A3;
let u be Element of REAL 3;
assume u in D;
then u in dom F by A2;
then F.u = F(u) by A2;
hence thesis;
end;
uniqueness
proof
let F,G be PartFunc of REAL 3,REAL;
assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
F.u = partdiff(f,u,2) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
G.u = partdiff(f,u,2);
now
let u be Element of REAL 3;
assume
A7: u in dom F;
then F.u = partdiff(f,u,2) by A5;
hence F.u = G.u by A5,A6,A7;
end;
hence thesis by A5,A6,PARTFUN1:5;
end;
end;
definition
let f be PartFunc of REAL 3,REAL;
let D be set;
assume A1: f is_partial_differentiable`3_on D;
func f`partial3|D -> PartFunc of REAL 3,REAL means
dom it = D & for u be Element of REAL 3 st u in D holds
it.u = partdiff(f,u,3);
existence
proof
defpred P[Element of REAL 3] means $1 in D;
deffunc F(Element of REAL 3) = In(partdiff(f,$1,3),REAL);
consider F being PartFunc of REAL 3,REAL such that
A2: (for u be Element of REAL 3 holds u in dom F iff P[u]) &
for u be Element of REAL 3 st u in dom F holds F.u = F(u)
from SEQ_1:sch 3;
take F;
for y be object st y in dom F holds y in D by A2;then
A3: dom F c= D;
now
let y be object such that
A4: y in D;
D c= dom f by A1;
then D is Subset of REAL 3 by XBOOLE_1:1;
hence y in dom F by A2,A4;
end;
then D c= dom F;
hence dom F = D by A3;
let u be Element of REAL 3;
assume u in D;
then u in dom F by A2;
then F.u = F(u) by A2;
hence thesis;
end;
uniqueness
proof
let F,G be PartFunc of REAL 3,REAL;
assume that
A5: dom F = D & for u be Element of REAL 3 st u in D holds
F.u = partdiff(f,u,3) and
A6: dom G = D & for u be Element of REAL 3 st u in D holds
G.u = partdiff(f,u,3);
now
let u be Element of REAL 3;
assume
A7: u in dom F;
then F.u = partdiff(f,u,3) by A5;
hence F.u = G.u by A5,A6,A7;
end;
hence thesis by A5,A6,PARTFUN1:5;
end;
end;
begin :: Main Properties of Partial Differentiation of Real Ternary Functions
theorem
for u0 being Element of REAL 3 for N being Neighbourhood of proj(1,3).u0 st
f is_partial_differentiable_in u0,1 & N c= dom SVF1(1,f,u0) holds
for h be 0-convergent non-zero Real_Sequence,
c be constant Real_Sequence st rng c = {proj(1,3).u0} & rng (h+c) c= N
holds h"(#)(SVF1(1,f,u0)/*(h+c) - SVF1(1,f,u0)/*c) is convergent &
partdiff(f,u0,1) = lim (h"(#)(SVF1(1,f,u0)/*(h+c) - SVF1(1,f,u0)/*c))
proof
let u0 be Element of REAL 3;
let N be Neighbourhood of proj(1,3).u0;
assume
A1: f is_partial_differentiable_in u0,1 & N c= dom SVF1(1,f,u0);
let h be 0-convergent non-zero Real_Sequence,
c be constant Real_Sequence such that
A2: rng c = {proj(1,3).u0} & rng (h+c) c= N;
consider x0,y0,z0 being Real such that
A3: u0 = <*x0,y0,z0*> & ex N1 being Neighbourhood of x0
st N1 c= dom SVF1(1,f,u0) & ex L,R st for x st x in N1 holds
SVF1(1,f,u0).x - SVF1(1,f,u0).x0 = L.(x-x0) + R.(x-x0) by A1,Th13;
consider N1 be Neighbourhood of x0 such that
A4: N1 c= dom SVF1(1,f,u0) & ex L,R st for x st x in N1 holds
SVF1(1,f,u0).x - SVF1(1,f,u0).x0 = L.(x-x0) + R.(x-x0) by A3;
consider L,R such that
A5: for x st x in N1 holds
SVF1(1,f,u0).x - SVF1(1,f,u0).x0 = L.(x-x0) + R.(x-x0) by A4;
A6: proj(1,3).u0 = x0 by A3,Th1;
then consider N2 be Neighbourhood of x0 such that
A7: N2 c= N & N2 c= N1 by RCOMP_1:17;
consider g be Real such that
A8: 0 < g & N2 = ].x0-g,x0+g.[ by RCOMP_1:def 6;
A9: x0 in N2
proof
A10: x0 + 0 < x0 + g by A8,XREAL_1:8;
x0 - g < x0 - 0 by A8,XREAL_1:44;
hence thesis by A8,A10;
end;
ex n st rng (c^\n) c= N2 & rng ((h+c)^\n) c= N2
proof
x0 in rng c by A2,A6,TARSKI:def 1;then
A11: lim c = x0 by SEQ_4:25;
h is convergent & lim h = 0;then
A12: lim (h+c) = 0+x0 by A11,SEQ_2:6
.= x0;
consider n being Nat such that
A13: for m being Nat st n <= m holds |.(h+c).m-x0.| < g
by A8,A12,SEQ_2:def 7;
A14: rng (c^\n) = {x0} by A2,A6,VALUED_0:26;
reconsider n as Element of NAT by ORDINAL1:def 12;
take n;
thus rng (c^\n) c= N2
by A9,A14,TARSKI:def 1;
let y be object;
assume y in rng ((h+c)^\n);
then consider m such that
A15: y = ((h+c)^\n).m by FUNCT_2:113;
n + 0 <= n+m by XREAL_1:7;
then |.(h+c).(n+m)-x0.|<g by A13;
then -g < (h+c).(m+n) - x0 & (h+c).(m+n) - x0 < g by SEQ_2:1;
then -g < ((h+c)^\n).m - x0 & ((h+c)^\n).m - x0 < g by NAT_1:def 3;
then
x0 +-g < ((h+c)^\n).m & ((h+c)^\n).m < x0 + g by XREAL_1:19,20;
hence thesis by A8,A15;
end;
then consider n such that
A16: rng (c^\n) c= N2 & rng ((h+c)^\n) c= N2;
A17: rng (c^\n) c= dom SVF1(1,f,u0)
proof
let y be object;
A18: rng (c^\n) = rng c by VALUED_0:26;
assume y in rng (c^\n);
then y = x0 by A2,A6,A18,TARSKI:def 1;
then y in N by A7,A9;
hence thesis by A1;
end;
A19: rng ((h+c)^\n) c= dom SVF1(1,f,u0)
by A16,A7,A1;
A20: rng c c= dom SVF1(1,f,u0)
proof
let y be object;
assume y in rng c;
then y = x0 by A2,A6,TARSKI:def 1;
then y in N by A7,A9;
hence thesis by A1;
end;
A21: rng (h+c) c= dom SVF1(1,f,u0)
by A2,A1;
A22: for x st x in N2 holds
SVF1(1,f,u0).x - SVF1(1,f,u0).x0 = L.(x-x0) + R.(x-x0) by A5,A7;
A23: for k holds SVF1(1,f,u0).(((h+c)^\n).k) - SVF1(1,f,u0).((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
A24: ((h+c)^\n).k in N2 by A16;
A25: ((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;
A26: (c^\n).k in rng (c^\n) by VALUED_0:28;
rng (c^\n) = rng c by VALUED_0:26;
then (c^\n).k = x0 by A2,A6,A26,TARSKI:def 1;
hence thesis by A5,A7,A24,A25;
end;
A27: L is total by FDIFF_1:def 3;
A28: R is total by FDIFF_1:def 2;
A29: SVF1(1,f,u0)/*((h+c)^\n) - SVF1(1,f,u0)/*(c^\n) = L/*(h^\n) + R/*(h^\n)
proof
now
let k;
thus (SVF1(1,f,u0)/*((h+c)^\n) - SVF1(1,f,u0)/*(c^\n)).k
= (SVF1(1,f,u0)/*((h+c)^\n)).k - (SVF1(1,f,u0)/*(c^\n)).k
by RFUNCT_2:1
.= SVF1(1,f,u0).(((h+c)^\n).k) - (SVF1(1,f,u0)/*(c^\n)).k
by A19,FUNCT_2:108
.= SVF1(1,f,u0).(((h+c)^\n).k) - SVF1(1,f,u0).((c^\n).k)
by A17,FUNCT_2:108
.= L.((h^\n).k) + R.((h^\n).k) by A23
.= (L/*(h^\n)).k + R.((h^\n).k) by A27,FUNCT_2:115
.= (L/*(h^\n)).k + (R/*(h^\n)).k by A28,FUNCT_2:115
.= (L/*(h^\n) + R/*(h^\n)).k by SEQ_1:7;
end;
hence thesis by FUNCT_2:63;
end;
A30: (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 be Real_Sequence such that
A31: for k being Nat holds s1.k = F(k) from SEQ_1:sch 1;
consider s such that
A32: for p1 be Real holds L.p1 = s*p1 by FDIFF_1:def 3;
A33: L.1 = s*1 by A32
.= s;
now
let m;
A34: (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 A27,FUNCT_2:115
.= (s*((h^\n).m))*((h^\n).m)" + ((R/*(h^\n))(#)(h^\n)").m by A32
.= s*(((h^\n).m)*((h^\n).m)") + ((R/*(h^\n))(#)(h^\n)").m
.= s*1 + ((R/*(h^\n))(#)(h^\n)").m by A34,XCMPLX_0:def 7
.= s1.m by A31,A33;
end;
then
A35: (L/*(h^\n) + R/*(h^\n))(#)(h^\n)" = s1 by FUNCT_2:63;
A36: now
let r be Real such that
A37: 0 < r;
((h^\n)")(#)(R/*(h^\n)) is convergent &
lim (((h^\n)")(#)(R/*(h^\n))) = 0 by FDIFF_1:def 2;
then consider m being Nat such that
A38: for k being Nat st m <= k holds
|.(((h^\n)")(#)(R/*(h^\n))).k-0 .| < r by A37,SEQ_2:def 7;
take n1 = m;
let k be Nat such that
A39: n1 <= k;
|.s1.k-L.1.| = |.L.1+((R/*(h^\n))(#)(h^\n)").k-L.1 .| by A31
.= |.(((h^\n)")(#)(R/*(h^\n))).k-0 .|;
hence |.s1.k-L.1.| < r by A38,A39;
end;
hence (L/*(h^\n)+R/*(h^\n))(#)(h^\n)" is convergent by A35,SEQ_2:def 6;
hence thesis by A35,A36,SEQ_2:def 7;
end;
A40: N2 c= dom SVF1(1,f,u0) by A1,A7;
A41: ((L/*(h^\n)+R/*(h^\n))(#)(h^\n)")
= ((((SVF1(1,f,u0)/*(h+c))^\n)-SVF1(1,f,u0)/*(c^\n))(#)(h^\n)")
by A21,A29,VALUED_0:27
.= ((((SVF1(1,f,u0)/*(h+c))^\n)-((SVF1(1,f,u0)/*c)^\n))(#)(h^\n)")
by A20,VALUED_0:27
.= ((((SVF1(1,f,u0)/*(h+c))-(SVF1(1,f,u0)/*c))^\n)(#)(h^\n)") by SEQM_3:17
.= ((((SVF1(1,f,u0)/*(h+c))-(SVF1(1,f,u0)/*c))^\n)(#)((h")^\n))
by SEQM_3:18
.= ((((SVF1(1,f,u0)/*(h+c))-(SVF1(1,f,u0)/*c))(#) h")^\n)
by SEQM_3:19;then
A42: L.1 = lim ((h")(#)((SVF1(1,f,u0)/*(h+c))-(SVF1(1,f,u0)/*c)))
by A30,SEQ_4:22;
thus h"(#)(SVF1(1,f,u0)/*(h+c)-SVF1(1,f,u0)/*c) is convergent
by A30,A41,SEQ_4:21;
thus thesis by A1,A3,A22,A40,A42,Th16;
end;
theorem
for u0 being Element of REAL 3 for N being Neighbourhood of proj(2,3).u0 st
f is_partial_differentiable_in u0,2 & N c= dom SVF1(2,f,u0) holds
for h be 0-convergent non-zero Real_Sequence,
c be constant Real_Sequence st rng c = {proj(2,3).u0} & rng (h+c) c= N
holds h"(#)(SVF1(2,f,u0)/*(h+c) - SVF1(2,f,u0)/*c) is convergent &
partdiff(f,u0,2) = lim (h"(#)(SVF1(2,f,u0)/*(h+c) - SVF1(2,f,u0)/*c))
proof
let u0 be Element of REAL 3;
let N be Neighbourhood of proj(2,3).u0;
assume
A1: f is_partial_differentiable_in u0,2 & N c= dom SVF1(2,f,u0);
let h be 0-convergent non-zero Real_Sequence,
c be constant Real_Sequence such that
A2: rng c = {proj(2,3).u0} & rng (h+c) c= N;
consider x0,y0,z0 being Real such that
A3: u0 = <*x0,y0,z0*> & ex N1 being Neighbourhood of y0
st N1 c= dom SVF1(2,f,u0) & ex L,R st for y st y in N1 holds
SVF1(2,f,u0).y - SVF1(2,f,u0).y0 = L.(y-y0) + R.(y-y0) by A1,Th14;
consider N1 be Neighbourhood of y0 such that
A4: N1 c= dom SVF1(2,f,u0) & ex L,R st for y st y in N1 holds
SVF1(2,f,u0).y - SVF1(2,f,u0).y0 = L.(y-y0) + R.(y-y0) by A3;
consider L,R such that
A5: for y st y in N1 holds
SVF1(2,f,u0).y - SVF1(2,f,u0).y0 = L.(y-y0) + R.(y-y0) by A4;
A6: proj(2,3).u0 = y0 by A3,Th2;
then consider N2 be Neighbourhood of y0 such that
A7: N2 c= N & N2 c= N1 by RCOMP_1:17;
consider g be Real such that
A8: 0 < g & N2 = ].y0-g,y0+g.[ by RCOMP_1:def 6;
A9: y0 in N2
proof
A10: y0 + 0 < y0 + g by A8,XREAL_1:8;
y0 - g < y0 - 0 by A8,XREAL_1:44;
hence thesis by A8,A10;
end;
ex n st rng (c^\n) c= N2 & rng ((h+c)^\n) c= N2
proof
y0 in rng c by A2,A6,TARSKI:def 1;then
A11: lim c = y0 by SEQ_4:25;
h is convergent & lim h = 0;then
A12: lim (h+c) = 0+y0 by A11,SEQ_2:6
.= y0;
consider n being Nat such that
A13: for m being Nat st n <= m holds |.(h+c).m-y0.| < g
by A8,A12,SEQ_2:def 7;
A14: rng (c^\n) = {y0} by A2,A6,VALUED_0:26;
reconsider n as Element of NAT by ORDINAL1:def 12;
take n;
thus rng (c^\n) c= N2
by A9,A14,TARSKI:def 1;
let y be object;
assume y in rng ((h+c)^\n);
then consider m such that
A15: y = ((h+c)^\n).m by FUNCT_2:113;
n + 0 <= n+m by XREAL_1:7;
then |.(h+c).(n+m)-y0.|<g by A13;
then -g < (h+c).(m+n) - y0 & (h+c).(m+n) - y0 < g by SEQ_2:1;
then -g < ((h+c)^\n).m - y0 & ((h+c)^\n).m - y0 < g by NAT_1:def 3;
then
y0 +-g < ((h+c)^\n).m & ((h+c)^\n).m < y0 + g by XREAL_1:19,20;
hence thesis by A8,A15;
end;
then consider n such that
A16: rng (c^\n) c= N2 & rng ((h+c)^\n) c= N2;
A17: rng (c^\n) c= dom SVF1(2,f,u0)
proof
let y be object;
A18: rng (c^\n) = rng c by VALUED_0:26;
assume y in rng (c^\n);
then y = y0 by A2,A6,A18,TARSKI:def 1;
then y in N by A7,A9;
hence thesis by A1;
end;
A19: rng ((h+c)^\n) c= dom SVF1(2,f,u0)
by A16,A7,A1;
A20: rng c c= dom SVF1(2,f,u0)
proof
let y be object;
assume y in rng c;
then y = y0 by A2,A6,TARSKI:def 1;
then y in N by A7,A9;
hence thesis by A1;
end;
A21: rng (h+c) c= dom SVF1(2,f,u0)
by A2,A1;
A22: for y st y in N2 holds
SVF1(2,f,u0).y - SVF1(2,f,u0).y0 = L.(y-y0) + R.(y-y0) by A5,A7;
A23: for k holds SVF1(2,f,u0).(((h+c)^\n).k) - SVF1(2,f,u0).((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
A24: ((h+c)^\n).k in N2 by A16;
A25: ((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;
A26: (c^\n).k in rng (c^\n) by VALUED_0:28;
rng (c^\n) = rng c by VALUED_0:26;
then (c^\n).k = y0 by A2,A6,A26,TARSKI:def 1;
hence thesis by A5,A7,A24,A25;
end;
A27: L is total by FDIFF_1:def 3;
A28: R is total by FDIFF_1:def 2;
A29: SVF1(2,f,u0)/*((h+c)^\n) - SVF1(2,f,u0)/*(c^\n) = L/*(h^\n) + R/*(h^\n)
proof
now
let k;
thus (SVF1(2,f,u0)/*((h+c)^\n) - SVF1(2,f,u0)/*(c^\n)).k
= (SVF1(2,f,u0)/*((h+c)^\n)).k - (SVF1(2,f,u0)/*(c^\n)).k
by RFUNCT_2:1
.= SVF1(2,f,u0).(((h+c)^\n).k) - (SVF1(2,f,u0)/*(c^\n)).k
by A19,FUNCT_2:108
.= SVF1(2,f,u0).(((h+c)^\n).k) - SVF1(2,f,u0).((c^\n).k)
by A17,FUNCT_2:108
.= L.((h^\n).k) + R.((h^\n).k) by A23
.= (L/*(h^\n)).k + R.((h^\n).k) by A27,FUNCT_2:115
.= (L/*(h^\n)).k + (R/*(h^\n)).k by A28,FUNCT_2:115
.= (L/*(h^\n) + R/*(h^\n)).k by SEQ_1:7;
end;
hence thesis by FUNCT_2:63;
end;
A30: (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 be Real_Sequence such that
A31: for k being Nat holds s1.k = F(k) from SEQ_1:sch 1;
consider s such that
A32: for p1 be Real holds L.p1 = s*p1 by FDIFF_1:def 3;
A33: L.1 = s*1 by A32
.= s;
now
let m;
A34: (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 A27,FUNCT_2:115
.= (s*((h^\n).m))*((h^\n).m)" + ((R/*(h^\n))(#)(h^\n)").m by A32
.= s*(((h^\n).m)*((h^\n).m)") + ((R/*(h^\n))(#)(h^\n)").m
.= s*1 + ((R/*(h^\n))(#)(h^\n)").m by A34,XCMPLX_0:def 7
.= s1.m by A31,A33;
end;
then
A35: (L/*(h^\n) + R/*(h^\n))(#)(h^\n)" = s1 by FUNCT_2:63;
A36: now
let r be Real such that
A37: 0 < r;
((h^\n)")(#)(R/*(h^\n)) is convergent &
lim (((h^\n)")(#)(R/*(h^\n))) = 0 by FDIFF_1:def 2;
then consider m being Nat such that
A38: for k being Nat st m <= k holds
|.(((h^\n)")(#)(R/*(h^\n))).k-0 .| < r by A37,SEQ_2:def 7;
take n1 = m;
let k be Nat such that
A39: n1 <= k;
|.s1.k-L.1.| = |.L.1+((R/*(h^\n))(#)(h^\n)").k-L.1 .| by A31
.= |.(((h^\n)")(#)(R/*(h^\n))).k-0 .|;
hence |.s1.k-L.1.| < r by A38,A39;
end;
hence (L/*(h^\n)+R/*(h^\n))(#)(h^\n)" is convergent by A35,SEQ_2:def 6;
hence thesis by A35,A36,SEQ_2:def 7;
end;
A40: N2 c= dom SVF1(2,f,u0) by A1,A7;
A41: ((L/*(h^\n)+R/*(h^\n))(#)(h^\n)")
= ((((SVF1(2,f,u0)/*(h+c))^\n)-SVF1(2,f,u0)/*(c^\n))(#)(h^\n)")
by A21,A29,VALUED_0:27
.= ((((SVF1(2,f,u0)/*(h+c))^\n)-((SVF1(2,f,u0)/*c)^\n))(#)(h^\n)")
by A20,VALUED_0:27
.= ((((SVF1(2,f,u0)/*(h+c))-(SVF1(2,f,u0)/*c))^\n)(#)(h^\n)") by SEQM_3:17
.= ((((SVF1(2,f,u0)/*(h+c))-(SVF1(2,f,u0)/*c))^\n)(#)((h")^\n))
by SEQM_3:18
.= ((((SVF1(2,f,u0)/*(h+c))-(SVF1(2,f,u0)/*c))(#) h")^\n)
by SEQM_3:19;then
A42: L.1 = lim ((h")(#)((SVF1(2,f,u0)/*(h+c))-(SVF1(2,f,u0)/*c)))
by A30,SEQ_4:22;
thus h"(#)(SVF1(2,f,u0)/*(h+c)-SVF1(2,f,u0)/*c) is convergent
by A30,A41,SEQ_4:21;
thus thesis by A1,A3,A22,A40,A42,Th17;
end;
theorem
for u0 being Element of REAL 3 for N being Neighbourhood of proj(3,3).u0 st
f is_partial_differentiable_in u0,3 & N c= dom SVF1(3,f,u0) holds
for h be 0-convergent non-zero Real_Sequence,
c be constant Real_Sequence st rng c = {proj(3,3).u0} & rng (h+c) c= N
holds h"(#)(SVF1(3,f,u0)/*(h+c) - SVF1(3,f,u0)/*c) is convergent &
partdiff(f,u0,3) = lim (h"(#)(SVF1(3,f,u0)/*(h+c) - SVF1(3,f,u0)/*c))
proof
let u0 be Element of REAL 3;
let N be Neighbourhood of proj(3,3).u0;
assume
A1: f is_partial_differentiable_in u0,3 & N c= dom SVF1(3,f,u0);
let h be 0-convergent non-zero Real_Sequence,
c be constant Real_Sequence such that
A2: rng c = {proj(3,3).u0} & rng (h+c) c= N;
consider x0,y0,z0 being Real such that
A3: u0 = <*x0,y0,z0*> & ex N1 being Neighbourhood of z0
st N1 c= dom SVF1(3,f,u0) & ex L,R st for z st z in N1 holds
SVF1(3,f,u0).z - SVF1(3,f,u0).z0 = L.(z-z0) + R.(z-z0)
by A1,Th15;
consider N1 be Neighbourhood of z0 such that
A4: N1 c= dom SVF1(3,f,u0) & ex L,R st for z st z in N1 holds
SVF1(3,f,u0).z - SVF1(3,f,u0).z0 = L.(z-z0) + R.(z-z0) by A3;
consider L,R such that
A5: for z st z in N1 holds
SVF1(3,f,u0).z - SVF1(3,f,u0).z0 = L.(z-z0) + R.(z-z0) by A4;
A6: proj(3,3).u0 = z0 by A3,Th3;
then consider N2 be Neighbourhood of z0 such that
A7: N2 c= N & N2 c= N1 by RCOMP_1:17;
consider g be Real such that
A8: 0 < g & N2 = ].z0-g,z0+g.[ by RCOMP_1:def 6;
A9: z0 in N2
proof
A10: z0 + 0 < z0 + g by A8,XREAL_1:8;
z0 - g < z0 - 0 by A8,XREAL_1:44;
hence thesis by A8,A10;
end;
ex n st rng (c^\n) c= N2 & rng ((h+c)^\n) c= N2
proof
z0 in rng c by A2,A6,TARSKI:def 1;then
A11: lim c = z0 by SEQ_4:25;
h is convergent & lim h = 0;then
A12: lim (h+c) = 0+z0 by A11,SEQ_2:6
.= z0;
consider n being Nat such that
A13: for m being Nat st n <= m holds |.(h+c).m-z0.| < g
by A8,A12,SEQ_2:def 7;
A14: rng (c^\n) = {z0} by A2,A6,VALUED_0:26;
reconsider n as Element of NAT by ORDINAL1:def 12;
take n;
thus rng (c^\n) c= N2
by A9,A14,TARSKI:def 1;
let z be object;
assume z in rng ((h+c)^\n);
then consider m such that
A15: z = ((h+c)^\n).m by FUNCT_2:113;
n + 0 <= n+m by XREAL_1:7;
then |.(h+c).(n+m)-z0.|<g by A13;
then -g < (h+c).(m+n) - z0 & (h+c).(m+n) - z0 < g by SEQ_2:1;
then -g < ((h+c)^\n).m - z0 & ((h+c)^\n).m - z0 < g by NAT_1:def 3;
then
z0 +-g < ((h+c)^\n).m & ((h+c)^\n).m < z0 + g by XREAL_1:19,20;
hence thesis by A8,A15;
end;
then consider n such that
A16: rng (c^\n) c= N2 & rng ((h+c)^\n) c= N2;
A17: rng (c^\n) c= dom SVF1(3,f,u0)
proof
let z be object;
A18: rng (c^\n) = rng c by VALUED_0:26;
assume z in rng (c^\n);
then z = z0 by A2,A6,A18,TARSKI:def 1;
then z in N by A7,A9;
hence thesis by A1;
end;
A19: rng ((h+c)^\n) c= dom SVF1(3,f,u0)
by A16,A7,A1;
A20: rng c c= dom SVF1(3,f,u0)
proof
let z be object;
assume z in rng c;
then z = z0 by A2,A6,TARSKI:def 1;
then z in N by A7,A9;
hence thesis by A1;
end;
A21: rng (h+c) c= dom SVF1(3,f,u0)
by A2,A1;
A22: for z st z in N2 holds
SVF1(3,f,u0).z - SVF1(3,f,u0).z0 = L.(z-z0) + R.(z-z0) by A5,A7;
A23: for k holds SVF1(3,f,u0).(((h+c)^\n).k) - SVF1(3,f,u0).((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
A24: ((h+c)^\n).k in N2 by A16;
A25: ((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;
A26: (c^\n).k in rng (c^\n) by VALUED_0:28;
rng (c^\n) = rng c by VALUED_0:26;
then (c^\n).k = z0 by A2,A6,A26,TARSKI:def 1;
hence thesis by A5,A7,A24,A25;
end;
A27: L is total by FDIFF_1:def 3;
A28: R is total by FDIFF_1:def 2;
A29: SVF1(3,f,u0)/*((h+c)^\n) - SVF1(3,f,u0)/*(c^\n) = L/*(h^\n) + R/*(h^\n)
proof
now
let k;
thus (SVF1(3,f,u0)/*((h+c)^\n) - SVF1(3,f,u0)/*(c^\n)).k
= (SVF1(3,f,u0)/*((h+c)^\n)).k - (SVF1(3,f,u0)/*(c^\n)).k
by RFUNCT_2:1
.= SVF1(3,f,u0).(((h+c)^\n).k) - (SVF1(3,f,u0)/*(c^\n)).k
by A19,FUNCT_2:108
.= SVF1(3,f,u0).(((h+c)^\n).k) - SVF1(3,f,u0).((c^\n).k)
by A17,FUNCT_2:108
.= L.((h^\n).k) + R.((h^\n).k) by A23
.= (L/*(h^\n)).k + R.((h^\n).k) by A27,FUNCT_2:115
.= (L/*(h^\n)).k + (R/*(h^\n)).k by A28,FUNCT_2:115
.= (L/*(h^\n) + R/*(h^\n)).k by SEQ_1:7;
end;
hence thesis by FUNCT_2:63;
end;
A30: (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 be Real_Sequence such that
A31: for k being Nat holds s1.k = F(k) from SEQ_1:sch 1;
consider s such that
A32: for p1 being Real holds L.p1 = s*p1 by FDIFF_1:def 3;
A33: L.1 = s*1 by A32
.= s;
now
let m;
A34: (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 A27,FUNCT_2:115
.= (s*((h^\n).m))*((h^\n).m)" + ((R/*(h^\n))(#)(h^\n)").m by A32
.= s*(((h^\n).m)*((h^\n).m)") + ((R/*(h^\n))(#)(h^\n)").m
.= s*1 + ((R/*(h^\n))(#)(h^\n)").m by A34,XCMPLX_0:def 7
.= s1.m by A31,A33;
end; then
A35: (L/*(h^\n) + R/*(h^\n))(#)(h^\n)" = s1 by FUNCT_2:63;
A36: now
let r be Real such that
A37: 0 < r;
((h^\n)")(#)(R/*(h^\n)) is convergent &
lim (((h^\n)")(#)(R/*(h^\n))) = 0 by FDIFF_1:def 2;
then consider m being Nat such that
A38: for k being Nat st m <= k holds
|.(((h^\n)")(#)(R/*(h^\n))).k-0 .| < r by A37,SEQ_2:def 7;
take n1 = m;
let k be Nat such that
A39: n1 <= k;
|.s1.k-L.1.| = |.L.1+((R/*(h^\n))(#)(h^\n)").k-L.1 .| by A31
.= |.(((h^\n)")(#)(R/*(h^\n))).k-0 .|;
hence |.s1.k-L.1.| < r by A38,A39;
end;
hence (L/*(h^\n)+R/*(h^\n))(#)(h^\n)" is convergent by A35,SEQ_2:def 6;
hence thesis by A35,A36,SEQ_2:def 7;
end;
A40: N2 c= dom SVF1(3,f,u0) by A1,A7;
A41: ((L/*(h^\n)+R/*(h^\n))(#)(h^\n)")
= ((((SVF1(3,f,u0)/*(h+c))^\n)-SVF1(3,f,u0)/*(c^\n))(#)(h^\n)")
by A21,A29,VALUED_0:27
.= ((((SVF1(3,f,u0)/*(h+c))^\n)-((SVF1(3,f,u0)/*c)^\n))(#)(h^\n)")
by A20,VALUED_0:27
.= ((((SVF1(3,f,u0)/*(h+c))-(SVF1(3,f,u0)/*c))^\n)(#)(h^\n)") by SEQM_3:17
.= ((((SVF1(3,f,u0)/*(h+c))-(SVF1(3,f,u0)/*c))^\n)(#)((h")^\n))
by SEQM_3:18
.= ((((SVF1(3,f,u0)/*(h+c))-(SVF1(3,f,u0)/*c))(#) h")^\n)
by SEQM_3:19;then
A42: L.1 = lim ((h")(#)((SVF1(3,f,u0)/*(h+c))-(SVF1(3,f,u0)/*c)))
by A30,SEQ_4:22;
thus h"(#)(SVF1(3,f,u0)/*(h+c)-SVF1(3,f,u0)/*c) is convergent
by A30,A41,SEQ_4:21;
thus thesis by A1,A3,A22,A40,A42,Th18;
end;
theorem
f1 is_partial_differentiable_in u0,1 &
f2 is_partial_differentiable_in u0,1 implies
f1(#)f2 is_partial_differentiable_in u0,1
proof
assume that
A1: f1 is_partial_differentiable_in u0,1 and
A2: f2 is_partial_differentiable_in u0,1;
consider x0,y0,z0 being Real such that
A3: u0 = <*x0,y0,z0*> & ex N being Neighbourhood of x0
st N c= dom SVF1(1,f1,u0) & ex L,R st for x st x in N holds
SVF1(1,f1,u0).x - SVF1(1,f1,u0).x0 = L.(x-x0) + R.(x-x0)
by A1,Th13;
consider N1 be Neighbourhood of x0 such that
A4: N1 c= dom SVF1(1,f1,u0) & ex L,R st for x st x in N1 holds
SVF1(1,f1,u0).x - SVF1(1,f1,u0).x0 = L.(x-x0) + R.(x-x0) by A3;
consider L1,R1 such that
A5: for x st x in N1 holds
SVF1(1,f1,u0).x - SVF1(1,f1,u0).x0 = L1.(x-x0) + R1.(x-x0) by A4;
consider x1,y1,z1 being Real such that
A6: u0 = <*x1,y1,z1*> & ex N being Neighbourhood of x1
st N c= dom SVF1(1,f2,u0) & ex L,R st for x st x in N holds
SVF1(1,f2,u0).x - SVF1(1,f2,u0).x1 = L.(x-x1) + R.(x-x1)
by A2,Th13;
x0 = x1 & y0 = y1 & z0 = z1 by A3,A6,FINSEQ_1:78;
then consider N2 be Neighbourhood of x0 such that
A7: N2 c= dom SVF1(1,f2,u0) & ex L,R st for x st x in N2 holds
SVF1(1,f2,u0).x - SVF1(1,f2,u0).x0 = L.(x-x0) + R.(x-x0) by A6;
consider L2,R2 such that
A8: for x st x in N2 holds
SVF1(1,f2,u0).x - SVF1(1,f2,u0).x0 = L2.(x-x0) + R2.(x-x0) by A7;
consider N be Neighbourhood of x0 such that
A9: N c= N1 & N c= N2 by RCOMP_1:17;
reconsider L11=(SVF1(1,f2,u0).x0)(#)L1, L12=(SVF1(1,f1,u0).x0)(#)L2
as LinearFunc by FDIFF_1:3;
A10: L11 is total & L12 is total & L1 is total & L2 is total by FDIFF_1:def 3;
reconsider L=L11+L12 as LinearFunc by FDIFF_1:2;
reconsider R11=(SVF1(1,f2,u0).x0)(#)R1 as RestFunc by FDIFF_1:5;
reconsider R12=(SVF1(1,f1,u0).x0)(#)R2 as RestFunc by FDIFF_1:5;
reconsider R13=R11+R12 as RestFunc by FDIFF_1:4;
reconsider R14=L1(#)L2 as RestFunc by FDIFF_1:6;
reconsider R15=R13+R14 as RestFunc by FDIFF_1:4;
reconsider R16=R1(#)L2, R18=R2(#)L1 as RestFunc by FDIFF_1:7;
reconsider 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;
A11: R1 is total & R2 is total & R11 is total & R12 is total &
R13 is total & R14 is total & R15 is total & R16 is total &
R17 is total & R18 is total & R19 is total & R20 is total
by FDIFF_1:def 2;
A12: N c= dom SVF1(1,f1,u0) by A4,A9;
A13: N c= dom SVF1(1,f2,u0) by A7,A9;
A14: for y st y in N holds y in dom SVF1(1,f1(#)f2,u0)
proof
let y;
assume
A15: y in N;
then
A16: y in dom reproj(1,u0) & reproj(1,u0).y in dom f1 by A12,FUNCT_1:11;
y in dom reproj(1,u0) & reproj(1,u0).y in dom f2 by A13,A15,FUNCT_1:11;
then y in dom reproj(1,u0) & reproj(1,u0).y in dom f1 /\ dom f2
by A16,XBOOLE_0:def 4;then
y in dom reproj(1,u0) & reproj(1,u0).y in dom (f1(#)f2)
by VALUED_1:def 4;
hence thesis by FUNCT_1:11;
end;
then for y be object st y in N holds y in dom SVF1(1,f1(#)f2,u0);then
A17: N c= dom SVF1(1,f1(#)f2,u0);
now
let x;
reconsider xx=x, xx0=x0 as Element of REAL by XREAL_0:def 1;
assume
A18: x in N;then
A19: SVF1(1,f1,u0).x - SVF1(1,f1,u0).x0 + SVF1(1,f1,u0).x0
= L1.(x-x0) + R1.(x-x0) + SVF1(1,f1,u0).x0 by A5,A9;
x in dom ((f1(#)f2)*reproj(1,u0)) by A14,A18;then
A20: x in dom reproj(1,u0) & reproj(1,u0).x in dom (f1(#)f2) by FUNCT_1:11;
then reproj(1,u0).x in dom f1 /\ dom f2 by VALUED_1:def 4;
then reproj(1,u0).x in dom f1 & reproj(1,u0).x in dom f2
by XBOOLE_0:def 4;then
A21: x in dom (f1*reproj(1,u0)) & x in dom (f2*reproj(1,u0))
by A20,FUNCT_1:11;
A22: x0 in N by RCOMP_1:16;
x0 in dom ((f1(#)f2)*reproj(1,u0)) by A14,RCOMP_1:16;then
A23: x0 in dom reproj(1,u0) & reproj(1,u0).x0 in dom (f1(#)f2) by FUNCT_1:11;
then reproj(1,u0).x0 in dom f1 /\ dom f2 by VALUED_1:def 4;
then reproj(1,u0).x0 in dom f1 & reproj(1,u0).x0 in dom f2
by XBOOLE_0:def 4;then
A24: x0 in dom (f1*reproj(1,u0)) & x0 in dom (f2*reproj(1,u0))
by A23,FUNCT_1:11;
thus SVF1(1,f1(#)f2,u0).x - SVF1(1,f1(#)f2,u0).x0
= (f1(#)f2).(reproj(1,u0).x) - SVF1(1,f1(#)f2,u0).x0
by A17,A18,FUNCT_1:12
.= (f1.(reproj(1,u0).x))*(f2.(reproj(1,u0).x)) - SVF1(1,f1(#)f2,u0).x0
by VALUED_1:5
.= (SVF1(1,f1,u0).x)*(f2.(reproj(1,u0).x)) - SVF1(1,f1(#)f2,u0).x0
by A21,FUNCT_1:12
.= (SVF1(1,f1,u0).x)*(SVF1(1,f2,u0).x) - ((f1(#)f2)*reproj(1,u0)).x0
by A21,FUNCT_1:12
.= (SVF1(1,f1,u0).x)*(SVF1(1,f2,u0).x) - (f1(#)f2).(reproj(1,u0).x0)
by A17,A22,FUNCT_1:12
.= (SVF1(1,f1,u0).x)*(SVF1(1,f2,u0).x) -
(f1.(reproj(1,u0).x0))*(f2.(reproj(1,u0).x0)) by VALUED_1:5
.= (SVF1(1,f1,u0).x)*(SVF1(1,f2,u0).x)
- (SVF1(1,f1,u0).x0)*(f2.(reproj(1,u0).x0)) by A24,FUNCT_1:12
.= (SVF1(1,f1,u0).x)*(SVF1(1,f2,u0).x)+-(SVF1(1,f1,u0).x)*
(SVF1(1,f2,u0).x0)+
(SVF1(1,f1,u0).x)*(SVF1(1,f2,u0).x0)-(SVF1(1,f1,u0).x0)*
(SVF1(1,f2,u0).x0) by A24,FUNCT_1:12
.= (SVF1(1,f1,u0).x)*(SVF1(1,f2,u0).x-SVF1(1,f2,u0).x0)+
(SVF1(1,f1,u0).x-SVF1(1,f1,u0).x0)*(SVF1(1,f2,u0).x0)
.= (SVF1(1,f1,u0).x)*(SVF1(1,f2,u0).x-SVF1(1,f2,u0).x0)+
(L1.(x-x0)+R1.(x-x0))*(SVF1(1,f2,u0).x0) by A5,A9,A18
.= (SVF1(1,f1,u0).x)*(SVF1(1,f2,u0).x-SVF1(1,f2,u0).x0)+
((SVF1(1,f2,u0).x0)*L1.(x-x0)+(SVF1(1,f2,u0).x0)*R1.(x-x0))
.= (SVF1(1,f1,u0).x)*(SVF1(1,f2,u0).x-SVF1(1,f2,u0).x0)+
(L11.(xx-x0)+(SVF1(1,f2,u0).x0)*R1.(xx-xx0)) by A10,RFUNCT_1:57
.= (L1.(x-x0)+R1.(xx-x0)+SVF1(1,f1,u0).x0)*
(SVF1(1,f2,u0).xx-SVF1(1,f2,u0).x0)+
(L11.(x-x0)+R11.(xx-x0)) by A11,A19,RFUNCT_1:57
.= (L1.(x-x0)+R1.(x-x0)+SVF1(1,f1,u0).x0)*(L2.(x-x0)+R2.(x-x0))+
(L11.(x-x0)+R11.(x-x0)) by A8,A9,A18
.= (L1.(x-x0)+R1.(x-x0))*(L2.(x-x0)+R2.(x-x0))+
((SVF1(1,f1,u0).x0)*L2.(x-x0)+(SVF1(1,f1,u0).x0)*R2.(x-x0))+
(L11.(x-x0)+R11.(x-x0))
.= (L1.(xx-x0)+R1.(xx-x0))*(L2.(xx-x0)+R2.(xx-xx0))+
(L12.(x-x0)+(SVF1(1,f1,u0).x0)*R2.(x-x0))+(L11.(x-x0)+R11.(x-x0))
by A10,RFUNCT_1:57
.= (L1.(x-x0)+R1.(xx-xx0))*(L2.(xx-x0)+R2.(x-x0))+
(L12.(xx-x0)+R12.(x-x0))+(L11.(xx-x0)+R11.(x-x0)) by A11,RFUNCT_1:57
.= (L1.(xx-x0)+R1.(x-x0))*(L2.(xx-x0)+R2.(x-x0))+
(L12.(xx-x0)+(L11.(x-x0)+(R11.(xx-x0)+R12.(x-x0))))
.= (L1.(xx-x0)+R1.(x-x0))*(L2.(xx-xx0)+R2.(xx-x0))+
(L12.(xx-x0)+(L11.(xx-x0)+R13.(xx-x0))) by A11,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.(xx-x0)*L2.(xx-x0)+L1.(xx-x0)*R2.(xx-x0))+
R1.(xx-xx0)*(L2.(xx-x0)+R2.(xx-x0))+(L.(xx-x0)+R13.(xx-x0))
by A10,RFUNCT_1:56
.= R14.(xx-x0)+R2.(xx-x0)*L1.(xx-x0)+R1.(xx-x0)*(L2.(xx-x0)+R2.(xx-x0))+
(L.(xx-x0)+R13.(xx-xx0)) by A10,RFUNCT_1:56
.= R14.(xx-x0)+R18.(xx-x0)+(R1.(xx-x0)*L2.(x-x0)+R1.(x-x0)*R2.(x-x0))+
(L.(x-x0)+R13.(x-xx0)) by A10,A11,RFUNCT_1:56
.= R14.(x-x0)+R18.(x-x0)+(R16.(x-x0)+R1.(x-x0)*R2.(x-x0))+
(L.(x-x0)+R13.(xx-xx0)) by A10,A11,RFUNCT_1:56
.= R14.(xx-x0)+R18.(x-x0)+(R16.(x-x0)+R17.(x-x0))+(L.(x-x0)+R13.(x-x0))
by A11,RFUNCT_1:56
.= R14.(xx-xx0)+R18.(x-x0)+R19.(x-x0)+(L.(x-x0)+R13.(x-x0))
by A11,RFUNCT_1:56
.= R14.(xx-x0)+(R19.(x-x0)+R18.(x-x0))+(L.(x-x0)+R13.(x-x0))
.= L.(xx-xx0)+R13.(x-x0)+(R14.(x-x0)+R20.(x-x0)) by A11,RFUNCT_1:56
.= L.(xx-x0)+(R13.(x-x0)+R14.(x-x0)+R20.(x-x0))
.= L.(xx-xx0)+(R15.(x-x0)+R20.(x-x0)) by A11,RFUNCT_1:56
.= L.(x-x0)+R.(x-x0) by A11,RFUNCT_1:56;
end;
hence thesis by A3,A17,Th13;
end;
theorem
f1 is_partial_differentiable_in u0,2 &
f2 is_partial_differentiable_in u0,2 implies
f1(#)f2 is_partial_differentiable_in u0,2
proof
assume that
A1: f1 is_partial_differentiable_in u0,2 and
A2: f2 is_partial_differentiable_in u0,2;
consider x0,y0,z0 being Real such that
A3: u0 = <*x0,y0,z0*> & ex N being Neighbourhood of y0
st N c= dom SVF1(2,f1,u0) & ex L,R st for y st y in N holds
SVF1(2,f1,u0).y - SVF1(2,f1,u0).y0 = L.(y-y0) + R.(y-y0)
by A1,Th14;
consider N1 be Neighbourhood of y0 such that
A4: N1 c= dom SVF1(2,f1,u0) & ex L,R st for y st y in N1 holds
SVF1(2,f1,u0).y - SVF1(2,f1,u0).y0 = L.(y-y0) + R.(y-y0) by A3;
consider L1,R1 such that
A5: for y st y in N1 holds
SVF1(2,f1,u0).y - SVF1(2,f1,u0).y0 = L1.(y-y0) + R1.(y-y0) by A4;
consider x1,y1,z1 being Real such that
A6: u0 = <*x1,y1,z1*> & ex N being Neighbourhood of y1
st N c= dom SVF1(2,f2,u0) & ex L,R st for y st y in N holds
SVF1(2,f2,u0).y - SVF1(2,f2,u0).y1 = L.(y-y1) + R.(y-y1)
by A2,Th14;
x0 = x1 & y0 = y1 & z0 = z1 by A3,A6,FINSEQ_1:78;
then consider N2 be Neighbourhood of y0 such that
A7: N2 c= dom SVF1(2,f2,u0) & ex L,R st for y st y in N2 holds
SVF1(2,f2,u0).y - SVF1(2,f2,u0).y0 = L.(y-y0) + R.(y-y0) by A6;
consider L2,R2 such that
A8: for y st y in N2 holds
SVF1(2,f2,u0).y - SVF1(2,f2,u0).y0 = L2.(y-y0) + R2.(y-y0) by A7;
consider N be Neighbourhood of y0 such that
A9: N c= N1 & N c= N2 by RCOMP_1:17;
reconsider L11=(SVF1(2,f2,u0).y0)(#)L1 as LinearFunc by FDIFF_1:3;
reconsider L12=(SVF1(2,f1,u0).y0)(#)L2 as LinearFunc by FDIFF_1:3;
A10: L11 is total & L12 is total & L1 is total & L2 is total by FDIFF_1:def 3;
reconsider L=L11+L12 as LinearFunc by FDIFF_1:2;
reconsider R11=(SVF1(2,f2,u0).y0)(#)R1, R12=(SVF1(2,f1,u0).y0)(#)R2
as RestFunc by FDIFF_1:5;
reconsider R13=R11+R12 as RestFunc by FDIFF_1:4;
reconsider R14=L1(#)L2 as RestFunc by FDIFF_1:6;
reconsider R15=R13+R14, R17=R1(#)R2 as RestFunc by FDIFF_1:4;
reconsider R16=R1(#)L2, R18=R2(#)L1 as RestFunc by FDIFF_1:7;
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;
A11: R1 is total & R2 is total & R11 is total & R12 is total &
R13 is total & R14 is total & R15 is total & R16 is total &
R17 is total & R18 is total & R19 is total & R20 is total
by FDIFF_1:def 2;
A12: N c= dom SVF1(2,f1,u0) by A4,A9;
A13: N c= dom SVF1(2,f2,u0) by A7,A9;
A14: for y st y in N holds y in dom SVF1(2,f1(#)f2,u0)
proof
let y;
assume
A15: y in N;
then
A16: y in dom reproj(2,u0) & reproj(2,u0).y in dom f1 by A12,FUNCT_1:11;
y in dom reproj(2,u0) & reproj(2,u0).y in dom f2 by A13,A15,FUNCT_1:11;
then y in dom reproj(2,u0) & reproj(2,u0).y in dom f1 /\ dom f2
by A16,XBOOLE_0:def 4;then
y in dom reproj(2,u0) & reproj(2,u0).y in dom (f1(#)f2)
by VALUED_1:def 4;
hence thesis by FUNCT_1:11;
end;
then for y be object st y in N holds y in dom SVF1(2,f1(#)f2,u0);then
A17: N c= dom SVF1(2,f1(#)f2,u0);
now
let yy be Real;
assume
A18: yy in N;
reconsider y=yy, yy0=y0 as Element of REAL by XREAL_0:def 1;
A19: SVF1(2,f1,u0).y - SVF1(2,f1,u0).y0 + SVF1(2,f1,u0).y0
= L1.(y-y0) + R1.(y-y0) + SVF1(2,f1,u0).y0 by A5,A9,A18;
y in dom ((f1(#)f2)*reproj(2,u0)) by A14,A18;then
A20: y in dom reproj(2,u0) & reproj(2,u0).y in dom (f1(#)f2) by FUNCT_1:11;
then reproj(2,u0).y in dom f1 /\ dom f2 by VALUED_1:def 4;
then reproj(2,u0).y in dom f1 & reproj(2,u0).y in dom f2
by XBOOLE_0:def 4;then
A21: y in dom (f1*reproj(2,u0)) & y in dom (f2*reproj(2,u0))
by A20,FUNCT_1:11;
A22: y0 in N by RCOMP_1:16;
y0 in dom ((f1(#)f2)*reproj(2,u0)) by A14,RCOMP_1:16;then
A23: y0 in dom reproj(2,u0) & reproj(2,u0).y0 in dom (f1(#)f2) by FUNCT_1:11;
then reproj(2,u0).y0 in dom f1 /\ dom f2 by VALUED_1:def 4;
then reproj(2,u0).y0 in dom f1 & reproj(2,u0).y0 in dom f2
by XBOOLE_0:def 4;then
A24: y0 in dom (f1*reproj(2,u0)) & y0 in dom (f2*reproj(2,u0))
by A23,FUNCT_1:11;
thus SVF1(2,f1(#)f2,u0).yy - SVF1(2,f1(#)f2,u0).y0
= (f1(#)f2).(reproj(2,u0).y) - SVF1(2,f1(#)f2,u0).y0
by A17,A18,FUNCT_1:12
.= (f1.(reproj(2,u0).y))*(f2.(reproj(2,u0).y)) - SVF1(2,f1(#)f2,u0).y0
by VALUED_1:5
.= (SVF1(2,f1,u0).y)*(f2.(reproj(2,u0).y)) - SVF1(2,f1(#)f2,u0).y0
by A21,FUNCT_1:12
.= (SVF1(2,f1,u0).y)*(SVF1(2,f2,u0).y) - ((f1(#)f2)*reproj(2,u0)).y0
by A21,FUNCT_1:12
.= (SVF1(2,f1,u0).y)*(SVF1(2,f2,u0).y) - (f1(#)f2).(reproj(2,u0).y0)
by A17,A22,FUNCT_1:12
.= (SVF1(2,f1,u0).y)*(SVF1(2,f2,u0).y) -
(f1.(reproj(2,u0).y0))*(f2.(reproj(2,u0).y0)) by VALUED_1:5
.= (SVF1(2,f1,u0).y)*(SVF1(2,f2,u0).y) -
(SVF1(2,f1,u0).y0)*(f2.(reproj(2,u0).y0)) by A24,FUNCT_1:12
.= (SVF1(2,f1,u0).y)*(SVF1(2,f2,u0).y)+
-(SVF1(2,f1,u0).y)*(SVF1(2,f2,u0).y0)+
(SVF1(2,f1,u0).y)*(SVF1(2,f2,u0).y0)-
(SVF1(2,f1,u0).y0)*(SVF1(2,f2,u0).y0) by A24,FUNCT_1:12
.= (SVF1(2,f1,u0).y)*(SVF1(2,f2,u0).y-SVF1(2,f2,u0).y0)+
(SVF1(2,f1,u0).y-SVF1(2,f1,u0).y0)*(SVF1(2,f2,u0).y0)
.= (SVF1(2,f1,u0).y)*(SVF1(2,f2,u0).y-SVF1(2,f2,u0).y0)+
(L1.(y-y0)+R1.(y-y0))*(SVF1(2,f2,u0).y0) by A5,A9,A18
.= (SVF1(2,f1,u0).y)*(SVF1(2,f2,u0).y-SVF1(2,f2,u0).y0)+
((SVF1(2,f2,u0).y0)*L1.(y-y0)+(SVF1(2,f2,u0).y0)*R1.(y-y0))
.= (SVF1(2,f1,u0).y)*(SVF1(2,f2,u0).y-SVF1(2,f2,u0).y0)+
(L11.(y-yy0)+(SVF1(2,f2,u0).y0)*R1.(y-yy0)) by A10,RFUNCT_1:57
.= (L1.(y-yy0)+R1.(y-yy0)+SVF1(2,f1,u0).y0)*
(SVF1(2,f2,u0).y-SVF1(2,f2,u0).y0)+
(L11.(y-y0)+R11.(y-y0)) by A11,A19,RFUNCT_1:57
.= (L1.(y-y0)+R1.(y-y0)+SVF1(2,f1,u0).y0)*(L2.(y-y0)+R2.(y-y0))+
(L11.(y-y0)+R11.(y-y0)) by A8,A9,A18
.= (L1.(y-y0)+R1.(y-y0))*(L2.(y-y0)+R2.(y-y0))+
((SVF1(2,f1,u0).y0)*L2.(y-y0)+(SVF1(2,f1,u0).y0)*R2.(y-y0))+
(L11.(y-y0)+R11.(y-y0))
.= (L1.(y-yy0)+R1.(y-y0))*(L2.(y-y0)+R2.(y-y0))+
(L12.(y-y0)+(SVF1(2,f1,u0).y0)*R2.(y-y0))+(L11.(y-y0)+R11.(y-y0))
by A10,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.(y-y0)) by A11,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.(y-y0))*(L2.(y-y0)+R2.(y-y0))+
(L12.(y-yy0)+(L11.(y-y0)+R13.(y-y0))) by A11,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-yy0)*(L2.(y-y0)+R2.(y-y0))+(L.(y-y0)+R13.(y-y0))
by A10,RFUNCT_1:56
.= R14.(y-y0)+R2.(y-y0)*L1.(y-y0)+R1.(y-y0)*(L2.(y-y0)+R2.(y-y0))+
(L.(y-yy0)+R13.(y-y0)) by A10,RFUNCT_1:56
.= R14.(y-y0)+R18.(y-y0)+(R1.(y-y0)*L2.(y-y0)+R1.(y-y0)*R2.(y-y0))+
(L.(y-yy0)+R13.(y-y0)) by A10,A11,RFUNCT_1:56
.= R14.(y-y0)+R18.(y-y0)+(R16.(y-y0)+R1.(y-y0)*R2.(y-y0))+
(L.(y-yy0)+R13.(y-y0)) by A10,A11,RFUNCT_1:56
.= R14.(y-y0)+R18.(y-y0)+(R16.(y-y0)+R17.(y-y0))+(L.(y-y0)+R13.(y-y0))
by A11,RFUNCT_1:56
.= R14.(y-yy0)+R18.(y-y0)+R19.(y-y0)+(L.(y-y0)+R13.(y-y0))
by A11,RFUNCT_1:56
.= R14.(y-y0)+(R19.(y-y0)+R18.(y-y0))+(L.(y-y0)+R13.(y-y0))
.= L.(y-yy0)+R13.(y-y0)+(R14.(y-y0)+R20.(y-y0)) by A11,RFUNCT_1:56
.= L.(y-y0)+(R13.(y-y0)+R14.(y-y0)+R20.(y-y0))
.= L.(y-yy0)+(R15.(y-y0)+R20.(y-y0)) by A11,RFUNCT_1:56
.= L.(yy-y0)+R.(yy-y0) by A11,RFUNCT_1:56;
end;
hence thesis by A3,A17,Th14;
end;
theorem
f1 is_partial_differentiable_in u0,3 &
f2 is_partial_differentiable_in u0,3 implies
f1(#)f2 is_partial_differentiable_in u0,3
proof
assume that
A1: f1 is_partial_differentiable_in u0,3 and
A2: f2 is_partial_differentiable_in u0,3;
consider x0,y0,z0 being Real such that
A3: u0 = <*x0,y0,z0*> & ex N being Neighbourhood of z0
st N c= dom SVF1(3,f1,u0) & ex L,R st for z st z in N holds
SVF1(3,f1,u0).z - SVF1(3,f1,u0).z0 = L.(z-z0) + R.(z-z0)
by A1,Th15;
consider N1 be Neighbourhood of z0 such that
A4: N1 c= dom SVF1(3,f1,u0) & ex L,R st for z st z in N1 holds
SVF1(3,f1,u0).z - SVF1(3,f1,u0).z0 = L.(z-z0) + R.(z-z0) by A3;
consider L1,R1 such that
A5: for z st z in N1 holds
SVF1(3,f1,u0).z - SVF1(3,f1,u0).z0 = L1.(z-z0) + R1.(z-z0) by A4;
consider x1,y1,z1 being Real such that
A6: u0 = <*x1,y1,z1*> & ex N being Neighbourhood of z1
st N c= dom SVF1(3,f2,u0) & ex L,R st for z st z in N holds
SVF1(3,f2,u0).z - SVF1(3,f2,u0).z1 = L.(z-z1) + R.(z-z1)
by A2,Th15;
x0 = x1 & y0 = y1 & z0 = z1 by A3,A6,FINSEQ_1:78;
then consider N2 be Neighbourhood of z0 such that
A7: N2 c= dom SVF1(3,f2,u0) & ex L,R st for z st z in N2 holds
SVF1(3,f2,u0).z - SVF1(3,f2,u0).z0 = L.(z-z0) + R.(z-z0) by A6;
consider L2,R2 such that
A8: for z st z in N2 holds
SVF1(3,f2,u0).z - SVF1(3,f2,u0).z0 = L2.(z-z0) + R2.(z-z0) by A7;
consider N be Neighbourhood of z0 such that
A9: N c= N1 & N c= N2 by RCOMP_1:17;
reconsider L11=(SVF1(3,f2,u0).z0)(#)L1 as LinearFunc by FDIFF_1:3;
reconsider L12=(SVF1(3,f1,u0).z0)(#)L2 as LinearFunc by FDIFF_1:3;
A10: L11 is total & L12 is total & L1 is total & L2 is total by FDIFF_1:def 3;
reconsider L=L11+L12 as LinearFunc by FDIFF_1:2;
reconsider R11=(SVF1(3,f2,u0).z0)(#)R1, R12=(SVF1(3,f1,u0).z0)(#)R2
as RestFunc by FDIFF_1:5;
reconsider R13=R11+R12 as RestFunc by FDIFF_1:4;
reconsider R14=L1(#)L2 as RestFunc by FDIFF_1:6;
reconsider R15=R13+R14, R17=R1(#)R2 as RestFunc by FDIFF_1:4;
reconsider R16=R1(#)L2, R18=R2(#)L1 as RestFunc by FDIFF_1:7;
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;
A11: R1 is total & R2 is total & R11 is total & R12 is total &
R13 is total & R14 is total & R15 is total & R16 is total &
R17 is total & R18 is total & R19 is total & R20 is total
by FDIFF_1:def 2;
A12: N c= dom SVF1(3,f1,u0) by A4,A9;
A13: N c= dom SVF1(3,f2,u0) by A7,A9;
A14: for z st z in N holds z in dom SVF1(3,f1(#)f2,u0)
proof
let z;
assume
A15: z in N;
then
A16: z in dom reproj(3,u0) & reproj(3,u0).z in dom f1 by A12,FUNCT_1:11;
z in dom reproj(3,u0) & reproj(3,u0).z in dom f2 by A13,A15,FUNCT_1:11;
then z in dom reproj(3,u0) & reproj(3,u0).z in dom f1 /\ dom f2
by A16,XBOOLE_0:def 4;then
z in dom reproj(3,u0) & reproj(3,u0).z in dom (f1(#)f2)
by VALUED_1:def 4;
hence thesis by FUNCT_1:11;
end;
then for z be object st z in N holds z in dom SVF1(3,f1(#)f2,u0);then
A17: N c= dom SVF1(3,f1(#)f2,u0);
now
let zz be Real;
assume
A18: zz in N;
reconsider z=zz, zz0=z0 as Element of REAL by XREAL_0:def 1;
A19: SVF1(3,f1,u0).z - SVF1(3,f1,u0).z0 + SVF1(3,f1,u0).z0
= L1.(z-z0) + R1.(z-z0) + SVF1(3,f1,u0).z0 by A5,A9,A18;
z in dom ((f1(#)f2)*reproj(3,u0)) by A14,A18;then
A20: z in dom reproj(3,u0) & reproj(3,u0).z in dom (f1(#)f2) by FUNCT_1:11;
then reproj(3,u0).z in dom f1 /\ dom f2 by VALUED_1:def 4;
then reproj(3,u0).z in dom f1 & reproj(3,u0).z in dom f2
by XBOOLE_0:def 4;then
A21: z in dom (f1*reproj(3,u0)) & z in dom (f2*reproj(3,u0))
by A20,FUNCT_1:11;
A22: z0 in N by RCOMP_1:16;
z0 in dom ((f1(#)f2)*reproj(3,u0)) by A14,RCOMP_1:16;then
A23: z0 in dom reproj(3,u0) & reproj(3,u0).z0 in dom (f1(#)f2) by FUNCT_1:11;
then reproj(3,u0).z0 in dom f1 /\ dom f2 by VALUED_1:def 4;
then reproj(3,u0).z0 in dom f1 & reproj(3,u0).z0 in dom f2
by XBOOLE_0:def 4;then
A24: z0 in dom (f1*reproj(3,u0)) & z0 in dom (f2*reproj(3,u0))
by A23,FUNCT_1:11;
thus SVF1(3,f1(#)f2,u0).zz - SVF1(3,f1(#)f2,u0).z0
= (f1(#)f2).(reproj(3,u0).z) - SVF1(3,f1(#)f2,u0).z0
by A17,A18,FUNCT_1:12
.= (f1.(reproj(3,u0).z))*(f2.(reproj(3,u0).z)) - SVF1(3,f1(#)f2,u0).z0
by VALUED_1:5
.= (SVF1(3,f1,u0).z)*(f2.(reproj(3,u0).z)) - SVF1(3,f1(#)f2,u0).z0
by A21,FUNCT_1:12
.= (SVF1(3,f1,u0).z)*(SVF1(3,f2,u0).z) - ((f1(#)f2)*reproj(3,u0)).z0
by A21,FUNCT_1:12
.= (SVF1(3,f1,u0).z)*(SVF1(3,f2,u0).z) - (f1(#)f2).(reproj(3,u0).z0)
by A17,A22,FUNCT_1:12
.= (SVF1(3,f1,u0).z)*(SVF1(3,f2,u0).z) -
(f1.(reproj(3,u0).z0))*(f2.(reproj(3,u0).z0)) by VALUED_1:5
.= (SVF1(3,f1,u0).z)*(SVF1(3,f2,u0).z) -
(SVF1(3,f1,u0).z0)*(f2.(reproj(3,u0).z0)) by A24,FUNCT_1:12
.= (SVF1(3,f1,u0).z)*(SVF1(3,f2,u0).z)+
-(SVF1(3,f1,u0).z)*(SVF1(3,f2,u0).z0)+
(SVF1(3,f1,u0).z)*(SVF1(3,f2,u0).z0)-
(SVF1(3,f1,u0).z0)*(SVF1(3,f2,u0).z0) by A24,FUNCT_1:12
.= (SVF1(3,f1,u0).z)*(SVF1(3,f2,u0).z-SVF1(3,f2,u0).z0)+
(SVF1(3,f1,u0).z-SVF1(3,f1,u0).z0)*(SVF1(3,f2,u0).z0)
.= (SVF1(3,f1,u0).z)*(SVF1(3,f2,u0).z-SVF1(3,f2,u0).z0)+
(L1.(z-z0)+R1.(z-z0))*(SVF1(3,f2,u0).z0) by A5,A9,A18
.= (SVF1(3,f1,u0).z)*(SVF1(3,f2,u0).z-SVF1(3,f2,u0).z0)+
((SVF1(3,f2,u0).z0)*L1.(z-z0)+(SVF1(3,f2,u0).z0)*R1.(z-z0))
.= (SVF1(3,f1,u0).z)*(SVF1(3,f2,u0).z-SVF1(3,f2,u0).z0)+
(L11.(z-z0)+(SVF1(3,f2,u0).z0)*R1.(z-zz0)) by A10,RFUNCT_1:57
.= (L1.(z-z0)+R1.(z-z0)+SVF1(3,f1,u0).z0)*
(SVF1(3,f2,u0).z-SVF1(3,f2,u0).z0)+
(L11.(z-z0)+R11.(z-zz0)) by A11,A19,RFUNCT_1:57
.= (L1.(z-z0)+R1.(z-z0)+SVF1(3,f1,u0).z0)*(L2.(z-z0)+R2.(z-z0))+
(L11.(z-z0)+R11.(z-z0)) by A8,A9,A18
.= (L1.(z-z0)+R1.(z-z0))*(L2.(z-z0)+R2.(z-z0))+
((SVF1(3,f1,u0).z0)*L2.(z-z0)+(SVF1(3,f1,u0).z0)*R2.(z-z0))+
(L11.(z-z0)+R11.(z-z0))
.= (L1.(z-z0)+R1.(z-z0))*(L2.(z-z0)+R2.(z-zz0))+
(L12.(z-z0)+(SVF1(3,f1,u0).z0)*R2.(z-z0))+(L11.(z-z0)+R11.(z-z0))
by A10,RFUNCT_1:57
.= (L1.(z-z0)+R1.(z-z0))*(L2.(z-z0)+R2.(z-zz0))+
(L12.(z-z0)+R12.(z-z0))+(L11.(z-z0)+R11.(z-z0)) by A11,RFUNCT_1:57
.= (L1.(z-z0)+R1.(z-z0))*(L2.(z-z0)+R2.(z-z0))+
(L12.(z-z0)+(L11.(z-z0)+(R11.(z-z0)+R12.(z-z0))))
.= (L1.(z-z0)+R1.(z-z0))*(L2.(z-z0)+R2.(z-zz0))+
(L12.(z-z0)+(L11.(z-z0)+R13.(z-z0))) by A11,RFUNCT_1:56
.= (L1.(z-z0)+R1.(z-z0))*(L2.(z-z0)+R2.(z-z0))+
(L11.(z-z0)+L12.(z-z0)+R13.(z-z0))
.= (L1.(z-z0)*L2.(z-z0)+L1.(z-z0)*R2.(z-z0))+
R1.(z-zz0)*(L2.(z-z0)+R2.(z-z0))+(L.(z-z0)+R13.(z-z0))
by A10,RFUNCT_1:56
.= R14.(z-z0)+R2.(z-z0)*L1.(z-z0)+R1.(z-z0)*(L2.(z-z0)+R2.(z-z0))+
(L.(z-z0)+R13.(z-zz0)) by A10,RFUNCT_1:56
.= R14.(z-z0)+R18.(z-z0)+(R1.(z-z0)*L2.(z-z0)+R1.(z-z0)*R2.(z-z0))+
(L.(z-z0)+R13.(z-zz0)) by A10,A11,RFUNCT_1:56
.= R14.(z-z0)+R18.(z-z0)+(R16.(z-z0)+R1.(z-z0)*R2.(z-z0))+
(L.(z-z0)+R13.(z-zz0)) by A10,A11,RFUNCT_1:56
.= R14.(z-z0)+R18.(z-z0)+(R16.(z-z0)+R17.(z-z0))+(L.(z-z0)+R13.(z-z0))
by A11,RFUNCT_1:56
.= R14.(z-zz0)+R18.(z-z0)+R19.(z-z0)+(L.(z-z0)+R13.(z-z0))
by A11,RFUNCT_1:56
.= R14.(z-z0)+(R19.(z-z0)+R18.(z-z0))+(L.(z-z0)+R13.(z-z0))
.= L.(z-zz0)+R13.(z-z0)+(R14.(z-z0)+R20.(z-z0)) by A11,RFUNCT_1:56
.= L.(z-z0)+(R13.(z-z0)+R14.(z-z0)+R20.(z-z0))
.= L.(z-zz0)+(R15.(z-z0)+R20.(z-zz0)) by A11,RFUNCT_1:56
.= L.(zz-z0)+R.(zz-z0) by A11,RFUNCT_1:56;
end;
hence thesis by A3,A17,Th15;
end;
theorem
for u0 being Element of REAL 3 holds f is_partial_differentiable_in u0,1
implies SVF1(1,f,u0) is_continuous_in proj(1,3).u0
by FDIFF_1:24;
theorem
for u0 being Element of REAL 3 holds f is_partial_differentiable_in u0,2
implies SVF1(2,f,u0) is_continuous_in proj(2,3).u0
by FDIFF_1:24;
theorem
for u0 being Element of REAL 3 holds f is_partial_differentiable_in u0,3
implies SVF1(3,f,u0) is_continuous_in proj(3,3).u0
by FDIFF_1:24;
begin :: Grads & Curl
Lm4:
|[ x1,y1,z1 ]| + |[ x2,y2,z2 ]| = |[ x1+x2,y1+y2,z1+z2 ]|
proof
A4: |[ x1,y1,z1 ]|.1 +|[ x2,y2,z2 ]|.1 = x1+x2;
A5: |[ x1,y1,z1 ]|.2 +|[ x2,y2,z2 ]|.2 = y1+y2;
|[ x1,y1,z1 ]|.3 +|[ x2,y2,z2 ]|.3 = z1+z2;
hence thesis by A4,A5,EUCLID_8:55;
end;
definition
let f be PartFunc of REAL 3,REAL;
let p be Element of REAL 3;
func grad(f,p) -> Element of REAL 3 equals
partdiff(f,p,1)*<e1>+partdiff(f,p,2)*<e2>+partdiff(f,p,3)*<e3>;
coherence;
end;
reconsider jj=1 as Real;
theorem Th34:
grad(f,p) = |[ partdiff(f,p,1),partdiff(f,p,2),partdiff(f,p,3) ]|
proof
grad(f,p) = |[ partdiff(f,p,1)*1,partdiff(f,p,1)*0,partdiff(f,p,1)*0 ]|+
partdiff(f,p,2)*|[ 0,jj,0 ]|+partdiff(f,p,3)*|[ 0,0,jj ]| by EUCLID_8:59
.= |[ partdiff(f,p,1),0,0 ]|+|[ partdiff(f,p,2)*0,partdiff(f,p,2)*1,
partdiff(f,p,2)*0 ]|+partdiff(f,p,3)*|[ 0,0,jj ]| by EUCLID_8:59
.= |[ partdiff(f,p,1),0,0 ]|+|[ 0,partdiff(f,p,2),0 ]|+
|[ partdiff(f,p,3)*0,partdiff(f,p,3)*0,partdiff(f,p,3)*1 ]| by EUCLID_8:59
.= |[ partdiff(f,p,1)+0,0+partdiff(f,p,2),0+0 ]|+|[ 0,0,partdiff(f,p,3) ]|
by Lm4
.= |[ partdiff(f,p,1)+0,partdiff(f,p,2)+0,0+partdiff(f,p,3) ]| by Lm4
.= |[ partdiff(f,p,1),partdiff(f,p,2),partdiff(f,p,3) ]|;
hence thesis;
end;
theorem Th35:
(f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 &
f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 &
g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3)
implies grad(f+g,p) = grad(f,p)+grad(g,p)
proof
assume that
A1: f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 &
f is_partial_differentiable_in p,3 and
A2: g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 &
g is_partial_differentiable_in p,3;
grad(f+g,p)
= |[ partdiff(f+g,p,1),partdiff(f+g,p,2),partdiff(f+g,p,3) ]| by Th34
.= |[ partdiff(f,p,1)+partdiff(g,p,1),partdiff(f+g,p,2),partdiff(f+g,p,3) ]|
by A1,A2,PDIFF_1:29
.= |[ partdiff(f,p,1)+partdiff(g,p,1),partdiff(f,p,2)+partdiff(g,p,2),
partdiff(f+g,p,3) ]| by A1,A2,PDIFF_1:29
.= |[ partdiff(f,p,1)+partdiff(g,p,1),partdiff(f,p,2)+partdiff(g,p,2),
partdiff(f,p,3)+partdiff(g,p,3) ]| by A1,A2,PDIFF_1:29
.= |[ partdiff(f,p,1),partdiff(f,p,2),partdiff(f,p,3) ]|+
|[ partdiff(g,p,1),partdiff(g,p,2),partdiff(g,p,3) ]| by Lm4
.= grad(f,p)+|[ partdiff(g,p,1),partdiff(g,p,2),partdiff(g,p,3) ]| by Th34
.= grad(f,p)+grad(g,p) by Th34;
hence thesis;
end;
theorem Th36:
(f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 &
f is_partial_differentiable_in p,3 & g is_partial_differentiable_in p,1 &
g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3)
implies grad(f-g,p) = grad(f,p)-grad(g,p)
proof
assume that
A1: f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 &
f is_partial_differentiable_in p,3 and
A2: g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 &
g is_partial_differentiable_in p,3;
grad(f-g,p)
= |[ partdiff(f-g,p,1),partdiff(f-g,p,2),partdiff(f-g,p,3) ]| by Th34
.= |[ partdiff(f,p,1)-partdiff(g,p,1),
partdiff(f-g,p,2),partdiff(f-g,p,3) ]| by A1,A2,PDIFF_1:31
.= |[ partdiff(f,p,1)-partdiff(g,p,1),partdiff(f,p,2)-partdiff(g,p,2),
partdiff(f-g,p,3) ]| by A1,A2,PDIFF_1:31
.= |[ partdiff(f,p,1)-partdiff(g,p,1),partdiff(f,p,2)-partdiff(g,p,2),
partdiff(f,p,3)-partdiff(g,p,3) ]| by A1,A2,PDIFF_1:31
.= |[ partdiff(f,p,1)+-partdiff(g,p,1),partdiff(f,p,2)+-partdiff(g,p,2),
partdiff(f,p,3)+-partdiff(g,p,3) ]|
.= |[ partdiff(f,p,1),partdiff(f,p,2),partdiff(f,p,3) ]|+
|[ -partdiff(g,p,1),-partdiff(g,p,2),-partdiff(g,p,3) ]| by Lm4
.= grad(f,p)+|[ (-1)*partdiff(g,p,1),(-1)*partdiff(g,p,2),
(-1)*partdiff(g,p,3) ]| by Th34
.= grad(f,p)+(-1)*|[ partdiff(g,p,1),partdiff(g,p,2),partdiff(g,p,3) ]|
by EUCLID_8:59
.= grad(f,p)-grad(g,p) by Th34;
hence thesis;
end;
theorem Th37:
(f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 &
f is_partial_differentiable_in p,3) implies grad(r(#)f,p) = r*grad(f,p)
proof
assume
A1: f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 &
f is_partial_differentiable_in p,3;
reconsider r as Real;
grad(r(#)f,p)
= |[ partdiff(r(#)f,p,1),partdiff(r(#)f,p,2),partdiff(r(#)f,p,3) ]|
by Th34
.= |[ r*partdiff(f,p,1),partdiff(r(#)f,p,2),partdiff(r(#)f,p,3) ]|
by A1,PDIFF_1:33
.= |[ r*partdiff(f,p,1),r*partdiff(f,p,2),partdiff(r(#)f,p,3)]|
by A1,PDIFF_1:33
.= |[ r*partdiff(f,p,1),r*partdiff(f,p,2),r*partdiff(f,p,3) ]|
by A1,PDIFF_1:33
.= r*|[ partdiff(f,p,1),partdiff(f,p,2),partdiff(f,p,3) ]| by EUCLID_8:59
.= r*grad(f,p) by Th34;
hence thesis;
end;
theorem
(f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 &
f is_partial_differentiable_in p,3) & (g is_partial_differentiable_in p,1 &
g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3)
implies grad(s(#)f+t(#)g,p) = s*grad(f,p)+t*grad(g,p)
proof
assume that
A1: f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 &
f is_partial_differentiable_in p,3 and
A2: g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 &
g is_partial_differentiable_in p,3;
reconsider s,t as Real;
A3: s(#)f is_partial_differentiable_in p,1 &
s(#)f is_partial_differentiable_in p,2 &
s(#)f is_partial_differentiable_in p,3 by A1,PDIFF_1:33;
t(#)g is_partial_differentiable_in p,1 &
t(#)g is_partial_differentiable_in p,2 &
t(#)g is_partial_differentiable_in p,3 by A2,PDIFF_1:33;
then grad(s(#)f+t(#)g,p) = grad(s(#)f,p)+grad(t(#)g,p) by A3,Th35
.= s*grad(f,p)+grad(t(#)g,p) by A1,Th37
.= s*grad(f,p)+t*grad(g,p) by A2,Th37;
hence thesis;
end;
theorem
(f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 &
f is_partial_differentiable_in p,3) & (g is_partial_differentiable_in p,1 &
g is_partial_differentiable_in p,2 & g is_partial_differentiable_in p,3)
implies grad(s(#)f-t(#)g,p) = s*grad(f,p)-t*grad(g,p)
proof
assume that
A1: f is_partial_differentiable_in p,1 & f is_partial_differentiable_in p,2 &
f is_partial_differentiable_in p,3 and
A2: g is_partial_differentiable_in p,1 & g is_partial_differentiable_in p,2 &
g is_partial_differentiable_in p,3;
reconsider s,t as Real;
A3: s(#)f is_partial_differentiable_in p,1 &
s(#)f is_partial_differentiable_in p,2 &
s(#)f is_partial_differentiable_in p,3 by A1,PDIFF_1:33;
t(#)g is_partial_differentiable_in p,1 &
t(#)g is_partial_differentiable_in p,2 &
t(#)g is_partial_differentiable_in p,3 by A2,PDIFF_1:33;
then grad(s(#)f-t(#)g,p) = grad(s(#)f,p)-grad(t(#)g,p) by A3,Th36
.= s*grad(f,p)-grad(t(#)g,p) by A1,Th37
.= s*grad(f,p)-t*grad(g,p) by A2,Th37;
hence thesis;
end;
theorem
f is total & f is constant implies grad(f,p) = 0.REAL 3
proof
assume
A1: f is total & f is constant;
then A2: dom f = REAL 3 by FUNCT_2:def 1;
REAL = [#]REAL;
then reconsider W = REAL as open Subset of REAL;
consider a being Element of REAL such that
A3: for p st p in REAL 3 holds f.p = a by A1,A2,PARTFUN2:def 1;
now
let x be Element of REAL;
assume x in dom (f*reproj(1,p));then
(f*reproj(1,p)).x = f.(reproj(1,p).x) by FUNCT_1:12;
hence (f*reproj(1,p)).x = a by A3;
end; then
A4: f*reproj(1,p) is constant by PARTFUN2:def 1;
set g1 = f*reproj(1,p);
A5: dom g1 = W by A1,FUNCT_2:def 1;
A6: g1|W is constant by A4;
then A7: g1 is_differentiable_on REAL by A5,FDIFF_1:22;
for x st x in REAL holds diff(g1,x) = 0
proof
let x;
assume x in REAL;
reconsider x as Element of REAL by XREAL_0:def 1;
diff(g1,x) = (g1`|W).x by A7,FDIFF_1:def 7
.= 0 by A5,A6,FDIFF_1:22;
hence thesis;
end;
then A8: partdiff(f,p,1) = 0;
now
let y be Element of REAL;
assume y in dom (f*reproj(2,p));then
(f*reproj(2,p)).y = f.(reproj(2,p).y) by FUNCT_1:12;
hence (f*reproj(2,p)).y = a by A3;
end;
then
A9: f*reproj(2,p) is constant by PARTFUN2:def 1;
set g2 = f*reproj(2,p);
A10: dom g2 = W by A1,FUNCT_2:def 1;
A11: g2|W is constant by A9;
then A12: g2 is_differentiable_on REAL & for y being Real st y in REAL
holds (g2`|W).y = 0 by A10,FDIFF_1:22;
for y st y in REAL holds diff(g2,y) = 0
proof
let y;
assume y in REAL;
reconsider y as Element of REAL by XREAL_0:def 1;
diff(g2,y) = (g2`|W).y by A12,FDIFF_1:def 7
.= 0 by A10,A11,FDIFF_1:22;
hence thesis;
end;
then A13: partdiff(f,p,2) = 0;
now
let z be Element of REAL;
assume z in dom (f*reproj(3,p));then
(f*reproj(3,p)).z = f.(reproj(3,p).z) by FUNCT_1:12;
hence (f*reproj(3,p)).z = a by A3;
end;
then
A14: f*reproj(3,p) is constant by PARTFUN2:def 1;
set g3 = f*reproj(3,p);
A15: dom g3 = W by A1,FUNCT_2:def 1;
A16: g3|W is constant by A14;
then A17: g3 is_differentiable_on REAL & for z being Real st z in REAL
holds (g3`|W).z = 0 by A15,FDIFF_1:22;
for z st z in REAL holds diff(g3,z) = 0
proof
let z;
assume z in REAL;
reconsider z as Element of REAL by XREAL_0:def 1;
diff(g3,z) = (g3`|W).z by A17,FDIFF_1:def 7
.= 0 by A15,A16,FDIFF_1:22;
hence thesis;
end;
then partdiff(f,p,3) = 0;
then grad(f,p) = |[ 0,0,0 ]| by A8,A13,Th34
.= 0.REAL 3 by FINSEQ_2:62;
hence thesis;
end;
definition
let a be Element of REAL 3;
func unitvector(a) -> Element of REAL 3 equals
|[ a.1/sqrt((a.1)^2+(a.2)^2+(a.3)^2),a.2/sqrt((a.1)^2+(a.2)^2+(a.3)^2),
a.3/sqrt((a.1)^2+(a.2)^2+(a.3)^2) ]|;
coherence;
end;
definition
let f be PartFunc of REAL 3,REAL;
let p, a be Element of REAL 3;
func Directiondiff(f,p,a) -> Real equals
partdiff(f,p,1)*(unitvector(a)).1+
partdiff(f,p,2)*(unitvector(a)).2+
partdiff(f,p,3)*(unitvector(a)).3;
coherence;
end;
theorem
a = <*x0,y0,z0*> implies Directiondiff(f,p,a) =
partdiff(f,p,1)*x0/sqrt(x0^2+y0^2+z0^2)+
partdiff(f,p,2)*y0/sqrt(x0^2+y0^2+z0^2)+
partdiff(f,p,3)*z0/sqrt(x0^2+y0^2+z0^2)
proof
assume
A1: a = <*x0,y0,z0*>;
Directiondiff(f,p,a) = partdiff(f,p,1)*(a.1/sqrt((a.1)^2+(a.2)^2+(a.3)^2))+
partdiff(f,p,2)*(unitvector(a)).2+partdiff(f,p,3)*(unitvector(a)).3
.= partdiff(f,p,1)*a.1/sqrt((a.1)^2+(a.2)^2+(a.3)^2)+
partdiff(f,p,2)*(unitvector(a)).2+partdiff(f,p,3)*(unitvector(a)).3
by XCMPLX_1:74
.= partdiff(f,p,1)*a.1/sqrt((a.1)^2+(a.2)^2+(a.3)^2)+
partdiff(f,p,2)*(a.2/sqrt((a.1)^2+(a.2)^2+(a.3)^2))+
partdiff(f,p,3)*(unitvector(a)).3
.= partdiff(f,p,1)*a.1/sqrt((a.1)^2+(a.2)^2+(a.3)^2)+
partdiff(f,p,2)*a.2/sqrt((a.1)^2+(a.2)^2+(a.3)^2)+
partdiff(f,p,3)*(unitvector(a)).3 by XCMPLX_1:74
.= partdiff(f,p,1)*a.1/sqrt((a.1)^2+(a.2)^2+(a.3)^2)+
partdiff(f,p,2)*a.2/sqrt((a.1)^2+(a.2)^2+(a.3)^2)+
partdiff(f,p,3)*(a.3/sqrt((a.1)^2+(a.2)^2+(a.3)^2))
.= partdiff(f,p,1)*a.1/sqrt((a.1)^2+(a.2)^2+(a.3)^2)+
partdiff(f,p,2)*a.2/sqrt((a.1)^2+(a.2)^2+(a.3)^2)+
partdiff(f,p,3)*a.3/sqrt((a.1)^2+(a.2)^2+(a.3)^2) by XCMPLX_1:74
.= partdiff(f,p,1)*x0/sqrt(x0^2+y0^2+z0^2)+
partdiff(f,p,2)*a.2/sqrt((a.1)^2+(a.2)^2+(a.3)^2)+
partdiff(f,p,3)*a.3/sqrt((a.1)^2+(a.2)^2+(a.3)^2) by A1
.= partdiff(f,p,1)*x0/sqrt(x0^2+y0^2+z0^2)+
partdiff(f,p,2)*y0/sqrt(x0^2+y0^2+z0^2)+
partdiff(f,p,3)*a.3/sqrt((a.1)^2+(a.2)^2+(a.3)^2) by A1
.= partdiff(f,p,1)*x0/sqrt(x0^2+y0^2+z0^2)+
partdiff(f,p,2)*y0/sqrt(x0^2+y0^2+z0^2)+
partdiff(f,p,3)*z0/sqrt(x0^2+y0^2+z0^2) by A1;
hence thesis;
end;
theorem
Directiondiff(f,p,a) = |( grad(f,p),unitvector(a) )|
proof
set p0 = grad(f,p);
reconsider g1=p0,g2=unitvector(a) as FinSequence of REAL;
A1: len g1 = len <* p0.1,p0.2,p0.3 *> by EUCLID_8:1
.= 3 by FINSEQ_1:45;
A2: len g2 = 3 by FINSEQ_1:45;
A3: p0 = |[ partdiff(f,p,1),partdiff(f,p,2),partdiff(f,p,3) ]| by Th34;
|( grad(f,p),unitvector(a) )|
= Sum <* g1.1*g2.1, g1.2*g2.2, g1.3*g2.3 *> by A1,A2,EUCLID_5:28
.= p0.1*g2.1+p0.2*g2.2+p0.3*g2.3 by RVSUM_1:78
.= partdiff(f,p,1)*g2.1+p0.2*g2.2+p0.3*g2.3 by A3
.= partdiff(f,p,1)*g2.1+partdiff(f,p,2)*g2.2+p0.3*g2.3
by A3
.= Directiondiff(f,p,a) by A3;
hence thesis;
end;
definition
let f1,f2,f3 be PartFunc of REAL 3,REAL;
let p be Element of REAL 3;
func curl(f1,f2,f3,p) -> Element of REAL 3 equals
(partdiff(f3,p,2)-partdiff(f2,p,3))*<e1>+
(partdiff(f1,p,3)-partdiff(f3,p,1))*<e2>+
(partdiff(f2,p,1)-partdiff(f1,p,2))*<e3>;
coherence;
end;
theorem
curl(f1,f2,f3,p) = |[ partdiff(f3,p,2)-partdiff(f2,p,3),
partdiff(f1,p,3)-partdiff(f3,p,1),partdiff(f2,p,1)-partdiff(f1,p,2) ]|
proof
curl(f1,f2,f3,p) = |[ (partdiff(f3,p,2)-partdiff(f2,p,3))*1,
(partdiff(f3,p,2)-partdiff(f2,p,3))*0,
(partdiff(f3,p,2)-partdiff(f2,p,3))*0 ]|+
(partdiff(f1,p,3)-partdiff(f3,p,1))*|[ 0,jj,0 ]|+
(partdiff(f2,p,1)-partdiff(f1,p,2))*|[ 0,0,jj]| by EUCLID_8:59
.= |[ partdiff(f3,p,2)-partdiff(f2,p,3),0,0 ]|+
|[ (partdiff(f1,p,3)-partdiff(f3,p,1))*0,
(partdiff(f1,p,3)-partdiff(f3,p,1))*1,
(partdiff(f1,p,3)-partdiff(f3,p,1))*0 ]|+
(partdiff(f2,p,1)-partdiff(f1,p,2))*|[ 0,0,jj ]| by EUCLID_8:59
.= |[ partdiff(f3,p,2)-partdiff(f2,p,3),0,0 ]|+
|[ 0,partdiff(f1,p,3)-partdiff(f3,p,1),0 ]|+
|[ (partdiff(f2,p,1)-partdiff(f1,p,2))*0,
(partdiff(f2,p,1)-partdiff(f1,p,2))*0,
(partdiff(f2,p,1)-partdiff(f1,p,2))*1 ]| by EUCLID_8:59
.= |[ (partdiff(f3,p,2)-partdiff(f2,p,3))+0,
0+(partdiff(f1,p,3)-partdiff(f3,p,1)),0+0 ]|+
|[ 0,0,partdiff(f2,p,1)-partdiff(f1,p,2) ]| by Lm4
.= |[ (partdiff(f3,p,2)-partdiff(f2,p,3))+0,
(partdiff(f1,p,3)-partdiff(f3,p,1))+0,
0+(partdiff(f2,p,1)-partdiff(f1,p,2)) ]| by Lm4
.= |[ partdiff(f3,p,2)-partdiff(f2,p,3),partdiff(f1,p,3)-partdiff(f3,p,1),
partdiff(f2,p,1)-partdiff(f1,p,2) ]|;
hence thesis;
end;