:: Partial Differentiation on Normed Linear Spaces $ {\cal R}^n$
:: by Noboru Endou , Yasunari Shidama and Keiichi Miyajima
::
:: Received June 6, 2007
:: Copyright (c) 2007-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, CARD_3, FUNCT_1, RELAT_1, FUNCT_2, FINSEQ_1,
FINSEQ_2, PARTFUN1, BORSUK_1, REAL_NS1, PRE_TOPC, AFINSQ_1, XBOOLE_0,
FDIFF_1, STRUCT_0, RLVECT_1, NORMSP_1, COMPLEX1, ARYTM_3, REAL_1,
ARYTM_1, SQUARE_1, RVSUM_1, LOPBAN_1, XXREAL_0, CARD_1, SUPINF_2, SEQ_1,
VALUED_1, SEQ_2, ORDINAL2, VALUED_0, TARSKI, NAT_1, RCOMP_1, XXREAL_1,
PDIFF_1, FCONT_1, FUNCT_7, XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1,
XCMPLX_0, FUNCT_2, FUNCT_7, PRE_TOPC, XREAL_0, COMPLEX1, ORDINAL1,
NUMBERS, REAL_1, RLVECT_1, VALUED_0, VALUED_1, SEQ_1, SEQ_2, RVSUM_1,
FINSEQ_1, FINSEQ_2, FINSEQ_7, SQUARE_1, RCOMP_1, VFUNCT_1, NORMSP_0,
NORMSP_1, EUCLID, LOPBAN_1, NFCONT_1, FDIFF_1, NDIFF_1, REAL_NS1,
XXREAL_0, STRUCT_0;
constructors REAL_1, SQUARE_1, RSSPACE3, SEQ_2, FINSEQ_7, VFUNCT_1, COMPLEX1,
NFCONT_1, RCOMP_1, FDIFF_1, NDIFF_1, REAL_NS1, EXTREAL1, RVSUM_1,
RELSET_1, BINOP_2, COMSEQ_2, XREAL_0, FUNCT_7, NUMBERS, GR_CY_1,
MONOID_0, VALUED_2;
registrations RELSET_1, STRUCT_0, ORDINAL1, XREAL_0, MEMBERED, LOPBAN_1,
FDIFF_1, NDIFF_1, FUNCT_1, FUNCT_2, NAT_1, REAL_NS1, NUMBERS, XBOOLE_0,
VALUED_0, VALUED_1, EUCLID, SQUARE_1, FINSEQ_1, RVSUM_1, NORMSP_1,
NORMSP_0, CARD_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TARSKI;
equalities LOPBAN_1, EUCLID;
expansions TARSKI;
theorems TARSKI, ABSVALUE, XBOOLE_0, XBOOLE_1, XREAL_0, RCOMP_1, RLVECT_1,
SEQ_4, COMPLEX1, SEQ_1, SEQ_2, FINSEQ_1, FINSEQ_2, FINSEQ_7, RVSUM_1,
RELAT_1, FUNCT_1, VFUNCT_1, FUNCT_2, NORMSP_1, LOPBAN_1, PARTFUN1,
PARTFUN2, NFCONT_1, FDIFF_1, NDIFF_1, FRECHET, REAL_NS1, VALUED_1,
VECTSP_1, NORMSP_0, CARD_1, ORDINAL1;
schemes SEQ_1, FUNCT_2, CLASSES1;
begin :: Preliminaries
definition
let i,n be Nat;
func proj(i,n) -> Function of REAL n,REAL means
:Def1:
for x be Element of REAL n holds it.x=x.i;
existence
proof
deffunc F(Element of REAL n) = In($1.i,REAL);
consider f being Function of REAL n,REAL such that
A1: for x being Element of REAL n
holds f.x = F(x) from FUNCT_2:sch 4;
take f;
let x be Element of REAL n;
f.x = F(x) by A1;
hence thesis;
end;
uniqueness
proof
let f,g be Function of REAL n,REAL;
assume that
A2: for x being Element of REAL n holds f.x = x.i and
A3: for x being Element of REAL n holds g.x = x.i;
now
let x be Element of REAL n;
f.x =x.i by A2;
hence f.x = g.x by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
set W = proj(1,1)qua Function";
Lm1: proj(1,1) is bijective & dom proj(1,1) = REAL 1 & rng proj(1,1) = REAL &
for x be Real holds proj(1,1).<*x*> = x & proj(1,1) qua Function".x
= <*x*>
proof
set f=proj(1,1);
for x1,x2 be object st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2
proof
let x1,x2 be object;
assume that
A1: x1 in dom f and
A2: x2 in dom f and
A3: f.x1 = f.x2;
reconsider y1=x1,y2=x2 as Element of REAL 1 by A1,A2;
x1 is Tuple of 1, REAL by A1,FINSEQ_2:131;
then consider d1 be Element of REAL such that
A4: x1=<*d1*> by FINSEQ_2:97;
d1 = <*d1*>.1;
then d1 = f.y1 by A4,Def1;
then
A5: d1 = y2.1 by A3,Def1;
x2 is Tuple of 1, REAL by A2,FINSEQ_2:131;
then ex d2 be Element of REAL st x2=<*d2*> by FINSEQ_2:97;
hence thesis by A4,A5;
end;
then
A6: f is one-to-one by FUNCT_1:def 4;
A7: dom f= REAL 1 by FUNCT_2:def 1;
A8: now
let x be Real;
reconsider xx=x as Element of REAL by XREAL_0:def 1;
A9: <*xx*> is Element of 1-tuples_on REAL by FINSEQ_2:98;
then proj(1,1).<*x*> =<*x*>.1 by Def1;
hence proj(1,1).<*x*> = x;
hence proj(1,1) qua Function".x = <*x*> by A7,A6,A9,FUNCT_1:34;
end;
A10: for y be object st y in REAL ex x be object st x in REAL 1 & y = f.x
proof
let y be object;
assume y in REAL;
then reconsider y1=y as Element of REAL;
reconsider x=<*y1*> as Element of REAL 1 by FINSEQ_2:98;
f.x = x.1 by Def1;
then f.x = y;
hence thesis;
end;
then rng f = REAL by FUNCT_2:10;
then f is onto by FUNCT_2:def 3;
hence thesis by A6,A10,A8,FUNCT_2:10,def 1;
end;
Lm2: for i, n be Nat st i in Seg n holds proj(i,n) is onto
proof
let i, n be Nat;
set f=proj(i,n);
assume
A1: i in Seg n;
for y be object st y in REAL ex x be object st x in REAL n & y = f.x
proof
let y be object;
assume y in REAL;
then reconsider y1 = y as Element of REAL;
reconsider x = n |-> y1 as Element of REAL n;
f.x = x.i by Def1;
then f.x = y by A1,FINSEQ_2:57;
hence thesis;
end;
then rng f = REAL by FUNCT_2:10;
hence thesis by FUNCT_2:def 3;
end;
theorem
(for i, n being Nat st i in Seg n holds dom proj(i,n) =
REAL n & rng proj(i,n) = REAL) & for x be Real holds proj(1,1).<*x*>
= x & proj(1,1) qua Function".x = <*x*>
proof
now
let i, n be Nat;
assume
A1: i in Seg n;
thus dom proj(i,n) = REAL n by FUNCT_2:def 1;
proj(i,n) is onto by A1,Lm2;
hence rng proj(i,n) = REAL by FUNCT_2:def 3;
end;
hence thesis by Lm1;
end;
theorem Th2:
proj(1,1) qua Function" is Function of REAL,REAL 1 &
proj(1,1) qua Function" is one-to-one &
dom(proj(1,1) qua Function") = REAL &
rng(proj(1,1) qua Function") = REAL 1 &
ex g be Function of REAL,REAL 1 st g is bijective
& proj(1,1) qua Function" = g
proof
A1: REAL 1 = rng(W) by Lm1,FUNCT_1:33;
REAL = dom(W) by Lm1,FUNCT_1:33;
then reconsider g=W as Function of REAL,REAL 1 by A1,FUNCT_2:1;
g is onto by A1,FUNCT_2:def 3;
hence thesis by Lm1,FUNCT_1:33;
end;
registration
cluster proj(1,1) -> bijective;
coherence by Lm1;
end;
definition
let g be PartFunc of REAL,REAL;
func <>*g -> PartFunc of REAL 1,REAL 1 equals
proj(1,1) qua Function" * g *
proj(1,1);
coherence
proof
reconsider f = proj(1,1) qua Function" as PartFunc of REAL,REAL 1 by
PARTFUN1:9;
f*g*proj(1,1) is PartFunc of REAL 1,REAL 1;
hence thesis;
end;
end;
definition
let n be Nat;
let g be PartFunc of REAL n,REAL;
func <>*g -> PartFunc of REAL n,REAL 1 equals
proj(1,1) qua Function" * g;
correctness
proof
reconsider f = proj(1,1) qua Function" as PartFunc of REAL,REAL 1 by
PARTFUN1:9;
f*g is PartFunc of REAL n,REAL 1;
hence thesis;
end;
end;
definition
let i,n be Nat;
func Proj(i,n) -> Function of REAL-NS n,REAL-NS 1 means
:Def4:
for x be Point of REAL-NS n holds it.x=<* proj(i,n).x *>;
existence
proof
deffunc F(Point of REAL-NS n) = <* proj(i,n).$1 *>;
A1: for x be Point of REAL-NS n holds F(x) is Element of REAL-NS 1
proof
let x be Point of REAL-NS n;
proj(i,n).x in REAL by XREAL_0:def 1; then
A2: F(x) is FinSequence of REAL by FINSEQ_1:74;
len F(x) = 1 by FINSEQ_1:39;
then F(x) is Element of 1-tuples_on REAL by A2,FINSEQ_2:92;
then F(x) in REAL 1;
hence thesis by REAL_NS1:def 4;
end;
thus ex f being Function of REAL-NS n,REAL-NS 1 st for x being Point of
REAL-NS n holds f.x = F(x) from FUNCT_2:sch 9(A1);
end;
uniqueness
proof
let f,g be Function of REAL-NS n, REAL-NS 1;
assume that
A3: for x being Point of REAL-NS n holds f.x = <* proj(i,n).x *> and
A4: for x being Point of REAL-NS n holds g.x = <* proj(i,n).x *>;
now
let x be Point of REAL-NS n;
f.x = <* proj(i,n).x *> by A3;
hence f.x = g.x by A4;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let i be Nat;
let x be FinSequence of REAL;
func reproj(i,x) -> Function means
:Def5:
dom it = REAL & for r be Element of REAL holds it.r = Replace(x,i,r);
existence
proof
deffunc F(Element of REAL) = Replace(x,i,$1);
consider f being Function such that
A1: dom f = REAL & for r being Element of REAL st r in REAL holds f.r
= F(r) from CLASSES1:sch 2;
take f;
thus thesis by A1;
end;
uniqueness
proof
let f,g be Function;
assume that
A2: dom f = REAL and
A3: for r being Element of REAL holds f.r = Replace(x,i,r) and
A4: dom g = REAL and
A5: for r being Element of REAL holds g.r = Replace(x,i,r);
now
let p be object;
assume p in dom f;
then reconsider r = p as Element of REAL by A2;
f.r = Replace(x,i,r) by A3;
hence f.p = g.p by A5;
end;
hence thesis by A2,A4,FUNCT_1:2;
end;
end;
definition
let n,i be Nat;
let x be Element of REAL n;
redefine func reproj(i,x) -> Function of REAL,REAL n; :: redefines reproj (PDIFF_1, definition)
correctness
proof
A1: now
let p be object;
assume p in REAL;
then reconsider r=p as Element of REAL;
A2: reproj(i,x).r = Replace(x,i,r) by Def5;
then reconsider IT = reproj(i,x).r as FinSequence of REAL;
len IT = len x by A2,FINSEQ_7:5
.= n by CARD_1:def 7;
then reconsider IT as Element of n-tuples_on REAL by FINSEQ_2:92;
IT is Element of REAL n;
hence reproj(i,x).p in REAL n;
end;
dom reproj(i,x) = REAL by Def5;
hence thesis by A1,FUNCT_2:3;
end;
end;
definition
let n,i be Nat;
let x be Point of REAL-NS n;
func reproj(i,x) -> Function of REAL-NS 1,REAL-NS n means
:Def6:
for r be
Element of REAL-NS 1 ex q be Element of REAL, y be Element of REAL n st r=<*q*>
& y=x & it.r = reproj(i,y).q;
existence
proof
defpred P[Element of REAL-NS 1, Point of REAL-NS n] means ex q be Element
of REAL, z be Element of REAL n st $1 = <*q*> & z = x & $2 = reproj(i,z).q;
A1: for r being Element of REAL-NS 1 ex y be Element of REAL-NS n st P[r,y ]
proof
reconsider z = x as Element of REAL n by REAL_NS1:def 4;
let r be Element of REAL-NS 1;
r is Element of REAL 1 by REAL_NS1:def 4;
then consider q be Element of REAL such that
A2: r=<*q*> by FINSEQ_2:97;
reproj(i,z).q is Element of REAL-NS n by REAL_NS1:def 4;
hence thesis by A2;
end;
thus ex f being Function of REAL-NS 1,REAL-NS n st for r be Element of
REAL-NS 1 holds P[r,f.r] from FUNCT_2:sch 3(A1);
end;
uniqueness
proof
let f,g be Function of REAL-NS 1,REAL-NS n;
assume that
A3: for r be Element of REAL-NS 1 ex q be Element of REAL, y be
Element of REAL n st r=<*q*> & y=x & f.r= reproj(i,y).q and
A4: for r be Element of REAL-NS 1 ex q be Element of REAL, y be
Element of REAL n st r=<*q*> & y=x & g.r= reproj(i,y).q;
now
let r be Point of REAL-NS 1;
consider p be Element of REAL, y be Element of REAL n such that
A5: r=<*p*> and
A6: y=x and
A7: f.r= reproj(i,y).p by A3;
A8: ex q be Element of REAL,z be Element of REAL n st r=<*q*> & z=x & g
.r= reproj(i,z).q by A4;
p = <*p*>.1;
hence f.r = g.r by A5,A6,A7,A8,FINSEQ_1:def 8;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let m,n be non zero Nat;
let f be PartFunc of REAL m,REAL n;
let x be Element of REAL m;
pred f is_differentiable_in x means
ex g be PartFunc of REAL-NS m,
REAL-NS n, y be Point of REAL-NS m st f=g & x=y & g is_differentiable_in y;
end;
definition
let m,n be non zero Nat;
let f be PartFunc of REAL m,REAL n;
let x be Element of REAL m;
assume
A1: f is_differentiable_in x;
func diff(f,x) -> Function of REAL m, REAL n means
:Def8:
ex g be PartFunc
of REAL-NS m,REAL-NS n, y be Point of REAL-NS m st f=g & x=y & it = diff(g,y);
correctness
proof
A2: the carrier of REAL-NS n = REAL n by REAL_NS1:def 4;
consider g be PartFunc of REAL-NS m,REAL-NS n, y be Point of REAL-NS m
such that
A3: f=g and
A4: x=y and
g is_differentiable_in y by A1;
the carrier of REAL-NS m = REAL m by REAL_NS1:def 4;
then diff(g,y) is Function of REAL m,REAL n by A2,LOPBAN_1:def 9;
hence thesis by A3,A4;
end;
end;
theorem Th3:
for I be Function of REAL,REAL 1 st I=proj(1,1) qua Function"
holds (for x be VECTOR of REAL-NS 1, y be Real st
x=I.y holds ||.x.|| = |.y.|) &
(for x,y be VECTOR of REAL-NS 1, a,b be Real st x=I.a
& y=I.b holds x+y = I.(a+b)) & (for x be VECTOR of REAL-NS 1,
y,a be Real st x=I.y holds a*x = I.(a*y)) &
(for x be VECTOR of REAL-NS 1,
a be Real st x=I.a holds -x = I.(-a)) & for x,y be
VECTOR of REAL-NS
1, a,b be Real st x=I.a & y=I.b holds x-y =I.(a-b)
proof
let I be Function of REAL,REAL 1;
assume
A1: I=proj(1,1) qua Function";
hereby
let x be VECTOR of REAL-NS 1, y be Real;
reconsider xx=x as Element of REAL 1 by REAL_NS1:def 4;
reconsider yy=y as Real;
reconsider yy2=yy^2 as Real;
assume x = I.y;
then xx = <*y*> by A1,Lm1;
then sqrt Sum sqr xx = sqrt Sum <*yy2*> by RVSUM_1:55;
then
A2: sqrt Sum sqr xx = sqrt (y^2) by RVSUM_1:73;
||.x.|| = |.xx.| by REAL_NS1:1;
hence ||.x.|| = |.y.| by A2,COMPLEX1:72;
end;
A3: now
let x,y be VECTOR of REAL-NS 1, a,b be Real;
reconsider xx=x, yy=y as Element of REAL 1 by REAL_NS1:def 4;
reconsider aa=a,bb=b as Real;
assume that
A4: x=I.a and
A5: y=I.b;
A6: <*b*> = yy by A1,A5,Lm1;
<*a*> = xx by A1,A4,Lm1;
then x-y = <*aa*> - <*bb*> by A6,REAL_NS1:5;
then x-y = <*a-b*> by RVSUM_1:29;
hence x-y =I.(a-b) by A1,Lm1;
end;
hereby
let x,y be VECTOR of REAL-NS 1, a,b be Real;
reconsider xx=x, yy = y as Element of REAL 1 by REAL_NS1:def 4;
reconsider aa=a,bb=b as Real;
assume that
A7: x=I.a and
A8: y=I.b;
A9: <*b*> = yy by A1,A8,Lm1;
<*a*> = xx by A1,A7,Lm1;
then x+y = <*aa*> + <*bb*> by A9,REAL_NS1:2;
then x+y =<*a+b*> by RVSUM_1:13;
hence x+y =I.(a + b) by A1,Lm1;
end;
A10: now
let x be VECTOR of REAL-NS 1, y,a be Real;
reconsider xx=x as Element of REAL 1 by REAL_NS1:def 4;
assume x=I.y;
then
A11: xx=<*y*> by A1,Lm1;
a*x = a*xx by REAL_NS1:3;
then a*x =<* a*y *> by A11,RVSUM_1:47;
hence a*x =I.(a*y) by A1,Lm1;
end;
now
let x be VECTOR of REAL-NS 1, a be Real;
assume x=I.a;
then (-1)*x = I.((-1)*a) by A10;
hence -x = I.(-a) by RLVECT_1:16;
end;
hence thesis by A10,A3;
end;
reconsider I = proj(1,1) qua Function" as Function of REAL,REAL 1 by Th2;
theorem Th4:
for J be Function of REAL 1,REAL st J=proj(1,1) holds (for x be
VECTOR of REAL-NS 1, y be Real st J.x=y holds ||.x.|| = |.y.|) &
(
for x,y be VECTOR of REAL-NS 1, a,b be Real st J.x=a & J.y=b holds
J
.(x+y) = a+b) & (for x be VECTOR of REAL-NS 1, y,a be Real
st J.x=y holds J.(a*x) = a*y) & (for x be VECTOR of REAL-NS 1, a be Real
st J.x=a holds J.(-x) = -a) & for x,y be VECTOR of REAL-NS 1, a,b be
Real st J.x=a & J.y=b holds J.(x-y) = a-b
proof
let J be Function of REAL 1,REAL;
assume
A1: J=proj(1,1);
hereby
let x be VECTOR of REAL-NS 1, y be Real;
reconsider xx=x as Element of REAL 1 by REAL_NS1:def 4;
assume J.x=y;
then I.(J.xx) = I.y;
then x = I.y by A1,Lm1,FUNCT_1:34;
hence ||.x.|| = |.y.| by Th3;
end;
hereby
let x,y be VECTOR of REAL-NS 1, a,b be Real;
reconsider xx=x, yy=y as Element of REAL 1 by REAL_NS1:def 4;
reconsider aa=a,bb=b as Element of REAL by XREAL_0:def 1;
assume that
A2: J.x=a and
A3: J.y=b;
I.(J.yy) = I.b by A3;
then
A4: y = I.b by A1,Lm1,FUNCT_1:34;
I.(J.xx) = I.a by A2;
then x = I.a by A1,Lm1,FUNCT_1:34;
then J.(x+y) = J.(I.(a+b)) by A4,Th3;
then J.(x+y) = J.(I.(aa+bb));
hence J.(x+y) = a+b by A1,Lm1,FUNCT_1:35;
end;
hereby
let x be VECTOR of REAL-NS 1, y,a be Real;
reconsider xx=x as Element of REAL 1 by REAL_NS1:def 4;
reconsider yy=y,aa=a as Element of REAL by XREAL_0:def 1;
assume J.x=y;
then I.(J.xx) = I.y;
then x = I.y by A1,Lm1,FUNCT_1:34;
then J.(a*x) = J.(I.(a*y)) by Th3;
then J.(a*x) = aa*yy by A1,Lm1,FUNCT_1:35;
hence J.(a*x) = a*y;
end;
hereby
let x be VECTOR of REAL-NS 1, y be Real;
reconsider xx=x as Element of REAL 1 by REAL_NS1:def 4;
reconsider yy=y as Element of REAL by XREAL_0:def 1;
assume J.x=y;
then I.y = I.(J.xx);
then x = I.y by A1,Lm1,FUNCT_1:34;
then J.(-x) = J.(I.(-y)) by Th3;
then J.(-x) = -yy by A1,Lm1,FUNCT_1:35;
hence J.(-x) = -y;
end;
let x,y be VECTOR of REAL-NS 1, a,b be Real;
reconsider xx=x, yy=y as Element of REAL 1 by REAL_NS1:def 4;
reconsider aa=a,bb=b as Element of REAL by XREAL_0:def 1;
assume that
A5: J.x=a and
A6: J.y=b;
I.(J.yy) = I.b by A6;
then
A7: y = I.b by A1,Lm1,FUNCT_1:34;
I.(J.xx) = I.a by A5;
then x = I.a by A1,Lm1,FUNCT_1:34;
then J.(x-y) =J.(I.(a - b)) by A7,Th3;
then J.(x-y) =aa-bb by A1,Lm1,FUNCT_1:35;
hence thesis;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
theorem Th5:
for I be Function of REAL,REAL 1, J be Function of REAL 1,REAL st
I=proj(1,1) qua Function" & J=proj(1,1) holds
(for R being RestFunc of REAL-NS 1, REAL-NS 1 holds J*R*I is RestFunc) &
for L being LinearOperator of REAL-NS 1, REAL-NS 1 holds
J*L*I is LinearFunc
proof
let I be Function of REAL,REAL 1, J be Function of REAL 1,REAL;
assume that
A1: I=proj(1,1) qua Function" and
A2: J=proj(1,1);
thus for R being RestFunc of REAL-NS 1, REAL-NS 1 holds J*R*I is RestFunc
proof
let R be RestFunc of REAL-NS 1,REAL-NS 1;
A3: R is total by NDIFF_1:def 5;
the carrier of REAL-NS 1 = REAL 1 by REAL_NS1:def 4;
then reconsider R0=R as Function of REAL 1,REAL 1 by A3;
reconsider R1=J*R*I as PartFunc of REAL,REAL;
A4: J*R0*I is Function of REAL,REAL;
then
A5: dom R1 = REAL by FUNCT_2:def 1;
A6: for r be Real st r > 0
ex d be Real st d > 0 & for z1 be Real st z1 <>
0 & |.z1.| < d holds |.z1.|"*|.R1.z1.| < r
proof
let r be Real;
assume r > 0;
then consider d be Real such that
A7: d > 0 and
A8: for z be Point of REAL-NS 1 st z <> 0.(REAL-NS 1) & ||.z.|| < d
holds ||.z.||"*||. R/.z .|| < r by A3,NDIFF_1:23;
take d;
for z1 be Real st
z1 <> 0 & |.z1.| < d holds |.z1.|" * |.R1.z1.| < r
proof
let z1 be Real such that
A9: z1 <> 0 and
A10: |.z1.| < d;
reconsider z1 as Element of REAL by XREAL_0:def 1;
reconsider z = I.z1 as Point of REAL-NS 1 by REAL_NS1:def 4;
|.z1.| > 0 by A9,COMPLEX1:47;
then ||.z.|| <> 0 by A1,Th3;
then
A11: z <> 0.(REAL-NS 1);
I*J =id dom(proj(1,1)) by A1,A2,FUNCT_1:39;
then
A12: I*J =id REAL 1 by FUNCT_2:def 1;
A13: dom(J*R0) = REAL 1 by FUNCT_2:def 1;
R is total by NDIFF_1:def 5;
then
A14: dom R = the carrier of REAL-NS 1 by PARTFUN1:def 2;
then R/.z = R.z by PARTFUN1:def 6;
then R/.z =((id the carrier of REAL-NS 1)*R).(I.z1) by FUNCT_2:17;
then R/.z =(I*J*R).(I.z1) by A12,REAL_NS1:def 4;
then
A15: R/.z =(I*J).(R.(I.z1)) by A14,FUNCT_1:13;
dom J = REAL 1 by FUNCT_2:def 1;
then R/.z =I.(J.(R0.z)) by A15,FUNCT_1:13,FUNCT_2:5;
then R/.z =I.((J*R0).(I.z1)) by A13,FUNCT_1:12;
then R/.z =I.(R1.z1) by A5,FUNCT_1:12;
then
A16: ||. R/.z .|| =|.R1.z1.| by A1,Th3;
A17: ||.z.||" = |.z1.|" by A1,Th3;
||.z.|| < d by A1,A10,Th3;
hence thesis by A8,A11,A17,A16;
end;
hence thesis by A7;
end;
for h be 0-convergent non-zero Real_Sequence holds h"(#)(R1/*h) is
convergent & lim(h"(#)(R1/*h)) = 0
proof
let h be 0-convergent non-zero Real_Sequence;
A18: now
let r0 be Real;
reconsider r = r0 as Real;
A19: lim h = 0;
assume r0 > 0;
then consider d be Real such that
A20: d > 0 and
A21: for z1 be Real st
z1 <> 0 & |.z1.| < d holds |.z1.|" * |.R1.z1.| < r by A6;
reconsider d1 =d as Real;
consider m be Nat such that
A22: for n be Nat st m <= n holds |.h.n-0 .| < d1 by A20,A19,
SEQ_2:def 7;
take m;
hereby
let n be Nat;
A23: h.n <> 0 by SEQ_1:5;
A24: n in NAT by ORDINAL1:def 12;
rng h c= dom R1 by A5;
then
A25: |.h.n.|" * |.R1.(h.n).| = |.h.n.|" * |.(R1/*h).n.| by FUNCT_2:108,A24
.= ((abs h).n)" * |.(R1/*h).n.| by SEQ_1:12
.= (abs h)".n * |.(R1/*h).n.| by VALUED_1:10
.= abs(h").n * |.(R1/*h).n.| by SEQ_1:54
.= |.h".n.| * |.(R1/*h).n.| by SEQ_1:12
.= |.h".n * (R1/*h).n.| by COMPLEX1:65
.= |.(h"(#)(R1/*h)).n - 0 .| by SEQ_1:8;
assume m <= n;
then |.h.n - 0 .| < d by A22;
hence |.(h"(#)(R1/*h)).n - 0 .| < r0 by A21,A23,A25;
end;
end;
hence h"(#)(R1/*h) is convergent by SEQ_2:def 6;
hence thesis by A18,SEQ_2:def 7;
end;
hence thesis by A4,FDIFF_1:def 2;
end;
thus for L being LinearOperator of REAL-NS 1,REAL-NS 1 holds
J*L*I is LinearFunc
proof
let L be LinearOperator of REAL-NS 1,REAL-NS 1;
A26: the carrier of REAL-NS 1 = REAL 1 by REAL_NS1:def 4;
then reconsider L0=L as Function of REAL 1, REAL 1;
reconsider L1=J*L0*I as PartFunc of REAL,REAL;
A27: dom(J*L0) = REAL 1 by FUNCT_2:def 1;
consider r be Real such that
A28: r = L1.1;
A29: dom(J*L0*I) = REAL by FUNCT_2:def 1;
A30: dom L0 = REAL 1 by FUNCT_2:def 1;
for p be Real holds L1.p = r*p
proof
reconsider 1p = I.jj as VECTOR of REAL-NS 1 by REAL_NS1:def 4;
let p be Real;
reconsider pp=p,jj=1 as Element of REAL by XREAL_0:def 1;
dom I = REAL by FUNCT_2:def 1;
then L1.p =(J*L).(I.(pp*jj)) by FUNCT_1:13;
then L1.p =(J*L).(p*1p) by A1,Th3;
then L1.p =J.(L.(p*1p)) by A26,A30,FUNCT_1:13;
then L1.p =J.(p*(L.1p)) by LOPBAN_1:def 5;
then L1.p =p*J.(L.1p) by A2,Th4;
then L1.p =p*((J*L0).(I.jj)) by A27,FUNCT_1:12;
hence thesis by A29,A28,FUNCT_1:12;
end;
hence thesis by FDIFF_1:def 3;
end;
end;
theorem Th6:
for I be Function of REAL,REAL 1, J be Function of REAL 1,REAL st
I=proj(1,1) qua Function" & J=proj(1,1) holds
(for R being RestFunc holds I*R*J is
RestFunc of REAL-NS 1,REAL-NS 1) &
for L being LinearFunc holds I*L*J is Lipschitzian
LinearOperator of REAL-NS 1,REAL-NS 1
proof
let I be Function of REAL,REAL 1, J be Function of REAL 1,REAL;
assume that
A1: I=proj(1,1) qua Function" and
A2: J=proj(1,1);
thus for R being RestFunc holds I*R*J is RestFunc of REAL-NS 1,REAL-NS 1
proof
let R be RestFunc;
R is total by FDIFF_1:def 2;
then reconsider R0=R as Function of REAL,REAL;
A3: the carrier of REAL-NS 1 = REAL 1 by REAL_NS1:def 4;
then reconsider R1 = I*R0*J as PartFunc of REAL-NS 1,REAL-NS 1;
for h be (0.(REAL-NS 1))-convergent non-zero sequence of REAL-NS 1
holds ||.h.||"(#)(R1/*h
) is convergent & lim(||.h.||"(#)(R1/*h)) = 0.(REAL-NS 1)
proof
let h be (0.(REAL-NS 1))-convergent non-zero sequence of REAL-NS 1;
A4: lim h = 0.(REAL-NS 1) by NDIFF_1:def 4;
deffunc F(Nat)=J.(h.$1);
consider s be Real_Sequence such that
A5: for n be Nat holds s.n = F(n) from SEQ_1:sch 1;
A6: h is convergent by NDIFF_1:def 4;
A7: now
let p be Real;
assume 0 < p;
then consider m be Nat such that
A8: for n be Nat st m <= n holds ||. h.n - 0.(REAL-NS
1).|| < p by A6,A4,NORMSP_1:def 7;
reconsider m as Nat;
take m;
now
let n be Nat;
assume
A9: m <= n;
reconsider nn=n as Nat;
||. h.nn - 0.(REAL-NS 1).|| < p by A8,A9;
then
A10: ||. h.nn .|| < p by RLVECT_1:13;
s.n = J.(h.n) by A5;
hence |.s.n-0 .| < p by A2,A10,Th4;
end;
hence for n be Nat st m <= n holds |.s.n-0 .|< p;
end;
then
A11: s is convergent by SEQ_2:def 6;
then
A12: lim s = 0 by A7,SEQ_2:def 7;
now
let x be object;
assume x in NAT;
then reconsider n=x as Element of NAT;
A13: 0 <= |.s.n.| by COMPLEX1:46;
h.n <> 0.(REAL-NS 1) by NDIFF_1:6;
then
A14: ||. h.n .|| <> 0 by NORMSP_0:def 5;
s.n = J.(h.n) by A5;
then |.s.x.| <> 0 by A2,A14,Th4;
hence s.x <> 0 by A13,COMPLEX1:47;
end;
then s is non-zero by SEQ_1:4;
then reconsider s as 0-convergent non-zero Real_Sequence by A11,A12,
FDIFF_1:def 1;
A15: J*I =id REAL by A1,A2,Lm1,FUNCT_1:39;
now
reconsider f1=R1 as Function;
let n be Element of NAT;
A16: rng h c= the carrier of REAL-NS 1;
h.n in the carrier of (REAL-NS 1);
then
A17: h.n in (REAL 1) by REAL_NS1:def 4;
A18: (R0*J).(h.n) in REAL by XREAL_0:def 1;
R1 is total by A3;
then (R/*s).n =R.(s.n) by FUNCT_2:115;
then (R/*s).n =R.(J.(h.n)) by A5;
then (R/*s).n =(J*I).(R0.(J.(h.n))) by A15;
then (R/*s).n =(J*I).((R0*J).(h.n)) by A17,FUNCT_2:15;
then (R/*s).n =J.(I.((R0*J).(h.n))) by FUNCT_2:15,A18;
then
A19: (R/*s).n =J.((I*(R0*J)).(h.n)) by A17,FUNCT_2:15;
NAT = dom h by FUNCT_2:def 1;
then
A20: R1.(h.n) =(f1*h).n by FUNCT_1:13;
dom R1 = REAL 1 by FUNCT_2:def 1;
then rng h c= dom R1 by A16,REAL_NS1:def 4;
then R1.(h.n) =(R1/*h).n by A20,FUNCT_2:def 11;
then
A21: (R/*s).n =J.((R1/*h).n) by A19,RELAT_1:36;
A22: s.n = J.(h.n) by A5;
||. ||.h.||"(#)(R1/*h).|| .n = ||.(||.h.||"(#)(R1/*h)).n .|| by
NORMSP_0:def 4
.= ||.(||.h.||").n * (R1/*h).n .|| by NDIFF_1:def 2
.= |.(||.h.||").n.| * ||.(R1/*h).n .|| by NORMSP_1:def 1
.= |.(||.h.||.n)".| * ||.(R1/*h).n .|| by VALUED_1:10
.= |.||.h.n.||".| * ||.(R1/*h).n .|| by NORMSP_0:def 4
.= ||.h.n .||" *||.(R1/*h).n .|| by ABSVALUE:def 1
.= (|.s.n.|)" *||.(R1/*h).n .|| by A2,A22,Th4
.= (|.s.n.|)" *|.(R/*s).n.| by A2,A21,Th4
.= (|.s.n.|)" *(|.R/*s.|).n by SEQ_1:12
.= ((abs s).n)" *(|.R/*s.|).n by SEQ_1:12
.= ((abs s)").n *(|.R/*s.|).n by VALUED_1:10
.= ((abs s)"(#)|.R/*s.|).n by SEQ_1:8
.= (|.s".|(#)abs(R/*s)).n by SEQ_1:54;
hence ||. ||.h.||"(#)(R1/*h) .|| .n = (|.s"(#)(R/*s).|).n by SEQ_1:52;
end;
then
A23: ||. ||.h.||"(#)(R1/*h) .|| = |.s"(#)(R/*s).| by FUNCT_2:63;
A24: lim(s"(#)(R/*s))=0 by FDIFF_1:def 2;
A25: s"(#)(R/*s) is convergent by FDIFF_1:def 2;
then lim |.s"(#)(R/*s).| = |.lim(s"(#)(R/*s)).| by SEQ_4:14;
then
A26: lim |.s"(#)(R/*s).| =0 by A24,ABSVALUE:2;
A27: abs(s"(#)(R/*s)) is convergent by A25,SEQ_4:13;
A28: now
let p be Real;
assume 0 < p;
then consider m be Nat such that
A29: for n be Nat st m <= n holds |.||. ||.h.||"(#)(
R1/*h).||.n - 0 .| < p by A23,A27,A26,SEQ_2:def 7;
reconsider m as Nat;
take m;
let n be Nat;
assume m <= n;
then |.||. ||.h.||"(#)(R1/*h).|| .n - 0 .| < p by A29;
then
A30: |. ||.(||.h.||"(#)(R1/*h)).n.||.| < p by NORMSP_0:def 4;
||.(||.h.||"(#)(R1/*h)).n.|| < p by A30,ABSVALUE:def 1;
hence ||.(||.h.||"(#)(R1/*h)).n -0.(REAL-NS 1).|| < p by RLVECT_1:13;
end;
then ||.h.||"(#)(R1/*h) is convergent by NORMSP_1:def 6;
hence thesis by A28,NORMSP_1:def 7;
end;
hence thesis by A3,NDIFF_1:def 10;
end;
thus for L being LinearFunc holds I*L*J is Lipschitzian
LinearOperator of REAL-NS 1,REAL-NS 1
proof
let L be LinearFunc;
consider r be Real such that
A31: for p be Real holds L.p = r * p by FDIFF_1:def 3;
L is total by FDIFF_1:def 3;
then reconsider L0 = L as Function of REAL,REAL;
reconsider r as Real;
set K = |.r.|;
A32: the carrier of REAL-NS 1 = REAL 1 by REAL_NS1:def 4;
I*L0*J is Function of REAL 1,REAL 1;
then reconsider L1 = I*L*J as Function of REAL-NS 1,REAL-NS 1 by A32;
A33: dom L1 = REAL 1 by A32,FUNCT_2:def 1;
A34: dom L0 = REAL by FUNCT_2:def 1;
A35: now
let x,y be VECTOR of REAL-NS 1;
A36: J.x+J.y in REAL by XREAL_0:def 1;
A37: J.x in REAL by XREAL_0:def 1;
J.y in REAL by XREAL_0:def 1; then
I.(L.(J.y)) = (I*L).(J.y) by A34,FUNCT_1:13;
then
A38: I.(L.(J.y)) = L1.y by A32,A33,FUNCT_1:12;
L1.(x+y) =(I*L).(J.(x+y)) by A32,A33,FUNCT_1:12;
then L1.(x+y) =(I*L).(J.x+J.y) by A2,Th4;
then L1.(x+y) =I.(L.((J.x+J.y))) by A36,A34,FUNCT_1:13;
then L1.(x+y) =I.(r*(J.x+J.y)) by A31;
then L1.(x+y) =I.(r*J.x+r*J.y);
then L1.(x+y) =I.(L.(J.x)+(r*J.y)) by A31;
then
A39: L1.(x+y) =I.(L.(J.x)+L.(J.y)) by A31;
I.(L.(J.x)) = (I*L).(J.x) by A37,A34,FUNCT_1:13;
then I.(L.(J.x)) = L1.x by A32,A33,FUNCT_1:12;
hence L1.(x+y) =L1.x + L1.y by A1,A38,A39,Th3;
end;
now
let x be VECTOR of REAL-NS 1, a be Real;
reconsider aa=a as Real;
A40: J.x in REAL by XREAL_0:def 1;
A41: aa*J.x in REAL by XREAL_0:def 1;
L1.(a*x) =(I*L).(J.(a*x)) by A32,A33,FUNCT_1:12;
then L1.(a*x) =(I*L).(a*J.x) by A2,Th4;
then L1.(aa*x) =I.(L.((aa*J.x))) by A41,A34,FUNCT_1:13;
then L1.(a*x) =I.(r*(a*J.x)) by A31;
then L1.(a*x) =I.(a*(r*J.x));
then
A42: L1.(a*x) =I.(a*L.(J.x)) by A31;
I.(L.(J.x)) = (I*L).(J.x) by A40,A34,FUNCT_1:13;
then I.(L.(J.x)) = L1.x by A32,A33,FUNCT_1:12;
hence L1.(a*x) =a*(L1.x) by A1,A42,Th3;
end;
then reconsider L1 as LinearOperator of REAL-NS 1,REAL-NS 1 by A35,
VECTSP_1:def 20,LOPBAN_1:def 5;
A43: now
let x be VECTOR of REAL-NS 1;
J.x in REAL by XREAL_0:def 1; then
I.(L.(J.x)) =(I*L).(J.x) by A34,FUNCT_1:13;
then I.(L.(J.x)) =L1.x by A32,A33,FUNCT_1:12;
then ||. L1.x .|| =|.L.(J.x).| by A1,Th3;
then ||. L1.x .|| =|.r*J.x.| by A31;
then ||. L1.x .|| =|.r.|*|.J.x.| by COMPLEX1:65;
hence ||. L1.x .|| <= K* ||.x.|| by A2,Th4;
end;
0 <= K by COMPLEX1:46;
hence thesis by A43,LOPBAN_1:def 8;
end;
end;
reserve f for PartFunc of REAL-NS 1,REAL-NS 1;
reserve g for PartFunc of REAL,REAL;
reserve x for Point of REAL-NS 1;
reserve y for Real;
theorem Th7:
f=<>*g & x=<*y*> & f is_differentiable_in x implies g
is_differentiable_in y & diff(g,y) = (proj(1,1)*diff(f,x)*(proj(1,1)qua
Function")).1
proof
set J = proj(1,1) qua Function;
reconsider L = diff(f,x) as
Lipschitzian LinearOperator of REAL-NS 1,REAL-NS 1 by LOPBAN_1:def 9;
A1: rng g c= dom I by Th2;
reconsider L0=J*L*I as LinearFunc by Th5;
assume that
A2: f=<>*g and
A3: x=<*y*> and
A4: f is_differentiable_in x;
consider NN being Neighbourhood of x such that
A5: NN c= dom f and
A6: ex R being RestFunc of REAL-NS 1,REAL-NS 1 st for y be Point of REAL-NS
1 st y in NN holds f/.y - f/.x = diff(f,x).(y-x) + R/.(y-x) by A4,NDIFF_1:def 7
;
consider e be Real such that
A7: 0 < e and
A8: {z where z is Point of REAL-NS 1 : ||.z-x.|| < e} c= NN by NFCONT_1:def 1;
consider R being RestFunc of REAL-NS 1,REAL-NS 1 such that
A9: for x9 be Point of REAL-NS 1 st x9 in NN holds f/.x9 - f/.x = diff(f
,x).(x9-x) + R/.(x9-x) by A6;
set N={z where z is Point of REAL-NS 1 : ||.z-x.|| < e};
A10: N c= the carrier of REAL-NS 1
proof
let y be object;
assume y in N;
then ex z be Point of REAL-NS 1 st y=z & ||.z-x.|| < e;
hence thesis;
end;
then reconsider N as Neighbourhood of x by A7,NFCONT_1:def 1;
set N0={z where z is Element of REAL: |.z-y.| < e};
A11: N c= dom f by A5,A8;
now
let z be object;
hereby
assume z in N0;
then consider y9 be Element of REAL such that
A12: z=y9 and
A13: |.y9-y.| < e;
reconsider w=I.y9 as Point of REAL-NS 1 by REAL_NS1:def 4;
x=I.y by A3,Lm1;
then w-x=I.(y9-y) by Th3;
then ||.w-x.||=|.y9-y.| by Th3;
then w in {z0 where z0 is Point of REAL-NS 1 : ||.z0 - x.|| < e} by A13;
then J.w in J.:N by FUNCT_2:35;
hence z in J.:N by A12,Lm1,FUNCT_1:35;
end;
assume z in J.:N;
then consider ww be object such that
ww in REAL 1 and
A14: ww in N and
A15: z=J.ww by FUNCT_2:64;
consider w be Point of REAL-NS 1 such that
A16: ww=w and
A17: ||.w-x.|| < e by A14;
reconsider y9=J.w as Element of REAL by XREAL_0:def 1;
J.x=y by A3,Lm1;
then J.(w-x) =y9-y by Th4;
then |.y9-y.| < e by A17,Th4;
hence z in N0 by A15,A16;
end;
then
A18: N0=J.:N by TARSKI:2;
dom f = J"(dom(I*g)) by A2,RELAT_1:147;
then J.:(dom f) = J.:(J"(dom g)) by A1,RELAT_1:27;
then
A19: J.:(dom f) = dom g by Lm1,FUNCT_1:77;
A20: I*J =id (REAL 1) by Lm1,FUNCT_1:39;
reconsider R0=J*R*I as RestFunc by Th5;
A21: J*I =id REAL by Lm1,FUNCT_1:39;
N c= dom f by A5,A8;
then
A22: N0 c= dom g by A19,A18,RELAT_1:123;
A23: ].y-e,y+e.[ c= N0
proof
let d be object such that
A24: d in ].y-e,y+e.[;
reconsider y0=d as Element of REAL by A24;
|.y0-y.| < e by A24,RCOMP_1:1;
hence thesis;
end;
N0 c= ].y-e,y+e.[
proof
let d be object;
assume d in N0;
then ex r be Element of REAL st d=r & |.r-y.| < e;
hence thesis by RCOMP_1:1;
end;
then N0 = ].y-e,y+e.[ by A23,XBOOLE_0:def 10;
then
A25: N0 is Neighbourhood of y by A7,RCOMP_1:def 6;
N c= REAL 1 by A10,REAL_NS1:def 4;
then (I*J).:N = N by A20,FRECHET:13;
then
A26: I.:N0 = N by A18,RELAT_1:126;
A27: for y0 be Real st
y0 in N0 holds g.y0 - g.y = L0.(y0-y) + R0.(y0-y)
proof
let y0 be Real;
reconsider yy0=y0,yy=y as Element of REAL by XREAL_0:def 1;
reconsider y9 = I.yy0 as Point of REAL-NS 1 by REAL_NS1:def 4;
R is total by NDIFF_1:def 5;
then
A28: dom R = the carrier of REAL-NS 1 by PARTFUN1:def 2;
R0 is total by FDIFF_1:def 2;
then dom(J*R*I) = REAL by PARTFUN1:def 2;
then yy0-yy in dom(J*R*I);
then
A29: y0-y in dom(J*(R*I)) by RELAT_1:36;
I.(yy0-yy) in REAL 1;
then I.(yy0-yy) in dom R by A28,REAL_NS1:def 4;
then J.(R/.(I.(yy0-yy))) =J.(R.(I.(yy0-yy))) by PARTFUN1:def 6;
then J.(R/.(I.(yy0-yy))) =J.((R*I).(yy0-yy)) by Th2,FUNCT_1:13;
then J.(R/.(I.(yy0-yy))) =(J*(R*I)).(yy0-yy) by A29,FUNCT_1:12;
then
A30: J.(R/.(I.(yy0-yy))) =R0.(yy0-yy) by RELAT_1:36;
L0 is total by FDIFF_1:def 3;
then dom(J*L*I) = REAL by PARTFUN1:def 2;
then yy0-yy in dom(J*L*I);
then
A31: y0-y in dom(J*(L*I)) by RELAT_1:36;
assume
A32: y0 in N0;
then
A33: I.yy0 in N by A26,FUNCT_2:35;
then J.(f/.(I.yy0)) =J.(f.(I.yy0)) by A11,PARTFUN1:def 6;
then
A34: J.(f/.(I.yy0)) =J.((f*I).yy0) by Th2,FUNCT_1:13;
J*f=J*(I*(g*J)) by A2,RELAT_1:36;
then
A35: J*f=(id REAL)*(g*J) by A21,RELAT_1:36;
rng(g*J) c= REAL;
then J*f*I = g*J*I by A35,RELAT_1:53;
then
A36: J*f*I = g*(id REAL) by A21,RELAT_1:36;
dom g c= REAL;
then
A37: g=J*f*I by A36,RELAT_1:51;
y0 in dom g by A22,A32;
then y0 in dom(J*(f*I)) by A37,RELAT_1:36;
then J.(f/.(I.y0)) =(J*(f*I)).y0 by A34,FUNCT_1:12;
then
A38: J.(f/.(I.y0)) =g.y0 by A37,RELAT_1:36;
A39: x=I.y by A3,Lm1;
set Iy = I.yy;
x in N by NFCONT_1:4;
then J.(f/.(I.y)) =J.(f.Iy) by A11,A39,PARTFUN1:def 6;
then
A40: J.(f/.Iy) =J.((f*I).yy) by Th2,FUNCT_1:13;
y in N0 by A25,RCOMP_1:16;
then y in dom g by A22;
then y in dom(J*(f*I)) by A37,RELAT_1:36;
then J.(f/.(I.y)) =(J*(f*I)).y by A40,FUNCT_1:12;
then
A41: J.(f/.(I.y)) =g.y by A37,RELAT_1:36;
J.(f/.y9 - f/.x)= J.(L.(y9-x) + R/.(y9-x)) by A9,A8,A33;
then J.(f/.y9)-J.(f/.x)=J.(L.(y9-x) + R/.(y9-x)) by Th4;
then J.(f/.(I.y0))-J.(f/.(I.y))=J.(L.(y9-x))+J.(R/.(y9-x)) by A39,Th4;
then
A42: J.(f/.(I.y0))-J.(f/.(I.y))=J.(L.(I.(y0-y))) + J.(R/.(y9-x)) by A39,Th3;
J.(L.(I.(yy0-yy))) =J.((L*I).(yy0-yy)) by Th2,FUNCT_1:13;
then J.(L.(I.(y0-y))) =(J*(L*I)).(y0-y) by A31,FUNCT_1:12;
then J.(L.(I.(y0-y))) =L0.(y0-y) by RELAT_1:36;
hence thesis by A39,A42,A38,A41,A30,Th3;
end;
hence g is_differentiable_in y by A25,A22,FDIFF_1:def 4;
hence thesis by A25,A22,A27,FDIFF_1:def 5;
end;
theorem Th8:
f=<>*g & x=<*y*> & g is_differentiable_in y implies f
is_differentiable_in x & diff(f,x).<*1*> =<*diff(g,y)*>
proof
set J =proj(1,1);
assume that
A1: f=<>*g and
A2: x=<*y*> and
A3: g is_differentiable_in y;
reconsider x0=y as Real;
consider N0 being Neighbourhood of x0 such that
A4: N0 c= dom g and
A5: ex L0 be LinearFunc, R0 be RestFunc st diff(g,x0)=L0.1 &
for y0 be Real st
y0 in N0 holds g.y0 - g.x0 = L0.(y0-x0) + R0.(y0-x0) by A3,FDIFF_1:def 5;
consider e0 be Real such that
A6: 0 < e0 and
A7: N0 = ].x0 - e0,x0 + e0.[ by RCOMP_1:def 6;
reconsider e = e0 as Real;
set N = {z where z is Point of REAL-NS 1 : ||.z-x.|| < e};
A8: rng(g*J) c= REAL;
consider L0 be LinearFunc, R0 be RestFunc such that
A9: diff(g,x0)=L0.1 and
A10: for y0 be Real st
y0 in N0 holds g.y0 - g.x0 = L0.(y0-x0) + R0.(y0-
x0) by A5;
reconsider R=I*R0*J as RestFunc of REAL-NS 1,REAL-NS 1 by Th6;
reconsider L=I*L0*J as Lipschitzian LinearOperator of REAL-NS 1,REAL-NS 1
by Th6;
A11: dom g c= REAL;
dom f c= the carrier of REAL-NS 1;
then
A12: dom f c= rng I by Th2,REAL_NS1:def 4;
A13: J*I=id REAL by Lm1,FUNCT_1:39;
now
let z be object;
hereby
assume z in N;
then consider w be Point of REAL-NS 1 such that
A14: z=w and
A15: ||.w-x.|| < e;
reconsider y=J.w as Element of REAL by XREAL_0:def 1;
J.x=x0 by A2,Lm1;
then J.(w-x) =y-x0 by Th4;
then |.y-x0.| < e by A15,Th4;
then
A16: y in N0 by A7,RCOMP_1:1;
w in the carrier of REAL-NS 1;
then w in dom J by Lm1,REAL_NS1:def 4;
then w=I.y by FUNCT_1:34;
hence z in I.:N0 by A14,A16,FUNCT_2:35;
end;
assume z in I.:N0;
then consider yy be object such that
A17: yy in REAL and
A18: yy in N0 and
A19: z=I.yy by FUNCT_2:64;
reconsider y=yy as Element of REAL by A17;
reconsider w=I.y as Point of REAL-NS 1 by REAL_NS1:def 4;
I.x0=x by A2,Lm1;
then
A20: w-x =I.(y-x0) by Th3;
|.y-x0.| < e by A7,A18,RCOMP_1:1;
then ||.w-x.|| < e by A20,Th3;
hence z in N by A19;
end;
then
A21: N=I.:N0 by TARSKI:2;
J*f=J*(I*(g*J)) by A1,RELAT_1:36;
then J*f=(id REAL)*(g*J) by A13,RELAT_1:36;
then J*f*I = g*J*I by A8,RELAT_1:53;
then J*f*I = g*(id REAL) by A13,RELAT_1:36;
then g=J*f*I by A11,RELAT_1:51;
then
A22: dom g = I"(dom(J*f)) by RELAT_1:147;
rng f c= the carrier of REAL-NS 1;
then rng f c= dom J by Lm1,REAL_NS1:def 4;
then I.:(dom g) = I.:(I"(dom f)) by A22,RELAT_1:27;
then I.:(dom g) = dom f by A12,FUNCT_1:77;
then
A23: N c= dom f by A4,A21,RELAT_1:123;
N c= the carrier of REAL-NS 1
proof
let y be object;
assume y in N;
then ex z be Point of REAL-NS 1 st y=z & ||.z-x.|| < e;
hence thesis;
end;
then
A24: N is Neighbourhood of x by A6,NFCONT_1:def 1;
J*I=id REAL by Lm1,FUNCT_1:39;
then (J*I).:N0 = N0 by FRECHET:13;
then
A25: J.:N = N0 by A21,RELAT_1:126;
A26: for y be Point of REAL-NS 1 st y in N holds f/.y - f/.x = L.(y-x) + R/.
(y-x)
proof
x in the carrier of REAL-NS 1;
then x in dom J by Lm1,REAL_NS1:def 4;
then
A27: I.(g.(J.x)) =I.((g*J).x) by FUNCT_1:13;
A28: x in N by A24,NFCONT_1:4;
then x in dom f by A23;
then x in dom(I*(g*J)) by A1,RELAT_1:36;
then I.(g.(J.x)) = (I*(g*J)).x by A27,FUNCT_1:12;
then I.(g.(J.x)) =f.x by A1,RELAT_1:36;
then
A29: I.(g.(J.x)) =f/.x by A23,A28,PARTFUN1:def 6;
let y be Point of REAL-NS 1;
assume
A30: y in N;
reconsider y0 = J.y as Element of REAL by XREAL_0:def 1;
reconsider y0x0 = y0 - x0 as Element of REAL by XREAL_0:def 1;
reconsider gy0 = g.y0, gx0 = g.x0, g0 = g.0 as Element of REAL
by XREAL_0:def 1;
reconsider L0y0x0 = L0.y0x0 as Element of REAL by XREAL_0:def 1;
reconsider R0y0x0 = R0.y0x0, Jyx = J.(y-x) as Element of REAL
by XREAL_0:def 1;
reconsider gJy = g.(J.y), gJx = g.(J.x) as Element of REAL
by XREAL_0:def 1;
reconsider R0Jyx = R0.Jyx, L0Jyx = L0.Jyx as Element of REAL
by XREAL_0:def 1;
reconsider p1=I.(gy0),p2=I.(gx0), q1=I.(L0y0x0), q2=I.(R0y0x0)
as VECTOR of REAL-NS 1 by REAL_NS1:def 4;
A31: J.x=x0 by A2,Lm1;
y in the carrier of REAL-NS 1;
then y in REAL 1 by REAL_NS1:def 4;
then I.(g.y0-g.x0) = I.(L0.(y0-x0) + R0.(y0-x0)) by A10,A25,A30,FUNCT_2:35;
then p1-p2=I.(L0.(y0-x0) + R0.(y0-x0)) by Th3;
then p1-p2=q1+q2 by Th3;
then I.(gy0) - I.gx0=q1+q2 by REAL_NS1:5;
then I.(gJy)-I.(gJx)=I.(L0y0x0) + I.(R0y0x0) by A31,REAL_NS1:2;
then I.(gJy)-I.(gJx)=I.(L0Jyx) + I.(R0y0x0) by A31,Th4;
then
A32: I.(gJy)-I.(gJx)=I.L0Jyx + I.R0Jyx by A31,Th4;
dom L = the carrier of REAL-NS 1 by FUNCT_2:def 1;
then y-x in dom(I*L0*J);
then
A33: y-x in dom(I*(L0*J)) by RELAT_1:36;
y-x in the carrier of REAL-NS 1;
then
A34: y-x in dom J by Lm1,REAL_NS1:def 4;
then
A35: I.(R0.(J.(y-x))) =I.((R0*J).(y-x)) by FUNCT_1:13;
R is total by NDIFF_1:def 5;
then
A36: dom(I*R0*J) = the carrier of REAL-NS 1 by PARTFUN1:def 2;
then y-x in dom(I*R0*J);
then y-x in dom(I*(R0*J)) by RELAT_1:36;
then I.(R0.(J.(y-x))) =(I*(R0*J)).(y-x) by A35,FUNCT_1:12;
then I.(R0.(J.(y-x))) =(I*R0*J).(y-x) by RELAT_1:36;
then
A37: I.(R0.(J.(y-x))) =R/.(y-x) by A36,PARTFUN1:def 6;
y in the carrier of REAL-NS 1;
then y in dom J by Lm1,REAL_NS1:def 4;
then
A38: I.(g.(J.y)) =I.((g*J).y) by FUNCT_1:13;
I.(L0.(J.(y-x))) =I.((L0*J).(y-x)) by A34,FUNCT_1:13;
then I.(L0.(J.(y-x))) =(I*(L0*J)).(y-x) by A33,FUNCT_1:12;
then
A39: I.(L0.(J.(y-x))) =L.(y-x) by RELAT_1:36;
y in dom f by A23,A30;
then y in dom(I*(g*J)) by A1,RELAT_1:36;
then I.(g.(J.y)) =(I*(g*J)).y by A38,FUNCT_1:12;
then I.(g.(J.y)) =f.y by A1,RELAT_1:36;
then I.(g.(J.y)) =f/.y by A23,A30,PARTFUN1:def 6;
then I.(gJy)-I.(gJx) = f/.y -f/.x by A29,REAL_NS1:5;
hence thesis by A32,A37,A39,REAL_NS1:2;
end;
L0 is total by FDIFF_1:def 3;
then
A40: dom L0 = REAL by PARTFUN1:def 2;
A41: L is Point of R_NormSpace_of_BoundedLinearOperators(REAL-NS 1,REAL-NS 1
) by LOPBAN_1:def 9;
then f is_differentiable_in x by A24,A23,A26,NDIFF_1:def 6;
then diff(f,x)=I*L0*J by A24,A23,A41,A26,NDIFF_1:def 7;
then diff(f,x).<*1*> =(I*L0*J).(I.1) by Lm1;
then diff(f,x).<*jj*> =(I*L0).(J.(I.jj)) by Lm1,FUNCT_1:13;
then diff(f,x).<*jj*> =I.(L0.(J.(I.jj))) by A40,FUNCT_1:13;
then diff(f,x).<*1*> =I.(L0.1) by Lm1,FUNCT_1:35;
hence thesis by A24,A23,A9,A41,A26,Lm1,NDIFF_1:def 6;
end;
theorem
f=<>*g & x=<*y*> implies (f is_differentiable_in x iff g
is_differentiable_in y) by Th7,Th8;
theorem Th10:
f=<>*g & x=<*y*> & f is_differentiable_in x implies diff(f,x).<*
1*>=<*diff(g,y)*>
proof
assume that
A1: f=<>*g and
A2: x=<*y*> and
A3: f is_differentiable_in x;
g is_differentiable_in y by A1,A2,A3,Th7;
hence thesis by A1,A2,Th8;
end;
begin :: Partial Differentiation
reserve m,n for non zero Nat;
reserve i,j for Nat;
reserve f for PartFunc of REAL-NS n,REAL-NS 1;
reserve g for PartFunc of REAL n,REAL;
reserve x for Point of REAL-NS n;
reserve y for Element of REAL n;
definition
let n,m be non zero Nat;
let i be Nat;
let f be PartFunc of REAL-NS m,REAL-NS n;
let x be Point of REAL-NS m;
pred f is_partial_differentiable_in x,i means
f*reproj(i,x) is_differentiable_in Proj(i,m).x;
end;
definition
let m,n be non zero Nat;
let i be Nat;
let f be PartFunc of REAL-NS m, REAL-NS n;
let x be Point of REAL-NS m;
func partdiff(f,x,i) -> Point of R_NormSpace_of_BoundedLinearOperators(
REAL-NS 1,REAL-NS n) equals
diff(f*reproj(i,x),Proj(i,m).x);
coherence;
end;
definition
let n be non zero Nat;
let i be Nat;
let f be PartFunc of REAL n,REAL;
let x be Element of REAL n;
pred f is_partial_differentiable_in x,i means
f*reproj(i,x) is_differentiable_in proj(i,n).x;
end;
definition
let n be non zero Nat;
let i be Nat;
let f be PartFunc of REAL n,REAL;
let x be Element of REAL n;
func partdiff(f,x,i) -> Real equals
diff(f*reproj(i,x),proj(i,n).x);
coherence;
end;
theorem Th11:
Proj(i,n)=proj(1,1)qua Function"*proj(i,n)
proof
reconsider h = proj(1,1)qua Function" as Function of REAL,REAL 1 by Th2;
A1: the carrier of REAL-NS n = REAL n by REAL_NS1:def 4;
A2: now
let x be Element of REAL n;
reconsider z=x as Point of REAL-NS n by REAL_NS1:def 4;
A3: (h*proj(i,n)).x =h.(proj(i,n).x) by FUNCT_2:15;
hence (h*proj(i,n)).x =<*proj(i,n).x*> by Lm1;
Proj(i,n).x =Proj(i,n).z;
then Proj(i,n).x =<*proj(i,n).x*> by Def4;
hence Proj(i,n).x = (h*proj(i,n)).x by A3,Lm1;
end;
the carrier of REAL-NS 1 = REAL 1 by REAL_NS1:def 4;
hence thesis by A1,A2,FUNCT_2:63;
end;
theorem Th12:
x = y implies reproj(i,y)*proj(1,1)=reproj(i,x)
proof
reconsider k = proj(1,1) as Function of REAL 1,REAL;
A1: the carrier of REAL-NS n = REAL n by REAL_NS1:def 4;
assume
A2: x=y;
A3: now
let s be Element of REAL 1;
reconsider r=s as Point of REAL-NS 1 by REAL_NS1:def 4;
A4: (reproj(i,y)*k).s = reproj(i,y).(k.s) by FUNCT_2:15;
ex q be Element of REAL, z be Element of REAL n st r=<*q *> & z=x &
reproj(i,x).r=reproj(i,z).q by Def6;
hence reproj(i,x).s=(reproj(i,y)*k).s by A2,A4,Lm1;
end;
the carrier of REAL-NS 1 = REAL 1 by REAL_NS1:def 4;
hence thesis by A1,A3,FUNCT_2:63;
end;
theorem Th13:
f=<>*g & x=y implies <>*(g*reproj(i,y)) = f*reproj(i,x)
proof
reconsider h=proj(1,1)qua Function" as Function of REAL,REAL 1 by Th2;
assume that
A1: f=<>*g and
A2: x=y;
reproj(i,y)*proj(1,1) = reproj(i,x) by A2,Th12;
then (h*g)*reproj(i,y)*proj(1,1) = f*reproj(i,x) by A1,RELAT_1:36;
hence thesis by RELAT_1:36;
end;
theorem Th14:
f=<>*g & x=y implies (f is_partial_differentiable_in x,i iff g
is_partial_differentiable_in y,i)
proof
assume that
A1: f=<>*g and
A2: x=y;
A3: <*proj(i,n).y*> = Proj(i,n).x by A2,Def4;
f*reproj(i,x)=<>*(g*reproj(i,y)) by A1,A2,Th13;
hence thesis by A3,Th7,Th8;
end;
theorem Th15:
f = <>*g & x = y & f is_partial_differentiable_in x,i implies
partdiff(f,x,i).<*1*> = <*partdiff(g,y,i)*>
proof
assume that
A1: f=<>*g and
A2: x=y and
A3: f is_partial_differentiable_in x,i;
A4: f*reproj(i,x) is_differentiable_in Proj(i,n).x by A3;
A5: <*proj(i,n).y*> = Proj(i,n).x by A2,Def4;
f*reproj(i,x) =<>*(g*reproj(i,y)) by A1,A2,Th13;
hence thesis by A4,A5,Th10;
end;
definition
let m,n be non zero Nat;
let i be Nat;
let f be PartFunc of REAL m,REAL n;
let x be Element of REAL m;
pred f is_partial_differentiable_in x,i means
ex g be PartFunc of
REAL-NS m,REAL-NS n, y be Point of REAL-NS m st f=g & x=y & g
is_partial_differentiable_in y,i;
end;
definition
let m,n be non zero Nat;
let i be Nat;
let f be PartFunc of REAL m,REAL n;
let x be Element of REAL m;
assume
A1: f is_partial_differentiable_in x,i;
func partdiff(f,x,i) -> Element of REAL n means
:Def14:
ex g be PartFunc of
REAL-NS m,REAL-NS n, y be Point of REAL-NS m st f=g & x=y & it = partdiff(g,y,i
).<*1*>;
correctness
proof
A2: the carrier of REAL-NS n = REAL n by REAL_NS1:def 4;
consider g be PartFunc of REAL-NS m,REAL-NS n, y be Point of REAL-NS m
such that
A3: f=g and
A4: x=y and
g is_partial_differentiable_in y,i by A1;
the carrier of REAL-NS 1 = REAL 1 by REAL_NS1:def 4;
then partdiff(g,y,i) is Function of REAL 1,REAL n by A2,LOPBAN_1:def 9;
then partdiff(g,y,i).<*jj*> is Element of REAL n by FINSEQ_2:98,FUNCT_2:5;
hence thesis by A3,A4;
end;
end;
theorem
for m,n be non zero Nat, F be PartFunc of REAL-NS m,
REAL-NS n, G be PartFunc of REAL m,REAL n, x be Point of REAL-NS m, y be
Element of REAL m st F = G & x = y holds F is_partial_differentiable_in x,i iff
G is_partial_differentiable_in y,i;
theorem Th17:
for m,n be non zero Nat, F be PartFunc of REAL-NS m,
REAL-NS n, G be PartFunc of REAL m,REAL n, x be Point of REAL-NS m, y be
Element of REAL m st F=G & x=y & F is_partial_differentiable_in x,i holds
partdiff(F,x,i).<*1*> = partdiff(G,y,i)
proof
let m,n be non zero Nat, F be PartFunc of REAL-NS m,REAL-NS n, G
be PartFunc of REAL m,REAL n, x be Point of REAL-NS m, y be Element of REAL m;
assume that
A1: F=G and
A2: x=y and
A3: F is_partial_differentiable_in x,i;
A4: the carrier of REAL-NS n = REAL n by REAL_NS1:def 4;
the carrier of REAL-NS 1 = REAL 1 by REAL_NS1:def 4;
then partdiff(F,x,i) is Function of REAL 1,REAL n by A4,LOPBAN_1:def 9;
then
A5: partdiff(F,x,i).<*jj*> is Element of REAL n by FINSEQ_2:98,FUNCT_2:5;
G is_partial_differentiable_in y,i by A1,A2,A3;
hence thesis by A1,A2,A5,Def14;
end;
theorem
for g1 be PartFunc of REAL n,REAL 1 holds g1 = <>*g implies (g1
is_partial_differentiable_in y,i iff g is_partial_differentiable_in y,i)
proof
let g1 be PartFunc of REAL n,REAL 1;
assume
A1: g1=<>*g;
reconsider y9=y as Point of REAL-NS n by REAL_NS1:def 4;
the carrier of REAL-NS 1 = REAL 1 by REAL_NS1:def 4;
then reconsider h=g1 as PartFunc of REAL-NS n,REAL-NS 1 by REAL_NS1:def 4;
h is_partial_differentiable_in y9,i iff g1 is_partial_differentiable_in
y, i;
hence thesis by A1,Th14;
end;
theorem
for g1 be PartFunc of REAL n,REAL 1 st g1 = <>*g & g1
is_partial_differentiable_in y,i holds partdiff(g1,y,i) = <*partdiff(g,y,i)*>
proof
let g1 be PartFunc of REAL n,REAL 1;
assume that
A1: g1=<>*g and
A2: g1 is_partial_differentiable_in y,i;
reconsider y9=y as Point of REAL-NS n by REAL_NS1:def 4;
the carrier of REAL-NS 1 = REAL 1 by REAL_NS1:def 4;
then reconsider h=g1 as PartFunc of REAL-NS n,REAL-NS 1 by REAL_NS1:def 4;
A3: h is_partial_differentiable_in y9,i by A2;
then partdiff(h,y9,i).<*1*>= partdiff(g1,y,i) by Th17;
hence thesis by A1,A3,Th15;
end;
begin :: Linearity of Partial Differential Operator
reserve X for set;
reserve r for Real;
reserve f,f1,f2 for PartFunc of REAL-NS m,REAL-NS n;
reserve g,g1,g2 for PartFunc of REAL n,REAL;
reserve h for PartFunc of REAL m,REAL n;
reserve x for Point of REAL-NS m;
reserve y for Element of REAL n;
reserve z for Element of REAL m;
definition
let m,n be non zero Nat;
let i,j be Nat;
let f be PartFunc of REAL-NS m,REAL-NS n;
let x be Point of REAL-NS m;
pred f is_partial_differentiable_in x,i,j means
Proj(j,n)*f*reproj(i ,x) is_differentiable_in Proj(i,m).x;
end;
definition
let m,n be non zero Nat;
let i,j be Nat;
let f be PartFunc of REAL-NS m,REAL-NS n;
let x be Point of REAL-NS m;
func partdiff(f,x,i,j) -> Point of R_NormSpace_of_BoundedLinearOperators(
REAL-NS 1,REAL-NS 1) equals
diff(Proj(j,n)*f*reproj(i,x),Proj(i,m).x);
correctness;
end;
definition
let m,n be non zero Nat;
let i,j be Nat;
let h be PartFunc of REAL m,REAL n;
let z be Element of REAL m;
pred h is_partial_differentiable_in z,i,j means
proj(j,n)*h*reproj(i ,z) is_differentiable_in proj(i,m).z;
end;
definition
let m,n be non zero Nat;
let i,j be Nat;
let h be PartFunc of REAL m,REAL n;
let z be Element of REAL m;
func partdiff(h,z,i,j) -> Real equals
diff(proj(j,n)*h*reproj(i,z),
proj(i,m).z);
correctness;
end;
theorem
for m,n be non zero Nat, F be PartFunc of REAL-NS m,
REAL-NS n, G be PartFunc of REAL m,REAL n, x be Point of REAL-NS m, y be
Element of REAL m st F=G & x=y holds F is_differentiable_in x iff G
is_differentiable_in y;
theorem
for m,n be non zero Nat, F be PartFunc of REAL-NS m,
REAL-NS n, G be PartFunc of REAL m,REAL n, x be Point of REAL-NS m, y be
Element of REAL m st F=G & x=y & F is_differentiable_in x holds diff(F,x)=diff(
G,y)
proof
let m,n be non zero Nat, F be PartFunc of REAL-NS m,REAL-NS n, G
be PartFunc of REAL m,REAL n, x be Point of REAL-NS m, y be Element of REAL m;
assume that
A1: F=G and
A2: x=y and
A3: F is_differentiable_in x;
A4: the carrier of REAL-NS n = REAL n by REAL_NS1:def 4;
the carrier of REAL-NS m = REAL m by REAL_NS1:def 4;
then
A5: diff(F,x) is Function of REAL m,REAL n by A4,LOPBAN_1:def 9;
G is_differentiable_in y by A1,A2,A3;
hence thesis by A1,A2,A5,Def8;
end;
theorem Th22:
f=h & x=z implies Proj(j,n)*f*reproj(i,x) = <>*(proj(j,n)*h* reproj(i,z))
proof
reconsider h1=proj(1,1)qua Function" as Function of REAL,REAL 1 by Th2;
assume that
A1: f=h and
A2: x=z;
<>*(proj(j,n)*h*reproj(i,z)) = h1*(proj(j,n)*(h*reproj(i,z)))*proj(1,1)
by RELAT_1:36
.= h1*proj(j,n)*(h*reproj(i,z))*proj(1,1) by RELAT_1:36
.= h1*proj(j,n)*(h*reproj(i,z)*proj(1,1)) by RELAT_1:36
.= h1*proj(j,n)*(h*(reproj(i,z)*proj(1,1))) by RELAT_1:36
.= Proj(j,n)*(h*(reproj(i,z)*proj(1,1))) by Th11
.= Proj(j,n)*(h*reproj(i,x)) by A2,Th12;
hence thesis by A1,RELAT_1:36;
end;
theorem
f = h & x = z implies (f is_partial_differentiable_in x,i,j iff
h is_partial_differentiable_in z,i,j)
proof
assume that
A1: f=h and
A2: x=z;
A3: Proj(i,m).x=<*proj(i,m).z*> by A2,Def4;
Proj(j,n)*f*reproj(i,x) = <>*(proj(j,n)*h*reproj(i,z)) by A1,A2,Th22;
hence thesis by A3,Th7,Th8;
end;
theorem
f=h & x=z & f is_partial_differentiable_in x,i,j implies
partdiff(f,x,i,j).<*1*> = <*partdiff(h,z,i,j)*>
proof
assume that
A1: f=h and
A2: x=z and
A3: f is_partial_differentiable_in x,i,j;
A4: Proj(i,m).x=<*proj(i,m).z*> by A2,Def4;
A5: Proj(j,n)*f*reproj(i,x) is_differentiable_in Proj(i,m).x by A3;
Proj(j,n)*f*reproj(i,x) =<>*(proj(j,n)*h*reproj(i,z)) by A1,A2,Th22;
hence thesis by A4,A5,Th10;
end;
definition
let m,n be non zero Nat;
let i be Nat;
let f be PartFunc of REAL-NS m,REAL-NS n;
let X be set;
pred f is_partial_differentiable_on X,i means
X c=dom f & for x be
Point of REAL-NS m st x in X holds f|X is_partial_differentiable_in x,i;
end;
theorem Th25:
f is_partial_differentiable_on X,i implies X is Subset of REAL-NS m
by XBOOLE_1:1;
definition
let m,n be non zero Nat;
let i be Nat;
let f be PartFunc of REAL-NS m,REAL-NS n;
let X;
assume
A1: f is_partial_differentiable_on X,i;
func f `partial|(X,i) -> PartFunc of REAL-NS m,
R_NormSpace_of_BoundedLinearOperators(REAL-NS 1,REAL-NS n) means
dom it = X &
for x be Point of REAL-NS m st x in X holds it/.x = partdiff(f,x,i);
existence
proof
deffunc F(Element of REAL-NS m) = partdiff(f,$1,i);
defpred P[Element of REAL-NS m] means $1 in X;
consider F being PartFunc of REAL-NS m,
R_NormSpace_of_BoundedLinearOperators(REAL-NS 1,REAL-NS n) such that
A2: (for x be Point of REAL-NS m holds x in dom F iff P[x]) & for x be
Point of REAL-NS m st x in dom F holds F.x = F(x) from SEQ_1:sch 3;
take F;
now
A3: X is Subset of REAL-NS m by A1,Th25;
let y be object;
assume y in X;
hence y in dom F by A2,A3;
end;
then
A4: X c= dom F;
for y be object st y in dom F holds y in X by A2;
then dom F c= X;
hence dom F = X by A4,XBOOLE_0:def 10;
hereby
let x be Point of REAL-NS m;
assume x in X;
then
A5: x in dom F by A2;
then F.x = partdiff(f,x,i) by A2;
hence F/.x = partdiff(f,x,i) by A5,PARTFUN1:def 6;
end;
end;
uniqueness
proof
let F,G be PartFunc of REAL-NS m,R_NormSpace_of_BoundedLinearOperators(
REAL-NS 1,REAL-NS n);
assume that
A6: dom F = X and
A7: for x be Point of REAL-NS m st x in X holds F/.x = partdiff(f,x,i ) and
A8: dom G = X and
A9: for x be Point of REAL-NS m st x in X holds G/.x = partdiff(f,x,i );
now
let x be Point of REAL-NS m;
assume
A10: x in dom F;
then F/.x = partdiff(f,x,i) by A6,A7;
hence F/.x=G/.x by A6,A9,A10;
end;
hence thesis by A6,A8,PARTFUN2:1;
end;
end;
theorem Th26:
(f1+f2)*reproj(i,x) = f1*reproj(i,x)+f2*reproj(i,x) & (f1-f2)*
reproj(i,x) = f1*reproj(i,x)-f2*reproj(i,x)
proof
A1: dom(reproj(i,x))=the carrier of REAL-NS 1 by FUNCT_2:def 1;
A2: dom(f1+f2) = dom f1 /\ dom f2 by VFUNCT_1:def 1;
for s be Element of REAL-NS 1 holds s in dom((f1+f2)*reproj(i,x)) iff s
in dom(f1*reproj(i,x)+f2*reproj(i,x))
proof
let s be Element of REAL-NS 1;
s in dom((f1+f2)*reproj(i,x)) iff reproj(i,x).s in dom f1 /\ dom f2 by A2
,A1,FUNCT_1:11;
then
s in dom((f1+f2)*reproj(i,x)) iff reproj(i,x).s in dom f1 & reproj(i,x
).s in dom f2 by XBOOLE_0:def 4;
then
s in dom((f1+f2)*reproj(i,x)) iff s in dom(f1*reproj(i,x)) & s in dom(
f2*reproj(i,x)) by A1,FUNCT_1:11;
then
s in dom((f1+f2)*reproj(i,x)) iff s in dom(f1*reproj(i,x)) /\ dom(f2*
reproj(i,x)) by XBOOLE_0:def 4;
hence thesis by VFUNCT_1:def 1;
end;
then
for s be object holds s in dom((f1+f2)*reproj(i,x)) iff s in dom(f1*reproj
(i,x) + f2*reproj(i,x));
then
A3: dom((f1+f2)*reproj(i,x)) = dom(f1*reproj(i,x)+f2*reproj(i,x)) by TARSKI:2;
A4: for z being Element of REAL-NS 1 st z in dom((f1+f2)*reproj(i,x)) holds
((f1+f2)*reproj(i,x)).z = (f1*reproj(i,x)+f2*reproj(i,x)).z
proof
let z be Element of REAL-NS 1;
assume
A5: z in dom((f1+f2)*reproj(i,x));
then
A6: reproj(i,x).z in dom(f1+f2) by FUNCT_1:11;
A7: reproj(i,x).z in dom f1 /\ dom f2 by A2,A5,FUNCT_1:11;
then
A8: reproj(i,x).z in dom f1 by XBOOLE_0:def 4;
then
A9: z in dom(f1*reproj(i,x)) by A1,FUNCT_1:11;
A10: reproj(i,x).z in dom f2 by A7,XBOOLE_0:def 4;
then
A11: z in dom(f2*reproj(i,x)) by A1,FUNCT_1:11;
A12: f2/.(reproj(i,x).z) = f2.(reproj(i,x).z) by A10,PARTFUN1:def 6
.=(f2*reproj(i,x)).z by A11,FUNCT_1:12
.=(f2*reproj(i,x))/.z by A11,PARTFUN1:def 6;
A13: f1/.(reproj(i,x).z) = f1.(reproj(i,x).z) by A8,PARTFUN1:def 6
.=(f1*reproj(i,x)).z by A9,FUNCT_1:12
.=(f1*reproj(i,x))/.z by A9,PARTFUN1:def 6;
((f1+f2)*reproj(i,x)).z = (f1+f2).(reproj(i,x).z) by A5,FUNCT_1:12
.=(f1+f2)/.(reproj(i,x).z) by A6,PARTFUN1:def 6
.= f1/.(reproj(i,x).z) +f2/.(reproj(i,x).z) by A6,VFUNCT_1:def 1
.=(f1*reproj(i,x)+ f2*reproj(i,x))/.z by A3,A5,A13,A12,VFUNCT_1:def 1;
hence thesis by A3,A5,PARTFUN1:def 6;
end;
A14: dom(f1-f2) = dom f1 /\ dom f2 by VFUNCT_1:def 2;
for s be Element of REAL-NS 1 holds s in dom((f1-f2)*reproj(i,x)) iff s
in dom(f1*reproj(i,x)-f2*reproj(i,x))
proof
let s be Element of REAL-NS 1;
s in dom((f1-f2)*reproj(i,x)) iff reproj(i,x).s in dom f1 /\ dom f2
by A14,A1,FUNCT_1:11;
then
s in dom((f1-f2)*reproj(i,x)) iff reproj(i,x).s in dom f1 & reproj(i,
x).s in dom f2 by XBOOLE_0:def 4;
then
s in dom((f1-f2)*reproj(i,x)) iff s in dom(f1*reproj(i,x)) & s in dom
(f2*reproj(i,x)) by A1,FUNCT_1:11;
then
s in dom((f1-f2)*reproj(i,x)) iff s in dom(f1*reproj(i,x)) /\ dom(f2*
reproj(i,x)) by XBOOLE_0:def 4;
hence thesis by VFUNCT_1:def 2;
end;
then
for s be object holds s in dom((f1-f2)*reproj(i,x)) iff s in dom(f1*reproj
(i,x) - f2*reproj(i,x));
then
A15: dom((f1-f2)*reproj(i,x)) = dom(f1*reproj(i,x)-f2*reproj(i,x)) by TARSKI:2;
for z being Element of REAL-NS 1 st z in dom((f1-f2)*reproj(i,x)) holds
((f1-f2)*reproj(i,x)).z = (f1*reproj(i,x)-f2*reproj(i,x)).z
proof
let z be Element of REAL-NS 1;
assume
A16: z in dom((f1-f2)*reproj(i,x));
then
A17: reproj(i,x).z in dom (f1-f2) by FUNCT_1:11;
A18: reproj(i,x).z in dom f1 /\ dom f2 by A14,A16,FUNCT_1:11;
then
A19: reproj(i,x).z in dom f1 by XBOOLE_0:def 4;
then
A20: z in dom(f1* reproj(i,x)) by A1,FUNCT_1:11;
A21: reproj(i,x).z in dom f2 by A18,XBOOLE_0:def 4;
then
A22: z in dom(f2* reproj(i,x)) by A1,FUNCT_1:11;
A23: f2/.(reproj(i,x).z) = f2.(reproj(i,x).z) by A21,PARTFUN1:def 6
.=(f2*reproj(i,x)).z by A22,FUNCT_1:12
.=(f2*reproj(i,x))/.z by A22,PARTFUN1:def 6;
A24: f1/.(reproj(i,x).z) = f1.(reproj(i,x).z) by A19,PARTFUN1:def 6
.=(f1*reproj(i,x)).z by A20,FUNCT_1:12
.=(f1*reproj(i,x))/.z by A20,PARTFUN1:def 6;
thus ((f1-f2)*reproj(i,x)).z =(f1-f2).(reproj(i,x).z) by A16,FUNCT_1:12
.=(f1-f2)/.(reproj(i,x).z) by A17,PARTFUN1:def 6
.= f1/.(reproj(i,x).z) - f2/.(reproj(i,x).z) by A17,VFUNCT_1:def 2
.=(f1*reproj(i,x)- f2*reproj(i,x))/.z by A15,A16,A24,A23,VFUNCT_1:def 2
.=(f1*reproj(i,x)- f2*reproj(i,x)).z by A15,A16,PARTFUN1:def 6;
end;
hence thesis by A3,A15,A4,PARTFUN1:5;
end;
theorem Th27:
r(#)(f*reproj(i,x)) = (r(#)f)*reproj(i,x)
proof
A1: dom(r(#)f) = dom f by VFUNCT_1:def 4;
A2: dom(r(#)(f*reproj(i,x))) =dom(f*reproj(i,x)) by VFUNCT_1:def 4;
A3: dom(reproj(i,x))=the carrier of REAL-NS 1 by FUNCT_2:def 1;
for s be Element of REAL-NS 1 holds s in dom((r(#)f)*reproj(i,x)) iff s
in dom(f*reproj(i,x))
proof
let s be Element of REAL-NS 1;
s in dom((r(#)f)*reproj(i,x)) iff reproj(i,x).s in dom(r(#)f) by A3,
FUNCT_1:11;
hence thesis by A1,A3,FUNCT_1:11;
end;
then for s be object
holds s in dom(r(#)(f*reproj(i,x))) iff s in dom((r(#)f)*
reproj(i,x)) by A2;
then
A4: dom(r(#)(f*reproj(i,x))) =dom((r(#)f)*reproj(i,x)) by TARSKI:2;
A5: for s be Element of REAL-NS 1 holds s in dom((r(#)f)*reproj(i,x)) iff
reproj(i,x).s in dom(r(#)f)
proof
let s be Element of REAL-NS 1;
dom(reproj(i,x))=the carrier of REAL-NS 1 by FUNCT_2:def 1;
hence thesis by FUNCT_1:11;
end;
for z being Element of REAL-NS 1 st z in dom(r(#)(f*reproj(i,x))) holds
(r(#)(f*reproj(i,x))).z = ((r(#)f)*reproj(i,x)).z
proof
let z be Element of REAL-NS 1;
assume
A6: z in dom(r(#)(f*reproj(i,x)));
then
A7: z in dom(f*reproj(i,x)) by VFUNCT_1:def 4;
A8: reproj(i,x).z in dom f by A1,A5,A4,A6;
then
A9: f/.(reproj(i,x).z) = f.(reproj(i,x).z) by PARTFUN1:def 6
.= (f*reproj(i,x)).z by A7,FUNCT_1:12
.= (f*reproj(i,x))/.z by A7,PARTFUN1:def 6;
A10: (r(#)(f*reproj(i,x))).z =(r(#)(f*reproj(i,x)))/.z by A6,PARTFUN1:def 6
.= r * f/.(reproj(i,x).z) by A6,A9,VFUNCT_1:def 4;
((r(#)f)*reproj(i,x)).z = (r(#)f).(reproj(i,x).z) by A4,A6,FUNCT_1:12
.= (r(#)f)/.(reproj(i,x).z) by A1,A8,PARTFUN1:def 6
.= r * f/.(reproj(i,x).z) by A1,A8,VFUNCT_1:def 4;
hence thesis by A10;
end;
hence thesis by A4,PARTFUN1:5;
end;
theorem Th28:
f1 is_partial_differentiable_in x,i & f2
is_partial_differentiable_in x,i implies f1+f2 is_partial_differentiable_in x,i
& partdiff(f1+f2,x,i)=partdiff(f1,x,i)+partdiff(f2,x,i)
proof
assume that
A1: f1 is_partial_differentiable_in x,i and
A2: f2 is_partial_differentiable_in x,i;
A3: f1*reproj(i,x) is_differentiable_in Proj(i,m).x by A1;
A4: f2*reproj(i,x) is_differentiable_in Proj(i,m).x by A2;
(f1+f2)*reproj(i,x) = f1*reproj(i,x)+f2*reproj(i,x) by Th26;
then (f1+f2)*reproj(i,x) is_differentiable_in Proj(i,m).x by A3,A4,NDIFF_1:35
;
hence f1+f2 is_partial_differentiable_in x,i;
diff(f1*reproj(i,x)+f2*reproj(i,x),Proj(i,m).x) = partdiff((f1+f2),x,i)
by Th26;
hence thesis by A3,A4,NDIFF_1:35;
end;
theorem
g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in
y,i implies g1+g2 is_partial_differentiable_in y,i & partdiff(g1+g2,y,i) =
partdiff(g1,y,i) + partdiff(g2,y,i)
proof
assume that
A1: g1 is_partial_differentiable_in y,i and
A2: g2 is_partial_differentiable_in y,i;
reconsider x=y as Point of REAL-NS n by REAL_NS1:def 4;
A3: the carrier of REAL-NS 1 = REAL 1 by REAL_NS1:def 4;
then reconsider f1=<>*g1, f2=<>*g2 as PartFunc of REAL-NS n,REAL-NS 1 by
REAL_NS1:def 4;
reconsider One = <*jj*> as VECTOR of REAL-NS 1 by A3,FINSEQ_2:98;
A4: f1 is_partial_differentiable_in x,i by A1,Th14;
then
A5: partdiff(f1,x,i).One = <*partdiff(g1,y,i)*> by Th15;
reconsider d2 = partdiff(g2,y,i) as Element of REAL by XREAL_0:def 1;
reconsider Pd2=<*d2*> as Element of REAL 1 by FINSEQ_2:98;
reconsider d1 = partdiff(g1,y,i) as Element of REAL by XREAL_0:def 1;
reconsider Pd1=<*d1*> as Element of REAL 1 by FINSEQ_2:98;
A6: the carrier of REAL-NS n = REAL n by REAL_NS1:def 4;
rng g2 c= dom W by Th2;
then
A7: dom(W*g2) = dom g2 by RELAT_1:27;
rng g1 c= dom W by Th2;
then
A8: dom(W*g1) = dom g1 by RELAT_1:27;
then dom(f1+f2) = dom g1 /\ dom g2 by A7,VFUNCT_1:def 1;
then
A9: dom(f1+f2) = dom(g1+g2) by VALUED_1:def 1;
A10: rng(g1+g2) c= dom W by Th2;
then
A11: dom(W*(g1+g2)) = dom(g1+g2) by RELAT_1:27;
A12: now
let x be Element of REAL-NS n;
assume
A13: x in dom(f1+f2);
then (f1+f2).x = (f1+f2)/.x by PARTFUN1:def 6;
then
A14: (f1+f2).x = f1/.x + f2/.x by A13,VFUNCT_1:def 1;
A15: x in dom f1 /\ dom f2 by A13,VFUNCT_1:def 1;
then x in dom f1 by XBOOLE_0:def 4;
then
A16: f1/.x = (W*g1).x by PARTFUN1:def 6;
x in dom f2 by A15,XBOOLE_0:def 4;
then
A17: f2/.x = (W*g2).x by PARTFUN1:def 6;
x in dom g2 by A7,A15,XBOOLE_0:def 4;
then
A18: f2/.x = W.(g2.x) by A17,FUNCT_1:13;
x in dom g1 by A8,A15,XBOOLE_0:def 4;
then
A19: f1/.x = W.(g1.x) by A16,FUNCT_1:13;
(<>*(g1+g2)).x = W.((g1+g2).x) by A9,A11,A13,FUNCT_1:12;
then (<>*(g1+g2)).x = W.(g1.x + g2.x) by A9,A13,VALUED_1:def 1;
hence (f1+f2).x = (<>*(g1+g2)).x by A14,A19,A18,Th2,Th3;
end;
A20: f2 is_partial_differentiable_in x,i by A2,Th14;
then
A21: partdiff(f2,x,i).One = <*partdiff(g2,y,i)*> by Th15;
A22: f1+f2 is_partial_differentiable_in x,i by A4,A20,Th28;
dom(f1+f2) = dom <>*(g1+g2) by A9,A10,RELAT_1:27;
then
A23: f1+f2 = <>*(g1+g2) by A6,A3,A12,PARTFUN1:5;
then <*partdiff(g1+g2,y,i)*> =partdiff(f1+f2,x,i).<*1*> by A4,A20,Th15,Th28
.=(partdiff(f1,x,i)+partdiff(f2,x,i)).<*1*> by A4,A20,Th28
.=partdiff(f1,x,i).One + partdiff(f2,x,i).One by LOPBAN_1:35
.=Pd1 + Pd2 by A5,A21,REAL_NS1:2
.=<*partdiff(g1,y,i)+partdiff(g2,y,i)*> by RVSUM_1:13;
then partdiff(g1+g2,y,i) =<*partdiff(g1,y,i) + partdiff(g2,y,i)*>.1;
hence thesis by A23,A22,Th14;
end;
theorem Th30:
f1 is_partial_differentiable_in x,i & f2
is_partial_differentiable_in x,i implies f1-f2 is_partial_differentiable_in x,i
& partdiff(f1-f2,x,i)=partdiff(f1,x,i)-partdiff(f2,x,i)
proof
assume that
A1: f1 is_partial_differentiable_in x,i and
A2: f2 is_partial_differentiable_in x,i;
A3: f1*reproj(i,x) is_differentiable_in Proj(i,m).x by A1;
A4: f2*reproj(i,x) is_differentiable_in Proj(i,m).x by A2;
(f1-f2)*reproj(i,x) = f1*reproj(i,x)-f2*reproj(i,x) by Th26;
then (f1-f2)*reproj(i,x) is_differentiable_in Proj(i,m).x by A3,A4,NDIFF_1:36
;
hence f1-f2 is_partial_differentiable_in x,i;
diff(f1*reproj(i,x)-f2*reproj(i,x),Proj(i,m).x) = partdiff(f1-f2,x,i) by Th26
;
hence thesis by A3,A4,NDIFF_1:36;
end;
theorem
g1 is_partial_differentiable_in y,i & g2 is_partial_differentiable_in
y,i implies g1-g2 is_partial_differentiable_in y,i & partdiff(g1-g2,y,i)=
partdiff(g1,y,i)-partdiff(g2,y,i)
proof
assume that
A1: g1 is_partial_differentiable_in y,i and
A2: g2 is_partial_differentiable_in y,i;
reconsider x=y as Point of REAL-NS n by REAL_NS1:def 4;
A3: the carrier of REAL-NS 1 = REAL 1 by REAL_NS1:def 4;
then reconsider f1=<>*g1, f2=<>*g2 as PartFunc of REAL-NS n,REAL-NS 1 by
REAL_NS1:def 4;
reconsider One = <*jj*> as VECTOR of REAL-NS 1 by A3,FINSEQ_2:98;
A4: f1 is_partial_differentiable_in x,i by A1,Th14;
then
A5: partdiff(f1,x,i).One = <*partdiff(g1,y,i)*> by Th15;
reconsider d2 = partdiff(g2,y,i) as Element of REAL by XREAL_0:def 1;
reconsider Pd2=<*d2*> as Element of REAL 1 by FINSEQ_2:98;
reconsider d1 = partdiff(g1,y,i) as Element of REAL by XREAL_0:def 1;
reconsider Pd1=<*d1*> as Element of REAL 1 by FINSEQ_2:98;
A6: the carrier of REAL-NS n = REAL n by REAL_NS1:def 4;
rng g2 c= dom(W) by Th2;
then
A7: dom(W*g2) = dom g2 by RELAT_1:27;
rng g1 c= dom(W) by Th2;
then
A8: dom(W*g1) = dom g1 by RELAT_1:27;
then dom(f1-f2) = dom g1 /\ dom g2 by A7,VFUNCT_1:def 2;
then
A9: dom(f1-f2) = dom(g1-g2) by VALUED_1:12;
A10: rng(g1-g2) c= dom(W) by Th2;
then
A11: dom(W*(g1-g2)) = dom(g1-g2) by RELAT_1:27;
A12: now
let x be Element of REAL-NS n;
assume
A13: x in dom(f1-f2);
then (f1-f2).x = (f1-f2)/.x by PARTFUN1:def 6;
then
A14: (f1-f2).x = f1/.x - f2/.x by A13,VFUNCT_1:def 2;
A15: x in dom f1 /\ dom f2 by A13,VFUNCT_1:def 2;
then x in dom f1 by XBOOLE_0:def 4;
then
A16: f1/.x = (W*g1).x by PARTFUN1:def 6;
x in dom f2 by A15,XBOOLE_0:def 4;
then
A17: f2/.x = (W*g2).x by PARTFUN1:def 6;
x in dom g2 by A7,A15,XBOOLE_0:def 4;
then
A18: f2/.x = W.(g2.x) by A17,FUNCT_1:13;
x in dom g1 by A8,A15,XBOOLE_0:def 4;
then
A19: f1/.x = W.(g1.x) by A16,FUNCT_1:13;
(<>*(g1-g2)).x = W.((g1-g2).x) by A9,A11,A13,FUNCT_1:12;
then (<>*(g1-g2)).x = W.(g1.x-g2.x) by A9,A13,VALUED_1:13;
hence (f1-f2).x = (<>*(g1-g2)).x by A14,A19,A18,Th2,Th3;
end;
A20: f2 is_partial_differentiable_in x,i by A2,Th14;
then
A21: partdiff(f2,x,i).One = <*partdiff(g2,y,i)*> by Th15;
A22: f1-f2 is_partial_differentiable_in x,i by A4,A20,Th30;
dom(f1-f2) = dom <>*(g1-g2) by A9,A10,RELAT_1:27;
then
A23: f1-f2=<>*(g1-g2) by A6,A3,A12,PARTFUN1:5;
then <*partdiff(g1-g2,y,i)*> = partdiff(f1-f2,x,i).<*1*> by A4,A20,Th15,Th30
.= (partdiff(f1,x,i)-partdiff(f2,x,i)).<*1*> by A4,A20,Th30
.= partdiff(f1,x,i).One - partdiff(f2,x,i).One by LOPBAN_1:40
.= Pd1 - Pd2 by A5,A21,REAL_NS1:5
.= <*partdiff(g1,y,i) - partdiff(g2,y,i)*> by RVSUM_1:29;
then partdiff(g1-g2,y,i) = <*partdiff(g1,y,i)-partdiff(g2,y,i)*>.1;
hence thesis by A23,A22,Th14;
end;
theorem Th32:
f is_partial_differentiable_in x,i implies r(#)f
is_partial_differentiable_in x,i & partdiff((r(#)f),x,i) = r*partdiff(f,x,i)
proof
assume f is_partial_differentiable_in x,i;
then
A1: f*reproj(i,x) is_differentiable_in Proj(i,m).x;
r(#)(f*reproj(i,x)) = (r(#)f)*reproj(i,x) by Th27;
then (r(#)f)*reproj(i,x) is_differentiable_in Proj(i,m).x by A1,NDIFF_1:37;
hence r(#)f is_partial_differentiable_in x,i;
diff(r(#)(f*reproj(i,x)),Proj(i,m).x) = partdiff(r(#)f,x,i) by Th27;
hence thesis by A1,NDIFF_1:37;
end;
theorem
g is_partial_differentiable_in y,i implies r(#)g
is_partial_differentiable_in y,i & partdiff(r(#)g,y,i) = r*partdiff(g,y,i)
proof
A1: the carrier of REAL-NS n = REAL n by REAL_NS1:def 4;
A2: rng g c= dom(W) by Th2;
then
A3: dom(W*g) = dom g by RELAT_1:27;
reconsider d = partdiff(g,y,i) as Element of REAL by XREAL_0:def 1;
reconsider Pd = <*d*> as Element of REAL 1 by FINSEQ_2:98;
reconsider x=y as Point of REAL-NS n by REAL_NS1:def 4;
A4: the carrier of REAL-NS 1 = REAL 1 by REAL_NS1:def 4;
then reconsider f=<>*g as PartFunc of REAL-NS n,REAL-NS 1 by REAL_NS1:def 4;
reconsider One = <*jj*> as VECTOR of REAL-NS 1 by A4,FINSEQ_2:98;
assume g is_partial_differentiable_in y,i;
then
A5: f is_partial_differentiable_in x,i by Th14;
then
A6: r(#)f is_partial_differentiable_in x,i by Th32;
dom(r(#)f) = dom(W*g) by VFUNCT_1:def 4;
then dom(r(#)f) = dom g by A2,RELAT_1:27;
then
A7: dom(r(#)f) = dom(r(#)g) by VALUED_1:def 5;
A8: rng(r(#)g) c= dom(W) by Th2;
then
A9: dom(W*(r(#)g)) = dom(r(#)g) by RELAT_1:27;
A10: now
let x be Element of REAL-NS n;
consider I be Function of REAL,REAL 1 such that
I is bijective and
A11: W = I by Th2;
assume
A12: x in dom(r(#)f);
then
A13: (<>*(r(#)g)).x = W.((r(#)g).x) by A7,A9,FUNCT_1:12;
(r(#)f).x = (r(#)f)/.x by A12,PARTFUN1:def 6;
then
A14: (r(#)f).x = r * (f/.x) by A12,VFUNCT_1:def 4;
A15: x in dom g by A3,A12,VFUNCT_1:def 4;
then
A16: x in dom(r(#)g) by VALUED_1:def 5;
x in dom f by A12,VFUNCT_1:def 4;
then f/.x = (W*g).x by PARTFUN1:def 6;
then f/.x = W.(g.x) by A15,FUNCT_1:13;
then r*(f/.x) = I.(r*(g.x)) by A11,Th3;
hence (r(#)f).x = (<>*(r(#)g)).x by A16,A14,A13,A11,VALUED_1:def 5;
end;
A17: partdiff(f,x,i).One = <*partdiff(g,y,i)*> by A5,Th15;
dom(r(#)f) = dom <>*(r(#)g) by A7,A8,RELAT_1:27;
then
A18: r(#)f=<>*(r(#)g) by A1,A4,A10,PARTFUN1:5;
then <*partdiff(r(#)g,y,i)*> = partdiff(r(#)f,x,i).<*1*> by A5,Th15,Th32
.= (r*partdiff(f,x,i)).<*1*> by A5,Th32
.= r*(partdiff(f,x,i).One) by LOPBAN_1:36
.= r*Pd by A17,REAL_NS1:3
.= <*r*partdiff(g,y,i)*> by RVSUM_1:47;
then partdiff(r(#)g,y,i) = <*r*partdiff(g,y,i)*>.1;
hence thesis by A18,A6,Th14;
end;