0 ex d be Real st d > 0 & for z be Real st
z <> 0 & |. z .| < d holds ( |. z .|"* ||. R/.z .||) < r by A7,A17,A19;
end;
now
assume
A21: for r be Real st r > 0 ex d be Real st d > 0 & for z be Real
st z <> 0 & |. z .| < d holds ( |. z .|"* ||. R/.z .||) < r;
now
let s be convergent_to_0 Real_Sequence;
A22: s is non-zero by FDIFF_1:def 1;
A23: s is convergent & lim s = 0 by FDIFF_1:def 1;
A24: now
let r be Real;
assume r > 0;
then consider d be Real such that
A25: d > 0 and
A26: for z be Real st z <> 0 & |. z .| < d holds ( |. z .|
"* ||. R/.z .||) < r by A21;
consider n0 be Element of NAT such that
A27: for m be Element of NAT st n0 <=m holds |. s.m-0 .| < d by A23,A25,
SEQ_2:def 7;
take n0;
thus for m be Element of NAT st n0 <=m holds ||. ((s")(#)(R/*s)).
m- 0.(REAL-NS n).|| < r
proof
dom R = REAL by A1,PARTFUN1:def 2;
then
A28: rng s c= dom R;
let m be Element of NAT;
assume n0 <=m;
then
B29: |. s.m-0 .| < d by A27;
A30: s.m <> 0 by A22,SEQ_1:5;
|. s.m .|" * ||.(R/.(s.m)).|| =abs((s.m)") * ||.(R/.(s.m)).||
by COMPLEX1:66
.= ||.(s.m)"*(R/.(s.m)).|| by NORMSP_1:def 1
.= ||.(s.m)"*((R/*s).m).|| by A28,FUNCT_2:109
.= ||.(s".m)*((R/*s).m).|| by VALUED_1:10
.= ||. ((s")(#)(R/*s)).m .|| by NDIFF_1:def 2
.= ||. ((s")(#)(R/*s)).m- 0.(REAL-NS n).|| by RLVECT_1:13;
hence thesis by A26,B29,A30;
end;
end;
hence
(s")(#)(R/*s) is convergent by NORMSP_1:def 6;
hence lim ((s")(#)(R/*s)) = 0.(REAL-NS n) by A24,NORMSP_1:def 7;
end;
hence R is REST-like by A1,NDIFF_3:def 1;
end;
hence thesis by A2;
end;
theorem DPREP120:
for g be PartFunc of REAL,REAL-NS n,
x0 be real number st
1 <= i & i <= n & g is_differentiable_in x0 holds
(Proj(i,n)*g) is_differentiable_in x0 &
Proj(i,n).(diff(g,x0)) = diff((Proj(i,n)*g),x0)
proof
let g be PartFunc of REAL,REAL-NS n, x0 be real number;
assume AS0: 1 <= i & i <= n & g is_differentiable_in x0; then
consider N being Neighbourhood of x0 such that
AS1:N c= dom g & ex DFG,GR st diff(g,x0) = DFG.1 &
for x be Real st x in N holds
g/.x - g/.x0 = DFG.(x-x0) + GR/.(x-x0) by NDIFF_3:def 4;
consider GR, DFG such that
AS2:diff(g,x0) = DFG.1 &
for x be Element of REAL st x in N holds
g/.x - g/.x0 = DFG.(x-x0) + GR/.(x-x0) by AS1;
consider LP be Point of REAL-NS n such that
Y11: for p be Real holds DFG.p = p*LP by NDIFF_3:def 2;
reconsider PG = Proj(i,n) as Function of REAL-NS n,REAL-NS 1;
reconsider L = Proj(i,n)*DFG as Function of REAL,REAL-NS 1;
AD1: for r being Real holds L.r = r*(Proj(i,n).LP)
proof
let r being Real;
P2: dom L = REAL by FUNCT_2:def 1;
DFG.r = r*LP by Y11; then
Proj(i,n).(DFG.r) = r*(Proj(i,n).LP) by PDIFF_6:27;
hence
L.r = r*(Proj(i,n).LP) by P2,FUNCT_1:12;
end; then
reconsider L as LINEAR of REAL-NS 1 by NDIFF_3:def 2;
A01: GR is total by NDIFF_3:def 1; then
reconsider FGR = GR as Function of REAL, REAL-NS n;
A3:Proj(i,n)*FGR is Function of REAL,REAL-NS 1;
Proj(i,n)*GR is REST of REAL-NS 1
proof
B21:dom GR = REAL by A01,PARTFUN1:def 2;
reconsider R = Proj(i,n)*GR as PartFunc of REAL,REAL-NS 1;
for r be Real st r > 0 ex d be Real st d > 0 &
(for z be Real st z <> 0 & |.z.| < d
holds (|.z.|" * ||. R/.z .||) < r)
proof
let r be Real;
assume r > 0; then
consider d be Real such that
B5: d > 0 &
(for z be Real st z <> 0 & |.z.| < d holds
(|.z.|"* ||. GR/.z .||) < r) by A01,NDIFF126;
take d;
thus d> 0 by B5;
let z be Element of REAL;
assume B6: z <> 0 & |.z.| < d;
Q12: GR/.z = GR.z by B21,PARTFUN1:def 6;
Q121:i in Seg n by AS0;
reconsider GRz = GR/.z as Point of REAL-NS n;
reconsider GRz1 = GRz as Element of REAL n by REAL_NS1:def 4;
reconsider GRzi = GRz1.i as Element of REAL;
dom Proj(i,n) = the carrier of REAL-NS n by PARTFUN1:def 2; then
Q123:z in dom (Proj(i,n)*GR) by B21,Q12,FUNCT_1:11; then
(Proj(i,n)*GR).z = Proj(i,n).(GR.z) by FUNCT_1:12
.= <* proj(i,n).(GRz1) *> by Q12,PDIFF_1:def 4; then
Q13: (Proj(i,n)*GR).z = <* GRzi *> by PDIFF_1:def 1;
Q15: abs GRzi <= ||. GR/.z .|| by Q121,REAL_NS1:9;
Q151:0 <= |.z.| by COMPLEX1:46;
0 <= abs GRzi by COMPLEX1:46; then
Q16: |.z.|"* abs GRzi <= |.z.|"* ||. GR/.z .|| by Q15,Q151,XREAL_1:66;
|.z.|"* ||. GR/.z .|| < r by B5,B6; then
B71: |.z.|"* abs GRzi < r by Q16,XXREAL_0:2;
(Proj(i,n)*GR).z in rng(Proj(i,n)*GR) by Q123,FUNCT_1:3; then
reconsider Rz = (Proj(i,n)*GR).z as VECTOR of REAL-NS 1;
set VGRzi = <* GRzi *>;
VGRzi is Element of REAL 1 by FINSEQ_2:98; then
||. Rz .|| = |. VGRzi .| by Q13,REAL_NS1:1; then
|.z.|"* ||. Rz .|| < r by B71,JORDAN2C:10;
hence thesis by Q123,PARTFUN1:def 6;
end;
hence thesis by A3,NDIFF126;
end; then
reconsider R = Proj(i,n)*GR as REST of REAL-NS 1;
set pg = Proj(i,n)*g;
E1:dom Proj(i,n) = the carrier of REAL-NS n by FUNCT_2:def 1; then
rng g c= dom Proj(i,n); then
E3:dom g = dom (Proj(i,n)*g) by RELAT_1:27;
E4:dom Proj(i,n) = REAL n by E1,REAL_NS1:def 4;
A5:for x be Real st x in N holds
pg/.x - pg/.x0 = L.(x-x0) + R/.(x-x0)
proof
let x be Real;
now assume C1: x in N; then
C2: g/.x - g/.x0 = DFG.(x-x0) + GR/.(x-x0) by AS2;
C3: x0 in N by RCOMP_1:16; then
C31: pg/.x = pg.x & pg/.x0 = pg.x0 by AS1,E3,C1,PARTFUN1:def 6;
C33: g/.x = g.x & g/.x0 = g.x0 by AS1,C1,C3,PARTFUN1:def 6;
reconsider PGSx = pg/.x - pg/.x0 as Element of REAL 1 by REAL_NS1:def 4;
pg.x in rng pg by AS1,E3,C1,FUNCT_1:3; then
reconsider PGdx = pg.x as Element of REAL 1 by REAL_NS1:def 4;
pg.x0 in rng pg by AS1,E3,C3,FUNCT_1:3; then
reconsider PGdx0 = pg.x0 as Element of REAL 1 by REAL_NS1:def 4;
g.x in rng g by AS1,C1,FUNCT_1:3; then
reconsider Gx = g.x as Element of REAL n by REAL_NS1:def 4;
g.x0 in rng g by AS1,C3,FUNCT_1:3; then
reconsider Gx0 = g.x0 as Element of REAL n by REAL_NS1:def 4;
set ProjGx = Proj(i,n).(g.x);
Gx in dom Proj(i,n) by E4; then
ProjGx in rng Proj(i,n) by FUNCT_1:3; then
reconsider ProjGx as Element of REAL 1 by REAL_NS1:def 4;
set ProjGx0 = Proj(i,n).(g.x0);
Gx0 in dom Proj(i,n) by E4; then
ProjGx0 in rng Proj(i,n) by FUNCT_1:3; then
reconsider ProjGx0 as Element of REAL 1 by REAL_NS1:def 4;
reconsider Gx1 = Gx as Element of REAL-NS n by REAL_NS1:def 4;
reconsider Gx01 = Gx0 as Element of REAL-NS n by REAL_NS1:def 4;
reconsider Gsx = g/.x as Element of REAL n by REAL_NS1:def 4;
reconsider Gsx0 = g/.x0 as Element of REAL n by REAL_NS1:def 4;
set dxx0 = x-x0;
reconsider Ldxx0 = L.(x-x0) as Element of REAL-NS 1;
F4: dom R = REAL by A3,PARTFUN1:def 2; then
F5: R/.(x-x0) = R.dxx0 by PARTFUN1:def 6; then
reconsider Rdxx0 = R.(x-x0) as Element of REAL-NS 1;
reconsider Lxx0Rxx0 = L.(x-x0) + R/.(x-x0) as Element of REAL 1
by REAL_NS1:def 4;
reconsider Ldiff = DFG.(x-x0) as Element of REAL n by REAL_NS1:def 4;
set ProjLdiff = Proj(i,n).Ldiff;
ProjLdiff in rng Proj(i,n) by E1,FUNCT_1:3; then
reconsider ProjLdiff as Element of REAL 1 by REAL_NS1:def 4;
F6: dom GR = REAL by A01,PARTFUN1:def 2; then
GR.dxx0 in rng GR by FUNCT_1:3; then
reconsider Rdiff = GR.dxx0 as Element of REAL n by REAL_NS1:def 4;
F82: Rdiff = GR/.dxx0 by F6,PARTFUN1:def 6;
set ProjRdiff = Proj(i,n).Rdiff;
ProjRdiff in rng Proj(i,n) by E4,FUNCT_1:3; then
reconsider ProjRdiff as Element of REAL 1 by REAL_NS1:def 4;
dom L = REAL by FUNCT_2:def 1; then
L.(x-x0) = Proj(i,n).Ldiff & R.(x-x0) = Proj(i,n).Rdiff
by F4,FUNCT_1:12; then
Lm1: Ldxx0 + Rdxx0 = ProjLdiff + ProjRdiff by REAL_NS1:2;
Proj(i,n).Ldiff = <* proj(i,n).Ldiff *> by PDIFF_1:def 4; then
Lm2: Proj(i,n).Ldiff = <* Ldiff.i *> by PDIFF_1:def 1;
Rdiff in dom Proj(i,n) by E4; then
Proj(i,n).Rdiff = <* proj(i,n).Rdiff *> by PDIFF_1:def 4; then
Lm3: Proj(i,n).Rdiff = <* Rdiff.i *> by PDIFF_1:def 1;
reconsider diffGR = DFG.(x-x0) + GR/.(x-x0)
as Element of REAL n by REAL_NS1:def 4;
reconsider Rsdiff = GR/.(x-x0) as Element of REAL n by REAL_NS1:def 4;
PGSx = PGdx - PGdx0 by C31,REAL_NS1:5
.= ProjGx - PGdx0 by AS1,E3,C1,FUNCT_1:12
.= ProjGx - ProjGx0 by AS1,E3,C3,FUNCT_1:12
.= <* proj(i,n).Gx1 *> - ProjGx0 by PDIFF_1:def 4
.= <* proj(i,n).Gx1 *> - <* proj(i,n).Gx01 *> by PDIFF_1:def 4
.= <* Gx.i *> - <* proj(i,n).Gx01 *> by PDIFF_1:def 1
.= <* Gx.i *> - <* Gx0.i *> by PDIFF_1:def 1
.= <* Gx.i - Gx0.i *> by RVSUM_1:29
.= <* (Gsx - Gsx0).i *> by C33,RVSUM_1:27
.= <* diffGR.i *> by C2,REAL_NS1:5
.= <* (Ldiff + Rsdiff).i *> by REAL_NS1:2
.= <* Ldiff.i + Rsdiff.i *> by RVSUM_1:11;
hence thesis by F5,Lm1,Lm2,Lm3,F82,RVSUM_1:13;
end;
hence thesis;
end;
hence X1:Proj(i,n)*g is_differentiable_in x0 by AS1,E3,NDIFF_3:def 3;
L.1 =1*(Proj(i,n).LP) by AD1
.= Proj(i,n).(LP) by RLVECT_1:def 8
.= Proj(i,n).(1*LP) by RLVECT_1:def 8
.= Proj(i,n).diff(g,x0) by AS2,Y11;
hence thesis by X1,AS1,E3,A5,NDIFF_3:def 4;
end;
theorem DPREP121:
for g be PartFunc of REAL,REAL-NS n,
x0 be real number holds
g is_differentiable_in x0 iff
(for i be Element of NAT st 1<=i & i <=n holds
Proj(i,n)*g is_differentiable_in x0)
proof
let g be PartFunc of REAL,REAL-NS n;
let x0 be real number;
thus g is_differentiable_in x0 implies
for i be Element of NAT st 1<=i & i <=n holds
Proj(i,n)*g is_differentiable_in x0 by DPREP120;
assume AS: for i be Element of NAT st 1 <= i & i <= n holds
Proj(i,n)*g is_differentiable_in x0;
defpred Pd[Element of NAT,Element of REAL] means
$2 > 0 &
]. x0-$2,x0+$2.[ c= dom (Proj($1,n)*g) &
ex Ri be REST of REAL-NS 1 st
for x be Real st x in ]. x0-$2,x0+$2.[ holds
(Proj($1,n)*g)/.x - (Proj($1,n)*g)/.x0
= (x-x0)*(diff((Proj($1,n)*g),x0)) + Ri/.(x-x0);
A1: for k be Element of NAT st k in Seg n ex dk be Element of REAL st Pd[k,dk]
proof
let k be Element of NAT;
assume k in Seg n; then
1 <= k & k <= n by FINSEQ_1:1; then
Proj(k,n)*g is_differentiable_in x0 by AS; then
consider Nk be Neighbourhood of x0 such that
B1: Nk c= dom (Proj(k,n)*g) & ex L be LINEAR of REAL-NS 1,
Rk be REST of REAL-NS 1 st L.1 = (diff((Proj(k,n)*g),x0)) &
for x be Real st
x in Nk holds (Proj(k,n)*g)/.x - (Proj(k,n)*g)/.x0
= L.(x-x0) + Rk/.(x-x0) by NDIFF_3:def 4;
consider dk be real number such that
B2: 0 < dk & Nk = ]. x0-dk,x0+dk.[ by RCOMP_1:def 6;
reconsider dk as Element of REAL by XREAL_0:def 1;
take dk;
thus 0 < dk by B2;
thus ]. x0-dk,x0+dk.[ c= dom(Proj(k,n)*g) by B2,B1;
thus ex Rk be REST of REAL-NS 1 st
for x be Real st x in ]. x0-dk,x0+dk.[ holds
(Proj(k,n)*g)/.x - (Proj(k,n)*g)/.x0
= (x-x0)*(diff((Proj(k,n)*g),x0))+Rk/.(x-x0)
proof
consider L be LINEAR of REAL-NS 1, Rk be REST of REAL-NS 1 such that
B30: L.1 = (diff((Proj(k,n)*g),x0)) &
for x be Real st x in Nk holds (Proj(k,n)*g)/.x - (Proj(k,n)*g)/.x0
= L.(x-x0) + Rk/.(x-x0) by B1;
B3: now let x be Real;
assume B31: x in Nk;
consider L1 be Point of REAL-NS 1 such that
B33: for p be Real holds L.p = p*L1 by NDIFF_3:def 2;
B34: (diff((Proj(k,n)*g),x0)) = 1*L1 by B33,B30
.= L1 by RLVECT_1:def 8;
B32: L.(x-x0) =(x-x0)*(diff((Proj(k,n)*g),x0)) by B34,B33;
thus (Proj(k,n)*g)/.x - (Proj(k,n)*g)/.x0
=(x-x0)*(diff((Proj(k,n)*g),x0))+Rk/.(x-x0) by B32,B30,B31;
end;
take Rk;
thus for x be Real st
x in ]. x0-dk,x0+dk.[ holds
(Proj(k,n)*g)/.x - (Proj(k,n)*g)/.x0
= (x-x0)*(diff((Proj(k,n)*g),x0))+Rk/.(x-x0) by B2,B3;
end;
end;
consider d be FinSequence of REAL such that
A2: dom d = Seg n & for k be Element of NAT st k in Seg n holds
Pd[k,d/.k] from RECDEF_1:sch 17(A1);
set d0 = min d;
len d = n by A2,FINSEQ_1:def 3; then
AP1:min_p d in dom d by RFINSEQ2:def 2; then
d/.(min_p d) > 0 by A2; then
AP2:d0 > 0 by AP1,PARTFUN1:def 6;
defpred LX[Real,set] means
ex y be Element of REAL n st $2 = y &
for i be Element of NAT st i in Seg n holds
y.i = proj(1,1).($1*(diff((Proj(i,n)*g),x0)));
A3: for x be Real holds ex y be Point of REAL-NS n st LX[x,y]
proof
let x being Real;
defpred YX[Element of NAT,set] means
$2 = proj(1,1).(x*(diff((Proj($1,n)*g),x0)));
P71: for i be Element of NAT st i in Seg n
ex r being Element of REAL st YX[i,r];
consider y be FinSequence of REAL such that
P73: dom y = Seg n & for i be Element of NAT st i in Seg n holds YX[i,y/.i]
from RECDEF_1:sch 17(P71);
len y = n by P73,FINSEQ_1:def 3; then
reconsider y as Element of REAL n by FINSEQ_2:92;
P77: now let i be Element of NAT;
assume i in Seg n; then
YX[i,y/.i] & y/.i = y.i by P73,PARTFUN1:def 6;
hence y.i =proj(1,1).(x*(diff((Proj(i,n)*g),x0)));
end;
reconsider y0=y as Point of REAL-NS n by REAL_NS1:def 4;
ex y be Element of REAL n st y0=y &
for i be Element of NAT st i in Seg n holds
y.i = proj(1,1).(x*(diff((Proj(i,n)*g),x0))) by P77;
hence ex y0 be Point of REAL-NS n st LX[x,y0];
end;
consider L be Function of REAL,REAL-NS n such that
A4: for x be Real holds LX[x,L.x] from FUNCT_2:sch 3(A3);
for r be Real holds L.r = r*(L.1)
proof
let r be Real;
consider Lx be Element of REAL n such that
B01: L.1 = Lx & for i be Element of NAT st i in Seg n holds
Lx.i = proj(1,1).(1*(diff((Proj(i,n)*g),x0))) by A4;
B1:now let i be Element of NAT;
assume i in Seg n;
then Lx.i = proj(1,1).(1*(diff((Proj(i,n)*g),x0))) by B01;
hence Lx.i = proj(1,1).(diff((Proj(i,n)*g),x0)) by RLVECT_1:def 8;
end;
consider Lrx be Element of REAL n such that
B2: L.r = Lrx & for i be Element of NAT st i in Seg n holds
Lrx.i = proj(1,1).(r*(diff((Proj(i,n)*g),x0))) by A4;
XX: dom (r*Lx) = Seg n by FINSEQ_2:124; then
B3: dom (r*Lx) = dom Lrx by FINSEQ_2:124;
for i0 be Nat st i0 in dom (r*Lx) holds (r*Lx).i0 = Lrx.i0
proof
let i0 be Nat;
reconsider i = i0 as Element of NAT by ORDINAL1:def 12;
assume i0 in dom(r*Lx); then
B7: Lx.i = proj(1,1).((diff((Proj(i,n)*g),x0))) &
Lrx.i = proj(1,1).(r*(diff((Proj(i,n)*g),x0))) by B1,B2,XX;
B5: (r*1) * diff((Proj(i,n)*g),x0) = r * (1*diff((Proj(i,n)*g),x0))
by RLVECT_1:def 8;
reconsider Diffrx = (r*1)*diff((Proj(i,n)*g),x0)
as Element of REAL 1 by REAL_NS1:def 4;
reconsider Diffx = 1*diff((Proj(i,n)*g),x0)
as Element of REAL 1 by REAL_NS1:def 4;
B51: Diffx = diff((Proj(i,n)*g),x0) by RLVECT_1:def 8;
Diffrx = r*Diffx by B5,REAL_NS1:3; then
Lrx.i0 = (r*Diffx).1 by B7,PDIFF_1:def 1; then
Lrx.i0 = r*(Diffx.1) by RVSUM_1:45;
then
Lrx.i0 = r*(Lx.i0) by B7,B51,PDIFF_1:def 1;
hence thesis by RVSUM_1:45;
end; then
r*Lx = Lrx by B3,FINSEQ_1:13;
hence thesis by B01,B2,REAL_NS1:3;
end; then
reconsider L as linear Function of REAL,REAL-NS n
by NDIFF_3:def 2;
reconsider L0 = L as LINEAR of REAL-NS n;
deffunc RD(Element of REAL) = g/.($1+x0) - g/.x0 - L.$1;
consider R be Function of REAL,REAL-NS n such that
A9: for x be Element of REAL holds R.x = RD(x) from FUNCT_2:sch 4;
A10:for x be Element of REAL, i be Element of NAT st
i in Seg n & x+x0 in dom g holds
(Proj(i,n)*R).x
= (Proj(i,n)*g)/.(x+x0) - (Proj(i,n)*g)/.x0 - (Proj(i,n)*L).x
proof
let x be Element of REAL, i be Element of NAT;
assume that
BS1: i in Seg n and
BS2: x+x0 in dom g;
P1: |. x0 - x0 .| = 0 by COMPLEX1:44;
P2: 0 < d/.i & ]. x0-d/.i,x0+d/.i.[ c= dom (Proj(i,n)*g) by BS1,A2; then
x0 in ]. x0-d/.i,x0+d/.i.[ by P1,RCOMP_1:1; then
P3: x0 in dom (Proj(i,n)*g) by P2;
P4: dom (Proj(i,n)*g) c= dom g by RELAT_1:25;
reconsider gxx0 = g/.(x+x0), gx0 = g/.x0, Lx = L.x as Element of REAL n
by REAL_NS1:def 4;
reconsider gxx01 = g/.(x+x0), gx01 = g/.x0, Lx1 = L.x
as Point of REAL-NS n;
B0: -gx0 = (-1)*(g/.x0) & -Lx = (-1)*(L.x) by REAL_NS1:3; then
gxx0 + -gx0 = g/.(x+x0) + (-1)*(g/.x0) by REAL_NS1:2; then
B2: gxx0 + -gx0 + -Lx = g/.(x+x0) + (-1)*(g/.x0) + (-1)*(L.x)
by B0,REAL_NS1:2;
N1: -1 is Real by XREAL_0:def 1;
gxx0-gx0 = g/.(x+x0)-g/.x0 by REAL_NS1:5; then
B1: g/.(x+x0) - g/.x0 - L.x = gxx0 - gx0 - Lx by REAL_NS1:5;
(Proj(i,n)*R).x = Proj(i,n).(R.x) by FUNCT_2:15; then
(Proj(i,n)*R).x = Proj(i,n).(g/.(x+x0) - g/.x0 - L.x) by A9; then
(Proj(i,n)*R).x = Proj(i,n).(g/.(x+x0) + (-1)*(g/.x0))
+ Proj(i,n).((-1)*(L.x)) by B1,B2,PDIFF_6:26; then
B3: (Proj(i,n)*R).x = Proj(i,n).(g/.(x+x0)) + Proj(i,n).((-1)*(g/.x0))
+ Proj(i,n).((-1)*(L.x)) by PDIFF_6:26;
Proj(i,n).((-1)*(g/.x0)) = (-1)*(Proj(i,n).(g/.x0)) &
Proj(i,n).((-1)*(Lx1)) = (-1)*(Proj(i,n).(Lx1)) by N1,PDIFF_6:27;
then
(Proj(i,n)*R).x = Proj(i,n).(g/.(x+x0)) + -Proj(i,n).(g/.x0)
+ (-1)*Proj(i,n).(L.x) by B3,RLVECT_1:16; then
C0: (Proj(i,n)*R).x = Proj(i,n).(g/.(x+x0)) - Proj(i,n).(g/.x0)
- Proj(i,n).(L.x) by RLVECT_1:16;
g/.(x+x0) in the carrier of REAL-NS n &
g/.x0 in the carrier of REAL-NS n; then
C1: g/.(x+x0) in dom (Proj(i,n)) & g/.x0 in dom (Proj(i,n)) by FUNCT_2:def 1;
C2: Proj(i,n).(g/.(x+x0)) = Proj(i,n)/.(g/.(x+x0))
.= (Proj(i,n)*g)/.(x+x0) by BS2,C1,PARTFUN2:4;
Proj(i,n).(g/.x0) = Proj(i,n)/.(g/.x0)
.= (Proj(i,n)*g)/.x0 by P3,P4,C1,PARTFUN2:4;
hence thesis by C0,C2,FUNCT_2:15;
end;
for r be Real st r > 0 ex d be Real st d > 0 &
for z be Real st
z <> 0 & |. z .| < d holds (|.z.|"* ||. R/.z .||) < r
proof
let r be Real;
assume B1: r > 0;
set r0 = (sqrt n)"*r;
DD0: sqrt n > 0 by SQUARE_1:25; then
DE0: r0 > 0 by B1,XREAL_1:129;
defpred DD[Element of NAT,Element of REAL] means $2 > 0 &
for z be Real st z <> 0 & |. z .| < $2 holds
|. z .|"* ||. (Proj($1,n)*R)/.z .|| < r0;
DD1: for k be Element of NAT st k in Seg n ex dd be Element of REAL st DD[k,dd]
proof
let k be Element of NAT;
assume D0: k in Seg n; then
1 <= k & k <= n by FINSEQ_1:1; then
Proj(k,n)*g is_differentiable_in x0 by AS; then
consider Nk be Neighbourhood of x0 such that
D1: Nk c= dom (Proj(k,n)*g) & ex LR be LINEAR of REAL-NS 1,
PR be REST of REAL-NS 1 st LR.1 = diff(Proj(k,n)*g,x0) &
for x be Real st x in Nk holds
(Proj(k,n)*g)/.x - (Proj(k,n)*g)/.x0
= LR.(x-x0) + PR/.(x-x0) by NDIFF_3:def 4;
consider d0 be real number such that
D2:0 < d0 & Nk = ]. x0-d0,x0+d0.[ by RCOMP_1:def 6;
reconsider d0 as Real by XREAL_0:def 1;
consider LR be LINEAR of REAL-NS 1,
PR be REST of REAL-NS 1 such that
D3: LR.1 = diff(Proj(k,n)*g,x0) &
for x be Real st x in Nk holds
(Proj(k,n)*g)/.x - (Proj(k,n)*g)/.x0 =LR.(x-x0) + PR/.(x-x0) by D1;
D30: now let x be Real;
assume E31: x in Nk;
consider L1 be Point of REAL-NS 1 such that
B33: for p be Real holds LR.p = p*L1 by NDIFF_3:def 2;
(diff((Proj(k,n)*g),x0)) = 1*L1 by B33,D3
.=L1 by RLVECT_1:def 8;
then LR.(x-x0) =(x-x0)*(diff((Proj(k,n)*g),x0)) by B33;
hence (Proj(k,n)*g)/.x - (Proj(k,n)*g)/.x0
=(x-x0)*diff(Proj(k,n)*g,x0) + PR/.(x-x0) by E31,D3;
end;
PR is total by NDIFF_3:def 1; then
consider d1 be Real such that
D4: d1 > 0 & for z be Real st z <> 0 & |. z .| < d1 holds
|. z .|"* ||. PR/.z .|| < r0 by DE0,NDIFF126;
set dd = min(d0,d1);
take dd;
for z be Real st z <> 0 & |. z .| < dd holds
(|. z .|"* ||. (Proj(k,n)*R)/.z .||) < r0
proof
let z be Real;
assume D6: z <> 0 & |. z .| < dd;
dd <= d1 by XXREAL_0:17; then
|. z .| < d1 by D6,XXREAL_0:2; then
D7: ( |. z .|"* ||. PR/.z .||) < r0 by D6,D4;
dd <= d0 by XXREAL_0:17; then
D8: |. z .| < d0 by D6,XXREAL_0:2;
z+x0 - x0 = z; then
E0: z+x0 in ]. x0-d0,x0+d0.[ by D8,RCOMP_1:1; then
E2: z+x0 in dom (Proj(k,n)*g) by D1,D2;
(Proj(k,n)*g)/.(z+x0) - (Proj(k,n)*g)/.x0
= (z+x0-x0)*diff(Proj(k,n)*g,x0) + PR/.(z+x0-x0) by E0,D2,D30;
then
D10: PR/.z = (Proj(k,n)*g)/.(z+x0) - (Proj(k,n)*g)/.x0
- z*diff(Proj(k,n)*g,x0) by RLVECT_4:1;
dom(Proj(k,n)*g) c= dom g by RELAT_1:25; then
E3: (Proj(k,n)*R).z
= (Proj(k,n)*g)/.(z+x0) - (Proj(k,n)*g)/.x0 - (Proj(k,n)*L).z
by E2,D0,A10;
consider y be Element of REAL n such that
D11: L.z = y & for i be Element of NAT st i in Seg n holds
y.i = proj(1,1).(z*(diff((Proj(i,n)*g),x0))) by A4;
D12: y.k = proj(1,1).(z*(diff((Proj(k,n)*g),x0))) by D11,D0;
z*(diff((Proj(k,n)*g),x0)) is Element of REAL 1 by REAL_NS1:def 4; then
consider Dk be Element of REAL such that
D13: z*(diff((Proj(k,n)*g),x0)) = <* Dk *> by FINSEQ_2:97;
reconsider y1 = y as Point of REAL-NS n by REAL_NS1:def 4;
dom L = REAL by FUNCT_2:def 1; then
(Proj(k,n)*L).z = (Proj(k,n)).(L.z) by FUNCT_1:13; then
(Proj(k,n)*L).z = <* proj(k,n).y1 *> by D11,PDIFF_1:def 4; then
(Proj(k,n)*L).z = <* proj(1,1).(z*(diff((Proj(k,n)*g),x0))) *>
by D12,PDIFF_1:def 1;
hence thesis by D7,D10,E3,D13,PDIFF_1:1;
end;
hence thesis by D2,D4,XXREAL_0:21;
end;
consider dd be FinSequence of REAL such that
DD2: dom dd = Seg n & for i be Element of NAT st i in Seg n holds DD[i,dd/.i]
from RECDEF_1:sch 17(DD1);
take d = min dd;
len dd = n by DD2,FINSEQ_1:def 3; then
PP1: min_p dd in dom dd by RFINSEQ2:def 2; then
DD3: dd/.(min_p dd) > 0 by DD2;
for z be Real st
z <> 0 & |. z .| < d holds (|.z.|"* ||. R/.z .||) < r
proof
let z be Real;
assume G0: z <> 0 & |. z .| < d;
reconsider Rz = R/.z as Element of REAL n by REAL_NS1:def 4;
reconsider R0 = (n |-> (|. z .| * r0)^2) as Element of n-tuples_on REAL;
reconsider SRz = sqr Rz as Element of n-tuples_on REAL;
GG4: |. z .| > 0 by G0,COMPLEX1:47;
DD4: for i0 be Nat st i0 in Seg n holds SRz.i0 < R0.i0
proof
let i0 be Nat;
reconsider i = i0 as Element of NAT by ORDINAL1:def 12;
assume G1: i0 in Seg n; then
i in dom Rz by FINSEQ_2:124; then
(sqr Rz).i = sqrreal.(Rz.i) by FUNCT_1:13; then
G3: (sqr Rz).i = (Rz.i)^2 by RVSUM_1:def 2;
1 <= i & i <= n by G1,FINSEQ_1:1; then
1 <= i & i <= len dd by DD2,FINSEQ_1:def 3; then
d <= dd.i by RFINSEQ2:2; then
d <= dd/.i by G1,DD2,PARTFUN1:def 6; then
|. z .| < dd/.i by G0,XXREAL_0:2; then
(|. z .|" * ||. (Proj(i,n)*R)/.z .||) < r0 by G0,G1,DD2; then
G5: ||. (Proj(i,n)*R)/.z .|| < r0 / (|. z .|") by GG4,XREAL_1:81;
reconsider Rzi = <* Rz.i *> as Element of REAL 1 by FINSEQ_2:98;
(Proj(i,n)*R).z = Proj(i,n).(R.z) by FUNCT_2:15; then
(Proj(i,n)*R).z = <* proj(i,n).Rz *> by PDIFF_1:def 4; then
(Proj(i,n)*R).z = <* Rz.i *> by PDIFF_1:def 1; then
||. (Proj(i,n)*R).z .|| = |. Rzi .| by REAL_NS1:1; then
|. Rz.i .| < |. z .| * r0 by G5,JORDAN2C:10; then
|. Rz.i .| ^2 < (|. z .| * r0)^2 by COMPLEX1:46,SQUARE_1:16; then
(Rz.i0)^2 < (|. z .| * r0)^2 by COMPLEX1:75;
hence thesis by G1,G3,FINSEQ_2:57;
end;
DD8: for i be Nat st i in dom (sqr Rz) holds 0 <= (sqr Rz).i
proof
let i be Nat;
assume i in dom(sqr Rz); then
i in dom (sqrreal*Rz) & dom(sqrreal*Rz) c= dom Rz by RELAT_1:25; then
(sqr Rz).i = sqrreal.(Rz.i) by FUNCT_1:13; then
(sqr Rz).i = (Rz.i)^2 by RVSUM_1:def 2;
hence thesis by XREAL_1:63;
end;
DD9: (|. z .| * r0)^2 >= 0 by XREAL_1:63;
DD5: ex i be Nat st i in Seg n & SRz.i < R0.i
proof
take 1;
1 <= n by NAT_1:14;
hence 1 in Seg n;
hence thesis by DD4;
end;
LP1: sqrt n > 0 by SQUARE_1:25;
for i0 be Nat st i0 in Seg n holds SRz.i0 <= R0.i0 by DD4; then
Sum SRz < Sum R0 by DD5,RVSUM_1:83; then
Sum (sqr Rz) < n * (|. z .| * r0)^2 by RVSUM_1:80; then
|. Rz .| < sqrt (n * (|. z .| * r0)^2)
by DD8,RVSUM_1:84,SQUARE_1:27; then
|. Rz .| < sqrt n * sqrt (|. z .| * r0)^2 by DD9,SQUARE_1:29; then
|. Rz .| < sqrt n * |. |. z .| * r0 .| by COMPLEX1:72; then
|. Rz .| < sqrt n * (|. z .| * r0) by DD0,B1,GG4,ABSVALUE:def 1; then
|. Rz .| < sqrt n * r0 * |. z .|; then
|. Rz .| / |. z .| < sqrt n * r0 by GG4,XREAL_1:83; then
|. z .|" * ||. R/.z .|| < sqrt n * (sqrt n)"*r by REAL_NS1:1; then
|. z .|" * ||. R/.z .|| < 1*r by LP1,XCMPLX_0:def 7;
hence |. z .|" * ||. R/.z .|| < r;
end;
hence thesis by DD3,PP1,PARTFUN1:def 6;
end; then
reconsider R as REST of REAL-NS n by NDIFF126;
reconsider N = ]. x0-d0,x0+d0.[ as Neighbourhood of x0
by AP2,RCOMP_1:def 6;
now let x be set;
assume AA1: x in N; then
reconsider y=x as Real;
T2: |. y - x0 .| < d0 by AA1,RCOMP_1:1;
1 <= n by NAT_1:14; then
T5: 1 in Seg n & 1 in dom d by A2; then
T3: ]. x0-d/.1,x0+d/.1.[ c= dom(Proj(1,n)*g) by A2;
dom(Proj(1,n)*g) c= dom g by RELAT_1:25; then
T4: ]. x0-d/.1,x0+d/.1.[ c= dom g by T3,XBOOLE_1:1;
len d = n by A2,FINSEQ_1:def 3; then
1 <= len d by NAT_1:14; then
d0 <= d.1 by RFINSEQ2:2; then
d0 <= d/.1 by T5,PARTFUN1:def 6; then
|. y - x0 .| < d/.1 by T2,XXREAL_0:2; then
y in ]. x0-d/.1,x0+d/.1.[ by RCOMP_1:1;
hence x in dom g by T4;
end; then
T1: N c= dom g by TARSKI:def 3;
ex L, R st for x be Real st x in N holds
g/.x - g/.x0 = L.(x-x0) + R/.(x-x0)
proof
take L0,R;
let x be Real;
assume x in N;
PP1: dom R = REAL by PARTFUN1:def 2;
R.(x-x0) = g/.(x-x0+x0) - g/.x0 - L.(x-x0) by A9; then
R/.(x-x0) = g/.x - g/.x0 + -(L0.(x-x0)) by PP1,PARTFUN1:def 6; then
L0.(x-x0) + R/.(x-x0)
= g/.x - g/.x0 + (-(L0.(x-x0)) + L0.(x-x0)) by RLVECT_1:def 3; then
L0.(x-x0) + R/.(x-x0) = g/.x - g/.x0 + (0.(REAL-NS n)) by RLVECT_1:5;
hence thesis by RLVECT_1:4;
end;
hence thesis by T1,NDIFF_3:def 3;
end;
theorem
for f be PartFunc of REAL,REAL n,
x0 be real number st
1 <= i & i <= n & f is_differentiable_in x0 holds
(Proj(i,n)*f) is_differentiable_in x0 &
Proj(i,n).(diff(f,x0)) = diff((Proj(i,n)*f),x0)
proof
let f be PartFunc of REAL,REAL n,
x0 be real number;
assume
AS: 1 <= i & i <= n & f is_differentiable_in x0;
then
consider g be PartFunc of REAL,REAL-NS n such that
A1: f=g & g is_differentiable_in x0 by def1;
diff(f,x0) = diff(g,x0) by A1,def2Th;
hence thesis by A1,AS,DPREP120;
end;
theorem
for f be PartFunc of REAL,REAL n,
x0 be real number holds
f is_differentiable_in x0 iff
(for i be Element of NAT st 1<=i & i <=n holds
Proj(i,n)*f is_differentiable_in x0)
proof
let f be PartFunc of REAL,REAL n, x0 be real number;
thus f is_differentiable_in x0 implies
(for i be Element of NAT st 1<=i & i <=n holds
Proj(i,n)*f is_differentiable_in x0)
proof
assume f is_differentiable_in x0;
then ex g be PartFunc of REAL,REAL-NS n st
f=g & g is_differentiable_in x0 by def1;
hence thesis by DPREP121;
end;
assume
AS: for i be Element of NAT st 1<=i & i <=n holds
Proj(i,n)*f is_differentiable_in x0;
reconsider g=f as PartFunc of REAL,REAL-NS n by REAL_NS1:def 4;
for i be Element of NAT st 1<=i & i <=n holds
Proj(i,n)*g is_differentiable_in x0 by AS;
then g is_differentiable_in x0 by DPREP121;
hence thesis by def1;
end;
theorem Th25:
for g be PartFunc of REAL,REAL-NS n st
1 <= i & i <= n & g is_differentiable_on X holds
(Proj(i,n)*g) is_differentiable_on X &
Proj(i,n)*(g`|X) = (Proj(i,n)*g)`|X
proof
let g be PartFunc of REAL,REAL-NS n;
assume
AS: 1 <= i & i <= n & g is_differentiable_on X;
then
A0: X is open Subset of REAL by NDIFF_3:9,11;
A2: dom(Proj(i,n)) = the carrier of REAL-NS n by FUNCT_2:def 1;
rng g c= the carrier of REAL-NS n;
then
dom(Proj(i,n)*g) = dom g by A2,RELAT_1:27;
then
A3: X c= dom(Proj(i,n)*g) by A0,AS,NDIFF_3:10;
now let x;
assume x in X;
then g is_differentiable_in x by A0,AS,NDIFF_3:10;
hence (Proj(i,n)*g) is_differentiable_in x by AS,DPREP120;
end;
hence
A40: (Proj(i,n)*g) is_differentiable_on X by A0,A3,NDIFF_3:10;
then
A4: dom ((Proj(i,n)*g)`|X) = X &
for x st x in X holds
((Proj(i,n)*g)`|X).x = diff((Proj(i,n)*g),x) by NDIFF_3:def 6;
A5: dom (g`|X) = X &
for x st x in X holds (g`|X).x = diff(g,x) by AS,NDIFF_3:def 6;
rng (g`|X) c= the carrier of REAL-NS n;
then
B10: dom (Proj(i,n)*(g`|X)) = dom (g`|X) by A2,RELAT_1:27;
now let x;
assume A60: x in dom ((Proj(i,n)*g)`|X);
then
A6: x in X by A40,NDIFF_3:def 6;
then g is_differentiable_in x by A0,AS,NDIFF_3:10;
then
A7: Proj(i,n).(diff(g,x)) = diff((Proj(i,n)*g),x) by AS,DPREP120;
A8: ((Proj(i,n)*g)`|X).x = diff((Proj(i,n)*g),x) by A60,A4;
(g`|X).x = diff(g,x) by A6,AS,NDIFF_3:def 6;
hence (Proj(i,n)*(g`|X)).x = ((Proj(i,n)*g)`|X).x
by A5,A6,A7,A8,FUNCT_1:13;
end;
hence thesis by B10,A4,A5,PARTFUN1:5;
end;
theorem Th25a:
for f be PartFunc of REAL,REAL n st
1 <= i & i <= n & f is_differentiable_on X holds
(Proj(i,n)*f) is_differentiable_on X &
Proj(i,n)*(f`|X) = (Proj(i,n)*f)`|X
proof
let f be PartFunc of REAL,REAL n;
assume
AS: 1 <= i & i <= n & f is_differentiable_on X;
then
A0: X is open Subset of REAL by Th15,OP1;
reconsider g=f as PartFunc of REAL,REAL-NS n by REAL_NS1:def 4;
A2: X c= dom g by A0,AS,Th16;
now let x;
assume x in X;
then f is_differentiable_in x by A0,AS,Th16;
hence g is_differentiable_in x by def1Th;
end;
then
A3: g is_differentiable_on X by A0,A2,NDIFF_3:10;
hence (Proj(i,n)*f) is_differentiable_on X by AS,Th25;
A6: dom (g`|X) = X &
for x st x in X holds (g`|X).x = diff(g,x) by A3,NDIFF_3:def 6;
B1: dom (f`|X) = dom (g`|X) by AS,Def8,A6;
B2: now let x;
assume x in dom (f`|X);
then
A7: x in X by AS,Def8;
then
A8: (f`|X).x = diff(f,x) by AS,Def8;
diff(f,x) = diff(g,x) by def2Th;
hence (f`|X).x = (g`|X).x by A8,A7,A3,NDIFF_3:def 6;
end;
g`|X is PartFunc of REAL,REAL n by REAL_NS1:def 4;
then Proj(i,n)*(f`|X) = Proj(i,n)*(g`|X) by B1,B2,PARTFUN1:5;
hence thesis by A3,AS,Th25;
end;
theorem Th26:
for g be PartFunc of REAL,REAL-NS n holds
g is_differentiable_on X iff
(for i be Element of NAT st 1<=i & i <=n holds
Proj(i,n)*g is_differentiable_on X)
proof
let g be PartFunc of REAL,REAL-NS n;
thus g is_differentiable_on X implies
(for i be Element of NAT st 1<=i & i <=n holds
Proj(i,n)*g is_differentiable_on X) by Th25;
assume AS: for i be Element of NAT st 1<=i & i <=n holds
Proj(i,n)*g is_differentiable_on X;
1 <=n by NAT_1:14;
then
A0: Proj(1,n)*g is_differentiable_on X by AS;
then
A1: X is open Subset of REAL by NDIFF_3:9,11;
XA2:dom(Proj(1,n)) = the carrier of REAL-NS n by FUNCT_2:def 1;
A30: rng g c= the carrier of REAL-NS n;
X c= dom (Proj(1,n)*g) by A0,A1,NDIFF_3:10;
then
A9: X c= dom g by A30,XA2,RELAT_1:27;
now let x;
assume AS0: x in X;
now let i be Element of NAT;
assume 1<=i & i <=n;
then Proj(i,n)*g is_differentiable_on X by AS;
hence Proj(i,n)*g is_differentiable_in x by AS0,A1,NDIFF_3:10;
end;
hence g is_differentiable_in x by DPREP121;
end;
hence thesis by A1,A9,NDIFF_3:10;
end;
theorem
for f be PartFunc of REAL,REAL n holds
f is_differentiable_on X iff
(for i be Element of NAT st 1<=i & i <=n holds
Proj(i,n)*f is_differentiable_on X)
proof
let f be PartFunc of REAL,REAL n;
thus f is_differentiable_on X implies
(for i be Element of NAT st 1<=i & i <=n holds
Proj(i,n)*f is_differentiable_on X) by Th25a;
assume AS: for i be Element of NAT st 1<=i & i <=n holds
Proj(i,n)*f is_differentiable_on X;
reconsider g=f as PartFunc of REAL,REAL-NS n by REAL_NS1:def 4;
for i be Element of NAT st 1<=i & i <=n holds
Proj(i,n)*g is_differentiable_on X by AS;
then
A1: g is_differentiable_on X by Th26;
then
A2: X is open Subset of REAL by NDIFF_3:9,11;
then
A4: X c= dom f by A1,NDIFF_3:10;
now let x;
assume x in X;
then g is_differentiable_in x by A2,A1,NDIFF_3:10;
hence f is_differentiable_in x by def1;
end;
hence thesis by A2,A4,Th16;
end;
theorem Th27:
for J be Function of REAL-NS 1,REAL,
x0 be Point of REAL-NS 1 st J=proj(1,1)
holds J is_continuous_in x0
proof
let J be Function of REAL-NS 1,REAL,
x0 be Point of REAL-NS 1;
assume AS: J=proj(1,1);
A1: dom J =the carrier of REAL-NS 1 by FUNCT_2:def 1;
now let r be Real;
assume AS1: 0 < r;
take s=r;
thus 0 < s by AS1;
thus for x1 be Point of REAL-NS 1 st x1
in dom J & ||. x1- x0 .|| ~~ = x & proj(1,1) qua Function".x
= <*x*>
proof
set f=proj(1,1);
for y be set st y in REAL ex x be set st x in REAL 1 & y = f.x
proof
let y be set;
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 PDIFF_1:def 1;
then f.x = y by FINSEQ_1:40;
hence thesis;
end;
hence thesis by FUNCT_2:10,def 1,PDIFF_1:1;
end;
theorem
for J be Function of REAL-NS 1,REAL,
x0 be Point of REAL-NS 1,
y0 be Element of REAL,
g be PartFunc of REAL,REAL-NS n,
f be PartFunc of REAL-NS 1,REAL-NS n
st J=proj(1,1)
& x0 in dom f & y0 in dom g & x0=<*y0*> & f = g*J
holds f is_continuous_in x0 iff g is_continuous_in y0
proof
let J be Function of REAL-NS 1,REAL,
x0 be Point of REAL-NS 1,
y0 be Element of REAL,
g be PartFunc of REAL,REAL-NS n,
f be PartFunc of REAL-NS 1,REAL-NS n;
assume AS: J=proj(1,1)
& x0 in dom f & y0 in dom g & x0=<*y0*> & f = g*J;
thus f is_continuous_in x0 implies g is_continuous_in y0
proof
reconsider I= proj(1,1) qua Function" as Function of REAL,REAL-NS 1
by PDIFF_1:2,REAL_NS1:def 4;
A3: J*I = id REAL by AS,Lm3,FUNCT_1:39;
A4: f*I = g*(id REAL) by AS,A3,RELAT_1:36
.= g by FUNCT_2:17;
I/.y0 = x0 by AS,PDIFF_1:1;
hence thesis by A4,Th27x,AS,NFCONT_3:15;
end;
J/.x0 = y0 by AS,PDIFF_1:1;
hence thesis by AS,Th27,Th28y;
end;
theorem
for I be Function of REAL,REAL-NS 1,
x0 be Point of REAL-NS 1,
y0 be Element of REAL,
g be PartFunc of REAL,REAL-NS n,
f be PartFunc of REAL-NS 1,REAL-NS n
st I=proj(1,1) qua Function" &
x0 in dom f & y0 in dom g & x0=<*y0*> & f*I = g
holds f is_continuous_in x0 iff g is_continuous_in y0
proof
let I be Function of REAL,REAL-NS 1,
x0 be Point of REAL-NS 1,
y0 be Element of REAL,
g be PartFunc of REAL,REAL-NS n,
f be PartFunc of REAL-NS 1,REAL-NS n;
assume AS: I=proj(1,1) qua Function" &
x0 in dom f & y0 in dom g & x0=<*y0*> & f*I = g;
reconsider J= proj(1,1) as Function of REAL-NS 1,REAL by LL;
thus f is_continuous_in x0 implies g is_continuous_in y0
proof
I/.y0 = x0 by AS,PDIFF_1:1;
hence thesis by AS,Th27x,NFCONT_3:15;
end;
A3: I*J = id REAL-NS 1 by AS,Lm3,LL,FUNCT_1:39;
A4: g*J = f*(id REAL-NS 1) by A3,AS,RELAT_1:36
.= f by FUNCT_2:17;
J/.x0 = y0 by AS,PDIFF_1:1;
hence thesis by A4,Th27,AS,Th28y;
end;
theorem
for I be Function of REAL,REAL-NS 1 st I = proj(1,1) qua Function"
holds I is_differentiable_in x0 & diff(I,x0) = <*1*>
proof
let I be Function of REAL,REAL-NS 1;
assume AS: I=proj(1,1) qua Function";
I.1 = <*1*> by AS,PDIFF_1:1;
then reconsider r = <*1*> as Point of REAL-NS 1;
Q0:for x be Real st x in ZR holds I/.x = x*r + 0.(REAL-NS 1)
proof
let x be Real;
assume x in ZR;
I.1 in REAL 1 by AS,FUNCT_1:3,PDIFF_1:2;
then
Q4: <*1*> is Element of REAL 1 by AS,PDIFF_1:1;
I/.x = <*x*1*> by AS,PDIFF_1:1
.= x*<*1*> by RVSUM_1:47;
hence I/.x = x*r by Q4,REAL_NS1:3
.= x*r + 0.(REAL-NS 1) by RLVECT_1:4;
end;
A1: ZR c= dom I by FUNCT_2:def 1;
then
P0:I is_differentiable_on ZR
& for x st x in ZR holds (I`|ZR).x = r by Q0,NDIFF_3:21;
r = (I`|ZR).x0 by A1,Q0,NDIFF_3:21
.= diff(I,x0) by P0,NDIFF_3:def 6;
hence thesis by P0,NDIFF_3:10;
end;
definition
let n be non empty Element of NAT;
let f be PartFunc of REAL-NS n,REAL;
let x be Point of REAL-NS n;
pred f is_differentiable_in x means
:PDIFF7def1a:
ex g be PartFunc of REAL n,REAL, y be Element of REAL n
st f=g & x=y & g is_differentiable_in y;
end;
definition
let n be non empty Element of NAT;
let f be PartFunc of REAL-NS n,REAL;
let x be Point of REAL-NS n;
func diff(f,x) -> Function of REAL-NS n,REAL means
:PDIFF7def2a:
ex g be PartFunc of REAL n,REAL, y be Element of REAL n
st f=g & x=y & it = diff(g,y);
existence
proof
reconsider g=f as PartFunc of REAL n,REAL by REAL_NS1:def 4;
reconsider y=x as Element of REAL n by REAL_NS1:def 4;
REAL n = the carrier of REAL-NS n by REAL_NS1:def 4;
then diff(g,y) is Function of REAL-NS n,REAL;
hence thesis;
end;
uniqueness;
end;
theorem Th29s:
for J be Function of REAL 1,REAL,
x0 be Element of REAL 1
st J=proj(1,1)
holds J is_differentiable_in x0 & diff(J,x0) = J
proof
let J be Function of REAL 1,REAL,
x0 be Element of REAL 1;
assume AS: J=proj(1,1);
P1: 1 in Seg 1;
set R = (REAL 1) --> (0*1);
set L = <>*J;
rng J = dom (proj(1,1) qua Function") by AS,P1,PDIFF_1:1,2;
then
P0: dom L = dom J by RELAT_1:27
.= REAL 1 by AS,P1,PDIFF_1:1;
reconsider L as Function of REAL 1,REAL 1 by PDIFF_1:2;
set f = <>*J;
X4: L= id (dom J) by AS,FUNCT_1:39
.= id (REAL 1) by AS,P1,PDIFF_1:1;
P2: for x,y being Element of REAL 1 holds L.(x+y) = L.x+L.y
proof
let x,y being Element of REAL 1;
thus L.(x+y) =x+y by X4,FUNCT_1:18
.=L.x+y by X4,FUNCT_1:18
.=L.x+L.y by X4,FUNCT_1:18;
end;
Q2: for x being Element of REAL 1, r being Real holds L.(r*x) = r*L.x
proof
let x being Element of REAL 1,r being Real;
thus L.(r*x) =r*x by X4,FUNCT_1:18
.=r*(L.x) by X4,FUNCT_1:18;
end;
then
P3: L is LinearOperator of 1,1 by P2,PDIFF_6:def 1,def 2;
reconsider r0=1 as Real;
P5: {y where y is Element of REAL 1: |.y-x0.| < r0} c= dom f
proof
let x be set;
assume x in {y where y is Element of REAL 1: |.y-x0.| < r0};
then ex y be Element of REAL 1 st x=y & |.y-x0.| < r0;
hence x in dom f by P0;
end;
P6:for r be Real st r > 0
ex d be Real st d > 0 &
for z be Element of REAL 1,w be Element of REAL 1 st
z <> 0*1 & |.z.| < d & w = R.z holds |.z.|"* |. w .| < r
proof
let r be Real;
assume A1: r > 0;
take d=r;
thus 0 < d by A1;
let z be Element of REAL 1,w be Element of REAL 1;
assume A2: z <> 0*1 & |.z.| < d & w = R.z;
w= 0*1 by A2,FUNCOP_1:7;
then |. w .| = 0 by EUCLID:7;
hence thesis by A1;
end;
A7: for x be Element of REAL 1 st |.x-x0.| < r0 holds
f/.x - f/.x0 = L.(x-x0) + R.(x-x0)
proof
let x be Element of REAL 1;
assume |.x-x0.| < r0;
A3: f/.x0 =L.x0 by P0,PARTFUN1:def 6;
A6: -1 is Real by XREAL_0:def 1;
thus f/.x - f/.x0 = L.x -L.x0 by A3,P0,PARTFUN1:def 6
.=L.x +L.((-1)*x0) by A6,Q2
.=L.(x-x0) by P2
.=L.(x-x0) + 0*1 by RVSUM_1:16
.= L.(x-x0) + R.(x-x0) by FUNCOP_1:7;
end;
then f is_differentiable_in x0 & diff(f,x0) = L by P3,P5,P6,PDIFF_6:24;
hence J is_differentiable_in x0 by PDIFF_7:def 1;
D2: rng J c= REAL;
thus diff(J,x0) =proj(1,1)*L by A7,P3,P5,P6,PDIFF_6:24
.=proj(1,1)*(proj(1,1) qua Function") * J by RELAT_1:36
.=id (rng proj(1,1) )* J by FUNCT_1:39
.= id REAL * J by P1,PDIFF_1:1
.=J by D2,RELAT_1:53;
end;
theorem
for J be Function of REAL-NS 1,REAL,
x0 be Point of REAL-NS 1
st J=proj(1,1)
holds J is_differentiable_in x0 & diff(J,x0) = J
proof
let J be Function of REAL-NS 1,REAL,
x0 be Point of REAL-NS 1;
assume AS: J=proj(1,1);
reconsider J0=J as Function of REAL 1,REAL by LL;
reconsider y0=x0 as Element of REAL 1 by REAL_NS1:def 4;
J0 is_differentiable_in y0 & diff(J0,y0) = J by AS,Th29s;
hence J is_differentiable_in x0 by PDIFF7def1a;
ex g be PartFunc of REAL 1,REAL, y be Element of REAL 1 st
J=g & x0=y & diff(J,x0) = diff(g,y) by PDIFF7def2a;
hence thesis by AS,Th29s;
end;
theorem PDIFF15:
for I be Function of REAL,REAL-NS 1 st
I=proj(1,1) qua Function" holds
(for R being REST of REAL-NS 1,REAL-NS n holds
R*I is REST of REAL-NS n) &
for L being LinearOperator of REAL-NS 1,REAL-NS n holds
L*I is LINEAR of REAL-NS n
proof
let I be Function of REAL,REAL-NS 1;
assume A1: I=proj(1,1) qua Function";
thus for R being REST of REAL-NS 1, REAL-NS n holds R*I is REST of REAL-NS n
proof
let R be REST of REAL-NS 1,REAL-NS n;
A3: R is total by NDIFF_1:def 5;
reconsider R0=R as Function of REAL 1,REAL n
by A3,LL,REAL_NS1:def 4;
reconsider R1=R*I as PartFunc of REAL,REAL-NS n;
A4: R0*I is Function of REAL,REAL n by LL;
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: abs z1 < d;
reconsider z = I.z1 as Point of REAL-NS 1;
z1 in REAL;
then reconsider z1r = z1 as R_eal by NUMBERS:31;
0 < |.z1r.| by A9,EXTREAL2:4;
then abs z1 > 0 by EXTREAL2:1;
then ||.z.|| <> 0 by A1,LL,PDIFF_1:3;
then
A11: z <> 0.(REAL-NS 1);
A12: dom I = REAL by FUNCT_2:def 1;
R is total by NDIFF_1:def 5;
then dom R = the carrier of REAL-NS 1 by PARTFUN1:def 2;
then R/.z = R.(I.z1) by PARTFUN1:def 6;
then R/.z = R1.z1 by A12,FUNCT_1:13;
then
A16: ||. R/.z .|| =||. R1/.z1 .|| by A5,PARTFUN1:def 6;
A17: ||.z.||" = abs(z1)" by A1,LL,PDIFF_1:3;
||.z.|| < d by A1,A10,LL,PDIFF_1:3;
hence thesis by A8,A11,A17,A16;
end;
hence thesis by A7;
end;
for h be convergent_to_0 Real_Sequence holds h"(#)(R1/*h) is
convergent & lim(h"(#)(R1/*h)) = 0.(REAL-NS n)
proof
let h be convergent_to_0 Real_Sequence;
A18: now
let r be Real;
A19: lim h = 0 by FDIFF_1:def 1;
assume r > 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 number;
h is convergent by FDIFF_1:def 1;
then consider n0 be Element of NAT such that
A22: for m be Element of NAT st n0 <= m holds abs(h.m-0) < d1 by A20,A19,
SEQ_2:def 7;
take n0;
hereby
let m be Element of NAT;
h is non-zero by FDIFF_1:def 1;
then
A23: h.m <> 0 by SEQ_1:5;
rng h c= dom R1 by A5;
then
A24: abs(h.m)" * ||. R1/.(h.m) .|| = abs(h.m)" * ||. (R1/*h).m .||
by FUNCT_2:109
.= ((abs h).m)" * ||. (R1/*h).m .|| by SEQ_1:12
.= (abs h)".m * ||. (R1/*h).m .|| by VALUED_1:10
.= abs(h").m * ||. (R1/*h).m .|| by SEQ_1:54
.= abs(h".m) * ||. (R1/*h).m .|| by SEQ_1:12
.= ||. h".m * (R1/*h).m .|| by NORMSP_1:def 1
.= ||. (h"(#)(R1/*h)).m .|| by NDIFF_1:def 2
.= ||. (h"(#)(R1/*h)).m - 0.(REAL-NS n) .|| by RLVECT_1:13;
assume n0 <= m;
then abs(h.m - 0) < d by A22;
hence ||. (h"(#)(R1/*h)).m - 0.(REAL-NS n) .|| < r
by A21,A23,A24;
end;
end;
hence (h")(#)(R1/*h) is convergent by NORMSP_1:def 6;
hence thesis by A18,NORMSP_1:def 7;
end;
hence thesis by A4,NDIFF_3:def 1;
end;
let L be LinearOperator of REAL-NS 1,REAL-NS n;
reconsider L0=L as Function of REAL 1, REAL n by LL,REAL_NS1:def 4;
reconsider L1=L0*I as PartFunc of REAL,REAL-NS n by REAL_NS1:def 4;
reconsider r = L1.1 as Point of (REAL-NS n) by FUNCT_2:5;
A28: dom(L0*I) = REAL by LL,FUNCT_2:def 1;
for p be Real holds L1.p = p*r
proof
reconsider 1p = I.1 as VECTOR of REAL-NS 1;
let p be Real;
dom I = REAL by FUNCT_2:def 1;
then L1.p = L.(I.(p*1)) by FUNCT_1:13;
then L1.p = L.(p*1p) by A1,LL,PDIFF_1:3;
then L1.p = p*(L.1p) by LOPBAN_1:def 5;
hence thesis by A28,FUNCT_1:12;
end;
hence thesis by NDIFF_3:def 2;
end;
theorem PDIFF16:
for J be Function of REAL-NS 1,REAL st J = proj(1,1) holds
(for R being REST of REAL-NS n holds
R*J is REST of REAL-NS 1,REAL-NS n) &
for L being LINEAR of REAL-NS n holds
L*J is Lipschitzian LinearOperator of REAL-NS 1,REAL-NS n
proof
let J be Function of REAL-NS 1,REAL;
assume A2: J=proj(1,1);
thus
for R being REST of REAL-NS n holds R*J is REST of REAL-NS 1,REAL-NS n
proof
let R be REST of REAL-NS n;
A3: R is total by NDIFF_3:def 1;
reconsider R0=R as Function of REAL,REAL n by A3,REAL_NS1:def 4;
reconsider R1 = R0*J as PartFunc of REAL-NS 1,REAL-NS n
by REAL_NS1:def 4;
for h be convergent_to_0 sequence of REAL-NS 1 holds ||.h.||"(#)(R1/*h
) is convergent & lim(||.h.||"(#)(R1/*h)) = 0.(REAL-NS n)
proof
let h be convergent_to_0 sequence of REAL-NS 1;
A4: lim h = 0.(REAL-NS 1) by NDIFF_1:def 4;
deffunc F(Element of NAT)=J.(h.$1);
consider s be Real_Sequence such that
A5: for n be Element of 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 number;
A8: p is Real by XREAL_0:def 1;
assume 0 < p;
then consider m be Element of NAT such that
A9: for n be Element of NAT st m <= n holds ||. h.n - 0.(REAL-NS
1).|| < p by A6,A4,A8,NORMSP_1:def 7;
take m;
now
let n be Element of NAT;
assume m <= n;
then ||. h.n - 0.(REAL-NS 1).|| < p by A9;
then
A10: ||. h.n .|| < p by RLVECT_1:13;
s.n = J.(h.n) by A5;
hence abs(s.n-0) < p by A2,A10,PDIFF_1:4;
end;
hence for n be Element of NAT st m <= n holds abs(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;
A13: h is non-zero by NDIFF_1:def 4;
now
let x be set;
assume x in NAT;
then reconsider n=x as Element of NAT;
A14: 0 <= abs(s.n) by COMPLEX1:46;
h.n <> 0.(REAL-NS 1) by A13,NDIFF_1:6;
then
A15: ||. h.n .|| <> 0 by NORMSP_0:def 5;
s.n = J.(h.n) by A5;
then abs(s.n) <> 0 by A2,A15,PDIFF_1:4;
hence s.x <> 0 by A14,COMPLEX1:47;
end;
then s is non-zero by SEQ_1:4;
then reconsider s as convergent_to_0 Real_Sequence
by A11,A12,FDIFF_1:def 1;
now
reconsider f1=R1 as Function;
let n be Element of NAT;
A17: rng h c= the carrier of REAL-NS 1;
(R/*s).n =R.(s.n) by A3,FUNCT_2:115;
then
B19: (R/*s).n =R.(J.(h.n)) by A5;
NAT = dom h by FUNCT_2:def 1;
then
A20: R1.(h.n) =(f1*h).n by FUNCT_1:13;
rng h c= dom R1 by A17,FUNCT_2:def 1;
then
B21: R1.(h.n) =(R1/*h).n by A20,FUNCT_2:def 11;
A23: 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
.= abs((||.h.||").n) * ||.(R1/*h).n .|| by NORMSP_1:def 1
.= abs((||.h.||.n)") * ||.(R1/*h).n .|| by VALUED_1:10
.= abs(||.h.n.||") * ||.(R1/*h).n .|| by NORMSP_0:def 4
.= ||.h.n .||" *||.(R1/*h).n .|| by ABSVALUE:def 1
.= (abs(s.n))" *||.(R1/*h).n .|| by A2,A23,PDIFF_1:4
.= (abs(s.n))" *||.(R/*s).n .|| by B21,B19,FUNCT_2:15
.= ((abs s).n)"*||.(R/*s).n .|| by SEQ_1:12
.= ((abs s)".n)*||.(R/*s).n .|| by VALUED_1:10
.=(abs(s").n)*||.(R/*s).n .|| by SEQ_1:54
.=abs(s".n)*||.(R/*s).n .|| by SEQ_1:12
.= ||. (s".n)*(R/*s).n .|| by NORMSP_1:def 1
.= ||. (s"(#)(R/*s)).n .|| by NDIFF_1:def 2
.= ||. (s"(#)(R/*s)) .||.n by NORMSP_0:def 4;
hence ||. ||.h.||"(#)(R1/*h) .|| .n = ||. (s"(#)(R/*s)) .||.n;
end;
then
A24: ||. ||.h.||"(#)(R1/*h) .|| = ||. s"(#)(R/*s) .|| by FUNCT_2:63;
A25: lim(s"(#)(R/*s))=0.(REAL-NS n) by NDIFF_3:def 1;
A26: s"(#)(R/*s) is convergent by NDIFF_3:def 1;
A27: lim ||. s"(#)(R/*s) .|| = ||.0.(REAL-NS n).|| by A25,A26,LOPBAN_1:20
.= 0;
A28: ||. s"(#)(R/*s) .|| is convergent by A26,NORMSP_1:23;
A29: now
let p be Real;
assume 0 < p;
then consider n0 be Element of NAT such that
A30: for m be Element of NAT st n0 <= m holds abs(||. ||.h.||"(#)(
R1/*h).||.m - 0) < p by A24,A28,A27,SEQ_2:def 7;
take n0;
hereby
let m be Element of NAT;
assume n0 <= m;
then abs(||. ||.h.||"(#)(R1/*h).|| .m - 0) < p by A30;
then
A31: abs ||.( ||.h.||"(#)(R1/*h)).m.|| < p by NORMSP_0:def 4;
||.(||.h.||"(#)(R1/*h)).m.|| < p by A31,ABSVALUE:def 1;
hence ||.(||.h.||"(#)(R1/*h)).m -0.(REAL-NS n) .|| < p
by RLVECT_1:13;
end;
end;
then ||.h.||"(#)(R1/*h) is convergent by NORMSP_1:def 6;
hence thesis by A29,NORMSP_1:def 7;
end;
hence thesis by NDIFF_1:def 5;
end;
let L be LINEAR of REAL-NS n;
consider r be Point of REAL-NS n such that
A32: for p be Real holds L.p = p*r by NDIFF_3:def 2;
reconsider L0 = L as Function of REAL,REAL n by REAL_NS1:def 4;
set K = ||.r.||;
reconsider L1 = L*J as Function of REAL-NS 1,REAL-NS n;
A34: dom L1 = REAL 1 by LL,FUNCT_2:def 1;
A36: now
let x,y be Point of REAL-NS 1;
L1.(x+y) =L.(J.(x+y)) by LL,A34,FUNCT_1:12;
then L1.(x+y) = L.((J.x+J.y)) by A2,PDIFF_1:4;
then L1.(x+y) = (J.x+J.y)*r by A32;
then L1.(x+y) = (J.x)*r+(J.y)*r by RLVECT_1:def 6;
then L1.(x+y) = L.(J.x)+(J.y)*r by A32;
then
A38: L1.(x+y) = L.(J.x)+L.(J.y) by A32;
L.(J.x) = L1.x by LL,A34,FUNCT_1:12;
hence L1.(x+y) =L1.x + L1.y by LL,A34,A38,FUNCT_1:12;
end;
now
let x be Point of REAL-NS 1, a be Real;
L1.(a*x) = L.(J.(a*x)) by LL,A34,FUNCT_1:12;
then L1.(a*x) = L.(a*(J.x)) by A2,PDIFF_1:4;
then L1.(a*x) = (a*(J.x))*r by A32;
then
B39: L1.(a*x) = a*((J.x)*r) by RLVECT_1:def 7;
L.(J.x) = L1.x by LL,A34,FUNCT_1:12;
hence L1.(a*x) =a*(L1.x) by B39,A32;
end;
then reconsider L1 as LinearOperator of REAL-NS 1,REAL-NS n by A36,
GRCAT_1:def 8,LOPBAN_1:def 5;
now
let x be Point of REAL-NS 1;
||. L1.x .|| =||. L.(J.x) .|| by LL,A34,FUNCT_1:12;
then ||. L1.x .|| =||. (J.x)*r .|| by A32;
then ||. L1.x .|| =||.r.||*|.J.x .| by NORMSP_1:def 1;
hence ||. L1.x .|| <= K* ||.x.|| by A2,PDIFF_1:4;
end;
hence thesis by LOPBAN_1:def 8;
end;
theorem Th30A:
for I be Function of REAL,REAL-NS 1,
x0 be Point of REAL-NS 1,
y0 be Element of REAL,
g be PartFunc of REAL,REAL-NS n,
f be PartFunc of REAL-NS 1,REAL-NS n
st I=proj(1,1) qua Function" & x0 in dom f & y0 in dom g
& x0=<*y0*> & f*I = g & f is_differentiable_in x0
holds g is_differentiable_in y0
& diff(g,y0)=diff(f,x0).<*1*>
& for r be Element of REAL holds diff(f,x0).<*r*> = r*diff(g,y0)
proof
let I be Function of REAL,REAL-NS 1,
x0 be Point of REAL-NS 1,
y0 be Element of REAL,
g be PartFunc of REAL,REAL-NS n,
f be PartFunc of REAL-NS 1,REAL-NS n;
assume that
AS: I=proj(1,1) qua Function" and
w1: x0 in dom f and
w2: y0 in dom g and
w3: x0=<*y0*> and
w4: f*I = g;
reconsider J= proj(1,1) as Function of REAL-NS 1, REAL by LL;
assume AS1: f is_differentiable_in x0;
then
consider NN being Neighbourhood of x0 such that
P1: NN c= dom f and
P2: ex L be
Point of R_NormSpace_of_BoundedLinearOperators(REAL-NS 1,REAL-NS n),
R be REST of REAL-NS 1,REAL-NS n
st for x be Point of REAL-NS 1 st x in NN
holds f/.x - f/.x0 = L.(x-x0) + R/.(x-x0) by NDIFF_1:def 6;
A0: I*J = id REAL-NS 1 by LL,AS,Lm3,FUNCT_1:39;
A1: g*J = f*(id REAL-NS 1) by A0,w4,RELAT_1:36
.= f by FUNCT_2:17;
consider e be Real such that
A7: 0 < e and
A8: {z where z is Point of REAL-NS 1 : ||.z-x0.|| < e} c= NN by NFCONT_1:def 1;
consider L be
Point of R_NormSpace_of_BoundedLinearOperators(REAL-NS 1,REAL-NS n),
R being REST of REAL-NS 1,REAL-NS n such that
A9: for x9 be Point of REAL-NS 1 st x9 in NN holds
f/.x9 - f/.x0 = L.(x9-x0) + R/.(x9-x0) by P2;
reconsider R0=R*I as REST of REAL-NS n by AS,PDIFF15;
L is LinearOperator of REAL-NS 1,REAL-NS n by LOPBAN_1:def 9;
then
reconsider L0=L*I as LINEAR of REAL-NS n by AS,PDIFF15;
set N={z where z is Point of REAL-NS 1 : ||.z-x0.|| < e};
A10: N c= the carrier of REAL-NS 1
proof
let y be set;
assume y in N;
then ex z be Point of REAL-NS 1 st y=z & ||.z-x0.|| < e;
hence thesis;
end;
then reconsider N as Neighbourhood of x0 by A7,NFCONT_1:def 1;
set N0={z where z is Element of REAL: abs(z-y0) < e};
A11: N c= dom f by P1,A8,XBOOLE_1:1;
now
let z be set;
hereby
assume z in N0;
then consider y9 be Element of REAL such that
A12: z=y9 and
A13: abs(y9-y0) < e;
reconsider w=I.y9 as Point of REAL-NS 1;
x0=I.y0 by AS,w3,Lm3;
then w-x0=I.(y9-y0) by AS,LL,PDIFF_1:3;
then ||.w-x0.||=abs(y9-y0) by AS,LL,PDIFF_1:3;
then
Y1: w in {z0 where z0 is Point of REAL-NS 1 : ||.z0 - x0.|| < e} by A13;
J.(I.y9) = y9 by AS,Lm3,FUNCT_1:35;
hence z in J.:N by Y1,A12,FUNCT_2:35;
end;
assume z in J.:N;
then consider ww be set 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-x0.|| < e by A14;
reconsider y9=J.w as Element of REAL;
J.x0=y0 by w3,Lm3;
then J.(w-x0) =y9-y0 by PDIFF_1:4;
then abs(y9-y0) < e by A17,PDIFF_1:4;
hence z in N0 by A15,A16;
end;
then
A18: N0=J.:N by TARSKI:1;
J.:(dom f) = J.:(J"(dom g)) by A1,RELAT_1:147;
then
A19: J.:(dom f) = dom(f*I) by w4,Lm3,FUNCT_1:77;
A20: I*J =id (REAL 1) by AS,Lm3,FUNCT_1:39;
N c= dom f by P1,A8,XBOOLE_1:1;
then
A22: N0 c= dom(f*I) by A19,A18,RELAT_1:123;
A23: ].y0-e,y0+e.[ c= N0
proof
now let d be set such that
A24: d in ].y0-e,y0+e.[;
reconsider y1=d as Element of REAL by A24;
abs(y1-y0) < e by A24,RCOMP_1:1;
hence d in N0;
end;
hence thesis by TARSKI:def 3;
end;
N0 c= ].y0-e,y0+e.[
proof
let d be set;
assume d in N0;
then ex r be Element of REAL st d=r & abs(r-y0) < e;
hence thesis by RCOMP_1:1;
end;
then
N0 = ].y0-e,y0+e.[ by A23,XBOOLE_0:def 10;
then
A25: N0 is Neighbourhood of y0 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 y1 be Real st y1 in N0 holds
(f*I)/.y1 - (f*I)/.y0 = L0.(y1-y0) + R0/.(y1-y0)
proof
let y1 be Real;
reconsider y9 = I.y1 as Point of REAL-NS 1;
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 NDIFF_3:def 1;
then
B29: dom(R*I) = REAL by PARTFUN1:def 2;
R/.(I.(y1-y0)) =R.(I.(y1-y0)) by A28,PARTFUN1:def 6;
then R/.(I.(y1-y0)) =R0.(y1-y0) by B29,FUNCT_1:12;
then
A30: R/.(I.(y1-y0)) =R0/.(y1-y0) by B29,PARTFUN1:def 6;
L0 is total;
then
B31: dom(L*I) = REAL by PARTFUN1:def 2;
assume
A32: y1 in N0;
then
A33: I.y1 in N by A26,FUNCT_2:35;
then
B33: f/.(I.y1) =f.(I.y1) by A11,PARTFUN1:def 6;
f/.(I.y1) =(f*I).y1 by B33,A22,A32,FUNCT_1:12;
then
A38: f/.(I.y1) =(f*I)/.y1 by A22,A32,PARTFUN1:def 6;
A39: x0=I.y0 by w3,AS,Lm3;
then f/.(I.y0) =f.(I.y0) by w1,PARTFUN1:def 6;
then f/.(I.y0) =(f*I).y0 by w2,w4,FUNCT_1:12;
then
A41: f/.(I.y0) =(f*I)/.y0 by w2,w4,PARTFUN1:def 6;
f/.y9 - f/.x0=L.(y9-x0) + R/.(y9-x0) by A9,A8,A33;
then
A42: f/.(I.y1) - f/.(I.y0)=L.(I.(y1-y0)) + R/.(y9-x0)
by AS,A39,LL,PDIFF_1:3;
L.(I.(y1-y0)) =L0.(y1-y0) by B31,FUNCT_1:12;
hence thesis by A39,A42,A30,A38,A41,AS,LL,PDIFF_1:3;
end;
then
XX2:f*I is_differentiable_in y0 by A25,A22,NDIFF_3:def 3;
thus
g is_differentiable_in y0 by w4,A27,A25,A22,NDIFF_3:def 3;
X5: diff(f*I,y0)=L0.1 by A27,XX2,A25,A22,NDIFF_3:def 4;
thus
XX7:diff(g,y0)=(diff(f,x0)*I).1 by w4,X5,AS1,A9,P1,NDIFF_1:def 7
.=diff(f,x0).(I.1) by AS,FUNCT_1:13,PDIFF_1:2
.=diff(f,x0).<*1*> by AS,Lm3;
let r be Element of REAL;
Q4: <*1*> is Element of REAL 1 by FINSEQ_2:98;
then reconsider x = <*1*> as Point of REAL-NS 1 by REAL_NS1:def 4;
Q6: diff(f,x0) is LinearOperator of REAL-NS 1,REAL-NS n
by LOPBAN_1:def 9;
thus diff(f,x0).<*r*> = diff(f,x0).<*r*1*>
.= diff(f,x0).(r*<*1*>) by RVSUM_1:47
.= diff(f,x0).(r*x) by Q4,REAL_NS1:3
.= r*diff(g,y0) by XX7,Q6,LOPBAN_1:def 5;
end;
theorem Th30:
for I be Function of REAL,REAL-NS 1,
x0 be Point of REAL-NS 1,
y0 be Element of REAL,
g be PartFunc of REAL,REAL-NS n,
f be PartFunc of REAL-NS 1,REAL-NS n
st I=proj(1,1) qua Function" & x0 in dom f & y0 in dom g
& x0=<*y0*> & f*I = g
holds f is_differentiable_in x0 iff g is_differentiable_in y0
proof
let I be Function of REAL,REAL-NS 1,
x0 be Point of REAL-NS 1,
y0 be Element of REAL,
g be PartFunc of REAL,REAL-NS n,
f be PartFunc of REAL-NS 1,REAL-NS n;
assume that
AS: I=proj(1,1) qua Function" and
w1: x0 in dom f and
w2: y0 in dom g and
w3: x0=<*y0*> and
w4: f*I = g;
reconsider J = proj(1,1) as Function of REAL-NS 1, REAL by LL;
thus f is_differentiable_in x0 implies g is_differentiable_in y0
by w1,w2,w3,w4,Th30A,AS;
assume g is_differentiable_in y0;
then
consider N0 being Neighbourhood of y0 such that
P1: N0 c= dom (f*I) and
P2: ex L be LINEAR of REAL-NS n,R be REST of REAL-NS n st
for y be Real st y in N0 holds
(f*I)/.y - (f*I)/.y0 = L.(y-y0) + R/.(y-y0) by w4,NDIFF_3:def 3;
A0: I*J = id REAL-NS 1 by LL,AS,Lm3,FUNCT_1:39;
A1: g*J = f*(id REAL-NS 1) by w4,A0,RELAT_1:36
.= f by FUNCT_2:17;
consider e0 be real number such that
A6: 0 < e0 and
A7: N0 = ].y0 - e0,y0 + e0.[ by RCOMP_1:def 6;
reconsider e = e0 as Real by XREAL_0:def 1;
set N = {z where z is Point of REAL-NS 1 : ||.z-x0.|| < e};
consider L be LINEAR of REAL-NS n, R be REST of REAL-NS n such that
A10: for y1 be Real st y1 in N0 holds
(f*I)/.y1 - (f*I)/.y0 = L.(y1-y0) + R/.(y1-y0) by P2;
reconsider R0=R*J as REST of REAL-NS 1,REAL-NS n by PDIFF16;
reconsider L0=L*J as Lipschitzian LinearOperator of REAL-NS 1,REAL-NS n
by PDIFF16;
now
let z be set;
hereby
assume z in N;
then consider w be Point of REAL-NS 1 such that
A14: z=w and
A15: ||.w-x0.|| < e;
reconsider y2=J.w as Element of REAL;
J.x0=y0 by w3,Lm3;
then J.(w-x0) =y2-y0 by PDIFF_1:4;
then abs(y2-y0) < e by A15,PDIFF_1:4;
then
A16: y2 in N0 by A7,RCOMP_1:1;
w in the carrier of REAL-NS 1;
then w in dom J by Lm3,REAL_NS1:def 4;
then w=I.y2 by AS,FUNCT_1:34;
hence z in I.:N0 by A14,A16,FUNCT_2:35;
end;
assume z in I.:N0;
then consider yy be set such that
A17: yy in REAL and
A18: yy in N0 and
A19: z=I.yy by FUNCT_2:64;
reconsider y3=yy as Element of REAL by A17;
set w = I.y3;
I.y0=x0 by w3,AS,Lm3;
then
A20: w-x0 =I.(y3-y0) by AS,LL,PDIFF_1:3;
abs(y3-y0) < e by A7,A18,RCOMP_1:1;
then ||.w-x0.|| < e by A20,AS,LL,PDIFF_1:3;
hence z in N by A19;
end;
then
A21: N=I.:N0 by TARSKI:1;
I.:(dom g) = I.:(I"(dom f)) by w4,RELAT_1:147;
then I.:(dom g) = dom f by AS,LL,FUNCT_1:77,PDIFF_1:2;
then
A23: N c= dom f by w4,P1,A21,RELAT_1:123;
N c= the carrier of REAL-NS 1
proof
let y be set;
assume y in N;
then ex z be Point of REAL-NS 1 st y=z & ||.z-x0.|| < e;
hence thesis;
end;
then
A24: N is Neighbourhood of x0 by A6,NFCONT_1:def 1;
J*I=id REAL by AS,Lm3,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/.x0 = L0.(y-x0) + R0/.(y-x0)
proof
x0 in the carrier of REAL-NS 1;
then x0 in dom J by Lm3,REAL_NS1:def 4;
then
g.(J.x0) =f.x0 by A1,FUNCT_1:13;
then
A29: g.(J.x0) =f/.x0 by w1,PARTFUN1:def 6;
C29: J.x0 = y0 by w3,Lm3;
let y be Point of REAL-NS 1;
assume
A30: y in N;
set y3 = J.y;
reconsider p1=g/.y3,p2=g/.y0, q1=L.(y3-y0), q2=R/.(y3-y0)
as VECTOR of REAL-NS n;
A31: J.x0=y0 by w3,Lm3;
g/.y3 - g/.y0=q1+q2 by w4,A10,A25,A30,FUNCT_2:35;
then g/.(J.y) - g/.(J.x0)=L.(J.(y-x0)) + R/.(y3-y0) by A31,PDIFF_1:4;
then
A32: g/.(J.y) - g/.(J.x0)= L.(J.(y-x0)) + R/.(J.(y-x0)) by A31,PDIFF_1:4;
B33: dom L0 = the carrier of REAL-NS 1 by FUNCT_2:def 1;
y-x0 in the carrier of REAL-NS 1;
then y-x0 in dom J by Lm3,REAL_NS1:def 4;
then
A35: R.(J.(y-x0)) =(R*J).(y-x0) by FUNCT_1:13;
R0 is total by NDIFF_1:def 5;
then
A36: dom(R*J) = the carrier of REAL-NS 1 by PARTFUN1:def 2;
A37: R.(J.(y-x0)) =R0/.(y-x0) by A35,A36,PARTFUN1:def 6;
J.(y-x0) in dom R by A36,FUNCT_1:11;
then
B37: R/.(J.(y-x0)) =R0/.(y-x0) by A37,PARTFUN1:def 6;
y in the carrier of REAL-NS 1;
then
B38: y in dom J by Lm3,REAL_NS1:def 4;
g.(J.y) =f.y by A1,B38,FUNCT_1:13;
then
C39: g.(J.y) =f/.y by A23,A30,PARTFUN1:def 6;
J.y in dom g by A23,A30,A1,FUNCT_1:11;
then g/.(J.y) =f/.y by C39,PARTFUN1:def 6;
then g/.(J.y) - g/.(J.x0) = f/.y -f/.x0 by w2,C29,A29,PARTFUN1:def 6;
hence thesis by A32,B37,B33,FUNCT_1:12;
end;
L0 is Point of R_NormSpace_of_BoundedLinearOperators(REAL-NS 1,REAL-NS n)
by LOPBAN_1:def 9;
hence thesis by A24,A23,A26,NDIFF_1:def 6;
end;
theorem Th31:
for J be Function of REAL-NS 1,REAL,
x0 be Point of REAL-NS 1,
y0 be Element of REAL,
g be PartFunc of REAL,REAL-NS n,
f be PartFunc of REAL-NS 1,REAL-NS n
st J=proj(1,1) & x0 in dom f & y0 in dom g
& x0=<*y0*> & f = g*J
holds f is_differentiable_in x0 iff g is_differentiable_in y0
proof
let J be Function of REAL-NS 1,REAL,
x0 be Point of REAL-NS 1,
y0 be Element of REAL,
g be PartFunc of REAL,REAL-NS n,
f be PartFunc of REAL-NS 1,
REAL-NS n;
assume AS: J=proj(1,1) & x0 in dom f & y0 in dom g & x0=<*y0*> & f = g*J;
reconsider I= (proj(1,1) qua Function") as Function of REAL,REAL-NS 1
by PDIFF_1:2,REAL_NS1:def 4;
A0: J*I = id REAL by AS,Lm3,FUNCT_1:39;
f*I = g*(id REAL) by AS,A0,RELAT_1:36
.= g by FUNCT_2:17;
hence thesis by AS,Th30;
end;
theorem
for J be Function of REAL-NS 1,REAL,
x0 be Point of REAL-NS 1,
y0 be Element of REAL,
g be PartFunc of REAL,REAL-NS n,
f be PartFunc of REAL-NS 1,REAL-NS n
st J=proj(1,1) & x0 in dom f & y0 in dom g
& x0=<*y0*> & f = g*J & g is_differentiable_in y0
holds
f is_differentiable_in x0
& diff(g,y0)=diff(f,x0).<*1*>
& for r be Element of REAL holds diff(f,x0).<*r*> = r*diff(g,y0)
proof
let J be Function of REAL-NS 1,REAL,
x0 be Point of REAL-NS 1,
y0 be Element of REAL,
g be PartFunc of REAL,REAL-NS n,
f be PartFunc of REAL-NS 1,REAL-NS n;
assume AS: J=proj(1,1) & x0 in dom f & y0 in dom g & x0=<*y0*> & f = g*J
& g is_differentiable_in y0;
hence
D1: f is_differentiable_in x0 by Th31;
reconsider I= (proj(1,1) qua Function") as Function of REAL,REAL-NS 1
by PDIFF_1:2,REAL_NS1:def 4;
A0: J*I = id REAL by AS,Lm3,FUNCT_1:39;
f*I = g*(id REAL) by AS,A0,RELAT_1:36
.= g by FUNCT_2:17;
hence thesis by AS,Th30A,D1;
end;
theorem NDIFF27:
for R be REST of REAL-NS n st R/.0=0.(REAL-NS n)
for e be Real st e > 0 ex d be Real st
d > 0 & for h be Real st |.h.| < d holds ||.R/.h.|| <= e*|.h.|
proof
let R be REST of REAL-NS n such that
A1: R/.0=0.(REAL-NS n);
let e be Real such that
A2: e > 0;
R is total by NDIFF_3:def 1;
then consider d be Real such that
A3: d > 0 and
A4: for z be Real st z <> 0 & |.z.| < d holds ( |.z.|"* ||.
R/.z .||) < e by A2,NDIFF126;
take d;
now
let h be Real such that
A5: |.h.| < d;
now
per cases;
case
A6: h <> 0;
then 0 <= |.h.| & |.h.|"*||. R/.h .|| <= e by A4,A5,COMPLEX1:46;
then |.h.|*(|.h.|"*||. R/.h .||) <= |.h.|*e by XREAL_1:64;
then
A7: |.h.|*|.h.|"*||. R/.h .|| <= e* |.h.|;
|.h.| <> 0 by A6,COMPLEX1:45;
then 1*||. R/.h .|| <= e* |.h.| by A7,XCMPLX_0:def 7;
hence ||. R/.h .|| <= e* |.h.|;
end;
case
A8: h = 0;
reconsider p0=0 as Real;
0 <= |.h.| by COMPLEX1:46;
then p0* |.h.| <= e* |.h.| by A2;
hence ||. R/.h .|| <= e* |.h.| by A1,A8;
end;
end;
hence ||. R/.h .|| <= e* |.h.|;
end;
hence thesis by A3;
end;
reserve m for non empty Element of NAT;
theorem NDIFF29:
for R be REST of REAL-NS n
for L be Lipschitzian LinearOperator of REAL-NS n,REAL-NS m holds
L*R is REST of REAL-NS m
proof
let R be REST of REAL-NS n;
let L be Lipschitzian LinearOperator of REAL-NS n,REAL-NS m;
set S=REAL-NS n;
set T=REAL-NS m;
consider K be Real such that
A1: 0 <= K and
A2: for z be Point of S holds ||.L.z.|| <= K * ||.z.|| by LOPBAN_1:def 8;
dom L = the carrier of S by FUNCT_2:def 1;
then
A3: rng R c= dom L;
A4: R is total by NDIFF_3:def 1;
then
A5: dom R = REAL by PARTFUN1:def 2;
reconsider p0=0, p1=1 as Real;
A6: p0 + K < p1 + K by XREAL_1:8;
now
let ee be Real such that
A8: ee > 0;
set e=ee/2;
e > 0 by A8,XREAL_1:215;
then
A9: 0/(1 + K) < e/(1 + K) by A1,XREAL_1:74;
set e1=e/( 1 + K );
consider d be Real such that
A10: 0 < d and
A11: for h be Real st h <> 0 & |.h.| < d holds (|.h.|"* ||.
R/.h.||) < e1 by A4,A9,NDIFF126;
A12: e < ee by A8,XREAL_1:216;
now
let h be Real such that
A13: h <> 0 and
A14: |.h.| < d;
|.h.|"* ||.(R/.h).|| < e1 by A11,A13,A14;
then ( K +1) *( |.h.|"* ||.R/.h.||) <=( K +1) *e1 by A1,XREAL_1:64;
then
A15: ( K +1) *( |.h.|"* ||.R/.h.||) <=e by A1,XCMPLX_1:87;
|.h.| <> 0 by A13,COMPLEX1:45;
then
A16: |.h.| > 0 by COMPLEX1:46;
A17: K * ||.R/.h.|| <= ( K +1) * ||.R/.h.|| by A6,XREAL_1:64;
||.L.(R/.h).|| <= K * ||.R/.h.|| by A2;
then ||.L.(R/.h).|| <= ( K +1) * ||.R/.h.|| by A17,XXREAL_0:2;
then
|.h.|"* ||.L.(R/.h).|| <= |.h.|"*(( K +1) * ||.R/.h.|| ) by A16,
XREAL_1:64;
then
A18: |.h.|"* ||.L.(R/.h).|| <= e by A15,XXREAL_0:2;
L.(R/.h) = L/.(R/.h) .=(L*R)/.h by A5,A3,PARTFUN2:5;
hence |.h.|"* ||.(L*R)/.h.|| < ee by A12,A18,XXREAL_0:2;
end;
hence ex d be Real st d > 0 & for h be Real st h <> 0 & |.h.| < d
holds |.h.|"* ||.(L*R)/.h.|| < ee by A10;
end;
hence thesis by A4,NDIFF126;
end;
theorem NDIFF211:
for R1 be REST of REAL-NS n st R1/.0=0.(REAL-NS n)
for R2 be REST of REAL-NS n,REAL-NS m st R2/.0.(REAL-NS n)=0.(REAL-NS m)
for L be LINEAR of REAL-NS n holds R2*(L+R1) is REST of REAL-NS m
proof
set S=REAL-NS n;
set T=REAL-NS m;
let R1 be REST of S;
assume R1/.0=0.S;
then consider d0 be Real such that
A1: 0 < d0 and
A2: for h be Real st |.h.| < d0 holds ||.R1/.h.|| <=1* |.h.| by NDIFF27;
let R2 be REST of REAL-NS n,REAL-NS m such that
A3: R2/.0.S=0.T;
let L be LINEAR of S;
consider r be Point of S such that
A4: for h be Real holds L.h = h*r by NDIFF_3:def 2;
set K=||.r.||;
R2 is total by NDIFF_1:def 5;
then dom R2 = the carrier of S by PARTFUN1:def 2;
then
A6: rng (L+R1) c= dom R2;
R1 is total by NDIFF_3:def 1;
then
A7: L+R1 is total by VFUNCT_1:32;
then
A8: dom(L+R1)=REAL by PARTFUN1:def 2;
A9: now
let ee be Real such that
A10: ee > 0;
set e=ee/2;
A11: e < ee by A10,XREAL_1:216;
set e1=e/(1 + K);
e > 0 by A10,XREAL_1:215;
then 0/(1 + K) < e/(1 + K) by XREAL_1:74;
then consider d be Real such that
A12: 0 < d and
A13: for z be Point of S st ||.z.|| < d holds ||.R2/.z.|| <= e1*||.z.||
by A3,NDIFF_2:7;
set d1=d/(1 + K);
set dd1=min(d0,d1);
A14: dd1 <=d1 by XXREAL_0:17;
A15: dd1 <=d0 by XXREAL_0:17;
A16: now
let h be Real such that
A17: h <> 0 and
A18: |.h.| < dd1;
|.h.| < d0 by A15,A18,XXREAL_0:2;
then
A19: ||.R1/.h.|| <=1* |.h.| by A2;
C19: L.h = h*r by A4;
reconsider p0=0 as Real;
||. L.h .|| - K * |.h.| + K * |.h.| <= p0 + K * |.h.|
by C19,NORMSP_1:def 1; then
||.L.h+R1/.h.|| <= ||.L.h.|| + ||.R1/.h.|| & ||.L.h.|| + ||.R1/.h
.|| <= K * |.h.| + 1* |.h.| by A19,NORMSP_1:def 1,XREAL_1:7;
then
A20: ||.L.h+R1/.h.|| <= ( K +1) * |.h.| by XXREAL_0:2;
|.h.| < d1 by A14,A18,XXREAL_0:2;
then (K +1) * |.h.| < (K +1) *d1 by XREAL_1:68;
then ||.L.h+R1/.h.|| < (K +1) * d1 by A20,XXREAL_0:2;
then ||.L.h+R1/.h.|| < d by XCMPLX_1:87;
then
A21: ||.R2/.(L.h+R1/.h).|| <= e1*||.L.h+R1/.h.|| by A13;
e1*||.L.h+R1/.h.|| <= e1* ((K +1) * |.h.|) by A10,A20,XREAL_1:64;
then
A22: ||.R2/.(L.h+R1/.h).|| <= e1* ((K +1) * |.h.|) by A21,XXREAL_0:2;
A23: R2/.(L.h+R1/.h) = R2/.(L/.h+R1/.h) .=R2/.((L+R1)/.h) by A8,VFUNCT_1:def 1
.=(R2*(L+R1))/.h by A8,A6,PARTFUN2:5;
A24: |.h.| <> 0 by A17,COMPLEX1:45;
then |.h.| > 0 by COMPLEX1:46;
then
|.h.|"* ||.(R2*(L+R1))/.h.|| <= |.h.|"* (e1* ( K +1) * |.h .|)
by A23,A22,XREAL_1:64;
then |.h.|"* ||.(R2*(L+R1))/.h.|| <= |.h.|*|.h.|"*e1* (K +1);
then |.h.|"* ||.(R2*(L+R1))/.h.|| <= 1*e1* (K +1) by A24,XCMPLX_0:def 7;
then |.h.|"* ||.(R2*(L+R1))/.h.|| <= e by XCMPLX_1:87;
hence |.h.|"* ||.(R2*(L+R1))/.h.|| < ee by A11,XXREAL_0:2;
end;
0/(1 + K) < d/(1 + K) by A12,XREAL_1:74;
then 0 < dd1 by A1,XXREAL_0:15;
hence ex dd1 be Real st dd1 > 0 & for h be Real st h <> 0 & |.h.|
< dd1 holds |.h.|"* ||.(R2*(L+R1))/.h.|| < ee by A16;
end;
dom (R2*(L+R1)) = dom(L+R1) by A6,RELAT_1:27
.=REAL by A7,PARTFUN1:def 2;
then R2*(L+R1) is total by PARTFUN1:def 2;
hence thesis by A9,NDIFF126;
end;
theorem NDIFF212:
for R1 be REST of REAL-NS n st R1/.0=0.(REAL-NS n)
for R2 be REST of REAL-NS n,REAL-NS m st R2/.0.(REAL-NS n)=0.(REAL-NS m)
for L1 be LINEAR of REAL-NS n
for L2 be Lipschitzian LinearOperator of REAL-NS n,REAL-NS m holds
L2*R1+ R2*(L1+R1) is REST of REAL-NS m
proof
let R1 be REST of REAL-NS n such that
A1: R1/.0=0.(REAL-NS n);
let R2 be REST of REAL-NS n,REAL-NS m such that
A2: R2/.0.(REAL-NS n)=0.(REAL-NS m);
let L1 be LINEAR of REAL-NS n;
let L2 be Lipschitzian LinearOperator of REAL-NS n,REAL-NS m;
A3: L2*R1 is REST of REAL-NS m by NDIFF29;
R2*(L1+R1) is REST of REAL-NS m by A1,A2,NDIFF211;
hence thesis by A3,NDIFF_3:7;
end;
theorem
for x0 be Element of REAL
for g be PartFunc of REAL,REAL-NS n st
g is_differentiable_in x0
for f be PartFunc of REAL-NS n,REAL-NS m st
f is_differentiable_in (g/.x0) holds
f*g is_differentiable_in x0 & diff(f*g,x0) = diff(f,g/.x0).diff(g,x0)
proof
let x0 be Element of REAL;
set S=REAL-NS n;
set T=REAL-NS m;
let g be PartFunc of REAL,S such that
A1: g is_differentiable_in x0;
consider N1 being Neighbourhood of x0 such that
A2: N1 c= dom g and
A3: ex L1 be LINEAR of S,R1 be REST of S st
diff(g,x0) = L1.1 & for x be Real st x in N1 holds
g/.x-g/.x0 = L1.(x-x0) + R1/.(x-x0) by A1,NDIFF_3:def 4;
let f be PartFunc of S,T;
assume f is_differentiable_in g/.x0;
then consider N2 being Neighbourhood of g/.x0 such that
A4: N2 c= dom f and
A5: ex R2 be REST of S,T st R2/.0.S=0.T & R2 is_continuous_in 0.S &
for y be Point of S st y in N2 holds
f/.y-f/.(g/.x0) = diff(f,g/.x0).(y-g/.x0) + R2/.(y-g/.x0) by NDIFF_1:47;
consider R2 be REST of S,T such that
A6: R2/.0.S=0.T and
A7: for y be Point of S st y in N2 holds f/.y-f/.(g/.x0) = diff(f,
g/.x0).(y-g/.x0) + R2/.(y-g/.x0) by A5;
reconsider L2 = diff(f,g/.x0) as Lipschitzian LinearOperator of S,T
by LOPBAN_1:def 9;
consider L1 be LINEAR of S,R1 be REST of S such that
A9: diff(g,x0) = L1.1 & for x be Real st x in N1 holds
g/.x-g/.x0 = L1.(x-x0) + R1/.(x-x0) by A3;
consider r be Point of S such that
B9: for p be Real holds L1.p = p*r by NDIFF_3:def 2;
reconsider p0=0 as Element of REAL;
g/.x0-g/.x0 = L1.(x0-x0) + R1/.(x0-x0) by A9,RCOMP_1:16;
then 0.S = L1.0 + R1/.0 by RLVECT_1:15;
then 0.S = p0*r + R1/.0 by B9;
then 0.S = 0.S + R1/.0 by RLVECT_1:10;
then
B10: R1/.0=0.S by RLVECT_1:4;
B11: dom(L2*L1) = REAL by FUNCT_2:def 1;
reconsider q=L2.r as Point of T;
for p be Real holds (L2*L1).p = p*q
proof
let p be Real;
L2.(L1.p) = L2.(p*r) by B9
.= p*q by LOPBAN_1:def 5;
hence thesis by B11,FUNCT_1:12;
end;
then reconsider L0=L2*L1 as LINEAR of T by NDIFF_3:def 2;
g is_continuous_in x0 by A1,NDIFF_3:22;
then consider N3 be Neighbourhood of x0 such that
A10: g.:N3 c= N2 by NFCONT_3:10;
reconsider R0=L2*R1+R2*(L1+R1) as REST of T by B10,A6,NDIFF212;
consider N be Neighbourhood of x0 such that
A11: N c= N1 and
A12: N c= N3 by RCOMP_1:17;
A13: N c= dom(f*g)
proof
let x be set;
assume
A14: x in N;
then reconsider x9 = x as Real;
A15: x in N1 by A11,A14;
then g.x9 in g.:N3 by A2,A12,A14,FUNCT_1:def 6;
then g.x9 in N2 by A10;
hence x in dom(f*g) by A2,A4,A15,FUNCT_1:11;
end;
A17: now
let x be Real such that
A18: x in N;
A19: g/.x-g/.x0 = L1.(x-x0) + R1/.(x-x0) by A9,A11,A18;
x in N1 by A11,A18;
then g.x in g.:N3 by A2,A12,A18,FUNCT_1:def 6;
then
A20: g.x in N2 by A10;
x in N1 by A11,A18;
then
A21: g/.x in N2 by A2,A20,PARTFUN1:def 6;
A23: x0 in N by RCOMP_1:16;
A24: R1 is total by NDIFF_3:def 1;
then
A25: dom R1 = REAL by PARTFUN1:def 2;
dom L2 = the carrier of S by FUNCT_2:def 1;
then
A26: rng R1 c= dom L2;
A27: dom(L2*R1) = REAL by A24,PARTFUN1:def 2;
A28: L1+R1 is total by A24,VFUNCT_1:32;
then
A29: dom(L1+R1)=REAL by PARTFUN1:def 2;
R2 is total by NDIFF_1:def 5;
then dom R2 = the carrier of S by PARTFUN1:def 2;
then
A30: rng (L1+R1) c= dom R2;
then dom (R2*(L1+R1)) = dom(L1+R1) by RELAT_1:27
.=REAL by A28,PARTFUN1:def 2; then
A31: dom (L2*R1+R2*(L1+R1)) = (REAL) /\ (REAL) by A27,VFUNCT_1:def 1
.= REAL;
A32: L2.(R1/.(x-x0)) = L2/.(R1/.(x-x0))
.=(L2*R1)/.(x-x0) by A25,A26,PARTFUN2:5;
A33: R2/.(L1.(x-x0)+R1/.(x-x0)) = R2/.(L1/.(x-x0)+R1/.(x-x0))
.=R2/.((L1+R1)/.(x-x0)) by A29,VFUNCT_1:def 1
.=(R2*(L1+R1))/.(x-x0) by A29,A30,PARTFUN2:5;
B33: (L2*L1).(x-x0) = L2.(L1.(x-x0)) by B11,FUNCT_1:12;
thus (f*g)/.x-(f*g)/.x0 =f/.(g/.x) -(f*g)/.x0 by A13,A18,PARTFUN2:3
.=f/.(g/.x) -f/.(g/.x0) by A13,A23,PARTFUN2:3
.=diff(f,g/.x0).(g/.x-g/.x0) + R2/.(g/.x-g/.x0) by A7,A21
.=L2.(L1.(x-x0)) + L2.(R1/.(x-x0)) + (R2*(L1+R1))/.(x-x0) by A19,A33,
GRCAT_1:def 8
.=L2.(L1.(x-x0)) + ((L2*R1)/.(x-x0) + (R2*(L1+R1))/.(x-x0)) by A32,
RLVECT_1:def 3
.=L0.(x-x0) + R0/.(x-x0) by B33,A31,VFUNCT_1:def 1;
end;
hence A34: f*g is_differentiable_in x0 by A13,NDIFF_3:def 3;
(L2*L1).1 = diff(f,g/.x0).diff(g,x0) by A9,B11,FUNCT_1:12;
hence thesis by A34,A13,A17,NDIFF_3:def 4;
end;
~~